src/HOL/Typedef.thy
 author krauss Fri Nov 24 13:44:51 2006 +0100 (2006-11-24) changeset 21512 3786eb1b69d6 parent 20426 9ffea7a8b31c child 22846 fb79144af9a3 permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
1 (*  Title:      HOL/Typedef.thy
2     ID:         \$Id\$
3     Author:     Markus Wenzel, TU Munich
4 *)
6 header {* HOL type definitions *}
8 theory Typedef
9 imports Set
10 uses
11   ("Tools/typedef_package.ML")
12   ("Tools/typecopy_package.ML")
13   ("Tools/typedef_codegen.ML")
14 begin
16 locale type_definition =
17   fixes Rep and Abs and A
18   assumes Rep: "Rep x \<in> A"
19     and Rep_inverse: "Abs (Rep x) = x"
20     and Abs_inverse: "y \<in> A ==> Rep (Abs y) = y"
21   -- {* This will be axiomatized for each typedef! *}
23 lemma (in type_definition) Rep_inject:
24   "(Rep x = Rep y) = (x = y)"
25 proof
26   assume "Rep x = Rep y"
27   hence "Abs (Rep x) = Abs (Rep y)" by (simp only:)
28   also have "Abs (Rep x) = x" by (rule Rep_inverse)
29   also have "Abs (Rep y) = y" by (rule Rep_inverse)
30   finally show "x = y" .
31 next
32   assume "x = y"
33   thus "Rep x = Rep y" by (simp only:)
34 qed
36 lemma (in type_definition) Abs_inject:
37   assumes x: "x \<in> A" and y: "y \<in> A"
38   shows "(Abs x = Abs y) = (x = y)"
39 proof
40   assume "Abs x = Abs y"
41   hence "Rep (Abs x) = Rep (Abs y)" by (simp only:)
42   also from x have "Rep (Abs x) = x" by (rule Abs_inverse)
43   also from y have "Rep (Abs y) = y" by (rule Abs_inverse)
44   finally show "x = y" .
45 next
46   assume "x = y"
47   thus "Abs x = Abs y" by (simp only:)
48 qed
50 lemma (in type_definition) Rep_cases [cases set]:
51   assumes y: "y \<in> A"
52     and hyp: "!!x. y = Rep x ==> P"
53   shows P
54 proof (rule hyp)
55   from y have "Rep (Abs y) = y" by (rule Abs_inverse)
56   thus "y = Rep (Abs y)" ..
57 qed
59 lemma (in type_definition) Abs_cases [cases type]:
60   assumes r: "!!y. x = Abs y ==> y \<in> A ==> P"
61   shows P
62 proof (rule r)
63   have "Abs (Rep x) = x" by (rule Rep_inverse)
64   thus "x = Abs (Rep x)" ..
65   show "Rep x \<in> A" by (rule Rep)
66 qed
68 lemma (in type_definition) Rep_induct [induct set]:
69   assumes y: "y \<in> A"
70     and hyp: "!!x. P (Rep x)"
71   shows "P y"
72 proof -
73   have "P (Rep (Abs y))" by (rule hyp)
74   also from y have "Rep (Abs y) = y" by (rule Abs_inverse)
75   finally show "P y" .
76 qed
78 lemma (in type_definition) Abs_induct [induct type]:
79   assumes r: "!!y. y \<in> A ==> P (Abs y)"
80   shows "P x"
81 proof -
82   have "Rep x \<in> A" by (rule Rep)
83   hence "P (Abs (Rep x))" by (rule r)
84   also have "Abs (Rep x) = x" by (rule Rep_inverse)
85   finally show "P x" .
86 qed
88 use "Tools/typedef_package.ML"
89 use "Tools/typecopy_package.ML"
90 use "Tools/typedef_codegen.ML"
92 setup {*
93   TypedefPackage.setup
94   #> TypecopyPackage.setup
95   #> TypedefCodegen.setup
96 *}
98 end