src/HOL/Typedef.thy
 changeset 23247 b99dce43d252 parent 22846 fb79144af9a3 child 23433 c2c10abd2a1e
```     1.1 --- a/src/HOL/Typedef.thy	Tue Jun 05 12:12:25 2007 +0200
1.2 +++ b/src/HOL/Typedef.thy	Tue Jun 05 15:16:08 2007 +0200
1.3 @@ -13,14 +13,19 @@
1.4    ("Tools/typedef_codegen.ML")
1.5  begin
1.6
1.7 +ML {*
1.8 +structure HOL = struct val thy = theory "HOL" end;
1.9 +*}  -- "belongs to theory HOL"
1.10 +
1.11  locale type_definition =
1.12    fixes Rep and Abs and A
1.13    assumes Rep: "Rep x \<in> A"
1.14      and Rep_inverse: "Abs (Rep x) = x"
1.15      and Abs_inverse: "y \<in> A ==> Rep (Abs y) = y"
1.16    -- {* This will be axiomatized for each typedef! *}
1.17 +begin
1.18
1.19 -lemma (in type_definition) Rep_inject:
1.20 +lemma Rep_inject:
1.21    "(Rep x = Rep y) = (x = y)"
1.22  proof
1.23    assume "Rep x = Rep y"
1.24 @@ -33,7 +38,7 @@
1.25    thus "Rep x = Rep y" by (simp only:)
1.26  qed
1.27
1.28 -lemma (in type_definition) Abs_inject:
1.29 +lemma Abs_inject:
1.30    assumes x: "x \<in> A" and y: "y \<in> A"
1.31    shows "(Abs x = Abs y) = (x = y)"
1.32  proof
1.33 @@ -47,7 +52,7 @@
1.34    thus "Abs x = Abs y" by (simp only:)
1.35  qed
1.36
1.37 -lemma (in type_definition) Rep_cases [cases set]:
1.38 +lemma Rep_cases [cases set]:
1.39    assumes y: "y \<in> A"
1.40      and hyp: "!!x. y = Rep x ==> P"
1.41    shows P
1.42 @@ -56,7 +61,7 @@
1.43    thus "y = Rep (Abs y)" ..
1.44  qed
1.45
1.46 -lemma (in type_definition) Abs_cases [cases type]:
1.47 +lemma Abs_cases [cases type]:
1.48    assumes r: "!!y. x = Abs y ==> y \<in> A ==> P"
1.49    shows P
1.50  proof (rule r)
1.51 @@ -65,7 +70,7 @@
1.52    show "Rep x \<in> A" by (rule Rep)
1.53  qed
1.54
1.55 -lemma (in type_definition) Rep_induct [induct set]:
1.56 +lemma Rep_induct [induct set]:
1.57    assumes y: "y \<in> A"
1.58      and hyp: "!!x. P (Rep x)"
1.59    shows "P y"
1.60 @@ -75,7 +80,7 @@
1.61    finally show "P y" .
1.62  qed
1.63
1.64 -lemma (in type_definition) Abs_induct [induct type]:
1.65 +lemma Abs_induct [induct type]:
1.66    assumes r: "!!y. y \<in> A ==> P (Abs y)"
1.67    shows "P x"
1.68  proof -
1.69 @@ -85,6 +90,8 @@
1.70    finally show "P x" .
1.71  qed
1.72
1.73 +end
1.74 +
1.75  use "Tools/typedef_package.ML"
1.76  use "Tools/typecopy_package.ML"
1.77  use "Tools/typedef_codegen.ML"
```