# HG changeset patch # User wenzelm # Date 1472739226 -7200 # Node ID 79f11158dcc41990fa0e85790f1e048d3289ca4f # Parent 622b54bbe8d4d9c98265cd2450630356f1854f6e# Parent 300f9782cb6fe3c88063ef75d1aa5d3a5bc24b47 merged diff -r 300f9782cb6f -r 79f11158dcc4 src/Doc/Nitpick/document/root.tex --- 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 diff -r 300f9782cb6f -r 79f11158dcc4 src/Doc/Sledgehammer/document/root.tex --- 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?} diff -r 300f9782cb6f -r 79f11158dcc4 src/HOL/Quickcheck_Examples/Quickcheck_Nesting.thy --- /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 \ +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 +\ + +end diff -r 300f9782cb6f -r 79f11158dcc4 src/HOL/Quickcheck_Examples/Quickcheck_Nesting_Example.thy --- /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 diff -r 300f9782cb6f -r 79f11158dcc4 src/HOL/ROOT --- 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 diff -r 300f9782cb6f -r 79f11158dcc4 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- 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; diff -r 300f9782cb6f -r 79f11158dcc4 src/HOL/Tools/Quickcheck/quickcheck_common.ML --- 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 diff -r 300f9782cb6f -r 79f11158dcc4 src/Tools/solve_direct.ML --- 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