75 | "furtherSEQ r11 r2 = [SEQ r11 r2]" |
75 | "furtherSEQ r11 r2 = [SEQ r11 r2]" |
76 | "turnIntoTerms (SEQ ONE r2) = turnIntoTerms r2" |
76 | "turnIntoTerms (SEQ ONE r2) = turnIntoTerms r2" |
77 | "turnIntoTerms (SEQ r1 r2) = concat (map (\<lambda>r11. furtherSEQ r11 r2) (turnIntoTerms r1))" |
77 | "turnIntoTerms (SEQ r1 r2) = concat (map (\<lambda>r11. furtherSEQ r11 r2) (turnIntoTerms r1))" |
78 | "turnIntoTerms r = [r]" |
78 | "turnIntoTerms r = [r]" |
79 |
79 |
80 fun regConcat :: "rexp \<Rightarrow> rexp list \<Rightarrow> rexp" where |
80 abbreviation "tint \<equiv> turnIntoTerms" |
81 "regConcat acc [] = acc" |
81 |
82 | "regConcat ONE (r # rs1) = regConcat r rs1" |
82 fun seqFold :: "rexp \<Rightarrow> rexp list \<Rightarrow> rexp" where |
83 | "regConcat acc (r # rs1) = regConcat (SEQ acc r) rs1" |
83 "seqFold acc [] = acc" |
|
84 | "seqFold ONE (r # rs1) = seqFold r rs1" |
|
85 | "seqFold acc (r # rs1) = seqFold (SEQ acc r) rs1" |
|
86 |
84 |
87 |
85 fun attachCtx :: "arexp \<Rightarrow> rexp list \<Rightarrow> rexp set" where |
88 fun attachCtx :: "arexp \<Rightarrow> rexp list \<Rightarrow> rexp set" where |
86 "attachCtx r ctx = set (turnIntoTerms (regConcat (erase r) ctx))" |
89 "attachCtx r ctx = set (turnIntoTerms (seqFold (erase r) ctx))" |
87 |
|
88 |
90 |
89 |
91 |
90 fun rs1_subseteq_rs2 :: "rexp set \<Rightarrow> rexp set \<Rightarrow> bool" where |
92 fun rs1_subseteq_rs2 :: "rexp set \<Rightarrow> rexp set \<Rightarrow> bool" where |
91 "rs1_subseteq_rs2 rs1 rs2 = (rs1 \<subseteq> rs2)" |
93 "rs1_subseteq_rs2 rs1 rs2 = (rs1 \<subseteq> rs2)" |
|
94 |
92 |
95 |
93 fun notZero :: "arexp \<Rightarrow> bool" where |
96 fun notZero :: "arexp \<Rightarrow> bool" where |
94 "notZero AZERO = True" |
97 "notZero AZERO = True" |
95 | "notZero _ = False" |
98 | "notZero _ = False" |
96 |
99 |
|
100 |
97 fun tset :: "arexp list \<Rightarrow> rexp set" where |
101 fun tset :: "arexp list \<Rightarrow> rexp set" where |
98 "tset rs = set (concat (map turnIntoTerms (map erase rs)))" |
102 "tset rs = set (concat (map turnIntoTerms (map erase rs)))" |
99 |
103 |
100 |
104 |
101 fun prune6 :: "rexp set \<Rightarrow> arexp \<Rightarrow> rexp list \<Rightarrow> arexp" where |
105 fun prune6 :: "rexp set \<Rightarrow> arexp \<Rightarrow> rexp list \<Rightarrow> arexp" where |
102 "prune6 acc a ctx = (if (ABIncludedByC a ctx acc attachCtx rs1_subseteq_rs2) then AZERO else |
106 "prune6 acc a ctx = (if (ABIncludedByC a ctx acc attachCtx rs1_subseteq_rs2) then AZERO else |
103 (case a of (ASEQ bs r1 r2) \<Rightarrow> bsimp_ASEQ bs (prune6 acc r1 (erase r2 # ctx)) r2 |
107 (case a of (ASEQ bs r1 r2) \<Rightarrow> bsimp_ASEQ bs (prune6 acc r1 (erase r2 # ctx)) r2 |
104 | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r.(prune6 acc r ctx)) rs0))) )" |
108 | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r.(prune6 acc r ctx)) rs0)) |
|
109 | r \<Rightarrow> r |
|
110 ) |
|
111 ) |
|
112 " |
105 |
113 |
106 abbreviation |
114 abbreviation |
107 "p acc r \<equiv> prune6 (set (concat (map turnIntoTerms (map erase acc)) ) ) r Nil" |
115 "p6 acc r \<equiv> prune6 (tset acc) r Nil" |
108 |
116 |
109 |
117 |
110 fun dB6 :: "arexp list \<Rightarrow> rexp set \<Rightarrow> arexp list" where |
118 fun dB6 :: "arexp list \<Rightarrow> rexp set \<Rightarrow> arexp list" where |
111 "dB6 [] acc = []" |
119 "dB6 [] acc = []" |
112 | "dB6 (a # as) acc = (if (erase a \<in> acc) then (dB6 as acc) |
120 | "dB6 (a # as) acc = (if (erase a \<in> acc) then (dB6 as acc) |
152 | ss2: "rs1 s\<leadsto> rs2 \<Longrightarrow> (r # rs1) s\<leadsto> (r # rs2)" |
160 | ss2: "rs1 s\<leadsto> rs2 \<Longrightarrow> (r # rs1) s\<leadsto> (r # rs2)" |
153 | ss3: "r1 \<leadsto> r2 \<Longrightarrow> (r1 # rs) s\<leadsto> (r2 # rs)" |
161 | ss3: "r1 \<leadsto> r2 \<Longrightarrow> (r1 # rs) s\<leadsto> (r2 # rs)" |
154 | ss4: "(AZERO # rs) s\<leadsto> rs" |
162 | ss4: "(AZERO # rs) s\<leadsto> rs" |
155 | ss5: "(AALTs bs1 rs1 # rsb) s\<leadsto> ((map (fuse bs1) rs1) @ rsb)" |
163 | ss5: "(AALTs bs1 rs1 # rsb) s\<leadsto> ((map (fuse bs1) rs1) @ rsb)" |
156 | ss6: "L (erase a2) \<subseteq> L (erase a1) \<Longrightarrow> (rsa@[a1]@rsb@[a2]@rsc) s\<leadsto> (rsa@[a1]@rsb@rsc)" |
164 | ss6: "L (erase a2) \<subseteq> L (erase a1) \<Longrightarrow> (rsa@[a1]@rsb@[a2]@rsc) s\<leadsto> (rsa@[a1]@rsb@rsc)" |
157 | ss7: " (as @ [a] @ as1) s\<leadsto> (as @ [prune6 (set (concat (map (\<lambda>r. turnIntoTerms (erase r)) as))) a Nil] @ as1)" |
165 | ss7: " (as @ [a] @ as1) s\<leadsto> (as @ [p6 as a] @ as1)" |
158 |
166 |
|
167 thm tset.simps |
159 |
168 |
160 inductive |
169 inductive |
161 rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100) |
170 rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100) |
162 where |
171 where |
163 rs1[intro, simp]:"r \<leadsto>* r" |
172 rs1[intro, simp]:"r \<leadsto>* r" |
289 apply simp |
298 apply simp |
290 apply(rename_tac cc' cc) |
299 apply(rename_tac cc' cc) |
291 apply(subgoal_tac "(cc @ a # cc') s\<leadsto>* (cc @ a # dB6 cc' (tset (cc @ [a])))") |
300 apply(subgoal_tac "(cc @ a # cc') s\<leadsto>* (cc @ a # dB6 cc' (tset (cc @ [a])))") |
292 prefer 2 |
301 prefer 2 |
293 apply (metis append.assoc append.left_neutral append_Cons) |
302 apply (metis append.assoc append.left_neutral append_Cons) |
294 apply(subgoal_tac "(cc @ a # dB6 cc' (tset (cc @ [a]))) s\<leadsto>* (cc @ (p cc a) # dB6 cc' (tset (cc @ [a])))") |
303 apply(subgoal_tac "(cc @ a # dB6 cc' (tset (cc @ [a]))) s\<leadsto>* (cc @ (p6 cc a) # dB6 cc' (tset (cc @ [a])))") |
295 sorry |
304 sorry |
296 |
305 |
297 |
306 (* |
298 lemma ss6_stronger_aux: |
307 lemma ss6_stronger_aux: |
299 shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (map erase rs1)))" |
308 shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (map erase rs1)))" |
300 apply(induct rs2 arbitrary: rs1) |
309 apply(induct rs2 arbitrary: rs1) |
301 apply simp |
310 apply simp |
302 apply(case_tac "erase a \<in> erase ` set rs1") |
311 apply(case_tac "erase a \<in> erase ` set rs1") |
311 |
320 |
312 apply(auto) |
321 apply(auto) |
313 prefer 2 |
322 prefer 2 |
314 apply(drule_tac x="rs1 @ [a]" in meta_spec) |
323 apply(drule_tac x="rs1 @ [a]" in meta_spec) |
315 apply(simp) |
324 apply(simp) |
316 apply(drule_tac x="rs1" in meta_spec) |
|
317 apply(subgoal_tac "(rs1 @ a # rs2) s\<leadsto>* (rs1 @ rs2)") |
|
318 using srewrites_trans apply blast |
|
319 apply(subgoal_tac "\<exists>rs1a rs1b. rs1 = rs1a @ [x] @ rs1b") |
|
320 prefer 2 |
|
321 apply (simp add: split_list) |
|
322 apply(erule exE)+ |
|
323 apply(simp) |
|
324 using eq1_L rs_in_rstar ss |
|
325 sorry |
325 sorry |
|
326 *) |
326 |
327 |
327 |
328 |
328 lemma ss6_stronger: |
329 lemma ss6_stronger: |
329 shows "rs1 s\<leadsto>* dB6 rs1 {}" |
330 shows "rs1 s\<leadsto>* dB6 rs1 {}" |
|
331 using ss6 |
|
332 by (metis append_Nil concat.simps(1) list.set(1) list.simps(8) ss6_realistic tset.simps) |
|
333 |
|
334 |
|
335 lemma tint_fuse: |
|
336 shows "tint (erase a) = tint (erase (fuse bs a))" |
|
337 by (simp add: erase_fuse) |
|
338 |
|
339 lemma tint_fuse2: |
|
340 shows " set (tint (erase a)) = |
|
341 set (tint (erase (fuse bs a)))" |
|
342 using tint_fuse by auto |
|
343 |
|
344 lemma fused_bits_at_head: |
|
345 shows "fuse bs a = ASEQ bs1 a1 a2 \<Longrightarrow> \<exists>bs2. bs1 = bs @ bs2" |
|
346 |
|
347 (* by (smt (verit) arexp.distinct(13) arexp.distinct(19) arexp.distinct(25) arexp.distinct(27) arexp.distinct(5) arexp.inject(3) fuse.elims) |
|
348 harmless sorry |
|
349 *) |
|
350 |
330 sorry |
351 sorry |
331 |
352 |
|
353 thm seqFold.simps |
|
354 |
|
355 lemma seqFold_concats: |
|
356 shows "r \<noteq> ONE \<Longrightarrow> seqFold r [r1] = SEQ r r1" |
|
357 apply(case_tac r) |
|
358 apply simp+ |
|
359 done |
|
360 |
|
361 |
|
362 lemma "set (tint (seqFold (erase x42) [erase x43])) = |
|
363 set (tint (SEQ (erase x42) (erase x43)))" |
|
364 apply(case_tac "erase x42 = ONE") |
|
365 apply simp |
|
366 apply simp |
|
367 |
|
368 lemma prune6_preserves_fuse: |
|
369 shows "fuse bs (p6 as a) = p6 as (fuse bs a)" |
|
370 using tint_fuse2 |
|
371 apply simp |
|
372 apply(case_tac a) |
|
373 apply simp |
|
374 apply simp |
|
375 apply simp |
|
376 |
|
377 using fused_bits_at_head |
|
378 |
|
379 apply simp |
|
380 apply(case_tac "erase x42 = ONE") |
|
381 apply simp |
|
382 |
|
383 sorry |
|
384 |
|
385 corollary prune6_preserves_fuse_srewrite: |
|
386 shows "(as @ map (fuse bs) [a] @ as2) s\<leadsto>* (as @ map (fuse bs) [p6 as a] @ as2)" |
|
387 apply(subgoal_tac "map (fuse bs) [a] = [fuse bs a]") |
|
388 apply(subgoal_tac "(as @ [fuse bs a] @ as2) s\<leadsto>* (as @ [ (p6 as (fuse bs a))] @ as2)") |
|
389 using prune6_preserves_fuse apply auto[1] |
|
390 using rs_in_rstar ss7 apply presburger |
|
391 by simp |
|
392 |
|
393 lemma prune6_invariant_fuse: |
|
394 shows "p6 as a = p6 (map (fuse bs) as) a" |
|
395 apply simp |
|
396 using erase_fuse by presburger |
|
397 |
|
398 |
|
399 lemma p6pfs_cor: |
|
400 shows "(map (fuse bs) as @ map (fuse bs) [a] @ map (fuse bs) as1) s\<leadsto>* (map (fuse bs) as @ map (fuse bs) [p6 as a] @ map (fuse bs) as1)" |
|
401 by (metis prune6_invariant_fuse prune6_preserves_fuse_srewrite) |
332 |
402 |
333 lemma rewrite_preserves_fuse: |
403 lemma rewrite_preserves_fuse: |
334 shows "r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto> fuse bs r3" |
404 shows "r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto> fuse bs r3" |
335 and "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto>* map (fuse bs) rs3" |
405 and "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto>* map (fuse bs) rs3" |
336 proof(induct rule: rrewrite_srewrite.inducts) |
406 proof(induct rule: rrewrite_srewrite.inducts) |
356 next |
426 next |
357 case (ss6 a1 a2 rsa rsb rsc) |
427 case (ss6 a1 a2 rsa rsb rsc) |
358 then show ?case |
428 then show ?case |
359 apply(simp only: map_append) |
429 apply(simp only: map_append) |
360 by (smt (verit, best) erase_fuse list.simps(8) list.simps(9) rrewrite_srewrite.ss6 srewrites.simps) |
430 by (smt (verit, best) erase_fuse list.simps(8) list.simps(9) rrewrite_srewrite.ss6 srewrites.simps) |
|
431 next |
|
432 case (ss7 as a as1) |
|
433 then show ?case |
|
434 apply(simp only: map_append) |
|
435 using p6pfs_cor by presburger |
361 qed (auto intro: rrewrite_srewrite.intros) |
436 qed (auto intro: rrewrite_srewrite.intros) |
|
437 |
362 |
438 |
363 |
439 |
364 lemma rewrites_fuse: |
440 lemma rewrites_fuse: |
365 assumes "r1 \<leadsto>* r2" |
441 assumes "r1 \<leadsto>* r2" |
366 shows "fuse bs r1 \<leadsto>* fuse bs r2" |
442 shows "fuse bs r1 \<leadsto>* fuse bs r2" |
422 by (simp add: srewrites7) |
498 by (simp add: srewrites7) |
423 |
499 |
424 lemma bnullable0: |
500 lemma bnullable0: |
425 shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 = bnullable r2" |
501 shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 = bnullable r2" |
426 and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 = bnullables rs2" |
502 and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 = bnullables rs2" |
427 apply(induct rule: rrewrite_srewrite.inducts) |
503 apply(induct rule: rrewrite_srewrite.inducts) |
428 apply(auto simp add: bnullable_fuse) |
504 apply simp |
429 apply (meson UnCI bnullable_fuse imageI) |
505 apply simp |
430 using bnullable_correctness nullable_correctness by blast |
506 apply (simp add: bnullable_fuse) |
431 |
507 using bnullable.simps(5) apply presburger |
|
508 apply simp |
|
509 apply simp |
|
510 sorry |
432 |
511 |
433 |
512 |
434 |
513 |
435 lemma rewritesnullable: |
514 lemma rewritesnullable: |
436 assumes "r1 \<leadsto>* r2" |
515 assumes "r1 \<leadsto>* r2" |
437 shows "bnullable r1 = bnullable r2" |
516 shows "bnullable r1 = bnullable r2" |
438 using assms |
517 using assms |
439 apply(induction r1 r2 rule: rrewrites.induct) |
518 apply(induction r1 r2 rule: rrewrites.induct) |
440 apply simp |
519 apply simp |
441 using bnullable0(1) by auto |
520 using bnullable0(1) by presburger |
442 |
521 |
443 lemma rewrite_bmkeps_aux: |
522 lemma rewrite_bmkeps_aux: |
444 shows "r1 \<leadsto> r2 \<Longrightarrow> (bnullable r1 \<and> bnullable r2 \<Longrightarrow> bmkeps r1 = bmkeps r2)" |
523 shows "r1 \<leadsto> r2 \<Longrightarrow> (bnullable r1 \<and> bnullable r2 \<Longrightarrow> bmkeps r1 = bmkeps r2)" |
445 and "rs1 s\<leadsto> rs2 \<Longrightarrow> (bnullables rs1 \<and> bnullables rs2 \<Longrightarrow> bmkepss rs1 = bmkepss rs2)" |
524 and "rs1 s\<leadsto> rs2 \<Longrightarrow> (bnullables rs1 \<and> bnullables rs2 \<Longrightarrow> bmkepss rs1 = bmkepss rs2)" |
446 proof (induct rule: rrewrite_srewrite.inducts) |
525 proof (induct rule: rrewrite_srewrite.inducts) |