src/HOL/Nitpick_Examples/Hotel_Nits.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 35078 6fd1052fe463
child 35284 9edc2bd6d2bd
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
     1 (*  Title:      HOL/Nitpick_Examples/Hotel_Nits.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2010
     4 
     5 Nitpick example based on Tobias Nipkow's hotel key card formalization.
     6 *)
     7 
     8 header {* Nitpick Example Based on Tobias Nipkow's Hotel Key Card
     9           Formalization *}
    10 
    11 theory Hotel_Nits
    12 imports Main
    13 begin
    14 
    15 nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 120 s]
    16 
    17 typedecl guest
    18 typedecl key
    19 typedecl room
    20 
    21 types keycard = "key \<times> key"
    22 
    23 record state =
    24   owns :: "room \<Rightarrow> guest option"
    25   currk :: "room \<Rightarrow> key"
    26   issued :: "key set"
    27   cards :: "guest \<Rightarrow> keycard set"
    28   roomk :: "room \<Rightarrow> key"
    29   isin :: "room \<Rightarrow> guest set"
    30   safe :: "room \<Rightarrow> bool"
    31 
    32 inductive_set reach :: "state set" where
    33 init:
    34 "inj initk \<Longrightarrow>
    35  \<lparr>owns = (\<lambda>r. None), currk = initk, issued = range initk, cards = (\<lambda>g. {}),
    36   roomk = initk, isin = (\<lambda>r. {}), safe = (\<lambda>r. True)\<rparr> \<in> reach" |
    37 check_in:
    38 "\<lbrakk>s \<in> reach; k \<notin> issued s\<rbrakk> \<Longrightarrow>
    39  s\<lparr>currk := (currk s)(r := k), issued := issued s \<union> {k},
    40    cards := (cards s)(g := cards s g \<union> {(currk s r, k)}),
    41    owns :=  (owns s)(r := Some g), safe := (safe s)(r := False)\<rparr> \<in> reach" |
    42 enter_room:
    43 "\<lbrakk>s \<in> reach; (k,k') \<in> cards s g; roomk s r \<in> {k,k'}\<rbrakk> \<Longrightarrow>
    44  s\<lparr>isin := (isin s)(r := isin s r \<union> {g}),
    45    roomk := (roomk s)(r := k'),
    46    safe := (safe s)(r := owns s r = Some g \<and> isin s r = {} (* \<and> k' = currk s r *)
    47                          \<or> safe s r)\<rparr> \<in> reach" |
    48 exit_room:
    49 "\<lbrakk>s \<in> reach; g \<in> isin s r\<rbrakk> \<Longrightarrow> s\<lparr>isin := (isin s)(r := isin s r - {g})\<rparr> \<in> reach"
    50 
    51 theorem safe: "s \<in> reach \<Longrightarrow> safe s r \<Longrightarrow> g \<in> isin s r \<Longrightarrow> owns s r = Some g"
    52 nitpick [card room = 1, card guest = 2, card "guest option" = 3,
    53          card key = 4, card state = 6, expect = genuine]
    54 nitpick [card room = 1, card guest = 2, expect = genuine]
    55 oops
    56 
    57 end