author | wenzelm |
Fri, 18 Aug 2017 20:47:47 +0200 | |
changeset 66453 | cc19f7ca2ed6 |
parent 62726 | 5b2a7caa855b |
permissions | -rw-r--r-- |
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 |
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
62726
diff
changeset
|
12 |
imports "HOL-Library.BNF_Corec" |
62696 | 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 |