1(* Title: HOL/Corec_Examples/Tests/Misc_Poly.thy 2 Author: Aymeric Bouzy, Ecole polytechnique 3 Author: Jasmin Blanchette, Inria, LORIA, MPII 4 Copyright 2015, 2016 5 6Miscellaneous polymorphic examples. 7*) 8 9section \<open>Miscellaneous Polymorphic Examples\<close> 10 11theory Misc_Poly 12imports "HOL-Library.BNF_Corec" 13begin 14 15codatatype ('a, 'b) T0 = 16 C1 (lab: "'a * 'b") (tl11: "('a, 'b) T0") (tl12: "('a, 'b) T0") 17| C2 (lab: "'a * 'b") (tl2: "('a, 'b) T0") 18| C3 (tl3: "('a, 'b) T0 list") 19 20codatatype stream = S (hd: nat) (tl: stream) 21 22corec test0 where 23 "test0 x y = (case (x, y) of 24 (S a1 s1, S a2 s2) \<Rightarrow> S (a1 + a2) (test0 s1 s2))" 25 26friend_of_corec test0 where 27 "test0 x y = (case (x, y) of 28 (S a1 s1, S a2 s2) \<Rightarrow> S (a1 + a2) (test0 s1 s2))" 29 sorry 30 31corec test01 where 32 "test01 x y = C2 (fst (lab x), snd (lab y)) (test01 (tl2 x) (tl2 y))" 33 34friend_of_corec test01 :: "('a, 'b) T0 \<Rightarrow> ('a, 'b) T0 \<Rightarrow> ('a, 'b) T0" where 35 "test01 x y = C2 (fst (lab x), snd (lab y)) (test01 (tl2 x) (tl2 y))" 36 sorry 37 38corec test02 where 39 "test02 x y = C2 (fst (lab x), snd (lab y)) (test01 (test02 x (tl2 y)) (test02 (tl2 x) y))" 40 41friend_of_corec test02 :: "('a, 'b) T0 \<Rightarrow> ('a, 'b) T0 \<Rightarrow> ('a, 'b) T0" where 42 "test02 x y = C2 (fst (lab x), snd (lab y)) (test01 (test02 x (tl2 y)) (test02 (tl2 x) y))" 43 sorry 44 45corec test03 where 46 "test03 x = C2 (lab x) (C2 (lab x) (test02 x x))" 47 48friend_of_corec test03 where 49 "test03 x = C2 (lab x) (C2 (lab x) (test02 (test03 (tl2 x)) (test03 (tl2 x))))" 50 sorry 51 52corec test04 where 53 "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)" 54 55friend_of_corec test04 where 56 "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)" 57 sorry 58 59corec test05 where 60 "test05 x y = (case (x, y) of 61 (C1 a t11 t12, C1 b t21 t22) \<Rightarrow> C1 (fst a, snd b) (test05 t11 t21) (test05 t12 t22) 62| (C1 a t11 _, C2 b t2) \<Rightarrow> C2 (fst a, snd b) (test05 t11 t2) 63| (C2 a t1, C1 b _ t22) \<Rightarrow> C2 (fst a, snd b) (test05 t1 t22) 64| (C2 a t1, C2 b t2) \<Rightarrow> C2 (fst a, snd b) (test05 t1 t2) 65| (_, _) \<Rightarrow> C3 [])" 66 67friend_of_corec test05 :: "('a, 'b) T0 \<Rightarrow> ('a, 'b) T0 \<Rightarrow> ('a, 'b) T0" where 68 "test05 x y = (case (x, y) of 69 (C1 a t11 t12, C1 b t21 t22) \<Rightarrow> C1 (fst a, snd b) (test05 t11 t21) (test05 t12 t22) 70| (C1 a t11 _, C2 b t2) \<Rightarrow> C2 (fst a, snd b) (test05 t11 t2) 71| (C2 a t1, C1 b _ t22) \<Rightarrow> C2 (fst a, snd b) (test05 t1 t22) 72| (C2 a t1, C2 b t2) \<Rightarrow> C2 (fst a, snd b) (test05 t1 t2) 73| (_, _) \<Rightarrow> C3 [])" 74 sorry 75 76corec test06 where 77 "test06 x = 78 (if \<not> is_C1 x then 79 let tail = tl2 x in 80 C1 (lab x) (test06 tail) tail 81 else 82 C2 (lab x) (test06 (tl12 x)))" 83 84friend_of_corec test06 where 85 "test06 x = 86 (if \<not> is_C1 x then 87 let tail = tl2 x in 88 C1 (lab x) (test06 tail) tail 89 else 90 C2 (lab x) (test06 (tl12 x)))" 91 sorry 92 93corec test07 where 94 "test07 xs = C3 (map (\<lambda>x. test07 (tl3 x)) xs)" 95 96friend_of_corec test07 :: "('a, 'b) T0 list \<Rightarrow> ('a, 'b) T0" where 97 "test07 xs = C3 (map (\<lambda>x. test07 (tl3 x)) xs)" 98 sorry 99 100corec test08 where 101 "test08 xs = (case xs of 102 [] \<Rightarrow> C3 [] 103 | T # r \<Rightarrow> C1 (lab T) (test08 r) T)" 104 105friend_of_corec test08 where 106 "test08 xs = (case xs of 107 [] \<Rightarrow> C3 [] 108 | T # r \<Rightarrow> C1 (lab T) (test08 r) T)" 109 sorry 110 111corec test09 where 112 "test09 xs = (case xs of 113 [] \<Rightarrow> C3 [] 114 | (C1 n T1 T2) # r \<Rightarrow> C1 n (test09 (T1 # r)) (test09 (T2 # r)) 115 | _ # r \<Rightarrow> C3 [test09 r])" 116 117friend_of_corec test09 where 118 "test09 xs = (case xs of 119 [] \<Rightarrow> C3 [] 120 | (C1 n T1 T2) # r \<Rightarrow> C1 n (test09 (T1 # r)) (test09 (T2 # r)) 121 | _ # r \<Rightarrow> C3 [test09 r])" 122 sorry 123 124codatatype 'h tree = 125 Node (node: 'h) (branches: "'h tree list") 126 127consts integerize_list :: "'a list \<Rightarrow> int" 128 129corec f10 where 130 "f10 x y = Node 131 (integerize_list (branches x) + integerize_list (branches y)) 132 (map (\<lambda>(x, y). f10 x y) (zip (branches x) (branches y)))" 133 134friend_of_corec f10 :: "int tree \<Rightarrow> int tree \<Rightarrow> int tree" where 135 "f10 x y = Node 136 (integerize_list (branches x) + integerize_list (branches y)) 137 (map (\<lambda>(x, y). f10 x y) (zip (branches x) (branches y)))" 138 sorry 139 140codatatype llist = 141 Nil | LCons llist 142 143consts friend :: "llist \<Rightarrow> llist" 144 145friend_of_corec friend where 146 "friend x = Nil" 147 sorry 148 149corec f11 where 150 "f11 x = (case friend x of Nil \<Rightarrow> Nil | LCons y \<Rightarrow> LCons (f11 y))" 151 152corec f12 where 153 "f12 t = Node (node t) (map f12 (branches t))" 154 155friend_of_corec f12 where 156 "f12 t = Node (node t) (map f12 (branches t))" 157 sorry 158 159corec f13 where 160 "f13 n ts = Node n (map (%t. f13 (node t) (branches t)) ts)" 161 162friend_of_corec f13 where 163 "f13 n ts = Node n (map (%t. f13 (node t) (branches t)) ts)" 164 sorry 165 166corec f14 where 167 "f14 t_opt = Node undefined 168 (case map_option branches t_opt of 169 None \<Rightarrow> [] 170 | Some ts \<Rightarrow> map (f14 o Some) ts)" 171 172friend_of_corec f14 :: "'a tree option \<Rightarrow> 'a tree" where 173 "f14 t_opt = Node undefined 174 (case map_option branches t_opt of 175 None \<Rightarrow> [] 176 | Some ts \<Rightarrow> map (f14 o Some) ts)" 177 sorry 178 179corec f15 where 180 "f15 ts_opt = Node undefined 181 (case map_option (map branches) ts_opt of 182 None \<Rightarrow> [] 183 | Some tss \<Rightarrow> map (f15 o Some) tss)" 184 185friend_of_corec f15 :: "'a tree list option \<Rightarrow> 'a tree" where 186 "f15 ts_opt = Node undefined 187 (case map_option (map branches) ts_opt of 188 None \<Rightarrow> [] 189 | Some tss \<Rightarrow> map (f15 o Some) tss)" 190 sorry 191 192corec f16 where 193 "f16 ts_opt = Node undefined 194 (case ts_opt of 195 None \<Rightarrow> [] 196 | Some ts \<Rightarrow> map (f16 o Some o branches) ts)" 197 198friend_of_corec f16 :: "'a tree list option \<Rightarrow> 'a tree" where 199 "f16 ts_opt = Node undefined 200 (case ts_opt of 201 None \<Rightarrow> [] 202 | Some ts \<Rightarrow> map (f16 o Some o branches) ts)" 203 sorry 204 205corec f18 :: "'a tree \<Rightarrow> 'a tree" where 206 "f18 t = Node (node t) (map (f18 o f12) (branches t))" 207 208friend_of_corec f18 :: "'z tree \<Rightarrow> 'z tree" where 209 "f18 t = Node (node t) (map (f18 o f12) (branches t))" 210 sorry 211 212corec f19 where 213 "f19 t = Node (node t) (map (%f. f [t]) (map f13 [undefined]))" 214 215friend_of_corec f19 where 216 "f19 t = Node (node t) (map (%f. f [t]) (map f13 [undefined]))" 217 sorry 218 219datatype ('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 220 221term "map_h (map_option f12) (%n. n) f12" 222 223corec f20 where 224 "f20 x y = Node (node y) (case (map_h (map_option f12) (%n. n) f12 x) of 225 H1 None r \<Rightarrow> (f20 r y) # (branches y) 226 | H1 (Some t) r \<Rightarrow> (f20 r t) # (branches y) 227 | H2 n t r \<Rightarrow> (f20 r (Node n [])) # (branches y) 228 | H3 \<Rightarrow> branches y)" 229 230friend_of_corec f20 :: "('a tree option, 'a, 'a tree) h \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where 231 "f20 x y = Node (node y) (case (map_h (map_option f12) (%n. n) f12 x) of 232 H1 None r \<Rightarrow> (f20 r y) # (branches y) 233 | H1 (Some t) r \<Rightarrow> (f20 r t) # (branches y) 234 | H2 n t r \<Rightarrow> (f20 r (Node n [])) # (branches y) 235 | H3 \<Rightarrow> branches y)" 236 sorry 237 238corec f21 where 239 "f21 x xh = 240 Node (node x) (case xh of 241 H1 (Some a) yh \<Rightarrow> (f21 x (map_h (map_option (f20 yh)) id id yh)) # (branches a) 242 | H1 None yh \<Rightarrow> [f21 x yh] 243 | H2 b c yh \<Rightarrow> (f21 c (map_h id (%n. n + b) id yh)) # (branches x) 244 | H3 \<Rightarrow> branches x)" 245 246friend_of_corec f21 where 247 "f21 x xh = 248 Node (node x) (case xh of 249 H1 (Some a) yh \<Rightarrow> (f21 x (map_h (map_option (f20 yh)) (%t. t) (%t. t) yh)) # (branches a) 250 | H1 None yh \<Rightarrow> [f21 x yh] 251 | H2 b c yh \<Rightarrow> (f21 c (map_h (%t. t) (%n. n + b) (%t. t) yh)) # (branches x) 252 | H3 \<Rightarrow> branches x)" 253 sorry 254 255corec f22 :: "('a \<Rightarrow> 'h tree) \<Rightarrow> 'a list \<Rightarrow> 'h tree" where 256 "f22 f x = Node undefined (map f x)" 257 258friend_of_corec f22 :: "('h \<Rightarrow> 'h tree) \<Rightarrow> 'h list \<Rightarrow> 'h tree" where 259 "f22 f x = Node undefined (map f x)" 260 sorry 261 262corec f23 where 263 "f23 xh = Node undefined 264 (if is_H1 xh then 265 (f23 (h_tail xh)) # (branches (h_a xh)) 266 else if is_H1 xh then 267 (f23 (h_tail xh)) # (h_c xh) # (branches (h_b xh)) 268 else 269 [])" 270 271friend_of_corec f23 where 272 "f23 xh = Node undefined 273 (if is_H1 xh then 274 (f23 (h_tail xh)) # (branches (h_a xh)) 275 else if is_H1 xh then 276 (f23 (h_tail xh)) # (h_c xh) # (branches (h_b xh)) 277 else 278 [])" 279 sorry 280 281corec f24 where 282 "f24 xh = 283 (if is_H1 xh then 284 Node 0 ((f24 (h_tail xh)) # (h_a xh 0)) 285 else if is_H2 xh then 286 Node (h_b xh) ((f24 (h_tail xh)) # (h_c xh 0)) 287 else 288 Node 0 [])" 289 290friend_of_corec f24 :: "(('b :: {zero}) \<Rightarrow> 'b tree list, 'b, 'b \<Rightarrow> 'b tree list) h \<Rightarrow> 'b tree" where 291 "f24 xh = 292 (if is_H1 xh then 293 Node 0 ((f24 (h_tail xh)) # (h_a xh 0)) 294 else if is_H2 xh then 295 Node (h_b xh) ((f24 (h_tail xh)) # (h_c xh 0)) 296 else 297 Node 0 [])" 298 sorry 299 300codatatype ('a, 'b, 'c) s = 301 S (s1: 'a) (s2: 'b) (s3: 'c) (s4: "('a, 'b, 'c) s") 302 303corec (friend) ga :: "('a, 'b, nat) s \<Rightarrow> _" where 304 "ga s = S (s1 s) (s2 s) (s3 s) (s4 s)" 305 306corec (friend) gb :: "('a, nat, 'b) s \<Rightarrow> _" where 307 "gb s = S (s1 s) (s2 s) (s3 s) (s4 s)" 308 309consts foo :: "('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a" 310 311corecursive (friend) gc :: "(nat, 'a, 'b) s \<Rightarrow> _" where 312 "gc s = S (s1 s) (s2 s) (s3 s) (foo (undefined :: 'a \<Rightarrow> 'a) s)" 313 sorry 314 315end 316