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.7 +    Copyright   2015, 2016
     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