# HG changeset patch # User blanchet # Date 1268140701 -3600 # Node ID ed2c3830d8817205f7150c38f58c178f2930ff7e # Parent ff2bf50505aba3d34980168eae9eebf8c229c733 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1" diff -r ff2bf50505ab -r ed2c3830d881 src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Tue Mar 09 09:25:23 2010 +0100 +++ b/src/HOL/Nitpick.thy Tue Mar 09 14:18:21 2010 +0100 @@ -36,7 +36,8 @@ and bisim :: "bisim_iterator \ 'a \ 'a \ bool" and bisim_iterator_max :: bisim_iterator and Quot :: "'a \ 'b" - and Tha :: "('a \ bool) \ 'a" + and safe_The :: "('a \ bool) \ 'a" + and safe_Eps :: "('a \ bool) \ 'a" datatype ('a, 'b) fin_fun = FinFun "('a \ 'b)" datatype ('a, 'b) fun_box = FunBox "('a \ 'b)" @@ -237,10 +238,11 @@ setup {* Nitpick_Isar.setup *} hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim - bisim_iterator_max Quot Tha FinFun FunBox PairBox Word refl' wf' wf_wfrec - wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm - Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac - times_frac uminus_frac number_of_frac inverse_frac less_eq_frac of_frac + bisim_iterator_max Quot safe_The safe_Eps FinFun FunBox PairBox Word refl' + wf' wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm + int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom + norm_frac frac plus_frac times_frac uminus_frac number_of_frac inverse_frac + less_eq_frac of_frac hide (open) type bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit word hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def diff -r ff2bf50505ab -r ed2c3830d881 src/HOL/Nitpick_Examples/Induct_Nits.thy --- a/src/HOL/Nitpick_Examples/Induct_Nits.thy Tue Mar 09 09:25:23 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy Tue Mar 09 14:18:21 2010 +0100 @@ -61,7 +61,7 @@ lemma "q2 = {}" nitpick [expect = genuine] nitpick [dont_star_linear_preds, expect = genuine] -nitpick [wf, expect = likely_genuine] +nitpick [wf, expect = quasi_genuine] oops lemma "p2 = UNIV" @@ -72,7 +72,7 @@ lemma "q2 = UNIV" nitpick [expect = none] nitpick [dont_star_linear_preds, expect = none] -nitpick [wf, expect = likely_genuine] +nitpick [wf, expect = quasi_genuine] sorry lemma "p2 = q2" diff -r ff2bf50505ab -r ed2c3830d881 src/HOL/Nitpick_Examples/Manual_Nits.thy --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Mar 09 09:25:23 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Mar 09 14:18:21 2010 +0100 @@ -18,29 +18,29 @@ subsection {* 3.1. Propositional Logic *} lemma "P \ Q" -nitpick +nitpick [expect = genuine] apply auto -nitpick 1 -nitpick 2 +nitpick [expect = genuine] 1 +nitpick [expect = genuine] 2 oops subsection {* 3.2. Type Variables *} lemma "P x \ P (THE y. P y)" -nitpick [verbose] +nitpick [verbose, expect = genuine] oops subsection {* 3.3. Constants *} lemma "P x \ P (THE y. P y)" -nitpick [show_consts] -nitpick [full_descrs, show_consts] -nitpick [dont_specialize, full_descrs, show_consts] +nitpick [show_consts, expect = genuine] +nitpick [full_descrs, show_consts, expect = genuine] +nitpick [dont_specialize, full_descrs, show_consts, expect = genuine] oops lemma "\!x. P x \ P (THE y. P y)" -nitpick -nitpick [card 'a = 1-50] +nitpick [expect = none] +nitpick [card 'a = 1\50, expect = none] (* sledgehammer *) apply (metis the_equality) done @@ -48,45 +48,45 @@ subsection {* 3.4. Skolemization *} lemma "\g. \x. g (f x) = x \ \y. \x. y = f x" -nitpick +nitpick [expect = genuine] oops lemma "\x. \f. f x = x" -nitpick +nitpick [expect = genuine] oops lemma "refl r \ sym r" -nitpick +nitpick [expect = genuine] oops subsection {* 3.5. Natural Numbers and Integers *} lemma "\i \ j; n \ (m\int)\ \ i * n + j * m \ i * m + j * n" -nitpick +nitpick [expect = genuine] oops lemma "\n. Suc n \ n \ P" -nitpick [card nat = 100, check_potential] +nitpick [card nat = 100, check_potential, expect = genuine] oops lemma "P Suc" -nitpick +nitpick [expect = none] oops lemma "P (op +\nat\nat\nat)" -nitpick [card nat = 1] -nitpick [card nat = 2] +nitpick [card nat = 1, expect = genuine] +nitpick [card nat = 2, expect = none] oops subsection {* 3.6. Inductive Datatypes *} lemma "hd (xs @ [y, y]) = hd xs" -nitpick -nitpick [show_consts, show_datatypes] +nitpick [expect = genuine] +nitpick [show_consts, show_datatypes, expect = genuine] oops lemma "\length xs = 1; length ys = 1\ \ xs = ys" -nitpick [show_datatypes] +nitpick [show_datatypes, expect = genuine] oops subsection {* 3.7. Typedefs, Records, Rationals, and Reals *} @@ -99,7 +99,7 @@ definition C :: three where "C \ Abs_three 2" lemma "\P A; P B\ \ P x" -nitpick [show_datatypes] +nitpick [show_datatypes, expect = genuine] oops fun my_int_rel where @@ -114,7 +114,7 @@ quotient_definition "add\my_int \ my_int \ my_int" is add_raw lemma "add x y = add x x" -nitpick [show_datatypes] +nitpick [show_datatypes, expect = genuine] oops record point = @@ -122,11 +122,11 @@ Ycoord :: int lemma "Xcoord (p\point) = Xcoord (q\point)" -nitpick [show_datatypes] +nitpick [show_datatypes, expect = genuine] oops lemma "4 * x + 3 * (y\real) \ 1 / 2" -nitpick [show_datatypes] +nitpick [show_datatypes, expect = genuine] oops subsection {* 3.8. Inductive and Coinductive Predicates *} @@ -136,11 +136,11 @@ "even n \ even (Suc (Suc n))" lemma "\n. even n \ even (Suc n)" -nitpick [card nat = 100, unary_ints, verbose] +nitpick [card nat = 100, unary_ints, verbose, expect = potential] oops lemma "\n \ 99. even n \ even (Suc n)" -nitpick [card nat = 100, unary_ints, verbose] +nitpick [card nat = 100, unary_ints, verbose, expect = genuine] oops inductive even' where @@ -149,18 +149,18 @@ "\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] +nitpick [card nat = 10, unary_ints, verbose, show_consts, expect = genuine] oops lemma "even' (n - 2) \ even' n" -nitpick [card nat = 10, show_consts] +nitpick [card nat = 10, show_consts, expect = genuine] oops coinductive nats where "nats (x\nat) \ nats x" lemma "nats = {0, 1, 2, 3, 4}" -nitpick [card nat = 10, show_consts] +nitpick [card nat = 10, show_consts, expect = genuine] oops inductive odd where @@ -168,7 +168,7 @@ "\odd m; even n\ \ odd (m + n)" lemma "odd n \ odd (n - 2)" -nitpick [card nat = 10, show_consts] +nitpick [card nat = 10, show_consts, expect = genuine] oops subsection {* 3.9. Coinductive Datatypes *} @@ -179,7 +179,8 @@ typedef 'a llist = "UNIV\('a list + (nat \ 'a)) set" by auto -definition LNil where "LNil = Abs_llist (Inl [])" +definition LNil where +"LNil = Abs_llist (Inl [])" definition LCons where "LCons y ys = Abs_llist (case Rep_llist ys of Inl ys' \ Inl (y # ys') @@ -197,16 +198,16 @@ *} lemma "xs \ LCons a xs" -nitpick +nitpick [expect = genuine] oops lemma "\xs = LCons a xs; ys = iterates (\b. a) b\ \ xs = ys" -nitpick [verbose] +nitpick [verbose, expect = genuine] oops lemma "\xs = LCons a xs; ys = LCons a ys\ \ xs = ys" -nitpick [bisim_depth = -1, show_datatypes] -nitpick +nitpick [bisim_depth = -1, show_datatypes, expect = quasi_genuine] +nitpick [expect = none] sorry subsection {* 3.10. Boxing *} @@ -230,9 +231,9 @@ "subst\<^isub>1 \ (App t u) = App (subst\<^isub>1 \ t) (subst\<^isub>1 \ u)" lemma "\ loose t 0 \ subst\<^isub>1 \ t = t" -nitpick [verbose] -nitpick [eval = "subst\<^isub>1 \ t"] -(* nitpick [dont_box] *) +nitpick [verbose, expect = genuine] +nitpick [eval = "subst\<^isub>1 \ t", expect = genuine] +(* nitpick [dont_box, expect = unknown] *) oops primrec subst\<^isub>2 where @@ -242,19 +243,19 @@ "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\6] +nitpick [card = 1\6, expect = none] sorry subsection {* 3.11. Scope Monotonicity *} lemma "length xs = length ys \ rev (zip xs ys) = zip xs (rev ys)" -nitpick [verbose] -nitpick [card = 8, verbose] +nitpick [verbose, expect = genuine] +nitpick [card = 8, verbose, expect = genuine] oops lemma "\g. \x\'b. g (f x) = x \ \y\'a. \x. y = f x" -nitpick [mono] -nitpick +nitpick [mono, expect = none] +nitpick [expect = genuine] oops subsection {* 3.12. Inductive Properties *} @@ -265,21 +266,21 @@ "n \ reach \ n + 2 \ reach" lemma "n \ reach \ 2 dvd n" -nitpick [unary_ints] +nitpick [unary_ints, expect = none] apply (induct set: reach) apply auto - nitpick + nitpick [expect = none] apply (thin_tac "n \ reach") - nitpick + nitpick [expect = genuine] oops lemma "n \ reach \ 2 dvd n \ n \ 0" -nitpick [unary_ints] +nitpick [unary_ints, expect = none] apply (induct set: reach) apply auto - nitpick + nitpick [expect = none] apply (thin_tac "n \ reach") - nitpick + nitpick [expect = genuine] oops lemma "n \ reach \ 2 dvd n \ n \ 4" @@ -297,13 +298,13 @@ "swap (Branch t u) a b = Branch (swap t a b) (swap u a b)" lemma "{a, b} \ labels t \ labels (swap t a b) = labels t" -nitpick +(* nitpick *) proof (induct t) case Leaf thus ?case by simp next case (Branch t u) thus ?case - nitpick - nitpick [non_std, show_all] + (* nitpick *) + nitpick [non_std, show_all, expect = genuine] oops lemma "labels (swap t a b) = @@ -338,7 +339,7 @@ theorem S\<^isub>1_sound: "w \ S\<^isub>1 \ length [x \ w. x = a] = length [x \ w. x = b]" -nitpick +nitpick [expect = genuine] oops inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where @@ -351,7 +352,7 @@ theorem S\<^isub>2_sound: "w \ S\<^isub>2 \ length [x \ w. x = a] = length [x \ w. x = b]" -nitpick +nitpick [expect = genuine] oops inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where @@ -369,7 +370,7 @@ theorem S\<^isub>3_complete: "length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^isub>3" -nitpick +nitpick [expect = genuine] oops inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where @@ -465,11 +466,11 @@ (if x > y then insort\<^isub>1 u x else u))" theorem wf_insort\<^isub>1: "wf t \ wf (insort\<^isub>1 t x)" -nitpick +nitpick [expect = genuine] oops theorem wf_insort\<^isub>1_nat: "wf t \ wf (insort\<^isub>1 t (x\nat))" -nitpick [eval = "insort\<^isub>1 t x"] +nitpick [eval = "insort\<^isub>1 t x", expect = genuine] oops primrec insort\<^isub>2 where diff -r ff2bf50505ab -r ed2c3830d881 src/HOL/Tools/Nitpick/HISTORY --- a/src/HOL/Tools/Nitpick/HISTORY Tue Mar 09 09:25:23 2010 +0100 +++ b/src/HOL/Tools/Nitpick/HISTORY Tue Mar 09 14:18:21 2010 +0100 @@ -2,13 +2,13 @@ * Added and implemented "binary_ints" and "bits" options * Added "std" option and implemented support for nonstandard models + * Added and implemented "finitize" option to improve the precision of infinite + datatypes based on a monotonicity analysis * Added support for quotient types - * Added support for local definitions - * Disabled "fast_descrs" option by default + * Added support for local definitions (for "function" and "termination" + proofs) * Optimized "Multiset.multiset" and "FinFun.finfun" * Improved efficiency of "destroy_constrs" optimization - * Improved precision of infinite datatypes whose constructors don't appear - in the formula to falsify based on a monotonicity analysis * Fixed soundness bugs related to "destroy_constrs" optimization and record getters * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to diff -r ff2bf50505ab -r ed2c3830d881 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Mar 09 09:25:23 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Mar 09 14:18:21 2010 +0100 @@ -326,8 +326,6 @@ val sound_finitizes = none_true (filter_out (fn (SOME (Type (@{type_name fun}, _)), _) => true | _ => false) finitizes) - val genuine_means_genuine = - got_all_user_axioms andalso none_true wfs andalso sound_finitizes val standard = forall snd stds (* val _ = List.app (priority o string_for_nut ctxt) (nondef_us @ def_us) @@ -603,7 +601,7 @@ fun show_kodkod_warning "" = () | show_kodkod_warning s = print_m (fn () => "Kodkod warning: " ^ s ^ ".") - (* bool -> KK.raw_bound list -> problem_extension -> bool option *) + (* bool -> KK.raw_bound list -> problem_extension -> bool * bool option *) fun print_and_check_model genuine bounds ({free_names, sel_names, nonsel_names, rel_table, scope, ...} : problem_extension) = @@ -614,119 +612,126 @@ show_consts = show_consts} scope formats frees free_names sel_names nonsel_names rel_table bounds - val genuine_means_genuine = genuine_means_genuine andalso codatatypes_ok + val genuine_means_genuine = + got_all_user_axioms andalso none_true wfs andalso + sound_finitizes andalso codatatypes_ok in - pprint (Pretty.chunks - [Pretty.blk (0, - (pstrs ("Nitpick found a" ^ - (if not genuine then " potential " - else if genuine_means_genuine then " " - else " likely genuine ") ^ das_wort_model) @ - (case pretties_for_scope scope verbose of - [] => [] - | pretties => pstrs " for " @ pretties) @ - [Pretty.str ":\n"])), - Pretty.indent indent_size reconstructed_model]); - if genuine then - (if check_genuine andalso standard then - (case prove_hol_model scope tac_timeout free_names sel_names + (pprint (Pretty.chunks + [Pretty.blk (0, + (pstrs ("Nitpick found a" ^ + (if not genuine then " potential " + else if genuine_means_genuine then " " + else " quasi genuine ") ^ das_wort_model) @ + (case pretties_for_scope scope verbose of + [] => [] + | pretties => pstrs " for " @ pretties) @ + [Pretty.str ":\n"])), + Pretty.indent indent_size reconstructed_model]); + if genuine then + (if check_genuine andalso standard then + case prove_hol_model scope tac_timeout free_names sel_names rel_table bounds assms_t of - SOME true => print ("Confirmation by \"auto\": The above " ^ - das_wort_model ^ " is really genuine.") + SOME true => + print ("Confirmation by \"auto\": The above " ^ + das_wort_model ^ " is really genuine.") | SOME false => if genuine_means_genuine then error ("A supposedly genuine " ^ das_wort_model ^ " was \ \shown to be spurious by \"auto\".\nThis should never \ \happen.\nPlease send a bug report to blanchet\ \te@in.tum.de.") - else - print ("Refutation by \"auto\": The above " ^ das_wort_model ^ - " is spurious.") - | NONE => print "No confirmation by \"auto\".") - else - (); - if not standard andalso likely_in_struct_induct_step then - print "The existence of a nonstandard model suggests that the \ - \induction hypothesis is not general enough or perhaps even \ - \wrong. See the \"Inductive Properties\" section of the \ - \Nitpick manual for details (\"isabelle doc nitpick\")." - else - (); - if has_syntactic_sorts orig_t then - print "Hint: Maybe you forgot a type constraint?" + else + print ("Refutation by \"auto\": The above " ^ + das_wort_model ^ " is spurious.") + | NONE => print "No confirmation by \"auto\"." + else + (); + if not standard andalso likely_in_struct_induct_step then + print "The existence of a nonstandard model suggests that the \ + \induction hypothesis is not general enough or perhaps \ + \even wrong. See the \"Inductive Properties\" section of \ + \the Nitpick manual for details (\"isabelle doc nitpick\")." + else + (); + if has_syntactic_sorts orig_t then + print "Hint: Maybe you forgot a type constraint?" + else + (); + if not genuine_means_genuine then + if no_poly_user_axioms then + let + val options = + [] |> not got_all_mono_user_axioms + ? cons ("user_axioms", "\"true\"") + |> not (none_true wfs) + ? cons ("wf", "\"smart\" or \"false\"") + |> not sound_finitizes + ? cons ("finitize", "\"smart\" or \"false\"") + |> not codatatypes_ok + ? cons ("bisim_depth", "a nonnegative value") + val ss = + map (fn (name, value) => quote name ^ " set to " ^ value) + options + in + print ("Try again with " ^ + space_implode " " (serial_commas "and" ss) ^ + " to confirm that the " ^ das_wort_model ^ + " is genuine.") + end + else + print ("Nitpick is unable to guarantee the authenticity of \ + \the " ^ das_wort_model ^ " in the presence of \ + \polymorphic axioms.") + else + (); + NONE) + else + if not genuine then + (Unsynchronized.inc met_potential; + if check_potential then + let + val status = prove_hol_model scope tac_timeout free_names + sel_names rel_table bounds assms_t + in + (case status of + SOME true => print ("Confirmation by \"auto\": The \ + \above " ^ das_wort_model ^ + " is genuine.") + | SOME false => print ("Refutation by \"auto\": The above " ^ + das_wort_model ^ " is spurious.") + | NONE => print "No confirmation by \"auto\"."); + status + end + else + NONE) else - (); - if not genuine_means_genuine then - if no_poly_user_axioms then - let - val options = - [] |> not got_all_mono_user_axioms - ? cons ("user_axioms", "\"true\"") - |> not (none_true wfs) - ? cons ("wf", "\"smart\" or \"false\"") - |> not sound_finitizes - ? cons ("finitize", "\"smart\" or \"false\"") - |> not codatatypes_ok - ? cons ("bisim_depth", "a nonnegative value") - val ss = - map (fn (name, value) => quote name ^ " set to " ^ value) - options - in - print ("Try again with " ^ - space_implode " " (serial_commas "and" ss) ^ - " to confirm that the " ^ das_wort_model ^ - " is genuine.") - end - else - print ("Nitpick is unable to guarantee the authenticity of \ - \the " ^ das_wort_model ^ " in the presence of \ - \polymorphic axioms.") - else - (); - NONE) - else - if not genuine then - (Unsynchronized.inc met_potential; - if check_potential then - let - val status = prove_hol_model scope tac_timeout free_names - sel_names rel_table bounds assms_t - in - (case status of - SOME true => print ("Confirmation by \"auto\": The above " ^ - das_wort_model ^ " is genuine.") - | SOME false => print ("Refutation by \"auto\": The above " ^ - das_wort_model ^ " is spurious.") - | NONE => print "No confirmation by \"auto\"."); - status - end - else - NONE) - else - NONE + NONE) + |> pair genuine_means_genuine end - (* int -> int -> int -> bool -> rich_problem list -> int * int * int *) - fun solve_any_problem max_potential max_genuine donno first_time problems = + (* bool * int * int * int -> bool -> rich_problem list + -> bool * int * int * int *) + fun solve_any_problem (found_really_genuine, max_potential, max_genuine, + donno) first_time problems = let val max_potential = Int.max (0, max_potential) val max_genuine = Int.max (0, max_genuine) - (* bool -> int * KK.raw_bound list -> bool option *) + (* bool -> int * KK.raw_bound list -> bool * bool option *) fun print_and_check genuine (j, bounds) = print_and_check_model genuine bounds (snd (nth problems j)) val max_solutions = max_potential + max_genuine |> not need_incremental ? curry Int.min 1 in if max_solutions <= 0 then - (0, 0, donno) + (found_really_genuine, 0, 0, donno) else case KK.solve_any_problem overlord deadline max_threads max_solutions (map fst problems) of KK.NotInstalled => (print_m install_kodkodi_message; - (max_potential, max_genuine, donno + 1)) + (found_really_genuine, max_potential, max_genuine, donno + 1)) | KK.Normal ([], unsat_js, s) => (update_checked_problems problems unsat_js; show_kodkod_warning s; - (max_potential, max_genuine, donno)) + (found_really_genuine, max_potential, max_genuine, donno)) | KK.Normal (sat_ps, unsat_js, s) => let val (lib_ps, con_ps) = @@ -736,16 +741,19 @@ show_kodkod_warning s; if null con_ps then let - val num_genuine = take max_potential lib_ps - |> map (print_and_check false) - |> filter (curry (op =) (SOME true)) - |> length + val genuine_codes = + lib_ps |> take max_potential + |> map (print_and_check false) + |> filter (curry (op =) (SOME true) o snd) + val found_really_genuine = + found_really_genuine orelse exists fst genuine_codes + val num_genuine = length genuine_codes val max_genuine = max_genuine - num_genuine val max_potential = max_potential - (length lib_ps - num_genuine) in if max_genuine <= 0 then - (0, 0, donno) + (found_really_genuine, 0, 0, donno) else let (* "co_js" is the list of sound problems whose unsound @@ -765,18 +773,21 @@ |> max_potential <= 0 ? filter_out (#unsound o snd) in - solve_any_problem max_potential max_genuine donno false - problems + solve_any_problem (found_really_genuine, max_potential, + max_genuine, donno) false problems end end else let - val _ = take max_genuine con_ps - |> List.app (ignore o print_and_check true) - val max_genuine = max_genuine - length con_ps + val genuine_codes = + con_ps |> take max_genuine + |> map (print_and_check true) + val max_genuine = max_genuine - length genuine_codes + val found_really_genuine = + found_really_genuine orelse exists fst genuine_codes in if max_genuine <= 0 orelse not first_time then - (0, max_genuine, donno) + (found_really_genuine, 0, max_genuine, donno) else let val bye_js = sort_distinct int_ord @@ -784,7 +795,10 @@ val problems = problems |> filter_out_indices bye_js |> filter_out (#unsound o snd) - in solve_any_problem 0 max_genuine donno false problems end + in + solve_any_problem (found_really_genuine, 0, max_genuine, + donno) false problems + end end end | KK.TimedOut unsat_js => @@ -795,11 +809,13 @@ | KK.Error (s, unsat_js) => (update_checked_problems problems unsat_js; print_v (K ("Kodkod error: " ^ s ^ ".")); - (max_potential, max_genuine, donno + 1)) + (found_really_genuine, max_potential, max_genuine, donno + 1)) end - (* int -> int -> scope list -> int * int * int -> int * int * int *) - fun run_batch j n scopes (max_potential, max_genuine, donno) = + (* int -> int -> scope list -> bool * int * int * int + -> bool * int * int * int *) + fun run_batch j n scopes (found_really_genuine, max_potential, max_genuine, + donno) = let val _ = if null scopes then @@ -869,7 +885,8 @@ else () in - solve_any_problem max_potential max_genuine donno true (rev problems) + solve_any_problem (found_really_genuine, max_potential, max_genuine, + donno) true (rev problems) end (* rich_problem list -> scope -> int *) @@ -901,8 +918,9 @@ "") ^ "." end - (* int -> int -> scope list -> int * int * int -> KK.outcome *) - fun run_batches _ _ [] (max_potential, max_genuine, donno) = + (* int -> int -> scope list -> bool * int * int * int -> KK.outcome *) + fun run_batches _ _ [] + (found_really_genuine, max_potential, max_genuine, donno) = if donno > 0 andalso max_genuine > 0 then (print_m (fn () => excipit "ran out of some resource"); "unknown") else if max_genuine = original_max_genuine then @@ -919,10 +937,12 @@ "Nitpick could not find a" ^ (if max_genuine = 1 then " better " ^ das_wort_model ^ "." else "ny better " ^ das_wort_model ^ "s.")); "potential") + else if found_really_genuine then + "genuine" else - if genuine_means_genuine then "genuine" else "likely_genuine" + "quasi_genuine" | run_batches j n (batch :: batches) z = - let val (z as (_, max_genuine, _)) = run_batch j n batch z in + let val (z as (_, _, max_genuine, _)) = run_batch j n batch z in run_batches (j + 1) n (if max_genuine > 0 then batches else []) z end @@ -942,7 +962,8 @@ val batches = batch_list batch_size (!scopes) val outcome_code = - (run_batches 0 (length batches) batches (max_potential, max_genuine, 0) + (run_batches 0 (length batches) batches + (false, max_potential, max_genuine, 0) handle Exn.Interrupt => do_interrupted ()) handle TimeLimit.TimeOut => (print_m (fn () => excipit "ran out of time"); diff -r ff2bf50505ab -r ed2c3830d881 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Mar 09 09:25:23 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Mar 09 14:18:21 2010 +0100 @@ -361,7 +361,8 @@ (@{const_name finite}, 1), (@{const_name unknown}, 0), (@{const_name is_unknown}, 1), - (@{const_name Tha}, 1), + (@{const_name safe_The}, 1), + (@{const_name safe_Eps}, 1), (@{const_name Frac}, 0), (@{const_name norm_frac}, 0)] val built_in_nat_consts = @@ -1821,7 +1822,7 @@ val bisim_max = @{const bisim_iterator_max} val n_var = Var (("n", 0), iter_T) val n_var_minus_1 = - Const (@{const_name Tha}, (iter_T --> bool_T) --> iter_T) + Const (@{const_name safe_The}, (iter_T --> bool_T) --> iter_T) $ Abs ("m", iter_T, HOLogic.eq_const iter_T $ (suc_const iter_T $ Bound 0) $ n_var) val x_var = Var (("x", 0), T) diff -r ff2bf50505ab -r ed2c3830d881 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Mar 09 09:25:23 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Mar 09 14:18:21 2010 +0100 @@ -1388,7 +1388,7 @@ (Func (R1, Formula Neut)) r)) (to_opt R1 u1) | _ => raise NUT ("Nitpick_Kodkod.to_r (SingletonSet)", [u])) - | Op1 (Tha, _, R, u1) => + | Op1 (SafeThe, _, R, u1) => if is_opt_rep R then kk_join (to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1) true_atom else diff -r ff2bf50505ab -r ed2c3830d881 src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Mar 09 09:25:23 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Mar 09 14:18:21 2010 +0100 @@ -768,12 +768,9 @@ | @{const_name rtrancl} => (print_g "*** rtrancl"; mtype_unsolvable) | @{const_name finite} => - if is_finite_type hol_ctxt T then - let val M1 = mtype_for (domain_type (domain_type T)) in - (MFun (plus_set_mtype_for_dom M1, S Minus, bool_M), accum) - end - else - (print_g "*** finite"; mtype_unsolvable) + let val M1 = mtype_for (domain_type (domain_type T)) in + (MFun (plus_set_mtype_for_dom M1, S Minus, bool_M), accum) + end | @{const_name rel_comp} => let val x = Unsynchronized.inc max_fresh @@ -813,14 +810,15 @@ (MFun (a_set_M, S Minus, MFun (a_to_b_set_M, S Minus, ab_set_M)), accum) end - | @{const_name Tha} => - let - val a_M = mtype_for (domain_type (domain_type T)) - val a_set_M = plus_set_mtype_for_dom a_M - in (MFun (a_set_M, S Minus, a_M), accum) end | _ => - if s = @{const_name minus_class.minus} andalso - is_set_type (domain_type T) then + if s = @{const_name safe_The} orelse + s = @{const_name safe_Eps} then + let + val a_set_M = mtype_for (domain_type T) + val a_M = dest_MFun a_set_M |> #1 + in (MFun (a_set_M, S Minus, a_M), accum) end + else if s = @{const_name minus_class.minus} andalso + is_set_type (domain_type T) then let val set_T = domain_type T val left_set_M = mtype_for set_T @@ -1206,7 +1204,13 @@ in case t of Const (x as (s, T)) => - if member (op =) [@{const_name "=="}, @{const_name "op ="}] s then + if s = @{const_name finite} then + case domain_type T' of + T1' as Type (@{type_name fin_fun}, _) => + Abs (Name.uu, T1', @{const True}) + | _ => Const (s, T') + else if s = @{const_name "=="} orelse + s = @{const_name "op ="} then Const (s, T') else if is_built_in_const thy stds fast_descrs x then coerce_term hol_ctxt Ts T' T t diff -r ff2bf50505ab -r ed2c3830d881 src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Mar 09 09:25:23 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Mar 09 14:18:21 2010 +0100 @@ -39,7 +39,7 @@ Closure | SingletonSet | IsUnknown | - Tha | + SafeThe | First | Second | Cast @@ -158,7 +158,7 @@ Closure | SingletonSet | IsUnknown | - Tha | + SafeThe | First | Second | Cast @@ -232,7 +232,7 @@ | string_for_op1 Closure = "Closure" | string_for_op1 SingletonSet = "SingletonSet" | string_for_op1 IsUnknown = "IsUnknown" - | string_for_op1 Tha = "Tha" + | string_for_op1 SafeThe = "SafeThe" | string_for_op1 First = "First" | string_for_op1 Second = "Second" | string_for_op1 Cast = "Cast" @@ -516,8 +516,15 @@ val t1 = list_comb (t0, ts') val T1 = fastype_of1 (Ts, t1) in Op2 (Apply, range_type T1, Any, sub t1, sub t2) end - (* styp -> term list -> term *) - fun construct (x as (_, T)) ts = + (* op2 -> string -> styp -> term -> nut *) + fun do_description_operator oper undef_s (x as (_, T)) t1 = + if fast_descrs then + Op2 (oper, range_type T, Any, sub t1, + sub (Const (undef_s, range_type T))) + else + do_apply (Const x) [t1] + (* styp -> term list -> nut *) + fun do_construct (x as (_, T)) ts = case num_binder_types T - length ts of 0 => Construct (map ((fn (s', T') => ConstName (s', T', Any)) o nth_sel_for_constr x) @@ -552,18 +559,10 @@ do_quantifier Exist s T t1 | (t0 as Const (@{const_name Ex}, _), [t1]) => sub' (t0 $ eta_expand Ts t1 1) - | (t0 as Const (@{const_name The}, T), [t1]) => - if fast_descrs then - Op2 (The, range_type T, Any, sub t1, - sub (Const (@{const_name undefined_fast_The}, range_type T))) - else - do_apply t0 [t1] - | (t0 as Const (@{const_name Eps}, T), [t1]) => - if fast_descrs then - Op2 (Eps, range_type T, Any, sub t1, - sub (Const (@{const_name undefined_fast_Eps}, range_type T))) - else - do_apply t0 [t1] + | (Const (x as (@{const_name The}, _)), [t1]) => + do_description_operator The @{const_name undefined_fast_The} x t1 + | (Const (x as (@{const_name Eps}, _)), [t1]) => + do_description_operator Eps @{const_name undefined_fast_Eps} x t1 | (Const (@{const_name "op ="}, T), [t1, t2]) => sub_equals T t1 t2 | (Const (@{const_name "op &"}, _), [t1, t2]) => Op2 (And, bool_T, Any, sub' t1, sub' t2) @@ -605,7 +604,7 @@ Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2) | (Const (x as (s as @{const_name Suc}, T)), []) => if is_built_in_const thy stds false x then Cst (Suc, T, Any) - else if is_constr thy stds x then construct x [] + else if is_constr thy stds x then do_construct x [] else ConstName (s, T, Any) | (Const (@{const_name finite}, T), [t1]) => (if is_finite_type hol_ctxt (domain_type T) then @@ -616,7 +615,7 @@ | (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any) | (Const (x as (s as @{const_name zero_class.zero}, T)), []) => if is_built_in_const thy stds false x then Cst (Num 0, T, Any) - else if is_constr thy stds x then construct x [] + else if is_constr thy stds x then do_construct x [] else ConstName (s, T, Any) | (Const (x as (s as @{const_name one_class.one}, T)), []) => if is_built_in_const thy stds false x then Cst (Num 1, T, Any) @@ -670,8 +669,11 @@ | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any) | (Const (@{const_name is_unknown}, _), [t1]) => Op1 (IsUnknown, bool_T, Any, sub t1) - | (Const (@{const_name Tha}, Type (@{type_name fun}, [_, T2])), [t1]) => - Op1 (Tha, T2, Any, sub t1) + | (Const (@{const_name safe_The}, + Type (@{type_name fun}, [_, T2])), [t1]) => + Op1 (SafeThe, T2, Any, sub t1) + | (Const (x as (@{const_name safe_Eps}, _)), [t1]) => + do_description_operator Eps @{const_name undefined_fast_Eps} x t1 | (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any) | (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any) | (Const (@{const_name of_nat}, T as @{typ "nat => int"}), []) => @@ -691,7 +693,7 @@ Op2 (Union, T1, Any, sub t1, sub t2) | (t0 as Const (x as (s, T)), ts) => if is_constr thy stds x then - construct x ts + do_construct x ts else if String.isPrefix numeral_prefix s then Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any) else diff -r ff2bf50505ab -r ed2c3830d881 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Mar 09 09:25:23 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Mar 09 14:18:21 2010 +0100 @@ -221,7 +221,8 @@ $ do_term new_Ts old_Ts polar t2 | Const (s as @{const_name The}, T) => do_description_operator s T | Const (s as @{const_name Eps}, T) => do_description_operator s T - | Const (s as @{const_name Tha}, T) => do_description_operator s T + | Const (s as @{const_name safe_The}, T) => do_description_operator s T + | Const (s as @{const_name safe_Eps}, T) => do_description_operator s T | Const (x as (s, T)) => Const (s, if s = @{const_name converse} orelse s = @{const_name trancl} then