Re: [isabelle] Changes in inductive tactics



On 01/07/10 14:58, Omar Montano Rivas wrote:
> 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?

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

-- 
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe





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