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