src/HOL/Lazy_Sequence.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 38857 97775f3e8722
child 40051 b6acda4d1c29
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
bulwahn@34948
     1
bulwahn@34948
     2
(* Author: Lukas Bulwahn, TU Muenchen *)
bulwahn@34948
     3
bulwahn@34948
     4
header {* Lazy sequences *}
bulwahn@34948
     5
bulwahn@34948
     6
theory Lazy_Sequence
bulwahn@34948
     7
imports List Code_Numeral
bulwahn@34948
     8
begin
bulwahn@34948
     9
bulwahn@34948
    10
datatype 'a lazy_sequence = Empty | Insert 'a "'a lazy_sequence"
bulwahn@34948
    11
bulwahn@34948
    12
definition Lazy_Sequence :: "(unit => ('a * 'a lazy_sequence) option) => 'a lazy_sequence"
bulwahn@34948
    13
where
bulwahn@34948
    14
  "Lazy_Sequence f = (case f () of None => Empty | Some (x, xq) => Insert x xq)"
bulwahn@34948
    15
bulwahn@34948
    16
code_datatype Lazy_Sequence 
bulwahn@34948
    17
bulwahn@34948
    18
primrec yield :: "'a lazy_sequence => ('a * 'a lazy_sequence) option"
bulwahn@34948
    19
where
bulwahn@34948
    20
  "yield Empty = None"
bulwahn@34948
    21
| "yield (Insert x xq) = Some (x, xq)"
bulwahn@34948
    22
bulwahn@34948
    23
lemma [simp]: "yield xq = Some (x, xq') ==> size xq' < size xq"
bulwahn@34948
    24
by (cases xq) auto
bulwahn@34948
    25
bulwahn@34948
    26
lemma yield_Seq [code]:
bulwahn@34948
    27
  "yield (Lazy_Sequence f) = f ()"
bulwahn@34948
    28
unfolding Lazy_Sequence_def by (cases "f ()") auto
bulwahn@34948
    29
bulwahn@34948
    30
lemma Seq_yield:
bulwahn@34948
    31
  "Lazy_Sequence (%u. yield f) = f"
bulwahn@34948
    32
unfolding Lazy_Sequence_def by (cases f) auto
bulwahn@34948
    33
bulwahn@34948
    34
lemma lazy_sequence_size_code [code]:
bulwahn@34948
    35
  "lazy_sequence_size s xq = (case yield xq of None => 0 | Some (x, xq') => s x + lazy_sequence_size s xq' + 1)"
bulwahn@34948
    36
by (cases xq) auto
bulwahn@34948
    37
bulwahn@34948
    38
lemma size_code [code]:
bulwahn@34948
    39
  "size xq = (case yield xq of None => 0 | Some (x, xq') => size xq' + 1)"
bulwahn@34948
    40
by (cases xq) auto
bulwahn@34948
    41
haftmann@38857
    42
lemma [code]: "HOL.equal xq yq = (case (yield xq, yield yq) of
haftmann@38857
    43
  (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.equal x y) \<and> (HOL.equal xq yq) | _ => False)"
haftmann@38857
    44
apply (cases xq) apply (cases yq) apply (auto simp add: equal_eq) 
haftmann@38857
    45
apply (cases yq) apply (auto simp add: equal_eq) done
haftmann@38857
    46
haftmann@38857
    47
lemma [code nbe]:
haftmann@38857
    48
  "HOL.equal (x :: 'a lazy_sequence) x \<longleftrightarrow> True"
haftmann@38857
    49
  by (fact equal_refl)
bulwahn@34948
    50
bulwahn@34948
    51
lemma seq_case [code]:
bulwahn@34948
    52
  "lazy_sequence_case f g xq = (case (yield xq) of None => f | Some (x, xq') => g x xq')"
bulwahn@34948
    53
by (cases xq) auto
bulwahn@34948
    54
bulwahn@34948
    55
lemma [code]: "lazy_sequence_rec f g xq = (case (yield xq) of None => f | Some (x, xq') => g x xq' (lazy_sequence_rec f g xq'))"
bulwahn@34948
    56
by (cases xq) auto
bulwahn@34948
    57
bulwahn@34948
    58
definition empty :: "'a lazy_sequence"
bulwahn@34948
    59
where
bulwahn@34948
    60
  [code]: "empty = Lazy_Sequence (%u. None)"
bulwahn@34948
    61
bulwahn@34948
    62
definition single :: "'a => 'a lazy_sequence"
bulwahn@34948
    63
where
bulwahn@34948
    64
  [code]: "single x = Lazy_Sequence (%u. Some (x, empty))"
bulwahn@34948
    65
bulwahn@34948
    66
primrec append :: "'a lazy_sequence => 'a lazy_sequence => 'a lazy_sequence"
bulwahn@34948
    67
where
bulwahn@34948
    68
  "append Empty yq = yq"
bulwahn@34948
    69
| "append (Insert x xq) yq = Insert x (append xq yq)"
bulwahn@34948
    70
bulwahn@34948
    71
lemma [code]:
bulwahn@34948
    72
  "append xq yq = Lazy_Sequence (%u. case yield xq of
bulwahn@34948
    73
     None => yield yq
bulwahn@34948
    74
  | Some (x, xq') => Some (x, append xq' yq))"
bulwahn@34948
    75
unfolding Lazy_Sequence_def
bulwahn@34948
    76
apply (cases "xq")
bulwahn@34948
    77
apply auto
bulwahn@34948
    78
apply (cases "yq")
bulwahn@34948
    79
apply auto
bulwahn@34948
    80
done
bulwahn@34948
    81
bulwahn@34948
    82
primrec flat :: "'a lazy_sequence lazy_sequence => 'a lazy_sequence"
bulwahn@34948
    83
where
bulwahn@34948
    84
  "flat Empty = Empty"
bulwahn@34948
    85
| "flat (Insert xq xqq) = append xq (flat xqq)"
bulwahn@34948
    86
 
bulwahn@34948
    87
lemma [code]:
bulwahn@34948
    88
  "flat xqq = Lazy_Sequence (%u. case yield xqq of
bulwahn@34948
    89
    None => None
bulwahn@34948
    90
  | Some (xq, xqq') => yield (append xq (flat xqq')))"
bulwahn@34948
    91
apply (cases "xqq")
bulwahn@34948
    92
apply (auto simp add: Seq_yield)
bulwahn@34948
    93
unfolding Lazy_Sequence_def
bulwahn@34948
    94
by auto
bulwahn@34948
    95
bulwahn@34948
    96
primrec map :: "('a => 'b) => 'a lazy_sequence => 'b lazy_sequence"
bulwahn@34948
    97
where
bulwahn@34948
    98
  "map f Empty = Empty"
bulwahn@34948
    99
| "map f (Insert x xq) = Insert (f x) (map f xq)"
bulwahn@34948
   100
bulwahn@34948
   101
lemma [code]:
bulwahn@34948
   102
  "map f xq = Lazy_Sequence (%u. Option.map (%(x, xq'). (f x, map f xq')) (yield xq))"
bulwahn@34948
   103
apply (cases xq)
bulwahn@34948
   104
apply (auto simp add: Seq_yield)
bulwahn@34948
   105
unfolding Lazy_Sequence_def
bulwahn@34948
   106
apply auto
bulwahn@34948
   107
done
bulwahn@34948
   108
bulwahn@34948
   109
definition bind :: "'a lazy_sequence => ('a => 'b lazy_sequence) => 'b lazy_sequence"
bulwahn@34948
   110
where
bulwahn@34948
   111
  [code]: "bind xq f = flat (map f xq)"
bulwahn@34948
   112
bulwahn@34948
   113
definition if_seq :: "bool => unit lazy_sequence"
bulwahn@34948
   114
where
bulwahn@34948
   115
  "if_seq b = (if b then single () else empty)"
bulwahn@34948
   116
bulwahn@36049
   117
function iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a Lazy_Sequence.lazy_sequence"
bulwahn@36049
   118
where
bulwahn@36049
   119
  "iterate_upto f n m = Lazy_Sequence.Lazy_Sequence (%u. if n > m then None else Some (f n, iterate_upto f (n + 1) m))"
bulwahn@36049
   120
by pat_completeness auto
bulwahn@36049
   121
bulwahn@36049
   122
termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
bulwahn@36049
   123
bulwahn@34948
   124
definition not_seq :: "unit lazy_sequence => unit lazy_sequence"
bulwahn@34948
   125
where
bulwahn@34948
   126
  "not_seq xq = (case yield xq of None => single () | Some ((), xq) => empty)"
bulwahn@34948
   127
bulwahn@34948
   128
subsection {* Code setup *}
bulwahn@34948
   129
haftmann@36533
   130
fun anamorph :: "('a \<Rightarrow> ('b \<times> 'a) option) \<Rightarrow> code_numeral \<Rightarrow> 'a \<Rightarrow> 'b list \<times> 'a" where
haftmann@36533
   131
  "anamorph f k x = (if k = 0 then ([], x)
haftmann@36533
   132
    else case f x of None \<Rightarrow> ([], x) | Some (v, y) \<Rightarrow>
haftmann@36533
   133
      let (vs, z) = anamorph f (k - 1) y
haftmann@36533
   134
    in (v # vs, z))"
bulwahn@34948
   135
haftmann@36533
   136
definition yieldn :: "code_numeral \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'a list \<times> 'a lazy_sequence" where
haftmann@36533
   137
  "yieldn = anamorph yield"
bulwahn@34948
   138
haftmann@36533
   139
code_reflect Lazy_Sequence
haftmann@36533
   140
  datatypes lazy_sequence = Lazy_Sequence
haftmann@36533
   141
  functions map yield yieldn
bulwahn@34948
   142
huffman@36902
   143
subsection {* With Hit Bound Value *}
bulwahn@36030
   144
text {* assuming in negative context *}
bulwahn@36030
   145
bulwahn@36030
   146
types 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
bulwahn@36030
   147
bulwahn@36030
   148
definition hit_bound :: "'a hit_bound_lazy_sequence"
bulwahn@36030
   149
where
bulwahn@36030
   150
  [code]: "hit_bound = Lazy_Sequence (%u. Some (None, empty))"
bulwahn@36030
   151
bulwahn@36030
   152
bulwahn@36030
   153
definition hb_single :: "'a => 'a hit_bound_lazy_sequence"
bulwahn@36030
   154
where
bulwahn@36030
   155
  [code]: "hb_single x = Lazy_Sequence (%u. Some (Some x, empty))"
bulwahn@36030
   156
bulwahn@36030
   157
primrec hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence => 'a hit_bound_lazy_sequence"
bulwahn@36030
   158
where
bulwahn@36030
   159
  "hb_flat Empty = Empty"
bulwahn@36030
   160
| "hb_flat (Insert xq xqq) = append (case xq of None => hit_bound | Some xq => xq) (hb_flat xqq)"
bulwahn@36030
   161
bulwahn@36030
   162
lemma [code]:
bulwahn@36030
   163
  "hb_flat xqq = Lazy_Sequence (%u. case yield xqq of
bulwahn@36030
   164
    None => None
bulwahn@36030
   165
  | Some (xq, xqq') => yield (append (case xq of None => hit_bound | Some xq => xq) (hb_flat xqq')))"
bulwahn@36030
   166
apply (cases "xqq")
bulwahn@36030
   167
apply (auto simp add: Seq_yield)
bulwahn@36030
   168
unfolding Lazy_Sequence_def
bulwahn@36030
   169
by auto
bulwahn@36030
   170
bulwahn@36030
   171
primrec hb_map :: "('a => 'b) => 'a hit_bound_lazy_sequence => 'b hit_bound_lazy_sequence"
bulwahn@36030
   172
where
bulwahn@36030
   173
  "hb_map f Empty = Empty"
bulwahn@36030
   174
| "hb_map f (Insert x xq) = Insert (Option.map f x) (hb_map f xq)"
bulwahn@36030
   175
bulwahn@36030
   176
lemma [code]:
bulwahn@36030
   177
  "hb_map f xq = Lazy_Sequence (%u. Option.map (%(x, xq'). (Option.map f x, hb_map f xq')) (yield xq))"
bulwahn@36030
   178
apply (cases xq)
bulwahn@36030
   179
apply (auto simp add: Seq_yield)
bulwahn@36030
   180
unfolding Lazy_Sequence_def
bulwahn@36030
   181
apply auto
bulwahn@36030
   182
done
bulwahn@36030
   183
bulwahn@36030
   184
definition hb_bind :: "'a hit_bound_lazy_sequence => ('a => 'b hit_bound_lazy_sequence) => 'b hit_bound_lazy_sequence"
bulwahn@36030
   185
where
bulwahn@36030
   186
  [code]: "hb_bind xq f = hb_flat (hb_map f xq)"
bulwahn@36030
   187
bulwahn@36030
   188
definition hb_if_seq :: "bool => unit hit_bound_lazy_sequence"
bulwahn@36030
   189
where
bulwahn@36030
   190
  "hb_if_seq b = (if b then hb_single () else empty)"
bulwahn@36030
   191
bulwahn@36030
   192
definition hb_not_seq :: "unit hit_bound_lazy_sequence => unit lazy_sequence"
bulwahn@36030
   193
where
bulwahn@36030
   194
  "hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
bulwahn@36030
   195
wenzelm@36176
   196
hide_type (open) lazy_sequence
wenzelm@36176
   197
hide_const (open) Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq iterate_upto not_seq
wenzelm@36176
   198
hide_fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def iterate_upto.simps if_seq_def not_seq_def
bulwahn@34948
   199
bulwahn@34948
   200
end