author | wenzelm |
Sun, 13 Mar 2011 21:21:48 +0100 | |
changeset 41956 | c15ef1b85035 |
parent 41413 | 64cd30d6b0b8 |
child 43885 | 7caa1139b4e5 |
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 |
41956 | 2 |
imports |
3 |
Hotel_Example |
|
4 |
"~~/src/HOL/Library/Predicate_Compile_Alternative_Defs" |
|
5 |
"~~/src/HOL/Library/Code_Prolog" |
|
40104
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
6 |
begin |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
7 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
8 |
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
|
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]: "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
|
11 |
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
|
12 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
13 |
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
|
14 |
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
|
15 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
16 |
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
|
17 |
{ensure_groundness = true, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
18 |
limit_globally = NONE, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
19 |
limited_types = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
20 |
limited_predicates = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
21 |
replacing = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
22 |
manual_reorder = []}) *} |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
23 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
24 |
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
|
25 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
26 |
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
|
27 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
28 |
lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g" |
40924 | 29 |
quickcheck[tester = random, iterations = 10000, report] |
30 |
quickcheck[tester = prolog, iterations = 1, expect = counterexample] |
|
40104
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
31 |
oops |
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 |
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
|
34 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
35 |
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
|
36 |
{ensure_groundness = true, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
37 |
limit_globally = NONE, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
38 |
limited_types = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
39 |
limited_predicates = [(["hotel"], 4)], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
40 |
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
|
41 |
manual_reorder = []}) *} |
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 |
lemma |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
44 |
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g" |
40924 | 45 |
quickcheck[tester = prolog, iterations = 1, expect = no_counterexample] |
40104
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
46 |
oops |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
47 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
48 |
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
|
49 |
{ensure_groundness = true, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
50 |
limit_globally = NONE, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
51 |
limited_types = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
52 |
limited_predicates = [(["hotel"], 5)], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
53 |
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
|
54 |
manual_reorder = []}) *} |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
55 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
56 |
lemma |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
57 |
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g" |
40924 | 58 |
quickcheck[tester = prolog, iterations = 1, expect = counterexample] |
40104
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
59 |
oops |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
60 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
61 |
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
|
62 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
63 |
setup {* |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
64 |
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
|
65 |
{ensure_groundness = true, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
66 |
limit_globally = NONE, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
67 |
limited_types = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
68 |
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
|
69 |
"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
|
70 |
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
|
71 |
manual_reorder = []}) |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
72 |
*} |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
73 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
74 |
lemma |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
75 |
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g" |
40924 | 76 |
quickcheck[tester = prolog, iterations = 1, expect = no_counterexample] |
40104
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
77 |
oops |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
78 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
79 |
setup {* |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
80 |
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
|
81 |
{ensure_groundness = true, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
82 |
limit_globally = NONE, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
83 |
limited_types = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
84 |
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
|
85 |
"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
|
86 |
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
|
87 |
manual_reorder = []}) |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
88 |
*} |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
89 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
90 |
lemma |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
91 |
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g" |
40924 | 92 |
quickcheck[tester = prolog, iterations = 1, expect = counterexample] |
40104
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
93 |
oops |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
94 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
95 |
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
|
96 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
97 |
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
|
98 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
99 |
setup {* |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
100 |
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
|
101 |
{ensure_groundness = true, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
102 |
limit_globally = SOME 13, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
103 |
limited_types = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
104 |
limited_predicates = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
105 |
replacing = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
106 |
manual_reorder = []}) |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
107 |
*} |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
108 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
109 |
lemma |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
110 |
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g" |
40924 | 111 |
quickcheck[tester = prolog, iterations = 1, expect = no_counterexample] |
40104
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
112 |
oops |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
113 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
114 |
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
|
115 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
116 |
setup {* |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
117 |
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
|
118 |
{ensure_groundness = true, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
119 |
limit_globally = SOME 14, |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
120 |
limited_types = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
121 |
limited_predicates = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
122 |
replacing = [], |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
123 |
manual_reorder = []}) |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
124 |
*} |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
125 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
126 |
lemma |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
127 |
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g" |
40924 | 128 |
quickcheck[tester = prolog, iterations = 1, expect = counterexample] |
40104
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
129 |
oops |
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
130 |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
131 |
end |