# HG changeset patch # User blanchet # Date 1266923669 -3600 # Node ID 99cd1f96b4006625498cb880eec7ce04f84fb86a # Parent 8f9a66fc9f806d697d9887366ce634176cce5edf improved precision of small sets in Nitpick diff -r 8f9a66fc9f80 -r 99cd1f96b400 doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Tue Feb 23 11:05:32 2010 +0100 +++ b/doc-src/Nitpick/nitpick.tex Tue Feb 23 12:14:29 2010 +0100 @@ -154,7 +154,7 @@ 15~seconds (instead of 30~seconds). This was done by adding the line \prew -\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1, \,\,\textit{timeout} = 15$\,s$] +\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1, \,\textit{timeout} = 15$\,s$] \postw after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with diff -r 8f9a66fc9f80 -r 99cd1f96b400 src/HOL/Nitpick_Examples/Manual_Nits.thy --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Feb 23 11:05:32 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Feb 23 12:14:29 2010 +0100 @@ -149,7 +149,7 @@ "\even' m; even' n\ \ even' (m + n)" lemma "\n \ {0, 2, 4, 6, 8}. \ even' n" -nitpick [card nat = 10, unary_ints, verbose, show_consts] (* FIXME: should be genuine *) +nitpick [card nat = 10, unary_ints, verbose, show_consts] oops lemma "even' (n - 2) \ even' n" diff -r 8f9a66fc9f80 -r 99cd1f96b400 src/HOL/Nitpick_Examples/Special_Nits.thy --- a/src/HOL/Nitpick_Examples/Special_Nits.thy Tue Feb 23 11:05:32 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Tue Feb 23 12:14:29 2010 +0100 @@ -110,12 +110,12 @@ lemma "\one \ {1}. \two \ {2}. f5 (\a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x" -nitpick [expect = potential] (* unfortunate *) +nitpick [expect = genuine] oops lemma "\two \ {2}. \one \ {1}. f5 (\a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x" -nitpick [expect = potential] (* unfortunate *) +nitpick [expect = genuine] oops lemma "\a. g a = a diff -r 8f9a66fc9f80 -r 99cd1f96b400 src/HOL/Nitpick_Examples/Typedef_Nits.thy --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Feb 23 11:05:32 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Feb 23 12:14:29 2010 +0100 @@ -143,11 +143,11 @@ by (rule Rep_Sum_inverse) lemma "0::nat \ Abs_Nat Zero_Rep" -(* nitpick [expect = none] FIXME *) +nitpick [expect = none] by (rule Zero_nat_def_raw) lemma "Suc \ \n. Abs_Nat (Suc_Rep (Rep_Nat n))" -(* nitpick [expect = none] FIXME *) +nitpick [expect = none] by (rule Suc_def) lemma "Suc \ \n. Abs_Nat (Suc_Rep (Suc_Rep (Rep_Nat n)))" diff -r 8f9a66fc9f80 -r 99cd1f96b400 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Feb 23 11:05:32 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Feb 23 12:14:29 2010 +0100 @@ -1595,12 +1595,7 @@ KK.Atom (offset_of_type ofs nat_T) else fold kk_join (map to_integer [u1, u2]) (KK.Rel nat_subtract_rel) - | Op2 (Apply, _, R, u1, u2) => - if is_Cst Unrep u2 andalso is_set_type (type_of u1) andalso - is_FreeName u1 then - false_atom - else - to_apply R u1 u2 + | Op2 (Apply, _, R, u1, u2) => to_apply R u1 u2 | Op2 (Lambda, _, R as Opt (Atom (1, j0)), u1, u2) => to_guard [u1, u2] R (KK.Atom j0) | Op2 (Lambda, _, Func (_, Formula Neut), u1, u2) => diff -r 8f9a66fc9f80 -r 99cd1f96b400 src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Feb 23 11:05:32 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Feb 23 12:14:29 2010 +0100 @@ -95,7 +95,6 @@ val nickname_of : nut -> string val is_skolem_name : nut -> bool val is_eval_name : nut -> bool - val is_FreeName : nut -> bool val is_Cst : cst -> nut -> bool val fold_nut : (nut -> 'a -> 'a) -> nut -> 'a -> 'a val map_nut : (nut -> nut) -> nut -> nut @@ -369,8 +368,6 @@ fun is_eval_name u = String.isPrefix eval_prefix (nickname_of u) handle NUT ("Nitpick_Nut.nickname_of", _) => false -fun is_FreeName (FreeName _) = true - | is_FreeName _ = false (* cst -> nut -> bool *) fun is_Cst cst (Cst (cst', _, _)) = (cst = cst') | is_Cst _ _ = false @@ -794,9 +791,9 @@ end (* A nut is said to be constructive if whenever it evaluates to unknown in our - three-valued logic, it would evaluate to a unrepresentable value ("unrep") + three-valued logic, it would evaluate to a unrepresentable value ("Unrep") according to the HOL semantics. For example, "Suc n" is constructive if "n" - is representable or "Unrep", because unknown implies unrep. *) + is representable or "Unrep", because unknown implies "Unrep". *) (* nut -> bool *) fun is_constructive u = is_Cst Unrep u orelse @@ -819,6 +816,16 @@ fun unknown_boolean T R = Cst (case R of Formula Pos => False | Formula Neg => True | _ => Unknown, T, R) +(* nut -> bool *) +fun is_fully_representable_set u = + not (is_opt_rep (rep_of u)) andalso + case u of + FreeName _ => true + | Op1 (SingletonSet, _, _, _) => true + | Op2 (oper, _, _, u1, u2) => + member (op =) [Union, SetDifference, Intersect] oper andalso + forall is_fully_representable_set [u1, u2] + | _ => false (* op1 -> typ -> rep -> nut -> nut *) fun s_op1 oper T R u1 = @@ -860,7 +867,7 @@ if is_constructive u1 then Cst (Unrep, T, R) else if is_boolean_type T then - if is_FreeName u1 then Cst (False, T, Formula Neut) + if is_fully_representable_set u1 then Cst (False, T, Formula Neut) else unknown_boolean T R else case u1 of Op2 (Apply, _, _, ConstName (@{const_name List.append}, _, _), _) => diff -r 8f9a66fc9f80 -r 99cd1f96b400 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Feb 23 11:05:32 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Feb 23 12:14:29 2010 +0100 @@ -1091,7 +1091,8 @@ else accum |> fold (add_nondef_axiom depth) (nondef_props_for_const thy false nondef_table x) - |> is_funky_typedef thy (range_type T) + |> (is_funky_typedef thy (range_type T) orelse + range_type T = nat_T) ? fold (add_maybe_def_axiom depth) (nondef_props_for_const thy true (extra_table def_table s) x) @@ -1101,7 +1102,8 @@ else accum |> fold (add_nondef_axiom depth) (nondef_props_for_const thy false nondef_table x) - |> is_funky_typedef thy (range_type T) + |> (is_funky_typedef thy (range_type T) orelse + range_type T = nat_T) ? fold (add_maybe_def_axiom depth) (nondef_props_for_const thy true (extra_table def_table s) x)