| author | nipkow |
| Tue, 23 Feb 2016 16:25:08 +0100 | |
| changeset 62390 | 842917225d56 |
| parent 48891 | c0eafbd55de3 |
| child 63167 | 0909deb8059b |
| permissions | -rw-r--r-- |
|
40104
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
1 |
theory Hotel_Example_Small_Generator |
|
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
41231
diff
changeset
|
2 |
imports Hotel_Example "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs" |
|
40104
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
3 |
begin |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
4 |
|
| 48891 | 5 |
ML_file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML" |
6 |
||
|
40104
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
7 |
declare Let_def[code_pred_inline] |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
8 |
|
|
40137
9eabcb1bfe50
changing test parameters in examples to get to a result within the global timelimit
bulwahn
parents:
40104
diff
changeset
|
9 |
lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)" |
|
9eabcb1bfe50
changing test parameters in examples to get to a result within the global timelimit
bulwahn
parents:
40104
diff
changeset
|
10 |
by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection) |
|
9eabcb1bfe50
changing test parameters in examples to get to a result within the global timelimit
bulwahn
parents:
40104
diff
changeset
|
11 |
|
|
9eabcb1bfe50
changing test parameters in examples to get to a result within the global timelimit
bulwahn
parents:
40104
diff
changeset
|
12 |
lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)" |
|
9eabcb1bfe50
changing test parameters in examples to get to a result within the global timelimit
bulwahn
parents:
40104
diff
changeset
|
13 |
by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection) |
|
9eabcb1bfe50
changing test parameters in examples to get to a result within the global timelimit
bulwahn
parents:
40104
diff
changeset
|
14 |
|
|
40104
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
15 |
instantiation room :: small_lazy |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
16 |
begin |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
17 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
18 |
definition |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
19 |
"small_lazy i = Lazy_Sequence.single Room0" |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
20 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
21 |
instance .. |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
22 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
23 |
end |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
24 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
25 |
instantiation key :: small_lazy |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
26 |
begin |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
27 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
28 |
definition |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
29 |
"small_lazy i = Lazy_Sequence.append (Lazy_Sequence.single Key0) (Lazy_Sequence.append (Lazy_Sequence.single Key1) (Lazy_Sequence.append (Lazy_Sequence.single Key2) (Lazy_Sequence.single Key3)))" |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
30 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
31 |
instance .. |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
32 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
33 |
end |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
34 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
35 |
instantiation guest :: small_lazy |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
36 |
begin |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
37 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
38 |
definition |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
39 |
"small_lazy i = Lazy_Sequence.append (Lazy_Sequence.single Guest0) (Lazy_Sequence.single Guest1)" |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
40 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
41 |
instance .. |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
42 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
43 |
end |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
44 |
|
|
43888
ee4be704c2a4
adapting an experimental setup to changes in quickcheck's infrastructure
bulwahn
parents:
42397
diff
changeset
|
45 |
ML {*
|
|
ee4be704c2a4
adapting an experimental setup to changes in quickcheck's infrastructure
bulwahn
parents:
42397
diff
changeset
|
46 |
val small_15_active = Attrib.setup_config_bool @{binding quickcheck_small_14_active} (K false);
|
|
ee4be704c2a4
adapting an experimental setup to changes in quickcheck's infrastructure
bulwahn
parents:
42397
diff
changeset
|
47 |
val small_14_active = Attrib.setup_config_bool @{binding quickcheck_small_15_active} (K false);
|
|
ee4be704c2a4
adapting an experimental setup to changes in quickcheck's infrastructure
bulwahn
parents:
42397
diff
changeset
|
48 |
*} |
|
40104
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
49 |
|
|
43888
ee4be704c2a4
adapting an experimental setup to changes in quickcheck's infrastructure
bulwahn
parents:
42397
diff
changeset
|
50 |
setup {*
|
|
ee4be704c2a4
adapting an experimental setup to changes in quickcheck's infrastructure
bulwahn
parents:
42397
diff
changeset
|
51 |
Context.theory_map (Quickcheck.add_tester ("small_generators_depth_14",
|
|
ee4be704c2a4
adapting an experimental setup to changes in quickcheck's infrastructure
bulwahn
parents:
42397
diff
changeset
|
52 |
(small_14_active, Predicate_Compile_Quickcheck.test_goals |
|
ee4be704c2a4
adapting an experimental setup to changes in quickcheck's infrastructure
bulwahn
parents:
42397
diff
changeset
|
53 |
(Predicate_Compile_Aux.Pos_Generator_DSeq, true, true, 14)))) |
|
ee4be704c2a4
adapting an experimental setup to changes in quickcheck's infrastructure
bulwahn
parents:
42397
diff
changeset
|
54 |
#> Context.theory_map (Quickcheck.add_tester ("small_generators_depth_15",
|
|
ee4be704c2a4
adapting an experimental setup to changes in quickcheck's infrastructure
bulwahn
parents:
42397
diff
changeset
|
55 |
(small_15_active, Predicate_Compile_Quickcheck.test_goals |
|
ee4be704c2a4
adapting an experimental setup to changes in quickcheck's infrastructure
bulwahn
parents:
42397
diff
changeset
|
56 |
(Predicate_Compile_Aux.Pos_Generator_DSeq, true, true, 15)))) |
|
ee4be704c2a4
adapting an experimental setup to changes in quickcheck's infrastructure
bulwahn
parents:
42397
diff
changeset
|
57 |
*} |
|
40104
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
58 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
59 |
lemma |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
60 |
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g" |
| 42291 | 61 |
(*quickcheck[tester = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 1200.0, expect = no_counterexample]*) |
| 42397 | 62 |
quickcheck[tester = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 2400.0, expect = counterexample] |
|
40104
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
63 |
oops |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
64 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
65 |
|
| 62390 | 66 |
end |