author | wenzelm |
Sun, 28 Nov 2010 14:01:20 +0100 | |
changeset 40781 | ba5be5c3d477 |
parent 40137 | 9eabcb1bfe50 |
child 40924 | a9be7f26b4e6 |
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_Prolog |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
2 |
imports Hotel_Example Predicate_Compile_Alternative_Defs Code_Prolog |
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 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
5 |
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
|
6 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
7 |
lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)" |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
8 |
by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection) |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
9 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
10 |
lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)" |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
11 |
by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection) |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
12 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
13 |
setup {* Code_Prolog.map_code_options (K |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
14 |
{ensure_groundness = true, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
15 |
limit_globally = NONE, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
16 |
limited_types = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
17 |
limited_predicates = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
18 |
replacing = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
19 |
manual_reorder = []}) *} |
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 |
values 40 "{s. hotel s}" |
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 |
setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *} |
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 |
lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g" |
40137
9eabcb1bfe50
changing test parameters in examples to get to a result within the global timelimit
bulwahn
parents:
40104
diff
changeset
|
26 |
quickcheck[generator = code, iterations = 10000, report] |
40104
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
27 |
quickcheck[generator = prolog, iterations = 1, expect = counterexample] |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
28 |
oops |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
29 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
30 |
section {* Manual setup to find the counterexample *} |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
31 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
32 |
setup {* Code_Prolog.map_code_options (K |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
33 |
{ensure_groundness = true, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
34 |
limit_globally = NONE, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
35 |
limited_types = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
36 |
limited_predicates = [(["hotel"], 4)], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
37 |
replacing = [(("hotel", "limited_hotel"), "quickcheck")], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
38 |
manual_reorder = []}) *} |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
39 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
40 |
lemma |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
41 |
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g" |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
42 |
quickcheck[generator = prolog, iterations = 1, expect = no_counterexample] |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
43 |
oops |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
44 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
45 |
setup {* Code_Prolog.map_code_options (K |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
46 |
{ensure_groundness = true, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
47 |
limit_globally = NONE, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
48 |
limited_types = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
49 |
limited_predicates = [(["hotel"], 5)], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
50 |
replacing = [(("hotel", "limited_hotel"), "quickcheck")], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
51 |
manual_reorder = []}) *} |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
52 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
53 |
lemma |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
54 |
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g" |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
55 |
quickcheck[generator = prolog, iterations = 1, expect = counterexample] |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
56 |
oops |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
57 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
58 |
section {* Simulating a global depth limit manually by limiting all predicates *} |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
59 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
60 |
setup {* |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
61 |
Code_Prolog.map_code_options (K |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
62 |
{ensure_groundness = true, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
63 |
limit_globally = NONE, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
64 |
limited_types = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
65 |
limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP", |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
66 |
"cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 12)], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
67 |
replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
68 |
manual_reorder = []}) |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
69 |
*} |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
70 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
71 |
lemma |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
72 |
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g" |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
73 |
quickcheck[generator = prolog, iterations = 1, expect = no_counterexample] |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
74 |
oops |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
75 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
76 |
setup {* |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
77 |
Code_Prolog.map_code_options (K |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
78 |
{ensure_groundness = true, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
79 |
limit_globally = NONE, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
80 |
limited_types = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
81 |
limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP", |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
82 |
"cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 13)], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
83 |
replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
84 |
manual_reorder = []}) |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
85 |
*} |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
86 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
87 |
lemma |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
88 |
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g" |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
89 |
quickcheck[generator = prolog, iterations = 1, expect = counterexample] |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
90 |
oops |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
91 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
92 |
section {* Using a global limit for limiting the execution *} |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
93 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
94 |
text {* A global depth limit of 13 does not suffice to find the counterexample. *} |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
95 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
96 |
setup {* |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
97 |
Code_Prolog.map_code_options (K |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
98 |
{ensure_groundness = true, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
99 |
limit_globally = SOME 13, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
100 |
limited_types = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
101 |
limited_predicates = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
102 |
replacing = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
103 |
manual_reorder = []}) |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
104 |
*} |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
105 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
106 |
lemma |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
107 |
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g" |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
108 |
quickcheck[generator = prolog, iterations = 1, expect = no_counterexample] |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
109 |
oops |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
110 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
111 |
text {* But a global depth limit of 14 does. *} |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
112 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
113 |
setup {* |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
114 |
Code_Prolog.map_code_options (K |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
115 |
{ensure_groundness = true, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
116 |
limit_globally = SOME 14, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
117 |
limited_types = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
118 |
limited_predicates = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
119 |
replacing = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
120 |
manual_reorder = []}) |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
121 |
*} |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
122 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
123 |
lemma |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
124 |
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g" |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
125 |
quickcheck[generator = prolog, iterations = 1, expect = counterexample] |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
126 |
oops |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
127 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
128 |
end |