Horrible Monsters

Here we talk about some nasty monsters in IsaPlanner and how we plan to hunt them down.

Interactive monster ate my wave-rule

Rippling behaves differently when called from synthesis and interactivly! We first run synthesis to get a bunch of theorems about @, map and rev:

print_depth 30; use "synthesis/synth_prf_tools.ML"; use "synthesis/constInfo.ML"; use "synthesis/synthesise.ML"; use_thy "dbg/SynthL2"; val thy = theory "SynthL2";

(* Make the initial constant-information*)

val (cs, thy2) = ConstInfo.mk_const_infos_ac thy;

(* Run synthesis, get a new theory with a bunch of new wave-rules: *)

val ((cs2,thy3),(conjs,thrms)) = Synthesis.synth_w_stats 10 2 thy2 cs;

At this point, note that we could not prove the conjecture "rev(rev a @ b) = rev b @ a".

Now try and run the proof interactively, using the latest variant of the theory:

val rippling = RippleLemCalc.induct_ripple_lemcalc; val myrst = PPInterface.ipp thry (rippling "g") ("g", "rev(rev a @ b) = rev b @ a");

Ok, this doesn't work either. The last wave-rule to be considered is the associativity of @ (which we have synthesised), then we get a weak fertilisation and fail to prove the calculated lemma.

Now, run synthesis again, using the constant info and theory that came from the previous run:

val ((cs3,thy4),(conjs,thrms)) = Synthesis.synth_w_stats 10 2 thy3 cs2;

Behold! The above theorem CAN be proved, by using another synthesised theorem as a wave-rule: "rev x @ y = rev y @ rev x". But why isn't this available when we try to run it interactively??? I've checked and the rule is in the wave-rule database, but it's for some reason not considered applicable from the reasoning state resulting from the interactive proof attempt.

Did a monster eat my wave-rule?

Other things to do

• Make nice interface to counter-example checking
• Allow given set of assumptions to make goal theorems that include them.
• Fix tactic application when we have all assumptions.
• Add goal names to tracer output for techn
• check dthm_unnamed_exp when using fun package and declaring wave rules.
• Fix handling of case/if statements: only break them open if they are in the WF.
• Fix reading in of terms with meta-vars already in proof plan (by unifying types?/extra stuff in parsing)
• Improve renaming of params
• Make wrule attr work for all kinds of wrules.
• Use subst zipper to identify rewrite's effect on embedding
• Finish writing subsumption library.
• Counter-example check lemmas being made in lemma calc.

• (50% of life size)

• http://homepage3.nifty.com/petspets/pede/pho/pic/mutilans10_y.JPG