summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Tue, 07 Dec 2004 16:15:05 +0100 | |

changeset 15380 | 455cfa766dad |

parent 15379 | 830239e6eb73 |

child 15381 | 780ea4c697f2 |

proof of subst by S Merz

src/HOL/HOL.thy | file | annotate | diff | comparison | revisions |

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