Re: [isabelle] Congruence rule for Let



Andreas Lochbihler wrote:
Hi all,

using the function package, I'd like to define a function whose definition contains a number of Let expressions. In the generated induction rule, a term "Let t (%x. y)" yields the induction hypothesis "!!x. x = t ==> P (y x)" However, I would like to get "P (y t)" directly. How do I have to change the congruence rule for Let to achieve this?

Andreas,

This seems easy enough using the functions in ch 5 of the Reference Manual

val iax = "!!x. x = t ==> P (y x)" : Thm.thm
> val ax' = forall_elim_var 0 iax ;
val ax' = "?x = t ==> P (y ?x)" : Thm.thm
> refl RS ax' ;
val it = "P (y t)" : Thm.thm

Cheers,

Jeremy






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