|
1 theory Free_Idempotent_Monoid imports |
|
2 "HOL-Library.Confluent_Quotient" |
|
3 begin |
|
4 |
|
5 inductive cancel1 :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
|
6 where cancel1: "xs \<noteq> [] \<Longrightarrow> cancel1 (gs @ xs @ xs @ gs') (gs @ xs @ gs')" |
|
7 |
|
8 abbreviation cancel where "cancel \<equiv> cancel1\<^sup>*\<^sup>*" |
|
9 |
|
10 lemma cancel1_append_same1: |
|
11 assumes "cancel1 xs ys" |
|
12 shows "cancel1 (zs @ xs) (zs @ ys)" |
|
13 using assms |
|
14 proof cases |
|
15 case (cancel1 ys gs gs') |
|
16 from \<open>ys \<noteq> []\<close> have "cancel1 ((zs @ gs) @ ys @ ys @ gs') ((zs @ gs) @ ys @ gs')" .. |
|
17 with cancel1 show ?thesis by simp |
|
18 qed |
|
19 |
|
20 lemma cancel_append_same1: "cancel (zs @ xs) (zs @ ys)" if "cancel xs ys" |
|
21 using that by induction(blast intro: rtranclp.rtrancl_into_rtrancl cancel1_append_same1)+ |
|
22 |
|
23 lemma cancel1_append_same2: "cancel1 xs ys \<Longrightarrow> cancel1 (xs @ zs) (ys @ zs)" |
|
24 by(cases rule: cancel1.cases)(auto intro: cancel1.intros) |
|
25 |
|
26 lemma cancel_append_same2: "cancel (xs @ zs) (ys @ zs)" if "cancel xs ys" |
|
27 using that by induction(blast intro: rtranclp.rtrancl_into_rtrancl cancel1_append_same2)+ |
|
28 |
|
29 lemma cancel1_same: |
|
30 assumes "xs \<noteq> []" |
|
31 shows "cancel1 (xs @ xs) xs" |
|
32 proof - |
|
33 have "cancel1 ([] @ xs @ xs @ []) ([] @ xs @ [])" using assms .. |
|
34 thus ?thesis by simp |
|
35 qed |
|
36 |
|
37 lemma cancel_same: "cancel (xs @ xs) xs" |
|
38 by(cases "xs = []")(auto intro: cancel1_same) |
|
39 |
|
40 abbreviation (input) eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
|
41 where "eq \<equiv> equivclp cancel1" |
|
42 |
|
43 lemma eq_sym: "eq x y \<Longrightarrow> eq y x" |
|
44 by(rule equivclp_sym) |
|
45 |
|
46 lemma equivp_eq: "equivp eq" by simp |
|
47 |
|
48 lemma eq_append_same1: "eq xs' ys' \<Longrightarrow> eq (xs @ xs') (xs @ ys')" |
|
49 by(induction rule: equivclp_induct)(auto intro: cancel1_append_same1 equivclp_into_equivclp) |
|
50 |
|
51 lemma append_eq_cong: "\<lbrakk>eq xs ys; eq xs' ys'\<rbrakk> \<Longrightarrow> eq (xs @ xs') (ys @ ys')" |
|
52 by(induction rule: equivclp_induct)(auto intro: eq_append_same1 equivclp_into_equivclp cancel1_append_same2) |
|
53 |
|
54 |
|
55 quotient_type 'a fim = "'a list" / eq by simp |
|
56 |
|
57 instantiation fim :: (type) monoid_add begin |
|
58 lift_definition zero_fim :: "'a fim" is "[]" . |
|
59 lift_definition plus_fim :: "'a fim \<Rightarrow> 'a fim \<Rightarrow> 'a fim" is "(@)" by(rule append_eq_cong) |
|
60 instance by(intro_classes; transfer; simp) |
|
61 end |
|
62 |
|
63 lemma plus_idem_fim [simp]: fixes x :: "'a fim" shows "x + x = x" |
|
64 proof transfer |
|
65 fix xs :: "'a list" |
|
66 show "eq (xs @ xs) xs" |
|
67 proof(cases "xs = []") |
|
68 case False thus ?thesis using cancel1_same[of xs] by(auto) |
|
69 qed simp |
|
70 qed |
|
71 |
|
72 |
|
73 inductive pcancel1 :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where |
|
74 pcancel1: "pcancel1 (concat xss) (concat yss)" if "list_all2 (\<lambda>xs ys. xs = ys \<or> xs = ys @ ys) xss yss" |
|
75 |
|
76 lemma cancel1_into_pcancel1: "pcancel1 xs ys" if "cancel1 xs ys" |
|
77 using that |
|
78 proof cases |
|
79 case (cancel1 xs gs gs') |
|
80 let ?xss = "[gs, xs @ xs, gs']" and ?yss = "[gs, xs, gs']" |
|
81 have "pcancel1 (concat ?xss) (concat ?yss)" by(rule pcancel1.intros) simp |
|
82 then show ?thesis using cancel1 by simp |
|
83 qed |
|
84 |
|
85 lemma pcancel_into_cancel: "cancel1\<^sup>*\<^sup>* xs ys" if "pcancel1 xs ys" |
|
86 using that |
|
87 proof cases |
|
88 case (pcancel1 xss yss) |
|
89 from pcancel1(3) show ?thesis unfolding pcancel1(1-2) |
|
90 apply induction |
|
91 apply simp |
|
92 apply(auto intro: cancel_append_same1) |
|
93 apply(rule rtranclp_trans) |
|
94 apply(subst append_assoc[symmetric]) |
|
95 apply(rule cancel_append_same2) |
|
96 apply(rule cancel_same) |
|
97 apply(auto intro: cancel_append_same1) |
|
98 done |
|
99 qed |
|
100 |
|
101 lemma pcancel1_cancel1_confluent: |
|
102 assumes "pcancel1 xs ys" |
|
103 and "cancel1 zs ys" |
|
104 shows "\<exists>us. cancel us xs \<and> pcancel1 us zs" |
|
105 proof - |
|
106 let ?P = "\<lambda>xs ys. xs = ys \<or> xs = ys @ ys" |
|
107 consider ass as2 bs1 bss bs2 cs1 css ass' as2bs1 bss' bs2cs1 css' |
|
108 where "ys = concat ass @ as2 @ bs1 @ concat bss @ bs2 @ cs1 @ concat css" |
|
109 and "xs = concat ass' @ as2bs1 @ concat bss' @ bs2cs1 @ concat css'" |
|
110 and "zs = concat ass @ as2 @ bs1 @ concat bss @ bs2 @ bs1 @ concat bss @ bs2 @ cs1 @ concat css" |
|
111 and "list_all2 ?P ass' ass" |
|
112 and "list_all2 ?P bss' bss" |
|
113 and "list_all2 ?P css' css" |
|
114 and "?P as2bs1 (as2 @ bs1)" |
|
115 and "?P bs2cs1 (bs2 @ cs1)" |
|
116 | ass as2 bs cs1 css ass' css' |
|
117 where "ys = concat ass @ as2 @ bs @ cs1 @ concat css" |
|
118 and "xs = concat ass' @ as2 @ bs @ cs1 @ as2 @ bs @ cs1 @ concat css'" |
|
119 and "zs = concat ass @ as2 @ bs @ bs @ cs1 @ concat css" |
|
120 and "list_all2 ?P ass' ass" |
|
121 and "list_all2 ?P css' css" |
|
122 proof - |
|
123 from assms obtain xss bs as cs yss |
|
124 where xs: "xs = concat xss" and zs: "zs = as @ bs @ bs @ cs" |
|
125 and xss: "list_all2 (\<lambda>xs ys. xs = ys \<or> xs = ys @ ys) xss yss" |
|
126 and ys: "ys = as @ bs @ cs" |
|
127 and yss: "concat yss = as @ bs @ cs" |
|
128 and bs: "bs \<noteq> []" |
|
129 by(clarsimp simp add: pcancel1.simps cancel1.simps) |
|
130 from yss bs obtain ass as2 BS bcss |
|
131 where yss: "yss = ass @ (as2 @ BS) # bcss" |
|
132 and as: "as = concat ass @ as2" |
|
133 and eq: "bs @ cs = BS @ concat bcss" |
|
134 by(auto simp add: concat_eq_append_conv split: if_split_asm) |
|
135 define bcss' where "bcss' = (if bcss = [] then [[]] else bcss)" |
|
136 have bcss': "bcss' \<noteq> []" by(simp add: bcss'_def) |
|
137 from eq consider us where "bs = BS @ us" "concat bcss = us @ cs" "bcss \<noteq> []" | |
|
138 "BS = bs @ cs" "bcss = []" | |
|
139 us where "BS = bs @ us" "cs = us @ concat bcss" |
|
140 by(cases "bcss = []")(auto simp add: append_eq_append_conv2) |
|
141 then show thesis |
|
142 proof cases |
|
143 case 1 |
|
144 from 1(2,3) obtain bss bs2 cs1 css |
|
145 where "bcss = bss @ (bs2 @ cs1) # css" |
|
146 and us: "us = concat bss @ bs2" |
|
147 and cs: "cs = cs1 @ concat css" by(auto simp add: concat_eq_append_conv) |
|
148 with 1 xs xss ys yss zs as that(1)[of ass as2 BS bss bs2 cs1 css] show ?thesis |
|
149 by(clarsimp simp add: list_all2_append2 list_all2_Cons2) |
|
150 next |
|
151 case 2 |
|
152 with xs xss ys yss zs as show ?thesis |
|
153 using that(1)[of ass as2 bs "[]" "[]" "[]" "[cs]" _ "as2 @ bs" "[]" "[]" "[cs]"] |
|
154 using that(2)[of ass as2 bs cs "[]"] |
|
155 by(auto simp add: list_all2_append2 list_all2_Cons2) |
|
156 next |
|
157 case 3 |
|
158 with xs xss ys yss zs as show ?thesis |
|
159 using that(1)[of ass as2 "[]" "[bs]" "[]" "us" "bcss" _ "as2" "[bs]"] that(2)[of ass as2 bs us bcss] |
|
160 by(auto simp add: list_all2_append2 list_all2_Cons2) |
|
161 qed |
|
162 qed |
|
163 then show ?thesis |
|
164 proof cases |
|
165 case 1 |
|
166 let ?us = "concat ass' @ as2bs1 @ concat bss' @ bs2 @ bs1 @ concat bss' @ bs2cs1 @ concat css'" |
|
167 have "?us = concat (ass' @ [as2bs1] @ bss' @ [bs2 @ bs1] @ bss' @ [bs2cs1] @ css')" by simp |
|
168 also have "pcancel1 \<dots> (concat (ass @ [as2 @ bs1] @ bss @ [bs2 @ bs1] @ bss @ [bs2 @ cs1] @ css))" |
|
169 by(rule pcancel1.intros)(use 1 in \<open>simp add: list_all2_appendI\<close>) |
|
170 also have "\<dots> = zs" using 1 by simp |
|
171 also have "cancel ?us xs" |
|
172 proof - |
|
173 define as2b where "as2b = (if as2bs1 = as2 @ bs1 then as2 else as2 @ bs1 @ as2)" |
|
174 have as2bs1: "as2bs1 = as2b @ bs1" using 1 by(auto simp add: as2b_def) |
|
175 define b2cs where "b2cs = (if bs2cs1 = bs2 @ cs1 then cs1 else cs1 @ bs2 @ cs1)" |
|
176 have bs2cs1: "bs2cs1 = bs2 @ b2cs" using 1 by(auto simp add: b2cs_def) |
|
177 have "?us = (concat ass' @ as2b) @ ((bs1 @ concat bss' @ bs2) @ (bs1 @ concat bss' @ bs2)) @ b2cs @ concat css'" |
|
178 by(simp add: as2bs1 bs2cs1) |
|
179 also have "cancel \<dots> ((concat ass' @ as2b) @ (bs1 @ concat bss' @ bs2) @ b2cs @ concat css')" |
|
180 by(rule cancel_append_same1 cancel_append_same2 cancel_same)+ |
|
181 also have "\<dots> = xs" using 1 bs2cs1 as2bs1 by simp |
|
182 finally show ?thesis . |
|
183 qed |
|
184 ultimately show ?thesis by blast |
|
185 next |
|
186 case 2 |
|
187 let ?us = "concat ass' @ as2 @ bs @ bs @ cs1 @ as2 @ bs @ bs @ cs1 @ concat css'" |
|
188 have "?us = concat (ass' @ [as2 @ bs @ bs @ cs1 @ as2 @ bs @ bs @ cs1] @ css')" by simp |
|
189 also have "pcancel1 \<dots> (concat (ass @ [as2 @ bs @ bs @ cs1] @ css))" |
|
190 by(intro pcancel1.intros list_all2_appendI)(simp_all add: 2) |
|
191 also have "\<dots> = zs" using 2 by simp |
|
192 also have "cancel ?us xs" |
|
193 proof - |
|
194 have "?us = (concat ass' @ as2) @ (bs @ bs) @ cs1 @ as2 @ bs @ bs @ cs1 @ concat css'" by simp |
|
195 also have "cancel \<dots> ((concat ass' @ as2) @ bs @ cs1 @ as2 @ bs @ bs @ cs1 @ concat css')" |
|
196 by(rule cancel_append_same1 cancel_append_same2 cancel_same)+ |
|
197 also have "\<dots> = (concat ass' @ as2 @ bs @ cs1 @ as2) @ (bs @ bs) @ cs1 @ concat css'" by simp |
|
198 also have "cancel \<dots> ((concat ass' @ as2 @ bs @ cs1 @ as2) @ bs @ cs1 @ concat css')" |
|
199 by(rule cancel_append_same1 cancel_append_same2 cancel_same)+ |
|
200 also have "\<dots> = xs" using 2 by simp |
|
201 finally show ?thesis . |
|
202 qed |
|
203 ultimately show ?thesis by blast |
|
204 qed |
|
205 qed |
|
206 |
|
207 lemma pcancel1_cancel_confluent: |
|
208 assumes "pcancel1 xs ys" |
|
209 and "cancel zs ys" |
|
210 shows "\<exists>us. cancel us xs \<and> pcancel1 us zs" |
|
211 using assms(2,1) |
|
212 by(induction arbitrary: xs)(fastforce elim!: rtranclp_trans dest: pcancel1_cancel1_confluent)+ |
|
213 |
|
214 lemma cancel1_semiconfluent: |
|
215 assumes "cancel1 xs ys" |
|
216 and "cancel zs ys" |
|
217 shows "\<exists>us. cancel us xs \<and> cancel us zs" |
|
218 using pcancel1_cancel_confluent[OF cancel1_into_pcancel1, OF assms] |
|
219 by(blast intro: pcancel_into_cancel) |
|
220 |
|
221 lemma semiconfluentp_cancel1: "semiconfluentp cancel1\<inverse>\<inverse>" |
|
222 by(auto simp add: semiconfluentp_def rtranclp_conversep dest: cancel1_semiconfluent) |
|
223 |
|
224 lemma retract_cancel1_aux: |
|
225 assumes "cancel1 ys (map f xs)" |
|
226 shows "\<exists>zs. cancel1 zs xs \<and> ys = map f zs" |
|
227 using assms |
|
228 by cases(fastforce simp add: map_eq_append_conv append_eq_map_conv intro: cancel1.intros) |
|
229 |
|
230 lemma retract_cancel1: |
|
231 assumes "cancel1 ys (map f xs)" |
|
232 shows "\<exists>zs. eq xs zs \<and> ys = map f zs" |
|
233 using retract_cancel1_aux[OF assms] by(blast intro: symclpI) |
|
234 |
|
235 lemma cancel1_set_eq: |
|
236 assumes "cancel1 ys xs" |
|
237 shows "set ys = set xs" |
|
238 using assms by cases auto |
|
239 |
|
240 lemma eq_set_eq: "set xs = set ys" if "eq xs ys" |
|
241 using that by(induction)(auto dest!: cancel1_set_eq elim!: symclpE) |
|
242 |
|
243 context includes lifting_syntax begin |
|
244 lemma map_respect_cancel1: "((=) ===> cancel1 ===> eq) map map" |
|
245 by(auto 4 4 simp add: rel_fun_def cancel1.simps intro: symclpI cancel1.intros) |
|
246 |
|
247 lemma map_respect_eq: "((=) ===> eq ===> eq) map map" |
|
248 apply(intro rel_funI; hypsubst) |
|
249 subgoal for _ f x y |
|
250 by(induction rule: equivclp_induct) |
|
251 (auto dest: map_respect_cancel1[THEN rel_funD, THEN rel_funD, OF refl] intro: eq_sym equivclp_trans) |
|
252 done |
|
253 end |
|
254 |
|
255 lemma confluent_quotient_fim: |
|
256 "confluent_quotient cancel1\<inverse>\<inverse> eq eq eq eq eq (map fst) (map snd) (map fst) (map snd) list_all2 list_all2 list_all2 set set" |
|
257 by(unfold_locales)(auto dest: retract_cancel1 eq_set_eq simp add: list.in_rel list.rel_compp map_respect_eq[THEN rel_funD, OF refl] semiconfluentp_imp_confluentp semiconfluentp_cancel1)+ |
|
258 |
|
259 lift_bnf 'a fim [wits: "[]"] |
|
260 subgoal for A B by(rule confluent_quotient.subdistributivity[OF confluent_quotient_fim]) |
|
261 subgoal by(force dest: eq_set_eq) |
|
262 subgoal by(auto elim: allE[where x="[]"]) |
|
263 done |
|
264 |
|
265 end |