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

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

2 
(* Author: Lukas Bulwahn, TU Muenchen *) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

3 

60758  4 
section \<open>Various kind of sequences inside the random monad\<close> 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

5 

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

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

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

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

9 

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

10 
type_synonym 'a random_dseq = "natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> ('a Limited_Sequence.dseq \<times> Random.seed)" 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

11 

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

12 
definition empty :: "'a random_dseq" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

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

14 
"empty = (%nrandom size. Pair (Limited_Sequence.empty))" 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

15 

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

16 
definition single :: "'a => 'a random_dseq" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

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

18 
"single x = (%nrandom size. Pair (Limited_Sequence.single x))" 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

19 

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

20 
definition bind :: "'a random_dseq => ('a \<Rightarrow> 'b random_dseq) \<Rightarrow> 'b random_dseq" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

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

22 
"bind R f = (\<lambda>nrandom size s. let 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

23 
(P, s') = R nrandom size s; 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

24 
(s1, s2) = Random.split_seed s' 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

25 
in (Limited_Sequence.bind P (%a. fst (f a nrandom size s1)), s2))" 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

26 

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

27 
definition union :: "'a random_dseq => 'a random_dseq => 'a random_dseq" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

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

29 
"union R1 R2 = (\<lambda>nrandom size s. let 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

30 
(S1, s') = R1 nrandom size s; (S2, s'') = R2 nrandom size s' 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

31 
in (Limited_Sequence.union S1 S2, s''))" 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

32 

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

33 
definition if_random_dseq :: "bool => unit random_dseq" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

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

35 
"if_random_dseq 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

36 

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

37 
definition not_random_dseq :: "unit random_dseq => unit random_dseq" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

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

39 
"not_random_dseq R = (\<lambda>nrandom size s. let 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

40 
(S, s') = R nrandom size s 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

41 
in (Limited_Sequence.not_seq S, s'))" 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

42 

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

43 
definition map :: "('a => 'b) => 'a random_dseq => 'b random_dseq" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

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

45 
"map f P = bind P (single o f)" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

46 

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

47 
fun Random :: "(natural \<Rightarrow> Random.seed \<Rightarrow> (('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)) \<Rightarrow> 'a random_dseq" 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

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

49 
"Random g nrandom = (%size. if nrandom <= 0 then (Pair Limited_Sequence.empty) else 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

50 
(scomp (g size) (%r. scomp (Random g (nrandom  1) size) (%rs. Pair (Limited_Sequence.union (Limited_Sequence.single (fst r)) rs)))))" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

51 

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

52 

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

53 
type_synonym 'a pos_random_dseq = "natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> 'a Limited_Sequence.pos_dseq" 
51126
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 pos_empty :: "'a pos_random_dseq" 
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 
"pos_empty = (%nrandom size seed. Limited_Sequence.pos_empty)" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

58 

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

59 
definition pos_single :: "'a => 'a pos_random_dseq" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

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

61 
"pos_single x = (%nrandom size seed. Limited_Sequence.pos_single x)" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

62 

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

63 
definition pos_bind :: "'a pos_random_dseq => ('a \<Rightarrow> 'b pos_random_dseq) \<Rightarrow> 'b pos_random_dseq" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

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

65 
"pos_bind R f = (\<lambda>nrandom size seed. Limited_Sequence.pos_bind (R nrandom size seed) (%a. f a nrandom size seed))" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

66 

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

67 
definition pos_decr_bind :: "'a pos_random_dseq => ('a \<Rightarrow> 'b pos_random_dseq) \<Rightarrow> 'b pos_random_dseq" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

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

69 
"pos_decr_bind R f = (\<lambda>nrandom size seed. Limited_Sequence.pos_decr_bind (R nrandom size seed) (%a. f a nrandom size seed))" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

70 

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

71 
definition pos_union :: "'a pos_random_dseq => 'a pos_random_dseq => 'a pos_random_dseq" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

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

73 
"pos_union R1 R2 = (\<lambda>nrandom size seed. Limited_Sequence.pos_union (R1 nrandom size seed) (R2 nrandom size seed))" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

74 

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

75 
definition pos_if_random_dseq :: "bool => unit pos_random_dseq" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

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

77 
"pos_if_random_dseq b = (if b then pos_single () else pos_empty)" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

78 

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

79 
definition pos_iterate_upto :: "(natural => 'a) => natural => natural => 'a pos_random_dseq" 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

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

81 
"pos_iterate_upto f n m = (\<lambda>nrandom size seed. Limited_Sequence.pos_iterate_upto f n m)" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

82 

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

83 
definition pos_map :: "('a => 'b) => 'a pos_random_dseq => 'b pos_random_dseq" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

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

85 
"pos_map f P = pos_bind P (pos_single o f)" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

86 

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

87 
fun iter :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset

88 
\<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> 'a Lazy_Sequence.lazy_sequence" 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

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

90 
"iter random nrandom seed = 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

91 
(if nrandom = 0 then Lazy_Sequence.empty else Lazy_Sequence.Lazy_Sequence (%u. let ((x, _), seed') = random seed in Some (x, iter random (nrandom  1) seed')))" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

92 

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

93 
definition pos_Random :: "(natural \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

94 
\<Rightarrow> 'a pos_random_dseq" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

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

96 
"pos_Random g = (%nrandom size seed depth. iter (g size) nrandom seed)" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

97 

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

98 

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

99 
type_synonym 'a neg_random_dseq = "natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> 'a Limited_Sequence.neg_dseq" 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

100 

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

101 
definition neg_empty :: "'a neg_random_dseq" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

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

103 
"neg_empty = (%nrandom size seed. Limited_Sequence.neg_empty)" 
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 neg_single :: "'a => 'a neg_random_dseq" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

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

107 
"neg_single x = (%nrandom size seed. Limited_Sequence.neg_single x)" 
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 
definition neg_bind :: "'a neg_random_dseq => ('a \<Rightarrow> 'b neg_random_dseq) \<Rightarrow> 'b neg_random_dseq" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

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

111 
"neg_bind R f = (\<lambda>nrandom size seed. Limited_Sequence.neg_bind (R nrandom size seed) (%a. f a nrandom size seed))" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

112 

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

113 
definition neg_decr_bind :: "'a neg_random_dseq => ('a \<Rightarrow> 'b neg_random_dseq) \<Rightarrow> 'b neg_random_dseq" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

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

115 
"neg_decr_bind R f = (\<lambda>nrandom size seed. Limited_Sequence.neg_decr_bind (R nrandom size seed) (%a. f a nrandom size seed))" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

116 

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

117 
definition neg_union :: "'a neg_random_dseq => 'a neg_random_dseq => 'a neg_random_dseq" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

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

119 
"neg_union R1 R2 = (\<lambda>nrandom size seed. Limited_Sequence.neg_union (R1 nrandom size seed) (R2 nrandom size seed))" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

120 

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

121 
definition neg_if_random_dseq :: "bool => unit neg_random_dseq" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

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

123 
"neg_if_random_dseq b = (if b then neg_single () else neg_empty)" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

124 

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

125 
definition neg_iterate_upto :: "(natural => 'a) => natural => natural => 'a neg_random_dseq" 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

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

127 
"neg_iterate_upto f n m = (\<lambda>nrandom size seed. Limited_Sequence.neg_iterate_upto f n m)" 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

128 

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

129 
definition neg_not_random_dseq :: "unit pos_random_dseq => unit neg_random_dseq" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

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

131 
"neg_not_random_dseq R = (\<lambda>nrandom size seed. Limited_Sequence.neg_not_seq (R nrandom size seed))" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

132 

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

133 
definition neg_map :: "('a => 'b) => 'a neg_random_dseq => 'b neg_random_dseq" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

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

135 
"neg_map f P = neg_bind P (neg_single o f)" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

136 

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

137 
definition pos_not_random_dseq :: "unit neg_random_dseq => unit pos_random_dseq" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

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

139 
"pos_not_random_dseq R = (\<lambda>nrandom size seed. Limited_Sequence.pos_not_seq (R nrandom size seed))" 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

140 

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

141 

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

142 
hide_const (open) 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

143 
empty single bind union if_random_dseq not_random_dseq map Random 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

144 
pos_empty pos_single pos_bind pos_decr_bind pos_union pos_if_random_dseq pos_iterate_upto 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

145 
pos_not_random_dseq pos_map iter pos_Random 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

146 
neg_empty neg_single neg_bind neg_decr_bind neg_union neg_if_random_dseq neg_iterate_upto 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

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

148 

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

149 
hide_fact (open) empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

150 
map_def Random.simps 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

151 
pos_empty_def pos_single_def pos_bind_def pos_decr_bind_def pos_union_def pos_if_random_dseq_def 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

152 
pos_iterate_upto_def pos_not_random_dseq_def pos_map_def iter.simps pos_Random_def 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

153 
neg_empty_def neg_single_def neg_bind_def neg_decr_bind_def neg_union_def neg_if_random_dseq_def 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

154 
neg_iterate_upto_def neg_not_random_dseq_def neg_map_def 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset

155 

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

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

157 