src/HOL/Corec_Examples/Tests/Merge_Poly.thy
changeset 62696 7325d8573fb8
child 62698 9d706e37ddab
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Corec_Examples/Tests/Merge_Poly.thy	Tue Mar 22 12:39:37 2016 +0100
     1.3 @@ -0,0 +1,133 @@
     1.4 +(*  Title:      HOL/Corec_Examples/Tests/Merge_Poly.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 polymorphic merges.
    1.10 +*)
    1.11 +
    1.12 +section {* Tests Polymorphic Merges *}
    1.13 +
    1.14 +theory Merge_Poly
    1.15 +imports "~~/src/HOL/Library/BNF_Corec"
    1.16 +begin
    1.17 +
    1.18 +subsection {* A Monomorphic Example *}
    1.19 +
    1.20 +codatatype r = R (rhd: nat) (rtl: r)
    1.21 +
    1.22 +corec id_r :: "r \<Rightarrow> r" where
    1.23 +  "id_r r = R (rhd r) (id_r (rtl r))"
    1.24 +
    1.25 +corec id_r' :: "r \<Rightarrow> r" where
    1.26 +  "id_r' r = R (rhd r) (id_r' (rtl r))"
    1.27 +
    1.28 +corec id_r'' :: "r \<Rightarrow> r" where
    1.29 +  "id_r'' r = R (rhd r) (id_r'' (rtl r))"
    1.30 +
    1.31 +consts
    1.32 +  f1 :: "r \<Rightarrow> r"
    1.33 +  f2 :: "r \<Rightarrow> r"
    1.34 +  f3 :: "r \<Rightarrow> r"
    1.35 +
    1.36 +friend_of_corec f1 :: "r \<Rightarrow> r" where
    1.37 +  "f1 r = R (rhd r) (f1 (R (rhd r) (rtl r)))"
    1.38 +  sorry
    1.39 +
    1.40 +friend_of_corec f2 :: "r \<Rightarrow> r" where
    1.41 +  "f2 r = R (rhd r) (f1 (f2 (rtl r)))"
    1.42 +  sorry
    1.43 +
    1.44 +friend_of_corec f3 :: "r \<Rightarrow> r" where
    1.45 +  "f3 r = R (rhd r) (f3 (rtl r))"
    1.46 +  sorry
    1.47 +
    1.48 +corec id_rx :: "r \<Rightarrow> r" where
    1.49 +  "id_rx r = f1 (f2 (f3 (R (rhd r) (id_rx (rtl r)))))"
    1.50 +
    1.51 +
    1.52 +subsection {* The Polymorphic Version *}
    1.53 +
    1.54 +codatatype 'a s = S (shd: 'a) (stl: "'a s")
    1.55 +
    1.56 +corec id_s :: "'a s \<Rightarrow> 'a s" where
    1.57 +  "id_s s = S (shd s) (id_s (stl s))"
    1.58 +
    1.59 +corec id_s' :: "'b s \<Rightarrow> 'b s" where
    1.60 +  "id_s' s = S (shd s) (id_s' (stl s))"
    1.61 +
    1.62 +corec id_s'' :: "'w s \<Rightarrow> 'w s" where
    1.63 +  "id_s'' s = S (shd s) (id_s'' (stl s))"
    1.64 +
    1.65 +(* Registers polymorphic and nonpolymorphic friends in an alternating fashion. *)
    1.66 +
    1.67 +consts
    1.68 +  g1 :: "'a \<Rightarrow> 'a s \<Rightarrow> 'a s"
    1.69 +  g2 :: "nat \<Rightarrow> nat s \<Rightarrow> nat s"
    1.70 +  g3 :: "'a \<Rightarrow> 'a s \<Rightarrow> 'a s"
    1.71 +  g4 :: "'a \<Rightarrow> 'a s \<Rightarrow> 'a s"
    1.72 +  g5 :: "nat \<Rightarrow> nat s \<Rightarrow> nat s"
    1.73 +
    1.74 +friend_of_corec g3 :: "'b \<Rightarrow> 'b s \<Rightarrow> 'b s" where
    1.75 +  "g3 x s = S (shd s) (g3 x (stl s))"
    1.76 +  sorry
    1.77 +
    1.78 +friend_of_corec g1 :: "'w \<Rightarrow> 'w s \<Rightarrow> 'w s" where
    1.79 +  "g1 x s = S (shd s) (g1 x (stl s))"
    1.80 +  sorry
    1.81 +
    1.82 +friend_of_corec g2 :: "nat \<Rightarrow> nat s \<Rightarrow> nat s" where
    1.83 +  "g2 x s = S (shd s) (g1 x (stl s))"
    1.84 +  sorry
    1.85 +
    1.86 +friend_of_corec g4 :: "'a \<Rightarrow> 'a s \<Rightarrow> 'a s" where
    1.87 +  "g4 x s = S (shd s) (g1 x (g4 x (stl s)))"
    1.88 +  sorry
    1.89 +
    1.90 +friend_of_corec g5 :: "nat \<Rightarrow> nat s \<Rightarrow> nat s" where
    1.91 +  "g5 x s = S (shd s) (g2 x (g5 x (stl s)))"
    1.92 +  sorry
    1.93 +
    1.94 +corec id_nat_s :: "nat s \<Rightarrow> nat s" where
    1.95 +  "id_nat_s s = g1 undefined (g2 undefined (g3 undefined (S (shd s) (id_nat_s (stl s)))))"
    1.96 +
    1.97 +codatatype ('a, 'b) ABstream = ACons 'a (ABtl: "('a, 'b) ABstream") | BCons 'b (ABtl: "('a, 'b) ABstream")
    1.98 +
    1.99 +consts
   1.100 +  h1 :: "('a, 'b) ABstream \<Rightarrow> ('a, 'b) ABstream"
   1.101 +  h2 :: "(nat, 'b) ABstream \<Rightarrow> (nat, 'b) ABstream"
   1.102 +  h3 :: "('a, nat) ABstream \<Rightarrow> ('a, nat) ABstream"
   1.103 +  h4 :: "('a :: zero, 'a) ABstream \<Rightarrow> ('a :: zero, 'a) ABstream"
   1.104 +
   1.105 +friend_of_corec h1 where
   1.106 +  "h1 x = ACons undefined undefined" sorry
   1.107 +
   1.108 +friend_of_corec h2 where 
   1.109 +  "h2 x = (case x of 
   1.110 +    ACons a t \<Rightarrow> ACons a (h1 (h2 t)) 
   1.111 +  | BCons b t \<Rightarrow> BCons b (h1 (h2 t)))"
   1.112 +  sorry
   1.113 +
   1.114 +friend_of_corec h3 where
   1.115 +  "h3 x = (case x of 
   1.116 +    ACons a t \<Rightarrow> ACons a (h1 (h3 t)) 
   1.117 +  | BCons b t \<Rightarrow> BCons b (h1 (h3 t)))"
   1.118 +  sorry
   1.119 +
   1.120 +friend_of_corec h4 where
   1.121 +  "h4 x = (case x of 
   1.122 +    ACons a t \<Rightarrow> ACons a (h1 (h4 t)) 
   1.123 +  | BCons b t \<Rightarrow> BCons b (h1 (h4 t)))"
   1.124 +  sorry
   1.125 +
   1.126 +corec (friend) h5 where
   1.127 +  "h5 x = (case x of
   1.128 +    ACons a t \<Rightarrow> ACons a (h1 (h2 (h3 (h4 (h5 t)))))
   1.129 +  | BCons b t \<Rightarrow> BCons b (h1 (h2 (h3 (h4 (h5 t))))))"
   1.130 +
   1.131 +corec (friend) h6 :: "(nat, nat) ABstream \<Rightarrow> (nat, nat) ABstream" where
   1.132 +  "h6 x = (case x of
   1.133 +    ACons a t \<Rightarrow> ACons a (h6 (h1 (h2 (h3 (h4 (h5 (h6 t)))))))
   1.134 +  | BCons b t \<Rightarrow> BCons b (h1 (h2 (h3 (h4 (h5 (h6 t)))))))"
   1.135 +
   1.136 +end