author haftmann Fri Oct 24 17:48:33 2008 +0200 (2008-10-24) changeset 28681 e8664643f543 parent 28680 f1c76cf10915 child 28682 5de9fc98ad96
subst is a proper axiom again
 src/FOL/IFOL.thy file | annotate | diff | revisions
```     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
```