author  wenzelm 
Sat, 18 Jul 2015 22:58:50 +0200  
changeset 60758  d8d85a8172b5 
parent 58889  5b7a9633cfa8 
permissions  rwrr 
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 

60758  3 
section \<open>Lazy sequences\<close> 
34948
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 

60758  9 
subsection \<open>Type of lazy sequences\<close> 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

10 

58350
919149921e46
added 'extraction' plugins  this might help 'HOLProofs'
blanchet
parents:
58334
diff
changeset

11 
datatype (plugins only: code extraction) (dead 'a) lazy_sequence = 
919149921e46
added 'extraction' plugins  this might help 'HOLProofs'
blanchet
parents:
58334
diff
changeset

12 
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

13 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

14 
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

15 
where 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

16 
"list_of_lazy_sequence (lazy_sequence_of_list xs) = xs" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

17 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

18 
lemma lazy_sequence_of_list_of_lazy_sequence [simp]: 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

19 
"lazy_sequence_of_list (list_of_lazy_sequence xq) = xq" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

20 
by (cases xq) simp_all 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

21 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

22 
lemma lazy_sequence_eqI: 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

23 
"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

24 
by (cases xq, cases yq) simp 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

25 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

26 
lemma lazy_sequence_eq_iff: 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

27 
"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

28 
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

29 

55416  30 
lemma case_lazy_sequence [simp]: 
31 
"case_lazy_sequence f xq = f (list_of_lazy_sequence xq)" 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

32 
by (cases xq) auto 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

33 

55416  34 
lemma rec_lazy_sequence [simp]: 
35 
"rec_lazy_sequence f xq = f (list_of_lazy_sequence xq)" 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

36 
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

37 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

38 
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

39 
where 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

40 
"Lazy_Sequence f = lazy_sequence_of_list (case f () of 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

41 
None \<Rightarrow> [] 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

42 
 Some (x, xq) \<Rightarrow> x # list_of_lazy_sequence xq)" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

43 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

44 
code_datatype Lazy_Sequence 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

45 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

46 
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

47 
declare lazy_sequence.case [code del] 
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55466
diff
changeset

48 
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

49 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

50 
lemma list_of_Lazy_Sequence [simp]: 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

51 
"list_of_lazy_sequence (Lazy_Sequence f) = (case f () of 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

52 
None \<Rightarrow> [] 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

53 
 Some (x, xq) \<Rightarrow> x # list_of_lazy_sequence xq)" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

54 
by (simp add: Lazy_Sequence_def) 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

55 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

56 
definition yield :: "'a lazy_sequence \<Rightarrow> ('a \<times> 'a lazy_sequence) option" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

57 
where 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

58 
"yield xq = (case list_of_lazy_sequence xq of 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

59 
[] \<Rightarrow> None 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

60 
 x # xs \<Rightarrow> Some (x, lazy_sequence_of_list xs))" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

61 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

62 
lemma yield_Seq [simp, code]: 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

63 
"yield (Lazy_Sequence f) = f ()" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

64 
by (cases "f ()") (simp_all add: yield_def split_def) 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

65 

55413
a8e96847523c
adapted theories to '{case,rec}_{list,option}' names
blanchet
parents:
51143
diff
changeset

66 
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

67 
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

68 
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

69 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

70 
lemma equal_lazy_sequence_code [code]: 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

71 
"HOL.equal xq yq = (case (yield xq, yield yq) of 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

72 
(None, None) \<Rightarrow> True 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

73 
 (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

74 
 _ \<Rightarrow> False)" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

75 
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

76 

97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36902
diff
changeset

77 
lemma [code nbe]: 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36902
diff
changeset

78 
"HOL.equal (x :: 'a lazy_sequence) x \<longleftrightarrow> True" 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36902
diff
changeset

79 
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

80 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

81 
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

82 
where 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

83 
"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

84 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

85 
lemma list_of_lazy_sequence_empty [simp]: 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

86 
"list_of_lazy_sequence empty = []" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

87 
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

88 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

89 
lemma empty_code [code]: 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

90 
"empty = Lazy_Sequence (\<lambda>_. None)" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

91 
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

92 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

93 
definition single :: "'a \<Rightarrow> 'a lazy_sequence" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

94 
where 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

95 
"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

96 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

97 
lemma list_of_lazy_sequence_single [simp]: 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

98 
"list_of_lazy_sequence (single x) = [x]" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

99 
by (simp add: single_def) 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

100 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

101 
lemma single_code [code]: 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

102 
"single x = Lazy_Sequence (\<lambda>_. Some (x, empty))" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

103 
by (simp add: lazy_sequence_eq_iff) 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

104 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

105 
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

106 
where 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

107 
"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

108 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

109 
lemma list_of_lazy_sequence_append [simp]: 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

110 
"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

111 
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

112 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

113 
lemma append_code [code]: 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

114 
"append xq yq = Lazy_Sequence (\<lambda>_. case yield xq of 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

115 
None \<Rightarrow> yield yq 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

116 
 Some (x, xq') \<Rightarrow> Some (x, append xq' yq))" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

117 
by (simp_all add: lazy_sequence_eq_iff split: list.splits) 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

118 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

119 
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

120 
where 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

121 
"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

122 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

123 
lemma list_of_lazy_sequence_map [simp]: 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

124 
"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

125 
by (simp add: map_def) 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

126 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

127 
lemma map_code [code]: 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

128 
"map f xq = 
55466  129 
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

130 
by (simp_all add: lazy_sequence_eq_iff split: list.splits) 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

131 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

132 
definition flat :: "'a lazy_sequence lazy_sequence \<Rightarrow> 'a lazy_sequence" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

133 
where 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

134 
"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

135 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

136 
lemma list_of_lazy_sequence_flat [simp]: 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

137 
"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

138 
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

139 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

140 
lemma flat_code [code]: 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

141 
"flat xqq = Lazy_Sequence (\<lambda>_. case yield xqq of 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

142 
None \<Rightarrow> None 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

143 
 Some (xq, xqq') \<Rightarrow> yield (append xq (flat xqq')))" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

144 
by (simp add: lazy_sequence_eq_iff split: list.splits) 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

145 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

146 
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

147 
where 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

148 
"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

149 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

150 
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

151 
where 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

152 
"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

153 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

154 
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

155 
where 
55466  156 
"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

157 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

158 
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

159 
where 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

160 
"iterate_upto f n m = 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

161 
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

162 
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

163 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

164 
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

165 
(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

166 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

167 
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

168 
where 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

169 
"not_seq xq = (case yield xq of 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

170 
None \<Rightarrow> single () 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

171 
 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

172 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

173 

60758  174 
subsection \<open>Code setup\<close> 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

175 

36533  176 
code_reflect Lazy_Sequence 
177 
datatypes lazy_sequence = Lazy_Sequence 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

178 

60758  179 
ML \<open> 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

180 
signature LAZY_SEQUENCE = 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

181 
sig 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

182 
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

183 
val map: ('a > 'b) > 'a lazy_sequence > 'b lazy_sequence 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

184 
val yield: 'a lazy_sequence > ('a * 'a lazy_sequence) option 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

185 
val yieldn: int > 'a lazy_sequence > 'a list * 'a lazy_sequence 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

186 
end; 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

187 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

188 
structure Lazy_Sequence : LAZY_SEQUENCE = 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

189 
struct 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

190 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

191 
datatype lazy_sequence = datatype Lazy_Sequence.lazy_sequence; 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

192 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

193 
fun map f = @{code Lazy_Sequence.map} f; 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

194 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

195 
fun yield P = @{code Lazy_Sequence.yield} P; 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

196 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

197 
fun yieldn k = Predicate.anamorph yield k; 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

198 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

199 
end; 
60758  200 
\<close> 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

201 

34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

202 

60758  203 
subsection \<open>Generator Sequences\<close> 
40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

204 

60758  205 
subsubsection \<open>General lazy sequence operation\<close> 
40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

206 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

207 
definition product :: "'a lazy_sequence \<Rightarrow> 'b lazy_sequence \<Rightarrow> ('a \<times> 'b) lazy_sequence" 
40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

208 
where 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

209 
"product s1 s2 = bind s1 (\<lambda>a. bind s2 (\<lambda>b. single (a, b)))" 
40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

210 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

211 

60758  212 
subsubsection \<open>Small lazy typeclasses\<close> 
40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

213 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

214 
class small_lazy = 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

215 
fixes small_lazy :: "natural \<Rightarrow> 'a lazy_sequence" 
40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

216 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

217 
instantiation unit :: small_lazy 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

218 
begin 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

219 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

220 
definition "small_lazy d = single ()" 
40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

221 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

222 
instance .. 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

223 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

224 
end 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

225 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

226 
instantiation int :: small_lazy 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

227 
begin 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

228 

60758  229 
text \<open>maybe optimise this expression > append (single x) xs == cons x xs 
230 
Performance difference?\<close> 

40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

231 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

232 
function small_lazy' :: "int \<Rightarrow> int \<Rightarrow> int lazy_sequence" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

233 
where 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

234 
"small_lazy' d i = (if d < i then empty 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

235 
else append (single i) (small_lazy' d (i + 1)))" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

236 
by pat_completeness auto 
40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

237 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

238 
termination 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

239 
by (relation "measure (%(d, i). nat (d + 1  i))") auto 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

240 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

241 
definition 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

242 
"small_lazy d = small_lazy' (int (nat_of_natural d)) ( (int (nat_of_natural d)))" 
40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

243 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

244 
instance .. 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

245 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

246 
end 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

247 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

248 
instantiation prod :: (small_lazy, small_lazy) small_lazy 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

249 
begin 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

250 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

251 
definition 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

252 
"small_lazy d = product (small_lazy d) (small_lazy d)" 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

253 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

254 
instance .. 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

255 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

256 
end 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

257 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

258 
instantiation list :: (small_lazy) small_lazy 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

259 
begin 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

260 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

261 
fun small_lazy_list :: "natural \<Rightarrow> 'a list lazy_sequence" 
40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

262 
where 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

263 
"small_lazy_list d = append (single []) 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

264 
(if d > 0 then bind (product (small_lazy (d  1)) 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

265 
(small_lazy (d  1))) (\<lambda>(x, xs). single (x # xs)) else empty)" 
40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

266 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

267 
instance .. 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

268 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

269 
end 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

270 

60758  271 
subsection \<open>With Hit Bound Value\<close> 
272 
text \<open>assuming in negative context\<close> 

36030  273 

42163
392fd6c4669c
renewing specifications in HOL: replacing types by type_synonym
bulwahn
parents:
40056
diff
changeset

274 
type_synonym 'a hit_bound_lazy_sequence = "'a option lazy_sequence" 
36030  275 

276 
definition hit_bound :: "'a hit_bound_lazy_sequence" 

277 
where 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

278 
"hit_bound = Lazy_Sequence (\<lambda>_. Some (None, empty))" 
36030  279 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

280 
lemma list_of_lazy_sequence_hit_bound [simp]: 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

281 
"list_of_lazy_sequence hit_bound = [None]" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

282 
by (simp add: hit_bound_def) 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

283 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

284 
definition hb_single :: "'a \<Rightarrow> 'a hit_bound_lazy_sequence" 
36030  285 
where 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

286 
"hb_single x = Lazy_Sequence (\<lambda>_. Some (Some x, empty))" 
36030  287 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

288 
definition hb_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a hit_bound_lazy_sequence \<Rightarrow> 'b hit_bound_lazy_sequence" 
36030  289 
where 
55466  290 
"hb_map f xq = map (map_option f) xq" 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

291 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

292 
lemma hb_map_code [code]: 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

293 
"hb_map f xq = 
55466  294 
Lazy_Sequence (\<lambda>_. map_option (\<lambda>(x, xq'). (map_option f x, hb_map f xq')) (yield xq))" 
295 
using map_code [of "map_option f" xq] by (simp add: hb_map_def) 

36030  296 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

297 
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

298 
where 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

299 
"hb_flat xqq = lazy_sequence_of_list (concat 
55466  300 
(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  301 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

302 
lemma list_of_lazy_sequence_hb_flat [simp]: 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

303 
"list_of_lazy_sequence (hb_flat xqq) = 
55466  304 
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

305 
by (simp add: hb_flat_def) 
36030  306 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

307 
lemma hb_flat_code [code]: 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

308 
"hb_flat xqq = Lazy_Sequence (\<lambda>_. case yield xqq of 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

309 
None \<Rightarrow> None 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

310 
 Some (xq, xqq') \<Rightarrow> yield 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

311 
(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

312 
by (simp add: lazy_sequence_eq_iff split: list.splits option.splits) 
36030  313 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

314 
definition hb_bind :: "'a hit_bound_lazy_sequence \<Rightarrow> ('a \<Rightarrow> 'b hit_bound_lazy_sequence) \<Rightarrow> 'b hit_bound_lazy_sequence" 
36030  315 
where 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

316 
"hb_bind xq f = hb_flat (hb_map f xq)" 
36030  317 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

318 
definition hb_if_seq :: "bool \<Rightarrow> unit hit_bound_lazy_sequence" 
36030  319 
where 
320 
"hb_if_seq b = (if b then hb_single () else empty)" 

321 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

322 
definition hb_not_seq :: "unit hit_bound_lazy_sequence \<Rightarrow> unit lazy_sequence" 
36030  323 
where 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

324 
"hb_not_seq xq = (case yield xq of 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

325 
None \<Rightarrow> single () 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

326 
 Some (x, xq) \<Rightarrow> empty)" 
36030  327 

51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

328 
hide_const (open) yield empty single append flat map bind 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

329 
if_seq those iterate_upto not_seq product 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

330 

df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

331 
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

332 
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

333 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

334 
end 