1.1 --- a/doc-src/Nitpick/nitpick.tex	Thu Mar 11 12:22:11 2010 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Thu Mar 11 15:33:45 2010 +0100
     1.3 @@ -137,8 +137,8 @@
     1.4  suggesting several textual improvements.
     1.5  % and Perry James for reporting a typo.
     1.6  
     1.7 -\section{Overview}
     1.8 -\label{overview}
     1.9 +\section{First Steps}
    1.10 +\label{first-steps}
    1.11  
    1.12  This section introduces Nitpick by presenting small examples. If possible, you
    1.13  should try out the examples on your workstation. Your theory file should start
    1.14 @@ -472,7 +472,7 @@
    1.15  
    1.16  \prew
    1.17  \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
    1.18 -\textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount]
    1.19 +\textbf{nitpick} [\textit{card~nat}~= 50, \textit{check\_potential}] \\[2\smallskipamount]
    1.20  \slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported
    1.21  fragment. Only potential counterexamples may be found. \\[2\smallskipamount]
    1.22  Nitpick found a potential counterexample: \\[2\smallskipamount]
    1.23 @@ -629,7 +629,7 @@
    1.24  unlikely that one could be found for smaller cardinalities.
    1.25  
    1.26  \subsection{Typedefs, Quotient Types, Records, Rationals, and Reals}
    1.27 -\label{typedefs-records-rationals-and-reals}
    1.28 +\label{typedefs-quotient-types-records-rationals-and-reals}
    1.29  
    1.30  Nitpick generally treats types declared using \textbf{typedef} as datatypes
    1.31  whose single constructor is the corresponding \textit{Abs\_\kern.1ex} function.
    1.32 @@ -684,7 +684,26 @@
    1.33  
    1.34  In the counterexample, $\Abs{(0,\, 0)}$ and $\Abs{(1,\, 0)}$ represent the
    1.35  integers $0$ and $1$, respectively. Other representants would have been
    1.36 -possible---e.g., $\Abs{(5,\, 5)}$ and $\Abs{(12,\, 11)}$.
    1.37 +possible---e.g., $\Abs{(5,\, 5)}$ and $\Abs{(12,\, 11)}$. If we are going to
    1.38 +use \textit{my\_int} extensively, it pays off to install a term postprocessor
    1.39 +that converts the pair notation to the standard mathematical notation:
    1.40 +
    1.41 +\prew
    1.42 +$\textbf{ML}~\,\{{*} \\
    1.43 +\!\begin{aligned}[t]
    1.44 +%& ({*}~\,\textit{Proof.context} \rightarrow \textit{string} \rightarrow (\textit{typ} \rightarrow \textit{term~list\/}) \rightarrow \textit{typ} \rightarrow \textit{term} \\[-2pt]
    1.45 +%& \phantom{(*}~\,{\rightarrow}\;\textit{term}~\,{*}) \\[-2pt]
    1.46 +& \textbf{fun}\,~\textit{my\_int\_postproc}~\_~\_~\_~T~(\textit{Const}~\_~\$~(\textit{Const}~\_~\$~\textit{t1}~\$~\textit{t2\/})) = {} \\[-2pt]
    1.47 +& \phantom{fun}\,~\textit{HOLogic.mk\_number}~T~(\textit{snd}~(\textit{HOLogic.dest\_number~t1}) \\[-2pt]
    1.48 +& \phantom{fun\,~\textit{HOLogic.mk\_number}~T~(}{-}~\textit{snd}~(\textit{HOLogic.dest\_number~t2\/})) \\[-2pt]
    1.49 +& \phantom{fun}\!{\mid}\,~\textit{my\_int\_postproc}~\_~\_~\_~\_~t = t \\[-2pt]
    1.50 +{*}\}\end{aligned}$ \\[2\smallskipamount]
    1.51 +$\textbf{setup}~\,\{{*} \\
    1.52 +\!\begin{aligned}[t]
    1.53 +& \textit{Nitpick.register\_term\_postprocessor}~\!\begin{aligned}[t]
    1.54 +  & @\{\textrm{typ}~\textit{my\_int}\}~\textit{my\_int\_postproc}\end{aligned} \\[-2pt]
    1.55 +{*}\}\end{aligned}$
    1.56 +\postw
    1.57  
    1.58  Records are also handled as datatypes with a single constructor:
    1.59  
    1.60 @@ -771,25 +790,25 @@
    1.61  
    1.62  \prew
    1.63  \textbf{lemma} ``$\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
    1.64 -\textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount]
    1.65 +\textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount]
    1.66  \slshape The inductive predicate ``\textit{even}'' was proved well-founded.
    1.67  Nitpick can compute it efficiently. \\[2\smallskipamount]
    1.68  Trying 1 scope: \\
    1.69 -\hbox{}\qquad \textit{card nat}~= 100. \\[2\smallskipamount]
    1.70 -Nitpick found a potential counterexample for \textit{card nat}~= 100: \\[2\smallskipamount]
    1.71 +\hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount]
    1.72 +Nitpick found a potential counterexample for \textit{card nat}~= 50: \\[2\smallskipamount]
    1.73  \hbox{}\qquad Empty assignment \\[2\smallskipamount]
    1.74  Nitpick could not find a better counterexample. \\[2\smallskipamount]
    1.75  Total time: 2274 ms.
    1.76  \postw
    1.77  
    1.78  No genuine counterexample is possible because Nitpick cannot rule out the
    1.79 -existence of a natural number $n \ge 100$ such that both $\textit{even}~n$ and
    1.80 +existence of a natural number $n \ge 50$ such that both $\textit{even}~n$ and
    1.81  $\textit{even}~(\textit{Suc}~n)$ are true. To help Nitpick, we can bound the
    1.82  existential quantifier:
    1.83  
    1.84  \prew
    1.85 -\textbf{lemma} ``$\exists n \mathbin{\le} 99.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
    1.86 -\textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}] \\[2\smallskipamount]
    1.87 +\textbf{lemma} ``$\exists n \mathbin{\le} 49.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
    1.88 +\textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}] \\[2\smallskipamount]
    1.89  \slshape Nitpick found a counterexample: \\[2\smallskipamount]
    1.90  \hbox{}\qquad Empty assignment
    1.91  \postw
    1.92 @@ -1211,26 +1230,26 @@
    1.93  Trying 8 scopes: \\
    1.94  \hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} $'b$~= 1,
    1.95  \textit{card} \textit{nat}~= 1, \textit{card} ``$('a \times {'}b)$
    1.96 -\textit{list}''~= 1, \\
    1.97 -\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 1, and
    1.98 -\textit{card} ``\kern1pt$'b$ \textit{list}''~= 1. \\
    1.99 +\textit{list\/}''~= 1, \\
   1.100 +\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 1, and
   1.101 +\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 1. \\
   1.102  \hbox{}\qquad \textit{card} $'a$~= 2, \textit{card} $'b$~= 2,
   1.103  \textit{card} \textit{nat}~= 2, \textit{card} ``$('a \times {'}b)$
   1.104 -\textit{list}''~= 2, \\
   1.105 -\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 2, and
   1.106 -\textit{card} ``\kern1pt$'b$ \textit{list}''~= 2. \\
   1.107 +\textit{list\/}''~= 2, \\
   1.108 +\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 2, and
   1.109 +\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 2. \\
   1.110  \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
   1.111  \hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} $'b$~= 8,
   1.112  \textit{card} \textit{nat}~= 8, \textit{card} ``$('a \times {'}b)$
   1.113 -\textit{list}''~= 8, \\
   1.114 -\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 8, and
   1.115 -\textit{card} ``\kern1pt$'b$ \textit{list}''~= 8.
   1.116 +\textit{list\/}''~= 8, \\
   1.117 +\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 8, and
   1.118 +\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 8.
   1.119  \\[2\smallskipamount]
   1.120  Nitpick found a counterexample for
   1.121  \textit{card} $'a$~= 5, \textit{card} $'b$~= 5,
   1.122  \textit{card} \textit{nat}~= 5, \textit{card} ``$('a \times {'}b)$
   1.123 -\textit{list}''~= 5, \textit{card} ``\kern1pt$'a$ \textit{list}''~= 5, and
   1.124 -\textit{card} ``\kern1pt$'b$ \textit{list}''~= 5:
   1.125 +\textit{list\/}''~= 5, \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 5, and
   1.126 +\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 5:
   1.127  \\[2\smallskipamount]
   1.128  \hbox{}\qquad Free variables: \nopagebreak \\
   1.129  \hbox{}\qquad\qquad $\textit{xs} = [a_1, a_2]$ \\
   1.130 @@ -1851,7 +1870,7 @@
   1.131  The number of options can be overwhelming at first glance. Do not let that worry
   1.132  you: Nitpick's defaults have been chosen so that it almost always does the right
   1.133  thing, and the most important options have been covered in context in
   1.134 -\S\ref{overview}.
   1.135 +\S\ref{first-steps}.
   1.136  
   1.137  The descriptions below refer to the following syntactic quantities:
   1.138  
   1.139 @@ -2622,7 +2641,7 @@
   1.140  
   1.141  then Nitpick assumes that the definition was made using an inductive package and
   1.142  based on the introduction rules marked with \textit{nitpick\_\allowbreak
   1.143 -ind\_\allowbreak intros} tries to determine whether the definition is
   1.144 +\allowbreak intros} tries to determine whether the definition is
   1.145  well-founded.
   1.146  \end{enum}
   1.147  \end{enum}
   1.148 @@ -2664,7 +2683,8 @@
   1.149  Nitpick provides a rich Standard ML interface used mainly for internal purposes
   1.150  and debugging. Among the most interesting functions exported by Nitpick are
   1.151  those that let you invoke the tool programmatically and those that let you
   1.152 -register and unregister custom coinductive datatypes.
   1.153 +register and unregister custom coinductive datatypes as well as term
   1.154 +postprocessors.
   1.155  
   1.156  \subsection{Invocation of Nitpick}
   1.157  \label{invocation-of-nitpick}
   1.158 @@ -2695,7 +2715,7 @@
   1.159  put into a \textit{params} record. Here is an example:
   1.160  
   1.161  \prew
   1.162 -$\textbf{val}\,~\textit{params} = \textit{Nitpick\_Isar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\
   1.163 +$\textbf{val}\,~\textit{params} = \textit{Nitpick\_Isar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout\/}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\
   1.164  $\textbf{val}\,~(\textit{outcome},\, \textit{state}') = \textit{Nitpick.pick\_nits\_in\_subgoal}~\begin{aligned}[t]
   1.165  & \textit{state}~\textit{params}~\textit{false} \\[-2pt]
   1.166  & \textit{subgoal}\end{aligned}$
   1.167 @@ -2726,7 +2746,7 @@
   1.168  \prew
   1.169  $\textbf{setup}~\,\{{*}\,~\!\begin{aligned}[t]
   1.170  & \textit{Nitpick.register\_codatatype} \\[-2pt]
   1.171 -& \qquad @\{\antiq{typ}~``\kern1pt'a~\textit{llist}\textrm{''}\}~@\{\antiq{const\_name}~ \textit{llist\_case}\} \\[-2pt] %% TYPESETTING
   1.172 +& \qquad @\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}~@\{\antiq{const\_name}~ \textit{llist\_case}\} \\[-2pt] %% TYPESETTING
   1.173  & \qquad (\textit{map}~\textit{dest\_Const}~[@\{\antiq{term}~\textit{LNil}\},\, @\{\antiq{term}~\textit{LCons}\}])\,\ {*}\}\end{aligned}$
   1.174  \postw
   1.175  
   1.176 @@ -2740,7 +2760,7 @@
   1.177  
   1.178  \prew
   1.179  $\textbf{setup}~\,\{{*}\,~\textit{Nitpick.unregister\_codatatype}~@\{\antiq{typ}~``
   1.180 -\kern1pt'a~\textit{list}\textrm{''}\}\ \,{*}\}$
   1.181 +\kern1pt'a~\textit{list\/}\textrm{''}\}\ \,{*}\}$
   1.182  \postw
   1.183  
   1.184  Inductive datatypes can be registered as coinductive datatypes, given
   1.185 @@ -2748,6 +2768,26 @@
   1.186  the use of the inductive constructors---Nitpick will generate an error if they
   1.187  are needed.
   1.188  
   1.189 +\subsection{Registration of Term Postprocessors}
   1.190 +\label{registration-of-term-postprocessors}
   1.191 +
   1.192 +It is possible to change the output of any term that Nitpick considers a
   1.193 +datatype by registering a term postprocessor. The interface for registering and
   1.194 +unregistering postprocessors consists of the following pair of functions defined
   1.195 +in the \textit{Nitpick} structure:
   1.196 +
   1.197 +\prew
   1.198 +$\textbf{type}\,~\textit{term\_postprocessor}\,~{=} {}$ \\
   1.199 +$\hbox{}\quad\textit{Proof.context} \rightarrow \textit{string} \rightarrow (\textit{typ} \rightarrow \textit{term~list\/}) \rightarrow \textit{typ} \rightarrow \textit{term} \rightarrow \textit{term}$ \\
   1.200 +$\textbf{val}\,~\textit{register\_term\_postprocessors} : {}$ \\
   1.201 +$\hbox{}\quad\textit{typ} \rightarrow \textit{term\_postprocessor} \rightarrow \textit{theory} \rightarrow \textit{theory}$ \\
   1.202 +$\textbf{val}\,~\textit{unregister\_term\_postprocessors} :\,
   1.203 +\textit{typ} \rightarrow \textit{theory} \rightarrow \textit{theory}$
   1.204 +\postw
   1.205 +
   1.206 +\S\ref{typedefs-quotient-types-records-rationals-and-reals} and
   1.207 +\texttt{src/HOL/Library/Multiset.thy} illustrate this feature in context.
   1.208 +
   1.209  \section{Known Bugs and Limitations}
   1.210  \label{known-bugs-and-limitations}
   1.211  

     2.1 --- a/src/HOL/Library/Multiset.thy	Thu Mar 11 12:22:11 2010 +0100
     2.2 +++ b/src/HOL/Library/Multiset.thy	Thu Mar 11 15:33:45 2010 +0100
     2.3 @@ -1729,4 +1729,33 @@
     2.4    "M \<subset># N ==> (\<not> P ==> N \<subset># (M::'a::order multiset)) ==> P"
     2.5    by (fact multiset_order.less_asym)
     2.6  
     2.7 +ML {*
     2.8 +(* Proof.context -> string -> (typ -> term list) -> typ -> term -> term *)
     2.9 +fun multiset_postproc _ maybe_name all_values (T as Type (_, [elem_T]))
    2.10 +                      (Const _ $ t') =
    2.11 +    let
    2.12 +      val (maybe_opt, ps) =
    2.13 +        Nitpick_Model.dest_plain_fun t' ||> op ~~
    2.14 +        ||> map (apsnd (snd o HOLogic.dest_number))
    2.15 +      fun elems_for t =
    2.16 +        case AList.lookup (op =) ps t of
    2.17 +          SOME n => replicate n t
    2.18 +        | NONE => [Const (maybe_name, elem_T --> elem_T) $ t]
    2.19 +    in
    2.20 +      case maps elems_for (all_values elem_T) @
    2.21 +           (if maybe_opt then [Const (Nitpick_Model.unrep, elem_T)] else []) of
    2.22 +        [] => Const (@{const_name zero_class.zero}, T)
    2.23 +      | ts => foldl1 (fn (t1, t2) =>
    2.24 +                         Const (@{const_name plus_class.plus}, T --> T --> T)
    2.25 +                         $ t1 $ t2)
    2.26 +                     (map (curry (op $) (Const (@{const_name single},
    2.27 +                                                elem_T --> T))) ts)
    2.28 +    end
    2.29 +  | multiset_postproc _ _ _ _ t = t
    2.30 +*}
    2.31 +
    2.32 +setup {*
    2.33 +Nitpick.register_term_postprocessor @{typ "'a multiset"} multiset_postproc
    2.34 +*}
    2.35 +
    2.36  end
    2.37 \ No newline at end of file

     3.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Mar 11 12:22:11 2010 +0100
     3.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Mar 11 15:33:45 2010 +0100
     3.3 @@ -118,10 +118,11 @@
     3.4  oops
     3.5  
     3.6  ML {*
     3.7 -(* Proof.context -> typ -> term -> term *)
     3.8 -fun my_int_postproc _ T (Const _ $ (Const _ $ t1 $ t2)) =
     3.9 -    HOLogic.mk_number T (snd (HOLogic.dest_number t1) - snd (HOLogic.dest_number t2))
    3.10 -  | my_int_postproc _ _ t = t
    3.11 +(* Proof.context -> string -> (typ -> term list) -> typ -> term -> term *)
    3.12 +fun my_int_postproc _ _ _ T (Const _ $ (Const _ $ t1 $ t2)) =
    3.13 +    HOLogic.mk_number T (snd (HOLogic.dest_number t1)
    3.14 +                         - snd (HOLogic.dest_number t2))
    3.15 +  | my_int_postproc _ _ _ _ t = t
    3.16  *}
    3.17  
    3.18  setup {* Nitpick.register_term_postprocessor @{typ my_int} my_int_postproc *}

     4.1 --- a/src/HOL/Tools/Nitpick/HISTORY	Thu Mar 11 12:22:11 2010 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/HISTORY	Thu Mar 11 15:33:45 2010 +0100
     4.3 @@ -7,6 +7,7 @@
     4.4    * Added support for quotient types
     4.5    * Added support for local definitions (for "function" and "termination"
     4.6      proofs)
     4.7 +  * Added support for term postprocessors
     4.8    * Optimized "Multiset.multiset" and "FinFun.finfun"
     4.9    * Improved efficiency of "destroy_constrs" optimization
    4.10    * Fixed soundness bugs related to "destroy_constrs" optimization and record

     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Mar 11 12:22:11 2010 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Mar 11 15:33:45 2010 +0100
     5.3 @@ -16,15 +16,20 @@
     5.4      show_skolems: bool,
     5.5      show_datatypes: bool,
     5.6      show_consts: bool}
     5.7 -  type term_postprocessor = Proof.context -> typ -> term -> term
     5.8 +  type term_postprocessor =
     5.9 +    Proof.context -> string -> (typ -> term list) -> typ -> term -> term
    5.10  
    5.11    structure NameTable : TABLE
    5.12  
    5.13 +  val irrelevant : string
    5.14 +  val unknown : string
    5.15 +  val unrep : string
    5.16    val register_term_postprocessor :
    5.17      typ -> term_postprocessor -> theory -> theory
    5.18    val unregister_term_postprocessor : typ -> theory -> theory
    5.19    val tuple_list_for_name :
    5.20      nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list
    5.21 +  val dest_plain_fun : term -> bool * (term list * term list)
    5.22    val reconstruct_hol_model :
    5.23      params -> scope -> (term option * int list) list -> styp list -> nut list
    5.24      -> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
    5.25 @@ -51,7 +56,8 @@
    5.26    show_datatypes: bool,
    5.27    show_consts: bool}
    5.28  
    5.29 -type term_postprocessor = Proof.context -> typ -> term -> term
    5.30 +type term_postprocessor =
    5.31 +  Proof.context -> string -> (typ -> term list) -> typ -> term -> term
    5.32  
    5.33  structure Data = Theory_Data(
    5.34    type T = (typ * term_postprocessor) list
    5.35 @@ -59,6 +65,7 @@
    5.36    val extend = I
    5.37    fun merge (ps1, ps2) = AList.merge (op =) (K true) (ps1, ps2))
    5.38  
    5.39 +val irrelevant = "_"
    5.40  val unknown = "?"
    5.41  val unrep = "\<dots>"
    5.42  val maybe_mixfix = "_\<^sup>?"
    5.43 @@ -182,9 +189,9 @@
    5.44      (* typ -> typ -> (term * term) list -> term *)
    5.45      fun aux T1 T2 [] =
    5.46          Const (if maybe_opt then opt_flag else non_opt_flag, T1 --> T2)
    5.47 -      | aux T1 T2 ((t1, t2) :: ps) =
    5.48 +      | aux T1 T2 ((t1, t2) :: tps) =
    5.49          Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
    5.50 -        $ aux T1 T2 ps $ t1 $ t2
    5.51 +        $ aux T1 T2 tps $ t1 $ t2
    5.52    in aux T1 T2 o rev end
    5.53  (* term -> bool *)
    5.54  fun is_plain_fun (Const (s, _)) = (s = opt_flag orelse s = non_opt_flag)
    5.55 @@ -195,9 +202,12 @@
    5.56  val dest_plain_fun =
    5.57    let
    5.58      (* term -> bool * (term list * term list) *)
    5.59 -    fun aux (Const (s, _)) = (s <> non_opt_flag, ([], []))
    5.60 +    fun aux (Abs (_, _, Const (s, _))) = (s <> irrelevant, ([], []))
    5.61 +      | aux (Const (s, _)) = (s <> non_opt_flag, ([], []))
    5.62        | aux (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
    5.63 -        let val (s, (ts1, ts2)) = aux t0 in (s, (t1 :: ts1, t2 :: ts2)) end
    5.64 +        let val (maybe_opt, (ts1, ts2)) = aux t0 in
    5.65 +          (maybe_opt, (t1 :: ts1, t2 :: ts2))
    5.66 +        end
    5.67        | aux t = raise TERM ("Nitpick_Model.dest_plain_fun", [t])
    5.68    in apsnd (pairself rev) o aux end
    5.69  
    5.70 @@ -227,22 +237,22 @@
    5.71        (* typ -> typ -> typ -> typ -> term -> term *)
    5.72        fun do_curry T1 T1a T1b T2 t =
    5.73          let
    5.74 -          val (maybe_opt, ps) = dest_plain_fun t
    5.75 -          val ps =
    5.76 -            ps |>> map (break_in_two T1 T1a T1b)
    5.77 -               |> uncurry (map2 (fn (t1a, t1b) => fn t2 => (t1a, (t1b, t2))))
    5.78 -               |> AList.coalesce (op =)
    5.79 -               |> map (apsnd (make_plain_fun maybe_opt T1b T2))
    5.80 -        in make_plain_fun maybe_opt T1a (T1b --> T2) ps end
    5.81 +          val (maybe_opt, tsp) = dest_plain_fun t
    5.82 +          val tps =
    5.83 +            tsp |>> map (break_in_two T1 T1a T1b)
    5.84 +                |> uncurry (map2 (fn (t1a, t1b) => fn t2 => (t1a, (t1b, t2))))
    5.85 +                |> AList.coalesce (op =)
    5.86 +                |> map (apsnd (make_plain_fun maybe_opt T1b T2))
    5.87 +        in make_plain_fun maybe_opt T1a (T1b --> T2) tps end
    5.88        (* typ -> typ -> term -> term *)
    5.89        and do_uncurry T1 T2 t =
    5.90          let
    5.91            val (maybe_opt, tsp) = dest_plain_fun t
    5.92 -          val ps =
    5.93 +          val tps =
    5.94              tsp |> op ~~
    5.95                  |> maps (fn (t1, t2) =>
    5.96                              multi_pair_up T1 t1 (snd (dest_plain_fun t2)))
    5.97 -        in make_plain_fun maybe_opt T1 T2 ps end
    5.98 +        in make_plain_fun maybe_opt T1 T2 tps end
    5.99        (* typ -> typ -> typ -> typ -> term -> term *)
   5.100        and do_arrow T1' T2' _ _ (Const (s, _)) = Const (s, T1' --> T2')
   5.101          | do_arrow T1' T2' T1 T2
   5.102 @@ -291,22 +301,37 @@
   5.103  (* theory -> typ * typ -> bool *)
   5.104  fun varified_type_match thy (candid_T, pat_T) =
   5.105    strict_type_match thy (candid_T, Logic.varifyT pat_T)
   5.106 -(* Proof.context -> typ -> term -> term *)
   5.107 -fun postprocess_term ctxt T =
   5.108 -  let val thy = ProofContext.theory_of ctxt in
   5.109 -    if null (Data.get thy) then
   5.110 -      I
   5.111 -    else
   5.112 -      (T |> AList.lookup (varified_type_match thy) (Data.get thy)
   5.113 -         |> the_default (K (K I))) ctxt T
   5.114 -  end
   5.115  
   5.116 +(* atom_pool -> (string * string) * (string * string) -> scope -> nut list
   5.117 +   -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ
   5.118 +   -> term list *)
   5.119 +fun all_values_of_type pool wacky_names (scope as {card_assigns, ...} : scope)
   5.120 +                       sel_names rel_table bounds card T =
   5.121 +  let
   5.122 +    val card = if card = 0 then card_of_type card_assigns T else card
   5.123 +    (* nat -> term *)
   5.124 +    fun nth_value_of_type n =
   5.125 +      let
   5.126 +        (* bool -> term *)
   5.127 +        fun term unfold =
   5.128 +          reconstruct_term unfold pool wacky_names scope sel_names rel_table
   5.129 +                           bounds T T (Atom (card, 0)) [[n]]
   5.130 +      in
   5.131 +        case term false of
   5.132 +          t as Const (s, _) =>
   5.133 +          if String.isPrefix cyclic_const_prefix s then
   5.134 +            HOLogic.mk_eq (t, term true)
   5.135 +          else
   5.136 +            t
   5.137 +        | t => t
   5.138 +      end
   5.139 +  in index_seq 0 card |> map nth_value_of_type |> sort nice_term_ord end
   5.140  (* bool -> atom_pool -> (string * string) * (string * string) -> scope
   5.141     -> nut list -> nut list -> nut list -> nut NameTable.table
   5.142     -> KK.raw_bound list -> typ -> typ -> rep -> int list list -> term *)
   5.143 -fun reconstruct_term unfold pool ((maybe_name, abs_name), _)
   5.144 -        ({hol_ctxt as {ctxt, thy, stds, ...}, binarize, card_assigns, bits,
   5.145 -          datatypes, ofs, ...} : scope) sel_names rel_table bounds =
   5.146 +and reconstruct_term unfold pool (wacky_names as ((maybe_name, abs_name), _))
   5.147 +        (scope as {hol_ctxt as {ctxt, thy, stds, ...}, binarize, card_assigns,
   5.148 +                   bits, datatypes, ofs, ...}) sel_names rel_table bounds =
   5.149    let
   5.150      val for_auto = (maybe_name = "")
   5.151      (* int list list -> int *)
   5.152 @@ -318,6 +343,25 @@
   5.153          fold (fn j => Integer.add (reasonable_power 2 j |> j = bits ? op ~))
   5.154               js 0
   5.155        end
   5.156 +    (* typ -> term list *)
   5.157 +    val all_values =
   5.158 +      all_values_of_type pool wacky_names scope sel_names rel_table bounds 0
   5.159 +    (* typ -> term -> term *)
   5.160 +    fun postprocess_term (Type (@{type_name fun}, _)) = I
   5.161 +      | postprocess_term T =
   5.162 +        if null (Data.get thy) then
   5.163 +          I
   5.164 +        else case AList.lookup (varified_type_match thy) (Data.get thy) T of
   5.165 +          SOME postproc => postproc ctxt maybe_name all_values T
   5.166 +        | NONE => I
   5.167 +    (* typ list -> term -> term *)
   5.168 +    fun postprocess_subterms Ts (t1 $ t2) =
   5.169 +        let val t = postprocess_subterms Ts t1 $ postprocess_subterms Ts t2 in
   5.170 +          postprocess_term (fastype_of1 (Ts, t)) t
   5.171 +        end
   5.172 +      | postprocess_subterms Ts (Abs (s, T, t')) =
   5.173 +        Abs (s, T, postprocess_subterms (T :: Ts) t')
   5.174 +      | postprocess_subterms Ts t = postprocess_term (fastype_of1 (Ts, t)) t
   5.175      (* bool -> typ -> typ -> (term * term) list -> term *)
   5.176      fun make_set maybe_opt T1 T2 tps =
   5.177        let
   5.178 @@ -352,16 +396,16 @@
   5.179                                    (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
   5.180          (* (term * term) list -> term *)
   5.181          fun aux' [] = Const (@{const_abbrev Map.empty}, T1 --> T2)
   5.182 -          | aux' ((t1, t2) :: ps) =
   5.183 +          | aux' ((t1, t2) :: tps) =
   5.184              (case t2 of
   5.185 -               Const (@{const_name None}, _) => aux' ps
   5.186 -             | _ => update_const $ aux' ps $ t1 $ t2)
   5.187 -        fun aux ps =
   5.188 +               Const (@{const_name None}, _) => aux' tps
   5.189 +             | _ => update_const $ aux' tps $ t1 $ t2)
   5.190 +        fun aux tps =
   5.191            if maybe_opt andalso not (is_complete_type datatypes false T1) then
   5.192 -            update_const $ aux' ps $ Const (unrep, T1)
   5.193 +            update_const $ aux' tps $ Const (unrep, T1)
   5.194              $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
   5.195            else
   5.196 -            aux' ps
   5.197 +            aux' tps
   5.198        in aux end
   5.199      (* typ list -> term -> term *)
   5.200      fun polish_funs Ts t =
   5.201 @@ -396,7 +440,11 @@
   5.202               | Abs (s, T, t') => Abs (s, T, polish_funs (T :: Ts) t')
   5.203               | Const (s, Type (@{type_name fun}, [T1, T2])) =>
   5.204                 if s = opt_flag orelse s = non_opt_flag then
   5.205 -                 Abs ("x", T1, Const (unknown, T2))
   5.206 +                 Abs ("x", T1,
   5.207 +                      Const (if is_complete_type datatypes false T1 then
   5.208 +                               irrelevant
   5.209 +                             else
   5.210 +                               unknown, T2))
   5.211                 else
   5.212                   t
   5.213               | t => t
   5.214 @@ -541,7 +589,6 @@
   5.215                    t
   5.216                end
   5.217            end
   5.218 -          |> postprocess_term ctxt T
   5.219      (* (typ * int) list -> int -> rep -> typ -> typ -> typ -> int list
   5.220         -> term *)
   5.221      and term_for_vect seen k R T1 T2 T' js =
   5.222 @@ -594,7 +641,10 @@
   5.223          raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
   5.224                     Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
   5.225                     string_of_int (length jss))
   5.226 -  in polish_funs [] o unarize_unbox_etc_term oooo term_for_rep true [] end
   5.227 +  in
   5.228 +    postprocess_subterms [] o polish_funs [] o unarize_unbox_etc_term
   5.229 +    oooo term_for_rep true []
   5.230 +  end
   5.231  
   5.232  (* atom_pool -> scope -> nut list -> nut NameTable.table -> KK.raw_bound list
   5.233     -> nut -> term *)
   5.234 @@ -702,14 +752,14 @@
   5.235              t
   5.236          | t => t
   5.237        end
   5.238 -    (* nat -> typ -> typ list *)
   5.239 -    fun all_values_of_type card T =
   5.240 -      index_seq 0 card |> map (nth_value_of_type card T) |> sort nice_term_ord
   5.241 +    (* nat -> typ -> term list *)
   5.242 +    val all_values =
   5.243 +      all_values_of_type pool wacky_names scope sel_names rel_table bounds
   5.244      (* dtype_spec list -> dtype_spec -> bool *)
   5.245      fun is_codatatype_wellformed (cos : dtype_spec list)
   5.246                                   ({typ, card, ...} : dtype_spec) =
   5.247        let
   5.248 -        val ts = all_values_of_type card typ
   5.249 +        val ts = all_values card typ
   5.250          val max_depth = Integer.sum (map #card cos)
   5.251        in
   5.252          forall (not o bisimilar_values (map #typ cos) max_depth)
   5.253 @@ -750,7 +800,7 @@
   5.254              | _ => []) @
   5.255             [Pretty.str "=",
   5.256              Pretty.enum "," "{" "}"
   5.257 -                (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
   5.258 +                (map (Syntax.pretty_term ctxt) (all_values card typ) @
   5.259                   (if fun_from_pair complete false then []
   5.260                    else [Pretty.str unrep]))]))
   5.261      (* typ -> dtype_spec list *)