|
1 (* Title: HOL/Nitpick_Examples/Hotel_Nits.thy |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 Copyright 2010 |
|
4 |
|
5 Nitpick example based on Tobias Nipkow's hotel key card formalization. |
|
6 *) |
|
7 |
|
8 header {* Nitpick Example Based on Tobias Nipkow's Hotel Key Card |
|
9 Formalization *} |
|
10 |
|
11 theory Hotel_Nits |
|
12 imports Main |
|
13 begin |
|
14 |
|
15 nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 120 s] |
|
16 |
|
17 typedecl guest |
|
18 typedecl key |
|
19 typedecl room |
|
20 |
|
21 types keycard = "key \<times> key" |
|
22 |
|
23 record state = |
|
24 owns :: "room \<Rightarrow> guest option" |
|
25 currk :: "room \<Rightarrow> key" |
|
26 issued :: "key set" |
|
27 cards :: "guest \<Rightarrow> keycard set" |
|
28 roomk :: "room \<Rightarrow> key" |
|
29 isin :: "room \<Rightarrow> guest set" |
|
30 safe :: "room \<Rightarrow> bool" |
|
31 |
|
32 inductive_set reach :: "state set" where |
|
33 init: |
|
34 "inj initk \<Longrightarrow> |
|
35 \<lparr>owns = (\<lambda>r. None), currk = initk, issued = range initk, cards = (\<lambda>g. {}), |
|
36 roomk = initk, isin = (\<lambda>r. {}), safe = (\<lambda>r. True)\<rparr> \<in> reach" | |
|
37 check_in: |
|
38 "\<lbrakk>s \<in> reach; k \<notin> issued s\<rbrakk> \<Longrightarrow> |
|
39 s\<lparr>currk := (currk s)(r := k), issued := issued s \<union> {k}, |
|
40 cards := (cards s)(g := cards s g \<union> {(currk s r, k)}), |
|
41 owns := (owns s)(r := Some g), safe := (safe s)(r := False)\<rparr> \<in> reach" | |
|
42 enter_room: |
|
43 "\<lbrakk>s \<in> reach; (k,k') \<in> cards s g; roomk s r \<in> {k,k'}\<rbrakk> \<Longrightarrow> |
|
44 s\<lparr>isin := (isin s)(r := isin s r \<union> {g}), |
|
45 roomk := (roomk s)(r := k'), |
|
46 safe := (safe s)(r := owns s r = Some g \<and> isin s r = {} (* \<and> k' = currk s r *) |
|
47 \<or> safe s r)\<rparr> \<in> reach" | |
|
48 exit_room: |
|
49 "\<lbrakk>s \<in> reach; g \<in> isin s r\<rbrakk> \<Longrightarrow> s\<lparr>isin := (isin s)(r := isin s r - {g})\<rparr> \<in> reach" |
|
50 |
|
51 theorem safe: "s \<in> reach \<Longrightarrow> safe s r \<Longrightarrow> g \<in> isin s r \<Longrightarrow> owns s r = Some g" |
|
52 nitpick [card room = 1, card guest = 2, card "guest option" = 3, |
|
53 card key = 4, card state = 6, expect = genuine] |
|
54 nitpick [card room = 1, card guest = 2, expect = genuine] |
|
55 oops |
|
56 |
|
57 end |