[isabelle] Mutual induction in ML



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

Attachment: Scratch.thy
Description: application/isabelle-theory



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