# HG changeset patch
# User blanchet
# Date 1281340670 -7200
# Node ID 3b708c0877ba3960bf1a6413954b5b652597c05a
# Parent  1954191fc6cff5262be5c2e723f6083380919778# Parent  275064b5ebf95f906f5397733ab49f7e7cb3caff
merge

diff -r 275064b5ebf9 -r 3b708c0877ba doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Sun Aug 08 20:51:02 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Mon Aug 09 09:57:50 2010 +0200
@@ -1237,11 +1237,13 @@
 
 where \textit{xs} is of type $'a~\textit{list}$ and \textit{ys} is of type
 $'b~\textit{list}$. A priori, Nitpick would need to consider $1\,000$ scopes to
-exhaust the specification \textit{card}~= 1--10. However, our intuition tells us
-that any counterexample found with a small scope would still be a counterexample
-in a larger scope---by simply ignoring the fresh $'a$ and $'b$ values provided
-by the larger scope. Nitpick comes to the same conclusion after a careful
-inspection of the formula and the relevant definitions:
+exhaust the specification \textit{card}~= 1--10 (10 cardinalies for $'a$
+$\times$ 10 cardinalities for $'b$ $\times$ 10 cardinalities for the datatypes).
+However, our intuition tells us that any counterexample found with a small scope
+would still be a counterexample in a larger scope---by simply ignoring the fresh
+$'a$ and $'b$ values provided by the larger scope. Nitpick comes to the same
+conclusion after a careful inspection of the formula and the relevant
+definitions:
 
 \prew
 \textbf{nitpick}~[\textit{verbose}] \\[2\smallskipamount]
@@ -1312,10 +1314,11 @@
 As insinuated in \S\ref{natural-numbers-and-integers} and
 \S\ref{inductive-datatypes}, \textit{nat}, \textit{int}, and inductive datatypes
 are normally monotonic and treated as such. The same is true for record types,
-\textit{rat}, \textit{real}, and some \textbf{typedef}'d types. Thus, given the
+\textit{rat}, and \textit{real}. Thus, given the
 cardinality specification 1--10, a formula involving \textit{nat}, \textit{int},
 \textit{int~list}, \textit{rat}, and \textit{rat~list} will lead Nitpick to
-consider only 10~scopes instead of $10\,000$.
+consider only 10~scopes instead of $10\,000$. On the other hand,
+\textbf{typedef}s and quotient types are generally nonmonotonic.
 
 \subsection{Inductive Properties}
 \label{inductive-properties}
@@ -2788,7 +2791,7 @@
 
 \prew
 $\textbf{val}\,~\textit{register\_codatatype\_global\/} : {}$ \\
-$\hbox{}\quad\textit{typ} \rightarrow \textit{string} \rightarrow \textit{styp~list} \rightarrow \textit{theory} \rightarrow \textit{theory}$ \\
+$\hbox{}\quad\textit{typ} \rightarrow \textit{string} \rightarrow (\textit{string} \times \textit{typ})\;\textit{list} \rightarrow \textit{theory} \rightarrow \textit{theory}$ \\
 $\textbf{val}\,~\textit{unregister\_codatatype\_global\/} :\,
 \textit{typ} \rightarrow \textit{theory} \rightarrow \textit{theory}$
 \postw
@@ -2799,9 +2802,9 @@
 
 \prew
 $\textbf{setup}~\,\{{*}$ \\
-$\hbox{}\qquad\textit{Nitpick\_HOL.register\_codatatype\_global\/}~@\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}$ \\
-$\hbox{}\qquad\qquad @\{\antiq{const\_name}~ \textit{llist\_case}\}$ \\
-$\hbox{}\qquad\qquad (\textit{map}~\textit{dest\_Const}~[@\{\antiq{term}~\textit{LNil}\},\, @\{\antiq{term}~\textit{LCons}\}])$ \\
+$\hbox{}\quad\textit{Nitpick\_HOL.register\_codatatype\_global\/}~@\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}$ \\
+$\hbox{}\qquad\quad @\{\antiq{const\_name}~ \textit{llist\_case}\}$ \\
+$\hbox{}\qquad\quad (\textit{map}~\textit{dest\_Const}~[@\{\antiq{term}~\textit{LNil}\},\, @\{\antiq{term}~\textit{LCons}\}])$ \\
 ${*}\}$
 \postw
 
@@ -2815,7 +2818,7 @@
 
 \prew
 $\textbf{setup}~\,\{{*}$ \\
-$\hbox{}\qquad\textit{Nitpick\_HOL.unregister\_codatatype\_global\/}~@\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}$ \\
+$\hbox{}\quad\textit{Nitpick\_HOL.unregister\_codatatype\_global\/}~@\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}$ \\
 ${*}\}$
 \postw
 
diff -r 275064b5ebf9 -r 3b708c0877ba src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Aug 08 20:51:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Aug 09 09:57:50 2010 +0200
@@ -212,12 +212,11 @@
    predicate variable. Leaves other theorems unchanged. We simply instantiate
    the conclusion variable to False. (Cf. "transform_elim_term" in
    "ATP_Systems".) *)
-(* FIXME: test! *)
 fun transform_elim_term t =
   case Logic.strip_imp_concl t of
     @{const Trueprop} $ Var (z, @{typ bool}) =>
-    subst_Vars [(z, @{const True})] t
-  | Var (z, @{typ prop}) => subst_Vars [(z, @{prop True})] t
+    subst_Vars [(z, @{const False})] t
+  | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t
   | _ => t
 
 fun presimplify_term thy =
@@ -684,7 +683,6 @@
   let
     val (ctxt, (_, th)) = goal;
     val thy = ProofContext.theory_of ctxt
-    (* ### FIXME: (1) preprocessing for "if" etc. *)
     val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
     val the_axioms =
       case axioms of