merged
authorblanchet
Wed Feb 17 12:14:21 2010 +0100 (2010-02-17)
changeset 35186bb64d089c643
parent 35165 58b9503a7f9a
parent 35185 9b8f351cced6
child 35187 3acab6c90d4a
merged
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Wed Feb 17 11:21:59 2010 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Wed Feb 17 12:14:21 2010 +0100
     1.3 @@ -472,7 +472,9 @@
     1.4  \prew
     1.5  \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
     1.6  \textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount]
     1.7 -\slshape Nitpick found a potential counterexample: \\[2\smallskipamount]
     1.8 +\slshape Warning: The conjecture either trivially holds or (more likely) lies outside Nitpick's supported
     1.9 +fragment. Only potential counterexamples may be found. \\[2\smallskipamount]
    1.10 +Nitpick found a potential counterexample: \\[2\smallskipamount]
    1.11  \hbox{}\qquad Free variable: \nopagebreak \\
    1.12  \hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount]
    1.13  Confirmation by ``\textit{auto}'': The above counterexample is genuine.
    1.14 @@ -1331,7 +1333,7 @@
    1.15  and this time \textit{arith} can finish off the subgoals.
    1.16  
    1.17  A similar technique can be employed for structural induction. The
    1.18 -following mini-formalization of full binary trees will serve as illustration:
    1.19 +following mini formalization of full binary trees will serve as illustration:
    1.20  
    1.21  \prew
    1.22  \textbf{datatype} $\kern1pt'a$~\textit{bin\_tree} = $\textit{Leaf}~{\kern1pt'a}$ $\mid$ $\textit{Branch}$ ``\kern1pt$'a$ \textit{bin\_tree}'' ``\kern1pt$'a$ \textit{bin\_tree}'' \\[2\smallskipamount]
    1.23 @@ -1350,8 +1352,7 @@
    1.24  obtained by swapping $a$ and $b$:
    1.25  
    1.26  \prew
    1.27 -\textbf{lemma} $``\lbrakk a \in \textit{labels}~t;\, b \in \textit{labels}~t;\, a \not= b\rbrakk {}$ \\
    1.28 -\phantom{\textbf{lemma} ``}$\,{\Longrightarrow}{\;\,} \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$''
    1.29 +\textbf{lemma} $``\{a, b\} \subseteq \textit{labels}~t \,\Longrightarrow\, \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$''
    1.30  \postw
    1.31  
    1.32  Nitpick can't find any counterexample, so we proceed with induction
    1.33 @@ -1369,48 +1370,47 @@
    1.34  
    1.35  \prew
    1.36  \slshape
    1.37 -Hint: To check that the induction hypothesis is general enough, try the following command:
    1.38 -\textbf{nitpick}~[\textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$'', \textit{show\_consts}].
    1.39 +Hint: To check that the induction hypothesis is general enough, try this command:
    1.40 +\textbf{nitpick}~[\textit{non\_std}, \textit{show\_all}].
    1.41  \postw
    1.42  
    1.43  If we follow the hint, we get a ``nonstandard'' counterexample for the step:
    1.44  
    1.45  \prew
    1.46 -\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
    1.47 +\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 3: \\[2\smallskipamount]
    1.48  \hbox{}\qquad Free variables: \nopagebreak \\
    1.49  \hbox{}\qquad\qquad $a = a_1$ \\
    1.50  \hbox{}\qquad\qquad $b = a_2$ \\
    1.51  \hbox{}\qquad\qquad $t = \xi_1$ \\
    1.52  \hbox{}\qquad\qquad $u = \xi_2$ \\
    1.53 +\hbox{}\qquad Datatype: \nopagebreak \\
    1.54 +\hbox{}\qquad\qquad $\alpha~\textit{btree} = \{\xi_1 \mathbin{=} \textit{Branch}~\xi_1~\xi_1,\> \xi_2 \mathbin{=} \textit{Branch}~\xi_2~\xi_2,\> \textit{Branch}~\xi_1~\xi_2\}$ \\
    1.55  \hbox{}\qquad {\slshape Constants:} \nopagebreak \\
    1.56  \hbox{}\qquad\qquad $\textit{labels} = \undef
    1.57      (\!\begin{aligned}[t]%
    1.58 -    & \xi_1 := \{a_1, a_4, a_3^\Q\},\> \xi_2 := \{a_2, a_3^\Q\}, \\[-2pt] %% TYPESETTING
    1.59 -    & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_4, a_3^\Q\}, \\[-2pt]
    1.60 -    & \textit{Branch}~\xi_2~\xi_2 := \{a_2, a_3^\Q\})\end{aligned}$ \\
    1.61 +    & \xi_1 := \{a_2, a_3\},\> \xi_2 := \{a_1\},\> \\[-2pt]
    1.62 +    & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_3\})\end{aligned}$ \\
    1.63  \hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \undef
    1.64      (\!\begin{aligned}[t]%
    1.65      & \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[-2pt]
    1.66 -    & \textit{Branch}~\xi_1~\xi_2 := \textit{Branch}~\xi_2~\xi_2, \\[-2pt]
    1.67 -    & \textit{Branch}~\xi_2~\xi_2 := \textit{Branch}~\xi_2~\xi_2)\end{aligned}$ \\[2\smallskipamount]
    1.68 +    & \textit{Branch}~\xi_1~\xi_2 := \xi_2)\end{aligned}$ \\[2\smallskipamount]
    1.69  The existence of a nonstandard model suggests that the induction hypothesis is not general enough or perhaps
    1.70  even wrong. See the ``Inductive Properties'' section of the Nitpick manual for details (``\textit{isabelle doc nitpick}'').
    1.71  \postw
    1.72  
    1.73  Reading the Nitpick manual is a most excellent idea.
    1.74 -But what's going on? The \textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$''
    1.75 -option told the tool to look for nonstandard models of binary trees, which
    1.76 -means that new ``nonstandard'' trees $\xi_1, \xi_2, \ldots$, are now allowed in
    1.77 -addition to the standard trees generated by the \textit{Leaf} and
    1.78 -\textit{Branch} constructors.%
    1.79 +But what's going on? The \textit{non\_std} option told the tool to look for
    1.80 +nonstandard models of binary trees, which means that new ``nonstandard'' trees
    1.81 +$\xi_1, \xi_2, \ldots$, are now allowed in addition to the standard trees
    1.82 +generated by the \textit{Leaf} and \textit{Branch} constructors.%
    1.83  \footnote{Notice the similarity between allowing nonstandard trees here and
    1.84  allowing unreachable states in the preceding example (by removing the ``$n \in
    1.85  \textit{reach\/}$'' assumption). In both cases, we effectively enlarge the
    1.86  set of objects over which the induction is performed while doing the step
    1.87  in order to test the induction hypothesis's strength.}
    1.88 -The new trees are so nonstandard that we know nothing about them, except what
    1.89 -the induction hypothesis states and what can be proved about all trees without
    1.90 -relying on induction or case distinction. The key observation is,
    1.91 +Unlike standard trees, these new trees contain cycles. We will see later that
    1.92 +every property of acyclic trees that can be proved without using induction also
    1.93 +holds for cyclic trees. Hence,
    1.94  %
    1.95  \begin{quote}
    1.96  \textsl{If the induction
    1.97 @@ -1418,9 +1418,9 @@
    1.98  objects, and Nitpick won't find any nonstandard counterexample.}
    1.99  \end{quote}
   1.100  %
   1.101 -But here, Nitpick did find some nonstandard trees $t = \xi_1$
   1.102 -and $u = \xi_2$ such that $a \in \textit{labels}~t$, $b \notin
   1.103 -\textit{labels}~t$, $a \notin \textit{labels}~u$, and $b \in \textit{labels}~u$.
   1.104 +But here the tool find some nonstandard trees $t = \xi_1$
   1.105 +and $u = \xi_2$ such that $a \notin \textit{labels}~t$, $b \in
   1.106 +\textit{labels}~t$, $a \in \textit{labels}~u$, and $b \notin \textit{labels}~u$.
   1.107  Because neither tree contains both $a$ and $b$, the induction hypothesis tells
   1.108  us nothing about the labels of $\textit{swap}~t~a~b$ and $\textit{swap}~u~a~b$,
   1.109  and as a result we know nothing about the labels of the tree
     2.1 --- a/src/HOL/Nitpick.thy	Wed Feb 17 11:21:59 2010 +0100
     2.2 +++ b/src/HOL/Nitpick.thy	Wed Feb 17 12:14:21 2010 +0100
     2.3 @@ -37,7 +37,6 @@
     2.4             and bisim_iterator_max :: bisim_iterator
     2.5             and Quot :: "'a \<Rightarrow> 'b"
     2.6             and quot_normal :: "'a \<Rightarrow> 'a"
     2.7 -           and NonStd :: "'a \<Rightarrow> 'b"
     2.8             and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
     2.9  
    2.10  datatype ('a, 'b) pair_box = PairBox 'a 'b
    2.11 @@ -45,7 +44,6 @@
    2.12  
    2.13  typedecl unsigned_bit
    2.14  typedecl signed_bit
    2.15 -typedecl \<xi>
    2.16  
    2.17  datatype 'a word = Word "('a set)"
    2.18  
    2.19 @@ -254,12 +252,12 @@
    2.20  setup {* Nitpick_Isar.setup *}
    2.21  
    2.22  hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim 
    2.23 -    bisim_iterator_max Quot quot_normal NonStd Tha PairBox FunBox Word refl' wf'
    2.24 +    bisim_iterator_max Quot quot_normal Tha PairBox FunBox Word refl' wf'
    2.25      wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd
    2.26      int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac
    2.27      plus_frac times_frac uminus_frac number_of_frac inverse_frac less_eq_frac
    2.28      of_frac
    2.29 -hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit \<xi> word
    2.30 +hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word
    2.31  hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
    2.32      wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
    2.33      The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
     3.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Feb 17 11:21:59 2010 +0100
     3.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Feb 17 12:14:21 2010 +0100
     3.3 @@ -259,14 +259,14 @@
     3.4   (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" |
     3.5  "swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
     3.6  
     3.7 -lemma "\<lbrakk>a \<in> labels t; b \<in> labels t; a \<noteq> b\<rbrakk> \<Longrightarrow> labels (swap t a b) = labels t"
     3.8 +lemma "{a, b} \<subseteq> labels t \<Longrightarrow> labels (swap t a b) = labels t"
     3.9  nitpick
    3.10  proof (induct t)
    3.11    case Leaf thus ?case by simp
    3.12  next
    3.13    case (Branch t u) thus ?case
    3.14    nitpick
    3.15 -  nitpick [non_std "'a bin_tree", show_consts]
    3.16 +  nitpick [non_std, show_all]
    3.17  oops
    3.18  
    3.19  lemma "labels (swap t a b) =
     4.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Wed Feb 17 11:21:59 2010 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Wed Feb 17 12:14:21 2010 +0100
     4.3 @@ -167,6 +167,7 @@
     4.4  
     4.5    val max_arity : int -> int
     4.6    val arity_of_rel_expr : rel_expr -> int
     4.7 +  val is_problem_trivially_false : problem -> bool
     4.8    val problems_equivalent : problem -> problem -> bool
     4.9    val solve_any_problem :
    4.10      bool -> Time.time option -> int -> int -> problem list -> outcome
    4.11 @@ -491,6 +492,10 @@
    4.12    | arity_of_decl (DeclSome ((n, _), _)) = n
    4.13    | arity_of_decl (DeclSet ((n, _), _)) = n
    4.14  
    4.15 +(* problem -> bool *)
    4.16 +fun is_problem_trivially_false ({formula = False, ...} : problem) = true
    4.17 +  | is_problem_trivially_false _ = false
    4.18 +
    4.19  (* string -> bool *)
    4.20  val is_relevant_setting = not o member (op =) ["solver", "delay"]
    4.21  
    4.22 @@ -1014,7 +1019,7 @@
    4.23      val indexed_problems = if j >= 0 then
    4.24                               [(j, nth problems j)]
    4.25                             else
    4.26 -                             filter (not_equal False o #formula o snd)
    4.27 +                             filter (is_problem_trivially_false o snd)
    4.28                                      (0 upto length problems - 1 ~~ problems)
    4.29      val triv_js = filter_out (AList.defined (op =) indexed_problems)
    4.30                               (0 upto length problems - 1)
     5.1 --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Wed Feb 17 11:21:59 2010 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Wed Feb 17 12:14:21 2010 +0100
     5.3 @@ -9,7 +9,7 @@
     5.4  sig
     5.5    val configured_sat_solvers : bool -> string list
     5.6    val smart_sat_solver_name : bool -> string
     5.7 -  val sat_solver_spec : bool -> string -> string * string list
     5.8 +  val sat_solver_spec : string -> string * string list
     5.9  end;
    5.10  
    5.11  structure Kodkod_SAT : KODKOD_SAT =
    5.12 @@ -51,15 +51,15 @@
    5.13     ("HaifaSat", ExternalV2 (ToStdout, "HAIFASAT_HOME", "HaifaSat", ["-p", "1"],
    5.14                              "s SATISFIABLE", "v ", "s UNSATISFIABLE"))]
    5.15  
    5.16 -(* bool -> string -> sink -> string -> string -> string list -> string list
    5.17 +(* string -> sink -> string -> string -> string list -> string list
    5.18     -> (string * (unit -> string list)) option *)
    5.19 -fun dynamic_entry_for_external overlord name dev home exec args markers =
    5.20 +fun dynamic_entry_for_external name dev home exec args markers =
    5.21    case getenv home of
    5.22      "" => NONE
    5.23    | dir =>
    5.24      SOME (name, fn () =>
    5.25                     let
    5.26 -                     val serial_str = if overlord then "" else serial_string ()
    5.27 +                     val serial_str = serial_string ()
    5.28                       val base = name ^ serial_str
    5.29                       val out_file = base ^ ".out"
    5.30                       val dir_sep =
    5.31 @@ -76,9 +76,9 @@
    5.32                     end)
    5.33  (* bool -> bool -> string * sat_solver_info
    5.34     -> (string * (unit -> string list)) option *)
    5.35 -fun dynamic_entry_for_info _ incremental (name, Internal (Java, mode, ss)) =
    5.36 +fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
    5.37      if incremental andalso mode = Batch then NONE else SOME (name, K ss)
    5.38 -  | dynamic_entry_for_info _ incremental (name, Internal (JNI, mode, ss)) =
    5.39 +  | dynamic_entry_for_info incremental (name, Internal (JNI, mode, ss)) =
    5.40      if incremental andalso mode = Batch then
    5.41        NONE
    5.42      else
    5.43 @@ -92,26 +92,25 @@
    5.44          else
    5.45            NONE
    5.46        end
    5.47 -  | dynamic_entry_for_info overlord false
    5.48 -    (name, External (dev, home, exec, args)) =
    5.49 -    dynamic_entry_for_external overlord name dev home exec args []
    5.50 -  | dynamic_entry_for_info overlord false
    5.51 +  | dynamic_entry_for_info false (name, External (dev, home, exec, args)) =
    5.52 +    dynamic_entry_for_external name dev home exec args []
    5.53 +  | dynamic_entry_for_info false
    5.54          (name, ExternalV2 (dev, home, exec, args, m1, m2, m3)) =
    5.55 -    dynamic_entry_for_external overlord name dev home exec args [m1, m2, m3]
    5.56 -  | dynamic_entry_for_info _ true _ = NONE
    5.57 -(* bool -> bool -> (string * (unit -> string list)) list *)
    5.58 -fun dynamic_list overlord incremental =
    5.59 -  map_filter (dynamic_entry_for_info overlord incremental) static_list
    5.60 +    dynamic_entry_for_external name dev home exec args [m1, m2, m3]
    5.61 +  | dynamic_entry_for_info true _ = NONE
    5.62 +(* bool -> (string * (unit -> string list)) list *)
    5.63 +fun dynamic_list incremental =
    5.64 +  map_filter (dynamic_entry_for_info incremental) static_list
    5.65  
    5.66  (* bool -> string list *)
    5.67 -val configured_sat_solvers = map fst o dynamic_list false
    5.68 +val configured_sat_solvers = map fst o dynamic_list
    5.69  (* bool -> string *)
    5.70 -val smart_sat_solver_name = fst o hd o dynamic_list false
    5.71 +val smart_sat_solver_name = fst o hd o dynamic_list
    5.72  
    5.73 -(* bool -> string -> string * string list *)
    5.74 -fun sat_solver_spec overlord name =
    5.75 +(* string -> string * string list *)
    5.76 +fun sat_solver_spec name =
    5.77    let
    5.78 -    val dyn_list = dynamic_list overlord false
    5.79 +    val dyn_list = dynamic_list false
    5.80      (* (string * 'a) list -> string *)
    5.81      fun enum_solvers solvers =
    5.82        commas (distinct (op =) (map (quote o fst) solvers))
     6.1 --- a/src/HOL/Tools/Nitpick/minipick.ML	Wed Feb 17 11:21:59 2010 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML	Wed Feb 17 12:14:21 2010 +0100
     6.3 @@ -84,7 +84,7 @@
     6.4  fun atom_from_formula f = RelIf (f, true_atom, false_atom)
     6.5  
     6.6  (* Proof.context -> (typ -> int) -> styp list -> term -> formula *)
     6.7 -fun kodkod_formula_for_term ctxt card frees =
     6.8 +fun kodkod_formula_from_term ctxt card frees =
     6.9    let
    6.10      (* typ -> rel_expr -> rel_expr *)
    6.11      fun R_rep_from_S_rep (T as Type ("fun", [T1, @{typ bool}])) r =
    6.12 @@ -145,7 +145,7 @@
    6.13         | Term.Var _ => raise SAME ()
    6.14         | Bound _ => raise SAME ()
    6.15         | Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s)
    6.16 -       | _ => raise TERM ("Minipick.kodkod_formula_for_term.to_F", [t]))
    6.17 +       | _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t]))
    6.18        handle SAME () => formula_from_atom (to_R_rep Ts t)
    6.19      (* typ list -> term -> rel_expr *)
    6.20      and to_S_rep Ts t =
    6.21 @@ -306,7 +306,7 @@
    6.22      val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
    6.23      val declarative_axioms =
    6.24        map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees
    6.25 -    val formula = kodkod_formula_for_term ctxt card frees neg_t
    6.26 +    val formula = kodkod_formula_from_term ctxt card frees neg_t
    6.27                    |> fold_rev (curry And) declarative_axioms
    6.28      val univ_card = univ_card 0 0 0 bounds formula
    6.29      val problem =
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Feb 17 11:21:59 2010 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Feb 17 12:14:21 2010 +0100
     7.3 @@ -130,7 +130,7 @@
     7.4    sel_names: nut list,
     7.5    nonsel_names: nut list,
     7.6    rel_table: nut NameTable.table,
     7.7 -  liberal: bool,
     7.8 +  unsound: bool,
     7.9    scope: scope,
    7.10    core: KK.formula,
    7.11    defs: KK.formula list}
    7.12 @@ -157,15 +157,15 @@
    7.13        (Path.variable "ISABELLE_HOME_USER" ::
    7.14         map Path.basic ["etc", "components"]))) ^ "\"."
    7.15  
    7.16 -val max_liberal_delay_ms = 200
    7.17 -val max_liberal_delay_percent = 2
    7.18 +val max_unsound_delay_ms = 200
    7.19 +val max_unsound_delay_percent = 2
    7.20  
    7.21  (* Time.time option -> int *)
    7.22 -fun liberal_delay_for_timeout NONE = max_liberal_delay_ms
    7.23 -  | liberal_delay_for_timeout (SOME timeout) =
    7.24 -    Int.max (0, Int.min (max_liberal_delay_ms,
    7.25 +fun unsound_delay_for_timeout NONE = max_unsound_delay_ms
    7.26 +  | unsound_delay_for_timeout (SOME timeout) =
    7.27 +    Int.max (0, Int.min (max_unsound_delay_ms,
    7.28                           Time.toMilliseconds timeout
    7.29 -                         * max_liberal_delay_percent div 100))
    7.30 +                         * max_unsound_delay_percent div 100))
    7.31  
    7.32  (* Time.time option -> bool *)
    7.33  fun passed_deadline NONE = false
    7.34 @@ -247,7 +247,7 @@
    7.35                  (if i <> 1 orelse n <> 1 then
    7.36                     "subgoal " ^ string_of_int i ^ " of " ^ string_of_int n
    7.37                   else
    7.38 -                   "goal")) [orig_t]))
    7.39 +                   "goal")) [Logic.list_implies (orig_assm_ts, orig_t)]))
    7.40      val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
    7.41                  else orig_t
    7.42      val assms_t = if assms orelse auto then
    7.43 @@ -382,29 +382,22 @@
    7.44        else
    7.45          ()
    7.46      val deep_dataTs = filter is_deep_datatype all_Ts
    7.47 -    (* FIXME: Implement proper detection of induction datatypes. *)
    7.48 +    (* This detection code is an ugly hack. Fortunately, it is used only to
    7.49 +       provide a hint to the user. *)
    7.50      (* string * (Rule_Cases.T * bool) -> bool *)
    7.51 -    fun is_inductive_case (_, (Rule_Cases.Case {fixes, assumes, ...}, _)) =
    7.52 -      false
    7.53 -(*
    7.54 -      not (null fixes) andalso exists (String.isSuffix ".hyps" o fst) assumes
    7.55 -*)
    7.56 -    (* unit -> typ list *)
    7.57 -    val induct_dataTs =
    7.58 -      if exists is_inductive_case (ProofContext.cases_of ctxt) then
    7.59 -        filter (is_datatype thy) all_Ts
    7.60 -      else
    7.61 -        []
    7.62 -    val _ = if standard andalso not (null induct_dataTs) then
    7.63 +    fun is_struct_induct_step (name, (Rule_Cases.Case {fixes, assumes, ...}, _)) =
    7.64 +      not (null fixes) andalso
    7.65 +      exists (String.isSuffix ".hyps" o fst) assumes andalso
    7.66 +      exists (exists (curry (op =) name o shortest_name o fst)
    7.67 +              o datatype_constrs hol_ctxt) deep_dataTs
    7.68 +    val likely_in_struct_induct_step =
    7.69 +      exists is_struct_induct_step (ProofContext.cases_of ctxt)
    7.70 +    val _ = if standard andalso likely_in_struct_induct_step then
    7.71                pprint_m (fn () => Pretty.blk (0,
    7.72                    pstrs "Hint: To check that the induction hypothesis is \
    7.73 -                        \general enough, try the following command: " @
    7.74 +                        \general enough, try this command: " @
    7.75                    [Pretty.mark Markup.sendback (Pretty.blk (0,
    7.76 -                       pstrs ("nitpick [" ^
    7.77 -                              commas (map (prefix "non_std " o maybe_quote
    7.78 -                                           o unyxml o string_for_type ctxt)
    7.79 -                                          induct_dataTs) ^
    7.80 -                              ", show_consts]")))] @ pstrs "."))
    7.81 +                       pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
    7.82              else
    7.83                ()
    7.84  (*
    7.85 @@ -441,7 +434,7 @@
    7.86      val too_big_scopes = Unsynchronized.ref []
    7.87  
    7.88      (* bool -> scope -> rich_problem option *)
    7.89 -    fun problem_for_scope liberal
    7.90 +    fun problem_for_scope unsound
    7.91              (scope as {card_assigns, bits, bisim_depth, datatypes, ofs, ...}) =
    7.92        let
    7.93          val _ = not (exists (fn other => scope_less_eq other scope)
    7.94 @@ -476,10 +469,10 @@
    7.95                           (univ_card nat_card int_card main_j0 [] KK.True)
    7.96          val _ = check_arity min_univ_card min_highest_arity
    7.97  
    7.98 -        val core_u = choose_reps_in_nut scope liberal rep_table false core_u
    7.99 -        val def_us = map (choose_reps_in_nut scope liberal rep_table true)
   7.100 +        val core_u = choose_reps_in_nut scope unsound rep_table false core_u
   7.101 +        val def_us = map (choose_reps_in_nut scope unsound rep_table true)
   7.102                           def_us
   7.103 -        val nondef_us = map (choose_reps_in_nut scope liberal rep_table false)
   7.104 +        val nondef_us = map (choose_reps_in_nut scope unsound rep_table false)
   7.105                              nondef_us
   7.106  (*
   7.107          val _ = List.app (priority o string_for_nut ctxt)
   7.108 @@ -495,21 +488,19 @@
   7.109          val core_u = rename_vars_in_nut pool rel_table core_u
   7.110          val def_us = map (rename_vars_in_nut pool rel_table) def_us
   7.111          val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
   7.112 -        (* nut -> KK.formula *)
   7.113 -        val to_f = kodkod_formula_from_nut bits ofs liberal kk
   7.114 -        val core_f = to_f core_u
   7.115 -        val def_fs = map to_f def_us
   7.116 -        val nondef_fs = map to_f nondef_us
   7.117 +        val core_f = kodkod_formula_from_nut bits ofs kk core_u
   7.118 +        val def_fs = map (kodkod_formula_from_nut bits ofs kk) def_us
   7.119 +        val nondef_fs = map (kodkod_formula_from_nut bits ofs kk) nondef_us
   7.120          val formula = fold (fold s_and) [def_fs, nondef_fs] core_f
   7.121 -        val comment = (if liberal then "liberal" else "conservative") ^ "\n" ^
   7.122 +        val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
   7.123                        PrintMode.setmp [] multiline_string_for_scope scope
   7.124          val kodkod_sat_solver =
   7.125 -          Kodkod_SAT.sat_solver_spec overlord effective_sat_solver |> snd
   7.126 +          Kodkod_SAT.sat_solver_spec effective_sat_solver |> snd
   7.127          val bit_width = if bits = 0 then 16 else bits + 1
   7.128 -        val delay = if liberal then
   7.129 +        val delay = if unsound then
   7.130                        Option.map (fn time => Time.- (time, Time.now ()))
   7.131                                   deadline
   7.132 -                      |> liberal_delay_for_timeout
   7.133 +                      |> unsound_delay_for_timeout
   7.134                      else
   7.135                        0
   7.136          val settings = [("solver", commas (map quote kodkod_sat_solver)),
   7.137 @@ -547,13 +538,13 @@
   7.138                 expr_assigns = [], formula = formula},
   7.139                {free_names = free_names, sel_names = sel_names,
   7.140                 nonsel_names = nonsel_names, rel_table = rel_table,
   7.141 -               liberal = liberal, scope = scope, core = core_f,
   7.142 +               unsound = unsound, scope = scope, core = core_f,
   7.143                 defs = nondef_fs @ def_fs @ declarative_axioms})
   7.144        end
   7.145        handle TOO_LARGE (loc, msg) =>
   7.146               if loc = "Nitpick_Kodkod.check_arity" andalso
   7.147                  not (Typtab.is_empty ofs) then
   7.148 -               problem_for_scope liberal
   7.149 +               problem_for_scope unsound
   7.150                     {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
   7.151                      bits = bits, bisim_depth = bisim_depth,
   7.152                      datatypes = datatypes, ofs = Typtab.empty}
   7.153 @@ -563,13 +554,13 @@
   7.154               else
   7.155                 (Unsynchronized.change too_big_scopes (cons scope);
   7.156                  print_v (fn () => ("Limit reached: " ^ msg ^
   7.157 -                                   ". Skipping " ^ (if liberal then "potential"
   7.158 +                                   ". Skipping " ^ (if unsound then "potential"
   7.159                                                      else "genuine") ^
   7.160                                     " component of scope."));
   7.161                  NONE)
   7.162             | TOO_SMALL (loc, msg) =>
   7.163               (print_v (fn () => ("Limit reached: " ^ msg ^
   7.164 -                                 ". Skipping " ^ (if liberal then "potential"
   7.165 +                                 ". Skipping " ^ (if unsound then "potential"
   7.166                                                    else "genuine") ^
   7.167                                   " component of scope."));
   7.168                NONE)
   7.169 @@ -584,7 +575,7 @@
   7.170  
   7.171      val scopes = Unsynchronized.ref []
   7.172      val generated_scopes = Unsynchronized.ref []
   7.173 -    val generated_problems = Unsynchronized.ref []
   7.174 +    val generated_problems = Unsynchronized.ref ([] : rich_problem list)
   7.175      val checked_problems = Unsynchronized.ref (SOME [])
   7.176      val met_potential = Unsynchronized.ref 0
   7.177  
   7.178 @@ -635,7 +626,7 @@
   7.179                | NONE => print "No confirmation by \"auto\".")
   7.180             else
   7.181               ();
   7.182 -           if not standard andalso not (null induct_dataTs) then
   7.183 +           if not standard andalso likely_in_struct_induct_step then
   7.184               print "The existence of a nonstandard model suggests that the \
   7.185                     \induction hypothesis is not general enough or perhaps even \
   7.186                     \wrong. See the \"Inductive Properties\" section of the \
   7.187 @@ -718,7 +709,7 @@
   7.188            | KK.Normal (sat_ps, unsat_js) =>
   7.189              let
   7.190                val (lib_ps, con_ps) =
   7.191 -                List.partition (#liberal o snd o nth problems o fst) sat_ps
   7.192 +                List.partition (#unsound o snd o nth problems o fst) sat_ps
   7.193              in
   7.194                update_checked_problems problems (unsat_js @ map fst lib_ps);
   7.195                if null con_ps then
   7.196 @@ -735,9 +726,9 @@
   7.197                      (0, 0, donno)
   7.198                    else
   7.199                      let
   7.200 -                      (* "co_js" is the list of conservative problems whose
   7.201 -                         liberal pendants couldn't be satisfied and hence that
   7.202 -                         most probably can't be satisfied themselves. *)
   7.203 +                      (* "co_js" is the list of sound problems whose unsound
   7.204 +                         pendants couldn't be satisfied and hence that most
   7.205 +                         probably can't be satisfied themselves. *)
   7.206                        val co_js =
   7.207                          map (fn j => j - 1) unsat_js
   7.208                          |> filter (fn j =>
   7.209 @@ -750,7 +741,7 @@
   7.210                        val problems =
   7.211                          problems |> filter_out_indices bye_js
   7.212                                   |> max_potential <= 0
   7.213 -                                    ? filter_out (#liberal o snd)
   7.214 +                                    ? filter_out (#unsound o snd)
   7.215                      in
   7.216                        solve_any_problem max_potential max_genuine donno false
   7.217                                          problems
   7.218 @@ -770,7 +761,7 @@
   7.219                                                   (map fst sat_ps @ unsat_js)
   7.220                        val problems =
   7.221                          problems |> filter_out_indices bye_js
   7.222 -                                 |> filter_out (#liberal o snd)
   7.223 +                                 |> filter_out (#unsound o snd)
   7.224                      in solve_any_problem 0 max_genuine donno false problems end
   7.225                  end
   7.226              end
   7.227 @@ -814,10 +805,10 @@
   7.228              ()
   7.229          (* scope * bool -> rich_problem list * bool
   7.230             -> rich_problem list * bool *)
   7.231 -        fun add_problem_for_scope (scope as {datatypes, ...}, liberal)
   7.232 +        fun add_problem_for_scope (scope as {datatypes, ...}, unsound)
   7.233                                    (problems, donno) =
   7.234            (check_deadline ();
   7.235 -           case problem_for_scope liberal scope of
   7.236 +           case problem_for_scope unsound scope of
   7.237               SOME problem =>
   7.238               (problems
   7.239                |> (null problems orelse
   7.240 @@ -833,6 +824,28 @@
   7.241                 ([], donno)
   7.242          val _ = Unsynchronized.change generated_problems (append problems)
   7.243          val _ = Unsynchronized.change generated_scopes (append scopes)
   7.244 +        val _ =
   7.245 +          if j + 1 = n then
   7.246 +            let
   7.247 +              val (unsound_problems, sound_problems) =
   7.248 +                List.partition (#unsound o snd) (!generated_problems)
   7.249 +            in
   7.250 +              if not (null sound_problems) andalso
   7.251 +                 forall (KK.is_problem_trivially_false o fst)
   7.252 +                        sound_problems then
   7.253 +                print_m (fn () =>
   7.254 +                    "Warning: The conjecture either trivially holds or (more \
   7.255 +                    \likely) lies outside Nitpick's supported fragment." ^
   7.256 +                    (if exists (not o KK.is_problem_trivially_false o fst)
   7.257 +                               unsound_problems then
   7.258 +                       " Only potential counterexamples may be found."
   7.259 +                     else
   7.260 +                       ""))
   7.261 +              else
   7.262 +                ()
   7.263 +            end
   7.264 +          else
   7.265 +            ()
   7.266        in
   7.267          solve_any_problem max_potential max_genuine donno true (rev problems)
   7.268        end
   7.269 @@ -845,7 +858,7 @@
   7.270        let
   7.271          (* rich_problem list -> rich_problem list *)
   7.272          val do_filter =
   7.273 -          if !met_potential = max_potential then filter_out (#liberal o snd)
   7.274 +          if !met_potential = max_potential then filter_out (#unsound o snd)
   7.275            else I
   7.276          val total = length (!scopes)
   7.277          val unsat =
   7.278 @@ -874,7 +887,7 @@
   7.279            if max_potential = original_max_potential then
   7.280              (print_m (fn () =>
   7.281                   "Nitpick found no " ^ das_wort_model ^ "." ^
   7.282 -                 (if not standard andalso not (null induct_dataTs) then
   7.283 +                 (if not standard andalso likely_in_struct_induct_step then
   7.284                      " This suggests that the induction hypothesis might be \
   7.285                      \general enough to prove this subgoal."
   7.286                    else
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Feb 17 11:21:59 2010 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Feb 17 12:14:21 2010 +0100
     8.3 @@ -97,6 +97,7 @@
     8.4    val dest_n_tuple : int -> term -> term list
     8.5    val instantiate_type : theory -> typ -> typ -> typ -> typ
     8.6    val is_real_datatype : theory -> string -> bool
     8.7 +  val is_standard_datatype : hol_context -> typ -> bool
     8.8    val is_quot_type : theory -> typ -> bool
     8.9    val is_codatatype : theory -> typ -> bool
    8.10    val is_pure_typedef : theory -> typ -> bool
    8.11 @@ -574,6 +575,10 @@
    8.12  (* theory -> string -> bool *)
    8.13  val is_typedef = is_some oo typedef_info
    8.14  val is_real_datatype = is_some oo Datatype.get_info
    8.15 +(* hol_context -> typ -> bool *)
    8.16 +fun is_standard_datatype ({thy, stds, ...} : hol_context) =
    8.17 +  the o triple_lookup (type_match thy) stds
    8.18 +
    8.19  (* theory -> typ -> bool *)
    8.20  fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
    8.21    | is_quot_type _ (Type ("FSet.fset", _)) = true
    8.22 @@ -828,9 +833,8 @@
    8.23  fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
    8.24  fun suc_const T = Const (@{const_name Suc}, T --> T)
    8.25  
    8.26 -(* hol_context -> typ -> styp list *)
    8.27 -fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
    8.28 -                              (T as Type (s, Ts)) =
    8.29 +(* theory -> typ -> styp list *)
    8.30 +fun uncached_datatype_constrs thy (T as Type (s, Ts)) =
    8.31      (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
    8.32         SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
    8.33       | _ =>
    8.34 @@ -843,8 +847,6 @@
    8.35               map (fn (s', Us) =>
    8.36                       (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
    8.37                            ---> T)) constrs
    8.38 -             |> (triple_lookup (type_match thy) stds T |> the |> not) ?
    8.39 -                cons (@{const_name NonStd}, @{typ \<xi>} --> T)
    8.40             end
    8.41           | NONE =>
    8.42             if is_record_type T then
    8.43 @@ -867,11 +869,11 @@
    8.44           [])
    8.45    | uncached_datatype_constrs _ _ = []
    8.46  (* hol_context -> typ -> styp list *)
    8.47 -fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
    8.48 +fun datatype_constrs ({thy, constr_cache, ...} : hol_context) T =
    8.49    case AList.lookup (op =) (!constr_cache) T of
    8.50      SOME xs => xs
    8.51    | NONE =>
    8.52 -    let val xs = uncached_datatype_constrs hol_ctxt T in
    8.53 +    let val xs = uncached_datatype_constrs thy T in
    8.54        (Unsynchronized.change constr_cache (cons (T, xs)); xs)
    8.55      end
    8.56  fun boxed_datatype_constrs hol_ctxt =
    8.57 @@ -957,10 +959,6 @@
    8.58        | _ => list_comb (Const x, args)
    8.59      end
    8.60  
    8.61 -(* The higher this number is, the more nonstandard models can be generated. It's
    8.62 -   not important enough to be a user option, though. *)
    8.63 -val xi_card = 8
    8.64 -
    8.65  (* (typ * int) list -> typ -> int *)
    8.66  fun card_of_type assigns (Type ("fun", [T1, T2])) =
    8.67      reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
    8.68 @@ -970,7 +968,6 @@
    8.69    | card_of_type _ @{typ prop} = 2
    8.70    | card_of_type _ @{typ bool} = 2
    8.71    | card_of_type _ @{typ unit} = 1
    8.72 -  | card_of_type _ @{typ \<xi>} = xi_card
    8.73    | card_of_type assigns T =
    8.74      case AList.lookup (op =) assigns T of
    8.75        SOME k => k
    8.76 @@ -1027,7 +1024,6 @@
    8.77         | @{typ prop} => 2
    8.78         | @{typ bool} => 2
    8.79         | @{typ unit} => 1
    8.80 -       | @{typ \<xi>} => xi_card
    8.81         | Type _ =>
    8.82           (case datatype_constrs hol_ctxt T of
    8.83              [] => if is_integer_type T orelse is_bit_type T then 0
    8.84 @@ -1393,21 +1389,11 @@
    8.85  fun optimized_case_def (hol_ctxt as {thy, ...}) dataT res_T =
    8.86    let
    8.87      val xs = datatype_constrs hol_ctxt dataT
    8.88 -    val xs' = filter_out (fn (s, _) => s = @{const_name NonStd}) xs
    8.89 -    val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs'
    8.90 +    val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
    8.91 +    val (xs', x) = split_last xs
    8.92    in
    8.93 -    (if length xs = length xs' then
    8.94 -       let
    8.95 -         val (xs'', x) = split_last xs'
    8.96 -       in
    8.97 -         constr_case_body thy (1, x)
    8.98 -         |> fold_rev (add_constr_case hol_ctxt res_T)
    8.99 -                     (length xs' downto 2 ~~ xs'')
   8.100 -       end
   8.101 -     else
   8.102 -       Const (@{const_name undefined}, dataT --> res_T) $ Bound 0
   8.103 -       |> fold_rev (add_constr_case hol_ctxt res_T)
   8.104 -                   (length xs' downto 1 ~~ xs'))
   8.105 +    constr_case_body thy (1, x)
   8.106 +    |> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs')
   8.107      |> fold_rev (curry absdummy) (func_Ts @ [dataT])
   8.108    end
   8.109  
   8.110 @@ -1738,10 +1724,11 @@
   8.111                                   (tac ctxt (auto_tac (clasimpset_of ctxt))))
   8.112         #> the #> Goal.finish ctxt) goal
   8.113  
   8.114 -val max_cached_wfs = 100
   8.115 -val cached_timeout = Unsynchronized.ref (SOME Time.zeroTime)
   8.116 -val cached_wf_props : (term * bool) list Unsynchronized.ref =
   8.117 -  Unsynchronized.ref []
   8.118 +val max_cached_wfs = 50
   8.119 +val cached_timeout =
   8.120 +  Synchronized.var "Nitpick_HOL.cached_timeout" (SOME Time.zeroTime)
   8.121 +val cached_wf_props =
   8.122 +  Synchronized.var "Nitpick_HOL.cached_wf_props" ([] : (term * bool) list)
   8.123  
   8.124  val termination_tacs = [Lexicographic_Order.lex_order_tac true,
   8.125                          ScnpReconstruct.sizechange_tac]
   8.126 @@ -1772,19 +1759,20 @@
   8.127                   else
   8.128                     ()
   8.129         in
   8.130 -         if tac_timeout = (!cached_timeout) andalso
   8.131 -            length (!cached_wf_props) < max_cached_wfs then
   8.132 +         if tac_timeout = Synchronized.value cached_timeout andalso
   8.133 +            length (Synchronized.value cached_wf_props) < max_cached_wfs then
   8.134             ()
   8.135           else
   8.136 -           (cached_wf_props := []; cached_timeout := tac_timeout);
   8.137 -         case AList.lookup (op =) (!cached_wf_props) prop of
   8.138 +           (Synchronized.change cached_wf_props (K []);
   8.139 +            Synchronized.change cached_timeout (K tac_timeout));
   8.140 +         case AList.lookup (op =) (Synchronized.value cached_wf_props) prop of
   8.141             SOME wf => wf
   8.142           | NONE =>
   8.143             let
   8.144               val goal = prop |> cterm_of thy |> Goal.init
   8.145               val wf = exists (terminates_by ctxt tac_timeout goal)
   8.146                               termination_tacs
   8.147 -           in Unsynchronized.change cached_wf_props (cons (prop, wf)); wf end
   8.148 +           in Synchronized.change cached_wf_props (cons (prop, wf)); wf end
   8.149         end)
   8.150      handle List.Empty => false
   8.151           | NO_TRIPLE () => false
   8.152 @@ -1799,14 +1787,14 @@
   8.153      SOME (SOME b) => b
   8.154    | _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'} orelse
   8.155           case AList.lookup (op =) (!wf_cache) x of
   8.156 -                  SOME (_, wf) => wf
   8.157 -                | NONE =>
   8.158 -                  let
   8.159 -                    val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
   8.160 -                    val wf = uncached_is_well_founded_inductive_pred hol_ctxt x
   8.161 -                  in
   8.162 -                    Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
   8.163 -                  end
   8.164 +           SOME (_, wf) => wf
   8.165 +         | NONE =>
   8.166 +           let
   8.167 +             val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
   8.168 +             val wf = uncached_is_well_founded_inductive_pred hol_ctxt x
   8.169 +           in
   8.170 +             Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
   8.171 +           end
   8.172  
   8.173  (* typ list -> typ -> typ -> term -> term *)
   8.174  fun ap_curry [_] _ _ t = t
   8.175 @@ -2032,8 +2020,7 @@
   8.176    | Type ("*", Ts) => fold (add_ground_types hol_ctxt) Ts accum
   8.177    | Type (@{type_name itself}, [T1]) => add_ground_types hol_ctxt T1 accum
   8.178    | Type (_, Ts) =>
   8.179 -    if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} ::
   8.180 -                      @{typ \<xi>} :: accum) T then
   8.181 +    if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) T then
   8.182        accum
   8.183      else
   8.184        T :: accum
     9.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Feb 17 11:21:59 2010 +0100
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Feb 17 12:14:21 2010 +0100
     9.3 @@ -36,7 +36,7 @@
     9.4      hol_context -> int -> int Typtab.table -> kodkod_constrs
     9.5      -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
     9.6    val kodkod_formula_from_nut :
     9.7 -    int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula
     9.8 +    int -> int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
     9.9  end;
    9.10  
    9.11  structure Nitpick_Kodkod : NITPICK_KODKOD =
    9.12 @@ -317,7 +317,9 @@
    9.13               [ts] |> not exclusive ? cons (KK.TupleSet [])
    9.14             else
    9.15               [KK.TupleSet [],
    9.16 -              if (* ### exclusive andalso*) T1 = T2 andalso epsilon > delta then
    9.17 +              if T1 = T2 andalso epsilon > delta andalso
    9.18 +                 (datatype_spec dtypes T1 |> the |> pairf #co #standard)
    9.19 +                 = (false, true) then
    9.20                  index_seq delta (epsilon - delta)
    9.21                  |> map (fn j =>
    9.22                             KK.TupleProduct (KK.TupleSet [Kodkod.Tuple [j + j0]],
    9.23 @@ -762,6 +764,7 @@
    9.24  (* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
    9.25     -> dtype_spec -> nfa_entry option *)
    9.26  fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
    9.27 +  | nfa_entry_for_datatype _ _ _ _ {standard = false, ...} = NONE
    9.28    | nfa_entry_for_datatype _ _ _ _ {deep = false, ...} = NONE
    9.29    | nfa_entry_for_datatype hol_ctxt kk rel_table dtypes {typ, constrs, ...} =
    9.30      SOME (typ, maps (nfa_transitions_for_constr hol_ctxt kk rel_table dtypes
    9.31 @@ -770,45 +773,47 @@
    9.32  val empty_rel = KK.Product (KK.None, KK.None)
    9.33  
    9.34  (* nfa_table -> typ -> typ -> KK.rel_expr list *)
    9.35 -fun direct_path_rel_exprs nfa start final =
    9.36 -  case AList.lookup (op =) nfa final of
    9.37 -    SOME trans => map fst (filter (curry (op =) start o snd) trans)
    9.38 +fun direct_path_rel_exprs nfa start_T final_T =
    9.39 +  case AList.lookup (op =) nfa final_T of
    9.40 +    SOME trans => map fst (filter (curry (op =) start_T o snd) trans)
    9.41    | NONE => []
    9.42  (* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> KK.rel_expr *)
    9.43 -and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start final =
    9.44 -    fold kk_union (direct_path_rel_exprs nfa start final)
    9.45 -         (if start = final then KK.Iden else empty_rel)
    9.46 -  | any_path_rel_expr (kk as {kk_union, ...}) nfa (q :: qs) start final =
    9.47 -    kk_union (any_path_rel_expr kk nfa qs start final)
    9.48 -             (knot_path_rel_expr kk nfa qs start q final)
    9.49 +and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T
    9.50 +                      final_T =
    9.51 +    fold kk_union (direct_path_rel_exprs nfa start_T final_T)
    9.52 +         (if start_T = final_T then KK.Iden else empty_rel)
    9.53 +  | any_path_rel_expr (kk as {kk_union, ...}) nfa (T :: Ts) start_T final_T =
    9.54 +    kk_union (any_path_rel_expr kk nfa Ts start_T final_T)
    9.55 +             (knot_path_rel_expr kk nfa Ts start_T T final_T)
    9.56  (* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> typ
    9.57     -> KK.rel_expr *)
    9.58 -and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa qs start
    9.59 -                       knot final =
    9.60 -  kk_join (kk_join (any_path_rel_expr kk nfa qs knot final)
    9.61 -                   (kk_reflexive_closure (loop_path_rel_expr kk nfa qs knot)))
    9.62 -          (any_path_rel_expr kk nfa qs start knot)
    9.63 +and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa Ts
    9.64 +                       start_T knot_T final_T =
    9.65 +  kk_join (kk_join (any_path_rel_expr kk nfa Ts knot_T final_T)
    9.66 +                   (kk_reflexive_closure (loop_path_rel_expr kk nfa Ts knot_T)))
    9.67 +          (any_path_rel_expr kk nfa Ts start_T knot_T)
    9.68  (* kodkod_constrs -> nfa_table -> typ list -> typ -> KK.rel_expr *)
    9.69 -and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start =
    9.70 -    fold kk_union (direct_path_rel_exprs nfa start start) empty_rel
    9.71 -  | loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (q :: qs) start =
    9.72 -    if start = q then
    9.73 -      kk_closure (loop_path_rel_expr kk nfa qs start)
    9.74 +and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T =
    9.75 +    fold kk_union (direct_path_rel_exprs nfa start_T start_T) empty_rel
    9.76 +  | loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (T :: Ts)
    9.77 +                       start_T =
    9.78 +    if start_T = T then
    9.79 +      kk_closure (loop_path_rel_expr kk nfa Ts start_T)
    9.80      else
    9.81 -      kk_union (loop_path_rel_expr kk nfa qs start)
    9.82 -               (knot_path_rel_expr kk nfa qs start q start)
    9.83 +      kk_union (loop_path_rel_expr kk nfa Ts start_T)
    9.84 +               (knot_path_rel_expr kk nfa Ts start_T T start_T)
    9.85  
    9.86  (* nfa_table -> unit NfaGraph.T *)
    9.87  fun graph_for_nfa nfa =
    9.88    let
    9.89      (* typ -> unit NfaGraph.T -> unit NfaGraph.T *)
    9.90 -    fun new_node q = perhaps (try (NfaGraph.new_node (q, ())))
    9.91 +    fun new_node T = perhaps (try (NfaGraph.new_node (T, ())))
    9.92      (* nfa_table -> unit NfaGraph.T -> unit NfaGraph.T *)
    9.93      fun add_nfa [] = I
    9.94        | add_nfa ((_, []) :: nfa) = add_nfa nfa
    9.95 -      | add_nfa ((q, ((_, q') :: transitions)) :: nfa) =
    9.96 -        add_nfa ((q, transitions) :: nfa) o NfaGraph.add_edge (q, q') o
    9.97 -        new_node q' o new_node q
    9.98 +      | add_nfa ((T, ((_, T') :: transitions)) :: nfa) =
    9.99 +        add_nfa ((T, transitions) :: nfa) o NfaGraph.add_edge (T, T') o
   9.100 +        new_node T' o new_node T
   9.101    in add_nfa nfa NfaGraph.empty end
   9.102  
   9.103  (* nfa_table -> nfa_table list *)
   9.104 @@ -816,22 +821,22 @@
   9.105    nfa |> graph_for_nfa |> NfaGraph.strong_conn
   9.106        |> map (fn keys => filter (member (op =) keys o fst) nfa)
   9.107  
   9.108 -(* dtype_spec list -> kodkod_constrs -> nfa_table -> typ -> KK.formula *)
   9.109 -fun acyclicity_axiom_for_datatype dtypes kk nfa start =
   9.110 +(* kodkod_constrs -> dtype_spec list -> nfa_table -> typ -> KK.formula *)
   9.111 +fun acyclicity_axiom_for_datatype kk dtypes nfa start_T =
   9.112    #kk_no kk (#kk_intersect kk
   9.113 -                 (loop_path_rel_expr kk nfa (map fst nfa) start) KK.Iden)
   9.114 +                 (loop_path_rel_expr kk nfa (map fst nfa) start_T) KK.Iden)
   9.115  (* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
   9.116     -> KK.formula list *)
   9.117  fun acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes =
   9.118    map_filter (nfa_entry_for_datatype hol_ctxt kk rel_table dtypes) dtypes
   9.119    |> strongly_connected_sub_nfas
   9.120 -  |> maps (fn nfa => map (acyclicity_axiom_for_datatype dtypes kk nfa o fst)
   9.121 -                         nfa)
   9.122 +  |> maps (fn nfa =>
   9.123 +              map (acyclicity_axiom_for_datatype kk dtypes nfa o fst) nfa)
   9.124  
   9.125  (* hol_context -> int -> kodkod_constrs -> nut NameTable.table -> KK.rel_expr
   9.126     -> constr_spec -> int -> KK.formula *)
   9.127  fun sel_axiom_for_sel hol_ctxt j0
   9.128 -        (kk as {kk_all, kk_implies, kk_formula_if, kk_subset, kk_rel_eq, kk_no,
   9.129 +        (kk as {kk_all, kk_formula_if, kk_implies, kk_subset, kk_rel_eq, kk_no,
   9.130                  kk_join, ...}) rel_table dom_r
   9.131          ({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec)
   9.132          n =
   9.133 @@ -862,19 +867,19 @@
   9.134        [formula_for_bool honors_explicit_max]
   9.135      else
   9.136        let
   9.137 -        val ran_r = discr_rel_expr rel_table const
   9.138 +        val dom_r = discr_rel_expr rel_table const
   9.139          val max_axiom =
   9.140            if honors_explicit_max then
   9.141              KK.True
   9.142            else if is_twos_complement_representable bits (epsilon - delta) then
   9.143 -            KK.LE (KK.Cardinality ran_r, KK.Num explicit_max)
   9.144 +            KK.LE (KK.Cardinality dom_r, KK.Num explicit_max)
   9.145            else
   9.146              raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr",
   9.147                               "\"bits\" value " ^ string_of_int bits ^
   9.148                               " too small for \"max\"")
   9.149        in
   9.150          max_axiom ::
   9.151 -        map (sel_axiom_for_sel hol_ctxt j0 kk rel_table ran_r constr)
   9.152 +        map (sel_axiom_for_sel hol_ctxt j0 kk rel_table dom_r constr)
   9.153              (index_seq 0 (num_sels_for_constr_type (snd const)))
   9.154        end
   9.155    end
   9.156 @@ -949,8 +954,8 @@
   9.157    acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes @
   9.158    maps (other_axioms_for_datatype hol_ctxt bits ofs kk rel_table) dtypes
   9.159  
   9.160 -(* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> KK.formula *)
   9.161 -fun kodkod_formula_from_nut bits ofs liberal
   9.162 +(* int -> int Typtab.table -> kodkod_constrs -> nut -> KK.formula *)
   9.163 +fun kodkod_formula_from_nut bits ofs
   9.164          (kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
   9.165                  kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no,
   9.166                  kk_lone, kk_one, kk_some, kk_rel_let, kk_rel_if, kk_union,
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Feb 17 11:21:59 2010 +0100
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Feb 17 12:14:21 2010 +0100
    10.3 @@ -53,6 +53,8 @@
    10.4  val base_mixfix = "_\<^bsub>base\<^esub>"
    10.5  val step_mixfix = "_\<^bsub>step\<^esub>"
    10.6  val abs_mixfix = "\<guillemotleft>_\<guillemotright>"
    10.7 +val cyclic_co_val_name = "\<omega>"
    10.8 +val cyclic_type_name = "\<xi>"
    10.9  val opt_flag = nitpick_prefix ^ "opt"
   10.10  val non_opt_flag = nitpick_prefix ^ "non_opt"
   10.11  
   10.12 @@ -88,7 +90,7 @@
   10.13      Const (nth_atom_name pool "" T j k, T)
   10.14  
   10.15  (* term -> real *)
   10.16 -fun extract_real_number (Const (@{const_name Rings.divide}, _) $ t1 $ t2) =
   10.17 +fun extract_real_number (Const (@{const_name divide}, _) $ t1 $ t2) =
   10.18      real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
   10.19    | extract_real_number t = real (snd (HOLogic.dest_number t))
   10.20  (* term * term -> order *)
   10.21 @@ -257,14 +259,13 @@
   10.22    | mk_tuple _ (t :: _) = t
   10.23    | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], [])
   10.24  
   10.25 -(* string * string * string * string -> scope -> nut list -> nut list
   10.26 -   -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ -> typ -> rep
   10.27 -   -> int list list -> term *)
   10.28 -fun reconstruct_term (maybe_name, base_name, step_name, abs_name)
   10.29 +(* bool -> atom_pool -> string * string * string * string -> scope -> nut list
   10.30 +   -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ
   10.31 +   -> typ -> rep -> int list list -> term *)
   10.32 +fun reconstruct_term elaborate pool (maybe_name, base_name, step_name, abs_name)
   10.33          ({hol_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
   10.34           : scope) sel_names rel_table bounds =
   10.35    let
   10.36 -    val pool = Unsynchronized.ref []
   10.37      val for_auto = (maybe_name = "")
   10.38      (* int list list -> int *)
   10.39      fun value_of_bits jss =
   10.40 @@ -397,13 +398,16 @@
   10.41          else case datatype_spec datatypes T of
   10.42            NONE => nth_atom pool for_auto T j k
   10.43          | SOME {deep = false, ...} => nth_atom pool for_auto T j k
   10.44 -        | SOME {co, constrs, ...} =>
   10.45 +        | SOME {co, standard, constrs, ...} =>
   10.46            let
   10.47              (* styp -> int list *)
   10.48              fun tuples_for_const (s, T) =
   10.49                tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
   10.50 -            (* unit -> indexname * typ *)
   10.51 -            fun var () = ((nth_atom_name pool "" T j k, 0), T)
   10.52 +            (* unit -> term *)
   10.53 +            fun cyclic_atom () =
   10.54 +              nth_atom pool for_auto (Type (cyclic_type_name, [])) j k
   10.55 +            fun cyclic_var () = Var ((nth_atom_name pool "" T j k, 0), T)
   10.56 +
   10.57              val discr_jsss = map (tuples_for_const o discr_for_constr o #const)
   10.58                                   constrs
   10.59              val real_j = j + offset_of_type ofs T
   10.60 @@ -428,16 +432,18 @@
   10.61                map (map_filter (fn js => if hd js = real_j then SOME (tl js)
   10.62                                          else NONE)) sel_jsss
   10.63              val uncur_arg_Ts = binder_types constr_T
   10.64 +            val maybe_cyclic = co orelse not standard
   10.65            in
   10.66 -            if co andalso member (op =) seen (T, j) then
   10.67 -              Var (var ())
   10.68 +            if maybe_cyclic andalso not (null seen) andalso
   10.69 +               member (op =) (seen |> elaborate ? (fst o split_last)) (T, j) then
   10.70 +              cyclic_var ()
   10.71              else if constr_s = @{const_name Word} then
   10.72                HOLogic.mk_number
   10.73                    (if T = @{typ "unsigned_bit word"} then nat_T else int_T)
   10.74                    (value_of_bits (the_single arg_jsss))
   10.75              else
   10.76                let
   10.77 -                val seen = seen |> co ? cons (T, j)
   10.78 +                val seen = seen |> maybe_cyclic ? cons (T, j)
   10.79                  val ts =
   10.80                    if length arg_Ts = 0 then
   10.81                      []
   10.82 @@ -459,7 +465,7 @@
   10.83                             0 => mk_num 0
   10.84                           | n1 => case HOLogic.dest_number t2 |> snd of
   10.85                                     1 => mk_num n1
   10.86 -                                 | n2 => Const (@{const_name Rings.divide},
   10.87 +                                 | n2 => Const (@{const_name divide},
   10.88                                                  num_T --> num_T --> num_T)
   10.89                                           $ mk_num n1 $ mk_num n2)
   10.90                        | _ => raise TERM ("Nitpick_Model.reconstruct_term.\
   10.91 @@ -469,19 +475,27 @@
   10.92                            (is_abs_fun thy constr_x orelse
   10.93                             constr_s = @{const_name Quot}) then
   10.94                      Const (abs_name, constr_T) $ the_single ts
   10.95 -                  else if not for_auto andalso
   10.96 -                          constr_s = @{const_name NonStd} then
   10.97 -                    Const (fst (dest_Const (the_single ts)), T)
   10.98                    else
   10.99                      list_comb (Const constr_x, ts)
  10.100                in
  10.101 -                if co then
  10.102 -                  let val var = var () in
  10.103 -                    if exists_subterm (curry (op =) (Var var)) t then
  10.104 -                      Const (@{const_name The}, (T --> bool_T) --> T)
  10.105 -                      $ Abs ("\<omega>", T,
  10.106 -                             Const (@{const_name "op ="}, T --> T --> bool_T)
  10.107 -                             $ Bound 0 $ abstract_over (Var var, t))
  10.108 +                if maybe_cyclic then
  10.109 +                  let val var = cyclic_var () in
  10.110 +                    if elaborate andalso not standard andalso
  10.111 +                       length seen = 1 andalso
  10.112 +                       exists_subterm (fn Const (s, _) =>
  10.113 +                                          String.isPrefix cyclic_type_name s
  10.114 +                                        | t' => t' = var) t then
  10.115 +                      let val atom = cyclic_atom () in
  10.116 +                        HOLogic.mk_eq (atom, subst_atomic [(var, atom)] t)
  10.117 +                      end
  10.118 +                    else if exists_subterm (curry (op =) var) t then
  10.119 +                      if co then
  10.120 +                        Const (@{const_name The}, (T --> bool_T) --> T)
  10.121 +                        $ Abs (cyclic_co_val_name, T,
  10.122 +                               Const (@{const_name "op ="}, T --> T --> bool_T)
  10.123 +                               $ Bound 0 $ abstract_over (var, t))
  10.124 +                      else
  10.125 +                        cyclic_atom ()
  10.126                      else
  10.127                        t
  10.128                    end
  10.129 @@ -537,17 +551,15 @@
  10.130          raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
  10.131                     Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
  10.132                     string_of_int (length jss))
  10.133 -  in
  10.134 -    polish_funs [] o unbit_and_unbox_term oooo term_for_rep []
  10.135 -  end
  10.136 +  in polish_funs [] o unbit_and_unbox_term oooo term_for_rep [] end
  10.137  
  10.138 -(* scope -> nut list -> nut NameTable.table -> KK.raw_bound list -> nut
  10.139 -   -> term *)
  10.140 -fun term_for_name scope sel_names rel_table bounds name =
  10.141 +(* atom_pool -> scope -> nut list -> nut NameTable.table -> KK.raw_bound list
  10.142 +   -> nut -> term *)
  10.143 +fun term_for_name pool scope sel_names rel_table bounds name =
  10.144    let val T = type_of name in
  10.145      tuple_list_for_name rel_table bounds name
  10.146 -    |> reconstruct_term ("", "", "", "") scope sel_names rel_table bounds T T
  10.147 -                        (rep_of name)
  10.148 +    |> reconstruct_term false pool ("", "", "", "") scope sel_names rel_table
  10.149 +                        bounds T T (rep_of name)
  10.150    end
  10.151  
  10.152  (* Proof.context -> (string * string * string * string) * Proof.context *)
  10.153 @@ -610,6 +622,7 @@
  10.154           card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
  10.155          formats all_frees free_names sel_names nonsel_names rel_table bounds =
  10.156    let
  10.157 +    val pool = Unsynchronized.ref []
  10.158      val (wacky_names as (_, base_name, step_name, _), ctxt) =
  10.159        add_wacky_syntax ctxt
  10.160      val hol_ctxt =
  10.161 @@ -629,11 +642,13 @@
  10.162      val scope = {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
  10.163                   bits = bits, bisim_depth = bisim_depth, datatypes = datatypes,
  10.164                   ofs = ofs}
  10.165 -    (* typ -> typ -> rep -> int list list -> term *)
  10.166 -    val term_for_rep = reconstruct_term wacky_names scope sel_names rel_table
  10.167 -                                        bounds
  10.168 +    (* bool -> typ -> typ -> rep -> int list list -> term *)
  10.169 +    fun term_for_rep elaborate =
  10.170 +      reconstruct_term elaborate pool wacky_names scope sel_names rel_table
  10.171 +                       bounds
  10.172      (* nat -> typ -> nat -> typ *)
  10.173 -    fun nth_value_of_type card T n = term_for_rep T T (Atom (card, 0)) [[n]]
  10.174 +    fun nth_value_of_type card T n =
  10.175 +      term_for_rep true T T (Atom (card, 0)) [[n]]
  10.176      (* nat -> typ -> typ list *)
  10.177      fun all_values_of_type card T =
  10.178        index_seq 0 card |> map (nth_value_of_type card T) |> sort nice_term_ord
  10.179 @@ -666,7 +681,7 @@
  10.180                     Const (@{const_name undefined}, T')
  10.181                   else
  10.182                     tuple_list_for_name rel_table bounds name
  10.183 -                   |> term_for_rep T T' (rep_of name)
  10.184 +                   |> term_for_rep false T T' (rep_of name)
  10.185        in
  10.186          Pretty.block (Pretty.breaks
  10.187              [setmp_show_all_types (Syntax.pretty_term ctxt) t1,
  10.188 @@ -682,7 +697,8 @@
  10.189      (* typ -> dtype_spec list *)
  10.190      fun integer_datatype T =
  10.191        [{typ = T, card = card_of_type card_assigns T, co = false,
  10.192 -        complete = false, concrete = true, deep = true, constrs = []}]
  10.193 +        standard = true, complete = false, concrete = true, deep = true,
  10.194 +        constrs = []}]
  10.195        handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
  10.196      val (codatatypes, datatypes) =
  10.197        datatypes |> filter #deep |> List.partition #co
  10.198 @@ -758,7 +774,7 @@
  10.199      (* nut -> term *)
  10.200      fun free_name_assm name =
  10.201        HOLogic.mk_eq (Free (nickname_of name, type_of name),
  10.202 -                     term_for_name scope sel_names rel_table bounds name)
  10.203 +                     term_for_name pool scope sel_names rel_table bounds name)
  10.204      val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns)
  10.205      val model_assms = map free_name_assm free_names
  10.206      val assm = foldr1 s_conj (freeT_assms @ model_assms)
    11.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Feb 17 11:21:59 2010 +0100
    11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Feb 17 12:14:21 2010 +0100
    11.3 @@ -892,7 +892,7 @@
    11.4  (* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *)
    11.5  fun choose_reps_in_nut (scope as {hol_ctxt as {thy, ctxt, ...}, card_assigns,
    11.6                                    bits, datatypes, ofs, ...})
    11.7 -                       liberal table def =
    11.8 +                       unsound table def =
    11.9    let
   11.10      val bool_atom_R = Atom (2, offset_of_type ofs bool_T)
   11.11      (* polarity -> bool -> rep *)
   11.12 @@ -1036,7 +1036,7 @@
   11.13                if is_constructive u then s_op2 Eq T (Formula Neut) u1' u2'
   11.14                else opt_opt_case ()
   11.15            in
   11.16 -            if liberal orelse polar = Neg orelse
   11.17 +            if unsound orelse polar = Neg orelse
   11.18                 is_concrete_type datatypes (type_of u1) then
   11.19                case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
   11.20                  (true, true) => opt_opt_case ()
   11.21 @@ -1138,7 +1138,7 @@
   11.22                else
   11.23                  let val quant_u = s_op2 oper T (Formula polar) u1' u2' in
   11.24                    if def orelse
   11.25 -                     (liberal andalso (polar = Pos) = (oper = All)) orelse
   11.26 +                     (unsound andalso (polar = Pos) = (oper = All)) orelse
   11.27                       is_complete_type datatypes (type_of u1) then
   11.28                      quant_u
   11.29                    else
    12.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Wed Feb 17 11:21:59 2010 +0100
    12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Wed Feb 17 12:14:21 2010 +0100
    12.3 @@ -22,6 +22,7 @@
    12.4      typ: typ,
    12.5      card: int,
    12.6      co: bool,
    12.7 +    standard: bool,
    12.8      complete: bool,
    12.9      concrete: bool,
   12.10      deep: bool,
   12.11 @@ -71,6 +72,7 @@
   12.12    typ: typ,
   12.13    card: int,
   12.14    co: bool,
   12.15 +  standard: bool,
   12.16    complete: bool,
   12.17    concrete: bool,
   12.18    deep: bool,
   12.19 @@ -162,7 +164,7 @@
   12.20      fun miscs () =
   12.21        (if bits = 0 then [] else ["bits = " ^ string_of_int bits]) @
   12.22        (if bisim_depth < 0 andalso forall (not o #co) datatypes then []
   12.23 -       else ["bisim_depth = " ^ string_of_int bisim_depth])
   12.24 +       else ["bisim_depth = " ^ signed_string_of_int bisim_depth])
   12.25    in
   12.26      setmp_show_all_types
   12.27          (fn () => (cards primary_card_assigns, cards secondary_card_assigns,
   12.28 @@ -466,6 +468,7 @@
   12.29    let
   12.30      val deep = member (op =) deep_dataTs T
   12.31      val co = is_codatatype thy T
   12.32 +    val standard = is_standard_datatype hol_ctxt T
   12.33      val xs = boxed_datatype_constrs hol_ctxt T
   12.34      val self_recs = map (is_self_recursive_constr_type o snd) xs
   12.35      val (num_self_recs, num_non_self_recs) =
   12.36 @@ -481,8 +484,8 @@
   12.37                                  num_non_self_recs)
   12.38                 (sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) []
   12.39    in
   12.40 -    {typ = T, card = card, co = co, complete = complete, concrete = concrete,
   12.41 -     deep = deep, constrs = constrs}
   12.42 +    {typ = T, card = card, co = co, standard = standard, complete = complete,
   12.43 +     concrete = concrete, deep = deep, constrs = constrs}
   12.44    end
   12.45  
   12.46  (* int -> int *)
    13.1 --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Wed Feb 17 11:21:59 2010 +0100
    13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Wed Feb 17 12:14:21 2010 +0100
    13.3 @@ -308,7 +308,7 @@
    13.4                         NameTable.empty
    13.5      val u = Op1 (Not, type_of u, rep_of u, u)
    13.6              |> rename_vars_in_nut pool table
    13.7 -    val formula = kodkod_formula_from_nut bits Typtab.empty false constrs u
    13.8 +    val formula = kodkod_formula_from_nut bits Typtab.empty constrs u
    13.9      val bounds = map (bound_for_plain_rel ctxt debug) free_rels
   13.10      val univ_card = univ_card nat_card int_card j0 bounds formula
   13.11      val declarative_axioms = map (declarative_axiom_for_plain_rel constrs)