Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Changes in inductive tactics


view this post on Zulip 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.

view this post on Zulip 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: Mar 28 2024 at 16:17 UTC