--- a/thys2/BasicIdentities.thy	Wed Mar 23 10:09:32 2022 +0000
+++ b/thys2/BasicIdentities.thy	Thu Mar 24 20:52:34 2022 +0000
@@ -71,6 +71,20 @@
 | "rsimp_ALTs [r] =  r"
 | "rsimp_ALTs rs = RALTS rs"
 
+lemma rsimpalts_gte2elems:
+  shows "size rlist \<ge> 2 \<Longrightarrow> rsimp_ALTs rlist = RALTS rlist"
+  apply(induct rlist)
+   apply simp
+  apply(induct rlist)
+   apply simp
+  apply (metis Suc_le_length_iff rsimp_ALTs.simps(3))
+  by blast
+
+lemma rsimpalts_conscons:
+  shows "rsimp_ALTs (r1 # rsa @ r2 # rsb) = RALTS (r1 # rsa @ r2 # rsb)"
+  by (metis Nil_is_append_conv list.exhaust rsimp_ALTs.simps(3))
+
+
 fun rsimp_SEQ :: " rrexp \<Rightarrow> rrexp \<Rightarrow> rrexp"
   where
   "rsimp_SEQ  RZERO _ = RZERO"
@@ -264,7 +278,7 @@
 lemma rders_simp_append:
   "rders_simp c (s1 @ s2) = rders_simp (rders_simp c s1) s2"
   apply(induct s1 arbitrary: c s2)
-  apply(simp_all)
+   apply(simp_all)
   done
 
 lemma inside_simp_removal:
@@ -332,7 +346,7 @@
   by (meson map_idI rsimp_inner_idem2)
 
 corollary rsimp_inner_idem4:
-  shows "rsimp r = RALTS rs \<Longrightarrow> flts rs = rs"
+  shows "rsimp r = RALTS rs \<Longrightarrow> rflts rs = rs"
   sorry