Mercurial Mercurial > hg > lexing / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
isarfied
authorChengsong
Mon, 09 May 2022 17:17:52 +0100
changeset 511 47618d607bbf
parent 510 e97681d4edae
child 512 a4b86ced5c32
isarfied
thys3/ClosedForms.thy file | annotate | diff | comparison | revisions 
--- 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
lexing