--- a/thys2/ClosedForms.thy	Sat Mar 12 14:33:54 2022 +0000
+++ b/thys2/ClosedForms.thy	Tue Mar 15 16:37:41 2022 +0000
@@ -2,6 +2,33 @@
 "BasicIdentities"
 begin
 
+
+
+lemma simp_rdistinct_f: shows 
+"f ` rset = frset \<Longrightarrow> rsimp (rsimp_ALTs (map f (rdistinct rs rset))) = rsimp (rsimp_ALTs (rdistinct (map f rs) frset))  "
+  apply(induct rs arbitrary: rset)
+   apply simp
+   apply(case_tac "a \<in> rset")
+  apply(case_tac " f a \<in> frset")
+   apply simp
+   apply blast
+  apply(subgoal_tac "f a \<notin> frset")
+   apply(simp)
+   apply(subgoal_tac "f ` (insert a rset) = insert (f a) frset")
+  prefer 2
+  apply (meson image_insert)
+  
+
+  
+  sorry
+
+
+lemma distinct_der:
+  shows "rsimp (rsimp_ALTs (map (rder x) (rdistinct rs {}))) = rsimp ( rsimp_ALTs (rdistinct (map (rder x) rs) {}))"
+
+  sorry
+
+
 lemma alts_closed_form: shows 
 "rsimp (rders_simp (RALTS rs) s) = 
 rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
@@ -14,6 +41,20 @@
    prefer 2
   apply (metis inside_simp_removal rders_simp_one_char)
   apply(simp only: )
+  apply(subst rders_simp_one_char)
+  apply(subst rsimp_idem)
+  apply(subgoal_tac "rsimp (rder x (rsimp_ALTs (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {}))) =
+                     rsimp ((rsimp_ALTs (map (rder x) (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {})))) ")
+  prefer 2
+  using rder_rsimp_ALTs_commute apply presburger
+  apply(simp only:)
+  apply(subgoal_tac "rsimp (rsimp_ALTs (map (rder x) (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {})))
+= rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}))")
+   prefer 2
+  
+  using distinct_der apply presburger
+  apply(simp only:)
+
   sorry
 
 lemma alts_closed_form_variant: shows