--- a/src/HOL/MetisExamples/BigO.thy Fri Oct 05 09:59:03 2007 +0200
+++ b/src/HOL/MetisExamples/BigO.thy Fri Oct 05 09:59:21 2007 +0200
@@ -26,7 +26,6 @@
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
apply (rule_tac x = "abs c" in exI, auto);
-txt{*Version 1: one-shot proof. MUCH SLOWER with types: 24 versus 6.7 seconds*}
apply (metis abs_ge_minus_self abs_ge_zero abs_minus_cancel abs_of_nonneg equation_minus_iff Orderings.xt1(6) abs_le_mult)
done
@@ -50,7 +49,7 @@
have 3: "\<And>X1 X3. \<bar>h X3\<bar> < X1 \<or> \<not> c * \<bar>f X3\<bar> < X1"
by (metis order_le_less_trans 0)
have 4: "\<And>X3. (1\<Colon>'a) * X3 \<le> X3 \<or> \<not> (1\<Colon>'a) \<le> (1\<Colon>'a)"
- by (metis mult_le_cancel_right2 order_refl)
+ by (metis mult_le_cancel_right2)
have 5: "\<And>X3. (1\<Colon>'a) * X3 \<le> X3"
by (metis 4 order_refl)
have 6: "\<And>X3. \<bar>0\<Colon>'a\<bar> = \<bar>X3\<bar> * (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (0\<Colon>'a)"
@@ -92,9 +91,9 @@
have 24: "\<And>X3. (0\<Colon>'a) = - X3 \<or> X3 \<noteq> (0\<Colon>'a)"
by (metis 23 minus_equation_iff)
have 25: "\<And>X3. \<bar>0\<Colon>'a\<bar> = \<bar>X3\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
- by (metis abs_minus_cancel 24)
+ by metis
have 26: "\<And>X3. (0\<Colon>'a) = \<bar>X3\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
- by (metis 25 8)
+ by (metis 8)
have 27: "\<And>X1 X3. (0\<Colon>'a) * \<bar>X1\<bar> = \<bar>X3 * X1\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
by (metis abs_mult 26)
have 28: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
@@ -108,7 +107,7 @@
have 32: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<bar>X1\<bar> \<noteq> (0\<Colon>'a)"
by (metis abs_mult 31)
have 33: "\<And>X3::'a. \<bar>X3 * X3\<bar> = X3 * X3"
- by (metis abs_mult_self abs_mult AC_mult.f.commute)
+ by (metis abs_mult_self abs_mult)
have 34: "\<And>X3. (0\<Colon>'a) \<le> \<bar>X3\<bar> \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
by (metis abs_ge_zero abs_mult_pos 20)
have 35: "\<And>X3. (0\<Colon>'a) \<le> \<bar>X3\<bar>"
@@ -1096,13 +1095,11 @@
lemma bigo_const1: "(%x. c) : O(%x. 1)"
by (auto simp add: bigo_def mult_ac)
-declare bigo_const1 [skolem]
-
ML{*ResAtp.problem_name:="BigO__bigo_const2"*}
lemma (*bigo_const2 [intro]:*) "O(%x. c) <= O(%x. 1)"
by (metis bigo_const1 bigo_elt_subset);
-lemma bigo_const2 [intro]: "O(%x. c) <= O(%x. 1)";
+lemma bigo_const2 [intro]: "O(%x. c::'b::ordered_idom) <= O(%x. 1)";
(*??FAILS because the two occurrences of COMBK have different polymorphic types
proof (neg_clausify)
assume 0: "\<not> O(COMBK (c\<Colon>'b\<Colon>ordered_idom)) \<subseteq> O(COMBK (1\<Colon>'b\<Colon>ordered_idom))"
@@ -1121,8 +1118,6 @@
apply (rule bigo_const1)
done
-declare bigo_const2 [skolem]
-
ML{*ResAtp.problem_name := "BigO__bigo_const3"*}
lemma bigo_const3: "(c::'a::ordered_field) ~= 0 ==> (%x. 1) : O(%x. c)"
apply (simp add: bigo_def)
@@ -1535,7 +1530,7 @@
EX C. ALL x. f x <= g x + C * abs(h x)"
apply (simp only: lesso_def bigo_alt_def)
apply clarsimp
- apply (metis abs_if abs_mult add_commute diff_le_eq less_not_permute mult_commute)
+ apply (metis abs_if abs_mult add_commute diff_le_eq less_not_permute)
done
end
--- a/src/HOL/MetisExamples/Tarski.thy Fri Oct 05 09:59:03 2007 +0200
+++ b/src/HOL/MetisExamples/Tarski.thy Fri Oct 05 09:59:21 2007 +0200
@@ -51,14 +51,6 @@
interval :: "[('a*'a) set,'a, 'a ] => 'a set"
"interval r a b == {x. (a,x): r & (x,b): r}"
-declare monotone_def [skolem]
- lub_def [skolem]
- glb_def [skolem]
- isLub_def [skolem]
- isGlb_def [skolem]
- fix_def [skolem]
- interval_def [skolem]
-
constdefs
Bot :: "'a potype => 'a"
"Bot po == least (%x. True) po"
@@ -82,12 +74,6 @@
induced :: "['a set, ('a * 'a) set] => ('a *'a)set"
"induced A r == {(a,b). a : A & b: A & (a,b): r}"
-declare Bot_def [skolem]
- Top_def [skolem]
- PartialOrder_def [skolem]
- CompleteLattice_def [skolem]
- CLF_def [skolem]
-
constdefs
sublattice :: "('a potype * 'a set)set"
"sublattice ==
@@ -204,13 +190,9 @@
lemma isLub_lub: "(\<exists>L. isLub S cl L) = isLub S cl (lub S cl)"
by (simp add: lub_def least_def isLub_def some_eq_ex [symmetric])
-declare isLub_lub [skolem]
-
lemma isGlb_glb: "(\<exists>G. isGlb S cl G) = isGlb S cl (glb S cl)"
by (simp add: glb_def greatest_def isGlb_def some_eq_ex [symmetric])
-declare isGlb_glb [skolem]
-
lemma isGlb_dual_isLub: "isGlb S cl = isLub S (dual cl)"
by (simp add: isLub_def isGlb_def dual_def converse_def)
@@ -235,8 +217,6 @@
apply (simp add: isLub_def, blast)
done
-declare Rdual [skolem]
-
lemma lub_dual_glb: "lub S cl = glb S (dual cl)"
by (simp add: lub_def glb_def least_def greatest_def dual_def converse_def)
@@ -268,8 +248,6 @@
apply (unfold CompleteLattice_def, blast)
done
-declare CompleteLatticeI [skolem]
-
lemma (in CL) CL_dualCL: "dual cl \<in> CompleteLattice"
apply (insert cl_co)
apply (simp add: CompleteLattice_def dual_def)
@@ -378,8 +356,6 @@
apply (simp add: lub_upper lub_least)
done
-declare (in CL) lubI [skolem]
-
lemma (in CL) lubIa: "[| S \<subseteq> A; isLub S cl L |] ==> L = lub S cl"
by (simp add: lubI isLub_def A_def r_def)
@@ -398,8 +374,6 @@
(\<forall>z \<in> A. (\<forall>y \<in> S. (y, z):r) --> (L, z) \<in> r)|] ==> isLub S cl L"
by (simp add: isLub_def A_def r_def)
-declare (in CL) isLub_least [skolem]
-declare (in CL) isLubI [skolem]
subsection {* glb *}
@@ -519,7 +493,7 @@
(*??no longer terminates, with combinators
apply (metis CO_refl lubH_le_flubH monotone_def monotone_f reflD1 reflD2)
*)
-apply (metis CO_refl lubH_le_flubH lub_dual_glb monotoneE [OF monotone_f] reflD1 reflD2)
+apply (metis CO_refl lubH_le_flubH monotoneE [OF monotone_f] reflD1 reflD2)
apply (metis CO_refl lubH_le_flubH reflD2)
done
declare CLF.f_in_funcset[rule del] funcset_mem[rule del]
@@ -605,7 +579,7 @@
apply (simp add: fix_def)
apply (rule conjI)
ML{*ResAtp.problem_name:="Tarski__CLF_lubH_is_fixp_simpler"*}
-apply (metis CO_refl Domain_iff lubH_le_flubH reflD1)
+apply (metis CO_refl lubH_le_flubH reflD1)
apply (metis antisymE flubH_le_lubH lubH_le_flubH)
done
@@ -640,7 +614,7 @@
apply (simp add: P_def)
apply (rule lubI)
ML{*ResAtp.problem_name:="Tarski__CLF_T_thm_1_lub_simpler"*}
-apply (metis P_def equalityE fix_subset subset_trans)
+apply (metis P_def fix_subset)
apply (metis Collect_conj_eq Collect_mem_eq Int_commute Int_lower1 lub_in_lattice vimage_def)
(*??no longer terminates, with combinators
apply (metis P_def fix_def fixf_le_lubH)
@@ -720,15 +694,11 @@
\<forall>x \<in> S. (a,x) \<in> r; \<forall>y \<in> S. (y, L) \<in> r |] ==> (a,L) \<in> r"
by (blast intro: transE)
-declare (in CLF) a_less_lub [skolem]
-
lemma (in CLF) glb_less_b:
"[| S \<subseteq> A; S \<noteq> {};
\<forall>x \<in> S. (x,b) \<in> r; \<forall>y \<in> S. (G, y) \<in> r |] ==> (G,b) \<in> r"
by (blast intro: transE)
-declare (in CLF) glb_less_b [skolem]
-
lemma (in CLF) S_intv_cl:
"[| a \<in> A; b \<in> A; S \<subseteq> interval r a b |]==> S \<subseteq> A"
by (simp add: subset_trans [OF _ interval_subset])
@@ -995,7 +965,7 @@
by (metis intY1_f_closed restrict_in_funcset)
ML{*ResAtp.problem_name:="Tarski__intY1_mono"*} (*ALL THEOREMS*)
-lemma (in Tarski) intY1_mono [skolem]:
+lemma (in Tarski) intY1_mono:
"monotone (%x: intY1. f x) intY1 (induced intY1 r)"
(*sledgehammer *)
apply (auto simp add: monotone_def induced_def intY1_f_closed)
--- a/src/HOL/MetisExamples/set.thy Fri Oct 05 09:59:03 2007 +0200
+++ b/src/HOL/MetisExamples/set.thy Fri Oct 05 09:59:21 2007 +0200
@@ -113,21 +113,21 @@
have 9: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
by (metis 5 sup_set_eq Un_upper2 sup_set_eq)
have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
- by (metis 3 sup_set_eq Un_upper2 sup_set_eq 1 sup_set_eq)
+ by (metis 3 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X"
- by (metis 8 Un_upper2 sup_set_eq 1 sup_set_eq)
+ by (metis 8 Un_upper2 sup_set_eq sup_set_eq)
have 12: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
- by (metis 10 Un_upper1 sup_set_eq 6)
+ by (metis 10 Un_upper1 sup_set_eq)
have 13: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
by (metis 9 Un_upper1 sup_set_eq)
have 14: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
by (metis equalityI 13 Un_least sup_set_eq)
have 15: "sup Y Z = X"
- by (metis 14 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 6)
+ by (metis 14 sup_set_eq 1 sup_set_eq sup_set_eq 6)
have 16: "Y \<subseteq> x"
- by (metis 7 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 6 15)
+ by (metis 7 Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq 15)
have 17: "\<not> X \<subseteq> x"
- by (metis 11 Un_upper1 sup_set_eq 6 15)
+ by (metis 11 Un_upper1 sup_set_eq 15)
have 18: "X \<subseteq> x"
by (metis Un_least sup_set_eq 15 12 15 16)
show "False"
@@ -152,19 +152,19 @@
have 7: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
by (metis 5 sup_set_eq Un_upper2 sup_set_eq)
have 8: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
- by (metis 2 sup_set_eq Un_upper2 sup_set_eq 1 sup_set_eq)
+ by (metis 2 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
have 9: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
- by (metis 6 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq)
+ by (metis 6 Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq sup_set_eq)
have 10: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
by (metis equalityI 7 Un_upper1 sup_set_eq)
have 11: "sup Y Z = X"
- by (metis 10 Un_least sup_set_eq Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq)
+ by (metis 10 Un_least sup_set_eq sup_set_eq 1 sup_set_eq sup_set_eq 0 sup_set_eq)
have 12: "Z \<subseteq> x"
by (metis 9 11)
have 13: "X \<subseteq> x"
- by (metis Un_least sup_set_eq 11 12 8 Un_upper1 sup_set_eq 0 sup_set_eq 11)
+ by (metis Un_least sup_set_eq 11 12 8 Un_upper1 sup_set_eq sup_set_eq 11)
show "False"
- by (metis 13 4 sup_set_eq Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 11)
+ by (metis 13 4 sup_set_eq Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq sup_set_eq 11)
qed
(*Example included in TPHOLs paper*)
@@ -185,9 +185,9 @@
have 6: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
by (metis 4 sup_set_eq)
have 7: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
- by (metis 3 sup_set_eq Un_upper2 sup_set_eq 1 sup_set_eq)
+ by (metis 3 sup_set_eq Un_upper2 sup_set_eq sup_set_eq)
have 8: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
- by (metis 7 Un_upper1 sup_set_eq 0 sup_set_eq)
+ by (metis 7 Un_upper1 sup_set_eq sup_set_eq)
have 9: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
by (metis equalityI 5 sup_set_eq Un_upper2 sup_set_eq Un_upper1 sup_set_eq Un_least sup_set_eq)
have 10: "Y \<subseteq> x"
@@ -238,20 +238,19 @@
lemma (*singleton_example_2:*)
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-by (metis UnE Un_absorb Un_absorb2 Un_eq_Union Union_insert insertI1 insert_Diff insert_Diff_single subset_def)
- --{*found by Vampire*}
+by (metis Un_absorb2 Union_insert insertI1 insert_Diff insert_Diff_single subset_def)
lemma singleton_example_2:
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
proof (neg_clausify)
-assume 0: "\<And>mes_ojD. \<not> S \<subseteq> {mes_ojD}"
-assume 1: "\<And>mes_ojE. mes_ojE \<notin> S \<or> \<Union>S \<subseteq> mes_ojE"
+assume 0: "\<And>A. \<not> S \<subseteq> {A}"
+assume 1: "\<And>A. A \<notin> S \<or> \<Union>S \<subseteq> A"
have 2: "\<And>X3. X3 = \<Union>S \<or> \<not> X3 \<subseteq> \<Union>S \<or> X3 \<notin> S"
- by (metis equalityI 1)
+ by (metis set_eq_subset 1)
have 3: "\<And>X3. S \<subseteq> insert (\<Union>S) X3"
- by (metis Set.subsetI 2 Union_upper Set.subsetI insertCI)
+ by (metis insert_iff Set.subsetI Union_upper 2 Set.subsetI)
show "False"
- by (metis 0 3)
+ by (metis 3 0)
qed
@@ -272,14 +271,14 @@
"P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
"\<exists>A. a \<notin> A"
"(\<forall>C. (0, 0) \<in> C \<and> (\<forall>x y. (x, y) \<in> C \<longrightarrow> (Suc x, Suc y) \<in> C) \<longrightarrow> (n, m) \<in> C) \<and> Q n \<longrightarrow> Q m"
-apply (metis atMost_iff);
+apply (metis atMost_iff)
apply (metis emptyE)
apply (metis insert_iff singletonE)
apply (metis insertCI singletonE zless_le)
apply (metis insert_iff singletonE)
apply (metis insert_iff singletonE)
apply (metis DiffE)
-apply (metis Suc_eq_add_numeral_1 nat_add_commute pair_in_Id_conv)
+apply (metis pair_in_Id_conv)
done
end
--- a/src/HOL/Tools/metis_tools.ML Fri Oct 05 09:59:03 2007 +0200
+++ b/src/HOL/Tools/metis_tools.ML Fri Oct 05 09:59:21 2007 +0200
@@ -440,6 +440,10 @@
translate isFO ctxt ((fol_th, th) :: thpairs) infpairs
end;
+ (*Determining which axiom clauses are actually used*)
+ fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th)
+ | used_axioms axioms _ = NONE;
+
(* ------------------------------------------------------------------------- *)
(* Translation of HO Clauses *)
(* ------------------------------------------------------------------------- *)
@@ -529,9 +533,13 @@
fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
+ fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2);
+
(* Main function to start metis prove and reconstruction *)
- fun FOL_SOLVE mode ctxt cls ths =
+ fun FOL_SOLVE mode ctxt cls ths0 =
let val thy = ProofContext.theory_of ctxt
+ val th_cls_pairs = map (fn th => (PureThy.get_name_hint th, ResAxioms.cnf_axiom th)) ths0
+ val ths = List.concat (map #2 th_cls_pairs)
val _ = if exists(is_false o prop_of) cls then error "problem contains the empty clause"
else ();
val _ = Output.debug (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
@@ -556,9 +564,15 @@
Metis.Thm.toString mth)
val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
(*add constraints arising from converting goal to clause form*)
- val result = translate isFO ctxt' axioms (Metis.Proof.proof mth)
- val _ = Output.debug (fn () => "METIS COMPLETED")
+ val proof = Metis.Proof.proof mth
+ val result = translate isFO ctxt' axioms proof
+ and used = List.mapPartial (used_axioms axioms) proof
+ val _ = Output.debug (fn () => "METIS COMPLETED...clauses actually used:")
+ val _ = app (fn th => Output.debug (fn () => string_of_thm th)) used
+ val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs
in
+ if null unused then ()
+ else warning ("Unused theorems: " ^ commas (map #1 unused));
case result of
(_,ith)::_ => (Output.debug (fn () => "success: " ^ string_of_thm ith); ith)
| _ => error "METIS: no result"
@@ -569,9 +583,8 @@
fun metis_general_tac mode ctxt ths i st0 =
let val _ = Output.debug (fn () =>
"Metis called with theorems " ^ cat_lines (map string_of_thm ths))
- val ths' = ResAxioms.cnf_rules_of_ths ths
in
- (Meson.MESON ResAxioms.neg_clausify (fn cls => rtac (FOL_SOLVE mode ctxt cls ths') 1) i
+ (Meson.MESON ResAxioms.neg_clausify (fn cls => rtac (FOL_SOLVE mode ctxt cls ths) 1) i
THEN ResAxioms.expand_defs_tac st0) st0
end;