1(*  Title:      HOL/Corec_Examples/Tests/Simple_Nesting.thy
2    Author:     Aymeric Bouzy, Ecole polytechnique
3    Author:     Jasmin Blanchette, Inria, LORIA, MPII
4    Copyright   2015, 2016
5
6Tests "corec"'s parsing of map functions.
7*)
8
9section \<open>Tests "corec"'s Parsing of Map Functions\<close>
10
11theory Simple_Nesting
12imports "HOL-Library.BNF_Corec"
13begin
14
15subsection \<open>Corecursion via Map Functions\<close>
16
17consts
18  g :: 'a
19  g' :: 'a
20  g'' :: 'a
21  h :: 'a
22  h' :: 'a
23  q :: 'a
24  q' :: 'a
25
26codatatype tree =
27  Node nat "tree list"
28
29(* a direct, intuitive way to define a function *)
30corec k0 where
31  "k0 x = Node (g x) (map (\<lambda>y. if q y then g' y else k0 (h' y :: 'a)) (h (x :: 'a) :: nat list))"
32
33(* another way -- this one is perhaps less intuitive but more systematic *)
34corec k0' where
35  "k0' x = Node (g x) (map (\<lambda>z. case z of Inl t \<Rightarrow> t | Inr (x' :: 'a) \<Rightarrow> k0' x')
36     (map (\<lambda>y. if q y then Inl (g' y) else Inr (h' y)) (h (x :: 'a) :: nat list)))"
37
38(* more examples, same story *)
39
40corec k1 :: "nat \<Rightarrow> tree" where
41  "k1 x = Node (g x) (map (\<lambda>y. k1 (h' y)) (h x :: nat list))"
42
43corec k1' :: "nat \<Rightarrow> tree" where
44  "k1' x = Node (g x) (map (\<lambda>z. case z of Inl t \<Rightarrow> t | Inr x' \<Rightarrow> k1' x')
45    (map (\<lambda>y. Inr (h' y)) (h x :: nat list)))"
46
47corec k2 :: "nat \<Rightarrow> tree" where
48  "k2 x = Node (g x) (map g' (h x :: nat list))"
49
50corec k2' :: "nat \<Rightarrow> tree" where
51  "k2' x = Node (g x) (map (\<lambda>z. case z of Inl t \<Rightarrow> t | Inr (x' :: nat) \<Rightarrow> k2' x')
52     (map (\<lambda>y. Inl (g' y)) (h x :: nat list)))"
53
54corec k3 :: "nat \<Rightarrow> tree" where
55  "k3 x = Node (g x) (h x)"
56
57corec k3' :: "nat \<Rightarrow> tree" where
58  "k3' x = Node (g x) (map (\<lambda>z. case z of Inl t \<Rightarrow> t | Inr (x' :: nat) \<Rightarrow> k3' x')
59    (map Inl (h x)))"
60
61
62subsection \<open>Constructors instead of Maps\<close>
63
64codatatype 'a y = Y 'a "'a y list"
65
66corec hh where
67  "hh a = Y a (map hh [a])"
68
69corec k where
70  "k a = Y a [k a, k undefined, k (a + a), undefined, k a]"
71
72codatatype 'a x = X 'a "'a x option"
73
74corec f where
75  "f a = X a (map_option f (Some a))"
76
77corec gg where
78  "gg a = X a (Some (gg a))"
79
80
81subsection \<open>Some Friends\<close>
82
83codatatype u =
84  U (lab: nat) (sub: "u list")
85
86definition u_id :: "u \<Rightarrow> u" where "u_id u = u"
87
88friend_of_corec u_id where
89  "u_id u = U (lab u) (sub u)"
90  by (simp add: u_id_def) transfer_prover
91
92corec u_id_f :: "u \<Rightarrow> u" where
93  "u_id_f u = u_id (U (lab u) (map u_id_f (sub u)))"
94
95corec (friend) u_id_g :: "u \<Rightarrow> u" where
96  "u_id_g u = U (lab u) (map (\<lambda>u'. u_id (u_id_g u')) (sub u))"
97
98corec (friend) u_id_g' :: "u \<Rightarrow> u" where
99  "u_id_g' u = U (lab u) (map (u_id o u_id_g') (sub u))"
100
101corec (friend) u_id_g'' :: "u \<Rightarrow> u" where
102  "u_id_g'' u = U (lab u) (map ((\<lambda>u'. u_id u') o u_id_g'') (sub u))"
103
104corec u_id_h :: "u \<Rightarrow> u" where
105  "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))))"
106
107corec u_id_h' :: "u \<Rightarrow> u" where
108  "u_id_h' u = u_id (u_id (U (lab u) (map (u_id o u_id o u_id_h') (sub u))))"
109
110corec u_id_h'' :: "u \<Rightarrow> u" where
111  "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))))"
112
113definition u_K :: "u \<Rightarrow> u \<Rightarrow> u" where "u_K u v = u"
114
115friend_of_corec u_K where
116  "u_K u v = U (lab u) (sub u)"
117  by (simp add: u_K_def) transfer_prover
118
119corec u_K_f :: "u \<Rightarrow> u" where
120  "u_K_f u = u_K (U (lab u) (map u_K_f (sub u))) undefined"
121
122corec (friend) u_K_g :: "u \<Rightarrow> u" where
123  "u_K_g u = U (lab u) (map (\<lambda>u'. u_K (u_K_g u') undefined) (sub u))"
124
125corec (friend) u_K_g' :: "u \<Rightarrow> u" where
126  "u_K_g' u = U (lab u) (map ((\<lambda>u'. u_K u' undefined) o u_K_g') (sub u))"
127
128corec (friend) u_K_g'' :: "u \<Rightarrow> u" where
129  "u_K_g'' u = U (lab u) (map (u_K undefined o u_K_g'') (sub u))"
130
131end
132