Re: [isabelle] Problem with mutual induction



On Tue, 21 Oct 2008, Mattias Ulbrich wrote:

> I experienced problems with a HOL formalisation written for an older 
> version of Isabelle. It successfully makes use of several mutual 
> inductions but I cannot redo these proofs in Isabelle2008.
> 
> The problem boils down to the observation that a mutual induction can 
> only be performed if a proof obligation has at least two 'parts':


> datatype foo = Foo bar | Empty
>   and bar = Bar foo
> 
> (* this works: thesis has two parts *)
> lemma 
>   shows "P (f::foo) (b::bar)"
>   and True
> apply (induct b and f)
> sorry
> 
> (* this does NOT work: Error message
> *** empty result sequence -- proof command failed
> *** At command "apply".
> *)
> lemma
>   shows "P (f::foo) (b::bar)"
> apply (induct b and f)
> sorry
> 
> ----------8<-------------
> 
> Is this behaviour intended? Shouldn't be the induction also possible in 
> the second case?

Yes, the "induct" method merely assembles given induction rules in a 
certain way (that is occasionally hard to analyse when things go wrong) 
expecting that the goal structure matches the basic rule outline. Writing 
(induct b and f) refers to the simultaneous rule of the corresponding 
simultaneous type.

Maybe src/HOL/Induct/Common_Patterns.thy helps to get a practical grip on 
how things work.  There are further sophistications of induct in the 
pipeline, and there might also be some kind of interactive proof scheme 
synthesis coming at some later stage.

Since "projected inductions" where some predicates are always True are a 
common case, the packages that produce induction rules could do a bit 
better in providing these additional version: foo.induct and bar.induct 
where one part of the full foo_bar.inducts is already instantiated with 
True.

If you have a dire need for such rules you may also produce them yourself 
for your specific definitions.  The "induct" method will accept them when 
specified with "rule: ..." for example.


	Makarius






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