--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- 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