added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
authorblanchet
Tue Mar 09 09:25:23 2010 +0100 (2010-03-09)
changeset 35665ff2bf50505ab
parent 35664 fee01e85605f
child 35666 6fd0ca1a3966
child 35671 ed2c3830d881
child 35751 f7f8d59b60b9
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
doc-src/Nitpick/nitpick.tex
doc-src/manual.bib
src/HOL/Nitpick.thy
src/HOL/Nitpick_Examples/Manual_Nits.thy
src/HOL/Tools/Nitpick/minipick.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_isar.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_preproc.ML
src/HOL/Tools/Nitpick/nitpick_rep.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Mon Mar 08 15:20:40 2010 -0800
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Tue Mar 09 09:25:23 2010 +0100
     1.3 @@ -136,8 +136,8 @@
     1.4  suggesting several textual improvements.
     1.5  % and Perry James for reporting a typo.
     1.6  
     1.7 -\section{First Steps}
     1.8 -\label{first-steps}
     1.9 +\section{Overview}
    1.10 +\label{overview}
    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 @@ -145,7 +145,7 @@
    1.15  
    1.16  \prew
    1.17  \textbf{theory}~\textit{Scratch} \\
    1.18 -\textbf{imports}~\textit{Main~Coinductive\_List~Quotient\_Product~RealDef} \\
    1.19 +\textbf{imports}~\textit{Main~Quotient\_Product~RealDef} \\
    1.20  \textbf{begin}
    1.21  \postw
    1.22  
    1.23 @@ -677,7 +677,7 @@
    1.24  \hbox{}\qquad\qquad $y = \Abs{(1,\, 0)}$ \\
    1.25  \hbox{}\qquad Datatypes: \\
    1.26  \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, \unr\}$ \\
    1.27 -\hbox{}\qquad\qquad $\textit{nat} \times \textit{nat} = \{(0,\, 0),\> (1,\, 0),\> \unr\}$ \\
    1.28 +\hbox{}\qquad\qquad $\textit{nat} \times \textit{nat}~[\textsl{boxed\/}] = \{(0,\, 0),\> (1,\, 0),\> \unr\}$ \\
    1.29  \hbox{}\qquad\qquad $\textit{my\_int} = \{\Abs{(0,\, 0)},\> \Abs{(1,\, 0)},\> \unr\}$
    1.30  \postw
    1.31  
    1.32 @@ -704,8 +704,6 @@
    1.33  & \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr,\, \unr\}\end{aligned}$
    1.34  \postw
    1.35  
    1.36 -
    1.37 -
    1.38  Finally, Nitpick provides rudimentary support for rationals and reals using a
    1.39  similar approach:
    1.40  
    1.41 @@ -940,9 +938,10 @@
    1.42  \label{coinductive-datatypes}
    1.43  
    1.44  While Isabelle regrettably lacks a high-level mechanism for defining coinductive
    1.45 -datatypes, the \textit{Coinductive\_List} theory provides a coinductive ``lazy
    1.46 -list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick supports
    1.47 -these lazy lists seamlessly and provides a hook, described in
    1.48 +datatypes, the \textit{Coinductive\_List} theory from Andreas Lochbihler's
    1.49 +\textit{Coinductive} AFP entry \cite{lochbihler-2010} provides a coinductive
    1.50 +``lazy list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick
    1.51 +supports these lazy lists seamlessly and provides a hook, described in
    1.52  \S\ref{registration-of-coinductive-datatypes}, to register custom coinductive
    1.53  datatypes.
    1.54  
    1.55 @@ -1165,10 +1164,11 @@
    1.56  
    1.57  {\looseness=-1
    1.58  Boxing can be enabled or disabled globally or on a per-type basis using the
    1.59 -\textit{box} option. Moreover, setting the cardinality of a function or
    1.60 -product type implicitly enables boxing for that type. Nitpick usually performs
    1.61 -reasonable choices about which types should be boxed, but option tweaking
    1.62 -sometimes helps.
    1.63 +\textit{box} option. Nitpick usually performs reasonable choices about which
    1.64 +types should be boxed, but option tweaking sometimes helps. A related optimization,
    1.65 +``finalization,'' attempts to wrap functions that constant at all but finitely
    1.66 +many points (e.g., finite sets); see the documentation for the \textit{finalize}
    1.67 +option in \S\ref{scope-of-search} for details.
    1.68  
    1.69  }
    1.70  
    1.71 @@ -1850,7 +1850,7 @@
    1.72  The number of options can be overwhelming at first glance. Do not let that worry
    1.73  you: Nitpick's defaults have been chosen so that it almost always does the right
    1.74  thing, and the most important options have been covered in context in
    1.75 -\S\ref{first-steps}.
    1.76 +\S\ref{overview}.
    1.77  
    1.78  The descriptions below refer to the following syntactic quantities:
    1.79  
    1.80 @@ -1936,14 +1936,10 @@
    1.81  Specifies the sequence of cardinalities to use for a given type.
    1.82  For free types, and often also for \textbf{typedecl}'d types, it usually makes
    1.83  sense to specify cardinalities as a range of the form \textit{$1$--$n$}.
    1.84 -Although function and product types are normally mapped directly to the
    1.85 -corresponding Kodkod concepts, setting
    1.86 -the cardinality of such types is also allowed and implicitly enables ``boxing''
    1.87 -for them, as explained in the description of the \textit{box}~\qty{type}
    1.88 -and \textit{box} (\S\ref{scope-of-search}) options.
    1.89  
    1.90  \nopagebreak
    1.91 -{\small See also \textit{mono} (\S\ref{scope-of-search}).}
    1.92 +{\small See also \textit{box} (\S\ref{scope-of-search}) and \textit{mono}
    1.93 +(\S\ref{scope-of-search}).}
    1.94  
    1.95  \opdefault{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$}
    1.96  Specifies the default sequence of cardinalities to use. This can be overridden
    1.97 @@ -2062,8 +2058,8 @@
    1.98  Specifies whether Nitpick should attempt to wrap (``box'') a given function or
    1.99  product type in an isomorphic datatype internally. Boxing is an effective mean
   1.100  to reduce the search space and speed up Nitpick, because the isomorphic datatype
   1.101 -is approximated by a subset of the possible function or pair values;
   1.102 -like other drastic optimizations, it can also prevent the discovery of
   1.103 +is approximated by a subset of the possible function or pair values.
   1.104 +Like other drastic optimizations, it can also prevent the discovery of
   1.105  counterexamples. The option can take the following values:
   1.106  
   1.107  \begin{enum}
   1.108 @@ -2075,30 +2071,68 @@
   1.109  higher-order functions are good candidates for boxing.
   1.110  \end{enum}
   1.111  
   1.112 -Setting the \textit{card}~\qty{type} option for a function or product type
   1.113 -implicitly enables boxing for that type.
   1.114 -
   1.115  \nopagebreak
   1.116 -{\small See also \textit{verbose} (\S\ref{output-format})
   1.117 -and \textit{debug} (\S\ref{output-format}).}
   1.118 +{\small See also \textit{finitize} (\S\ref{scope-of-search}), \textit{verbose}
   1.119 +(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}).}
   1.120  
   1.121  \opsmart{box}{dont\_box}
   1.122  Specifies the default boxing setting to use. This can be overridden on a
   1.123  per-type basis using the \textit{box}~\qty{type} option described above.
   1.124  
   1.125 +\opargboolorsmart{finitize}{type}{dont\_finitize}
   1.126 +Specifies whether Nitpick should attempt to finitize a given type, which can be
   1.127 +a function type or an infinite ``shallow datatype'' (an infinite datatype whose
   1.128 +constructors don't appear in the problem).
   1.129 +
   1.130 +For function types, Nitpick performs a monotonicity analysis to detect functions
   1.131 +that are constant at all but finitely many points (e.g., finite sets) and treats
   1.132 +such occurrences specially, thereby increasing the precision. The option can
   1.133 +then take the following values:
   1.134 +
   1.135 +\begin{enum}
   1.136 +\item[$\bullet$] \textbf{\textit{false}}: Don't attempt to finitize the type.
   1.137 +\item[$\bullet$] \textbf{\textit{true}} or \textbf{\textit{smart}}: Finitize the
   1.138 +type wherever possible.
   1.139 +\end{enum}
   1.140 +
   1.141 +The semantics of the option is somewhat different for infinite shallow
   1.142 +datatypes:
   1.143 +
   1.144 +\begin{enum}
   1.145 +\item[$\bullet$] \textbf{\textit{true}}: Finitize the datatype. Since this is
   1.146 +unsound, counterexamples generated under these conditions are tagged as ``likely
   1.147 +genuine.''
   1.148 +\item[$\bullet$] \textbf{\textit{false}}: Don't attempt to finitize the datatype.
   1.149 +\item[$\bullet$] \textbf{\textit{smart}}: Perform a monotonicity analysis to
   1.150 +detect whether the datatype can be safely finitized before finitizing it.
   1.151 +\end{enum}
   1.152 +
   1.153 +Like other drastic optimizations, finitization can sometimes prevent the
   1.154 +discovery of counterexamples.
   1.155 +
   1.156 +\nopagebreak
   1.157 +{\small See also \textit{box} (\S\ref{scope-of-search}), \textit{mono}
   1.158 +(\S\ref{scope-of-search}), \textit{verbose} (\S\ref{output-format}), and
   1.159 +\textit{debug} (\S\ref{output-format}).}
   1.160 +
   1.161 +\opsmart{finitize}{dont\_finitize}
   1.162 +Specifies the default finitization setting to use. This can be overridden on a
   1.163 +per-type basis using the \textit{finitize}~\qty{type} option described above.
   1.164 +
   1.165  \opargboolorsmart{mono}{type}{non\_mono}
   1.166 -Specifies whether the given type should be considered monotonic when
   1.167 -enumerating scopes. If the option is set to \textit{smart}, Nitpick performs a
   1.168 -monotonicity check on the type. Setting this option to \textit{true} can reduce
   1.169 -the number of scopes tried, but it also diminishes the theoretical chance of
   1.170 +Specifies whether the given type should be considered monotonic when enumerating
   1.171 +scopes and finitizing types. If the option is set to \textit{smart}, Nitpick
   1.172 +performs a monotonicity check on the type. Setting this option to \textit{true}
   1.173 +can reduce the number of scopes tried, but it can also diminish the chance of
   1.174  finding a counterexample, as demonstrated in \S\ref{scope-monotonicity}.
   1.175  
   1.176  \nopagebreak
   1.177  {\small See also \textit{card} (\S\ref{scope-of-search}),
   1.178 +\textit{finitize} (\S\ref{scope-of-search}),
   1.179  \textit{merge\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose}
   1.180  (\S\ref{output-format}).}
   1.181  
   1.182 -\opsmart{mono}{non\_box}
   1.183 +\opsmart{mono}{non\_mono}
   1.184  Specifies the default monotonicity setting to use. This can be overridden on a
   1.185  per-type basis using the \textit{mono}~\qty{type} option described above.
   1.186  
     2.1 --- a/doc-src/manual.bib	Mon Mar 08 15:20:40 2010 -0800
     2.2 +++ b/doc-src/manual.bib	Tue Mar 09 09:25:23 2010 +0100
     2.3 @@ -1759,3 +1759,12 @@
     2.4    key = "Wikipedia",
     2.5    title = "Wikipedia: {AA} Tree",
     2.6    note = "\url{http://en.wikipedia.org/wiki/AA_tree}"}
     2.7 +
     2.8 +@incollection{lochbihler-2010,
     2.9 +  title = "Coinduction",
    2.10 +  author = "Andreas Lochbihler",
    2.11 +  booktitle = "The Archive of Formal Proofs",
    2.12 +  editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson",
    2.13 +  publisher = "\url{http://afp.sourceforge.net/entries/Coinductive.shtml}",
    2.14 +  month = "Feb.",
    2.15 +  year = 2010}
     3.1 --- a/src/HOL/Nitpick.thy	Mon Mar 08 15:20:40 2010 -0800
     3.2 +++ b/src/HOL/Nitpick.thy	Tue Mar 09 09:25:23 2010 +0100
     3.3 @@ -38,8 +38,9 @@
     3.4             and Quot :: "'a \<Rightarrow> 'b"
     3.5             and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
     3.6  
     3.7 +datatype ('a, 'b) fin_fun = FinFun "('a \<Rightarrow> 'b)"
     3.8 +datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)"
     3.9  datatype ('a, 'b) pair_box = PairBox 'a 'b
    3.10 -datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)"
    3.11  
    3.12  typedecl unsigned_bit
    3.13  typedecl signed_bit
    3.14 @@ -220,8 +221,8 @@
    3.15  use "Tools/Nitpick/kodkod_sat.ML"
    3.16  use "Tools/Nitpick/nitpick_util.ML"
    3.17  use "Tools/Nitpick/nitpick_hol.ML"
    3.18 +use "Tools/Nitpick/nitpick_mono.ML"
    3.19  use "Tools/Nitpick/nitpick_preproc.ML"
    3.20 -use "Tools/Nitpick/nitpick_mono.ML"
    3.21  use "Tools/Nitpick/nitpick_scope.ML"
    3.22  use "Tools/Nitpick/nitpick_peephole.ML"
    3.23  use "Tools/Nitpick/nitpick_rep.ML"
    3.24 @@ -236,11 +237,12 @@
    3.25  setup {* Nitpick_Isar.setup *}
    3.26  
    3.27  hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim 
    3.28 -    bisim_iterator_max Quot Tha PairBox FunBox Word refl' wf' wf_wfrec wf_wfrec'
    3.29 -    wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac
    3.30 -    Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac
    3.31 +    bisim_iterator_max Quot Tha FinFun FunBox PairBox Word refl' wf' wf_wfrec
    3.32 +    wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm
    3.33 +    Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac
    3.34      times_frac uminus_frac number_of_frac inverse_frac less_eq_frac of_frac
    3.35 -hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word
    3.36 +hide (open) type bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
    3.37 +    word
    3.38  hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
    3.39      wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
    3.40      The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
     4.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Mar 08 15:20:40 2010 -0800
     4.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Mar 09 09:25:23 2010 +0100
     4.3 @@ -8,7 +8,7 @@
     4.4  header {* Examples from the Nitpick Manual *}
     4.5  
     4.6  theory Manual_Nits
     4.7 -imports Main Coinductive_List Quotient_Product RealDef
     4.8 +imports Main Quotient_Product RealDef
     4.9  begin
    4.10  
    4.11  chapter {* 3. First Steps *}
    4.12 @@ -173,13 +173,35 @@
    4.13  
    4.14  subsection {* 3.9. Coinductive Datatypes *}
    4.15  
    4.16 +(* Lazy lists are defined in Andreas Lochbihler's "Coinductive" AFP entry. Since
    4.17 +we cannot rely on its presence, we expediently provide our own axiomatization.
    4.18 +The examples also work unchanged with Lochbihler's "Coinductive_List" theory. *)
    4.19 +
    4.20 +typedef 'a llist = "UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set" by auto
    4.21 +
    4.22 +definition LNil where "LNil = Abs_llist (Inl [])"
    4.23 +definition LCons where
    4.24 +"LCons y ys = Abs_llist (case Rep_llist ys of
    4.25 +                           Inl ys' \<Rightarrow> Inl (y # ys')
    4.26 +                         | Inr f \<Rightarrow> Inr (\<lambda>n. case n of 0 \<Rightarrow> y | Suc m \<Rightarrow> f m))"
    4.27 +
    4.28 +axiomatization iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist"
    4.29 +
    4.30 +lemma iterates_def [nitpick_simp]:
    4.31 +"iterates f a = LCons a (iterates f (f a))"
    4.32 +sorry
    4.33 +
    4.34 +setup {*
    4.35 +Nitpick.register_codatatype @{typ "'a llist"} ""
    4.36 +    (map dest_Const [@{term LNil}, @{term LCons}])
    4.37 +*}
    4.38 +
    4.39  lemma "xs \<noteq> LCons a xs"
    4.40  nitpick
    4.41  oops
    4.42  
    4.43  lemma "\<lbrakk>xs = LCons a xs; ys = iterates (\<lambda>b. a) b\<rbrakk> \<Longrightarrow> xs = ys"
    4.44  nitpick [verbose]
    4.45 -nitpick [bisim_depth = -1, verbose]
    4.46  oops
    4.47  
    4.48  lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
     5.1 --- a/src/HOL/Tools/Nitpick/minipick.ML	Mon Mar 08 15:20:40 2010 -0800
     5.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML	Tue Mar 09 09:25:23 2010 +0100
     5.3 @@ -36,8 +36,10 @@
     5.4  datatype rep = SRep | RRep
     5.5  
     5.6  (* Proof.context -> typ -> unit *)
     5.7 -fun check_type ctxt (Type ("fun", Ts)) = List.app (check_type ctxt) Ts
     5.8 -  | check_type ctxt (Type ("*", Ts)) = List.app (check_type ctxt) Ts
     5.9 +fun check_type ctxt (Type (@{type_name fun}, Ts)) =
    5.10 +    List.app (check_type ctxt) Ts
    5.11 +  | check_type ctxt (Type (@{type_name "*"}, Ts)) =
    5.12 +    List.app (check_type ctxt) Ts
    5.13    | check_type _ @{typ bool} = ()
    5.14    | check_type _ (TFree (_, @{sort "{}"})) = ()
    5.15    | check_type _ (TFree (_, @{sort HOL.type})) = ()
    5.16 @@ -45,13 +47,14 @@
    5.17      raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))
    5.18  
    5.19  (* rep -> (typ -> int) -> typ -> int list *)
    5.20 -fun atom_schema_of SRep card (Type ("fun", [T1, T2])) =
    5.21 +fun atom_schema_of SRep card (Type (@{type_name fun}, [T1, T2])) =
    5.22      replicate_list (card T1) (atom_schema_of SRep card T2)
    5.23 -  | atom_schema_of RRep card (Type ("fun", [T1, @{typ bool}])) =
    5.24 +  | atom_schema_of RRep card (Type (@{type_name fun}, [T1, @{typ bool}])) =
    5.25      atom_schema_of SRep card T1
    5.26 -  | atom_schema_of RRep card (Type ("fun", [T1, T2])) =
    5.27 +  | atom_schema_of RRep card (Type (@{type_name fun}, [T1, T2])) =
    5.28      atom_schema_of SRep card T1 @ atom_schema_of RRep card T2
    5.29 -  | atom_schema_of _ card (Type ("*", Ts)) = maps (atom_schema_of SRep card) Ts
    5.30 +  | atom_schema_of _ card (Type (@{type_name "*"}, Ts)) =
    5.31 +    maps (atom_schema_of SRep card) Ts
    5.32    | atom_schema_of _ card T = [card T]
    5.33  (* rep -> (typ -> int) -> typ -> int *)
    5.34  val arity_of = length ooo atom_schema_of
    5.35 @@ -89,7 +92,7 @@
    5.36  fun kodkod_formula_from_term ctxt card frees =
    5.37    let
    5.38      (* typ -> rel_expr -> rel_expr *)
    5.39 -    fun R_rep_from_S_rep (T as Type ("fun", [T1, @{typ bool}])) r =
    5.40 +    fun R_rep_from_S_rep (T as Type (@{type_name fun}, [T1, @{typ bool}])) r =
    5.41          let
    5.42            val jss = atom_schema_of SRep card T1 |> map (rpair 0)
    5.43                      |> all_combinations
    5.44 @@ -100,7 +103,7 @@
    5.45                 (index_seq 0 (length jss)) jss
    5.46            |> foldl1 Union
    5.47          end
    5.48 -      | R_rep_from_S_rep (Type ("fun", [T1, T2])) r =
    5.49 +      | R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =
    5.50          let
    5.51            val jss = atom_schema_of SRep card T1 |> map (rpair 0)
    5.52                      |> all_combinations
    5.53 @@ -115,7 +118,7 @@
    5.54          end
    5.55        | R_rep_from_S_rep _ r = r
    5.56      (* typ list -> typ -> rel_expr -> rel_expr *)
    5.57 -    fun S_rep_from_R_rep Ts (T as Type ("fun", _)) r =
    5.58 +    fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r =
    5.59          Comprehension (decls_for SRep card Ts T,
    5.60              RelEq (R_rep_from_S_rep T
    5.61                         (rel_expr_for_bound_var card SRep (T :: Ts) 0), r))
    5.62 @@ -137,7 +140,9 @@
    5.63         | Const (@{const_name "op ="}, _) $ t1 $ t2 =>
    5.64           RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
    5.65         | Const (@{const_name ord_class.less_eq},
    5.66 -                Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>
    5.67 +                Type (@{type_name fun},
    5.68 +                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
    5.69 +         $ t1 $ t2 =>
    5.70           Subset (to_R_rep Ts t1, to_R_rep Ts t2)
    5.71         | @{const "op &"} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
    5.72         | @{const "op |"} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
    5.73 @@ -179,7 +184,8 @@
    5.74         | Const (@{const_name "op ="}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
    5.75         | Const (@{const_name "op ="}, _) => to_R_rep Ts (eta_expand Ts t 2)
    5.76         | Const (@{const_name ord_class.less_eq},
    5.77 -                Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ _ =>
    5.78 +                Type (@{type_name fun},
    5.79 +                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
    5.80           to_R_rep Ts (eta_expand Ts t 1)
    5.81         | Const (@{const_name ord_class.less_eq}, _) =>
    5.82           to_R_rep Ts (eta_expand Ts t 2)
    5.83 @@ -190,7 +196,7 @@
    5.84         | @{const "op -->"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
    5.85         | @{const "op -->"} => to_R_rep Ts (eta_expand Ts t 2)
    5.86         | Const (@{const_name bot_class.bot},
    5.87 -                T as Type ("fun", [_, @{typ bool}])) =>
    5.88 +                T as Type (@{type_name fun}, [_, @{typ bool}])) =>
    5.89           empty_n_ary_rel (arity_of RRep card T)
    5.90         | Const (@{const_name insert}, _) $ t1 $ t2 =>
    5.91           Union (to_S_rep Ts t1, to_R_rep Ts t2)
    5.92 @@ -203,27 +209,35 @@
    5.93             raise NOT_SUPPORTED "transitive closure for function or pair type"
    5.94         | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)
    5.95         | Const (@{const_name semilattice_inf_class.inf},
    5.96 -                Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>
    5.97 +                Type (@{type_name fun},
    5.98 +                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
    5.99 +         $ t1 $ t2 =>
   5.100           Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
   5.101         | Const (@{const_name semilattice_inf_class.inf}, _) $ _ =>
   5.102           to_R_rep Ts (eta_expand Ts t 1)
   5.103         | Const (@{const_name semilattice_inf_class.inf}, _) =>
   5.104           to_R_rep Ts (eta_expand Ts t 2)
   5.105         | Const (@{const_name semilattice_sup_class.sup},
   5.106 -                Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>
   5.107 +                Type (@{type_name fun},
   5.108 +                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   5.109 +         $ t1 $ t2 =>
   5.110           Union (to_R_rep Ts t1, to_R_rep Ts t2)
   5.111         | Const (@{const_name semilattice_sup_class.sup}, _) $ _ =>
   5.112           to_R_rep Ts (eta_expand Ts t 1)
   5.113         | Const (@{const_name semilattice_sup_class.sup}, _) =>
   5.114           to_R_rep Ts (eta_expand Ts t 2)
   5.115         | Const (@{const_name minus_class.minus},
   5.116 -                Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>
   5.117 +                Type (@{type_name fun},
   5.118 +                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   5.119 +         $ t1 $ t2 =>
   5.120           Difference (to_R_rep Ts t1, to_R_rep Ts t2)
   5.121         | Const (@{const_name minus_class.minus},
   5.122 -                Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ _ =>
   5.123 +                Type (@{type_name fun},
   5.124 +                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
   5.125           to_R_rep Ts (eta_expand Ts t 1)
   5.126         | Const (@{const_name minus_class.minus},
   5.127 -                Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) =>
   5.128 +                Type (@{type_name fun},
   5.129 +                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) =>
   5.130           to_R_rep Ts (eta_expand Ts t 2)
   5.131         | Const (@{const_name Pair}, _) $ _ $ _ => raise SAME ()
   5.132         | Const (@{const_name Pair}, _) $ _ => raise SAME ()
   5.133 @@ -277,7 +291,8 @@
   5.134    end
   5.135  
   5.136  (* (typ -> int) -> typ list -> typ -> rel_expr -> formula *)
   5.137 -fun declarative_axiom_for_rel_expr card Ts (Type ("fun", [T1, T2])) r =
   5.138 +fun declarative_axiom_for_rel_expr card Ts (Type (@{type_name fun}, [T1, T2]))
   5.139 +                                   r =
   5.140      if body_type T2 = bool_T then
   5.141        True
   5.142      else
   5.143 @@ -294,8 +309,9 @@
   5.144    let
   5.145      val thy = ProofContext.theory_of ctxt
   5.146      (* typ -> int *)
   5.147 -    fun card (Type ("fun", [T1, T2])) = reasonable_power (card T2) (card T1)
   5.148 -      | card (Type ("*", [T1, T2])) = card T1 * card T2
   5.149 +    fun card (Type (@{type_name fun}, [T1, T2])) =
   5.150 +        reasonable_power (card T2) (card T1)
   5.151 +      | card (Type (@{type_name "*"}, [T1, T2])) = card T1 * card T2
   5.152        | card @{typ bool} = 2
   5.153        | card T = Int.max (1, raw_card T)
   5.154      val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Mar 08 15:20:40 2010 -0800
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Mar 09 09:25:23 2010 +0100
     6.3 @@ -15,6 +15,7 @@
     6.4      bitss: int list,
     6.5      bisim_depths: int list,
     6.6      boxes: (typ option * bool option) list,
     6.7 +    finitizes: (typ option * bool option) list,
     6.8      monos: (typ option * bool option) list,
     6.9      stds: (typ option * bool) list,
    6.10      wfs: (styp option * bool option) list,
    6.11 @@ -87,6 +88,7 @@
    6.12    bitss: int list,
    6.13    bisim_depths: int list,
    6.14    boxes: (typ option * bool option) list,
    6.15 +  finitizes: (typ option * bool option) list,
    6.16    monos: (typ option * bool option) list,
    6.17    stds: (typ option * bool) list,
    6.18    wfs: (styp option * bool option) list,
    6.19 @@ -200,13 +202,13 @@
    6.20              error "You must import the theory \"Nitpick\" to use Nitpick"
    6.21  *)
    6.22      val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
    6.23 -         boxes, monos, stds, wfs, sat_solver, falsify, debug, verbose, overlord,
    6.24 -         user_axioms, assms, merge_type_vars, binary_ints, destroy_constrs,
    6.25 -         specialize, skolemize, star_linear_preds, uncurry, fast_descrs,
    6.26 -         peephole_optim, tac_timeout, sym_break, sharing_depth, flatten_props,
    6.27 -         max_threads, show_skolems, show_datatypes, show_consts, evals, formats,
    6.28 -         max_potential, max_genuine, check_potential, check_genuine, batch_size,
    6.29 -         ...} =
    6.30 +         boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
    6.31 +         verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
    6.32 +         destroy_constrs, specialize, skolemize, star_linear_preds, uncurry,
    6.33 +         fast_descrs, peephole_optim, tac_timeout, sym_break, sharing_depth,
    6.34 +         flatten_props, max_threads, show_skolems, show_datatypes, show_consts,
    6.35 +         evals, formats, max_potential, max_genuine, check_potential,
    6.36 +         check_genuine, batch_size, ...} =
    6.37        params
    6.38      val state_ref = Unsynchronized.ref state
    6.39      (* Pretty.T -> unit *)
    6.40 @@ -289,7 +291,7 @@
    6.41      val _ = null (Term.add_tvars assms_t []) orelse
    6.42              raise NOT_SUPPORTED "schematic type variables"
    6.43      val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms,
    6.44 -         binarize) = preprocess_term hol_ctxt assms_t
    6.45 +         binarize) = preprocess_term hol_ctxt finitizes monos assms_t
    6.46      val got_all_user_axioms =
    6.47        got_all_mono_user_axioms andalso no_poly_user_axioms
    6.48  
    6.49 @@ -321,7 +323,11 @@
    6.50        fold add_free_and_const_names (nondef_us @ def_us) ([], [])
    6.51      val (sel_names, nonsel_names) =
    6.52        List.partition (is_sel o nickname_of) const_names
    6.53 -    val genuine_means_genuine = got_all_user_axioms andalso none_true wfs
    6.54 +    val sound_finitizes =
    6.55 +      none_true (filter_out (fn (SOME (Type (@{type_name fun}, _)), _) => true
    6.56 +                          | _ => false) finitizes)
    6.57 +    val genuine_means_genuine =
    6.58 +      got_all_user_axioms andalso none_true wfs andalso sound_finitizes
    6.59      val standard = forall snd stds
    6.60  (*
    6.61      val _ = List.app (priority o string_for_nut ctxt) (nondef_us @ def_us)
    6.62 @@ -340,21 +346,30 @@
    6.63          ". " ^ extra
    6.64        end
    6.65      (* typ -> bool *)
    6.66 -    fun is_type_always_monotonic T =
    6.67 +    fun is_type_fundamentally_monotonic T =
    6.68        (is_datatype thy stds T andalso not (is_quot_type thy T) andalso
    6.69         (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
    6.70        is_number_type thy T orelse is_bit_type T
    6.71      fun is_type_actually_monotonic T =
    6.72        formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
    6.73 +    fun is_type_kind_of_monotonic T =
    6.74 +      case triple_lookup (type_match thy) monos T of
    6.75 +        SOME (SOME false) => false
    6.76 +      | _ => is_type_actually_monotonic T
    6.77      fun is_type_monotonic T =
    6.78        unique_scope orelse
    6.79        case triple_lookup (type_match thy) monos T of
    6.80          SOME (SOME b) => b
    6.81 -      | _ => is_type_always_monotonic T orelse is_type_actually_monotonic T
    6.82 -    fun is_type_finitizable T =
    6.83 -      case triple_lookup (type_match thy) monos T of
    6.84 -        SOME (SOME false) => false
    6.85 -      | _ => is_type_actually_monotonic T
    6.86 +      | _ => is_type_fundamentally_monotonic T orelse
    6.87 +             is_type_actually_monotonic T
    6.88 +    fun is_shallow_datatype_finitizable (T as Type (@{type_name fin_fun}, _)) =
    6.89 +        is_type_kind_of_monotonic T
    6.90 +      | is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) =
    6.91 +        is_type_kind_of_monotonic T
    6.92 +      | is_shallow_datatype_finitizable T =
    6.93 +        case triple_lookup (type_match thy) finitizes T of
    6.94 +          SOME (SOME b) => b
    6.95 +        | _ => is_type_kind_of_monotonic T
    6.96      fun is_datatype_deep T =
    6.97        not standard orelse T = nat_T orelse is_word_type T orelse
    6.98        exists (curry (op =) T o domain_type o type_of) sel_names
    6.99 @@ -371,7 +386,7 @@
   6.100      val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
   6.101      val _ =
   6.102        if verbose andalso not unique_scope then
   6.103 -        case filter_out is_type_always_monotonic mono_Ts of
   6.104 +        case filter_out is_type_fundamentally_monotonic mono_Ts of
   6.105            [] => ()
   6.106          | interesting_mono_Ts =>
   6.107            print_v (K (monotonicity_message interesting_mono_Ts
   6.108 @@ -382,7 +397,7 @@
   6.109        all_Ts |> filter (is_datatype thy stds) |> List.partition is_datatype_deep
   6.110      val finitizable_dataTs =
   6.111        shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
   6.112 -                     |> filter is_type_finitizable
   6.113 +                     |> filter is_shallow_datatype_finitizable
   6.114      val _ =
   6.115        if verbose andalso not (null finitizable_dataTs) then
   6.116          print_v (K (monotonicity_message finitizable_dataTs
   6.117 @@ -649,6 +664,8 @@
   6.118                           ? cons ("user_axioms", "\"true\"")
   6.119                        |> not (none_true wfs)
   6.120                           ? cons ("wf", "\"smart\" or \"false\"")
   6.121 +                      |> not sound_finitizes
   6.122 +                         ? cons ("finitize", "\"smart\" or \"false\"")
   6.123                        |> not codatatypes_ok
   6.124                           ? cons ("bisim_depth", "a nonnegative value")
   6.125                   val ss =
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 08 15:20:40 2010 -0800
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Mar 09 09:25:23 2010 +0100
     7.3 @@ -65,8 +65,8 @@
     7.4    val strip_any_connective : term -> term list * term
     7.5    val conjuncts_of : term -> term list
     7.6    val disjuncts_of : term -> term list
     7.7 -  val unarize_and_unbox_type : typ -> typ
     7.8 -  val unarize_unbox_and_uniterize_type : typ -> typ
     7.9 +  val unarize_unbox_etc_type : typ -> typ
    7.10 +  val uniterize_unarize_unbox_etc_type : typ -> typ
    7.11    val string_for_type : Proof.context -> typ -> string
    7.12    val prefix_name : string -> string -> string
    7.13    val shortest_name : string -> string
    7.14 @@ -148,11 +148,13 @@
    7.15      theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term
    7.16    val construct_value :
    7.17      theory -> (typ option * bool) list -> styp -> term list -> term
    7.18 +  val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term
    7.19    val card_of_type : (typ * int) list -> typ -> int
    7.20    val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
    7.21    val bounded_exact_card_of_type :
    7.22      hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int
    7.23    val is_finite_type : hol_context -> typ -> bool
    7.24 +  val is_small_finite_type : hol_context -> typ -> bool
    7.25    val special_bounds : term list -> (indexname * typ) list
    7.26    val abs_var : indexname * typ -> term -> term
    7.27    val is_funky_typedef : theory -> typ -> bool
    7.28 @@ -401,22 +403,24 @@
    7.29    | unarize_type @{typ "signed_bit word"} = int_T
    7.30    | unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts)
    7.31    | unarize_type T = T
    7.32 -fun unarize_and_unbox_type (Type (@{type_name fun_box}, Ts)) =
    7.33 -    unarize_and_unbox_type (Type ("fun", Ts))
    7.34 -  | unarize_and_unbox_type (Type (@{type_name pair_box}, Ts)) =
    7.35 -    Type ("*", map unarize_and_unbox_type Ts)
    7.36 -  | unarize_and_unbox_type @{typ "unsigned_bit word"} = nat_T
    7.37 -  | unarize_and_unbox_type @{typ "signed_bit word"} = int_T
    7.38 -  | unarize_and_unbox_type (Type (s, Ts as _ :: _)) =
    7.39 -    Type (s, map unarize_and_unbox_type Ts)
    7.40 -  | unarize_and_unbox_type T = T
    7.41 +fun unarize_unbox_etc_type (Type (@{type_name fin_fun}, Ts)) =
    7.42 +    unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
    7.43 +  | unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) =
    7.44 +    unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
    7.45 +  | unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) =
    7.46 +    Type (@{type_name "*"}, map unarize_unbox_etc_type Ts)
    7.47 +  | unarize_unbox_etc_type @{typ "unsigned_bit word"} = nat_T
    7.48 +  | unarize_unbox_etc_type @{typ "signed_bit word"} = int_T
    7.49 +  | unarize_unbox_etc_type (Type (s, Ts as _ :: _)) =
    7.50 +    Type (s, map unarize_unbox_etc_type Ts)
    7.51 +  | unarize_unbox_etc_type T = T
    7.52  fun uniterize_type (Type (s, Ts as _ :: _)) = Type (s, map uniterize_type Ts)
    7.53    | uniterize_type @{typ bisim_iterator} = nat_T
    7.54    | uniterize_type T = T
    7.55 -val unarize_unbox_and_uniterize_type = uniterize_type o unarize_and_unbox_type
    7.56 +val uniterize_unarize_unbox_etc_type = uniterize_type o unarize_unbox_etc_type
    7.57  
    7.58  (* Proof.context -> typ -> string *)
    7.59 -fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_and_unbox_type
    7.60 +fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_unbox_etc_type
    7.61  
    7.62  (* string -> string -> string *)
    7.63  val prefix_name = Long_Name.qualify o Long_Name.base_name
    7.64 @@ -439,9 +443,10 @@
    7.65    #> map_types shorten_names_in_type
    7.66  
    7.67  (* theory -> typ * typ -> bool *)
    7.68 -fun type_match thy (T1, T2) =
    7.69 +fun strict_type_match thy (T1, T2) =
    7.70    (Sign.typ_match thy (T2, T1) Vartab.empty; true)
    7.71    handle Type.TYPE_MATCH => false
    7.72 +fun type_match thy = strict_type_match thy o pairself unarize_unbox_etc_type
    7.73  (* theory -> styp * styp -> bool *)
    7.74  fun const_match thy ((s1, T1), (s2, T2)) =
    7.75    s1 = s2 andalso type_match thy (T1, T2)
    7.76 @@ -454,14 +459,14 @@
    7.77  (* typ -> bool *)
    7.78  fun is_TFree (TFree _) = true
    7.79    | is_TFree _ = false
    7.80 -fun is_higher_order_type (Type ("fun", _)) = true
    7.81 +fun is_higher_order_type (Type (@{type_name fun}, _)) = true
    7.82    | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
    7.83    | is_higher_order_type _ = false
    7.84 -fun is_fun_type (Type ("fun", _)) = true
    7.85 +fun is_fun_type (Type (@{type_name fun}, _)) = true
    7.86    | is_fun_type _ = false
    7.87 -fun is_set_type (Type ("fun", [_, @{typ bool}])) = true
    7.88 +fun is_set_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
    7.89    | is_set_type _ = false
    7.90 -fun is_pair_type (Type ("*", _)) = true
    7.91 +fun is_pair_type (Type (@{type_name "*"}, _)) = true
    7.92    | is_pair_type _ = false
    7.93  fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
    7.94    | is_lfp_iterator_type _ = false
    7.95 @@ -494,19 +499,20 @@
    7.96  
    7.97  (* int -> typ -> typ list * typ *)
    7.98  fun strip_n_binders 0 T = ([], T)
    7.99 -  | strip_n_binders n (Type ("fun", [T1, T2])) =
   7.100 +  | strip_n_binders n (Type (@{type_name fun}, [T1, T2])) =
   7.101      strip_n_binders (n - 1) T2 |>> cons T1
   7.102    | strip_n_binders n (Type (@{type_name fun_box}, Ts)) =
   7.103 -    strip_n_binders n (Type ("fun", Ts))
   7.104 +    strip_n_binders n (Type (@{type_name fun}, Ts))
   7.105    | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
   7.106  (* typ -> typ *)
   7.107  val nth_range_type = snd oo strip_n_binders
   7.108  
   7.109  (* typ -> int *)
   7.110 -fun num_factors_in_type (Type ("*", [T1, T2])) =
   7.111 +fun num_factors_in_type (Type (@{type_name "*"}, [T1, T2])) =
   7.112      fold (Integer.add o num_factors_in_type) [T1, T2] 0
   7.113    | num_factors_in_type _ = 1
   7.114 -fun num_binder_types (Type ("fun", [_, T2])) = 1 + num_binder_types T2
   7.115 +fun num_binder_types (Type (@{type_name fun}, [_, T2])) =
   7.116 +    1 + num_binder_types T2
   7.117    | num_binder_types _ = 0
   7.118  (* typ -> typ list *)
   7.119  val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types
   7.120 @@ -515,7 +521,7 @@
   7.121  
   7.122  (* typ -> term list -> term *)
   7.123  fun mk_flat_tuple _ [t] = t
   7.124 -  | mk_flat_tuple (Type ("*", [T1, T2])) (t :: ts) =
   7.125 +  | mk_flat_tuple (Type (@{type_name "*"}, [T1, T2])) (t :: ts) =
   7.126      HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
   7.127    | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
   7.128  (* int -> term -> term list *)
   7.129 @@ -595,7 +601,7 @@
   7.130      val (co_s, co_Ts) = dest_Type co_T
   7.131      val _ =
   7.132        if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso
   7.133 -         co_s <> "fun" andalso
   7.134 +         co_s <> @{type_name fun} andalso
   7.135           not (is_basic_datatype thy [(NONE, true)] co_s) then
   7.136          ()
   7.137        else
   7.138 @@ -669,7 +675,7 @@
   7.139    find_index (curry (op =) s o fst)
   7.140               (Record.get_extT_fields thy T1 ||> single |> op @)
   7.141  (* theory -> styp -> bool *)
   7.142 -fun is_record_get thy (s, Type ("fun", [T1, _])) =
   7.143 +fun is_record_get thy (s, Type (@{type_name fun}, [T1, _])) =
   7.144      exists (curry (op =) s o fst) (all_record_fields thy T1)
   7.145    | is_record_get _ _ = false
   7.146  fun is_record_update thy (s, T) =
   7.147 @@ -677,30 +683,33 @@
   7.148    exists (curry (op =) (unsuffix Record.updateN s) o fst)
   7.149           (all_record_fields thy (body_type T))
   7.150    handle TYPE _ => false
   7.151 -fun is_abs_fun thy (s, Type ("fun", [_, Type (s', _)])) =
   7.152 +fun is_abs_fun thy (s, Type (@{type_name fun}, [_, Type (s', _)])) =
   7.153      (case typedef_info thy s' of
   7.154         SOME {Abs_name, ...} => s = Abs_name
   7.155       | NONE => false)
   7.156    | is_abs_fun _ _ = false
   7.157 -fun is_rep_fun thy (s, Type ("fun", [Type (s', _), _])) =
   7.158 +fun is_rep_fun thy (s, Type (@{type_name fun}, [Type (s', _), _])) =
   7.159      (case typedef_info thy s' of
   7.160         SOME {Rep_name, ...} => s = Rep_name
   7.161       | NONE => false)
   7.162    | is_rep_fun _ _ = false
   7.163  (* Proof.context -> styp -> bool *)
   7.164 -fun is_quot_abs_fun ctxt (x as (_, Type ("fun", [_, Type (s', _)]))) =
   7.165 +fun is_quot_abs_fun ctxt
   7.166 +                    (x as (_, Type (@{type_name fun}, [_, Type (s', _)]))) =
   7.167      (try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s'
   7.168       = SOME (Const x))
   7.169    | is_quot_abs_fun _ _ = false
   7.170 -fun is_quot_rep_fun ctxt (x as (_, Type ("fun", [Type (s', _), _]))) =
   7.171 +fun is_quot_rep_fun ctxt
   7.172 +                    (x as (_, Type (@{type_name fun}, [Type (s', _), _]))) =
   7.173      (try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s'
   7.174       = SOME (Const x))
   7.175    | is_quot_rep_fun _ _ = false
   7.176  
   7.177  (* theory -> styp -> styp *)
   7.178 -fun mate_of_rep_fun thy (x as (_, Type ("fun", [T1 as Type (s', _), T2]))) =
   7.179 +fun mate_of_rep_fun thy (x as (_, Type (@{type_name fun},
   7.180 +                                        [T1 as Type (s', _), T2]))) =
   7.181      (case typedef_info thy s' of
   7.182 -       SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1]))
   7.183 +       SOME {Abs_name, ...} => (Abs_name, Type (@{type_name fun}, [T2, T1]))
   7.184       | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
   7.185    | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
   7.186  (* theory -> typ -> typ *)
   7.187 @@ -729,10 +738,10 @@
   7.188    end
   7.189    handle TYPE ("dest_Type", _, _) => false
   7.190  fun is_constr_like thy (s, T) =
   7.191 -  member (op =) [@{const_name FunBox}, @{const_name PairBox},
   7.192 -                 @{const_name Quot}, @{const_name Zero_Rep},
   7.193 -                 @{const_name Suc_Rep}] s orelse
   7.194 -  let val (x as (_, T)) = (s, unarize_and_unbox_type T) in
   7.195 +  member (op =) [@{const_name FinFun}, @{const_name FunBox},
   7.196 +                 @{const_name PairBox}, @{const_name Quot},
   7.197 +                 @{const_name Zero_Rep}, @{const_name Suc_Rep}] s orelse
   7.198 +  let val (x as (_, T)) = (s, unarize_unbox_etc_type T) in
   7.199      Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
   7.200      (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
   7.201      is_coconstr thy x
   7.202 @@ -749,8 +758,8 @@
   7.203  (* string -> bool *)
   7.204  val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
   7.205  val is_sel_like_and_no_discr =
   7.206 -  String.isPrefix sel_prefix
   7.207 -  orf (member (op =) [@{const_name fst}, @{const_name snd}])
   7.208 +  String.isPrefix sel_prefix orf
   7.209 +  (member (op =) [@{const_name fst}, @{const_name snd}])
   7.210  
   7.211  (* boxability -> boxability *)
   7.212  fun in_fun_lhs_for InConstr = InSel
   7.213 @@ -763,10 +772,10 @@
   7.214  (* hol_context -> boxability -> typ -> bool *)
   7.215  fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T =
   7.216    case T of
   7.217 -    Type ("fun", _) =>
   7.218 +    Type (@{type_name fun}, _) =>
   7.219      (boxy = InPair orelse boxy = InFunLHS) andalso
   7.220      not (is_boolean_type (body_type T))
   7.221 -  | Type ("*", Ts) =>
   7.222 +  | Type (@{type_name "*"}, Ts) =>
   7.223      boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
   7.224      ((boxy = InExpr orelse boxy = InFunLHS) andalso
   7.225       exists (is_boxing_worth_it hol_ctxt InPair)
   7.226 @@ -780,7 +789,7 @@
   7.227  (* hol_context -> boxability -> typ -> typ *)
   7.228  and box_type hol_ctxt boxy T =
   7.229    case T of
   7.230 -    Type (z as ("fun", [T1, T2])) =>
   7.231 +    Type (z as (@{type_name fun}, [T1, T2])) =>
   7.232      if boxy <> InConstr andalso boxy <> InSel andalso
   7.233         should_box_type hol_ctxt boxy z then
   7.234        Type (@{type_name fun_box},
   7.235 @@ -788,12 +797,13 @@
   7.236      else
   7.237        box_type hol_ctxt (in_fun_lhs_for boxy) T1
   7.238        --> box_type hol_ctxt (in_fun_rhs_for boxy) T2
   7.239 -  | Type (z as ("*", Ts)) =>
   7.240 +  | Type (z as (@{type_name "*"}, Ts)) =>
   7.241      if boxy <> InConstr andalso boxy <> InSel
   7.242         andalso should_box_type hol_ctxt boxy z then
   7.243        Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts)
   7.244      else
   7.245 -      Type ("*", map (box_type hol_ctxt
   7.246 +      Type (@{type_name "*"},
   7.247 +            map (box_type hol_ctxt
   7.248                            (if boxy = InConstr orelse boxy = InSel then boxy
   7.249                             else InPair)) Ts)
   7.250    | _ => T
   7.251 @@ -979,7 +989,7 @@
   7.252      else
   7.253        let
   7.254          (* int -> typ -> int * term *)
   7.255 -        fun aux m (Type ("*", [T1, T2])) =
   7.256 +        fun aux m (Type (@{type_name "*"}, [T1, T2])) =
   7.257              let
   7.258                val (m, t1) = aux m T1
   7.259                val (m, t2) = aux m T2
   7.260 @@ -1018,10 +1028,85 @@
   7.261        | _ => list_comb (Const x, args)
   7.262      end
   7.263  
   7.264 +(* hol_context -> typ -> term -> term *)
   7.265 +fun constr_expand (hol_ctxt as {thy, stds, ...}) T t =
   7.266 +  (case head_of t of
   7.267 +     Const x => if is_constr_like thy x then t else raise SAME ()
   7.268 +   | _ => raise SAME ())
   7.269 +  handle SAME () =>
   7.270 +         let
   7.271 +           val x' as (_, T') =
   7.272 +             if is_pair_type T then
   7.273 +               let val (T1, T2) = HOLogic.dest_prodT T in
   7.274 +                 (@{const_name Pair}, T1 --> T2 --> T)
   7.275 +               end
   7.276 +             else
   7.277 +               datatype_constrs hol_ctxt T |> hd
   7.278 +           val arg_Ts = binder_types T'
   7.279 +         in
   7.280 +           list_comb (Const x', map2 (select_nth_constr_arg thy stds x' t)
   7.281 +                                     (index_seq 0 (length arg_Ts)) arg_Ts)
   7.282 +         end
   7.283 +
   7.284 +(* (term -> term) -> int -> term -> term *)
   7.285 +fun coerce_bound_no f j t =
   7.286 +  case t of
   7.287 +    t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
   7.288 +  | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
   7.289 +  | Bound j' => if j' = j then f t else t
   7.290 +  | _ => t
   7.291 +(* hol_context -> typ -> typ -> term -> term *)
   7.292 +fun coerce_bound_0_in_term hol_ctxt new_T old_T =
   7.293 +  old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
   7.294 +(* hol_context -> typ list -> typ -> typ -> term -> term *)
   7.295 +and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t =
   7.296 +  if old_T = new_T then
   7.297 +    t
   7.298 +  else
   7.299 +    case (new_T, old_T) of
   7.300 +      (Type (new_s, new_Ts as [new_T1, new_T2]),
   7.301 +       Type (@{type_name fun}, [old_T1, old_T2])) =>
   7.302 +      (case eta_expand Ts t 1 of
   7.303 +         Abs (s, _, t') =>
   7.304 +         Abs (s, new_T1,
   7.305 +              t' |> coerce_bound_0_in_term hol_ctxt new_T1 old_T1
   7.306 +                 |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)
   7.307 +         |> Envir.eta_contract
   7.308 +         |> new_s <> @{type_name fun}
   7.309 +            ? construct_value thy stds
   7.310 +                  (if new_s = @{type_name fin_fun} then @{const_name FinFun}
   7.311 +                   else @{const_name FunBox},
   7.312 +                   Type (@{type_name fun}, new_Ts) --> new_T)
   7.313 +              o single
   7.314 +       | t' => raise TERM ("Nitpick_HOL.coerce_term", [t']))
   7.315 +    | (Type (new_s, new_Ts as [new_T1, new_T2]),
   7.316 +       Type (old_s, old_Ts as [old_T1, old_T2])) =>
   7.317 +      if old_s = @{type_name fin_fun} orelse old_s = @{type_name fun_box} orelse
   7.318 +         old_s = @{type_name pair_box} orelse old_s = @{type_name "*"} then
   7.319 +        case constr_expand hol_ctxt old_T t of
   7.320 +          Const (old_s, _) $ t1 =>
   7.321 +          if new_s = @{type_name fun} then
   7.322 +            coerce_term hol_ctxt Ts new_T (Type (@{type_name fun}, old_Ts)) t1
   7.323 +          else
   7.324 +            construct_value thy stds
   7.325 +                (old_s, Type (@{type_name fun}, new_Ts) --> new_T)
   7.326 +                [coerce_term hol_ctxt Ts (Type (@{type_name fun}, new_Ts))
   7.327 +                             (Type (@{type_name fun}, old_Ts)) t1]
   7.328 +        | Const _ $ t1 $ t2 =>
   7.329 +          construct_value thy stds
   7.330 +              (if new_s = @{type_name "*"} then @{const_name Pair}
   7.331 +               else @{const_name PairBox}, new_Ts ---> new_T)
   7.332 +              (map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2]
   7.333 +                    [t1, t2])
   7.334 +        | t' => raise TERM ("Nitpick_HOL.coerce_term", [t'])
   7.335 +      else
   7.336 +        raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t])
   7.337 +    | _ => raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t])
   7.338 +
   7.339  (* (typ * int) list -> typ -> int *)
   7.340 -fun card_of_type assigns (Type ("fun", [T1, T2])) =
   7.341 +fun card_of_type assigns (Type (@{type_name fun}, [T1, T2])) =
   7.342      reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
   7.343 -  | card_of_type assigns (Type ("*", [T1, T2])) =
   7.344 +  | card_of_type assigns (Type (@{type_name "*"}, [T1, T2])) =
   7.345      card_of_type assigns T1 * card_of_type assigns T2
   7.346    | card_of_type _ (Type (@{type_name itself}, _)) = 1
   7.347    | card_of_type _ @{typ prop} = 2
   7.348 @@ -1033,7 +1118,8 @@
   7.349      | NONE => if T = @{typ bisim_iterator} then 0
   7.350                else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
   7.351  (* int -> (typ * int) list -> typ -> int *)
   7.352 -fun bounded_card_of_type max default_card assigns (Type ("fun", [T1, T2])) =
   7.353 +fun bounded_card_of_type max default_card assigns
   7.354 +                         (Type (@{type_name fun}, [T1, T2])) =
   7.355      let
   7.356        val k1 = bounded_card_of_type max default_card assigns T1
   7.357        val k2 = bounded_card_of_type max default_card assigns T2
   7.358 @@ -1041,7 +1127,8 @@
   7.359        if k1 = max orelse k2 = max then max
   7.360        else Int.min (max, reasonable_power k2 k1)
   7.361      end
   7.362 -  | bounded_card_of_type max default_card assigns (Type ("*", [T1, T2])) =
   7.363 +  | bounded_card_of_type max default_card assigns
   7.364 +                         (Type (@{type_name "*"}, [T1, T2])) =
   7.365      let
   7.366        val k1 = bounded_card_of_type max default_card assigns T1
   7.367        val k2 = bounded_card_of_type max default_card assigns T2
   7.368 @@ -1064,7 +1151,7 @@
   7.369         else if member (op =) finitizable_dataTs T then
   7.370           raise SAME ()
   7.371         else case T of
   7.372 -         Type ("fun", [T1, T2]) =>
   7.373 +         Type (@{type_name fun}, [T1, T2]) =>
   7.374           let
   7.375             val k1 = aux avoid T1
   7.376             val k2 = aux avoid T2
   7.377 @@ -1073,7 +1160,7 @@
   7.378             else if k1 >= max orelse k2 >= max then max
   7.379             else Int.min (max, reasonable_power k2 k1)
   7.380           end
   7.381 -       | Type ("*", [T1, T2]) =>
   7.382 +       | Type (@{type_name "*"}, [T1, T2]) =>
   7.383           let
   7.384             val k1 = aux avoid T1
   7.385             val k2 = aux avoid T2
   7.386 @@ -1104,9 +1191,16 @@
   7.387               AList.lookup (op =) assigns T |> the_default default_card
   7.388    in Int.min (max, aux [] T) end
   7.389  
   7.390 +val small_type_max_card = 5
   7.391 +
   7.392  (* hol_context -> typ -> bool *)
   7.393  fun is_finite_type hol_ctxt T =
   7.394 -  bounded_exact_card_of_type hol_ctxt [] 1 2 [] T <> 0
   7.395 +  bounded_exact_card_of_type hol_ctxt [] 1 2 [] T > 0
   7.396 +(* hol_context -> typ -> bool *)
   7.397 +fun is_small_finite_type hol_ctxt T =
   7.398 +  let val n = bounded_exact_card_of_type hol_ctxt [] 1 2 [] T in
   7.399 +    n > 0 andalso n <= small_type_max_card
   7.400 +  end
   7.401  
   7.402  (* term -> bool *)
   7.403  fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
   7.404 @@ -1144,7 +1238,8 @@
   7.405      is_typedef_axiom thy boring t2
   7.406    | is_typedef_axiom thy boring
   7.407          (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
   7.408 -         $ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) =
   7.409 +         $ Const (_, Type (@{type_name fun}, [Type (s, _), _]))
   7.410 +         $ Const _ $ _)) =
   7.411      boring <> is_funky_typedef_name thy s andalso is_typedef thy s
   7.412    | is_typedef_axiom _ _ _ = false
   7.413  
   7.414 @@ -1538,8 +1633,8 @@
   7.415  fun is_inductive_pred hol_ctxt =
   7.416    is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt)
   7.417  fun is_equational_fun hol_ctxt =
   7.418 -  (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt
   7.419 -   orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
   7.420 +  (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt orf
   7.421 +   (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
   7.422  
   7.423  (* term * term -> term *)
   7.424  fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
   7.425 @@ -1586,7 +1681,7 @@
   7.426      fun do_term depth Ts t =
   7.427        case t of
   7.428          (t0 as Const (@{const_name Int.number_class.number_of},
   7.429 -                      Type ("fun", [_, ran_T]))) $ t1 =>
   7.430 +                      Type (@{type_name fun}, [_, ran_T]))) $ t1 =>
   7.431          ((if is_number_type thy ran_T then
   7.432              let
   7.433                val j = t1 |> HOLogic.dest_numeral
   7.434 @@ -1612,7 +1707,7 @@
   7.435          betapplys (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
   7.436                     map (do_term depth Ts) [t1, t2])
   7.437        | Const (x as (@{const_name distinct},
   7.438 -               Type ("fun", [Type (@{type_name list}, [T']), _])))
   7.439 +               Type (@{type_name fun}, [Type (@{type_name list}, [T']), _])))
   7.440          $ (t1 as _ $ _) =>
   7.441          (t1 |> HOLogic.dest_list |> distinctness_formula T'
   7.442           handle TERM _ => do_const depth Ts t x [t1])
   7.443 @@ -1969,7 +2064,7 @@
   7.444      val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
   7.445      val set_T = tuple_T --> bool_T
   7.446      val curried_T = tuple_T --> set_T
   7.447 -    val uncurried_T = Type ("*", [tuple_T, tuple_T]) --> bool_T
   7.448 +    val uncurried_T = Type (@{type_name "*"}, [tuple_T, tuple_T]) --> bool_T
   7.449      val (base_rhs, step_rhs) = linear_pred_base_and_step_rhss fp_app
   7.450      val base_x as (base_s, _) = (base_prefix ^ s, outer_Ts ---> set_T)
   7.451      val base_eq = HOLogic.mk_eq (list_comb (Const base_x, outer_vars), base_rhs)
   7.452 @@ -2092,8 +2187,8 @@
   7.453    let
   7.454      fun aux T accum =
   7.455        case T of
   7.456 -        Type ("fun", Ts) => fold aux Ts accum
   7.457 -      | Type ("*", Ts) => fold aux Ts accum
   7.458 +        Type (@{type_name fun}, Ts) => fold aux Ts accum
   7.459 +      | Type (@{type_name "*"}, Ts) => fold aux Ts accum
   7.460        | Type (@{type_name itself}, [T1]) => aux T1 accum
   7.461        | Type (_, Ts) =>
   7.462          if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum)
   7.463 @@ -2161,7 +2256,7 @@
   7.464  (* int list -> int list -> typ -> typ *)
   7.465  fun format_type default_format format T =
   7.466    let
   7.467 -    val T = unarize_unbox_and_uniterize_type T
   7.468 +    val T = uniterize_unarize_unbox_etc_type T
   7.469      val format = format |> filter (curry (op <) 0)
   7.470    in
   7.471      if forall (curry (op =) 1) format then
   7.472 @@ -2200,7 +2295,7 @@
   7.473             (* term -> term *)
   7.474             val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t')
   7.475             val (x' as (_, T'), js, ts) =
   7.476 -             AList.find (op =) (!special_funs) (s, unarize_and_unbox_type T)
   7.477 +             AList.find (op =) (!special_funs) (s, unarize_unbox_etc_type T)
   7.478               |> the_single
   7.479             val max_j = List.last js
   7.480             val Ts = List.take (binder_types T', max_j + 1)
   7.481 @@ -2294,7 +2389,7 @@
   7.482           let val t = Const (original_name s, T) in
   7.483             (t, format_term_type thy def_table formats t)
   7.484           end)
   7.485 -      |>> map_types unarize_unbox_and_uniterize_type
   7.486 +      |>> map_types uniterize_unarize_unbox_etc_type
   7.487        |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
   7.488    in do_const end
   7.489  
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Mar 08 15:20:40 2010 -0800
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Mar 09 09:25:23 2010 +0100
     8.3 @@ -39,6 +39,7 @@
     8.4     ("bits", ["1,2,3,4,6,8,10,12"]),
     8.5     ("bisim_depth", ["7"]),
     8.6     ("box", ["smart"]),
     8.7 +   ("finitize", ["smart"]),
     8.8     ("mono", ["smart"]),
     8.9     ("std", ["true"]),
    8.10     ("wf", ["smart"]),
    8.11 @@ -78,6 +79,7 @@
    8.12  
    8.13  val negated_params =
    8.14    [("dont_box", "box"),
    8.15 +   ("dont_finitize", "finitize"),
    8.16     ("non_mono", "mono"),
    8.17     ("non_std", "std"),
    8.18     ("non_wf", "wf"),
    8.19 @@ -111,8 +113,8 @@
    8.20    AList.defined (op =) negated_params s orelse
    8.21    s = "max" orelse s = "eval" orelse s = "expect" orelse
    8.22    exists (fn p => String.isPrefix (p ^ " ") s)
    8.23 -         ["card", "max", "iter", "box", "dont_box", "mono", "non_mono", "std",
    8.24 -          "non_std", "wf", "non_wf", "format"]
    8.25 +         ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
    8.26 +          "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format"]
    8.27  
    8.28  (* string * 'a -> unit *)
    8.29  fun check_raw_param (s, _) =
    8.30 @@ -297,14 +299,8 @@
    8.31      val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0
    8.32      val bitss = lookup_int_seq "bits" 1
    8.33      val bisim_depths = lookup_int_seq "bisim_depth" ~1
    8.34 -    val boxes =
    8.35 -      lookup_bool_option_assigns read_type_polymorphic "box" @
    8.36 -      map_filter (fn (SOME T, _) =>
    8.37 -                     if is_fun_type T orelse is_pair_type T then
    8.38 -                       SOME (SOME T, SOME true)
    8.39 -                     else
    8.40 -                       NONE
    8.41 -                   | (NONE, _) => NONE) cards_assigns
    8.42 +    val boxes = lookup_bool_option_assigns read_type_polymorphic "box"
    8.43 +    val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize"
    8.44      val monos = lookup_bool_option_assigns read_type_polymorphic "mono"
    8.45      val stds = lookup_bool_assigns read_type_polymorphic "std"
    8.46      val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"
    8.47 @@ -349,8 +345,8 @@
    8.48    in
    8.49      {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
    8.50       iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths,
    8.51 -     boxes = boxes, monos = monos, stds = stds, wfs = wfs,
    8.52 -     sat_solver = sat_solver, blocking = blocking, falsify = falsify,
    8.53 +     boxes = boxes, finitizes = finitizes, monos = monos, stds = stds,
    8.54 +     wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify,
    8.55       debug = debug, verbose = verbose, overlord = overlord,
    8.56       user_axioms = user_axioms, assms = assms,
    8.57       merge_type_vars = merge_type_vars, binary_ints = binary_ints,
     9.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Mar 08 15:20:40 2010 -0800
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Mar 09 09:25:23 2010 +0100
     9.3 @@ -301,8 +301,8 @@
     9.4  
     9.5  (* Proof.context -> bool -> dtype_spec list -> nut -> KK.bound *)
     9.6  fun bound_for_sel_rel ctxt debug dtypes
     9.7 -        (FreeRel (x, T as Type ("fun", [T1, T2]), R as Func (Atom (_, j0), R2),
     9.8 -                  nick)) =
     9.9 +        (FreeRel (x, T as Type (@{type_name fun}, [T1, T2]),
    9.10 +                  R as Func (Atom (_, j0), R2), nick)) =
    9.11      let
    9.12        val {delta, epsilon, exclusive, explicit_max, ...} =
    9.13          constr_spec dtypes (original_name nick, T1)
    9.14 @@ -1208,7 +1208,7 @@
    9.15                             (rel_expr_from_rel_expr kk min_R R2 r2))
    9.16            end
    9.17        | Cst (Iden, _, Func (Atom (1, j0), Formula Neut)) => KK.Atom j0
    9.18 -      | Cst (Iden, T as Type ("fun", [T1, _]), R as Func (R1, _)) =>
    9.19 +      | Cst (Iden, T as Type (@{type_name fun}, [T1, _]), R as Func (R1, _)) =>
    9.20          to_rep R (Cst (Iden, T, Func (one_rep ofs T1 R1, Formula Neut)))
    9.21        | Cst (Num j, T, R) =>
    9.22          if is_word_type T then
    9.23 @@ -1229,36 +1229,36 @@
    9.24        | Cst (Suc, @{typ "nat => nat"}, Func (Atom x, _)) =>
    9.25          kk_intersect (KK.Rel suc_rel) (kk_product KK.Univ (KK.AtomSeq x))
    9.26        | Cst (Suc, _, Func (Atom _, _)) => KK.Rel suc_rel
    9.27 -      | Cst (Add, Type ("fun", [@{typ nat}, _]), _) => KK.Rel nat_add_rel
    9.28 -      | Cst (Add, Type ("fun", [@{typ int}, _]), _) => KK.Rel int_add_rel
    9.29 -      | Cst (Add, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
    9.30 +      | Cst (Add, Type (_, [@{typ nat}, _]), _) => KK.Rel nat_add_rel
    9.31 +      | Cst (Add, Type (_, [@{typ int}, _]), _) => KK.Rel int_add_rel
    9.32 +      | Cst (Add, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>
    9.33          to_bit_word_binary_op T R NONE (SOME (curry KK.Add))
    9.34 -      | Cst (Add, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
    9.35 +      | Cst (Add, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>
    9.36          to_bit_word_binary_op T R
    9.37              (SOME (fn i1 => fn i2 => fn i3 =>
    9.38                   kk_implies (KK.LE (KK.Num 0, KK.BitXor (i1, i2)))
    9.39                              (KK.LE (KK.Num 0, KK.BitXor (i2, i3)))))
    9.40              (SOME (curry KK.Add))
    9.41 -      | Cst (Subtract, Type ("fun", [@{typ nat}, _]), _) =>
    9.42 +      | Cst (Subtract, Type (_, [@{typ nat}, _]), _) =>
    9.43          KK.Rel nat_subtract_rel
    9.44 -      | Cst (Subtract, Type ("fun", [@{typ int}, _]), _) =>
    9.45 +      | Cst (Subtract, Type (_, [@{typ int}, _]), _) =>
    9.46          KK.Rel int_subtract_rel
    9.47 -      | Cst (Subtract, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
    9.48 +      | Cst (Subtract, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>
    9.49          to_bit_word_binary_op T R NONE
    9.50              (SOME (fn i1 => fn i2 =>
    9.51                        KK.IntIf (KK.LE (i1, i2), KK.Num 0, KK.Sub (i1, i2))))
    9.52 -      | Cst (Subtract, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
    9.53 +      | Cst (Subtract, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>
    9.54          to_bit_word_binary_op T R
    9.55              (SOME (fn i1 => fn i2 => fn i3 =>
    9.56                   kk_implies (KK.LT (KK.BitXor (i1, i2), KK.Num 0))
    9.57                              (KK.LT (KK.BitXor (i2, i3), KK.Num 0))))
    9.58              (SOME (curry KK.Sub))
    9.59 -      | Cst (Multiply, Type ("fun", [@{typ nat}, _]), _) =>
    9.60 +      | Cst (Multiply, Type (_, [@{typ nat}, _]), _) =>
    9.61          KK.Rel nat_multiply_rel
    9.62 -      | Cst (Multiply, Type ("fun", [@{typ int}, _]), _) =>
    9.63 +      | Cst (Multiply, Type (_, [@{typ int}, _]), _) =>
    9.64          KK.Rel int_multiply_rel
    9.65        | Cst (Multiply,
    9.66 -             T as Type ("fun", [Type (@{type_name word}, [bit_T]), _]), R) =>
    9.67 +             T as Type (_, [Type (@{type_name word}, [bit_T]), _]), R) =>
    9.68          to_bit_word_binary_op T R
    9.69              (SOME (fn i1 => fn i2 => fn i3 =>
    9.70                  kk_or (KK.IntEq (i2, KK.Num 0))
    9.71 @@ -1267,14 +1267,14 @@
    9.72                            ? kk_and (KK.LE (KK.Num 0,
    9.73                                             foldl1 KK.BitAnd [i1, i2, i3])))))
    9.74              (SOME (curry KK.Mult))
    9.75 -      | Cst (Divide, Type ("fun", [@{typ nat}, _]), _) => KK.Rel nat_divide_rel
    9.76 -      | Cst (Divide, Type ("fun", [@{typ int}, _]), _) => KK.Rel int_divide_rel
    9.77 -      | Cst (Divide, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
    9.78 +      | Cst (Divide, Type (_, [@{typ nat}, _]), _) => KK.Rel nat_divide_rel
    9.79 +      | Cst (Divide, Type (_, [@{typ int}, _]), _) => KK.Rel int_divide_rel
    9.80 +      | Cst (Divide, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>
    9.81          to_bit_word_binary_op T R NONE
    9.82              (SOME (fn i1 => fn i2 =>
    9.83                        KK.IntIf (KK.IntEq (i2, KK.Num 0),
    9.84                                  KK.Num 0, KK.Div (i1, i2))))
    9.85 -      | Cst (Divide, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
    9.86 +      | Cst (Divide, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>
    9.87          to_bit_word_binary_op T R
    9.88              (SOME (fn i1 => fn i2 => fn i3 =>
    9.89                        KK.LE (KK.Num 0, foldl1 KK.BitAnd [i1, i2, i3])))
    9.90 @@ -1293,9 +1293,9 @@
    9.91        | Cst (Fracs, _, Func (Struct _, _)) =>
    9.92          kk_project_seq (KK.Rel norm_frac_rel) 2 2
    9.93        | Cst (NormFrac, _, _) => KK.Rel norm_frac_rel
    9.94 -      | Cst (NatToInt, Type ("fun", [@{typ nat}, _]), Func (Atom _, Atom _)) =>
    9.95 +      | Cst (NatToInt, Type (_, [@{typ nat}, _]), Func (Atom _, Atom _)) =>
    9.96          KK.Iden
    9.97 -      | Cst (NatToInt, Type ("fun", [@{typ nat}, _]),
    9.98 +      | Cst (NatToInt, Type (_, [@{typ nat}, _]),
    9.99               Func (Atom (_, nat_j0), Opt (Atom (int_k, int_j0)))) =>
   9.100          if nat_j0 = int_j0 then
   9.101            kk_intersect KK.Iden
   9.102 @@ -1303,9 +1303,9 @@
   9.103                            KK.Univ)
   9.104          else
   9.105            raise BAD ("Nitpick_Kodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"")
   9.106 -      | Cst (NatToInt, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
   9.107 +      | Cst (NatToInt, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>
   9.108          to_bit_word_unary_op T R I
   9.109 -      | Cst (IntToNat, Type ("fun", [@{typ int}, _]),
   9.110 +      | Cst (IntToNat, Type (_, [@{typ int}, _]),
   9.111               Func (Atom (int_k, int_j0), nat_R)) =>
   9.112          let
   9.113            val abs_card = max_int_for_card int_k + 1
   9.114 @@ -1321,7 +1321,7 @@
   9.115            else
   9.116              raise BAD ("Nitpick_Kodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"")
   9.117          end
   9.118 -      | Cst (IntToNat, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
   9.119 +      | Cst (IntToNat, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>
   9.120          to_bit_word_unary_op T R
   9.121              (fn i => KK.IntIf (KK.LE (i, KK.Num 0), KK.Num 0, i))
   9.122        | Op1 (Not, _, R, u1) => kk_not3 (to_rep R u1)
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Mar 08 15:20:40 2010 -0800
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Mar 09 09:25:23 2010 +0100
    10.3 @@ -110,48 +110,53 @@
    10.4    the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
    10.5  
    10.6  (* term -> term *)
    10.7 -fun unarize_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) =
    10.8 -    unarize_and_unbox_term t1
    10.9 -  | unarize_and_unbox_term (Const (@{const_name PairBox},
   10.10 -                                   Type ("fun", [T1, Type ("fun", [T2, _])]))
   10.11 -                            $ t1 $ t2) =
   10.12 -    let val Ts = map unarize_unbox_and_uniterize_type [T1, T2] in
   10.13 -      Const (@{const_name Pair}, Ts ---> Type ("*", Ts))
   10.14 -      $ unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
   10.15 +fun unarize_unbox_etc_term (Const (@{const_name FinFun}, _) $ t1) =
   10.16 +    unarize_unbox_etc_term t1
   10.17 +  | unarize_unbox_etc_term (Const (@{const_name FunBox}, _) $ t1) =
   10.18 +    unarize_unbox_etc_term t1
   10.19 +  | unarize_unbox_etc_term
   10.20 +        (Const (@{const_name PairBox},
   10.21 +                Type (@{type_name fun}, [T1, Type (@{type_name fun}, [T2, _])]))
   10.22 +         $ t1 $ t2) =
   10.23 +    let val Ts = map uniterize_unarize_unbox_etc_type [T1, T2] in
   10.24 +      Const (@{const_name Pair}, Ts ---> Type (@{type_name "*"}, Ts))
   10.25 +      $ unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2
   10.26      end
   10.27 -  | unarize_and_unbox_term (Const (s, T)) =
   10.28 -    Const (s, unarize_unbox_and_uniterize_type T)
   10.29 -  | unarize_and_unbox_term (t1 $ t2) =
   10.30 -    unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
   10.31 -  | unarize_and_unbox_term (Free (s, T)) =
   10.32 -    Free (s, unarize_unbox_and_uniterize_type T)
   10.33 -  | unarize_and_unbox_term (Var (x, T)) =
   10.34 -    Var (x, unarize_unbox_and_uniterize_type T)
   10.35 -  | unarize_and_unbox_term (Bound j) = Bound j
   10.36 -  | unarize_and_unbox_term (Abs (s, T, t')) =
   10.37 -    Abs (s, unarize_unbox_and_uniterize_type T, unarize_and_unbox_term t')
   10.38 +  | unarize_unbox_etc_term (Const (s, T)) =
   10.39 +    Const (s, uniterize_unarize_unbox_etc_type T)
   10.40 +  | unarize_unbox_etc_term (t1 $ t2) =
   10.41 +    unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2
   10.42 +  | unarize_unbox_etc_term (Free (s, T)) =
   10.43 +    Free (s, uniterize_unarize_unbox_etc_type T)
   10.44 +  | unarize_unbox_etc_term (Var (x, T)) =
   10.45 +    Var (x, uniterize_unarize_unbox_etc_type T)
   10.46 +  | unarize_unbox_etc_term (Bound j) = Bound j
   10.47 +  | unarize_unbox_etc_term (Abs (s, T, t')) =
   10.48 +    Abs (s, uniterize_unarize_unbox_etc_type T, unarize_unbox_etc_term t')
   10.49  
   10.50  (* typ -> typ -> (typ * typ) * (typ * typ) *)
   10.51 -fun factor_out_types (T1 as Type ("*", [T11, T12]))
   10.52 -                     (T2 as Type ("*", [T21, T22])) =
   10.53 +fun factor_out_types (T1 as Type (@{type_name "*"}, [T11, T12]))
   10.54 +                     (T2 as Type (@{type_name "*"}, [T21, T22])) =
   10.55      let val (n1, n2) = pairself num_factors_in_type (T11, T21) in
   10.56        if n1 = n2 then
   10.57          let
   10.58            val ((T11', opt_T12'), (T21', opt_T22')) = factor_out_types T12 T22
   10.59          in
   10.60 -          ((Type ("*", [T11, T11']), opt_T12'),
   10.61 -           (Type ("*", [T21, T21']), opt_T22'))
   10.62 +          ((Type (@{type_name "*"}, [T11, T11']), opt_T12'),
   10.63 +           (Type (@{type_name "*"}, [T21, T21']), opt_T22'))
   10.64          end
   10.65        else if n1 < n2 then
   10.66          case factor_out_types T1 T21 of
   10.67            (p1, (T21', NONE)) => (p1, (T21', SOME T22))
   10.68          | (p1, (T21', SOME T22')) =>
   10.69 -          (p1, (T21', SOME (Type ("*", [T22', T22]))))
   10.70 +          (p1, (T21', SOME (Type (@{type_name "*"}, [T22', T22]))))
   10.71        else
   10.72          swap (factor_out_types T2 T1)
   10.73      end
   10.74 -  | factor_out_types (Type ("*", [T11, T12])) T2 = ((T11, SOME T12), (T2, NONE))
   10.75 -  | factor_out_types T1 (Type ("*", [T21, T22])) = ((T1, NONE), (T21, SOME T22))
   10.76 +  | factor_out_types (Type (@{type_name "*"}, [T11, T12])) T2 =
   10.77 +    ((T11, SOME T12), (T2, NONE))
   10.78 +  | factor_out_types T1 (Type (@{type_name "*"}, [T21, T22])) =
   10.79 +    ((T1, NONE), (T21, SOME T22))
   10.80    | factor_out_types T1 T2 = ((T1, NONE), (T2, NONE))
   10.81  
   10.82  (* bool -> typ -> typ -> (term * term) list -> term *)
   10.83 @@ -188,10 +193,11 @@
   10.84      val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut
   10.85    in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end
   10.86  (* typ -> term -> term -> term *)
   10.87 -fun pair_up (Type ("*", [T1', T2']))
   10.88 +fun pair_up (Type (@{type_name "*"}, [T1', T2']))
   10.89              (t1 as Const (@{const_name Pair},
   10.90 -                          Type ("fun", [_, Type ("fun", [_, T1])])) $ t11 $ t12)
   10.91 -            t2 =
   10.92 +                          Type (@{type_name fun},
   10.93 +                                [_, Type (@{type_name fun}, [_, T1])]))
   10.94 +             $ t11 $ t12) t2 =
   10.95      if T1 = T1' then HOLogic.mk_prod (t1, t2)
   10.96      else HOLogic.mk_prod (t11, pair_up T2' t12 t2)
   10.97    | pair_up _ t1 t2 = HOLogic.mk_prod (t1, t2)
   10.98 @@ -199,7 +205,7 @@
   10.99  fun multi_pair_up T1 t1 (ts2, ts3) = map2 (pair o pair_up T1 t1) ts2 ts3
  10.100  
  10.101  (* typ -> typ -> typ -> term -> term *)
  10.102 -fun typecast_fun (Type ("fun", [T1', T2'])) T1 T2 t =
  10.103 +fun typecast_fun (Type (@{type_name fun}, [T1', T2'])) T1 T2 t =
  10.104      let
  10.105        (* typ -> typ -> typ -> typ -> term -> term *)
  10.106        fun do_curry T1 T1a T1b T2 t =
  10.107 @@ -238,9 +244,11 @@
  10.108            t |> do_arrow T1a' (T1b' --> T2') T1 T2 |> do_uncurry T1' T2'
  10.109          | _ => raise TYPE ("Nitpick_Model.typecast_fun.do_fun", [T1, T1'], [])
  10.110        (* typ -> typ -> term -> term *)
  10.111 -      and do_term (Type ("fun", [T1', T2'])) (Type ("fun", [T1, T2])) t =
  10.112 +      and do_term (Type (@{type_name fun}, [T1', T2']))
  10.113 +                  (Type (@{type_name fun}, [T1, T2])) t =
  10.114            do_fun T1' T2' T1 T2 t
  10.115 -        | do_term (T' as Type ("*", Ts' as [T1', T2'])) (Type ("*", [T1, T2]))
  10.116 +        | do_term (T' as Type (@{type_name "*"}, Ts' as [T1', T2']))
  10.117 +                  (Type (@{type_name "*"}, [T1, T2]))
  10.118                    (Const (@{const_name Pair}, _) $ t1 $ t2) =
  10.119            Const (@{const_name Pair}, Ts' ---> T')
  10.120            $ do_term T1' T1 t1 $ do_term T2' T2 t2
  10.121 @@ -257,7 +265,7 @@
  10.122    | truth_const_sort_key _ = "1"
  10.123  
  10.124  (* typ -> term list -> term *)
  10.125 -fun mk_tuple (Type ("*", [T1, T2])) ts =
  10.126 +fun mk_tuple (Type (@{type_name "*"}, [T1, T2])) ts =
  10.127      HOLogic.mk_prod (mk_tuple T1 ts,
  10.128          mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1))))
  10.129    | mk_tuple _ (t :: _) = t
  10.130 @@ -307,8 +315,8 @@
  10.131          else
  10.132            aux tps
  10.133        end
  10.134 -    (* typ -> typ -> typ -> (term * term) list -> term *)
  10.135 -    fun make_map T1 T2 T2' =
  10.136 +    (* bool -> typ -> typ -> typ -> (term * term) list -> term *)
  10.137 +    fun make_map maybe_opt T1 T2 T2' =
  10.138        let
  10.139          val update_const = Const (@{const_name fun_upd},
  10.140                                    (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
  10.141 @@ -319,7 +327,7 @@
  10.142                 Const (@{const_name None}, _) => aux' ps
  10.143               | _ => update_const $ aux' ps $ t1 $ t2)
  10.144          fun aux ps =
  10.145 -          if not (is_complete_type datatypes false T1) then
  10.146 +          if maybe_opt andalso not (is_complete_type datatypes false T1) then
  10.147              update_const $ aux' ps $ Const (unrep, T1)
  10.148              $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
  10.149            else
  10.150 @@ -328,7 +336,7 @@
  10.151      (* typ list -> term -> term *)
  10.152      fun polish_funs Ts t =
  10.153        (case fastype_of1 (Ts, t) of
  10.154 -         Type ("fun", [T1, T2]) =>
  10.155 +         Type (@{type_name fun}, [T1, T2]) =>
  10.156           if is_plain_fun t then
  10.157             case T2 of
  10.158               @{typ bool} =>
  10.159 @@ -341,9 +349,9 @@
  10.160               end
  10.161             | Type (@{type_name option}, [T2']) =>
  10.162               let
  10.163 -               val ts_pair = snd (dest_plain_fun t)
  10.164 -                             |> pairself (map (polish_funs Ts))
  10.165 -             in make_map T1 T2 T2' (rev (op ~~ ts_pair)) end
  10.166 +               val (maybe_opt, ts_pair) =
  10.167 +                 dest_plain_fun t ||> pairself (map (polish_funs Ts))
  10.168 +             in make_map maybe_opt T1 T2 T2' (rev (op ~~ ts_pair)) end
  10.169             | _ => raise SAME ()
  10.170           else
  10.171             raise SAME ()
  10.172 @@ -356,7 +364,7 @@
  10.173                 else polish_funs Ts t1 $ polish_funs Ts t2
  10.174               | t1 $ t2 => polish_funs Ts t1 $ polish_funs Ts t2
  10.175               | Abs (s, T, t') => Abs (s, T, polish_funs (T :: Ts) t')
  10.176 -             | Const (s, Type ("fun", [T1, T2])) =>
  10.177 +             | Const (s, Type (@{type_name fun}, [T1, T2])) =>
  10.178                 if s = opt_flag orelse s = non_opt_flag then
  10.179                   Abs ("x", T1, Const (unknown, T2))
  10.180                 else
  10.181 @@ -366,24 +374,24 @@
  10.182      fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
  10.183        ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
  10.184                   |> make_plain_fun maybe_opt T1 T2
  10.185 -                 |> unarize_and_unbox_term
  10.186 -                 |> typecast_fun (unarize_unbox_and_uniterize_type T')
  10.187 -                                 (unarize_unbox_and_uniterize_type T1)
  10.188 -                                 (unarize_unbox_and_uniterize_type T2)
  10.189 +                 |> unarize_unbox_etc_term
  10.190 +                 |> typecast_fun (uniterize_unarize_unbox_etc_type T')
  10.191 +                                 (uniterize_unarize_unbox_etc_type T1)
  10.192 +                                 (uniterize_unarize_unbox_etc_type T2)
  10.193      (* (typ * int) list -> typ -> typ -> int -> term *)
  10.194 -    fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j _ =
  10.195 +    fun term_for_atom seen (T as Type (@{type_name fun}, [T1, T2])) T' j _ =
  10.196          let
  10.197            val k1 = card_of_type card_assigns T1
  10.198            val k2 = card_of_type card_assigns T2
  10.199          in
  10.200 -          term_for_rep seen T T' (Vect (k1, Atom (k2, 0)))
  10.201 +          term_for_rep true seen T T' (Vect (k1, Atom (k2, 0)))
  10.202                         [nth_combination (replicate k1 (k2, 0)) j]
  10.203            handle General.Subscript =>
  10.204                   raise ARG ("Nitpick_Model.reconstruct_term.term_for_atom",
  10.205                              signed_string_of_int j ^ " for " ^
  10.206                              string_for_rep (Vect (k1, Atom (k2, 0))))
  10.207          end
  10.208 -      | term_for_atom seen (Type ("*", [T1, T2])) _ j k =
  10.209 +      | term_for_atom seen (Type (@{type_name "*"}, [T1, T2])) _ j k =
  10.210          let
  10.211            val k1 = card_of_type card_assigns T1
  10.212            val k2 = k div k1
  10.213 @@ -461,8 +469,9 @@
  10.214                    if length arg_Ts = 0 then
  10.215                      []
  10.216                    else
  10.217 -                    map3 (fn Ts => term_for_rep seen Ts Ts) arg_Ts arg_Rs
  10.218 -                         arg_jsss
  10.219 +                    map3 (fn Ts =>
  10.220 +                             term_for_rep (constr_s <> @{const_name FinFun})
  10.221 +                                          seen Ts Ts) arg_Ts arg_Rs arg_jsss
  10.222                      |> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts)
  10.223                      |> dest_n_tuple (length uncur_arg_Ts)
  10.224                  val t =
  10.225 @@ -519,50 +528,54 @@
  10.226      and term_for_vect seen k R T1 T2 T' js =
  10.227        make_fun true T1 T2 T'
  10.228                 (map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k))
  10.229 -               (map (term_for_rep seen T2 T2 R o single)
  10.230 +               (map (term_for_rep true seen T2 T2 R o single)
  10.231                      (batch_list (arity_of_rep R) js))
  10.232 -    (* (typ * int) list -> typ -> typ -> rep -> int list list -> term *)
  10.233 -    and term_for_rep seen T T' Unit [[]] = term_for_atom seen T T' 0 1
  10.234 -      | term_for_rep seen T T' (R as Atom (k, j0)) [[j]] =
  10.235 +    (* bool -> (typ * int) list -> typ -> typ -> rep -> int list list -> term *)
  10.236 +    and term_for_rep _ seen T T' Unit [[]] = term_for_atom seen T T' 0 1
  10.237 +      | term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] =
  10.238          if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k
  10.239          else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R])
  10.240 -      | term_for_rep seen (Type ("*", [T1, T2])) _ (Struct [R1, R2]) [js] =
  10.241 +      | term_for_rep _ seen (Type (@{type_name "*"}, [T1, T2])) _
  10.242 +                     (Struct [R1, R2]) [js] =
  10.243          let
  10.244            val arity1 = arity_of_rep R1
  10.245            val (js1, js2) = chop arity1 js
  10.246          in
  10.247            list_comb (HOLogic.pair_const T1 T2,
  10.248 -                     map3 (fn T => term_for_rep seen T T) [T1, T2] [R1, R2]
  10.249 +                     map3 (fn T => term_for_rep true seen T T) [T1, T2] [R1, R2]
  10.250                            [[js1], [js2]])
  10.251          end
  10.252 -      | term_for_rep seen (Type ("fun", [T1, T2])) T' (Vect (k, R')) [js] =
  10.253 +      | term_for_rep _ seen (Type (@{type_name fun}, [T1, T2])) T'
  10.254 +                     (Vect (k, R')) [js] =
  10.255          term_for_vect seen k R' T1 T2 T' js
  10.256 -      | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, Formula Neut))
  10.257 -                     jss =
  10.258 +      | term_for_rep _ seen (Type (@{type_name fun}, [T1, T2])) T'
  10.259 +                     (Func (R1, Formula Neut)) jss =
  10.260          let
  10.261            val jss1 = all_combinations_for_rep R1
  10.262 -          val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1
  10.263 +          val ts1 = map (term_for_rep true seen T1 T1 R1 o single) jss1
  10.264            val ts2 =
  10.265 -            map (fn js => term_for_rep seen T2 T2 (Atom (2, 0))
  10.266 +            map (fn js => term_for_rep true seen T2 T2 (Atom (2, 0))
  10.267                                         [[int_from_bool (member (op =) jss js)]])
  10.268                  jss1
  10.269          in make_fun false T1 T2 T' ts1 ts2 end
  10.270 -      | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, R2)) jss =
  10.271 +      | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T'
  10.272 +                     (Func (R1, R2)) jss =
  10.273          let
  10.274            val arity1 = arity_of_rep R1
  10.275            val jss1 = all_combinations_for_rep R1
  10.276 -          val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1
  10.277 +          val ts1 = map (term_for_rep false seen T1 T1 R1 o single) jss1
  10.278            val grouped_jss2 = AList.group (op =) (map (chop arity1) jss)
  10.279 -          val ts2 = map (term_for_rep seen T2 T2 R2 o the_default []
  10.280 +          val ts2 = map (term_for_rep false seen T2 T2 R2 o the_default []
  10.281                           o AList.lookup (op =) grouped_jss2) jss1
  10.282 -        in make_fun true T1 T2 T' ts1 ts2 end
  10.283 -      | term_for_rep seen T T' (Opt R) jss =
  10.284 -        if null jss then Const (unknown, T) else term_for_rep seen T T' R jss
  10.285 -      | term_for_rep _ T _ R jss =
  10.286 +        in make_fun maybe_opt T1 T2 T' ts1 ts2 end
  10.287 +      | term_for_rep _ seen T T' (Opt R) jss =
  10.288 +        if null jss then Const (unknown, T)
  10.289 +        else term_for_rep true seen T T' R jss
  10.290 +      | term_for_rep _ _ T _ R jss =
  10.291          raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
  10.292                     Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
  10.293                     string_of_int (length jss))
  10.294 -  in polish_funs [] o unarize_and_unbox_term oooo term_for_rep [] end
  10.295 +  in polish_funs [] o unarize_unbox_etc_term oooo term_for_rep true [] end
  10.296  
  10.297  (* atom_pool -> scope -> nut list -> nut NameTable.table -> KK.raw_bound list
  10.298     -> nut -> term *)
  10.299 @@ -689,7 +702,7 @@
  10.300          val (oper, (t1, T'), T) =
  10.301            case name of
  10.302              FreeName (s, T, _) =>
  10.303 -            let val t = Free (s, unarize_unbox_and_uniterize_type T) in
  10.304 +            let val t = Free (s, uniterize_unarize_unbox_etc_type T) in
  10.305                ("=", (t, format_term_type thy def_table formats t), T)
  10.306              end
  10.307            | ConstName (s, T, _) =>
  10.308 @@ -710,12 +723,17 @@
  10.309      (* dtype_spec -> Pretty.T *)
  10.310      fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
  10.311        Pretty.block (Pretty.breaks
  10.312 -          [Syntax.pretty_typ ctxt (unarize_unbox_and_uniterize_type typ),
  10.313 -           Pretty.str "=",
  10.314 -           Pretty.enum "," "{" "}"
  10.315 -               (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
  10.316 -                (if fun_from_pair complete false then []
  10.317 -                 else [Pretty.str unrep]))])
  10.318 +          (Syntax.pretty_typ ctxt (uniterize_unarize_unbox_etc_type typ) ::
  10.319 +           (case typ of
  10.320 +              Type (@{type_name fin_fun}, _) => [Pretty.str "[finite]"]
  10.321 +            | Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"]
  10.322 +            | Type (@{type_name pair_box}, _) => [Pretty.str "[boxed]"]
  10.323 +            | _ => []) @
  10.324 +           [Pretty.str "=",
  10.325 +            Pretty.enum "," "{" "}"
  10.326 +                (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
  10.327 +                 (if fun_from_pair complete false then []
  10.328 +                  else [Pretty.str unrep]))]))
  10.329      (* typ -> dtype_spec list *)
  10.330      fun integer_datatype T =
  10.331        [{typ = T, card = card_of_type card_assigns T, co = false,
  10.332 @@ -752,13 +770,14 @@
  10.333      val (eval_names, noneval_nonskolem_nonsel_names) =
  10.334        List.partition (String.isPrefix eval_prefix o nickname_of)
  10.335                       nonskolem_nonsel_names
  10.336 -      ||> filter_out (curry (op =) @{const_name bisim_iterator_max}
  10.337 +      ||> filter_out (member (op =) [@{const_name bisim},
  10.338 +                                     @{const_name bisim_iterator_max}]
  10.339                        o nickname_of)
  10.340      val free_names =
  10.341        map (fn x as (s, T) =>
  10.342                case filter (curry (op =) x
  10.343                         o pairf nickname_of
  10.344 -                               (unarize_unbox_and_uniterize_type o type_of))
  10.345 +                               (uniterize_unarize_unbox_etc_type o type_of))
  10.346                         free_names of
  10.347                  [name] => name
  10.348                | [] => FreeName (s, T, Any)
    11.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Mar 08 15:20:40 2010 -0800
    11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Mar 09 09:25:23 2010 +0100
    11.3 @@ -11,6 +11,9 @@
    11.4  
    11.5    val formulas_monotonic :
    11.6      hol_context -> bool -> typ -> term list * term list -> bool
    11.7 +  val finitize_funs :
    11.8 +    hol_context -> bool -> (typ option * bool option) list -> typ
    11.9 +    -> term list * term list -> term list * term list
   11.10  end;
   11.11  
   11.12  structure Nitpick_Mono : NITPICK_MONO =
   11.13 @@ -42,14 +45,17 @@
   11.14    {hol_ctxt: hol_context,
   11.15     binarize: bool,
   11.16     alpha_T: typ,
   11.17 +   no_harmless: bool,
   11.18     max_fresh: int Unsynchronized.ref,
   11.19 -   datatype_cache: ((string * typ list) * mtyp) list Unsynchronized.ref,
   11.20 -   constr_cache: (styp * mtyp) list Unsynchronized.ref}
   11.21 +   datatype_mcache: ((string * typ list) * mtyp) list Unsynchronized.ref,
   11.22 +   constr_mcache: (styp * mtyp) list Unsynchronized.ref}
   11.23  
   11.24 -exception MTYPE of string * mtyp list
   11.25 +exception MTYPE of string * mtyp list * typ list
   11.26 +exception MTERM of string * mterm list
   11.27  
   11.28  (* string -> unit *)
   11.29  fun print_g (_ : string) = ()
   11.30 +(* val print_g = tracing *)
   11.31  
   11.32  (* var -> string *)
   11.33  val string_for_var = signed_string_of_int
   11.34 @@ -70,7 +76,7 @@
   11.35  
   11.36  (* sign_atom -> string *)
   11.37  fun string_for_sign_atom (S sn) = string_for_sign sn
   11.38 -  | string_for_sign_atom (V j) = string_for_var j
   11.39 +  | string_for_sign_atom (V x) = string_for_var x
   11.40  
   11.41  (* literal -> string *)
   11.42  fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn
   11.43 @@ -83,7 +89,7 @@
   11.44    | is_MRec _ = false
   11.45  (* mtyp -> mtyp * sign_atom * mtyp *)
   11.46  fun dest_MFun (MFun z) = z
   11.47 -  | dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M])
   11.48 +  | dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M], [])
   11.49  
   11.50  val no_prec = 100
   11.51  
   11.52 @@ -157,13 +163,18 @@
   11.53    | mtype_of_mterm (MApp (m1, _)) =
   11.54      case mtype_of_mterm m1 of
   11.55        MFun (_, _, M12) => M12
   11.56 -    | M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1])
   11.57 +    | M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1], [])
   11.58 +
   11.59 +(* mterm -> mterm * mterm list *)
   11.60 +fun strip_mcomb (MApp (m1, m2)) = strip_mcomb m1 ||> (fn ms => append ms [m2])
   11.61 +  | strip_mcomb m = (m, [])
   11.62  
   11.63 -(* hol_context -> bool -> typ -> mdata *)
   11.64 -fun initial_mdata hol_ctxt binarize alpha_T =
   11.65 +(* hol_context -> bool -> bool -> typ -> mdata *)
   11.66 +fun initial_mdata hol_ctxt binarize no_harmless alpha_T =
   11.67    ({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
   11.68 -    max_fresh = Unsynchronized.ref 0, datatype_cache = Unsynchronized.ref [],
   11.69 -    constr_cache = Unsynchronized.ref []} : mdata)
   11.70 +    no_harmless = no_harmless, max_fresh = Unsynchronized.ref 0,
   11.71 +    datatype_mcache = Unsynchronized.ref [],
   11.72 +    constr_mcache = Unsynchronized.ref []} : mdata)
   11.73  
   11.74  (* typ -> typ -> bool *)
   11.75  fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
   11.76 @@ -215,7 +226,7 @@
   11.77             else repair_mtype cache (M :: seen) M
   11.78  
   11.79  (* ((string * typ list) * mtyp) list Unsynchronized.ref -> unit *)
   11.80 -fun repair_datatype_cache cache =
   11.81 +fun repair_datatype_mcache cache =
   11.82    let
   11.83      (* (string * typ list) * mtyp -> unit *)
   11.84      fun repair_one (z, M) =
   11.85 @@ -224,20 +235,41 @@
   11.86    in List.app repair_one (rev (!cache)) end
   11.87  
   11.88  (* (typ * mtyp) list -> (styp * mtyp) list Unsynchronized.ref -> unit *)
   11.89 -fun repair_constr_cache dtype_cache constr_cache =
   11.90 +fun repair_constr_mcache dtype_cache constr_mcache =
   11.91    let
   11.92      (* styp * mtyp -> unit *)
   11.93      fun repair_one (x, M) =
   11.94 -      Unsynchronized.change constr_cache
   11.95 +      Unsynchronized.change constr_mcache
   11.96            (AList.update (op =) (x, repair_mtype dtype_cache [] M))
   11.97 -  in List.app repair_one (!constr_cache) end
   11.98 +  in List.app repair_one (!constr_mcache) end
   11.99 +
  11.100 +(* typ -> bool *)
  11.101 +fun is_fin_fun_supported_type @{typ prop} = true
  11.102 +  | is_fin_fun_supported_type @{typ bool} = true
  11.103 +  | is_fin_fun_supported_type (Type (@{type_name option}, _)) = true
  11.104 +  | is_fin_fun_supported_type _ = false
  11.105 +(* typ -> typ -> term -> term option *)
  11.106 +fun fin_fun_body _ _ (t as @{term False}) = SOME t
  11.107 +  | fin_fun_body _ _ (t as Const (@{const_name None}, _)) = SOME t
  11.108 +  | fin_fun_body dom_T ran_T
  11.109 +                 ((t0 as Const (@{const_name If}, _))
  11.110 +                  $ (t1 as Const (@{const_name "op ="}, _) $ Bound 0 $ t1')
  11.111 +                  $ t2 $ t3) =
  11.112 +    (if loose_bvar1 (t1', 0) then
  11.113 +       NONE
  11.114 +     else case fin_fun_body dom_T ran_T t3 of
  11.115 +       NONE => NONE
  11.116 +     | SOME t3 =>
  11.117 +       SOME (t0 $ (Const (@{const_name is_unknown}, dom_T --> bool_T) $ t1')
  11.118 +                $ (Const (@{const_name unknown}, ran_T)) $ (t0 $ t1 $ t2 $ t3)))
  11.119 +  | fin_fun_body _ _ _ = NONE
  11.120  
  11.121  (* mdata -> typ -> typ -> mtyp * sign_atom * mtyp *)
  11.122  fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) T1 T2 =
  11.123    let
  11.124      val M1 = fresh_mtype_for_type mdata T1
  11.125      val M2 = fresh_mtype_for_type mdata T2
  11.126 -    val a = if is_boolean_type (body_type T2) andalso
  11.127 +    val a = if is_fin_fun_supported_type (body_type T2) andalso
  11.128                 exists_alpha_sub_mtype_fresh M1 then
  11.129                V (Unsynchronized.inc max_fresh)
  11.130              else
  11.131 @@ -245,25 +277,23 @@
  11.132    in (M1, a, M2) end
  11.133  (* mdata -> typ -> mtyp *)
  11.134  and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T,
  11.135 -                                    datatype_cache, constr_cache, ...}) =
  11.136 +                                    datatype_mcache, constr_mcache, ...}) =
  11.137    let
  11.138 -    (* typ -> typ -> mtyp *)
  11.139 -    val do_fun = MFun oo fresh_mfun_for_fun_type mdata
  11.140      (* typ -> mtyp *)
  11.141      fun do_type T =
  11.142        if T = alpha_T then
  11.143          MAlpha
  11.144        else case T of
  11.145 -        Type ("fun", [T1, T2]) => do_fun T1 T2
  11.146 -      | Type (@{type_name fun_box}, [T1, T2]) => do_fun T1 T2
  11.147 -      | Type ("*", [T1, T2]) => MPair (pairself do_type (T1, T2))
  11.148 +        Type (@{type_name fun}, [T1, T2]) =>
  11.149 +        MFun (fresh_mfun_for_fun_type mdata T1 T2)
  11.150 +      | Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2))
  11.151        | Type (z as (s, _)) =>
  11.152          if could_exist_alpha_sub_mtype thy alpha_T T then
  11.153 -          case AList.lookup (op =) (!datatype_cache) z of
  11.154 +          case AList.lookup (op =) (!datatype_mcache) z of
  11.155              SOME M => M
  11.156            | NONE =>
  11.157              let
  11.158 -              val _ = Unsynchronized.change datatype_cache (cons (z, MRec z))
  11.159 +              val _ = Unsynchronized.change datatype_mcache (cons (z, MRec z))
  11.160                val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
  11.161                val (all_Ms, constr_Ms) =
  11.162                  fold_rev (fn (_, T') => fn (all_Ms, constr_Ms) =>
  11.163 @@ -279,15 +309,15 @@
  11.164                               end)
  11.165                           xs ([], [])
  11.166                val M = MType (s, all_Ms)
  11.167 -              val _ = Unsynchronized.change datatype_cache
  11.168 +              val _ = Unsynchronized.change datatype_mcache
  11.169                            (AList.update (op =) (z, M))
  11.170 -              val _ = Unsynchronized.change constr_cache
  11.171 +              val _ = Unsynchronized.change constr_mcache
  11.172                            (append (xs ~~ constr_Ms))
  11.173              in
  11.174 -              if forall (not o is_MRec o snd) (!datatype_cache) then
  11.175 -                (repair_datatype_cache datatype_cache;
  11.176 -                 repair_constr_cache (!datatype_cache) constr_cache;
  11.177 -                 AList.lookup (op =) (!datatype_cache) z |> the)
  11.178 +              if forall (not o is_MRec o snd) (!datatype_mcache) then
  11.179 +                (repair_datatype_mcache datatype_mcache;
  11.180 +                 repair_constr_mcache (!datatype_mcache) constr_mcache;
  11.181 +                 AList.lookup (op =) (!datatype_mcache) z |> the)
  11.182                else
  11.183                  M
  11.184              end
  11.185 @@ -300,7 +330,7 @@
  11.186  fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
  11.187    | prodM_factors M = [M]
  11.188  (* mtyp -> mtyp list * mtyp *)
  11.189 -fun curried_strip_mtype (MFun (M1, S Minus, M2)) =
  11.190 +fun curried_strip_mtype (MFun (M1, _, M2)) =
  11.191      curried_strip_mtype M2 |>> append (prodM_factors M1)
  11.192    | curried_strip_mtype M = ([], M)
  11.193  (* string -> mtyp -> mtyp *)
  11.194 @@ -311,36 +341,34 @@
  11.195    end
  11.196  
  11.197  (* mdata -> styp -> mtyp *)
  11.198 -fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_cache,
  11.199 +fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_mcache,
  11.200                                  ...}) (x as (_, T)) =
  11.201    if could_exist_alpha_sub_mtype thy alpha_T T then
  11.202 -    case AList.lookup (op =) (!constr_cache) x of
  11.203 +    case AList.lookup (op =) (!constr_mcache) x of
  11.204        SOME M => M
  11.205      | NONE => if T = alpha_T then
  11.206                  let val M = fresh_mtype_for_type mdata T in
  11.207 -                  (Unsynchronized.change constr_cache (cons (x, M)); M)
  11.208 +                  (Unsynchronized.change constr_mcache (cons (x, M)); M)
  11.209                  end
  11.210                else
  11.211                  (fresh_mtype_for_type mdata (body_type T);
  11.212 -                 AList.lookup (op =) (!constr_cache) x |> the)
  11.213 +                 AList.lookup (op =) (!constr_mcache) x |> the)
  11.214    else
  11.215      fresh_mtype_for_type mdata T
  11.216  fun mtype_for_sel (mdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
  11.217    x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
  11.218      |> mtype_for_constr mdata |> sel_mtype_from_constr_mtype s
  11.219  
  11.220 +(* literal list -> sign_atom -> sign_atom *)
  11.221 +fun resolve_sign_atom lits (V x) =
  11.222 +    x |> AList.lookup (op =) lits |> Option.map S |> the_default (V x)
  11.223 +  | resolve_sign_atom _ a = a
  11.224  (* literal list -> mtyp -> mtyp *)
  11.225 -fun instantiate_mtype lits =
  11.226 +fun resolve_mtype lits =
  11.227    let
  11.228      (* mtyp -> mtyp *)
  11.229      fun aux MAlpha = MAlpha
  11.230 -      | aux (MFun (M1, V x, M2)) =
  11.231 -        let
  11.232 -          val a = case AList.lookup (op =) lits x of
  11.233 -                    SOME sn => S sn
  11.234 -                  | NONE => V x
  11.235 -        in MFun (aux M1, a, aux M2) end
  11.236 -      | aux (MFun (M1, a, M2)) = MFun (aux M1, a, aux M2)
  11.237 +      | aux (MFun (M1, a, M2)) = MFun (aux M1, resolve_sign_atom lits a, aux M2)
  11.238        | aux (MPair Mp) = MPair (pairself aux Mp)
  11.239        | aux (MType (s, Ms)) = MType (s, map aux Ms)
  11.240        | aux (MRec z) = MRec z
  11.241 @@ -417,11 +445,12 @@
  11.242                    accum =
  11.243      (accum |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)]
  11.244       handle Library.UnequalLengths =>
  11.245 -            raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2]))
  11.246 +            raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2], []))
  11.247    | do_mtype_comp _ _ (MType _) (MType _) accum =
  11.248      accum (* no need to compare them thanks to the cache *)
  11.249 -  | do_mtype_comp _ _ M1 M2 _ =
  11.250 -    raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2])
  11.251 +  | do_mtype_comp cmp _ M1 M2 _ =
  11.252 +    raise MTYPE ("Nitpick_Mono.do_mtype_comp (" ^ string_for_comp_op cmp ^ ")",
  11.253 +                 [M1, M2], [])
  11.254  
  11.255  (* comp_op -> mtyp -> mtyp -> constraint_set -> constraint_set *)
  11.256  fun add_mtype_comp _ _ _ UnsolvableCSet = UnsolvableCSet
  11.257 @@ -471,20 +500,20 @@
  11.258    | do_notin_mtype_fv sn sexp (MType (_, Ms)) accum =
  11.259      accum |> fold (do_notin_mtype_fv sn sexp) Ms
  11.260    | do_notin_mtype_fv _ _ M _ =
  11.261 -    raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M])
  11.262 +    raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], [])
  11.263  
  11.264  (* sign -> mtyp -> constraint_set -> constraint_set *)
  11.265  fun add_notin_mtype_fv _ _ UnsolvableCSet = UnsolvableCSet
  11.266    | add_notin_mtype_fv sn M (CSet (lits, comps, sexps)) =
  11.267 -    (print_g ("*** Add " ^ string_for_mtype M ^ " is right-" ^
  11.268 -              (case sn of Minus => "unique" | Plus => "total") ^ ".");
  11.269 +    (print_g ("*** Add " ^ string_for_mtype M ^ " is " ^
  11.270 +              (case sn of Minus => "concrete" | Plus => "complete") ^ ".");
  11.271       case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of
  11.272         NONE => (print_g "**** Unsolvable"; UnsolvableCSet)
  11.273       | SOME (lits, sexps) => CSet (lits, comps, sexps))
  11.274  
  11.275  (* mtyp -> constraint_set -> constraint_set *)
  11.276 -val add_mtype_is_right_unique = add_notin_mtype_fv Minus
  11.277 -val add_mtype_is_right_total = add_notin_mtype_fv Plus
  11.278 +val add_mtype_is_concrete = add_notin_mtype_fv Minus
  11.279 +val add_mtype_is_complete = add_notin_mtype_fv Plus
  11.280  
  11.281  val bool_from_minus = true
  11.282  
  11.283 @@ -574,34 +603,35 @@
  11.284  
  11.285  type mtype_schema = mtyp * constraint_set
  11.286  type mtype_context =
  11.287 -  {bounds: mtyp list,
  11.288 +  {bound_Ts: typ list,
  11.289 +   bound_Ms: mtyp list,
  11.290     frees: (styp * mtyp) list,
  11.291     consts: (styp * mtyp) list}
  11.292  
  11.293  type accumulator = mtype_context * constraint_set
  11.294  
  11.295 -val initial_gamma = {bounds = [], frees = [], consts = []}
  11.296 +val initial_gamma = {bound_Ts = [], bound_Ms = [], frees = [], consts = []}
  11.297  val unsolvable_accum = (initial_gamma, UnsolvableCSet)
  11.298  
  11.299 -(* mtyp -> mtype_context -> mtype_context *)
  11.300 -fun push_bound M {bounds, frees, consts} =
  11.301 -  {bounds = M :: bounds, frees = frees, consts = consts}
  11.302 +(* typ -> mtyp -> mtype_context -> mtype_context *)
  11.303 +fun push_bound T M {bound_Ts, bound_Ms, frees, consts} =
  11.304 +  {bound_Ts = T :: bound_Ts, bound_Ms = M :: bound_Ms, frees = frees,
  11.305 +   consts = consts}
  11.306  (* mtype_context -> mtype_context *)
  11.307 -fun pop_bound {bounds, frees, consts} =
  11.308 -  {bounds = tl bounds, frees = frees, consts = consts}
  11.309 -  handle List.Empty => initial_gamma
  11.310 +fun pop_bound {bound_Ts, bound_Ms, frees, consts} =
  11.311 +  {bound_Ts = tl bound_Ts, bound_Ms = tl bound_Ms, frees = frees,
  11.312 +   consts = consts}
  11.313 +  handle List.Empty => initial_gamma (* FIXME: needed? *)
  11.314  
  11.315  (* mdata -> term -> accumulator -> mterm * accumulator *)
  11.316  fun consider_term (mdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs,
  11.317 -                                         def_table, ...},
  11.318 +                                          def_table, ...},
  11.319                               alpha_T, max_fresh, ...}) =
  11.320    let
  11.321 -    (* typ -> typ -> mtyp * sign_atom * mtyp *)
  11.322 -    val mfun_for = fresh_mfun_for_fun_type mdata
  11.323      (* typ -> mtyp *)
  11.324      val mtype_for = fresh_mtype_for_type mdata
  11.325      (* mtyp -> mtyp *)
  11.326 -    fun pos_set_mtype_for_dom M =
  11.327 +    fun plus_set_mtype_for_dom M =
  11.328        MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M)
  11.329      (* typ -> accumulator -> mterm * accumulator *)
  11.330      fun do_all T (gamma, cset) =
  11.331 @@ -610,13 +640,13 @@
  11.332          val body_M = mtype_for (body_type T)
  11.333        in
  11.334          (MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M),
  11.335 -         (gamma, cset |> add_mtype_is_right_total abs_M))
  11.336 +         (gamma, cset |> add_mtype_is_complete abs_M))
  11.337        end
  11.338      fun do_equals T (gamma, cset) =
  11.339        let val M = mtype_for (domain_type T) in
  11.340          (MFun (M, S Minus, MFun (M, V (Unsynchronized.inc max_fresh),
  11.341                                   mtype_for (nth_range_type 2 T))),
  11.342 -         (gamma, cset |> add_mtype_is_right_unique M))
  11.343 +         (gamma, cset |> add_mtype_is_concrete M))
  11.344        end
  11.345      fun do_robust_set_operation T (gamma, cset) =
  11.346        let
  11.347 @@ -633,25 +663,25 @@
  11.348          val set_T = domain_type T
  11.349          val set_M = mtype_for set_T
  11.350          (* typ -> mtyp *)
  11.351 -        fun custom_mtype_for (T as Type ("fun", [T1, T2])) =
  11.352 +        fun custom_mtype_for (T as Type (@{type_name fun}, [T1, T2])) =
  11.353              if T = set_T then set_M
  11.354              else MFun (custom_mtype_for T1, S Minus, custom_mtype_for T2)
  11.355            | custom_mtype_for T = mtype_for T
  11.356        in
  11.357 -        (custom_mtype_for T, (gamma, cset |> add_mtype_is_right_unique set_M))
  11.358 +        (custom_mtype_for T, (gamma, cset |> add_mtype_is_concrete set_M))
  11.359        end
  11.360      (* typ -> accumulator -> mtyp * accumulator *)
  11.361      fun do_pair_constr T accum =
  11.362        case mtype_for (nth_range_type 2 T) of
  11.363          M as MPair (a_M, b_M) =>
  11.364          (MFun (a_M, S Minus, MFun (b_M, S Minus, M)), accum)
  11.365 -      | M => raise MTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [M])
  11.366 +      | M => raise MTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [M], [])
  11.367      (* int -> typ -> accumulator -> mtyp * accumulator *)
  11.368      fun do_nth_pair_sel n T =
  11.369        case mtype_for (domain_type T) of
  11.370          M as MPair (a_M, b_M) =>
  11.371          pair (MFun (M, S Minus, if n = 0 then a_M else b_M))
  11.372 -      | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M])
  11.373 +      | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M], [])
  11.374      (* mtyp * accumulator *)
  11.375      val mtype_unsolvable = (dummy_M, unsolvable_accum)
  11.376      (* term -> mterm * accumulator *)
  11.377 @@ -661,8 +691,9 @@
  11.378      fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum =
  11.379        let
  11.380          val abs_M = mtype_for abs_T
  11.381 -        val (bound_m, accum) = accum |>> push_bound abs_M |> do_term bound_t
  11.382 -        val expected_bound_M = pos_set_mtype_for_dom abs_M
  11.383 +        val (bound_m, accum) =
  11.384 +          accum |>> push_bound abs_T abs_M |> do_term bound_t
  11.385 +        val expected_bound_M = plus_set_mtype_for_dom abs_M
  11.386          val (body_m, accum) =
  11.387            accum ||> add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m)
  11.388                  |> do_term body_t ||> apfst pop_bound
  11.389 @@ -678,7 +709,8 @@
  11.390        end
  11.391      (* term -> accumulator -> mterm * accumulator *)
  11.392      and do_term t (_, UnsolvableCSet) = mterm_unsolvable t
  11.393 -      | do_term t (accum as (gamma as {bounds, frees, consts}, cset)) =
  11.394 +      | do_term t (accum as (gamma as {bound_Ts, bound_Ms, frees, consts},
  11.395 +                             cset)) =
  11.396          (case t of
  11.397             Const (x as (s, T)) =>
  11.398             (case AList.lookup (op =) consts x of
  11.399 @@ -714,12 +746,12 @@
  11.400                  let
  11.401                    val set_T = domain_type (range_type T)
  11.402                    val M1 = mtype_for (domain_type set_T)
  11.403 -                  val M1' = pos_set_mtype_for_dom M1
  11.404 +                  val M1' = plus_set_mtype_for_dom M1
  11.405                    val M2 = mtype_for set_T
  11.406                    val M3 = mtype_for set_T
  11.407                  in
  11.408                    (MFun (M1, S Minus, MFun (M2, S Minus, M3)),
  11.409 -                   (gamma, cset |> add_mtype_is_right_unique M1
  11.410 +                   (gamma, cset |> add_mtype_is_concrete M1
  11.411                                  |> add_is_sub_mtype M1' M3
  11.412                                  |> add_is_sub_mtype M2 M3))
  11.413                  end
  11.414 @@ -738,7 +770,7 @@
  11.415                | @{const_name finite} =>
  11.416                  if is_finite_type hol_ctxt T then
  11.417                    let val M1 = mtype_for (domain_type (domain_type T)) in
  11.418 -                    (MFun (pos_set_mtype_for_dom M1, S Minus, bool_M), accum)
  11.419 +                    (MFun (plus_set_mtype_for_dom M1, S Minus, bool_M), accum)
  11.420                    end
  11.421                  else
  11.422                    (print_g "*** finite"; mtype_unsolvable)
  11.423 @@ -761,8 +793,8 @@
  11.424                    val b_M = mtype_for (range_type (domain_type T))
  11.425                  in
  11.426                    (MFun (MFun (a_M, S Minus, b_M), S Minus,
  11.427 -                         MFun (pos_set_mtype_for_dom a_M, S Minus,
  11.428 -                               pos_set_mtype_for_dom b_M)), accum)
  11.429 +                         MFun (plus_set_mtype_for_dom a_M, S Minus,
  11.430 +                               plus_set_mtype_for_dom b_M)), accum)
  11.431                  end
  11.432                | @{const_name Sigma} =>
  11.433                  let
  11.434 @@ -784,12 +816,8 @@
  11.435                | @{const_name Tha} =>
  11.436                  let
  11.437                    val a_M = mtype_for (domain_type (domain_type T))
  11.438 -                  val a_set_M = pos_set_mtype_for_dom a_M
  11.439 +                  val a_set_M = plus_set_mtype_for_dom a_M
  11.440                  in (MFun (a_set_M, S Minus, a_M), accum) end
  11.441 -              | @{const_name FunBox} =>
  11.442 -                let val dom_M = mtype_for (domain_type T) in
  11.443 -                  (MFun (dom_M, S Minus, dom_M), accum)
  11.444 -                end
  11.445                | _ =>
  11.446                  if s = @{const_name minus_class.minus} andalso
  11.447                     is_set_type (domain_type T) then
  11.448 @@ -800,7 +828,7 @@
  11.449                    in
  11.450                      (MFun (left_set_M, S Minus,
  11.451                             MFun (right_set_M, S Minus, left_set_M)),
  11.452 -                     (gamma, cset |> add_mtype_is_right_unique right_set_M
  11.453 +                     (gamma, cset |> add_mtype_is_concrete right_set_M
  11.454                                    |> add_is_sub_mtype right_set_M left_set_M))
  11.455                    end
  11.456                  else if s = @{const_name ord_class.less_eq} andalso
  11.457 @@ -811,50 +839,54 @@
  11.458                          is_set_type (domain_type T) then
  11.459                    do_robust_set_operation T accum
  11.460                  else if is_sel s then
  11.461 -                  if constr_name_for_sel_like s = @{const_name FunBox} then
  11.462 -                    let val dom_M = mtype_for (domain_type T) in
  11.463 -                      (MFun (dom_M, S Minus, dom_M), accum)
  11.464 -                    end
  11.465 -                  else
  11.466 -                    (mtype_for_sel mdata x, accum)
  11.467 +                  (mtype_for_sel mdata x, accum)
  11.468                  else if is_constr thy stds x then
  11.469                    (mtype_for_constr mdata x, accum)
  11.470 -                else if is_built_in_const thy stds fast_descrs x then
  11.471 +                else if is_built_in_const thy stds fast_descrs x andalso
  11.472 +                        s <> @{const_name is_unknown} andalso
  11.473 +                        s <> @{const_name unknown} then
  11.474 +                  (* the "unknown" part is a hack *)
  11.475                    case def_of_const thy def_table x of
  11.476                      SOME t' => do_term t' accum |>> mtype_of_mterm
  11.477                    | NONE => (print_g ("*** built-in " ^ s); mtype_unsolvable)
  11.478                  else
  11.479                    let val M = mtype_for T in
  11.480 -                    (M, ({bounds = bounds, frees = frees,
  11.481 -                          consts = (x, M) :: consts}, cset))
  11.482 +                    (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
  11.483 +                          frees = frees, consts = (x, M) :: consts}, cset))
  11.484                    end) |>> curry MRaw t
  11.485           | Free (x as (_, T)) =>
  11.486             (case AList.lookup (op =) frees x of
  11.487                SOME M => (M, accum)
  11.488              | NONE =>
  11.489                let val M = mtype_for T in
  11.490 -                (M, ({bounds = bounds, frees = (x, M) :: frees,
  11.491 -                      consts = consts}, cset))
  11.492 +                (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
  11.493 +                      frees = (x, M) :: frees, consts = consts}, cset))
  11.494                end) |>> curry MRaw t
  11.495           | Var _ => (print_g "*** Var"; mterm_unsolvable t)
  11.496 -         | Bound j => (MRaw (t, nth bounds j), accum)
  11.497 -         | Abs (s, T, t' as @{const False}) =>
  11.498 -           let val (M1, a, M2) = mfun_for T bool_T in
  11.499 -             (MAbs (s, T, M1, a, MRaw (t', M2)), accum)
  11.500 -           end
  11.501 +         | Bound j => (MRaw (t, nth bound_Ms j), accum)
  11.502           | Abs (s, T, t') =>
  11.503 -           ((case t' of
  11.504 -               t1' $ Bound 0 =>
  11.505 -               if not (loose_bvar1 (t1', 0)) then
  11.506 -                 do_term (incr_boundvars ~1 t1') accum
  11.507 -               else
  11.508 -                 raise SAME ()
  11.509 -             | _ => raise SAME ())
  11.510 -            handle SAME () =>
  11.511 -                   let
  11.512 -                     val M = mtype_for T
  11.513 -                     val (m', accum) = do_term t' (accum |>> push_bound M)
  11.514 -                   in (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound) end)
  11.515 +           (case fin_fun_body T (fastype_of1 (T :: bound_Ts, t')) t' of
  11.516 +              SOME t' =>
  11.517 +              let
  11.518 +                val M = mtype_for T
  11.519 +                val a = V (Unsynchronized.inc max_fresh)
  11.520 +                val (m', accum) = do_term t' (accum |>> push_bound T M)
  11.521 +              in (MAbs (s, T, M, a, m'), accum |>> pop_bound) end
  11.522 +            | NONE =>
  11.523 +              ((case t' of
  11.524 +                  t1' $ Bound 0 =>
  11.525 +                  if not (loose_bvar1 (t1', 0)) then
  11.526 +                    do_term (incr_boundvars ~1 t1') accum
  11.527 +                  else
  11.528 +                    raise SAME ()
  11.529 +                | _ => raise SAME ())
  11.530 +               handle SAME () =>
  11.531 +                      let
  11.532 +                        val M = mtype_for T
  11.533 +                        val (m', accum) = do_term t' (accum |>> push_bound T M)
  11.534 +                      in
  11.535 +                        (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound)
  11.536 +                      end))
  11.537           | (t0 as Const (@{const_name All}, _))
  11.538             $ Abs (s', T', (t10 as @{const "op -->"}) $ (t11 $ Bound 0) $ t12) =>
  11.539             do_bounded_quantifier t0 s' T' t10 t11 t12 accum
  11.540 @@ -872,6 +904,8 @@
  11.541                 (_, UnsolvableCSet) => mterm_unsolvable t
  11.542               | _ =>
  11.543                 let
  11.544 +                 val T11 = domain_type (fastype_of1 (bound_Ts, t1))
  11.545 +                 val T2 = fastype_of1 (bound_Ts, t2)
  11.546                   val M11 = mtype_of_mterm m1 |> dest_MFun |> #1
  11.547                   val M2 = mtype_of_mterm m2
  11.548                 in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end
  11.549 @@ -880,18 +914,38 @@
  11.550                                        string_for_mterm ctxt m))
  11.551    in do_term end
  11.552  
  11.553 -(* mdata -> styp -> term -> term -> mterm * accumulator *)
  11.554 -fun consider_general_equals mdata (x as (_, T)) t1 t2 accum =
  11.555 +(*
  11.556 +    accum |> (case a of
  11.557 +                S Minus => accum 
  11.558 +              | S Plus => unsolvable_accum
  11.559 +              | V x => do_literal (x, Minus) lits)
  11.560 +*)
  11.561 +
  11.562 +(* int -> mtyp -> accumulator -> accumulator *)
  11.563 +fun force_minus_funs 0 _ = I
  11.564 +  | force_minus_funs n (M as MFun (M1, _, M2)) =
  11.565 +    add_mtypes_equal M (MFun (M1, S Minus, M2))
  11.566 +    #> force_minus_funs (n - 1) M2
  11.567 +  | force_minus_funs _ M =
  11.568 +    raise MTYPE ("Nitpick_Mono.force_minus_funs", [M], [])
  11.569 +(* mdata -> bool -> styp -> term -> term -> mterm * accumulator *)
  11.570 +fun consider_general_equals mdata def (x as (_, T)) t1 t2 accum =
  11.571    let
  11.572      val (m1, accum) = consider_term mdata t1 accum
  11.573      val (m2, accum) = consider_term mdata t2 accum
  11.574      val M1 = mtype_of_mterm m1
  11.575      val M2 = mtype_of_mterm m2
  11.576 +    val accum = accum ||> add_mtypes_equal M1 M2
  11.577      val body_M = fresh_mtype_for_type mdata (nth_range_type 2 T)
  11.578 +    val m = MApp (MApp (MRaw (Const x,
  11.579 +                MFun (M1, S Minus, MFun (M2, S Minus, body_M))), m1), m2)
  11.580    in
  11.581 -    (MApp (MApp (MRaw (Const x,
  11.582 -         MFun (M1, S Minus, MFun (M2, S Minus, body_M))), m1), m2),
  11.583 -     accum ||> add_mtypes_equal M1 M2)
  11.584 +    (m, if def then
  11.585 +          let val (head_m, arg_ms) = strip_mcomb m1 in
  11.586 +            accum ||> force_minus_funs (length arg_ms) (mtype_of_mterm head_m)
  11.587 +          end
  11.588 +        else
  11.589 +          accum)
  11.590    end
  11.591  
  11.592  (* mdata -> sign -> term -> accumulator -> mterm * accumulator *)
  11.593 @@ -912,11 +966,13 @@
  11.594                val abs_M = mtype_for abs_T
  11.595                val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
  11.596                val (body_m, accum) =
  11.597 -                accum ||> side_cond ? add_mtype_is_right_total abs_M
  11.598 -                      |>> push_bound abs_M |> do_formula sn body_t
  11.599 +                accum ||> side_cond ? add_mtype_is_complete abs_M
  11.600 +                      |>> push_bound abs_T abs_M |> do_formula sn body_t
  11.601                val body_M = mtype_of_mterm body_m
  11.602              in
  11.603 -              (MApp (MRaw (Const quant_x, MFun (abs_M, S Minus, body_M)),
  11.604 +              (MApp (MRaw (Const quant_x,
  11.605 +                           MFun (MFun (abs_M, S Minus, body_M), S Minus,
  11.606 +                                 body_M)),
  11.607                       MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
  11.608                 accum |>> pop_bound)
  11.609              end
  11.610 @@ -924,7 +980,7 @@
  11.611            fun do_equals x t1 t2 =
  11.612              case sn of
  11.613                Plus => do_term t accum
  11.614 -            | Minus => consider_general_equals mdata x t1 t2 accum
  11.615 +            | Minus => consider_general_equals mdata false x t1 t2 accum
  11.616          in
  11.617            case t of
  11.618              Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
  11.619 @@ -947,7 +1003,7 @@
  11.620              (case sn of
  11.621                 Plus => do_quantifier x0 s1 T1 t1'
  11.622               | Minus =>
  11.623 -               (* ### do elsewhere *)
  11.624 +               (* FIXME: Move elsewhere *)
  11.625                 do_term (@{const Not}
  11.626                          $ (HOLogic.eq_const (domain_type T0) $ t1
  11.627                             $ Abs (Name.uu, T1, @{const False}))) accum)
  11.628 @@ -981,23 +1037,24 @@
  11.629    [@{const_name ord_class.less}, @{const_name ord_class.less_eq}]
  11.630  val bounteous_consts = [@{const_name bisim}]
  11.631  
  11.632 -(* term -> bool *)
  11.633 -fun is_harmless_axiom ({thy, stds, fast_descrs, ...} : hol_context) t =
  11.634 -  Term.add_consts t []
  11.635 -  |> filter_out (is_built_in_const thy stds fast_descrs)
  11.636 -  |> (forall (member (op =) harmless_consts o original_name o fst)
  11.637 -      orf exists (member (op =) bounteous_consts o fst))
  11.638 +(* mdata -> term -> bool *)
  11.639 +fun is_harmless_axiom ({no_harmless = true, ...} : mdata) _ = false
  11.640 +  | is_harmless_axiom {hol_ctxt = {thy, stds, fast_descrs, ...}, ...} t =
  11.641 +    Term.add_consts t []
  11.642 +    |> filter_out (is_built_in_const thy stds fast_descrs)
  11.643 +    |> (forall (member (op =) harmless_consts o original_name o fst) orf
  11.644 +        exists (member (op =) bounteous_consts o fst))
  11.645  
  11.646  (* mdata -> term -> accumulator -> mterm * accumulator *)
  11.647 -fun consider_nondefinitional_axiom (mdata as {hol_ctxt, ...}) t =
  11.648 -  if is_harmless_axiom hol_ctxt t then pair (MRaw (t, dummy_M))
  11.649 +fun consider_nondefinitional_axiom mdata t =
  11.650 +  if is_harmless_axiom mdata t then pair (MRaw (t, dummy_M))
  11.651    else consider_general_formula mdata Plus t
  11.652  
  11.653  (* mdata -> term -> accumulator -> mterm * accumulator *)
  11.654 -fun consider_definitional_axiom (mdata as {hol_ctxt as {thy, ...}, ...}) t =
  11.655 +fun consider_definitional_axiom (mdata as {hol_ctxt = {thy, ...}, ...}) t =
  11.656    if not (is_constr_pattern_formula thy t) then
  11.657      consider_nondefinitional_axiom mdata t
  11.658 -  else if is_harmless_axiom hol_ctxt t then
  11.659 +  else if is_harmless_axiom mdata t then
  11.660      pair (MRaw (t, dummy_M))
  11.661    else
  11.662      let
  11.663 @@ -1010,10 +1067,11 @@
  11.664          let
  11.665            val abs_M = mtype_for abs_T
  11.666            val (body_m, accum) =
  11.667 -            accum |>> push_bound abs_M |> do_formula body_t
  11.668 +            accum |>> push_bound abs_T abs_M |> do_formula body_t
  11.669            val body_M = mtype_of_mterm body_m
  11.670          in
  11.671 -          (MApp (MRaw (quant_t, MFun (abs_M, S Minus, body_M)),
  11.672 +          (MApp (MRaw (quant_t,
  11.673 +                       MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M)),
  11.674                   MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
  11.675             accum |>> pop_bound)
  11.676          end
  11.677 @@ -1039,16 +1097,20 @@
  11.678            case t of
  11.679              (t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
  11.680              do_all t0 s1 T1 t1 accum
  11.681 -          | @{const Trueprop} $ t1 => do_formula t1 accum
  11.682 +          | @{const Trueprop} $ t1 =>
  11.683 +            let val (m1, accum) = do_formula t1 accum in
  11.684 +              (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
  11.685 +                     m1), accum)
  11.686 +            end
  11.687            | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 =>
  11.688 -            consider_general_equals mdata x t1 t2 accum
  11.689 +            consider_general_equals mdata true x t1 t2 accum
  11.690            | (t0 as @{const "==>"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
  11.691            | (t0 as @{const Pure.conjunction}) $ t1 $ t2 =>
  11.692              do_conjunction t0 t1 t2 accum
  11.693            | (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
  11.694              do_all t0 s0 T1 t1 accum
  11.695            | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
  11.696 -            consider_general_equals mdata x t1 t2 accum
  11.697 +            consider_general_equals mdata true x t1 t2 accum
  11.698            | (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
  11.699            | (t0 as @{const "op -->"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
  11.700            | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
  11.701 @@ -1057,8 +1119,7 @@
  11.702  
  11.703  (* Proof.context -> literal list -> term -> mtyp -> string *)
  11.704  fun string_for_mtype_of_term ctxt lits t M =
  11.705 -  Syntax.string_of_term ctxt t ^ " : " ^
  11.706 -  string_for_mtype (instantiate_mtype lits M)
  11.707 +  Syntax.string_of_term ctxt t ^ " : " ^ string_for_mtype (resolve_mtype lits M)
  11.708  
  11.709  (* theory -> literal list -> mtype_context -> unit *)
  11.710  fun print_mtype_context ctxt lits ({frees, consts, ...} : mtype_context) =
  11.711 @@ -1067,31 +1128,135 @@
  11.712    |> cat_lines |> print_g
  11.713  
  11.714  (* ('a -> 'b -> 'c * 'd) -> 'a -> 'c list * 'b -> 'c list * 'd *)
  11.715 -fun gather f t (ms, accum) =
  11.716 +fun amass f t (ms, accum) =
  11.717    let val (m, accum) = f t accum in (m :: ms, accum) end
  11.718  
  11.719 -(* hol_context -> bool -> typ -> term list * term list -> bool *)
  11.720 -fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T
  11.721 -                       (nondef_ts, def_ts) =
  11.722 +(* string -> bool -> hol_context -> bool -> typ -> term list * term list
  11.723 +   -> (literal list * (mterm list * mterm list) * (styp * mtyp) list) option *)
  11.724 +fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize alpha_T
  11.725 +          (nondef_ts, def_ts) =
  11.726    let
  11.727 -    val _ = print_g ("****** Monotonicity analysis: " ^
  11.728 +    val _ = print_g ("****** " ^ which ^ " analysis: " ^
  11.729                       string_for_mtype MAlpha ^ " is " ^
  11.730                       Syntax.string_of_typ ctxt alpha_T)
  11.731 -    val mdata as {max_fresh, constr_cache, ...} =
  11.732 -      initial_mdata hol_ctxt binarize alpha_T
  11.733 -
  11.734 +    val mdata as {max_fresh, constr_mcache, ...} =
  11.735 +      initial_mdata hol_ctxt binarize no_harmless alpha_T
  11.736      val accum = (initial_gamma, slack)
  11.737      val (nondef_ms, accum) =
  11.738 -      ([], accum) |> gather (consider_general_formula mdata Plus) (hd nondef_ts)
  11.739 -                  |> fold (gather (consider_nondefinitional_axiom mdata))
  11.740 +      ([], accum) |> amass (consider_general_formula mdata Plus) (hd nondef_ts)
  11.741 +                  |> fold (amass (consider_nondefinitional_axiom mdata))
  11.742                            (tl nondef_ts)
  11.743      val (def_ms, (gamma, cset)) =
  11.744 -      ([], accum) |> fold (gather (consider_definitional_axiom mdata)) def_ts
  11.745 +      ([], accum) |> fold (amass (consider_definitional_axiom mdata)) def_ts
  11.746    in
  11.747      case solve (!max_fresh) cset of
  11.748 -      SOME lits => (print_mtype_context ctxt lits gamma; true)
  11.749 -    | _ => false
  11.750 +      SOME lits => (print_mtype_context ctxt lits gamma;
  11.751 +                    SOME (lits, (nondef_ms, def_ms), !constr_mcache))
  11.752 +    | _ => NONE
  11.753    end
  11.754 -  handle MTYPE (loc, Ms) => raise BAD (loc, commas (map string_for_mtype Ms))
  11.755 +  handle MTYPE (loc, Ms, Ts) =>
  11.756 +         raise BAD (loc, commas (map string_for_mtype Ms @
  11.757 +                                 map (Syntax.string_of_typ ctxt) Ts))
  11.758 +       | MTERM (loc, ms) =>
  11.759 +         raise BAD (loc, commas (map (string_for_mterm ctxt) ms))
  11.760 +
  11.761 +(* hol_context -> bool -> typ -> term list * term list -> bool *)
  11.762 +val formulas_monotonic = is_some oooo infer "Monotonicity" false
  11.763 +
  11.764 +(* typ -> typ -> styp *)
  11.765 +fun fin_fun_constr T1 T2 =
  11.766 +  (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
  11.767 +
  11.768 +(* hol_context -> bool -> (typ option * bool option) list -> typ
  11.769 +   -> term list * term list -> term list * term list *)
  11.770 +fun finitize_funs (hol_ctxt as {thy, stds, fast_descrs, constr_cache, ...})
  11.771 +                  binarize finitizes alpha_T tsp =
  11.772 +  case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
  11.773 +    SOME (lits, msp, constr_mtypes) =>
  11.774 +    let
  11.775 +      (* typ -> sign_atom -> bool *)
  11.776 +      fun should_finitize T a =
  11.777 +        case triple_lookup (type_match thy) finitizes T of
  11.778 +          SOME (SOME false) => false
  11.779 +        | _ => resolve_sign_atom lits a = S Plus
  11.780 +      (* typ -> mtyp -> typ *)
  11.781 +      fun type_from_mtype T M =
  11.782 +        case (M, T) of
  11.783 +          (MAlpha, _) => T
  11.784 +        | (MFun (M1, a, M2), Type (@{type_name fun}, Ts)) =>
  11.785 +          Type (if should_finitize T a then @{type_name fin_fun}
  11.786 +                else @{type_name fun}, map2 type_from_mtype Ts [M1, M2])
  11.787 +        | (MPair (M1, M2), Type (@{type_name "*"}, Ts)) =>
  11.788 +          Type (@{type_name "*"}, map2 type_from_mtype Ts [M1, M2])
  11.789 +        | (MType _, _) => T
  11.790 +        | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype",
  11.791 +                            [M], [T])
  11.792 +      (* styp -> styp *)
  11.793 +      fun finitize_constr (x as (s, T)) =
  11.794 +        (s, case AList.lookup (op =) constr_mtypes x of
  11.795 +              SOME M => type_from_mtype T M
  11.796 +            | NONE => T)
  11.797 +      (* typ list -> mterm -> term *)
  11.798 +      fun term_from_mterm Ts m =
  11.799 +        case m of
  11.800 +          MRaw (t, M) =>
  11.801 +          let
  11.802 +            val T = fastype_of1 (Ts, t)
  11.803 +            val T' = type_from_mtype T M
  11.804 +          in
  11.805 +            case t of
  11.806 +              Const (x as (s, T)) =>
  11.807 +              if member (op =) [@{const_name "=="}, @{const_name "op ="}] s then
  11.808 +                Const (s, T')
  11.809 +              else if is_built_in_const thy stds fast_descrs x then
  11.810 +                coerce_term hol_ctxt Ts T' T t
  11.811 +              else if is_constr thy stds x then
  11.812 +                Const (finitize_constr x)
  11.813 +              else if is_sel s then
  11.814 +                let
  11.815 +                  val n = sel_no_from_name s
  11.816 +                  val x' = x |> binarized_and_boxed_constr_for_sel hol_ctxt
  11.817 +                                                                   binarize
  11.818 +                             |> finitize_constr
  11.819 +                  val x'' = binarized_and_boxed_nth_sel_for_constr hol_ctxt
  11.820 +                                                                   binarize x' n
  11.821 +                in Const x'' end
  11.822 +              else
  11.823 +                Const (s, T')
  11.824 +            | Free (s, T) => Free (s, type_from_mtype T M)
  11.825 +            | Bound _ => t
  11.826 +            | _ => raise MTERM ("Nitpick_Mono.finitize_funs.term_from_mterm",
  11.827 +                                [m])
  11.828 +          end
  11.829 +        | MAbs (s, T, M, a, m') =>
  11.830 +          let
  11.831 +            val T = type_from_mtype T M
  11.832 +            val t' = term_from_mterm (T :: Ts) m'
  11.833 +            val T' = fastype_of1 (T :: Ts, t')
  11.834 +          in
  11.835 +            Abs (s, T, t')
  11.836 +            |> should_finitize (T --> T') a
  11.837 +               ? construct_value thy stds (fin_fun_constr T T') o single
  11.838 +          end
  11.839 +        | MApp (m1, m2) =>
  11.840 +          let
  11.841 +            val (t1, t2) = pairself (term_from_mterm Ts) (m1, m2)
  11.842 +            val (T1, T2) = pairself (curry fastype_of1 Ts) (t1, t2)
  11.843 +            val (t1', T2') =
  11.844 +              case T1 of
  11.845 +                Type (s, [T11, T12]) => 
  11.846 +                (if s = @{type_name fin_fun} then
  11.847 +                   select_nth_constr_arg thy stds (fin_fun_constr T11 T12) t1 0
  11.848 +                                         (T11 --> T12)
  11.849 +                 else
  11.850 +                   t1, T11)
  11.851 +              | _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm",
  11.852 +                                 [T1], [])
  11.853 +          in betapply (t1', coerce_term hol_ctxt Ts T2' T2 t2) end
  11.854 +    in
  11.855 +      Unsynchronized.change constr_cache (map (apsnd (map finitize_constr)));
  11.856 +      pairself (map (term_from_mterm [])) msp
  11.857 +    end
  11.858 +  | NONE => tsp
  11.859  
  11.860  end;
    12.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Mar 08 15:20:40 2010 -0800
    12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Mar 09 09:25:23 2010 +0100
    12.3 @@ -287,8 +287,9 @@
    12.4         "Tuple " ^ Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^
    12.5         implode (map sub us)
    12.6       | Construct (us', T, R, us) =>
    12.7 -       "Construct " ^ implode (map sub us') ^ Syntax.string_of_typ ctxt T ^
    12.8 -       " " ^ string_for_rep R ^ " " ^ implode (map sub us)
    12.9 +       "Construct " ^ implode (map sub us') ^ " " ^
   12.10 +       Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^
   12.11 +       implode (map sub us)
   12.12       | BoundName (j, T, R, nick) =>
   12.13         "BoundName " ^ signed_string_of_int j ^ " " ^
   12.14         Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^ nick
   12.15 @@ -459,7 +460,8 @@
   12.16        (res_T, Const (@{const_name snd}, T --> res_T) $ t)
   12.17      end
   12.18  (* typ * term -> (typ * term) list *)
   12.19 -fun factorize (z as (Type ("*", _), _)) = maps factorize [mk_fst z, mk_snd z]
   12.20 +fun factorize (z as (Type (@{type_name "*"}, _), _)) =
   12.21 +    maps factorize [mk_fst z, mk_snd z]
   12.22    | factorize z = [z]
   12.23  
   12.24  (* hol_context -> op2 -> term -> nut *)
   12.25 @@ -623,7 +625,8 @@
   12.26            if is_built_in_const thy stds false x then Cst (Add, T, Any)
   12.27            else ConstName (s, T, Any)
   12.28          | (Const (@{const_name minus_class.minus},
   12.29 -                  Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
   12.30 +                  Type (@{type_name fun},
   12.31 +                        [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
   12.32             [t1, t2]) =>
   12.33            Op2 (SetDifference, T1, Any, sub t1, sub t2)
   12.34          | (Const (x as (s as @{const_name minus_class.minus}, T)), []) =>
   12.35 @@ -642,7 +645,8 @@
   12.36            else
   12.37              do_apply t0 ts
   12.38          | (Const (@{const_name ord_class.less_eq},
   12.39 -                  Type ("fun", [Type ("fun", [_, @{typ bool}]), _])),
   12.40 +                  Type (@{type_name fun},
   12.41 +                        [Type (@{type_name fun}, [_, @{typ bool}]), _])),
   12.42             [t1, t2]) =>
   12.43            Op2 (Subset, bool_T, Any, sub t1, sub t2)
   12.44          (* FIXME: find out if this case is necessary *)
   12.45 @@ -666,7 +670,7 @@
   12.46          | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
   12.47          | (Const (@{const_name is_unknown}, _), [t1]) =>
   12.48            Op1 (IsUnknown, bool_T, Any, sub t1)
   12.49 -        | (Const (@{const_name Tha}, Type ("fun", [_, T2])), [t1]) =>
   12.50 +        | (Const (@{const_name Tha}, Type (@{type_name fun}, [_, T2])), [t1]) =>
   12.51            Op1 (Tha, T2, Any, sub t1)
   12.52          | (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any)
   12.53          | (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any)
   12.54 @@ -676,11 +680,13 @@
   12.55                    T as @{typ "unsigned_bit word => signed_bit word"}), []) =>
   12.56            Cst (NatToInt, T, Any)
   12.57          | (Const (@{const_name semilattice_inf_class.inf},
   12.58 -                  Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
   12.59 +                  Type (@{type_name fun},
   12.60 +                        [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
   12.61             [t1, t2]) =>
   12.62            Op2 (Intersect, T1, Any, sub t1, sub t2)
   12.63          | (Const (@{const_name semilattice_sup_class.sup},
   12.64 -                  Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
   12.65 +                  Type (@{type_name fun},
   12.66 +                        [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
   12.67             [t1, t2]) =>
   12.68            Op2 (Union, T1, Any, sub t1, sub t2)
   12.69          | (t0 as Const (x as (s, T)), ts) =>
   12.70 @@ -956,7 +962,7 @@
   12.71                   if ok then Cst (Num j, T, Atom (k, j0))
   12.72                   else Cst (Unrep, T, Opt (Atom (k, j0)))
   12.73                 end)
   12.74 -        | Cst (Suc, T as Type ("fun", [T1, _]), _) =>
   12.75 +        | Cst (Suc, T as Type (@{type_name fun}, [T1, _]), _) =>
   12.76            let val R = Atom (spec_of_type scope T1) in
   12.77              Cst (Suc, T, Func (R, Opt R))
   12.78            end
   12.79 @@ -1306,12 +1312,13 @@
   12.80    in (w :: ws, pool, NameTable.update (v, w) table) end
   12.81  
   12.82  (* typ -> rep -> nut list -> nut *)
   12.83 -fun shape_tuple (T as Type ("*", [T1, T2])) (R as Struct [R1, R2]) us =
   12.84 +fun shape_tuple (T as Type (@{type_name "*"}, [T1, T2])) (R as Struct [R1, R2])
   12.85 +                us =
   12.86      let val arity1 = arity_of_rep R1 in
   12.87        Tuple (T, R, [shape_tuple T1 R1 (List.take (us, arity1)),
   12.88                      shape_tuple T2 R2 (List.drop (us, arity1))])
   12.89      end
   12.90 -  | shape_tuple (T as Type ("fun", [_, T2])) (R as Vect (k, R')) us =
   12.91 +  | shape_tuple (T as Type (@{type_name fun}, [_, T2])) (R as Vect (k, R')) us =
   12.92      Tuple (T, R, map (shape_tuple T2 R') (batch_list (length us div k) us))
   12.93    | shape_tuple T _ [u] =
   12.94      if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u])
    13.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Mar 08 15:20:40 2010 -0800
    13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Mar 09 09:25:23 2010 +0100
    13.3 @@ -9,7 +9,9 @@
    13.4  sig
    13.5    type hol_context = Nitpick_HOL.hol_context
    13.6    val preprocess_term :
    13.7 -    hol_context -> term -> term list * term list * bool * bool * bool
    13.8 +    hol_context -> (typ option * bool option) list
    13.9 +    -> (typ option * bool option) list -> term
   13.10 +    -> term list * term list * bool * bool * bool
   13.11  end
   13.12  
   13.13  structure Nitpick_Preproc : NITPICK_PREPROC =
   13.14 @@ -17,6 +19,7 @@
   13.15  
   13.16  open Nitpick_Util
   13.17  open Nitpick_HOL
   13.18 +open Nitpick_Mono
   13.19  
   13.20  (* polarity -> string -> bool *)
   13.21  fun is_positive_existential polar quant_s =
   13.22 @@ -115,88 +118,15 @@
   13.23  
   13.24  (** Boxing **)
   13.25  
   13.26 -(* hol_context -> typ -> term -> term *)
   13.27 -fun constr_expand (hol_ctxt as {thy, stds, ...}) T t =
   13.28 -  (case head_of t of
   13.29 -     Const x => if is_constr_like thy x then t else raise SAME ()
   13.30 -   | _ => raise SAME ())
   13.31 -  handle SAME () =>
   13.32 -         let
   13.33 -           val x' as (_, T') =
   13.34 -             if is_pair_type T then
   13.35 -               let val (T1, T2) = HOLogic.dest_prodT T in
   13.36 -                 (@{const_name Pair}, T1 --> T2 --> T)
   13.37 -               end
   13.38 -             else
   13.39 -               datatype_constrs hol_ctxt T |> hd
   13.40 -           val arg_Ts = binder_types T'
   13.41 -         in
   13.42 -           list_comb (Const x', map2 (select_nth_constr_arg thy stds x' t)
   13.43 -                                     (index_seq 0 (length arg_Ts)) arg_Ts)
   13.44 -         end
   13.45 -
   13.46 -(* (term -> term) -> int -> term -> term *)
   13.47 -fun coerce_bound_no f j t =
   13.48 -  case t of
   13.49 -    t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
   13.50 -  | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
   13.51 -  | Bound j' => if j' = j then f t else t
   13.52 -  | _ => t
   13.53 -(* hol_context -> typ -> typ -> term -> term *)
   13.54 -fun coerce_bound_0_in_term hol_ctxt new_T old_T =
   13.55 -  old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
   13.56 -(* hol_context -> typ list -> typ -> typ -> term -> term *)
   13.57 -and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t =
   13.58 -  if old_T = new_T then
   13.59 -    t
   13.60 -  else
   13.61 -    case (new_T, old_T) of
   13.62 -      (Type (new_s, new_Ts as [new_T1, new_T2]),
   13.63 -       Type ("fun", [old_T1, old_T2])) =>
   13.64 -      (case eta_expand Ts t 1 of
   13.65 -         Abs (s, _, t') =>
   13.66 -         Abs (s, new_T1,
   13.67 -              t' |> coerce_bound_0_in_term hol_ctxt new_T1 old_T1
   13.68 -                 |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)
   13.69 -         |> Envir.eta_contract
   13.70 -         |> new_s <> "fun"
   13.71 -            ? construct_value thy stds
   13.72 -                  (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
   13.73 -                  o single
   13.74 -       | t' => raise TERM ("Nitpick_Preproc.coerce_term", [t']))
   13.75 -    | (Type (new_s, new_Ts as [new_T1, new_T2]),
   13.76 -       Type (old_s, old_Ts as [old_T1, old_T2])) =>
   13.77 -      if old_s = @{type_name fun_box} orelse
   13.78 -         old_s = @{type_name pair_box} orelse old_s = "*" then
   13.79 -        case constr_expand hol_ctxt old_T t of
   13.80 -          Const (old_s, _) $ t1 =>
   13.81 -          if new_s = "fun" then
   13.82 -            coerce_term hol_ctxt Ts new_T (Type ("fun", old_Ts)) t1
   13.83 -          else
   13.84 -            construct_value thy stds
   13.85 -                (old_s, Type ("fun", new_Ts) --> new_T)
   13.86 -                [coerce_term hol_ctxt Ts (Type ("fun", new_Ts))
   13.87 -                             (Type ("fun", old_Ts)) t1]
   13.88 -        | Const _ $ t1 $ t2 =>
   13.89 -          construct_value thy stds
   13.90 -              (if new_s = "*" then @{const_name Pair}
   13.91 -               else @{const_name PairBox}, new_Ts ---> new_T)
   13.92 -              [coerce_term hol_ctxt Ts new_T1 old_T1 t1,
   13.93 -               coerce_term hol_ctxt Ts new_T2 old_T2 t2]
   13.94 -        | t' => raise TERM ("Nitpick_Preproc.coerce_term", [t'])
   13.95 -      else
   13.96 -        raise TYPE ("Nitpick_Preproc.coerce_term", [new_T, old_T], [t])
   13.97 -    | _ => raise TYPE ("Nitpick_Preproc.coerce_term", [new_T, old_T], [t])
   13.98 -
   13.99  (* hol_context -> bool -> term -> term *)
  13.100  fun box_fun_and_pair_in_term (hol_ctxt as {thy, stds, fast_descrs, ...}) def
  13.101                               orig_t =
  13.102    let
  13.103      (* typ -> typ *)
  13.104 -    fun box_relational_operator_type (Type ("fun", Ts)) =
  13.105 -        Type ("fun", map box_relational_operator_type Ts)
  13.106 -      | box_relational_operator_type (Type ("*", Ts)) =
  13.107 -        Type ("*", map (box_type hol_ctxt InPair) Ts)
  13.108 +    fun box_relational_operator_type (Type (@{type_name fun}, Ts)) =
  13.109 +        Type (@{type_name fun}, map box_relational_operator_type Ts)
  13.110 +      | box_relational_operator_type (Type (@{type_name "*"}, Ts)) =
  13.111 +        Type (@{type_name "*"}, map (box_type hol_ctxt InPair) Ts)
  13.112        | box_relational_operator_type T = T
  13.113      (* indexname * typ -> typ * term -> typ option list -> typ option list *)
  13.114      fun add_boxed_types_for_var (z as (_, T)) (T', t') =
  13.115 @@ -320,12 +250,13 @@
  13.116            val T2 = fastype_of1 (new_Ts, t2)
  13.117            val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
  13.118          in
  13.119 -          betapply (if s1 = "fun" then
  13.120 +          betapply (if s1 = @{type_name fun} then
  13.121                        t1
  13.122                      else
  13.123                        select_nth_constr_arg thy stds
  13.124 -                          (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
  13.125 -                          (Type ("fun", Ts1)), t2)
  13.126 +                          (@{const_name FunBox},
  13.127 +                           Type (@{type_name fun}, Ts1) --> T1) t1 0
  13.128 +                          (Type (@{type_name fun}, Ts1)), t2)
  13.129          end
  13.130        | t1 $ t2 =>
  13.131          let
  13.132 @@ -336,12 +267,13 @@
  13.133            val T2 = fastype_of1 (new_Ts, t2)
  13.134            val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
  13.135          in
  13.136 -          betapply (if s1 = "fun" then
  13.137 +          betapply (if s1 = @{type_name fun} then
  13.138                        t1
  13.139                      else
  13.140                        select_nth_constr_arg thy stds
  13.141 -                          (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
  13.142 -                          (Type ("fun", Ts1)), t2)
  13.143 +                          (@{const_name FunBox},
  13.144 +                           Type (@{type_name fun}, Ts1) --> T1) t1 0
  13.145 +                          (Type (@{type_name fun}, Ts1)), t2)
  13.146          end
  13.147        | Free (s, T) => Free (s, box_type hol_ctxt InExpr T)
  13.148        | Var (z as (x, T)) =>
  13.149 @@ -597,7 +529,7 @@
  13.150                 if pass1 then do_eq false t2 t1 else raise SAME ()
  13.151               else case t1 of
  13.152                 Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
  13.153 -             | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
  13.154 +             | Const (s, Type (@{type_name fun}, [T1, T2])) $ Bound j' =>
  13.155                 if j' = j andalso
  13.156                    s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
  13.157                   SOME (construct_value thy stds (@{const_name FunBox}, T2 --> T1)
  13.158 @@ -1141,8 +1073,8 @@
  13.159      (* int -> typ -> accumulator -> accumulator *)
  13.160      and add_axioms_for_type depth T =
  13.161        case T of
  13.162 -        Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts
  13.163 -      | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts
  13.164 +        Type (@{type_name fun}, Ts) => fold (add_axioms_for_type depth) Ts
  13.165 +      | Type (@{type_name "*"}, Ts) => fold (add_axioms_for_type depth) Ts
  13.166        | @{typ prop} => I
  13.167        | @{typ bool} => I
  13.168        | @{typ unit} => I
  13.169 @@ -1399,11 +1331,29 @@
  13.170               | _ => t
  13.171    in aux "" [] [] end
  13.172  
  13.173 +(** Inference of finite functions **)
  13.174 +
  13.175 +(* hol_context -> bool -> (typ option * bool option) list
  13.176 +   -> (typ option * bool option) list -> term list * term list
  13.177 +   -> term list * term list *)
  13.178 +fun finitize_all_types_of_funs (hol_ctxt as {thy, ...}) binarize finitizes monos
  13.179 +                               (nondef_ts, def_ts) =
  13.180 +  let
  13.181 +    val Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
  13.182 +             |> filter_out (fn Type (@{type_name fun_box}, _) => true
  13.183 +                             | T => is_small_finite_type hol_ctxt T orelse
  13.184 +                                    triple_lookup (type_match thy) monos T
  13.185 +                                    = SOME (SOME false))
  13.186 +  in fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts) end
  13.187 +
  13.188  (** Preprocessor entry point **)
  13.189  
  13.190 -(* hol_context -> term -> term list * term list * bool * bool * bool *)
  13.191 +(* hol_context -> (typ option * bool option) list
  13.192 +   -> (typ option * bool option) list -> term
  13.193 +   -> term list * term list * bool * bool * bool *)
  13.194  fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
  13.195 -                                  boxes, skolemize, uncurry, ...}) t =
  13.196 +                                  boxes, skolemize, uncurry, ...})
  13.197 +                    finitizes monos t =
  13.198    let
  13.199      val skolem_depth = if skolemize then 4 else ~1
  13.200      val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
  13.201 @@ -1442,6 +1392,9 @@
  13.202        #> Term.map_abs_vars shortest_name
  13.203      val nondef_ts = map (do_rest false) nondef_ts
  13.204      val def_ts = map (do_rest true) def_ts
  13.205 +    val (nondef_ts, def_ts) =
  13.206 +      finitize_all_types_of_funs hol_ctxt binarize finitizes monos
  13.207 +                                 (nondef_ts, def_ts)
  13.208    in
  13.209      (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms, binarize)
  13.210    end
    14.1 --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML	Mon Mar 08 15:20:40 2010 -0800
    14.2 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML	Tue Mar 09 09:25:23 2010 +0100
    14.3 @@ -158,9 +158,9 @@
    14.4    | smart_range_rep _ _ _ (Func (_, R2)) = R2
    14.5    | smart_range_rep ofs T ran_card (Opt R) =
    14.6      Opt (smart_range_rep ofs T ran_card R)
    14.7 -  | smart_range_rep ofs (Type ("fun", [_, T2])) _ (Atom (1, _)) =
    14.8 +  | smart_range_rep ofs (Type (@{type_name fun}, [_, T2])) _ (Atom (1, _)) =
    14.9      Atom (1, offset_of_type ofs T2)
   14.10 -  | smart_range_rep ofs (Type ("fun", [_, T2])) ran_card (Atom _) =
   14.11 +  | smart_range_rep ofs (Type (@{type_name fun}, [_, T2])) ran_card (Atom _) =
   14.12      Atom (ran_card (), offset_of_type ofs T2)
   14.13    | smart_range_rep _ _ _ R = raise REP ("Nitpick_Rep.smart_range_rep", [R])
   14.14  
   14.15 @@ -183,10 +183,10 @@
   14.16    | one_rep _ _ (Vect z) = Vect z
   14.17    | one_rep ofs T (Opt R) = one_rep ofs T R
   14.18    | one_rep ofs T R = Atom (card_of_rep R, offset_of_type ofs T)
   14.19 -fun optable_rep ofs (Type ("fun", [_, T2])) (Func (R1, R2)) =
   14.20 +fun optable_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) =
   14.21      Func (R1, optable_rep ofs T2 R2)
   14.22    | optable_rep ofs T R = one_rep ofs T R
   14.23 -fun opt_rep ofs (Type ("fun", [_, T2])) (Func (R1, R2)) =
   14.24 +fun opt_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) =
   14.25      Func (R1, opt_rep ofs T2 R2)
   14.26    | opt_rep ofs T R = Opt (optable_rep ofs T R)
   14.27  (* rep -> rep *)
   14.28 @@ -264,11 +264,11 @@
   14.29  
   14.30  (* scope -> typ -> rep *)
   14.31  fun best_one_rep_for_type (scope as {card_assigns, ...} : scope)
   14.32 -                          (Type ("fun", [T1, T2])) =
   14.33 +                          (Type (@{type_name fun}, [T1, T2])) =
   14.34      (case best_one_rep_for_type scope T2 of
   14.35         Unit => Unit
   14.36       | R2 => Vect (card_of_type card_assigns T1, R2))
   14.37 -  | best_one_rep_for_type scope (Type ("*", [T1, T2])) =
   14.38 +  | best_one_rep_for_type scope (Type (@{type_name "*"}, [T1, T2])) =
   14.39      (case (best_one_rep_for_type scope T1, best_one_rep_for_type scope T2) of
   14.40         (Unit, Unit) => Unit
   14.41       | (R1, R2) => Struct [R1, R2])
   14.42 @@ -284,12 +284,12 @@
   14.43  (* Datatypes are never represented by Unit, because it would confuse
   14.44     "nfa_transitions_for_ctor". *)
   14.45  (* scope -> typ -> rep *)
   14.46 -fun best_opt_set_rep_for_type scope (Type ("fun", [T1, T2])) =
   14.47 +fun best_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) =
   14.48      Func (best_one_rep_for_type scope T1, best_opt_set_rep_for_type scope T2)
   14.49    | best_opt_set_rep_for_type (scope as {ofs, ...}) T =
   14.50      opt_rep ofs T (best_one_rep_for_type scope T)
   14.51  fun best_non_opt_set_rep_for_type (scope as {ofs, ...})
   14.52 -                                  (Type ("fun", [T1, T2])) =
   14.53 +                                  (Type (@{type_name fun}, [T1, T2])) =
   14.54      (case (best_one_rep_for_type scope T1,
   14.55             best_non_opt_set_rep_for_type scope T2) of
   14.56         (_, Unit) => Unit
   14.57 @@ -302,7 +302,7 @@
   14.58    (if is_exact_type datatypes true T then best_non_opt_set_rep_for_type
   14.59     else best_opt_set_rep_for_type) scope T
   14.60  fun best_non_opt_symmetric_reps_for_fun_type (scope as {ofs, ...})
   14.61 -                                             (Type ("fun", [T1, T2])) =
   14.62 +                                           (Type (@{type_name fun}, [T1, T2])) =
   14.63      (optable_rep ofs T1 (best_one_rep_for_type scope T1),
   14.64       optable_rep ofs T2 (best_one_rep_for_type scope T2))
   14.65    | best_non_opt_symmetric_reps_for_fun_type _ T =
   14.66 @@ -325,11 +325,11 @@
   14.67  fun type_schema_of_rep _ (Formula _) = []
   14.68    | type_schema_of_rep _ Unit = []
   14.69    | type_schema_of_rep T (Atom _) = [T]
   14.70 -  | type_schema_of_rep (Type ("*", [T1, T2])) (Struct [R1, R2]) =
   14.71 +  | type_schema_of_rep (Type (@{type_name "*"}, [T1, T2])) (Struct [R1, R2]) =
   14.72      type_schema_of_reps [T1, T2] [R1, R2]
   14.73 -  | type_schema_of_rep (Type ("fun", [_, T2])) (Vect (k, R)) =
   14.74 +  | type_schema_of_rep (Type (@{type_name fun}, [_, T2])) (Vect (k, R)) =
   14.75      replicate_list k (type_schema_of_rep T2 R)
   14.76 -  | type_schema_of_rep (Type ("fun", [T1, T2])) (Func (R1, R2)) =
   14.77 +  | type_schema_of_rep (Type (@{type_name fun}, [T1, T2])) (Func (R1, R2)) =
   14.78      type_schema_of_rep T1 R1 @ type_schema_of_rep T2 R2
   14.79    | type_schema_of_rep T (Opt R) = type_schema_of_rep T R
   14.80    | type_schema_of_rep _ R = raise REP ("Nitpick_Rep.type_schema_of_rep", [R])
    15.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Mar 08 15:20:40 2010 -0800
    15.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Mar 09 09:25:23 2010 +0100
    15.3 @@ -106,22 +106,26 @@
    15.4      | NONE => constr_spec dtypes x
    15.5  
    15.6  (* dtype_spec list -> bool -> typ -> bool *)
    15.7 -fun is_complete_type dtypes facto (Type ("fun", [T1, T2])) =
    15.8 +fun is_complete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) =
    15.9      is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2
   15.10 -  | is_complete_type dtypes facto (Type ("*", Ts)) =
   15.11 +  | is_complete_type dtypes facto (Type (@{type_name fin_fun}, [T1, T2])) =
   15.12 +    is_exact_type dtypes facto T1 andalso is_complete_type dtypes facto T2
   15.13 +  | is_complete_type dtypes facto (Type (@{type_name "*"}, Ts)) =
   15.14      forall (is_complete_type dtypes facto) Ts
   15.15    | is_complete_type dtypes facto T =
   15.16      not (is_integer_like_type T) andalso not (is_bit_type T) andalso
   15.17      fun_from_pair (#complete (the (datatype_spec dtypes T))) facto
   15.18      handle Option.Option => true
   15.19 -and is_concrete_type dtypes facto (Type ("fun", [T1, T2])) =
   15.20 +and is_concrete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) =
   15.21      is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2
   15.22 -  | is_concrete_type dtypes facto (Type ("*", Ts)) =
   15.23 +  | is_concrete_type dtypes facto (Type (@{type_name fin_fun}, [_, T2])) =
   15.24 +    is_concrete_type dtypes facto T2
   15.25 +  | is_concrete_type dtypes facto (Type (@{type_name "*"}, Ts)) =
   15.26      forall (is_concrete_type dtypes facto) Ts
   15.27    | is_concrete_type dtypes facto T =
   15.28      fun_from_pair (#concrete (the (datatype_spec dtypes T))) facto
   15.29      handle Option.Option => true
   15.30 -fun is_exact_type dtypes facto =
   15.31 +and is_exact_type dtypes facto =
   15.32    is_complete_type dtypes facto andf is_concrete_type dtypes facto
   15.33  
   15.34  (* int Typtab.table -> typ -> int *)
   15.35 @@ -528,15 +532,15 @@
   15.36  
   15.37  (* theory -> typ list -> (typ option * int list) list
   15.38     -> (typ option * int list) list *)
   15.39 -fun repair_cards_assigns_wrt_boxing _ _ [] = []
   15.40 -  | repair_cards_assigns_wrt_boxing thy Ts ((SOME T, ks) :: cards_assigns) =
   15.41 +fun repair_cards_assigns_wrt_boxing_etc _ _ [] = []
   15.42 +  | repair_cards_assigns_wrt_boxing_etc thy Ts ((SOME T, ks) :: cards_assigns) =
   15.43      (if is_fun_type T orelse is_pair_type T then
   15.44 -       Ts |> filter (curry (type_match thy o swap) T o unarize_and_unbox_type)
   15.45 -          |> map (rpair ks o SOME)
   15.46 +       Ts |> filter (curry (type_match thy o swap) T) |> map (rpair ks o SOME)
   15.47       else
   15.48 -       [(SOME T, ks)]) @ repair_cards_assigns_wrt_boxing thy Ts cards_assigns
   15.49 -  | repair_cards_assigns_wrt_boxing thy Ts ((NONE, ks) :: cards_assigns) =
   15.50 -    (NONE, ks) :: repair_cards_assigns_wrt_boxing thy Ts cards_assigns
   15.51 +       [(SOME T, ks)]) @
   15.52 +       repair_cards_assigns_wrt_boxing_etc thy Ts cards_assigns
   15.53 +  | repair_cards_assigns_wrt_boxing_etc thy Ts ((NONE, ks) :: cards_assigns) =
   15.54 +    (NONE, ks) :: repair_cards_assigns_wrt_boxing_etc thy Ts cards_assigns
   15.55  
   15.56  val max_scopes = 4096
   15.57  val distinct_threshold = 512
   15.58 @@ -548,8 +552,8 @@
   15.59                 maxes_assigns iters_assigns bitss bisim_depths mono_Ts nonmono_Ts
   15.60                 deep_dataTs finitizable_dataTs =
   15.61    let
   15.62 -    val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts
   15.63 -                                                        cards_assigns
   15.64 +    val cards_assigns = repair_cards_assigns_wrt_boxing_etc thy mono_Ts
   15.65 +                                                            cards_assigns
   15.66      val blocks = blocks_for_types hol_ctxt binarize cards_assigns maxes_assigns
   15.67                                    iters_assigns bitss bisim_depths mono_Ts
   15.68                                    nonmono_Ts