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))"