# HG changeset patch
# User Chengsong
# Date 1652113072 -3600
# Node ID 47618d607bbf52e0e43f1ecc7ecacc75d64f99fb
# Parent  e97681d4edaea9a8bcb96580aa9e6f8e34eb1987
isarfied

diff -r e97681d4edae -r 47618d607bbf thys3/ClosedForms.thy
--- a/thys3/ClosedForms.thy	Sun May 08 15:44:04 2022 +0100
+++ b/thys3/ClosedForms.thy	Mon May 09 17:17:52 2022 +0100
@@ -462,6 +462,16 @@
 
 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))"
   apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = 
                      rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) ")
   prefer 2
@@ -1537,7 +1547,7 @@
   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