author | blanchet |
Tue, 31 Aug 2010 21:01:47 +0200 | |
changeset 38944 | 827c98e8ba8b |
parent 38734 | e5508a74b11f |
child 38949 | 1afa9e89c885 |
permissions | -rw-r--r-- |
38730 | 1 |
theory Hotel_Example |
2 |
imports Predicate_Compile_Alternative_Defs Code_Prolog |
|
3 |
begin |
|
4 |
||
5 |
datatype guest = Guest0 | Guest1 |
|
6 |
datatype key = Key0 | Key1 | Key2 | Key3 |
|
7 |
datatype room = Room0 |
|
8 |
||
9 |
types card = "key * key" |
|
10 |
||
11 |
datatype event = |
|
12 |
Check_in guest room card | Enter guest room card | Exit guest room |
|
13 |
||
14 |
definition initk :: "room \<Rightarrow> key" |
|
15 |
where "initk = (%r. Key0)" |
|
16 |
||
17 |
declare initk_def[code_pred_def, code] |
|
18 |
||
19 |
primrec owns :: "event list \<Rightarrow> room \<Rightarrow> guest option" |
|
20 |
where |
|
21 |
"owns [] r = None" |
|
22 |
| "owns (e#s) r = (case e of |
|
23 |
Check_in g r' c \<Rightarrow> if r' = r then Some g else owns s r | |
|
24 |
Enter g r' c \<Rightarrow> owns s r | |
|
25 |
Exit g r' \<Rightarrow> owns s r)" |
|
26 |
||
27 |
primrec currk :: "event list \<Rightarrow> room \<Rightarrow> key" |
|
28 |
where |
|
29 |
"currk [] r = initk r" |
|
30 |
| "currk (e#s) r = (let k = currk s r in |
|
31 |
case e of Check_in g r' (k1, k2) \<Rightarrow> if r' = r then k2 else k |
|
32 |
| Enter g r' c \<Rightarrow> k |
|
33 |
| Exit g r \<Rightarrow> k)" |
|
34 |
||
35 |
primrec issued :: "event list \<Rightarrow> key set" |
|
36 |
where |
|
37 |
"issued [] = range initk" |
|
38 |
| "issued (e#s) = issued s \<union> |
|
39 |
(case e of Check_in g r (k1, k2) \<Rightarrow> {k2} | Enter g r c \<Rightarrow> {} | Exit g r \<Rightarrow> {})" |
|
40 |
||
41 |
primrec cards :: "event list \<Rightarrow> guest \<Rightarrow> card set" |
|
42 |
where |
|
43 |
"cards [] g = {}" |
|
44 |
| "cards (e#s) g = (let C = cards s g in |
|
45 |
case e of Check_in g' r c \<Rightarrow> if g' = g then insert c C |
|
46 |
else C |
|
47 |
| Enter g r c \<Rightarrow> C |
|
48 |
| Exit g r \<Rightarrow> C)" |
|
49 |
||
50 |
primrec roomk :: "event list \<Rightarrow> room \<Rightarrow> key" |
|
51 |
where |
|
52 |
"roomk [] r = initk r" |
|
53 |
| "roomk (e#s) r = (let k = roomk s r in |
|
54 |
case e of Check_in g r' c \<Rightarrow> k |
|
55 |
| Enter g r' (x,y) \<Rightarrow> if r' = r (*& x = k*) then y else k |
|
56 |
| Exit g r \<Rightarrow> k)" |
|
57 |
||
58 |
primrec isin :: "event list \<Rightarrow> room \<Rightarrow> guest set" |
|
59 |
where |
|
60 |
"isin [] r = {}" |
|
61 |
| "isin (e#s) r = (let G = isin s r in |
|
62 |
case e of Check_in g r c \<Rightarrow> G |
|
63 |
| Enter g r' c \<Rightarrow> if r' = r then {g} \<union> G else G |
|
64 |
| Exit g r' \<Rightarrow> if r'=r then G - {g} else G)" |
|
65 |
||
66 |
primrec hotel :: "event list \<Rightarrow> bool" |
|
67 |
where |
|
68 |
"hotel [] = True" |
|
69 |
| "hotel (e # s) = (hotel s & (case e of |
|
70 |
Check_in g r (k,k') \<Rightarrow> k = currk s r \<and> k' \<notin> issued s | |
|
71 |
Enter g r (k,k') \<Rightarrow> (k,k') : cards s g & (roomk s r : {k, k'}) | |
|
38734
e5508a74b11f
changing hotel trace definition; adding simple handling of numerals on natural numbers
bulwahn
parents:
38733
diff
changeset
|
72 |
Exit g r \<Rightarrow> g : isin s r))" |
38730 | 73 |
|
74 |
lemma issued_nil: "issued [] = {Key0}" |
|
75 |
by (auto simp add: initk_def) |
|
76 |
||
77 |
lemmas issued_simps[code, code_pred_def] = issued_nil issued.simps(2) |
|
78 |
||
79 |
declare Let_def[code_pred_inline] |
|
80 |
||
81 |
lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)" |
|
82 |
by (auto simp add: insert_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection) |
|
83 |
||
84 |
lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)" |
|
85 |
by (auto simp add: Diff_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection) |
|
86 |
||
87 |
ML {* Code_Prolog.options := {ensure_groundness = true} *} |
|
88 |
||
38734
e5508a74b11f
changing hotel trace definition; adding simple handling of numerals on natural numbers
bulwahn
parents:
38733
diff
changeset
|
89 |
values 40 "{s. hotel s}" |
38730 | 90 |
|
38731
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38730
diff
changeset
|
91 |
|
38733
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38731
diff
changeset
|
92 |
setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *} |
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38731
diff
changeset
|
93 |
ML {* set Code_Prolog.trace *} |
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38731
diff
changeset
|
94 |
|
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38731
diff
changeset
|
95 |
lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g" |
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38731
diff
changeset
|
96 |
quickcheck[generator = code, iterations = 100000, report] |
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38731
diff
changeset
|
97 |
quickcheck[generator = prolog, iterations = 1] |
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38731
diff
changeset
|
98 |
oops |
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38731
diff
changeset
|
99 |
|
38731
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38730
diff
changeset
|
100 |
|
38730 | 101 |
end |