5 *) |
5 *) |
6 |
6 |
7 section \<open>Type Definition Theorems\<close> |
7 section \<open>Type Definition Theorems\<close> |
8 |
8 |
9 theory Misc_Typedef |
9 theory Misc_Typedef |
10 imports Main |
10 imports Main |
11 begin |
11 begin |
12 |
12 |
13 section "More lemmas about normal type definitions" |
13 section "More lemmas about normal type definitions" |
14 |
14 |
15 lemma |
15 lemma tdD1: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Rep x \<in> A" |
16 tdD1: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Rep x \<in> A" and |
16 and tdD2: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Abs (Rep x) = x" |
17 tdD2: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Abs (Rep x) = x" and |
17 and tdD3: "type_definition Rep Abs A \<Longrightarrow> \<forall>y. y \<in> A \<longrightarrow> Rep (Abs y) = y" |
18 tdD3: "type_definition Rep Abs A \<Longrightarrow> \<forall>y. y \<in> A \<longrightarrow> Rep (Abs y) = y" |
|
19 by (auto simp: type_definition_def) |
18 by (auto simp: type_definition_def) |
20 |
19 |
21 lemma td_nat_int: |
20 lemma td_nat_int: "type_definition int nat (Collect (op \<le> 0))" |
22 "type_definition int nat (Collect (op <= 0))" |
|
23 unfolding type_definition_def by auto |
21 unfolding type_definition_def by auto |
24 |
22 |
25 context type_definition |
23 context type_definition |
26 begin |
24 begin |
27 |
25 |
28 declare Rep [iff] Rep_inverse [simp] Rep_inject [simp] |
26 declare Rep [iff] Rep_inverse [simp] Rep_inject [simp] |
29 |
27 |
30 lemma Abs_eqD: "Abs x = Abs y ==> x \<in> A ==> y \<in> A ==> x = y" |
28 lemma Abs_eqD: "Abs x = Abs y \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x = y" |
31 by (simp add: Abs_inject) |
29 by (simp add: Abs_inject) |
32 |
30 |
33 lemma Abs_inverse': |
31 lemma Abs_inverse': "r \<in> A \<Longrightarrow> Abs r = a \<Longrightarrow> Rep a = r" |
34 "r : A ==> Abs r = a ==> Rep a = r" |
|
35 by (safe elim!: Abs_inverse) |
32 by (safe elim!: Abs_inverse) |
36 |
33 |
37 lemma Rep_comp_inverse: |
34 lemma Rep_comp_inverse: "Rep \<circ> f = g \<Longrightarrow> Abs \<circ> g = f" |
38 "Rep \<circ> f = g ==> Abs \<circ> g = f" |
|
39 using Rep_inverse by auto |
35 using Rep_inverse by auto |
40 |
36 |
41 lemma Rep_eqD [elim!]: "Rep x = Rep y ==> x = y" |
37 lemma Rep_eqD [elim!]: "Rep x = Rep y \<Longrightarrow> x = y" |
42 by simp |
38 by simp |
43 |
39 |
44 lemma Rep_inverse': "Rep a = r ==> Abs r = a" |
40 lemma Rep_inverse': "Rep a = r \<Longrightarrow> Abs r = a" |
45 by (safe intro!: Rep_inverse) |
41 by (safe intro!: Rep_inverse) |
46 |
42 |
47 lemma comp_Abs_inverse: |
43 lemma comp_Abs_inverse: "f \<circ> Abs = g \<Longrightarrow> g \<circ> Rep = f" |
48 "f \<circ> Abs = g ==> g \<circ> Rep = f" |
|
49 using Rep_inverse by auto |
44 using Rep_inverse by auto |
50 |
45 |
51 lemma set_Rep: |
46 lemma set_Rep: "A = range Rep" |
52 "A = range Rep" |
|
53 proof (rule set_eqI) |
47 proof (rule set_eqI) |
54 fix x |
48 show "x \<in> A \<longleftrightarrow> x \<in> range Rep" for x |
55 show "(x \<in> A) = (x \<in> range Rep)" |
|
56 by (auto dest: Abs_inverse [of x, symmetric]) |
49 by (auto dest: Abs_inverse [of x, symmetric]) |
57 qed |
50 qed |
58 |
51 |
59 lemma set_Rep_Abs: "A = range (Rep \<circ> Abs)" |
52 lemma set_Rep_Abs: "A = range (Rep \<circ> Abs)" |
60 proof (rule set_eqI) |
53 proof (rule set_eqI) |
61 fix x |
54 show "x \<in> A \<longleftrightarrow> x \<in> range (Rep \<circ> Abs)" for x |
62 show "(x \<in> A) = (x \<in> range (Rep \<circ> Abs))" |
|
63 by (auto dest: Abs_inverse [of x, symmetric]) |
55 by (auto dest: Abs_inverse [of x, symmetric]) |
64 qed |
56 qed |
65 |
57 |
66 lemma Abs_inj_on: "inj_on Abs A" |
58 lemma Abs_inj_on: "inj_on Abs A" |
67 unfolding inj_on_def |
59 unfolding inj_on_def |
70 lemma image: "Abs ` A = UNIV" |
62 lemma image: "Abs ` A = UNIV" |
71 by (auto intro!: image_eqI) |
63 by (auto intro!: image_eqI) |
72 |
64 |
73 lemmas td_thm = type_definition_axioms |
65 lemmas td_thm = type_definition_axioms |
74 |
66 |
75 lemma fns1: |
67 lemma fns1: "Rep \<circ> fa = fr \<circ> Rep \<or> fa \<circ> Abs = Abs \<circ> fr \<Longrightarrow> Abs \<circ> fr \<circ> Rep = fa" |
76 "Rep \<circ> fa = fr \<circ> Rep | fa \<circ> Abs = Abs \<circ> fr ==> Abs \<circ> fr \<circ> Rep = fa" |
|
77 by (auto dest: Rep_comp_inverse elim: comp_Abs_inverse simp: o_assoc) |
68 by (auto dest: Rep_comp_inverse elim: comp_Abs_inverse simp: o_assoc) |
78 |
69 |
79 lemmas fns1a = disjI1 [THEN fns1] |
70 lemmas fns1a = disjI1 [THEN fns1] |
80 lemmas fns1b = disjI2 [THEN fns1] |
71 lemmas fns1b = disjI2 [THEN fns1] |
81 |
72 |
82 lemma fns4: |
73 lemma fns4: "Rep \<circ> fa \<circ> Abs = fr \<Longrightarrow> Rep \<circ> fa = fr \<circ> Rep \<and> fa \<circ> Abs = Abs \<circ> fr" |
83 "Rep \<circ> fa \<circ> Abs = fr ==> |
|
84 Rep \<circ> fa = fr \<circ> Rep & fa \<circ> Abs = Abs \<circ> fr" |
|
85 by auto |
74 by auto |
86 |
75 |
87 end |
76 end |
88 |
77 |
89 interpretation nat_int: type_definition int nat "Collect (op <= 0)" |
78 interpretation nat_int: type_definition int nat "Collect (op \<le> 0)" |
90 by (rule td_nat_int) |
79 by (rule td_nat_int) |
91 |
80 |
92 declare |
81 declare |
93 nat_int.Rep_cases [cases del] |
82 nat_int.Rep_cases [cases del] |
94 nat_int.Abs_cases [cases del] |
83 nat_int.Abs_cases [cases del] |
97 |
86 |
98 |
87 |
99 subsection "Extended form of type definition predicate" |
88 subsection "Extended form of type definition predicate" |
100 |
89 |
101 lemma td_conds: |
90 lemma td_conds: |
102 "norm \<circ> norm = norm ==> (fr \<circ> norm = norm \<circ> fr) = |
91 "norm \<circ> norm = norm \<Longrightarrow> |
103 (norm \<circ> fr \<circ> norm = fr \<circ> norm & norm \<circ> fr \<circ> norm = norm \<circ> fr)" |
92 fr \<circ> norm = norm \<circ> fr \<longleftrightarrow> norm \<circ> fr \<circ> norm = fr \<circ> norm \<and> norm \<circ> fr \<circ> norm = norm \<circ> fr" |
104 apply safe |
93 apply safe |
105 apply (simp_all add: comp_assoc) |
94 apply (simp_all add: comp_assoc) |
106 apply (simp_all add: o_assoc) |
95 apply (simp_all add: o_assoc) |
107 done |
96 done |
108 |
97 |
109 lemma fn_comm_power: |
98 lemma fn_comm_power: "fa \<circ> tr = tr \<circ> fr \<Longrightarrow> fa ^^ n \<circ> tr = tr \<circ> fr ^^ n" |
110 "fa \<circ> tr = tr \<circ> fr ==> fa ^^ n \<circ> tr = tr \<circ> fr ^^ n" |
|
111 apply (rule ext) |
99 apply (rule ext) |
112 apply (induct n) |
100 apply (induct n) |
113 apply (auto dest: fun_cong) |
101 apply (auto dest: fun_cong) |
114 done |
102 done |
115 |
103 |
120 locale td_ext = type_definition + |
108 locale td_ext = type_definition + |
121 fixes norm |
109 fixes norm |
122 assumes eq_norm: "\<And>x. Rep (Abs x) = norm x" |
110 assumes eq_norm: "\<And>x. Rep (Abs x) = norm x" |
123 begin |
111 begin |
124 |
112 |
125 lemma Abs_norm [simp]: |
113 lemma Abs_norm [simp]: "Abs (norm x) = Abs x" |
126 "Abs (norm x) = Abs x" |
|
127 using eq_norm [of x] by (auto elim: Rep_inverse') |
114 using eq_norm [of x] by (auto elim: Rep_inverse') |
128 |
115 |
129 lemma td_th: |
116 lemma td_th: "g \<circ> Abs = f \<Longrightarrow> f (Rep x) = g x" |
130 "g \<circ> Abs = f ==> f (Rep x) = g x" |
|
131 by (drule comp_Abs_inverse [symmetric]) simp |
117 by (drule comp_Abs_inverse [symmetric]) simp |
132 |
118 |
133 lemma eq_norm': "Rep \<circ> Abs = norm" |
119 lemma eq_norm': "Rep \<circ> Abs = norm" |
134 by (auto simp: eq_norm) |
120 by (auto simp: eq_norm) |
135 |
121 |
139 lemmas td = td_thm |
125 lemmas td = td_thm |
140 |
126 |
141 lemma set_iff_norm: "w : A \<longleftrightarrow> w = norm w" |
127 lemma set_iff_norm: "w : A \<longleftrightarrow> w = norm w" |
142 by (auto simp: set_Rep_Abs eq_norm' eq_norm [symmetric]) |
128 by (auto simp: set_Rep_Abs eq_norm' eq_norm [symmetric]) |
143 |
129 |
144 lemma inverse_norm: |
130 lemma inverse_norm: "Abs n = w \<longleftrightarrow> Rep w = norm n" |
145 "(Abs n = w) = (Rep w = norm n)" |
|
146 apply (rule iffI) |
131 apply (rule iffI) |
147 apply (clarsimp simp add: eq_norm) |
132 apply (clarsimp simp add: eq_norm) |
148 apply (simp add: eq_norm' [symmetric]) |
133 apply (simp add: eq_norm' [symmetric]) |
149 done |
134 done |
150 |
135 |
151 lemma norm_eq_iff: |
136 lemma norm_eq_iff: "norm x = norm y \<longleftrightarrow> Abs x = Abs y" |
152 "(norm x = norm y) = (Abs x = Abs y)" |
|
153 by (simp add: eq_norm' [symmetric]) |
137 by (simp add: eq_norm' [symmetric]) |
154 |
138 |
155 lemma norm_comps: |
139 lemma norm_comps: |
156 "Abs \<circ> norm = Abs" |
140 "Abs \<circ> norm = Abs" |
157 "norm \<circ> Rep = Rep" |
141 "norm \<circ> Rep = Rep" |
158 "norm \<circ> norm = norm" |
142 "norm \<circ> norm = norm" |
159 by (auto simp: eq_norm' [symmetric] o_def) |
143 by (auto simp: eq_norm' [symmetric] o_def) |
160 |
144 |
161 lemmas norm_norm [simp] = norm_comps |
145 lemmas norm_norm [simp] = norm_comps |
162 |
146 |
163 lemma fns5: |
147 lemma fns5: "Rep \<circ> fa \<circ> Abs = fr \<Longrightarrow> fr \<circ> norm = fr \<and> norm \<circ> fr = fr" |
164 "Rep \<circ> fa \<circ> Abs = fr ==> |
|
165 fr \<circ> norm = fr & norm \<circ> fr = fr" |
|
166 by (fold eq_norm') auto |
148 by (fold eq_norm') auto |
167 |
149 |
168 (* following give conditions for converses to td_fns1 |
150 (* following give conditions for converses to td_fns1 |
169 the condition (norm \<circ> fr \<circ> norm = fr \<circ> norm) says that |
151 the condition (norm \<circ> fr \<circ> norm = fr \<circ> norm) says that |
170 fr takes normalised arguments to normalised results, |
152 fr takes normalised arguments to normalised results, |
172 takes norm-equivalent arguments to norm-equivalent results, |
154 takes norm-equivalent arguments to norm-equivalent results, |
173 (fr \<circ> norm = fr) says that fr |
155 (fr \<circ> norm = fr) says that fr |
174 takes norm-equivalent arguments to the same result, and |
156 takes norm-equivalent arguments to the same result, and |
175 (norm \<circ> fr = fr) says that fr takes any argument to a normalised result |
157 (norm \<circ> fr = fr) says that fr takes any argument to a normalised result |
176 *) |
158 *) |
177 lemma fns2: |
159 lemma fns2: "Abs \<circ> fr \<circ> Rep = fa \<Longrightarrow> norm \<circ> fr \<circ> norm = fr \<circ> norm \<longleftrightarrow> Rep \<circ> fa = fr \<circ> Rep" |
178 "Abs \<circ> fr \<circ> Rep = fa ==> |
|
179 (norm \<circ> fr \<circ> norm = fr \<circ> norm) = (Rep \<circ> fa = fr \<circ> Rep)" |
|
180 apply (fold eq_norm') |
160 apply (fold eq_norm') |
181 apply safe |
161 apply safe |
182 prefer 2 |
162 prefer 2 |
183 apply (simp add: o_assoc) |
163 apply (simp add: o_assoc) |
184 apply (rule ext) |
164 apply (rule ext) |
185 apply (drule_tac x="Rep x" in fun_cong) |
165 apply (drule_tac x="Rep x" in fun_cong) |
186 apply auto |
166 apply auto |
187 done |
167 done |
188 |
168 |
189 lemma fns3: |
169 lemma fns3: "Abs \<circ> fr \<circ> Rep = fa \<Longrightarrow> norm \<circ> fr \<circ> norm = norm \<circ> fr \<longleftrightarrow> fa \<circ> Abs = Abs \<circ> fr" |
190 "Abs \<circ> fr \<circ> Rep = fa ==> |
|
191 (norm \<circ> fr \<circ> norm = norm \<circ> fr) = (fa \<circ> Abs = Abs \<circ> fr)" |
|
192 apply (fold eq_norm') |
170 apply (fold eq_norm') |
193 apply safe |
171 apply safe |
194 prefer 2 |
172 prefer 2 |
195 apply (simp add: comp_assoc) |
173 apply (simp add: comp_assoc) |
196 apply (rule ext) |
174 apply (rule ext) |
197 apply (drule_tac f="a \<circ> b" for a b in fun_cong) |
175 apply (drule_tac f="a \<circ> b" for a b in fun_cong) |
198 apply simp |
176 apply simp |
199 done |
177 done |
200 |
178 |
201 lemma fns: |
179 lemma fns: "fr \<circ> norm = norm \<circ> fr \<Longrightarrow> fa \<circ> Abs = Abs \<circ> fr \<longleftrightarrow> Rep \<circ> fa = fr \<circ> Rep" |
202 "fr \<circ> norm = norm \<circ> fr ==> |
|
203 (fa \<circ> Abs = Abs \<circ> fr) = (Rep \<circ> fa = fr \<circ> Rep)" |
|
204 apply safe |
180 apply safe |
205 apply (frule fns1b) |
181 apply (frule fns1b) |
206 prefer 2 |
182 prefer 2 |
207 apply (frule fns1a) |
183 apply (frule fns1a) |
208 apply (rule fns3 [THEN iffD1]) |
184 apply (rule fns3 [THEN iffD1]) |