src/HOL/Limited_Sequence.thy
author wenzelm
Tue Oct 10 19:23:03 2017 +0200 (23 months ago)
changeset 66831 29ea2b900a05
parent 60758 d8d85a8172b5
child 67091 1393c2340eec
permissions -rw-r--r--
tuned: each session has at most one defining entry;
bulwahn@34948
     1
bulwahn@34948
     2
(* Author: Lukas Bulwahn, TU Muenchen *)
bulwahn@34948
     3
wenzelm@60758
     4
section \<open>Depth-Limited Sequences with failure element\<close>
bulwahn@34948
     5
haftmann@51126
     6
theory Limited_Sequence
haftmann@50055
     7
imports Lazy_Sequence
bulwahn@34948
     8
begin
bulwahn@34948
     9
wenzelm@60758
    10
subsection \<open>Depth-Limited Sequence\<close>
haftmann@51126
    11
haftmann@51143
    12
type_synonym 'a dseq = "natural \<Rightarrow> bool \<Rightarrow> 'a lazy_sequence option"
bulwahn@34948
    13
bulwahn@34948
    14
definition empty :: "'a dseq"
bulwahn@34948
    15
where
haftmann@51126
    16
  "empty = (\<lambda>_ _. Some Lazy_Sequence.empty)"
bulwahn@34948
    17
haftmann@51126
    18
definition single :: "'a \<Rightarrow> 'a dseq"
bulwahn@34948
    19
where
haftmann@51126
    20
  "single x = (\<lambda>_ _. Some (Lazy_Sequence.single x))"
bulwahn@34948
    21
haftmann@51143
    22
definition eval :: "'a dseq \<Rightarrow> natural \<Rightarrow> bool \<Rightarrow> 'a lazy_sequence option"
bulwahn@34948
    23
where
haftmann@51126
    24
  [simp]: "eval f i pol = f i pol"
bulwahn@34948
    25
haftmann@51143
    26
definition yield :: "'a dseq \<Rightarrow> natural \<Rightarrow> bool \<Rightarrow> ('a \<times> 'a dseq) option" 
bulwahn@34948
    27
where
haftmann@51126
    28
  "yield f i pol = (case eval f i pol of
haftmann@51126
    29
    None \<Rightarrow> None
blanchet@55466
    30
  | Some s \<Rightarrow> (map_option \<circ> apsnd) (\<lambda>r _ _. Some r) (Lazy_Sequence.yield s))"
bulwahn@34948
    31
haftmann@51126
    32
definition map_seq :: "('a \<Rightarrow> 'b dseq) \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'b dseq"
haftmann@50092
    33
where
blanchet@55466
    34
  "map_seq f xq i pol = map_option Lazy_Sequence.flat
haftmann@51126
    35
    (Lazy_Sequence.those (Lazy_Sequence.map (\<lambda>x. f x i pol) xq))"
haftmann@50092
    36
haftmann@51126
    37
lemma map_seq_code [code]:
bulwahn@34948
    38
  "map_seq f xq i pol = (case Lazy_Sequence.yield xq of
haftmann@51126
    39
    None \<Rightarrow> Some Lazy_Sequence.empty
haftmann@51126
    40
  | Some (x, xq') \<Rightarrow> (case eval (f x) i pol of
haftmann@51126
    41
      None \<Rightarrow> None
haftmann@51126
    42
    | Some yq \<Rightarrow> (case map_seq f xq' i pol of
haftmann@51126
    43
        None \<Rightarrow> None
haftmann@51126
    44
      | Some zq \<Rightarrow> Some (Lazy_Sequence.append yq zq))))"
haftmann@51126
    45
  by (cases xq)
haftmann@51126
    46
    (auto simp add: map_seq_def Lazy_Sequence.those_def lazy_sequence_eq_iff split: list.splits option.splits)
bulwahn@34948
    47
haftmann@51126
    48
definition bind :: "'a dseq \<Rightarrow> ('a \<Rightarrow> 'b dseq) \<Rightarrow> 'b dseq"
bulwahn@34948
    49
where
haftmann@51126
    50
  "bind x f = (\<lambda>i pol. 
bulwahn@34948
    51
     if i = 0 then
bulwahn@34948
    52
       (if pol then Some Lazy_Sequence.empty else None)
bulwahn@34948
    53
     else
bulwahn@34948
    54
       (case x (i - 1) pol of
haftmann@51126
    55
         None \<Rightarrow> None
haftmann@51126
    56
       | Some xq \<Rightarrow> map_seq f xq i pol))"
bulwahn@34948
    57
haftmann@51126
    58
definition union :: "'a dseq \<Rightarrow> 'a dseq \<Rightarrow> 'a dseq"
bulwahn@34948
    59
where
haftmann@51126
    60
  "union x y = (\<lambda>i pol. case (x i pol, y i pol) of
haftmann@51126
    61
      (Some xq, Some yq) \<Rightarrow> Some (Lazy_Sequence.append xq yq)
haftmann@51126
    62
    | _ \<Rightarrow> None)"
bulwahn@34948
    63
haftmann@51126
    64
definition if_seq :: "bool \<Rightarrow> unit dseq"
bulwahn@34948
    65
where
bulwahn@34948
    66
  "if_seq b = (if b then single () else empty)"
bulwahn@34948
    67
haftmann@51126
    68
definition not_seq :: "unit dseq \<Rightarrow> unit dseq"
haftmann@51126
    69
where
haftmann@51126
    70
  "not_seq x = (\<lambda>i pol. case x i (\<not> pol) of
haftmann@51126
    71
    None \<Rightarrow> Some Lazy_Sequence.empty
haftmann@51126
    72
  | Some xq \<Rightarrow> (case Lazy_Sequence.yield xq of
haftmann@51126
    73
      None \<Rightarrow> Some (Lazy_Sequence.single ())
haftmann@51126
    74
    | Some _ \<Rightarrow> Some (Lazy_Sequence.empty)))"
haftmann@51126
    75
haftmann@51126
    76
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a dseq \<Rightarrow> 'b dseq"
haftmann@51126
    77
where
haftmann@51126
    78
  "map f g = (\<lambda>i pol. case g i pol of
haftmann@51126
    79
     None \<Rightarrow> None
haftmann@51126
    80
   | Some xq \<Rightarrow> Some (Lazy_Sequence.map f xq))"
haftmann@51126
    81
haftmann@51126
    82
wenzelm@60758
    83
subsection \<open>Positive Depth-Limited Sequence\<close>
haftmann@51126
    84
haftmann@51143
    85
type_synonym 'a pos_dseq = "natural \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
haftmann@51126
    86
haftmann@51126
    87
definition pos_empty :: "'a pos_dseq"
haftmann@51126
    88
where
haftmann@51126
    89
  "pos_empty = (\<lambda>i. Lazy_Sequence.empty)"
haftmann@51126
    90
haftmann@51126
    91
definition pos_single :: "'a \<Rightarrow> 'a pos_dseq"
haftmann@51126
    92
where
haftmann@51126
    93
  "pos_single x = (\<lambda>i. Lazy_Sequence.single x)"
haftmann@51126
    94
haftmann@51126
    95
definition pos_bind :: "'a pos_dseq \<Rightarrow> ('a \<Rightarrow> 'b pos_dseq) \<Rightarrow> 'b pos_dseq"
haftmann@51126
    96
where
haftmann@51126
    97
  "pos_bind x f = (\<lambda>i. Lazy_Sequence.bind (x i) (\<lambda>a. f a i))"
haftmann@51126
    98
haftmann@51126
    99
definition pos_decr_bind :: "'a pos_dseq \<Rightarrow> ('a \<Rightarrow> 'b pos_dseq) \<Rightarrow> 'b pos_dseq"
haftmann@51126
   100
where
haftmann@51126
   101
  "pos_decr_bind x f = (\<lambda>i. 
haftmann@51126
   102
     if i = 0 then
haftmann@51126
   103
       Lazy_Sequence.empty
haftmann@51126
   104
     else
haftmann@51126
   105
       Lazy_Sequence.bind (x (i - 1)) (\<lambda>a. f a i))"
haftmann@51126
   106
haftmann@51126
   107
definition pos_union :: "'a pos_dseq \<Rightarrow> 'a pos_dseq \<Rightarrow> 'a pos_dseq"
haftmann@51126
   108
where
haftmann@51126
   109
  "pos_union xq yq = (\<lambda>i. Lazy_Sequence.append (xq i) (yq i))"
haftmann@51126
   110
haftmann@51126
   111
definition pos_if_seq :: "bool \<Rightarrow> unit pos_dseq"
haftmann@51126
   112
where
haftmann@51126
   113
  "pos_if_seq b = (if b then pos_single () else pos_empty)"
haftmann@51126
   114
haftmann@51143
   115
definition pos_iterate_upto :: "(natural \<Rightarrow> 'a) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> 'a pos_dseq"
haftmann@51126
   116
where
haftmann@51126
   117
  "pos_iterate_upto f n m = (\<lambda>i. Lazy_Sequence.iterate_upto f n m)"
haftmann@51126
   118
 
haftmann@51126
   119
definition pos_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pos_dseq \<Rightarrow> 'b pos_dseq"
bulwahn@34948
   120
where
haftmann@51126
   121
  "pos_map f xq = (\<lambda>i. Lazy_Sequence.map f (xq i))"
haftmann@51126
   122
haftmann@51126
   123
wenzelm@60758
   124
subsection \<open>Negative Depth-Limited Sequence\<close>
haftmann@51126
   125
haftmann@51143
   126
type_synonym 'a neg_dseq = "natural \<Rightarrow> 'a Lazy_Sequence.hit_bound_lazy_sequence"
haftmann@51126
   127
haftmann@51126
   128
definition neg_empty :: "'a neg_dseq"
haftmann@51126
   129
where
haftmann@51126
   130
  "neg_empty = (\<lambda>i. Lazy_Sequence.empty)"
haftmann@51126
   131
haftmann@51126
   132
definition neg_single :: "'a \<Rightarrow> 'a neg_dseq"
haftmann@51126
   133
where
haftmann@51126
   134
  "neg_single x = (\<lambda>i. Lazy_Sequence.hb_single x)"
haftmann@51126
   135
haftmann@51126
   136
definition neg_bind :: "'a neg_dseq \<Rightarrow> ('a \<Rightarrow> 'b neg_dseq) \<Rightarrow> 'b neg_dseq"
haftmann@51126
   137
where
haftmann@51126
   138
  "neg_bind x f = (\<lambda>i. hb_bind (x i) (\<lambda>a. f a i))"
haftmann@51126
   139
haftmann@51126
   140
definition neg_decr_bind :: "'a neg_dseq \<Rightarrow> ('a \<Rightarrow> 'b neg_dseq) \<Rightarrow> 'b neg_dseq"
haftmann@51126
   141
where
haftmann@51126
   142
  "neg_decr_bind x f = (\<lambda>i. 
haftmann@51126
   143
     if i = 0 then
haftmann@51126
   144
       Lazy_Sequence.hit_bound
haftmann@51126
   145
     else
haftmann@51126
   146
       hb_bind (x (i - 1)) (\<lambda>a. f a i))"
bulwahn@34948
   147
haftmann@51126
   148
definition neg_union :: "'a neg_dseq \<Rightarrow> 'a neg_dseq \<Rightarrow> 'a neg_dseq"
haftmann@51126
   149
where
haftmann@51126
   150
  "neg_union x y = (\<lambda>i. Lazy_Sequence.append (x i) (y i))"
haftmann@51126
   151
haftmann@51126
   152
definition neg_if_seq :: "bool \<Rightarrow> unit neg_dseq"
haftmann@51126
   153
where
haftmann@51126
   154
  "neg_if_seq b = (if b then neg_single () else neg_empty)"
haftmann@51126
   155
haftmann@51126
   156
definition neg_iterate_upto 
haftmann@51126
   157
where
haftmann@51126
   158
  "neg_iterate_upto f n m = (\<lambda>i. Lazy_Sequence.iterate_upto (\<lambda>i. Some (f i)) n m)"
haftmann@51126
   159
haftmann@51126
   160
definition neg_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a neg_dseq \<Rightarrow> 'b neg_dseq"
bulwahn@34948
   161
where
haftmann@51126
   162
  "neg_map f xq = (\<lambda>i. Lazy_Sequence.hb_map f (xq i))"
haftmann@51126
   163
haftmann@51126
   164
wenzelm@60758
   165
subsection \<open>Negation\<close>
haftmann@51126
   166
haftmann@51126
   167
definition pos_not_seq :: "unit neg_dseq \<Rightarrow> unit pos_dseq"
haftmann@51126
   168
where
haftmann@51126
   169
  "pos_not_seq xq = (\<lambda>i. Lazy_Sequence.hb_not_seq (xq (3 * i)))"
haftmann@51126
   170
haftmann@51126
   171
definition neg_not_seq :: "unit pos_dseq \<Rightarrow> unit neg_dseq"
haftmann@51126
   172
where
haftmann@51126
   173
  "neg_not_seq x = (\<lambda>i. case Lazy_Sequence.yield (x i) of
haftmann@51126
   174
    None => Lazy_Sequence.hb_single ()
haftmann@51126
   175
  | Some ((), xq) => Lazy_Sequence.empty)"
haftmann@51126
   176
bulwahn@34948
   177
wenzelm@60758
   178
ML \<open>
haftmann@51126
   179
signature LIMITED_SEQUENCE =
bulwahn@34948
   180
sig
haftmann@51143
   181
  type 'a dseq = Code_Numeral.natural -> bool -> 'a Lazy_Sequence.lazy_sequence option
haftmann@51126
   182
  val map : ('a -> 'b) -> 'a dseq -> 'b dseq
haftmann@51143
   183
  val yield : 'a dseq -> Code_Numeral.natural -> bool -> ('a * 'a dseq) option
haftmann@51143
   184
  val yieldn : int -> 'a dseq -> Code_Numeral.natural -> bool -> 'a list * 'a dseq
bulwahn@34948
   185
end;
bulwahn@34948
   186
haftmann@51126
   187
structure Limited_Sequence : LIMITED_SEQUENCE =
bulwahn@34948
   188
struct
bulwahn@34948
   189
haftmann@51143
   190
type 'a dseq = Code_Numeral.natural -> bool -> 'a Lazy_Sequence.lazy_sequence option
bulwahn@34948
   191
haftmann@51126
   192
fun map f = @{code Limited_Sequence.map} f;
haftmann@51126
   193
haftmann@51126
   194
fun yield f = @{code Limited_Sequence.yield} f;
haftmann@51126
   195
haftmann@51126
   196
fun yieldn n f i pol = (case f i pol of
haftmann@51126
   197
    NONE => ([], fn _ => fn _ => NONE)
haftmann@51126
   198
  | SOME s => let val (xs, s') = Lazy_Sequence.yieldn n s in (xs, fn _ => fn _ => SOME s') end);
bulwahn@34948
   199
bulwahn@34948
   200
end;
wenzelm@60758
   201
\<close>
bulwahn@34948
   202
haftmann@51126
   203
code_reserved Eval Limited_Sequence
haftmann@51126
   204
bulwahn@34948
   205
haftmann@51126
   206
hide_const (open) yield empty single eval map_seq bind union if_seq not_seq map
haftmann@51126
   207
  pos_empty pos_single pos_bind pos_decr_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map
haftmann@51126
   208
  neg_empty neg_single neg_bind neg_decr_bind neg_union neg_if_seq neg_iterate_upto neg_not_seq neg_map
haftmann@51126
   209
haftmann@51126
   210
hide_fact (open) yield_def empty_def single_def eval_def map_seq_def bind_def union_def
bulwahn@34953
   211
  if_seq_def not_seq_def map_def
haftmann@51126
   212
  pos_empty_def pos_single_def pos_bind_def pos_union_def pos_if_seq_def pos_iterate_upto_def pos_not_seq_def pos_map_def
haftmann@51126
   213
  neg_empty_def neg_single_def neg_bind_def neg_union_def neg_if_seq_def neg_iterate_upto_def neg_not_seq_def neg_map_def
bulwahn@34948
   214
bulwahn@34948
   215
end
haftmann@50092
   216