11 ("Tools/typedef_package.ML") |
11 ("Tools/typedef_package.ML") |
12 ("Tools/typecopy_package.ML") |
12 ("Tools/typecopy_package.ML") |
13 ("Tools/typedef_codegen.ML") |
13 ("Tools/typedef_codegen.ML") |
14 begin |
14 begin |
15 |
15 |
|
16 ML {* |
|
17 structure HOL = struct val thy = theory "HOL" end; |
|
18 *} -- "belongs to theory HOL" |
|
19 |
16 locale type_definition = |
20 locale type_definition = |
17 fixes Rep and Abs and A |
21 fixes Rep and Abs and A |
18 assumes Rep: "Rep x \<in> A" |
22 assumes Rep: "Rep x \<in> A" |
19 and Rep_inverse: "Abs (Rep x) = x" |
23 and Rep_inverse: "Abs (Rep x) = x" |
20 and Abs_inverse: "y \<in> A ==> Rep (Abs y) = y" |
24 and Abs_inverse: "y \<in> A ==> Rep (Abs y) = y" |
21 -- {* This will be axiomatized for each typedef! *} |
25 -- {* This will be axiomatized for each typedef! *} |
|
26 begin |
22 |
27 |
23 lemma (in type_definition) Rep_inject: |
28 lemma Rep_inject: |
24 "(Rep x = Rep y) = (x = y)" |
29 "(Rep x = Rep y) = (x = y)" |
25 proof |
30 proof |
26 assume "Rep x = Rep y" |
31 assume "Rep x = Rep y" |
27 hence "Abs (Rep x) = Abs (Rep y)" by (simp only:) |
32 hence "Abs (Rep x) = Abs (Rep y)" by (simp only:) |
28 also have "Abs (Rep x) = x" by (rule Rep_inverse) |
33 also have "Abs (Rep x) = x" by (rule Rep_inverse) |
31 next |
36 next |
32 assume "x = y" |
37 assume "x = y" |
33 thus "Rep x = Rep y" by (simp only:) |
38 thus "Rep x = Rep y" by (simp only:) |
34 qed |
39 qed |
35 |
40 |
36 lemma (in type_definition) Abs_inject: |
41 lemma Abs_inject: |
37 assumes x: "x \<in> A" and y: "y \<in> A" |
42 assumes x: "x \<in> A" and y: "y \<in> A" |
38 shows "(Abs x = Abs y) = (x = y)" |
43 shows "(Abs x = Abs y) = (x = y)" |
39 proof |
44 proof |
40 assume "Abs x = Abs y" |
45 assume "Abs x = Abs y" |
41 hence "Rep (Abs x) = Rep (Abs y)" by (simp only:) |
46 hence "Rep (Abs x) = Rep (Abs y)" by (simp only:) |
45 next |
50 next |
46 assume "x = y" |
51 assume "x = y" |
47 thus "Abs x = Abs y" by (simp only:) |
52 thus "Abs x = Abs y" by (simp only:) |
48 qed |
53 qed |
49 |
54 |
50 lemma (in type_definition) Rep_cases [cases set]: |
55 lemma Rep_cases [cases set]: |
51 assumes y: "y \<in> A" |
56 assumes y: "y \<in> A" |
52 and hyp: "!!x. y = Rep x ==> P" |
57 and hyp: "!!x. y = Rep x ==> P" |
53 shows P |
58 shows P |
54 proof (rule hyp) |
59 proof (rule hyp) |
55 from y have "Rep (Abs y) = y" by (rule Abs_inverse) |
60 from y have "Rep (Abs y) = y" by (rule Abs_inverse) |
56 thus "y = Rep (Abs y)" .. |
61 thus "y = Rep (Abs y)" .. |
57 qed |
62 qed |
58 |
63 |
59 lemma (in type_definition) Abs_cases [cases type]: |
64 lemma Abs_cases [cases type]: |
60 assumes r: "!!y. x = Abs y ==> y \<in> A ==> P" |
65 assumes r: "!!y. x = Abs y ==> y \<in> A ==> P" |
61 shows P |
66 shows P |
62 proof (rule r) |
67 proof (rule r) |
63 have "Abs (Rep x) = x" by (rule Rep_inverse) |
68 have "Abs (Rep x) = x" by (rule Rep_inverse) |
64 thus "x = Abs (Rep x)" .. |
69 thus "x = Abs (Rep x)" .. |
65 show "Rep x \<in> A" by (rule Rep) |
70 show "Rep x \<in> A" by (rule Rep) |
66 qed |
71 qed |
67 |
72 |
68 lemma (in type_definition) Rep_induct [induct set]: |
73 lemma Rep_induct [induct set]: |
69 assumes y: "y \<in> A" |
74 assumes y: "y \<in> A" |
70 and hyp: "!!x. P (Rep x)" |
75 and hyp: "!!x. P (Rep x)" |
71 shows "P y" |
76 shows "P y" |
72 proof - |
77 proof - |
73 have "P (Rep (Abs y))" by (rule hyp) |
78 have "P (Rep (Abs y))" by (rule hyp) |
74 also from y have "Rep (Abs y) = y" by (rule Abs_inverse) |
79 also from y have "Rep (Abs y) = y" by (rule Abs_inverse) |
75 finally show "P y" . |
80 finally show "P y" . |
76 qed |
81 qed |
77 |
82 |
78 lemma (in type_definition) Abs_induct [induct type]: |
83 lemma Abs_induct [induct type]: |
79 assumes r: "!!y. y \<in> A ==> P (Abs y)" |
84 assumes r: "!!y. y \<in> A ==> P (Abs y)" |
80 shows "P x" |
85 shows "P x" |
81 proof - |
86 proof - |
82 have "Rep x \<in> A" by (rule Rep) |
87 have "Rep x \<in> A" by (rule Rep) |
83 hence "P (Abs (Rep x))" by (rule r) |
88 hence "P (Abs (Rep x))" by (rule r) |
84 also have "Abs (Rep x) = x" by (rule Rep_inverse) |
89 also have "Abs (Rep x) = x" by (rule Rep_inverse) |
85 finally show "P x" . |
90 finally show "P x" . |
86 qed |
91 qed |
|
92 |
|
93 end |
87 |
94 |
88 use "Tools/typedef_package.ML" |
95 use "Tools/typedef_package.ML" |
89 use "Tools/typecopy_package.ML" |
96 use "Tools/typecopy_package.ML" |
90 use "Tools/typedef_codegen.ML" |
97 use "Tools/typedef_codegen.ML" |
91 |
98 |