--- a/thys2/ClosedForms.thy	Fri Apr 15 23:31:31 2022 +0100
+++ b/thys2/ClosedForms.thy	Sat Apr 16 09:52:57 2022 +0100
@@ -530,7 +530,8 @@
 
 
 lemma good_flatten_aux:
-  shows " \<lbrakk>\<forall>r\<in>set rs. good r; \<forall>r\<in>set rsa. good r; \<forall>r\<in>set rsb. good r;
+  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)) {});
@@ -553,17 +554,17 @@
   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 flts3 nn1b nn1c qqq1 test)
+  apply (metis flts3 nonalt_flts_rd qqq1 rdistinct_set_equality)
   apply(subgoal_tac "\<forall>r \<in> set (rflts rsb). good r \<and> r \<noteq> RZERO \<and> nonalt r")
   prefer 2  
-  apply (metis flts3 nn1b nn1c qqq1 test)
+  apply (metis flts3 nonalt_flts_rd qqq1 rdistinct_set_equality)
   by (smt (verit, ccfv_threshold) good_flatten_aux_aux)
 
   
 
 
 lemma good_flatten_middle:
-  shows "\<lbrakk>\<forall>r \<in> set rs. good r; \<forall>r \<in> set rsa. good r; \<forall>r \<in> set rsb. good r\<rbrakk> \<Longrightarrow>
+  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)) {})")
@@ -577,17 +578,17 @@
   apply(simp only:)
   apply(subgoal_tac "map rsimp rsa = rsa")
   prefer 2
-  apply (simp add: map_idI test)
+  apply (metis map_idI rsimp.simps(3) test)
   apply(simp only:)
   apply(subgoal_tac "map rsimp rsb = rsb")
    prefer 2
-  apply (meson map_idI test)
+  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 (meson map_idI test)
+  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:)
@@ -600,7 +601,7 @@
   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
+   apply presburger
   using good_flatten_aux by blast
 
 
@@ -620,14 +621,17 @@
  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")
-   apply(subgoal_tac "\<forall>r \<in> set (map rsimp rs). good r")
-    apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsb). good r")
+  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
   
-
-  sorry
+  apply (simp add: good1)
+  apply (simp add: good1)
+  apply (simp add: good1)
+
+  done