87 |
87 |
88 |
88 |
89 |
89 |
90 lemma "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s" |
90 lemma "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s" |
91 (*nitpick |
91 (*nitpick |
92 quickcheck[generator = code, iterations = 10000] |
92 quickcheck[tester = random, iterations = 10000] |
93 quickcheck[generator = predicate_compile_wo_ff] |
93 quickcheck[tester = predicate_compile_wo_ff] |
94 quickcheck[generator = predicate_compile_ff_fs] |
94 quickcheck[tester = predicate_compile_ff_fs] |
95 oops*) |
95 oops*) |
96 oops |
96 oops |
97 |
97 |
98 |
98 |
99 setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *} |
99 setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *} |
113 |
113 |
114 text {* Finding the counterexample still seems out of reach for the |
114 text {* Finding the counterexample still seems out of reach for the |
115 prolog-style generation. *} |
115 prolog-style generation. *} |
116 |
116 |
117 lemma "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s" |
117 lemma "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s" |
118 quickcheck[generator = code, iterations = 100000, expect = counterexample] |
118 quickcheck[tester = random, iterations = 100000, expect = counterexample] |
119 (*quickcheck[generator = predicate_compile_wo_ff]*) |
119 (*quickcheck[tester = predicate_compile_wo_ff]*) |
120 (*quickcheck[generator = predicate_compile_ff_fs, iterations = 1]*) |
120 (*quickcheck[tester = predicate_compile_ff_fs, iterations = 1]*) |
121 (*quickcheck[generator = prolog, iterations = 1, size = 1]*) |
121 (*quickcheck[tester = prolog, iterations = 1, size = 1]*) |
122 oops |
122 oops |
123 |
123 |
124 section {* Given a partial solution *} |
124 section {* Given a partial solution *} |
125 |
125 |
126 lemma |
126 lemma |
128 assumes "k = Suc (Suc Zer)"*) |
128 assumes "k = Suc (Suc Zer)"*) |
129 assumes "p = Sym N0" |
129 assumes "p = Sym N0" |
130 assumes "q = Seq (Sym N0) (Sym N0)" |
130 assumes "q = Seq (Sym N0) (Sym N0)" |
131 (* assumes "s = [N0, N0]"*) |
131 (* assumes "s = [N0, N0]"*) |
132 shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s" |
132 shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s" |
133 (*quickcheck[generator = predicate_compile_wo_ff, iterations = 1]*) |
133 (*quickcheck[tester = predicate_compile_wo_ff, iterations = 1]*) |
134 quickcheck[generator = prolog, iterations = 1, size = 1, expect = counterexample] |
134 quickcheck[tester = prolog, iterations = 1, size = 1, expect = counterexample] |
135 oops |
135 oops |
136 |
136 |
137 section {* Checking the counterexample *} |
137 section {* Checking the counterexample *} |
138 |
138 |
139 definition a_sol |
139 definition a_sol |
145 assumes "k = Suc (Suc Zer)" |
145 assumes "k = Suc (Suc Zer)" |
146 assumes "p = Sym N0" |
146 assumes "p = Sym N0" |
147 assumes "q = Seq (Sym N0) (Sym N0)" |
147 assumes "q = Seq (Sym N0) (Sym N0)" |
148 assumes "s = [N0, N0]" |
148 assumes "s = [N0, N0]" |
149 shows "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s" |
149 shows "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s" |
150 (*quickcheck[generator = predicate_compile_wo_ff]*) |
150 (*quickcheck[tester = predicate_compile_wo_ff]*) |
151 oops |
151 oops |
152 |
152 |
153 lemma |
153 lemma |
154 assumes "n = Zer" |
154 assumes "n = Zer" |
155 assumes "k = Suc (Suc Zer)" |
155 assumes "k = Suc (Suc Zer)" |
156 assumes "p = Sym N0" |
156 assumes "p = Sym N0" |
157 assumes "q = Seq (Sym N0) (Sym N0)" |
157 assumes "q = Seq (Sym N0) (Sym N0)" |
158 assumes "s = [N0, N0]" |
158 assumes "s = [N0, N0]" |
159 shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s" |
159 shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s" |
160 (*quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]*) |
160 (*quickcheck[tester = predicate_compile_wo_ff, iterations = 1, expect = counterexample]*) |
161 quickcheck[generator = prolog, iterations = 1, size = 1, expect = counterexample] |
161 quickcheck[tester = prolog, iterations = 1, size = 1, expect = counterexample] |
162 oops |
162 oops |
163 |
163 |
164 lemma |
164 lemma |
165 assumes "n = Zer" |
165 assumes "n = Zer" |
166 assumes "k = Suc (Suc Zer)" |
166 assumes "k = Suc (Suc Zer)" |
167 assumes "p = Sym N0" |
167 assumes "p = Sym N0" |
168 assumes "q = Seq (Sym N0) (Sym N0)" |
168 assumes "q = Seq (Sym N0) (Sym N0)" |
169 assumes "s = [N0, N0]" |
169 assumes "s = [N0, N0]" |
170 shows "prop_regex (n, (k, (p, (q, s))))" |
170 shows "prop_regex (n, (k, (p, (q, s))))" |
171 quickcheck[generator = predicate_compile_wo_ff] |
171 quickcheck[tester = predicate_compile_wo_ff] |
172 quickcheck[generator = prolog, expect = counterexample] |
172 quickcheck[tester = prolog, expect = counterexample] |
173 oops |
173 oops |
174 |
174 |
175 lemma "prop_regex a_sol" |
175 lemma "prop_regex a_sol" |
176 quickcheck[generator = code, expect = counterexample] |
176 quickcheck[tester = random, expect = counterexample] |
177 quickcheck[generator = predicate_compile_ff_fs] |
177 quickcheck[tester = predicate_compile_ff_fs] |
178 oops |
178 oops |
179 |
179 |
180 value [code] "prop_regex a_sol" |
180 value [code] "prop_regex a_sol" |
181 |
181 |
182 |
182 |