summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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;

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

5 Nitpick example based on Tobias Nipkow's hotel key card formalization.

6 *)

8 header {* Nitpick Example Based on Tobias Nipkow's Hotel Key Card

9 Formalization *}

11 theory Hotel_Nits

12 imports Main

13 begin

15 nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 120 s]

17 typedecl guest

18 typedecl key

19 typedecl room

21 types keycard = "key \<times> key"

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"

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"

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

57 end