src/HOL/Corec_Examples/Tests/Small_Concrete.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/Small_Concrete.thy	Tue Mar 22 12:39:37 2016 +0100
     1.3 @@ -0,0 +1,174 @@
     1.4 +(*  Title:      HOL/Corec_Examples/Tests/Small_Concrete.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 +Small concrete examples.
    1.10 +*)
    1.11 +
    1.12 +section {* Small Concrete Examples *}
    1.13 +
    1.14 +theory Small_Concrete
    1.15 +imports "~~/src/HOL/Library/BNF_Corec"
    1.16 +begin
    1.17 +
    1.18 +subsection {* Streams of Natural Numbers *}
    1.19 +
    1.20 +codatatype natstream = S (head: nat) (tail: natstream)
    1.21 +
    1.22 +corec (friend) incr_all where
    1.23 +  "incr_all s = S (head s + 1) (incr_all (tail s))"
    1.24 +
    1.25 +corec all_numbers where
    1.26 +  "all_numbers = S 0 (incr_all all_numbers)"
    1.27 +
    1.28 +corec all_numbers_efficient where
    1.29 +  "all_numbers_efficient n = S n (all_numbers_efficient (n + 1))"
    1.30 +
    1.31 +corec remove_multiples where
    1.32 +  "remove_multiples n s =
    1.33 +    (if (head s) mod n = 0 then
    1.34 +      S (head (tail s)) (remove_multiples n (tail (tail s)))
    1.35 +    else
    1.36 +      S (head s) (remove_multiples n (tail s)))"
    1.37 +
    1.38 +corec prime_numbers where
    1.39 +  "prime_numbers known_primes =
    1.40 +    (let next_prime = head (fold (%n s. remove_multiples n s) known_primes (tail (tail all_numbers))) in
    1.41 +      S next_prime (prime_numbers (next_prime # known_primes)))"
    1.42 +
    1.43 +term "prime_numbers []"
    1.44 +
    1.45 +corec prime_numbers_more_efficient where
    1.46 +  "prime_numbers_more_efficient n remaining_numbers =
    1.47 +    (let remaining_numbers = remove_multiples n remaining_numbers in
    1.48 +      S (head remaining_numbers) (prime_numbers_more_efficient (head remaining_numbers) remaining_numbers))"
    1.49 +
    1.50 +term "prime_numbers_more_efficient 0 (tail (tail all_numbers))"
    1.51 +
    1.52 +corec (friend) alternate where
    1.53 +  "alternate s1 s2 = S (head s1) (S (head s2) (alternate (tail s1) (tail s2)))"
    1.54 +
    1.55 +corec (friend) all_sums where
    1.56 +  "all_sums s1 s2 = S (head s1 + head s2) (alternate (all_sums s1 (tail s2)) (all_sums (tail s1) s2))"
    1.57 +
    1.58 +corec app_list where
    1.59 +  "app_list s l = (case l of
    1.60 +    [] \<Rightarrow> s
    1.61 +  | a # r \<Rightarrow> S a (app_list s r))"
    1.62 +
    1.63 +friend_of_corec app_list where
    1.64 +  "app_list s l = (case l of
    1.65 +    [] \<Rightarrow> (case s of S a b \<Rightarrow> S a b)
    1.66 +  | a # r \<Rightarrow> S a (app_list s r))"
    1.67 +  sorry
    1.68 +
    1.69 +corec expand_with where
    1.70 +  "expand_with f s = (let l = f (head s) in S (hd l) (app_list (expand_with f (tail s)) (tl l)))"
    1.71 +
    1.72 +friend_of_corec expand_with where
    1.73 +  "expand_with f s = (let l = f (head s) in S (hd l) (app_list (expand_with f (tail s)) (tl l)))"
    1.74 +  sorry
    1.75 +
    1.76 +corec iterations where
    1.77 +  "iterations f a = S a (iterations f (f a))"
    1.78 +
    1.79 +corec exponential_iterations where
    1.80 +  "exponential_iterations f a = S (f a) (exponential_iterations (f o f) a)"
    1.81 +
    1.82 +corec (friend) alternate_list where
    1.83 +  "alternate_list l = (let heads = (map head l) in S (hd heads) (app_list (alternate_list (map tail l)) (tl heads)))"
    1.84 +
    1.85 +corec switch_one_two0 where
    1.86 +  "switch_one_two0 f a s = (case s of
    1.87 +    S b r \<Rightarrow> S b (S a (f r)))"
    1.88 +
    1.89 +corec switch_one_two where
    1.90 +  "switch_one_two s = (case s of
    1.91 +    S a (S b r) \<Rightarrow> S b (S a (switch_one_two r)))"
    1.92 +
    1.93 +corec fibonacci where
    1.94 +  "fibonacci n m = S m (fibonacci (n + m) n)"
    1.95 +
    1.96 +corec sequence2 where
    1.97 +  "sequence2 f u1 u0 = S u0 (sequence2 f (f u1 u0) u1)"
    1.98 +
    1.99 +corec (friend) alternate_with_function where
   1.100 +  "alternate_with_function f s =
   1.101 +    (let f_head_s = f (head s) in S (head f_head_s) (alternate (tail f_head_s) (alternate_with_function f (tail s))))"
   1.102 +
   1.103 +corec h where
   1.104 +  "h l s = (case l of
   1.105 +    [] \<Rightarrow> s
   1.106 +  | (S a s') # r \<Rightarrow> S a (alternate s (h r s')))"
   1.107 +
   1.108 +friend_of_corec h where
   1.109 +  "h l s = (case l of
   1.110 +    [] \<Rightarrow> (case s of S a b \<Rightarrow> S a b)
   1.111 +  | (S a s') # r \<Rightarrow> S a (alternate s (h r s')))"
   1.112 +  sorry
   1.113 +
   1.114 +corec z where
   1.115 +  "z = S 0 (S 0 z)"
   1.116 +
   1.117 +lemma "\<And>x. x = S 0 (S 0 x) \<Longrightarrow> x = z"
   1.118 +  apply corec_unique
   1.119 +  apply (rule z.code)
   1.120 +  done
   1.121 +
   1.122 +corec enum where
   1.123 +  "enum m = S m (enum (m + 1))"
   1.124 +
   1.125 +lemma "(\<And>m. f m = S m (f (m + 1))) \<Longrightarrow> f m = enum m"
   1.126 +  apply corec_unique
   1.127 +  apply (rule enum.code)
   1.128 +  done
   1.129 +
   1.130 +lemma "(\<forall>m. f m = S m (f (m + 1))) \<Longrightarrow> f m = enum m"
   1.131 +  apply corec_unique
   1.132 +  apply (rule enum.code)
   1.133 +  done
   1.134 +
   1.135 +
   1.136 +subsection {* Lazy Lists of Natural Numbers *}
   1.137 +
   1.138 +codatatype llist = LNil | LCons nat llist
   1.139 +
   1.140 +corec h1 where
   1.141 +  "h1 x = (if x = 1 then
   1.142 +    LNil
   1.143 +  else
   1.144 +    let x = if x mod 2 = 0 then x div 2 else 3 * x + 1 in
   1.145 +    LCons x (h1 x))"
   1.146 +
   1.147 +corec h3 where
   1.148 +  "h3 s = (case s of
   1.149 +    LNil \<Rightarrow> LNil
   1.150 +  | LCons x r \<Rightarrow> LCons x (h3 r))"
   1.151 +
   1.152 +corec (friend) fold_map where
   1.153 +  "fold_map f a s = (let v = f a (head s) in S v (fold_map f v (tail s)))"
   1.154 +
   1.155 +
   1.156 +subsection {* Coinductie Natural Numbers *}
   1.157 +
   1.158 +codatatype conat = CoZero | CoSuc conat
   1.159 +
   1.160 +corec sum where
   1.161 +  "sum x y = (case x of
   1.162 +      CoZero \<Rightarrow> y
   1.163 +    | CoSuc x \<Rightarrow> CoSuc (sum x y))"
   1.164 +
   1.165 +friend_of_corec sum where
   1.166 +  "sum x y = (case x of
   1.167 +      CoZero \<Rightarrow> (case y of CoZero \<Rightarrow> CoZero | CoSuc y \<Rightarrow> CoSuc y)
   1.168 +    | CoSuc x \<Rightarrow> CoSuc (sum x y))"
   1.169 +  sorry
   1.170 +
   1.171 +corec (friend) prod where
   1.172 +  "prod x y = (case (x, y) of
   1.173 +      (CoZero, _) \<Rightarrow> CoZero
   1.174 +    | (_, CoZero) \<Rightarrow> CoZero
   1.175 +    | (CoSuc x, CoSuc y) \<Rightarrow> CoSuc (sum (prod x y) (sum x y)))"
   1.176 +
   1.177 +end