improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
--- 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 \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
and bisim_iterator_max :: bisim_iterator
and Quot :: "'a \<Rightarrow> 'b"
- and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
+ and safe_The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
+ and safe_Eps :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
datatype ('a, 'b) fin_fun = FinFun "('a \<Rightarrow> 'b)"
datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> '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
--- 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"
--- 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 \<longleftrightarrow> 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 \<Longrightarrow> P (THE y. P y)"
-nitpick [verbose]
+nitpick [verbose, expect = genuine]
oops
subsection {* 3.3. Constants *}
lemma "P x \<Longrightarrow> 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 "\<exists>!x. P x \<Longrightarrow> P (THE y. P y)"
-nitpick
-nitpick [card 'a = 1-50]
+nitpick [expect = none]
+nitpick [card 'a = 1\<midarrow>50, expect = none]
(* sledgehammer *)
apply (metis the_equality)
done
@@ -48,45 +48,45 @@
subsection {* 3.4. Skolemization *}
lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
-nitpick
+nitpick [expect = genuine]
oops
lemma "\<exists>x. \<forall>f. f x = x"
-nitpick
+nitpick [expect = genuine]
oops
lemma "refl r \<Longrightarrow> sym r"
-nitpick
+nitpick [expect = genuine]
oops
subsection {* 3.5. Natural Numbers and Integers *}
lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
-nitpick
+nitpick [expect = genuine]
oops
lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> 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 +\<Colon>nat\<Rightarrow>nat\<Rightarrow>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 "\<lbrakk>length xs = 1; length ys = 1\<rbrakk> \<Longrightarrow> 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 \<equiv> Abs_three 2"
lemma "\<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P x"
-nitpick [show_datatypes]
+nitpick [show_datatypes, expect = genuine]
oops
fun my_int_rel where
@@ -114,7 +114,7 @@
quotient_definition "add\<Colon>my_int \<Rightarrow> my_int \<Rightarrow> 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\<Colon>point) = Xcoord (q\<Colon>point)"
-nitpick [show_datatypes]
+nitpick [show_datatypes, expect = genuine]
oops
lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
-nitpick [show_datatypes]
+nitpick [show_datatypes, expect = genuine]
oops
subsection {* 3.8. Inductive and Coinductive Predicates *}
@@ -136,11 +136,11 @@
"even n \<Longrightarrow> even (Suc (Suc n))"
lemma "\<exists>n. even n \<and> even (Suc n)"
-nitpick [card nat = 100, unary_ints, verbose]
+nitpick [card nat = 100, unary_ints, verbose, expect = potential]
oops
lemma "\<exists>n \<le> 99. even n \<and> 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 @@
"\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> 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) \<Longrightarrow> even' n"
-nitpick [card nat = 10, show_consts]
+nitpick [card nat = 10, show_consts, expect = genuine]
oops
coinductive nats where
"nats (x\<Colon>nat) \<Longrightarrow> 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 @@
"\<lbrakk>odd m; even n\<rbrakk> \<Longrightarrow> odd (m + n)"
lemma "odd n \<Longrightarrow> 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\<Colon>('a list + (nat \<Rightarrow> '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' \<Rightarrow> Inl (y # ys')
@@ -197,16 +198,16 @@
*}
lemma "xs \<noteq> LCons a xs"
-nitpick
+nitpick [expect = genuine]
oops
lemma "\<lbrakk>xs = LCons a xs; ys = iterates (\<lambda>b. a) b\<rbrakk> \<Longrightarrow> xs = ys"
-nitpick [verbose]
+nitpick [verbose, expect = genuine]
oops
lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> 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 \<sigma> (App t u) = App (subst\<^isub>1 \<sigma> t) (subst\<^isub>1 \<sigma> u)"
lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>1 \<sigma> t = t"
-nitpick [verbose]
-nitpick [eval = "subst\<^isub>1 \<sigma> t"]
-(* nitpick [dont_box] *)
+nitpick [verbose, expect = genuine]
+nitpick [eval = "subst\<^isub>1 \<sigma> t", expect = genuine]
+(* nitpick [dont_box, expect = unknown] *)
oops
primrec subst\<^isub>2 where
@@ -242,19 +243,19 @@
"subst\<^isub>2 \<sigma> (App t u) = App (subst\<^isub>2 \<sigma> t) (subst\<^isub>2 \<sigma> u)"
lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>2 \<sigma> t = t"
-nitpick [card = 1\<midarrow>6]
+nitpick [card = 1\<midarrow>6, expect = none]
sorry
subsection {* 3.11. Scope Monotonicity *}
lemma "length xs = length ys \<Longrightarrow> 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 "\<exists>g. \<forall>x\<Colon>'b. g (f x) = x \<Longrightarrow> \<forall>y\<Colon>'a. \<exists>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 \<in> reach \<Longrightarrow> n + 2 \<in> reach"
lemma "n \<in> reach \<Longrightarrow> 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 \<in> reach")
- nitpick
+ nitpick [expect = genuine]
oops
lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<noteq> 0"
-nitpick [unary_ints]
+nitpick [unary_ints, expect = none]
apply (induct set: reach)
apply auto
- nitpick
+ nitpick [expect = none]
apply (thin_tac "n \<in> reach")
- nitpick
+ nitpick [expect = genuine]
oops
lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4"
@@ -297,13 +298,13 @@
"swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
lemma "{a, b} \<subseteq> labels t \<Longrightarrow> 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 \<in> S\<^isub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> 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 \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> 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 \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> 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 \<Longrightarrow> wf (insort\<^isub>1 t x)"
-nitpick
+nitpick [expect = genuine]
oops
theorem wf_insort\<^isub>1_nat: "wf t \<Longrightarrow> wf (insort\<^isub>1 t (x\<Colon>nat))"
-nitpick [eval = "insort\<^isub>1 t x"]
+nitpick [eval = "insort\<^isub>1 t x", expect = genuine]
oops
primrec insort\<^isub>2 where
--- 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
--- 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");
--- 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)
--- 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
--- 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
--- 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
--- 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