# Theory Hotel_Nits

theory Hotel_Nits
imports Main
```(*  Title:      HOL/Nitpick_Examples/Hotel_Nits.thy
Author:     Jasmin Blanchette, TU Muenchen
Copyright   2010-2011

Nitpick example based on Tobias Nipkow's hotel key card formalization.
*)

section ‹Nitpick Example Based on Tobias Nipkow's Hotel Key Card
Formalization›

theory Hotel_Nits
imports Main
begin

nitpick_params [verbose, max_potential = 0, sat_solver = MiniSat_JNI,
max_threads = 1, timeout = 240]

typedecl guest
typedecl key
typedecl room

type_synonym keycard = "key × key"

record state =
owns :: "room ⇒ guest option"
currk :: "room ⇒ key"
issued :: "key set"
cards :: "guest ⇒ keycard set"
roomk :: "room ⇒ key"
isin :: "room ⇒ guest set"
safe :: "room ⇒ bool"

inductive_set reach :: "state set" where
init:
"inj initk ⟹
⦇owns = (λr. None), currk = initk, issued = range initk, cards = (λg. {}),
roomk = initk, isin = (λr. {}), safe = (λr. True)⦈ ∈ reach" |
check_in:
"⟦s ∈ reach; k ∉ issued s⟧ ⟹
s⦇currk := (currk s)(r := k), issued := issued s ∪ {k},
cards := (cards s)(g := cards s g ∪ {(currk s r, k)}),
owns :=  (owns s)(r := Some g), safe := (safe s)(r := False)⦈ ∈ reach" |
enter_room:
"⟦s ∈ reach; (k,k') ∈ cards s g; roomk s r ∈ {k,k'}⟧ ⟹
s⦇isin := (isin s)(r := isin s r ∪ {g}),
roomk := (roomk s)(r := k'),
safe := (safe s)(r := owns s r = Some g ∧ isin s r = {} (* ∧ k' = currk s r *)
∨ safe s r)⦈ ∈ reach" |
exit_room:
"⟦s ∈ reach; g ∈ isin s r⟧ ⟹ s⦇isin := (isin s)(r := isin s r - {g})⦈ ∈ reach"

theorem safe: "s ∈ reach ⟹ safe s r ⟹ g ∈ isin s r ⟹ owns s r = Some g"
nitpick [card room = 1, card guest = 2, card "guest option" = 3,
card key = 4, card state = 6, show_consts, format = 2,
expect = genuine]
(* nitpick [card room = 1, card guest = 2, expect = genuine] *) (* slow *)
oops

end
```