--- a/src/HOL/Divides.thy Tue Mar 09 14:36:41 2010 +0100
+++ b/src/HOL/Divides.thy Tue Mar 09 20:23:19 2010 +0100
@@ -376,7 +376,7 @@
end
-class ring_div = semiring_div + idom
+class ring_div = semiring_div + comm_ring_1
begin
text {* Negation respects modular equivalence. *}
@@ -2353,47 +2353,6 @@
apply (rule Divides.div_less_dividend, simp_all)
done
-text {* code generator setup *}
-
-context ring_1
-begin
-
-lemma of_int_num [code]:
- "of_int k = (if k = 0 then 0 else if k < 0 then
- - of_int (- k) else let
- (l, m) = divmod_int k 2;
- l' = of_int l
- in if m = 0 then l' + l' else l' + l' + 1)"
-proof -
- have aux1: "k mod (2\<Colon>int) \<noteq> (0\<Colon>int) \<Longrightarrow>
- of_int k = of_int (k div 2 * 2 + 1)"
- proof -
- have "k mod 2 < 2" by (auto intro: pos_mod_bound)
- moreover have "0 \<le> k mod 2" by (auto intro: pos_mod_sign)
- moreover assume "k mod 2 \<noteq> 0"
- ultimately have "k mod 2 = 1" by arith
- moreover have "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
- ultimately show ?thesis by auto
- qed
- have aux2: "\<And>x. of_int 2 * x = x + x"
- proof -
- fix x
- have int2: "(2::int) = 1 + 1" by arith
- show "of_int 2 * x = x + x"
- unfolding int2 of_int_add left_distrib by simp
- qed
- have aux3: "\<And>x. x * of_int 2 = x + x"
- proof -
- fix x
- have int2: "(2::int) = 1 + 1" by arith
- show "x * of_int 2 = x + x"
- unfolding int2 of_int_add right_distrib by simp
- qed
- from aux1 show ?thesis by (auto simp add: divmod_int_mod_div Let_def aux2 aux3)
-qed
-
-end
-
lemma zmod_eq_dvd_iff: "(x::int) mod n = y mod n \<longleftrightarrow> n dvd x - y"
proof
assume H: "x mod n = y mod n"
@@ -2482,6 +2441,7 @@
mod_div_equality' [THEN eq_reflection]
zmod_zdiv_equality' [THEN eq_reflection]
+
subsubsection {* Code generation *}
definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
@@ -2515,6 +2475,45 @@
then show ?thesis by (simp add: divmod_int_pdivmod)
qed
+context ring_1
+begin
+
+lemma of_int_num [code]:
+ "of_int k = (if k = 0 then 0 else if k < 0 then
+ - of_int (- k) else let
+ (l, m) = divmod_int k 2;
+ l' = of_int l
+ in if m = 0 then l' + l' else l' + l' + 1)"
+proof -
+ have aux1: "k mod (2\<Colon>int) \<noteq> (0\<Colon>int) \<Longrightarrow>
+ of_int k = of_int (k div 2 * 2 + 1)"
+ proof -
+ have "k mod 2 < 2" by (auto intro: pos_mod_bound)
+ moreover have "0 \<le> k mod 2" by (auto intro: pos_mod_sign)
+ moreover assume "k mod 2 \<noteq> 0"
+ ultimately have "k mod 2 = 1" by arith
+ moreover have "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
+ ultimately show ?thesis by auto
+ qed
+ have aux2: "\<And>x. of_int 2 * x = x + x"
+ proof -
+ fix x
+ have int2: "(2::int) = 1 + 1" by arith
+ show "of_int 2 * x = x + x"
+ unfolding int2 of_int_add left_distrib by simp
+ qed
+ have aux3: "\<And>x. x * of_int 2 = x + x"
+ proof -
+ fix x
+ have int2: "(2::int) = 1 + 1" by arith
+ show "x * of_int 2 = x + x"
+ unfolding int2 of_int_add right_distrib by simp
+ qed
+ from aux1 show ?thesis by (auto simp add: divmod_int_mod_div Let_def aux2 aux3)
+qed
+
+end
+
code_modulename SML
Divides Arith
--- a/src/HOL/Nitpick.thy Tue Mar 09 14:36:41 2010 +0100
+++ b/src/HOL/Nitpick.thy Tue Mar 09 20:23:19 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 14:36:41 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy Tue Mar 09 20:23:19 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 14:36:41 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Mar 09 20:23:19 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 14:36:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY Tue Mar 09 20:23:19 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 14:36:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Mar 09 20:23:19 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 14:36:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Mar 09 20:23:19 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 14:36:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Mar 09 20:23:19 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 14:36:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Mar 09 20:23:19 2010 +0100
@@ -264,20 +264,22 @@
$ (Const (@{const_name unknown}, ran_T)) $ (t0 $ t1 $ t2 $ t3)))
| fin_fun_body _ _ _ = NONE
-(* mdata -> typ -> typ -> mtyp * sign_atom * mtyp *)
-fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) T1 T2 =
+(* mdata -> bool -> typ -> typ -> mtyp * sign_atom * mtyp *)
+fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) all_minus
+ T1 T2 =
let
- val M1 = fresh_mtype_for_type mdata T1
- val M2 = fresh_mtype_for_type mdata T2
- val a = if is_fin_fun_supported_type (body_type T2) andalso
- exists_alpha_sub_mtype_fresh M1 then
+ val M1 = fresh_mtype_for_type mdata all_minus T1
+ val M2 = fresh_mtype_for_type mdata all_minus T2
+ val a = if not all_minus andalso exists_alpha_sub_mtype_fresh M1 andalso
+ is_fin_fun_supported_type (body_type T2) then
V (Unsynchronized.inc max_fresh)
else
S Minus
in (M1, a, M2) end
-(* mdata -> typ -> mtyp *)
+(* mdata -> bool -> typ -> mtyp *)
and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T,
- datatype_mcache, constr_mcache, ...}) =
+ datatype_mcache, constr_mcache, ...})
+ all_minus =
let
(* typ -> mtyp *)
fun do_type T =
@@ -285,7 +287,7 @@
MAlpha
else case T of
Type (@{type_name fun}, [T1, T2]) =>
- MFun (fresh_mfun_for_fun_type mdata T1 T2)
+ MFun (fresh_mfun_for_fun_type mdata false T1 T2)
| Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2))
| Type (z as (s, _)) =>
if could_exist_alpha_sub_mtype thy alpha_T T then
@@ -347,14 +349,14 @@
case AList.lookup (op =) (!constr_mcache) x of
SOME M => M
| NONE => if T = alpha_T then
- let val M = fresh_mtype_for_type mdata T in
+ let val M = fresh_mtype_for_type mdata false T in
(Unsynchronized.change constr_mcache (cons (x, M)); M)
end
else
- (fresh_mtype_for_type mdata (body_type T);
+ (fresh_mtype_for_type mdata false (body_type T);
AList.lookup (op =) (!constr_mcache) x |> the)
else
- fresh_mtype_for_type mdata T
+ fresh_mtype_for_type mdata false T
fun mtype_for_sel (mdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
|> mtype_for_constr mdata |> sel_mtype_from_constr_mtype s
@@ -629,7 +631,7 @@
alpha_T, max_fresh, ...}) =
let
(* typ -> mtyp *)
- val mtype_for = fresh_mtype_for_type mdata
+ val mtype_for = fresh_mtype_for_type mdata false
(* mtyp -> mtyp *)
fun plus_set_mtype_for_dom M =
MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M)
@@ -765,15 +767,6 @@
val ba_set_M = range_type T |> mtype_for_set
in (MFun (ab_set_M, S Minus, ba_set_M), accum) end
| @{const_name trancl} => do_fragile_set_operation T accum
- | @{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)
| @{const_name rel_comp} =>
let
val x = Unsynchronized.inc max_fresh
@@ -796,6 +789,10 @@
MFun (plus_set_mtype_for_dom a_M, S Minus,
plus_set_mtype_for_dom b_M)), accum)
end
+ | @{const_name finite} =>
+ 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 Sigma} =>
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
@@ -842,13 +840,8 @@
(mtype_for_sel mdata x, accum)
else if is_constr thy stds x then
(mtype_for_constr mdata x, accum)
- else if is_built_in_const thy stds fast_descrs x andalso
- s <> @{const_name is_unknown} andalso
- s <> @{const_name unknown} then
- (* the "unknown" part is a hack *)
- case def_of_const thy def_table x of
- SOME t' => do_term t' accum |>> mtype_of_mterm
- | NONE => (print_g ("*** built-in " ^ s); mtype_unsolvable)
+ else if is_built_in_const thy stds fast_descrs x then
+ (fresh_mtype_for_type mdata true T, accum)
else
let val M = mtype_for T in
(M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
@@ -936,7 +929,7 @@
val M1 = mtype_of_mterm m1
val M2 = mtype_of_mterm m2
val accum = accum ||> add_mtypes_equal M1 M2
- val body_M = fresh_mtype_for_type mdata (nth_range_type 2 T)
+ val body_M = fresh_mtype_for_type mdata false (nth_range_type 2 T)
val m = MApp (MApp (MRaw (Const x,
MFun (M1, S Minus, MFun (M2, S Minus, body_M))), m1), m2)
in
@@ -952,7 +945,7 @@
fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, ...}) =
let
(* typ -> mtyp *)
- val mtype_for = fresh_mtype_for_type mdata
+ val mtype_for = fresh_mtype_for_type mdata false
(* term -> accumulator -> mterm * accumulator *)
val do_term = consider_term mdata
(* sign -> term -> accumulator -> mterm * accumulator *)
@@ -1059,7 +1052,7 @@
else
let
(* typ -> mtyp *)
- val mtype_for = fresh_mtype_for_type mdata
+ val mtype_for = fresh_mtype_for_type mdata false
(* term -> accumulator -> mterm * accumulator *)
val do_term = consider_term mdata
(* term -> string -> typ -> term -> accumulator -> mterm * accumulator *)
@@ -1205,8 +1198,26 @@
val T' = type_from_mtype T M
in
case t of
- Const (x as (s, T)) =>
- if member (op =) [@{const_name "=="}, @{const_name "op ="}] s then
+ Const (x as (s, _)) =>
+ if s = @{const_name insert} then
+ case nth_range_type 2 T' of
+ set_T' as Type (@{type_name fin_fun}, [elem_T', _]) =>
+ Abs (Name.uu, elem_T', Abs (Name.uu, set_T',
+ Const (@{const_name If},
+ bool_T --> set_T' --> set_T' --> set_T')
+ $ (Const (@{const_name is_unknown}, elem_T' --> bool_T)
+ $ Bound 1)
+ $ (Const (@{const_name unknown}, set_T'))
+ $ (coerce_term hol_ctxt Ts T' T (Const x)
+ $ Bound 1 $ Bound 0)))
+ | _ => Const (s, T')
+ else if s = @{const_name finite} then
+ case domain_type T' of
+ set_T' as Type (@{type_name fin_fun}, _) =>
+ Abs (Name.uu, set_T', @{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
@@ -1228,16 +1239,6 @@
| _ => raise MTERM ("Nitpick_Mono.finitize_funs.term_from_mterm",
[m])
end
- | MAbs (s, T, M, a, m') =>
- let
- val T = type_from_mtype T M
- val t' = term_from_mterm (T :: Ts) m'
- val T' = fastype_of1 (T :: Ts, t')
- in
- Abs (s, T, t')
- |> should_finitize (T --> T') a
- ? construct_value thy stds (fin_fun_constr T T') o single
- end
| MApp (m1, m2) =>
let
val (t1, t2) = pairself (term_from_mterm Ts) (m1, m2)
@@ -1253,6 +1254,16 @@
| _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm",
[T1], [])
in betapply (t1', coerce_term hol_ctxt Ts T2' T2 t2) end
+ | MAbs (s, T, M, a, m') =>
+ let
+ val T = type_from_mtype T M
+ val t' = term_from_mterm (T :: Ts) m'
+ val T' = fastype_of1 (T :: Ts, t')
+ in
+ Abs (s, T, t')
+ |> should_finitize (T --> T') a
+ ? construct_value thy stds (fin_fun_constr T T') o single
+ end
in
Unsynchronized.change constr_cache (map (apsnd (map finitize_constr)));
pairself (map (term_from_mterm [])) msp
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Mar 09 14:36:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Mar 09 20:23:19 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 14:36:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Mar 09 20:23:19 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
@@ -1341,6 +1342,8 @@
let
val Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
|> filter_out (fn Type (@{type_name fun_box}, _) => true
+ | @{typ signed_bit} => true
+ | @{typ unsigned_bit} => true
| T => is_small_finite_type hol_ctxt T orelse
triple_lookup (type_match thy) monos T
= SOME (SOME false))
--- a/src/HOL/Tools/transfer.ML Tue Mar 09 14:36:41 2010 +0100
+++ b/src/HOL/Tools/transfer.ML Tue Mar 09 20:23:19 2010 +0100
@@ -8,10 +8,11 @@
signature TRANSFER =
sig
datatype selection = Direction of term * term | Hints of string list | Prop
- val transfer: Context.generic -> selection -> string list -> thm -> thm
+ val transfer: Context.generic -> selection -> string list -> thm -> thm list
type entry
- val add: entry * entry -> thm -> Context.generic -> Context.generic
- val del: thm -> Context.generic -> Context.generic
+ val add: thm -> bool -> entry -> Context.generic -> Context.generic
+ val del: thm -> entry -> Context.generic -> Context.generic
+ val drop: thm -> Context.generic -> Context.generic
val setup: theory -> theory
end;
@@ -29,14 +30,15 @@
("Transfer: expected theorem of the form " ^ quote (Display.string_of_thm ctxt @{thm transfer_morphismI}));
in direction_of key end;
-type entry = { inj : thm list, emb : thm list, ret : thm list, cong : thm list,
- guess : bool, hints : string list };
+type entry = { inj : thm list, embed : thm list, return : thm list, cong : thm list,
+ hints : string list };
-fun merge_entry ({ inj = inj1, emb = emb1, ret = ret1, cong = cong1, guess = guess1, hints = hints1 } : entry,
- { inj = inj2, emb = emb2, ret = ret2, cong = cong2, guess = guess2, hints = hints2 } : entry) =
- { inj = merge Thm.eq_thm (inj1, inj2), emb = merge Thm.eq_thm (emb1, emb2),
- ret = merge Thm.eq_thm (ret1, ret2), cong = merge Thm.eq_thm (cong1, cong2),
- guess = guess1 andalso guess2, hints = merge (op =) (hints1, hints2) };
+val empty_entry = { inj = [], embed = [], return = [], cong = [], hints = [] };
+fun merge_entry ({ inj = inj1, embed = embed1, return = return1, cong = cong1, hints = hints1 } : entry,
+ { inj = inj2, embed = embed2, return = return2, cong = cong2, hints = hints2 } : entry) =
+ { inj = merge Thm.eq_thm (inj1, inj2), embed = merge Thm.eq_thm (embed1, embed2),
+ return = merge Thm.eq_thm (return1, return2), cong = merge Thm.eq_thm (cong1, cong2),
+ hints = merge (op =) (hints1, hints2) };
structure Data = Generic_Data
(
@@ -49,6 +51,9 @@
(* data lookup *)
+fun transfer_rules_of { inj, embed, return, cong, ... } =
+ (inj, embed, return, cong);
+
fun get_by_direction context (a, D) =
let
val ctxt = Context.proof_of context;
@@ -58,9 +63,9 @@
fun eq_direction ((a, D), thm') =
let
val (a', D') = direction_of thm';
- in a0 aconvc a' andalso D0 aconvc D' end;
- in case AList.lookup eq_direction (Data.get context) (a, D) of
- SOME e => ((a0, D0), e)
+ in a aconvc a' andalso D aconvc D' end;
+ in case AList.lookup eq_direction (Data.get context) (a0, D0) of
+ SOME e => ((a0, D0), transfer_rules_of e)
| NONE => error ("Transfer: no such instance: ("
^ Syntax.string_of_term ctxt a ^ ", " ^ Syntax.string_of_term ctxt D ^ ")")
end;
@@ -68,7 +73,7 @@
fun get_by_hints context hints =
let
val insts = map_filter (fn (k, e) => if exists (member (op =) (#hints e)) hints
- then SOME (direction_of k, e) else NONE) (Data.get context);
+ then SOME (direction_of k, transfer_rules_of e) else NONE) (Data.get context);
val _ = if null insts then error ("Transfer: no such labels: " ^ commas (map quote hints)) else ();
in insts end;
@@ -84,9 +89,9 @@
val _ = if null tys then error "Transfer: unable to guess instance" else ();
val tyss = splits (curry Type.could_unify) tys;
val get_ty = typ_of o ctyp_of_term o fst o direction_of;
- val insts = map_filter (fn tys => get_first (fn (k, ss) =>
+ val insts = map_filter (fn tys => get_first (fn (k, e) =>
if Type.could_unify (hd tys, range_type (get_ty k))
- then SOME (direction_of k, ss)
+ then SOME (direction_of k, transfer_rules_of e)
else NONE) (Data.get context)) tyss;
val _ = if null insts then
error "Transfer: no instances, provide direction or hints explicitly" else ();
@@ -95,8 +100,7 @@
(* applying transfer data *)
-fun transfer_thm inj_only a0 D0 {inj = inj, emb = emb, ret = ret, cong = cg, guess = _, hints = _}
- leave ctxt0 th =
+fun transfer_thm inj_only ((a0, D0), (inj, embed, return, cong)) leave ctxt0 th =
let
val ([a, D], ctxt) = apfst (map Drule.dest_term o snd)
(Variable.import true (map Drule.mk_term [a0, D0]) ctxt0);
@@ -116,15 +120,14 @@
Thm.capply @{cterm "Trueprop"} (Thm.capply D ct)) cfis) ctxt'';
val th1 = Drule.cterm_instantiate (cns ~~ cis) th;
val th2 = fold Thm.elim_implies hs (fold_rev implies_intr (map cprop_of hs) th1);
- val simpset = (Simplifier.context ctxt''' HOL_ss)
- addsimps inj addsimps (if inj_only then [] else emb @ ret) addcongs cg;
+ val simpset = Simplifier.context ctxt''' HOL_ss
+ addsimps inj addsimps (if inj_only then [] else embed @ return) addcongs cong;
val th3 = Simplifier.asm_full_simplify simpset
(fold_rev implies_intr (map cprop_of hs) th2);
in hd (Variable.export ctxt''' ctxt0 [th3]) end;
fun transfer_thm_multiple inj_only insts leave ctxt thm =
- Conjunction.intr_balanced (map
- (fn ((a, D), e) => transfer_thm false a D e leave ctxt thm) insts);
+ map (fn inst => transfer_thm false inst leave ctxt thm) insts;
datatype selection = Direction of term * term | Hints of string list | Prop;
@@ -138,44 +141,41 @@
(* maintaining transfer data *)
-fun merge_update eq m (k, v) [] = [(k, v)]
- | merge_update eq m (k, v) ((k', v') :: al) =
- if eq (k, k') then (k', m (v, v')) :: al else (k', v') :: merge_update eq m (k, v) al;
-
-(*? fun merge_update eq m (k, v) = AList.map_entry eq k (fn v' => m (v, v'));*)
-
-fun merge_entries {inj = inj0, emb = emb0, ret = ret0, cong = cg0, guess = g0, hints = hints0}
- ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
- {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2} : entry) =
+fun extend_entry ctxt (a, D) guess
+ { inj = inj1, embed = embed1, return = return1, cong = cong1, hints = hints1 }
+ { inj = inj2, embed = embed2, return = return2, cong = cong2, hints = hints2 } =
let
- fun h xs0 xs ys = subtract Thm.eq_thm xs0 (merge Thm.eq_thm (xs, ys))
+ fun add_del eq del add = union eq add #> subtract eq del;
+ val guessed = if guess
+ then map (fn thm => transfer_thm true
+ ((a, D), (if null inj1 then inj2 else inj1, [], [], cong1)) [] ctxt thm RS sym) embed1
+ else [];
in
- {inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2,
- ret = h ret0 ret1 ret2, cong = h cg0 cg1 cg2, guess = g1 andalso g2,
- hints = subtract (op =) hints0 (union (op =) hints1 hints2) }
+ { inj = union Thm.eq_thm inj1 inj2, embed = union Thm.eq_thm embed1 embed2,
+ return = union Thm.eq_thm guessed (union Thm.eq_thm return1 return2),
+ cong = union Thm.eq_thm cong1 cong2, hints = union (op =) hints1 hints2 }
end;
-fun add (e0 as {inj = inja, emb = emba, ret = reta, cong = cga, guess = g, hints = hintsa},
- ed as {inj = injd, emb = embd, ret = retd, cong = cgd, guess = _, hints = hintsd}) key context =
- context
- |> Data.map (fn al =>
- let
- val ctxt = Context.proof_of context;
- val (a0, D0) = check_morphism_key ctxt key;
- val entry = if g then
- let
- val inj' = if null inja then #inj
- (case AList.lookup Thm.eq_thm al key of SOME e => e
- | NONE => error "Transfer: cannot generate return rules on the fly, either add injectivity axiom or force manual mode with mode: manual")
- else inja
- val ret' = merge Thm.eq_thm (reta, map
- (fn th => transfer_thm true a0 D0 {inj = inj', emb = [], ret = [], cong = cga, guess = g,
- hints = hintsa} [] ctxt th RS sym) emba);
- in {inj = inja, emb = emba, ret = ret', cong = cga, guess = g, hints = hintsa} end
- else e0;
- in merge_update Thm.eq_thm (merge_entries ed) (key, entry) al end);
+fun diminish_entry
+ { inj = inj0, embed = embed0, return = return0, cong = cong0, hints = hints0 }
+ { inj = inj2, embed = embed2, return = return2, cong = cong2, hints = hints2 } =
+ { inj = subtract Thm.eq_thm inj0 inj2, embed = subtract Thm.eq_thm embed0 embed2,
+ return = subtract Thm.eq_thm return0 return2, cong = subtract Thm.eq_thm cong0 cong2,
+ hints = subtract (op =) hints0 hints2 };
-fun del key = Data.map (remove (eq_fst Thm.eq_thm) (key, []));
+fun add key guess entry context =
+ let
+ val ctxt = Context.proof_of context;
+ val a_D = check_morphism_key ctxt key;
+ in
+ context
+ |> Data.map (AList.map_default Thm.eq_thm
+ (key, empty_entry) (extend_entry ctxt a_D guess entry))
+ end;
+
+fun del key entry = Data.map (AList.map_entry Thm.eq_thm key (diminish_entry entry));
+
+fun drop key = Data.map (AList.delete Thm.eq_thm key);
(* syntax *)
@@ -188,22 +188,24 @@
fun keyword k = Scan.lift (Args.$$$ k) >> K ();
fun keyword_colon k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
-val congN = "cong";
-val injN = "inj";
-val embedN = "embed";
-val returnN = "return";
val addN = "add";
val delN = "del";
val modeN = "mode";
val automaticN = "automatic";
val manualN = "manual";
-val directionN = "direction";
+val injN = "inj";
+val embedN = "embed";
+val returnN = "return";
+val congN = "cong";
val labelsN = "labels";
-val leavingN = "leaving";
-val any_keyword = keyword_colon congN || keyword_colon injN || keyword_colon embedN
- || keyword_colon returnN || keyword_colon directionN || keyword_colon modeN
- || keyword_colon delN || keyword_colon labelsN || keyword_colon leavingN;
+val leavingN = "leaving";
+val directionN = "direction";
+
+val any_keyword = keyword_colon addN || keyword_colon delN || keyword_colon modeN
+ || keyword_colon injN || keyword_colon embedN || keyword_colon returnN
+ || keyword_colon congN || keyword_colon labelsN
+ || keyword_colon leavingN || keyword_colon directionN;
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
val names = Scan.repeat (Scan.unless any_keyword (Scan.lift Args.name))
@@ -216,23 +218,26 @@
val cong = (keyword_colon congN |-- thms) -- these (keyword_colon delN |-- thms);
val labels = (keyword_colon labelsN |-- names) -- these (keyword_colon delN |-- names);
-val entry_pair = Scan.optional mode true -- these_pair inj -- these_pair embed
+val entry_pair = these_pair inj -- these_pair embed
-- these_pair return -- these_pair cong -- these_pair labels
- >> (fn (((((g, (inja, injd)), (emba, embd)), (reta, retd)), (cga, cgd)), (hintsa, hintsd)) =>
- ({inj = inja, emb = emba, ret = reta, cong = cga, guess = g, hints = hintsa},
- {inj = injd, emb = embd, ret = retd, cong = cgd, guess = g, hints = hintsd}));
+ >> (fn (((((inja, injd), (embeda, embedd)), (returna, returnd)), (conga, congd)),
+ (hintsa, hintsd)) =>
+ ({inj = inja, embed = embeda, return = returna, cong = conga, hints = hintsa},
+ {inj = injd, embed = embedd, return = returnd, cong = congd, hints = hintsd}));
val selection = (keyword_colon directionN |-- (Args.term -- Args.term) >> Direction)
|| these names >> (fn hints => if null hints then Prop else Hints hints);
in
-val transfer_attribute = Scan.lift (Args.$$$ delN >> K (Thm.declaration_attribute del))
- || Scan.unless any_keyword (keyword addN) |-- entry_pair
- >> (fn entry_pair => Thm.declaration_attribute (add entry_pair))
+val transfer_attribute = Scan.lift (Args.$$$ delN >> K (Thm.declaration_attribute drop))
+ || Scan.unless any_keyword (keyword addN) |-- Scan.optional mode true -- entry_pair
+ >> (fn (guess, (entry_add, entry_del)) => Thm.declaration_attribute
+ (fn thm => add thm guess entry_add #> del thm entry_del));
val transferred_attribute = selection -- these (keyword_colon leavingN |-- names)
- >> (fn (selection, leave) => Thm.rule_attribute (fn context => transfer context selection leave));
+ >> (fn (selection, leave) => Thm.rule_attribute (fn context =>
+ Conjunction.intr_balanced o transfer context selection leave));
end;