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