--- a/src/Doc/Nitpick/document/root.tex Thu Sep 01 16:12:55 2016 +0200
+++ b/src/Doc/Nitpick/document/root.tex Thu Sep 01 16:13:46 2016 +0200
@@ -272,12 +272,12 @@
\hbox{}\qquad \textit{card}~$'a$~= 1; \\
\hbox{}\qquad \textit{card}~$'a$~= 2; \\
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
-\hbox{}\qquad \textit{card}~$'a$~= 10. \\[2\smallskipamount]
+\hbox{}\qquad \textit{card}~$'a$~= 10 \\[2\smallskipamount]
Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $A = \{a_2,\, a_3\}$ \\
\hbox{}\qquad\qquad $x = a_3$ \\[2\smallskipamount]
-Total time: 963 ms.
+Total time: 963 ms
\postw
Nitpick found a counterexample in which $'a$ has cardinality 3. (For
@@ -334,7 +334,7 @@
\prew
\textbf{nitpick} \\[2\smallskipamount]
-\slshape Nitpick found no counterexample.
+\slshape Nitpick found no counterexample
\postw
We can further increase our confidence in the formula by exhausting all
@@ -351,7 +351,7 @@
\prew
\textbf{sledgehammer} \\[2\smallskipamount]
{\slshape Sledgehammer: ``$e$'' on goal \\
-Try this: \textbf{by}~(\textit{metis~theI}) (42 ms).} \\
+Try this: \textbf{by}~(\textit{metis~theI}) (42 ms)} \\
\hbox{}\qquad\vdots \\[2\smallskipamount]
\textbf{by}~(\textit{metis~theI\/})
\postw
@@ -469,7 +469,7 @@
\textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
\textbf{nitpick} [\textit{card~nat}~= 50] \\[2\smallskipamount]
\slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported
-fragment. Only potentially spurious counterexamples may be found. \\[2\smallskipamount]
+fragment; only potentially spurious counterexamples may be found \\[2\smallskipamount]
Nitpick found a potentially spurious counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variable: \nopagebreak \\
\hbox{}\qquad\qquad $P = \textit{False}$
@@ -490,7 +490,7 @@
\textbf{lemma} ``$P~\textit{Suc\/}$'' \\
\textbf{nitpick} \\[2\smallskipamount]
\slshape
-Nitpick found no counterexample.
+Nitpick found no counterexample
\postw
On any finite set $N$, \textit{Suc} is a partial function; for example, if $N =
@@ -780,15 +780,16 @@
\prew
\textbf{lemma} ``$\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
\textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount]
-\slshape The inductive predicate ``\textit{even}'' was proved well-founded.
-Nitpick can compute it efficiently. \\[2\smallskipamount]
+\slshape The inductive predicate ``\textit{even}'' was proved well-founded;
+Nitpick can compute it efficiently \\[2\smallskipamount]
Trying 1 scope: \\
\hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount]
-Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported fragment. Only
-potentially spurious counterexamples may be found. \\[2\smallskipamount]
+Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported fragment; only
+potentially spurious counterexamples may be found \\[2\smallskipamount]
Nitpick found a potentially spurious counterexample for \textit{card nat}~= 50: \\[2\smallskipamount]
\hbox{}\qquad Empty assignment \\[2\smallskipamount]
-Nitpick could not find a better counterexample. It checked 1 of 1 scope. \\[2\smallskipamount]
+Nitpick could not find a better counterexample
+It checked 1 of 1 scope \\[2\smallskipamount]
Total time: 1.62 s.
\postw
@@ -827,15 +828,14 @@
\lnot\;\textit{even}'~n$'' \\
\textbf{nitpick}~[\textit{card nat}~= 10,\, \textit{verbose},\, \textit{show\_consts}] \\[2\smallskipamount]
\slshape
-The inductive predicate ``$\textit{even}'\!$'' could not be proved well-founded.
-Nitpick might need to unroll it. \\[2\smallskipamount]
+The inductive predicate ``$\textit{even}'\!$'' could not be proved well-founded; Nitpick might need to unroll it \\[2\smallskipamount]
Trying 6 scopes: \\
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 0; \\
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 1; \\
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2; \\
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 4; \\
\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 8; \\
-\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 9. \\[2\smallskipamount]
+\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 9 \\[2\smallskipamount]
Nitpick found a counterexample for \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2: \\[2\smallskipamount]
\hbox{}\qquad Constant: \nopagebreak \\
\hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\unkef(\!\begin{aligned}[t]
@@ -984,14 +984,14 @@
\textbf{lemma}~``$\lbrakk\textit{xs} = \textit{LCons}~a~\textit{xs};\>\,
\textit{ys} = \textit{iterates}~(\lambda b.\> a)~b\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys\/}$'' \\
\textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
-\slshape The type $'a$ passed the monotonicity test. Nitpick might be able to skip
-some scopes. \\[2\smallskipamount]
+\slshape The type $'a$ passed the monotonicity test; Nitpick might be able to skip
+some scopes \\[2\smallskipamount]
Trying 10 scopes: \\
\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 1,
-and \textit{bisim\_depth}~= 0. \\
+and \textit{bisim\_depth}~= 0; \\
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
\hbox{}\qquad \textit{card} $'a$~= 10, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 10,
-and \textit{bisim\_depth}~= 9. \\[2\smallskipamount]
+and \textit{bisim\_depth}~= 9 \\[2\smallskipamount]
Nitpick found a counterexample for {\itshape card}~$'a$ = 2,
\textit{card}~``\kern1pt$'a~\textit{llist\/}$''~= 2, and \textit{bisim\_\allowbreak
depth}~= 1:
@@ -1001,7 +1001,7 @@
\hbox{}\qquad\qquad $\textit{b} = a_2$ \\
\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
\hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_2~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega)$ \\[2\smallskipamount]
-Total time: 1.11 s.
+Total time: 1.11 s
\postw
The lazy list $\textit{xs}$ is simply $[a_1, a_1, a_1, \ldots]$, whereas
@@ -1054,9 +1054,9 @@
& \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega,\> \unr\}\end{aligned}$
\\[2\smallskipamount]
Try again with ``\textit{bisim\_depth}'' set to a nonnegative value to confirm
-that the counterexample is genuine. \\[2\smallskipamount]
+that the counterexample is genuine \\[2\smallskipamount]
{\upshape\textbf{nitpick}} \\[2\smallskipamount]
-\slshape Nitpick found no counterexample.
+\slshape Nitpick found no counterexample
\postw
In the first \textbf{nitpick} invocation, the after-the-fact check discovered
@@ -1139,7 +1139,7 @@
\hbox{}\qquad \textit{card~nat}~= 1, \textit{card tm}~= 1, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm\/}$'' = 1; \\
\hbox{}\qquad \textit{card~nat}~= 2, \textit{card tm}~= 2, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm\/}$'' = 2; \\
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
-\hbox{}\qquad \textit{card~nat}~= 10, \textit{card tm}~= 10, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm\/}$'' = 10. \\[2\smallskipamount]
+\hbox{}\qquad \textit{card~nat}~= 10, \textit{card tm}~= 10, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm\/}$'' = 10 \\[2\smallskipamount]
Nitpick found a counterexample for \textit{card~nat}~= 6, \textit{card~tm}~= 6,
and \textit{card}~``$\textit{nat} \Rightarrow \textit{tm\/}$''~= 6: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
@@ -1151,7 +1151,7 @@
4 := \textit{Var}~0,\>
5 := \textit{Lam}~(\textit{Lam}~(\textit{Var}~0)))\end{aligned}$ \\
\hbox{}\qquad\qquad $t = \textit{Lam}~(\textit{Lam}~(\textit{Var}~1))$ \\[2\smallskipamount]
-Total time: 3.08 s.
+Total time: 3.08 s
\postw
Using \textit{eval}, we find out that $\textit{subst}~\sigma~t =
@@ -1170,7 +1170,7 @@
\prew
\textbf{nitpick} [\textit{dont\_box}] \\[2\smallskipamount]
-{\slshape Nitpick ran out of time after checking 3 of 10 scopes.}
+{\slshape Nitpick ran out of time after checking 3 of 10 scopes}
\postw
Boxing can be enabled or disabled globally or on a per-type basis using the
@@ -1216,26 +1216,25 @@
\prew
\textbf{nitpick}~[\textit{verbose}] \\[2\smallskipamount]
\slshape
-The types $'a$ and $'b$ passed the monotonicity test.
-Nitpick might be able to skip some scopes.
+The types $'a$ and $'b$ passed the monotonicity test; Nitpick might be able to skip some scopes.
\\[2\smallskipamount]
Trying 10 scopes: \\
\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} $'b$~= 1,
\textit{card} \textit{nat}~= 1, \textit{card} ``$('a \times {'}b)$
\textit{list\/}''~= 1, \\
\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 1, and
-\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 1. \\
+\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 1; \\
\hbox{}\qquad \textit{card} $'a$~= 2, \textit{card} $'b$~= 2,
\textit{card} \textit{nat}~= 2, \textit{card} ``$('a \times {'}b)$
\textit{list\/}''~= 2, \\
\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 2, and
-\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 2. \\
+\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 2; \\
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
\hbox{}\qquad \textit{card} $'a$~= 10, \textit{card} $'b$~= 10,
\textit{card} \textit{nat}~= 10, \textit{card} ``$('a \times {'}b)$
\textit{list\/}''~= 10, \\
\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 10, and
-\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 10.
+\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 10
\\[2\smallskipamount]
Nitpick found a counterexample for
\textit{card} $'a$~= 5, \textit{card} $'b$~= 5,
@@ -1267,7 +1266,7 @@
\textbf{lemma} ``$\exists g.\; \forall x\Colon 'b.~g~(f~x) = x
\,\Longrightarrow\, \forall y\Colon {'}a.\; \exists x.~y = f~x$'' \\
\textbf{nitpick} [\textit{mono}] \\[2\smallskipamount]
-{\slshape Nitpick found no counterexample.} \\[2\smallskipamount]
+{\slshape Nitpick found no counterexample} \\[2\smallskipamount]
\textbf{nitpick} \\[2\smallskipamount]
\slshape
Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\
@@ -1518,7 +1517,7 @@
``$w \in A \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] + 1$'' \\
``$w \in B \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] + 1$'' \\
\textbf{nitpick} \\[2\smallskipamount]
-\slshape Nitpick found no counterexample.
+\slshape Nitpick found no counterexample
\postw
\subsection{AA Trees}
@@ -1627,7 +1626,7 @@
``$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\
``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\
\textbf{nitpick} \\[2\smallskipamount]
-{\slshape Nitpick ran out of time after checking 9 of 10 scopes.}
+{\slshape Nitpick ran out of time after checking 9 of 10 scopes}
\postw
Furthermore, applying \textit{skew} or \textit{split} on a well-formed tree
@@ -1638,7 +1637,7 @@
``$\textit{wf}~t\,\Longrightarrow\, \textit{skew}~t = t$'' \\
``$\textit{wf}~t\,\Longrightarrow\, \textit{split}~t = t$'' \\
\textbf{nitpick} \\[2\smallskipamount]
-{\slshape Nitpick found no counterexample.}
+{\slshape Nitpick found no counterexample}
\postw
Insertion is implemented recursively. It preserves the sort order:
@@ -1689,7 +1688,7 @@
\prew
\textbf{theorem}~\textit{wf\_insort\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
\textbf{nitpick} \\[2\smallskipamount]
-{\slshape Nitpick ran out of time after checking 8 of 10 scopes.}
+{\slshape Nitpick ran out of time after checking 8 of 10 scopes}
\postw
Insertion should transform the set of elements represented by the tree in the
@@ -1699,7 +1698,7 @@
\textbf{theorem} \textit{dataset\_insort\/}:\kern.4em
``$\textit{dataset}~(\textit{insort}~t~x) = \{x\} \cup \textit{dataset}~t$'' \\
\textbf{nitpick} \\[2\smallskipamount]
-{\slshape Nitpick ran out of time after checking 7 of 10 scopes.}
+{\slshape Nitpick ran out of time after checking 7 of 10 scopes}
\postw
We could continue like this and sketch a full-blown theory of AA trees. Once the
--- a/src/Doc/Sledgehammer/document/root.tex Thu Sep 01 16:12:55 2016 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Sep 01 16:13:46 2016 +0200
@@ -261,13 +261,13 @@
\prew
\slshape
Proof found\ldots \\
-``\textit{e\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms). \\
+``\textit{e\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms) \\
%
-``\textit{cvc4\/}'': Try this: \textbf{by} \textit{simp} (0.4 ms). \\
+``\textit{cvc4\/}'': Try this: \textbf{by} \textit{simp} (0.4 ms) \\
%
-``\textit{z3\/}'': Try this: \textbf{by} \textit{simp} (0.5 ms). \\
+``\textit{z3\/}'': Try this: \textbf{by} \textit{simp} (0.5 ms) \\
%
-``\textit{spass\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms).
+``\textit{spass\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms)
%
\postw
@@ -498,7 +498,7 @@
\prew
\slshape
-Metis: Falling back on ``\textit{metis} (\textit{full\_types})''.
+Metis: Falling back on ``\textit{metis} (\textit{full\_types})''
\postw
for a successful \textit{metis} proof, you can advantageously pass the
@@ -530,16 +530,7 @@
\point{A strange error occurred---what should I do?}
Sledgehammer tries to give informative error messages. Please report any strange
-error to the author at \authoremail. This applies doubly if you get the message
-
-\prew
-\slshape
-The prover derived ``\textit{False}'' using ``\textit{foo\/}'',
-``\textit{bar\/}'', and ``\textit{baz\/}''.
-This could be due to inconsistent axioms (including ``\textbf{sorry}''s) or to
-a bug in Sledgehammer. If the problem persists, please contact the
-Isabelle developers.
-\postw
+error to the author at \authoremail.
\point{Auto can solve it---why not Sledgehammer?}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Nesting.thy Thu Sep 01 16:13:46 2016 +0200
@@ -0,0 +1,19 @@
+theory Quickcheck_Nesting
+imports Main
+begin
+
+ML \<open>
+let
+ open BNF_FP_Def_Sugar
+ open BNF_LFP_Compat
+
+ val compat_plugin = Plugin_Name.declare_setup @{binding compat};
+
+ fun compat fp_sugars =
+ perhaps (try (datatype_compat (map (fst o dest_Type o #T) fp_sugars)));
+in
+ Theory.setup (fp_sugars_interpretation compat_plugin compat)
+end
+\<close>
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Nesting_Example.thy Thu Sep 01 16:13:46 2016 +0200
@@ -0,0 +1,11 @@
+theory Quickcheck_Nesting_Example
+imports Quickcheck_Nesting
+begin
+
+datatype x = X "x list"
+
+lemma "X a = X b"
+quickcheck[exhaustive, size = 4, expect = counterexample]
+oops
+
+end
--- a/src/HOL/ROOT Thu Sep 01 16:12:55 2016 +0200
+++ b/src/HOL/ROOT Thu Sep 01 16:13:46 2016 +0200
@@ -978,6 +978,7 @@
Quickcheck_Lattice_Examples
Completeness
Quickcheck_Interfaces
+ Quickcheck_Nesting_Example
theories [condition = ISABELLE_GHC]
Hotel_Example
Quickcheck_Narrowing_Examples
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Sep 01 16:12:55 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Sep 01 16:13:46 2016 +0200
@@ -221,7 +221,7 @@
val fpTs0 as Type (_, var_As) :: _ =
map (#T o checked_fp_sugar_of o fst o dest_Type)
(#Ts (#fp_res (checked_fp_sugar_of (hd fpT_names0))));
- val fpT_names = map (fst o dest_Type) fpTs0;
+ val fpT_names as fpT_name1 :: _ = map (fst o dest_Type) fpTs0;
val _ = check_names (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0;
@@ -237,7 +237,8 @@
fun mk_typ_descr index (Type (T_name, Ts)) ({ctrs, ...} : ctr_sugar) =
(index, (T_name, map mk_dtyp Ts, map (mk_ctr_descr Ts) ctrs));
- val fp_ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar o checked_fp_sugar_of) fpT_names;
+ val fp_sugars as {fp, ...} :: _ = map checked_fp_sugar_of fpT_names;
+ val fp_ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar) fp_sugars;
val orig_descr = @{map 3} mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars;
val all_infos = Old_Datatype_Data.get_all thy;
val (orig_descr' :: nested_descrs) =
@@ -310,11 +311,13 @@
if member (op =) prefs Keep_Nesting orelse
not (exists (exists (exists is_nested_rec_type)) ctrXs_Tsss') then
((lfp_sugar_thms', (inducts, induct, recs, rec_thmss)), lthy')
- else
+ else if fp = Least_FP then
define_split_rec_derive_induct_rec_thms Xs' fpTs' ctrXs_Tsss' ctrss' inducts induct recs
rec_thmss lthy'
|>> `(fn (inducts', induct', _, rec'_thmss) =>
- SOME ((inducts', induct', mk_induct_attrs ctrss'), (rec'_thmss, [])));
+ SOME ((inducts', induct', mk_induct_attrs ctrss'), (rec'_thmss, [])))
+ else
+ not_datatype fpT_name1;
val rec'_names = map (fst o dest_Const) recs';
val rec'_thms = flat rec'_thmss;
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Thu Sep 01 16:12:55 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Thu Sep 01 16:13:46 2016 +0200
@@ -49,7 +49,7 @@
(* static options *)
-val compat_prefs = [BNF_LFP_Compat.Keep_Nesting, BNF_LFP_Compat.Include_GFPs]
+val compat_prefs = [BNF_LFP_Compat.Include_GFPs]
val define_foundationally = false
--- a/src/Tools/solve_direct.ML Thu Sep 01 16:12:55 2016 +0200
+++ b/src/Tools/solve_direct.ML Thu Sep 01 16:13:46 2016 +0200
@@ -79,11 +79,11 @@
let val msg = Pretty.string_of (Pretty.chunks (message results))
in if mode = Auto_Try then [msg] else (writeln msg; []) end)
| SOME NONE =>
- (if mode = Normal then writeln "No proof found."
+ (if mode = Normal then writeln "No proof found"
else ();
(noneN, []))
| NONE =>
- (if mode = Normal then writeln "An error occurred."
+ (if mode = Normal then writeln "An error occurred"
else ();
(unknownN, [])))
end