Re: [isabelle] Congruence rule for Let

 On 09/08/2010 06:02 PM, Alexander Krauss wrote:

Jeremy Dawson wrote:
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
The ind.hyp. Andreas is referring to appears nested inside the induction rule, where it cannot be easily manipulated by hand...


Yes, I see. How deeply is it nested ? If it is simply a hypothesis to the theorem, rather than being nested more deeply, could you get what you need in this way ?

val th = "(!!x. x = t ==> ?P (?y x)) ==> ?Q" : Thm.thm
> val th' = rule_by_tactic (hyp_subst_tac 1) th ;
val th' = "(!!x. ?P (?y t)) ==> ?Q" : Thm.thm


