Theory NewCard

(*  Title:      State based hotel key card system with "new card"
    ID:         $Id: NewCard.thy,v 1.3 2007-07-11 10:14:40 stefanberghofer Exp $
    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 split_if_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\<^isub>1,k) ∈ cards s g\<^isub>1; (k\<^isub>2,k) ∈ cards s g\<^isub>2 |] ==> g\<^isub>1=g\<^isub>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 @{text"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 @{text prevk} to \mbox{@{term"(prevk s)(r := currk s r)"}}.
Event @{text 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
(*>*)