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.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.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.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.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
```