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