added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
authorblanchet
Fri Feb 05 14:27:21 2010 +0100 (2010-02-05)
changeset 35076cc19e2aef17e
parent 35075 888802be2019
child 35077 c1dac8ace020
added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
src/HOL/IsaMakefile
src/HOL/Nitpick_Examples/Core_Nits.thy
src/HOL/Nitpick_Examples/Datatype_Nits.thy
src/HOL/Nitpick_Examples/Hotel_Nits.thy
src/HOL/Nitpick_Examples/Induct_Nits.thy
src/HOL/Nitpick_Examples/Integer_Nits.thy
src/HOL/Nitpick_Examples/Manual_Nits.thy
src/HOL/Nitpick_Examples/Mini_Nits.thy
src/HOL/Nitpick_Examples/Mono_Nits.thy
src/HOL/Nitpick_Examples/Nitpick_Examples.thy
src/HOL/Nitpick_Examples/Pattern_Nits.thy
src/HOL/Nitpick_Examples/Record_Nits.thy
src/HOL/Nitpick_Examples/Refute_Nits.thy
src/HOL/Nitpick_Examples/Special_Nits.thy
src/HOL/Nitpick_Examples/Tests_Nits.thy
src/HOL/Nitpick_Examples/Typedef_Nits.thy
src/HOL/Tools/Nitpick/nitpick_model.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Feb 05 12:04:54 2010 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Feb 05 14:27:21 2010 +0100
     1.3 @@ -623,12 +623,13 @@
     1.4  
     1.5  $(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \
     1.6    Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \
     1.7 -  Nitpick_Examples/Induct_Nits.thy Nitpick_Examples/Integer_Nits.thy \
     1.8 -  Nitpick_Examples/Manual_Nits.thy Nitpick_Examples/Mini_Nits.thy \
     1.9 -  Nitpick_Examples/Mono_Nits.thy Nitpick_Examples/Nitpick_Examples.thy \
    1.10 -  Nitpick_Examples/Pattern_Nits.thy Nitpick_Examples/Record_Nits.thy \
    1.11 -  Nitpick_Examples/Refute_Nits.thy Nitpick_Examples/Special_Nits.thy \
    1.12 -  Nitpick_Examples/Tests_Nits.thy Nitpick_Examples/Typedef_Nits.thy
    1.13 +  Nitpick_Examples/Hotel_Nits.thy Nitpick_Examples/Induct_Nits.thy \
    1.14 +  Nitpick_Examples/Integer_Nits.thy Nitpick_Examples/Manual_Nits.thy \
    1.15 +  Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \
    1.16 +  Nitpick_Examples/Nitpick_Examples.thy Nitpick_Examples/Pattern_Nits.thy \
    1.17 +  Nitpick_Examples/Record_Nits.thy Nitpick_Examples/Refute_Nits.thy \
    1.18 +  Nitpick_Examples/Special_Nits.thy Nitpick_Examples/Tests_Nits.thy \
    1.19 +  Nitpick_Examples/Typedef_Nits.thy
    1.20  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples
    1.21  
    1.22  
     2.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
     2.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
     2.3 @@ -1,6 +1,6 @@
     2.4  (*  Title:      HOL/Nitpick_Examples/Core_Nits.thy
     2.5      Author:     Jasmin Blanchette, TU Muenchen
     2.6 -    Copyright   2009
     2.7 +    Copyright   2009, 2010
     2.8  
     2.9  Examples featuring Nitpick's functional core.
    2.10  *)
     3.1 --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
     3.2 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
     3.3 @@ -1,6 +1,6 @@
     3.4  (*  Title:      HOL/Nitpick_Examples/Datatype_Nits.thy
     3.5      Author:     Jasmin Blanchette, TU Muenchen
     3.6 -    Copyright   2009
     3.7 +    Copyright   2009, 2010
     3.8  
     3.9  Examples featuring Nitpick applied to datatypes.
    3.10  *)
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
     4.3 @@ -0,0 +1,57 @@
     4.4 +(*  Title:      HOL/Nitpick_Examples/Hotel_Nits.thy
     4.5 +    Author:     Jasmin Blanchette, TU Muenchen
     4.6 +    Copyright   2010
     4.7 +
     4.8 +Nitpick example based on Tobias Nipkow's hotel key card formalization.
     4.9 +*)
    4.10 +
    4.11 +header {* Nitpick Example Based on Tobias Nipkow's Hotel Key Card
    4.12 +          Formalization *}
    4.13 +
    4.14 +theory Hotel_Nits
    4.15 +imports Main
    4.16 +begin
    4.17 +
    4.18 +nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 120 s]
    4.19 +
    4.20 +typedecl guest
    4.21 +typedecl key
    4.22 +typedecl room
    4.23 +
    4.24 +types keycard = "key \<times> key"
    4.25 +
    4.26 +record state =
    4.27 +  owns :: "room \<Rightarrow> guest option"
    4.28 +  currk :: "room \<Rightarrow> key"
    4.29 +  issued :: "key set"
    4.30 +  cards :: "guest \<Rightarrow> keycard set"
    4.31 +  roomk :: "room \<Rightarrow> key"
    4.32 +  isin :: "room \<Rightarrow> guest set"
    4.33 +  safe :: "room \<Rightarrow> bool"
    4.34 +
    4.35 +inductive_set reach :: "state set" where
    4.36 +init:
    4.37 +"inj initk \<Longrightarrow>
    4.38 + \<lparr>owns = (\<lambda>r. None), currk = initk, issued = range initk, cards = (\<lambda>g. {}),
    4.39 +  roomk = initk, isin = (\<lambda>r. {}), safe = (\<lambda>r. True)\<rparr> \<in> reach" |
    4.40 +check_in:
    4.41 +"\<lbrakk>s \<in> reach; k \<notin> issued s\<rbrakk> \<Longrightarrow>
    4.42 + s\<lparr>currk := (currk s)(r := k), issued := issued s \<union> {k},
    4.43 +   cards := (cards s)(g := cards s g \<union> {(currk s r, k)}),
    4.44 +   owns :=  (owns s)(r := Some g), safe := (safe s)(r := False)\<rparr> \<in> reach" |
    4.45 +enter_room:
    4.46 +"\<lbrakk>s \<in> reach; (k,k') \<in> cards s g; roomk s r \<in> {k,k'}\<rbrakk> \<Longrightarrow>
    4.47 + s\<lparr>isin := (isin s)(r := isin s r \<union> {g}),
    4.48 +   roomk := (roomk s)(r := k'),
    4.49 +   safe := (safe s)(r := owns s r = Some g \<and> isin s r = {} (* \<and> k' = currk s r *)
    4.50 +                         \<or> safe s r)\<rparr> \<in> reach" |
    4.51 +exit_room:
    4.52 +"\<lbrakk>s \<in> reach; g \<in> isin s r\<rbrakk> \<Longrightarrow> s\<lparr>isin := (isin s)(r := isin s r - {g})\<rparr> \<in> reach"
    4.53 +
    4.54 +theorem safe: "s \<in> reach \<Longrightarrow> safe s r \<Longrightarrow> g \<in> isin s r \<Longrightarrow> owns s r = Some g"
    4.55 +nitpick [card room = 1, card guest = 2, card "guest option" = 3,
    4.56 +         card key = 4, card state = 6, expect = genuine]
    4.57 +nitpick [card room = 1, card guest = 2, expect = genuine]
    4.58 +oops
    4.59 +
    4.60 +end
     5.1 --- a/src/HOL/Nitpick_Examples/Induct_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
     5.2 +++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
     5.3 @@ -1,6 +1,6 @@
     5.4  (*  Title:      HOL/Nitpick_Examples/Induct_Nits.thy
     5.5      Author:     Jasmin Blanchette, TU Muenchen
     5.6 -    Copyright   2009
     5.7 +    Copyright   2009, 2010
     5.8  
     5.9  Examples featuring Nitpick applied to (co)inductive definitions.
    5.10  *)
     6.1 --- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
     6.2 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
     6.3 @@ -1,6 +1,6 @@
     6.4  (*  Title:      HOL/Nitpick_Examples/Integer_Nits.thy
     6.5      Author:     Jasmin Blanchette, TU Muenchen
     6.6 -    Copyright   2009
     6.7 +    Copyright   2009, 2010
     6.8  
     6.9  Examples featuring Nitpick applied to natural numbers and integers.
    6.10  *)
     7.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
     7.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
     7.3 @@ -1,6 +1,6 @@
     7.4  (*  Title:      HOL/Nitpick_Examples/Manual_Nits.thy
     7.5      Author:     Jasmin Blanchette, TU Muenchen
     7.6 -    Copyright   2009
     7.7 +    Copyright   2009, 2010
     7.8  
     7.9  Examples from the Nitpick manual.
    7.10  *)
     8.1 --- a/src/HOL/Nitpick_Examples/Mini_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
     8.2 +++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
     8.3 @@ -1,6 +1,6 @@
     8.4  (*  Title:      HOL/Nitpick_Examples/Mini_Nits.thy
     8.5      Author:     Jasmin Blanchette, TU Muenchen
     8.6 -    Copyright   2009
     8.7 +    Copyright   2009, 2010
     8.8  
     8.9  Examples featuring Minipick, the minimalistic version of Nitpick.
    8.10  *)
     9.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
     9.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
     9.3 @@ -1,6 +1,6 @@
     9.4  (*  Title:      HOL/Nitpick_Examples/Mono_Nits.thy
     9.5      Author:     Jasmin Blanchette, TU Muenchen
     9.6 -    Copyright   2009
     9.7 +    Copyright   2009, 2010
     9.8  
     9.9  Examples featuring Nitpick's monotonicity check.
    9.10  *)
    10.1 --- a/src/HOL/Nitpick_Examples/Nitpick_Examples.thy	Fri Feb 05 12:04:54 2010 +0100
    10.2 +++ b/src/HOL/Nitpick_Examples/Nitpick_Examples.thy	Fri Feb 05 14:27:21 2010 +0100
    10.3 @@ -1,13 +1,13 @@
    10.4  (*  Title:      HOL/Nitpick_Examples/Nitpick_Examples.thy
    10.5      Author:     Jasmin Blanchette, TU Muenchen
    10.6 -    Copyright   2009
    10.7 +    Copyright   2009, 2010
    10.8  
    10.9  Nitpick examples.
   10.10  *)
   10.11  
   10.12  theory Nitpick_Examples
   10.13 -imports Core_Nits Datatype_Nits Induct_Nits Integer_Nits Manual_Nits Mini_Nits
   10.14 -        Mono_Nits Pattern_Nits Record_Nits Refute_Nits Special_Nits Tests_Nits
   10.15 -        Typedef_Nits
   10.16 +imports Core_Nits Datatype_Nits Hotel_Nits Induct_Nits Integer_Nits Manual_Nits
   10.17 +        Mini_Nits Mono_Nits Pattern_Nits Record_Nits Refute_Nits Special_Nits
   10.18 +        Tests_Nits Typedef_Nits
   10.19  begin
   10.20  end
    11.1 --- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
    11.2 +++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
    11.3 @@ -1,6 +1,6 @@
    11.4  (*  Title:      HOL/Nitpick_Examples/Pattern_Nits.thy
    11.5      Author:     Jasmin Blanchette, TU Muenchen
    11.6 -    Copyright   2009
    11.7 +    Copyright   2009, 2010
    11.8  
    11.9  Examples featuring Nitpick's "destroy_constrs" optimization.
   11.10  *)
    12.1 --- a/src/HOL/Nitpick_Examples/Record_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
    12.2 +++ b/src/HOL/Nitpick_Examples/Record_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
    12.3 @@ -1,6 +1,6 @@
    12.4  (*  Title:      HOL/Nitpick_Examples/Record_Nits.thy
    12.5      Author:     Jasmin Blanchette, TU Muenchen
    12.6 -    Copyright   2009
    12.7 +    Copyright   2009, 2010
    12.8  
    12.9  Examples featuring Nitpick applied to records.
   12.10  *)
    13.1 --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
    13.2 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
    13.3 @@ -1,6 +1,6 @@
    13.4  (*  Title:      HOL/Nitpick_Examples/Refute_Nits.thy
    13.5      Author:     Jasmin Blanchette, TU Muenchen
    13.6 -    Copyright   2009
    13.7 +    Copyright   2009, 2010
    13.8  
    13.9  Refute examples adapted to Nitpick.
   13.10  *)
    14.1 --- a/src/HOL/Nitpick_Examples/Special_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
    14.2 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
    14.3 @@ -1,6 +1,6 @@
    14.4  (*  Title:      HOL/Nitpick_Examples/Special_Nits.thy
    14.5      Author:     Jasmin Blanchette, TU Muenchen
    14.6 -    Copyright   2009
    14.7 +    Copyright   2009, 2010
    14.8  
    14.9  Examples featuring Nitpick's "specialize" optimization.
   14.10  *)
    15.1 --- a/src/HOL/Nitpick_Examples/Tests_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
    15.2 +++ b/src/HOL/Nitpick_Examples/Tests_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
    15.3 @@ -1,6 +1,6 @@
    15.4  (*  Title:      HOL/Nitpick_Examples/Tests_Nits.thy
    15.5      Author:     Jasmin Blanchette, TU Muenchen
    15.6 -    Copyright   2009
    15.7 +    Copyright   2009, 2010
    15.8  
    15.9  Nitpick tests.
   15.10  *)
    16.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Feb 05 12:04:54 2010 +0100
    16.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Feb 05 14:27:21 2010 +0100
    16.3 @@ -1,6 +1,6 @@
    16.4  (*  Title:      HOL/Nitpick_Examples/Typedef_Nits.thy
    16.5      Author:     Jasmin Blanchette, TU Muenchen
    16.6 -    Copyright   2009
    16.7 +    Copyright   2009, 2010
    16.8  
    16.9  Examples featuring Nitpick applied to typedefs.
   16.10  *)
    17.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Feb 05 12:04:54 2010 +0100
    17.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Feb 05 14:27:21 2010 +0100
    17.3 @@ -56,26 +56,36 @@
    17.4  val opt_flag = nitpick_prefix ^ "opt"
    17.5  val non_opt_flag = nitpick_prefix ^ "non_opt"
    17.6  
    17.7 -(* string -> int -> int -> string *)
    17.8 -fun nth_atom_suffix s j k =
    17.9 -  nat_subscript (k - j)
   17.10 +type atom_pool = ((string * int) * int list) list
   17.11 +
   17.12 +(* atom_pool Unsynchronized.ref -> string -> int -> int -> string *)
   17.13 +fun nth_atom_suffix pool s j k =
   17.14 +  (case AList.lookup (op =) (!pool) (s, k) of
   17.15 +     SOME js =>
   17.16 +     (case find_index (curry (op =) j) js of
   17.17 +        ~1 => (Unsynchronized.change pool (cons ((s, k), j :: js));
   17.18 +               length js + 1)
   17.19 +      | n => length js - n)
   17.20 +   | NONE => (Unsynchronized.change pool (cons ((s, k), [j])); 1))
   17.21 +  |> nat_subscript
   17.22    |> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
   17.23       ? prefix "\<^isub>,"
   17.24 -(* string -> typ -> int -> int -> string *)
   17.25 -fun nth_atom_name prefix (T as Type (s, _)) j k =
   17.26 +(* atom_pool Unsynchronized.ref -> string -> typ -> int -> int -> string *)
   17.27 +fun nth_atom_name pool prefix (T as Type (s, _)) j k =
   17.28      let val s' = shortest_name s in
   17.29        prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
   17.30 -      nth_atom_suffix s j k
   17.31 +      nth_atom_suffix pool s j k
   17.32      end
   17.33 -  | nth_atom_name prefix (T as TFree (s, _)) j k =
   17.34 -    prefix ^ perhaps (try (unprefix "'")) s ^ nth_atom_suffix s j k
   17.35 -  | nth_atom_name _ T _ _ = raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
   17.36 -(* bool -> typ -> int -> int -> term *)
   17.37 -fun nth_atom for_auto T j k =
   17.38 +  | nth_atom_name pool prefix (T as TFree (s, _)) j k =
   17.39 +    prefix ^ perhaps (try (unprefix "'")) s ^ nth_atom_suffix pool s j k
   17.40 +  | nth_atom_name _ _ T _ _ =
   17.41 +    raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
   17.42 +(* atom_pool Unsynchronized.ref -> bool -> typ -> int -> int -> term *)
   17.43 +fun nth_atom pool for_auto T j k =
   17.44    if for_auto then
   17.45 -    Free (nth_atom_name (hd (space_explode "." nitpick_prefix)) T j k, T)
   17.46 +    Free (nth_atom_name pool (hd (space_explode "." nitpick_prefix)) T j k, T)
   17.47    else
   17.48 -    Const (nth_atom_name "" T j k, T)
   17.49 +    Const (nth_atom_name pool "" T j k, T)
   17.50  
   17.51  (* term -> real *)
   17.52  fun extract_real_number (Const (@{const_name Algebras.divide}, _) $ t1 $ t2) =
   17.53 @@ -254,6 +264,7 @@
   17.54          ({hol_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
   17.55           : scope) sel_names rel_table bounds =
   17.56    let
   17.57 +    val pool = Unsynchronized.ref []
   17.58      val for_auto = (maybe_name = "")
   17.59      (* int list list -> int *)
   17.60      fun value_of_bits jss =
   17.61 @@ -384,15 +395,15 @@
   17.62          else if T = @{typ bisim_iterator} then
   17.63            HOLogic.mk_number nat_T j
   17.64          else case datatype_spec datatypes T of
   17.65 -          NONE => nth_atom for_auto T j k
   17.66 -        | SOME {deep = false, ...} => nth_atom for_auto T j k
   17.67 +          NONE => nth_atom pool for_auto T j k
   17.68 +        | SOME {deep = false, ...} => nth_atom pool for_auto T j k
   17.69          | SOME {co, constrs, ...} =>
   17.70            let
   17.71              (* styp -> int list *)
   17.72              fun tuples_for_const (s, T) =
   17.73                tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
   17.74              (* unit -> indexname * typ *)
   17.75 -            fun var () = ((nth_atom_name "" T j k, 0), T)
   17.76 +            fun var () = ((nth_atom_name pool "" T j k, 0), T)
   17.77              val discr_jsss = map (tuples_for_const o discr_for_constr o #const)
   17.78                                   constrs
   17.79              val real_j = j + offset_of_type ofs T
   17.80 @@ -731,11 +742,12 @@
   17.81                                 card_assigns, ...})
   17.82                      auto_timeout free_names sel_names rel_table bounds prop =
   17.83    let
   17.84 +    val pool = Unsynchronized.ref []
   17.85      (* typ * int -> term *)
   17.86      fun free_type_assm (T, k) =
   17.87        let
   17.88          (* int -> term *)
   17.89 -        fun atom j = nth_atom true T j k
   17.90 +        fun atom j = nth_atom pool true T j k
   17.91          fun equation_for_atom j = HOLogic.eq_const T $ Bound 0 $ atom j
   17.92          val eqs = map equation_for_atom (index_seq 0 k)
   17.93          val compreh_assm =