author | bulwahn |
Thu, 16 Sep 2010 13:49:08 +0200 | |
changeset 39463 | 7ce0ed8dc4d6 |
parent 39189 | d183bf90dabd |
child 39800 | 17e29ddd538e |
permissions | -rw-r--r-- |
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
1 |
theory Context_Free_Grammar_Example |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
2 |
imports Code_Prolog |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
3 |
begin |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
4 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
5 |
declare mem_def[code_pred_inline] |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
6 |
|
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 |
|
39463 | 22 |
setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *} |
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
23 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
24 |
datatype alphabet = a | b |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
25 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
26 |
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
|
27 |
"[] \<in> S\<^isub>1" |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
28 |
| "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
|
29 |
| "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
|
30 |
| "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
|
31 |
| "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
|
32 |
| "\<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
|
33 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
34 |
lemma |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
35 |
"w \<in> S\<^isub>1 \<Longrightarrow> w = []" |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
36 |
quickcheck[generator = prolog, iterations=1, expect = counterexample] |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
37 |
oops |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
38 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
39 |
definition "filter_a = filter (\<lambda>x. x = a)" |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
40 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
41 |
lemma [code_pred_def]: "filter_a [] = []" |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
42 |
unfolding filter_a_def by simp |
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 (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
|
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 |
declare filter_a_def[symmetric, code_pred_inline] |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
48 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
49 |
definition "filter_b = filter (\<lambda>x. x = b)" |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
50 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
51 |
lemma [code_pred_def]: "filter_b [] = []" |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
52 |
unfolding filter_b_def by simp |
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 (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
|
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 |
declare filter_b_def[symmetric, code_pred_inline] |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
58 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
59 |
setup {* Code_Prolog.map_code_options (K |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
60 |
{ensure_groundness = true, |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
61 |
limited_types = [], |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
62 |
limited_predicates = [(["s1", "a1", "b1"], 2)], |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
63 |
replacing = [(("s1", "limited_s1"), "quickcheck")], |
39463 | 64 |
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
|
65 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
66 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
67 |
theorem S\<^isub>1_sound: |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
68 |
"w \<in> S\<^isub>1 \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
69 |
quickcheck[generator = prolog, iterations=1, expect = counterexample] |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
70 |
oops |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
71 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
72 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
73 |
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
|
74 |
"[] \<in> S\<^isub>2" |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
75 |
| "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
|
76 |
| "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
|
77 |
| "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
|
78 |
| "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
|
79 |
| "\<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
|
80 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
81 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
82 |
setup {* Code_Prolog.map_code_options (K |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
83 |
{ensure_groundness = true, |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
84 |
limited_types = [], |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
85 |
limited_predicates = [(["s2", "a2", "b2"], 3)], |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
86 |
replacing = [(("s2", "limited_s2"), "quickcheck")], |
39463 | 87 |
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
|
88 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
89 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
90 |
theorem S\<^isub>2_sound: |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
91 |
"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
92 |
quickcheck[generator=prolog, iterations=1, expect = counterexample] |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
93 |
oops |
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 |
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
|
96 |
"[] \<in> S\<^isub>3" |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
97 |
| "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
|
98 |
| "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
|
99 |
| "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
|
100 |
| "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
|
101 |
| "\<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
|
102 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
103 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
104 |
setup {* Code_Prolog.map_code_options (K |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
105 |
{ensure_groundness = true, |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
106 |
limited_types = [], |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
107 |
limited_predicates = [(["s3", "a3", "b3"], 6)], |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
108 |
replacing = [(("s3", "limited_s3"), "quickcheck")], |
39463 | 109 |
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
|
110 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
111 |
lemma S\<^isub>3_sound: |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
112 |
"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
113 |
quickcheck[generator=prolog, iterations=1, size=1, expect = no_counterexample] |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
114 |
oops |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
115 |
|
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 |
(* |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
118 |
setup {* Code_Prolog.map_code_options (K |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
119 |
{ensure_groundness = true, |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
120 |
limited_types = [], |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
121 |
limited_predicates = [], |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
122 |
replacing = [], |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
123 |
manual_reorder = [], |
39189 | 124 |
timeout = Time.fromSeconds 10, |
38962
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
125 |
prolog_system = Code_Prolog.SWI_PROLOG}) *} |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
126 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
127 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
128 |
theorem S\<^isub>3_complete: |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
129 |
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3" |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
130 |
quickcheck[generator = prolog, size=1, iterations=1] |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
131 |
oops |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
132 |
*) |
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 |
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
|
135 |
"[] \<in> S\<^isub>4" |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
136 |
| "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
|
137 |
| "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
|
138 |
| "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
|
139 |
| "\<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
|
140 |
| "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
|
141 |
| "\<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
|
142 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
143 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
144 |
setup {* Code_Prolog.map_code_options (K |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
145 |
{ensure_groundness = true, |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
146 |
limited_types = [], |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
147 |
limited_predicates = [(["s4", "a4", "b4"], 6)], |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
148 |
replacing = [(("s4", "limited_s4"), "quickcheck")], |
39463 | 149 |
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
|
150 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
151 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
152 |
theorem S\<^isub>4_sound: |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
153 |
"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
154 |
quickcheck[generator = prolog, size=1, iterations=1, expect = no_counterexample] |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
155 |
oops |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
156 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
157 |
(* |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
158 |
theorem S\<^isub>4_complete: |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
159 |
"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
|
160 |
oops |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
161 |
*) |
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
162 |
|
3917c2acaec4
adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff
changeset
|
163 |
hide_const a b |
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 |
end |