diff -r aecf1ddf3541 -r c27f04bb2262 thys3/HarderProps.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys3/HarderProps.thy	Wed Jun 29 12:38:05 2022 +0100
@@ -0,0 +1,289 @@
+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
\ No newline at end of file