author  wenzelm 
Mon, 15 Jul 2013 20:36:27 +0200  
changeset 52666  391913d17d15 
parent 45970  b6d0cff57d96 
child 53015  a1119cf551e8 
permissions  rwrr 
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

1 
theory Context_Free_Grammar_Example 
41956  2 
imports "~~/src/HOL/Library/Code_Prolog" 
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

3 
begin 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
43913
diff
changeset

4 
(* 
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

5 
declare mem_def[code_pred_inline] 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
43913
diff
changeset

6 
*) 
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

7 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

8 
subsection {* Alternative rules for length *} 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

9 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

10 
definition size_list :: "'a list => nat" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

11 
where "size_list = size" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

12 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

13 
lemma size_list_simps: 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

14 
"size_list [] = 0" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

15 
"size_list (x # xs) = Suc (size_list xs)" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

16 
by (auto simp add: size_list_def) 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

17 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

18 
declare size_list_simps[code_pred_def] 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

19 
declare size_list_def[symmetric, code_pred_inline] 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

20 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

21 

52666  22 
setup {* 
23 
Context.theory_map 

24 
(Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) 

25 
*} 

38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

26 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

27 
datatype alphabet = a  b 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

28 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

29 
inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

30 
"[] \<in> S\<^isub>1" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

31 
 "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

32 
 "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

33 
 "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

34 
 "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

35 
 "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

36 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

37 
lemma 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
43913
diff
changeset

38 
"S\<^isub>1p w \<Longrightarrow> w = []" 
40924  39 
quickcheck[tester = prolog, iterations=1, expect = counterexample] 
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

40 
oops 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

41 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

42 
definition "filter_a = filter (\<lambda>x. x = a)" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

43 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

44 
lemma [code_pred_def]: "filter_a [] = []" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

45 
unfolding filter_a_def by simp 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

46 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

47 
lemma [code_pred_def]: "filter_a (x#xs) = (if x = a then x # filter_a xs else filter_a xs)" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

48 
unfolding filter_a_def by simp 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

49 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

50 
declare filter_a_def[symmetric, code_pred_inline] 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

51 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

52 
definition "filter_b = filter (\<lambda>x. x = b)" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

53 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

54 
lemma [code_pred_def]: "filter_b [] = []" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

55 
unfolding filter_b_def by simp 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

56 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

57 
lemma [code_pred_def]: "filter_b (x#xs) = (if x = b then x # filter_b xs else filter_b xs)" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

58 
unfolding filter_b_def by simp 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

59 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

60 
declare filter_b_def[symmetric, code_pred_inline] 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

61 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

62 
setup {* Code_Prolog.map_code_options (K 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

63 
{ensure_groundness = true, 
39800  64 
limit_globally = NONE, 
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

65 
limited_types = [], 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
43913
diff
changeset

66 
limited_predicates = [(["s1p", "a1p", "b1p"], 2)], 
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
43913
diff
changeset

67 
replacing = [(("s1p", "limited_s1p"), "quickcheck")], 
39463  68 
manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *} 
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

69 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

70 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

71 
theorem S\<^isub>1_sound: 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
43913
diff
changeset

72 
"S\<^isub>1p w \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" 
40924  73 
quickcheck[tester = prolog, iterations=1, expect = counterexample] 
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

74 
oops 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

75 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

76 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

77 
inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

78 
"[] \<in> S\<^isub>2" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

79 
 "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

80 
 "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

81 
 "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

82 
 "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

83 
 "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

84 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

85 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

86 
setup {* Code_Prolog.map_code_options (K 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

87 
{ensure_groundness = true, 
39800  88 
limit_globally = NONE, 
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

89 
limited_types = [], 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
43913
diff
changeset

90 
limited_predicates = [(["s2p", "a2p", "b2p"], 3)], 
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
43913
diff
changeset

91 
replacing = [(("s2p", "limited_s2p"), "quickcheck")], 
39463  92 
manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *} 
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

93 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

94 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

95 
theorem S\<^isub>2_sound: 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
43913
diff
changeset

96 
"S\<^isub>2p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" 
40924  97 
quickcheck[tester = prolog, iterations=1, expect = counterexample] 
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

98 
oops 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

99 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

100 
inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

101 
"[] \<in> S\<^isub>3" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

102 
 "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

103 
 "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

104 
 "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

105 
 "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

106 
 "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

107 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

108 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

109 
setup {* Code_Prolog.map_code_options (K 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

110 
{ensure_groundness = true, 
39800  111 
limit_globally = NONE, 
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

112 
limited_types = [], 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
43913
diff
changeset

113 
limited_predicates = [(["s3p", "a3p", "b3p"], 6)], 
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
43913
diff
changeset

114 
replacing = [(("s3p", "limited_s3p"), "quickcheck")], 
39463  115 
manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *} 
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

116 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

117 
lemma S\<^isub>3_sound: 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
43913
diff
changeset

118 
"S\<^isub>3p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" 
40924  119 
quickcheck[tester = prolog, iterations=1, size=1, expect = no_counterexample] 
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

120 
oops 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

121 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

122 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

123 
(* 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

124 
setup {* Code_Prolog.map_code_options (K 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

125 
{ensure_groundness = true, 
39800  126 
limit_globally = NONE, 
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

127 
limited_types = [], 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

128 
limited_predicates = [], 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

129 
replacing = [], 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

130 
manual_reorder = [], 
40301  131 
timeout = seconds 10.0, 
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

132 
prolog_system = Code_Prolog.SWI_PROLOG}) *} 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

133 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

134 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

135 
theorem S\<^isub>3_complete: 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

136 
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3" 
40924  137 
quickcheck[tester = prolog, size=1, iterations=1] 
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

138 
oops 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

139 
*) 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

140 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

141 
inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

142 
"[] \<in> S\<^isub>4" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

143 
 "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

144 
 "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

145 
 "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

146 
 "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

147 
 "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

148 
 "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

149 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

150 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

151 
setup {* Code_Prolog.map_code_options (K 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

152 
{ensure_groundness = true, 
39800  153 
limit_globally = NONE, 
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

154 
limited_types = [], 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
43913
diff
changeset

155 
limited_predicates = [(["s4p", "a4p", "b4p"], 6)], 
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
43913
diff
changeset

156 
replacing = [(("s4p", "limited_s4p"), "quickcheck")], 
39463  157 
manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *} 
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

158 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

159 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

160 
theorem S\<^isub>4_sound: 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
43913
diff
changeset

161 
"S\<^isub>4p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" 
40924  162 
quickcheck[tester = prolog, size=1, iterations=1, expect = no_counterexample] 
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

163 
oops 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

164 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

165 
(* 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

166 
theorem S\<^isub>4_complete: 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

167 
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4" 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

168 
oops 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

169 
*) 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

170 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

171 
hide_const a b 
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

172 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

173 

3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset

174 
end 