tuned code
authorblanchet
Mon Mar 03 22:33:22 2014 +0100 (2014-03-03)
changeset 558896bfbec3dff62
parent 55888 cac1add157e8
child 55890 bd7927cca152
tuned code
NEWS
src/Doc/Nitpick/document/root.tex
src/HOL/Nitpick_Examples/Manual_Nits.thy
src/HOL/Tools/Nitpick/kodkod.ML
src/HOL/Tools/Nitpick/kodkod_sat.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_commands.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_peephole.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Nitpick/nitpick_rep.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
     1.1 --- a/NEWS	Mon Mar 03 22:33:22 2014 +0100
     1.2 +++ b/NEWS	Mon Mar 03 22:33:22 2014 +0100
     1.3 @@ -367,6 +367,11 @@
     1.4  * Nitpick:
     1.5    - Fixed soundness bug whereby mutually recursive datatypes could take
     1.6      infinite values.
     1.7 +  - Fixed soundness bug with low-level number functions such as "Abs_Integ" and
     1.8 +    "Rep_Integ".
     1.9 +  - Removed "std" option.
    1.10 +  - Renamed "show_datatypes" to "show_types" and "hide_datatypes" to
    1.11 +    "hide_types".
    1.12  
    1.13  * HOL-Multivariate_Analysis:
    1.14    - type class ordered_real_vector for ordered vector spaces
    1.15 @@ -812,16 +817,16 @@
    1.16  INCOMPATIBILITY.
    1.17  
    1.18  * Nitpick:
    1.19 -  - Added option "spy"
    1.20 -  - Reduce incidence of "too high arity" errors
    1.21 +  - Added option "spy".
    1.22 +  - Reduce incidence of "too high arity" errors.
    1.23  
    1.24  * Sledgehammer:
    1.25    - Renamed option:
    1.26        isar_shrink ~> isar_compress
    1.27      INCOMPATIBILITY.
    1.28 -  - Added options "isar_try0", "spy"
    1.29 -  - Better support for "isar_proofs"
    1.30 -  - MaSh has been fined-tuned and now runs as a local server
    1.31 +  - Added options "isar_try0", "spy".
    1.32 +  - Better support for "isar_proofs".
    1.33 +  - MaSh has been fined-tuned and now runs as a local server.
    1.34  
    1.35  * Improved support for ad hoc overloading of constants (see also
    1.36  isar-ref manual and ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy).
     2.1 --- a/src/Doc/Nitpick/document/root.tex	Mon Mar 03 22:33:22 2014 +0100
     2.2 +++ b/src/Doc/Nitpick/document/root.tex	Mon Mar 03 22:33:22 2014 +0100
     2.3 @@ -609,7 +609,7 @@
     2.4  \textbf{lemma} ``$\lbrakk \textit{length}~\textit{xs} = 1;\> \textit{length}~\textit{ys} = 1
     2.5  \rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys\/}$''
     2.6  \\
     2.7 -\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
     2.8 +\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount]
     2.9  \slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
    2.10  \hbox{}\qquad Free variables: \nopagebreak \\
    2.11  \hbox{}\qquad\qquad $\textit{xs} = [a_2]$ \\
    2.12 @@ -638,7 +638,7 @@
    2.13  \textbf{definition}~$B \mathbin{\Colon} \textit{three}$ \textbf{where} ``$B \,\equiv\, \textit{Abs\_three}~1$'' \\
    2.14  \textbf{definition}~$C \mathbin{\Colon} \textit{three}$ \textbf{where} ``$C \,\equiv\, \textit{Abs\_three}~2$'' \\[2\smallskipamount]
    2.15  \textbf{lemma} ``$\lbrakk A \in X;\> B \in X\rbrakk \,\Longrightarrow\, c \in X$'' \\
    2.16 -\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
    2.17 +\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount]
    2.18  \slshape Nitpick found a counterexample: \\[2\smallskipamount]
    2.19  \hbox{}\qquad Free variables: \nopagebreak \\
    2.20  \hbox{}\qquad\qquad $X = \{\Abs{0},\, \Abs{1}\}$ \\
    2.21 @@ -667,7 +667,7 @@
    2.22  \textbf{quotient\_definition} ``$\textit{add\/}\Colon\textit{my\_int} \Rightarrow \textit{my\_int} \Rightarrow \textit{my\_int\/}$'' \textbf{is} \textit{add\_raw} \\[2\smallskipamount]
    2.23  %
    2.24  \textbf{lemma} ``$\textit{add}~x~y = \textit{add}~x~x$'' \\
    2.25 -\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
    2.26 +\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount]
    2.27  \slshape Nitpick found a counterexample: \\[2\smallskipamount]
    2.28  \hbox{}\qquad Free variables: \nopagebreak \\
    2.29  \hbox{}\qquad\qquad $x = \Abs{(0,\, 0)}$ \\
    2.30 @@ -709,7 +709,7 @@
    2.31  \hbox{}\quad $\textit{Xcoord} \mathbin{\Colon} \textit{int}$ \\
    2.32  \hbox{}\quad $\textit{Ycoord} \mathbin{\Colon} \textit{int}$ \\[2\smallskipamount]
    2.33  \textbf{lemma} ``$\textit{Xcoord}~(p\Colon\textit{point}) = \textit{Xcoord}~(q\Colon\textit{point})$'' \\
    2.34 -\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
    2.35 +\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount]
    2.36  \slshape Nitpick found a counterexample: \\[2\smallskipamount]
    2.37  \hbox{}\qquad Free variables: \nopagebreak \\
    2.38  \hbox{}\qquad\qquad $p = \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr$ \\
    2.39 @@ -726,7 +726,7 @@
    2.40  
    2.41  \prew
    2.42  \textbf{lemma} ``$4 * x + 3 * (y\Colon\textit{real}) \not= 1/2$'' \\
    2.43 -\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
    2.44 +\textbf{nitpick} [\textit{show\_types}] \\[2\smallskipamount]
    2.45  \slshape Nitpick found a counterexample: \\[2\smallskipamount]
    2.46  \hbox{}\qquad Free variables: \nopagebreak \\
    2.47  \hbox{}\qquad\qquad $x = 1/2$ \\
    2.48 @@ -1048,7 +1048,7 @@
    2.49  \prew
    2.50  \textbf{lemma} ``$\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk
    2.51  \,\Longrightarrow\, \textit{xs} = \textit{ys\/}$'' \\
    2.52 -\textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_datatypes}] \\[2\smallskipamount]
    2.53 +\textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_types}] \\[2\smallskipamount]
    2.54  \slshape Nitpick found a quasi genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
    2.55  \hbox{}\qquad Free variables: \nopagebreak \\
    2.56  \hbox{}\qquad\qquad $a = a_1$ \\
    2.57 @@ -1916,7 +1916,7 @@
    2.58  \textit{Suc}, \textit{gcd}, or \textit{lcm}.
    2.59  
    2.60  {\small See also \textit{bits} (\S\ref{scope-of-search}) and
    2.61 -\textit{show\_datatypes} (\S\ref{output-format}).}
    2.62 +\textit{show\_types} (\S\ref{output-format}).}
    2.63  
    2.64  \opdefault{bits}{int\_seq}{\upshape 1--10}
    2.65  Specifies the number of bits to use to represent natural numbers and integers in
    2.66 @@ -2079,7 +2079,7 @@
    2.67  \textit{overlord} (\S\ref{mode-of-operation}), and
    2.68  \textit{batch\_size} (\S\ref{optimizations}).}
    2.69  
    2.70 -\opfalse{show\_datatypes}{hide\_datatypes}
    2.71 +\opfalse{show\_types}{hide\_types}
    2.72  Specifies whether the subsets used to approximate (co)in\-duc\-tive data\-types should
    2.73  be displayed as part of counterexamples. Such subsets are sometimes helpful when
    2.74  investigating whether a potentially spurious counterexample is genuine, but
    2.75 @@ -2098,7 +2098,7 @@
    2.76  genuine, but they can clutter the output.
    2.77  
    2.78  \opnodefault{show\_all}{bool}
    2.79 -Abbreviation for \textit{show\_datatypes}, \textit{show\_skolems}, and
    2.80 +Abbreviation for \textit{show\_types}, \textit{show\_skolems}, and
    2.81  \textit{show\_consts}.
    2.82  
    2.83  \opdefault{max\_potential}{int}{\upshape 1}
     3.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Mar 03 22:33:22 2014 +0100
     3.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Mar 03 22:33:22 2014 +0100
     3.3 @@ -92,11 +92,11 @@
     3.4  
     3.5  lemma "hd (xs @ [y, y]) = hd xs"
     3.6  nitpick [expect = genuine]
     3.7 -nitpick [show_consts, show_datatypes, expect = genuine]
     3.8 +nitpick [show_consts, show_types, expect = genuine]
     3.9  oops
    3.10  
    3.11  lemma "\<lbrakk>length xs = 1; length ys = 1\<rbrakk> \<Longrightarrow> xs = ys"
    3.12 -nitpick [show_datatypes, expect = genuine]
    3.13 +nitpick [show_types, expect = genuine]
    3.14  oops
    3.15  
    3.16  
    3.17 @@ -111,7 +111,7 @@
    3.18  definition C :: three where "C \<equiv> Abs_three 2"
    3.19  
    3.20  lemma "\<lbrakk>A \<in> X; B \<in> X\<rbrakk> \<Longrightarrow> c \<in> X"
    3.21 -nitpick [show_datatypes, expect = genuine]
    3.22 +nitpick [show_types, expect = genuine]
    3.23  oops
    3.24  
    3.25  fun my_int_rel where
    3.26 @@ -127,7 +127,7 @@
    3.27  unfolding add_raw_def by auto
    3.28  
    3.29  lemma "add x y = add x x"
    3.30 -nitpick [show_datatypes, expect = genuine]
    3.31 +nitpick [show_types, expect = genuine]
    3.32  oops
    3.33  
    3.34  ML {*
    3.35 @@ -142,7 +142,7 @@
    3.36  *}
    3.37  
    3.38  lemma "add x y = add x x"
    3.39 -nitpick [show_datatypes]
    3.40 +nitpick [show_types]
    3.41  oops
    3.42  
    3.43  record point =
    3.44 @@ -150,11 +150,11 @@
    3.45    Ycoord :: int
    3.46  
    3.47  lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)"
    3.48 -nitpick [show_datatypes, expect = genuine]
    3.49 +nitpick [show_types, expect = genuine]
    3.50  oops
    3.51  
    3.52  lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
    3.53 -nitpick [show_datatypes, expect = genuine]
    3.54 +nitpick [show_types, expect = genuine]
    3.55  oops
    3.56  
    3.57  
    3.58 @@ -217,7 +217,7 @@
    3.59  oops
    3.60  
    3.61  lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
    3.62 -nitpick [bisim_depth = -1, show_datatypes, expect = quasi_genuine]
    3.63 +nitpick [bisim_depth = -1, show_types, expect = quasi_genuine]
    3.64  nitpick [card = 1\<emdash>5, expect = none]
    3.65  sorry
    3.66  
     4.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Mon Mar 03 22:33:22 2014 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Mon Mar 03 22:33:22 2014 +0100
     4.3 @@ -433,6 +433,7 @@
     4.4     tuple_set_func: tuple_set -> 'a -> 'a}
     4.5  
     4.6  fun fold_tuple (F : 'a fold_tuple_funcs) = #tuple_func F
     4.7 +
     4.8  fun fold_tuple_set F tuple_set =
     4.9    case tuple_set of
    4.10      TupleUnion (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
    4.11 @@ -445,18 +446,22 @@
    4.12    | TupleArea (t1, t2) => fold_tuple F t1 #> fold_tuple F t2
    4.13    | TupleAtomSeq _ => #tuple_set_func F tuple_set
    4.14    | TupleSetReg _ => #tuple_set_func F tuple_set
    4.15 +
    4.16  fun fold_tuple_assign F assign =
    4.17    case assign of
    4.18      AssignTuple (x, t) => fold_tuple F (TupleReg x) #> fold_tuple F t
    4.19    | AssignTupleSet (x, ts) =>
    4.20      fold_tuple_set F (TupleSetReg x) #> fold_tuple_set F ts
    4.21 +
    4.22  fun fold_bound expr_F tuple_F (zs, tss) =
    4.23    fold (fold_rel_expr expr_F) (map (Rel o fst) zs)
    4.24    #> fold (fold_tuple_set tuple_F) tss
    4.25 +
    4.26  fun fold_int_bound F (_, tss) = fold (fold_tuple_set F) tss
    4.27  
    4.28  fun max_arity univ_card = floor (Math.ln 2147483647.0
    4.29                                   / Math.ln (Real.fromInt univ_card))
    4.30 +
    4.31  fun arity_of_rel_expr (RelLet (_, r)) = arity_of_rel_expr r
    4.32    | arity_of_rel_expr (RelIf (_, r1, _)) = arity_of_rel_expr r1
    4.33    | arity_of_rel_expr (Union (r1, _)) = arity_of_rel_expr r1
    4.34 @@ -539,6 +544,7 @@
    4.35    | inline_comment comment =
    4.36      " /* " ^ translate_string (fn "\n" => " " | "*" => "* " | s => s) comment ^
    4.37      " */"
    4.38 +
    4.39  fun block_comment "" = ""
    4.40    | block_comment comment = prefix_lines "// " comment ^ "\n"
    4.41  
     5.1 --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Mon Mar 03 22:33:22 2014 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Mon Mar 03 22:33:22 2014 +0100
     5.3 @@ -74,6 +74,7 @@
     5.4                         else [if dev = ToFile then out_file else ""]) @ markers @
     5.5                       (if dev = ToFile then [out_file] else []) @ args
     5.6                     end)
     5.7 +
     5.8  fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
     5.9      if incremental andalso mode = Batch then NONE else SOME (name, K ss)
    5.10    | dynamic_entry_for_info incremental
    5.11 @@ -98,6 +99,7 @@
    5.12          (name, ExternalV2 (dev, home, exec, args, m1, m2, m3)) =
    5.13      dynamic_entry_for_external name dev home exec args [m1, m2, m3]
    5.14    | dynamic_entry_for_info true _ = NONE
    5.15 +
    5.16  fun dynamic_list incremental =
    5.17    map_filter (dynamic_entry_for_info incremental) static_list
    5.18  
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Mar 03 22:33:22 2014 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Mar 03 22:33:22 2014 +0100
     6.3 @@ -7,21 +7,20 @@
     6.4  
     6.5  signature NITPICK =
     6.6  sig
     6.7 -  type styp = Nitpick_Util.styp
     6.8    type term_postprocessor = Nitpick_Model.term_postprocessor
     6.9  
    6.10    datatype mode = Auto_Try | Try | Normal | TPTP
    6.11  
    6.12    type params =
    6.13      {cards_assigns: (typ option * int list) list,
    6.14 -     maxes_assigns: (styp option * int list) list,
    6.15 -     iters_assigns: (styp option * int list) list,
    6.16 +     maxes_assigns: ((string * typ) option * int list) list,
    6.17 +     iters_assigns: ((string * typ) option * int list) list,
    6.18       bitss: int list,
    6.19       bisim_depths: int list,
    6.20       boxes: (typ option * bool option) list,
    6.21       finitizes: (typ option * bool option) list,
    6.22       monos: (typ option * bool option) list,
    6.23 -     wfs: (styp option * bool option) list,
    6.24 +     wfs: ((string * typ) option * bool option) list,
    6.25       sat_solver: string,
    6.26       blocking: bool,
    6.27       falsify: bool,
    6.28 @@ -45,7 +44,7 @@
    6.29       timeout: Time.time,
    6.30       tac_timeout: Time.time,
    6.31       max_threads: int,
    6.32 -     show_datatypes: bool,
    6.33 +     show_types: bool,
    6.34       show_skolems: bool,
    6.35       show_consts: bool,
    6.36       evals: term list,
    6.37 @@ -65,7 +64,8 @@
    6.38    val unknownN : string
    6.39    val register_frac_type : string -> (string * string) list -> theory -> theory
    6.40    val unregister_frac_type : string -> theory -> theory
    6.41 -  val register_codatatype : typ -> string -> styp list -> theory -> theory
    6.42 +  val register_codatatype : typ -> string -> (string * typ) list -> theory ->
    6.43 +    theory
    6.44    val unregister_codatatype : typ -> theory -> theory
    6.45    val register_term_postprocessor :
    6.46      typ -> term_postprocessor -> theory -> theory
    6.47 @@ -99,14 +99,14 @@
    6.48  
    6.49  type params =
    6.50    {cards_assigns: (typ option * int list) list,
    6.51 -   maxes_assigns: (styp option * int list) list,
    6.52 -   iters_assigns: (styp option * int list) list,
    6.53 +   maxes_assigns: ((string * typ) option * int list) list,
    6.54 +   iters_assigns: ((string * typ) option * int list) list,
    6.55     bitss: int list,
    6.56     bisim_depths: int list,
    6.57     boxes: (typ option * bool option) list,
    6.58     finitizes: (typ option * bool option) list,
    6.59     monos: (typ option * bool option) list,
    6.60 -   wfs: (styp option * bool option) list,
    6.61 +   wfs: ((string * typ) option * bool option) list,
    6.62     sat_solver: string,
    6.63     blocking: bool,
    6.64     falsify: bool,
    6.65 @@ -130,7 +130,7 @@
    6.66     timeout: Time.time,
    6.67     tac_timeout: Time.time,
    6.68     max_threads: int,
    6.69 -   show_datatypes: bool,
    6.70 +   show_types: bool,
    6.71     show_skolems: bool,
    6.72     show_consts: bool,
    6.73     evals: term list,
    6.74 @@ -181,13 +181,14 @@
    6.75  
    6.76  val isabelle_wrong_message =
    6.77    "Something appears to be wrong with your Isabelle installation."
    6.78 -fun java_not_found_message () =
    6.79 +val java_not_found_message =
    6.80    "Java could not be launched. " ^ isabelle_wrong_message
    6.81 -fun java_too_old_message () =
    6.82 +val java_too_old_message =
    6.83    "The Java version is too old. " ^ isabelle_wrong_message
    6.84 -fun kodkodi_not_installed_message () =
    6.85 +val kodkodi_not_installed_message =
    6.86    "Nitpick requires the external Java program Kodkodi."
    6.87 -fun kodkodi_too_old_message () = "The installed Kodkodi version is too old."
    6.88 +val kodkodi_too_old_message = "The installed Kodkodi version is too old."
    6.89 +
    6.90  val max_unsound_delay_ms = 200
    6.91  val max_unsound_delay_percent = 2
    6.92  
    6.93 @@ -205,6 +206,7 @@
    6.94  val syntactic_sorts =
    6.95    @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @
    6.96    @{sort numeral}
    6.97 +
    6.98  fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) =
    6.99      subset (op =) (S, syntactic_sorts)
   6.100    | has_tfree_syntactic_sort _ = false
   6.101 @@ -229,9 +231,9 @@
   6.102           overlord, spy, user_axioms, assms, whacks, merge_type_vars,
   6.103           binary_ints, destroy_constrs, specialize, star_linear_preds,
   6.104           total_consts, needs, peephole_optim, datatype_sym_break,
   6.105 -         kodkod_sym_break, tac_timeout, max_threads, show_datatypes,
   6.106 -         show_skolems, show_consts, evals, formats, atomss, max_potential,
   6.107 -         max_genuine, check_potential, check_genuine, batch_size, ...} = params
   6.108 +         kodkod_sym_break, tac_timeout, max_threads, show_types, show_skolems,
   6.109 +         show_consts, evals, formats, atomss, max_potential, max_genuine,
   6.110 +         check_potential, check_genuine, batch_size, ...} = params
   6.111      val state_ref = Unsynchronized.ref state
   6.112      fun pprint print =
   6.113        if mode = Auto_Try then
   6.114 @@ -652,7 +654,7 @@
   6.115                 "% SZS output start FiniteModel")
   6.116          val (reconstructed_model, codatatypes_ok) =
   6.117            reconstruct_hol_model
   6.118 -              {show_datatypes = show_datatypes, show_skolems = show_skolems,
   6.119 +              {show_types = show_types, show_skolems = show_skolems,
   6.120                 show_consts = show_consts}
   6.121                scope formats atomss real_frees pseudo_frees free_names sel_names
   6.122                nonsel_names rel_table bounds
   6.123 @@ -771,16 +773,16 @@
   6.124            case KK.solve_any_problem debug overlord deadline max_threads
   6.125                                      max_solutions (map fst problems) of
   6.126              KK.JavaNotFound =>
   6.127 -            (print_nt java_not_found_message;
   6.128 +            (print_nt (K java_not_found_message);
   6.129               (found_really_genuine, max_potential, max_genuine, donno + 1))
   6.130            | KK.JavaTooOld =>
   6.131 -            (print_nt java_too_old_message;
   6.132 +            (print_nt (K java_too_old_message);
   6.133               (found_really_genuine, max_potential, max_genuine, donno + 1))
   6.134            | KK.KodkodiNotInstalled =>
   6.135 -            (print_nt kodkodi_not_installed_message;
   6.136 +            (print_nt (K kodkodi_not_installed_message);
   6.137               (found_really_genuine, max_potential, max_genuine, donno + 1))
   6.138            | KK.KodkodiTooOld =>
   6.139 -            (print_nt kodkodi_too_old_message;
   6.140 +            (print_nt (K kodkodi_too_old_message);
   6.141               (found_really_genuine, max_potential, max_genuine, donno + 1))
   6.142            | KK.Normal ([], unsat_js, s) =>
   6.143              (update_checked_problems problems unsat_js; show_kodkod_warning s;
   6.144 @@ -1029,7 +1031,7 @@
   6.145      if getenv "KODKODI" = "" then
   6.146        (* The "expect" argument is deliberately ignored if Kodkodi is missing so
   6.147           that the "Nitpick_Examples" can be processed on any machine. *)
   6.148 -      (print_nt (Pretty.string_of (plazy kodkodi_not_installed_message));
   6.149 +      (print_nt (Pretty.string_of (plazy (K kodkodi_not_installed_message)));
   6.150         ("no_kodkodi", state))
   6.151      else
   6.152        let
   6.153 @@ -1062,6 +1064,7 @@
   6.154                        (Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) =
   6.155      Variable.is_fixed ctxt s
   6.156    | is_fixed_equation _ _ = false
   6.157 +
   6.158  fun extract_fixed_frees ctxt (assms, t) =
   6.159    let
   6.160      val (subst, other_assms) =
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Mon Mar 03 22:33:22 2014 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Mon Mar 03 22:33:22 2014 +0100
     7.3 @@ -71,7 +71,7 @@
     7.4     ("verbose", "false"),
     7.5     ("overlord", "false"),
     7.6     ("spy", "false"),
     7.7 -   ("show_datatypes", "false"),
     7.8 +   ("show_types", "false"),
     7.9     ("show_skolems", "true"),
    7.10     ("show_consts", "false"),
    7.11     ("format", "1"),
    7.12 @@ -100,7 +100,7 @@
    7.13     ("quiet", "verbose"),
    7.14     ("no_overlord", "overlord"),
    7.15     ("dont_spy", "spy"),
    7.16 -   ("hide_datatypes", "show_datatypes"),
    7.17 +   ("hide_types", "show_types"),
    7.18     ("hide_skolems", "show_skolems"),
    7.19     ("hide_consts", "show_consts"),
    7.20     ("trust_potential", "check_potential"),
    7.21 @@ -125,6 +125,7 @@
    7.22              else if String.isPrefix "non_" name then SOME (unprefix "non_" name)
    7.23              else NONE
    7.24    | some_name => some_name
    7.25 +
    7.26  fun normalize_raw_param (name, value) =
    7.27    case unnegate_param_name name of
    7.28      SOME name' => [(name', case value of
    7.29 @@ -133,7 +134,7 @@
    7.30                             | [] => ["false"]
    7.31                             | _ => value)]
    7.32    | NONE => if name = "show_all" then
    7.33 -              [("show_datatypes", value), ("show_skolems", value),
    7.34 +              [("show_types", value), ("show_skolems", value),
    7.35                 ("show_consts", value)]
    7.36              else
    7.37                [(name, value)]
    7.38 @@ -267,7 +268,7 @@
    7.39      val tac_timeout = lookup_time "tac_timeout"
    7.40      val max_threads =
    7.41        if mode = Normal then Int.max (0, lookup_int "max_threads") else 1
    7.42 -    val show_datatypes = debug orelse lookup_bool "show_datatypes"
    7.43 +    val show_types = debug orelse lookup_bool "show_types"
    7.44      val show_skolems = debug orelse lookup_bool "show_skolems"
    7.45      val show_consts = debug orelse lookup_bool "show_consts"
    7.46      val evals = lookup_term_list_option_polymorphic "eval" |> these
    7.47 @@ -297,7 +298,7 @@
    7.48       datatype_sym_break = datatype_sym_break,
    7.49       kodkod_sym_break = kodkod_sym_break, timeout = timeout,
    7.50       tac_timeout = tac_timeout, max_threads = max_threads,
    7.51 -     show_datatypes = show_datatypes, show_skolems = show_skolems,
    7.52 +     show_types = show_types, show_skolems = show_skolems,
    7.53       show_consts = show_consts, evals = evals, formats = formats,
    7.54       atomss = atomss, max_potential = max_potential, max_genuine = max_genuine,
    7.55       check_potential = check_potential, check_genuine = check_genuine,
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 03 22:33:22 2014 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 03 22:33:22 2014 +0100
     8.3 @@ -7,18 +7,17 @@
     8.4  
     8.5  signature NITPICK_HOL =
     8.6  sig
     8.7 -  type styp = Nitpick_Util.styp
     8.8    type const_table = term list Symtab.table
     8.9 -  type special_fun = (styp * int list * term list) * styp
    8.10 -  type unrolled = styp * styp
    8.11 -  type wf_cache = (styp * (bool * bool)) list
    8.12 +  type special_fun = ((string * typ) * int list * term list) * (string * typ)
    8.13 +  type unrolled = (string * typ) * (string * typ)
    8.14 +  type wf_cache = ((string * typ) * (bool * bool)) list
    8.15  
    8.16    type hol_context =
    8.17      {thy: theory,
    8.18       ctxt: Proof.context,
    8.19       max_bisim_depth: int,
    8.20       boxes: (typ option * bool option) list,
    8.21 -     wfs: (styp option * bool option) list,
    8.22 +     wfs: ((string * typ) option * bool option) list,
    8.23       user_axioms: bool option,
    8.24       debug: bool,
    8.25       whacks: term list,
    8.26 @@ -44,7 +43,7 @@
    8.27       special_funs: special_fun list Unsynchronized.ref,
    8.28       unrolled_preds: unrolled list Unsynchronized.ref,
    8.29       wf_cache: wf_cache Unsynchronized.ref,
    8.30 -     constr_cache: (typ * styp list) list Unsynchronized.ref}
    8.31 +     constr_cache: (typ * (string * typ) list) list Unsynchronized.ref}
    8.32  
    8.33    datatype fixpoint_kind = Lfp | Gfp | NoFp
    8.34    datatype boxability =
    8.35 @@ -81,7 +80,7 @@
    8.36    val shorten_names_in_term : term -> term
    8.37    val strict_type_match : theory -> typ * typ -> bool
    8.38    val type_match : theory -> typ * typ -> bool
    8.39 -  val const_match : theory -> styp * styp -> bool
    8.40 +  val const_match : theory -> (string * typ) * (string * typ) -> bool
    8.41    val term_match : theory -> term * term -> bool
    8.42    val frac_from_term_pair : typ -> term -> term -> term
    8.43    val is_TFree : typ -> bool
    8.44 @@ -105,41 +104,40 @@
    8.45    val elem_type : typ -> typ
    8.46    val pseudo_domain_type : typ -> typ
    8.47    val pseudo_range_type : typ -> typ
    8.48 -  val const_for_iterator_type : typ -> styp
    8.49 +  val const_for_iterator_type : typ -> string * typ
    8.50    val strip_n_binders : int -> typ -> typ list * typ
    8.51    val nth_range_type : int -> typ -> typ
    8.52    val num_factors_in_type : typ -> int
    8.53    val curried_binder_types : typ -> typ list
    8.54    val mk_flat_tuple : typ -> term list -> term
    8.55    val dest_n_tuple : int -> term -> term list
    8.56 -  val is_real_datatype : theory -> string -> bool
    8.57    val is_codatatype : Proof.context -> typ -> bool
    8.58    val is_quot_type : Proof.context -> typ -> bool
    8.59    val is_pure_typedef : Proof.context -> typ -> bool
    8.60    val is_univ_typedef : Proof.context -> typ -> bool
    8.61    val is_datatype : Proof.context -> typ -> bool
    8.62 -  val is_record_constr : styp -> bool
    8.63 -  val is_record_get : theory -> styp -> bool
    8.64 -  val is_record_update : theory -> styp -> bool
    8.65 -  val is_abs_fun : Proof.context -> styp -> bool
    8.66 -  val is_rep_fun : Proof.context -> styp -> bool
    8.67 -  val is_quot_abs_fun : Proof.context -> styp -> bool
    8.68 -  val is_quot_rep_fun : Proof.context -> styp -> bool
    8.69 -  val mate_of_rep_fun : Proof.context -> styp -> styp
    8.70 -  val is_constr_like : Proof.context -> styp -> bool
    8.71 -  val is_constr_like_injective : Proof.context -> styp -> bool
    8.72 -  val is_constr : Proof.context -> styp -> bool
    8.73 +  val is_record_constr : string * typ -> bool
    8.74 +  val is_record_get : theory -> string * typ -> bool
    8.75 +  val is_record_update : theory -> string * typ -> bool
    8.76 +  val is_abs_fun : Proof.context -> string * typ -> bool
    8.77 +  val is_rep_fun : Proof.context -> string * typ -> bool
    8.78 +  val is_quot_abs_fun : Proof.context -> string * typ -> bool
    8.79 +  val is_quot_rep_fun : Proof.context -> string * typ -> bool
    8.80 +  val mate_of_rep_fun : Proof.context -> string * typ -> string * typ
    8.81 +  val is_nonfree_constr : Proof.context -> string * typ -> bool
    8.82 +  val is_free_constr : Proof.context -> string * typ -> bool
    8.83 +  val is_constr : Proof.context -> string * typ -> bool
    8.84    val is_sel : string -> bool
    8.85    val is_sel_like_and_no_discr : string -> bool
    8.86    val box_type : hol_context -> boxability -> typ -> typ
    8.87    val binarize_nat_and_int_in_type : typ -> typ
    8.88    val binarize_nat_and_int_in_term : term -> term
    8.89 -  val discr_for_constr : styp -> styp
    8.90 +  val discr_for_constr : string * typ -> string * typ
    8.91    val num_sels_for_constr_type : typ -> int
    8.92    val nth_sel_name_for_constr_name : string -> int -> string
    8.93 -  val nth_sel_for_constr : styp -> int -> styp
    8.94 +  val nth_sel_for_constr : string * typ -> int -> string * typ
    8.95    val binarized_and_boxed_nth_sel_for_constr :
    8.96 -    hol_context -> bool -> styp -> int -> styp
    8.97 +    hol_context -> bool -> string * typ -> int -> string * typ
    8.98    val sel_no_from_name : string -> int
    8.99    val close_form : term -> term
   8.100    val distinctness_formula : typ -> term list -> term
   8.101 @@ -155,18 +153,20 @@
   8.102      (string * string) list -> morphism -> Context.generic -> Context.generic
   8.103    val register_ersatz_global : (string * string) list -> theory -> theory
   8.104    val register_codatatype :
   8.105 -    typ -> string -> styp list -> morphism -> Context.generic -> Context.generic
   8.106 +    typ -> string -> (string * typ) list -> morphism -> Context.generic ->
   8.107 +    Context.generic
   8.108    val register_codatatype_global :
   8.109 -    typ -> string -> styp list -> theory -> theory
   8.110 +    typ -> string -> (string * typ) list -> theory -> theory
   8.111    val unregister_codatatype :
   8.112      typ -> morphism -> Context.generic -> Context.generic
   8.113    val unregister_codatatype_global : typ -> theory -> theory
   8.114 -  val datatype_constrs : hol_context -> typ -> styp list
   8.115 +  val datatype_constrs : hol_context -> typ -> (string * typ) list
   8.116    val binarized_and_boxed_datatype_constrs :
   8.117 -    hol_context -> bool -> typ -> styp list
   8.118 +    hol_context -> bool -> typ -> (string * typ) list
   8.119    val num_datatype_constrs : hol_context -> typ -> int
   8.120    val constr_name_for_sel_like : string -> string
   8.121 -  val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp
   8.122 +  val binarized_and_boxed_constr_for_sel : hol_context -> bool ->
   8.123 +    string * typ -> string * typ
   8.124    val card_of_type : (typ * int) list -> typ -> int
   8.125    val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
   8.126    val bounded_exact_card_of_type :
   8.127 @@ -178,17 +178,17 @@
   8.128      typ list -> string -> int -> typ -> typ -> (term -> term) -> term -> term
   8.129    val s_betapply : typ list -> term * term -> term
   8.130    val s_betapplys : typ list -> term * term list -> term
   8.131 -  val discriminate_value : hol_context -> styp -> term -> term
   8.132 +  val discriminate_value : hol_context -> string * typ -> term -> term
   8.133    val select_nth_constr_arg :
   8.134 -    Proof.context -> styp -> term -> int -> typ -> term
   8.135 -  val construct_value : Proof.context -> styp -> term list -> term
   8.136 +    Proof.context -> string * typ -> term -> int -> typ -> term
   8.137 +  val construct_value : Proof.context -> string * typ -> term list -> term
   8.138    val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term
   8.139    val special_bounds : term list -> (indexname * typ) list
   8.140    val is_funky_typedef : Proof.context -> typ -> bool
   8.141    val all_defs_of : theory -> (term * term) list -> term list
   8.142    val all_nondefs_of : Proof.context -> (term * term) list -> term list
   8.143 -  val arity_of_built_in_const : styp -> int option
   8.144 -  val is_built_in_const : styp -> bool
   8.145 +  val arity_of_built_in_const : string * typ -> int option
   8.146 +  val is_built_in_const : string * typ -> bool
   8.147    val term_under_def : term -> term
   8.148    val case_const_names : Proof.context -> (string * int) list
   8.149    val unfold_defs_in_term : hol_context -> term -> term
   8.150 @@ -206,29 +206,31 @@
   8.151    val ground_theorem_table : theory -> term list Inttab.table
   8.152    val ersatz_table : Proof.context -> (string * string) list
   8.153    val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
   8.154 -  val inverse_axioms_for_rep_fun : Proof.context -> styp -> term list
   8.155 +  val inverse_axioms_for_rep_fun : Proof.context -> string * typ -> term list
   8.156    val optimized_typedef_axioms : Proof.context -> string * typ list -> term list
   8.157    val optimized_quot_type_axioms :
   8.158      Proof.context -> string * typ list -> term list
   8.159 -  val def_of_const : theory -> const_table * const_table -> styp -> term option
   8.160 +  val def_of_const : theory -> const_table * const_table -> string * typ ->
   8.161 +    term option
   8.162    val fixpoint_kind_of_rhs : term -> fixpoint_kind
   8.163    val fixpoint_kind_of_const :
   8.164      theory -> const_table * const_table -> string * typ -> fixpoint_kind
   8.165 -  val is_real_inductive_pred : hol_context -> styp -> bool
   8.166 +  val is_raw_inductive_pred : hol_context -> string * typ -> bool
   8.167    val is_constr_pattern : Proof.context -> term -> bool
   8.168    val is_constr_pattern_lhs : Proof.context -> term -> bool
   8.169    val is_constr_pattern_formula : Proof.context -> term -> bool
   8.170    val nondef_props_for_const :
   8.171 -    theory -> bool -> const_table -> styp -> term list
   8.172 -  val is_choice_spec_fun : hol_context -> styp -> bool
   8.173 +    theory -> bool -> const_table -> string * typ -> term list
   8.174 +  val is_choice_spec_fun : hol_context -> string * typ -> bool
   8.175    val is_choice_spec_axiom : theory -> const_table -> term -> bool
   8.176 -  val is_real_equational_fun : hol_context -> styp -> bool
   8.177 -  val is_equational_fun_but_no_plain_def : hol_context -> styp -> bool
   8.178 +  val is_raw_equational_fun : hol_context -> string * typ -> bool
   8.179 +  val is_equational_fun : hol_context -> string * typ -> bool
   8.180    val codatatype_bisim_axioms : hol_context -> typ -> term list
   8.181 -  val is_well_founded_inductive_pred : hol_context -> styp -> bool
   8.182 -  val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term
   8.183 -  val equational_fun_axioms : hol_context -> styp -> term list
   8.184 -  val is_equational_fun_surely_complete : hol_context -> styp -> bool
   8.185 +  val is_well_founded_inductive_pred : hol_context -> string * typ -> bool
   8.186 +  val unrolled_inductive_pred_const : hol_context -> bool -> string * typ ->
   8.187 +    term
   8.188 +  val equational_fun_axioms : hol_context -> string * typ -> term list
   8.189 +  val is_equational_fun_surely_complete : hol_context -> string * typ -> bool
   8.190    val merged_type_var_table_for_terms :
   8.191      theory -> term list -> (sort * string) list
   8.192    val merge_type_vars_in_term :
   8.193 @@ -243,16 +245,16 @@
   8.194  open Nitpick_Util
   8.195  
   8.196  type const_table = term list Symtab.table
   8.197 -type special_fun = (styp * int list * term list) * styp
   8.198 -type unrolled = styp * styp
   8.199 -type wf_cache = (styp * (bool * bool)) list
   8.200 +type special_fun = ((string * typ) * int list * term list) * (string * typ)
   8.201 +type unrolled = (string * typ) * (string * typ)
   8.202 +type wf_cache = ((string * typ) * (bool * bool)) list
   8.203  
   8.204  type hol_context =
   8.205    {thy: theory,
   8.206     ctxt: Proof.context,
   8.207     max_bisim_depth: int,
   8.208     boxes: (typ option * bool option) list,
   8.209 -   wfs: (styp option * bool option) list,
   8.210 +   wfs: ((string * typ) option * bool option) list,
   8.211     user_axioms: bool option,
   8.212     debug: bool,
   8.213     whacks: term list,
   8.214 @@ -278,7 +280,7 @@
   8.215     special_funs: special_fun list Unsynchronized.ref,
   8.216     unrolled_preds: unrolled list Unsynchronized.ref,
   8.217     wf_cache: wf_cache Unsynchronized.ref,
   8.218 -   constr_cache: (typ * styp list) list Unsynchronized.ref}
   8.219 +   constr_cache: (typ * (string * typ) list) list Unsynchronized.ref}
   8.220  
   8.221  datatype fixpoint_kind = Lfp | Gfp | NoFp
   8.222  datatype boxability =
   8.223 @@ -289,7 +291,7 @@
   8.224  (
   8.225    type T = {frac_types: (string * (string * string) list) list,
   8.226              ersatz_table: (string * string) list,
   8.227 -            codatatypes: (string * (string * styp list)) list}
   8.228 +            codatatypes: (string * (string * (string * typ) list)) list}
   8.229    val empty = {frac_types = [], ersatz_table = [], codatatypes = []}
   8.230    val extend = I
   8.231    fun merge ({frac_types = fs1, ersatz_table = et1, codatatypes = cs1},
   8.232 @@ -320,12 +322,14 @@
   8.233  (** Constant/type information and term/type manipulation **)
   8.234  
   8.235  fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
   8.236 +
   8.237  fun quot_normal_name_for_type ctxt T =
   8.238    quot_normal_prefix ^ unyxml (Syntax.string_of_typ ctxt T)
   8.239  
   8.240  val strip_first_name_sep =
   8.241    Substring.full #> Substring.position name_sep ##> Substring.triml 1
   8.242    #> pairself Substring.string
   8.243 +
   8.244  fun original_name s =
   8.245    if String.isPrefix nitpick_prefix s then
   8.246      case strip_first_name_sep s of (s1, "") => s1 | (_, s2) => original_name s2
   8.247 @@ -337,6 +341,7 @@
   8.248    | s_conj (t1, t2) =
   8.249      if t1 = @{const False} orelse t2 = @{const False} then @{const False}
   8.250      else HOLogic.mk_conj (t1, t2)
   8.251 +
   8.252  fun s_disj (t1, @{const False}) = t1
   8.253    | s_disj (@{const False}, t2) = t2
   8.254    | s_disj (t1, t2) =
   8.255 @@ -346,6 +351,7 @@
   8.256  fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
   8.257      if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
   8.258    | strip_connective _ t = [t]
   8.259 +
   8.260  fun strip_any_connective (t as (t0 $ _ $ _)) =
   8.261      if t0 = @{const HOL.conj} orelse t0 = @{const HOL.disj} then
   8.262        (strip_connective t0 t, t0)
   8.263 @@ -420,6 +426,7 @@
   8.264    | unarize_type @{typ "signed_bit word"} = int_T
   8.265    | unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts)
   8.266    | unarize_type T = T
   8.267 +
   8.268  fun unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) =
   8.269      unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
   8.270    | unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) =
   8.271 @@ -429,6 +436,7 @@
   8.272    | unarize_unbox_etc_type (Type (s, Ts as _ :: _)) =
   8.273      Type (s, map unarize_unbox_etc_type Ts)
   8.274    | unarize_unbox_etc_type T = T
   8.275 +
   8.276  fun uniterize_type (Type (s, Ts as _ :: _)) = Type (s, map uniterize_type Ts)
   8.277    | uniterize_type @{typ bisim_iterator} = nat_T
   8.278    | uniterize_type T = T
   8.279 @@ -440,13 +448,16 @@
   8.280  val prefix_name = Long_Name.qualify o Long_Name.base_name
   8.281  fun shortest_name s = List.last (space_explode "." s) handle List.Empty => ""
   8.282  val prefix_abs_vars = Term.map_abs_vars o prefix_name
   8.283 +
   8.284  fun short_name s =
   8.285    case space_explode name_sep s of
   8.286      [_] => s |> String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix
   8.287    | ss => map shortest_name ss |> space_implode "_"
   8.288 +
   8.289  fun shorten_names_in_type (Type (s, Ts)) =
   8.290      Type (short_name s, map shorten_names_in_type Ts)
   8.291    | shorten_names_in_type T = T
   8.292 +
   8.293  val shorten_names_in_term =
   8.294    map_aterms (fn Const (s, T) => Const (short_name s, T) | t => t)
   8.295    #> map_types shorten_names_in_type
   8.296 @@ -454,9 +465,12 @@
   8.297  fun strict_type_match thy (T1, T2) =
   8.298    (Sign.typ_match thy (T2, T1) Vartab.empty; true)
   8.299    handle Type.TYPE_MATCH => false
   8.300 +
   8.301  fun type_match thy = strict_type_match thy o pairself unarize_unbox_etc_type
   8.302 +
   8.303  fun const_match thy ((s1, T1), (s2, T2)) =
   8.304    s1 = s2 andalso type_match thy (T1, T2)
   8.305 +
   8.306  fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2)
   8.307    | term_match thy (Free (s1, T1), Free (s2, T2)) =
   8.308      const_match thy ((shortest_name s1, T1), (shortest_name s2, T2))
   8.309 @@ -472,35 +486,53 @@
   8.310  
   8.311  fun is_TFree (TFree _) = true
   8.312    | is_TFree _ = false
   8.313 +
   8.314  fun is_fun_type (Type (@{type_name fun}, _)) = true
   8.315    | is_fun_type _ = false
   8.316 +
   8.317  fun is_set_type (Type (@{type_name set}, _)) = true
   8.318    | is_set_type _ = false
   8.319 +
   8.320  val is_fun_or_set_type = is_fun_type orf is_set_type
   8.321 +
   8.322  fun is_set_like_type (Type (@{type_name fun}, [_, T'])) =
   8.323      (body_type T' = bool_T)
   8.324    | is_set_like_type (Type (@{type_name set}, _)) = true
   8.325    | is_set_like_type _ = false
   8.326 +
   8.327  fun is_pair_type (Type (@{type_name prod}, _)) = true
   8.328    | is_pair_type _ = false
   8.329 +
   8.330  fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
   8.331    | is_lfp_iterator_type _ = false
   8.332 +
   8.333  fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s
   8.334    | is_gfp_iterator_type _ = false
   8.335 +
   8.336  val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type
   8.337 +
   8.338  fun is_iterator_type T =
   8.339    (T = @{typ bisim_iterator} orelse is_fp_iterator_type T)
   8.340 +
   8.341  fun is_boolean_type T = (T = prop_T orelse T = bool_T)
   8.342 +
   8.343  fun is_integer_type T = (T = nat_T orelse T = int_T)
   8.344 +
   8.345  fun is_bit_type T = (T = @{typ unsigned_bit} orelse T = @{typ signed_bit})
   8.346 +
   8.347  fun is_word_type (Type (@{type_name word}, _)) = true
   8.348    | is_word_type _ = false
   8.349 +
   8.350  val is_integer_like_type = is_iterator_type orf is_integer_type orf is_word_type
   8.351 +
   8.352  val is_record_type = not o null o Record.dest_recTs
   8.353 +
   8.354  fun is_frac_type ctxt (Type (s, [])) =
   8.355      s |> AList.defined (op =) (#frac_types (Data.get (Context.Proof ctxt)))
   8.356    | is_frac_type _ _ = false
   8.357 +
   8.358  fun is_number_type ctxt = is_integer_like_type orf is_frac_type ctxt
   8.359 +
   8.360  fun is_higher_order_type (Type (@{type_name fun}, _)) = true
   8.361    | is_higher_order_type (Type (@{type_name set}, _)) = true
   8.362    | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
   8.363 @@ -508,8 +540,10 @@
   8.364  
   8.365  fun elem_type (Type (@{type_name set}, [T'])) = T'
   8.366    | elem_type T = raise TYPE ("Nitpick_HOL.elem_type", [T], [])
   8.367 +
   8.368  fun pseudo_domain_type (Type (@{type_name fun}, [T1, _])) = T1
   8.369    | pseudo_domain_type T = elem_type T
   8.370 +
   8.371  fun pseudo_range_type (Type (@{type_name fun}, [_, T2])) = T2
   8.372    | pseudo_range_type (Type (@{type_name set}, _)) = bool_T
   8.373    | pseudo_range_type T = raise TYPE ("Nitpick_HOL.pseudo_range_type", [T], [])
   8.374 @@ -517,6 +551,7 @@
   8.375  fun iterator_type_for_const gfp (s, T) =
   8.376    Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s,
   8.377          binder_types T)
   8.378 +
   8.379  fun const_for_iterator_type (Type (s, Ts)) =
   8.380      (strip_first_name_sep s |> snd, Ts ---> bool_T)
   8.381    | const_for_iterator_type T =
   8.382 @@ -528,12 +563,15 @@
   8.383    | strip_n_binders n (Type (@{type_name fun_box}, Ts)) =
   8.384      strip_n_binders n (Type (@{type_name fun}, Ts))
   8.385    | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
   8.386 +
   8.387  val nth_range_type = snd oo strip_n_binders
   8.388  
   8.389  fun num_factors_in_type (Type (@{type_name prod}, [T1, T2])) =
   8.390      fold (Integer.add o num_factors_in_type) [T1, T2] 0
   8.391    | num_factors_in_type _ = 1
   8.392 +
   8.393  val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types
   8.394 +
   8.395  fun maybe_curried_binder_types T =
   8.396    (if is_pair_type (body_type T) then binder_types else curried_binder_types) T
   8.397  
   8.398 @@ -541,6 +579,7 @@
   8.399    | mk_flat_tuple (Type (@{type_name prod}, [T1, T2])) (t :: ts) =
   8.400      HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
   8.401    | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
   8.402 +
   8.403  fun dest_n_tuple 1 t = [t]
   8.404    | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op ::
   8.405  
   8.406 @@ -571,8 +610,8 @@
   8.407            Abs_inverse = SOME Abs_inverse, Rep_inverse = SOME Rep_inverse}
   8.408    | _ => NONE
   8.409  
   8.410 -val is_typedef = is_some oo typedef_info
   8.411 -val is_real_datatype = is_some oo Datatype.get_info
   8.412 +val is_raw_typedef = is_some oo typedef_info
   8.413 +val is_raw_old_datatype = is_some oo Datatype.get_info
   8.414  
   8.415  (* FIXME: Use antiquotation for "natural" below or detect "rep_datatype",
   8.416     e.g., by adding a field to "Datatype_Aux.info". *)
   8.417 @@ -590,15 +629,19 @@
   8.418      val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types
   8.419    in Data.put {frac_types = frac_types, ersatz_table = ersatz_table,
   8.420                 codatatypes = codatatypes} generic end
   8.421 +
   8.422  (* TODO: Consider morphism. *)
   8.423  fun register_frac_type frac_s ersaetze (_ : morphism) =
   8.424    register_frac_type_generic frac_s ersaetze
   8.425 +
   8.426  val register_frac_type_global = Context.theory_map oo register_frac_type_generic
   8.427  
   8.428  fun unregister_frac_type_generic frac_s = register_frac_type_generic frac_s []
   8.429  (* TODO: Consider morphism. *)
   8.430 +
   8.431  fun unregister_frac_type frac_s (_ : morphism) =
   8.432    unregister_frac_type_generic frac_s
   8.433 +
   8.434  val unregister_frac_type_global =
   8.435    Context.theory_map o unregister_frac_type_generic
   8.436  
   8.437 @@ -608,9 +651,11 @@
   8.438      val ersatz_table = AList.merge (op =) (K true) (ersatz_table, ersatz)
   8.439    in Data.put {frac_types = frac_types, ersatz_table = ersatz_table,
   8.440                 codatatypes = codatatypes} generic end
   8.441 +
   8.442  (* TODO: Consider morphism. *)
   8.443  fun register_ersatz ersatz (_ : morphism) =
   8.444    register_ersatz_generic ersatz
   8.445 +
   8.446  val register_ersatz_global = Context.theory_map o register_ersatz_generic
   8.447  
   8.448  fun register_codatatype_generic coT case_name constr_xs generic =
   8.449 @@ -628,41 +673,56 @@
   8.450                                     codatatypes
   8.451    in Data.put {frac_types = frac_types, ersatz_table = ersatz_table,
   8.452                 codatatypes = codatatypes} generic end
   8.453 +
   8.454  (* TODO: Consider morphism. *)
   8.455  fun register_codatatype coT case_name constr_xs (_ : morphism) =
   8.456    register_codatatype_generic coT case_name constr_xs
   8.457 +
   8.458  val register_codatatype_global =
   8.459    Context.theory_map ooo register_codatatype_generic
   8.460  
   8.461  fun unregister_codatatype_generic coT = register_codatatype_generic coT "" []
   8.462  (* TODO: Consider morphism. *)
   8.463 +
   8.464  fun unregister_codatatype coT (_ : morphism) =
   8.465    unregister_codatatype_generic coT
   8.466  val unregister_codatatype_global =
   8.467    Context.theory_map o unregister_codatatype_generic
   8.468  
   8.469 +fun is_raw_codatatype ctxt s =
   8.470 +  not (null (these (Option.map snd (AList.lookup (op =)
   8.471 +    (#codatatypes (Data.get (Context.Proof ctxt))) s))))
   8.472 +
   8.473 +fun is_registered_codatatype ctxt s =
   8.474 +  Option.map #fp (BNF_FP_Def_Sugar.fp_sugar_of ctxt s)
   8.475 +  = SOME BNF_Util.Greatest_FP
   8.476 +
   8.477  fun is_codatatype ctxt (Type (s, _)) =
   8.478 -    Option.map #fp (BNF_FP_Def_Sugar.fp_sugar_of ctxt s)
   8.479 -        = SOME BNF_Util.Greatest_FP orelse
   8.480 -    not (null (these (Option.map snd (AList.lookup (op =)
   8.481 -                            (#codatatypes (Data.get (Context.Proof ctxt))) s))))
   8.482 +    is_raw_codatatype ctxt s orelse is_registered_codatatype ctxt s
   8.483    | is_codatatype _ _ = false
   8.484 -fun is_registered_type ctxt T = is_frac_type ctxt T orelse is_codatatype ctxt T
   8.485 -fun is_real_quot_type ctxt (Type (s, _)) =
   8.486 +
   8.487 +fun is_registered_type ctxt (T as Type (s, _)) =
   8.488 +    is_frac_type ctxt T orelse is_registered_codatatype ctxt s
   8.489 +  | is_registered_type _ _ = false
   8.490 +
   8.491 +fun is_raw_quot_type ctxt (Type (s, _)) =
   8.492      is_some (Quotient_Info.lookup_quotients ctxt s)
   8.493 -  | is_real_quot_type _ _ = false
   8.494 +  | is_raw_quot_type _ _ = false
   8.495 +
   8.496  fun is_quot_type ctxt T =
   8.497 -  is_real_quot_type ctxt T andalso not (is_registered_type ctxt T) andalso
   8.498 +  is_raw_quot_type ctxt T andalso not (is_registered_type ctxt T) andalso
   8.499    T <> @{typ int}
   8.500 +
   8.501  fun is_pure_typedef ctxt (T as Type (s, _)) =
   8.502      let val thy = Proof_Context.theory_of ctxt in
   8.503        is_frac_type ctxt T orelse
   8.504 -      (is_typedef ctxt s andalso
   8.505 -       not (is_real_datatype thy s orelse is_real_quot_type ctxt T orelse
   8.506 +      (is_raw_typedef ctxt s andalso
   8.507 +       not (is_raw_old_datatype thy s orelse is_raw_quot_type ctxt T orelse
   8.508              is_codatatype ctxt T orelse is_record_type T orelse
   8.509              is_integer_like_type T))
   8.510      end
   8.511    | is_pure_typedef _ _ = false
   8.512 +
   8.513  fun is_univ_typedef ctxt (Type (s, _)) =
   8.514      (case typedef_info ctxt s of
   8.515         SOME {prop_of_Rep, ...} =>
   8.516 @@ -683,9 +743,10 @@
   8.517         end
   8.518       | NONE => false)
   8.519    | is_univ_typedef _ _ = false
   8.520 +
   8.521  fun is_datatype ctxt (T as Type (s, _)) =
   8.522 -    (is_typedef ctxt s orelse is_registered_type ctxt T orelse
   8.523 -     T = @{typ ind} orelse is_real_quot_type ctxt T) andalso
   8.524 +    (is_raw_typedef ctxt s orelse is_registered_type ctxt T orelse
   8.525 +     T = @{typ ind} orelse is_raw_quot_type ctxt T) andalso
   8.526      not (is_basic_datatype s)
   8.527    | is_datatype _ _ = false
   8.528  
   8.529 @@ -694,39 +755,48 @@
   8.530      recs @ more :: all_record_fields thy (snd more)
   8.531    end
   8.532    handle TYPE _ => []
   8.533 +
   8.534  fun is_record_constr (s, T) =
   8.535    String.isSuffix Record.extN s andalso
   8.536    let val dataT = body_type T in
   8.537      is_record_type dataT andalso
   8.538      s = unsuffix Record.ext_typeN (fst (dest_Type dataT)) ^ Record.extN
   8.539    end
   8.540 +
   8.541  val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields
   8.542 +
   8.543  fun no_of_record_field thy s T1 =
   8.544    find_index (curry (op =) s o fst)
   8.545               (Record.get_extT_fields thy T1 ||> single |> op @)
   8.546 +
   8.547  fun is_record_get thy (s, Type (@{type_name fun}, [T1, _])) =
   8.548      exists (curry (op =) s o fst) (all_record_fields thy T1)
   8.549    | is_record_get _ _ = false
   8.550 +
   8.551  fun is_record_update thy (s, T) =
   8.552    String.isSuffix Record.updateN s andalso
   8.553    exists (curry (op =) (unsuffix Record.updateN s) o fst)
   8.554           (all_record_fields thy (body_type T))
   8.555    handle TYPE _ => false
   8.556 +
   8.557  fun is_abs_fun ctxt (s, Type (@{type_name fun}, [_, Type (s', _)])) =
   8.558      (case typedef_info ctxt s' of
   8.559         SOME {Abs_name, ...} => s = Abs_name
   8.560       | NONE => false)
   8.561    | is_abs_fun _ _ = false
   8.562 +
   8.563  fun is_rep_fun ctxt (s, Type (@{type_name fun}, [Type (s', _), _])) =
   8.564      (case typedef_info ctxt s' of
   8.565         SOME {Rep_name, ...} => s = Rep_name
   8.566       | NONE => false)
   8.567    | is_rep_fun _ _ = false
   8.568 +
   8.569  fun is_quot_abs_fun ctxt (x as (_, Type (@{type_name fun},
   8.570                                           [_, abs_T as Type (s', _)]))) =
   8.571      try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.AbsF) s'
   8.572      = SOME (Const x) andalso not (is_registered_type ctxt abs_T)
   8.573    | is_quot_abs_fun _ _ = false
   8.574 +
   8.575  fun is_quot_rep_fun ctxt (s, Type (@{type_name fun},
   8.576                                     [abs_T as Type (abs_s, _), _])) =
   8.577      (case try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.RepF) abs_s of
   8.578 @@ -741,6 +811,7 @@
   8.579         SOME {Abs_name, ...} => (Abs_name, Type (@{type_name fun}, [T2, T1]))
   8.580       | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
   8.581    | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
   8.582 +
   8.583  fun rep_type_for_quot_type ctxt (T as Type (s, _)) =
   8.584      let
   8.585        val thy = Proof_Context.theory_of ctxt
   8.586 @@ -750,6 +821,7 @@
   8.587      end
   8.588    | rep_type_for_quot_type _ T =
   8.589      raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])
   8.590 +
   8.591  fun equiv_relation_for_quot_type thy (Type (s, Ts)) =
   8.592      let
   8.593        val {qtyp, equiv_rel, equiv_thm, ...} =
   8.594 @@ -765,6 +837,16 @@
   8.595    | equiv_relation_for_quot_type _ T =
   8.596      raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], [])
   8.597  
   8.598 +fun is_raw_old_datatype_constr thy (s, T) =
   8.599 +  case body_type T of
   8.600 +    Type (s', _) =>
   8.601 +    (case Datatype.get_constrs thy s' of
   8.602 +       SOME constrs =>
   8.603 +       List.exists (fn (cname, cty) =>
   8.604 +         cname = s andalso Sign.typ_instance thy (T, cty)) constrs
   8.605 +     | NONE => false)
   8.606 +  | _  => false
   8.607 +
   8.608  fun is_coconstr ctxt (s, T) =
   8.609    case body_type T of
   8.610      coT as Type (co_s, _) =>
   8.611 @@ -783,7 +865,8 @@
   8.612               (ctrs1 @ ctrs2)
   8.613      end
   8.614    | _ => false
   8.615 -fun is_constr_like ctxt (s, T) =
   8.616 +
   8.617 +fun is_nonfree_constr ctxt (s, T) =
   8.618    member (op =) [@{const_name FunBox}, @{const_name PairBox},
   8.619                   @{const_name Quot}, @{const_name Zero_Rep},
   8.620                   @{const_name Suc_Rep}] s orelse
   8.621 @@ -791,22 +874,26 @@
   8.622      val thy = Proof_Context.theory_of ctxt
   8.623      val (x as (_, T)) = (s, unarize_unbox_etc_type T)
   8.624    in
   8.625 -    is_real_constr thy x orelse is_record_constr x orelse
   8.626 +    is_raw_old_datatype_constr thy x orelse is_record_constr x orelse
   8.627      (is_abs_fun ctxt x andalso is_pure_typedef ctxt (range_type T)) orelse
   8.628      is_coconstr ctxt x
   8.629    end
   8.630 -fun is_constr_like_injective ctxt (s, T) =
   8.631 -  is_constr_like ctxt (s, T) andalso
   8.632 +
   8.633 +fun is_free_constr ctxt (s, T) =
   8.634 +  is_nonfree_constr ctxt (s, T) andalso
   8.635    let val (x as (_, T)) = (s, unarize_unbox_etc_type T) in
   8.636      not (is_abs_fun ctxt x) orelse is_univ_typedef ctxt (range_type T)
   8.637    end
   8.638 +
   8.639  fun is_stale_constr ctxt (x as (s, T)) =
   8.640 -  is_registered_type ctxt (body_type T) andalso is_constr_like ctxt x andalso
   8.641 +  is_registered_type ctxt (body_type T) andalso is_nonfree_constr ctxt x andalso
   8.642    not (s = @{const_name Nitpick.Abs_Frac} orelse is_coconstr ctxt x)
   8.643 +
   8.644  fun is_constr ctxt (x as (_, T)) =
   8.645 -  is_constr_like ctxt x andalso
   8.646 +  is_nonfree_constr ctxt x andalso
   8.647    not (is_basic_datatype (fst (dest_Type (unarize_type (body_type T))))) andalso
   8.648    not (is_stale_constr ctxt x)
   8.649 +
   8.650  val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
   8.651  val is_sel_like_and_no_discr =
   8.652    String.isPrefix sel_prefix orf
   8.653 @@ -814,6 +901,7 @@
   8.654  
   8.655  fun in_fun_lhs_for InConstr = InSel
   8.656    | in_fun_lhs_for _ = InFunLHS
   8.657 +
   8.658  fun in_fun_rhs_for InConstr = InConstr
   8.659    | in_fun_rhs_for InSel = InSel
   8.660    | in_fun_rhs_for InFunRHS1 = InFunRHS2
   8.661 @@ -865,15 +953,18 @@
   8.662  fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T --> bool_T)
   8.663  
   8.664  fun num_sels_for_constr_type T = length (maybe_curried_binder_types T)
   8.665 +
   8.666  fun nth_sel_name_for_constr_name s n =
   8.667    if s = @{const_name Pair} then
   8.668      if n = 0 then @{const_name fst} else @{const_name snd}
   8.669    else
   8.670      sel_prefix_for n ^ s
   8.671 +
   8.672  fun nth_sel_for_constr x ~1 = discr_for_constr x
   8.673    | nth_sel_for_constr (s, T) n =
   8.674      (nth_sel_name_for_constr_name s n,
   8.675       body_type T --> nth (maybe_curried_binder_types T) n)
   8.676 +
   8.677  fun binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize =
   8.678    apsnd ((binarize ? binarize_nat_and_int_in_type) o box_type hol_ctxt InSel)
   8.679    oo nth_sel_for_constr
   8.680 @@ -943,7 +1034,7 @@
   8.681                    val T' = (Record.get_extT_fields thy T
   8.682                             |> apsnd single |> uncurry append |> map snd) ---> T
   8.683                  in [(s', T')] end
   8.684 -              else if is_real_quot_type ctxt T then
   8.685 +              else if is_raw_quot_type ctxt T then
   8.686                  [(@{const_name Quot}, rep_type_for_quot_type ctxt T --> T)]
   8.687                else case typedef_info ctxt s of
   8.688                  SOME {abs_type, rep_type, Abs_name, ...} =>
   8.689 @@ -957,6 +1048,7 @@
   8.690            else
   8.691              []))
   8.692    | uncached_datatype_constrs _ _ = []
   8.693 +
   8.694  fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
   8.695    case AList.lookup (op =) (!constr_cache) T of
   8.696      SOME xs => xs
   8.697 @@ -964,6 +1056,7 @@
   8.698      let val xs = uncached_datatype_constrs hol_ctxt T in
   8.699        (Unsynchronized.change constr_cache (cons (T, xs)); xs)
   8.700      end
   8.701 +
   8.702  fun binarized_and_boxed_datatype_constrs hol_ctxt binarize =
   8.703    map (apsnd ((binarize ? binarize_nat_and_int_in_type)
   8.704                o box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
   8.705 @@ -972,6 +1065,7 @@
   8.706  fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
   8.707    | constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
   8.708    | constr_name_for_sel_like s' = original_name s'
   8.709 +
   8.710  fun binarized_and_boxed_constr_for_sel hol_ctxt binarize (s', T') =
   8.711    let val s = constr_name_for_sel_like s' in
   8.712      AList.lookup (op =)
   8.713 @@ -1127,6 +1221,7 @@
   8.714       handle TERM _ => betapply (t1, t2)
   8.715            | General.Subscript => betapply (t1, t2))
   8.716    | s_betapply _ (t1, t2) = t1 $ t2
   8.717 +
   8.718  fun s_betapplys Ts = Library.foldl (s_betapply Ts)
   8.719  
   8.720  fun s_beta_norm Ts t =
   8.721 @@ -1153,11 +1248,12 @@
   8.722      else
   8.723        Abs (Name.uu, dataT, @{const True})
   8.724    end
   8.725 +
   8.726  fun discriminate_value (hol_ctxt as {ctxt, ...}) x t =
   8.727    case head_of t of
   8.728      Const x' =>
   8.729      if x = x' then @{const True}
   8.730 -    else if is_constr_like ctxt x' then @{const False}
   8.731 +    else if is_nonfree_constr ctxt x' then @{const False}
   8.732      else s_betapply [] (discr_term_for_constr hol_ctxt x, t)
   8.733    | _ => s_betapply [] (discr_term_for_constr hol_ctxt x, t)
   8.734  
   8.735 @@ -1181,12 +1277,13 @@
   8.736                       (List.take (arg_Ts, n)) 0
   8.737        in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
   8.738    end
   8.739 +
   8.740  fun select_nth_constr_arg ctxt x t n res_T =
   8.741    (case strip_comb t of
   8.742       (Const x', args) =>
   8.743       if x = x' then
   8.744 -        if is_constr_like_injective ctxt x then nth args n else raise SAME ()
   8.745 -     else if is_constr_like ctxt x' then
   8.746 +        if is_free_constr ctxt x then nth args n else raise SAME ()
   8.747 +     else if is_nonfree_constr ctxt x' then
   8.748         Const (@{const_name unknown}, res_T)
   8.749       else
   8.750         raise SAME ()
   8.751 @@ -1210,7 +1307,7 @@
   8.752  
   8.753  fun constr_expand (hol_ctxt as {ctxt, ...}) T t =
   8.754    (case head_of t of
   8.755 -     Const x => if is_constr_like ctxt x then t else raise SAME ()
   8.756 +     Const x => if is_nonfree_constr ctxt x then t else raise SAME ()
   8.757     | _ => raise SAME ())
   8.758    handle SAME () =>
   8.759           let
   8.760 @@ -1233,6 +1330,7 @@
   8.761    | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
   8.762    | Bound j' => if j' = j then f t else t
   8.763    | _ => t
   8.764 +
   8.765  fun coerce_bound_0_in_term hol_ctxt new_T old_T =
   8.766    old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
   8.767  and coerce_term (hol_ctxt as {ctxt, ...}) Ts new_T old_T t =
   8.768 @@ -1290,6 +1388,7 @@
   8.769    member (op =) [@{type_name unit}, @{type_name prod}, @{type_name set},
   8.770                   @{type_name Sum_Type.sum}, @{type_name int}] s orelse
   8.771    is_frac_type ctxt (Type (s, []))
   8.772 +
   8.773  fun is_funky_typedef ctxt (Type (s, _)) = is_funky_typedef_name ctxt s
   8.774    | is_funky_typedef _ _ = false
   8.775  
   8.776 @@ -1415,6 +1514,7 @@
   8.777         | NONE => false)
   8.778      | _ => false
   8.779    end
   8.780 +
   8.781  fun unfold_mutually_inductive_preds thy table =
   8.782    map_aterms (fn t as Const x =>
   8.783                   (case def_of_const thy table x of
   8.784 @@ -1449,13 +1549,14 @@
   8.785    else fixpoint_kind_of_rhs (the (def_of_const thy table x))
   8.786    handle Option.Option => NoFp
   8.787  
   8.788 -fun is_real_inductive_pred ({thy, def_tables, intro_table, ...} : hol_context)
   8.789 -                           x =
   8.790 +fun is_raw_inductive_pred ({thy, def_tables, intro_table, ...} : hol_context)
   8.791 +                          x =
   8.792    fixpoint_kind_of_const thy def_tables x <> NoFp andalso
   8.793    not (null (def_props_for_const thy intro_table x))
   8.794 +
   8.795  fun is_inductive_pred hol_ctxt (x as (s, _)) =
   8.796 -  is_real_inductive_pred hol_ctxt x orelse String.isPrefix ubfp_prefix s orelse
   8.797 -  String.isPrefix lbfp_prefix s
   8.798 +  String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s orelse
   8.799 +  is_raw_inductive_pred hol_ctxt x
   8.800  
   8.801  fun lhs_of_equation t =
   8.802    case t of
   8.803 @@ -1467,15 +1568,18 @@
   8.804    | Const (@{const_name HOL.eq}, _) $ t1 $ _ => SOME t1
   8.805    | @{const HOL.implies} $ _ $ t2 => lhs_of_equation t2
   8.806    | _ => NONE
   8.807 +
   8.808  fun is_constr_pattern _ (Bound _) = true
   8.809    | is_constr_pattern _ (Var _) = true
   8.810    | is_constr_pattern ctxt t =
   8.811      case strip_comb t of
   8.812        (Const x, args) =>
   8.813 -      is_constr_like ctxt x andalso forall (is_constr_pattern ctxt) args
   8.814 +      is_nonfree_constr ctxt x andalso forall (is_constr_pattern ctxt) args
   8.815      | _ => false
   8.816 +
   8.817  fun is_constr_pattern_lhs ctxt t =
   8.818    forall (is_constr_pattern ctxt) (snd (strip_comb t))
   8.819 +
   8.820  fun is_constr_pattern_formula ctxt t =
   8.821    case lhs_of_equation t of
   8.822      SOME t' => is_constr_pattern_lhs ctxt t'
   8.823 @@ -1505,6 +1609,7 @@
   8.824            ys
   8.825        | aux _ ys = ys
   8.826    in map snd (fold_aterms aux t []) end
   8.827 +
   8.828  fun nondef_props_for_const thy slack table (x as (s, _)) =
   8.829    these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
   8.830  
   8.831 @@ -1512,11 +1617,13 @@
   8.832    | unvarify_term (Var ((s, 0), T)) = Free (s, T)
   8.833    | unvarify_term (Abs (s, T, t')) = Abs (s, T, unvarify_term t')
   8.834    | unvarify_term t = t
   8.835 +
   8.836  fun axiom_for_choice_spec thy =
   8.837    unvarify_term
   8.838    #> Object_Logic.atomize_term thy
   8.839    #> Choice_Specification.close_form
   8.840    #> HOLogic.mk_Trueprop
   8.841 +
   8.842  fun is_choice_spec_fun ({thy, def_tables, nondef_table, choice_spec_table, ...}
   8.843                          : hol_context) x =
   8.844    case nondef_props_for_const thy true choice_spec_table x of
   8.845 @@ -1533,16 +1640,16 @@
   8.846              end
   8.847  
   8.848  fun is_choice_spec_axiom thy choice_spec_table t =
   8.849 -  Symtab.exists (fn (_, ts) =>
   8.850 -                    exists (curry (op aconv) t o axiom_for_choice_spec thy) ts)
   8.851 +  Symtab.exists (exists (curry (op aconv) t o axiom_for_choice_spec thy) o snd)
   8.852                  choice_spec_table
   8.853  
   8.854 -fun is_real_equational_fun ({thy, simp_table, psimp_table, ...}
   8.855 -                            : hol_context) x =
   8.856 +fun is_raw_equational_fun ({thy, simp_table, psimp_table, ...} : hol_context)
   8.857 +                          x =
   8.858    exists (fn table => not (null (def_props_for_const thy table x)))
   8.859           [!simp_table, psimp_table]
   8.860 -fun is_equational_fun_but_no_plain_def hol_ctxt =
   8.861 -  is_real_equational_fun hol_ctxt orf is_inductive_pred hol_ctxt
   8.862 +
   8.863 +fun is_equational_fun hol_ctxt =
   8.864 +  is_raw_equational_fun hol_ctxt orf is_inductive_pred hol_ctxt
   8.865  
   8.866  (** Constant unfolding **)
   8.867  
   8.868 @@ -1551,12 +1658,14 @@
   8.869      s_betapplys Ts (func_t, map2 (select_nth_constr_arg ctxt x (Bound 0))
   8.870                                   (index_seq 0 (length arg_Ts)) arg_Ts)
   8.871    end
   8.872 +
   8.873  fun add_constr_case res_T (body_t, guard_t) res_t =
   8.874    if res_T = bool_T then
   8.875      s_conj (HOLogic.mk_imp (guard_t, body_t), res_t)
   8.876    else
   8.877      Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
   8.878      $ guard_t $ body_t $ res_t
   8.879 +
   8.880  fun optimized_case_def (hol_ctxt as {ctxt, ...}) Ts dataT res_T func_ts =
   8.881    let
   8.882      val xs = datatype_constrs hol_ctxt dataT
   8.883 @@ -1601,6 +1710,7 @@
   8.884                                  []))
   8.885      | j => select_nth_constr_arg ctxt constr_x t j res_T
   8.886    end
   8.887 +
   8.888  fun optimized_record_update (hol_ctxt as {thy, ctxt, ...}) s rec_T fun_t
   8.889                              rec_t =
   8.890    let
   8.891 @@ -1818,7 +1928,7 @@
   8.892                    else
   8.893                      (Const x, ts)
   8.894                  end
   8.895 -              else if is_equational_fun_but_no_plain_def hol_ctxt x orelse
   8.896 +              else if is_equational_fun hol_ctxt x orelse
   8.897                        is_choice_spec_fun hol_ctxt x then
   8.898                  (Const x, ts)
   8.899                else case def_of_const_ext thy def_tables x of
   8.900 @@ -1894,12 +2004,14 @@
   8.901          (map pair_for_prop ts) Symtab.empty)
   8.902  
   8.903  fun paired_with_consts t = map (rpair t) (Term.add_const_names t [])
   8.904 +
   8.905  fun const_nondef_table ts =
   8.906    fold (append o paired_with_consts) ts [] |> AList.group (op =) |> Symtab.make
   8.907  
   8.908  fun const_simp_table ctxt =
   8.909    def_table_for (map_filter (equationalize_term ctxt "nitpick_simp" o prop_of)
   8.910                   o Nitpick_Simps.get) ctxt
   8.911 +
   8.912  fun const_psimp_table ctxt =
   8.913    def_table_for (map_filter (equationalize_term ctxt "nitpick_psimp" o prop_of)
   8.914                   o Nitpick_Psimps.get) ctxt
   8.915 @@ -1941,6 +2053,7 @@
   8.916      |> pairself (specialize_type thy x o prop_of o the)
   8.917      ||> single |> op ::
   8.918    end
   8.919 +
   8.920  fun optimized_typedef_axioms ctxt (abs_z as (abs_s, _)) =
   8.921    let
   8.922      val thy = Proof_Context.theory_of ctxt
   8.923 @@ -1964,6 +2077,7 @@
   8.924        end
   8.925      | NONE => []
   8.926    end
   8.927 +
   8.928  fun optimized_quot_type_axioms ctxt abs_z =
   8.929    let
   8.930      val abs_T = Type abs_z
   8.931 @@ -2044,6 +2158,7 @@
   8.932    end
   8.933  
   8.934  val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb
   8.935 +
   8.936  fun wf_constraint_for rel side concl main =
   8.937    let
   8.938      val core = HOLogic.mk_mem (HOLogic.mk_prod
   8.939 @@ -2056,6 +2171,7 @@
   8.940                        $ Abs (x, T, abstract_over (Var ((x, j), T), t')))
   8.941                    (t, vars)
   8.942    end
   8.943 +
   8.944  fun wf_constraint_for_triple rel (side, main, concl) =
   8.945    map (wf_constraint_for rel side concl) main |> foldr1 s_conj
   8.946  
   8.947 @@ -2267,7 +2383,7 @@
   8.948      val unrolled_const = Const x' $ zero_const iter_T
   8.949      val def = the (def_of_const thy def_tables x)
   8.950    in
   8.951 -    if is_equational_fun_but_no_plain_def hol_ctxt x' then
   8.952 +    if is_equational_fun hol_ctxt x' then
   8.953        unrolled_const (* already done *)
   8.954      else if not gfp andalso star_linear_preds andalso
   8.955           is_linear_inductive_pred_def def andalso
   8.956 @@ -2314,6 +2430,7 @@
   8.957      HOLogic.mk_eq (list_comb (Const x, bounds), naked_rhs)
   8.958      |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
   8.959    end
   8.960 +
   8.961  fun inductive_pred_axiom hol_ctxt (x as (s, T)) =
   8.962    if String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s then
   8.963      let val x' = (strip_first_name_sep s |> snd, T) in
   8.964 @@ -2335,6 +2452,7 @@
   8.965                      | NONE => [])
   8.966             | psimps => psimps)
   8.967    | simps => simps
   8.968 +
   8.969  fun is_equational_fun_surely_complete hol_ctxt x =
   8.970    case equational_fun_axioms hol_ctxt x of
   8.971      [@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ _)] =>
   8.972 @@ -2383,8 +2501,10 @@
   8.973                         | xs => map snd xs)
   8.974        | _ => insert (op =) T accum
   8.975    in aux end
   8.976 +
   8.977  fun ground_types_in_type hol_ctxt binarize T =
   8.978    add_ground_types hol_ctxt binarize T []
   8.979 +
   8.980  fun ground_types_in_terms hol_ctxt binarize ts =
   8.981    fold (fold_types (add_ground_types hol_ctxt binarize)) ts []
   8.982  
     9.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Mar 03 22:33:22 2014 +0100
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Mar 03 22:33:22 2014 +0100
     9.3 @@ -126,7 +126,9 @@
     9.4  val upper_bound_for_rep = tuple_set_from_atom_schema o atom_schema_of_rep
     9.5  
     9.6  val single_atom = KK.TupleSet o single o KK.Tuple o single
     9.7 +
     9.8  fun sequential_int_bounds n = [(NONE, map single_atom (index_seq 0 n))]
     9.9 +
    9.10  fun pow_of_two_int_bounds bits j0 =
    9.11    let
    9.12      fun aux 0  _ _ = []
    9.13 @@ -164,6 +166,7 @@
    9.14                            else
    9.15                              NONE
    9.16                          end) (index_seq 0 k))
    9.17 +
    9.18  fun tabulate_op2 debug univ_card (k, j0) res_j0 f =
    9.19    (check_table_size (k * k);
    9.20     map_filter (fn j => let
    9.21 @@ -177,6 +180,7 @@
    9.22                           else
    9.23                             NONE
    9.24                         end) (index_seq 0 (k * k)))
    9.25 +
    9.26  fun tabulate_op2_2 debug univ_card (k, j0) res_j0 f =
    9.27    (check_table_size (k * k);
    9.28     map_filter (fn j => let
    9.29 @@ -191,11 +195,14 @@
    9.30                           else
    9.31                             NONE
    9.32                         end) (index_seq 0 (k * k)))
    9.33 +
    9.34  fun tabulate_nat_op2 debug univ_card (k, j0) f =
    9.35    tabulate_op2 debug univ_card (k, j0) j0 (atom_for_nat (k, 0) o f)
    9.36 +
    9.37  fun tabulate_int_op2 debug univ_card (k, j0) f =
    9.38    tabulate_op2 debug univ_card (k, j0) j0
    9.39                 (atom_for_int (k, 0) o f o pairself (int_for_atom (k, 0)))
    9.40 +
    9.41  fun tabulate_int_op2_2 debug univ_card (k, j0) f =
    9.42    tabulate_op2_2 debug univ_card (k, j0) j0
    9.43                   (pairself (atom_for_int (k, 0)) o f
    9.44 @@ -203,10 +210,13 @@
    9.45  
    9.46  fun isa_div (m, n) = m div n handle General.Div => 0
    9.47  fun isa_mod (m, n) = m mod n handle General.Div => m
    9.48 +
    9.49  fun isa_gcd (m, 0) = m
    9.50    | isa_gcd (m, n) = isa_gcd (n, isa_mod (m, n))
    9.51 +
    9.52  fun isa_lcm (m, n) = isa_div (m * n, isa_gcd (m, n))
    9.53  val isa_zgcd = isa_gcd o pairself abs
    9.54 +
    9.55  fun isa_norm_frac (m, n) =
    9.56    if n < 0 then isa_norm_frac (~m, ~n)
    9.57    else if m = 0 orelse n = 0 then (0, 1)
    9.58 @@ -282,6 +292,7 @@
    9.59      end
    9.60    else
    9.61      NONE
    9.62 +
    9.63  fun bounds_and_axioms_for_built_in_rels_in_formulas debug univ_card nat_card
    9.64                                                      int_card main_j0 formulas =
    9.65    let val rels = built_in_rels_in_formulas formulas in
    9.66 @@ -424,6 +435,7 @@
    9.67  fun unary_var_seq j0 n = map (curry KK.Var 1) (index_seq j0 n)
    9.68  
    9.69  val singleton_from_combination = foldl1 KK.Product o map KK.Atom
    9.70 +
    9.71  fun all_singletons_for_rep R =
    9.72    if is_lone_rep R then
    9.73      all_combinations_for_rep R |> map singleton_from_combination
    9.74 @@ -433,10 +445,12 @@
    9.75  fun unpack_products (KK.Product (r1, r2)) =
    9.76      unpack_products r1 @ unpack_products r2
    9.77    | unpack_products r = [r]
    9.78 +
    9.79  fun unpack_joins (KK.Join (r1, r2)) = unpack_joins r1 @ unpack_joins r2
    9.80    | unpack_joins r = [r]
    9.81  
    9.82  val empty_rel_for_rep = empty_n_ary_rel o arity_of_rep
    9.83 +
    9.84  fun full_rel_for_rep R =
    9.85    case atom_schema_of_rep R of
    9.86      [] => raise REP ("Nitpick_Kodkod.full_rel_for_rep", [R])
    9.87 @@ -471,6 +485,7 @@
    9.88      else
    9.89        KK.True
    9.90    end
    9.91 +
    9.92  fun kk_n_ary_function kk R (r as KK.Rel x) =
    9.93      if not (is_opt_rep R) then
    9.94        if x = suc_rel then
    9.95 @@ -499,15 +514,19 @@
    9.96      let val x = (KK.arity_of_rel_expr r, j) in
    9.97        kk_rel_let [KK.AssignRelReg (x, r)] (f (KK.RelReg x))
    9.98      end
    9.99 +
   9.100  val single_rel_rel_let = basic_rel_rel_let 0
   9.101 +
   9.102  fun double_rel_rel_let kk f r1 r2 =
   9.103    single_rel_rel_let kk (fn r1 => basic_rel_rel_let 1 kk (f r1) r2) r1
   9.104 +
   9.105  fun triple_rel_rel_let kk f r1 r2 r3 =
   9.106    double_rel_rel_let kk
   9.107        (fn r1 => fn r2 => basic_rel_rel_let 2 kk (f r1 r2) r3) r1 r2
   9.108  
   9.109  fun atom_from_formula ({kk_rel_if, ...} : kodkod_constrs) j0 f =
   9.110    kk_rel_if f (KK.Atom (j0 + 1)) (KK.Atom j0)
   9.111 +
   9.112  fun rel_expr_from_formula kk R f =
   9.113    case unopt_rep R of
   9.114      Atom (2, j0) => atom_from_formula kk j0 f
   9.115 @@ -723,7 +742,9 @@
   9.116                         unsigned_bit_word_sel_rel
   9.117                       else
   9.118                         signed_bit_word_sel_rel))
   9.119 +
   9.120  val int_expr_from_atom = KK.SetSum ooo bit_set_from_atom
   9.121 +
   9.122  fun atom_from_int_expr (kk as {kk_rel_eq, kk_comprehension, ...}
   9.123                          : kodkod_constrs) T R i =
   9.124    kk_comprehension (decls_for_atom_schema ~1 (atom_schema_of_rep R))
   9.125 @@ -1493,10 +1514,12 @@
   9.126                     else SOME ((x, kk_project r (map KK.Num [0, j])), T))
   9.127                 (index_seq 1 (arity - 1) ~~ tl type_schema)
   9.128    end
   9.129 +
   9.130  fun nfa_transitions_for_constr hol_ctxt binarize kk rel_table dtypes
   9.131                                 (x as (_, T)) =
   9.132    maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x)
   9.133         (index_seq 0 (num_sels_for_constr_type T))
   9.134 +
   9.135  fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : datatype_spec) = NONE
   9.136    | nfa_entry_for_datatype _ _ _ _ _ {deep = false, ...} = NONE
   9.137    | nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes
   9.138 @@ -1551,6 +1574,7 @@
   9.139      [kk_no (kk_intersect
   9.140                  (loop_path_rel_expr kk nfa (pull start_T (map fst nfa)) start_T)
   9.141                  KK.Iden)]
   9.142 +
   9.143  fun acyclicity_axioms_for_datatypes kk =
   9.144    maps (fn nfa => maps (acyclicity_axioms_for_datatype kk nfa o fst) nfa)
   9.145  
   9.146 @@ -1603,6 +1627,7 @@
   9.147  
   9.148  fun all_ge ({kk_join, kk_reflexive_closure, ...} : kodkod_constrs) z r =
   9.149    kk_join r (kk_reflexive_closure (KK.Rel (suc_rel_for_atom_seq z)))
   9.150 +
   9.151  fun gt ({kk_subset, kk_join, kk_closure, ...} : kodkod_constrs) z r1 r2 =
   9.152    kk_subset r1 (kk_join r2 (kk_closure (KK.Rel (suc_rel_for_atom_seq z))))
   9.153  
   9.154 @@ -1794,6 +1819,7 @@
   9.155                                 (kk_n_ary_function kk R2 r') (kk_no r'))]
   9.156        end
   9.157    end
   9.158 +
   9.159  fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk need_vals rel_table
   9.160          dtype (constr as {const, delta, epsilon, explicit_max, ...}) =
   9.161    let
   9.162 @@ -1822,6 +1848,7 @@
   9.163               (index_seq 0 (num_sels_for_constr_type (snd const)))
   9.164        end
   9.165    end
   9.166 +
   9.167  fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table need_vals
   9.168                              (dtype as {constrs, ...}) =
   9.169    maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table need_vals
   9.170 @@ -1851,12 +1878,14 @@
   9.171                     (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
   9.172                     (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))]
   9.173    end
   9.174 +
   9.175  fun uniqueness_axioms_for_datatype hol_ctxt binarize kk need_vals rel_table
   9.176                                     (dtype as {constrs, ...}) =
   9.177    maps (uniqueness_axioms_for_constr hol_ctxt binarize kk need_vals rel_table
   9.178                                       dtype) constrs
   9.179  
   9.180  fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
   9.181 +
   9.182  fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...})
   9.183          need_vals rel_table (dtype as {card, constrs, ...}) =
   9.184    if forall #exclusive constrs then
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Mar 03 22:33:22 2014 +0100
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Mar 03 22:33:22 2014 +0100
    10.3 @@ -7,13 +7,12 @@
    10.4  
    10.5  signature NITPICK_MODEL =
    10.6  sig
    10.7 -  type styp = Nitpick_Util.styp
    10.8    type scope = Nitpick_Scope.scope
    10.9    type rep = Nitpick_Rep.rep
   10.10    type nut = Nitpick_Nut.nut
   10.11  
   10.12    type params =
   10.13 -    {show_datatypes: bool,
   10.14 +    {show_types: bool,
   10.15       show_skolems: bool,
   10.16       show_consts: bool}
   10.17  
   10.18 @@ -37,9 +36,9 @@
   10.19    val dest_plain_fun : term -> bool * (term list * term list)
   10.20    val reconstruct_hol_model :
   10.21      params -> scope -> (term option * int list) list
   10.22 -    -> (typ option * string list) list -> styp list -> styp list -> nut list
   10.23 -    -> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
   10.24 -    -> Pretty.T * bool
   10.25 +    -> (typ option * string list) list -> (string * typ) list ->
   10.26 +    (string * typ) list -> nut list -> nut list -> nut list ->
   10.27 +    nut NameTable.table -> Kodkod.raw_bound list -> Pretty.T * bool
   10.28    val prove_hol_model :
   10.29      scope -> Time.time -> nut list -> nut list -> nut NameTable.table
   10.30      -> Kodkod.raw_bound list -> term -> bool option
   10.31 @@ -58,7 +57,7 @@
   10.32  structure KK = Kodkod
   10.33  
   10.34  type params =
   10.35 -  {show_datatypes: bool,
   10.36 +  {show_types: bool,
   10.37     show_skolems: bool,
   10.38     show_consts: bool}
   10.39  
   10.40 @@ -122,10 +121,12 @@
   10.41                length js + 1)
   10.42       | n => length js - n)
   10.43    | NONE => (Unsynchronized.change pool (cons (T, [j])); 1)
   10.44 +
   10.45  fun atom_suffix s =
   10.46    nat_subscript
   10.47    #> (s <> "" andalso Symbol.is_ascii_digit (List.last (raw_explode s)))  (* FIXME Symbol.explode (?) *)
   10.48       ? prefix "\<^sub>,"
   10.49 +
   10.50  fun nth_atom_name thy atomss pool prefix T j =
   10.51    let
   10.52      val ss = these (triple_lookup (type_match thy) atomss T)
   10.53 @@ -144,6 +145,7 @@
   10.54      | TFree (s, _) => prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s m
   10.55      | _ => raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
   10.56    end
   10.57 +
   10.58  fun nth_atom thy atomss pool for_auto T j =
   10.59    if for_auto then
   10.60      Free (nth_atom_name thy atomss pool (hd (space_explode "." nitpick_prefix))
   10.61 @@ -154,6 +156,7 @@
   10.62  fun extract_real_number (Const (@{const_name divide}, _) $ t1 $ t2) =
   10.63      real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
   10.64    | extract_real_number t = real (snd (HOLogic.dest_number t))
   10.65 +
   10.66  fun nice_term_ord (Abs (_, _, t1), Abs (_, _, t2)) = nice_term_ord (t1, t2)
   10.67    | nice_term_ord tp = Real.compare (pairself extract_real_number tp)
   10.68      handle TERM ("dest_number", _) =>
   10.69 @@ -166,16 +169,20 @@
   10.70  
   10.71  fun register_term_postprocessor_generic T postproc =
   10.72    Data.map (cons (T, postproc))
   10.73 +
   10.74  (* TODO: Consider morphism. *)
   10.75  fun register_term_postprocessor T postproc (_ : morphism) =
   10.76    register_term_postprocessor_generic T postproc
   10.77 +
   10.78  val register_term_postprocessor_global =
   10.79    Context.theory_map oo register_term_postprocessor_generic
   10.80  
   10.81  fun unregister_term_postprocessor_generic T = Data.map (AList.delete (op =) T)
   10.82  (* TODO: Consider morphism. *)
   10.83 +
   10.84  fun unregister_term_postprocessor T (_ : morphism) =
   10.85    unregister_term_postprocessor_generic T
   10.86 +
   10.87  val unregister_term_postprocessor_global =
   10.88    Context.theory_map o unregister_term_postprocessor_generic
   10.89  
   10.90 @@ -238,6 +245,7 @@
   10.91          Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
   10.92          $ aux T1 T2 tps $ t1 $ t2
   10.93    in aux T1 T2 o rev end
   10.94 +
   10.95  fun is_plain_fun (Const (s, _)) = (s = opt_flag orelse s = non_opt_flag)
   10.96    | is_plain_fun (Const (@{const_name fun_upd}, _) $ t0 $ _ $ _) =
   10.97      is_plain_fun t0
   10.98 @@ -260,6 +268,7 @@
   10.99      val (ps1, ps2) = pairself HOLogic.flat_tupleT_paths (T1, T2)
  10.100      val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut
  10.101    in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end
  10.102 +
  10.103  fun pair_up (Type (@{type_name prod}, [T1', T2']))
  10.104              (t1 as Const (@{const_name Pair},
  10.105                            Type (@{type_name fun},
  10.106 @@ -268,6 +277,7 @@
  10.107      if T1 = T1' then HOLogic.mk_prod (t1, t2)
  10.108      else HOLogic.mk_prod (t11, pair_up T2' t12 t2)
  10.109    | pair_up _ t1 t2 = HOLogic.mk_prod (t1, t2)
  10.110 +
  10.111  fun multi_pair_up T1 t1 (ts2, ts3) = map2 (pair o pair_up T1 t1) ts2 ts3
  10.112  
  10.113  fun format_fun T' T1 T2 t =
  10.114 @@ -689,6 +699,7 @@
  10.115                 else
  10.116                   [num_binder_types T]
  10.117    | NONE => [num_binder_types T]
  10.118 +
  10.119  fun intersect_formats _ [] = []
  10.120    | intersect_formats [] _ = []
  10.121    | intersect_formats ks1 ks2 =
  10.122 @@ -727,6 +738,7 @@
  10.123            |> map (HOLogic.mk_tupleT o rev)
  10.124        in List.foldl (op -->) body_T batched end
  10.125    end
  10.126 +
  10.127  fun format_term_type thy def_tables formats t =
  10.128    format_type (the (AList.lookup (op =) formats NONE))
  10.129                (lookup_format thy def_tables formats t) (fastype_of t)
  10.130 @@ -851,6 +863,7 @@
  10.131                                                  $ Bound 0 $ t')) =
  10.132      betapply (Abs (s, T, t'), t) |> unfold_outer_the_binders
  10.133    | unfold_outer_the_binders t = t
  10.134 +
  10.135  fun bisimilar_values _ 0 _ = true
  10.136    | bisimilar_values coTs max_depth (t1, t2) =
  10.137      let val T = fastype_of t1 in
  10.138 @@ -867,7 +880,7 @@
  10.139          t1 = t2
  10.140      end
  10.141  
  10.142 -fun reconstruct_hol_model {show_datatypes, show_skolems, show_consts}
  10.143 +fun reconstruct_hol_model {show_types, show_skolems, show_consts}
  10.144          ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, wfs, user_axioms,
  10.145                        debug, whacks, binary_ints, destroy_constrs, specialize,
  10.146                        star_linear_preds, total_consts, needs, tac_timeout,
  10.147 @@ -958,13 +971,13 @@
  10.148        datatypes |> filter #deep |> List.partition #co
  10.149                  ||> append (integer_datatype nat_T @ integer_datatype int_T)
  10.150      val block_of_datatypes =
  10.151 -      if show_datatypes andalso not (null datatypes) then
  10.152 +      if show_types andalso not (null datatypes) then
  10.153          [Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":")
  10.154                           (map pretty_for_datatype datatypes)]
  10.155        else
  10.156          []
  10.157      val block_of_codatatypes =
  10.158 -      if show_datatypes andalso not (null codatatypes) then
  10.159 +      if show_types andalso not (null codatatypes) then
  10.160          [Pretty.big_list ("Codatatype" ^ plural_s_for_list codatatypes ^ ":")
  10.161                           (map pretty_for_datatype codatatypes)]
  10.162        else
    11.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Mar 03 22:33:22 2014 +0100
    11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Mar 03 22:33:22 2014 +0100
    11.3 @@ -42,12 +42,13 @@
    11.4     alpha_T: typ,
    11.5     max_fresh: int Unsynchronized.ref,
    11.6     datatype_mcache: ((string * typ list) * mtyp) list Unsynchronized.ref,
    11.7 -   constr_mcache: (styp * mtyp) list Unsynchronized.ref}
    11.8 +   constr_mcache: ((string * typ) * mtyp) list Unsynchronized.ref}
    11.9  
   11.10  exception UNSOLVABLE of unit
   11.11  exception MTYPE of string * mtyp list * typ list
   11.12  
   11.13  val trace = Unsynchronized.ref false
   11.14 +
   11.15  fun trace_msg msg = if !trace then tracing (msg ()) else ()
   11.16  
   11.17  fun string_for_sign Plus = "+"
   11.18 @@ -57,8 +58,10 @@
   11.19    | negate_sign Minus = Plus
   11.20  
   11.21  val string_for_var = signed_string_of_int
   11.22 +
   11.23  fun string_for_vars sep [] = "0\<^bsub>" ^ sep ^ "\<^esub>"
   11.24    | string_for_vars sep xs = space_implode sep (map string_for_var xs)
   11.25 +
   11.26  fun subscript_string_for_vars sep xs =
   11.27    if null xs then "" else "\<^bsub>" ^ string_for_vars sep xs ^ "\<^esub>"
   11.28  
   11.29 @@ -79,6 +82,7 @@
   11.30  
   11.31  fun is_MRec (MRec _) = true
   11.32    | is_MRec _ = false
   11.33 +
   11.34  fun dest_MFun (MFun z) = z
   11.35    | dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M], [])
   11.36  
   11.37 @@ -126,6 +130,7 @@
   11.38      T = alpha_T orelse (not (is_fp_iterator_type T) andalso
   11.39                          exists (could_exist_alpha_subtype alpha_T) Ts)
   11.40    | could_exist_alpha_subtype alpha_T T = (T = alpha_T)
   11.41 +
   11.42  fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
   11.43      could_exist_alpha_subtype alpha_T T
   11.44    | could_exist_alpha_sub_mtype ctxt alpha_T T =
   11.45 @@ -269,9 +274,11 @@
   11.46  
   11.47  fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
   11.48    | prodM_factors M = [M]
   11.49 +
   11.50  fun curried_strip_mtype (MFun (M1, _, M2)) =
   11.51      curried_strip_mtype M2 |>> append (prodM_factors M1)
   11.52    | curried_strip_mtype M = ([], M)
   11.53 +
   11.54  fun sel_mtype_from_constr_mtype s M =
   11.55    let
   11.56      val (arg_Ms, dataM) = curried_strip_mtype M
   11.57 @@ -299,6 +306,7 @@
   11.58                   AList.lookup (op =) (!constr_mcache) x |> the)
   11.59    else
   11.60      fresh_mtype_for_type mdata false T
   11.61 +
   11.62  fun mtype_for_sel (mdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
   11.63    x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
   11.64      |> mtype_for_constr mdata |> sel_mtype_from_constr_mtype s
   11.65 @@ -306,6 +314,7 @@
   11.66  fun resolve_annotation_atom asgs (V x) =
   11.67      x |> AList.lookup (op =) asgs |> Option.map A |> the_default (V x)
   11.68    | resolve_annotation_atom _ aa = aa
   11.69 +
   11.70  fun resolve_mtype asgs =
   11.71    let
   11.72      fun aux MAlpha = MAlpha
   11.73 @@ -474,29 +483,37 @@
   11.74  val annotation_from_bools = AList.find (op =) bool_table #> the_single
   11.75  
   11.76  fun prop_for_bool b = if b then Prop_Logic.True else Prop_Logic.False
   11.77 +
   11.78  fun prop_for_bool_var_equality (v1, v2) =
   11.79    Prop_Logic.SAnd (Prop_Logic.SOr (Prop_Logic.BoolVar v1,
   11.80                                     Prop_Logic.SNot (Prop_Logic.BoolVar v2)),
   11.81                     Prop_Logic.SOr (Prop_Logic.SNot (Prop_Logic.BoolVar v1),
   11.82                                     Prop_Logic.BoolVar v2))
   11.83 +
   11.84  fun prop_for_assign (x, a) =
   11.85    let val (b1, b2) = bools_from_annotation a in
   11.86      Prop_Logic.SAnd (Prop_Logic.BoolVar (fst_var x) |> not b1 ? Prop_Logic.SNot,
   11.87                       Prop_Logic.BoolVar (snd_var x) |> not b2 ? Prop_Logic.SNot)
   11.88    end
   11.89 +
   11.90  fun prop_for_assign_literal (x, (Plus, a)) = prop_for_assign (x, a)
   11.91    | prop_for_assign_literal (x, (Minus, a)) =
   11.92      Prop_Logic.SNot (prop_for_assign (x, a))
   11.93 +
   11.94  fun prop_for_atom_assign (A a', a) = prop_for_bool (a = a')
   11.95    | prop_for_atom_assign (V x, a) = prop_for_assign_literal (x, (Plus, a))
   11.96 +
   11.97  fun prop_for_atom_equality (aa1, A a2) = prop_for_atom_assign (aa1, a2)
   11.98    | prop_for_atom_equality (A a1, aa2) = prop_for_atom_assign (aa2, a1)
   11.99    | prop_for_atom_equality (V x1, V x2) =
  11.100      Prop_Logic.SAnd (prop_for_bool_var_equality (pairself fst_var (x1, x2)),
  11.101               prop_for_bool_var_equality (pairself snd_var (x1, x2)))
  11.102 +
  11.103  val prop_for_assign_clause = Prop_Logic.exists o map prop_for_assign_literal
  11.104 +
  11.105  fun prop_for_exists_var_assign_literal xs a =
  11.106    Prop_Logic.exists (map (fn x => prop_for_assign_literal (x, (Plus, a))) xs)
  11.107 +
  11.108  fun prop_for_comp (aa1, aa2, Eq, []) =
  11.109      Prop_Logic.SAnd (prop_for_comp (aa1, aa2, Leq, []),
  11.110               prop_for_comp (aa2, aa1, Leq, []))
  11.111 @@ -578,16 +595,18 @@
  11.112    {bound_Ts: typ list,
  11.113     bound_Ms: mtyp list,
  11.114     frame: (int * annotation_atom) list,
  11.115 -   frees: (styp * mtyp) list,
  11.116 -   consts: (styp * mtyp) list}
  11.117 +   frees: ((string * typ) * mtyp) list,
  11.118 +   consts: ((string * typ) * mtyp) list}
  11.119  
  11.120  fun string_for_bound ctxt Ms (j, aa) =
  11.121    Syntax.string_of_term ctxt (Bound (length Ms - j - 1)) ^ " :\<^bsup>" ^
  11.122    string_for_annotation_atom aa ^ "\<^esup> " ^
  11.123    string_for_mtype (nth Ms (length Ms - j - 1))
  11.124 +
  11.125  fun string_for_free relevant_frees ((s, _), M) =
  11.126    if member (op =) relevant_frees s then SOME (s ^ " : " ^ string_for_mtype M)
  11.127    else NONE
  11.128 +
  11.129  fun string_for_mcontext ctxt t ({bound_Ms, frame, frees, ...} : mcontext) =
  11.130    (map_filter (string_for_free (Term.add_free_names t [])) frees @
  11.131     map (string_for_bound ctxt bound_Ms) frame)
  11.132 @@ -599,6 +618,7 @@
  11.133  fun push_bound aa T M {bound_Ts, bound_Ms, frame, frees, consts} =
  11.134    {bound_Ts = T :: bound_Ts, bound_Ms = M :: bound_Ms,
  11.135     frame = frame @ [(length bound_Ts, aa)], frees = frees, consts = consts}
  11.136 +
  11.137  fun pop_bound {bound_Ts, bound_Ms, frame, frees, consts} =
  11.138    {bound_Ts = tl bound_Ts, bound_Ms = tl bound_Ms,
  11.139     frame = frame |> filter_out (fn (j, _) => j = length bound_Ts - 1),
  11.140 @@ -678,6 +698,7 @@
  11.141                         string_for_annotation_atom aa2);
  11.142     fold (add_assign_clause o assign_clause_from_quasi_clause)
  11.143          (mk_quasi_clauses res_aa aa1 aa2))
  11.144 +
  11.145  fun add_connective_frames conn mk_quasi_clauses res_frame frame1 frame2 =
  11.146    fold I (map3 (fn (_, res_aa) => fn (_, aa1) => fn (_, aa2) =>
  11.147                     add_connective_var conn mk_quasi_clauses res_aa aa1 aa2)
  11.148 @@ -709,6 +730,7 @@
  11.149  
  11.150  fun add_arg_order1 ((_, aa), (_, prev_aa)) = I
  11.151    add_annotation_atom_comp_alt Neq prev_aa (A Gen) aa
  11.152 +
  11.153  fun add_app1 fun_aa ((_, res_aa), (_, arg_aa)) = I
  11.154    let
  11.155      val clause = [(arg_aa, (Eq, New)), (res_aa, (Eq, Gen))]
  11.156 @@ -718,6 +740,7 @@
  11.157      apsnd (add_assign_clause clause)
  11.158      #> add_annotation_atom_comp_alt Leq arg_aa fun_aa res_aa
  11.159    end
  11.160 +
  11.161  fun add_app _ [] [] = I
  11.162    | add_app fun_aa res_frame arg_frame =
  11.163      add_comp_frame (A New) Leq arg_frame
  11.164 @@ -986,6 +1009,7 @@
  11.165    | force_gen_funs n (M as MFun (M1, _, M2)) =
  11.166      add_mtypes_equal M (MFun (M1, A Gen, M2)) #> force_gen_funs (n - 1) M2
  11.167    | force_gen_funs _ M = raise MTYPE ("Nitpick_Mono.force_gen_funs", [M], [])
  11.168 +
  11.169  fun consider_general_equals mdata def t1 t2 accum =
  11.170    let
  11.171      val (M1, accum) = consider_term mdata t1 accum
    12.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Mar 03 22:33:22 2014 +0100
    12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Mar 03 22:33:22 2014 +0100
    12.3 @@ -7,7 +7,6 @@
    12.4  
    12.5  signature NITPICK_NUT =
    12.6  sig
    12.7 -  type styp = Nitpick_Util.styp
    12.8    type hol_context = Nitpick_HOL.hol_context
    12.9    type scope = Nitpick_Scope.scope
   12.10    type name_pool = Nitpick_Peephole.name_pool
   12.11 @@ -100,7 +99,7 @@
   12.12    val nut_from_term : hol_context -> op2 -> term -> nut
   12.13    val is_fully_representable_set : nut -> bool
   12.14    val choose_reps_for_free_vars :
   12.15 -    scope -> styp list -> nut list -> rep NameTable.table
   12.16 +    scope -> (string * typ) list -> nut list -> rep NameTable.table
   12.17      -> nut list * rep NameTable.table
   12.18    val choose_reps_for_consts :
   12.19      scope -> bool -> nut list -> rep NameTable.table
   12.20 @@ -333,9 +332,11 @@
   12.21    space_explode name_sep (nickname_of u)
   12.22    |> exists (String.isPrefix skolem_prefix)
   12.23    handle NUT ("Nitpick_Nut.nickname_of", _) => false
   12.24 +
   12.25  fun is_eval_name u =
   12.26    String.isPrefix eval_prefix (nickname_of u)
   12.27    handle NUT ("Nitpick_Nut.nickname_of", _) => false
   12.28 +
   12.29  fun is_Cst cst (Cst (cst', _, _)) = (cst = cst')
   12.30    | is_Cst _ _ = false
   12.31  
   12.32 @@ -347,6 +348,7 @@
   12.33    | Tuple (_, _, us) => fold (fold_nut f) us
   12.34    | Construct (us', _, _, us) => fold (fold_nut f) us #> fold (fold_nut f) us'
   12.35    | _ => f u
   12.36 +
   12.37  fun map_nut f u =
   12.38    case u of
   12.39      Op1 (oper, T, R, u1) => Op1 (oper, T, R, map_nut f u1)
   12.40 @@ -398,6 +400,7 @@
   12.41    case NameTable.lookup table name of
   12.42      SOME u => u
   12.43    | NONE => raise NUT ("Nitpick_Nut.the_name", [name])
   12.44 +
   12.45  fun the_rel table name =
   12.46    case the_name table name of
   12.47      FreeRel (x, _, _, _) => x
   12.48 @@ -408,12 +411,14 @@
   12.49      let val res_T = fst (HOLogic.dest_prodT T) in
   12.50        (res_T, Const (@{const_name fst}, T --> res_T) $ t)
   12.51      end
   12.52 +
   12.53  fun mk_snd (_, Const (@{const_name Pair}, T) $ _ $ t2) =
   12.54      (domain_type (range_type T), t2)
   12.55    | mk_snd (T, t) =
   12.56      let val res_T = snd (HOLogic.dest_prodT T) in
   12.57        (res_T, Const (@{const_name snd}, T --> res_T) $ t)
   12.58      end
   12.59 +
   12.60  fun factorize (z as (Type (@{type_name prod}, _), _)) =
   12.61      maps factorize [mk_fst z, mk_snd z]
   12.62    | factorize z = [z]
   12.63 @@ -649,6 +654,7 @@
   12.64                 best_non_opt_set_rep_for_type) scope (type_of v)
   12.65      val v = modify_name_rep v R
   12.66    in (v :: vs, NameTable.update (v, R) table) end
   12.67 +
   12.68  fun choose_rep_for_const (scope as {hol_ctxt = {ctxt, ...}, ...}) total_consts v
   12.69                           (vs, table) =
   12.70    let
   12.71 @@ -674,6 +680,7 @@
   12.72  
   12.73  fun choose_reps_for_free_vars scope pseudo_frees vs table =
   12.74    fold (choose_rep_for_free_var scope pseudo_frees) vs ([], table)
   12.75 +
   12.76  fun choose_reps_for_consts scope total_consts vs table =
   12.77    fold (choose_rep_for_const scope total_consts) vs ([], table)
   12.78  
   12.79 @@ -690,12 +697,15 @@
   12.80                 best_opt_set_rep_for_type scope T' |> unopt_rep
   12.81      val v = ConstName (s', T', R')
   12.82    in (v :: vs, NameTable.update (v, R') table) end
   12.83 +
   12.84  fun choose_rep_for_sels_for_constr scope (x as (_, T)) =
   12.85    fold_rev (choose_rep_for_nth_sel_for_constr scope x)
   12.86             (~1 upto num_sels_for_constr_type T - 1)
   12.87 +
   12.88  fun choose_rep_for_sels_of_datatype _ ({deep = false, ...} : datatype_spec) = I
   12.89    | choose_rep_for_sels_of_datatype scope {constrs, ...} =
   12.90      fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
   12.91 +
   12.92  fun choose_reps_for_all_sels (scope as {datatypes, ...}) =
   12.93    fold (choose_rep_for_sels_of_datatype scope) datatypes o pair []
   12.94  
   12.95 @@ -744,6 +754,7 @@
   12.96      else
   12.97        raise SAME ())
   12.98     handle SAME () => Op1 (oper, T, R, u1))
   12.99 +
  12.100  fun s_op2 oper T R u1 u2 =
  12.101    ((case oper of
  12.102        All => if is_subnut_of u1 u2 then Op2 (All, T, R, u1, u2) else u2
  12.103 @@ -785,6 +796,7 @@
  12.104          raise SAME ()
  12.105      | _ => raise SAME ())
  12.106     handle SAME () => Op2 (oper, T, R, u1, u2))
  12.107 +
  12.108  fun s_op3 oper T R u1 u2 u3 =
  12.109    ((case oper of
  12.110        Let =>
  12.111 @@ -794,6 +806,7 @@
  12.112          raise SAME ()
  12.113      | _ => raise SAME ())
  12.114     handle SAME () => Op3 (oper, T, R, u1, u2, u3))
  12.115 +
  12.116  fun s_tuple T R us =
  12.117    if exists (is_Cst Unrep) us then Cst (Unrep, T, R) else Tuple (T, R, us)
  12.118  
  12.119 @@ -1077,19 +1090,23 @@
  12.120    | fresh_n_ary_index n ((m, j) :: xs) ys =
  12.121      if m = n then (j, ys @ ((m, j + 1) :: xs))
  12.122      else fresh_n_ary_index n xs ((m, j) :: ys)
  12.123 +
  12.124  fun fresh_rel n {rels, vars, formula_reg, rel_reg} =
  12.125    let val (j, rels') = fresh_n_ary_index n rels [] in
  12.126      (j, {rels = rels', vars = vars, formula_reg = formula_reg,
  12.127           rel_reg = rel_reg})
  12.128    end
  12.129 +
  12.130  fun fresh_var n {rels, vars, formula_reg, rel_reg} =
  12.131    let val (j, vars') = fresh_n_ary_index n vars [] in
  12.132      (j, {rels = rels, vars = vars', formula_reg = formula_reg,
  12.133           rel_reg = rel_reg})
  12.134    end
  12.135 +
  12.136  fun fresh_formula_reg {rels, vars, formula_reg, rel_reg} =
  12.137    (formula_reg, {rels = rels, vars = vars, formula_reg = formula_reg + 1,
  12.138                   rel_reg = rel_reg})
  12.139 +
  12.140  fun fresh_rel_reg {rels, vars, formula_reg, rel_reg} =
  12.141    (rel_reg, {rels = rels, vars = vars, formula_reg = formula_reg,
  12.142               rel_reg = rel_reg + 1})
    13.1 --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Mon Mar 03 22:33:22 2014 +0100
    13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Mon Mar 03 22:33:22 2014 +0100
    13.3 @@ -128,14 +128,18 @@
    13.4  fun formula_for_bool b = if b then True else False
    13.5  
    13.6  fun atom_for_nat (k, j0) n = if n < 0 orelse n >= k then ~1 else n + j0
    13.7 +
    13.8  fun min_int_for_card k = ~k div 2 + 1
    13.9  fun max_int_for_card k = k div 2
   13.10 +
   13.11  fun int_for_atom (k, j0) j =
   13.12    let val j = j - j0 in if j <= max_int_for_card k then j else j - k end
   13.13 +
   13.14  fun atom_for_int (k, j0) n =
   13.15    if n < min_int_for_card k orelse n > max_int_for_card k then ~1
   13.16    else if n < 0 then n + k + j0
   13.17    else n + j0
   13.18 +
   13.19  fun is_twos_complement_representable bits n =
   13.20    let val max = reasonable_power 2 bits in n >= ~ max andalso n < max end
   13.21  
   13.22 @@ -147,6 +151,7 @@
   13.23                       "too large cardinality (" ^ string_of_int n ^ ")")
   13.24    else
   13.25      (max_squeeze_card + 1) * m + n
   13.26 +
   13.27  fun unsqueeze p = (p div (max_squeeze_card + 1), p mod (max_squeeze_card + 1))
   13.28  
   13.29  fun boolify (j, b) = 2 * j + (if b then 0 else 1)
   13.30 @@ -154,6 +159,7 @@
   13.31  
   13.32  fun suc_rel_for_atom_seq (x, tabulate) =
   13.33    (2, suc_rels_base - boolify (squeeze x, tabulate))
   13.34 +
   13.35  fun atom_seq_for_suc_rel (_, j) = unboolify (~ j + suc_rels_base) |>> unsqueeze
   13.36  
   13.37  fun is_none_product (Product (r1, r2)) =
   13.38 @@ -206,8 +212,10 @@
   13.39  
   13.40  fun is_Num (Num _) = true
   13.41    | is_Num _ = false
   13.42 +
   13.43  fun dest_Num (Num k) = k
   13.44    | dest_Num _ = raise ARG ("Nitpick_Peephole.dest_Num", "not \"Num\"")
   13.45 +
   13.46  fun num_seq j0 n = map Num (index_seq j0 n)
   13.47  
   13.48  fun occurs_in_union r (Union (r1, r2)) =
    14.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Mar 03 22:33:22 2014 +0100
    14.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Mar 03 22:33:22 2014 +0100
    14.3 @@ -74,7 +74,7 @@
    14.4          let val table = aux t2 [] table in aux t1 (t2 :: args) table end
    14.5        | aux (Abs (_, _, t')) _ table = aux t' [] table
    14.6        | aux (t as Const (x as (s, _))) args table =
    14.7 -        if is_built_in_const x orelse is_constr_like ctxt x orelse
    14.8 +        if is_built_in_const x orelse is_nonfree_constr ctxt x orelse
    14.9             is_sel s orelse s = @{const_name Sigma} then
   14.10            table
   14.11          else
   14.12 @@ -230,7 +230,7 @@
   14.13                      else if is_built_in_const x orelse
   14.14                              s = @{const_name Sigma} then
   14.15                        T
   14.16 -                    else if is_constr_like ctxt x then
   14.17 +                    else if is_nonfree_constr ctxt x then
   14.18                        box_type hol_ctxt InConstr T
   14.19                      else if is_sel s orelse is_rep_fun ctxt x then
   14.20                        box_type hol_ctxt InSel T
   14.21 @@ -617,8 +617,8 @@
   14.22          | (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 =>
   14.23            t0 $ t1 $ aux ss Ts js skolemizable polar t2
   14.24          | Const (x as (s, T)) =>
   14.25 -          if is_real_inductive_pred hol_ctxt x andalso
   14.26 -             not (is_real_equational_fun hol_ctxt x) andalso
   14.27 +          if is_raw_inductive_pred hol_ctxt x andalso
   14.28 +             not (is_raw_equational_fun hol_ctxt x) andalso
   14.29               not (is_well_founded_inductive_pred hol_ctxt x) then
   14.30              let
   14.31                val gfp = (fixpoint_kind_of_const thy def_tables x = Gfp)
   14.32 @@ -704,6 +704,7 @@
   14.33                   | [t as Free _] => cons (j, SOME t)
   14.34                   | _ => I) indexed_sets []
   14.35    end
   14.36 +
   14.37  fun static_args_in_terms hol_ctxt x =
   14.38    map (static_args_in_term hol_ctxt x)
   14.39    #> fold1 (Ord_List.inter (prod_ord int_ord (option_ord Term_Ord.term_ord)))
   14.40 @@ -740,7 +741,7 @@
   14.41            ((if not (member (op =) blacklist x) andalso not (null args) andalso
   14.42                 not (String.isPrefix special_prefix s) andalso
   14.43                 not (is_built_in_const x) andalso
   14.44 -               (is_equational_fun_but_no_plain_def hol_ctxt x orelse
   14.45 +               (is_equational_fun hol_ctxt x orelse
   14.46                  (is_some (def_of_const thy def_tables x) andalso
   14.47                   not (is_of_class_const thy x) andalso
   14.48                   not (is_constr ctxt x) andalso
   14.49 @@ -804,7 +805,7 @@
   14.50          | aux args _ t = list_comb (t, args)
   14.51      in aux [] [] t end
   14.52  
   14.53 -type special_triple = int list * term list * styp
   14.54 +type special_triple = int list * term list * (string * typ)
   14.55  
   14.56  val cong_var_prefix = "c"
   14.57  
   14.58 @@ -880,6 +881,7 @@
   14.59    | NONE => false
   14.60  
   14.61  fun all_table_entries table = Symtab.fold (append o snd) table []
   14.62 +
   14.63  fun extra_table tables s =
   14.64    Symtab.make [(s, pairself all_table_entries tables |> op @)]
   14.65  
   14.66 @@ -899,7 +901,7 @@
   14.67      val (def_assm_ts, nondef_assm_ts) =
   14.68        List.partition (assumption_exclusively_defines_free assm_ts) assm_ts
   14.69      val def_assm_table = map (`(the o defined_free_by_assumption)) def_assm_ts
   14.70 -    type accumulator = styp list * (term list * term list)
   14.71 +    type accumulator = (string * typ) list * (term list * term list)
   14.72      fun add_axiom get app def depth t (accum as (seen, axs)) =
   14.73        let
   14.74          val t = t |> unfold_defs_in_term hol_ctxt
   14.75 @@ -951,7 +953,7 @@
   14.76               else if is_descr (original_name s) then
   14.77                 fold (add_nondef_axiom depth) (equational_fun_axioms hol_ctxt x)
   14.78                      accum
   14.79 -             else if is_equational_fun_but_no_plain_def hol_ctxt x then
   14.80 +             else if is_equational_fun hol_ctxt x then
   14.81                 fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
   14.82                      accum
   14.83               else if is_choice_spec_fun hol_ctxt x then
   14.84 @@ -1066,7 +1068,7 @@
   14.85          do_term t1 []
   14.86        | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
   14.87        | do_term (t as Const (x as (s, T))) (args as _ :: _) =
   14.88 -        ((if is_constr_like ctxt x then
   14.89 +        ((if is_nonfree_constr ctxt x then
   14.90              if length args = num_binder_types T then
   14.91                case hd args of
   14.92                  Const (_, T') $ t' =>
   14.93 @@ -1082,7 +1084,7 @@
   14.94            else if is_sel_like_and_no_discr s then
   14.95              case strip_comb (hd args) of
   14.96                (Const (x' as (s', T')), ts') =>
   14.97 -              if is_constr_like_injective ctxt x' andalso
   14.98 +              if is_free_constr ctxt x' andalso
   14.99                   constr_name_for_sel_like s = s' andalso
  14.100                   not (exists is_pair_type (binder_types T')) then
  14.101                  list_comb (nth ts' (sel_no_from_name s), tl args)
    15.1 --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML	Mon Mar 03 22:33:22 2014 +0100
    15.2 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML	Mon Mar 03 22:33:22 2014 +0100
    15.3 @@ -97,8 +97,10 @@
    15.4  
    15.5  fun is_Func (Func _) = true
    15.6    | is_Func _ = false
    15.7 +
    15.8  fun is_Opt (Opt _) = true
    15.9    | is_Opt _ = false
   15.10 +
   15.11  fun is_opt_rep (Func (_, R2)) = is_opt_rep R2
   15.12    | is_opt_rep (Opt _) = true
   15.13    | is_opt_rep _ = false
   15.14 @@ -111,6 +113,7 @@
   15.15    | card_of_rep (Func (R1, R2)) =
   15.16      reasonable_power (card_of_rep R2) (card_of_rep R1)
   15.17    | card_of_rep (Opt R) = card_of_rep R
   15.18 +
   15.19  fun arity_of_rep Any = raise REP ("Nitpick_Rep.arity_of_rep", [Any])
   15.20    | arity_of_rep (Formula _) = 0
   15.21    | arity_of_rep (Atom _) = 1
   15.22 @@ -118,6 +121,7 @@
   15.23    | arity_of_rep (Vect (k, R)) = k * arity_of_rep R
   15.24    | arity_of_rep (Func (R1, R2)) = arity_of_rep R1 + arity_of_rep R2
   15.25    | arity_of_rep (Opt R) = arity_of_rep R
   15.26 +
   15.27  fun min_univ_card_of_rep Any =
   15.28      raise REP ("Nitpick_Rep.min_univ_card_of_rep", [Any])
   15.29    | min_univ_card_of_rep (Formula _) = 0
   15.30 @@ -133,11 +137,13 @@
   15.31    | is_one_rep (Struct _) = true
   15.32    | is_one_rep (Vect _) = true
   15.33    | is_one_rep _ = false
   15.34 +
   15.35  fun is_lone_rep (Opt R) = is_one_rep R
   15.36    | is_lone_rep R = is_one_rep R
   15.37  
   15.38  fun dest_Func (Func z) = z
   15.39    | dest_Func R = raise REP ("Nitpick_Rep.dest_Func", [R])
   15.40 +
   15.41  fun lazy_range_rep _ _ _ (Vect (_, R)) = R
   15.42    | lazy_range_rep _ _ _ (Func (_, R2)) = R2
   15.43    | lazy_range_rep ofs T ran_card (Opt R) =
   15.44 @@ -150,6 +156,7 @@
   15.45  
   15.46  fun binder_reps (Func (R1, R2)) = R1 :: binder_reps R2
   15.47    | binder_reps _ = []
   15.48 +
   15.49  fun body_rep (Func (_, R2)) = body_rep R2
   15.50    | body_rep R = R
   15.51  
   15.52 @@ -163,16 +170,19 @@
   15.53    | one_rep _ _ (Vect z) = Vect z
   15.54    | one_rep ofs T (Opt R) = one_rep ofs T R
   15.55    | one_rep ofs T R = Atom (card_of_rep R, offset_of_type ofs T)
   15.56 +
   15.57  fun optable_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) =
   15.58      Func (R1, optable_rep ofs T2 R2)
   15.59    | optable_rep ofs (Type (@{type_name set}, [T'])) R =
   15.60      optable_rep ofs (T' --> bool_T) R
   15.61    | optable_rep ofs T R = one_rep ofs T R
   15.62 +
   15.63  fun opt_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) =
   15.64      Func (R1, opt_rep ofs T2 R2)
   15.65    | opt_rep ofs (Type (@{type_name set}, [T'])) R =
   15.66      opt_rep ofs (T' --> bool_T) R
   15.67    | opt_rep ofs T R = Opt (optable_rep ofs T R)
   15.68 +
   15.69  fun unopt_rep (Func (R1, R2)) = Func (R1, unopt_rep R2)
   15.70    | unopt_rep (Opt R) = R
   15.71    | unopt_rep R = R
   15.72 @@ -254,6 +264,7 @@
   15.73      best_opt_set_rep_for_type scope (T' --> bool_T)
   15.74    | best_opt_set_rep_for_type (scope as {ofs, ...}) T =
   15.75      opt_rep ofs T (best_one_rep_for_type scope T)
   15.76 +
   15.77  fun best_non_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) =
   15.78      (case (best_one_rep_for_type scope T1,
   15.79             best_non_opt_set_rep_for_type scope T2) of
   15.80 @@ -262,9 +273,11 @@
   15.81    | best_non_opt_set_rep_for_type scope (Type (@{type_name set}, [T'])) =
   15.82      best_non_opt_set_rep_for_type scope (T' --> bool_T)
   15.83    | best_non_opt_set_rep_for_type scope T = best_one_rep_for_type scope T
   15.84 +
   15.85  fun best_set_rep_for_type (scope as {datatypes, ...}) T =
   15.86    (if is_exact_type datatypes true T then best_non_opt_set_rep_for_type
   15.87     else best_opt_set_rep_for_type) scope T
   15.88 +
   15.89  fun best_non_opt_symmetric_reps_for_fun_type (scope as {ofs, ...})
   15.90                                             (Type (@{type_name fun}, [T1, T2])) =
   15.91      (optable_rep ofs T1 (best_one_rep_for_type scope T1),
    16.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Mar 03 22:33:22 2014 +0100
    16.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Mar 03 22:33:22 2014 +0100
    16.3 @@ -7,11 +7,10 @@
    16.4  
    16.5  signature NITPICK_SCOPE =
    16.6  sig
    16.7 -  type styp = Nitpick_Util.styp
    16.8    type hol_context = Nitpick_HOL.hol_context
    16.9  
   16.10    type constr_spec =
   16.11 -    {const: styp,
   16.12 +    {const: string * typ,
   16.13       delta: int,
   16.14       epsilon: int,
   16.15       exclusive: bool,
   16.16 @@ -39,7 +38,7 @@
   16.17  
   16.18    val is_asymmetric_nondatatype : typ -> bool
   16.19    val datatype_spec : datatype_spec list -> typ -> datatype_spec option
   16.20 -  val constr_spec : datatype_spec list -> styp -> constr_spec
   16.21 +  val constr_spec : datatype_spec list -> string * typ -> constr_spec
   16.22    val is_complete_type : datatype_spec list -> bool -> typ -> bool
   16.23    val is_concrete_type : datatype_spec list -> bool -> typ -> bool
   16.24    val is_exact_type : datatype_spec list -> bool -> typ -> bool
   16.25 @@ -51,10 +50,10 @@
   16.26    val scope_less_eq : scope -> scope -> bool
   16.27    val is_self_recursive_constr_type : typ -> bool
   16.28    val all_scopes :
   16.29 -    hol_context -> bool -> (typ option * int list) list
   16.30 -    -> (styp option * int list) list -> (styp option * int list) list
   16.31 -    -> int list -> int list -> typ list -> typ list -> typ list -> typ list
   16.32 -    -> int * scope list
   16.33 +    hol_context -> bool -> (typ option * int list) list ->
   16.34 +    ((string * typ) option * int list) list ->
   16.35 +    ((string * typ) option * int list) list -> int list -> int list ->
   16.36 +    typ list -> typ list -> typ list -> typ list -> int * scope list
   16.37  end;
   16.38  
   16.39  structure Nitpick_Scope : NITPICK_SCOPE =
   16.40 @@ -64,7 +63,7 @@
   16.41  open Nitpick_HOL
   16.42  
   16.43  type constr_spec =
   16.44 -  {const: styp,
   16.45 +  {const: string * typ,
   16.46     delta: int,
   16.47     epsilon: int,
   16.48     exclusive: bool,
   16.49 @@ -90,7 +89,7 @@
   16.50     datatypes: datatype_spec list,
   16.51     ofs: int Typtab.table}
   16.52  
   16.53 -datatype row_kind = Card of typ | Max of styp
   16.54 +datatype row_kind = Card of typ | Max of string * typ
   16.55  
   16.56  type row = row_kind * int list
   16.57  type block = row list
   16.58 @@ -212,23 +211,29 @@
   16.59  
   16.60  fun scopes_equivalent (s1 : scope, s2 : scope) =
   16.61    #datatypes s1 = #datatypes s2 andalso #card_assigns s1 = #card_assigns s2
   16.62 +
   16.63  fun scope_less_eq (s1 : scope) (s2 : scope) =
   16.64    (s1, s2) |> pairself (map snd o #card_assigns) |> op ~~ |> forall (op <=)
   16.65  
   16.66  fun rank_of_row (_, ks) = length ks
   16.67 +
   16.68  fun rank_of_block block = fold Integer.max (map rank_of_row block) 1
   16.69 +
   16.70  fun project_row _ (y, []) = (y, [1]) (* desperate measure *)
   16.71    | project_row column (y, ks) = (y, [nth ks (Int.min (column, length ks - 1))])
   16.72 +
   16.73  fun project_block (column, block) = map (project_row column) block
   16.74  
   16.75  fun lookup_ints_assign eq assigns key =
   16.76    case triple_lookup eq assigns key of
   16.77      SOME ks => ks
   16.78    | NONE => raise ARG ("Nitpick_Scope.lookup_ints_assign", "")
   16.79 +
   16.80  fun lookup_type_ints_assign thy assigns T =
   16.81    map (Integer.max 1) (lookup_ints_assign (type_match thy) assigns T)
   16.82    handle ARG ("Nitpick_Scope.lookup_ints_assign", _) =>
   16.83           raise TYPE ("Nitpick_Scope.lookup_type_ints_assign", [T], [])
   16.84 +
   16.85  fun lookup_const_ints_assign thy assigns x =
   16.86    lookup_ints_assign (const_match thy) assigns x
   16.87    handle ARG ("Nitpick_Scope.lookup_ints_assign", _) =>
   16.88 @@ -295,7 +300,7 @@
   16.89  
   16.90  fun constr_max maxes x = the_default ~1 (AList.lookup (op =) maxes x)
   16.91  
   16.92 -type scope_desc = (typ * int) list * (styp * int) list
   16.93 +type scope_desc = (typ * int) list * ((string * typ) * int) list
   16.94  
   16.95  fun is_surely_inconsistent_card_assign hol_ctxt binarize
   16.96                                         (card_assigns, max_assigns) (T, k) =
   16.97 @@ -311,6 +316,7 @@
   16.98          | effective_max card max = Int.min (card, max)
   16.99        val max = map2 effective_max dom_cards maxes |> Integer.sum
  16.100      in max < k end
  16.101 +
  16.102  fun is_surely_inconsistent_scope_description hol_ctxt binarize seen rest
  16.103                                               max_assigns =
  16.104    exists (is_surely_inconsistent_card_assign hol_ctxt binarize
  16.105 @@ -348,8 +354,10 @@
  16.106    case kind of
  16.107      Card T => ((T, the_single ks) :: card_assigns, max_assigns)
  16.108    | Max x => (card_assigns, (x, the_single ks) :: max_assigns)
  16.109 +
  16.110  fun scope_descriptor_from_block block =
  16.111    fold_rev add_row_to_scope_descriptor block ([], [])
  16.112 +
  16.113  fun scope_descriptor_from_combination (hol_ctxt as {ctxt, ...}) binarize blocks
  16.114                                        columns =
  16.115    let
    17.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Mar 03 22:33:22 2014 +0100
    17.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Mar 03 22:33:22 2014 +0100
    17.3 @@ -7,7 +7,6 @@
    17.4  
    17.5  signature NITPICK_UTIL =
    17.6  sig
    17.7 -  type styp = string * typ
    17.8    datatype polarity = Pos | Neg | Neut
    17.9  
   17.10    exception ARG of string * string
   17.11 @@ -61,7 +60,6 @@
   17.12    val int_T : typ
   17.13    val simple_string_of_typ : typ -> string
   17.14    val num_binder_types : typ -> int
   17.15 -  val is_real_constr : theory -> string * typ -> bool
   17.16    val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ
   17.17    val varify_type : Proof.context -> typ -> typ
   17.18    val instantiate_type : theory -> typ -> typ -> typ -> typ
   17.19 @@ -84,8 +82,6 @@
   17.20  structure Nitpick_Util : NITPICK_UTIL =
   17.21  struct
   17.22  
   17.23 -type styp = string * typ
   17.24 -
   17.25  datatype polarity = Pos | Neg | Neut
   17.26  
   17.27  exception ARG of string * string
   17.28 @@ -154,6 +150,7 @@
   17.29    | replicate_list n xs = xs @ replicate_list (n - 1) xs
   17.30  
   17.31  fun offset_list ns = rev (tl (fold (fn x => fn xs => (x + hd xs) :: xs) ns [0]))
   17.32 +
   17.33  fun index_seq j0 n = if j0 < 0 then j0 downto j0 - n + 1 else j0 upto j0 + n - 1
   17.34  
   17.35  fun filter_indices js xs =
   17.36 @@ -164,6 +161,7 @@
   17.37        | aux _ _ _ = raise ARG ("Nitpick_Util.filter_indices",
   17.38                                 "indices unordered or out of range")
   17.39    in aux 0 js xs end
   17.40 +
   17.41  fun filter_out_indices js xs =
   17.42    let
   17.43      fun aux _ [] xs = xs
   17.44 @@ -212,6 +210,7 @@
   17.45                      (SOME key) of
   17.46      SOME z => SOME z
   17.47    | NONE => ps |> find_first (is_none o fst) |> Option.map snd
   17.48 +
   17.49  fun triple_lookup _ [(NONE, z)] _ = SOME z
   17.50    | triple_lookup eq ps key =
   17.51      case AList.lookup (op =) ps (SOME key) of
   17.52 @@ -242,6 +241,7 @@
   17.53  val string_of_time = ATP_Util.string_of_time
   17.54  
   17.55  val subscript = implode o map (prefix "\<^sub>") o Symbol.explode
   17.56 +
   17.57  fun nat_subscript n =
   17.58    n |> signed_string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
   17.59  
   17.60 @@ -260,16 +260,6 @@
   17.61  
   17.62  val num_binder_types = BNF_Util.num_binder_types
   17.63  
   17.64 -fun is_real_constr thy (s, T) =
   17.65 -  case body_type T of
   17.66 -    Type (s', _) =>
   17.67 -    (case Datatype.get_constrs thy s' of
   17.68 -       SOME constrs =>
   17.69 -       List.exists (fn (cname, cty) =>
   17.70 -         cname = s andalso Sign.typ_instance thy (T, cty)) constrs
   17.71 -     | NONE => false)
   17.72 -  | _  => false
   17.73 -
   17.74  fun typ_of_dtyp _ typ_assoc (Datatype.DtTFree a) =
   17.75      the (AList.lookup (op =) typ_assoc (Datatype.DtTFree a))
   17.76    | typ_of_dtyp descr typ_assoc (Datatype.DtType (s, Us)) =
   17.77 @@ -309,6 +299,7 @@
   17.78  val unyxml = ATP_Util.unyxml
   17.79  
   17.80  val maybe_quote = ATP_Util.maybe_quote
   17.81 +
   17.82  fun pretty_maybe_quote pretty =
   17.83    let val s = Pretty.str_of pretty in
   17.84      if maybe_quote s = s then pretty else Pretty.enum "" "\"" "\"" [pretty]