diff -r 0497408a3598 -r 94604a5fd271 thys3/src/BasicIdentities.thy --- a/thys3/src/BasicIdentities.thy Wed Jul 13 08:35:09 2022 +0100 +++ b/thys3/src/BasicIdentities.thy Wed Jul 13 08:35:45 2022 +0100 @@ -9,6 +9,7 @@ | RSEQ rrexp rrexp | RALTS "rrexp list" | RSTAR rrexp +| RNTIMES rrexp nat abbreviation "RALT r1 r2 \ RALTS [r1, r2]" @@ -23,7 +24,7 @@ | "rnullable (RALTS rs) = (\r \ set rs. rnullable r)" | "rnullable (RSEQ r1 r2) = (rnullable r1 \ rnullable r2)" | "rnullable (RSTAR r) = True" - +| "rnullable (RNTIMES r n) = (if n = 0 then True else rnullable r)" fun rder :: "char \ rrexp \ rrexp" @@ -36,8 +37,8 @@ (if rnullable r1 then RALT (RSEQ (rder c r1) r2) (rder c r2) else RSEQ (rder c r1) r2)" -| "rder c (RSTAR r) = RSEQ (rder c r) (RSTAR r)" - +| "rder c (RSTAR r) = RSEQ (rder c r) (RSTAR r)" +| "rder c (RNTIMES r n) = (if n = 0 then RZERO else RSEQ (rder c r) (RNTIMES r (n - 1)))" fun rders :: "rrexp \ string \ rrexp" @@ -191,6 +192,7 @@ | "rsize (RALTS rs) = Suc (sum_list (map rsize rs))" | "rsize (RSEQ r1 r2) = Suc (rsize r1 + rsize r2)" | "rsize (RSTAR r) = Suc (rsize r)" +| "rsize (RNTIMES r n) = Suc (rsize r) + n" abbreviation rsizes where "rsizes rs \ sum_list (map rsize rs)" @@ -237,7 +239,9 @@ apply(case_tac r2) apply simp_all apply(case_tac r2) - apply simp_all + apply simp_all + apply(case_tac r2) + apply simp_all done lemma ralts_cap_mono: @@ -329,7 +333,9 @@ apply(case_tac r2) apply simp_all apply(case_tac r2) - apply simp_all + apply simp_all +apply(case_tac r2) + apply simp_all done lemma rders__onechar: @@ -374,7 +380,7 @@ | "good (RSEQ _ RZERO) = False" | "good (RSEQ r1 r2) = (good r1 \ good r2)" | "good (RSTAR r) = True" - +| "good (RNTIMES r n) = True" lemma k0a: shows "rflts [RALTS rs] = rs" @@ -424,9 +430,8 @@ apply (metis flts1 good.simps(5) good.simps(6) k0a neq_Nil_conv) apply (metis flts1 good.simps(5) good.simps(6) k0a neq_Nil_conv) apply fastforce - apply(simp) - done - + apply(simp) + by simp lemma flts3: @@ -458,7 +463,9 @@ apply(case_tac r2) apply(simp_all) apply(case_tac r2) - apply(simp_all) + apply(simp_all) +apply(case_tac r2) + apply(simp_all) done lemma rsize0: @@ -509,7 +516,7 @@ apply(induct rs ) apply(auto) apply (metis list.set_intros(1) nn1qq nonalt.elims(3)) - apply (metis nonalt.elims(2) nonnested.simps(3) nonnested.simps(4) nonnested.simps(5) nonnested.simps(6) nonnested.simps(7)) + apply (metis nonalt.elims(2) nonnested.simps(3) nonnested.simps(4) nonnested.simps(5) nonnested.simps(6) nonnested.simps(7) nonnested.simps(8)) using bbbbs1 apply fastforce by (metis bbbbs1 list.set_intros(2) nn1qq) @@ -552,8 +559,8 @@ apply(case_tac "\bs. rsimp r1 = RONE") apply(auto)[1] using idiot apply fastforce - using idiot2 nonnested.simps(11) apply presburger - by (metis (mono_tags, lifting) Diff_empty image_iff list.set_map nn1bb nn1c rdistinct_set_equality1) + apply (simp add: idiot2) + by (metis (mono_tags, lifting) image_iff list.set_map nn1bb nn1c rdistinct_set_equality) lemma nonalt_flts_rd: shows "\xa \ set (rdistinct (rflts (map rsimp rs)) {})\ @@ -603,6 +610,7 @@ apply (simp add: elem_smaller_than_set) by (metis Diff_empty flts3 rdistinct_set_equality1) +thm Diff_empty flts3 rdistinct_set_equality1 lemma good1: shows "good (rsimp a) \ rsimp a = RZERO" @@ -632,8 +640,9 @@ apply blast apply fastforce using less_add_Suc2 apply blast - using less_iff_Suc_add by blast - + using less_iff_Suc_add apply blast + using good.simps(45) rsimp.simps(7) by presburger + fun @@ -645,28 +654,51 @@ | "RL (RSEQ r1 r2) = (RL r1) ;; (RL r2)" | "RL (RALTS rs) = (\ (set (map RL rs)))" | "RL (RSTAR r) = (RL r)\" +| "RL (RNTIMES r n) = (RL r) ^^ n" +lemma pow_rempty_iff: + shows "[] \ (RL r) ^^ n \ (if n = 0 then True else [] \ (RL r))" + by (induct n) (auto simp add: Sequ_def) lemma RL_rnullable: shows "rnullable r = ([] \ RL r)" apply(induct r) - apply(auto simp add: Sequ_def) + apply(auto simp add: Sequ_def pow_rempty_iff) done +lemma concI_if_Nil1: "[] \ A \ xs : B \ xs \ A ;; B" +by (metis append_Nil concI) + + +lemma empty_pow_add: + fixes A::"string set" + assumes "[] \ A" "s \ A ^^ n" + shows "s \ A ^^ (n + m)" + using assms + apply(induct m arbitrary: n) + apply(auto simp add: Sequ_def) + done + +(* +lemma der_pow: + shows "Der c (A ^^ n) = (if n = 0 then {} else (Der c A) ;; (A ^^ (n - 1)))" + apply(induct n arbitrary: A) + apply(auto) + by (smt (verit, best) Suc_pred concE concI concI_if_Nil2 conc_pow_comm lang_pow.simps(2)) +*) + lemma RL_rder: shows "RL (rder c r) = Der c (RL r)" apply(induct r) - apply(auto simp add: Sequ_def Der_def) + apply(auto simp add: Sequ_def Der_def)[5] apply (metis append_Cons) using RL_rnullable apply blast apply (metis append_eq_Cons_conv) apply (metis append_Cons) - apply (metis RL_rnullable append_eq_Cons_conv) - apply (metis Star.step append_Cons) - using Star_decomp by auto - - - + apply (metis RL_rnullable append_eq_Cons_conv) + apply simp + apply(simp) + done lemma RL_rsimp_RSEQ: shows "RL (rsimp_SEQ r1 r2) = (RL r1 ;; RL r2)" @@ -843,12 +875,14 @@ apply(case_tac "rsimp aa") apply simp+ apply (metis no_alt_short_list_after_simp no_further_dB_after_simp) - by simp + apply(simp) + apply(simp) + done lemma identity_wwo0: shows "rsimp (rsimp_ALTs (RZERO # rs)) = rsimp (rsimp_ALTs rs)" - by (metis idem_after_simp1 list.exhaust list.simps(8) list.simps(9) rflts.simps(2) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3)) - + apply (metis idem_after_simp1 list.exhaust list.simps(8) list.simps(9) rflts.simps(2) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3)) + done lemma distinct_removes_last: shows "\a \ set as\ @@ -994,12 +1028,15 @@ apply(subgoal_tac "\r \ set( rflts (map rsimp rsa)). good r") apply(case_tac "rdistinct (rflts (map rsimp rsa)) {}") - apply simp - apply(case_tac "listb") - apply simp+ - apply (metis Cons_eq_appendI good1_flatten rflts.simps(3) rsimp.simps(2) rsimp_ALTs.simps(3)) - by (metis (mono_tags, lifting) flts3 good1 image_iff list.set_map) - + apply simp + apply auto[1] + apply simp + apply(simp) + apply(case_tac "lista") + apply simp_all + + apply (metis append_Cons append_Nil good1_flatten rflts.simps(2) rsimp.simps(2) rsimp_ALTs.elims) + by (metis (no_types, opaque_lifting) append_Cons append_Nil good1_flatten rflts.simps(2) rsimp.simps(2) rsimp_ALTs.elims) lemma last_elem_out: shows "\x \ set xs; x \ rset \ \ rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]" @@ -1127,8 +1164,9 @@ apply fastforce apply fastforce apply fastforce - by fastforce - + apply fastforce + by simp + lemma distinct_removes_duplicate_flts: shows " a \ set rsa @@ -1143,29 +1181,19 @@ apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} = rdistinct (rflts (map rsimp rsa @ [RONE])) {}") apply (simp only:) - apply(subst flts_keeps1) - apply (metis distinct_removes_last(1) rflts_def_idiot2 rrexp.simps(20) rrexp.simps(6)) + apply(subst flts_keeps1) + apply (metis distinct_removes_last(1) flts_append in_set_conv_decomp rflts.simps(4)) apply presburger apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} = rdistinct ((rflts (map rsimp rsa)) @ [RCHAR x]) {}") apply (simp only:) - prefer 2 - apply (metis flts_keeps_others rrexp.distinct(21) rrexp.distinct(3)) - apply (metis distinct_removes_last(1) rflts_def_idiot2 rrexp.distinct(21) rrexp.distinct(3)) - - apply (metis distinct_removes_last(1) flts_keeps_others rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(5)) - prefer 2 - apply (metis distinct_removes_last(1) flts_keeps_others flts_removes0 rflts_def_idiot2 rrexp.distinct(29)) - apply(subgoal_tac "rflts (map rsimp rsa @ [rsimp a]) = rflts (map rsimp rsa) @ x") - prefer 2 - apply (simp add: rflts_spills_last) - apply(subgoal_tac "\ r \ set x. r \ set (rflts (map rsimp rsa))") - prefer 2 - apply (metis (mono_tags, lifting) image_iff image_set spilled_alts_contained) - apply (metis rflts_spills_last) - by (metis distinct_removes_list spilled_alts_contained) - - + prefer 2 + apply (metis flts_append rflts.simps(1) rflts.simps(5)) + apply (metis distinct_removes_last(1) rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(3)) + apply (metis distinct_removes_last(1) flts_append rflts.simps(1) rflts.simps(6) rflts_def_idiot2 rrexp.distinct(31) rrexp.distinct(5)) + apply (metis distinct_removes_list rflts_spills_last spilled_alts_contained) + apply (metis distinct_removes_last(1) flts_append good.simps(1) good.simps(44) rflts.simps(1) rflts.simps(7) rflts_def_idiot2 rrexp.distinct(37)) + by (metis distinct_removes_last(1) flts_append rflts.simps(1) rflts.simps(8) rflts_def_idiot2 rrexp.distinct(11) rrexp.distinct(39)) (*some basic facts about rsimp*)