# HG changeset patch
# User paulson
# Date 1191571161 -7200
# Node ID 161eb8381b4940bb00a174cccf840e86c25cd405
# Parent  0ebcd575d3c6ea4e997237e379edc6b486852cb1
metis method: used theorems

diff -r 0ebcd575d3c6 -r 161eb8381b49 src/HOL/MetisExamples/BigO.thy
--- 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
diff -r 0ebcd575d3c6 -r 161eb8381b49 src/HOL/MetisExamples/Tarski.thy
--- 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)
diff -r 0ebcd575d3c6 -r 161eb8381b49 src/HOL/MetisExamples/set.thy
--- 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
diff -r 0ebcd575d3c6 -r 161eb8381b49 src/HOL/Tools/metis_tools.ML
--- 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;