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 \<Rightarrow> 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) \<Rightarrow> {k2} | Enter g r c \<Rightarrow> {} | Exit g r \<Rightarrow> {})"
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 \<Rightarrow> C
| Exit g r \<Rightarrow> 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 \<^cancel>\\ x = k\ then y else k
| Exit g r \<Rightarrow> 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 \<Rightarrow> 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 \<Rightarrow> g \<in> 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\<^sub>1 s\<^sub>2 s\<^sub>3 g c c'.
s = s\<^sub>3 @ [Enter g r c] @ s\<^sub>2 @ [Check_in g r c'] @ s\<^sub>1 \<and>
no_Check_in (s\<^sub>3 @ s\<^sub>2) r \<and> isin (s\<^sub>2 @ [Check_in g r c] @ s\<^sub>1) r = {})"
section \<open>Some setup\<close>
lemma issued_nil: "issued [] = {Key0}"
by (auto simp add: initk_def)
lemmas issued_simps[code, code_pred_def] = issued_nil issued.simps(2)
end
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
