# HG changeset patch
# User blanchet
# Date 1366902804 -7200
# Node ID 190f89980f7b60100fee9269795578ba446222fb
# Parent  48a0ae342ea00a397bec3573c504f99cc5b4ba35
adjusted stream library to coinduct attributes

diff -r 48a0ae342ea0 -r 190f89980f7b src/HOL/BNF/Examples/Stream.thy
--- a/src/HOL/BNF/Examples/Stream.thy	Thu Apr 25 17:13:24 2013 +0200
+++ b/src/HOL/BNF/Examples/Stream.thy	Thu Apr 25 17:13:24 2013 +0200
@@ -1,7 +1,7 @@
 (*  Title:      HOL/BNF/Examples/Stream.thy
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Andrei Popescu, TU Muenchen
-    Copyright   2012
+    Copyright   2012, 2013
 
 Infinite streams.
 *)
@@ -262,15 +262,15 @@
   by (auto simp: cycle_def)
 
 lemma cycle_decomp: "u \<noteq> [] \<Longrightarrow> cycle u = u @- cycle u"
-proof (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>u. s1 = cycle u \<and> s2 = u @- cycle u \<and> u \<noteq> []"])
-  case (2 s1 s2)
+proof (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>u. s1 = cycle u \<and> s2 = u @- cycle u \<and> u \<noteq> []", consumes 0, case_names _ Eqstream])
+  case (Eqstream s1 s2)
   then obtain u where "s1 = cycle u \<and> s2 = u @- cycle u \<and> u \<noteq> []" by blast
   thus ?case using stream.unfold[of hd "\<lambda>xs. tl xs @ [hd xs]" u] by (auto simp: cycle_def)
 qed auto
 
 lemma cycle_Cons[code]: "cycle (x # xs) = x ## cycle (xs @ [x])"
-proof (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>x xs. s1 = cycle (x # xs) \<and> s2 = x ## cycle (xs @ [x])"])
-  case (2 s1 s2)
+proof (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>x xs. s1 = cycle (x # xs) \<and> s2 = x ## cycle (xs @ [x])", consumes 0, case_names _ Eqstream])
+  case (Eqstream s1 s2)
   then obtain x xs where "s1 = cycle (x # xs) \<and> s2 = x ## cycle (xs @ [x])" by blast
   thus ?case
     by (auto simp: cycle_def intro!: exI[of _ "hd (xs @ [x])"] exI[of _ "tl (xs @ [x])"] stream.unfold)