src/HOL/Corec_Examples/Tests/Misc_Mono.thy
changeset 62696 7325d8573fb8
child 62726 5b2a7caa855b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Corec_Examples/Tests/Misc_Mono.thy	Tue Mar 22 12:39:37 2016 +0100
     1.3 @@ -0,0 +1,435 @@
     1.4 +(*  Title:      HOL/Corec_Examples/Tests/Misc_Mono.thy
     1.5 +    Author:     Aymeric Bouzy, Ecole polytechnique
     1.6 +    Author:     Jasmin Blanchette, Inria, LORIA, MPII
     1.7 +    Copyright   2015, 2016
     1.8 +
     1.9 +Miscellaneous monomorphic examples.
    1.10 +*)
    1.11 +
    1.12 +section {* Miscellaneous Monomorphic Examples *}
    1.13 +
    1.14 +theory Misc_Mono
    1.15 +imports "~~/src/HOL/Library/BNF_Corec"
    1.16 +begin
    1.17 +
    1.18 +codatatype T0 =
    1.19 +  C1 (lab: nat) (tl11: T0) (tl12: T0)
    1.20 +| C2 (lab: nat) (tl2: T0)
    1.21 +| C3 (tl3: "T0 list")
    1.22 +
    1.23 +codatatype stream =
    1.24 +  S (hd: nat) (tl: stream)
    1.25 +
    1.26 +corec (friend) ff where
    1.27 +  "ff x = S 0 (ff (ff x))"
    1.28 +
    1.29 +corec test0 where
    1.30 +  "test0 x y = (case (x, y) of
    1.31 +  (S a1 s1, S a2 s2) \<Rightarrow> S (a1 + a2) (test0 s1 s2))"
    1.32 +
    1.33 +friend_of_corec test0 where
    1.34 +  "test0 x y = (case (x, y) of
    1.35 +  (S a1 s1, S a2 s2) \<Rightarrow> S (a1 + a2) (test0 s1 s2))"
    1.36 +   apply (rule test0.code)
    1.37 +  apply transfer_prover
    1.38 +  done
    1.39 +
    1.40 +corec test01 where
    1.41 +  "test01 x y = C2 (lab x + lab y) (test01 (tl2 x) (tl2 y))"
    1.42 +
    1.43 +friend_of_corec test01 where
    1.44 +  "test01 x y = C2 (lab x + lab y) (test01 (tl2 x) (tl2 y))"
    1.45 +   apply (rule test01.code)
    1.46 +  sorry (* not parametric *)
    1.47 +
    1.48 +corec test02 where
    1.49 +  "test02 x y = C2 (lab x * lab y) (test01 (test02 x (tl2 y)) (test02 (tl2 x) y))"
    1.50 +
    1.51 +friend_of_corec test02 where
    1.52 +  "test02 x y = C2 (lab x * lab y) (test01 (test02 x (tl2 y)) (test02 (tl2 x) y))"
    1.53 +   apply (rule test02.code)
    1.54 +  sorry (* not parametric *)
    1.55 +
    1.56 +corec test03 where
    1.57 +  "test03 x = C2 (lab x) (C2 (lab x) (test02 (test03 (tl2 x)) (test03 (tl2 x))))"
    1.58 +
    1.59 +friend_of_corec test03 where
    1.60 +  "test03 x = C2 (lab x) (C2 (lab x) (test02 (test03 (tl2 x)) (test03 (tl2 x))))"
    1.61 +   apply (rule test03.code)
    1.62 +  sorry (* not parametric *)
    1.63 +
    1.64 +corec (friend) test04a where
    1.65 +  "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)"
    1.66 +
    1.67 +corec test04 where
    1.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)"
    1.69 +
    1.70 +friend_of_corec test04 where
    1.71 +  "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)"
    1.72 +   apply (rule test04.code)
    1.73 +  apply transfer_prover
    1.74 +  done
    1.75 +
    1.76 +corec test05 where
    1.77 +  "test05 x y = (case (x, y) of
    1.78 +  (C1 a t11 t12, C1 b t21 t22) \<Rightarrow> C1 (a + b) (test05 t11 t21) (test05 t12 t22)
    1.79 +| (C1 a t11 _, C2 b t2) \<Rightarrow> C2 (a + b) (test05 t11 t2)
    1.80 +| (C2 a t1, C1 b _ t22) \<Rightarrow> C2 (a + b) (test05 t1 t22)
    1.81 +| (C2 a t1, C2 b t2) \<Rightarrow> C2 (a + b) (test05 t1 t2)
    1.82 +| (_, _) \<Rightarrow> C3 [])"
    1.83 +
    1.84 +friend_of_corec test05 where
    1.85 +  "test05 x y = (case (x, y) of
    1.86 +  (C1 a t11 t12, C1 b t21 t22) \<Rightarrow> C1 (a + b) (test05 t11 t21) (test05 t12 t22)
    1.87 +| (C1 a t11 _, C2 b t2) \<Rightarrow> C2 (a + b) (test05 t11 t2)
    1.88 +| (C2 a t1, C1 b _ t22) \<Rightarrow> C2 (a + b) (test05 t1 t22)
    1.89 +| (C2 a t1, C2 b t2) \<Rightarrow> C2 (a + b) (test05 t1 t2)
    1.90 +| (_, _) \<Rightarrow> C3 [])"
    1.91 +   apply (rule test05.code)
    1.92 +  apply transfer_prover
    1.93 +  done
    1.94 +
    1.95 +corec test06 :: "T0 \<Rightarrow> T0" where
    1.96 +  "test06 x =
    1.97 +  (if \<not> is_C1 x then
    1.98 +    let tail = tl2 x in
    1.99 +    C1 (lab x) (test06 tail) tail
   1.100 +  else
   1.101 +    C2 (lab x) (test06 (tl12 x)))"
   1.102 +
   1.103 +friend_of_corec test06 :: "T0 \<Rightarrow> T0" where
   1.104 +  "test06 x =
   1.105 +  (if \<not> is_C1 x then
   1.106 +    let tail = tl2 x in
   1.107 +    C1 (lab x) (test06 tail) tail
   1.108 +  else
   1.109 +    C2 (lab x) (test06 (tl12 x)))"
   1.110 +   apply (rule test06.code)
   1.111 +  sorry (* not parametric *)
   1.112 +
   1.113 +corec test07 where
   1.114 +  "test07 xs = C3 (map (\<lambda>x. test07 (tl3 x)) xs)"
   1.115 +
   1.116 +friend_of_corec test07 where
   1.117 +  "test07 xs = C3 (map (\<lambda>x. test07 (tl3 x)) xs)"
   1.118 +   apply (rule test07.code)
   1.119 +  sorry (* not parametric *)
   1.120 +
   1.121 +corec test08 where
   1.122 +  "test08 xs = (case xs of
   1.123 +    [] \<Rightarrow> C2 0 (test08 [])
   1.124 +  | T # r \<Rightarrow> C1 1 (test08 r) T)"
   1.125 +
   1.126 +friend_of_corec test08 where
   1.127 +  "test08 xs = (case xs of
   1.128 +    [] \<Rightarrow> C2 0 (test08 [])
   1.129 +  | T # r \<Rightarrow> C1 1 (test08 r) T)"
   1.130 +   apply (rule test08.code)
   1.131 +  apply transfer_prover
   1.132 +  done
   1.133 +
   1.134 +corec test09 where
   1.135 +  "test09 xs = test08 [case xs of
   1.136 +    [] \<Rightarrow> C2 0 (test09 [])
   1.137 +  | (C1 n T1 T2) # r \<Rightarrow> C1 n (test09 (T1 # r)) (test09 (T2 # r))
   1.138 +  | _ # r \<Rightarrow> C3 [test09 r]]"
   1.139 +
   1.140 +friend_of_corec test09 where
   1.141 +  "test09 xs = (case xs of
   1.142 +    [] \<Rightarrow> C2 0 (test09 [])
   1.143 +  | (C1 n T1 T2) # r \<Rightarrow> C1 n (test09 (T1 # r)) (test09 (T2 # r))
   1.144 +  | _ # r \<Rightarrow> C3 [test09 r])"
   1.145 +   defer
   1.146 +   apply transfer_prover
   1.147 +  sorry (* not sure the specifications are equal *)
   1.148 +
   1.149 +codatatype tree =
   1.150 +  Node (node: int) (branches: "tree list")
   1.151 +
   1.152 +consts integerize_tree_list :: "'a list \<Rightarrow> int"
   1.153 +
   1.154 +lemma integerize_tree_list_transfer[transfer_rule]:
   1.155 +  "rel_fun (list_all2 R) op = integerize_tree_list integerize_tree_list"
   1.156 +  sorry
   1.157 +
   1.158 +corec (friend) f10a where
   1.159 +  "f10a x y = Node
   1.160 +  (integerize_tree_list (branches x) + integerize_tree_list (branches y))
   1.161 +  (map (\<lambda>(x, y). f10a x y) (zip (branches x) (branches y)))"
   1.162 +
   1.163 +corec f10 where
   1.164 +  "f10 x y = Node
   1.165 +  (integerize_tree_list (branches x) + integerize_tree_list (branches y))
   1.166 +  (map (\<lambda>(x, y). f10 x y) (zip (branches x) (branches y)))"
   1.167 +
   1.168 +friend_of_corec f10 where
   1.169 +  "f10 x y = Node
   1.170 +  (integerize_tree_list (branches x) + integerize_tree_list (branches y))
   1.171 +  (map (\<lambda>(x, y). f10 x y) (zip (branches x) (branches y)))"
   1.172 +     apply (rule f10.code)
   1.173 +    by transfer_prover+
   1.174 +
   1.175 +corec f12 where
   1.176 +  "f12 t = Node (node t) (map f12 (branches t))"
   1.177 +
   1.178 +friend_of_corec f12 where
   1.179 +  "f12 t = Node (node t) (map f12 (branches t))"
   1.180 +  sorry
   1.181 +
   1.182 +corec f13 where
   1.183 +  "f13 n ts = Node n (map (%t. f13 (node t) (branches t)) ts)"
   1.184 +
   1.185 +friend_of_corec f13 where
   1.186 +  "f13 n ts = Node n (map (%t. f13 (node t) (branches t)) ts)"
   1.187 +  sorry
   1.188 +
   1.189 +corec f14 :: "tree option \<Rightarrow> tree" where
   1.190 +  "f14 t_opt = Node 0
   1.191 +    (case map_option branches t_opt of
   1.192 +      None \<Rightarrow> []
   1.193 +    | Some ts \<Rightarrow> map (f14 o Some) ts)"
   1.194 +
   1.195 +friend_of_corec f14 where
   1.196 +  "f14 t_opt = Node 0
   1.197 +    (case map_option branches t_opt of
   1.198 +      None \<Rightarrow> []
   1.199 +    | Some ts \<Rightarrow> map (f14 o Some) ts)"
   1.200 +  sorry
   1.201 +
   1.202 +corec f15 :: "tree list option \<Rightarrow> tree" where
   1.203 +  "f15 ts_opt = Node 0
   1.204 +    (case map_option (map branches) ts_opt of
   1.205 +      None \<Rightarrow> []
   1.206 +    | Some tss \<Rightarrow> map (f15 o Some) tss)"
   1.207 +
   1.208 +friend_of_corec f15 where
   1.209 +  "f15 ts_opt = Node 0
   1.210 +    (case map_option (map branches) ts_opt of
   1.211 +      None \<Rightarrow> []
   1.212 +    | Some tss \<Rightarrow> map (f15 o Some) tss)"
   1.213 +    sorry
   1.214 +
   1.215 +corec f16 :: "tree list option \<Rightarrow> tree" where
   1.216 +  "f16 ts_opt = Node 0
   1.217 +    (case ts_opt of
   1.218 +      None \<Rightarrow> []
   1.219 +    | Some ts \<Rightarrow> map (f16 o Some o branches) ts)"
   1.220 +
   1.221 +friend_of_corec f16 where
   1.222 +  "f16 ts_opt = Node 0
   1.223 +    (case ts_opt of
   1.224 +      None \<Rightarrow> []
   1.225 +    | Some ts \<Rightarrow> map (f16 o Some o branches) ts)"
   1.226 +    sorry
   1.227 +
   1.228 +corec f17 :: "tree list option \<Rightarrow> tree" where
   1.229 +  "f17 ts_opt = Node 0 (case ts_opt of
   1.230 +    None \<Rightarrow> []
   1.231 +  | Some ts \<Rightarrow> [f17 (Some (map (List.hd o branches) ts))])"
   1.232 +
   1.233 +(* not parametric
   1.234 +friend_of_corec f17 where
   1.235 +  "f17 ts_opt = Node 0 (case ts_opt of
   1.236 +    None \<Rightarrow> []
   1.237 +  | Some ts \<Rightarrow> [f17 (Some (map (List.hd o branches) ts))])"
   1.238 +  sorry
   1.239 +*)
   1.240 +
   1.241 +corec f18 :: "tree \<Rightarrow> tree" where
   1.242 +  "f18 t = Node (node t) (map (f18 o f12) (branches t))"
   1.243 +
   1.244 +friend_of_corec f18 :: "tree \<Rightarrow> tree" where
   1.245 +  "f18 t = Node (node t) (map (f18 o f12) (branches t))"
   1.246 +  sorry
   1.247 +
   1.248 +corec f19 :: "tree \<Rightarrow> tree" where
   1.249 +  "f19 t = Node (node t) (map (%f. f [t]) (map f13 [1, 2, 3]))"
   1.250 +
   1.251 +friend_of_corec f19 :: "tree \<Rightarrow> tree" where
   1.252 +  "f19 t = Node (node t) (map (%f. f [t]) (map f13 [1, 2, 3]))"
   1.253 +  sorry
   1.254 +
   1.255 +datatype ('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
   1.256 +
   1.257 +term "map_h (map_option f12) (%n. n) f12"
   1.258 +
   1.259 +corec f20 :: "(tree option, int, tree) h \<Rightarrow> tree \<Rightarrow> tree" where
   1.260 +  "f20 x y = Node (node y) (case (map_h (map_option f12) (%n. n) f12 x) of
   1.261 +    H1 None r \<Rightarrow> (f20 r y) # (branches y)
   1.262 +  | H1 (Some t) r \<Rightarrow> (f20 r t) # (branches y)
   1.263 +  | H2 n t r \<Rightarrow> (f20 r (Node n [])) # (branches y)
   1.264 +  | H3 \<Rightarrow> branches y)"
   1.265 +
   1.266 +friend_of_corec f20 where
   1.267 +  "f20 x y = Node (node y) (case (map_h (map_option f12) (%n. n) f12 x) of
   1.268 +    H1 None r \<Rightarrow> (f20 r y) # (branches y)
   1.269 +  | H1 (Some t) r \<Rightarrow> (f20 r t) # (branches y)
   1.270 +  | H2 n t r \<Rightarrow> (f20 r (Node n [])) # (branches y)
   1.271 +  | H3 \<Rightarrow> branches y)"
   1.272 +  sorry
   1.273 +
   1.274 +corec f21 where
   1.275 +  "f21 x xh =
   1.276 +  Node (node x) (case xh of
   1.277 +    H1 (Some a) yh \<Rightarrow> (f21 x (map_h (map_option (f20 yh)) id id yh)) # (branches a)
   1.278 +  | H1 None yh \<Rightarrow> [f21 x yh]
   1.279 +  | H2 b c yh \<Rightarrow> (f21 c (map_h id (%n. n + b) id yh)) # (branches x)
   1.280 +  | H3 \<Rightarrow> branches x)"
   1.281 +
   1.282 +friend_of_corec f21 where
   1.283 +  "f21 x xh =
   1.284 +  Node (node x) (case xh of
   1.285 +    H1 (Some a) yh \<Rightarrow> (f21 x (map_h (map_option (f20 yh)) (%t. t) (%t. t) yh)) # (branches a)
   1.286 +  | H1 None yh \<Rightarrow> [f21 x yh]
   1.287 +  | H2 b c yh \<Rightarrow> (f21 c (map_h (%t. t) (%n. n + b) (%t. t) yh)) # (branches x)
   1.288 +  | H3 \<Rightarrow> branches x)"
   1.289 +  sorry
   1.290 +
   1.291 +corec f22 :: "('a \<Rightarrow> tree) \<Rightarrow> 'a list \<Rightarrow> tree" where
   1.292 +  "f22 f x = Node 0 (map f x)"
   1.293 +
   1.294 +friend_of_corec f22:: "(nat \<Rightarrow> tree) \<Rightarrow> nat list \<Rightarrow> tree"  where
   1.295 +  "f22 f x = Node 0 (map f x)"
   1.296 +    sorry
   1.297 +
   1.298 +corec f23 where
   1.299 +  "f23 xh = Node 0
   1.300 +    (if is_H1 xh then
   1.301 +      (f23 (h_tail xh)) # (branches (h_a xh))
   1.302 +    else if is_H1 xh then
   1.303 +      (f23 (h_tail xh)) # (h_c xh) # (branches (h_b xh))
   1.304 +    else
   1.305 +      [])"
   1.306 +
   1.307 +friend_of_corec f23 where
   1.308 +  "f23 xh = Node 0
   1.309 +    (if is_H1 xh then
   1.310 +      (f23 (h_tail xh)) # (branches (h_a xh))
   1.311 +    else if is_H1 xh then
   1.312 +      (f23 (h_tail xh)) # (h_c xh) # (branches (h_b xh))
   1.313 +    else
   1.314 +      [])"
   1.315 +  sorry
   1.316 +
   1.317 +corec f24 where
   1.318 +  "f24 xh =
   1.319 +    (if is_H1 xh then
   1.320 +      Node 0 ((f24 (h_tail xh)) # (h_a xh 0))
   1.321 +    else if is_H2 xh then
   1.322 +      Node (h_b xh) ((f24 (h_tail xh)) # (h_c xh 0))
   1.323 +    else
   1.324 +      Node 0 [])"
   1.325 +
   1.326 +friend_of_corec f24 :: "(nat \<Rightarrow> tree list, int, int \<Rightarrow> tree list) h \<Rightarrow> tree" where
   1.327 +  "f24 xh =
   1.328 +    (if is_H1 xh then
   1.329 +      Node 0 ((f24 (h_tail xh)) # (h_a xh 0))
   1.330 +    else if is_H2 xh then
   1.331 +      Node (h_b xh) ((f24 (h_tail xh)) # (h_c xh 0))
   1.332 +    else
   1.333 +      Node 0 [])"
   1.334 +  sorry
   1.335 +
   1.336 +corec f25 where
   1.337 +  "f25 x = Node (node x) (map f25 ((id branches) x))"
   1.338 +
   1.339 +codatatype ('a, 'b) y_type =
   1.340 +  Y (lab: "'a \<Rightarrow> 'b") (y_tail: "('a, 'b) y_type")
   1.341 +
   1.342 +corec f26 :: "(int, tree) y_type \<Rightarrow> tree \<Rightarrow> tree" where
   1.343 +  "f26 y x = (case map_y_type f12 y of
   1.344 +  Y f y' \<Rightarrow> Node (node x) ((f (node x)) # (map (f26 y') (branches x))))"
   1.345 +
   1.346 +friend_of_corec f26 where
   1.347 +  "f26 y x = (case map_y_type f12 y of
   1.348 +  Y f y' \<Rightarrow> Node (node x) ((f (node x)) # (map (f26 y') (branches x))))"
   1.349 +  sorry
   1.350 +
   1.351 +consts int_of_list :: "'a list \<Rightarrow> int"
   1.352 +
   1.353 +corec f27 :: "(int, tree) y_type \<Rightarrow> tree \<Rightarrow> tree" where
   1.354 +  "f27 y x = Node (int_of_list (map (f26 (y_tail y)) (branches x))) [lab y (node x)]"
   1.355 +
   1.356 +friend_of_corec f27 :: "(int, tree) y_type \<Rightarrow> tree \<Rightarrow> tree" where
   1.357 +  "f27 y x = Node (int_of_list (map (f26 (y_tail y)) (branches x))) [lab y (node x)]"
   1.358 +  sorry
   1.359 +
   1.360 +corec f28 :: "(tree option list, (int \<Rightarrow> int) \<Rightarrow> int list \<Rightarrow> tree, tree) h \<Rightarrow> tree" where
   1.361 +  "f28 xh = (case xh of
   1.362 +    H3 \<Rightarrow> Node 0 []
   1.363 +  | H1 l r \<Rightarrow> Node 0 ((f28 r) # map the (filter (%opt. case opt of None \<Rightarrow> False | Some _ \<Rightarrow> True) l))
   1.364 +  | H2 f t r \<Rightarrow> Node (node t) (map (%t. f id [node t]) (branches t)))"
   1.365 +
   1.366 +codatatype llist =
   1.367 +  LNil | LCons (head: nat) (tail: llist)
   1.368 +
   1.369 +inductive llist_in where
   1.370 +  "llist_in (LCons x xs) x"
   1.371 +| "llist_in xs y \<Longrightarrow> llist_in (LCons x xs) y"
   1.372 +
   1.373 +abbreviation "lset xs \<equiv> {x. llist_in xs x}"
   1.374 +
   1.375 +corecursive lfilter where
   1.376 +  "lfilter P xs = (if \<forall> x \<in> lset xs. \<not> P x then
   1.377 +    LNil
   1.378 +    else if P (head xs) then
   1.379 +      LCons (head xs) (lfilter P (tail xs))
   1.380 +    else
   1.381 +      lfilter P (tail xs))"
   1.382 +proof (relation "measure (\<lambda>(P, xs). LEAST n. P (head ((tail ^^ n) xs)))", rule wf_measure, clarsimp)
   1.383 +  fix P xs x
   1.384 +  assume "llist_in xs x" "P x" "\<not> P (head xs)"
   1.385 +  from this(1,2) obtain a where "P (head ((tail ^^ a) xs))"
   1.386 +    by (atomize_elim, induct xs x rule: llist_in.induct) (auto simp: funpow_Suc_right
   1.387 +      simp del: funpow.simps(2) intro: exI[of _ 0] exI[of _ "Suc i" for i])
   1.388 +  moreover
   1.389 +  with \<open>\<not> P (head xs)\<close>
   1.390 +    have "(LEAST n. P (head ((tail ^^ n) xs))) = Suc (LEAST n. P (head ((tail ^^ Suc n) xs)))"
   1.391 +    by (intro Least_Suc) auto
   1.392 +  then show "(LEAST n. P (head ((tail ^^ n) (tail xs)))) < (LEAST n. P (head ((tail ^^ n) xs)))"
   1.393 +    by (simp add: funpow_swap1[of tail])
   1.394 +qed
   1.395 +
   1.396 +codatatype Stream =
   1.397 +  SCons (head: nat) (tail: Stream)
   1.398 +
   1.399 +corec map_Stream where
   1.400 +  "map_Stream f s = SCons (f (head s)) (map_Stream f (tail s))"
   1.401 +
   1.402 +friend_of_corec map_Stream where
   1.403 +  "map_Stream f s = SCons (f (head s)) (map_Stream f (tail s))"
   1.404 +  sorry
   1.405 +
   1.406 +corec f29 where
   1.407 +  "f29 f ll = SCons (head ll) (f29 f (map_Stream f (tail ll)))"
   1.408 +
   1.409 +friend_of_corec f29 where
   1.410 +  "f29 f ll = SCons (head ll) (f29 f (map_Stream f (tail ll)))"
   1.411 +  sorry
   1.412 +
   1.413 +corec f30 where
   1.414 +  "f30 n m = (if n = 0 then SCons m (f30 m m) else f30 (n - 1) (n * m))"
   1.415 +
   1.416 +corec f31 :: "llist \<Rightarrow> llist" where
   1.417 +  "f31 x = (if x = LNil then LCons undefined (f31 undefined) else LCons undefined undefined)"
   1.418 +
   1.419 +friend_of_corec f31 where
   1.420 +  "f31 x = (if x = LNil then LCons undefined (f31 undefined) else LCons undefined undefined)"
   1.421 +  sorry
   1.422 +
   1.423 +corec f32 :: "tree \<Rightarrow> tree" where
   1.424 +  "f32 t = Node (node t) (map ((\<lambda>t'. f18  t') o f32) (branches t))"
   1.425 +
   1.426 +corec f33 :: "tree \<Rightarrow> tree" where
   1.427 +  "f33 t = f18 (f18 (Node (node t) (map (\<lambda>t'. (f18 o f18) (f18 (f18 (f33 t')))) (branches t))))"
   1.428 +
   1.429 +corec f34 :: "tree \<Rightarrow> tree" where
   1.430 +  "f34 t = f18 (f18 (Node (node t) (map (f18 o f18 o f34) (branches t))))"
   1.431 +
   1.432 +corec f35 :: "tree \<Rightarrow> tree" where
   1.433 +  "f35 t = f18 (f18 (Node (node t) (map (f18 o (f18 o (\<lambda>t'. f18 t')) o f35) (branches t))))"
   1.434 +
   1.435 +corec f37 :: "int \<Rightarrow> tree list \<Rightarrow> tree option \<Rightarrow> nat \<Rightarrow> tree"  where
   1.436 +  "f37 a x1 = undefined a x1"
   1.437 +
   1.438 +end