Email Gateway (Aug 18 2022 at 15:42): Email Gateway (Aug 18 2022 at 15:42):From: Omar Montano Rivas <O.Montano-Rivas-2@sms.ed.ac.uk>
Hi,
I have noticed that the Isabelle function 'Induct.induct_tac' has changed its signature from
val induct_tac: Proof.context -> (binding option * term) option list list ->
(string * typ) list list -> term option list -> thm list option ->
thm list -> int -> cases_tactic
to
val induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
(string * typ) list list -> term option list -> thm list option ->
thm list -> int -> cases_tactic
in the new Isabelle release 2009-2. However, I could not tell from the source code what are the bool on the second argument and the bools paired to the terms on the third argument.
Does anybody know how they are used?
Best regards,
Omar.
Email Gateway (Aug 18 2022 at 15:45):From: Stefan Berghofer <berghofe@in.tum.de>
Hi Omar,
the induction and case analysis tactics now pre-simplify the cases using
injectivity and distinctness theorems for datatypes. The second argument
of type bool indicates whether or not the cases should be pre-simplified
("true" means that pre-simplification is switched on, "false" means that
induct_tac should behave like in the old version). The bools in the list
(binding option * (term * bool)) option list list
are used to control the treatment of instantiations of induction rules.
In Isabelle 2009-2, "induct t" (where t is not a variable) is now
treated as a shorthand for "induct x==t". If this effect is not intended,
the corresponding bools in the list have to be set to true.
Greetings,
Stefan
Last updated: Nov 21 2024 at 12:39 UTC