src/HOL/Typedef.thy
changeset 13412 666137b488a4
parent 12023 d982f98e0f0d
child 13421 8fcdf4a26468
     1.1 --- a/src/HOL/Typedef.thy	Wed Jul 24 00:09:44 2002 +0200
     1.2 +++ b/src/HOL/Typedef.thy	Wed Jul 24 00:10:52 2002 +0200
     1.3 @@ -8,105 +8,79 @@
     1.4  theory Typedef = Set
     1.5  files ("Tools/typedef_package.ML"):
     1.6  
     1.7 -constdefs
     1.8 -  type_definition :: "('a => 'b) => ('b => 'a) => 'b set => bool"
     1.9 -  "type_definition Rep Abs A ==
    1.10 -    (\<forall>x. Rep x \<in> A) \<and>
    1.11 -    (\<forall>x. Abs (Rep x) = x) \<and>
    1.12 -    (\<forall>y \<in> A. Rep (Abs y) = y)"
    1.13 -  -- {* This will be stated as an axiom for each typedef! *}
    1.14 +locale type_definition =
    1.15 +  fixes Rep and Abs and A
    1.16 +  assumes Rep: "Rep x \<in> A"
    1.17 +    and Rep_inverse: "Abs (Rep x) = x"
    1.18 +    and Abs_inverse: "y \<in> A ==> Rep (Abs y) = y"
    1.19 +  -- {* This will be axiomatized for each typedef! *}
    1.20  
    1.21 -lemma type_definitionI [intro]:
    1.22 -  "(!!x. Rep x \<in> A) ==>
    1.23 -    (!!x. Abs (Rep x) = x) ==>
    1.24 -    (!!y. y \<in> A ==> Rep (Abs y) = y) ==>
    1.25 -    type_definition Rep Abs A"
    1.26 -  by (unfold type_definition_def) blast
    1.27 -
    1.28 -theorem Rep: "type_definition Rep Abs A ==> Rep x \<in> A"
    1.29 -  by (unfold type_definition_def) blast
    1.30 +lemmas type_definitionI [intro] =
    1.31 +  type_definition.intro [OF type_definition_axioms.intro]
    1.32  
    1.33 -theorem Rep_inverse: "type_definition Rep Abs A ==> Abs (Rep x) = x"
    1.34 -  by (unfold type_definition_def) blast
    1.35 -
    1.36 -theorem Abs_inverse: "type_definition Rep Abs A ==> y \<in> A ==> Rep (Abs y) = y"
    1.37 -  by (unfold type_definition_def) blast
    1.38 +lemma (in type_definition) Rep_inject:
    1.39 +  "(Rep x = Rep y) = (x = y)"
    1.40 +proof
    1.41 +  assume "Rep x = Rep y"
    1.42 +  hence "Abs (Rep x) = Abs (Rep y)" by (simp only:)
    1.43 +  also have "Abs (Rep x) = x" by (rule Rep_inverse)
    1.44 +  also have "Abs (Rep y) = y" by (rule Rep_inverse)
    1.45 +  finally show "x = y" .
    1.46 +next
    1.47 +  assume "x = y"
    1.48 +  thus "Rep x = Rep y" by (simp only:)
    1.49 +qed
    1.50  
    1.51 -theorem Rep_inject: "type_definition Rep Abs A ==> (Rep x = Rep y) = (x = y)"
    1.52 -proof -
    1.53 -  assume tydef: "type_definition Rep Abs A"
    1.54 -  show ?thesis
    1.55 -  proof
    1.56 -    assume "Rep x = Rep y"
    1.57 -    hence "Abs (Rep x) = Abs (Rep y)" by (simp only:)
    1.58 -    thus "x = y" by (simp only: Rep_inverse [OF tydef])
    1.59 -  next
    1.60 -    assume "x = y"
    1.61 -    thus "Rep x = Rep y" by simp
    1.62 -  qed
    1.63 +lemma (in type_definition) Abs_inject:
    1.64 +  assumes x: "x \<in> A" and y: "y \<in> A"
    1.65 +  shows "(Abs x = Abs y) = (x = y)"
    1.66 +proof
    1.67 +  assume "Abs x = Abs y"
    1.68 +  hence "Rep (Abs x) = Rep (Abs y)" by (simp only:)
    1.69 +  also from x have "Rep (Abs x) = x" by (rule Abs_inverse)
    1.70 +  also from y have "Rep (Abs y) = y" by (rule Abs_inverse)
    1.71 +  finally show "x = y" .
    1.72 +next
    1.73 +  assume "x = y"
    1.74 +  thus "Abs x = Abs y" by (simp only:)
    1.75  qed
    1.76  
    1.77 -theorem Abs_inject:
    1.78 -  "type_definition Rep Abs A ==> x \<in> A ==> y \<in> A ==> (Abs x = Abs y) = (x = y)"
    1.79 -proof -
    1.80 -  assume tydef: "type_definition Rep Abs A"
    1.81 -  assume x: "x \<in> A" and y: "y \<in> A"
    1.82 -  show ?thesis
    1.83 -  proof
    1.84 -    assume "Abs x = Abs y"
    1.85 -    hence "Rep (Abs x) = Rep (Abs y)" by simp
    1.86 -    moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse [OF tydef])
    1.87 -    moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
    1.88 -    ultimately show "x = y" by (simp only:)
    1.89 -  next
    1.90 -    assume "x = y"
    1.91 -    thus "Abs x = Abs y" by simp
    1.92 -  qed
    1.93 +lemma (in type_definition) Rep_cases [cases set]:
    1.94 +  assumes y: "y \<in> A"
    1.95 +    and hyp: "!!x. y = Rep x ==> P"
    1.96 +  shows P
    1.97 +proof (rule hyp)
    1.98 +  from y have "Rep (Abs y) = y" by (rule Abs_inverse)
    1.99 +  thus "y = Rep (Abs y)" ..
   1.100  qed
   1.101  
   1.102 -theorem Rep_cases:
   1.103 -  "type_definition Rep Abs A ==> y \<in> A ==> (!!x. y = Rep x ==> P) ==> P"
   1.104 -proof -
   1.105 -  assume tydef: "type_definition Rep Abs A"
   1.106 -  assume y: "y \<in> A" and r: "(!!x. y = Rep x ==> P)"
   1.107 -  show P
   1.108 -  proof (rule r)
   1.109 -    from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
   1.110 -    thus "y = Rep (Abs y)" ..
   1.111 -  qed
   1.112 +lemma (in type_definition) Abs_cases [cases type]:
   1.113 +  assumes r: "!!y. x = Abs y ==> y \<in> A ==> P"
   1.114 +  shows P
   1.115 +proof (rule r)
   1.116 +  have "Abs (Rep x) = x" by (rule Rep_inverse)
   1.117 +  thus "x = Abs (Rep x)" ..
   1.118 +  show "Rep x \<in> A" by (rule Rep)
   1.119  qed
   1.120  
   1.121 -theorem Abs_cases:
   1.122 -  "type_definition Rep Abs A ==> (!!y. x = Abs y ==> y \<in> A ==> P) ==> P"
   1.123 +lemma (in type_definition) Rep_induct [induct set]:
   1.124 +  assumes y: "y \<in> A"
   1.125 +    and hyp: "!!x. P (Rep x)"
   1.126 +  shows "P y"
   1.127  proof -
   1.128 -  assume tydef: "type_definition Rep Abs A"
   1.129 -  assume r: "!!y. x = Abs y ==> y \<in> A ==> P"
   1.130 -  show P
   1.131 -  proof (rule r)
   1.132 -    have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])
   1.133 -    thus "x = Abs (Rep x)" ..
   1.134 -    show "Rep x \<in> A" by (rule Rep [OF tydef])
   1.135 -  qed
   1.136 +  have "P (Rep (Abs y))" by (rule hyp)
   1.137 +  also from y have "Rep (Abs y) = y" by (rule Abs_inverse)
   1.138 +  finally show "P y" .
   1.139  qed
   1.140  
   1.141 -theorem Rep_induct:
   1.142 -  "type_definition Rep Abs A ==> y \<in> A ==> (!!x. P (Rep x)) ==> P y"
   1.143 +lemma (in type_definition) Abs_induct [induct type]:
   1.144 +  assumes r: "!!y. y \<in> A ==> P (Abs y)"
   1.145 +  shows "P x"
   1.146  proof -
   1.147 -  assume tydef: "type_definition Rep Abs A"
   1.148 -  assume "!!x. P (Rep x)" hence "P (Rep (Abs y))" .
   1.149 -  moreover assume "y \<in> A" hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
   1.150 -  ultimately show "P y" by (simp only:)
   1.151 -qed
   1.152 -
   1.153 -theorem Abs_induct:
   1.154 -  "type_definition Rep Abs A ==> (!!y. y \<in> A ==> P (Abs y)) ==> P x"
   1.155 -proof -
   1.156 -  assume tydef: "type_definition Rep Abs A"
   1.157 -  assume r: "!!y. y \<in> A ==> P (Abs y)"
   1.158 -  have "Rep x \<in> A" by (rule Rep [OF tydef])
   1.159 +  have "Rep x \<in> A" by (rule Rep)
   1.160    hence "P (Abs (Rep x))" by (rule r)
   1.161 -  moreover have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])
   1.162 -  ultimately show "P x" by (simp only:)
   1.163 +  also have "Abs (Rep x) = x" by (rule Rep_inverse)
   1.164 +  finally show "P x" .
   1.165  qed
   1.166  
   1.167  use "Tools/typedef_package.ML"