author paulson Fri, 05 Oct 2007 09:59:21 +0200 changeset 24855 161eb8381b49 parent 24854 0ebcd575d3c6 child 24856 f06829479407
metis method: used theorems
 src/HOL/MetisExamples/BigO.thy file | annotate | diff | comparison | revisions src/HOL/MetisExamples/Tarski.thy file | annotate | diff | comparison | revisions src/HOL/MetisExamples/set.thy file | annotate | diff | comparison | revisions src/HOL/Tools/metis_tools.ML file | annotate | diff | comparison | revisions
```--- 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)"
@@ -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 @@
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)
@@ -378,8 +356,6 @@
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 (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 (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 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;
```