4 |
4 |
5 lemma add0_isomorphic: |
5 lemma add0_isomorphic: |
6 shows "rsimp_ALTs (rdistinct (rflts [rsimp r, RZERO]) {}) = rsimp r" |
6 shows "rsimp_ALTs (rdistinct (rflts [rsimp r, RZERO]) {}) = rsimp r" |
7 sorry |
7 sorry |
8 |
8 |
|
9 |
|
10 |
|
11 |
|
12 lemma distinct_removes_last: |
|
13 shows "\<lbrakk>(a::rrexp) \<in> set as\<rbrakk> |
|
14 \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset" |
|
15 and "rdistinct (ab # as @ [ab]) rset1 = rdistinct (ab # as) rset1" |
|
16 apply(induct as arbitrary: rset ab rset1 a) |
|
17 apply simp |
|
18 apply simp |
|
19 apply(case_tac "aa \<in> rset") |
|
20 apply(case_tac "a = aa") |
|
21 apply (metis append_Cons) |
|
22 apply simp |
|
23 apply(case_tac "a \<in> set as") |
|
24 apply (metis append_Cons rdistinct.simps(2) set_ConsD) |
|
25 apply(case_tac "a = aa") |
|
26 prefer 2 |
|
27 apply simp |
|
28 apply (metis append_Cons) |
|
29 apply(case_tac "ab \<in> rset1") |
|
30 prefer 2 |
|
31 apply(subgoal_tac "rdistinct (ab # (a # as) @ [ab]) rset1 = |
|
32 ab # (rdistinct ((a # as) @ [ab]) (insert ab rset1))") |
|
33 prefer 2 |
|
34 apply force |
|
35 apply(simp only:) |
|
36 apply(subgoal_tac "rdistinct (ab # a # as) rset1 = ab # (rdistinct (a # as) (insert ab rset1))") |
|
37 apply(simp only:) |
|
38 apply(subgoal_tac "rdistinct ((a # as) @ [ab]) (insert ab rset1) = rdistinct (a # as) (insert ab rset1)") |
|
39 apply blast |
|
40 apply(case_tac "a \<in> insert ab rset1") |
|
41 apply simp |
|
42 apply (metis insertI1) |
|
43 apply simp |
|
44 apply (meson insertI1) |
|
45 apply simp |
|
46 apply(subgoal_tac "rdistinct ((a # as) @ [ab]) rset1 = rdistinct (a # as) rset1") |
|
47 apply simp |
|
48 by (metis append_Cons insert_iff insert_is_Un rdistinct.simps(2)) |
|
49 |
|
50 |
|
51 lemma distinct_removes_last2: |
|
52 shows "\<lbrakk>(a::rrexp) \<in> set as\<rbrakk> |
|
53 \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset" |
|
54 using distinct_removes_last(1) by presburger |
9 |
55 |
10 lemma distinct_append_simp: |
56 lemma distinct_append_simp: |
11 shows " rsimp (rsimp_ALTs rs1) = rsimp (rsimp_ALTs rs2) \<Longrightarrow> |
57 shows " rsimp (rsimp_ALTs rs1) = rsimp (rsimp_ALTs rs2) \<Longrightarrow> |
12 rsimp (rsimp_ALTs (f a # rs1)) = |
58 rsimp (rsimp_ALTs (f a # rs1)) = |
13 rsimp (rsimp_ALTs (f a # rs2))" |
59 rsimp (rsimp_ALTs (f a # rs2))" |
132 shows "\<not>rnullable a \<Longrightarrow> rder x (RSEQ (RSTAR a) b) = rder x (RALT (RSEQ (RSEQ a (RSTAR a)) b) b)" |
176 shows "\<not>rnullable a \<Longrightarrow> rder x (RSEQ (RSTAR a) b) = rder x (RALT (RSEQ (RSEQ a (RSTAR a)) b) b)" |
133 apply (subst star_seq) |
177 apply (subst star_seq) |
134 apply simp |
178 apply simp |
135 done |
179 done |
136 |
180 |
137 |
181 |
138 |
|
139 |
|
140 lemma alts_preimage_cases: |
|
141 shows "rder x r = RALT (RSEQ r1 r2) r3 \<Longrightarrow> (\<exists>ra rb. r = RSEQ ra rb) \<or> (\<exists>rc rd re. r = RALT (RSEQ rc rd) re)" |
|
142 apply(case_tac r) |
|
143 apply simp+ |
|
144 |
|
145 apply (metis rrexp.simps(12) rrexp.simps(20)) |
|
146 prefer 3 |
|
147 apply simp |
|
148 apply blast |
|
149 apply(frule alts_preimage_case2_2) |
|
150 apply(case_tac "(\<exists>ra rb. r = RSEQ ra rb)") |
|
151 apply blast |
|
152 apply(subgoal_tac " (\<exists> rc rd. r = RALT rc rd )") |
|
153 prefer 2 |
|
154 apply blast |
|
155 apply(erule exE)+ |
|
156 apply(subgoal_tac "rder x r = RALT (rder x rc) (rder x rd)") |
|
157 prefer 2 |
|
158 apply force |
|
159 apply(subgoal_tac "rder x rc = RSEQ r1 r2") |
|
160 oops |
|
161 |
|
162 |
|
163 lemma der_seq_eq_case: |
|
164 shows "\<lbrakk>r1 \<noteq> r2 ; r1 = RSEQ ra rb; rder x r1 = rder x r2\<rbrakk> \<Longrightarrow> rsimp (rder x r1) = RZERO \<and> rsimp (rder x r2) = RZERO" |
|
165 apply(case_tac "rnullable ra") |
|
166 apply simp |
|
167 oops |
|
168 |
|
169 |
|
170 |
|
171 |
|
172 lemma der_map_unequal_to_equal_zero_only: |
|
173 shows "\<lbrakk>r1 \<noteq> r2 ; rder x r1 = rder x r2 \<rbrakk> \<Longrightarrow> rsimp (rder x r1) = RZERO" |
|
174 apply(induct r1) |
|
175 apply simp |
|
176 apply simp |
|
177 apply simp |
|
178 apply(case_tac "x = xa") |
|
179 apply simp |
|
180 apply(subgoal_tac "r2 = RCHAR xa") |
|
181 prefer 2 |
|
182 using inv_one_derx apply blast |
|
183 apply simp |
|
184 using rsimp.simps(3) apply presburger |
|
185 apply(case_tac "rder x (RSEQ r11 r12)") |
|
186 apply simp |
|
187 apply (metis inv_one_derx) |
|
188 apply (metis rrexp.distinct(21) rrexp.simps(24) shape_of_derseq) |
|
189 apply(subgoal_tac "rder x r2 = RSEQ x41 x42") |
|
190 prefer 2 |
|
191 apply presburger |
|
192 apply(subgoal_tac "x41 = rder x r11") |
|
193 prefer 2 |
|
194 apply (meson shape_of_derseq2) |
|
195 apply(case_tac r2) |
|
196 apply simp+ |
|
197 apply (metis rrexp.distinct(13) rrexp.simps(10)) |
|
198 apply(subgoal_tac "x42a = x42") |
|
199 prefer 2 |
|
200 apply (metis rrexp.inject(2) rrexp.simps(30) shape_of_derseq) |
|
201 apply(subgoal_tac "rder x x41a = x41") |
|
202 prefer 2 |
|
203 apply (metis shape_of_derseq2) |
|
204 apply(simp) |
|
205 apply(subgoal_tac "\<not> rnullable r11") |
|
206 prefer 2 |
|
207 apply force |
|
208 apply simp |
|
209 apply(subgoal_tac "\<not> rnullable x41a") |
|
210 prefer 2 |
|
211 apply force |
|
212 apply simp |
|
213 |
|
214 oops |
|
215 |
|
216 |
|
217 |
|
218 lemma der_maps_1to1_except0: |
|
219 shows "\<lbrakk>rder x ` rset = dset; a \<notin> rset; rder x a \<in> dset\<rbrakk> \<Longrightarrow> rsimp (rder x a) = RZERO" |
|
220 |
|
221 |
|
222 sorry |
|
223 |
182 |
224 lemma distinct_der_set: |
183 lemma distinct_der_set: |
225 shows "(rder x) ` rset = dset \<Longrightarrow> |
184 shows "(rder x) ` rset = dset \<Longrightarrow> |
226 rsimp (rsimp_ALTs (map (rder x) (rdistinct rs rset))) = rsimp ( rsimp_ALTs (rdistinct (map (rder x) rs) dset))" |
185 rsimp (rsimp_ALTs (map (rder x) (rdistinct rs rset))) = rsimp ( rsimp_ALTs (rdistinct (map (rder x) rs) dset))" |
227 apply(induct rs arbitrary: rset dset) |
186 apply(induct rs arbitrary: rset dset) |
261 |
220 |
262 sorry |
221 sorry |
263 |
222 |
264 lemma non_empty_list: |
223 lemma non_empty_list: |
265 shows "a \<in> set as \<Longrightarrow> as \<noteq> []" |
224 shows "a \<in> set as \<Longrightarrow> as \<noteq> []" |
266 |
|
267 by (metis empty_iff empty_set) |
225 by (metis empty_iff empty_set) |
268 |
226 |
269 |
227 lemma distinct_comp: |
270 lemma distinct_removes_last: |
228 shows "rdistinct (rs1@rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))" |
271 shows "\<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as)\<rbrakk> |
229 apply(induct rs2 arbitrary: rs1) |
272 \<Longrightarrow> rsimp_ALTs (rdistinct (rflts (map rsimp as @ [rsimp a])) {}) = |
230 apply simp |
273 rsimp_ALTs (rdistinct (rflts (map rsimp as)) {})" |
231 apply(subgoal_tac "rs1 @ a # rs2 = (rs1 @ [a]) @ rs2") |
274 apply(induct "rsimp a" arbitrary: as) |
232 apply(simp only:) |
275 apply(simp) |
233 apply(case_tac "a \<in> set rs1") |
276 apply (metis append.right_neutral append_self_conv2 empty_set list.simps(9) map_append rflts.simps(2) rsimp.simps(2) rsimp_idem simp_more_distinct spawn_simp_rsimpalts) |
234 apply simp |
277 apply simp |
235 oops |
278 sorry |
236 |
|
237 lemma instantiate1: |
|
238 shows "\<lbrakk>\<And>ab rset1. rdistinct (ab # as) rset1 = rdistinct (ab # as @ [ab]) rset1\<rbrakk> \<Longrightarrow> |
|
239 rdistinct (aa # as) rset = rdistinct (aa # as @ [aa]) rset" |
|
240 apply(drule_tac x = "aa" in meta_spec) |
|
241 apply(drule_tac x = "rset" in meta_spec) |
|
242 apply simp |
|
243 done |
|
244 |
|
245 |
|
246 lemma not_head_elem: |
|
247 shows " \<lbrakk>aa \<in> set (a # as); aa \<notin> (set as)\<rbrakk> \<Longrightarrow> a = aa" |
|
248 |
|
249 by fastforce |
|
250 |
|
251 (* |
|
252 apply simp |
|
253 apply (metis append_Cons) |
|
254 apply(case_tac "ab \<in> rset1") |
|
255 apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left) |
|
256 apply(subgoal_tac "rdistinct (ab # (aa # as) @ [ab]) rset1 = |
|
257 ab # (rdistinct ((aa # as) @ [ab]) (insert ab rset1))") |
|
258 apply(simp only:) |
|
259 apply(subgoal_tac "rdistinct (ab # aa # as) rset1 = ab # (rdistinct (aa # as) (insert ab rset1))") |
|
260 apply(simp only:) |
|
261 apply(subgoal_tac "rdistinct ((aa # as) @ [ab]) (insert ab rset1) = rdistinct (aa # as) (insert ab rset1)") |
|
262 apply blast |
|
263 *) |
|
264 |
279 |
265 |
280 lemma flts_identity1: |
266 lemma flts_identity1: |
281 shows "rflts (rs @ [RONE]) = rflts rs @ [RONE] " |
267 shows "rflts (rs @ [RONE]) = rflts rs @ [RONE] " |
282 apply(induct rs) |
268 apply(induct rs) |
283 apply simp+ |
269 apply simp+ |
317 using flts_identity1 apply auto[1] |
303 using flts_identity1 apply auto[1] |
318 using flts_identity10 apply blast |
304 using flts_identity10 apply blast |
319 using flts_identity11 apply auto[1] |
305 using flts_identity11 apply auto[1] |
320 apply blast |
306 apply blast |
321 using flts_identity12 by presburger |
307 using flts_identity12 by presburger |
322 |
308 |
|
309 lemma flts_identity3: |
|
310 shows "a = RZERO \<Longrightarrow> rflts (rs @ [a]) = rflts rs" |
|
311 apply simp |
|
312 apply(induct rs) |
|
313 apply simp+ |
|
314 apply(case_tac aa) |
|
315 apply simp+ |
|
316 done |
|
317 |
|
318 lemma distinct_removes_last3: |
|
319 shows "\<lbrakk>(a::rrexp) \<in> set as\<rbrakk> |
|
320 \<Longrightarrow> rdistinct as {} = rdistinct (as @ [a]) {}" |
|
321 using distinct_removes_last2 by blast |
|
322 |
|
323 lemma set_inclusion_with_flts1: |
|
324 shows " \<lbrakk>RONE \<in> set rs\<rbrakk> \<Longrightarrow> RONE \<in> set (rflts rs)" |
|
325 apply(induct rs) |
|
326 apply simp |
|
327 apply(case_tac " RONE \<in> set rs") |
|
328 apply simp |
|
329 apply (metis Un_upper2 insert_absorb insert_subset list.set_intros(2) rflts.simps(2) rflts.simps(3) rflts_def_idiot set_append) |
|
330 apply(case_tac "RONE = a") |
|
331 apply simp |
|
332 apply simp |
|
333 done |
|
334 |
|
335 lemma set_inclusion_with_flts10: |
|
336 shows " \<lbrakk>RCHAR x \<in> set rs\<rbrakk> \<Longrightarrow> RCHAR x \<in> set (rflts rs)" |
|
337 apply(induct rs) |
|
338 apply simp |
|
339 apply(case_tac " RCHAR x \<in> set rs") |
|
340 apply simp |
|
341 apply (metis Un_upper2 insert_absorb insert_subset rflts.simps(2) rflts.simps(3) rflts_def_idiot set_append set_subset_Cons) |
|
342 apply(case_tac "RCHAR x = a") |
|
343 apply simp |
|
344 apply fastforce |
|
345 apply simp |
|
346 done |
|
347 |
|
348 lemma set_inclusion_with_flts11: |
|
349 shows " \<lbrakk>RSEQ r1 r2 \<in> set rs\<rbrakk> \<Longrightarrow> RSEQ r1 r2 \<in> set (rflts rs)" |
|
350 apply(induct rs) |
|
351 apply simp |
|
352 apply(case_tac " RSEQ r1 r2 \<in> set rs") |
|
353 apply simp |
|
354 apply (metis Un_upper2 insert_absorb insert_subset rflts.simps(2) rflts.simps(3) rflts_def_idiot set_append set_subset_Cons) |
|
355 apply(case_tac "RSEQ r1 r2 = a") |
|
356 apply simp |
|
357 apply fastforce |
|
358 apply simp |
|
359 done |
|
360 |
|
361 |
|
362 lemma set_inclusion_with_flts: |
|
363 shows " \<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as); rsimp a = RONE\<rbrakk> \<Longrightarrow> rsimp a \<in> set (rflts (map rsimp as))" |
|
364 by (simp add: set_inclusion_with_flts1) |
|
365 |
|
366 lemma "\<And>x5. \<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as); rsimp a = RALTS x5\<rbrakk> |
|
367 \<Longrightarrow> rsimp_ALTs (rdistinct (rflts (map rsimp as @ [rsimp a])) {}) = |
|
368 rsimp_ALTs (rdistinct (rflts (map rsimp as @ x5)) {})" |
|
369 |
323 |
370 |
324 lemma last_elem_dup1: |
371 lemma last_elem_dup1: |
325 shows " a \<in> set as \<Longrightarrow> rsimp (RALTS (as @ [a] )) = rsimp (RALTS (as ))" |
372 shows " a \<in> set as \<Longrightarrow> rsimp (RALTS (as @ [a] )) = rsimp (RALTS (as ))" |
326 apply simp |
373 apply simp |
327 apply(subgoal_tac "rsimp a \<in> set (map rsimp as)") |
374 apply(subgoal_tac "rsimp a \<in> set (map rsimp as)") |
328 prefer 2 |
375 prefer 2 |
329 apply simp |
376 apply simp |
330 |
377 apply(case_tac "rsimp a") |
|
378 apply simp |
|
379 |
|
380 using flts_identity3 apply presburger |
|
381 apply(subst flts_identity2) |
|
382 using rrexp.distinct(1) rrexp.distinct(15) apply presburger |
|
383 apply(subst distinct_removes_last3[symmetric]) |
|
384 using set_inclusion_with_flts apply blast |
|
385 apply simp |
|
386 apply (metis distinct_removes_last3 flts_identity10 set_inclusion_with_flts10) |
|
387 apply (metis distinct_removes_last3 flts_identity11 set_inclusion_with_flts11) |
331 sorry |
388 sorry |
332 |
389 |
333 lemma last_elem_dup: |
390 lemma last_elem_dup: |
334 shows " a \<in> set as \<Longrightarrow> rsimp (rsimp_ALTs (as @ [a] )) = rsimp (rsimp_ALTs (as ))" |
391 shows " a \<in> set as \<Longrightarrow> rsimp (rsimp_ALTs (as @ [a] )) = rsimp (rsimp_ALTs (as ))" |
335 apply(induct as rule: rev_induct) |
392 apply(induct as rule: rev_induct) |