# HG changeset patch
# User blanchet
# Date 1265367894 -3600
# Node ID 888802be2019ba7c0f2bb996306d5ba60d52a8ac
# Parent  a886420664483951a08490f724991820dfd73076
handle Nitpick's nonstandard model enumeration in a cleaner way;
and renumber the atoms so that we get more often a_1 and a_2
and less often a_{n-1} and a_{n-2} in counterexamples

diff -r a88642066448 -r 888802be2019 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Feb 05 11:24:53 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Feb 05 12:04:54 2010 +0100
@@ -339,7 +339,7 @@
     fun is_type_always_monotonic T =
       (is_datatype thy T andalso not (is_quot_type thy T) andalso
        (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
-      is_number_type thy T orelse is_bit_type T orelse T = @{typ \<xi>}
+      is_number_type thy T orelse is_bit_type T
     fun is_type_monotonic T =
       unique_scope orelse
       case triple_lookup (type_match thy) monos T of
diff -r a88642066448 -r 888802be2019 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Feb 05 11:24:53 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Feb 05 12:04:54 2010 +0100
@@ -940,6 +940,10 @@
       | _ => list_comb (Const x, args)
     end
 
+(* The higher this number is, the more nonstandard models can be generated. It's
+   not important enough to be a user option, though. *)
+val xi_card = 8
+
 (* (typ * int) list -> typ -> int *)
 fun card_of_type assigns (Type ("fun", [T1, T2])) =
     reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
@@ -949,6 +953,7 @@
   | card_of_type _ @{typ prop} = 2
   | card_of_type _ @{typ bool} = 2
   | card_of_type _ @{typ unit} = 1
+  | card_of_type _ @{typ \<xi>} = xi_card
   | card_of_type assigns T =
     case AList.lookup (op =) assigns T of
       SOME k => k
@@ -1005,6 +1010,7 @@
        | @{typ prop} => 2
        | @{typ bool} => 2
        | @{typ unit} => 1
+       | @{typ \<xi>} => xi_card
        | Type _ =>
          (case datatype_constrs hol_ctxt T of
             [] => if is_integer_type T orelse is_bit_type T then 0
@@ -2009,7 +2015,8 @@
   | Type ("*", Ts) => fold (add_ground_types hol_ctxt) Ts accum
   | Type (@{type_name itself}, [T1]) => add_ground_types hol_ctxt T1 accum
   | Type (_, Ts) =>
-    if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) T then
+    if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} ::
+                      @{typ \<xi>} :: accum) T then
       accum
     else
       T :: accum
diff -r a88642066448 -r 888802be2019 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Feb 05 11:24:53 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Feb 05 12:04:54 2010 +0100
@@ -56,26 +56,26 @@
 val opt_flag = nitpick_prefix ^ "opt"
 val non_opt_flag = nitpick_prefix ^ "non_opt"
 
-(* string -> int -> string *)
-fun atom_suffix s j =
-  nat_subscript (j + 1)
+(* string -> int -> int -> string *)
+fun nth_atom_suffix s j k =
+  nat_subscript (k - j)
   |> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
      ? prefix "\<^isub>,"
-(* string -> typ -> int -> string *)
-fun atom_name prefix (T as Type (s, _)) j =
+(* string -> typ -> int -> int -> string *)
+fun nth_atom_name 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)) ^
-      atom_suffix s j
+      nth_atom_suffix s j k
     end
-  | atom_name prefix (T as TFree (s, _)) j =
-    prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s j
-  | atom_name _ T _ = raise TYPE ("Nitpick_Model.atom_name", [T], [])
-(* bool -> typ -> int -> term *)
-fun atom for_auto T j =
+  | 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 =
   if for_auto then
-    Free (atom_name (hd (space_explode "." nitpick_prefix)) T j, T)
+    Free (nth_atom_name (hd (space_explode "." nitpick_prefix)) T j k, T)
   else
-    Const (atom_name "" T j, T)
+    Const (nth_atom_name "" T j k, T)
 
 (* term -> real *)
 fun extract_real_number (Const (@{const_name Algebras.divide}, _) $ t1 $ t2) =
@@ -348,7 +348,7 @@
                                  (unbit_and_unbox_type T1)
                                  (unbit_and_unbox_type T2)
     (* (typ * int) list -> typ -> typ -> int -> term *)
-    fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j =
+    fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j k =
         let
           val k1 = card_of_type card_assigns T1
           val k2 = card_of_type card_assigns T2
@@ -360,37 +360,39 @@
                             signed_string_of_int j ^ " for " ^
                             string_for_rep (Vect (k1, Atom (k2, 0))))
         end
-      | term_for_atom seen (Type ("*", [T1, T2])) _ j =
-        let val k1 = card_of_type card_assigns T1 in
+      | term_for_atom seen (Type ("*", [T1, T2])) _ j k =
+        let
+          val k1 = card_of_type card_assigns T1
+          val k2 = k div k1
+        in
           list_comb (HOLogic.pair_const T1 T2,
-                     map2 (fn T => term_for_atom seen T T) [T1, T2]
-                          [j div k1, j mod k1])
+                     map3 (fn T => term_for_atom seen T T) [T1, T2]
+                          [j div k2, j mod k2] [k1, k2]) (* ### k2 or k1? FIXME *)
         end
-      | term_for_atom seen @{typ prop} _ j =
-        HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j)
-      | term_for_atom _ @{typ bool} _ j =
+      | term_for_atom seen @{typ prop} _ j k =
+        HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j k)
+      | term_for_atom _ @{typ bool} _ j _ =
         if j = 0 then @{const False} else @{const True}
-      | term_for_atom _ @{typ unit} _ _ = @{const Unity}
-      | term_for_atom seen T _ j =
+      | term_for_atom _ @{typ unit} _ _ _ = @{const Unity}
+      | term_for_atom seen T _ j k =
         if T = nat_T then
           HOLogic.mk_number nat_T j
         else if T = int_T then
-          HOLogic.mk_number int_T
-              (int_for_atom (card_of_type card_assigns int_T, 0) j)
+          HOLogic.mk_number int_T (int_for_atom (k, 0) j)
         else if is_fp_iterator_type T then
-          HOLogic.mk_number nat_T (card_of_type card_assigns T - j - 1)
+          HOLogic.mk_number nat_T (k - j - 1)
         else if T = @{typ bisim_iterator} then
           HOLogic.mk_number nat_T j
         else case datatype_spec datatypes T of
-          NONE => atom for_auto T j
-        | SOME {deep = false, ...} => atom for_auto T j
+          NONE => nth_atom for_auto T j k
+        | SOME {deep = false, ...} => nth_atom 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 () = ((atom_name "" T j, 0), T)
+            fun var () = ((nth_atom_name "" 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
@@ -479,13 +481,14 @@
     (* (typ * int) list -> int -> rep -> typ -> typ -> typ -> int list
        -> term *)
     and term_for_vect seen k R T1 T2 T' js =
-      make_fun true T1 T2 T' (map (term_for_atom seen T1 T1) (index_seq 0 k))
+      make_fun true T1 T2 T'
+               (map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k))
                (map (term_for_rep seen T2 T2 R o single)
                     (batch_list (arity_of_rep R) js))
     (* (typ * int) list -> typ -> typ -> rep -> int list list -> term *)
-    and term_for_rep seen T T' Unit [[]] = term_for_atom seen T T' 0
+    and term_for_rep seen T T' Unit [[]] = term_for_atom seen T T' 0 1
       | term_for_rep seen T T' (R as Atom (k, j0)) [[j]] =
-        if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0)
+        if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k
         else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R])
       | term_for_rep seen (Type ("*", [T1, T2])) _ (Struct [R1, R2]) [js] =
         let
@@ -732,7 +735,7 @@
     fun free_type_assm (T, k) =
       let
         (* int -> term *)
-        val atom = atom true T
+        fun atom j = nth_atom 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 =
diff -r a88642066448 -r 888802be2019 src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Fri Feb 05 11:24:53 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Fri Feb 05 12:04:54 2010 +0100
@@ -134,7 +134,7 @@
 fun quintuple_for_scope quote ({hol_ctxt as {thy, ctxt, ...}, card_assigns,
                                 bits, bisim_depth, datatypes, ...} : scope) =
   let
-    val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit}, @{typ \<xi>},
+    val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
                      @{typ bisim_iterator}]
     val (iter_assigns, card_assigns) =
       card_assigns |> filter_out (member (op =) boring_Ts o fst)