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