# HG changeset patch
# User blanchet
# Date 1458646777 -3600
# Node ID 7325d8573fb87f0d61f0891eee958c00efcfbae6
# Parent  b287b56a6ce556194a31f22bd3245823985387be
added 'corec' examples and tests

diff -r b287b56a6ce5 -r 7325d8573fb8 src/HOL/Corec_Examples/Tests/GPV_Bare_Bones.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Corec_Examples/Tests/GPV_Bare_Bones.thy	Tue Mar 22 12:39:37 2016 +0100
@@ -0,0 +1,48 @@
+(*  Title:      HOL/Corec_Examples/Tests/GPV_Bare_Bones
+    Author:     Andreas Lochbihler, ETH Zuerich
+    Author:     Jasmin Blanchette, Inria, LORIA, MPII
+    Copyright   2016
+
+A bare bones version of generative probabilistic values (GPVs).
+*)
+
+section {* A Bare Bones Version of Generative Probabilistic Values (GPVs) *}
+
+theory GPV_Bare_Bones
+imports "~~/src/HOL/Library/BNF_Corec"
+begin
+
+datatype 'a pmf = return_pmf 'a
+
+type_synonym 'a spmf = "'a option pmf"
+
+abbreviation map_spmf :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a spmf \<Rightarrow> 'b spmf"
+where "map_spmf f \<equiv> map_pmf (map_option f)"
+
+abbreviation return_spmf :: "'a \<Rightarrow> 'a spmf"
+where "return_spmf x \<equiv> return_pmf (Some x)"
+
+datatype (generat_pures: 'a, generat_outs: 'b, generat_conts: 'c) generat =
+  Pure (result: 'a)
+| IO ("output": 'b) (continuation: "'c")
+
+codatatype (results'_gpv: 'a, outs'_gpv: 'out, 'in) gpv =
+  GPV (the_gpv: "('a, 'out, 'in \<Rightarrow> ('a, 'out, 'in) gpv) generat spmf")
+
+codatatype ('a, 'call, 'ret, 'x) gpv' =
+  GPV' (the_gpv': "('a, 'call, 'ret \<Rightarrow> ('a, 'call, 'ret, 'x) gpv') generat spmf")
+
+consts bind_gpv' :: "('a, 'call, 'ret) gpv \<Rightarrow> ('a \<Rightarrow> ('b, 'call, 'ret, 'a) gpv') \<Rightarrow> ('b, 'call, 'ret, 'a) gpv'"
+
+definition bind_spmf :: "'a spmf \<Rightarrow> ('a \<Rightarrow> 'b spmf) \<Rightarrow> 'b spmf"
+where "bind_spmf x f = undefined x (\<lambda>a. case a of None \<Rightarrow> return_pmf None | Some a' \<Rightarrow> f a')"
+
+friend_of_corec bind_gpv'
+where "bind_gpv' r f =
+GPV' (map_spmf (map_generat id id (op \<circ> (case_sum id (\<lambda>r. bind_gpv' r f))))
+      (bind_spmf (the_gpv r)
+        (case_generat (\<lambda>x. map_spmf (map_generat id id (op \<circ> Inl)) (the_gpv' (f x)))
+          (\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))))))"
+  sorry
+
+end
diff -r b287b56a6ce5 -r 7325d8573fb8 src/HOL/Corec_Examples/Tests/Merge_A.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Corec_Examples/Tests/Merge_A.thy	Tue Mar 22 12:39:37 2016 +0100
@@ -0,0 +1,32 @@
+(*  Title:      HOL/Corec_Examples/Tests/Merge_A.thy
+    Author:     Aymeric Bouzy, Ecole polytechnique
+    Author:     Jasmin Blanchette, Inria, LORIA, MPII
+    Copyright   2015, 2016
+
+Tests theory merges.
+*)
+
+section {* Tests Theory Merges *}
+
+theory Merge_A
+imports "~~/src/HOL/Library/BNF_Corec"
+begin
+
+codatatype 'a ta = Ca (sa1: 'a) (sa2: "'a ta")
+
+consts gb :: "'a ta \<Rightarrow> 'a ta"
+
+corec fa where
+  "fa = Ca (Suc 0) fa"
+
+corec ga :: "'a ta \<Rightarrow> 'a ta" where
+  "ga t = Ca (sa1 t) (sa2 t)"
+
+friend_of_corec ga :: "'a ta \<Rightarrow> 'a ta" where
+  "ga t = Ca (sa1 t) (Ca (sa1 t) (sa2 t))"
+  sorry
+
+thm ta.coinduct_upto
+thm ta.cong_refl
+
+end
diff -r b287b56a6ce5 -r 7325d8573fb8 src/HOL/Corec_Examples/Tests/Merge_B.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Corec_Examples/Tests/Merge_B.thy	Tue Mar 22 12:39:37 2016 +0100
@@ -0,0 +1,26 @@
+(*  Title:      HOL/Corec_Examples/Tests/Merge_A.thy
+    Author:     Aymeric Bouzy, Ecole polytechnique
+    Author:     Jasmin Blanchette, Inria, LORIA, MPII
+    Copyright   2015, 2016
+
+Tests theory merges.
+*)
+
+section {* Tests Theory Merges *}
+
+theory Merge_B
+imports Merge_A
+begin
+
+consts fb :: "'a ta \<Rightarrow> 'a ta"
+consts gb :: "'a ta \<Rightarrow> 'a ta"
+
+friend_of_corec fb :: "'a ta \<Rightarrow> 'a ta" where
+  "fb t = Ca (sa1 t) (sa2 t)"
+  sorry
+
+friend_of_corec gb :: "'a ta \<Rightarrow> 'a ta" where
+  "gb t = Ca (sa1 t) (sa2 t)"
+  sorry
+
+end
diff -r b287b56a6ce5 -r 7325d8573fb8 src/HOL/Corec_Examples/Tests/Merge_C.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Corec_Examples/Tests/Merge_C.thy	Tue Mar 22 12:39:37 2016 +0100
@@ -0,0 +1,30 @@
+(*  Title:      HOL/Corec_Examples/Tests/Merge_A.thy
+    Author:     Aymeric Bouzy, Ecole polytechnique
+    Author:     Jasmin Blanchette, Inria, LORIA, MPII
+    Copyright   2015, 2016
+
+Tests theory merges.
+*)
+
+section {* Tests Theory Merges *}
+
+theory Merge_C
+imports Merge_A
+begin
+
+consts fc :: "'a ta \<Rightarrow> 'a ta"
+consts gc :: "'a ta \<Rightarrow> 'a ta"
+
+friend_of_corec fc :: "'a ta \<Rightarrow> 'a ta" where
+  "fc t = Ca (sa1 t) (sa2 t)"
+  sorry
+
+friend_of_corec gb :: "'a ta \<Rightarrow> 'a ta" where
+  "gb t = Ca (sa1 t) (sa2 t)"
+  sorry
+
+friend_of_corec gc :: "'a ta \<Rightarrow> 'a ta" where
+  "gc t = Ca (sa1 t) (sa2 t)"
+  sorry
+
+end
diff -r b287b56a6ce5 -r 7325d8573fb8 src/HOL/Corec_Examples/Tests/Merge_D.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Corec_Examples/Tests/Merge_D.thy	Tue Mar 22 12:39:37 2016 +0100
@@ -0,0 +1,41 @@
+(*  Title:      HOL/Corec_Examples/Tests/Merge_A.thy
+    Author:     Aymeric Bouzy, Ecole polytechnique
+    Author:     Jasmin Blanchette, Inria, LORIA, MPII
+    Copyright   2015, 2016
+
+Tests theory merges.
+*)
+
+section {* Tests Theory Merges *}
+
+theory Merge_D
+imports Merge_B Merge_C
+begin
+
+thm ta.coinduct_upto
+
+(* Merges files having defined their own friends and uses these friends to
+define another corecursive function. *)
+
+corec gd where
+  "gd = fc (gc (gb (fb (ga (Ca 0 gd)))))"
+
+thm gd_def
+
+term fc
+
+corec hd :: "('a::zero) ta \<Rightarrow> 'a ta" where
+  "hd s = fc (gc (gb (fb (ga (Ca 0 (hd s))))))"
+
+friend_of_corec hd where
+  "hd s = Ca 0 (fc (gc (gb (fb (ga (Ca 0 (hd s)))))))"
+  sorry
+
+corecursive (friend) ff :: "'a ta \<Rightarrow> 'a ta" where
+  "ff x = Ca undefined (ff x)"
+  sorry
+
+thm ta.cong_intros
+thm ta.cong_gb
+
+end
diff -r b287b56a6ce5 -r 7325d8573fb8 src/HOL/Corec_Examples/Tests/Merge_Poly.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Corec_Examples/Tests/Merge_Poly.thy	Tue Mar 22 12:39:37 2016 +0100
@@ -0,0 +1,133 @@
+(*  Title:      HOL/Corec_Examples/Tests/Merge_Poly.thy
+    Author:     Aymeric Bouzy, Ecole polytechnique
+    Author:     Jasmin Blanchette, Inria, LORIA, MPII
+    Copyright   2015, 2016
+
+Tests polymorphic merges.
+*)
+
+section {* Tests Polymorphic Merges *}
+
+theory Merge_Poly
+imports "~~/src/HOL/Library/BNF_Corec"
+begin
+
+subsection {* A Monomorphic Example *}
+
+codatatype r = R (rhd: nat) (rtl: r)
+
+corec id_r :: "r \<Rightarrow> r" where
+  "id_r r = R (rhd r) (id_r (rtl r))"
+
+corec id_r' :: "r \<Rightarrow> r" where
+  "id_r' r = R (rhd r) (id_r' (rtl r))"
+
+corec id_r'' :: "r \<Rightarrow> r" where
+  "id_r'' r = R (rhd r) (id_r'' (rtl r))"
+
+consts
+  f1 :: "r \<Rightarrow> r"
+  f2 :: "r \<Rightarrow> r"
+  f3 :: "r \<Rightarrow> r"
+
+friend_of_corec f1 :: "r \<Rightarrow> r" where
+  "f1 r = R (rhd r) (f1 (R (rhd r) (rtl r)))"
+  sorry
+
+friend_of_corec f2 :: "r \<Rightarrow> r" where
+  "f2 r = R (rhd r) (f1 (f2 (rtl r)))"
+  sorry
+
+friend_of_corec f3 :: "r \<Rightarrow> r" where
+  "f3 r = R (rhd r) (f3 (rtl r))"
+  sorry
+
+corec id_rx :: "r \<Rightarrow> r" where
+  "id_rx r = f1 (f2 (f3 (R (rhd r) (id_rx (rtl r)))))"
+
+
+subsection {* The Polymorphic Version *}
+
+codatatype 'a s = S (shd: 'a) (stl: "'a s")
+
+corec id_s :: "'a s \<Rightarrow> 'a s" where
+  "id_s s = S (shd s) (id_s (stl s))"
+
+corec id_s' :: "'b s \<Rightarrow> 'b s" where
+  "id_s' s = S (shd s) (id_s' (stl s))"
+
+corec id_s'' :: "'w s \<Rightarrow> 'w s" where
+  "id_s'' s = S (shd s) (id_s'' (stl s))"
+
+(* Registers polymorphic and nonpolymorphic friends in an alternating fashion. *)
+
+consts
+  g1 :: "'a \<Rightarrow> 'a s \<Rightarrow> 'a s"
+  g2 :: "nat \<Rightarrow> nat s \<Rightarrow> nat s"
+  g3 :: "'a \<Rightarrow> 'a s \<Rightarrow> 'a s"
+  g4 :: "'a \<Rightarrow> 'a s \<Rightarrow> 'a s"
+  g5 :: "nat \<Rightarrow> nat s \<Rightarrow> nat s"
+
+friend_of_corec g3 :: "'b \<Rightarrow> 'b s \<Rightarrow> 'b s" where
+  "g3 x s = S (shd s) (g3 x (stl s))"
+  sorry
+
+friend_of_corec g1 :: "'w \<Rightarrow> 'w s \<Rightarrow> 'w s" where
+  "g1 x s = S (shd s) (g1 x (stl s))"
+  sorry
+
+friend_of_corec g2 :: "nat \<Rightarrow> nat s \<Rightarrow> nat s" where
+  "g2 x s = S (shd s) (g1 x (stl s))"
+  sorry
+
+friend_of_corec g4 :: "'a \<Rightarrow> 'a s \<Rightarrow> 'a s" where
+  "g4 x s = S (shd s) (g1 x (g4 x (stl s)))"
+  sorry
+
+friend_of_corec g5 :: "nat \<Rightarrow> nat s \<Rightarrow> nat s" where
+  "g5 x s = S (shd s) (g2 x (g5 x (stl s)))"
+  sorry
+
+corec id_nat_s :: "nat s \<Rightarrow> nat s" where
+  "id_nat_s s = g1 undefined (g2 undefined (g3 undefined (S (shd s) (id_nat_s (stl s)))))"
+
+codatatype ('a, 'b) ABstream = ACons 'a (ABtl: "('a, 'b) ABstream") | BCons 'b (ABtl: "('a, 'b) ABstream")
+
+consts
+  h1 :: "('a, 'b) ABstream \<Rightarrow> ('a, 'b) ABstream"
+  h2 :: "(nat, 'b) ABstream \<Rightarrow> (nat, 'b) ABstream"
+  h3 :: "('a, nat) ABstream \<Rightarrow> ('a, nat) ABstream"
+  h4 :: "('a :: zero, 'a) ABstream \<Rightarrow> ('a :: zero, 'a) ABstream"
+
+friend_of_corec h1 where
+  "h1 x = ACons undefined undefined" sorry
+
+friend_of_corec h2 where 
+  "h2 x = (case x of 
+    ACons a t \<Rightarrow> ACons a (h1 (h2 t)) 
+  | BCons b t \<Rightarrow> BCons b (h1 (h2 t)))"
+  sorry
+
+friend_of_corec h3 where
+  "h3 x = (case x of 
+    ACons a t \<Rightarrow> ACons a (h1 (h3 t)) 
+  | BCons b t \<Rightarrow> BCons b (h1 (h3 t)))"
+  sorry
+
+friend_of_corec h4 where
+  "h4 x = (case x of 
+    ACons a t \<Rightarrow> ACons a (h1 (h4 t)) 
+  | BCons b t \<Rightarrow> BCons b (h1 (h4 t)))"
+  sorry
+
+corec (friend) h5 where
+  "h5 x = (case x of
+    ACons a t \<Rightarrow> ACons a (h1 (h2 (h3 (h4 (h5 t)))))
+  | BCons b t \<Rightarrow> BCons b (h1 (h2 (h3 (h4 (h5 t))))))"
+
+corec (friend) h6 :: "(nat, nat) ABstream \<Rightarrow> (nat, nat) ABstream" where
+  "h6 x = (case x of
+    ACons a t \<Rightarrow> ACons a (h6 (h1 (h2 (h3 (h4 (h5 (h6 t)))))))
+  | BCons b t \<Rightarrow> BCons b (h1 (h2 (h3 (h4 (h5 (h6 t)))))))"
+
+end
diff -r b287b56a6ce5 -r 7325d8573fb8 src/HOL/Corec_Examples/Tests/Misc_Mono.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Corec_Examples/Tests/Misc_Mono.thy	Tue Mar 22 12:39:37 2016 +0100
@@ -0,0 +1,435 @@
+(*  Title:      HOL/Corec_Examples/Tests/Misc_Mono.thy
+    Author:     Aymeric Bouzy, Ecole polytechnique
+    Author:     Jasmin Blanchette, Inria, LORIA, MPII
+    Copyright   2015, 2016
+
+Miscellaneous monomorphic examples.
+*)
+
+section {* Miscellaneous Monomorphic Examples *}
+
+theory Misc_Mono
+imports "~~/src/HOL/Library/BNF_Corec"
+begin
+
+codatatype T0 =
+  C1 (lab: nat) (tl11: T0) (tl12: T0)
+| C2 (lab: nat) (tl2: T0)
+| C3 (tl3: "T0 list")
+
+codatatype stream =
+  S (hd: nat) (tl: stream)
+
+corec (friend) ff where
+  "ff x = S 0 (ff (ff x))"
+
+corec test0 where
+  "test0 x y = (case (x, y) of
+  (S a1 s1, S a2 s2) \<Rightarrow> S (a1 + a2) (test0 s1 s2))"
+
+friend_of_corec test0 where
+  "test0 x y = (case (x, y) of
+  (S a1 s1, S a2 s2) \<Rightarrow> S (a1 + a2) (test0 s1 s2))"
+   apply (rule test0.code)
+  apply transfer_prover
+  done
+
+corec test01 where
+  "test01 x y = C2 (lab x + lab y) (test01 (tl2 x) (tl2 y))"
+
+friend_of_corec test01 where
+  "test01 x y = C2 (lab x + lab y) (test01 (tl2 x) (tl2 y))"
+   apply (rule test01.code)
+  sorry (* not parametric *)
+
+corec test02 where
+  "test02 x y = C2 (lab x * lab y) (test01 (test02 x (tl2 y)) (test02 (tl2 x) y))"
+
+friend_of_corec test02 where
+  "test02 x y = C2 (lab x * lab y) (test01 (test02 x (tl2 y)) (test02 (tl2 x) y))"
+   apply (rule test02.code)
+  sorry (* not parametric *)
+
+corec test03 where
+  "test03 x = C2 (lab x) (C2 (lab x) (test02 (test03 (tl2 x)) (test03 (tl2 x))))"
+
+friend_of_corec test03 where
+  "test03 x = C2 (lab x) (C2 (lab x) (test02 (test03 (tl2 x)) (test03 (tl2 x))))"
+   apply (rule test03.code)
+  sorry (* not parametric *)
+
+corec (friend) test04a where
+  "test04a x = (case x of C1 a t1 t2 \<Rightarrow> C1 (a * a) (test04a t1) (test04a t2) | C2 a t \<Rightarrow> C2 (a * a) (test04a t) | C3 l \<Rightarrow> C3 l)"
+
+corec test04 where
+  "test04 x = (case x of C1 a t1 t2 \<Rightarrow> C1 (a * a) (test04 t1) (test04 t2) | C2 a t \<Rightarrow> C2 (a * a) (test04 t) | C3 l \<Rightarrow> C3 l)"
+
+friend_of_corec test04 where
+  "test04 x = (case x of C1 a t1 t2 \<Rightarrow> C1 (a * a) (test04 t1) (test04 t2) | C2 a t \<Rightarrow> C2 (a * a) (test04 t) | C3 l \<Rightarrow> C3 l)"
+   apply (rule test04.code)
+  apply transfer_prover
+  done
+
+corec test05 where
+  "test05 x y = (case (x, y) of
+  (C1 a t11 t12, C1 b t21 t22) \<Rightarrow> C1 (a + b) (test05 t11 t21) (test05 t12 t22)
+| (C1 a t11 _, C2 b t2) \<Rightarrow> C2 (a + b) (test05 t11 t2)
+| (C2 a t1, C1 b _ t22) \<Rightarrow> C2 (a + b) (test05 t1 t22)
+| (C2 a t1, C2 b t2) \<Rightarrow> C2 (a + b) (test05 t1 t2)
+| (_, _) \<Rightarrow> C3 [])"
+
+friend_of_corec test05 where
+  "test05 x y = (case (x, y) of
+  (C1 a t11 t12, C1 b t21 t22) \<Rightarrow> C1 (a + b) (test05 t11 t21) (test05 t12 t22)
+| (C1 a t11 _, C2 b t2) \<Rightarrow> C2 (a + b) (test05 t11 t2)
+| (C2 a t1, C1 b _ t22) \<Rightarrow> C2 (a + b) (test05 t1 t22)
+| (C2 a t1, C2 b t2) \<Rightarrow> C2 (a + b) (test05 t1 t2)
+| (_, _) \<Rightarrow> C3 [])"
+   apply (rule test05.code)
+  apply transfer_prover
+  done
+
+corec test06 :: "T0 \<Rightarrow> T0" where
+  "test06 x =
+  (if \<not> is_C1 x then
+    let tail = tl2 x in
+    C1 (lab x) (test06 tail) tail
+  else
+    C2 (lab x) (test06 (tl12 x)))"
+
+friend_of_corec test06 :: "T0 \<Rightarrow> T0" where
+  "test06 x =
+  (if \<not> is_C1 x then
+    let tail = tl2 x in
+    C1 (lab x) (test06 tail) tail
+  else
+    C2 (lab x) (test06 (tl12 x)))"
+   apply (rule test06.code)
+  sorry (* not parametric *)
+
+corec test07 where
+  "test07 xs = C3 (map (\<lambda>x. test07 (tl3 x)) xs)"
+
+friend_of_corec test07 where
+  "test07 xs = C3 (map (\<lambda>x. test07 (tl3 x)) xs)"
+   apply (rule test07.code)
+  sorry (* not parametric *)
+
+corec test08 where
+  "test08 xs = (case xs of
+    [] \<Rightarrow> C2 0 (test08 [])
+  | T # r \<Rightarrow> C1 1 (test08 r) T)"
+
+friend_of_corec test08 where
+  "test08 xs = (case xs of
+    [] \<Rightarrow> C2 0 (test08 [])
+  | T # r \<Rightarrow> C1 1 (test08 r) T)"
+   apply (rule test08.code)
+  apply transfer_prover
+  done
+
+corec test09 where
+  "test09 xs = test08 [case xs of
+    [] \<Rightarrow> C2 0 (test09 [])
+  | (C1 n T1 T2) # r \<Rightarrow> C1 n (test09 (T1 # r)) (test09 (T2 # r))
+  | _ # r \<Rightarrow> C3 [test09 r]]"
+
+friend_of_corec test09 where
+  "test09 xs = (case xs of
+    [] \<Rightarrow> C2 0 (test09 [])
+  | (C1 n T1 T2) # r \<Rightarrow> C1 n (test09 (T1 # r)) (test09 (T2 # r))
+  | _ # r \<Rightarrow> C3 [test09 r])"
+   defer
+   apply transfer_prover
+  sorry (* not sure the specifications are equal *)
+
+codatatype tree =
+  Node (node: int) (branches: "tree list")
+
+consts integerize_tree_list :: "'a list \<Rightarrow> int"
+
+lemma integerize_tree_list_transfer[transfer_rule]:
+  "rel_fun (list_all2 R) op = integerize_tree_list integerize_tree_list"
+  sorry
+
+corec (friend) f10a where
+  "f10a x y = Node
+  (integerize_tree_list (branches x) + integerize_tree_list (branches y))
+  (map (\<lambda>(x, y). f10a x y) (zip (branches x) (branches y)))"
+
+corec f10 where
+  "f10 x y = Node
+  (integerize_tree_list (branches x) + integerize_tree_list (branches y))
+  (map (\<lambda>(x, y). f10 x y) (zip (branches x) (branches y)))"
+
+friend_of_corec f10 where
+  "f10 x y = Node
+  (integerize_tree_list (branches x) + integerize_tree_list (branches y))
+  (map (\<lambda>(x, y). f10 x y) (zip (branches x) (branches y)))"
+     apply (rule f10.code)
+    by transfer_prover+
+
+corec f12 where
+  "f12 t = Node (node t) (map f12 (branches t))"
+
+friend_of_corec f12 where
+  "f12 t = Node (node t) (map f12 (branches t))"
+  sorry
+
+corec f13 where
+  "f13 n ts = Node n (map (%t. f13 (node t) (branches t)) ts)"
+
+friend_of_corec f13 where
+  "f13 n ts = Node n (map (%t. f13 (node t) (branches t)) ts)"
+  sorry
+
+corec f14 :: "tree option \<Rightarrow> tree" where
+  "f14 t_opt = Node 0
+    (case map_option branches t_opt of
+      None \<Rightarrow> []
+    | Some ts \<Rightarrow> map (f14 o Some) ts)"
+
+friend_of_corec f14 where
+  "f14 t_opt = Node 0
+    (case map_option branches t_opt of
+      None \<Rightarrow> []
+    | Some ts \<Rightarrow> map (f14 o Some) ts)"
+  sorry
+
+corec f15 :: "tree list option \<Rightarrow> tree" where
+  "f15 ts_opt = Node 0
+    (case map_option (map branches) ts_opt of
+      None \<Rightarrow> []
+    | Some tss \<Rightarrow> map (f15 o Some) tss)"
+
+friend_of_corec f15 where
+  "f15 ts_opt = Node 0
+    (case map_option (map branches) ts_opt of
+      None \<Rightarrow> []
+    | Some tss \<Rightarrow> map (f15 o Some) tss)"
+    sorry
+
+corec f16 :: "tree list option \<Rightarrow> tree" where
+  "f16 ts_opt = Node 0
+    (case ts_opt of
+      None \<Rightarrow> []
+    | Some ts \<Rightarrow> map (f16 o Some o branches) ts)"
+
+friend_of_corec f16 where
+  "f16 ts_opt = Node 0
+    (case ts_opt of
+      None \<Rightarrow> []
+    | Some ts \<Rightarrow> map (f16 o Some o branches) ts)"
+    sorry
+
+corec f17 :: "tree list option \<Rightarrow> tree" where
+  "f17 ts_opt = Node 0 (case ts_opt of
+    None \<Rightarrow> []
+  | Some ts \<Rightarrow> [f17 (Some (map (List.hd o branches) ts))])"
+
+(* not parametric
+friend_of_corec f17 where
+  "f17 ts_opt = Node 0 (case ts_opt of
+    None \<Rightarrow> []
+  | Some ts \<Rightarrow> [f17 (Some (map (List.hd o branches) ts))])"
+  sorry
+*)
+
+corec f18 :: "tree \<Rightarrow> tree" where
+  "f18 t = Node (node t) (map (f18 o f12) (branches t))"
+
+friend_of_corec f18 :: "tree \<Rightarrow> tree" where
+  "f18 t = Node (node t) (map (f18 o f12) (branches t))"
+  sorry
+
+corec f19 :: "tree \<Rightarrow> tree" where
+  "f19 t = Node (node t) (map (%f. f [t]) (map f13 [1, 2, 3]))"
+
+friend_of_corec f19 :: "tree \<Rightarrow> tree" where
+  "f19 t = Node (node t) (map (%f. f [t]) (map f13 [1, 2, 3]))"
+  sorry
+
+datatype ('a, 'b, 'c) h = H1 (h_a: 'a) (h_tail: "('a, 'b, 'c) h") | H2 (h_b: 'b) (h_c: 'c) (h_tail: "('a, 'b, 'c) h") | H3
+
+term "map_h (map_option f12) (%n. n) f12"
+
+corec f20 :: "(tree option, int, tree) h \<Rightarrow> tree \<Rightarrow> tree" where
+  "f20 x y = Node (node y) (case (map_h (map_option f12) (%n. n) f12 x) of
+    H1 None r \<Rightarrow> (f20 r y) # (branches y)
+  | H1 (Some t) r \<Rightarrow> (f20 r t) # (branches y)
+  | H2 n t r \<Rightarrow> (f20 r (Node n [])) # (branches y)
+  | H3 \<Rightarrow> branches y)"
+
+friend_of_corec f20 where
+  "f20 x y = Node (node y) (case (map_h (map_option f12) (%n. n) f12 x) of
+    H1 None r \<Rightarrow> (f20 r y) # (branches y)
+  | H1 (Some t) r \<Rightarrow> (f20 r t) # (branches y)
+  | H2 n t r \<Rightarrow> (f20 r (Node n [])) # (branches y)
+  | H3 \<Rightarrow> branches y)"
+  sorry
+
+corec f21 where
+  "f21 x xh =
+  Node (node x) (case xh of
+    H1 (Some a) yh \<Rightarrow> (f21 x (map_h (map_option (f20 yh)) id id yh)) # (branches a)
+  | H1 None yh \<Rightarrow> [f21 x yh]
+  | H2 b c yh \<Rightarrow> (f21 c (map_h id (%n. n + b) id yh)) # (branches x)
+  | H3 \<Rightarrow> branches x)"
+
+friend_of_corec f21 where
+  "f21 x xh =
+  Node (node x) (case xh of
+    H1 (Some a) yh \<Rightarrow> (f21 x (map_h (map_option (f20 yh)) (%t. t) (%t. t) yh)) # (branches a)
+  | H1 None yh \<Rightarrow> [f21 x yh]
+  | H2 b c yh \<Rightarrow> (f21 c (map_h (%t. t) (%n. n + b) (%t. t) yh)) # (branches x)
+  | H3 \<Rightarrow> branches x)"
+  sorry
+
+corec f22 :: "('a \<Rightarrow> tree) \<Rightarrow> 'a list \<Rightarrow> tree" where
+  "f22 f x = Node 0 (map f x)"
+
+friend_of_corec f22:: "(nat \<Rightarrow> tree) \<Rightarrow> nat list \<Rightarrow> tree"  where
+  "f22 f x = Node 0 (map f x)"
+    sorry
+
+corec f23 where
+  "f23 xh = Node 0
+    (if is_H1 xh then
+      (f23 (h_tail xh)) # (branches (h_a xh))
+    else if is_H1 xh then
+      (f23 (h_tail xh)) # (h_c xh) # (branches (h_b xh))
+    else
+      [])"
+
+friend_of_corec f23 where
+  "f23 xh = Node 0
+    (if is_H1 xh then
+      (f23 (h_tail xh)) # (branches (h_a xh))
+    else if is_H1 xh then
+      (f23 (h_tail xh)) # (h_c xh) # (branches (h_b xh))
+    else
+      [])"
+  sorry
+
+corec f24 where
+  "f24 xh =
+    (if is_H1 xh then
+      Node 0 ((f24 (h_tail xh)) # (h_a xh 0))
+    else if is_H2 xh then
+      Node (h_b xh) ((f24 (h_tail xh)) # (h_c xh 0))
+    else
+      Node 0 [])"
+
+friend_of_corec f24 :: "(nat \<Rightarrow> tree list, int, int \<Rightarrow> tree list) h \<Rightarrow> tree" where
+  "f24 xh =
+    (if is_H1 xh then
+      Node 0 ((f24 (h_tail xh)) # (h_a xh 0))
+    else if is_H2 xh then
+      Node (h_b xh) ((f24 (h_tail xh)) # (h_c xh 0))
+    else
+      Node 0 [])"
+  sorry
+
+corec f25 where
+  "f25 x = Node (node x) (map f25 ((id branches) x))"
+
+codatatype ('a, 'b) y_type =
+  Y (lab: "'a \<Rightarrow> 'b") (y_tail: "('a, 'b) y_type")
+
+corec f26 :: "(int, tree) y_type \<Rightarrow> tree \<Rightarrow> tree" where
+  "f26 y x = (case map_y_type f12 y of
+  Y f y' \<Rightarrow> Node (node x) ((f (node x)) # (map (f26 y') (branches x))))"
+
+friend_of_corec f26 where
+  "f26 y x = (case map_y_type f12 y of
+  Y f y' \<Rightarrow> Node (node x) ((f (node x)) # (map (f26 y') (branches x))))"
+  sorry
+
+consts int_of_list :: "'a list \<Rightarrow> int"
+
+corec f27 :: "(int, tree) y_type \<Rightarrow> tree \<Rightarrow> tree" where
+  "f27 y x = Node (int_of_list (map (f26 (y_tail y)) (branches x))) [lab y (node x)]"
+
+friend_of_corec f27 :: "(int, tree) y_type \<Rightarrow> tree \<Rightarrow> tree" where
+  "f27 y x = Node (int_of_list (map (f26 (y_tail y)) (branches x))) [lab y (node x)]"
+  sorry
+
+corec f28 :: "(tree option list, (int \<Rightarrow> int) \<Rightarrow> int list \<Rightarrow> tree, tree) h \<Rightarrow> tree" where
+  "f28 xh = (case xh of
+    H3 \<Rightarrow> Node 0 []
+  | H1 l r \<Rightarrow> Node 0 ((f28 r) # map the (filter (%opt. case opt of None \<Rightarrow> False | Some _ \<Rightarrow> True) l))
+  | H2 f t r \<Rightarrow> Node (node t) (map (%t. f id [node t]) (branches t)))"
+
+codatatype llist =
+  LNil | LCons (head: nat) (tail: llist)
+
+inductive llist_in where
+  "llist_in (LCons x xs) x"
+| "llist_in xs y \<Longrightarrow> llist_in (LCons x xs) y"
+
+abbreviation "lset xs \<equiv> {x. llist_in xs x}"
+
+corecursive lfilter where
+  "lfilter P xs = (if \<forall> x \<in> lset xs. \<not> P x then
+    LNil
+    else if P (head xs) then
+      LCons (head xs) (lfilter P (tail xs))
+    else
+      lfilter P (tail xs))"
+proof (relation "measure (\<lambda>(P, xs). LEAST n. P (head ((tail ^^ n) xs)))", rule wf_measure, clarsimp)
+  fix P xs x
+  assume "llist_in xs x" "P x" "\<not> P (head xs)"
+  from this(1,2) obtain a where "P (head ((tail ^^ a) xs))"
+    by (atomize_elim, induct xs x rule: llist_in.induct) (auto simp: funpow_Suc_right
+      simp del: funpow.simps(2) intro: exI[of _ 0] exI[of _ "Suc i" for i])
+  moreover
+  with \<open>\<not> P (head xs)\<close>
+    have "(LEAST n. P (head ((tail ^^ n) xs))) = Suc (LEAST n. P (head ((tail ^^ Suc n) xs)))"
+    by (intro Least_Suc) auto
+  then show "(LEAST n. P (head ((tail ^^ n) (tail xs)))) < (LEAST n. P (head ((tail ^^ n) xs)))"
+    by (simp add: funpow_swap1[of tail])
+qed
+
+codatatype Stream =
+  SCons (head: nat) (tail: Stream)
+
+corec map_Stream where
+  "map_Stream f s = SCons (f (head s)) (map_Stream f (tail s))"
+
+friend_of_corec map_Stream where
+  "map_Stream f s = SCons (f (head s)) (map_Stream f (tail s))"
+  sorry
+
+corec f29 where
+  "f29 f ll = SCons (head ll) (f29 f (map_Stream f (tail ll)))"
+
+friend_of_corec f29 where
+  "f29 f ll = SCons (head ll) (f29 f (map_Stream f (tail ll)))"
+  sorry
+
+corec f30 where
+  "f30 n m = (if n = 0 then SCons m (f30 m m) else f30 (n - 1) (n * m))"
+
+corec f31 :: "llist \<Rightarrow> llist" where
+  "f31 x = (if x = LNil then LCons undefined (f31 undefined) else LCons undefined undefined)"
+
+friend_of_corec f31 where
+  "f31 x = (if x = LNil then LCons undefined (f31 undefined) else LCons undefined undefined)"
+  sorry
+
+corec f32 :: "tree \<Rightarrow> tree" where
+  "f32 t = Node (node t) (map ((\<lambda>t'. f18  t') o f32) (branches t))"
+
+corec f33 :: "tree \<Rightarrow> tree" where
+  "f33 t = f18 (f18 (Node (node t) (map (\<lambda>t'. (f18 o f18) (f18 (f18 (f33 t')))) (branches t))))"
+
+corec f34 :: "tree \<Rightarrow> tree" where
+  "f34 t = f18 (f18 (Node (node t) (map (f18 o f18 o f34) (branches t))))"
+
+corec f35 :: "tree \<Rightarrow> tree" where
+  "f35 t = f18 (f18 (Node (node t) (map (f18 o (f18 o (\<lambda>t'. f18 t')) o f35) (branches t))))"
+
+corec f37 :: "int \<Rightarrow> tree list \<Rightarrow> tree option \<Rightarrow> nat \<Rightarrow> tree"  where
+  "f37 a x1 = undefined a x1"
+
+end
diff -r b287b56a6ce5 -r 7325d8573fb8 src/HOL/Corec_Examples/Tests/Misc_Poly.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Corec_Examples/Tests/Misc_Poly.thy	Tue Mar 22 12:39:37 2016 +0100
@@ -0,0 +1,315 @@
+(*  Title:      HOL/Corec_Examples/Tests/Misc_Poly.thy
+    Author:     Aymeric Bouzy, Ecole polytechnique
+    Author:     Jasmin Blanchette, Inria, LORIA, MPII
+    Copyright   2015, 2016
+
+Miscellaneous polymorphic examples.
+*)
+
+section {* Miscellaneous Polymorphic Examples *}
+
+theory Misc_Poly
+imports "~~/src/HOL/Library/BNF_Corec"
+begin
+
+codatatype ('a, 'b) T0 =
+  C1 (lab: "'a * 'b") (tl11: "('a, 'b) T0") (tl12: "('a, 'b) T0")
+| C2 (lab: "'a * 'b") (tl2: "('a, 'b) T0")
+| C3 (tl3: "('a, 'b) T0 list")
+
+codatatype stream = S (hd: nat) (tl: stream)
+
+corec test0 where
+  "test0 x y = (case (x, y) of
+  (S a1 s1, S a2 s2) \<Rightarrow> S (a1 + a2) (test0 s1 s2))"
+
+friend_of_corec test0 where
+  "test0 x y = (case (x, y) of
+  (S a1 s1, S a2 s2) \<Rightarrow> S (a1 + a2) (test0 s1 s2))"
+  sorry
+
+corec test01 where
+  "test01 x y = C2 (fst (lab x), snd (lab y)) (test01 (tl2 x) (tl2 y))"
+
+friend_of_corec test01 :: "('a, 'b) T0 \<Rightarrow> ('a, 'b) T0 \<Rightarrow> ('a, 'b) T0" where
+  "test01 x y = C2 (fst (lab x), snd (lab y)) (test01 (tl2 x) (tl2 y))"
+  sorry
+
+corec test02 where
+  "test02 x y = C2 (fst (lab x), snd (lab y)) (test01 (test02 x (tl2 y)) (test02 (tl2 x) y))"
+
+friend_of_corec test02 :: "('a, 'b) T0 \<Rightarrow> ('a, 'b) T0 \<Rightarrow> ('a, 'b) T0"  where
+  "test02 x y = C2 (fst (lab x), snd (lab y)) (test01 (test02 x (tl2 y)) (test02 (tl2 x) y))"
+  sorry
+
+corec test03 where
+  "test03 x = C2 (lab x) (C2 (lab x) (test02 x x))"
+
+friend_of_corec test03 where
+  "test03 x = C2 (lab x) (C2 (lab x) (test02 (test03 (tl2 x)) (test03 (tl2 x))))"
+  sorry
+
+corec test04 where
+  "test04 x = (case x of C1 a t1 t2 \<Rightarrow> C1 a (test04 t1) (test04 t2) | C2 a t \<Rightarrow> C2 a (test04 t) | C3 l \<Rightarrow> C3 l)"
+
+friend_of_corec test04 where
+  "test04 x = (case x of C1 a t1 t2 \<Rightarrow> C1 a (test04 t1) (test04 t2) | C2 a t \<Rightarrow> C2 a (test04 t) | C3 l \<Rightarrow> C3 l)"
+  sorry
+
+corec test05 where
+  "test05 x y = (case (x, y) of
+  (C1 a t11 t12, C1 b t21 t22) \<Rightarrow> C1 (fst a, snd b) (test05 t11 t21) (test05 t12 t22)
+| (C1 a t11 _, C2 b t2) \<Rightarrow> C2 (fst a, snd b) (test05 t11 t2)
+| (C2 a t1, C1 b _ t22) \<Rightarrow> C2 (fst a, snd b) (test05 t1 t22)
+| (C2 a t1, C2 b t2) \<Rightarrow> C2 (fst a, snd b) (test05 t1 t2)
+| (_, _) \<Rightarrow> C3 [])"
+
+friend_of_corec test05 :: "('a, 'b) T0 \<Rightarrow> ('a, 'b) T0 \<Rightarrow> ('a, 'b) T0" where
+  "test05 x y = (case (x, y) of
+  (C1 a t11 t12, C1 b t21 t22) \<Rightarrow> C1 (fst a, snd b) (test05 t11 t21) (test05 t12 t22)
+| (C1 a t11 _, C2 b t2) \<Rightarrow> C2 (fst a, snd b) (test05 t11 t2)
+| (C2 a t1, C1 b _ t22) \<Rightarrow> C2 (fst a, snd b) (test05 t1 t22)
+| (C2 a t1, C2 b t2) \<Rightarrow> C2 (fst a, snd b) (test05 t1 t2)
+| (_, _) \<Rightarrow> C3 [])"
+  sorry
+
+corec test06 where
+  "test06 x =
+  (if \<not> is_C1 x then
+    let tail = tl2 x in
+    C1 (lab x) (test06 tail) tail
+  else
+    C2 (lab x) (test06 (tl12 x)))"
+
+friend_of_corec test06 where
+  "test06 x =
+  (if \<not> is_C1 x then
+    let tail = tl2 x in
+    C1 (lab x) (test06 tail) tail
+  else
+    C2 (lab x) (test06 (tl12 x)))"
+    sorry
+
+corec test07 where
+  "test07 xs = C3 (map (\<lambda>x. test07 (tl3 x)) xs)"
+
+friend_of_corec test07 :: "('a, 'b) T0 list \<Rightarrow> ('a, 'b) T0" where
+  "test07 xs = C3 (map (\<lambda>x. test07 (tl3 x)) xs)"
+  sorry
+
+corec test08 where
+  "test08 xs = (case xs of
+    [] \<Rightarrow> C3 []
+  | T # r \<Rightarrow> C1 (lab T) (test08 r) T)"
+
+friend_of_corec test08 where
+  "test08 xs = (case xs of
+    [] \<Rightarrow> C3 []
+  | T # r \<Rightarrow> C1 (lab T) (test08 r) T)"
+  sorry
+
+corec test09 where
+  "test09 xs = (case xs of
+    [] \<Rightarrow> C3 []
+  | (C1 n T1 T2) # r \<Rightarrow> C1 n (test09 (T1 # r)) (test09 (T2 # r))
+  | _ # r \<Rightarrow> C3 [test09 r])"
+
+friend_of_corec test09 where
+  "test09 xs = (case xs of
+    [] \<Rightarrow> C3 []
+  | (C1 n T1 T2) # r \<Rightarrow> C1 n (test09 (T1 # r)) (test09 (T2 # r))
+  | _ # r \<Rightarrow> C3 [test09 r])"
+  sorry
+
+codatatype 'h tree =
+  Node (node: 'h) (branches: "'h tree list")
+
+consts integerize_list :: "'a list \<Rightarrow> int"
+
+corec f10 where
+  "f10 x y = Node
+  (integerize_list (branches x) + integerize_list (branches y))
+  (map (\<lambda>(x, y). f10 x y) (zip (branches x) (branches y)))"
+
+friend_of_corec f10 :: "int tree \<Rightarrow> int tree \<Rightarrow> int tree" where
+  "f10 x y = Node
+  (integerize_list (branches x) + integerize_list (branches y))
+  (map (\<lambda>(x, y). f10 x y) (zip (branches x) (branches y)))"
+  sorry
+
+codatatype llist =
+  Nil | LCons llist
+
+consts friend :: "llist \<Rightarrow> llist"
+
+friend_of_corec friend where
+  "friend x = Nil"
+  sorry
+
+corec f11 where
+  "f11 x = (case friend x of Nil \<Rightarrow> Nil | LCons y \<Rightarrow> LCons (f11 y))"
+
+corec f12 where
+  "f12 t = Node (node t) (map f12 (branches t))"
+
+friend_of_corec f12 where
+  "f12 t = Node (node t) (map f12 (branches t))"
+  sorry
+
+corec f13 where
+  "f13 n ts = Node n (map (%t. f13 (node t) (branches t)) ts)"
+
+friend_of_corec f13 where
+  "f13 n ts = Node n (map (%t. f13 (node t) (branches t)) ts)"
+  sorry
+
+corec f14 where
+  "f14 t_opt = Node undefined
+    (case map_option branches t_opt of
+      None \<Rightarrow> []
+    | Some ts \<Rightarrow> map (f14 o Some) ts)"
+
+friend_of_corec f14 :: "'a tree option \<Rightarrow> 'a tree" where
+  "f14 t_opt = Node undefined
+    (case map_option branches t_opt of
+      None \<Rightarrow> []
+    | Some ts \<Rightarrow> map (f14 o Some) ts)"
+  sorry
+
+corec f15 where
+  "f15 ts_opt = Node undefined
+    (case map_option (map branches) ts_opt of
+      None \<Rightarrow> []
+    | Some tss \<Rightarrow> map (f15 o Some) tss)"
+
+friend_of_corec f15 :: "'a tree list option \<Rightarrow> 'a tree" where
+  "f15 ts_opt = Node undefined
+    (case map_option (map branches) ts_opt of
+      None \<Rightarrow> []
+    | Some tss \<Rightarrow> map (f15 o Some) tss)"
+    sorry
+
+corec f16 where
+  "f16 ts_opt = Node undefined
+    (case ts_opt of
+      None \<Rightarrow> []
+    | Some ts \<Rightarrow> map (f16 o Some o branches) ts)"
+
+friend_of_corec f16 :: "'a tree list option \<Rightarrow> 'a tree" where
+  "f16 ts_opt = Node undefined
+    (case ts_opt of
+      None \<Rightarrow> []
+    | Some ts \<Rightarrow> map (f16 o Some o branches) ts)"
+    sorry
+
+corec f18 :: "'a tree \<Rightarrow> 'a tree" where
+  "f18 t = Node (node t) (map (f18 o f12) (branches t))"
+
+friend_of_corec f18 :: "'z tree \<Rightarrow> 'z tree" where
+  "f18 t = Node (node t) (map (f18 o f12) (branches t))"
+  sorry
+
+corec f19 where
+  "f19 t = Node (node t) (map (%f. f [t]) (map f13 [undefined]))"
+
+friend_of_corec f19 where
+  "f19 t = Node (node t) (map (%f. f [t]) (map f13 [undefined]))"
+  sorry
+
+datatype ('a, 'b, 'c) h = H1 (h_a: 'a) (h_tail: "('a, 'b, 'c) h") | H2 (h_b: 'b) (h_c: 'c) (h_tail: "('a, 'b, 'c) h") | H3
+
+term "map_h (map_option f12) (%n. n) f12"
+
+corec f20 where
+  "f20 x y = Node (node y) (case (map_h (map_option f12) (%n. n) f12 x) of
+    H1 None r \<Rightarrow> (f20 r y) # (branches y)
+  | H1 (Some t) r \<Rightarrow> (f20 r t) # (branches y)
+  | H2 n t r \<Rightarrow> (f20 r (Node n [])) # (branches y)
+  | H3 \<Rightarrow> branches y)"
+
+friend_of_corec f20 :: "('a tree option, 'a, 'a tree) h \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+  "f20 x y = Node (node y) (case (map_h (map_option f12) (%n. n) f12 x) of
+    H1 None r \<Rightarrow> (f20 r y) # (branches y)
+  | H1 (Some t) r \<Rightarrow> (f20 r t) # (branches y)
+  | H2 n t r \<Rightarrow> (f20 r (Node n [])) # (branches y)
+  | H3 \<Rightarrow> branches y)"
+  sorry
+
+corec f21 where
+  "f21 x xh =
+  Node (node x) (case xh of
+    H1 (Some a) yh \<Rightarrow> (f21 x (map_h (map_option (f20 yh)) id id yh)) # (branches a)
+  | H1 None yh \<Rightarrow> [f21 x yh]
+  | H2 b c yh \<Rightarrow> (f21 c (map_h id (%n. n + b) id yh)) # (branches x)
+  | H3 \<Rightarrow> branches x)"
+
+friend_of_corec f21 where
+  "f21 x xh =
+  Node (node x) (case xh of
+    H1 (Some a) yh \<Rightarrow> (f21 x (map_h (map_option (f20 yh)) (%t. t) (%t. t) yh)) # (branches a)
+  | H1 None yh \<Rightarrow> [f21 x yh]
+  | H2 b c yh \<Rightarrow> (f21 c (map_h (%t. t) (%n. n + b) (%t. t) yh)) # (branches x)
+  | H3 \<Rightarrow> branches x)"
+  sorry
+
+corec f22 :: "('a \<Rightarrow> 'h tree) \<Rightarrow> 'a list \<Rightarrow> 'h tree" where
+  "f22 f x = Node undefined (map f x)"
+
+friend_of_corec f22 :: "('h \<Rightarrow> 'h tree) \<Rightarrow> 'h list \<Rightarrow> 'h tree" where
+  "f22 f x = Node undefined (map f x)"
+  sorry
+
+corec f23 where
+  "f23 xh = Node undefined 
+    (if is_H1 xh then
+      (f23 (h_tail xh)) # (branches (h_a xh))
+    else if is_H1 xh then
+      (f23 (h_tail xh)) # (h_c xh) # (branches (h_b xh))
+    else
+      [])"
+
+friend_of_corec f23 where
+  "f23 xh = Node undefined 
+    (if is_H1 xh then
+      (f23 (h_tail xh)) # (branches (h_a xh))
+    else if is_H1 xh then
+      (f23 (h_tail xh)) # (h_c xh) # (branches (h_b xh))
+    else
+      [])"
+  sorry
+
+corec f24 where
+  "f24 xh = 
+    (if is_H1 xh then
+      Node 0 ((f24 (h_tail xh)) # (h_a xh 0))
+    else if is_H2 xh then
+      Node (h_b xh) ((f24 (h_tail xh)) # (h_c xh 0))
+    else
+      Node 0 [])"
+
+friend_of_corec f24 :: "(('b :: {zero}) \<Rightarrow> 'b tree list, 'b, 'b \<Rightarrow> 'b tree list) h \<Rightarrow> 'b tree" where
+  "f24 xh = 
+    (if is_H1 xh then
+      Node 0 ((f24 (h_tail xh)) # (h_a xh 0))
+    else if is_H2 xh then
+      Node (h_b xh) ((f24 (h_tail xh)) # (h_c xh 0))
+    else
+      Node 0 [])"
+  sorry
+
+codatatype ('a, 'b, 'c) s =
+  S (s1: 'a) (s2: 'b) (s3: 'c) (s4: "('a, 'b, 'c) s")
+
+corec (friend) ga :: "('a, 'b, nat) s \<Rightarrow> _" where
+  "ga s = S (s1 s) (s2 s) (s3 s) (s4 s)"
+
+corec (friend) gb :: "('a, nat, 'b) s \<Rightarrow> _" where
+  "gb s = S (s1 s) (s2 s) (s3 s) (s4 s)"
+
+consts foo :: "('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a"
+
+corecursive (friend) gc :: "(nat, 'a, 'b) s \<Rightarrow> _" where
+  "gc s = S (s1 s) (s2 s) (s3 s) (foo (undefined :: 'a \<Rightarrow> 'a) s)"
+  sorry
+
+end
diff -r b287b56a6ce5 -r 7325d8573fb8 src/HOL/Corec_Examples/Tests/Simple_Nesting.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Corec_Examples/Tests/Simple_Nesting.thy	Tue Mar 22 12:39:37 2016 +0100
@@ -0,0 +1,131 @@
+(*  Title:      HOL/Corec_Examples/Tests/Simple_Nesting.thy
+    Author:     Aymeric Bouzy, Ecole polytechnique
+    Author:     Jasmin Blanchette, Inria, LORIA, MPII
+    Copyright   2015, 2016
+
+Tests "corec"'s parsing of map functions.
+*)
+
+section {* Tests "corec"'s Parsing of Map Functions *}
+
+theory Simple_Nesting
+imports "~~/src/HOL/Library/BNF_Corec"
+begin
+
+subsection {* Corecursion via Map Functions *}
+
+consts
+  g :: 'a
+  g' :: 'a
+  g'' :: 'a
+  h :: 'a
+  h' :: 'a
+  q :: 'a
+  q' :: 'a
+
+codatatype tree =
+  Node nat "tree list"
+
+(* a direct, intuitive way to define a function *)
+corec k0 where
+  "k0 x = Node (g x) (map (\<lambda>y. if q y then g' y else k0 (h' y :: 'a)) (h (x :: 'a) :: nat list))"
+
+(* another way -- this one is perhaps less intuitive but more systematic *)
+corec k0' where
+  "k0' x = Node (g x) (map (\<lambda>z. case z of Inl t \<Rightarrow> t | Inr (x' :: 'a) \<Rightarrow> k0' x')
+     (map (\<lambda>y. if q y then Inl (g' y) else Inr (h' y)) (h (x :: 'a) :: nat list)))"
+
+(* more examples, same story *)
+
+corec k1 :: "nat \<Rightarrow> tree" where
+  "k1 x = Node (g x) (map (\<lambda>y. k1 (h' y)) (h x :: nat list))"
+
+corec k1' :: "nat \<Rightarrow> tree" where
+  "k1' x = Node (g x) (map (\<lambda>z. case z of Inl t \<Rightarrow> t | Inr x' \<Rightarrow> k1' x')
+    (map (\<lambda>y. Inr (h' y)) (h x :: nat list)))"
+
+corec k2 :: "nat \<Rightarrow> tree" where
+  "k2 x = Node (g x) (map g' (h x :: nat list))"
+
+corec k2' :: "nat \<Rightarrow> tree" where
+  "k2' x = Node (g x) (map (\<lambda>z. case z of Inl t \<Rightarrow> t | Inr (x' :: nat) \<Rightarrow> k2' x')
+     (map (\<lambda>y. Inl (g' y)) (h x :: nat list)))"
+
+corec k3 :: "nat \<Rightarrow> tree" where
+  "k3 x = Node (g x) (h x)"
+
+corec k3' :: "nat \<Rightarrow> tree" where
+  "k3' x = Node (g x) (map (\<lambda>z. case z of Inl t \<Rightarrow> t | Inr (x' :: nat) \<Rightarrow> k3' x')
+    (map Inl (h x)))"
+
+
+subsection {* Constructors instead of Maps *}
+
+codatatype 'a y = Y 'a "'a y list"
+
+corec hh where
+  "hh a = Y a (map hh [a])"
+
+corec k where
+  "k a = Y a [k a, k undefined, k (a + a), undefined, k a]"
+
+codatatype 'a x = X 'a "'a x option"
+
+corec f where
+  "f a = X a (map_option f (Some a))"
+
+corec gg where
+  "gg a = X a (Some (gg a))"
+
+
+subsection {* Some Friends *}
+
+codatatype u =
+  U (lab: nat) (sub: "u list")
+
+definition u_id :: "u \<Rightarrow> u" where "u_id u = u"
+
+friend_of_corec u_id where
+  "u_id u = U (lab u) (sub u)"
+  by (simp add: u_id_def) transfer_prover
+
+corec u_id_f :: "u \<Rightarrow> u" where
+  "u_id_f u = u_id (U (lab u) (map u_id_f (sub u)))"
+
+corec (friend) u_id_g :: "u \<Rightarrow> u" where
+  "u_id_g u = U (lab u) (map (\<lambda>u'. u_id (u_id_g u')) (sub u))"
+
+corec (friend) u_id_g' :: "u \<Rightarrow> u" where
+  "u_id_g' u = U (lab u) (map (u_id o u_id_g') (sub u))"
+
+corec (friend) u_id_g'' :: "u \<Rightarrow> u" where
+  "u_id_g'' u = U (lab u) (map ((\<lambda>u'. u_id u') o u_id_g'') (sub u))"
+
+corec u_id_h :: "u \<Rightarrow> u" where
+  "u_id_h u = u_id (u_id (U (lab u) (map (\<lambda>u'. (u_id o u_id) (u_id (u_id (u_id_h u')))) (sub u))))"
+
+corec u_id_h' :: "u \<Rightarrow> u" where
+  "u_id_h' u = u_id (u_id (U (lab u) (map (u_id o u_id o u_id_h') (sub u))))"
+
+corec u_id_h'' :: "u \<Rightarrow> u" where
+  "u_id_h'' u = u_id (u_id (U (lab u) (map (u_id o (u_id o (\<lambda>u'. u_id u')) o u_id_h'') (sub u))))"
+
+definition u_K :: "u \<Rightarrow> u \<Rightarrow> u" where "u_K u v = u"
+
+friend_of_corec u_K where
+  "u_K u v = U (lab u) (sub u)"
+  by (simp add: u_K_def) transfer_prover
+
+corec u_K_f :: "u \<Rightarrow> u" where
+  "u_K_f u = u_K (U (lab u) (map u_K_f (sub u))) undefined"
+
+corec (friend) u_K_g :: "u \<Rightarrow> u" where
+  "u_K_g u = U (lab u) (map (\<lambda>u'. u_K (u_K_g u') undefined) (sub u))"
+
+corec (friend) u_K_g' :: "u \<Rightarrow> u" where
+  "u_K_g' u = U (lab u) (map ((\<lambda>u'. u_K u' undefined) o u_K_g') (sub u))"
+
+corec (friend) u_K_g'' :: "u \<Rightarrow> u" where
+  "u_K_g'' u = U (lab u) (map (u_K undefined o u_K_g'') (sub u))"
+
+end
diff -r b287b56a6ce5 -r 7325d8573fb8 src/HOL/Corec_Examples/Tests/Small_Concrete.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Corec_Examples/Tests/Small_Concrete.thy	Tue Mar 22 12:39:37 2016 +0100
@@ -0,0 +1,174 @@
+(*  Title:      HOL/Corec_Examples/Tests/Small_Concrete.thy
+    Author:     Aymeric Bouzy, Ecole polytechnique
+    Author:     Jasmin Blanchette, Inria, LORIA, MPII
+    Copyright   2015, 2016
+
+Small concrete examples.
+*)
+
+section {* Small Concrete Examples *}
+
+theory Small_Concrete
+imports "~~/src/HOL/Library/BNF_Corec"
+begin
+
+subsection {* Streams of Natural Numbers *}
+
+codatatype natstream = S (head: nat) (tail: natstream)
+
+corec (friend) incr_all where
+  "incr_all s = S (head s + 1) (incr_all (tail s))"
+
+corec all_numbers where
+  "all_numbers = S 0 (incr_all all_numbers)"
+
+corec all_numbers_efficient where
+  "all_numbers_efficient n = S n (all_numbers_efficient (n + 1))"
+
+corec remove_multiples where
+  "remove_multiples n s =
+    (if (head s) mod n = 0 then
+      S (head (tail s)) (remove_multiples n (tail (tail s)))
+    else
+      S (head s) (remove_multiples n (tail s)))"
+
+corec prime_numbers where
+  "prime_numbers known_primes =
+    (let next_prime = head (fold (%n s. remove_multiples n s) known_primes (tail (tail all_numbers))) in
+      S next_prime (prime_numbers (next_prime # known_primes)))"
+
+term "prime_numbers []"
+
+corec prime_numbers_more_efficient where
+  "prime_numbers_more_efficient n remaining_numbers =
+    (let remaining_numbers = remove_multiples n remaining_numbers in
+      S (head remaining_numbers) (prime_numbers_more_efficient (head remaining_numbers) remaining_numbers))"
+
+term "prime_numbers_more_efficient 0 (tail (tail all_numbers))"
+
+corec (friend) alternate where
+  "alternate s1 s2 = S (head s1) (S (head s2) (alternate (tail s1) (tail s2)))"
+
+corec (friend) all_sums where
+  "all_sums s1 s2 = S (head s1 + head s2) (alternate (all_sums s1 (tail s2)) (all_sums (tail s1) s2))"
+
+corec app_list where
+  "app_list s l = (case l of
+    [] \<Rightarrow> s
+  | a # r \<Rightarrow> S a (app_list s r))"
+
+friend_of_corec app_list where
+  "app_list s l = (case l of
+    [] \<Rightarrow> (case s of S a b \<Rightarrow> S a b)
+  | a # r \<Rightarrow> S a (app_list s r))"
+  sorry
+
+corec expand_with where
+  "expand_with f s = (let l = f (head s) in S (hd l) (app_list (expand_with f (tail s)) (tl l)))"
+
+friend_of_corec expand_with where
+  "expand_with f s = (let l = f (head s) in S (hd l) (app_list (expand_with f (tail s)) (tl l)))"
+  sorry
+
+corec iterations where
+  "iterations f a = S a (iterations f (f a))"
+
+corec exponential_iterations where
+  "exponential_iterations f a = S (f a) (exponential_iterations (f o f) a)"
+
+corec (friend) alternate_list where
+  "alternate_list l = (let heads = (map head l) in S (hd heads) (app_list (alternate_list (map tail l)) (tl heads)))"
+
+corec switch_one_two0 where
+  "switch_one_two0 f a s = (case s of
+    S b r \<Rightarrow> S b (S a (f r)))"
+
+corec switch_one_two where
+  "switch_one_two s = (case s of
+    S a (S b r) \<Rightarrow> S b (S a (switch_one_two r)))"
+
+corec fibonacci where
+  "fibonacci n m = S m (fibonacci (n + m) n)"
+
+corec sequence2 where
+  "sequence2 f u1 u0 = S u0 (sequence2 f (f u1 u0) u1)"
+
+corec (friend) alternate_with_function where
+  "alternate_with_function f s =
+    (let f_head_s = f (head s) in S (head f_head_s) (alternate (tail f_head_s) (alternate_with_function f (tail s))))"
+
+corec h where
+  "h l s = (case l of
+    [] \<Rightarrow> s
+  | (S a s') # r \<Rightarrow> S a (alternate s (h r s')))"
+
+friend_of_corec h where
+  "h l s = (case l of
+    [] \<Rightarrow> (case s of S a b \<Rightarrow> S a b)
+  | (S a s') # r \<Rightarrow> S a (alternate s (h r s')))"
+  sorry
+
+corec z where
+  "z = S 0 (S 0 z)"
+
+lemma "\<And>x. x = S 0 (S 0 x) \<Longrightarrow> x = z"
+  apply corec_unique
+  apply (rule z.code)
+  done
+
+corec enum where
+  "enum m = S m (enum (m + 1))"
+
+lemma "(\<And>m. f m = S m (f (m + 1))) \<Longrightarrow> f m = enum m"
+  apply corec_unique
+  apply (rule enum.code)
+  done
+
+lemma "(\<forall>m. f m = S m (f (m + 1))) \<Longrightarrow> f m = enum m"
+  apply corec_unique
+  apply (rule enum.code)
+  done
+
+
+subsection {* Lazy Lists of Natural Numbers *}
+
+codatatype llist = LNil | LCons nat llist
+
+corec h1 where
+  "h1 x = (if x = 1 then
+    LNil
+  else
+    let x = if x mod 2 = 0 then x div 2 else 3 * x + 1 in
+    LCons x (h1 x))"
+
+corec h3 where
+  "h3 s = (case s of
+    LNil \<Rightarrow> LNil
+  | LCons x r \<Rightarrow> LCons x (h3 r))"
+
+corec (friend) fold_map where
+  "fold_map f a s = (let v = f a (head s) in S v (fold_map f v (tail s)))"
+
+
+subsection {* Coinductie Natural Numbers *}
+
+codatatype conat = CoZero | CoSuc conat
+
+corec sum where
+  "sum x y = (case x of
+      CoZero \<Rightarrow> y
+    | CoSuc x \<Rightarrow> CoSuc (sum x y))"
+
+friend_of_corec sum where
+  "sum x y = (case x of
+      CoZero \<Rightarrow> (case y of CoZero \<Rightarrow> CoZero | CoSuc y \<Rightarrow> CoSuc y)
+    | CoSuc x \<Rightarrow> CoSuc (sum x y))"
+  sorry
+
+corec (friend) prod where
+  "prod x y = (case (x, y) of
+      (CoZero, _) \<Rightarrow> CoZero
+    | (_, CoZero) \<Rightarrow> CoZero
+    | (CoSuc x, CoSuc y) \<Rightarrow> CoSuc (sum (prod x y) (sum x y)))"
+
+end
diff -r b287b56a6ce5 -r 7325d8573fb8 src/HOL/Corec_Examples/Tests/TLList_Friends.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Corec_Examples/Tests/TLList_Friends.thy	Tue Mar 22 12:39:37 2016 +0100
@@ -0,0 +1,126 @@
+(*  Title:      HOL/Corec_Examples/Tests/TLList_Friends.thy
+    Author:     Aymeric Bouzy, Ecole polytechnique
+    Author:     Jasmin Blanchette, Inria, LORIA, MPII
+    Copyright   2015, 2016
+
+Terminated lists examples
+*)
+
+section {* Small Concrete Examples *}
+
+theory TLList_Friends
+imports "~~/src/HOL/Library/BNF_Corec"
+begin
+
+codatatype ('a, 'b) tllist =
+  TLNil (trm: 'b)
+| TLCons (tlhd: 'a) (tltl: "('a, 'b) tllist")
+
+corec pls :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where
+  "pls s s' = TLCons (tlhd s + tlhd s') (pls (tltl s) (tltl s'))"
+
+friend_of_corec pls where
+  "pls s s' = TLCons (tlhd s + tlhd s') (pls (tltl s) (tltl s'))"
+  sorry
+
+corec prd :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where
+  "prd xs ys = TLCons (tlhd xs * tlhd ys) (pls (prd xs (tltl ys)) (prd (tltl xs) ys))"
+
+friend_of_corec prd where
+  "prd xs ys = TLCons (tlhd xs * tlhd ys) (pls (prd xs (tltl ys)) (prd (tltl xs) ys))"
+  sorry
+
+corec onetwo :: "(nat, 'b) tllist" where
+  "onetwo = TLCons 1 (TLCons 2 onetwo)"
+
+corec Exp :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where
+  "Exp xs = TLCons (2 ^^ tlhd xs) (prd (tltl xs) (Exp xs))"
+
+friend_of_corec Exp where
+  "Exp xs = TLCons (2 ^^ tlhd xs) (prd (tltl xs) (Exp xs))"
+  sorry
+
+corec prd2 :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where
+  "prd2 xs ys = TLCons (tlhd xs * tlhd ys) (pls (prd xs (tltl ys)) (prd2 (tltl xs) ys))"
+
+text {* Outer if: *}
+
+corec takeUntilOdd :: "(int, int) tllist \<Rightarrow> (int, int) tllist" where
+  "takeUntilOdd xs =
+     (if is_TLNil xs then TLNil (trm xs)
+      else if tlhd xs mod 2 = 0 then TLCons (tlhd xs) (takeUntilOdd (tltl xs))
+      else TLNil (tlhd xs))"
+
+friend_of_corec takeUntilOdd where
+  "takeUntilOdd xs =
+     (if is_TLNil xs then TLNil (trm xs)
+      else if tlhd xs mod 2 = 0 then TLCons (tlhd xs) (takeUntilOdd (tltl xs))
+      else TLNil (tlhd xs))"
+      sorry
+
+corec takeUntilEven :: "(int, int) tllist \<Rightarrow> (int, int) tllist" where
+  "takeUntilEven xs =
+     (case xs of
+        TLNil y \<Rightarrow> TLNil y
+      | TLCons y ys \<Rightarrow>
+        if y mod 2 = 1 then TLCons y (takeUntilEven ys)
+        else TLNil y)"
+
+friend_of_corec takeUntilEven where
+  "takeUntilEven xs =
+     (case xs of
+        TLNil y \<Rightarrow> TLNil y
+      | TLCons y ys \<Rightarrow>
+        if y mod 2 = 1 then TLCons y (takeUntilEven ys)
+        else TLNil y)"
+        sorry
+
+text {* If inside the constructor: *}
+
+corec prd3 :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where
+  "prd3 xs ys = TLCons (tlhd xs * tlhd ys)
+     (if undefined then pls (prd xs (tltl ys)) (prd (tltl xs) ys)
+      else prd3 (tltl xs) (tltl ys))"
+
+friend_of_corec prd3 where
+  "prd3 xs ys = TLCons (tlhd xs * tlhd ys)
+     (if undefined then pls (prd xs (tltl ys)) (prd (tltl xs) ys)
+      else prd3 (tltl xs) (tltl ys))"
+ sorry
+
+text {* If inside the inner friendly operation: *}
+
+corec prd4 :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where
+  "prd4 xs ys = TLCons (tlhd xs * tlhd ys)
+     (pls (if undefined then prd xs (tltl ys) else xs) (prd (tltl xs) ys))"
+
+friend_of_corec prd4 :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where
+  "prd4 xs ys = TLCons (tlhd xs * tlhd ys)
+     (pls (if undefined then prd xs (tltl ys) else xs) (prd (tltl xs) ys))"
+  sorry
+
+text {* Lots of if's: *}
+
+corec iffy :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where
+  "iffy xs =
+   (if undefined (0::nat) then
+      TLNil undefined
+    else
+      Exp (if undefined (1::nat) then
+             Exp undefined
+           else
+             TLCons undefined
+               (if undefined (2::nat) then
+                  Exp (if undefined (3::nat) then
+                         Exp (if undefined (4::nat) then
+                                iffy (tltl xs)
+                              else if undefined (5::nat) then
+                                iffy xs
+                              else
+                                xs)
+                       else
+                         xs)
+                else
+                  undefined)))"
+
+end
diff -r b287b56a6ce5 -r 7325d8573fb8 src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Mar 22 12:39:37 2016 +0100
+++ b/src/HOL/ROOT	Tue Mar 22 12:39:37 2016 +0100
@@ -815,6 +815,15 @@
   theories
     LFilter
     Stream_Processor
+    "Tests/Simple_Nesting"
+  theories [quick_and_dirty]
+    "Tests/GPV_Bare_Bones"
+    "Tests/Merge_D"
+    "Tests/Merge_Poly"
+    "Tests/Misc_Mono"
+    "Tests/Misc_Poly"
+    "Tests/Small_Concrete"
+    "Tests/TLList_Friends"
 
 session "HOL-Word" (main) in Word = HOL +
   theories Word