# HG changeset patch # User blanchet # Date 1306188093 -7200 # Node ID ee829022381dc5de1769ed3fd8b62bf3e0d594d7 # Parent 034fc4d0c9093c2631fefbf77f35ae274b24b324 use \ rather than \ diff -r 034fc4d0c909 -r ee829022381d doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Tue May 24 00:01:33 2011 +0200 +++ b/doc-src/Nitpick/nitpick.tex Tue May 24 00:01:33 2011 +0200 @@ -346,7 +346,7 @@ \prew \textbf{nitpick} [\textit{card} $'a$~= 1--50]\footnote{The symbol `--' can be entered as \texttt{-} (hyphen) or -\texttt{\char`\\\char`\}.} \\[2\smallskipamount] +\texttt{\char`\\\char`\}.} \\[2\smallskipamount] \slshape Nitpick found no counterexample. \postw @@ -1890,7 +1890,7 @@ \item[$\bullet$] \qtybf{int\/}: An integer. Negative integers are prefixed with a hyphen. \item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}. \item[$\bullet$] \qtybf{int\_range}: An integer (e.g., 3) or a range -of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\}. +of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\}. \item[$\bullet$] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8). \item[$\bullet$] \qtybf{float\_or\_none}: An integer (e.g., 60) or floating-point number (e.g., 0.5) expressing a number of seconds, or the keyword \textit{none} diff -r 034fc4d0c909 -r ee829022381d src/HOL/Nitpick_Examples/Core_Nits.thy --- a/src/HOL/Nitpick_Examples/Core_Nits.thy Tue May 24 00:01:33 2011 +0200 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Tue May 24 00:01:33 2011 +0200 @@ -11,29 +11,29 @@ imports Main begin -nitpick_params [verbose, card = 1\6, unary_ints, max_potential = 0, +nitpick_params [verbose, card = 1\6, unary_ints, max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240] subsection {* Curry in a Hurry *} lemma "(\f x y. (curry o split) f x y) = (\f x y. (\x. x) f x y)" -nitpick [card = 1\12, expect = none] +nitpick [card = 1\12, expect = none] by auto lemma "(\f p. (split o curry) f p) = (\f p. (\x. x) f p)" -nitpick [card = 1\12, expect = none] +nitpick [card = 1\12, expect = none] by auto lemma "split (curry f) = f" -nitpick [card = 1\12, expect = none] +nitpick [card = 1\12, expect = none] by auto lemma "curry (split f) = f" -nitpick [card = 1\12, expect = none] +nitpick [card = 1\12, expect = none] by auto lemma "split (\x y. f (x, y)) = f" -nitpick [card = 1\12, expect = none] +nitpick [card = 1\12, expect = none] by auto subsection {* Representations *} @@ -44,7 +44,7 @@ lemma "(\g. \x. g (f x) = x) \ (\y. \x. y = f x)" nitpick [card 'a = 25, card 'b = 24, expect = genuine] -nitpick [card = 1\10, mono, expect = none] +nitpick [card = 1\10, mono, expect = none] oops lemma "\f. f = (\x. x) \ f y \ y" @@ -56,39 +56,39 @@ oops lemma "{(a\'a\'a, b\'b)}^-1 = {(b, a)}" -nitpick [card = 1\12, expect = none] +nitpick [card = 1\12, expect = none] by auto lemma "fst (a, b) = a" -nitpick [card = 1\20, expect = none] +nitpick [card = 1\20, expect = none] by auto lemma "\P. P = Id" -nitpick [card = 1\20, expect = none] +nitpick [card = 1\20, expect = none] by auto lemma "(a\'a\'b, a) \ Id\<^sup>*" -nitpick [card = 1\3, expect = none] +nitpick [card = 1\3, expect = none] by auto lemma "(a\'a\'a, a) \ Id\<^sup>* \ {(a, b)}\<^sup>*" -nitpick [card = 1\4, expect = none] +nitpick [card = 1\4, expect = none] by auto lemma "Id (a, a)" -nitpick [card = 1\50, expect = none] +nitpick [card = 1\50, expect = none] by (auto simp: Id_def Collect_def) lemma "Id ((a\'a, b\'a), (a, b))" -nitpick [card = 1\10, expect = none] +nitpick [card = 1\10, expect = none] by (auto simp: Id_def Collect_def) lemma "UNIV (x\'a\'a)" -nitpick [card = 1\50, expect = none] +nitpick [card = 1\50, expect = none] sorry lemma "{} = A - A" -nitpick [card = 1\100, expect = none] +nitpick [card = 1\100, expect = none] by auto lemma "g = Let (A \ B)" @@ -132,7 +132,7 @@ oops lemma "(x\'a) = (\a. \b. \c. if c then a else b) x x True" -nitpick [card = 1\10, expect = none] +nitpick [card = 1\10, expect = none] by auto lemma "\F. F a b = G a b" @@ -149,7 +149,7 @@ lemma "(A, B) \ R \ (\C. (A, C) \ R \ (C, B) \ R) \ A = B \ (A, B) \ R \ (\C. (A, C) \ R \ (C, B) \ R)" -nitpick [card = 1\25, expect = none] +nitpick [card = 1\25, expect = none] by auto lemma "f = (\x\'a\'b. x)" @@ -174,19 +174,19 @@ oops lemma "\x\'a \ bool. x = y" -nitpick [card 'a = 1\15, expect = none] +nitpick [card 'a = 1\15, expect = none] by auto lemma "\x y\'a \ bool. x = y" -nitpick [card = 1\15, expect = none] +nitpick [card = 1\15, expect = none] by auto lemma "\x. \y. f x y = f x (g x)" -nitpick [card = 1\4, expect = none] +nitpick [card = 1\4, expect = none] by auto lemma "\u. \v. \w. \x. f u v w x = f u (g u) w (h u w)" -nitpick [card = 1\4, expect = none] +nitpick [card = 1\4, expect = none] by auto lemma "\u. \v. \w. \x. f u v w x = f u (g u w) w (h u)" @@ -195,42 +195,42 @@ lemma "\u. \v. \w. \x. \y. \z. f u v w x y z = f u (g u) w (h u w) y (k u w y)" -nitpick [card = 1\2, expect = none] +nitpick [card = 1\2, expect = none] sorry lemma "\u. \v. \w. \x. \y. \z. f u v w x y z = f u (g u) w (h u w y) y (k u w y)" -nitpick [card = 1\2, expect = genuine] +nitpick [card = 1\2, expect = genuine] oops lemma "\u. \v. \w. \x. \y. \z. f u v w x y z = f u (g u w) w (h u w) y (k u w y)" -nitpick [card = 1\2, expect = genuine] +nitpick [card = 1\2, expect = genuine] oops lemma "\u\'a \ 'b. \v\'c. \w\'d. \x\'e \ 'f. f u v w x = f u (g u) w (h u w)" -nitpick [card = 1\2, expect = none] +nitpick [card = 1\2, expect = none] sorry lemma "\u\'a \ 'b. \v\'c. \w\'d. \x\'e \ 'f. f u v w x = f u (g u w) w (h u)" -nitpick [card = 1\2, dont_box, expect = genuine] +nitpick [card = 1\2, dont_box, expect = genuine] oops lemma "\u\'a \ 'b. \v\'c. \w\'d. \x\'e \ 'f. f u v w x = f u (g u) w (h u w)" -nitpick [card = 1\2, dont_box, expect = none] +nitpick [card = 1\2, dont_box, expect = none] sorry lemma "\u\'a \ 'b. \v\'c. \w\'d. \x\'e \ 'f. f u v w x = f u (g u w) w (h u)" -nitpick [card = 1\2, dont_box, expect = genuine] +nitpick [card = 1\2, dont_box, expect = genuine] oops lemma "\x. if (\y. x = y) then False else True" nitpick [card = 1, expect = genuine] -nitpick [card = 2\5, expect = none] +nitpick [card = 2\5, expect = none] oops lemma "\x\'a\'b. if (\y. x = y) then False else True" @@ -323,15 +323,15 @@ oops lemma "P x \ P x" -nitpick [card = 1\10, expect = none] +nitpick [card = 1\10, expect = none] by auto lemma "P x \ Q x \ P x = Q x" -nitpick [card = 1\10, expect = none] +nitpick [card = 1\10, expect = none] by auto lemma "P x = Q x \ P x \ Q x" -nitpick [card = 1\10, expect = none] +nitpick [card = 1\10, expect = none] by auto lemma "x \ (op \) \ False" @@ -343,7 +343,7 @@ by auto lemma "P x \ P x" -nitpick [card = 1\10, expect = none] +nitpick [card = 1\10, expect = none] by auto lemma "True \ True" "False \ True" "False \ False" @@ -604,11 +604,11 @@ by simp lemma "I = (\x. x) \ trancl = (\x. trancl (I x))" -nitpick [card = 1\2, expect = none] +nitpick [card = 1\2, expect = none] by auto lemma "rtrancl = (\x. rtrancl x \ {(y, y)})" -nitpick [card = 1\3, expect = none] +nitpick [card = 1\3, expect = none] apply (rule ext) by auto @@ -617,11 +617,11 @@ by auto lemma "((x, x), (x, x)) \ rtrancl {}" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] by auto lemma "I = (\x. x) \ op \ = (\x. op \ (I x))" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] by auto lemma "a \ A \ a \ (A \ B)" "b \ B \ b \ (A \ B)" @@ -629,27 +629,27 @@ by auto lemma "I = (\x. x) \ op \ = (\x. op \ (I x))" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] by auto lemma "a \ A \ a \ (A \ B)" "b \ B \ b \ (A \ B)" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] by auto lemma "x \ ((A\'a set) - B) \ x \ A \ x \ B" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] by auto lemma "I = (\x. x) \ op \ = (\x. op \ (I x))" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] by auto lemma "A \ B \ (\a \ A. a \ B) \ (\b \ B. b \ A)" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] by auto lemma "A \ B \ \a \ A. a \ B" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] by auto lemma "A \ B \ A \ B" @@ -661,7 +661,7 @@ by auto lemma "I = (\x\'a set. x) \ uminus = (\x. uminus (I x))" -nitpick [card = 1\7, expect = none] +nitpick [card = 1\7, expect = none] by auto lemma "A \ - A = UNIV" @@ -695,7 +695,7 @@ oops lemma "\x. x = The" -nitpick [card = 1\3] +nitpick [card = 1\3] by auto lemma "P x \ (\y. P y \ y = x) \ The P = x" @@ -708,11 +708,11 @@ lemma "P x \ P y \ x \ y \ The P = x \ The P = y" nitpick [card = 2, expect = none] -nitpick [card = 3\5, expect = genuine] +nitpick [card = 3\5, expect = genuine] oops lemma "P x \ P (The P)" -nitpick [card = 1\2, expect = none] +nitpick [card = 1\2, expect = none] nitpick [card = 8, expect = genuine] oops @@ -721,7 +721,7 @@ oops lemma "I = (\x. x) \ The = (\x. The (I x))" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] by auto lemma "x = Eps" @@ -729,7 +729,7 @@ oops lemma "\x. x = Eps" -nitpick [card = 1\3, expect = none] +nitpick [card = 1\3, expect = none] by auto lemma "P x \ (\y. P y \ y = x) \ Eps P = x" @@ -742,7 +742,7 @@ oops lemma "P x \ P (Eps P)" -nitpick [card = 1\8, expect = none] +nitpick [card = 1\8, expect = none] by (metis exE_some) lemma "\x. \ P x \ Eps P = y" diff -r 034fc4d0c909 -r ee829022381d src/HOL/Nitpick_Examples/Datatype_Nits.thy --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Tue May 24 00:01:33 2011 +0200 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Tue May 24 00:01:33 2011 +0200 @@ -11,7 +11,7 @@ imports Main begin -nitpick_params [verbose, card = 1\8, max_potential = 0, +nitpick_params [verbose, card = 1\8, max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240] primrec rot where @@ -23,7 +23,7 @@ "rot NibbleF = Nibble0" lemma "rot n \ n" -nitpick [card = 1\8,16, verbose, expect = none] +nitpick [card = 1\8,16, verbose, expect = none] sorry lemma "rot Nibble2 \ Nibble3" diff -r 034fc4d0c909 -r ee829022381d src/HOL/Nitpick_Examples/Induct_Nits.thy --- a/src/HOL/Nitpick_Examples/Induct_Nits.thy Tue May 24 00:01:33 2011 +0200 +++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy Tue May 24 00:01:33 2011 +0200 @@ -11,7 +11,7 @@ imports Main begin -nitpick_params [verbose, card = 1\8, unary_ints, +nitpick_params [verbose, card = 1\8, unary_ints, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240] inductive p1 :: "nat \ bool" where diff -r 034fc4d0c909 -r ee829022381d src/HOL/Nitpick_Examples/Integer_Nits.thy --- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Tue May 24 00:01:33 2011 +0200 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Tue May 24 00:01:33 2011 +0200 @@ -11,7 +11,7 @@ imports Nitpick begin -nitpick_params [verbose, card = 1\5, bits = 1,2,3,4,6, +nitpick_params [verbose, card = 1\5, bits = 1,2,3,4,6, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240] lemma "Suc x = x + 1" @@ -187,7 +187,7 @@ lemma "y \ 0 \ x * y div y = (x::int)" nitpick [unary_ints, expect = none] -nitpick [binary_ints, card = 1\4, bits = 1\4, expect = none] +nitpick [binary_ints, card = 1\4, bits = 1\4, expect = none] sorry lemma "(x * y < 0) \ (x > 0 \ y < 0) \ (x < 0 \ y > (0::int))" diff -r 034fc4d0c909 -r ee829022381d src/HOL/Nitpick_Examples/Manual_Nits.thy --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue May 24 00:01:33 2011 +0200 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue May 24 00:01:33 2011 +0200 @@ -44,7 +44,7 @@ lemma "\!x. P x \ P (THE y. P y)" nitpick [expect = none] -nitpick [card 'a = 1\50, expect = none] +nitpick [card 'a = 1\50, expect = none] (* sledgehammer *) apply (metis the_equality) done @@ -227,7 +227,7 @@ lemma "\xs = LCons a xs; ys = LCons a ys\ \ xs = ys" nitpick [bisim_depth = -1, show_datatypes, expect = quasi_genuine] -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] sorry subsection {* 3.10. Boxing *} @@ -263,7 +263,7 @@ "subst\<^isub>2 \ (App t u) = App (subst\<^isub>2 \ t) (subst\<^isub>2 \ u)" lemma "\ loose t 0 \ subst\<^isub>2 \ t = t" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] sorry subsection {* 3.11. Scope Monotonicity *} @@ -288,7 +288,7 @@ (* nitpick *) apply (induct set: reach) apply auto - nitpick [card = 1\4, bits = 1\4, expect = none] + nitpick [card = 1\4, bits = 1\4, expect = none] apply (thin_tac "n \ reach") nitpick [expect = genuine] oops @@ -297,7 +297,7 @@ (* nitpick *) apply (induct set: reach) apply auto - nitpick [card = 1\4, bits = 1\4, expect = none] + nitpick [card = 1\4, bits = 1\4, expect = none] apply (thin_tac "n \ reach") nitpick [expect = genuine] oops @@ -336,7 +336,7 @@ case Leaf thus ?case by simp next case (Branch t u) thus ?case - nitpick [non_std, card = 1\4, expect = none] + nitpick [non_std, card = 1\4, expect = none] by auto qed @@ -384,7 +384,7 @@ theorem S\<^isub>3_sound: "w \ S\<^isub>3 \ length [x \ w. x = a] = length [x \ w. x = b]" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] sorry theorem S\<^isub>3_complete: @@ -403,19 +403,19 @@ theorem S\<^isub>4_sound: "w \ S\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b]" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] sorry theorem S\<^isub>4_complete: "length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^isub>4" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] sorry theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete: "w \ S\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b]" "w \ A\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b] + 1" "w \ B\<^isub>4 \ length [x \ w. x = b] = length [x \ w. x = a] + 1" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] sorry subsection {* 4.2. AA Trees *} @@ -469,13 +469,13 @@ theorem dataset_skew_split: "dataset (skew t) = dataset t" "dataset (split t) = dataset t" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] sorry theorem wf_skew_split: "wf t \ skew t = t" "wf t \ split t = t" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] sorry primrec insort\<^isub>1 where @@ -499,11 +499,11 @@ (if x > y then insort\<^isub>2 u x else u))" theorem wf_insort\<^isub>2: "wf t \ wf (insort\<^isub>2 t x)" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] sorry theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \ dataset t" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] sorry end diff -r 034fc4d0c909 -r ee829022381d src/HOL/Nitpick_Examples/Record_Nits.thy --- a/src/HOL/Nitpick_Examples/Record_Nits.thy Tue May 24 00:01:33 2011 +0200 +++ b/src/HOL/Nitpick_Examples/Record_Nits.thy Tue May 24 00:01:33 2011 +0200 @@ -11,7 +11,7 @@ imports Main begin -nitpick_params [verbose, card = 1\6, max_potential = 0, +nitpick_params [verbose, card = 1\6, max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240] record point2d = diff -r 034fc4d0c909 -r ee829022381d src/HOL/Nitpick_Examples/Refute_Nits.thy --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Tue May 24 00:01:33 2011 +0200 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Tue May 24 00:01:33 2011 +0200 @@ -11,7 +11,7 @@ imports Main begin -nitpick_params [verbose, card = 1\6, max_potential = 0, +nitpick_params [verbose, card = 1\6, max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240] lemma "P \ Q" @@ -283,7 +283,7 @@ text {* ``Every point is a fixed point of some function.'' *} lemma "\f. f x = x" -nitpick [card = 1\7, expect = none] +nitpick [card = 1\7, expect = none] apply (rule_tac x = "\x. x" in exI) apply simp done @@ -745,7 +745,7 @@ oops lemma "T3_rec e (E x) = e x" -nitpick [card = 1\4, expect = none] +nitpick [card = 1\4, expect = none] apply simp done @@ -774,7 +774,7 @@ oops lemma "P Suc" -nitpick [card = 1\7, expect = none] +nitpick [card = 1\7, expect = none] oops lemma "nat_rec zero suc 0 = zero" @@ -810,12 +810,12 @@ oops lemma "list_rec nil cons [] = nil" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] apply simp done lemma "list_rec nil cons (x#xs) = cons x xs (list_rec nil cons xs)" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] apply simp done @@ -888,7 +888,7 @@ done lemma "BinTree_rec l n (Node x y) = n x y (BinTree_rec l n x) (BinTree_rec l n y)" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] apply simp done @@ -926,12 +926,12 @@ oops lemma "aexp_bexp_rec_1 number ite equal (Number x) = number x" -nitpick [card = 1\3, expect = none] +nitpick [card = 1\3, expect = none] apply simp done lemma "aexp_bexp_rec_1 number ite equal (ITE x y z) = ite x y z (aexp_bexp_rec_2 number ite equal x) (aexp_bexp_rec_1 number ite equal y) (aexp_bexp_rec_1 number ite equal z)" -nitpick [card = 1\3, expect = none] +nitpick [card = 1\3, expect = none] apply simp done @@ -944,7 +944,7 @@ oops lemma "aexp_bexp_rec_2 number ite equal (Equal x y) = equal x y (aexp_bexp_rec_1 number ite equal x) (aexp_bexp_rec_1 number ite equal y)" -nitpick [card = 1\3, expect = none] +nitpick [card = 1\3, expect = none] apply simp done @@ -1004,32 +1004,32 @@ oops lemma "X_Y_rec_1 a b c d e f A = a" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] apply simp done lemma "X_Y_rec_1 a b c d e f (B x) = b x (X_Y_rec_1 a b c d e f x)" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] apply simp done lemma "X_Y_rec_1 a b c d e f (C y) = c y (X_Y_rec_2 a b c d e f y)" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] apply simp done lemma "X_Y_rec_2 a b c d e f (D x) = d x (X_Y_rec_1 a b c d e f x)" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] apply simp done lemma "X_Y_rec_2 a b c d e f (E y) = e y (X_Y_rec_2 a b c d e f y)" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] apply simp done lemma "X_Y_rec_2 a b c d e f F = f" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] apply simp done @@ -1060,32 +1060,32 @@ oops lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (CX x) = cx x (XOpt_rec_2 cx dx n1 s1 n2 s2 x)" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] apply simp done lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\b. XOpt_rec_3 cx dx n1 s1 n2 s2 (x b))" -nitpick [card = 1\3, expect = none] +nitpick [card = 1\3, expect = none] apply simp done lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 None = n1" -nitpick [card = 1\4, expect = none] +nitpick [card = 1\4, expect = none] apply simp done lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)" -nitpick [card = 1\4, expect = none] +nitpick [card = 1\4, expect = none] apply simp done lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 None = n2" -nitpick [card = 1\4, expect = none] +nitpick [card = 1\4, expect = none] apply simp done lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)" -nitpick [card = 1\4, expect = none] +nitpick [card = 1\4, expect = none] apply simp done @@ -1116,17 +1116,17 @@ oops lemma "YOpt_rec_1 cy n s (CY x) = cy x (YOpt_rec_2 cy n s x)" -nitpick [card = 1\2, expect = none] +nitpick [card = 1\2, expect = none] apply simp done lemma "YOpt_rec_2 cy n s None = n" -nitpick [card = 1\2, expect = none] +nitpick [card = 1\2, expect = none] apply simp done lemma "YOpt_rec_2 cy n s (Some x) = s x (\a. YOpt_rec_1 cy n s (x a))" -nitpick [card = 1\2, expect = none] +nitpick [card = 1\2, expect = none] apply simp done @@ -1153,17 +1153,17 @@ oops lemma "Trie_rec_1 tr nil cons (TR x) = tr x (Trie_rec_2 tr nil cons x)" -nitpick [card = 1\4, expect = none] +nitpick [card = 1\4, expect = none] apply simp done lemma "Trie_rec_2 tr nil cons [] = nil" -nitpick [card = 1\4, expect = none] +nitpick [card = 1\4, expect = none] apply simp done lemma "Trie_rec_2 tr nil cons (x#xs) = cons x xs (Trie_rec_1 tr nil cons x) (Trie_rec_2 tr nil cons xs)" -nitpick [card = 1\4, expect = none] +nitpick [card = 1\4, expect = none] apply simp done @@ -1190,12 +1190,12 @@ oops lemma "InfTree_rec leaf node Leaf = leaf" -nitpick [card = 1\3, expect = none] +nitpick [card = 1\3, expect = none] apply simp done lemma "InfTree_rec leaf node (Node x) = node x (\n. InfTree_rec leaf node (x n))" -nitpick [card = 1\3, expect = none] +nitpick [card = 1\3, expect = none] apply simp done @@ -1214,22 +1214,22 @@ oops lemma "P (Lam (\a. Var a))" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\5, expect = none] nitpick [card 'a = 4, card "'a lambda" = 5, expect = genuine] oops lemma "lambda_rec var app lam (Var x) = var x" -nitpick [card = 1\3, expect = none] +nitpick [card = 1\3, expect = none] apply simp done lemma "lambda_rec var app lam (App x y) = app x y (lambda_rec var app lam x) (lambda_rec var app lam y)" -nitpick [card = 1\3, expect = none] +nitpick [card = 1\3, expect = none] apply simp done lemma "lambda_rec var app lam (Lam x) = lam x (\a. lambda_rec var app lam (x a))" -nitpick [card = 1\3, expect = none] +nitpick [card = 1\3, expect = none] apply simp done @@ -1255,27 +1255,27 @@ oops lemma "U_rec_1 e c d nil cons (E x) = e x (U_rec_2 e c d nil cons x)" -nitpick [card = 1\3, expect = none] +nitpick [card = 1\3, expect = none] apply simp done lemma "U_rec_2 e c d nil cons (C x) = c x" -nitpick [card = 1\3, expect = none] +nitpick [card = 1\3, expect = none] apply simp done lemma "U_rec_2 e c d nil cons (D x) = d x (U_rec_3 e c d nil cons x)" -nitpick [card = 1\3, expect = none] +nitpick [card = 1\3, expect = none] apply simp done lemma "U_rec_3 e c d nil cons [] = nil" -nitpick [card = 1\3, expect = none] +nitpick [card = 1\3, expect = none] apply simp done lemma "U_rec_3 e c d nil cons (x#xs) = cons x xs (U_rec_1 e c d nil cons x) (U_rec_3 e c d nil cons xs)" -nitpick [card = 1\3, expect = none] +nitpick [card = 1\3, expect = none] apply simp done diff -r 034fc4d0c909 -r ee829022381d src/HOL/Nitpick_Examples/Typedef_Nits.thy --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue May 24 00:01:33 2011 +0200 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue May 24 00:01:33 2011 +0200 @@ -11,7 +11,7 @@ imports Complex_Main begin -nitpick_params [verbose, card = 1\4, sat_solver = MiniSat_JNI, max_threads = 1, +nitpick_params [verbose, card = 1\4, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240] typedef three = "{0\nat, 1, 2}" @@ -68,7 +68,7 @@ sorry lemma "x \ (y\(bool \ bool) bounded) \ z = x \ z = y" -nitpick [card = 1\5, expect = genuine] +nitpick [card = 1\5, expect = genuine] oops lemma "True \ ((\x\bool. x) = (\x. x))" @@ -96,11 +96,11 @@ oops lemma "Pair a b = Abs_prod (Pair_Rep a b)" -nitpick [card = 1\2, expect = none] +nitpick [card = 1\2, expect = none] by (rule Pair_def) lemma "Pair a b = Abs_prod (Pair_Rep b a)" -nitpick [card = 1\2, expect = none] +nitpick [card = 1\2, expect = none] nitpick [dont_box, expect = genuine] oops @@ -109,7 +109,7 @@ by (simp add: Pair_def [THEN sym]) lemma "fst (Abs_prod (Pair_Rep a b)) = b" -nitpick [card = 1\2, expect = none] +nitpick [card = 1\2, expect = none] nitpick [dont_box, expect = genuine] oops @@ -163,7 +163,7 @@ by (rule Zero_int_def_raw) lemma "Abs_list (Rep_list a) = a" -nitpick [card = 1\2, expect = none] +nitpick [card = 1\2, expect = none] by (rule Rep_list_inverse) record point = diff -r 034fc4d0c909 -r ee829022381d src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Tue May 24 00:01:33 2011 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue May 24 00:01:33 2011 +0200 @@ -352,11 +352,12 @@ pstrs ("The type" ^ plural_s_for_list pretties ^ " ") @ pretty_serial_commas "and" pretties @ pstrs (" " ^ - (if none_true monos then - "passed the monotonicity test" - else - (if length pretties = 1 then "is" else "are") ^ " considered monotonic") ^ - ". " ^ extra)) + (if none_true monos then + "passed the monotonicity test" + else + (if length pretties = 1 then "is" else "are") ^ + " considered monotonic") ^ + ". " ^ extra)) end fun is_type_fundamentally_monotonic T = (is_datatype ctxt stds T andalso not (is_quot_type ctxt T) andalso diff -r 034fc4d0c909 -r ee829022381d src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue May 24 00:01:33 2011 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue May 24 00:01:33 2011 +0200 @@ -38,7 +38,7 @@ type raw_param = string * string list val default_default_params = - [("card", "1\10"), + [("card", "1\10"), ("iter", "0,1,2,4,8,12,16,20,24,28"), ("bits", "1,2,3,4,6,8,10,12,14,16"), ("bisim_depth", "9"), @@ -148,7 +148,7 @@ Data.map o fold (AList.update (op =)) o normalize_raw_param val default_raw_params = Data.get -fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\") +fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\") fun stringify_raw_param_value [] = "" | stringify_raw_param_value [s] = s @@ -187,7 +187,7 @@ let val (k1, k2) = (case space_explode "-" s of - [s] => the_default (s, s) (first_field "\" s) + [s] => the_default (s, s) (first_field "\" s) | ["", s2] => ("-" ^ s2, "-" ^ s2) | [s1, s2] => (s1, s2) | _ => raise Option) diff -r 034fc4d0c909 -r ee829022381d src/HOL/Tools/Nitpick/nitrox.ML --- a/src/HOL/Tools/Nitpick/nitrox.ML Tue May 24 00:01:33 2011 +0200 +++ b/src/HOL/Tools/Nitpick/nitrox.ML Tue May 24 00:01:33 2011 +0200 @@ -2,7 +2,7 @@ Author: Jasmin Blanchette, TU Muenchen Copyright 2010, 2011 -Finite model generation for TPTP first-order formulas via Nitpick. +Finite model generation for TPTP first-order formulas (FOF and CNF) via Nitpick. *) signature NITROX = @@ -182,8 +182,7 @@ *) val state = Proof.init @{context} val params = - [("card iota", "1\100"), - ("card", "1\8"), + [("card", "1\8"), ("box", "false"), ("sat_solver", "smart"), ("max_threads", "1"),