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)