# HG changeset patch
# User blanchet
# Date 1265376441 -3600
# Node ID cc19e2aef17e3fb127b427871cebce915f0ca9a6
# Parent  888802be2019ba7c0f2bb996306d5ba60d52a8ac
added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability

diff -r 888802be2019 -r cc19e2aef17e src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Feb 05 12:04:54 2010 +0100
+++ b/src/HOL/IsaMakefile	Fri Feb 05 14:27:21 2010 +0100
@@ -623,12 +623,13 @@
 
 $(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \
   Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \
-  Nitpick_Examples/Induct_Nits.thy Nitpick_Examples/Integer_Nits.thy \
-  Nitpick_Examples/Manual_Nits.thy Nitpick_Examples/Mini_Nits.thy \
-  Nitpick_Examples/Mono_Nits.thy Nitpick_Examples/Nitpick_Examples.thy \
-  Nitpick_Examples/Pattern_Nits.thy Nitpick_Examples/Record_Nits.thy \
-  Nitpick_Examples/Refute_Nits.thy Nitpick_Examples/Special_Nits.thy \
-  Nitpick_Examples/Tests_Nits.thy Nitpick_Examples/Typedef_Nits.thy
+  Nitpick_Examples/Hotel_Nits.thy Nitpick_Examples/Induct_Nits.thy \
+  Nitpick_Examples/Integer_Nits.thy Nitpick_Examples/Manual_Nits.thy \
+  Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \
+  Nitpick_Examples/Nitpick_Examples.thy Nitpick_Examples/Pattern_Nits.thy \
+  Nitpick_Examples/Record_Nits.thy Nitpick_Examples/Refute_Nits.thy \
+  Nitpick_Examples/Special_Nits.thy Nitpick_Examples/Tests_Nits.thy \
+  Nitpick_Examples/Typedef_Nits.thy
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples
 
 
diff -r 888802be2019 -r cc19e2aef17e src/HOL/Nitpick_Examples/Core_Nits.thy
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Nitpick_Examples/Core_Nits.thy
     Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2009
+    Copyright   2009, 2010
 
 Examples featuring Nitpick's functional core.
 *)
diff -r 888802be2019 -r cc19e2aef17e src/HOL/Nitpick_Examples/Datatype_Nits.thy
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Nitpick_Examples/Datatype_Nits.thy
     Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2009
+    Copyright   2009, 2010
 
 Examples featuring Nitpick applied to datatypes.
 *)
diff -r 888802be2019 -r cc19e2aef17e src/HOL/Nitpick_Examples/Hotel_Nits.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
@@ -0,0 +1,57 @@
+(*  Title:      HOL/Nitpick_Examples/Hotel_Nits.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2010
+
+Nitpick example based on Tobias Nipkow's hotel key card formalization.
+*)
+
+header {* Nitpick Example Based on Tobias Nipkow's Hotel Key Card
+          Formalization *}
+
+theory Hotel_Nits
+imports Main
+begin
+
+nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 120 s]
+
+typedecl guest
+typedecl key
+typedecl room
+
+types keycard = "key \<times> key"
+
+record state =
+  owns :: "room \<Rightarrow> guest option"
+  currk :: "room \<Rightarrow> key"
+  issued :: "key set"
+  cards :: "guest \<Rightarrow> keycard set"
+  roomk :: "room \<Rightarrow> key"
+  isin :: "room \<Rightarrow> guest set"
+  safe :: "room \<Rightarrow> bool"
+
+inductive_set reach :: "state set" where
+init:
+"inj initk \<Longrightarrow>
+ \<lparr>owns = (\<lambda>r. None), currk = initk, issued = range initk, cards = (\<lambda>g. {}),
+  roomk = initk, isin = (\<lambda>r. {}), safe = (\<lambda>r. True)\<rparr> \<in> reach" |
+check_in:
+"\<lbrakk>s \<in> reach; k \<notin> issued s\<rbrakk> \<Longrightarrow>
+ s\<lparr>currk := (currk s)(r := k), issued := issued s \<union> {k},
+   cards := (cards s)(g := cards s g \<union> {(currk s r, k)}),
+   owns :=  (owns s)(r := Some g), safe := (safe s)(r := False)\<rparr> \<in> reach" |
+enter_room:
+"\<lbrakk>s \<in> reach; (k,k') \<in> cards s g; roomk s r \<in> {k,k'}\<rbrakk> \<Longrightarrow>
+ s\<lparr>isin := (isin s)(r := isin s r \<union> {g}),
+   roomk := (roomk s)(r := k'),
+   safe := (safe s)(r := owns s r = Some g \<and> isin s r = {} (* \<and> k' = currk s r *)
+                         \<or> safe s r)\<rparr> \<in> reach" |
+exit_room:
+"\<lbrakk>s \<in> reach; g \<in> isin s r\<rbrakk> \<Longrightarrow> s\<lparr>isin := (isin s)(r := isin s r - {g})\<rparr> \<in> reach"
+
+theorem safe: "s \<in> reach \<Longrightarrow> safe s r \<Longrightarrow> g \<in> isin s r \<Longrightarrow> owns s r = Some g"
+nitpick [card room = 1, card guest = 2, card "guest option" = 3,
+         card key = 4, card state = 6, expect = genuine]
+nitpick [card room = 1, card guest = 2, expect = genuine]
+oops
+
+end
diff -r 888802be2019 -r cc19e2aef17e src/HOL/Nitpick_Examples/Induct_Nits.thy
--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Nitpick_Examples/Induct_Nits.thy
     Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2009
+    Copyright   2009, 2010
 
 Examples featuring Nitpick applied to (co)inductive definitions.
 *)
diff -r 888802be2019 -r cc19e2aef17e src/HOL/Nitpick_Examples/Integer_Nits.thy
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Nitpick_Examples/Integer_Nits.thy
     Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2009
+    Copyright   2009, 2010
 
 Examples featuring Nitpick applied to natural numbers and integers.
 *)
diff -r 888802be2019 -r cc19e2aef17e src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Nitpick_Examples/Manual_Nits.thy
     Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2009
+    Copyright   2009, 2010
 
 Examples from the Nitpick manual.
 *)
diff -r 888802be2019 -r cc19e2aef17e src/HOL/Nitpick_Examples/Mini_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mini_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Nitpick_Examples/Mini_Nits.thy
     Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2009
+    Copyright   2009, 2010
 
 Examples featuring Minipick, the minimalistic version of Nitpick.
 *)
diff -r 888802be2019 -r cc19e2aef17e src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Nitpick_Examples/Mono_Nits.thy
     Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2009
+    Copyright   2009, 2010
 
 Examples featuring Nitpick's monotonicity check.
 *)
diff -r 888802be2019 -r cc19e2aef17e src/HOL/Nitpick_Examples/Nitpick_Examples.thy
--- a/src/HOL/Nitpick_Examples/Nitpick_Examples.thy	Fri Feb 05 12:04:54 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Nitpick_Examples.thy	Fri Feb 05 14:27:21 2010 +0100
@@ -1,13 +1,13 @@
 (*  Title:      HOL/Nitpick_Examples/Nitpick_Examples.thy
     Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2009
+    Copyright   2009, 2010
 
 Nitpick examples.
 *)
 
 theory Nitpick_Examples
-imports Core_Nits Datatype_Nits Induct_Nits Integer_Nits Manual_Nits Mini_Nits
-        Mono_Nits Pattern_Nits Record_Nits Refute_Nits Special_Nits Tests_Nits
-        Typedef_Nits
+imports Core_Nits Datatype_Nits Hotel_Nits Induct_Nits Integer_Nits Manual_Nits
+        Mini_Nits Mono_Nits Pattern_Nits Record_Nits Refute_Nits Special_Nits
+        Tests_Nits Typedef_Nits
 begin
 end
diff -r 888802be2019 -r cc19e2aef17e src/HOL/Nitpick_Examples/Pattern_Nits.thy
--- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Nitpick_Examples/Pattern_Nits.thy
     Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2009
+    Copyright   2009, 2010
 
 Examples featuring Nitpick's "destroy_constrs" optimization.
 *)
diff -r 888802be2019 -r cc19e2aef17e src/HOL/Nitpick_Examples/Record_Nits.thy
--- a/src/HOL/Nitpick_Examples/Record_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Nitpick_Examples/Record_Nits.thy
     Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2009
+    Copyright   2009, 2010
 
 Examples featuring Nitpick applied to records.
 *)
diff -r 888802be2019 -r cc19e2aef17e src/HOL/Nitpick_Examples/Refute_Nits.thy
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Nitpick_Examples/Refute_Nits.thy
     Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2009
+    Copyright   2009, 2010
 
 Refute examples adapted to Nitpick.
 *)
diff -r 888802be2019 -r cc19e2aef17e src/HOL/Nitpick_Examples/Special_Nits.thy
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Nitpick_Examples/Special_Nits.thy
     Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2009
+    Copyright   2009, 2010
 
 Examples featuring Nitpick's "specialize" optimization.
 *)
diff -r 888802be2019 -r cc19e2aef17e src/HOL/Nitpick_Examples/Tests_Nits.thy
--- a/src/HOL/Nitpick_Examples/Tests_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Tests_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Nitpick_Examples/Tests_Nits.thy
     Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2009
+    Copyright   2009, 2010
 
 Nitpick tests.
 *)
diff -r 888802be2019 -r cc19e2aef17e src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Nitpick_Examples/Typedef_Nits.thy
     Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2009
+    Copyright   2009, 2010
 
 Examples featuring Nitpick applied to typedefs.
 *)
diff -r 888802be2019 -r cc19e2aef17e src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Feb 05 12:04:54 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Feb 05 14:27:21 2010 +0100
@@ -56,26 +56,36 @@
 val opt_flag = nitpick_prefix ^ "opt"
 val non_opt_flag = nitpick_prefix ^ "non_opt"
 
-(* string -> int -> int -> string *)
-fun nth_atom_suffix s j k =
-  nat_subscript (k - j)
+type atom_pool = ((string * int) * int list) list
+
+(* atom_pool Unsynchronized.ref -> string -> int -> int -> string *)
+fun nth_atom_suffix pool s j k =
+  (case AList.lookup (op =) (!pool) (s, k) of
+     SOME js =>
+     (case find_index (curry (op =) j) js of
+        ~1 => (Unsynchronized.change pool (cons ((s, k), j :: js));
+               length js + 1)
+      | n => length js - n)
+   | NONE => (Unsynchronized.change pool (cons ((s, k), [j])); 1))
+  |> nat_subscript
   |> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
      ? prefix "\<^isub>,"
-(* string -> typ -> int -> int -> string *)
-fun nth_atom_name prefix (T as Type (s, _)) j k =
+(* atom_pool Unsynchronized.ref -> string -> typ -> int -> int -> string *)
+fun nth_atom_name pool prefix (T as Type (s, _)) j k =
     let val s' = shortest_name s in
       prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
-      nth_atom_suffix s j k
+      nth_atom_suffix pool s j k
     end
-  | nth_atom_name prefix (T as TFree (s, _)) j k =
-    prefix ^ perhaps (try (unprefix "'")) s ^ nth_atom_suffix s j k
-  | nth_atom_name _ T _ _ = raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
-(* bool -> typ -> int -> int -> term *)
-fun nth_atom for_auto T j k =
+  | nth_atom_name pool prefix (T as TFree (s, _)) j k =
+    prefix ^ perhaps (try (unprefix "'")) s ^ nth_atom_suffix pool s j k
+  | nth_atom_name _ _ T _ _ =
+    raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
+(* atom_pool Unsynchronized.ref -> bool -> typ -> int -> int -> term *)
+fun nth_atom pool for_auto T j k =
   if for_auto then
-    Free (nth_atom_name (hd (space_explode "." nitpick_prefix)) T j k, T)
+    Free (nth_atom_name pool (hd (space_explode "." nitpick_prefix)) T j k, T)
   else
-    Const (nth_atom_name "" T j k, T)
+    Const (nth_atom_name pool "" T j k, T)
 
 (* term -> real *)
 fun extract_real_number (Const (@{const_name Algebras.divide}, _) $ t1 $ t2) =
@@ -254,6 +264,7 @@
         ({hol_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
          : scope) sel_names rel_table bounds =
   let
+    val pool = Unsynchronized.ref []
     val for_auto = (maybe_name = "")
     (* int list list -> int *)
     fun value_of_bits jss =
@@ -384,15 +395,15 @@
         else if T = @{typ bisim_iterator} then
           HOLogic.mk_number nat_T j
         else case datatype_spec datatypes T of
-          NONE => nth_atom for_auto T j k
-        | SOME {deep = false, ...} => nth_atom for_auto T j k
+          NONE => nth_atom pool for_auto T j k
+        | SOME {deep = false, ...} => nth_atom pool for_auto T j k
         | SOME {co, constrs, ...} =>
           let
             (* styp -> int list *)
             fun tuples_for_const (s, T) =
               tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
             (* unit -> indexname * typ *)
-            fun var () = ((nth_atom_name "" T j k, 0), T)
+            fun var () = ((nth_atom_name pool "" T j k, 0), T)
             val discr_jsss = map (tuples_for_const o discr_for_constr o #const)
                                  constrs
             val real_j = j + offset_of_type ofs T
@@ -731,11 +742,12 @@
                                card_assigns, ...})
                     auto_timeout free_names sel_names rel_table bounds prop =
   let
+    val pool = Unsynchronized.ref []
     (* typ * int -> term *)
     fun free_type_assm (T, k) =
       let
         (* int -> term *)
-        fun atom j = nth_atom true T j k
+        fun atom j = nth_atom pool true T j k
         fun equation_for_atom j = HOLogic.eq_const T $ Bound 0 $ atom j
         val eqs = map equation_for_atom (index_seq 0 k)
         val compreh_assm =