--- a/thys3/ClosedForms.thy Sun Jun 26 22:22:47 2022 +0100
+++ b/thys3/ClosedForms.thy Tue Jun 28 21:07:42 2022 +0100
@@ -1,20 +1,8 @@
theory ClosedForms
- imports "BasicIdentities"
+ imports "HarderProps"
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 \<Rightarrow> rrexp \<Rightarrow> bool" ("_ h\<leadsto> _" [99, 99] 99)
@@ -68,44 +56,8 @@
by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2)
-lemma simp_removes_duplicate1:
- shows " a \<in> set rsa \<Longrightarrow> 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 \<in> set rsa \<Longrightarrow> 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 \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ a # rsb)) = rsimp (RALTS (rsa @ rsb))"
- using simp_removes_duplicate2 by auto
-(*
-lemma distinct_removes_middle4:
- shows "a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ [a] @ rsb) rset = rdistinct (rsa @ rsb) rset"
- using distinct_removes_middle(1) by fastforce
-*)
-
-(*
-lemma distinct_removes_middle_list:
- shows "\<forall>a \<in> set x. a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ x @ rsb) rset = rdistinct (rsa @ rsb) rset"
- apply(induct x)
- apply simp
- by (simp add: distinct_removes_middle3)
-*)
inductive frewrite:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>f _" [10, 10] 10)
where
@@ -260,11 +212,6 @@
using grewrites_append apply blast
by (meson greal_trans grewrites.simps grewrites_concat)
-fun alt_set:: "rrexp \<Rightarrow> rrexp set"
- where
- "alt_set (RALTS rs) = set rs \<union> \<Union> (alt_set ` (set rs))"
-| "alt_set r = {r}"
-
lemma grewrite_cases_middle:
shows "rs1 \<leadsto>g rs2 \<Longrightarrow>
@@ -279,211 +226,6 @@
by blast
-lemma good_singleton:
- shows "good a \<and> nonalt a \<Longrightarrow> rflts [a] = [a]"
- using good.simps(1) k0b by blast
-
-
-
-
-
-
-
-
-lemma distinct_early_app1:
- shows "rset1 \<subseteq> rset \<Longrightarrow> rdistinct rs rset = rdistinct (rdistinct rs rset1) rset"
- apply(induct rs arbitrary: rset rset1)
- apply simp
- apply simp
- apply(case_tac "a \<in> rset1")
- apply simp
- apply(case_tac "a \<in> rset")
- apply simp+
-
- apply blast
- apply(case_tac "a \<in> rset1")
- apply simp+
- apply(case_tac "a \<in> 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 \<in> rset \<Longrightarrow> 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 "\<lbrakk> size rs \<ge>2;
-\<forall>r \<in> set rs. good r \<and> r \<noteq> RZERO \<and> nonalt r; \<forall>r \<in> set rsb. good r \<and> r \<noteq> RZERO \<and> nonalt r \<rbrakk>
- \<Longrightarrow> rdistinct (rs @ rsb) rset =
- rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset"
- apply(induct rs arbitrary: rset)
- apply simp
- apply(case_tac "a \<in> 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 "\<lbrakk>\<exists>a aa lista list. rs = a # list \<and> list = aa # lista;
-\<forall>r \<in> set rs. good r \<and> r \<noteq> RZERO \<and> nonalt r; \<forall>r \<in> set rsb. good r \<and> r \<noteq> RZERO \<and> nonalt r \<rbrakk>
- \<Longrightarrow> rdistinct (rs @ rsb) rset =
- rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset"
- apply(erule exE)+
- apply(subgoal_tac "size rs \<ge> 2")
- apply (metis good_flatten_aux_aux1)
- by (simp add: Suc_leI length_Cons less_add_Suc1)
-
-
-
-lemma good_flatten_aux:
- shows " \<lbrakk>\<forall>r\<in>set rs. good r \<or> r = RZERO; \<forall>r\<in>set rsa . good r \<or> r = RZERO;
- \<forall>r\<in>set rsb. good r \<or> 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))\<rbrakk>
- \<Longrightarrow> 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 \<in> 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 "\<forall>r \<in> set (rflts rs). good r \<and> r \<noteq> RZERO \<and> nonalt r")
- prefer 2
- apply (metis Diff_empty flts3 nonalt_flts_rd qqq1 rdistinct_set_equality1)
- apply(subgoal_tac "\<forall>r \<in> set (rflts rsb). good r \<and> r \<noteq> RZERO \<and> 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 "\<lbrakk>\<forall>r \<in> set rs. good r \<or> r = RZERO; \<forall>r \<in> set rsa. good r \<or> r = RZERO; \<forall>r \<in> set rsb. good r \<or> r = RZERO\<rbrakk> \<Longrightarrow>
-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 flts_append)+
- 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 "\<forall>r \<in> set (map rsimp rsa). good r \<or> r = RZERO")
- apply(subgoal_tac "\<forall>r \<in> set (map rsimp rs). good r \<or> r = RZERO")
- apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsb). good r \<or> r = RZERO")
-
- using good_flatten_middle apply presburger
-
- apply (simp add: good1)
- apply (simp add: good1)
- apply (simp add: good1)
-
- done
-
@@ -1286,6 +1028,16 @@
by fastforce
+fun vsuf :: "char list \<Rightarrow> rrexp \<Rightarrow> 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 (\<lambda>s. s @ [x]) (vsuf xs r) )
@@ -1533,6 +1285,30 @@
(*AALTS [a\x . b.c, b\x .c, c \x]*)
(*AALTS [a\x . b.c, AALTS [b\x .c, c\x]]*)
+fun star_update :: "char \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> 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 \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list"
+ where
+"star_updates [] r Ss = Ss"
+| "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)"
+
+
+lemma stupdates_append: shows
+"star_updates (s @ [c]) r Ss = star_update c r (star_updates s r Ss)"
+ apply(induct s arbitrary: Ss)
+ apply simp
+ apply simp
+ done
+
+
+
+
+
lemma stupdate_induct1:
shows " concat (map (hflat_aux \<circ> (rder x \<circ> (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) =
map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_update x r0 Ss)"