equal
deleted
inserted
replaced
1 theory RegExp_Example |
1 theory Reg_Exp_Example |
2 imports Predicate_Compile_Quickcheck Code_Prolog |
2 imports Predicate_Compile_Quickcheck Code_Prolog |
3 begin |
3 begin |
4 |
4 |
5 text {* An example from the experiments from SmallCheck (http://www.cs.york.ac.uk/fp/smallcheck/) *} |
5 text {* An example from the experiments from SmallCheck (http://www.cs.york.ac.uk/fp/smallcheck/) *} |
6 text {* The example (original in Haskell) was imported with Haskabelle and |
6 text {* The example (original in Haskell) was imported with Haskabelle and |
156 assumes "k = Suc (Suc Zer)" |
156 assumes "k = Suc (Suc Zer)" |
157 assumes "p = Sym N0" |
157 assumes "p = Sym N0" |
158 assumes "q = Seq (Sym N0) (Sym N0)" |
158 assumes "q = Seq (Sym N0) (Sym N0)" |
159 assumes "s = [N0, N0]" |
159 assumes "s = [N0, N0]" |
160 shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s" |
160 shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s" |
161 quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample] |
161 (*quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]*) |
162 quickcheck[generator = prolog, iterations = 1, size = 1, expect = counterexample] |
162 quickcheck[generator = prolog, iterations = 1, size = 1, expect = counterexample] |
163 oops |
163 oops |
164 |
164 |
165 lemma |
165 lemma |
166 assumes "n = Zer" |
166 assumes "n = Zer" |