src/HOL/Corec_Examples/Tests/Simple_Nesting.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/Simple_Nesting.thy	Tue Mar 22 12:39:37 2016 +0100
1.3 @@ -0,0 +1,131 @@
1.4 +(*  Title:      HOL/Corec_Examples/Tests/Simple_Nesting.thy
1.5 +    Author:     Aymeric Bouzy, Ecole polytechnique
1.6 +    Author:     Jasmin Blanchette, Inria, LORIA, MPII
1.8 +
1.9 +Tests "corec"'s parsing of map functions.
1.10 +*)
1.11 +
1.12 +section {* Tests "corec"'s Parsing of Map Functions *}
1.13 +
1.14 +theory Simple_Nesting
1.15 +imports "~~/src/HOL/Library/BNF_Corec"
1.16 +begin
1.17 +
1.18 +subsection {* Corecursion via Map Functions *}
1.19 +
1.20 +consts
1.21 +  g :: 'a
1.22 +  g' :: 'a
1.23 +  g'' :: 'a
1.24 +  h :: 'a
1.25 +  h' :: 'a
1.26 +  q :: 'a
1.27 +  q' :: 'a
1.28 +
1.29 +codatatype tree =
1.30 +  Node nat "tree list"
1.31 +
1.32 +(* a direct, intuitive way to define a function *)
1.33 +corec k0 where
1.34 +  "k0 x = Node (g x) (map (\<lambda>y. if q y then g' y else k0 (h' y :: 'a)) (h (x :: 'a) :: nat list))"
1.35 +
1.36 +(* another way -- this one is perhaps less intuitive but more systematic *)
1.37 +corec k0' where
1.38 +  "k0' x = Node (g x) (map (\<lambda>z. case z of Inl t \<Rightarrow> t | Inr (x' :: 'a) \<Rightarrow> k0' x')
1.39 +     (map (\<lambda>y. if q y then Inl (g' y) else Inr (h' y)) (h (x :: 'a) :: nat list)))"
1.40 +
1.41 +(* more examples, same story *)
1.42 +
1.43 +corec k1 :: "nat \<Rightarrow> tree" where
1.44 +  "k1 x = Node (g x) (map (\<lambda>y. k1 (h' y)) (h x :: nat list))"
1.45 +
1.46 +corec k1' :: "nat \<Rightarrow> tree" where
1.47 +  "k1' x = Node (g x) (map (\<lambda>z. case z of Inl t \<Rightarrow> t | Inr x' \<Rightarrow> k1' x')
1.48 +    (map (\<lambda>y. Inr (h' y)) (h x :: nat list)))"
1.49 +
1.50 +corec k2 :: "nat \<Rightarrow> tree" where
1.51 +  "k2 x = Node (g x) (map g' (h x :: nat list))"
1.52 +
1.53 +corec k2' :: "nat \<Rightarrow> tree" where
1.54 +  "k2' x = Node (g x) (map (\<lambda>z. case z of Inl t \<Rightarrow> t | Inr (x' :: nat) \<Rightarrow> k2' x')
1.55 +     (map (\<lambda>y. Inl (g' y)) (h x :: nat list)))"
1.56 +
1.57 +corec k3 :: "nat \<Rightarrow> tree" where
1.58 +  "k3 x = Node (g x) (h x)"
1.59 +
1.60 +corec k3' :: "nat \<Rightarrow> tree" where
1.61 +  "k3' x = Node (g x) (map (\<lambda>z. case z of Inl t \<Rightarrow> t | Inr (x' :: nat) \<Rightarrow> k3' x')
1.62 +    (map Inl (h x)))"
1.63 +
1.64 +
1.65 +subsection {* Constructors instead of Maps *}
1.66 +
1.67 +codatatype 'a y = Y 'a "'a y list"
1.68 +
1.69 +corec hh where
1.70 +  "hh a = Y a (map hh [a])"
1.71 +
1.72 +corec k where
1.73 +  "k a = Y a [k a, k undefined, k (a + a), undefined, k a]"
1.74 +
1.75 +codatatype 'a x = X 'a "'a x option"
1.76 +
1.77 +corec f where
1.78 +  "f a = X a (map_option f (Some a))"
1.79 +
1.80 +corec gg where
1.81 +  "gg a = X a (Some (gg a))"
1.82 +
1.83 +
1.84 +subsection {* Some Friends *}
1.85 +
1.86 +codatatype u =
1.87 +  U (lab: nat) (sub: "u list")
1.88 +
1.89 +definition u_id :: "u \<Rightarrow> u" where "u_id u = u"
1.90 +
1.91 +friend_of_corec u_id where
1.92 +  "u_id u = U (lab u) (sub u)"
1.93 +  by (simp add: u_id_def) transfer_prover
1.94 +
1.95 +corec u_id_f :: "u \<Rightarrow> u" where
1.96 +  "u_id_f u = u_id (U (lab u) (map u_id_f (sub u)))"
1.97 +
1.98 +corec (friend) u_id_g :: "u \<Rightarrow> u" where
1.99 +  "u_id_g u = U (lab u) (map (\<lambda>u'. u_id (u_id_g u')) (sub u))"
1.100 +
1.101 +corec (friend) u_id_g' :: "u \<Rightarrow> u" where
1.102 +  "u_id_g' u = U (lab u) (map (u_id o u_id_g') (sub u))"
1.103 +
1.104 +corec (friend) u_id_g'' :: "u \<Rightarrow> u" where
1.105 +  "u_id_g'' u = U (lab u) (map ((\<lambda>u'. u_id u') o u_id_g'') (sub u))"
1.106 +
1.107 +corec u_id_h :: "u \<Rightarrow> u" where
1.108 +  "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))))"
1.109 +
1.110 +corec u_id_h' :: "u \<Rightarrow> u" where
1.111 +  "u_id_h' u = u_id (u_id (U (lab u) (map (u_id o u_id o u_id_h') (sub u))))"
1.112 +
1.113 +corec u_id_h'' :: "u \<Rightarrow> u" where
1.114 +  "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))))"
1.115 +
1.116 +definition u_K :: "u \<Rightarrow> u \<Rightarrow> u" where "u_K u v = u"
1.117 +
1.118 +friend_of_corec u_K where
1.119 +  "u_K u v = U (lab u) (sub u)"
1.120 +  by (simp add: u_K_def) transfer_prover
1.121 +
1.122 +corec u_K_f :: "u \<Rightarrow> u" where
1.123 +  "u_K_f u = u_K (U (lab u) (map u_K_f (sub u))) undefined"
1.124 +
1.125 +corec (friend) u_K_g :: "u \<Rightarrow> u" where
1.126 +  "u_K_g u = U (lab u) (map (\<lambda>u'. u_K (u_K_g u') undefined) (sub u))"
1.127 +
1.128 +corec (friend) u_K_g' :: "u \<Rightarrow> u" where
1.129 +  "u_K_g' u = U (lab u) (map ((\<lambda>u'. u_K u' undefined) o u_K_g') (sub u))"
1.130 +
1.131 +corec (friend) u_K_g'' :: "u \<Rightarrow> u" where
1.132 +  "u_K_g'' u = U (lab u) (map (u_K undefined o u_K_g'') (sub u))"
1.133 +
1.134 +end
```