theory HarderProps imports BasicIdentities

begin

lemma spawn_simp_rsimpalts:

  shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (map rsimp rs))"

  apply(cases rs)

   apply simp

  apply(case_tac list)

   apply simp

   apply(subst rsimp_idem[symmetric])

   apply simp

  apply(subgoal_tac "rsimp_ALTs rs = RALTS rs")

   apply(simp only:)

   apply(subgoal_tac "rsimp_ALTs (map rsimp rs) = RALTS (map rsimp rs)")

    apply(simp only:)

  prefer 2

  apply simp

   prefer 2

  using rsimp_ALTs.simps(3) apply presburger

  apply auto

  apply(subst rsimp_idem)+

  by (metis comp_apply rsimp_idem)

lemma good1_rsimpalts:

  shows "rsimp r = RALTS rs \<Longrightarrow> rsimp_ALTs rs = RALTS rs"

  by (metis no_alt_short_list_after_simp) 

lemma good1_flatten:

  shows "\<lbrakk> rsimp r =  (RALTS rs1)\<rbrakk>

       \<Longrightarrow> rflts (rsimp_ALTs rs1 # map rsimp rsb) = rflts (rs1 @ map rsimp rsb)"

  apply(subst good1_rsimpalts)

   apply simp+

  apply(subgoal_tac "rflts (rs1 @ map rsimp rsb) = rs1 @ rflts (map rsimp rsb)")

   apply simp

  using flts_append rsimp_inner_idem4 by presburger

lemma flatten_rsimpalts:

  shows "rflts (rsimp_ALTs (rdistinct (rflts (map rsimp rsa)) {}) # map rsimp rsb) = 

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

  apply(case_tac "map rsimp rsa")

   apply simp

  apply(case_tac "list")

   apply simp

   apply(case_tac a)

        apply simp+

    apply(rename_tac rs1)

    apply (metis good1_flatten map_eq_Cons_D no_further_dB_after_simp)

  apply simp

  apply(subgoal_tac "\<forall>r \<in> 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)

lemma simp_flatten:

  shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))"

  apply simp

  apply(subst flatten_rsimpalts)

  apply(simp add: flts_append)

  by (metis Diff_empty distinct_once_enough flts_append nonalt0_fltseq nonalt_flts_rd qqq1 rdistinct_set_equality1)

lemma simp_flatten_aux0:

  shows "rsimp (RALTS rs) = rsimp (RALTS (map rsimp rs))"

  apply(induct rs)

   apply simp+

  by (metis (mono_tags, opaque_lifting) comp_eq_dest_lhs map_eq_conv rsimp_idem)

lemma good_singleton:

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

  using good.simps(1) k0b by blast

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

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

end