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