--- a/thys3/ClosedForms.thy	Fri Jun 24 21:49:23 2022 +0100
+++ b/thys3/ClosedForms.thy	Sun Jun 26 22:22:47 2022 +0100
@@ -2,6 +2,7 @@
   imports "BasicIdentities"
 begin
 
+
 lemma flts_middle0:
   shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)"
   apply(induct rsa)
@@ -288,14 +289,6 @@
 
 
 
-lemma all_that_same_elem:
-  shows "\<lbrakk> a \<in> rset; rdistinct rs {a} = []\<rbrakk>
-       \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct rsb rset"
-  apply(induct rs)
-   apply simp
-  apply(subgoal_tac "aa = a")
-   apply simp
-  by (metis empty_iff insert_iff list.discI rdistinct.simps(2))
 
 lemma distinct_early_app1:
   shows "rset1 \<subseteq> rset \<Longrightarrow> rdistinct rs rset = rdistinct (rdistinct rs rset1) rset"
@@ -390,7 +383,9 @@
      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;
+     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) {} =
@@ -439,7 +434,7 @@
    prefer 2
   apply (metis map_idI rsimp.simps(3) test)
   apply(simp only:)
-  apply(subst k00)+
+  apply(subst flts_append)+
   apply(subgoal_tac "map rsimp rs = rs")
    apply(simp only:)
    prefer 2
@@ -460,15 +455,6 @@
   using good_flatten_aux by blast
 
 
-lemma simp_flatten3:
-  shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))"
-proof -
-  have  "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = 
-                     rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) " 
-    by (metis append_Cons append_Nil list.simps(9) map_append simp_flatten_aux0)
-  apply(simp only:)
-
-oops
 
 lemma simp_flatten3:
   shows "rsimp (RALTS (rsa @ [RALTS rs ] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))"
@@ -876,39 +862,8 @@
   by (metis append.right_neutral grewrite.intros(2) grewrite_simpalts rsimp_ALTs.simps(2) simp_der_flts)
 
 
-lemma basic_regex_property1:
-  shows "rnullable r \<Longrightarrow> rsimp r \<noteq> RZERO"
-  apply(induct r rule: rsimp.induct)
-  apply(auto)
-  apply (metis idiot idiot2 rrexp.distinct(5))
-  by (metis der_simp_nullability rnullable.simps(1) rnullable.simps(4) rsimp.simps(2))
 
 
-lemma inside_simp_seq_nullable:
-  shows 
-"\<And>r1 r2.
-       \<lbrakk>rsimp (rder x (rsimp r1)) = rsimp (rder x r1); rsimp (rder x (rsimp r2)) = rsimp (rder x r2);
-        rnullable r1\<rbrakk>
-       \<Longrightarrow> rsimp (rder x (rsimp_SEQ (rsimp r1) (rsimp r2))) =
-           rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp (rder x r1)) (rsimp r2), rsimp (rder x r2)]) {})"
-  apply(case_tac "rsimp r1 = RONE")
-   apply(simp)
-  apply(subst basic_rsimp_SEQ_property1)
-   apply (simp add: idem_after_simp1)
-  apply(case_tac "rsimp r1 = RZERO")
-  
-  using basic_regex_property1 apply blast
-  apply(case_tac "rsimp r2 = RZERO")
-  
-  apply (simp add: basic_rsimp_SEQ_property3)
-  apply(subst idiot2)
-     apply simp+
-  apply(subgoal_tac "rnullable (rsimp r1)")
-   apply simp
-  using rsimp_idem apply presburger
-  using der_simp_nullability by presburger
-  
-
 
 lemma grewrite_ralts:
   shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs h\<leadsto>* RALTS rs'"
@@ -1118,6 +1073,30 @@
 
 
 
+lemma inside_simp_seq_nullable:
+  shows 
+"\<And>r1 r2.
+       \<lbrakk>rsimp (rder x (rsimp r1)) = rsimp (rder x r1); rsimp (rder x (rsimp r2)) = rsimp (rder x r2);
+        rnullable r1\<rbrakk>
+       \<Longrightarrow> rsimp (rder x (rsimp_SEQ (rsimp r1) (rsimp r2))) =
+           rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp (rder x r1)) (rsimp r2), rsimp (rder x r2)]) {})"
+  apply(case_tac "rsimp r1 = RONE")
+   apply(simp)
+  apply(subst basic_rsimp_SEQ_property1)
+   apply (simp add: idem_after_simp1)
+  apply(case_tac "rsimp r1 = RZERO")
+  using basic_regex_property1 apply blast
+  apply(case_tac "rsimp r2 = RZERO")
+  apply (simp add: basic_rsimp_SEQ_property3)
+  apply(subst idiot2)
+     apply simp+
+  apply(subgoal_tac "rnullable (rsimp r1)")
+   apply simp
+  using rsimp_idem apply presburger
+  using der_simp_nullability by presburger
+  
+
+
 lemma inside_simp_removal:
   shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)"
   apply(induct r)