diff -r 56057198e4f5 -r 70c10dc41606 thys3/ClosedForms.thy --- a/thys3/ClosedForms.thy Fri May 26 08:09:30 2023 +0100 +++ b/thys3/ClosedForms.thy Fri May 26 08:10:17 2023 +0100 @@ -1,9 +1,20 @@ theory ClosedForms - imports "HarderProps" + imports "BasicIdentities" begin +lemma flts_middle0: + shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)" + apply(induct rsa) + apply simp + by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) + +lemma simp_flatten_aux0: + shows "rsimp (RALTS rs) = rsimp (RALTS (map rsimp rs))" + by (metis append_Nil head_one_more_simp identity_wwo0 list.simps(8) rdistinct.simps(1) rflts.simps(1) rsimp.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(3) simp_flatten spawn_simp_rsimpalts) + + inductive hrewrite:: "rrexp \ rrexp \ bool" ("_ h\ _" [99, 99] 99) where @@ -56,8 +67,44 @@ by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2) +lemma simp_removes_duplicate1: + shows " a \ set rsa \ rsimp (RALTS (rsa @ [a])) = rsimp (RALTS (rsa))" +and " rsimp (RALTS (a1 # rsa @ [a1])) = rsimp (RALTS (a1 # rsa))" + apply(induct rsa arbitrary: a1) + apply simp + apply simp + prefer 2 + apply(case_tac "a = aa") + apply simp + apply simp + apply (metis Cons_eq_appendI Cons_eq_map_conv distinct_removes_duplicate_flts list.set_intros(2)) + apply (metis append_Cons append_Nil distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9)) + by (metis (mono_tags, lifting) append_Cons distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9) map_append rsimp.simps(2)) + +lemma simp_removes_duplicate2: + shows "a \ set rsa \ rsimp (RALTS (rsa @ [a] @ rsb)) = rsimp (RALTS (rsa @ rsb))" + apply(induct rsb arbitrary: rsa) + apply simp + using distinct_removes_duplicate_flts apply auto[1] + by (metis append.assoc head_one_more_simp rsimp.simps(2) simp_flatten simp_removes_duplicate1(1)) +lemma simp_removes_duplicate3: + shows "a \ set rsa \ rsimp (RALTS (rsa @ a # rsb)) = rsimp (RALTS (rsa @ rsb))" + using simp_removes_duplicate2 by auto +(* +lemma distinct_removes_middle4: + shows "a \ set rsa \ rdistinct (rsa @ [a] @ rsb) rset = rdistinct (rsa @ rsb) rset" + using distinct_removes_middle(1) by fastforce +*) + +(* +lemma distinct_removes_middle_list: + shows "\a \ set x. a \ set rsa \ rdistinct (rsa @ x @ rsb) rset = rdistinct (rsa @ rsb) rset" + apply(induct x) + apply simp + by (simp add: distinct_removes_middle3) +*) inductive frewrite:: "rrexp list \ rrexp list \ bool" ("_ \f _" [10, 10] 10) where @@ -212,6 +259,11 @@ using grewrites_append apply blast by (meson greal_trans grewrites.simps grewrites_concat) +fun alt_set:: "rrexp \ rrexp set" + where + "alt_set (RALTS rs) = set rs \ \ (alt_set ` (set rs))" +| "alt_set r = {r}" + lemma grewrite_cases_middle: shows "rs1 \g rs2 \ @@ -226,6 +278,216 @@ by blast +lemma good_singleton: + shows "good a \ nonalt a \ rflts [a] = [a]" + using good.simps(1) k0b by blast + + + + + + + +lemma all_that_same_elem: + shows "\ a \ rset; rdistinct rs {a} = []\ + \ rdistinct (rs @ rsb) rset = rdistinct rsb rset" + apply(induct rs) + apply simp + apply(subgoal_tac "aa = a") + apply simp + by (metis empty_iff insert_iff list.discI rdistinct.simps(2)) + +lemma distinct_early_app1: + shows "rset1 \ rset \ rdistinct rs rset = rdistinct (rdistinct rs rset1) rset" + apply(induct rs arbitrary: rset rset1) + apply simp + apply simp + apply(case_tac "a \ rset1") + apply simp + apply(case_tac "a \ rset") + apply simp+ + + apply blast + apply(case_tac "a \ rset1") + apply simp+ + apply(case_tac "a \ rset") + apply simp + apply (metis insert_subsetI) + apply simp + by (meson insert_mono) + + +lemma distinct_early_app: + shows " rdistinct (rs @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset" + apply(induct rsb) + apply simp + using distinct_early_app1 apply blast + by (metis distinct_early_app1 distinct_once_enough empty_subsetI) + + +lemma distinct_eq_interesting1: + shows "a \ rset \ rdistinct (rs @ rsb) rset = rdistinct (rdistinct (a # rs) {} @ rsb) rset" + apply(subgoal_tac "rdistinct (rdistinct (a # rs) {} @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset") + apply(simp only:) + using distinct_early_app apply blast + by (metis append_Cons distinct_early_app rdistinct.simps(2)) + + + +lemma good_flatten_aux_aux1: + shows "\ size rs \2; +\r \ set rs. good r \ r \ RZERO \ nonalt r; \r \ set rsb. good r \ r \ RZERO \ nonalt r \ + \ rdistinct (rs @ rsb) rset = + rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset" + apply(induct rs arbitrary: rset) + apply simp + apply(case_tac "a \ rset") + apply simp + apply(case_tac "rdistinct rs {a}") + apply simp + apply(subst good_singleton) + apply force + apply simp + apply (meson all_that_same_elem) + apply(subgoal_tac "rflts [rsimp_ALTs (a # rdistinct rs {a})] = a # rdistinct rs {a} ") + prefer 2 + using k0a rsimp_ALTs.simps(3) apply presburger + apply(simp only:) + apply(subgoal_tac "rdistinct (rs @ rsb) rset = rdistinct ((rdistinct (a # rs) {}) @ rsb) rset ") + apply (metis insert_absorb insert_is_Un insert_not_empty rdistinct.simps(2)) + apply (meson distinct_eq_interesting1) + apply simp + apply(case_tac "rdistinct rs {a}") + prefer 2 + apply(subgoal_tac "rsimp_ALTs (a # rdistinct rs {a}) = RALTS (a # rdistinct rs {a})") + apply(simp only:) + apply(subgoal_tac "a # rdistinct (rs @ rsb) (insert a rset) = + rdistinct (rflts [RALTS (a # rdistinct rs {a})] @ rsb) rset") + apply simp + apply (metis append_Cons distinct_early_app empty_iff insert_is_Un k0a rdistinct.simps(2)) + using rsimp_ALTs.simps(3) apply presburger + by (metis Un_insert_left append_Cons distinct_early_app empty_iff good_singleton rdistinct.simps(2) rsimp_ALTs.simps(2) sup_bot_left) + + + + + +lemma good_flatten_aux_aux: + shows "\\a aa lista list. rs = a # list \ list = aa # lista; +\r \ set rs. good r \ r \ RZERO \ nonalt r; \r \ set rsb. good r \ r \ RZERO \ nonalt r \ + \ rdistinct (rs @ rsb) rset = + rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset" + apply(erule exE)+ + apply(subgoal_tac "size rs \ 2") + apply (metis good_flatten_aux_aux1) + by (simp add: Suc_leI length_Cons less_add_Suc1) + + + +lemma good_flatten_aux: + shows " \\r\set rs. good r \ r = RZERO; \r\set rsa . good r \ r = RZERO; + \r\set rsb. good r \ r = RZERO; + rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (rsa @ rs @ rsb)) {}); + rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = + rsimp_ALTs (rdistinct (rflts (rsa @ [rsimp (RALTS rs)] @ rsb)) {}); + map rsimp rsa = rsa; map rsimp rsb = rsb; map rsimp rs = rs; + rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = + rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa)); + rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} = + rdistinct (rflts rsa) {} @ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))\ + \ rdistinct (rflts rs @ rflts rsb) rset = + rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) rset" + apply simp + apply(case_tac "rflts rs ") + apply simp + apply(case_tac "list") + apply simp + apply(case_tac "a \ rset") + apply simp + apply (metis append.left_neutral append_Cons equals0D k0b list.set_intros(1) nonalt_flts_rd qqq1 rdistinct.simps(2)) + apply simp + apply (metis Un_insert_left append_Cons append_Nil ex_in_conv flts_single1 insertI1 list.simps(15) nonalt_flts_rd nonazero.elims(3) qqq1 rdistinct.simps(2) sup_bot_left) + apply(subgoal_tac "\r \ set (rflts rs). good r \ r \ RZERO \ nonalt r") + prefer 2 + apply (metis Diff_empty flts3 nonalt_flts_rd qqq1 rdistinct_set_equality1) + apply(subgoal_tac "\r \ set (rflts rsb). good r \ r \ RZERO \ nonalt r") + prefer 2 + apply (metis Diff_empty flts3 good.simps(1) nonalt_flts_rd rdistinct_set_equality1) + by (smt (verit, ccfv_threshold) good_flatten_aux_aux) + + + + +lemma good_flatten_middle: + shows "\\r \ set rs. good r \ r = RZERO; \r \ set rsa. good r \ r = RZERO; \r \ set rsb. good r \ r = RZERO\ \ +rsimp (RALTS (rsa @ rs @ rsb)) = rsimp (RALTS (rsa @ [RALTS rs] @ rsb))" + apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ +map rsimp rs @ map rsimp rsb)) {})") + prefer 2 + apply simp + apply(simp only:) + apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ +[rsimp (RALTS rs)] @ map rsimp rsb)) {})") + prefer 2 + apply simp + apply(simp only:) + apply(subgoal_tac "map rsimp rsa = rsa") + prefer 2 + apply (metis map_idI rsimp.simps(3) test) + apply(simp only:) + apply(subgoal_tac "map rsimp rsb = rsb") + prefer 2 + apply (metis map_idI rsimp.simps(3) test) + apply(simp only:) + apply(subst k00)+ + apply(subgoal_tac "map rsimp rs = rs") + apply(simp only:) + prefer 2 + apply (metis map_idI rsimp.simps(3) test) + apply(subgoal_tac "rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = +rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa))") + apply(simp only:) + prefer 2 + using rdistinct_concat_general apply blast + apply(subgoal_tac "rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} = +rdistinct (rflts rsa) {} @ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))") + apply(simp only:) + prefer 2 + using rdistinct_concat_general apply blast + apply(subgoal_tac "rdistinct (rflts rs @ rflts rsb) (set (rflts rsa)) = + rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))") + apply presburger + using good_flatten_aux by blast + + +lemma simp_flatten3: + shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))" + apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = + rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) ") + prefer 2 + apply (metis append.left_neutral append_Cons list.simps(9) map_append simp_flatten_aux0) + apply (simp only:) + apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = +rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb))") + prefer 2 + apply (metis map_append simp_flatten_aux0) + apply(simp only:) + apply(subgoal_tac "rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb)) = + rsimp (RALTS (map rsimp rsa @ [RALTS (map rsimp rs)] @ map rsimp rsb))") + + apply (metis (no_types, lifting) head_one_more_simp map_append simp_flatten_aux0) + apply(subgoal_tac "\r \ set (map rsimp rsa). good r \ r = RZERO") + apply(subgoal_tac "\r \ set (map rsimp rs). good r \ r = RZERO") + apply(subgoal_tac "\r \ set (map rsimp rsb). good r \ r = RZERO") + + using good_flatten_middle apply presburger + + apply (simp add: good1) + apply (simp add: good1) + apply (simp add: good1) + + done + @@ -277,8 +539,10 @@ apply (simp add: frewrites_alt) apply (simp add: frewrites_cons) apply (simp add: frewrites_append) - by (simp add: frewrites_cons) - + apply (simp add: frewrites_cons) + apply (auto simp add: frewrites_cons) + using frewrite.intros(1) many_steps_later by blast + lemma gstar0: shows "rsa @ (rdistinct rs (set rsa)) \g* rsa @ (rdistinct rs (insert RZERO (set rsa)))" @@ -380,7 +644,8 @@ apply(induct r) apply simp+ apply (metis list.set_intros(1)) - by blast + apply blast + by simp @@ -604,8 +869,39 @@ by (metis append.right_neutral grewrite.intros(2) grewrite_simpalts rsimp_ALTs.simps(2) simp_der_flts) +lemma basic_regex_property1: + shows "rnullable r \ rsimp r \ RZERO" + apply(induct r rule: rsimp.induct) + apply(auto) + apply (metis idiot idiot2 rrexp.distinct(5)) + by (metis der_simp_nullability rnullable.simps(1) rnullable.simps(4) rsimp.simps(2)) +lemma inside_simp_seq_nullable: + shows +"\r1 r2. + \rsimp (rder x (rsimp r1)) = rsimp (rder x r1); rsimp (rder x (rsimp r2)) = rsimp (rder x r2); + rnullable r1\ + \ rsimp (rder x (rsimp_SEQ (rsimp r1) (rsimp r2))) = + rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp (rder x r1)) (rsimp r2), rsimp (rder x r2)]) {})" + apply(case_tac "rsimp r1 = RONE") + apply(simp) + apply(subst basic_rsimp_SEQ_property1) + apply (simp add: idem_after_simp1) + apply(case_tac "rsimp r1 = RZERO") + + using basic_regex_property1 apply blast + apply(case_tac "rsimp r2 = RZERO") + + apply (simp add: basic_rsimp_SEQ_property3) + apply(subst idiot2) + apply simp+ + apply(subgoal_tac "rnullable (rsimp r1)") + apply simp + using rsimp_idem apply presburger + using der_simp_nullability by presburger + + lemma grewrite_ralts: shows "rs \g rs' \ RALTS rs h\* RALTS rs'" @@ -754,7 +1050,7 @@ apply (meson flts_gstar greal_trans grewrites_ralts_rsimpalts gstar_rdistinct) apply (simp add: grewrites_ralts hrewrites_list) - by simp + by simp_all lemma interleave_aux1: shows " RALT (RSEQ RZERO r1) r h\* r" @@ -815,30 +1111,6 @@ -lemma inside_simp_seq_nullable: - shows -"\r1 r2. - \rsimp (rder x (rsimp r1)) = rsimp (rder x r1); rsimp (rder x (rsimp r2)) = rsimp (rder x r2); - rnullable r1\ - \ rsimp (rder x (rsimp_SEQ (rsimp r1) (rsimp r2))) = - rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp (rder x r1)) (rsimp r2), rsimp (rder x r2)]) {})" - apply(case_tac "rsimp r1 = RONE") - apply(simp) - apply(subst basic_rsimp_SEQ_property1) - apply (simp add: idem_after_simp1) - apply(case_tac "rsimp r1 = RZERO") - using basic_regex_property1 apply blast - apply(case_tac "rsimp r2 = RZERO") - apply (simp add: basic_rsimp_SEQ_property3) - apply(subst idiot2) - apply simp+ - apply(subgoal_tac "rnullable (rsimp r1)") - apply simp - using rsimp_idem apply presburger - using der_simp_nullability by presburger - - - lemma inside_simp_removal: shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)" apply(induct r) @@ -852,7 +1124,7 @@ apply(subgoal_tac "rder x (RALTS xa) h\* rder x (rsimp (RALTS xa))") using hrewrites_simpeq apply presburger using interleave_star1 simp_hrewrites apply presburger - by simp + by simp_all @@ -887,16 +1159,14 @@ using rders_simp_same_simpders rsimp_idem by auto lemma repeated_altssimp: - shows "\r \ set rs. rsimp r = r \ - rsimp (rsimp_ALTs (rdistinct (rflts rs) {})) = + shows "\r \ set rs. rsimp r = r \ rsimp (rsimp_ALTs (rdistinct (rflts rs) {})) = rsimp_ALTs (rdistinct (rflts rs) {})" by (metis map_idI rsimp.simps(2) rsimp_idem) lemma alts_closed_form: - shows "rsimp (rders_simp (RALTS rs) s) = - rsimp (RALTS (map (\r. rders_simp r s) rs))" + shows "rsimp (rders_simp (RALTS rs) s) = rsimp (RALTS (map (\r. rders_simp r s) rs))" apply(induct s rule: rev_induct) apply simp apply simp @@ -981,11 +1251,15 @@ apply simp+ using created_by_seq.cases apply blast - - apply (meson created_by_seq.cases rrexp.distinct(19) rrexp.distinct(21)) - apply (metis created_by_seq.simps rder.simps(5)) - apply (smt (verit, ccfv_threshold) created_by_seq.simps list.set_intros(1) list.simps(8) list.simps(9) rder.simps(4) rrexp.distinct(25) rrexp.inject(3)) - using created_by_seq.intros(1) by force + apply(auto) + apply (meson created_by_seq.cases rrexp.distinct(23) rrexp.distinct(25)) + using created_by_seq.simps apply blast + apply (meson created_by_seq.simps) + using created_by_seq.intros(1) apply blast + apply (metis (no_types, lifting) created_by_seq.simps k0a list.set_intros(1) list.simps(8) list.simps(9) rrexp.distinct(31)) + apply (simp add: created_by_seq.intros(1)) + using created_by_seq.simps apply blast + by (simp add: created_by_seq.intros(1)) lemma createdbyseq_left_creatable: shows "created_by_seq (RALT r1 r2) \ created_by_seq r1" @@ -1030,16 +1304,6 @@ by fastforce -fun vsuf :: "char list \ rrexp \ char list list" where -"vsuf [] _ = []" -|"vsuf (c#cs) r1 = (if (rnullable r1) then (vsuf cs (rder c r1)) @ [c # cs] - else (vsuf cs (rder c r1)) - ) " - - - - - lemma vsuf_prop1: shows "vsuf (xs @ [x]) r = (if (rnullable (rders r xs)) then [x] # (map (\s. s @ [x]) (vsuf xs r) ) @@ -1071,75 +1335,44 @@ apply simp by (simp add: rders_append) -thm sfau_idem_der -lemma oneCharvsuf: - shows "breakHead [rder x (RSEQ r1 r2)] = RSEQ (rder x r1) r2 # map (rders r2) (vsuf [x] r1)" - by simp - - -lemma vsuf_compose2: - shows "(map (rders r2) (vsuf [x] (rders r1 xs))) @ map (rder x) (map (rders r2) (vsuf xs r1)) = - map (rders r2) (vsuf (xs @ [x]) r1)" -proof(induct xs arbitrary: r1) - case Nil - then show ?case - by simp -next - case (Cons a xs) - have "rnullable (rders r1 xs) \ map (rders r2) (vsuf [x] (rders r1 (a # xs))) @ map (rder x) (map (rders r2) (vsuf (a # xs) r1)) = - map (rders r2) (vsuf ((a # xs) @ [x]) r1)" - proof - assume nullableCond: "rnullable (rders r1 xs)" - have "rnullable r1 \ rder x (rders (rder a r2) xs) = rders (rder a r2) (xs @ [x])" - by (simp add: rders_append) - show " map (rders r2) (vsuf [x] (rders r1 (a # xs))) @ map (rder x) (map (rders r2) (vsuf (a # xs) r1)) = - map (rders r2) (vsuf ((a # xs) @ [x]) r1)" - using \rnullable r1 \ rder x (rders (rder a r2) xs) = rders (rder a r2) (xs @ [x])\ local.Cons by auto - qed - then have "\ rnullable (rders r1 xs) \ map (rders r2) (vsuf [x] (rders r1 (a # xs))) @ map (rder x) (map (rders r2) (vsuf (a # xs) r1)) = - map (rders r2) (vsuf ((a # xs) @ [x]) r1)" - apply simp - by (smt (verit, ccfv_threshold) append_Cons append_Nil list.map_comp list.simps(8) list.simps(9) local.Cons rders.simps(1) rders.simps(2) rders_append vsuf.simps(1) vsuf.simps(2)) - then show ?case - using \rnullable (rders r1 xs) \ map (rders r2) (vsuf [x] (rders r1 (a # xs))) @ map (rder x) (map (rders r2) (vsuf (a # xs) r1)) = map (rders r2) (vsuf ((a # xs) @ [x]) r1)\ by blast -qed lemma seq_sfau0: shows "sflat_aux (rders (RSEQ r1 r2) s) = (RSEQ (rders r1 s) r2) # (map (rders r2) (vsuf s r1)) " -proof(induct s rule: rev_induct) - case Nil - then show ?case - by simp -next - case (snoc x xs) - then have LHS1:"sflat_aux (rders (RSEQ r1 r2) (xs @ [x])) = sflat_aux (rder x (rders (RSEQ r1 r2) xs)) " - by (simp add: rders_append) - then have LHS1A: "... = breakHead (map (rder x) (sflat_aux (rders (RSEQ r1 r2) xs)))" - using recursively_derseq sfau_idem_der by auto - then have LHS1B: "... = breakHead (map (rder x) (RSEQ (rders r1 xs) r2 # map (rders r2) (vsuf xs r1)))" - using snoc by auto - then have LHS1C: "... = breakHead (rder x (RSEQ (rders r1 xs) r2) # map (rder x) (map (rders r2) (vsuf xs r1)))" - by simp - then have LHS1D: "... = breakHead [rder x (RSEQ (rders r1 xs) r2)] @ map (rder x) (map (rders r2) (vsuf xs r1))" - by simp - then have LHS1E: "... = RSEQ (rder x (rders r1 xs)) r2 # (map (rders r2) (vsuf [x] (rders r1 xs))) @ map (rder x) (map (rders r2) (vsuf xs r1))" - by force - then have LHS1F: "... = RSEQ (rder x (rders r1 xs)) r2 # (map (rders r2) (vsuf (xs @ [x]) r1))" - using vsuf_compose2 by blast - then have LHS1G: "... = RSEQ (rders r1 (xs @ [x])) r2 # (map (rders r2) (vsuf (xs @ [x]) r1))" - using rders.simps(1) rders.simps(2) rders_append by presburger - then show ?case - using LHS1 LHS1A LHS1C LHS1D LHS1E LHS1F snoc by presburger -qed + apply(induct s rule: rev_induct) + apply simp + apply(subst rders_append)+ + apply(subgoal_tac "created_by_seq (rders (RSEQ r1 r2) xs)") + prefer 2 + using recursively_derseq1 apply blast + apply simp + apply(subst sfau_idem_der) + + apply blast + apply(case_tac "rnullable (rders r1 xs)") + apply simp + apply(subst vsuf_prop1) + apply simp + apply (simp add: rders_append) + apply simp + using vsuf_compose1 by blast + + + +thm sflat.elims + + + + + lemma sflat_rsimpeq: shows "created_by_seq r1 \ sflat_aux r1 = rs \ rsimp r1 = rsimp (RALTS rs)" apply(induct r1 arbitrary: rs rule: created_by_seq.induct) @@ -1225,8 +1458,7 @@ lemma seq_closed_form_variant: assumes "s \ []" shows "rders_simp (RSEQ r1 r2) s = - rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # - (map (rders_simp r2) (vsuf s r1))))" + rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # (map (rders_simp r2) (vsuf s r1))))" using assms q seq_closed_form by force @@ -1243,20 +1475,9 @@ "created_by_star (RSEQ ra (RSTAR rb))" | "\created_by_star r1; created_by_star r2\ \ created_by_star (RALT r1 r2)" - - -fun star_update :: "char \ rrexp \ char list list \ char list list" where -"star_update c r [] = []" -|"star_update c r (s # Ss) = (if (rnullable (rders r s)) - then (s@[c]) # [c] # (star_update c r Ss) - else (s@[c]) # (star_update c r Ss) )" - - -fun star_updates :: "char list \ rrexp \ char list list \ char list list" - where -"star_updates [] r Ss = Ss" -| "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)" - +fun hElem :: "rrexp \ rrexp list" where + "hElem (RALT r1 r2) = (hElem r1 ) @ (hElem r2)" +| "hElem r = [r]" lemma cbs_ders_cbs: @@ -1277,38 +1498,20 @@ - lemma hfau_pushin: - shows "created_by_star r \ hflat_aux (rder c r) = concat (map hflat_aux (map (rder c) (hflat_aux r)))" -proof(induct r rule: created_by_star.induct) - case (1 ra rb) - then show ?case by simp -next - case (2 r1 r2) - then have "created_by_star (rder c r1)" - using cbs_ders_cbs by blast - then have "created_by_star (rder c r2)" - using "2.hyps"(3) cbs_ders_cbs by auto - then show ?case - by (simp add: "2.hyps"(2) "2.hyps"(4)) - qed - -(*AALTS [a\x . b.c, b\x .c, c \x]*) -(*AALTS [a\x . b.c, AALTS [b\x .c, c\x]]*) - -lemma stupdates_append: shows -"star_updates (s @ [c]) r Ss = star_update c r (star_updates s r Ss)" - apply(induct s arbitrary: Ss) + shows "created_by_star r \ hflat_aux (rder c r) = concat (map hElem (map (rder c) (hflat_aux r)))" + apply(induct r rule: created_by_star.induct) apply simp + apply(subgoal_tac "created_by_star (rder c r1)") + prefer 2 + apply(subgoal_tac "created_by_star (rder c r2)") + using cbs_ders_cbs apply blast + using cbs_ders_cbs apply auto[1] apply simp done - - - - lemma stupdate_induct1: - shows " concat (map (hflat_aux \ (rder x \ (\s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) = + shows " concat (map (hElem \ (rder x \ (\s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) = map (\s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_update x r0 Ss)" apply(induct Ss) apply simp+ @@ -1317,11 +1520,8 @@ lemma stupdates_join_general: - shows "concat - (map hflat_aux (map (rder x) - (map (\s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 Ss))) - ) = - map (\s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates (xs @ [x]) r0 Ss)" + shows "concat (map hElem (map (rder x) (map (\s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 Ss)))) = + map (\s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates (xs @ [x]) r0 Ss)" apply(induct xs arbitrary: Ss) apply (simp) prefer 2 @@ -1341,14 +1541,16 @@ apply (simp add: star_ders_cbs) apply(subst hfau_pushin) apply simp - apply(subgoal_tac "concat (map hflat_aux (map (rder x) (hflat_aux (rders (RSEQ (rder c r0) (RSTAR r0)) xs)))) = - concat (map hflat_aux (map (rder x) ( map (\s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 [[c]])))) ") + apply(subgoal_tac "concat (map hElem (map (rder x) (hflat_aux (rders (RSEQ (rder c r0) (RSTAR r0)) xs)))) = + concat (map hElem (map (rder x) ( map (\s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 [[c]])))) ") apply(simp only:) prefer 2 apply presburger apply(subst stupdates_append[symmetric]) using stupdates_join_general by blast + + lemma starders_hfau_also1: shows "hflat_aux (rders (RSTAR r) (c # xs)) = map (\s1. RSEQ (rders r s1) (RSTAR r)) (star_updates xs r [[c]])" using star_hfau_induct by force @@ -1366,7 +1568,7 @@ apply simp apply (metis (no_types, lifting) append_Cons append_eq_append_conv2 gmany_steps_later greal_trans grewrite.intros(2) grewrites_append self_append_conv) apply simp - by simp + by simp_all @@ -1380,10 +1582,29 @@ lemma hfau_rsimpeq2: shows "created_by_star r \ rsimp r = rsimp ( (RALTS (hflat_aux r)))" - apply(induct rule: created_by_star.induct) + apply(induct r) + apply simp+ + + apply (metis rsimp_seq_equal1) + prefer 2 + apply simp + apply(case_tac x) + apply simp + apply(case_tac "list") apply simp - apply (metis rsimp.simps(6) rsimp_seq_equal1) - using cbs_hfau_rsimpeq1 hflat_aux.simps(1) by presburger + + apply (metis idem_after_simp1) + apply(case_tac "lista") + prefer 2 + apply (metis hflat_aux.simps(8) idem_after_simp1 list.simps(8) list.simps(9) rsimp.simps(2)) + apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux (RALT a aa)))") + apply simp + apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux a @ hflat_aux aa))") + using hflat_aux.simps(1) apply presburger + apply simp + using cbs_hfau_rsimpeq1 apply(fastforce) + by simp + lemma star_closed_form1: shows "rsimp (rders (RSTAR r0) (c#s)) = @@ -1427,8 +1648,11 @@ using hrewrites_simpeq srewritescf_alt1 apply fastforce using star_closed_form6_hrewrites by blast + + + lemma stupdate_nonempty: - shows "\s \ set Ss. s \ [] \ \s \ set (star_update c r Ss). s \ []" + shows "\s \ set Ss. s \ [] \ \s \ set (star_update c r Ss). s \ []" apply(induct Ss) apply simp apply(case_tac "rnullable (rders r a)") @@ -1454,12 +1678,518 @@ lemma star_closed_form: shows "rders_simp (RSTAR r0) (c#s) = rsimp ( RALTS ( (map (\s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))" - apply(induct s) + apply(case_tac s) apply simp apply (metis idem_after_simp1 rsimp.simps(1) rsimp.simps(6) rsimp_idem) using star_closed_form4 star_closed_form5 star_closed_form6 star_closed_form8 by presburger -unused_thms + + +fun nupdate :: "char \ rrexp \ (string * nat) option list \ (string * nat) option list" where + "nupdate c r [] = []" +| "nupdate c r (Some (s, Suc n) # Ss) = (if (rnullable (rders r s)) + then Some (s@[c], Suc n) # Some ([c], n) # (nupdate c r Ss) + else Some ((s@[c]), Suc n) # (nupdate c r Ss) + )" +| "nupdate c r (Some (s, 0) # Ss) = (if (rnullable (rders r s)) + then Some (s@[c], 0) # None # (nupdate c r Ss) + else Some ((s@[c]), 0) # (nupdate c r Ss) + ) " +| "nupdate c r (None # Ss) = (None # nupdate c r Ss)" + + +fun nupdates :: "char list \ rrexp \ (string * nat) option list \ (string * nat) option list" + where + "nupdates [] r Ss = Ss" +| "nupdates (c # cs) r Ss = nupdates cs r (nupdate c r Ss)" + +fun ntset :: "rrexp \ nat \ string \ (string * nat) option list" where + "ntset r (Suc n) (c # cs) = nupdates cs r [Some ([c], n)]" +| "ntset r 0 _ = [None]" +| "ntset r _ [] = []" + +inductive created_by_ntimes :: "rrexp \ bool" where + "created_by_ntimes RZERO" +| "created_by_ntimes (RSEQ ra (RNTIMES rb n))" +| "\created_by_ntimes r1; created_by_ntimes r2\ \ created_by_ntimes (RALT r1 r2)" +| "\created_by_ntimes r \ \ created_by_ntimes (RALT r RZERO)" + +fun highest_power_aux :: "(string * nat) option list \ nat \ nat" where + "highest_power_aux [] n = n" +| "highest_power_aux (None # rs) n = highest_power_aux rs n" +| "highest_power_aux (Some (s, n) # rs) m = highest_power_aux rs (max n m)" + +fun hpower :: "(string * nat) option list \ nat" where + "hpower rs = highest_power_aux rs 0" + + +lemma nupdate_mono: + shows " (highest_power_aux (nupdate c r optlist) m) \ (highest_power_aux optlist m)" + apply(induct optlist arbitrary: m) + apply simp + apply(case_tac a) + apply simp + apply(case_tac aa) + apply(case_tac b) + apply simp+ + done + +lemma nupdate_mono1: + shows "hpower (nupdate c r optlist) \ hpower optlist" + by (simp add: nupdate_mono) + + + +lemma cbn_ders_cbn: + shows "created_by_ntimes r \ created_by_ntimes (rder c r)" + apply(induct r rule: created_by_ntimes.induct) + apply simp + + using created_by_ntimes.intros(1) created_by_ntimes.intros(2) created_by_ntimes.intros(3) apply presburger + + apply (metis created_by_ntimes.simps rder.simps(5) rder.simps(7)) + using created_by_star.intros(1) created_by_star.intros(2) apply auto[1] + using created_by_ntimes.intros(1) created_by_ntimes.intros(3) apply auto[1] + by (metis (mono_tags, lifting) created_by_ntimes.simps list.simps(8) list.simps(9) rder.simps(1) rder.simps(4)) + +lemma ntimes_ders_cbn: + shows "created_by_ntimes (rders (RSEQ r' (RNTIMES r n)) s)" + apply(induct s rule: rev_induct) + apply simp + apply (simp add: created_by_ntimes.intros(2)) + apply(subst rders_append) + using cbn_ders_cbn by auto + +lemma always0: + shows "rders RZERO s = RZERO" + apply(induct s) + by simp+ + +lemma ntimes_ders_cbn1: + shows "created_by_ntimes (rders (RNTIMES r n) (c#s))" + apply(case_tac n) + apply simp + using always0 created_by_ntimes.intros(1) apply auto[1] + by (simp add: ntimes_ders_cbn) + + +lemma ntimes_hfau_pushin: + shows "created_by_ntimes r \ hflat_aux (rder c r) = concat (map hflat_aux (map (rder c) (hflat_aux r)))" + apply(induct r rule: created_by_ntimes.induct) + apply simp+ + done + + +abbreviation + "opterm r SN \ case SN of + Some (s, n) \ RSEQ (rders r s) (RNTIMES r n) + | None \ RZERO + + +" + +fun nonempty_string :: "(string * nat) option \ bool" where + "nonempty_string None = True" +| "nonempty_string (Some ([], n)) = False" +| "nonempty_string (Some (c#s, n)) = True" + + +lemma nupdate_nonempty: + shows "\\opt \ set Ss. nonempty_string opt \ \ \opt \ set (nupdate c r Ss). nonempty_string opt" + apply(induct c r Ss rule: nupdate.induct) + apply(auto) + apply (metis Nil_is_append_conv neq_Nil_conv nonempty_string.simps(3)) + by (metis Nil_is_append_conv neq_Nil_conv nonempty_string.simps(3)) + + + +lemma nupdates_nonempty: + shows "\\opt \ set Ss. nonempty_string opt \ \ \opt \ set (nupdates s r Ss). nonempty_string opt" + apply(induct s arbitrary: Ss) + apply simp + apply simp + using nupdate_nonempty by presburger + +lemma nullability1: shows "rnullable (rders r s) = rnullable (rders_simp r s)" + by (metis der_simp_nullability rders.simps(1) rders_simp.simps(1) rders_simp_same_simpders) + +lemma nupdate_induct1: + shows + "concat (map (hflat_aux \ (rder c \ (opterm r))) sl ) = + map (opterm r) (nupdate c r sl)" + apply(induct sl) + apply simp + apply(simp add: rders_append) + apply(case_tac "a") + apply simp+ + apply(case_tac "aa") + apply(case_tac "b") + apply(case_tac "rnullable (rders r ab)") + apply(subgoal_tac "rnullable (rders_simp r ab)") + apply simp + using rders.simps(1) rders.simps(2) rders_append apply presburger + using nullability1 apply blast + apply simp + using rders.simps(1) rders.simps(2) rders_append apply presburger + apply simp + using rders.simps(1) rders.simps(2) rders_append by presburger + + +lemma nupdates_join_general: + shows "concat (map hflat_aux (map (rder x) (map (opterm r) (nupdates xs r Ss)) )) = + map (opterm r) (nupdates (xs @ [x]) r Ss)" + apply(induct xs arbitrary: Ss) + apply (simp) + prefer 2 + apply auto[1] + using nupdate_induct1 by blast + + +lemma nupdates_join_general1: + shows "concat (map (hflat_aux \ (rder x) \ (opterm r)) (nupdates xs r Ss)) = + map (opterm r) (nupdates (xs @ [x]) r Ss)" + by (metis list.map_comp nupdates_join_general) + +lemma nupdates_append: shows +"nupdates (s @ [c]) r Ss = nupdate c r (nupdates s r Ss)" + apply(induct s arbitrary: Ss) + apply simp + apply simp + done + +lemma nupdates_mono: + shows "highest_power_aux (nupdates s r optlist) m \ highest_power_aux optlist m" + apply(induct s rule: rev_induct) + apply simp + apply(subst nupdates_append) + by (meson le_trans nupdate_mono) + +lemma nupdates_mono1: + shows "hpower (nupdates s r optlist) \ hpower optlist" + by (simp add: nupdates_mono) + + +(*"\r \ set (nupdates s r [Some ([c], n)]). r = None \( \s' m. r = Some (s', m) \ m \ n)"*) +lemma nupdates_mono2: + shows "hpower (nupdates s r [Some ([c], n)]) \ n" + by (metis highest_power_aux.simps(1) highest_power_aux.simps(3) hpower.simps max_nat.right_neutral nupdates_mono1) + +lemma hpow_arg_mono: + shows "m \ n \ highest_power_aux rs m \ highest_power_aux rs n" + apply(induct rs arbitrary: m n) + apply simp + apply(case_tac a) + apply simp + apply(case_tac aa) + apply simp + done + + +lemma hpow_increase: + shows "highest_power_aux (a # rs') m \ highest_power_aux rs' m" + apply(case_tac a) + apply simp + apply simp + apply(case_tac aa) + apply(case_tac b) + apply simp+ + apply(case_tac "Suc nat > m") + using hpow_arg_mono max.cobounded2 apply blast + using hpow_arg_mono max.cobounded2 by blast + +lemma hpow_append: + shows "highest_power_aux (rsa @ rsb) m = highest_power_aux rsb (highest_power_aux rsa m)" + apply (induct rsa arbitrary: rsb m) + apply simp + apply simp + apply(case_tac a) + apply simp + apply(case_tac aa) + apply simp + done + +lemma hpow_aux_mono: + shows "highest_power_aux (rsa @ rsb) m \ highest_power_aux rsb m" + apply(induct rsa arbitrary: rsb rule: rev_induct) + apply simp + apply simp + using hpow_increase order.trans by blast + + + + +lemma hpow_mono: + shows "hpower (rsa @ rsb) \ n \ hpower rsb \ n" + apply(induct rsb arbitrary: rsa) + apply simp + apply(subgoal_tac "hpower rsb \ n") + apply simp + apply (metis dual_order.trans hpow_aux_mono) + by (metis hpow_append hpow_increase hpower.simps nat_le_iff_add trans_le_add1) + + +lemma hpower_rs_elems_aux: + shows "highest_power_aux rs k \ n \ \r\set rs. r = None \ (\s' m. r = Some (s', m) \ m \ n)" +apply(induct rs k arbitrary: n rule: highest_power_aux.induct) + apply(auto) + by (metis dual_order.trans highest_power_aux.simps(1) hpow_append hpow_aux_mono linorder_le_cases max.absorb1 max.absorb2) + +lemma hpower_rs_elems: + shows "hpower rs \ n \ \r \ set rs. r = None \( \s' m. r = Some (s', m) \ m \ n)" + by (simp add: hpower_rs_elems_aux) + +lemma nupdates_elems_leqn: + shows "\r \ set (nupdates s r [Some ([c], n)]). r = None \( \s' m. r = Some (s', m) \ m \ n)" + by (meson hpower_rs_elems nupdates_mono2) + +lemma ntimes_hfau_induct: + shows "hflat_aux (rders (RSEQ (rder c r) (RNTIMES r n)) s) = + map (opterm r) (nupdates s r [Some ([c], n)])" + apply(induct s rule: rev_induct) + apply simp + apply(subst rders_append)+ + apply simp + apply(subst nupdates_append) + apply(subgoal_tac "created_by_ntimes (rders (RSEQ (rder c r) (RNTIMES r n)) xs)") + prefer 2 + apply (simp add: ntimes_ders_cbn) + apply(subst ntimes_hfau_pushin) + apply simp + apply(subgoal_tac "concat (map hflat_aux (map (rder x) (hflat_aux (rders (RSEQ (rder c r) (RNTIMES r n)) xs)))) = + concat (map hflat_aux (map (rder x) ( map (opterm r) (nupdates xs r [Some ([c], n)])))) ") + apply(simp only:) + prefer 2 + apply presburger + apply(subst nupdates_append[symmetric]) + using nupdates_join_general by blast + + +(*nupdates s r [Some ([c], n)]*) +lemma ntimes_ders_hfau_also1: + shows "hflat_aux (rders (RNTIMES r (Suc n)) (c # xs)) = map (opterm r) (nupdates xs r [Some ([c], n)])" + using ntimes_hfau_induct by force + + + +lemma hfau_rsimpeq2_ntimes: + shows "created_by_ntimes r \ rsimp r = rsimp ( (RALTS (hflat_aux r)))" + apply(induct r) + apply simp+ + + apply (metis rsimp_seq_equal1) + prefer 2 + apply simp + apply(case_tac x) + apply simp + apply(case_tac "list") + apply simp + + apply (metis idem_after_simp1) + apply(case_tac "lista") + prefer 2 + apply (metis hflat_aux.simps(8) idem_after_simp1 list.simps(8) list.simps(9) rsimp.simps(2)) + apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux (RALT a aa)))") + apply simp + apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux a @ hflat_aux aa))") + using hflat_aux.simps(1) apply presburger + apply simp + using cbs_hfau_rsimpeq1 apply(fastforce) + by simp + + +lemma ntimes_closed_form1: + shows "rsimp (rders (RNTIMES r (Suc n)) (c#s)) = +rsimp ( ( RALTS ( map (opterm r) (nupdates s r [Some ([c], n)]) )))" + apply(subgoal_tac "created_by_ntimes (rders (RNTIMES r (Suc n)) (c#s))") + apply(subst hfau_rsimpeq2_ntimes) + apply linarith + using ntimes_ders_hfau_also1 apply auto[1] + using ntimes_ders_cbn1 by blast + + +lemma ntimes_closed_form2: + shows "rsimp (rders_simp (RNTIMES r (Suc n)) (c#s) ) = +rsimp ( ( RALTS ( (map (opterm r ) (nupdates s r [Some ([c], n)]) ) )))" + by (metis list.distinct(1) ntimes_closed_form1 rders_simp_same_simpders rsimp_idem) + + +lemma ntimes_closed_form3: + shows "rsimp (rders_simp (RNTIMES r n) (c#s)) = (rders_simp (RNTIMES r n) (c#s))" + by (metis list.distinct(1) rders_simp_same_simpders rsimp_idem) + + +lemma ntimes_closed_form4: + shows " (rders_simp (RNTIMES r (Suc n)) (c#s)) = +rsimp ( ( RALTS ( (map (opterm r ) (nupdates s r [Some ([c], n)]) ) )))" + using ntimes_closed_form2 ntimes_closed_form3 + by metis + + + + +lemma ntimes_closed_form5: + shows " rsimp ( RALTS (map (\s1. RSEQ (rders r0 s1) (RNTIMES r n) ) Ss)) = + rsimp ( RALTS (map (\s1. rsimp (RSEQ (rders r0 s1) (RNTIMES r n)) ) Ss))" + by (smt (verit, ccfv_SIG) list.map_comp map_eq_conv o_apply simp_flatten_aux0) + + + +lemma ntimes_closed_form6_hrewrites: + shows " +(map (\s1. (RSEQ (rsimp (rders r0 s1)) (RNTIMES r0 n)) ) Ss ) + scf\* +(map (\s1. rsimp (RSEQ (rders r0 s1) (RNTIMES r0 n)) ) Ss )" + apply(induct Ss) + apply simp + apply (simp add: ss1) + by (metis (no_types, lifting) list.simps(9) rsimp.simps(1) rsimp_idem simp_hrewrites ss2) + + + +lemma ntimes_closed_form6: + shows " rsimp ( ( RALTS ( (map (\s1. rsimp (RSEQ (rders r0 s1) (RNTIMES r0 n)) ) Ss )))) = + rsimp ( ( RALTS ( (map (\s1. (RSEQ (rsimp (rders r0 s1)) (RNTIMES r0 n)) ) Ss ))))" + apply(subgoal_tac " map (\s1. (RSEQ (rsimp (rders r0 s1)) (RNTIMES r0 n)) ) Ss scf\* + map (\s1. rsimp (RSEQ (rders r0 s1) (RNTIMES r0 n)) ) Ss ") + using hrewrites_simpeq srewritescf_alt1 apply fastforce + using ntimes_closed_form6_hrewrites by blast + +abbreviation + "optermsimp r SN \ case SN of + Some (s, n) \ RSEQ (rders_simp r s) (RNTIMES r n) + | None \ RZERO + + +" + +abbreviation + "optermOsimp r SN \ case SN of + Some (s, n) \ rsimp (RSEQ (rders r s) (RNTIMES r n)) + | None \ RZERO + + +" + +abbreviation + "optermosimp r SN \ case SN of + Some (s, n) \ RSEQ (rsimp (rders r s)) (RNTIMES r n) + | None \ RZERO +" + +lemma ntimes_closed_form51: + shows "rsimp (RALTS (map (opterm r) (nupdates s r [Some ([c], n)]))) = + rsimp (RALTS (map (rsimp \ (opterm r)) (nupdates s r [Some ([c], n)])))" + by (metis map_map simp_flatten_aux0) + + + +lemma osimp_Osimp: + shows " nonempty_string sn \ optermosimp r sn = optermsimp r sn" + apply(induct rule: nonempty_string.induct) + apply force + apply auto[1] + apply simp + by (metis list.distinct(1) rders.simps(2) rders_simp.simps(2) rders_simp_same_simpders) + + + +lemma osimp_Osimp_list: + shows "\sn \ set snlist. nonempty_string sn \ map (optermosimp r) snlist = map (optermsimp r) snlist" + by (simp add: osimp_Osimp) + + +lemma ntimes_closed_form8: + shows +"rsimp (RALTS (map (optermosimp r) (nupdates s r [Some ([c], n)]))) = + rsimp (RALTS (map (optermsimp r) (nupdates s r [Some ([c], n)])))" + apply(subgoal_tac "\opt \ set (nupdates s r [Some ([c], n)]). nonempty_string opt") + using osimp_Osimp_list apply presburger + by (metis list.distinct(1) list.set_cases nonempty_string.simps(3) nupdates_nonempty set_ConsD) + + + +lemma ntimes_closed_form9aux: + shows "\snopt \ set (nupdates s r [Some ([c], n)]). nonempty_string snopt" + by (metis list.distinct(1) list.set_cases nonempty_string.simps(3) nupdates_nonempty set_ConsD) + +lemma ntimes_closed_form9aux1: + shows "\snopt \ set snlist. nonempty_string snopt \ +rsimp (RALTS (map (optermosimp r) snlist)) = +rsimp (RALTS (map (optermOsimp r) snlist))" + apply(induct snlist) + apply simp+ + apply(case_tac "a") + apply simp+ + by (smt (z3) case_prod_conv idem_after_simp1 map_eq_conv nonempty_string.elims(2) o_apply option.simps(4) option.simps(5) rsimp.simps(1) rsimp.simps(7) rsimp_idem) + + + + +lemma ntimes_closed_form9: + shows +"rsimp (RALTS (map (optermosimp r) (nupdates s r [Some ([c], n)]))) = + rsimp (RALTS (map (optermOsimp r) (nupdates s r [Some ([c], n)])))" + using ntimes_closed_form9aux ntimes_closed_form9aux1 by presburger + + +lemma ntimes_closed_form10rewrites_aux: + shows " map (rsimp \ (opterm r)) optlist scf\* + map (optermOsimp r) optlist" + apply(induct optlist) + apply simp + apply (simp add: ss1) + apply simp + apply(case_tac a) + using ss2 apply fastforce + using ss2 by force + + +lemma ntimes_closed_form10rewrites: + shows " map (rsimp \ (opterm r)) (nupdates s r [Some ([c], n)]) scf\* + map (optermOsimp r) (nupdates s r [Some ([c], n)])" + using ntimes_closed_form10rewrites_aux by blast + +lemma ntimes_closed_form10: + shows "rsimp (RALTS (map (rsimp \ (opterm r)) (nupdates s r [Some ([c], n)]))) = + rsimp (RALTS (map (optermOsimp r) (nupdates s r [Some ([c], n)])))" + by (smt (verit, best) case_prod_conv hpower_rs_elems map_eq_conv nupdates_mono2 o_apply option.case(2) option.simps(4) rsimp.simps(3)) + + +lemma rders_simp_cons: + shows "rders_simp r (c # s) = rders_simp (rsimp (rder c r)) s" + by simp + +lemma rder_ntimes: + shows "rder c (RNTIMES r (Suc n)) = RSEQ (rder c r) (RNTIMES r n)" + by simp + + +lemma ntimes_closed_form: + shows "rders_simp (RNTIMES r0 (Suc n)) (c#s) = +rsimp ( RALTS ( (map (optermsimp r0 ) (nupdates s r0 [Some ([c], n)]) ) ))" + apply (subst rders_simp_cons) + apply(subst rder_ntimes) + using ntimes_closed_form10 ntimes_closed_form4 ntimes_closed_form51 ntimes_closed_form8 ntimes_closed_form9 by force + + + + + + +(* +lemma ntimes_closed_form: + assumes "s \ []" + shows "rders_simp (RNTIMES r (Suc n)) s = +rsimp ( RALTS ( map + (\ optSN. case optSN of + Some (s, n) \ RSEQ (rders_simp r s) (RNTIMES r n) + | None \ RZERO + ) + (ntset r n s) + ) + )" + +*) end \ No newline at end of file