src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 58310 91ea607a34d8
child 62390 842917225d56
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
bulwahn@38730
     1
theory Hotel_Example
bulwahn@40104
     2
imports Main
bulwahn@38730
     3
begin
bulwahn@38730
     4
blanchet@58310
     5
datatype guest = Guest0 | Guest1
blanchet@58310
     6
datatype key = Key0 | Key1 | Key2 | Key3
blanchet@58310
     7
datatype room = Room0
bulwahn@38730
     8
wenzelm@42463
     9
type_synonym card = "key * key"
bulwahn@38730
    10
blanchet@58310
    11
datatype event =
bulwahn@38730
    12
   Check_in guest room card | Enter guest room card | Exit guest room
bulwahn@38730
    13
bulwahn@38730
    14
definition initk :: "room \<Rightarrow> key"
bulwahn@38730
    15
  where "initk = (%r. Key0)"
bulwahn@38730
    16
bulwahn@38730
    17
declare initk_def[code_pred_def, code]
bulwahn@38730
    18
bulwahn@38730
    19
primrec owns :: "event list \<Rightarrow> room \<Rightarrow> guest option"
bulwahn@38730
    20
where
bulwahn@38730
    21
  "owns [] r = None"
bulwahn@38730
    22
| "owns (e#s) r = (case e of
bulwahn@38730
    23
    Check_in g r' c \<Rightarrow> if r' = r then Some g else owns s r |
bulwahn@38730
    24
    Enter g r' c \<Rightarrow> owns s r |
bulwahn@38730
    25
    Exit g r' \<Rightarrow> owns s r)"
bulwahn@38730
    26
bulwahn@38730
    27
primrec currk :: "event list \<Rightarrow> room \<Rightarrow> key"
bulwahn@38730
    28
where
bulwahn@38730
    29
  "currk [] r = initk r"
bulwahn@38730
    30
| "currk (e#s) r = (let k = currk s r in
bulwahn@38730
    31
    case e of Check_in g r' (k1, k2) \<Rightarrow> if r' = r then k2 else k
bulwahn@38730
    32
            | Enter g r' c \<Rightarrow> k
bulwahn@38730
    33
            | Exit g r \<Rightarrow> k)"
bulwahn@38730
    34
bulwahn@38730
    35
primrec issued :: "event list \<Rightarrow> key set"
bulwahn@38730
    36
where
bulwahn@38730
    37
  "issued [] = range initk"
bulwahn@38730
    38
| "issued (e#s) = issued s \<union>
bulwahn@38730
    39
  (case e of Check_in g r (k1, k2) \<Rightarrow> {k2} | Enter g r c \<Rightarrow> {} | Exit g r \<Rightarrow> {})"
bulwahn@38730
    40
bulwahn@38730
    41
primrec cards :: "event list \<Rightarrow> guest \<Rightarrow> card set"
bulwahn@38730
    42
where
bulwahn@38730
    43
  "cards [] g = {}"
bulwahn@38730
    44
| "cards (e#s) g = (let C = cards s g in
bulwahn@38730
    45
                    case e of Check_in g' r c \<Rightarrow> if g' = g then insert c C
bulwahn@38730
    46
                                                else C
bulwahn@38730
    47
                            | Enter g r c \<Rightarrow> C
bulwahn@38730
    48
                            | Exit g r \<Rightarrow> C)"
bulwahn@38730
    49
bulwahn@38730
    50
primrec roomk :: "event list \<Rightarrow> room \<Rightarrow> key"
bulwahn@38730
    51
where
bulwahn@38730
    52
  "roomk [] r = initk r"
bulwahn@38730
    53
| "roomk (e#s) r = (let k = roomk s r in
bulwahn@38730
    54
    case e of Check_in g r' c \<Rightarrow> k
bulwahn@38730
    55
            | Enter g r' (x,y) \<Rightarrow> if r' = r (*& x = k*) then y else k
bulwahn@38730
    56
            | Exit g r \<Rightarrow> k)"
bulwahn@38730
    57
bulwahn@38730
    58
primrec isin :: "event list \<Rightarrow> room \<Rightarrow> guest set"
bulwahn@38730
    59
where
bulwahn@38730
    60
  "isin [] r = {}"
bulwahn@38730
    61
| "isin (e#s) r = (let G = isin s r in
bulwahn@38730
    62
                 case e of Check_in g r c \<Rightarrow> G
bulwahn@38730
    63
                 | Enter g r' c \<Rightarrow> if r' = r then {g} \<union> G else G
bulwahn@38730
    64
                 | Exit g r' \<Rightarrow> if r'=r then G - {g} else G)"
bulwahn@38730
    65
bulwahn@38730
    66
primrec hotel :: "event list \<Rightarrow> bool"
bulwahn@38730
    67
where
bulwahn@38730
    68
  "hotel []  = True"
bulwahn@38730
    69
| "hotel (e # s) = (hotel s & (case e of
bulwahn@38730
    70
  Check_in g r (k,k') \<Rightarrow> k = currk s r \<and> k' \<notin> issued s |
bulwahn@38730
    71
  Enter g r (k,k') \<Rightarrow> (k,k') : cards s g & (roomk s r : {k, k'}) |
bulwahn@38734
    72
  Exit g r \<Rightarrow> g : isin s r))"
bulwahn@38730
    73
bulwahn@38953
    74
definition no_Check_in :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*)
bulwahn@38953
    75
[code del]: "no_Check_in s r \<equiv> \<not>(\<exists>g c. Check_in g r c \<in> set s)"
bulwahn@38953
    76
bulwahn@38953
    77
definition feels_safe :: "event list \<Rightarrow> room \<Rightarrow> bool"
bulwahn@38953
    78
where
wenzelm@53015
    79
  "feels_safe s r = (\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 g c c'.
wenzelm@53015
    80
   s = s\<^sub>3 @ [Enter g r c] @ s\<^sub>2 @ [Check_in g r c'] @ s\<^sub>1 \<and>
wenzelm@53015
    81
   no_Check_in (s\<^sub>3 @ s\<^sub>2) r \<and> isin (s\<^sub>2 @ [Check_in g r c] @ s\<^sub>1) r = {})"
bulwahn@38953
    82
bulwahn@39799
    83
bulwahn@40104
    84
section {* Some setup *}
bulwahn@39799
    85
bulwahn@40104
    86
lemma issued_nil: "issued [] = {Key0}"
bulwahn@40104
    87
by (auto simp add: initk_def)
bulwahn@39799
    88
bulwahn@40104
    89
lemmas issued_simps[code, code_pred_def] = issued_nil issued.simps(2)
bulwahn@39799
    90
bulwahn@38730
    91
end