62696
|
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 |
|
|
6 |
Tests "corec"'s parsing of map functions.
|
|
7 |
*)
|
|
8 |
|
62726
|
9 |
section \<open>Tests "corec"'s Parsing of Map Functions\<close>
|
62696
|
10 |
|
|
11 |
theory Simple_Nesting
|
|
12 |
imports "~~/src/HOL/Library/BNF_Corec"
|
|
13 |
begin
|
|
14 |
|
62726
|
15 |
subsection \<open>Corecursion via Map Functions\<close>
|
62696
|
16 |
|
|
17 |
consts
|
|
18 |
g :: 'a
|
|
19 |
g' :: 'a
|
|
20 |
g'' :: 'a
|
|
21 |
h :: 'a
|
|
22 |
h' :: 'a
|
|
23 |
q :: 'a
|
|
24 |
q' :: 'a
|
|
25 |
|
|
26 |
codatatype tree =
|
|
27 |
Node nat "tree list"
|
|
28 |
|
|
29 |
(* a direct, intuitive way to define a function *)
|
|
30 |
corec 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 *)
|
|
34 |
corec 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 |
|
|
40 |
corec k1 :: "nat \<Rightarrow> tree" where
|
|
41 |
"k1 x = Node (g x) (map (\<lambda>y. k1 (h' y)) (h x :: nat list))"
|
|
42 |
|
|
43 |
corec 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 |
|
|
47 |
corec k2 :: "nat \<Rightarrow> tree" where
|
|
48 |
"k2 x = Node (g x) (map g' (h x :: nat list))"
|
|
49 |
|
|
50 |
corec 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 |
|
|
54 |
corec k3 :: "nat \<Rightarrow> tree" where
|
|
55 |
"k3 x = Node (g x) (h x)"
|
|
56 |
|
|
57 |
corec 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 |
|
62726
|
62 |
subsection \<open>Constructors instead of Maps\<close>
|
62696
|
63 |
|
|
64 |
codatatype 'a y = Y 'a "'a y list"
|
|
65 |
|
|
66 |
corec hh where
|
|
67 |
"hh a = Y a (map hh [a])"
|
|
68 |
|
|
69 |
corec k where
|
|
70 |
"k a = Y a [k a, k undefined, k (a + a), undefined, k a]"
|
|
71 |
|
|
72 |
codatatype 'a x = X 'a "'a x option"
|
|
73 |
|
|
74 |
corec f where
|
|
75 |
"f a = X a (map_option f (Some a))"
|
|
76 |
|
|
77 |
corec gg where
|
|
78 |
"gg a = X a (Some (gg a))"
|
|
79 |
|
|
80 |
|
62726
|
81 |
subsection \<open>Some Friends\<close>
|
62696
|
82 |
|
|
83 |
codatatype u =
|
|
84 |
U (lab: nat) (sub: "u list")
|
|
85 |
|
|
86 |
definition u_id :: "u \<Rightarrow> u" where "u_id u = u"
|
|
87 |
|
|
88 |
friend_of_corec u_id where
|
|
89 |
"u_id u = U (lab u) (sub u)"
|
|
90 |
by (simp add: u_id_def) transfer_prover
|
|
91 |
|
|
92 |
corec u_id_f :: "u \<Rightarrow> u" where
|
|
93 |
"u_id_f u = u_id (U (lab u) (map u_id_f (sub u)))"
|
|
94 |
|
|
95 |
corec (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 |
|
|
98 |
corec (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 |
|
|
101 |
corec (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 |
|
|
104 |
corec 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 |
|
|
107 |
corec 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 |
|
|
110 |
corec 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 |
|
|
113 |
definition u_K :: "u \<Rightarrow> u \<Rightarrow> u" where "u_K u v = u"
|
|
114 |
|
|
115 |
friend_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 |
|
|
119 |
corec 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 |
|
|
122 |
corec (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 |
|
|
125 |
corec (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 |
|
|
128 |
corec (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 |
|
|
131 |
end
|