renamed theory "subset" to "Typedef";
authorwenzelm
Thu Sep 27 22:26:00 2001 +0200 (2001-09-27)
changeset 11608c760ea8154ee
parent 11607 c7e1db87b98a
child 11609 3f3d1add4d94
renamed theory "subset" to "Typedef";
src/HOL/Tools/typedef_package.ML
src/HOL/Typedef.thy
src/HOL/subset.thy
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Thu Sep 27 22:25:12 2001 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Thu Sep 27 22:26:00 2001 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4  
     1.5  (** theory context references **)
     1.6  
     1.7 -val type_definitionN = "subset.type_definition";
     1.8 +val type_definitionN = "Typedef.type_definition";
     1.9  val type_definition_def = thm "type_definition_def";
    1.10  
    1.11  val Rep = thm "Rep";
    1.12 @@ -98,7 +98,7 @@
    1.13  
    1.14  fun prepare_typedef prep_term no_def name (t, vs, mx) raw_set thy =
    1.15    let
    1.16 -    val _ = Theory.requires thy "subset" "typedefs";
    1.17 +    val _ = Theory.requires thy "Typedef" "typedefs";
    1.18      val sign = Theory.sign_of thy;
    1.19      val full = Sign.full_name sign;
    1.20  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Typedef.thy	Thu Sep 27 22:26:00 2001 +0200
     2.3 @@ -0,0 +1,139 @@
     2.4 +(*  Title:      HOL/Typedef.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Markus Wenzel, TU Munich
     2.7 +
     2.8 +Misc set-theory lemmas and HOL type definitions.
     2.9 +*)
    2.10 +
    2.11 +theory Typedef = Set
    2.12 +files "subset.ML" "equalities.ML" "mono.ML"
    2.13 +  "Tools/induct_attrib.ML" ("Tools/typedef_package.ML"):
    2.14 +
    2.15 +(** belongs to theory Ord **)
    2.16 +  
    2.17 +theorems linorder_cases [case_names less equal greater] =
    2.18 +  linorder_less_split
    2.19 +
    2.20 +(* Courtesy of Stephan Merz *)
    2.21 +lemma Least_mono: 
    2.22 +  "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
    2.23 +    ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
    2.24 +  apply clarify
    2.25 +  apply (erule_tac P = "%x. x : S" in LeastI2)
    2.26 +   apply fast
    2.27 +  apply (rule LeastI2)
    2.28 +  apply (auto elim: monoD intro!: order_antisym)
    2.29 +  done
    2.30 +
    2.31 +
    2.32 +(*belongs to theory Set*)
    2.33 +setup Rulify.setup
    2.34 +
    2.35 +
    2.36 +section {* HOL type definitions *}
    2.37 +
    2.38 +constdefs
    2.39 +  type_definition :: "('a => 'b) => ('b => 'a) => 'b set => bool"
    2.40 +  "type_definition Rep Abs A ==
    2.41 +    (\<forall>x. Rep x \<in> A) \<and>
    2.42 +    (\<forall>x. Abs (Rep x) = x) \<and>
    2.43 +    (\<forall>y \<in> A. Rep (Abs y) = y)"
    2.44 +  -- {* This will be stated as an axiom for each typedef! *}
    2.45 +
    2.46 +lemma type_definitionI [intro]:
    2.47 +  "(!!x. Rep x \<in> A) ==>
    2.48 +    (!!x. Abs (Rep x) = x) ==>
    2.49 +    (!!y. y \<in> A ==> Rep (Abs y) = y) ==>
    2.50 +    type_definition Rep Abs A"
    2.51 +  by (unfold type_definition_def) blast
    2.52 +
    2.53 +theorem Rep: "type_definition Rep Abs A ==> Rep x \<in> A"
    2.54 +  by (unfold type_definition_def) blast
    2.55 +
    2.56 +theorem Rep_inverse: "type_definition Rep Abs A ==> Abs (Rep x) = x"
    2.57 +  by (unfold type_definition_def) blast
    2.58 +
    2.59 +theorem Abs_inverse: "type_definition Rep Abs A ==> y \<in> A ==> Rep (Abs y) = y"
    2.60 +  by (unfold type_definition_def) blast
    2.61 +
    2.62 +theorem Rep_inject: "type_definition Rep Abs A ==> (Rep x = Rep y) = (x = y)"
    2.63 +proof -
    2.64 +  assume tydef: "type_definition Rep Abs A"
    2.65 +  show ?thesis
    2.66 +  proof
    2.67 +    assume "Rep x = Rep y"
    2.68 +    hence "Abs (Rep x) = Abs (Rep y)" by (simp only:)
    2.69 +    thus "x = y" by (simp only: Rep_inverse [OF tydef])
    2.70 +  next
    2.71 +    assume "x = y"
    2.72 +    thus "Rep x = Rep y" by simp
    2.73 +  qed
    2.74 +qed
    2.75 +
    2.76 +theorem Abs_inject:
    2.77 +  "type_definition Rep Abs A ==> x \<in> A ==> y \<in> A ==> (Abs x = Abs y) = (x = y)"
    2.78 +proof -
    2.79 +  assume tydef: "type_definition Rep Abs A"
    2.80 +  assume x: "x \<in> A" and y: "y \<in> A"
    2.81 +  show ?thesis
    2.82 +  proof
    2.83 +    assume "Abs x = Abs y"
    2.84 +    hence "Rep (Abs x) = Rep (Abs y)" by simp
    2.85 +    moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse [OF tydef])
    2.86 +    moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
    2.87 +    ultimately show "x = y" by (simp only:)
    2.88 +  next
    2.89 +    assume "x = y"
    2.90 +    thus "Abs x = Abs y" by simp
    2.91 +  qed
    2.92 +qed
    2.93 +
    2.94 +theorem Rep_cases:
    2.95 +  "type_definition Rep Abs A ==> y \<in> A ==> (!!x. y = Rep x ==> P) ==> P"
    2.96 +proof -
    2.97 +  assume tydef: "type_definition Rep Abs A"
    2.98 +  assume y: "y \<in> A" and r: "(!!x. y = Rep x ==> P)"
    2.99 +  show P
   2.100 +  proof (rule r)
   2.101 +    from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
   2.102 +    thus "y = Rep (Abs y)" ..
   2.103 +  qed
   2.104 +qed
   2.105 +
   2.106 +theorem Abs_cases:
   2.107 +  "type_definition Rep Abs A ==> (!!y. x = Abs y ==> y \<in> A ==> P) ==> P"
   2.108 +proof -
   2.109 +  assume tydef: "type_definition Rep Abs A"
   2.110 +  assume r: "!!y. x = Abs y ==> y \<in> A ==> P"
   2.111 +  show P
   2.112 +  proof (rule r)
   2.113 +    have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])
   2.114 +    thus "x = Abs (Rep x)" ..
   2.115 +    show "Rep x \<in> A" by (rule Rep [OF tydef])
   2.116 +  qed
   2.117 +qed
   2.118 +
   2.119 +theorem Rep_induct:
   2.120 +  "type_definition Rep Abs A ==> y \<in> A ==> (!!x. P (Rep x)) ==> P y"
   2.121 +proof -
   2.122 +  assume tydef: "type_definition Rep Abs A"
   2.123 +  assume "!!x. P (Rep x)" hence "P (Rep (Abs y))" .
   2.124 +  moreover assume "y \<in> A" hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
   2.125 +  ultimately show "P y" by (simp only:)
   2.126 +qed
   2.127 +
   2.128 +theorem Abs_induct:
   2.129 +  "type_definition Rep Abs A ==> (!!y. y \<in> A ==> P (Abs y)) ==> P x"
   2.130 +proof -
   2.131 +  assume tydef: "type_definition Rep Abs A"
   2.132 +  assume r: "!!y. y \<in> A ==> P (Abs y)"
   2.133 +  have "Rep x \<in> A" by (rule Rep [OF tydef])
   2.134 +  hence "P (Abs (Rep x))" by (rule r)
   2.135 +  moreover have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])
   2.136 +  ultimately show "P x" by (simp only:)
   2.137 +qed
   2.138 +
   2.139 +setup InductAttrib.setup
   2.140 +use "Tools/typedef_package.ML"
   2.141 +
   2.142 +end
     3.1 --- a/src/HOL/subset.thy	Thu Sep 27 22:25:12 2001 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,139 +0,0 @@
     3.4 -(*  Title:      HOL/subset.thy
     3.5 -    ID:         $Id$
     3.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 -    Copyright   1994  University of Cambridge
     3.8 -
     3.9 -Subset lemmas and HOL type definitions.
    3.10 -*)
    3.11 -
    3.12 -theory subset = Set
    3.13 -files "Tools/induct_attrib.ML" ("Tools/typedef_package.ML"):
    3.14 -
    3.15 -(** belongs to theory Ord **)
    3.16 -  
    3.17 -theorems linorder_cases [case_names less equal greater] =
    3.18 -  linorder_less_split
    3.19 -
    3.20 -(* Courtesy of Stephan Merz *)
    3.21 -lemma Least_mono: 
    3.22 -"[| mono (f::'a::order => 'b::order); EX x:S. ALL y:S. x <= y |]  
    3.23 -   ==> (LEAST y. y : f`S) = f(LEAST x. x : S)"
    3.24 -apply clarify
    3.25 -apply (erule_tac P = "%x. x : S" in LeastI2)
    3.26 -apply  fast
    3.27 -apply (rule LeastI2)
    3.28 -apply (auto elim: monoD intro!: order_antisym)
    3.29 -done
    3.30 -
    3.31 -
    3.32 -(*belongs to theory Set*)
    3.33 -setup Rulify.setup
    3.34 -
    3.35 -
    3.36 -section {* HOL type definitions *}
    3.37 -
    3.38 -constdefs
    3.39 -  type_definition :: "('a => 'b) => ('b => 'a) => 'b set => bool"
    3.40 -  "type_definition Rep Abs A ==
    3.41 -    (\\<forall>x. Rep x \\<in> A) \\<and>
    3.42 -    (\\<forall>x. Abs (Rep x) = x) \\<and>
    3.43 -    (\\<forall>y \\<in> A. Rep (Abs y) = y)"
    3.44 -  -- {* This will be stated as an axiom for each typedef! *}
    3.45 -
    3.46 -lemma type_definitionI [intro]:
    3.47 -  "(!!x. Rep x \\<in> A) ==>
    3.48 -    (!!x. Abs (Rep x) = x) ==>
    3.49 -    (!!y. y \\<in> A ==> Rep (Abs y) = y) ==>
    3.50 -    type_definition Rep Abs A"
    3.51 -  by (unfold type_definition_def) blast
    3.52 -
    3.53 -theorem Rep: "type_definition Rep Abs A ==> Rep x \\<in> A"
    3.54 -  by (unfold type_definition_def) blast
    3.55 -
    3.56 -theorem Rep_inverse: "type_definition Rep Abs A ==> Abs (Rep x) = x"
    3.57 -  by (unfold type_definition_def) blast
    3.58 -
    3.59 -theorem Abs_inverse: "type_definition Rep Abs A ==> y \\<in> A ==> Rep (Abs y) = y"
    3.60 -  by (unfold type_definition_def) blast
    3.61 -
    3.62 -theorem Rep_inject: "type_definition Rep Abs A ==> (Rep x = Rep y) = (x = y)"
    3.63 -proof -
    3.64 -  assume tydef: "type_definition Rep Abs A"
    3.65 -  show ?thesis
    3.66 -  proof
    3.67 -    assume "Rep x = Rep y"
    3.68 -    hence "Abs (Rep x) = Abs (Rep y)" by (simp only:)
    3.69 -    thus "x = y" by (simp only: Rep_inverse [OF tydef])
    3.70 -  next
    3.71 -    assume "x = y"
    3.72 -    thus "Rep x = Rep y" by simp
    3.73 -  qed
    3.74 -qed
    3.75 -
    3.76 -theorem Abs_inject:
    3.77 -  "type_definition Rep Abs A ==> x \\<in> A ==> y \\<in> A ==> (Abs x = Abs y) = (x = y)"
    3.78 -proof -
    3.79 -  assume tydef: "type_definition Rep Abs A"
    3.80 -  assume x: "x \\<in> A" and y: "y \\<in> A"
    3.81 -  show ?thesis
    3.82 -  proof
    3.83 -    assume "Abs x = Abs y"
    3.84 -    hence "Rep (Abs x) = Rep (Abs y)" by simp
    3.85 -    moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse [OF tydef])
    3.86 -    moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
    3.87 -    ultimately show "x = y" by (simp only:)
    3.88 -  next
    3.89 -    assume "x = y"
    3.90 -    thus "Abs x = Abs y" by simp
    3.91 -  qed
    3.92 -qed
    3.93 -
    3.94 -theorem Rep_cases:
    3.95 -  "type_definition Rep Abs A ==> y \\<in> A ==> (!!x. y = Rep x ==> P) ==> P"
    3.96 -proof -
    3.97 -  assume tydef: "type_definition Rep Abs A"
    3.98 -  assume y: "y \\<in> A" and r: "(!!x. y = Rep x ==> P)"
    3.99 -  show P
   3.100 -  proof (rule r)
   3.101 -    from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
   3.102 -    thus "y = Rep (Abs y)" ..
   3.103 -  qed
   3.104 -qed
   3.105 -
   3.106 -theorem Abs_cases:
   3.107 -  "type_definition Rep Abs A ==> (!!y. x = Abs y ==> y \\<in> A ==> P) ==> P"
   3.108 -proof -
   3.109 -  assume tydef: "type_definition Rep Abs A"
   3.110 -  assume r: "!!y. x = Abs y ==> y \\<in> A ==> P"
   3.111 -  show P
   3.112 -  proof (rule r)
   3.113 -    have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])
   3.114 -    thus "x = Abs (Rep x)" ..
   3.115 -    show "Rep x \\<in> A" by (rule Rep [OF tydef])
   3.116 -  qed
   3.117 -qed
   3.118 -
   3.119 -theorem Rep_induct:
   3.120 -  "type_definition Rep Abs A ==> y \\<in> A ==> (!!x. P (Rep x)) ==> P y"
   3.121 -proof -
   3.122 -  assume tydef: "type_definition Rep Abs A"
   3.123 -  assume "!!x. P (Rep x)" hence "P (Rep (Abs y))" .
   3.124 -  moreover assume "y \\<in> A" hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
   3.125 -  ultimately show "P y" by (simp only:)
   3.126 -qed
   3.127 -
   3.128 -theorem Abs_induct:
   3.129 -  "type_definition Rep Abs A ==> (!!y. y \\<in> A ==> P (Abs y)) ==> P x"
   3.130 -proof -
   3.131 -  assume tydef: "type_definition Rep Abs A"
   3.132 -  assume r: "!!y. y \\<in> A ==> P (Abs y)"
   3.133 -  have "Rep x \\<in> A" by (rule Rep [OF tydef])
   3.134 -  hence "P (Abs (Rep x))" by (rule r)
   3.135 -  moreover have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])
   3.136 -  ultimately show "P x" by (simp only:)
   3.137 -qed
   3.138 -
   3.139 -setup InductAttrib.setup
   3.140 -use "Tools/typedef_package.ML"
   3.141 -
   3.142 -end