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.