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