subst is a proper axiom again
authorhaftmann
Fri Oct 24 17:48:33 2008 +0200 (2008-10-24)
changeset 28681e8664643f543
parent 28680 f1c76cf10915
child 28682 5de9fc98ad96
subst is a proper axiom again
src/FOL/IFOL.thy
     1.1 --- a/src/FOL/IFOL.thy	Fri Oct 24 10:41:15 2008 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Fri Oct 24 17:48:33 2008 +0200
     1.3 @@ -101,6 +101,7 @@
     1.4    (* Equality *)
     1.5  
     1.6    refl:         "a=a"
     1.7 +  subst:        "a=b \<Longrightarrow> P(a) \<Longrightarrow> P(b)"
     1.8  
     1.9    (* Propositional logic *)
    1.10  
    1.11 @@ -125,7 +126,10 @@
    1.12    exI:          "P(x) ==> (EX x. P(x))"
    1.13    exE:          "[| EX x. P(x);  !!x. P(x) ==> R |] ==> R"
    1.14  
    1.15 -  (* Reflection *)
    1.16 +
    1.17 +axioms
    1.18 +
    1.19 +  (* Reflection, admissible *)
    1.20  
    1.21    eq_reflection:  "(x=y)   ==> (x==y)"
    1.22    iff_reflection: "(P<->Q) ==> (P==Q)"
    1.23 @@ -134,18 +138,6 @@
    1.24  lemmas strip = impI allI
    1.25  
    1.26  
    1.27 -text{*Thanks to Stephan Merz*}
    1.28 -theorem subst:
    1.29 -  assumes eq: "a = b" and p: "P(a)"
    1.30 -  shows "P(b)"
    1.31 -proof -
    1.32 -  from eq have meta: "a \<equiv> b"
    1.33 -    by (rule eq_reflection)
    1.34 -  from p show ?thesis
    1.35 -    by (unfold meta)
    1.36 -qed
    1.37 -
    1.38 -
    1.39  defs
    1.40    (* Definitions *)
    1.41