# HG changeset patch
# User paulson
# Date 1102432505 -3600
# Node ID 455cfa766dad456661f6959c7c1fd192d424451b
# Parent  830239e6eb73aa59afc97ff1efdae6d89b84106e
proof of subst by S Merz

diff -r 830239e6eb73 -r 455cfa766dad src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Dec 07 14:42:08 2004 +0100
+++ b/src/HOL/HOL.thy	Tue Dec 07 16:15:05 2004 +0100
@@ -121,20 +121,31 @@
 subsubsection {* Axioms and basic definitions *}
 
 axioms
-  eq_reflection: "(x=y) ==> (x==y)"
+  eq_reflection:  "(x=y) ==> (x==y)"
 
-  refl:         "t = (t::'a)"
-  subst:        "[| s = t; P(s) |] ==> P(t::'a)"
+  refl:           "t = (t::'a)"
 
-  ext:          "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
-    -- {* Extensionality is built into the meta-logic, and this rule expresses *}
-    -- {* a related property.  It is an eta-expanded version of the traditional *}
-    -- {* rule, and similar to the ABS rule of HOL *}
+  ext:            "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
+    -- {*Extensionality is built into the meta-logic, and this rule expresses
+         a related property.  It is an eta-expanded version of the traditional
+         rule, and similar to the ABS rule of HOL*}
 
   the_eq_trivial: "(THE x. x = a) = (a::'a)"
 
-  impI:         "(P ==> Q) ==> P-->Q"
-  mp:           "[| P-->Q;  P |] ==> Q"
+  impI:           "(P ==> Q) ==> P-->Q"
+  mp:             "[| P-->Q;  P |] ==> Q"
+
+
+text{*Thanks to Stephan Merz*}
+theorem subst:
+  assumes eq: "s = t" and p: "P(s)"
+  shows "P(t::'a)"
+proof -
+  from eq have meta: "s \<equiv> t"
+    by (rule eq_reflection)
+  from p show ?thesis
+    by (unfold meta)
+qed
 
 defs
   True_def:     "True      == ((%x::bool. x) = (%x. x))"