# Re: [isabelle] Mutual induction in ML

On Sun, 2 Oct 2011, Mathieu Giorgino wrote:

`I'm wondering what is the right way to apply a mutual induction using a
``rule generated by the function package in ML ?
`

`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

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*