--- a/thys3/ClosedForms.thy	Sat May 07 13:38:44 2022 +0100
+++ b/thys3/ClosedForms.thy	Sun May 08 13:26:31 2022 +0100
@@ -1526,15 +1526,22 @@
 
 lemma hfau_pushin: 
   shows "created_by_star r \<Longrightarrow> hflat_aux (rder c r) = concat (map hflat_aux (map (rder c) (hflat_aux r)))"
-  apply(induct r rule: created_by_star.induct)
-   apply simp
-  apply(subgoal_tac "created_by_star (rder c r1)")
-  prefer 2
-  apply(subgoal_tac "created_by_star (rder c r2)")
-  using cbs_ders_cbs apply blast
-  using cbs_ders_cbs apply auto[1]
-  apply simp
-  done
+
+proof(induct r rule: created_by_star.induct)
+  case (1 ra rb)
+  then show ?case by simp
+next
+  case (2 r1 r2)
+  then have "created_by_star (rder c r1)"
+    using cbs_ders_cbs by blast
+  then have "created_by_star (rder c r2)"
+    using "2.hyps"(3) cbs_ders_cbs by auto
+  then show ?case
+    apply simp
+    by (simp add: "2.hyps"(2) "2.hyps"(4))
+  qed
+
+
 
 lemma stupdate_induct1:
   shows " concat (map (hflat_aux \<circ> (rder x \<circ> (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) =
@@ -1606,9 +1613,16 @@
 
 lemma hfau_rsimpeq2:
   shows "created_by_star r \<Longrightarrow> rsimp r = rsimp ( (RALTS (hflat_aux r)))"
+  apply(induct rule: created_by_star.induct)
+   apply simp
+  apply (metis rsimp.simps(6) rsimp_seq_equal1)
+  using cbs_hfau_rsimpeq1 hflat_aux.simps(1) by presburger
+
+  
+(*
+lemma hfau_rsimpeq2_oldproof:  shows "created_by_star r \<Longrightarrow> rsimp r = rsimp ( (RALTS (hflat_aux r)))"
   apply(induct r)
        apply simp+
-  
     apply (metis rsimp_seq_equal1)
   prefer 2
    apply simp
@@ -1616,7 +1630,6 @@
    apply simp
   apply(case_tac "list")
    apply simp
-  
   apply (metis idem_after_simp1)
   apply(case_tac "lista")
   prefer 2
@@ -1627,6 +1640,7 @@
   using hflat_aux.simps(1) apply presburger
   apply simp
   using cbs_hfau_rsimpeq1 by fastforce
+*)
 
 lemma star_closed_form1:
   shows "rsimp (rders (RSTAR r0) (c#s)) =