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