diff -r 31abe0e496bc -r 599239394c51 thys2/ClosedForms.thy
--- a/thys2/ClosedForms.thy	Thu Mar 24 20:59:43 2022 +0000
+++ b/thys2/ClosedForms.thy	Thu Mar 24 21:11:12 2022 +0000
@@ -468,26 +468,46 @@
   apply(subgoal_tac "rsimp_ALTs (aa # list @ aaa # lista) = RALTS (aa # list @ aaa # lista)")
    apply simp
   using rsimpalts_conscons by presburger
+
+
+
+
+lemma distinct_flts_no0:
+  shows "rdistinct (rflts rs) (insert RZERO rset) = rdistinct (rflts rs) rset"
+  apply(induct rs)
+   apply simp
+  apply(case_tac a)
+  using rflts.simps(2) apply presburger
+  sorry
+
+
+lemma simp_der_flts:
+  shows "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) rset))= 
+         rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) rset))"
+
+  apply(induct rs arbitrary: rset)
+   apply simp
+  apply(case_tac a)
+       apply simp
+      apply(case_tac "RZERO \<in> rset")
+       apply simp
+      apply simp
   
+  sorry
+
+
 lemma simp_der_pierce_flts:
   shows " rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})) =
            rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}))"
-  oops
+  sorry
+
 
 
 
 lemma simp_more_distinct:
   shows "rsimp  (rsimp_ALTs (rsa @ rs)) = rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) "
-and  "a1 \<in> set rsb \<Longrightarrow> rsimp (rsimp_ALTs (rsb @ a1 # rs)) =  rsimp (rsimp_ALTs (rsb @ rs))"
-  apply(induct rs arbitrary: rsa rsb a1)
-     apply simp
-  apply simp
-  apply(case_tac " a \<in> set rsa")
-   apply simp
-   prefer 2
-   apply simp
-   apply(drule_tac x = "rsa @ [a]" in meta_spec)
-   apply simp
+  
+
 
 
   sorry
@@ -756,7 +776,7 @@
      apply simp
   using add0_isomorphic apply blast 
     apply simp
-  sorry
+  oops
 
 lemma alts_closed_form: shows 
 "rsimp (rders_simp (RALTS rs) s) =