src/HOL/Lazy_Sequence.thy
author hoelzl
Mon, 03 Dec 2012 18:19:08 +0100
changeset 50328 25b1e8686ce0
parent 50055 94041d602ecb
child 51126 df86080de4cb
permissions -rw-r--r--
tuned proof
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
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
     2
(* 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
     3
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
     4
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
     5
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
     6
theory Lazy_Sequence
50055
94041d602ecb tuned import order
haftmann
parents: 45214
diff changeset
     7
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
     8
begin
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
     9
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    10
datatype 'a lazy_sequence = Empty | Insert 'a "'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
    11
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    12
definition Lazy_Sequence :: "(unit => ('a * 'a lazy_sequence) option) => '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
    13
where
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    14
  "Lazy_Sequence f = (case f () of None => Empty | Some (x, xq) => Insert x xq)"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    15
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    16
code_datatype Lazy_Sequence 
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    17
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    18
primrec yield :: "'a lazy_sequence => ('a * 'a lazy_sequence) option"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    19
where
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    20
  "yield Empty = None"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    21
| "yield (Insert x xq) = Some (x, xq)"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    22
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    23
lemma [simp]: "yield xq = Some (x, xq') ==> size xq' < size xq"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    24
by (cases xq) auto
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    25
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    26
lemma yield_Seq [code]:
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    27
  "yield (Lazy_Sequence f) = f ()"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    28
unfolding Lazy_Sequence_def by (cases "f ()") auto
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    29
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    30
lemma Seq_yield:
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    31
  "Lazy_Sequence (%u. yield f) = f"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    32
unfolding Lazy_Sequence_def by (cases f) auto
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    33
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    34
lemma lazy_sequence_size_code [code]:
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    35
  "lazy_sequence_size s xq = (case yield xq of None => 0 | Some (x, xq') => s x + lazy_sequence_size s xq' + 1)"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    36
by (cases xq) auto
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    37
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    38
lemma size_code [code]:
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    39
  "size xq = (case yield xq of None => 0 | Some (x, xq') => size xq' + 1)"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    40
by (cases xq) auto
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    41
38857
97775f3e8722 renamed class/constant eq to equal; tuned some instantiations
haftmann
parents: 36902
diff changeset
    42
lemma [code]: "HOL.equal xq yq = (case (yield xq, yield yq) of
97775f3e8722 renamed class/constant eq to equal; tuned some instantiations
haftmann
parents: 36902
diff changeset
    43
  (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.equal x y) \<and> (HOL.equal xq yq) | _ => False)"
97775f3e8722 renamed class/constant eq to equal; tuned some instantiations
haftmann
parents: 36902
diff changeset
    44
apply (cases xq) apply (cases yq) apply (auto simp add: equal_eq) 
97775f3e8722 renamed class/constant eq to equal; tuned some instantiations
haftmann
parents: 36902
diff changeset
    45
apply (cases yq) apply (auto simp add: equal_eq) done
97775f3e8722 renamed class/constant eq to equal; tuned some instantiations
haftmann
parents: 36902
diff changeset
    46
97775f3e8722 renamed class/constant eq to equal; tuned some instantiations
haftmann
parents: 36902
diff changeset
    47
lemma [code nbe]:
97775f3e8722 renamed class/constant eq to equal; tuned some instantiations
haftmann
parents: 36902
diff changeset
    48
  "HOL.equal (x :: 'a lazy_sequence) x \<longleftrightarrow> True"
97775f3e8722 renamed class/constant eq to equal; tuned some instantiations
haftmann
parents: 36902
diff changeset
    49
  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
    50
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    51
lemma seq_case [code]:
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    52
  "lazy_sequence_case f g xq = (case (yield xq) of None => f | Some (x, xq') => g x xq')"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    53
by (cases xq) auto
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    54
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    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'))"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    56
by (cases xq) auto
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    57
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    58
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
    59
where
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    60
  [code]: "empty = Lazy_Sequence (%u. None)"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    61
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    62
definition single :: "'a => '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
    63
where
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    64
  [code]: "single x = Lazy_Sequence (%u. Some (x, empty))"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    65
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    66
primrec append :: "'a lazy_sequence => 'a lazy_sequence => '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
    67
where
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    68
  "append Empty yq = yq"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    69
| "append (Insert x xq) yq = Insert x (append xq yq)"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    70
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    71
lemma [code]:
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    72
  "append xq yq = Lazy_Sequence (%u. case yield xq of
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    73
     None => yield yq
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    74
  | Some (x, xq') => Some (x, append xq' yq))"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    75
unfolding Lazy_Sequence_def
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    76
apply (cases "xq")
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    77
apply auto
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    78
apply (cases "yq")
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    79
apply auto
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    80
done
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    81
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    82
primrec flat :: "'a lazy_sequence lazy_sequence => '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
    83
where
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    84
  "flat Empty = Empty"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    85
| "flat (Insert xq xqq) = append xq (flat xqq)"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    86
 
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    87
lemma [code]:
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    88
  "flat xqq = Lazy_Sequence (%u. case yield xqq of
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    89
    None => None
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    90
  | Some (xq, xqq') => yield (append xq (flat xqq')))"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    91
apply (cases "xqq")
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    92
apply (auto simp add: Seq_yield)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    93
unfolding Lazy_Sequence_def
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    94
by auto
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    95
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    96
primrec map :: "('a => 'b) => 'a lazy_sequence => 'b lazy_sequence"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    97
where
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    98
  "map f Empty = Empty"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    99
| "map f (Insert x xq) = Insert (f x) (map f xq)"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   100
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   101
lemma [code]:
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   102
  "map f xq = Lazy_Sequence (%u. Option.map (%(x, xq'). (f x, map f xq')) (yield xq))"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   103
apply (cases xq)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   104
apply (auto simp add: Seq_yield)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   105
unfolding Lazy_Sequence_def
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   106
apply auto
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   107
done
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   108
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   109
definition bind :: "'a lazy_sequence => ('a => 'b lazy_sequence) => 'b lazy_sequence"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   110
where
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   111
  [code]: "bind xq f = flat (map f xq)"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   112
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   113
definition if_seq :: "bool => unit lazy_sequence"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   114
where
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   115
  "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
   116
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
   117
function iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a Lazy_Sequence.lazy_sequence"
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
   118
where
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
   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))"
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
   120
by pat_completeness auto
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
   121
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
   122
termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
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
   123
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   124
definition not_seq :: "unit lazy_sequence => unit lazy_sequence"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   125
where
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   126
  "not_seq xq = (case yield xq of None => single () | Some ((), xq) => empty)"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   127
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   128
subsection {* Code setup *}
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   129
36533
f8df589ca2a5 dropped unnecessary ML code
haftmann
parents: 36516
diff changeset
   130
fun anamorph :: "('a \<Rightarrow> ('b \<times> 'a) option) \<Rightarrow> code_numeral \<Rightarrow> 'a \<Rightarrow> 'b list \<times> 'a" where
f8df589ca2a5 dropped unnecessary ML code
haftmann
parents: 36516
diff changeset
   131
  "anamorph f k x = (if k = 0 then ([], x)
f8df589ca2a5 dropped unnecessary ML code
haftmann
parents: 36516
diff changeset
   132
    else case f x of None \<Rightarrow> ([], x) | Some (v, y) \<Rightarrow>
f8df589ca2a5 dropped unnecessary ML code
haftmann
parents: 36516
diff changeset
   133
      let (vs, z) = anamorph f (k - 1) y
f8df589ca2a5 dropped unnecessary ML code
haftmann
parents: 36516
diff changeset
   134
    in (v # vs, z))"
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   135
36533
f8df589ca2a5 dropped unnecessary ML code
haftmann
parents: 36516
diff changeset
   136
definition yieldn :: "code_numeral \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'a list \<times> 'a lazy_sequence" where
f8df589ca2a5 dropped unnecessary ML code
haftmann
parents: 36516
diff changeset
   137
  "yieldn = anamorph yield"
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   138
36533
f8df589ca2a5 dropped unnecessary ML code
haftmann
parents: 36516
diff changeset
   139
code_reflect Lazy_Sequence
f8df589ca2a5 dropped unnecessary ML code
haftmann
parents: 36516
diff changeset
   140
  datatypes lazy_sequence = Lazy_Sequence
f8df589ca2a5 dropped unnecessary ML code
haftmann
parents: 36516
diff changeset
   141
  functions map yield yieldn
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   142
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   143
subsection {* Generator Sequences *}
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   144
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   145
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   146
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
   147
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   148
definition product :: "'a Lazy_Sequence.lazy_sequence \<Rightarrow> 'b Lazy_Sequence.lazy_sequence \<Rightarrow> ('a * 'b) Lazy_Sequence.lazy_sequence"
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   149
where
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   150
  "product s1 s2 = Lazy_Sequence.bind s1 (%a. Lazy_Sequence.bind s2 (%b. Lazy_Sequence.single (a, b)))"
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   151
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   152
40056
0bee30e3a4ad Changed section title to please LaTeX.
hoelzl
parents: 40051
diff changeset
   153
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
   154
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   155
class small_lazy =
45214
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 42163
diff changeset
   156
  fixes small_lazy :: "code_numeral \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   157
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   158
instantiation unit :: small_lazy
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   159
begin
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   160
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   161
definition "small_lazy d = Lazy_Sequence.single ()"
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   162
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   163
instance ..
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   164
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   165
end
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   166
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   167
instantiation int :: small_lazy
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   168
begin
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   169
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   170
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
   171
Performance difference? *}
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   172
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   173
function small_lazy' :: "int => int => int Lazy_Sequence.lazy_sequence"
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   174
where "small_lazy' d i = (if d < i then Lazy_Sequence.empty else
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   175
  Lazy_Sequence.append (Lazy_Sequence.single i) (small_lazy' d (i + 1)))"
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   176
by pat_completeness auto
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   177
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   178
termination 
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   179
  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
   180
45214
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 42163
diff changeset
   181
definition "small_lazy d = small_lazy' (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   182
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   183
instance ..
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   184
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   185
end
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   186
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   187
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
   188
begin
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   189
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   190
definition
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   191
  "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
   192
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   193
instance ..
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   194
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   195
end
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   196
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   197
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
   198
begin
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   199
45214
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 42163
diff changeset
   200
fun small_lazy_list :: "code_numeral => 'a list Lazy_Sequence.lazy_sequence"
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   201
where
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   202
  "small_lazy_list d = Lazy_Sequence.append (Lazy_Sequence.single []) (if d > 0 then Lazy_Sequence.bind (product (small_lazy (d - 1)) (small_lazy (d - 1))) (%(x, xs). Lazy_Sequence.single (x # xs)) else Lazy_Sequence.empty)"
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
instance ..
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   205
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   206
end
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   207
36902
c6bae4456741 use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
huffman
parents: 36533
diff changeset
   208
subsection {* With Hit Bound Value *}
36030
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   209
text {* assuming in negative context *}
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   210
42163
392fd6c4669c renewing specifications in HOL: replacing types by type_synonym
bulwahn
parents: 40056
diff changeset
   211
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
   212
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   213
definition hit_bound :: "'a hit_bound_lazy_sequence"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   214
where
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   215
  [code]: "hit_bound = Lazy_Sequence (%u. Some (None, empty))"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   216
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   217
definition hb_single :: "'a => 'a hit_bound_lazy_sequence"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   218
where
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   219
  [code]: "hb_single x = Lazy_Sequence (%u. Some (Some x, empty))"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   220
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   221
primrec hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence => 'a hit_bound_lazy_sequence"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   222
where
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   223
  "hb_flat Empty = Empty"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   224
| "hb_flat (Insert xq xqq) = append (case xq of None => hit_bound | Some xq => xq) (hb_flat xqq)"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   225
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   226
lemma [code]:
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   227
  "hb_flat xqq = Lazy_Sequence (%u. case yield xqq of
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   228
    None => None
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   229
  | Some (xq, xqq') => yield (append (case xq of None => hit_bound | Some xq => xq) (hb_flat xqq')))"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   230
apply (cases "xqq")
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   231
apply (auto simp add: Seq_yield)
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   232
unfolding Lazy_Sequence_def
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   233
by auto
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   234
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   235
primrec hb_map :: "('a => 'b) => 'a hit_bound_lazy_sequence => 'b hit_bound_lazy_sequence"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   236
where
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   237
  "hb_map f Empty = Empty"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   238
| "hb_map f (Insert x xq) = Insert (Option.map f x) (hb_map f xq)"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   239
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   240
lemma [code]:
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   241
  "hb_map f xq = Lazy_Sequence (%u. Option.map (%(x, xq'). (Option.map f x, hb_map f xq')) (yield xq))"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   242
apply (cases xq)
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   243
apply (auto simp add: Seq_yield)
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   244
unfolding Lazy_Sequence_def
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   245
apply auto
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   246
done
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   247
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   248
definition hb_bind :: "'a hit_bound_lazy_sequence => ('a => 'b hit_bound_lazy_sequence) => 'b hit_bound_lazy_sequence"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   249
where
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   250
  [code]: "hb_bind xq f = hb_flat (hb_map f xq)"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   251
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   252
definition hb_if_seq :: "bool => unit hit_bound_lazy_sequence"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   253
where
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   254
  "hb_if_seq b = (if b then hb_single () else empty)"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   255
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   256
definition hb_not_seq :: "unit hit_bound_lazy_sequence => unit lazy_sequence"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   257
where
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   258
  "hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   259
36176
3fe7e97ccca8 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents: 36049
diff changeset
   260
hide_type (open) lazy_sequence
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   261
hide_const (open) Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   262
  iterate_upto not_seq product
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   263
  
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   264
hide_fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 38857
diff changeset
   265
  iterate_upto.simps product_def if_seq_def not_seq_def
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   266
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   267
end