1(* Title: HOL/Corec_Examples/Tests/Misc_Mono.thy 2 Author: Aymeric Bouzy, Ecole polytechnique 3 Author: Jasmin Blanchette, Inria, LORIA, MPII 4 Copyright 2015, 2016 5 6Miscellaneous monomorphic examples. 7*) 8 9section \<open>Miscellaneous Monomorphic Examples\<close> 10 11theory Misc_Mono 12imports "HOL-Library.BNF_Corec" 13begin 14 15codatatype T0 = 16 C1 (lab: nat) (tl11: T0) (tl12: T0) 17| C2 (lab: nat) (tl2: T0) 18| C3 (tl3: "T0 list") 19 20codatatype stream = 21 S (hd: nat) (tl: stream) 22 23corec (friend) ff where 24 "ff x = S 0 (ff (ff x))" 25 26corec 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 30friend_of_corec test0 where 31 "test0 x y = (case (x, y) of 32 (S a1 s1, S a2 s2) \<Rightarrow> S (a1 + a2) (test0 s1 s2))" 33 apply (rule test0.code) 34 apply transfer_prover 35 done 36 37corec test01 where 38 "test01 x y = C2 (lab x + lab y) (test01 (tl2 x) (tl2 y))" 39 40friend_of_corec test01 where 41 "test01 x y = C2 (lab x + lab y) (test01 (tl2 x) (tl2 y))" 42 apply (rule test01.code) 43 sorry (* not parametric *) 44 45corec test02 where 46 "test02 x y = C2 (lab x * lab y) (test01 (test02 x (tl2 y)) (test02 (tl2 x) y))" 47 48friend_of_corec test02 where 49 "test02 x y = C2 (lab x * lab y) (test01 (test02 x (tl2 y)) (test02 (tl2 x) y))" 50 apply (rule test02.code) 51 sorry (* not parametric *) 52 53corec test03 where 54 "test03 x = C2 (lab x) (C2 (lab x) (test02 (test03 (tl2 x)) (test03 (tl2 x))))" 55 56friend_of_corec test03 where 57 "test03 x = C2 (lab x) (C2 (lab x) (test02 (test03 (tl2 x)) (test03 (tl2 x))))" 58 apply (rule test03.code) 59 sorry (* not parametric *) 60 61corec (friend) test04a where 62 "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)" 63 64corec test04 where 65 "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)" 66 67friend_of_corec test04 where 68 "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)" 69 apply (rule test04.code) 70 apply transfer_prover 71 done 72 73corec test05 where 74 "test05 x y = (case (x, y) of 75 (C1 a t11 t12, C1 b t21 t22) \<Rightarrow> C1 (a + b) (test05 t11 t21) (test05 t12 t22) 76| (C1 a t11 _, C2 b t2) \<Rightarrow> C2 (a + b) (test05 t11 t2) 77| (C2 a t1, C1 b _ t22) \<Rightarrow> C2 (a + b) (test05 t1 t22) 78| (C2 a t1, C2 b t2) \<Rightarrow> C2 (a + b) (test05 t1 t2) 79| (_, _) \<Rightarrow> C3 [])" 80 81friend_of_corec test05 where 82 "test05 x y = (case (x, y) of 83 (C1 a t11 t12, C1 b t21 t22) \<Rightarrow> C1 (a + b) (test05 t11 t21) (test05 t12 t22) 84| (C1 a t11 _, C2 b t2) \<Rightarrow> C2 (a + b) (test05 t11 t2) 85| (C2 a t1, C1 b _ t22) \<Rightarrow> C2 (a + b) (test05 t1 t22) 86| (C2 a t1, C2 b t2) \<Rightarrow> C2 (a + b) (test05 t1 t2) 87| (_, _) \<Rightarrow> C3 [])" 88 apply (rule test05.code) 89 apply transfer_prover 90 done 91 92corec test06 :: "T0 \<Rightarrow> T0" where 93 "test06 x = 94 (if \<not> is_C1 x then 95 let tail = tl2 x in 96 C1 (lab x) (test06 tail) tail 97 else 98 C2 (lab x) (test06 (tl12 x)))" 99 100friend_of_corec test06 :: "T0 \<Rightarrow> T0" where 101 "test06 x = 102 (if \<not> is_C1 x then 103 let tail = tl2 x in 104 C1 (lab x) (test06 tail) tail 105 else 106 C2 (lab x) (test06 (tl12 x)))" 107 apply (rule test06.code) 108 sorry (* not parametric *) 109 110corec test07 where 111 "test07 xs = C3 (map (\<lambda>x. test07 (tl3 x)) xs)" 112 113friend_of_corec test07 where 114 "test07 xs = C3 (map (\<lambda>x. test07 (tl3 x)) xs)" 115 apply (rule test07.code) 116 sorry (* not parametric *) 117 118corec test08 where 119 "test08 xs = (case xs of 120 [] \<Rightarrow> C2 0 (test08 []) 121 | T # r \<Rightarrow> C1 1 (test08 r) T)" 122 123friend_of_corec test08 where 124 "test08 xs = (case xs of 125 [] \<Rightarrow> C2 0 (test08 []) 126 | T # r \<Rightarrow> C1 1 (test08 r) T)" 127 apply (rule test08.code) 128 apply transfer_prover 129 done 130 131corec test09 where 132 "test09 xs = test08 [case xs of 133 [] \<Rightarrow> C2 0 (test09 []) 134 | (C1 n T1 T2) # r \<Rightarrow> C1 n (test09 (T1 # r)) (test09 (T2 # r)) 135 | _ # r \<Rightarrow> C3 [test09 r]]" 136 137friend_of_corec test09 where 138 "test09 xs = (case xs of 139 [] \<Rightarrow> C2 0 (test09 []) 140 | (C1 n T1 T2) # r \<Rightarrow> C1 n (test09 (T1 # r)) (test09 (T2 # r)) 141 | _ # r \<Rightarrow> C3 [test09 r])" 142 defer 143 apply transfer_prover 144 sorry (* not sure the specifications are equal *) 145 146codatatype tree = 147 Node (node: int) (branches: "tree list") 148 149consts integerize_tree_list :: "'a list \<Rightarrow> int" 150 151lemma integerize_tree_list_transfer[transfer_rule]: 152 "rel_fun (list_all2 R) (=) integerize_tree_list integerize_tree_list" 153 sorry 154 155corec (friend) f10a where 156 "f10a x y = Node 157 (integerize_tree_list (branches x) + integerize_tree_list (branches y)) 158 (map (\<lambda>(x, y). f10a x y) (zip (branches x) (branches y)))" 159 160corec f10 where 161 "f10 x y = Node 162 (integerize_tree_list (branches x) + integerize_tree_list (branches y)) 163 (map (\<lambda>(x, y). f10 x y) (zip (branches x) (branches y)))" 164 165friend_of_corec f10 where 166 "f10 x y = Node 167 (integerize_tree_list (branches x) + integerize_tree_list (branches y)) 168 (map (\<lambda>(x, y). f10 x y) (zip (branches x) (branches y)))" 169 apply (rule f10.code) 170 by transfer_prover+ 171 172corec f12 where 173 "f12 t = Node (node t) (map f12 (branches t))" 174 175friend_of_corec f12 where 176 "f12 t = Node (node t) (map f12 (branches t))" 177 sorry 178 179corec f13 where 180 "f13 n ts = Node n (map (%t. f13 (node t) (branches t)) ts)" 181 182friend_of_corec f13 where 183 "f13 n ts = Node n (map (%t. f13 (node t) (branches t)) ts)" 184 sorry 185 186corec f14 :: "tree option \<Rightarrow> tree" where 187 "f14 t_opt = Node 0 188 (case map_option branches t_opt of 189 None \<Rightarrow> [] 190 | Some ts \<Rightarrow> map (f14 o Some) ts)" 191 192friend_of_corec f14 where 193 "f14 t_opt = Node 0 194 (case map_option branches t_opt of 195 None \<Rightarrow> [] 196 | Some ts \<Rightarrow> map (f14 o Some) ts)" 197 sorry 198 199corec f15 :: "tree list option \<Rightarrow> tree" where 200 "f15 ts_opt = Node 0 201 (case map_option (map branches) ts_opt of 202 None \<Rightarrow> [] 203 | Some tss \<Rightarrow> map (f15 o Some) tss)" 204 205friend_of_corec f15 where 206 "f15 ts_opt = Node 0 207 (case map_option (map branches) ts_opt of 208 None \<Rightarrow> [] 209 | Some tss \<Rightarrow> map (f15 o Some) tss)" 210 sorry 211 212corec f16 :: "tree list option \<Rightarrow> tree" where 213 "f16 ts_opt = Node 0 214 (case ts_opt of 215 None \<Rightarrow> [] 216 | Some ts \<Rightarrow> map (f16 o Some o branches) ts)" 217 218friend_of_corec f16 where 219 "f16 ts_opt = Node 0 220 (case ts_opt of 221 None \<Rightarrow> [] 222 | Some ts \<Rightarrow> map (f16 o Some o branches) ts)" 223 sorry 224 225corec f17 :: "tree list option \<Rightarrow> tree" where 226 "f17 ts_opt = Node 0 (case ts_opt of 227 None \<Rightarrow> [] 228 | Some ts \<Rightarrow> [f17 (Some (map (List.hd o branches) ts))])" 229 230(* not parametric 231friend_of_corec f17 where 232 "f17 ts_opt = Node 0 (case ts_opt of 233 None \<Rightarrow> [] 234 | Some ts \<Rightarrow> [f17 (Some (map (List.hd o branches) ts))])" 235 sorry 236*) 237 238corec f18 :: "tree \<Rightarrow> tree" where 239 "f18 t = Node (node t) (map (f18 o f12) (branches t))" 240 241friend_of_corec f18 :: "tree \<Rightarrow> tree" where 242 "f18 t = Node (node t) (map (f18 o f12) (branches t))" 243 sorry 244 245corec f19 :: "tree \<Rightarrow> tree" where 246 "f19 t = Node (node t) (map (%f. f [t]) (map f13 [1, 2, 3]))" 247 248friend_of_corec f19 :: "tree \<Rightarrow> tree" where 249 "f19 t = Node (node t) (map (%f. f [t]) (map f13 [1, 2, 3]))" 250 sorry 251 252datatype ('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 253 254term "map_h (map_option f12) (%n. n) f12" 255 256corec f20 :: "(tree option, int, tree) h \<Rightarrow> tree \<Rightarrow> tree" where 257 "f20 x y = Node (node y) (case (map_h (map_option f12) (%n. n) f12 x) of 258 H1 None r \<Rightarrow> (f20 r y) # (branches y) 259 | H1 (Some t) r \<Rightarrow> (f20 r t) # (branches y) 260 | H2 n t r \<Rightarrow> (f20 r (Node n [])) # (branches y) 261 | H3 \<Rightarrow> branches y)" 262 263friend_of_corec f20 where 264 "f20 x y = Node (node y) (case (map_h (map_option f12) (%n. n) f12 x) of 265 H1 None r \<Rightarrow> (f20 r y) # (branches y) 266 | H1 (Some t) r \<Rightarrow> (f20 r t) # (branches y) 267 | H2 n t r \<Rightarrow> (f20 r (Node n [])) # (branches y) 268 | H3 \<Rightarrow> branches y)" 269 sorry 270 271corec f21 where 272 "f21 x xh = 273 Node (node x) (case xh of 274 H1 (Some a) yh \<Rightarrow> (f21 x (map_h (map_option (f20 yh)) id id yh)) # (branches a) 275 | H1 None yh \<Rightarrow> [f21 x yh] 276 | H2 b c yh \<Rightarrow> (f21 c (map_h id (%n. n + b) id yh)) # (branches x) 277 | H3 \<Rightarrow> branches x)" 278 279friend_of_corec f21 where 280 "f21 x xh = 281 Node (node x) (case xh of 282 H1 (Some a) yh \<Rightarrow> (f21 x (map_h (map_option (f20 yh)) (%t. t) (%t. t) yh)) # (branches a) 283 | H1 None yh \<Rightarrow> [f21 x yh] 284 | H2 b c yh \<Rightarrow> (f21 c (map_h (%t. t) (%n. n + b) (%t. t) yh)) # (branches x) 285 | H3 \<Rightarrow> branches x)" 286 sorry 287 288corec f22 :: "('a \<Rightarrow> tree) \<Rightarrow> 'a list \<Rightarrow> tree" where 289 "f22 f x = Node 0 (map f x)" 290 291friend_of_corec f22:: "(nat \<Rightarrow> tree) \<Rightarrow> nat list \<Rightarrow> tree" where 292 "f22 f x = Node 0 (map f x)" 293 sorry 294 295corec f23 where 296 "f23 xh = Node 0 297 (if is_H1 xh then 298 (f23 (h_tail xh)) # (branches (h_a xh)) 299 else if is_H1 xh then 300 (f23 (h_tail xh)) # (h_c xh) # (branches (h_b xh)) 301 else 302 [])" 303 304friend_of_corec f23 where 305 "f23 xh = Node 0 306 (if is_H1 xh then 307 (f23 (h_tail xh)) # (branches (h_a xh)) 308 else if is_H1 xh then 309 (f23 (h_tail xh)) # (h_c xh) # (branches (h_b xh)) 310 else 311 [])" 312 sorry 313 314corec f24 where 315 "f24 xh = 316 (if is_H1 xh then 317 Node 0 ((f24 (h_tail xh)) # (h_a xh 0)) 318 else if is_H2 xh then 319 Node (h_b xh) ((f24 (h_tail xh)) # (h_c xh 0)) 320 else 321 Node 0 [])" 322 323friend_of_corec f24 :: "(nat \<Rightarrow> tree list, int, int \<Rightarrow> tree list) h \<Rightarrow> tree" where 324 "f24 xh = 325 (if is_H1 xh then 326 Node 0 ((f24 (h_tail xh)) # (h_a xh 0)) 327 else if is_H2 xh then 328 Node (h_b xh) ((f24 (h_tail xh)) # (h_c xh 0)) 329 else 330 Node 0 [])" 331 sorry 332 333corec f25 where 334 "f25 x = Node (node x) (map f25 ((id branches) x))" 335 336codatatype ('a, 'b) y_type = 337 Y (lab: "'a \<Rightarrow> 'b") (y_tail: "('a, 'b) y_type") 338 339corec f26 :: "(int, tree) y_type \<Rightarrow> tree \<Rightarrow> tree" where 340 "f26 y x = (case map_y_type f12 y of 341 Y f y' \<Rightarrow> Node (node x) ((f (node x)) # (map (f26 y') (branches x))))" 342 343friend_of_corec f26 where 344 "f26 y x = (case map_y_type f12 y of 345 Y f y' \<Rightarrow> Node (node x) ((f (node x)) # (map (f26 y') (branches x))))" 346 sorry 347 348consts int_of_list :: "'a list \<Rightarrow> int" 349 350corec f27 :: "(int, tree) y_type \<Rightarrow> tree \<Rightarrow> tree" where 351 "f27 y x = Node (int_of_list (map (f26 (y_tail y)) (branches x))) [lab y (node x)]" 352 353friend_of_corec f27 :: "(int, tree) y_type \<Rightarrow> tree \<Rightarrow> tree" where 354 "f27 y x = Node (int_of_list (map (f26 (y_tail y)) (branches x))) [lab y (node x)]" 355 sorry 356 357corec f28 :: "(tree option list, (int \<Rightarrow> int) \<Rightarrow> int list \<Rightarrow> tree, tree) h \<Rightarrow> tree" where 358 "f28 xh = (case xh of 359 H3 \<Rightarrow> Node 0 [] 360 | H1 l r \<Rightarrow> Node 0 ((f28 r) # map the (filter (%opt. case opt of None \<Rightarrow> False | Some _ \<Rightarrow> True) l)) 361 | H2 f t r \<Rightarrow> Node (node t) (map (%t. f id [node t]) (branches t)))" 362 363codatatype llist = 364 LNil | LCons (head: nat) (tail: llist) 365 366inductive llist_in where 367 "llist_in (LCons x xs) x" 368| "llist_in xs y \<Longrightarrow> llist_in (LCons x xs) y" 369 370abbreviation "lset xs \<equiv> {x. llist_in xs x}" 371 372corecursive lfilter where 373 "lfilter P xs = (if \<forall> x \<in> lset xs. \<not> P x then 374 LNil 375 else if P (head xs) then 376 LCons (head xs) (lfilter P (tail xs)) 377 else 378 lfilter P (tail xs))" 379proof (relation "measure (\<lambda>(P, xs). LEAST n. P (head ((tail ^^ n) xs)))", rule wf_measure, clarsimp) 380 fix P xs x 381 assume "llist_in xs x" "P x" "\<not> P (head xs)" 382 from this(1,2) obtain a where "P (head ((tail ^^ a) xs))" 383 by (atomize_elim, induct xs x rule: llist_in.induct) (auto simp: funpow_Suc_right 384 simp del: funpow.simps(2) intro: exI[of _ 0] exI[of _ "Suc i" for i]) 385 with \<open>\<not> P (head xs)\<close> 386 have "(LEAST n. P (head ((tail ^^ n) xs))) = Suc (LEAST n. P (head ((tail ^^ Suc n) xs)))" 387 by (intro Least_Suc) auto 388 then show "(LEAST n. P (head ((tail ^^ n) (tail xs)))) < (LEAST n. P (head ((tail ^^ n) xs)))" 389 by (simp add: funpow_swap1[of tail]) 390qed 391 392codatatype Stream = 393 SCons (head: nat) (tail: Stream) 394 395corec map_Stream where 396 "map_Stream f s = SCons (f (head s)) (map_Stream f (tail s))" 397 398friend_of_corec map_Stream where 399 "map_Stream f s = SCons (f (head s)) (map_Stream f (tail s))" 400 sorry 401 402corec f29 where 403 "f29 f ll = SCons (head ll) (f29 f (map_Stream f (tail ll)))" 404 405friend_of_corec f29 where 406 "f29 f ll = SCons (head ll) (f29 f (map_Stream f (tail ll)))" 407 sorry 408 409corec f30 where 410 "f30 n m = (if n = 0 then SCons m (f30 m m) else f30 (n - 1) (n * m))" 411 412corec f31 :: "llist \<Rightarrow> llist" where 413 "f31 x = (if x = LNil then LCons undefined (f31 undefined) else LCons undefined undefined)" 414 415friend_of_corec f31 where 416 "f31 x = (if x = LNil then LCons undefined (f31 undefined) else LCons undefined undefined)" 417 sorry 418 419corec f32 :: "tree \<Rightarrow> tree" where 420 "f32 t = Node (node t) (map ((\<lambda>t'. f18 t') o f32) (branches t))" 421 422corec f33 :: "tree \<Rightarrow> tree" where 423 "f33 t = f18 (f18 (Node (node t) (map (\<lambda>t'. (f18 o f18) (f18 (f18 (f33 t')))) (branches t))))" 424 425corec f34 :: "tree \<Rightarrow> tree" where 426 "f34 t = f18 (f18 (Node (node t) (map (f18 o f18 o f34) (branches t))))" 427 428corec f35 :: "tree \<Rightarrow> tree" where 429 "f35 t = f18 (f18 (Node (node t) (map (f18 o (f18 o (\<lambda>t'. f18 t')) o f35) (branches t))))" 430 431corec f37 :: "int \<Rightarrow> tree list \<Rightarrow> tree option \<Rightarrow> nat \<Rightarrow> tree" where 432 "f37 a x1 = undefined a x1" 433 434end 435