Theory NewCard

(*  Title:      State based hotel key card system with "new card"

    Author:     Tobias Nipkow, TU Muenchen

Like State.thy but with additional features: cards can be lost and new
ones can be issued. Cannot build on State.thy because record state
needs to be extended with a new field. This would require explaining
Isabelle's record inheritance. An interesting project, but not now.
*)

(*<*)
theory NewCard
imports Main
begin

abbreviation
 "SomeFloor" (‹(⌊_⌋)›) where "⌊x⌋ ≡ Some x"

declare if_split_asm[split]

typedecl guest
typedecl key
type_synonym card = "key * key"
typedecl room

record state =
 (* reception: *)
 owns :: "room ⇒ guest option"
 prevk :: "room ⇒ key"
 currk :: "room ⇒ key"
 issued :: "key set"
 (* guests: *)
 cards :: "guest ⇒ card set"
 (* rooms: *)
 roomk :: "room ⇒ key"
 isin :: "room ⇒ guest set"
 (* ghost variable: *)
 safe :: "room ⇒ bool"

inductive_set reach :: "state set"
where
init: (* prevk = arbitrary prevents the invariant prevk : issued *)
"∀r r'. (initk r = initk r') = (r = r') ⟹
⦇ owns = (λr. None), prevk = initk, currk = initk, issued = range initk,
  cards = (λg. {}), roomk = initk, isin = (λr. {}),
  safe = (λr. True) ⦈ ∈ 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 = ⌊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"

| check_in:
"⟦ s : reach; k ∉ issued s ⟧ ⟹
 s⦇currk := (currk s)(r := k), prevk := (prevk s)(r := currk s r),
   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"

| loose_card:
"s : reach ⟹ c : cards s g ⟹
 s⦇cards := (cards s)(g := cards s g - {c})⦈ : reach"

| new_card:
"s : reach ⟹ owns s r = Some g ⟹
 s⦇cards := (cards s)(g := cards s g ∪ {(prevk s r, currk s r)})⦈ : reach"


lemma currk_issued[simp]: "s : reach ⟹ currk s r : issued s"
by (induct set: reach) auto

lemma prevk_issued[simp]: "s : reach ⟹ prevk s r : issued s"
by (induct set: reach) auto

lemma key2_issued[simp]: "s : reach ⟹ (k,k') : cards s g ⟹ k' : issued s"
by (induct set: reach) auto

lemma key1_issued[simp]: "s : reach ⟹ (k,k') : cards s g ⟹ k : issued s"
by (induct set: reach) auto

lemma roomk_issued[simp]: "s : reach ⟹ roomk s k : issued s"
by (induct set: reach) auto

lemma currk_inj[simp]:
 "s : reach ⟹ ∀r r'. (currk s r = currk s r') = (r = r')"
by (induct set: reach) auto

lemma currk_not_prevk[simp]:
 "s : reach ⟹ owns s r' = Some g ⟹ currk s r ≠ prevk s r'"
by (induct set: reach) auto

lemma key1_not_currk[simp]:
 "s : reach ⟹ (currk s r,k') ∉ cards s g"
by (induct set: reach) auto

lemma key2_not_currk:
 "s : reach ⟹ owns s r = Some g ⟹ g ≠ g' ⟹ (k, currk s r) ∉ cards s g'"
by (induct set: reach) auto

lemma guest_key2_disj2[simp]:
"⟦ s : reach; (k⇩1,k) ∈ cards s g⇩1; (k⇩2,k) ∈ cards s g⇩2 ⟧ ⟹ g⇩1=g⇩2"
by (induct set: reach) (auto simp:key2_not_currk)

lemma safe_roomk_currk[simp]:
 "s : reach ⟹ safe s r ⟹ roomk s r = currk s r"
by (induct set: reach) auto

lemma only_owner_enter_normal[simp]:
 "⟦ s : reach; safe s r; (k',roomk s r) ∈ cards s g ⟧ ⟹ owns s r = Some g"
by (induct set: reach) auto

theorem "s : reach ⟹ safe s r ⟹ g : isin s r ⟹ owns s r = Some g"
by (induct set: reach) auto

lemmas new_invs = prevk_issued currk_not_prevk key2_not_currk
(*>*)

subsection‹An extension›

text‹
To test the flexibility of our model we extended it with the
possibility for obtaining a new card, e.g.\ when one has lost one's
card. Now reception needs to remember not just the current but also
the previous key for each room, i.e.\ a new field ‹prevk :: room
⇒ key› is added to @{typ state}. It is initialized with the same value
as @{const currk}: though strictly speaking it could be arbitrary,
this permits the convenient invariant @{prop"prevk s r ∈ issued s"}.
Upon check-in we set ‹prevk› to \mbox{@{term"(prevk s)(r := currk s r)"}}.
Event ‹new_card› is simple enough:
@{thm[display] new_card}

The verification is not seriously affected. Some additional
invariants are required
@{thm[display] new_invs}
but the proofs are still of the same trivial induct-auto format.

Adding a further event for loosing a card has no impact at all on the proofs.
›

(*<*)
end
(*>*)