proof of subst by S Merz
authorpaulson
Tue Dec 07 11:31:14 2004 +0100 (2004-12-07)
changeset 153773d99eea28a9b
parent 15376 302ef111b621
child 15378 b1c5add0a65e
proof of subst by S Merz
src/FOL/IFOL.thy
     1.1 --- a/src/FOL/IFOL.thy	Mon Dec 06 14:14:03 2004 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Tue Dec 07 11:31:14 2004 +0100
     1.3 @@ -82,7 +82,6 @@
     1.4    (* Equality *)
     1.5  
     1.6    refl:         "a=a"
     1.7 -  subst:        "[| a=b;  P(a) |] ==> P(b)"
     1.8  
     1.9    (* Propositional logic *)
    1.10  
    1.11 @@ -113,6 +112,18 @@
    1.12    iff_reflection: "(P<->Q) ==> (P==Q)"
    1.13  
    1.14  
    1.15 +text{*Thanks to Stephan Merz*}
    1.16 +theorem subst:
    1.17 +  assumes eq: "a = b" and p: "P(a)"
    1.18 +  shows "P(b)"
    1.19 +proof -
    1.20 +  from eq have meta: "a \<equiv> b"
    1.21 +    by (rule eq_reflection)
    1.22 +  from p show ?thesis
    1.23 +    by (unfold meta)
    1.24 +qed
    1.25 +
    1.26 +
    1.27  defs
    1.28    (* Definitions *)
    1.29