src/HOL/Lazy_Sequence.thy
author blanchet
Mon, 15 Sep 2014 10:49:07 +0200
changeset 58335 a5a3b576fcfb
parent 58334 7553a1bcecb7
child 58350 919149921e46
permissions -rw-r--r--
generate 'code' attribute only if 'code' plugin is enabled
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
     1
(* Author: Lukas Bulwahn, TU Muenchen *)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
     2
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
     3
header {* Lazy sequences *}
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
     4
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
     5
theory Lazy_Sequence
50055
94041d602ecb tuned import order
haftmann
parents: 45214
diff changeset
     6
imports Predicate
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
     7
begin
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
     8
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
     9
subsection {* Type of lazy sequences *}
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    10
58334
7553a1bcecb7 disable datatype 'plugins' for internal types
blanchet
parents: 58310
diff changeset
    11
datatype (plugins only: code) (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list"
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    12
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    13
primrec list_of_lazy_sequence :: "'a lazy_sequence \<Rightarrow> 'a list"
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    14
where
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    15
  "list_of_lazy_sequence (lazy_sequence_of_list xs) = xs"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    16
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    17
lemma lazy_sequence_of_list_of_lazy_sequence [simp]:
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    18
  "lazy_sequence_of_list (list_of_lazy_sequence xq) = xq"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    19
  by (cases xq) simp_all
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    20
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    21
lemma lazy_sequence_eqI:
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    22
  "list_of_lazy_sequence xq = list_of_lazy_sequence yq \<Longrightarrow> xq = yq"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    23
  by (cases xq, cases yq) simp
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    24
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    25
lemma lazy_sequence_eq_iff:
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    26
  "xq = yq \<longleftrightarrow> list_of_lazy_sequence xq = list_of_lazy_sequence yq"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    27
  by (auto intro: lazy_sequence_eqI)
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    28
55416
dd7992d4a61a adapted theories to 'xxx_case' to 'case_xxx'
blanchet
parents: 55413
diff changeset
    29
lemma case_lazy_sequence [simp]:
dd7992d4a61a adapted theories to 'xxx_case' to 'case_xxx'
blanchet
parents: 55413
diff changeset
    30
  "case_lazy_sequence f xq = f (list_of_lazy_sequence xq)"
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    31
  by (cases xq) auto
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    32
55416
dd7992d4a61a adapted theories to 'xxx_case' to 'case_xxx'
blanchet
parents: 55413
diff changeset
    33
lemma rec_lazy_sequence [simp]:
dd7992d4a61a adapted theories to 'xxx_case' to 'case_xxx'
blanchet
parents: 55413
diff changeset
    34
  "rec_lazy_sequence f xq = f (list_of_lazy_sequence xq)"
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    35
  by (cases xq) auto
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    36
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    37
definition Lazy_Sequence :: "(unit \<Rightarrow> ('a \<times> 'a lazy_sequence) option) \<Rightarrow> 'a lazy_sequence"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    38
where
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    39
  "Lazy_Sequence f = lazy_sequence_of_list (case f () of
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    40
    None \<Rightarrow> []
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    41
  | Some (x, xq) \<Rightarrow> x # list_of_lazy_sequence xq)"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    42
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    43
code_datatype Lazy_Sequence
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    44
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    45
declare list_of_lazy_sequence.simps [code del]
55642
63beb38e9258 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents: 55466
diff changeset
    46
declare lazy_sequence.case [code del]
63beb38e9258 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents: 55466
diff changeset
    47
declare lazy_sequence.rec [code del]
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    48
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    49
lemma list_of_Lazy_Sequence [simp]:
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    50
  "list_of_lazy_sequence (Lazy_Sequence f) = (case f () of
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    51
    None \<Rightarrow> []
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    52
  | Some (x, xq) \<Rightarrow> x # list_of_lazy_sequence xq)"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    53
  by (simp add: Lazy_Sequence_def)
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    54
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    55
definition yield :: "'a lazy_sequence \<Rightarrow> ('a \<times> 'a lazy_sequence) option"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    56
where
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    57
  "yield xq = (case list_of_lazy_sequence xq of
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    58
    [] \<Rightarrow> None
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    59
  | x # xs \<Rightarrow> Some (x, lazy_sequence_of_list xs))" 
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    60
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    61
lemma yield_Seq [simp, code]:
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    62
  "yield (Lazy_Sequence f) = f ()"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    63
  by (cases "f ()") (simp_all add: yield_def split_def)
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    64
55413
a8e96847523c adapted theories to '{case,rec}_{list,option}' names
blanchet
parents: 51143
diff changeset
    65
lemma case_yield_eq [simp]: "case_option g h (yield xq) =
a8e96847523c adapted theories to '{case,rec}_{list,option}' names
blanchet
parents: 51143
diff changeset
    66
  case_list g (\<lambda>x. curry h x \<circ> lazy_sequence_of_list) (list_of_lazy_sequence xq)"
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    67
  by (cases "list_of_lazy_sequence xq") (simp_all add: yield_def)
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    68
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    69
lemma equal_lazy_sequence_code [code]:
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    70
  "HOL.equal xq yq = (case (yield xq, yield yq) of
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    71
    (None, None) \<Rightarrow> True
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    72
  | (Some (x, xq'), Some (y, yq')) \<Rightarrow> HOL.equal x y \<and> HOL.equal xq yq
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    73
  | _ \<Rightarrow> False)"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    74
  by (simp_all add: lazy_sequence_eq_iff equal_eq split: list.splits)
38857
97775f3e8722 renamed class/constant eq to equal; tuned some instantiations
haftmann
parents: 36902
diff changeset
    75
97775f3e8722 renamed class/constant eq to equal; tuned some instantiations
haftmann
parents: 36902
diff changeset
    76
lemma [code nbe]:
97775f3e8722 renamed class/constant eq to equal; tuned some instantiations
haftmann
parents: 36902
diff changeset
    77
  "HOL.equal (x :: 'a lazy_sequence) x \<longleftrightarrow> True"
97775f3e8722 renamed class/constant eq to equal; tuned some instantiations
haftmann
parents: 36902
diff changeset
    78
  by (fact equal_refl)
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    79
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    80
definition empty :: "'a lazy_sequence"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    81
where
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    82
  "empty = lazy_sequence_of_list []"
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    83
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    84
lemma list_of_lazy_sequence_empty [simp]:
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    85
  "list_of_lazy_sequence empty = []"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    86
  by (simp add: empty_def)
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    87
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    88
lemma empty_code [code]:
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    89
  "empty = Lazy_Sequence (\<lambda>_. None)"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    90
  by (simp add: lazy_sequence_eq_iff)
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    91
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    92
definition single :: "'a \<Rightarrow> 'a lazy_sequence"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    93
where
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    94
  "single x = lazy_sequence_of_list [x]"
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    95
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    96
lemma list_of_lazy_sequence_single [simp]:
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    97
  "list_of_lazy_sequence (single x) = [x]"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    98
  by (simp add: single_def)
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
    99
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   100
lemma single_code [code]:
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   101
  "single x = Lazy_Sequence (\<lambda>_. Some (x, empty))"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   102
  by (simp add: lazy_sequence_eq_iff)
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   103
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   104
definition append :: "'a lazy_sequence \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'a lazy_sequence"
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   105
where
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   106
  "append xq yq = lazy_sequence_of_list (list_of_lazy_sequence xq @ list_of_lazy_sequence yq)"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   107
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   108
lemma list_of_lazy_sequence_append [simp]:
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   109
  "list_of_lazy_sequence (append xq yq) = list_of_lazy_sequence xq @ list_of_lazy_sequence yq"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   110
  by (simp add: append_def)
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   111
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   112
lemma append_code [code]:
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   113
  "append xq yq = Lazy_Sequence (\<lambda>_. case yield xq of
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   114
    None \<Rightarrow> yield yq
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   115
  | Some (x, xq') \<Rightarrow> Some (x, append xq' yq))"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   116
  by (simp_all add: lazy_sequence_eq_iff split: list.splits)
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   117
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   118
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'b lazy_sequence"
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   119
where
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   120
  "map f xq = lazy_sequence_of_list (List.map f (list_of_lazy_sequence xq))"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   121
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   122
lemma list_of_lazy_sequence_map [simp]:
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   123
  "list_of_lazy_sequence (map f xq) = List.map f (list_of_lazy_sequence xq)"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   124
  by (simp add: map_def)
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   125
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   126
lemma map_code [code]:
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   127
  "map f xq =
55466
786edc984c98 merged 'Option.map' and 'Option.map_option'
blanchet
parents: 55416
diff changeset
   128
    Lazy_Sequence (\<lambda>_. map_option (\<lambda>(x, xq'). (f x, map f xq')) (yield xq))"
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   129
  by (simp_all add: lazy_sequence_eq_iff split: list.splits)
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   130
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   131
definition flat :: "'a lazy_sequence lazy_sequence \<Rightarrow> 'a lazy_sequence"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   132
where
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   133
  "flat xqq = lazy_sequence_of_list (concat (List.map list_of_lazy_sequence (list_of_lazy_sequence xqq)))"
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   134
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   135
lemma list_of_lazy_sequence_flat [simp]:
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   136
  "list_of_lazy_sequence (flat xqq) = concat (List.map list_of_lazy_sequence (list_of_lazy_sequence xqq))"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   137
  by (simp add: flat_def)
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   138
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   139
lemma flat_code [code]:
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   140
  "flat xqq = Lazy_Sequence (\<lambda>_. case yield xqq of
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   141
    None \<Rightarrow> None
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   142
  | Some (xq, xqq') \<Rightarrow> yield (append xq (flat xqq')))"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   143
  by (simp add: lazy_sequence_eq_iff split: list.splits)
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   144
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   145
definition bind :: "'a lazy_sequence \<Rightarrow> ('a \<Rightarrow> 'b lazy_sequence) \<Rightarrow> 'b lazy_sequence"
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   146
where
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   147
  "bind xq f = flat (map f xq)"
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   148
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   149
definition if_seq :: "bool \<Rightarrow> unit lazy_sequence"
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   150
where
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   151
  "if_seq b = (if b then single () else empty)"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   152
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   153
definition those :: "'a option lazy_sequence \<Rightarrow> 'a lazy_sequence option"
36049
0ce5b7a5c2fd adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents: 36030
diff changeset
   154
where
55466
786edc984c98 merged 'Option.map' and 'Option.map_option'
blanchet
parents: 55416
diff changeset
   155
  "those xq = map_option lazy_sequence_of_list (List.those (list_of_lazy_sequence xq))"
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   156
  
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   157
function iterate_upto :: "(natural \<Rightarrow> 'a) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> 'a lazy_sequence"
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   158
where
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   159
  "iterate_upto f n m =
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   160
    Lazy_Sequence (\<lambda>_. if n > m then None else Some (f n, iterate_upto f (n + 1) m))"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   161
  by pat_completeness auto
36049
0ce5b7a5c2fd adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents: 36030
diff changeset
   162
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   163
termination by (relation "measure (\<lambda>(f, n, m). nat_of_natural (m + 1 - n))")
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   164
  (auto simp add: less_natural_def)
36049
0ce5b7a5c2fd adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents: 36030
diff changeset
   165
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   166
definition not_seq :: "unit lazy_sequence \<Rightarrow> unit lazy_sequence"
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   167
where
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   168
  "not_seq xq = (case yield xq of
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   169
    None \<Rightarrow> single ()
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   170
  | Some ((), xq) \<Rightarrow> empty)"
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   171
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   172
  
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   173
subsection {* Code setup *}
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   174
36533
f8df589ca2a5 dropped unnecessary ML code
haftmann
parents: 36516
diff changeset
   175
code_reflect Lazy_Sequence
f8df589ca2a5 dropped unnecessary ML code
haftmann
parents: 36516
diff changeset
   176
  datatypes lazy_sequence = Lazy_Sequence
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   177
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   178
ML {*
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   179
signature LAZY_SEQUENCE =
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   180
sig
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   181
  datatype 'a lazy_sequence = Lazy_Sequence of (unit -> ('a * 'a Lazy_Sequence.lazy_sequence) option)
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   182
  val map: ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   183
  val yield: 'a lazy_sequence -> ('a * 'a lazy_sequence) option
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   184
  val yieldn: int -> 'a lazy_sequence -> 'a list * 'a lazy_sequence
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   185
end;
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   186
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   187
structure Lazy_Sequence : LAZY_SEQUENCE =
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   188
struct
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   189
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   190
datatype lazy_sequence = datatype Lazy_Sequence.lazy_sequence;
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   191
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   192
fun map f = @{code Lazy_Sequence.map} f;
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   193
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   194
fun yield P = @{code Lazy_Sequence.yield} P;
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   195
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   196
fun yieldn k = Predicate.anamorph yield k;
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   197
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   198
end;
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   199
*}
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   200
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   201
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   202
subsection {* Generator Sequences *}
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   203
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   204
subsubsection {* General lazy sequence operation *}
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   205
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   206
definition product :: "'a lazy_sequence \<Rightarrow> 'b lazy_sequence \<Rightarrow> ('a \<times> 'b) lazy_sequence"
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   207
where
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   208
  "product s1 s2 = bind s1 (\<lambda>a. bind s2 (\<lambda>b. single (a, b)))"
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   209
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   210
40056
0bee30e3a4ad Changed section title to please LaTeX.
hoelzl
parents: 40051
diff changeset
   211
subsubsection {* Small lazy typeclasses *}
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   212
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   213
class small_lazy =
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   214
  fixes small_lazy :: "natural \<Rightarrow> 'a lazy_sequence"
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   215
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   216
instantiation unit :: small_lazy
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   217
begin
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   218
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   219
definition "small_lazy d = single ()"
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   220
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   221
instance ..
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   222
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   223
end
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   224
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   225
instantiation int :: small_lazy
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   226
begin
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   227
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   228
text {* maybe optimise this expression -> append (single x) xs == cons x xs 
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   229
Performance difference? *}
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   230
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   231
function small_lazy' :: "int \<Rightarrow> int \<Rightarrow> int lazy_sequence"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   232
where
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   233
  "small_lazy' d i = (if d < i then empty
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   234
    else append (single i) (small_lazy' d (i + 1)))"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   235
    by pat_completeness auto
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   236
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   237
termination 
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   238
  by (relation "measure (%(d, i). nat (d + 1 - i))") auto
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   239
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   240
definition
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   241
  "small_lazy d = small_lazy' (int (nat_of_natural d)) (- (int (nat_of_natural d)))"
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   242
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   243
instance ..
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   244
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   245
end
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   246
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   247
instantiation prod :: (small_lazy, small_lazy) small_lazy
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   248
begin
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   249
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   250
definition
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   251
  "small_lazy d = product (small_lazy d) (small_lazy d)"
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   252
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   253
instance ..
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   254
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   255
end
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   256
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   257
instantiation list :: (small_lazy) small_lazy
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   258
begin
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   259
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   260
fun small_lazy_list :: "natural \<Rightarrow> 'a list lazy_sequence"
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   261
where
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   262
  "small_lazy_list d = append (single [])
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   263
    (if d > 0 then bind (product (small_lazy (d - 1))
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   264
      (small_lazy (d - 1))) (\<lambda>(x, xs). single (x # xs)) else empty)"
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   265
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   266
instance ..
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   267
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   268
end
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   269
36902
c6bae4456741 use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
huffman
parents: 36533
diff changeset
   270
subsection {* With Hit Bound Value *}
36030
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   271
text {* assuming in negative context *}
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   272
42163
392fd6c4669c renewing specifications in HOL: replacing types by type_synonym
bulwahn
parents: 40056
diff changeset
   273
type_synonym 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
36030
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   274
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   275
definition hit_bound :: "'a hit_bound_lazy_sequence"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   276
where
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   277
  "hit_bound = Lazy_Sequence (\<lambda>_. Some (None, empty))"
36030
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   278
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   279
lemma list_of_lazy_sequence_hit_bound [simp]:
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   280
  "list_of_lazy_sequence hit_bound = [None]"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   281
  by (simp add: hit_bound_def)
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   282
  
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   283
definition hb_single :: "'a \<Rightarrow> 'a hit_bound_lazy_sequence"
36030
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   284
where
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   285
  "hb_single x = Lazy_Sequence (\<lambda>_. Some (Some x, empty))"
36030
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   286
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   287
definition hb_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a hit_bound_lazy_sequence \<Rightarrow> 'b hit_bound_lazy_sequence"
36030
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   288
where
55466
786edc984c98 merged 'Option.map' and 'Option.map_option'
blanchet
parents: 55416
diff changeset
   289
  "hb_map f xq = map (map_option f) xq"
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   290
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   291
lemma hb_map_code [code]:
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   292
  "hb_map f xq =
55466
786edc984c98 merged 'Option.map' and 'Option.map_option'
blanchet
parents: 55416
diff changeset
   293
    Lazy_Sequence (\<lambda>_. map_option (\<lambda>(x, xq'). (map_option f x, hb_map f xq')) (yield xq))"
786edc984c98 merged 'Option.map' and 'Option.map_option'
blanchet
parents: 55416
diff changeset
   294
  using map_code [of "map_option f" xq] by (simp add: hb_map_def)
36030
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   295
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   296
definition hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence \<Rightarrow> 'a hit_bound_lazy_sequence"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   297
where
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   298
  "hb_flat xqq = lazy_sequence_of_list (concat
55466
786edc984c98 merged 'Option.map' and 'Option.map_option'
blanchet
parents: 55416
diff changeset
   299
    (List.map ((\<lambda>x. case x of None \<Rightarrow> [None] | Some xs \<Rightarrow> xs) \<circ> map_option list_of_lazy_sequence) (list_of_lazy_sequence xqq)))"
36030
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   300
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   301
lemma list_of_lazy_sequence_hb_flat [simp]:
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   302
  "list_of_lazy_sequence (hb_flat xqq) =
55466
786edc984c98 merged 'Option.map' and 'Option.map_option'
blanchet
parents: 55416
diff changeset
   303
    concat (List.map ((\<lambda>x. case x of None \<Rightarrow> [None] | Some xs \<Rightarrow> xs) \<circ> map_option list_of_lazy_sequence) (list_of_lazy_sequence xqq))"
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   304
  by (simp add: hb_flat_def)
36030
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   305
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   306
lemma hb_flat_code [code]:
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   307
  "hb_flat xqq = Lazy_Sequence (\<lambda>_. case yield xqq of
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   308
    None \<Rightarrow> None
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   309
  | Some (xq, xqq') \<Rightarrow> yield
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   310
     (append (case xq of None \<Rightarrow> hit_bound | Some xq \<Rightarrow> xq) (hb_flat xqq')))"
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   311
  by (simp add: lazy_sequence_eq_iff split: list.splits option.splits)
36030
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   312
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   313
definition hb_bind :: "'a hit_bound_lazy_sequence \<Rightarrow> ('a \<Rightarrow> 'b hit_bound_lazy_sequence) \<Rightarrow> 'b hit_bound_lazy_sequence"
36030
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   314
where
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   315
  "hb_bind xq f = hb_flat (hb_map f xq)"
36030
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   316
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   317
definition hb_if_seq :: "bool \<Rightarrow> unit hit_bound_lazy_sequence"
36030
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   318
where
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   319
  "hb_if_seq b = (if b then hb_single () else empty)"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   320
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   321
definition hb_not_seq :: "unit hit_bound_lazy_sequence \<Rightarrow> unit lazy_sequence"
36030
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   322
where
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   323
  "hb_not_seq xq = (case yield xq of
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   324
    None \<Rightarrow> single ()
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   325
  | Some (x, xq) \<Rightarrow> empty)"
36030
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   326
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   327
hide_const (open) yield empty single append flat map bind
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   328
  if_seq those iterate_upto not_seq product
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   329
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   330
hide_fact (open) yield_def empty_def single_def append_def flat_def map_def bind_def
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
   331
  if_seq_def those_def not_seq_def product_def 
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   332
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   333
end