src/HOL/Lazy_Sequence.thy
author bulwahn
Mon, 29 Mar 2010 17:30:49 +0200
changeset 36030 1cd962a0b1a6
parent 36024 c1ce2f60b0f2
child 36049 0ce5b7a5c2fd
permissions -rw-r--r--
adding Lazy_Sequences with explicit depth-bound
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
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
     7
imports List Code_Numeral
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
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    42
lemma [code]: "eq_class.eq xq yq = (case (yield xq, yield yq) of
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    43
  (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.eq x y) \<and> (eq_class.eq xq yq) | _ => False)"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    44
apply (cases xq) apply (cases yq) apply (auto simp add: eq_class.eq_equals) 
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    45
apply (cases yq) apply (auto simp add: eq_class.eq_equals) done
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    46
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    47
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
    48
  "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
    49
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
    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 [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
    52
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
    53
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    54
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
    55
where
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    56
  [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
    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 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
    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]: "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
    61
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    62
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
    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
  "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
    65
| "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
    66
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    67
lemma [code]:
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    68
  "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
    69
     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
    70
  | 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
    71
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
    72
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
    73
apply auto
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    74
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
    75
apply auto
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    76
done
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    77
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    78
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
    79
where
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    80
  "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
    81
| "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
    82
 
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    83
lemma [code]:
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    84
  "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
    85
    None => None
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    86
  | 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
    87
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
    88
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
    89
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
    90
by auto
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    91
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    92
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
    93
where
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    94
  "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
    95
| "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
    96
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
    97
lemma [code]:
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 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
    99
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
   100
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
   101
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
   102
apply auto
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   103
done
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   104
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   105
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
   106
where
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   107
  [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
   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 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
   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
  "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
   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 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
   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
  "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
   116
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   117
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
   118
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   119
ML {*
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   120
signature LAZY_SEQUENCE =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   121
sig
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   122
  datatype 'a lazy_sequence = Lazy_Sequence of unit -> ('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
   123
  val 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
   124
  val yieldn : int -> 'a lazy_sequence -> ('a list * 'a lazy_sequence)
36020
3ee4c29ead7f adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck
bulwahn
parents: 34957
diff changeset
   125
  val map : ('a -> 'b) -> 'a lazy_sequence -> '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
   126
end;
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
structure Lazy_Sequence : LAZY_SEQUENCE =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   129
struct
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   130
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   131
@{code_datatype lazy_sequence = Lazy_Sequence}
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   132
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   133
val yield = @{code yield}
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   134
36024
c1ce2f60b0f2 removed yieldn in Lazy_Sequence and put in the ML structure; corrects behaviour of values command
bulwahn
parents: 36020
diff changeset
   135
fun anamorph f k x = (if k = 0 then ([], x)
c1ce2f60b0f2 removed yieldn in Lazy_Sequence and put in the ML structure; corrects behaviour of values command
bulwahn
parents: 36020
diff changeset
   136
  else case f x
c1ce2f60b0f2 removed yieldn in Lazy_Sequence and put in the ML structure; corrects behaviour of values command
bulwahn
parents: 36020
diff changeset
   137
   of NONE => ([], x)
c1ce2f60b0f2 removed yieldn in Lazy_Sequence and put in the ML structure; corrects behaviour of values command
bulwahn
parents: 36020
diff changeset
   138
    | SOME (v, y) => let
c1ce2f60b0f2 removed yieldn in Lazy_Sequence and put in the ML structure; corrects behaviour of values command
bulwahn
parents: 36020
diff changeset
   139
        val (vs, z) = anamorph f (k - 1) y
c1ce2f60b0f2 removed yieldn in Lazy_Sequence and put in the ML structure; corrects behaviour of values command
bulwahn
parents: 36020
diff changeset
   140
      in (v :: vs, z) end);
c1ce2f60b0f2 removed yieldn in Lazy_Sequence and put in the ML structure; corrects behaviour of values command
bulwahn
parents: 36020
diff changeset
   141
c1ce2f60b0f2 removed yieldn in Lazy_Sequence and put in the ML structure; corrects behaviour of values command
bulwahn
parents: 36020
diff changeset
   142
fun yieldn S = anamorph yield S;
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   143
36020
3ee4c29ead7f adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck
bulwahn
parents: 34957
diff changeset
   144
val map = @{code map}
3ee4c29ead7f adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck
bulwahn
parents: 34957
diff changeset
   145
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   146
end;
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   147
*}
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   148
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   149
code_reserved Eval Lazy_Sequence
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   150
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   151
code_type lazy_sequence (Eval "_/ Lazy'_Sequence.lazy'_sequence")
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   152
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   153
code_const Lazy_Sequence (Eval "Lazy'_Sequence.Lazy'_Sequence")
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   154
36030
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   155
section {* With Hit Bound Value *}
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   156
text {* assuming in negative context *}
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   157
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   158
types 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   159
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   160
definition hit_bound :: "'a hit_bound_lazy_sequence"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   161
where
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   162
  [code]: "hit_bound = Lazy_Sequence (%u. Some (None, empty))"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   163
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   164
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   165
definition hb_single :: "'a => 'a hit_bound_lazy_sequence"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   166
where
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   167
  [code]: "hb_single x = Lazy_Sequence (%u. Some (Some x, empty))"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   168
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   169
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
   170
where
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   171
  "hb_flat Empty = Empty"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   172
| "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
   173
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   174
lemma [code]:
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   175
  "hb_flat xqq = Lazy_Sequence (%u. case yield xqq of
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   176
    None => None
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   177
  | 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
   178
apply (cases "xqq")
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   179
apply (auto simp add: Seq_yield)
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   180
unfolding Lazy_Sequence_def
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   181
by auto
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   182
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   183
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
   184
where
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   185
  "hb_map f Empty = Empty"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   186
| "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
   187
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   188
lemma [code]:
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   189
  "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
   190
apply (cases xq)
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   191
apply (auto simp add: Seq_yield)
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   192
unfolding Lazy_Sequence_def
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   193
apply auto
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   194
done
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   195
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   196
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
   197
where
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   198
  [code]: "hb_bind xq f = hb_flat (hb_map f xq)"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   199
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   200
definition hb_if_seq :: "bool => unit hit_bound_lazy_sequence"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   201
where
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   202
  "hb_if_seq b = (if b then hb_single () else empty)"
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   203
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   204
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
   205
where
1cd962a0b1a6 adding Lazy_Sequences with explicit depth-bound
bulwahn
parents: 36024
diff changeset
   206
  "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
   207
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   208
hide (open) type lazy_sequence
36024
c1ce2f60b0f2 removed yieldn in Lazy_Sequence and put in the ML structure; corrects behaviour of values command
bulwahn
parents: 36020
diff changeset
   209
hide (open) const Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq not_seq
c1ce2f60b0f2 removed yieldn in Lazy_Sequence and put in the ML structure; corrects behaviour of values command
bulwahn
parents: 36020
diff changeset
   210
hide fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_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
   211
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff changeset
   212
end