|
1 theory Regex_ACIDZ |
|
2 imports "HOL-Library.Confluent_Quotient" |
|
3 begin |
|
4 |
|
5 datatype (discs_sels) 'a rexp = Zero | Eps | Atom 'a |
|
6 | Alt "'a rexp" "'a rexp" | Conc "'a rexp" "'a rexp" | Star "'a rexp" |
|
7 |
|
8 fun elim_zeros where |
|
9 "elim_zeros (Alt r s) = |
|
10 (let r' = elim_zeros r; s' = elim_zeros s in |
|
11 if r' = Zero then s' else if s' = Zero then r' else Alt r' s')" |
|
12 | "elim_zeros (Conc r s) = (let r' = elim_zeros r in if r' = Zero then Zero else Conc r' s)" |
|
13 | "elim_zeros r = r" |
|
14 |
|
15 fun distribute where |
|
16 "distribute t (Alt r s) = Alt (distribute t r) (distribute t s)" |
|
17 | "distribute t (Conc r s) = Conc (distribute s r) t" |
|
18 | "distribute t r = Conc r t" |
|
19 |
|
20 inductive ACIDZ (infix "~" 64) where |
|
21 a1: "Alt (Alt r s) t ~ Alt r (Alt s t)" |
|
22 | a2: "Alt r (Alt s t) ~ Alt (Alt r s) t" |
|
23 | c: "Alt r s ~ Alt s r" |
|
24 | i: "r ~ Alt r r" |
|
25 | z: "r ~ s \<Longrightarrow> r ~ elim_zeros s" |
|
26 | d: "Conc r t ~ distribute t r" |
|
27 | R: "r ~ r" |
|
28 | A: "r ~ r' \<Longrightarrow> s ~ s' \<Longrightarrow> Alt r s ~ Alt r' s'" |
|
29 | C: "r ~ r' \<Longrightarrow> Conc r s ~ Conc r' s" |
|
30 |
|
31 inductive_cases ACIDZ_AltE[elim]: "Alt r s ~ t" |
|
32 inductive_cases ACIDZ_ConcE[elim]: "Conc r s ~ t" |
|
33 inductive_cases ACIDZ_StarE[elim]: "Star r ~ t" |
|
34 |
|
35 declare ACIDZ.intros[intro] |
|
36 |
|
37 abbreviation ACIDZcl (infix "~~" 64) where "(~~) \<equiv> equivclp (~)" |
|
38 |
|
39 lemma map_rexp_distribute[simp]: "map_rexp f (distribute t r) = distribute (map_rexp f t) (map_rexp f r)" |
|
40 by (induct r arbitrary: t) auto |
|
41 |
|
42 lemma set_rexp_distribute[simp]: "set_rexp (distribute t r) = set_rexp r \<union> set_rexp t" |
|
43 by (induct r arbitrary: t) auto |
|
44 |
|
45 lemma Zero_eq_map_rexp_iff[simp]: |
|
46 "Zero = map_rexp f x \<longleftrightarrow> x = Zero" |
|
47 "map_rexp f x = Zero \<longleftrightarrow> x = Zero" |
|
48 by (cases x; auto)+ |
|
49 |
|
50 lemma Alt_eq_map_rexp_iff: |
|
51 "Alt r s = map_rexp f x \<longleftrightarrow> (\<exists>r' s'. x = Alt r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)" |
|
52 "map_rexp f x = Alt r s \<longleftrightarrow> (\<exists>r' s'. x = Alt r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)" |
|
53 by (cases x; auto)+ |
|
54 |
|
55 lemma map_rexp_elim_zeros[simp]: "map_rexp f (elim_zeros r) = elim_zeros (map_rexp f r)" |
|
56 by (induct r rule: elim_zeros.induct) (auto simp: Let_def) |
|
57 |
|
58 lemma set_rexp_elim_zeros: "set_rexp (elim_zeros r) \<subseteq> set_rexp r" |
|
59 by (induct r rule: elim_zeros.induct) (auto simp: Let_def) |
|
60 |
|
61 lemma ACIDZ_map_respects: |
|
62 fixes f :: "'a \<Rightarrow> 'b" and r s :: "'a rexp" |
|
63 assumes "r ~ s" |
|
64 shows "map_rexp f r ~ map_rexp f s" |
|
65 using assms by (induct r s rule: ACIDZ.induct) (auto simp: Let_def) |
|
66 |
|
67 lemma ACIDZcl_map_respects: |
|
68 fixes f :: "'a \<Rightarrow> 'b" and r s :: "'a rexp" |
|
69 assumes "r ~~ s" |
|
70 shows "map_rexp f r ~~ map_rexp f s" |
|
71 using assms by (induct rule: equivclp_induct) (auto intro: ACIDZ_map_respects equivclp_trans) |
|
72 |
|
73 lemma finite_set_rexp: "finite (set_rexp r)" |
|
74 by (induct r) auto |
|
75 |
|
76 lemma ACIDZ_set_rexp: "r ~ s \<Longrightarrow> set_rexp s \<subseteq> set_rexp r" |
|
77 by (induct r s rule: ACIDZ.induct) (auto dest: set_mp[OF set_rexp_elim_zeros] simp: Let_def) |
|
78 |
|
79 lemma ACIDZ_set_rexp': "(~)\<^sup>*\<^sup>* r s \<Longrightarrow> set_rexp s \<subseteq> set_rexp r" |
|
80 by (induct rule: rtranclp.induct) (auto dest: ACIDZ_set_rexp) |
|
81 |
|
82 |
|
83 lemma Conc_eq_map_rexp_iff: |
|
84 "Conc r s = map_rexp f x \<longleftrightarrow> (\<exists>r' s'. x = Conc r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)" |
|
85 "map_rexp f x = Conc r s \<longleftrightarrow> (\<exists>r' s'. x = Conc r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)" |
|
86 by (cases x; auto)+ |
|
87 |
|
88 lemma Star_eq_map_rexp_iff: |
|
89 "Star r = map_rexp f x \<longleftrightarrow> (\<exists>r'. x = Star r' \<and> map_rexp f r' = r)" |
|
90 "map_rexp f x = Star r \<longleftrightarrow> (\<exists>r'. x = Star r' \<and> map_rexp f r' = r)" |
|
91 by (cases x; auto)+ |
|
92 |
|
93 lemma AAA: "(~)\<^sup>*\<^sup>* r r' \<Longrightarrow> (~)\<^sup>*\<^sup>* s s' \<Longrightarrow> (~)\<^sup>*\<^sup>* (Alt r s) (Alt r' s')" |
|
94 proof (induct r r' rule: rtranclp.induct) |
|
95 case (rtrancl_refl r) |
|
96 then show ?case |
|
97 by (induct s s' rule: rtranclp.induct) |
|
98 (auto elim!: rtranclp.rtrancl_into_rtrancl) |
|
99 next |
|
100 case (rtrancl_into_rtrancl a b c) |
|
101 then show ?case |
|
102 by (auto elim!: rtranclp.rtrancl_into_rtrancl) |
|
103 qed |
|
104 |
|
105 lemma CCC: "(~)\<^sup>*\<^sup>* r r' \<Longrightarrow> (~)\<^sup>*\<^sup>* (Conc r s) (Conc r' s)" |
|
106 proof (induct r r' rule: rtranclp.induct) |
|
107 case (rtrancl_refl r) |
|
108 then show ?case |
|
109 by simp |
|
110 next |
|
111 case (rtrancl_into_rtrancl a b c) |
|
112 then show ?case |
|
113 by (auto elim!: rtranclp.rtrancl_into_rtrancl) |
|
114 qed |
|
115 |
|
116 lemma map_rexp_ACIDZ_inv: "map_rexp f x ~ y \<Longrightarrow> \<exists>z. (~)\<^sup>*\<^sup>* x z \<and> y = map_rexp f z" |
|
117 proof (induct "map_rexp f x" y arbitrary: x rule: ACIDZ.induct) |
|
118 case (a1 r s t) |
|
119 then obtain r' s' t' where "x = Alt (Alt r' s') t'" |
|
120 "map_rexp f r' = r" "map_rexp f s' = s" "map_rexp f t' = t" |
|
121 by (auto simp: Alt_eq_map_rexp_iff) |
|
122 then show ?case |
|
123 by (intro exI[of _ "Alt r' (Alt s' t')"]) auto |
|
124 next |
|
125 case (a2 r s t) |
|
126 then obtain r' s' t' where "x = Alt r' (Alt s' t')" |
|
127 "map_rexp f r' = r" "map_rexp f s' = s" "map_rexp f t' = t" |
|
128 by (auto simp: Alt_eq_map_rexp_iff) |
|
129 then show ?case |
|
130 by (intro exI[of _ "Alt (Alt r' s') t'"]) auto |
|
131 next |
|
132 case (c r s) |
|
133 then obtain r' s' where "x = Alt r' s'" |
|
134 "map_rexp f r' = r" "map_rexp f s' = s" |
|
135 by (auto simp: Alt_eq_map_rexp_iff) |
|
136 then show ?case |
|
137 by (intro exI[of _ "Alt s' r'"]) auto |
|
138 next |
|
139 case (i r) |
|
140 then show ?case |
|
141 by (intro exI[of _ "Alt r r"]) auto |
|
142 next |
|
143 case (z r) |
|
144 then show ?case |
|
145 by (metis ACIDZ.z R map_rexp_elim_zeros rtranclp.simps) |
|
146 next |
|
147 case (d r s) |
|
148 then obtain r' s' where "x = Conc r' s'" |
|
149 "map_rexp f r' = r" "map_rexp f s' = s" |
|
150 by (auto simp: Conc_eq_map_rexp_iff) |
|
151 then show ?case |
|
152 by (intro exI[of _ "distribute s' r'"]) auto |
|
153 next |
|
154 case (R r) |
|
155 then show ?case by (auto intro: exI[of _ r]) |
|
156 next |
|
157 case (A r rr s ss) |
|
158 then obtain r' s' where "x = Alt r' s'" |
|
159 "map_rexp f r' = r" "map_rexp f s' = s" |
|
160 by (auto simp: Alt_eq_map_rexp_iff) |
|
161 moreover from A(2)[OF this(2)[symmetric]] A(4)[OF this(3)[symmetric]] obtain rr' ss' where |
|
162 "(~)\<^sup>*\<^sup>* r' rr'" "rr = map_rexp f rr'" "(~)\<^sup>*\<^sup>* s' ss'" "ss = map_rexp f ss'" |
|
163 by blast |
|
164 ultimately show ?case using A(1,3) |
|
165 by (intro exI[of _ "Alt rr' ss'"]) (auto intro!: AAA) |
|
166 next |
|
167 case (C r rr s) |
|
168 then obtain r' s' where "x = Conc r' s'" |
|
169 "map_rexp f r' = r" "map_rexp f s' = s" |
|
170 by (auto simp: Conc_eq_map_rexp_iff) |
|
171 moreover from C(2)[OF this(2)[symmetric]] obtain rr' where |
|
172 "(~)\<^sup>*\<^sup>* r' rr'" "rr = map_rexp f rr'" |
|
173 by blast |
|
174 ultimately show ?case using C(1,3) |
|
175 by (intro exI[of _ "Conc rr' s'"]) (auto intro!: CCC) |
|
176 qed |
|
177 |
|
178 lemma reflclp_ACIDZ: "(~)\<^sup>=\<^sup>= = (~)" |
|
179 unfolding fun_eq_iff |
|
180 by auto |
|
181 |
|
182 lemma elim_zeros_distribute_Zero: "elim_zeros r = Zero \<Longrightarrow> elim_zeros (distribute t r) = Zero" |
|
183 by (induct r arbitrary: t) (auto simp: Let_def split: if_splits) |
|
184 |
|
185 lemma elim_zeros_ACIDZ_Zero: "r ~ s \<Longrightarrow> elim_zeros r = Zero \<Longrightarrow> elim_zeros s = Zero" |
|
186 by (induct r s rule: ACIDZ.induct) (auto simp: Let_def elim_zeros_distribute_Zero split: if_splits) |
|
187 |
|
188 lemma AZZ[simp]: "Alt Zero Zero ~ Zero" |
|
189 by (metis elim_zeros.simps(3) elim_zeros_ACIDZ_Zero i z) |
|
190 |
|
191 lemma elim_zeros_idem[simp]: "elim_zeros (elim_zeros r) = elim_zeros r" |
|
192 by (induct r rule: elim_zeros.induct) (auto simp: Let_def) |
|
193 |
|
194 lemma elim_zeros_distribute_idem: "elim_zeros (distribute s (elim_zeros r)) = elim_zeros (distribute s r)" |
|
195 by (induct r arbitrary: s rule: elim_zeros.induct) (auto simp: Let_def) |
|
196 |
|
197 lemma zz: "r ~ s \<Longrightarrow> t = elim_zeros s \<Longrightarrow> r ~ t" |
|
198 by (metis z) |
|
199 |
|
200 lemma elim_zeros_ACIDZ1: "r ~ s \<Longrightarrow> elim_zeros r ~ elim_zeros s" |
|
201 proof (induct r s rule: ACIDZ.induct) |
|
202 case (c r s) |
|
203 then show ?case by (auto simp: Let_def) |
|
204 next |
|
205 case (d r t) |
|
206 then show ?case |
|
207 by (smt (z3) ACIDZ.d R distribute.simps(3) elim_zeros.simps(2) elim_zeros.simps(3) elim_zeros_distribute_idem z) |
|
208 next |
|
209 case (A r r' s s') |
|
210 then show ?case |
|
211 by (auto 0 2 simp: Let_def dest: elim_zeros_ACIDZ_Zero elim: zz[OF ACIDZ.A]) |
|
212 next |
|
213 case (C r r' s) |
|
214 then show ?case |
|
215 by (smt (z3) ACIDZ.C elim_zeros.simps(2,3) z elim_zeros_ACIDZ_Zero) |
|
216 qed (auto simp: Let_def) |
|
217 |
|
218 lemma AA': "r ~ r' \<Longrightarrow> s ~ s' \<Longrightarrow> t = elim_zeros (Alt r' s') \<Longrightarrow> Alt r s ~ t" |
|
219 by (auto simp del: elim_zeros.simps) |
|
220 |
|
221 lemma distribute_ACIDZ1: "r ~ r' \<Longrightarrow> distribute s r ~ elim_zeros (distribute s r')" |
|
222 proof (induct r r' arbitrary: s rule: ACIDZ.induct) |
|
223 case (A r r' s s' u) |
|
224 from A(2,4)[of u] show ?case |
|
225 by (auto simp: Let_def elim: zz[OF ACIDZ.A]) |
|
226 next |
|
227 case (C r r' s) |
|
228 then show ?case |
|
229 by (smt (verit, best) ACIDZ.C distribute.simps(2,3) elim_zeros.simps(2,3) z) |
|
230 qed (auto simp del: elim_zeros.simps simp: elim_zeros_distribute_idem) |
|
231 |
|
232 lemma elim_zeros_ACIDZ: "r ~ s \<Longrightarrow> (~)\<^sup>*\<^sup>* (elim_zeros r) (elim_zeros s)" |
|
233 using elim_zeros_ACIDZ1 by blast |
|
234 |
|
235 lemma elim_zeros_ACIDZ_rtranclp: "(~)\<^sup>*\<^sup>* r s \<Longrightarrow> (~)\<^sup>*\<^sup>* (elim_zeros r) (elim_zeros s)" |
|
236 by (induct rule: rtranclp_induct) (auto elim!: rtranclp_trans elim_zeros_ACIDZ) |
|
237 |
|
238 lemma distribute_ACIDZ: "(~) r r' \<Longrightarrow> (~)\<^sup>*\<^sup>* (distribute s r) (elim_zeros (distribute s r'))" |
|
239 by (metis distribute_ACIDZ1 rtranclp.simps) |
|
240 |
|
241 lemma ACIDZ_elim_zeros: "(~) r s \<Longrightarrow> elim_zeros r = Zero \<Longrightarrow> elim_zeros s = Zero" |
|
242 by (meson elim_zeros_ACIDZ1 elim_zeros_ACIDZ_Zero) |
|
243 |
|
244 lemma ACIDZ_elim_zeros_rtranclp: |
|
245 "(~)\<^sup>*\<^sup>* r s \<Longrightarrow> elim_zeros r = Zero \<Longrightarrow> elim_zeros s = Zero" |
|
246 by (induct rule: rtranclp_induct) (auto elim: ACIDZ_elim_zeros) |
|
247 |
|
248 lemma Alt_elim_zeros[simp]: |
|
249 "Alt (elim_zeros r) s ~ elim_zeros (Alt r s)" |
|
250 "Alt r (elim_zeros s) ~ elim_zeros (Alt r s)" |
|
251 by (smt (verit, ccfv_threshold) ACIDZ.simps elim_zeros.simps(1) elim_zeros_idem)+ |
|
252 |
|
253 lemma strong_confluentp_ACIDZ: "strong_confluentp (~)" |
|
254 proof (rule strong_confluentpI, unfold reflclp_ACIDZ) |
|
255 fix x y z :: "'a rexp" |
|
256 assume "x ~ y" "x ~ z" |
|
257 then show "\<exists>u. (~)\<^sup>*\<^sup>* y u \<and> z ~ u" |
|
258 proof (induct x y arbitrary: z rule: ACIDZ.induct) |
|
259 case (a1 r s t) |
|
260 then show ?case |
|
261 by (auto intro: AAA converse_rtranclp_into_rtranclp) |
|
262 next |
|
263 case (a2 r s t) |
|
264 then show ?case |
|
265 by (auto intro: AAA converse_rtranclp_into_rtranclp) |
|
266 next |
|
267 case (c r s) |
|
268 then show ?case |
|
269 by (cases rule: ACIDZ.cases) |
|
270 (auto 0 4 intro: exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ R], rotated] |
|
271 converse_rtranclp_into_rtranclp[where r="(~)", OF ACIDZ.c]) |
|
272 next |
|
273 case (i r) |
|
274 then show ?case |
|
275 by (auto intro: AAA) |
|
276 next |
|
277 case (z r s) |
|
278 then show ?case |
|
279 by (meson ACIDZ.z elim_zeros_ACIDZ_rtranclp) |
|
280 next |
|
281 case (d r s t) |
|
282 then show ?case |
|
283 by (induct "Conc r s" t rule: ACIDZ.induct) |
|
284 (force intro: exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ z], rotated] |
|
285 exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ z[OF elim_zeros_ACIDZ1]], rotated] |
|
286 distribute_ACIDZ1 elim!: rtranclp_trans)+ |
|
287 next |
|
288 case (R r) |
|
289 then show ?case |
|
290 by auto |
|
291 next |
|
292 note A1 = ACIDZ.A[OF _ R] |
|
293 note A2 = ACIDZ.A[OF R] |
|
294 case (A r r' s s') |
|
295 from A(5,1-4) show ?case |
|
296 proof (induct "Alt r s" z rule: ACIDZ.induct) |
|
297 case inner: (a1 r'' s'') |
|
298 from A(1,3) show ?case |
|
299 unfolding inner.hyps[symmetric] |
|
300 proof (induct "Alt r'' s''" r' rule: ACIDZ.induct[consumes 1, case_names Xa1 Xa2 Xc Xi Xz Xd XR XA XC]) |
|
301 case Xa1 |
|
302 with A(3) show ?case |
|
303 by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A2[OF A2]], rotated]) |
|
304 (metis A1 a1 a2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) |
|
305 next |
|
306 case Xa2 |
|
307 then show ?case |
|
308 by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A2[OF A2]], rotated]) |
|
309 (metis a1 A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) |
|
310 next |
|
311 case Xc |
|
312 then show ?case |
|
313 by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A2[OF A2]], rotated]) |
|
314 (metis a1 c A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) |
|
315 next |
|
316 case Xi |
|
317 then show ?case |
|
318 apply (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ ACIDZ.A[OF i ACIDZ.A[OF i]]], rotated]) |
|
319 apply (rule converse_rtranclp_into_rtranclp, rule a1) |
|
320 apply (rule converse_rtranclp_into_rtranclp, rule a1) |
|
321 apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) |
|
322 apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A1, rule c) |
|
323 apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1) |
|
324 apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1) |
|
325 apply (rule converse_rtranclp_into_rtranclp, rule a2) |
|
326 apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) |
|
327 apply blast |
|
328 done |
|
329 next |
|
330 case Xz |
|
331 with A show ?case |
|
332 by (auto elim!: exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ z], rotated] |
|
333 converse_rtranclp_into_rtranclp[rotated, OF elim_zeros_ACIDZ_rtranclp] |
|
334 simp del: elim_zeros.simps) |
|
335 qed auto |
|
336 next |
|
337 case inner: (a2 s'' t'') |
|
338 from A(3,1) show ?case |
|
339 unfolding inner.hyps[symmetric] |
|
340 proof (induct "Alt s'' t''" s' rule: ACIDZ.induct[consumes 1, case_names Xa1 Xa2 Xc Xi Xz Xd XR XA XC]) |
|
341 case Xa1 |
|
342 with A(3) show ?case |
|
343 by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A1[OF A1]], rotated]) |
|
344 (metis a2 A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) |
|
345 next |
|
346 case Xa2 |
|
347 then show ?case |
|
348 by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A1[OF A1]], rotated]) |
|
349 (metis a1 a2 A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) |
|
350 next |
|
351 case Xc |
|
352 then show ?case |
|
353 by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A1[OF A1]], rotated]) |
|
354 (metis a2 c A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) |
|
355 next |
|
356 case Xi |
|
357 then show ?case |
|
358 apply (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ ACIDZ.A[OF ACIDZ.A[OF _ i] i]], rotated]) |
|
359 apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) |
|
360 apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A1, rule c) |
|
361 apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1) |
|
362 apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A2, rule a1) |
|
363 apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) |
|
364 apply (rule converse_rtranclp_into_rtranclp, rule a2) |
|
365 apply blast |
|
366 done |
|
367 next |
|
368 case Xz |
|
369 then show ?case |
|
370 by (auto elim!: exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ z], rotated] |
|
371 converse_rtranclp_into_rtranclp[rotated, OF elim_zeros_ACIDZ_rtranclp] |
|
372 simp del: elim_zeros.simps) |
|
373 qed auto |
|
374 next |
|
375 case (z rs) with A show ?case |
|
376 by (auto elim!: rtranclp_trans |
|
377 intro!: exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ elim_zeros_ACIDZ1], rotated]) |
|
378 qed (auto 5 0 intro: AAA) |
|
379 next |
|
380 case (C r r' s s') |
|
381 from C(3,1-2) show ?case |
|
382 by (induct "Conc r s" s' rule: ACIDZ.induct) |
|
383 (auto intro: CCC elim!: rtranclp_trans |
|
384 exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ elim_zeros_ACIDZ1], rotated] |
|
385 exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ distribute_ACIDZ1], rotated]) |
|
386 qed |
|
387 qed |
|
388 |
|
389 lemma confluent_quotient_ACIDZ: |
|
390 "confluent_quotient (~) (~~) (~~) (~~) (~~) (~~) |
|
391 (map_rexp fst) (map_rexp snd) (map_rexp fst) (map_rexp snd) |
|
392 rel_rexp rel_rexp rel_rexp set_rexp set_rexp" |
|
393 by unfold_locales |
|
394 (auto 4 4 dest: ACIDZ_set_rexp' simp: rexp.in_rel rexp.rel_compp dest: map_rexp_ACIDZ_inv intro: rtranclp_into_equivclp |
|
395 intro: equivpI reflpI sympI transpI ACIDZcl_map_respects |
|
396 strong_confluentp_imp_confluentp[OF strong_confluentp_ACIDZ]) |
|
397 |
|
398 lemma wide_intersection_finite_ACIDZ: "wide_intersection_finite (~~) map_rexp set_rexp" |
|
399 by unfold_locales |
|
400 (auto intro: ACIDZcl_map_respects rexp.map_cong simp: rexp.map_id rexp.set_map finite_set_rexp) |
|
401 |
|
402 inductive ACIDZEQ (infix "\<approx>" 64) where |
|
403 a: "Alt (Alt r s) t \<approx> Alt r (Alt s t)" |
|
404 | c: "Alt r s \<approx> Alt s r" |
|
405 | i: "Alt r r \<approx> r" |
|
406 | cz: "Conc Zero r \<approx> Zero" |
|
407 | az: "Alt Zero r \<approx> r" |
|
408 | d: "Conc (Alt r s) t \<approx> Alt (Conc r t) (Conc s t)" |
|
409 | A: "r \<approx> r' \<Longrightarrow> s \<approx> s' \<Longrightarrow> Alt r s \<approx> Alt r' s'" |
|
410 | C: "r \<approx> r' \<Longrightarrow> Conc r s \<approx> Conc r' s" |
|
411 | r: "r \<approx> r" |
|
412 | s: "r \<approx> s \<Longrightarrow> s \<approx> r" |
|
413 | t: "r \<approx> s \<Longrightarrow> s \<approx> t \<Longrightarrow> r \<approx> t" |
|
414 |
|
415 context begin |
|
416 |
|
417 private lemma AA: "r ~~ r' \<Longrightarrow> s ~~ s' \<Longrightarrow> Alt r s ~~ Alt r' s'" |
|
418 proof (induct rule: equivclp_induct) |
|
419 case base |
|
420 then show ?case |
|
421 by (induct rule: equivclp_induct) (auto elim!: equivclp_trans) |
|
422 next |
|
423 case (step s t) |
|
424 then show ?case |
|
425 by (auto elim!: equivclp_trans) |
|
426 qed |
|
427 |
|
428 private lemma CC: "r ~~ r' \<Longrightarrow> Conc r s ~~ Conc r' s" |
|
429 proof (induct rule: equivclp_induct) |
|
430 case base |
|
431 then show ?case |
|
432 by simp |
|
433 next |
|
434 case (step s t) |
|
435 then show ?case |
|
436 by (auto elim!: equivclp_trans) |
|
437 qed |
|
438 |
|
439 private lemma CZ: "Conc Zero r ~~ Zero" |
|
440 by (smt (z3) R elim_zeros.simps(2) elim_zeros.simps(3) r_into_equivclp z) |
|
441 |
|
442 private lemma AZ: "Alt Zero r ~~ r" |
|
443 by (smt (verit, ccfv_threshold) converse_r_into_equivclp converse_rtranclp_into_rtranclp |
|
444 elim_zeros.simps(1) elim_zeros.simps(3) equivclp_def symclpI1 z R) |
|
445 |
|
446 private lemma D: "Conc (Alt r s) t ~~ Alt (Conc r t) (Conc s t)" |
|
447 by (smt (verit, ccfv_threshold) AA ACIDZ.d converse_r_into_equivclp distribute.simps(1) |
|
448 equivclp_sym rtranclp.simps rtranclp_equivclp) |
|
449 |
|
450 lemma ACIDZEQ_le_ACIDZcl: "r \<approx> s \<Longrightarrow> r ~~ s" |
|
451 by (induct r s rule: ACIDZEQ.induct) (auto intro: AA CC AZ CZ D equivclp_sym equivclp_trans) |
|
452 |
|
453 end |
|
454 |
|
455 lemma ACIDZEQ_z[simp]: "r \<approx> elim_zeros r" |
|
456 by (induct r rule: elim_zeros.induct) (auto 0 3 intro: ACIDZEQ.intros simp: Let_def) |
|
457 |
|
458 lemma ACIDZEQ_d[simp]: "Conc r s \<approx> distribute s r" |
|
459 by (induct s r rule: distribute.induct) (auto 0 3 intro: ACIDZEQ.intros) |
|
460 |
|
461 lemma ACIDZ_le_ACIDZEQ: "r ~ s \<Longrightarrow> r \<approx> s" |
|
462 by (induct r s rule: ACIDZ.induct) (auto 0 2 intro: ACIDZEQ.intros simp: Let_def) |
|
463 |
|
464 lemma ACIDZcl_le_ACIDZEQ: "r ~~ s \<Longrightarrow> r \<approx> s" |
|
465 by (induct rule: equivclp_induct) (auto 0 3 intro: ACIDZEQ.intros ACIDZ_le_ACIDZEQ) |
|
466 |
|
467 lemma ACIDZEQ_alt: "(\<approx>) = (~~)" |
|
468 by (simp add: ACIDZEQ_le_ACIDZcl ACIDZcl_le_ACIDZEQ antisym predicate2I) |
|
469 |
|
470 quotient_type 'a rexp_ACIDZ = "'a rexp" / "(\<approx>)" |
|
471 unfolding ACIDZEQ_alt by (auto intro!: equivpI reflpI sympI transpI) |
|
472 |
|
473 lift_bnf 'a rexp_ACIDZ |
|
474 unfolding ACIDZEQ_alt |
|
475 subgoal for A Q by (rule confluent_quotient.subdistributivity[OF confluent_quotient_ACIDZ]) |
|
476 subgoal for Ss by (elim wide_intersection_finite.wide_intersection[OF wide_intersection_finite_ACIDZ]) |
|
477 done |
|
478 |
|
479 datatype ldl = Prop string | And ldl ldl | Not ldl | Match "ldl rexp_ACIDZ" |
|
480 |
|
481 end |