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