src/HOL/Lazy_Sequence.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 34957 3b1957113753
child 36020 3ee4c29ead7f
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
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
fun yieldn :: "code_numeral => 'a lazy_sequence => 'a list * 'a lazy_sequence"
bulwahn@34948
    24
where
bulwahn@34948
    25
  "yieldn i S = (if i = 0 then ([], S) else
bulwahn@34948
    26
    case yield S of
bulwahn@34948
    27
      None => ([], S)
bulwahn@34948
    28
    | Some (x, S') => let
bulwahn@34948
    29
       (xs, S'') = yieldn (i - 1) S'
bulwahn@34948
    30
      in (x # xs, S''))"
bulwahn@34948
    31
bulwahn@34948
    32
lemma [simp]: "yield xq = Some (x, xq') ==> size xq' < size xq"
bulwahn@34948
    33
by (cases xq) auto
bulwahn@34948
    34
bulwahn@34948
    35
lemma yield_Seq [code]:
bulwahn@34948
    36
  "yield (Lazy_Sequence f) = f ()"
bulwahn@34948
    37
unfolding Lazy_Sequence_def by (cases "f ()") auto
bulwahn@34948
    38
bulwahn@34948
    39
lemma Seq_yield:
bulwahn@34948
    40
  "Lazy_Sequence (%u. yield f) = f"
bulwahn@34948
    41
unfolding Lazy_Sequence_def by (cases f) auto
bulwahn@34948
    42
bulwahn@34948
    43
lemma lazy_sequence_size_code [code]:
bulwahn@34948
    44
  "lazy_sequence_size s xq = (case yield xq of None => 0 | Some (x, xq') => s x + lazy_sequence_size s xq' + 1)"
bulwahn@34948
    45
by (cases xq) auto
bulwahn@34948
    46
bulwahn@34948
    47
lemma size_code [code]:
bulwahn@34948
    48
  "size xq = (case yield xq of None => 0 | Some (x, xq') => size xq' + 1)"
bulwahn@34948
    49
by (cases xq) auto
bulwahn@34948
    50
bulwahn@34948
    51
lemma [code]: "eq_class.eq xq yq = (case (yield xq, yield yq) of
bulwahn@34948
    52
  (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.eq x y) \<and> (eq_class.eq xq yq) | _ => False)"
bulwahn@34948
    53
apply (cases xq) apply (cases yq) apply (auto simp add: eq_class.eq_equals) 
bulwahn@34948
    54
apply (cases yq) apply (auto simp add: eq_class.eq_equals) done
bulwahn@34948
    55
bulwahn@34948
    56
lemma seq_case [code]:
bulwahn@34948
    57
  "lazy_sequence_case f g xq = (case (yield xq) of None => f | Some (x, xq') => g x xq')"
bulwahn@34948
    58
by (cases xq) auto
bulwahn@34948
    59
bulwahn@34948
    60
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
    61
by (cases xq) auto
bulwahn@34948
    62
bulwahn@34948
    63
definition empty :: "'a lazy_sequence"
bulwahn@34948
    64
where
bulwahn@34948
    65
  [code]: "empty = Lazy_Sequence (%u. None)"
bulwahn@34948
    66
bulwahn@34948
    67
definition single :: "'a => 'a lazy_sequence"
bulwahn@34948
    68
where
bulwahn@34948
    69
  [code]: "single x = Lazy_Sequence (%u. Some (x, empty))"
bulwahn@34948
    70
bulwahn@34948
    71
primrec append :: "'a lazy_sequence => 'a lazy_sequence => 'a lazy_sequence"
bulwahn@34948
    72
where
bulwahn@34948
    73
  "append Empty yq = yq"
bulwahn@34948
    74
| "append (Insert x xq) yq = Insert x (append xq yq)"
bulwahn@34948
    75
bulwahn@34948
    76
lemma [code]:
bulwahn@34948
    77
  "append xq yq = Lazy_Sequence (%u. case yield xq of
bulwahn@34948
    78
     None => yield yq
bulwahn@34948
    79
  | Some (x, xq') => Some (x, append xq' yq))"
bulwahn@34948
    80
unfolding Lazy_Sequence_def
bulwahn@34948
    81
apply (cases "xq")
bulwahn@34948
    82
apply auto
bulwahn@34948
    83
apply (cases "yq")
bulwahn@34948
    84
apply auto
bulwahn@34948
    85
done
bulwahn@34948
    86
bulwahn@34948
    87
primrec flat :: "'a lazy_sequence lazy_sequence => 'a lazy_sequence"
bulwahn@34948
    88
where
bulwahn@34948
    89
  "flat Empty = Empty"
bulwahn@34948
    90
| "flat (Insert xq xqq) = append xq (flat xqq)"
bulwahn@34948
    91
 
bulwahn@34948
    92
lemma [code]:
bulwahn@34948
    93
  "flat xqq = Lazy_Sequence (%u. case yield xqq of
bulwahn@34948
    94
    None => None
bulwahn@34948
    95
  | Some (xq, xqq') => yield (append xq (flat xqq')))"
bulwahn@34948
    96
apply (cases "xqq")
bulwahn@34948
    97
apply (auto simp add: Seq_yield)
bulwahn@34948
    98
unfolding Lazy_Sequence_def
bulwahn@34948
    99
by auto
bulwahn@34948
   100
bulwahn@34948
   101
primrec map :: "('a => 'b) => 'a lazy_sequence => 'b lazy_sequence"
bulwahn@34948
   102
where
bulwahn@34948
   103
  "map f Empty = Empty"
bulwahn@34948
   104
| "map f (Insert x xq) = Insert (f x) (map f xq)"
bulwahn@34948
   105
bulwahn@34948
   106
lemma [code]:
bulwahn@34948
   107
  "map f xq = Lazy_Sequence (%u. Option.map (%(x, xq'). (f x, map f xq')) (yield xq))"
bulwahn@34948
   108
apply (cases xq)
bulwahn@34948
   109
apply (auto simp add: Seq_yield)
bulwahn@34948
   110
unfolding Lazy_Sequence_def
bulwahn@34948
   111
apply auto
bulwahn@34948
   112
done
bulwahn@34948
   113
bulwahn@34948
   114
definition bind :: "'a lazy_sequence => ('a => 'b lazy_sequence) => 'b lazy_sequence"
bulwahn@34948
   115
where
bulwahn@34948
   116
  [code]: "bind xq f = flat (map f xq)"
bulwahn@34948
   117
bulwahn@34948
   118
definition if_seq :: "bool => unit lazy_sequence"
bulwahn@34948
   119
where
bulwahn@34948
   120
  "if_seq b = (if b then single () else empty)"
bulwahn@34948
   121
bulwahn@34948
   122
definition not_seq :: "unit lazy_sequence => unit lazy_sequence"
bulwahn@34948
   123
where
bulwahn@34948
   124
  "not_seq xq = (case yield xq of None => single () | Some ((), xq) => empty)"
bulwahn@34948
   125
bulwahn@34948
   126
subsection {* Code setup *}
bulwahn@34948
   127
bulwahn@34948
   128
ML {*
bulwahn@34948
   129
signature LAZY_SEQUENCE =
bulwahn@34948
   130
sig
bulwahn@34948
   131
  datatype 'a lazy_sequence = Lazy_Sequence of unit -> ('a * 'a lazy_sequence) option
bulwahn@34948
   132
  val yield : 'a lazy_sequence -> ('a * 'a lazy_sequence) option
bulwahn@34948
   133
  val yieldn : int -> 'a lazy_sequence -> ('a list * 'a lazy_sequence)
bulwahn@34948
   134
end;
bulwahn@34948
   135
bulwahn@34948
   136
structure Lazy_Sequence : LAZY_SEQUENCE =
bulwahn@34948
   137
struct
bulwahn@34948
   138
bulwahn@34948
   139
@{code_datatype lazy_sequence = Lazy_Sequence}
bulwahn@34948
   140
bulwahn@34948
   141
val yield = @{code yield}
bulwahn@34948
   142
bulwahn@34948
   143
val yieldn = @{code yieldn}
bulwahn@34948
   144
bulwahn@34948
   145
end;
bulwahn@34948
   146
*}
bulwahn@34948
   147
bulwahn@34948
   148
code_reserved Eval Lazy_Sequence
bulwahn@34948
   149
bulwahn@34948
   150
code_type lazy_sequence (Eval "_/ Lazy'_Sequence.lazy'_sequence")
bulwahn@34948
   151
bulwahn@34948
   152
code_const Lazy_Sequence (Eval "Lazy'_Sequence.Lazy'_Sequence")
bulwahn@34948
   153
bulwahn@34948
   154
hide (open) type lazy_sequence
bulwahn@34948
   155
hide (open) const Empty Insert Lazy_Sequence yield yieldn empty single append flat map bind if_seq not_seq
bulwahn@34957
   156
hide fact yield.simps yieldn.simps empty_def single_def append.simps flat.simps map.simps bind_def if_seq_def not_seq_def
bulwahn@34948
   157
bulwahn@34948
   158
end