proof of subst by S Merz
authorpaulson
Tue Dec 07 16:15:05 2004 +0100 (2004-12-07)
changeset 15380455cfa766dad
parent 15379 830239e6eb73
child 15381 780ea4c697f2
proof of subst by S Merz
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Tue Dec 07 14:42:08 2004 +0100
     1.2 +++ b/src/HOL/HOL.thy	Tue Dec 07 16:15:05 2004 +0100
     1.3 @@ -121,20 +121,31 @@
     1.4  subsubsection {* Axioms and basic definitions *}
     1.5  
     1.6  axioms
     1.7 -  eq_reflection: "(x=y) ==> (x==y)"
     1.8 +  eq_reflection:  "(x=y) ==> (x==y)"
     1.9  
    1.10 -  refl:         "t = (t::'a)"
    1.11 -  subst:        "[| s = t; P(s) |] ==> P(t::'a)"
    1.12 +  refl:           "t = (t::'a)"
    1.13  
    1.14 -  ext:          "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
    1.15 -    -- {* Extensionality is built into the meta-logic, and this rule expresses *}
    1.16 -    -- {* a related property.  It is an eta-expanded version of the traditional *}
    1.17 -    -- {* rule, and similar to the ABS rule of HOL *}
    1.18 +  ext:            "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
    1.19 +    -- {*Extensionality is built into the meta-logic, and this rule expresses
    1.20 +         a related property.  It is an eta-expanded version of the traditional
    1.21 +         rule, and similar to the ABS rule of HOL*}
    1.22  
    1.23    the_eq_trivial: "(THE x. x = a) = (a::'a)"
    1.24  
    1.25 -  impI:         "(P ==> Q) ==> P-->Q"
    1.26 -  mp:           "[| P-->Q;  P |] ==> Q"
    1.27 +  impI:           "(P ==> Q) ==> P-->Q"
    1.28 +  mp:             "[| P-->Q;  P |] ==> Q"
    1.29 +
    1.30 +
    1.31 +text{*Thanks to Stephan Merz*}
    1.32 +theorem subst:
    1.33 +  assumes eq: "s = t" and p: "P(s)"
    1.34 +  shows "P(t::'a)"
    1.35 +proof -
    1.36 +  from eq have meta: "s \<equiv> t"
    1.37 +    by (rule eq_reflection)
    1.38 +  from p show ?thesis
    1.39 +    by (unfold meta)
    1.40 +qed
    1.41  
    1.42  defs
    1.43    True_def:     "True      == ((%x::bool. x) = (%x. x))"