1(* Title: HOL/Corec_Examples/Tests/Small_Concrete.thy 2 Author: Aymeric Bouzy, Ecole polytechnique 3 Author: Jasmin Blanchette, Inria, LORIA, MPII 4 Copyright 2015, 2016 5 6Small concrete examples. 7*) 8 9section \<open>Small Concrete Examples\<close> 10 11theory Small_Concrete 12imports "HOL-Library.BNF_Corec" 13begin 14 15subsection \<open>Streams of Natural Numbers\<close> 16 17codatatype natstream = S (head: nat) (tail: natstream) 18 19corec (friend) incr_all where 20 "incr_all s = S (head s + 1) (incr_all (tail s))" 21 22corec all_numbers where 23 "all_numbers = S 0 (incr_all all_numbers)" 24 25corec all_numbers_efficient where 26 "all_numbers_efficient n = S n (all_numbers_efficient (n + 1))" 27 28corec remove_multiples where 29 "remove_multiples n s = 30 (if (head s) mod n = 0 then 31 S (head (tail s)) (remove_multiples n (tail (tail s))) 32 else 33 S (head s) (remove_multiples n (tail s)))" 34 35corec prime_numbers where 36 "prime_numbers known_primes = 37 (let next_prime = head (fold (%n s. remove_multiples n s) known_primes (tail (tail all_numbers))) in 38 S next_prime (prime_numbers (next_prime # known_primes)))" 39 40term "prime_numbers []" 41 42corec prime_numbers_more_efficient where 43 "prime_numbers_more_efficient n remaining_numbers = 44 (let remaining_numbers = remove_multiples n remaining_numbers in 45 S (head remaining_numbers) (prime_numbers_more_efficient (head remaining_numbers) remaining_numbers))" 46 47term "prime_numbers_more_efficient 0 (tail (tail all_numbers))" 48 49corec (friend) alternate where 50 "alternate s1 s2 = S (head s1) (S (head s2) (alternate (tail s1) (tail s2)))" 51 52corec (friend) all_sums where 53 "all_sums s1 s2 = S (head s1 + head s2) (alternate (all_sums s1 (tail s2)) (all_sums (tail s1) s2))" 54 55corec app_list where 56 "app_list s l = (case l of 57 [] \<Rightarrow> s 58 | a # r \<Rightarrow> S a (app_list s r))" 59 60friend_of_corec app_list where 61 "app_list s l = (case l of 62 [] \<Rightarrow> (case s of S a b \<Rightarrow> S a b) 63 | a # r \<Rightarrow> S a (app_list s r))" 64 sorry 65 66corec expand_with where 67 "expand_with f s = (let l = f (head s) in S (hd l) (app_list (expand_with f (tail s)) (tl l)))" 68 69friend_of_corec expand_with where 70 "expand_with f s = (let l = f (head s) in S (hd l) (app_list (expand_with f (tail s)) (tl l)))" 71 sorry 72 73corec iterations where 74 "iterations f a = S a (iterations f (f a))" 75 76corec exponential_iterations where 77 "exponential_iterations f a = S (f a) (exponential_iterations (f o f) a)" 78 79corec (friend) alternate_list where 80 "alternate_list l = (let heads = (map head l) in S (hd heads) (app_list (alternate_list (map tail l)) (tl heads)))" 81 82corec switch_one_two0 where 83 "switch_one_two0 f a s = (case s of 84 S b r \<Rightarrow> S b (S a (f r)))" 85 86corec switch_one_two where 87 "switch_one_two s = (case s of 88 S a (S b r) \<Rightarrow> S b (S a (switch_one_two r)))" 89 90corec fibonacci where 91 "fibonacci n m = S m (fibonacci (n + m) n)" 92 93corec sequence2 where 94 "sequence2 f u1 u0 = S u0 (sequence2 f (f u1 u0) u1)" 95 96corec (friend) alternate_with_function where 97 "alternate_with_function f s = 98 (let f_head_s = f (head s) in S (head f_head_s) (alternate (tail f_head_s) (alternate_with_function f (tail s))))" 99 100corec h where 101 "h l s = (case l of 102 [] \<Rightarrow> s 103 | (S a s') # r \<Rightarrow> S a (alternate s (h r s')))" 104 105friend_of_corec h where 106 "h l s = (case l of 107 [] \<Rightarrow> (case s of S a b \<Rightarrow> S a b) 108 | (S a s') # r \<Rightarrow> S a (alternate s (h r s')))" 109 sorry 110 111corec z where 112 "z = S 0 (S 0 z)" 113 114lemma "\<And>x. x = S 0 (S 0 x) \<Longrightarrow> x = z" 115 apply corec_unique 116 apply (rule z.code) 117 done 118 119corec enum where 120 "enum m = S m (enum (m + 1))" 121 122lemma "(\<And>m. f m = S m (f (m + 1))) \<Longrightarrow> f m = enum m" 123 apply corec_unique 124 apply (rule enum.code) 125 done 126 127lemma "(\<forall>m. f m = S m (f (m + 1))) \<Longrightarrow> f m = enum m" 128 apply corec_unique 129 apply (rule enum.code) 130 done 131 132 133subsection \<open>Lazy Lists of Natural Numbers\<close> 134 135codatatype llist = LNil | LCons nat llist 136 137corec h1 where 138 "h1 x = (if x = 1 then 139 LNil 140 else 141 let x = if x mod 2 = 0 then x div 2 else 3 * x + 1 in 142 LCons x (h1 x))" 143 144corec h3 where 145 "h3 s = (case s of 146 LNil \<Rightarrow> LNil 147 | LCons x r \<Rightarrow> LCons x (h3 r))" 148 149corec fold_map where 150 "fold_map f a s = (let v = f a (head s) in S v (fold_map f v (tail s)))" 151 152friend_of_corec fold_map where 153 "fold_map f a s = (let v = f a (head s) in S v (fold_map f v (tail s)))" 154 apply (rule fold_map.code) 155 sorry 156 157 158subsection \<open>Coinductive Natural Numbers\<close> 159 160codatatype conat = CoZero | CoSuc conat 161 162corec sum where 163 "sum x y = (case x of 164 CoZero \<Rightarrow> y 165 | CoSuc x \<Rightarrow> CoSuc (sum x y))" 166 167friend_of_corec sum where 168 "sum x y = (case x of 169 CoZero \<Rightarrow> (case y of CoZero \<Rightarrow> CoZero | CoSuc y \<Rightarrow> CoSuc y) 170 | CoSuc x \<Rightarrow> CoSuc (sum x y))" 171 sorry 172 173corec (friend) prod where 174 "prod x y = (case (x, y) of 175 (CoZero, _) \<Rightarrow> CoZero 176 | (_, CoZero) \<Rightarrow> CoZero 177 | (CoSuc x, CoSuc y) \<Rightarrow> CoSuc (sum (prod x y) (sum x y)))" 178 179end 180