(*  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') ==>
\<lparr> 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₁,k) ∈ cards s g₁; (k₂,k) ∈ cards s g₂ ] ==> g₁=g₂"
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‹
  test the flexibility of our model we extended it with the
  for obtaining a new card, e.g.\ when one has lost one's
 . Now reception needs to remember not just the current but also
  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
  @{const currk}: though strictly speaking it could be arbitrary,
  permits the convenient invariant @{prop"prevk s r ∈ issued s"}.
  check-in we set ‹prevk› to \mbox{@{term"(prevk s)(r := currk s r)"}}.
  ‹new_card› is simple enough:
 {thm[display] new_card}

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

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

(*<*)
end
(*>*)