blanchet@35076: (*  Title:      HOL/Nitpick_Examples/Hotel_Nits.thy
blanchet@35076:     Author:     Jasmin Blanchette, TU Muenchen
blanchet@45035:     Copyright   2010-2011
blanchet@35076: 
blanchet@35076: Nitpick example based on Tobias Nipkow's hotel key card formalization.
blanchet@35076: *)
blanchet@35076: 
blanchet@35076: header {* Nitpick Example Based on Tobias Nipkow's Hotel Key Card
blanchet@35076:           Formalization *}
blanchet@35076: 
blanchet@35076: theory Hotel_Nits
blanchet@35076: imports Main
blanchet@35076: begin
blanchet@35076: 
blanchet@41278: nitpick_params [verbose, max_potential = 0, sat_solver = MiniSat_JNI,
krauss@42208:                 max_threads = 1, timeout = 240]
blanchet@35076: 
blanchet@35076: typedecl guest
blanchet@35076: typedecl key
blanchet@35076: typedecl room
blanchet@35076: 
wenzelm@42463: type_synonym keycard = "key \<times> key"
blanchet@35076: 
blanchet@35076: record state =
blanchet@35076:   owns :: "room \<Rightarrow> guest option"
blanchet@35076:   currk :: "room \<Rightarrow> key"
blanchet@35076:   issued :: "key set"
blanchet@35076:   cards :: "guest \<Rightarrow> keycard set"
blanchet@35076:   roomk :: "room \<Rightarrow> key"
blanchet@35076:   isin :: "room \<Rightarrow> guest set"
blanchet@35076:   safe :: "room \<Rightarrow> bool"
blanchet@35076: 
blanchet@35076: inductive_set reach :: "state set" where
blanchet@35076: init:
blanchet@35076: "inj initk \<Longrightarrow>
blanchet@35076:  \<lparr>owns = (\<lambda>r. None), currk = initk, issued = range initk, cards = (\<lambda>g. {}),
blanchet@35076:   roomk = initk, isin = (\<lambda>r. {}), safe = (\<lambda>r. True)\<rparr> \<in> reach" |
blanchet@35076: check_in:
blanchet@35076: "\<lbrakk>s \<in> reach; k \<notin> issued s\<rbrakk> \<Longrightarrow>
blanchet@35076:  s\<lparr>currk := (currk s)(r := k), issued := issued s \<union> {k},
blanchet@35076:    cards := (cards s)(g := cards s g \<union> {(currk s r, k)}),
blanchet@35076:    owns :=  (owns s)(r := Some g), safe := (safe s)(r := False)\<rparr> \<in> reach" |
blanchet@35076: enter_room:
blanchet@35076: "\<lbrakk>s \<in> reach; (k,k') \<in> cards s g; roomk s r \<in> {k,k'}\<rbrakk> \<Longrightarrow>
blanchet@35076:  s\<lparr>isin := (isin s)(r := isin s r \<union> {g}),
blanchet@35076:    roomk := (roomk s)(r := k'),
blanchet@35076:    safe := (safe s)(r := owns s r = Some g \<and> isin s r = {} (* \<and> k' = currk s r *)
blanchet@35076:                          \<or> safe s r)\<rparr> \<in> reach" |
blanchet@35076: exit_room:
blanchet@35076: "\<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: 
blanchet@35076: theorem safe: "s \<in> reach \<Longrightarrow> safe s r \<Longrightarrow> g \<in> isin s r \<Longrightarrow> owns s r = Some g"
blanchet@35076: nitpick [card room = 1, card guest = 2, card "guest option" = 3,
blanchet@41360:          card key = 4, card state = 6, show_consts, format = 2,
blanchet@41360:          expect = genuine]
blanchet@46082: (* nitpick [card room = 1, card guest = 2, expect = genuine] *) (* slow *)
blanchet@35076: oops
blanchet@35076: 
blanchet@35076: end