src/HOL/Lazy_Sequence.thy
author haftmann
Thu Feb 14 15:27:10 2013 +0100 (2013-02-14)
changeset 51126 df86080de4cb
parent 50055 94041d602ecb
child 51143 0a2371e7ced3
permissions -rw-r--r--
reform of predicate compiler / quickcheck theories:
implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers!
avoid odd New_ prefix by joining related theories;
avoid overcompact name DSequence;
separated predicate inside random monad into separate theory;
consolidated name of theory Quickcheck
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
haftmann@50055
     7
imports Predicate
bulwahn@34948
     8
begin
bulwahn@34948
     9
haftmann@51126
    10
subsection {* Type of lazy sequences *}
bulwahn@34948
    11
haftmann@51126
    12
datatype 'a lazy_sequence = lazy_sequence_of_list "'a list"
bulwahn@34948
    13
haftmann@51126
    14
primrec list_of_lazy_sequence :: "'a lazy_sequence \<Rightarrow> 'a list"
bulwahn@34948
    15
where
haftmann@51126
    16
  "list_of_lazy_sequence (lazy_sequence_of_list xs) = xs"
haftmann@51126
    17
haftmann@51126
    18
lemma lazy_sequence_of_list_of_lazy_sequence [simp]:
haftmann@51126
    19
  "lazy_sequence_of_list (list_of_lazy_sequence xq) = xq"
haftmann@51126
    20
  by (cases xq) simp_all
haftmann@51126
    21
haftmann@51126
    22
lemma lazy_sequence_eqI:
haftmann@51126
    23
  "list_of_lazy_sequence xq = list_of_lazy_sequence yq \<Longrightarrow> xq = yq"
haftmann@51126
    24
  by (cases xq, cases yq) simp
haftmann@51126
    25
haftmann@51126
    26
lemma lazy_sequence_eq_iff:
haftmann@51126
    27
  "xq = yq \<longleftrightarrow> list_of_lazy_sequence xq = list_of_lazy_sequence yq"
haftmann@51126
    28
  by (auto intro: lazy_sequence_eqI)
bulwahn@34948
    29
haftmann@51126
    30
lemma lazy_sequence_size_eq:
haftmann@51126
    31
  "lazy_sequence_size f xq = Suc (list_size f (list_of_lazy_sequence xq))"
haftmann@51126
    32
  by (cases xq) simp
haftmann@51126
    33
haftmann@51126
    34
lemma size_lazy_sequence_eq [code]:
haftmann@51126
    35
  "size (xq :: 'a lazy_sequence) = 0"
haftmann@51126
    36
  by (cases xq) simp
haftmann@51126
    37
haftmann@51126
    38
lemma lazy_sequence_case [simp]:
haftmann@51126
    39
  "lazy_sequence_case f xq = f (list_of_lazy_sequence xq)"
haftmann@51126
    40
  by (cases xq) auto
haftmann@51126
    41
haftmann@51126
    42
lemma lazy_sequence_rec [simp]:
haftmann@51126
    43
  "lazy_sequence_rec f xq = f (list_of_lazy_sequence xq)"
haftmann@51126
    44
  by (cases xq) auto
bulwahn@34948
    45
haftmann@51126
    46
definition Lazy_Sequence :: "(unit \<Rightarrow> ('a \<times> 'a lazy_sequence) option) \<Rightarrow> 'a lazy_sequence"
haftmann@51126
    47
where
haftmann@51126
    48
  "Lazy_Sequence f = lazy_sequence_of_list (case f () of
haftmann@51126
    49
    None \<Rightarrow> []
haftmann@51126
    50
  | Some (x, xq) \<Rightarrow> x # list_of_lazy_sequence xq)"
haftmann@51126
    51
haftmann@51126
    52
code_datatype Lazy_Sequence
haftmann@51126
    53
haftmann@51126
    54
declare list_of_lazy_sequence.simps [code del]
haftmann@51126
    55
declare lazy_sequence.cases [code del]
haftmann@51126
    56
declare lazy_sequence.recs [code del]
bulwahn@34948
    57
haftmann@51126
    58
lemma list_of_Lazy_Sequence [simp]:
haftmann@51126
    59
  "list_of_lazy_sequence (Lazy_Sequence f) = (case f () of
haftmann@51126
    60
    None \<Rightarrow> []
haftmann@51126
    61
  | Some (x, xq) \<Rightarrow> x # list_of_lazy_sequence xq)"
haftmann@51126
    62
  by (simp add: Lazy_Sequence_def)
haftmann@51126
    63
haftmann@51126
    64
definition yield :: "'a lazy_sequence \<Rightarrow> ('a \<times> 'a lazy_sequence) option"
haftmann@51126
    65
where
haftmann@51126
    66
  "yield xq = (case list_of_lazy_sequence xq of
haftmann@51126
    67
    [] \<Rightarrow> None
haftmann@51126
    68
  | x # xs \<Rightarrow> Some (x, lazy_sequence_of_list xs))" 
haftmann@51126
    69
haftmann@51126
    70
lemma yield_Seq [simp, code]:
haftmann@51126
    71
  "yield (Lazy_Sequence f) = f ()"
haftmann@51126
    72
  by (cases "f ()") (simp_all add: yield_def split_def)
haftmann@51126
    73
haftmann@51126
    74
lemma case_yield_eq [simp]: "option_case g h (yield xq) =
haftmann@51126
    75
  list_case g (\<lambda>x. curry h x \<circ> lazy_sequence_of_list) (list_of_lazy_sequence xq)"
haftmann@51126
    76
  by (cases "list_of_lazy_sequence xq") (simp_all add: yield_def)
bulwahn@34948
    77
bulwahn@34948
    78
lemma lazy_sequence_size_code [code]:
haftmann@51126
    79
  "lazy_sequence_size s xq = (case yield xq of
haftmann@51126
    80
    None \<Rightarrow> 1
haftmann@51126
    81
  | Some (x, xq') \<Rightarrow> Suc (s x + lazy_sequence_size s xq'))"
haftmann@51126
    82
  by (cases "list_of_lazy_sequence xq") (simp_all add: lazy_sequence_size_eq)
bulwahn@34948
    83
haftmann@51126
    84
lemma equal_lazy_sequence_code [code]:
haftmann@51126
    85
  "HOL.equal xq yq = (case (yield xq, yield yq) of
haftmann@51126
    86
    (None, None) \<Rightarrow> True
haftmann@51126
    87
  | (Some (x, xq'), Some (y, yq')) \<Rightarrow> HOL.equal x y \<and> HOL.equal xq yq
haftmann@51126
    88
  | _ \<Rightarrow> False)"
haftmann@51126
    89
  by (simp_all add: lazy_sequence_eq_iff equal_eq split: list.splits)
haftmann@38857
    90
haftmann@38857
    91
lemma [code nbe]:
haftmann@38857
    92
  "HOL.equal (x :: 'a lazy_sequence) x \<longleftrightarrow> True"
haftmann@38857
    93
  by (fact equal_refl)
bulwahn@34948
    94
bulwahn@34948
    95
definition empty :: "'a lazy_sequence"
bulwahn@34948
    96
where
haftmann@51126
    97
  "empty = lazy_sequence_of_list []"
bulwahn@34948
    98
haftmann@51126
    99
lemma list_of_lazy_sequence_empty [simp]:
haftmann@51126
   100
  "list_of_lazy_sequence empty = []"
haftmann@51126
   101
  by (simp add: empty_def)
bulwahn@34948
   102
haftmann@51126
   103
lemma empty_code [code]:
haftmann@51126
   104
  "empty = Lazy_Sequence (\<lambda>_. None)"
haftmann@51126
   105
  by (simp add: lazy_sequence_eq_iff)
bulwahn@34948
   106
haftmann@51126
   107
definition single :: "'a \<Rightarrow> 'a lazy_sequence"
haftmann@51126
   108
where
haftmann@51126
   109
  "single x = lazy_sequence_of_list [x]"
bulwahn@34948
   110
haftmann@51126
   111
lemma list_of_lazy_sequence_single [simp]:
haftmann@51126
   112
  "list_of_lazy_sequence (single x) = [x]"
haftmann@51126
   113
  by (simp add: single_def)
haftmann@51126
   114
haftmann@51126
   115
lemma single_code [code]:
haftmann@51126
   116
  "single x = Lazy_Sequence (\<lambda>_. Some (x, empty))"
haftmann@51126
   117
  by (simp add: lazy_sequence_eq_iff)
haftmann@51126
   118
haftmann@51126
   119
definition append :: "'a lazy_sequence \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'a lazy_sequence"
bulwahn@34948
   120
where
haftmann@51126
   121
  "append xq yq = lazy_sequence_of_list (list_of_lazy_sequence xq @ list_of_lazy_sequence yq)"
haftmann@51126
   122
haftmann@51126
   123
lemma list_of_lazy_sequence_append [simp]:
haftmann@51126
   124
  "list_of_lazy_sequence (append xq yq) = list_of_lazy_sequence xq @ list_of_lazy_sequence yq"
haftmann@51126
   125
  by (simp add: append_def)
bulwahn@34948
   126
haftmann@51126
   127
lemma append_code [code]:
haftmann@51126
   128
  "append xq yq = Lazy_Sequence (\<lambda>_. case yield xq of
haftmann@51126
   129
    None \<Rightarrow> yield yq
haftmann@51126
   130
  | Some (x, xq') \<Rightarrow> Some (x, append xq' yq))"
haftmann@51126
   131
  by (simp_all add: lazy_sequence_eq_iff split: list.splits)
haftmann@51126
   132
haftmann@51126
   133
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'b lazy_sequence"
bulwahn@34948
   134
where
haftmann@51126
   135
  "map f xq = lazy_sequence_of_list (List.map f (list_of_lazy_sequence xq))"
haftmann@51126
   136
haftmann@51126
   137
lemma list_of_lazy_sequence_map [simp]:
haftmann@51126
   138
  "list_of_lazy_sequence (map f xq) = List.map f (list_of_lazy_sequence xq)"
haftmann@51126
   139
  by (simp add: map_def)
haftmann@51126
   140
haftmann@51126
   141
lemma map_code [code]:
haftmann@51126
   142
  "map f xq =
haftmann@51126
   143
    Lazy_Sequence (\<lambda>_. Option.map (\<lambda>(x, xq'). (f x, map f xq')) (yield xq))"
haftmann@51126
   144
  by (simp_all add: lazy_sequence_eq_iff split: list.splits)
haftmann@51126
   145
haftmann@51126
   146
definition flat :: "'a lazy_sequence lazy_sequence \<Rightarrow> 'a lazy_sequence"
haftmann@51126
   147
where
haftmann@51126
   148
  "flat xqq = lazy_sequence_of_list (concat (List.map list_of_lazy_sequence (list_of_lazy_sequence xqq)))"
bulwahn@34948
   149
haftmann@51126
   150
lemma list_of_lazy_sequence_flat [simp]:
haftmann@51126
   151
  "list_of_lazy_sequence (flat xqq) = concat (List.map list_of_lazy_sequence (list_of_lazy_sequence xqq))"
haftmann@51126
   152
  by (simp add: flat_def)
bulwahn@34948
   153
haftmann@51126
   154
lemma flat_code [code]:
haftmann@51126
   155
  "flat xqq = Lazy_Sequence (\<lambda>_. case yield xqq of
haftmann@51126
   156
    None \<Rightarrow> None
haftmann@51126
   157
  | Some (xq, xqq') \<Rightarrow> yield (append xq (flat xqq')))"
haftmann@51126
   158
  by (simp add: lazy_sequence_eq_iff split: list.splits)
haftmann@51126
   159
haftmann@51126
   160
definition bind :: "'a lazy_sequence \<Rightarrow> ('a \<Rightarrow> 'b lazy_sequence) \<Rightarrow> 'b lazy_sequence"
bulwahn@34948
   161
where
haftmann@51126
   162
  "bind xq f = flat (map f xq)"
bulwahn@34948
   163
haftmann@51126
   164
definition if_seq :: "bool \<Rightarrow> unit lazy_sequence"
bulwahn@34948
   165
where
bulwahn@34948
   166
  "if_seq b = (if b then single () else empty)"
bulwahn@34948
   167
haftmann@51126
   168
definition those :: "'a option lazy_sequence \<Rightarrow> 'a lazy_sequence option"
bulwahn@36049
   169
where
haftmann@51126
   170
  "those xq = Option.map lazy_sequence_of_list (List.those (list_of_lazy_sequence xq))"
haftmann@51126
   171
  
haftmann@51126
   172
function iterate_upto :: "(code_numeral \<Rightarrow> 'a) \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a lazy_sequence"
haftmann@51126
   173
where
haftmann@51126
   174
  "iterate_upto f n m =
haftmann@51126
   175
    Lazy_Sequence (\<lambda>_. if n > m then None else Some (f n, iterate_upto f (n + 1) m))"
haftmann@51126
   176
  by pat_completeness auto
bulwahn@36049
   177
bulwahn@36049
   178
termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
bulwahn@36049
   179
haftmann@51126
   180
definition not_seq :: "unit lazy_sequence \<Rightarrow> unit lazy_sequence"
bulwahn@34948
   181
where
haftmann@51126
   182
  "not_seq xq = (case yield xq of
haftmann@51126
   183
    None \<Rightarrow> single ()
haftmann@51126
   184
  | Some ((), xq) \<Rightarrow> empty)"
bulwahn@34948
   185
haftmann@51126
   186
  
haftmann@51126
   187
subsection {* Code setup *}
bulwahn@34948
   188
haftmann@36533
   189
code_reflect Lazy_Sequence
haftmann@36533
   190
  datatypes lazy_sequence = Lazy_Sequence
haftmann@51126
   191
haftmann@51126
   192
ML {*
haftmann@51126
   193
signature LAZY_SEQUENCE =
haftmann@51126
   194
sig
haftmann@51126
   195
  datatype 'a lazy_sequence = Lazy_Sequence of (unit -> ('a * 'a Lazy_Sequence.lazy_sequence) option)
haftmann@51126
   196
  val map: ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
haftmann@51126
   197
  val yield: 'a lazy_sequence -> ('a * 'a lazy_sequence) option
haftmann@51126
   198
  val yieldn: int -> 'a lazy_sequence -> 'a list * 'a lazy_sequence
haftmann@51126
   199
end;
haftmann@51126
   200
haftmann@51126
   201
structure Lazy_Sequence : LAZY_SEQUENCE =
haftmann@51126
   202
struct
haftmann@51126
   203
haftmann@51126
   204
datatype lazy_sequence = datatype Lazy_Sequence.lazy_sequence;
haftmann@51126
   205
haftmann@51126
   206
fun map f = @{code Lazy_Sequence.map} f;
haftmann@51126
   207
haftmann@51126
   208
fun yield P = @{code Lazy_Sequence.yield} P;
haftmann@51126
   209
haftmann@51126
   210
fun yieldn k = Predicate.anamorph yield k;
haftmann@51126
   211
haftmann@51126
   212
end;
haftmann@51126
   213
*}
haftmann@51126
   214
bulwahn@34948
   215
bulwahn@40051
   216
subsection {* Generator Sequences *}
bulwahn@40051
   217
bulwahn@40051
   218
subsubsection {* General lazy sequence operation *}
bulwahn@40051
   219
haftmann@51126
   220
definition product :: "'a lazy_sequence \<Rightarrow> 'b lazy_sequence \<Rightarrow> ('a \<times> 'b) lazy_sequence"
bulwahn@40051
   221
where
haftmann@51126
   222
  "product s1 s2 = bind s1 (\<lambda>a. bind s2 (\<lambda>b. single (a, b)))"
bulwahn@40051
   223
bulwahn@40051
   224
hoelzl@40056
   225
subsubsection {* Small lazy typeclasses *}
bulwahn@40051
   226
bulwahn@40051
   227
class small_lazy =
haftmann@51126
   228
  fixes small_lazy :: "code_numeral \<Rightarrow> 'a lazy_sequence"
bulwahn@40051
   229
bulwahn@40051
   230
instantiation unit :: small_lazy
bulwahn@40051
   231
begin
bulwahn@40051
   232
haftmann@51126
   233
definition "small_lazy d = single ()"
bulwahn@40051
   234
bulwahn@40051
   235
instance ..
bulwahn@40051
   236
bulwahn@40051
   237
end
bulwahn@40051
   238
bulwahn@40051
   239
instantiation int :: small_lazy
bulwahn@40051
   240
begin
bulwahn@40051
   241
bulwahn@40051
   242
text {* maybe optimise this expression -> append (single x) xs == cons x xs 
bulwahn@40051
   243
Performance difference? *}
bulwahn@40051
   244
haftmann@51126
   245
function small_lazy' :: "int \<Rightarrow> int \<Rightarrow> int lazy_sequence"
haftmann@51126
   246
where
haftmann@51126
   247
  "small_lazy' d i = (if d < i then empty
haftmann@51126
   248
    else append (single i) (small_lazy' d (i + 1)))"
haftmann@51126
   249
    by pat_completeness auto
bulwahn@40051
   250
bulwahn@40051
   251
termination 
bulwahn@40051
   252
  by (relation "measure (%(d, i). nat (d + 1 - i))") auto
bulwahn@40051
   253
haftmann@51126
   254
definition
haftmann@51126
   255
  "small_lazy d = small_lazy' (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
bulwahn@40051
   256
bulwahn@40051
   257
instance ..
bulwahn@40051
   258
bulwahn@40051
   259
end
bulwahn@40051
   260
bulwahn@40051
   261
instantiation prod :: (small_lazy, small_lazy) small_lazy
bulwahn@40051
   262
begin
bulwahn@40051
   263
bulwahn@40051
   264
definition
bulwahn@40051
   265
  "small_lazy d = product (small_lazy d) (small_lazy d)"
bulwahn@40051
   266
bulwahn@40051
   267
instance ..
bulwahn@40051
   268
bulwahn@40051
   269
end
bulwahn@40051
   270
bulwahn@40051
   271
instantiation list :: (small_lazy) small_lazy
bulwahn@40051
   272
begin
bulwahn@40051
   273
haftmann@51126
   274
fun small_lazy_list :: "code_numeral \<Rightarrow> 'a list lazy_sequence"
bulwahn@40051
   275
where
haftmann@51126
   276
  "small_lazy_list d = append (single [])
haftmann@51126
   277
    (if d > 0 then bind (product (small_lazy (d - 1))
haftmann@51126
   278
      (small_lazy (d - 1))) (\<lambda>(x, xs). single (x # xs)) else empty)"
bulwahn@40051
   279
bulwahn@40051
   280
instance ..
bulwahn@40051
   281
bulwahn@40051
   282
end
bulwahn@40051
   283
huffman@36902
   284
subsection {* With Hit Bound Value *}
bulwahn@36030
   285
text {* assuming in negative context *}
bulwahn@36030
   286
bulwahn@42163
   287
type_synonym 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
bulwahn@36030
   288
bulwahn@36030
   289
definition hit_bound :: "'a hit_bound_lazy_sequence"
bulwahn@36030
   290
where
haftmann@51126
   291
  "hit_bound = Lazy_Sequence (\<lambda>_. Some (None, empty))"
bulwahn@36030
   292
haftmann@51126
   293
lemma list_of_lazy_sequence_hit_bound [simp]:
haftmann@51126
   294
  "list_of_lazy_sequence hit_bound = [None]"
haftmann@51126
   295
  by (simp add: hit_bound_def)
haftmann@51126
   296
  
haftmann@51126
   297
definition hb_single :: "'a \<Rightarrow> 'a hit_bound_lazy_sequence"
bulwahn@36030
   298
where
haftmann@51126
   299
  "hb_single x = Lazy_Sequence (\<lambda>_. Some (Some x, empty))"
bulwahn@36030
   300
haftmann@51126
   301
definition hb_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a hit_bound_lazy_sequence \<Rightarrow> 'b hit_bound_lazy_sequence"
bulwahn@36030
   302
where
haftmann@51126
   303
  "hb_map f xq = map (Option.map f) xq"
haftmann@51126
   304
haftmann@51126
   305
lemma hb_map_code [code]:
haftmann@51126
   306
  "hb_map f xq =
haftmann@51126
   307
    Lazy_Sequence (\<lambda>_. Option.map (\<lambda>(x, xq'). (Option.map f x, hb_map f xq')) (yield xq))"
haftmann@51126
   308
  using map_code [of "Option.map f" xq] by (simp add: hb_map_def)
bulwahn@36030
   309
haftmann@51126
   310
definition hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence \<Rightarrow> 'a hit_bound_lazy_sequence"
haftmann@51126
   311
where
haftmann@51126
   312
  "hb_flat xqq = lazy_sequence_of_list (concat
haftmann@51126
   313
    (List.map ((\<lambda>x. case x of None \<Rightarrow> [None] | Some xs \<Rightarrow> xs) \<circ> Option.map list_of_lazy_sequence) (list_of_lazy_sequence xqq)))"
bulwahn@36030
   314
haftmann@51126
   315
lemma list_of_lazy_sequence_hb_flat [simp]:
haftmann@51126
   316
  "list_of_lazy_sequence (hb_flat xqq) =
haftmann@51126
   317
    concat (List.map ((\<lambda>x. case x of None \<Rightarrow> [None] | Some xs \<Rightarrow> xs) \<circ> Option.map list_of_lazy_sequence) (list_of_lazy_sequence xqq))"
haftmann@51126
   318
  by (simp add: hb_flat_def)
bulwahn@36030
   319
haftmann@51126
   320
lemma hb_flat_code [code]:
haftmann@51126
   321
  "hb_flat xqq = Lazy_Sequence (\<lambda>_. case yield xqq of
haftmann@51126
   322
    None \<Rightarrow> None
haftmann@51126
   323
  | Some (xq, xqq') \<Rightarrow> yield
haftmann@51126
   324
     (append (case xq of None \<Rightarrow> hit_bound | Some xq \<Rightarrow> xq) (hb_flat xqq')))"
haftmann@51126
   325
  by (simp add: lazy_sequence_eq_iff split: list.splits option.splits)
bulwahn@36030
   326
haftmann@51126
   327
definition hb_bind :: "'a hit_bound_lazy_sequence \<Rightarrow> ('a \<Rightarrow> 'b hit_bound_lazy_sequence) \<Rightarrow> 'b hit_bound_lazy_sequence"
bulwahn@36030
   328
where
haftmann@51126
   329
  "hb_bind xq f = hb_flat (hb_map f xq)"
bulwahn@36030
   330
haftmann@51126
   331
definition hb_if_seq :: "bool \<Rightarrow> unit hit_bound_lazy_sequence"
bulwahn@36030
   332
where
bulwahn@36030
   333
  "hb_if_seq b = (if b then hb_single () else empty)"
bulwahn@36030
   334
haftmann@51126
   335
definition hb_not_seq :: "unit hit_bound_lazy_sequence \<Rightarrow> unit lazy_sequence"
bulwahn@36030
   336
where
haftmann@51126
   337
  "hb_not_seq xq = (case yield xq of
haftmann@51126
   338
    None \<Rightarrow> single ()
haftmann@51126
   339
  | Some (x, xq) \<Rightarrow> empty)"
bulwahn@36030
   340
haftmann@51126
   341
hide_const (open) yield empty single append flat map bind
haftmann@51126
   342
  if_seq those iterate_upto not_seq product
haftmann@51126
   343
haftmann@51126
   344
hide_fact (open) yield_def empty_def single_def append_def flat_def map_def bind_def
haftmann@51126
   345
  if_seq_def those_def not_seq_def product_def 
bulwahn@34948
   346
bulwahn@34948
   347
end
haftmann@51126
   348