# HG changeset patch
# User traytel
# Date 1380713344 -7200
# Node ID e5853a648b59b1855d02b13c130d3065fcd77bb5
# Parent  82d9b2701a036727f05f52313a290f4e540a4820
use new coinduction method and primcorec in examples

diff -r 82d9b2701a03 -r e5853a648b59 src/HOL/BNF/Examples/Derivation_Trees/Prelim.thy
--- a/src/HOL/BNF/Examples/Derivation_Trees/Prelim.thy	Wed Oct 02 11:57:52 2013 +0200
+++ b/src/HOL/BNF/Examples/Derivation_Trees/Prelim.thy	Wed Oct 02 13:29:04 2013 +0200
@@ -28,9 +28,6 @@
 abbreviation sum_case_abbrev ("[[_,_]]" 800)
 where "[[f,g]] \<equiv> Sum_Type.sum_case f g"
 
-lemma inj_Inl[simp]: "inj Inl" unfolding inj_on_def by auto
-lemma inj_Inr[simp]: "inj Inr" unfolding inj_on_def by auto
-
 lemma Inl_oplus_elim:
 assumes "Inl tr \<in> (id \<oplus> f) ` tns"
 shows "Inl tr \<in> tns"
diff -r 82d9b2701a03 -r e5853a648b59 src/HOL/BNF/Examples/Koenig.thy
--- a/src/HOL/BNF/Examples/Koenig.thy	Wed Oct 02 11:57:52 2013 +0200
+++ b/src/HOL/BNF/Examples/Koenig.thy	Wed Oct 02 13:29:04 2013 +0200
@@ -23,13 +23,6 @@
 apply (auto simp add: stl_def)
 by (simp add: Stream_def stream.dtor_ctor)
 
-lemma unfold_pair_fun_shd[simp]: "shd (stream_dtor_unfold (f \<odot> g) t) = f t"
-unfolding shd_def' pair_fun_def stream.dtor_unfold by simp
-
-lemma unfold_pair_fun_stl[simp]: "stl (stream_dtor_unfold (f \<odot> g) t) =
- stream_dtor_unfold (f \<odot> g) (g t)"
-unfolding stl_def' pair_fun_def stream.dtor_unfold by simp
-
 (* infinite trees: *)
 coinductive infiniteTr where
 "\<lbrakk>tr' \<in> listF_set (sub tr); infiniteTr tr'\<rbrakk> \<Longrightarrow> infiniteTr tr"
@@ -50,13 +43,9 @@
 "infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> listF_set (sub tr). infiniteTr tr')"
 by (erule infiniteTr.cases) blast
 
-definition "konigPath \<equiv> stream_dtor_unfold
-  (lab \<odot> (\<lambda>tr. SOME tr'. tr' \<in> listF_set (sub tr) \<and> infiniteTr tr'))"
-
-lemma konigPath_simps[simp]:
-"shd (konigPath t) = lab t"
-"stl (konigPath t) = konigPath (SOME tr. tr \<in> listF_set (sub t) \<and> infiniteTr tr)"
-unfolding konigPath_def by simp+
+primcorec konigPath where
+  "shd (konigPath t) = lab t"
+| "stl (konigPath t) = konigPath (SOME tr. tr \<in> listF_set (sub t) \<and> infiniteTr tr)"
 
 (* proper paths in trees: *)
 coinductive properPath where
@@ -97,16 +86,14 @@
 proof-
   {fix as
    assume "infiniteTr tr \<and> as = konigPath tr" hence "properPath as tr"
-   proof (induct rule: properPath_coind, safe)
-     fix t
-     let ?t = "SOME t'. t' \<in> listF_set (sub t) \<and> infiniteTr t'"
-     assume "infiniteTr t"
-     hence "\<exists>t' \<in> listF_set (sub t). infiniteTr t'" by simp
-     hence "\<exists>t'. t' \<in> listF_set (sub t) \<and> infiniteTr t'" by blast
-     hence "?t \<in> listF_set (sub t) \<and> infiniteTr ?t" by (elim someI_ex)
-     moreover have "stl (konigPath t) = konigPath ?t" by simp
-     ultimately show "\<exists>t' \<in> listF_set (sub t).
-             infiniteTr t' \<and> stl (konigPath t) = konigPath t'" by blast
+   proof (coinduction arbitrary: tr as rule: properPath_coind)
+     case (sub tr as)
+     let ?t = "SOME t'. t' \<in> listF_set (sub tr) \<and> infiniteTr t'"
+     from sub have "\<exists>t' \<in> listF_set (sub tr). infiniteTr t'" by simp
+     then have "\<exists>t'. t' \<in> listF_set (sub tr) \<and> infiniteTr t'" by blast
+     then have "?t \<in> listF_set (sub tr) \<and> infiniteTr ?t" by (rule someI_ex)
+     moreover have "stl (konigPath tr) = konigPath ?t" by simp
+     ultimately show ?case using sub by blast
    qed simp
   }
   thus ?thesis using assms by blast
@@ -114,38 +101,33 @@
 
 (* some more stream theorems *)
 
-lemma stream_map[simp]: "smap f = stream_dtor_unfold (f o shd \<odot> stl)"
-unfolding smap_def pair_fun_def shd_def'[abs_def] stl_def'[abs_def]
-  map_pair_def o_def prod_case_beta by simp
-
-definition plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where
-  [simp]: "plus xs ys =
-    stream_dtor_unfold ((%(xs, ys). shd xs + shd ys) \<odot> (%(xs, ys). (stl xs, stl ys))) (xs, ys)"
+primcorec plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where
+  "shd (plus xs ys) = shd xs + shd ys"
+| "stl (plus xs ys) = plus (stl xs) (stl ys)"
 
 definition scalar :: "nat \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<cdot>" 68) where
   [simp]: "scalar n = smap (\<lambda>x. n * x)"
 
-definition ones :: "nat stream" where [simp]: "ones = stream_dtor_unfold ((%x. 1) \<odot> id) ()"
-definition twos :: "nat stream" where [simp]: "twos = stream_dtor_unfold ((%x. 2) \<odot> id) ()"
+primcorec ones :: "nat stream" where "ones = 1 ## ones"
+primcorec twos :: "nat stream" where "twos = 2 ## twos"
 definition ns :: "nat \<Rightarrow> nat stream" where [simp]: "ns n = scalar n ones"
 
 lemma "ones \<oplus> ones = twos"
-by (rule stream.coinduct[of "%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"]) auto
+  by coinduction simp
 
 lemma "n \<cdot> twos = ns (2 * n)"
-by (rule stream.coinduct[of "%x1 x2. \<exists>n. x1 = n \<cdot> twos \<and> x2 = ns (2 * n)"]) force+
+  by coinduction simp
 
 lemma prod_scalar: "(n * m) \<cdot> xs = n \<cdot> m \<cdot> xs"
-by (rule stream.coinduct[of "%x1 x2. \<exists>n m xs. x1 = (n * m) \<cdot> xs \<and> x2 = n \<cdot> m \<cdot> xs"]) force+
+  by (coinduction arbitrary: xs) auto
 
 lemma scalar_plus: "n \<cdot> (xs \<oplus> ys) = n \<cdot> xs \<oplus> n \<cdot> ys"
-by (rule stream.coinduct[of "%x1 x2. \<exists>n xs ys. x1 = n \<cdot> (xs \<oplus> ys) \<and> x2 = n \<cdot> xs \<oplus> n \<cdot> ys"])
-   (force simp: add_mult_distrib2)+
+  by (coinduction arbitrary: xs ys) (auto simp: add_mult_distrib2)
 
 lemma plus_comm: "xs \<oplus> ys = ys \<oplus> xs"
-by (rule stream.coinduct[of "%x1 x2. \<exists>xs ys. x1 = xs \<oplus> ys \<and> x2 = ys \<oplus> xs"]) force+
+  by (coinduction arbitrary: xs ys) auto
 
 lemma plus_assoc: "(xs \<oplus> ys) \<oplus> zs = xs \<oplus> ys \<oplus> zs"
-by (rule stream.coinduct[of "%x1 x2. \<exists>xs ys zs. x1 = (xs \<oplus> ys) \<oplus> zs \<and> x2 = xs \<oplus> ys \<oplus> zs"]) force+
+  by (coinduction arbitrary: xs ys zs) auto
 
 end
diff -r 82d9b2701a03 -r e5853a648b59 src/HOL/BNF/Examples/Process.thy
--- a/src/HOL/BNF/Examples/Process.thy	Wed Oct 02 11:57:52 2013 +0200
+++ b/src/HOL/BNF/Examples/Process.thy	Wed Oct 02 13:29:04 2013 +0200
@@ -71,19 +71,10 @@
 
 subsection{* Single-guard fixpoint definition *}
 
-definition
-"BX \<equiv>
- process_unfold
-   (\<lambda> P. True)
-   (\<lambda> P. ''a'')
-   (\<lambda> P. P)
-   undefined
-   undefined
-   ()"
-
-lemma BX: "BX = Action ''a'' BX"
-unfolding BX_def
-using process.unfold(1)[of "\<lambda> P. True" "()"  "\<lambda> P. ''a''" "\<lambda> P. P"] by simp
+primcorec BX where
+  "isAction BX"
+| "prefOf BX = ''a''"
+| "contOf BX = BX"
 
 
 subsection{* Multi-guard fixpoint definitions, simulated with auxiliary arguments *}
@@ -172,28 +163,9 @@
 
 definition "guarded sys \<equiv> \<forall> X Y. sys X \<noteq> VAR Y"
 
-definition
-"solution sys \<equiv>
- process_unfold
-   (isACT sys)
-   (PREF sys)
-   (CONT sys)
-   (CH1 sys)
-   (CH2 sys)"
-
-lemma solution_Action:
-assumes "isACT sys T"
-shows "solution sys T = Action (PREF sys T) (solution sys (CONT sys T))"
-unfolding solution_def
-using process.unfold(1)[of "isACT sys" T "PREF sys" "CONT sys" "CH1 sys" "CH2 sys"]
-  assms by simp
-
-lemma solution_Choice:
-assumes "\<not> isACT sys T"
-shows "solution sys T = Choice (solution sys (CH1 sys T)) (solution sys (CH2 sys T))"
-unfolding solution_def
-using process.unfold(2)[of "isACT sys" T "PREF sys" "CONT sys" "CH1 sys" "CH2 sys"]
-  assms by simp
+primcorec solution where
+  "isACT sys T \<Longrightarrow> solution sys T = Action (PREF sys T) (solution sys (CONT sys T))"
+| "_ \<Longrightarrow> solution sys T = Choice (solution sys (CH1 sys T)) (solution sys (CH2 sys T))"
 
 lemma isACT_VAR:
 assumes g: "guarded sys"
@@ -207,13 +179,13 @@
   case True
   hence T: "isACT sys (sys X)" unfolding isACT_VAR[OF g] .
   show ?thesis
-  unfolding solution_Action[OF T] using solution_Action[of sys "VAR X"] True g
+  unfolding solution.ctr(1)[OF T] using solution.ctr(1)[of sys "VAR X"] True g
   unfolding guarded_def by (cases "sys X", auto)
 next
   case False note FFalse = False
   hence TT: "\<not> isACT sys (sys X)" unfolding isACT_VAR[OF g] .
   show ?thesis
-  unfolding solution_Choice[OF TT] using solution_Choice[of sys "VAR X"] FFalse g
+  unfolding solution.ctr(2)[OF TT] using solution.ctr(2)[of sys "VAR X"] FFalse g
   unfolding guarded_def by (cases "sys X", auto)
 qed
 
@@ -222,29 +194,27 @@
 proof-
   {fix q assume "q = solution sys (PROC p)"
    hence "p = q"
-   proof(induct rule: process_coind)
+   proof (coinduct rule: process_coind)
      case (iss p p')
      from isAction_isChoice[of p] show ?case
      proof
        assume p: "isAction p"
        hence 0: "isACT sys (PROC p)" by simp
-       thus ?thesis using iss not_isAction_isChoice
-       unfolding solution_Action[OF 0] by auto
+       thus ?thesis using iss not_isAction_isChoice by auto
      next
        assume "isChoice p"
        hence 0: "\<not> isACT sys (PROC p)"
        using not_isAction_isChoice by auto
-       thus ?thesis using iss isAction_isChoice
-       unfolding solution_Choice[OF 0] by auto
+       thus ?thesis using iss isAction_isChoice by auto
      qed
    next
      case (Action a a' p p')
      hence 0: "isACT sys (PROC (Action a p))" by simp
-     show ?case using Action unfolding solution_Action[OF 0] by simp
+     show ?case using Action unfolding solution.ctr(1)[OF 0] by simp
    next
      case (Choice p q p' q')
      hence 0: "\<not> isACT sys (PROC (Choice p q))" using not_isAction_isChoice by auto
-     show ?case using Choice unfolding solution_Choice[OF 0] by simp
+     show ?case using Choice unfolding solution.ctr(2)[OF 0] by simp
    qed
   }
   thus ?thesis by metis
@@ -252,11 +222,11 @@
 
 lemma solution_ACT[simp]:
 "solution sys (ACT a T) = Action a (solution sys T)"
-by (metis CONT.simps(3) PREF.simps(3) isACT.simps(3) solution_Action)
+by (metis CONT.simps(3) PREF.simps(3) isACT.simps(3) solution.ctr(1))
 
 lemma solution_CH[simp]:
 "solution sys (CH T1 T2) = Choice (solution sys T1) (solution sys T2)"
-by (metis CH1.simps(3) CH2.simps(3) isACT.simps(4) solution_Choice)
+by (metis CH1.simps(3) CH2.simps(3) isACT.simps(4) solution.ctr(2))
 
 
 (* Example: *)
diff -r 82d9b2701a03 -r e5853a648b59 src/HOL/BNF/Examples/Stream.thy
--- a/src/HOL/BNF/Examples/Stream.thy	Wed Oct 02 11:57:52 2013 +0200
+++ b/src/HOL/BNF/Examples/Stream.thy	Wed Oct 02 13:29:04 2013 +0200
@@ -101,14 +101,8 @@
 lemma sset_streams:
   assumes "sset s \<subseteq> A"
   shows "s \<in> streams A"
-proof (coinduct rule: streams.coinduct[of "\<lambda>s'. \<exists>a s. s' = a ## s \<and> a \<in> A \<and> sset s \<subseteq> A"])
-  case streams from assms show ?case by (cases s) auto
-next
-  fix s' assume "\<exists>a s. s' = a ## s \<and> a \<in> A \<and> sset s \<subseteq> A"
-  then guess a s by (elim exE)
-  with assms show "\<exists>a l. s' = a ## l \<and>
-    a \<in> A \<and> ((\<exists>a s. l = a ## s \<and> a \<in> A \<and> sset s \<subseteq> A) \<or> l \<in> streams A)"
-    by (cases s) auto
+using assms proof (coinduction arbitrary: s)
+  case streams then show ?case by (cases s) simp
 qed
 
 
@@ -175,9 +169,9 @@
 lemma smap_alt: "smap f s = s' \<longleftrightarrow> (\<forall>n. f (s !! n) = s' !! n)" (is "?L = ?R")
 proof
   assume ?R
-  thus ?L 
-    by (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>n. s1 = smap f (sdrop n s) \<and> s2 = sdrop n s'", consumes 0])
-      (auto intro: exI[of _ 0] simp del: sdrop.simps(2))
+  then have "\<And>n. smap f (sdrop n s) = sdrop n s'"
+    by coinduction (auto intro: exI[of _ 0] simp del: sdrop.simps(2))
+  then show ?L using sdrop.simps(1) by metis
 qed auto
 
 lemma stake_invert_Nil[iff]: "stake n s = [] \<longleftrightarrow> n = 0"
@@ -218,15 +212,15 @@
   qed (metis comp_apply sdrop.simps(1) sdrop_while.simps snth.simps(1))
 qed
 
-definition "sfilter P = stream_unfold (shd o sdrop_while (Not o P)) (stl o sdrop_while (Not o P))"
+primcorec sfilter where
+  "shd (sfilter P s) = shd (sdrop_while (Not o P) s)"
+| "stl (sfilter P s) = sfilter P (stl (sdrop_while (Not o P) s))"
 
 lemma sfilter_Stream: "sfilter P (x ## s) = (if P x then x ## sfilter P s else sfilter P s)"
 proof (cases "P x")
-  case True thus ?thesis unfolding sfilter_def
-    by (subst stream.unfold) (simp add: sdrop_while_Stream)
+  case True thus ?thesis by (subst sfilter.ctr) (simp add: sdrop_while_Stream)
 next
-  case False thus ?thesis unfolding sfilter_def
-    by (subst (1 2) stream.unfold) (simp add: sdrop_while_Stream)
+  case False thus ?thesis by (subst (1 2) sfilter.ctr) (simp add: sdrop_while_Stream)
 qed
 
 
@@ -243,28 +237,17 @@
 
 subsection {* recurring stream out of a list *}
 
-definition cycle :: "'a list \<Rightarrow> 'a stream" where
-  "cycle = stream_unfold hd (\<lambda>xs. tl xs @ [hd xs])"
-
-lemma cycle_simps[simp]:
-  "shd (cycle u) = hd u"
-  "stl (cycle u) = cycle (tl u @ [hd u])"
-  by (auto simp: cycle_def)
-
+primcorec cycle :: "'a list \<Rightarrow> 'a stream" where
+  "shd (cycle xs) = hd xs"
+| "stl (cycle xs) = cycle (tl xs @ [hd xs])"
 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> []", consumes 0, case_names _ Eq_stream])
-  case (Eq_stream 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
+proof (coinduction arbitrary: u)
+  case Eq_stream then show ?case using stream.collapse[of "cycle u"]
+    by (auto intro!: exI[of _ "tl u @ [hd u]"])
+qed
 
 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])", consumes 0, case_names _ Eq_stream])
-  case (Eq_stream 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)
-qed auto
+  by (subst cycle.ctr) simp
 
 lemma cycle_rotated: "\<lbrakk>v \<noteq> []; cycle u = v @- s\<rbrakk> \<Longrightarrow> cycle (tl u @ [hd u]) = tl v @- s"
   by (auto dest: arg_cong[of _ _ stl])
@@ -304,13 +287,9 @@
 
 subsection {* stream repeating a single element *}
 
-definition "same x = stream_unfold (\<lambda>_. x) id ()"
-
-lemma same_simps[simp]: "shd (same x) = x" "stl (same x) = same x"
-  unfolding same_def by auto
-
-lemma same_unfold[code]: "same x = x ## same x"
-  by (metis same_simps stream.collapse)
+primcorec same where
+  "shd (same x) = x"
+| "stl (same x) = same x"
 
 lemma snth_same[simp]: "same x !! n = x"
   unfolding same_def by (induct n) auto
@@ -328,18 +307,13 @@
   unfolding stream_all_def by auto
 
 lemma same_cycle: "same x = cycle [x]"
-  by (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. s1 = same x \<and> s2 = cycle [x]"]) auto
+  by coinduction auto
 
 
 subsection {* stream of natural numbers *}
 
-definition "fromN n = stream_unfold id Suc n"
-
-lemma fromN_simps[simp]: "shd (fromN n) = n" "stl (fromN n) = fromN (Suc n)"
-  unfolding fromN_def by auto
-
-lemma fromN_unfold[code]: "fromN n = n ## fromN (Suc n)"
-  unfolding fromN_def by (metis id_def stream.unfold)
+primcorec fromN :: "nat \<Rightarrow> nat stream" where
+  "fromN n = n ## fromN (n + 1)"
 
 lemma snth_fromN[simp]: "fromN n !! m = n + m"
   unfolding fromN_def by (induct m arbitrary: n) auto
@@ -352,12 +326,12 @@
 
 lemma sset_fromN[simp]: "sset (fromN n) = {n ..}" (is "?L = ?R")
 proof safe
-  fix m assume "m : ?L"
+  fix m assume "m \<in> ?L"
   moreover
   { fix s assume "m \<in> sset s" "\<exists>n'\<ge>n. s = fromN n'"
-    hence "n \<le> m" by (induct arbitrary: n rule: sset_induct1) fastforce+
+    hence "n \<le> m"  by (induct arbitrary: n rule: sset_induct1) fastforce+
   }
-  ultimately show "n \<le> m" by blast
+  ultimately show "n \<le> m" by auto
 next
   fix m assume "n \<le> m" thus "m \<in> ?L" by (metis le_iff_add snth_fromN snth_sset)
 qed
@@ -367,16 +341,12 @@
 
 subsection {* flatten a stream of lists *}
 
-definition flat where
-  "flat \<equiv> stream_unfold (hd o shd) (\<lambda>s. if tl (shd s) = [] then stl s else tl (shd s) ## stl s)"
-
-lemma flat_simps[simp]:
+primcorec flat where
   "shd (flat ws) = hd (shd ws)"
-  "stl (flat ws) = flat (if tl (shd ws) = [] then stl ws else tl (shd ws) ## stl ws)"
-  unfolding flat_def by auto
+| "stl (flat ws) = flat (if tl (shd ws) = [] then stl ws else tl (shd ws) ## stl ws)"
 
 lemma flat_Cons[simp, code]: "flat ((x # xs) ## ws) = x ## flat (if xs = [] then ws else xs ## ws)"
-  unfolding flat_def using stream.unfold[of "hd o shd" _ "(x # xs) ## ws"] by auto
+  by (subst flat.ctr) simp
 
 lemma flat_Stream[simp]: "xs \<noteq> [] \<Longrightarrow> flat (xs ## ws) = xs @- flat ws"
   by (induct xs) auto
@@ -465,17 +435,13 @@
 
 subsection {* interleave two streams *}
 
-definition sinterleave :: "'a stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where
-  [code del]: "sinterleave s1 s2 =
-    stream_unfold (\<lambda>(s1, s2). shd s1) (\<lambda>(s1, s2). (s2, stl s1)) (s1, s2)"
-
-lemma sinterleave_simps[simp]:
-  "shd (sinterleave s1 s2) = shd s1" "stl (sinterleave s1 s2) = sinterleave s2 (stl s1)"
-  unfolding sinterleave_def by auto
+primcorec sinterleave where
+  "shd (sinterleave s1 s2) = shd s1"
+| "stl (sinterleave s1 s2) = sinterleave s2 (stl s1)"
 
 lemma sinterleave_code[code]:
   "sinterleave (x ## s1) s2 = x ## sinterleave s2 s1"
-  by (metis sinterleave_simps stream.exhaust stream.sel)
+  by (subst sinterleave.ctr) simp
 
 lemma sinterleave_snth[simp]:
   "even n \<Longrightarrow> sinterleave s1 s2 !! n = s1 !! (n div 2)"
@@ -507,15 +473,12 @@
 
 subsection {* zip *}
 
-definition "szip s1 s2 =
-  stream_unfold (map_pair shd shd) (map_pair stl stl) (s1, s2)"
-
-lemma szip_simps[simp]:
-  "shd (szip s1 s2) = (shd s1, shd s2)" "stl (szip s1 s2) = szip (stl s1) (stl s2)"
-  unfolding szip_def by auto
+primcorec szip where
+  "shd (szip s1 s2) = (shd s1, shd s2)"
+| "stl (szip s1 s2) = szip (stl s1) (stl s2)"
 
 lemma szip_unfold[code]: "szip (Stream a s1) (Stream b s2) = Stream (a, b) (szip s1 s2)"
-  unfolding szip_def by (subst stream.unfold) simp
+  by (subst szip.ctr) simp
 
 lemma snth_szip[simp]: "szip s1 s2 !! n = (s1 !! n, s2 !! n)"
   by (induct n arbitrary: s1 s2) auto
@@ -523,35 +486,24 @@
 
 subsection {* zip via function *}
 
-definition "smap2 f s1 s2 =
-  stream_unfold (\<lambda>(s1,s2). f (shd s1) (shd s2)) (map_pair stl stl) (s1, s2)"
-
-lemma smap2_simps[simp]:
+primcorec smap2 where
   "shd (smap2 f s1 s2) = f (shd s1) (shd s2)"
-  "stl (smap2 f s1 s2) = smap2 f (stl s1) (stl s2)"
-  unfolding smap2_def by auto
+| "stl (smap2 f s1 s2) = smap2 f (stl s1) (stl s2)"
 
 lemma smap2_unfold[code]:
   "smap2 f (Stream a s1) (Stream b s2) = Stream (f a b) (smap2 f s1 s2)"
-  unfolding smap2_def by (subst stream.unfold) simp
+  by (subst smap2.ctr) simp
 
 lemma smap2_szip:
   "smap2 f s1 s2 = smap (split f) (szip s1 s2)"
-  by (coinduct rule: stream.coinduct[of
-    "\<lambda>s1 s2. \<exists>s1' s2'. s1 = smap2 f s1' s2' \<and> s2 = smap (split f) (szip s1' s2')"])
-    fastforce+
+  by (coinduction arbitrary: s1 s2) auto
 
 
 subsection {* iterated application of a function *}
 
-definition siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
-  "siterate f x = x ## stream_unfold f f x"
-
-lemma siterate_simps[simp]: "shd (siterate f x) = x" "stl (siterate f x) = siterate f (f x)"
-  unfolding siterate_def by (auto intro: stream.unfold)
-
-lemma siterate_code[code]: "siterate f x = x ## siterate f (f x)"
-  by (metis siterate_def stream.unfold)
+primcorec siterate where
+  "shd (siterate f x) = x"
+| "stl (siterate f x) = siterate f (f x)"
 
 lemma stake_Suc: "stake (Suc n) s = stake n s @ [s !! n]"
   by (induct n arbitrary: s) auto
diff -r 82d9b2701a03 -r e5853a648b59 src/HOL/BNF/Examples/TreeFI.thy
--- a/src/HOL/BNF/Examples/TreeFI.thy	Wed Oct 02 11:57:52 2013 +0200
+++ b/src/HOL/BNF/Examples/TreeFI.thy	Wed Oct 02 13:29:04 2013 +0200
@@ -14,17 +14,10 @@
 
 codatatype 'a treeFI = Tree (lab: 'a) (sub: "'a treeFI listF")
 
-definition pair_fun (infixr "\<odot>" 50) where
-  "f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
-
 (* Tree reverse:*)
-definition "trev \<equiv> treeFI_unfold lab (lrev o sub)"
-
-lemma trev_simps1[simp]: "lab (trev t) = lab t"
-  unfolding trev_def by simp
-
-lemma trev_simps2[simp]: "sub (trev t) = mapF trev (lrev (sub t))"
-  unfolding trev_def by simp
+primcorec trev where
+  "lab (trev t) = lab t"
+| "sub (trev t) = mapF trev (lrev (sub t))"
 
 lemma treeFI_coinduct:
   assumes *: "phi x y"
@@ -33,9 +26,10 @@
      lengthh (sub a) = lengthh (sub b) \<and>
      (\<forall>i < lengthh (sub a). phi (nthh (sub a) i) (nthh (sub b) i))"
   shows "x = y"
-using * proof (coinduct rule: treeFI.coinduct)
-  fix t1 t2 assume "phi t1 t2" note * = step[OF this] and ** = conjunct2[OF *]
-  from conjunct1[OF **] conjunct2[OF **] have "relF phi (sub t1) (sub t2)"
+using * proof (coinduction arbitrary: x y)
+  case (Eq_treeFI t1 t2)
+  from conjunct1[OF conjunct2[OF step[OF Eq_treeFI]]] conjunct2[OF conjunct2[OF step[OF Eq_treeFI]]]
+  have "relF phi (sub t1) (sub t2)"
   proof (induction "sub t1" "sub t2" arbitrary: t1 t2 rule: listF_induct2)
     case (Conss x xs y ys)
     note sub = Conss(2,3)[symmetric] and phi = mp[OF spec[OF Conss(4)], unfolded sub]
@@ -43,10 +37,10 @@
         unfolded sub, simplified]
     from phi[of 0] show ?case unfolding sub by (auto intro!: IH dest: phi[simplified, OF Suc_mono])
   qed simp
-  with conjunct1[OF *] show "lab t1 = lab t2 \<and> relF phi (sub t1) (sub t2)" ..
+  with conjunct1[OF step[OF Eq_treeFI]] show ?case by simp
 qed
 
 lemma trev_trev: "trev (trev tr) = tr"
-  by (rule treeFI_coinduct[of "%a b. trev (trev b) = a"]) auto
+  by (coinduction arbitrary: tr rule: treeFI_coinduct) auto
 
 end
diff -r 82d9b2701a03 -r e5853a648b59 src/HOL/BNF/Examples/TreeFsetI.thy
--- a/src/HOL/BNF/Examples/TreeFsetI.thy	Wed Oct 02 11:57:52 2013 +0200
+++ b/src/HOL/BNF/Examples/TreeFsetI.thy	Wed Oct 02 13:29:04 2013 +0200
@@ -16,22 +16,12 @@
 
 codatatype 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
 
-definition pair_fun (infixr "\<odot>" 50) where
-  "f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
-
 (* tree map (contrived example): *)
-definition tmap where
-"tmap f = treeFsetI_unfold (f o lab) sub"
-
-lemma tmap_simps[simp]:
-"lab (tmap f t) = f (lab t)"
+primcorec tmap where
+"lab (tmap f t) = f (lab t)" |
 "sub (tmap f t) = fimage (tmap f) (sub t)"
-unfolding tmap_def treeFsetI.sel_unfold by simp+
 
 lemma "tmap (f o g) x = tmap f (tmap g x)"
-apply (rule treeFsetI.coinduct[of "%x1 x2. \<exists>x. x1 = tmap (f o g) x \<and> x2 = tmap f (tmap g x)"])
-apply auto
-apply (unfold fset_rel_alt)
-by auto
+  by (coinduction arbitrary: x) (auto simp: fset_rel_alt)
 
 end