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

author | wenzelm |

Thu, 27 Sep 2001 22:26:00 +0200 | |

changeset 11608 | c760ea8154ee |

parent 11607 | c7e1db87b98a |

child 11609 | 3f3d1add4d94 |

renamed theory "subset" to "Typedef";

src/HOL/Tools/typedef_package.ML | file | annotate | diff | comparison | revisions | |

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

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

--- a/src/HOL/Tools/typedef_package.ML Thu Sep 27 22:25:12 2001 +0200 +++ b/src/HOL/Tools/typedef_package.ML Thu Sep 27 22:26:00 2001 +0200 @@ -28,7 +28,7 @@ (** theory context references **) -val type_definitionN = "subset.type_definition"; +val type_definitionN = "Typedef.type_definition"; val type_definition_def = thm "type_definition_def"; val Rep = thm "Rep"; @@ -98,7 +98,7 @@ fun prepare_typedef prep_term no_def name (t, vs, mx) raw_set thy = let - val _ = Theory.requires thy "subset" "typedefs"; + val _ = Theory.requires thy "Typedef" "typedefs"; val sign = Theory.sign_of thy; val full = Sign.full_name sign;

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Typedef.thy Thu Sep 27 22:26:00 2001 +0200 @@ -0,0 +1,139 @@ +(* Title: HOL/Typedef.thy + ID: $Id$ + Author: Markus Wenzel, TU Munich + +Misc set-theory lemmas and HOL type definitions. +*) + +theory Typedef = Set +files "subset.ML" "equalities.ML" "mono.ML" + "Tools/induct_attrib.ML" ("Tools/typedef_package.ML"): + +(** belongs to theory Ord **) + +theorems linorder_cases [case_names less equal greater] = + linorder_less_split + +(* Courtesy of Stephan Merz *) +lemma Least_mono: + "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y + ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)" + apply clarify + apply (erule_tac P = "%x. x : S" in LeastI2) + apply fast + apply (rule LeastI2) + apply (auto elim: monoD intro!: order_antisym) + done + + +(*belongs to theory Set*) +setup Rulify.setup + + +section {* HOL type definitions *} + +constdefs + type_definition :: "('a => 'b) => ('b => 'a) => 'b set => bool" + "type_definition Rep Abs A == + (\<forall>x. Rep x \<in> A) \<and> + (\<forall>x. Abs (Rep x) = x) \<and> + (\<forall>y \<in> A. Rep (Abs y) = y)" + -- {* This will be stated as an axiom for each typedef! *} + +lemma type_definitionI [intro]: + "(!!x. Rep x \<in> A) ==> + (!!x. Abs (Rep x) = x) ==> + (!!y. y \<in> A ==> Rep (Abs y) = y) ==> + type_definition Rep Abs A" + by (unfold type_definition_def) blast + +theorem Rep: "type_definition Rep Abs A ==> Rep x \<in> A" + by (unfold type_definition_def) blast + +theorem Rep_inverse: "type_definition Rep Abs A ==> Abs (Rep x) = x" + by (unfold type_definition_def) blast + +theorem Abs_inverse: "type_definition Rep Abs A ==> y \<in> A ==> Rep (Abs y) = y" + by (unfold type_definition_def) blast + +theorem Rep_inject: "type_definition Rep Abs A ==> (Rep x = Rep y) = (x = y)" +proof - + assume tydef: "type_definition Rep Abs A" + show ?thesis + proof + assume "Rep x = Rep y" + hence "Abs (Rep x) = Abs (Rep y)" by (simp only:) + thus "x = y" by (simp only: Rep_inverse [OF tydef]) + next + assume "x = y" + thus "Rep x = Rep y" by simp + qed +qed + +theorem Abs_inject: + "type_definition Rep Abs A ==> x \<in> A ==> y \<in> A ==> (Abs x = Abs y) = (x = y)" +proof - + assume tydef: "type_definition Rep Abs A" + assume x: "x \<in> A" and y: "y \<in> A" + show ?thesis + proof + assume "Abs x = Abs y" + hence "Rep (Abs x) = Rep (Abs y)" by simp + moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse [OF tydef]) + moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef]) + ultimately show "x = y" by (simp only:) + next + assume "x = y" + thus "Abs x = Abs y" by simp + qed +qed + +theorem Rep_cases: + "type_definition Rep Abs A ==> y \<in> A ==> (!!x. y = Rep x ==> P) ==> P" +proof - + assume tydef: "type_definition Rep Abs A" + assume y: "y \<in> A" and r: "(!!x. y = Rep x ==> P)" + show P + proof (rule r) + from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef]) + thus "y = Rep (Abs y)" .. + qed +qed + +theorem Abs_cases: + "type_definition Rep Abs A ==> (!!y. x = Abs y ==> y \<in> A ==> P) ==> P" +proof - + assume tydef: "type_definition Rep Abs A" + assume r: "!!y. x = Abs y ==> y \<in> A ==> P" + show P + proof (rule r) + have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef]) + thus "x = Abs (Rep x)" .. + show "Rep x \<in> A" by (rule Rep [OF tydef]) + qed +qed + +theorem Rep_induct: + "type_definition Rep Abs A ==> y \<in> A ==> (!!x. P (Rep x)) ==> P y" +proof - + assume tydef: "type_definition Rep Abs A" + assume "!!x. P (Rep x)" hence "P (Rep (Abs y))" . + moreover assume "y \<in> A" hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef]) + ultimately show "P y" by (simp only:) +qed + +theorem Abs_induct: + "type_definition Rep Abs A ==> (!!y. y \<in> A ==> P (Abs y)) ==> P x" +proof - + assume tydef: "type_definition Rep Abs A" + assume r: "!!y. y \<in> A ==> P (Abs y)" + have "Rep x \<in> A" by (rule Rep [OF tydef]) + hence "P (Abs (Rep x))" by (rule r) + moreover have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef]) + ultimately show "P x" by (simp only:) +qed + +setup InductAttrib.setup +use "Tools/typedef_package.ML" + +end

--- a/src/HOL/subset.thy Thu Sep 27 22:25:12 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,139 +0,0 @@ -(* Title: HOL/subset.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1994 University of Cambridge - -Subset lemmas and HOL type definitions. -*) - -theory subset = Set -files "Tools/induct_attrib.ML" ("Tools/typedef_package.ML"): - -(** belongs to theory Ord **) - -theorems linorder_cases [case_names less equal greater] = - linorder_less_split - -(* Courtesy of Stephan Merz *) -lemma Least_mono: -"[| mono (f::'a::order => 'b::order); EX x:S. ALL y:S. x <= y |] - ==> (LEAST y. y : f`S) = f(LEAST x. x : S)" -apply clarify -apply (erule_tac P = "%x. x : S" in LeastI2) -apply fast -apply (rule LeastI2) -apply (auto elim: monoD intro!: order_antisym) -done - - -(*belongs to theory Set*) -setup Rulify.setup - - -section {* HOL type definitions *} - -constdefs - type_definition :: "('a => 'b) => ('b => 'a) => 'b set => bool" - "type_definition Rep Abs A == - (\\<forall>x. Rep x \\<in> A) \\<and> - (\\<forall>x. Abs (Rep x) = x) \\<and> - (\\<forall>y \\<in> A. Rep (Abs y) = y)" - -- {* This will be stated as an axiom for each typedef! *} - -lemma type_definitionI [intro]: - "(!!x. Rep x \\<in> A) ==> - (!!x. Abs (Rep x) = x) ==> - (!!y. y \\<in> A ==> Rep (Abs y) = y) ==> - type_definition Rep Abs A" - by (unfold type_definition_def) blast - -theorem Rep: "type_definition Rep Abs A ==> Rep x \\<in> A" - by (unfold type_definition_def) blast - -theorem Rep_inverse: "type_definition Rep Abs A ==> Abs (Rep x) = x" - by (unfold type_definition_def) blast - -theorem Abs_inverse: "type_definition Rep Abs A ==> y \\<in> A ==> Rep (Abs y) = y" - by (unfold type_definition_def) blast - -theorem Rep_inject: "type_definition Rep Abs A ==> (Rep x = Rep y) = (x = y)" -proof - - assume tydef: "type_definition Rep Abs A" - show ?thesis - proof - assume "Rep x = Rep y" - hence "Abs (Rep x) = Abs (Rep y)" by (simp only:) - thus "x = y" by (simp only: Rep_inverse [OF tydef]) - next - assume "x = y" - thus "Rep x = Rep y" by simp - qed -qed - -theorem Abs_inject: - "type_definition Rep Abs A ==> x \\<in> A ==> y \\<in> A ==> (Abs x = Abs y) = (x = y)" -proof - - assume tydef: "type_definition Rep Abs A" - assume x: "x \\<in> A" and y: "y \\<in> A" - show ?thesis - proof - assume "Abs x = Abs y" - hence "Rep (Abs x) = Rep (Abs y)" by simp - moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse [OF tydef]) - moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef]) - ultimately show "x = y" by (simp only:) - next - assume "x = y" - thus "Abs x = Abs y" by simp - qed -qed - -theorem Rep_cases: - "type_definition Rep Abs A ==> y \\<in> A ==> (!!x. y = Rep x ==> P) ==> P" -proof - - assume tydef: "type_definition Rep Abs A" - assume y: "y \\<in> A" and r: "(!!x. y = Rep x ==> P)" - show P - proof (rule r) - from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef]) - thus "y = Rep (Abs y)" .. - qed -qed - -theorem Abs_cases: - "type_definition Rep Abs A ==> (!!y. x = Abs y ==> y \\<in> A ==> P) ==> P" -proof - - assume tydef: "type_definition Rep Abs A" - assume r: "!!y. x = Abs y ==> y \\<in> A ==> P" - show P - proof (rule r) - have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef]) - thus "x = Abs (Rep x)" .. - show "Rep x \\<in> A" by (rule Rep [OF tydef]) - qed -qed - -theorem Rep_induct: - "type_definition Rep Abs A ==> y \\<in> A ==> (!!x. P (Rep x)) ==> P y" -proof - - assume tydef: "type_definition Rep Abs A" - assume "!!x. P (Rep x)" hence "P (Rep (Abs y))" . - moreover assume "y \\<in> A" hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef]) - ultimately show "P y" by (simp only:) -qed - -theorem Abs_induct: - "type_definition Rep Abs A ==> (!!y. y \\<in> A ==> P (Abs y)) ==> P x" -proof - - assume tydef: "type_definition Rep Abs A" - assume r: "!!y. y \\<in> A ==> P (Abs y)" - have "Rep x \\<in> A" by (rule Rep [OF tydef]) - hence "P (Abs (Rep x))" by (rule r) - moreover have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef]) - ultimately show "P x" by (simp only:) -qed - -setup InductAttrib.setup -use "Tools/typedef_package.ML" - -end