theory ClosedForms 

  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 \<Rightarrow> rrexp \<Rightarrow> bool" ("_ h\<leadsto> _" [99, 99] 99)

where

  "RSEQ  RZERO r2 h\<leadsto> RZERO"

| "RSEQ  r1 RZERO h\<leadsto> RZERO"

| "RSEQ  RONE r h\<leadsto>  r"

| "r1 h\<leadsto> r2 \<Longrightarrow> RSEQ  r1 r3 h\<leadsto> RSEQ r2 r3"

| "r3 h\<leadsto> r4 \<Longrightarrow> RSEQ r1 r3 h\<leadsto> RSEQ r1 r4"

| "r h\<leadsto> r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) h\<leadsto> (RALTS  (rs1 @ [r'] @ rs2))"

(*context rule for eliminating 0, alts--corresponds to the recursive call flts r::rs = r::(flts rs)*)

| "RALTS  (rsa @ [RZERO] @ rsb) h\<leadsto> RALTS  (rsa @ rsb)"

| "RALTS  (rsa @ [RALTS rs1] @ rsb) h\<leadsto> RALTS (rsa @ rs1 @ rsb)"

| "RALTS  [] h\<leadsto> RZERO"

| "RALTS  [r] h\<leadsto> r"

| "a1 = a2 \<Longrightarrow> RALTS (rsa@[a1]@rsb@[a2]@rsc) h\<leadsto> RALTS (rsa @ [a1] @ rsb @ rsc)"

inductive 

  hrewrites:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ h\<leadsto>* _" [100, 100] 100)

where 

  rs1[intro, simp]:"r h\<leadsto>* r"

| rs2[intro]: "\<lbrakk>r1 h\<leadsto>* r2; r2 h\<leadsto> r3\<rbrakk> \<Longrightarrow> r1 h\<leadsto>* r3"

lemma hr_in_rstar : "r1 h\<leadsto> r2 \<Longrightarrow> r1 h\<leadsto>* r2"

  using hrewrites.intros(1) hrewrites.intros(2) by blast

lemma hreal_trans[trans]: 

  assumes a1: "r1 h\<leadsto>* r2"  and a2: "r2 h\<leadsto>* r3"

  shows "r1 h\<leadsto>* r3"

  using a2 a1

  apply(induct r2 r3 arbitrary: r1 rule: hrewrites.induct) 

  apply(auto)

  done

lemma hrewrites_seq_context:

  shows "r1 h\<leadsto>* r2 \<Longrightarrow> RSEQ r1 r3 h\<leadsto>* RSEQ r2 r3"

  apply(induct r1 r2 rule: hrewrites.induct)

   apply simp

  using hrewrite.intros(4) by blast

lemma hrewrites_seq_context2:

  shows "r1 h\<leadsto>* r2 \<Longrightarrow> RSEQ r0 r1 h\<leadsto>* RSEQ r0 r2"

  apply(induct r1 r2 rule: hrewrites.induct)

   apply simp

  using hrewrite.intros(5) by blast

lemma hrewrites_seq_contexts:

  shows "\<lbrakk>r1 h\<leadsto>* r2; r3 h\<leadsto>* r4\<rbrakk> \<Longrightarrow> RSEQ r1 r3 h\<leadsto>* RSEQ r2 r4"

  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

  "(RZERO # rs) \<leadsto>f rs"

| "((RALTS rs) # rsa) \<leadsto>f (rs @ rsa)"

| "rs1 \<leadsto>f rs2 \<Longrightarrow> (r # rs1) \<leadsto>f (r # rs2)"

inductive 

  frewrites:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>f* _" [10, 10] 10)

where 

  [intro, simp]:"rs \<leadsto>f* rs"

| [intro]: "\<lbrakk>rs1 \<leadsto>f* rs2; rs2 \<leadsto>f rs3\<rbrakk> \<Longrightarrow> rs1 \<leadsto>f* rs3"

inductive grewrite:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>g _" [10, 10] 10)

  where

  "(RZERO # rs) \<leadsto>g rs"

| "((RALTS rs) # rsa) \<leadsto>g (rs @ rsa)"

| "rs1 \<leadsto>g rs2 \<Longrightarrow> (r # rs1) \<leadsto>g (r # rs2)"

| "rsa @ [a] @ rsb @ [a] @ rsc \<leadsto>g rsa @ [a] @ rsb @ rsc" 

lemma grewrite_variant1:

  shows "a \<in> set rs1 \<Longrightarrow> rs1 @ a # rs \<leadsto>g rs1 @ rs"

  apply (metis append.assoc append_Cons append_Nil grewrite.intros(4) split_list_first)

  done

inductive 

  grewrites:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>g* _" [10, 10] 10)

where 

  [intro, simp]:"rs \<leadsto>g* rs"

| [intro]: "\<lbrakk>rs1 \<leadsto>g* rs2; rs2 \<leadsto>g rs3\<rbrakk> \<Longrightarrow> rs1 \<leadsto>g* rs3"

(*

inductive 

  frewrites2:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ <\<leadsto>f* _" [10, 10] 10)

where 

 [intro]: "\<lbrakk>rs1 \<leadsto>f* rs2; rs2 \<leadsto>f* rs1\<rbrakk> \<Longrightarrow> rs1 <\<leadsto>f* rs2"

*)

lemma fr_in_rstar : "r1 \<leadsto>f r2 \<Longrightarrow> r1 \<leadsto>f* r2"

  using frewrites.intros(1) frewrites.intros(2) by blast

lemma freal_trans[trans]: 

  assumes a1: "r1 \<leadsto>f* r2"  and a2: "r2 \<leadsto>f* r3"

  shows "r1 \<leadsto>f* r3"

  using a2 a1

  apply(induct r2 r3 arbitrary: r1 rule: frewrites.induct) 

  apply(auto)

  done

lemma  many_steps_later: "\<lbrakk>r1 \<leadsto>f r2; r2 \<leadsto>f* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>f* r3"

  by (meson fr_in_rstar freal_trans)

lemma gr_in_rstar : "r1 \<leadsto>g r2 \<Longrightarrow> r1 \<leadsto>g* r2"

  using grewrites.intros(1) grewrites.intros(2) by blast

lemma greal_trans[trans]: 

  assumes a1: "r1 \<leadsto>g* r2"  and a2: "r2 \<leadsto>g* r3"

  shows "r1 \<leadsto>g* r3"

  using a2 a1

  apply(induct r2 r3 arbitrary: r1 rule: grewrites.induct) 

  apply(auto)

  done

lemma  gmany_steps_later: "\<lbrakk>r1 \<leadsto>g r2; r2 \<leadsto>g* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>g* r3"

  by (meson gr_in_rstar greal_trans)

lemma gstar_rdistinct_general:

  shows "rs1 @  rs \<leadsto>g* rs1 @ (rdistinct rs (set rs1))"

  apply(induct rs arbitrary: rs1)

   apply simp

  apply(case_tac " a \<in> set rs1")

   apply simp

  apply(subgoal_tac "rs1 @ a # rs \<leadsto>g rs1 @ rs")

  using gmany_steps_later apply auto[1]

  apply (metis append.assoc append_Cons append_Nil grewrite.intros(4) split_list_first)

  apply simp

  apply(drule_tac x = "rs1 @ [a]" in meta_spec)

  by simp

lemma gstar_rdistinct:

  shows "rs \<leadsto>g* rdistinct rs {}"

  apply(induct rs)

   apply simp

  by (metis append.left_neutral empty_set gstar_rdistinct_general)

lemma grewrite_append:

  shows "\<lbrakk> rsa \<leadsto>g rsb \<rbrakk> \<Longrightarrow> rs @ rsa \<leadsto>g rs @ rsb"

  apply(induct rs)

   apply simp+

  using grewrite.intros(3) by blast

lemma frewrites_cons:

  shows "\<lbrakk> rsa \<leadsto>f* rsb \<rbrakk> \<Longrightarrow> r # rsa \<leadsto>f* r # rsb"

  apply(induct rsa rsb rule: frewrites.induct)

   apply simp

  using frewrite.intros(3) by blast

lemma grewrites_cons:

  shows "\<lbrakk> rsa \<leadsto>g* rsb \<rbrakk> \<Longrightarrow> r # rsa \<leadsto>g* r # rsb"

  apply(induct rsa rsb rule: grewrites.induct)

   apply simp

  using grewrite.intros(3) by blast

lemma frewrites_append:

  shows " \<lbrakk>rsa \<leadsto>f* rsb\<rbrakk> \<Longrightarrow> (rs @ rsa) \<leadsto>f* (rs @ rsb)"

  apply(induct rs)

   apply simp

  by (simp add: frewrites_cons)

lemma grewrites_append:

  shows " \<lbrakk>rsa \<leadsto>g* rsb\<rbrakk> \<Longrightarrow> (rs @ rsa) \<leadsto>g* (rs @ rsb)"

  apply(induct rs)

   apply simp

  by (simp add: grewrites_cons)

lemma grewrites_concat:

  shows "\<lbrakk>rs1 \<leadsto>g rs2; rsa \<leadsto>g* rsb \<rbrakk> \<Longrightarrow> (rs1 @ rsa) \<leadsto>g* (rs2 @ rsb)"

  apply(induct rs1 rs2 rule: grewrite.induct)

    apply(simp)

  apply(subgoal_tac "(RZERO # rs @ rsa) \<leadsto>g (rs @ rsa)")

  prefer 2

  using grewrite.intros(1) apply blast

    apply(subgoal_tac "(rs @ rsa) \<leadsto>g* (rs @ rsb)")

  using gmany_steps_later apply blast

  apply (simp add: grewrites_append)

  apply (metis append.assoc append_Cons grewrite.intros(2) grewrites_append gmany_steps_later)

  using grewrites_cons apply auto

  apply(subgoal_tac "rsaa @ a # rsba @ a # rsc @ rsa \<leadsto>g* rsaa @ a # rsba @ a # rsc @ rsb")

  using grewrite.intros(4) grewrites.intros(2) apply force

  using grewrites_append by auto

lemma grewritess_concat:

  shows "\<lbrakk>rsa \<leadsto>g* rsb; rsc \<leadsto>g* rsd \<rbrakk> \<Longrightarrow> (rsa @ rsc) \<leadsto>g* (rsb @ rsd)"

  apply(induct rsa rsb rule: grewrites.induct)

   apply(case_tac rs)

    apply simp

  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> 

(\<exists>rsa rsb rsc. rs1 =  (rsa @ [RALTS rsb] @ rsc) \<and> rs2 = (rsa @ rsb @ rsc)) \<or>

(\<exists>rsa rsc. rs1 = rsa @ [RZERO] @ rsc \<and> rs2 = rsa @ rsc) \<or>

(\<exists>rsa rsb rsc a. rs1 = rsa @ [a] @ rsb @ [a] @ rsc \<and> rs2 = rsa @ [a] @ rsb @ rsc)"

  apply( induct rs1 rs2 rule: grewrite.induct)

     apply simp

  apply blast

  apply (metis append_Cons append_Nil)

  apply (metis append_Cons)

  by blast

lemma good_singleton:

  shows "good a \<and> nonalt a  \<Longrightarrow> rflts [a] = [a]"

  using good.simps(1) k0b by blast

lemma all_that_same_elem:

  shows "\<lbrakk> a \<in> rset; rdistinct rs {a} = []\<rbrakk>

       \<Longrightarrow> 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 \<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 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 "\<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

lemma grewrite_equal_rsimp:

  shows "rs1 \<leadsto>g rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"

  apply(frule grewrite_cases_middle)

  apply(case_tac "(\<exists>rsa rsb rsc. rs1 = rsa @ [RALTS rsb] @ rsc \<and> rs2 = rsa @ rsb @ rsc)")  

  using simp_flatten3 apply auto[1]

  apply(case_tac "(\<exists>rsa rsc. rs1 = rsa @ [RZERO] @ rsc \<and> rs2 = rsa @ rsc)")

  apply (metis (mono_tags, opaque_lifting) append_Cons append_Nil list.set_intros(1) list.simps(9) rflts.simps(2) rsimp.simps(2) rsimp.simps(3) simp_removes_duplicate3)

  by (smt (verit) append.assoc append_Cons append_Nil in_set_conv_decomp simp_removes_duplicate3)

lemma grewrites_equal_rsimp:

  shows "rs1 \<leadsto>g* rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"

  apply (induct rs1 rs2 rule: grewrites.induct)

  apply simp

  using grewrite_equal_rsimp by presburger

lemma grewrites_last:

  shows "r # [RALTS rs] \<leadsto>g*  r # rs"

  by (metis gr_in_rstar grewrite.intros(2) grewrite.intros(3) self_append_conv)

lemma simp_flatten2:

  shows "rsimp (RALTS (r # [RALTS rs])) = rsimp (RALTS (r # rs))"

  using grewrites_equal_rsimp grewrites_last by blast

lemma frewrites_alt:

  shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> (RALT r1 r2) # rs1 \<leadsto>f* r1 # r2 # rs2"  

  by (metis Cons_eq_appendI append_self_conv2 frewrite.intros(2) frewrites_cons many_steps_later)

lemma early_late_der_frewrites:

  shows "map (rder x) (rflts rs) \<leadsto>f* rflts (map (rder x) rs)"

  apply(induct rs)

   apply simp