Email Gateway (Aug 18 2022 at 12:33): Email Gateway (Aug 18 2022 at 12:33):From: Mattias Ulbrich <mulbrich@ira.uka.de>
Hello everyone,
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':
----------8<-------------
(* Problem with mutual induction *)
theory foobar
imports Main
begin
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?
Thank you very much for an answer!
Kind regards
Mattias
Email Gateway (Aug 18 2022 at 12:33):From: Makarius <makarius@sketis.net>
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
Last updated: May 03 2024 at 04:19 UTC