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