286 |
287 |
287 |
288 |
288 |
289 |
289 |
290 |
290 |
291 |
291 lemma all_that_same_elem: |
|
292 shows "\<lbrakk> a \<in> rset; rdistinct rs {a} = []\<rbrakk> |
|
293 \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct rsb rset" |
|
294 apply(induct rs) |
|
295 apply simp |
|
296 apply(subgoal_tac "aa = a") |
|
297 apply simp |
|
298 by (metis empty_iff insert_iff list.discI rdistinct.simps(2)) |
|
299 |
292 |
300 lemma distinct_early_app1: |
293 lemma distinct_early_app1: |
301 shows "rset1 \<subseteq> rset \<Longrightarrow> rdistinct rs rset = rdistinct (rdistinct rs rset1) rset" |
294 shows "rset1 \<subseteq> rset \<Longrightarrow> rdistinct rs rset = rdistinct (rdistinct rs rset1) rset" |
302 apply(induct rs arbitrary: rset rset1) |
295 apply(induct rs arbitrary: rset rset1) |
303 apply simp |
296 apply simp |
388 shows " \<lbrakk>\<forall>r\<in>set rs. good r \<or> r = RZERO; \<forall>r\<in>set rsa . good r \<or> r = RZERO; |
381 shows " \<lbrakk>\<forall>r\<in>set rs. good r \<or> r = RZERO; \<forall>r\<in>set rsa . good r \<or> r = RZERO; |
389 \<forall>r\<in>set rsb. good r \<or> r = RZERO; |
382 \<forall>r\<in>set rsb. good r \<or> r = RZERO; |
390 rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (rsa @ rs @ rsb)) {}); |
383 rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (rsa @ rs @ rsb)) {}); |
391 rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = |
384 rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = |
392 rsimp_ALTs (rdistinct (rflts (rsa @ [rsimp (RALTS rs)] @ rsb)) {}); |
385 rsimp_ALTs (rdistinct (rflts (rsa @ [rsimp (RALTS rs)] @ rsb)) {}); |
393 map rsimp rsa = rsa; map rsimp rsb = rsb; map rsimp rs = rs; |
386 map rsimp rsa = rsa; |
|
387 map rsimp rsb = rsb; |
|
388 map rsimp rs = rs; |
394 rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = |
389 rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = |
395 rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa)); |
390 rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa)); |
396 rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} = |
391 rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} = |
397 rdistinct (rflts rsa) {} @ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))\<rbrakk> |
392 rdistinct (rflts rsa) {} @ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))\<rbrakk> |
398 \<Longrightarrow> rdistinct (rflts rs @ rflts rsb) rset = |
393 \<Longrightarrow> rdistinct (rflts rs @ rflts rsb) rset = |
437 apply(simp only:) |
432 apply(simp only:) |
438 apply(subgoal_tac "map rsimp rsb = rsb") |
433 apply(subgoal_tac "map rsimp rsb = rsb") |
439 prefer 2 |
434 prefer 2 |
440 apply (metis map_idI rsimp.simps(3) test) |
435 apply (metis map_idI rsimp.simps(3) test) |
441 apply(simp only:) |
436 apply(simp only:) |
442 apply(subst k00)+ |
437 apply(subst flts_append)+ |
443 apply(subgoal_tac "map rsimp rs = rs") |
438 apply(subgoal_tac "map rsimp rs = rs") |
444 apply(simp only:) |
439 apply(simp only:) |
445 prefer 2 |
440 prefer 2 |
446 apply (metis map_idI rsimp.simps(3) test) |
441 apply (metis map_idI rsimp.simps(3) test) |
447 apply(subgoal_tac "rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = |
442 apply(subgoal_tac "rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = |
458 rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))") |
453 rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))") |
459 apply presburger |
454 apply presburger |
460 using good_flatten_aux by blast |
455 using good_flatten_aux by blast |
461 |
456 |
462 |
457 |
463 lemma simp_flatten3: |
|
464 shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))" |
|
465 proof - |
|
466 have "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = |
|
467 rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) " |
|
468 by (metis append_Cons append_Nil list.simps(9) map_append simp_flatten_aux0) |
|
469 apply(simp only:) |
|
470 |
|
471 oops |
|
472 |
458 |
473 lemma simp_flatten3: |
459 lemma simp_flatten3: |
474 shows "rsimp (RALTS (rsa @ [RALTS rs ] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))" |
460 shows "rsimp (RALTS (rsa @ [RALTS rs ] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))" |
475 apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = |
461 apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = |
476 rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) ") |
462 rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) ") |
874 shows "rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts rs)) {})) |
860 shows "rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts rs)) {})) |
875 = rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) rs)) {}))" |
861 = rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) rs)) {}))" |
876 by (metis append.right_neutral grewrite.intros(2) grewrite_simpalts rsimp_ALTs.simps(2) simp_der_flts) |
862 by (metis append.right_neutral grewrite.intros(2) grewrite_simpalts rsimp_ALTs.simps(2) simp_der_flts) |
877 |
863 |
878 |
864 |
879 lemma basic_regex_property1: |
865 |
880 shows "rnullable r \<Longrightarrow> rsimp r \<noteq> RZERO" |
|
881 apply(induct r rule: rsimp.induct) |
|
882 apply(auto) |
|
883 apply (metis idiot idiot2 rrexp.distinct(5)) |
|
884 by (metis der_simp_nullability rnullable.simps(1) rnullable.simps(4) rsimp.simps(2)) |
|
885 |
|
886 |
|
887 lemma inside_simp_seq_nullable: |
|
888 shows |
|
889 "\<And>r1 r2. |
|
890 \<lbrakk>rsimp (rder x (rsimp r1)) = rsimp (rder x r1); rsimp (rder x (rsimp r2)) = rsimp (rder x r2); |
|
891 rnullable r1\<rbrakk> |
|
892 \<Longrightarrow> rsimp (rder x (rsimp_SEQ (rsimp r1) (rsimp r2))) = |
|
893 rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp (rder x r1)) (rsimp r2), rsimp (rder x r2)]) {})" |
|
894 apply(case_tac "rsimp r1 = RONE") |
|
895 apply(simp) |
|
896 apply(subst basic_rsimp_SEQ_property1) |
|
897 apply (simp add: idem_after_simp1) |
|
898 apply(case_tac "rsimp r1 = RZERO") |
|
899 |
|
900 using basic_regex_property1 apply blast |
|
901 apply(case_tac "rsimp r2 = RZERO") |
|
902 |
|
903 apply (simp add: basic_rsimp_SEQ_property3) |
|
904 apply(subst idiot2) |
|
905 apply simp+ |
|
906 apply(subgoal_tac "rnullable (rsimp r1)") |
|
907 apply simp |
|
908 using rsimp_idem apply presburger |
|
909 using der_simp_nullability by presburger |
|
910 |
|
911 |
866 |
912 |
867 |
913 lemma grewrite_ralts: |
868 lemma grewrite_ralts: |
914 shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs h\<leadsto>* RALTS rs'" |
869 shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs h\<leadsto>* RALTS rs'" |
915 by (smt (verit) grewrite_cases_middle hr_in_rstar hrewrite.intros(11) hrewrite.intros(7) hrewrite.intros(8)) |
870 by (smt (verit) grewrite_cases_middle hr_in_rstar hrewrite.intros(11) hrewrite.intros(7) hrewrite.intros(8)) |
1114 shows "r h\<leadsto>* r' \<Longrightarrow> rder c r h\<leadsto>* rder c r'" |
1069 shows "r h\<leadsto>* r' \<Longrightarrow> rder c r h\<leadsto>* rder c r'" |
1115 apply(induct rule : hrewrites.induct) |
1070 apply(induct rule : hrewrites.induct) |
1116 apply simp |
1071 apply simp |
1117 by (meson hreal_trans interleave1) |
1072 by (meson hreal_trans interleave1) |
1118 |
1073 |
|
1074 |
|
1075 |
|
1076 lemma inside_simp_seq_nullable: |
|
1077 shows |
|
1078 "\<And>r1 r2. |
|
1079 \<lbrakk>rsimp (rder x (rsimp r1)) = rsimp (rder x r1); rsimp (rder x (rsimp r2)) = rsimp (rder x r2); |
|
1080 rnullable r1\<rbrakk> |
|
1081 \<Longrightarrow> rsimp (rder x (rsimp_SEQ (rsimp r1) (rsimp r2))) = |
|
1082 rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp (rder x r1)) (rsimp r2), rsimp (rder x r2)]) {})" |
|
1083 apply(case_tac "rsimp r1 = RONE") |
|
1084 apply(simp) |
|
1085 apply(subst basic_rsimp_SEQ_property1) |
|
1086 apply (simp add: idem_after_simp1) |
|
1087 apply(case_tac "rsimp r1 = RZERO") |
|
1088 using basic_regex_property1 apply blast |
|
1089 apply(case_tac "rsimp r2 = RZERO") |
|
1090 apply (simp add: basic_rsimp_SEQ_property3) |
|
1091 apply(subst idiot2) |
|
1092 apply simp+ |
|
1093 apply(subgoal_tac "rnullable (rsimp r1)") |
|
1094 apply simp |
|
1095 using rsimp_idem apply presburger |
|
1096 using der_simp_nullability by presburger |
|
1097 |
1119 |
1098 |
1120 |
1099 |
1121 lemma inside_simp_removal: |
1100 lemma inside_simp_removal: |
1122 shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)" |
1101 shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)" |
1123 apply(induct r) |
1102 apply(induct r) |