src/HOL/Corec_Examples/Tests/Small_Concrete.thy
 author blanchet Tue Mar 22 12:39:37 2016 +0100 (2016-03-22) changeset 62696 7325d8573fb8 child 62726 5b2a7caa855b permissions -rw-r--r--
```     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
```
```     6 Small concrete examples.
```
```     7 *)
```
```     8
```
```     9 section {* Small Concrete Examples *}
```
```    10
```
```    11 theory Small_Concrete
```
```    12 imports "~~/src/HOL/Library/BNF_Corec"
```
```    13 begin
```
```    14
```
```    15 subsection {* Streams of Natural Numbers *}
```
```    16
```
```    17 codatatype natstream = S (head: nat) (tail: natstream)
```
```    18
```
```    19 corec (friend) incr_all where
```
```    20   "incr_all s = S (head s + 1) (incr_all (tail s))"
```
```    21
```
```    22 corec all_numbers where
```
```    23   "all_numbers = S 0 (incr_all all_numbers)"
```
```    24
```
```    25 corec all_numbers_efficient where
```
```    26   "all_numbers_efficient n = S n (all_numbers_efficient (n + 1))"
```
```    27
```
```    28 corec 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
```
```    35 corec 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
```
```    40 term "prime_numbers []"
```
```    41
```
```    42 corec 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
```
```    47 term "prime_numbers_more_efficient 0 (tail (tail all_numbers))"
```
```    48
```
```    49 corec (friend) alternate where
```
```    50   "alternate s1 s2 = S (head s1) (S (head s2) (alternate (tail s1) (tail s2)))"
```
```    51
```
```    52 corec (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
```
```    55 corec 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
```
```    60 friend_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
```
```    66 corec 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
```
```    69 friend_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
```
```    73 corec iterations where
```
```    74   "iterations f a = S a (iterations f (f a))"
```
```    75
```
```    76 corec exponential_iterations where
```
```    77   "exponential_iterations f a = S (f a) (exponential_iterations (f o f) a)"
```
```    78
```
```    79 corec (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
```
```    82 corec 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
```
```    86 corec 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
```
```    90 corec fibonacci where
```
```    91   "fibonacci n m = S m (fibonacci (n + m) n)"
```
```    92
```
```    93 corec sequence2 where
```
```    94   "sequence2 f u1 u0 = S u0 (sequence2 f (f u1 u0) u1)"
```
```    95
```
```    96 corec (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
```
```   100 corec 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
```
```   105 friend_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
```
```   111 corec z where
```
```   112   "z = S 0 (S 0 z)"
```
```   113
```
```   114 lemma "\<And>x. x = S 0 (S 0 x) \<Longrightarrow> x = z"
```
```   115   apply corec_unique
```
```   116   apply (rule z.code)
```
```   117   done
```
```   118
```
```   119 corec enum where
```
```   120   "enum m = S m (enum (m + 1))"
```
```   121
```
```   122 lemma "(\<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
```
```   127 lemma "(\<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
```
```   133 subsection {* Lazy Lists of Natural Numbers *}
```
```   134
```
```   135 codatatype llist = LNil | LCons nat llist
```
```   136
```
```   137 corec 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
```
```   144 corec h3 where
```
```   145   "h3 s = (case s of
```
```   146     LNil \<Rightarrow> LNil
```
```   147   | LCons x r \<Rightarrow> LCons x (h3 r))"
```
```   148
```
```   149 corec (friend) 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
```
```   152
```
```   153 subsection {* Coinductie Natural Numbers *}
```
```   154
```
```   155 codatatype conat = CoZero | CoSuc conat
```
```   156
```
```   157 corec sum where
```
```   158   "sum x y = (case x of
```
```   159       CoZero \<Rightarrow> y
```
```   160     | CoSuc x \<Rightarrow> CoSuc (sum x y))"
```
```   161
```
```   162 friend_of_corec sum where
```
```   163   "sum x y = (case x of
```
```   164       CoZero \<Rightarrow> (case y of CoZero \<Rightarrow> CoZero | CoSuc y \<Rightarrow> CoSuc y)
```
```   165     | CoSuc x \<Rightarrow> CoSuc (sum x y))"
```
```   166   sorry
```
```   167
```
```   168 corec (friend) prod where
```
```   169   "prod x y = (case (x, y) of
```
```   170       (CoZero, _) \<Rightarrow> CoZero
```
```   171     | (_, CoZero) \<Rightarrow> CoZero
```
```   172     | (CoSuc x, CoSuc y) \<Rightarrow> CoSuc (sum (prod x y) (sum x y)))"
```
```   173
```
```   174 end
```