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  hmany_steps_later: "\<lbrakk>r1 h\<leadsto> r2; r2 h\<leadsto>* r3 \<rbrakk> \<Longrightarrow> r1 h\<leadsto>* r3"

  by (meson hr_in_rstar hreal_trans)

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_context0:

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

  apply(subgoal_tac "RSEQ r1 r3 h\<leadsto>* RSEQ RZERO r3")

  using hrewrite.intros(1) apply blast

  by (simp add: hrewrites_seq_context)

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 map_concat_cons:

  shows "map f rsa @ f a # rs = map f (rsa @ [a]) @ rs"

  by simp

lemma neg_removal_element_of:

  shows " \<not> a \<notin> aset \<Longrightarrow> a \<in> aset"

  by simp

lemma flts_middle01:

  shows "rflts (rsa @ [RZERO] @ rsb) = rflts (rsa @ rsb)"

  by (simp add: flts_middle0)

lemma flts_append1:

  shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1; a \<in> set rs\<rbrakk>  \<Longrightarrow>

         rflts (rsa @ [a] @ rsb) = rflts rsa @ [a] @ (rflts rsb)"

  apply(induct rsa arbitrary: rsb)

   apply simp

  using rflts_def_idiot apply presburger

  apply(case_tac aa)  

       apply simp+

  done

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)

lemma distinct_removes_duplicate_flts2:

  shows " a \<in> set rsa

       \<Longrightarrow> rdistinct (rflts (rsa @ [a] @ rsb)) {} =

           rdistinct (rflts (rsa @ rsb)) {}"

  apply(induct a arbitrary: rsb)

  using flts_middle01 apply presburger

      apply(subgoal_tac "rflts (rsa @ [RONE] @ rsb) = rflts rsa @ [RONE] @ rflts rsb")

  prefer 2

  using flts_append1 apply blast

      apply simp

      apply(subgoal_tac "RONE \<in> set (rflts rsa)")

  prefer 2

  using rflts_def_idiot2 apply blast

      apply(subst distinct_removes_middle3)

       apply simp

  using flts_append apply presburger

     apply simp

  apply (metis distinct_removes_middle3 flts_append in_set_conv_decomp rflts.simps(5))

  apply (metis distinct_removes_middle(1) flts_append flts_append1 rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(5))

   apply(subgoal_tac "rflts (rsa @ [RALTS x] @ rsb) = rflts rsa @ x @ rflts rsb")

    prefer 2

  apply (simp add: flts_append)

   apply (simp only:)

   apply(subgoal_tac "\<forall>r1 \<in> set x. r1 \<in> set (rflts rsa)")

    prefer 2

  using spilled_alts_contained apply blast

  apply(subst flts_append)

  using distinct_removes_middle_list apply blast

  using distinct_removes_middle2 flts_append rflts_def_idiot2 by fastforce

lemma simp_removes_duplicate:

  shows "a \<in> set rsa \<Longrightarrow> rsimp (rsimp_ALTs (rsa @ a # rs)) =  rsimp (rsimp_ALTs (rsa @ rs))"

  apply(subgoal_tac "rsimp (rsimp_ALTs (rsa @ a # rs)) = rsimp (RALTS (rsa @ a # rs))")

   prefer 2

  apply (smt (verit, best) Cons_eq_append_conv append_is_Nil_conv empty_set equals0D list.distinct(1) rsimp_ALTs.elims)

  apply(simp only:)

  apply simp

  apply(subgoal_tac "(rdistinct (rflts (map rsimp rsa @ rsimp a # map rsimp rs)) {}) = (rdistinct (rflts (map rsimp rsa @  map rsimp rs)) {})")

   apply(simp only:)

  prefer 2

   apply(subgoal_tac "rsimp a \<in> set (map rsimp rsa)")

    prefer 2

  apply simp

  using distinct_removes_duplicate_flts2 apply force

  apply(case_tac rsa)

   apply simp

  apply(case_tac rs)

   apply simp

   apply(case_tac list)

    apply simp

  using idem_after_simp1 apply presburger

   apply simp+

  apply(subgoal_tac "rsimp_ALTs (aa # list @ aaa # lista) = RALTS (aa # list @ aaa # lista)")

   apply simp

  using rsimpalts_conscons by presburger

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 frewrite_append:

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

  apply(induct rs)

   apply simp+

  using frewrite.intros(3) by blast

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 frewrites_concat:

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

  apply(induct rs1 rs2 rule: frewrite.induct)

    apply(simp)

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

  prefer 2

  using frewrite.intros(1) apply blast

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

  using many_steps_later apply blast

  apply (simp add: frewrites_append)

  apply (metis append.assoc append_Cons frewrite.intros(2) frewrites_append many_steps_later)

  using frewrites_cons by auto

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 alt_set_has_all:

  shows "RALTS rs \<in> alt_set rx \<Longrightarrow> set rs \<subseteq> alt_set rx"

  apply(induct rx arbitrary: rs)

       apply simp_all

  apply(rename_tac rSS rss)

  using in_mono by fastforce

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}")