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"