Email Gateway (Aug 18 2022 at 18:29): Email Gateway (Aug 18 2022 at 18:29):From: Makarius <makarius@sketis.net>
This is indeed a bit difficult, because the induct method has accumulated
so many add-on features over time, and there are many versions of the
underlying tactics. In your example, you are using
InductTacs.induct_rules_tac, which is actually dead code in Isabelle2011 /
Isabelle2011-1, so it will require some further digging in the history to
understand why it is (still) there.
Below is my attempt to make use to the actual tactic behind the "induct"
method in 45 min ... (using Isabelle2011-1-RC2). Note that the
Isabelle/jEdit Prover IDE allows to jump to the ML source of the proof
method definition in ML by hovering with CONTROL/COMMAND overit and
clicking on the hyperlink (blue underline).
This wraps up Induct.induct_tac with some sane defaults:
ML {*
fun infer_term x ctxt =
let val (T, ctxt') = Proof_Context.inferred_param x ctxt
in (Free (x, T), ctxt') end;
fun induct_tac ctxt xss rule i =
let
val (tss, ctxt') = (fold_map o fold_map) infer_term xss ctxt;
val instss = map (map (fn inst => SOME (NONE, (inst, false)))) tss;
in Seq.map snd o Induct.induct_tac ctxt' false instss [] [] (SOME rule) [] i end;
*}
Here is the revised example:
datatype 'a T1 = A1 "'a T2" | B1
and 'a T2 = A2 "'a T1"
fun foo1 and foo2 where
"foo1 (A1 a) = foo2 a"
| "foo1 a = a"
| "foo2 (A2 b) = foo1 b"
lemma
"foo1 (a::'a T1) = B1"
"foo2 (b::'a T2) = B1"
apply (induct a and b rule: foo1_foo2.induct)
apply simp_all
done
lemma
"foo1 (a::'a T1) = B1"
"foo2 (b::'a T2) = B1"
apply (raw_tactic {* induct_tac @{context} [["a"], ["b"]] @{thms foo1_foo2.induct} 1 *})
apply simp_all
done
Makarius
Email Gateway (Aug 18 2022 at 18:34):From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
Hello all,
I'm wondering what is the right way to apply a mutual induction using a rule
generated by the function package in ML ?
From the function package documentation, I have seen the mutual goals can be
proved by stating them in parallel (as a conjunction in Pure, if I understand
well, unless Isar also comes into play) and then applying the proof method
"induct" on the induction variables with the function induction rule.
However I can't simulate this behavior in ML:
I have tried "Induct_Tacs.induct_rules_tac" in "Goal.prove" but it seems it
can't be applied to multiple goals.
I also tried to use "Induct.induct_tac" but I don't really understand how I
could use a "cases_tactic".
Do you have any hint ?
I attach an example,
Thanks in advance,
Mathieu Giorgino
Scratch.thy
Last updated: Nov 21 2024 at 12:39 UTC