Theory Hotel_Example

theory Hotel_Example
imports Main
begin

datatype guest = Guest0 | Guest1
datatype key = Key0 | Key1 | Key2 | Key3
datatype room = Room0

type_synonym card = "key * key"

datatype event =
   Check_in guest room card | Enter guest room card | Exit guest room

definition initk :: "room ⇒ key"
  where "initk = (%r. Key0)"

declare initk_def[code_pred_def, code]

primrec owns :: "event list ⇒ room ⇒ guest option"
where
  "owns [] r = None"
| "owns (e#s) r = (case e of
    Check_in g r' c ⇒ if r' = r then Some g else owns s r |
    Enter g r' c ⇒ owns s r |
    Exit g r' ⇒ owns s r)"

primrec currk :: "event list ⇒ room ⇒ key"
where
  "currk [] r = initk r"
| "currk (e#s) r = (let k = currk s r in
    case e of Check_in g r' (k1, k2) ⇒ if r' = r then k2 else k
            | Enter g r' c ⇒ k
            | Exit g r ⇒ k)"

primrec issued :: "event list ⇒ key set"
where
  "issued [] = range initk"
| "issued (e#s) = issued s ∪
  (case e of Check_in g r (k1, k2) ⇒ {k2} | Enter g r c ⇒ {} | Exit g r ⇒ {})"

primrec cards :: "event list ⇒ guest ⇒ card set"
where
  "cards [] g = {}"
| "cards (e#s) g = (let C = cards s g in
                    case e of Check_in g' r c ⇒ if g' = g then insert c C
                                                else C
                            | Enter g r c ⇒ C
                            | Exit g r ⇒ C)"

primrec roomk :: "event list ⇒ room ⇒ key"
where
  "roomk [] r = initk r"
| "roomk (e#s) r = (let k = roomk s r in
    case e of Check_in g r' c ⇒ k
            | Enter g r' (x,y) ⇒ if r' = r ⌦‹∧ x = k› then y else k
            | Exit g r ⇒ k)"

primrec isin :: "event list ⇒ room ⇒ guest set"
where
  "isin [] r = {}"
| "isin (e#s) r = (let G = isin s r in
                 case e of Check_in g r c ⇒ G
                 | Enter g r' c ⇒ if r' = r then {g} ∪ G else G
                 | Exit g r' ⇒ if r'=r then G - {g} else G)"

primrec hotel :: "event list ⇒ bool"
where
  "hotel []  = True"
| "hotel (e # s) = (hotel s ∧ (case e of
  Check_in g r (k,k') ⇒ k = currk s r ∧ k' ∉ issued s |
  Enter g r (k,k') ⇒ (k,k') ∈ cards s g ∧ (roomk s r ∈ {k, k'}) |
  Exit g r ⇒ g ∈ isin s r))"

definition no_Check_in :: "event list ⇒ room ⇒ bool" where(*>*)
[code del]: "no_Check_in s r ≡ ¬(∃g c. Check_in g r c ∈ set s)"

definition feels_safe :: "event list ⇒ room ⇒ bool"
where
  "feels_safe s r = (∃s⇩1 s⇩2 s⇩3 g c c'.
   s = s⇩3 @ [Enter g r c] @ s⇩2 @ [Check_in g r c'] @ s⇩1 ∧
   no_Check_in (s⇩3 @ s⇩2) r ∧ isin (s⇩2 @ [Check_in g r c] @ s⇩1) r = {})"


section ‹Some setup›

lemma issued_nil: "issued [] = {Key0}"
by (auto simp add: initk_def)

lemmas issued_simps [code, code_pred_def] = issued_nil issued.simps(2)

end