# HG changeset patch
# User blanchet
# Date 1327940159 -3600
# Node ID 9ac0c64ad8e75f20c46a7bb19cc320f8ad3023db
# Parent  ded0390eceae59f78c8c0acd4b796f99a0c5f308
example tuning

diff -r ded0390eceae -r 9ac0c64ad8e7 src/HOL/Metis_Examples/Big_O.thy
--- a/src/HOL/Metis_Examples/Big_O.thy	Mon Jan 30 17:15:59 2012 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy	Mon Jan 30 17:15:59 2012 +0100
@@ -197,6 +197,7 @@
 apply clarify
 (* sledgehammer *)
 apply (rule_tac x = "max c ca" in exI)
+
 apply (rule conjI)
  apply (metis less_max_iff_disj)
 apply clarify
@@ -210,9 +211,8 @@
   defer 1
   apply (metis abs_triangle_ineq)
  apply (metis add_nonneg_nonneg)
-apply (rule add_mono)
- apply (metis le_maxI2 linorder_linear min_max.sup_absorb1 mult_right_mono xt1(6))
-by (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
+by (metis (no_types) add_mono le_maxI2 linorder_linear min_max.sup_absorb1
+          mult_right_mono xt1(6))
 
 lemma bigo_bounded_alt: "\<forall>x. 0 <= f x \<Longrightarrow> \<forall>x. f x <= c * g x \<Longrightarrow> f : O(g)"
 apply (auto simp add: bigo_def)
@@ -234,15 +234,10 @@
 lemma bigo_bounded2: "\<forall>x. lb x <= f x \<Longrightarrow> \<forall>x. f x <= lb x + g x \<Longrightarrow> f : lb +o O(g)"
 apply (rule set_minus_imp_plus)
 apply (rule bigo_bounded)
- apply (auto simp add: diff_minus fun_Compl_def func_plus)
- prefer 2
- apply (drule_tac x = x in spec)+
- apply (metis add_right_mono add_commute diff_add_cancel diff_minus_eq_add le_less order_trans)
-proof -
-  fix x :: 'a
-  assume "\<forall>x. lb x \<le> f x"
-  thus "(0\<Colon>'b) \<le> f x + - lb x" by (metis not_leE diff_minus less_iff_diff_less_0 less_le_not_le)
-qed
+ apply (metis add_le_cancel_left diff_add_cancel diff_self minus_apply
+              comm_semiring_1_class.normalizing_semiring_rules(24))
+by (metis add_le_cancel_left diff_add_cancel func_plus le_fun_def
+          comm_semiring_1_class.normalizing_semiring_rules(24))
 
 lemma bigo_abs: "(\<lambda>x. abs(f x)) =o O(f)"
 apply (unfold bigo_def)
@@ -273,10 +268,8 @@
   also have "... <= O(\<lambda>x. abs (f x - g x))"
     apply (rule bigo_elt_subset)
     apply (rule bigo_bounded)
-    apply force
-    apply (rule allI)
-    apply (rule abs_triangle_ineq3)
-    done
+     apply (metis abs_ge_zero)
+    by (metis abs_triangle_ineq3)
   also have "... <= O(f - g)"
     apply (rule bigo_elt_subset)
     apply (subst fun_diff_def)
@@ -296,9 +289,7 @@
   also have "... <= O(g) \<oplus> O(h)"
     by (auto del: subsetI)
   also have "... = O(\<lambda>x. abs(g x)) \<oplus> O(\<lambda>x. abs(h x))"
-    apply (subst bigo_abs3 [symmetric])+
-    apply (rule refl)
-    done
+    by (metis bigo_abs3)
   also have "... = O((\<lambda>x. abs(g x)) + (\<lambda>x. abs(h x)))"
     by (rule bigo_plus_eq [symmetric], auto)
   finally have "f : ...".
@@ -310,39 +301,21 @@
     by (simp add: bigo_abs3 [symmetric])
 qed
 
-lemma bigo_mult [intro]: "O(f)\<otimes>O(g) <= O(f * g)"
-  apply (rule subsetI)
-  apply (subst bigo_def)
-  apply (auto simp del: abs_mult mult_ac
-              simp add: bigo_alt_def set_times_def func_times)
+lemma bigo_mult [intro]: "O(f) \<otimes> O(g) <= O(f * g)"
+apply (rule subsetI)
+apply (subst bigo_def)
+apply (auto simp del: abs_mult mult_ac
+            simp add: bigo_alt_def set_times_def func_times)
 (* sledgehammer *)
-  apply (rule_tac x = "c * ca" in exI)
-  apply(rule allI)
-  apply(erule_tac x = x in allE)+
-  apply(subgoal_tac "c * ca * abs(f x * g x) =
-      (c * abs(f x)) * (ca * abs(g x))")
-prefer 2
-apply (metis mult_assoc mult_left_commute
-  abs_of_pos mult_left_commute
-  abs_mult mult_pos_pos)
-  apply (erule ssubst)
-  apply (subst abs_mult)
-(* not quite as hard as BigO__bigo_mult_simpler_1 (a hard problem!) since
-   abs_mult has just been done *)
-by (metis abs_ge_zero mult_mono')
+apply (rule_tac x = "c * ca" in exI)
+apply (rule allI)
+apply (erule_tac x = x in allE)+
+apply (subgoal_tac "c * ca * abs (f x * g x) = (c * abs(f x)) * (ca * abs (g x))")
+ apply (metis (no_types) abs_ge_zero abs_mult mult_mono')
+by (metis mult_assoc mult_left_commute abs_of_pos mult_left_commute abs_mult)
 
 lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)"
-  apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult)
-(* sledgehammer *)
-  apply (rule_tac x = c in exI)
-  apply clarify
-  apply (drule_tac x = x in spec)
-(*sledgehammer [no luck]*)
-  apply (subgoal_tac "abs(f x) * abs(b x) <= abs(f x) * (c * abs(g x))")
-  apply (simp add: mult_ac)
-  apply (rule mult_left_mono, assumption)
-  apply (rule abs_ge_zero)
-done
+by (metis bigo_mult bigo_refl set_times_mono3 subset_trans)
 
 lemma bigo_mult3: "f : O(h) \<Longrightarrow> g : O(j) \<Longrightarrow> f * g : O(h * j)"
 by (metis bigo_mult set_rev_mp set_times_intro)
@@ -364,157 +337,101 @@
       by (rule bigo_mult2)
     also have "(\<lambda>x. 1 / f x) * (f * g) = g"
       apply (simp add: func_times)
-      apply (rule ext)
-      apply (simp add: a h nonzero_divide_eq_eq mult_ac)
-      done
+      by (metis (lifting, no_types) a ext mult_ac(2) nonzero_divide_eq_eq)
     finally have "(\<lambda>x. (1\<Colon>'b) / f x) * h : O(g)".
     then have "f * ((\<lambda>x. (1\<Colon>'b) / f x) * h) : f *o O(g)"
       by auto
     also have "f * ((\<lambda>x. (1\<Colon>'b) / f x) * h) = h"
       apply (simp add: func_times)
-      apply (rule ext)
-      apply (simp add: a h nonzero_divide_eq_eq mult_ac)
-      done
+      by (metis (lifting, no_types) a eq_divide_imp ext
+                comm_semiring_1_class.normalizing_semiring_rules(7))
     finally show "h : f *o O(g)".
   qed
 qed
 
-lemma bigo_mult6: "\<forall>x. f x ~= 0 \<Longrightarrow>
-    O(f * g) = (f\<Colon>'a => ('b\<Colon>{linordered_field,number_ring})) *o O(g)"
+lemma bigo_mult6:
+"\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = (f\<Colon>'a \<Rightarrow> ('b\<Colon>{linordered_field,number_ring})) *o O(g)"
 by (metis bigo_mult2 bigo_mult5 order_antisym)
 
 (*proof requires relaxing relevance: 2007-01-25*)
 declare bigo_mult6 [simp]
 
-lemma bigo_mult7: "\<forall>x. f x ~= 0 \<Longrightarrow>
-    O(f * g) <= O(f\<Colon>'a => ('b\<Colon>{linordered_field,number_ring})) \<otimes> O(g)"
-(* sledgehammer *)
-  apply (subst bigo_mult6)
-  apply assumption
-  apply (rule set_times_mono3)
-  apply (rule bigo_refl)
-done
+lemma bigo_mult7:
+"\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) \<le> O(f\<Colon>'a \<Rightarrow> ('b\<Colon>{linordered_field,number_ring})) \<otimes> O(g)"
+by (metis bigo_refl bigo_mult6 set_times_mono3)
 
 declare bigo_mult6 [simp del]
 declare bigo_mult7 [intro!]
 
-lemma bigo_mult8: "\<forall>x. f x ~= 0 \<Longrightarrow>
-    O(f * g) = O(f\<Colon>'a => ('b\<Colon>{linordered_field,number_ring})) \<otimes> O(g)"
+lemma bigo_mult8:
+"\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = O(f\<Colon>'a \<Rightarrow> ('b\<Colon>{linordered_field,number_ring})) \<otimes> O(g)"
 by (metis bigo_mult bigo_mult7 order_antisym_conv)
 
 lemma bigo_minus [intro]: "f : O(g) \<Longrightarrow> - f : O(g)"
-  by (auto simp add: bigo_def fun_Compl_def)
+by (auto simp add: bigo_def fun_Compl_def)
 
 lemma bigo_minus2: "f : g +o O(h) \<Longrightarrow> -f : -g +o O(h)"
-  apply (rule set_minus_imp_plus)
-  apply (drule set_plus_imp_minus)
-  apply (drule bigo_minus)
-  apply (simp add: diff_minus)
-done
+by (metis (no_types) bigo_elt_subset bigo_minus bigo_mult4 bigo_refl
+          comm_semiring_1_class.normalizing_semiring_rules(11) minus_mult_left
+          set_plus_mono_b)
 
 lemma bigo_minus3: "O(-f) = O(f)"
-  by (auto simp add: bigo_def fun_Compl_def abs_minus_cancel)
+by (metis bigo_elt_subset bigo_minus bigo_refl equalityI minus_minus)
 
-lemma bigo_plus_absorb_lemma1: "f : O(g) \<Longrightarrow> f +o O(g) <= O(g)"
-proof -
-  assume a: "f : O(g)"
-  show "f +o O(g) <= O(g)"
-  proof -
-    have "f : O(f)" by auto
-    then have "f +o O(g) <= O(f) \<oplus> O(g)"
-      by (auto del: subsetI)
-    also have "... <= O(g) \<oplus> O(g)"
-    proof -
-      from a have "O(f) <= O(g)" by (auto del: subsetI)
-      thus ?thesis by (auto del: subsetI)
-    qed
-    also have "... <= O(g)" by (simp add: bigo_plus_idemp)
-    finally show ?thesis .
-  qed
-qed
+lemma bigo_plus_absorb_lemma1: "f : O(g) \<Longrightarrow> f +o O(g) \<le> O(g)"
+by (metis bigo_plus_idemp set_plus_mono3)
 
-lemma bigo_plus_absorb_lemma2: "f : O(g) \<Longrightarrow> O(g) <= f +o O(g)"
-proof -
-  assume a: "f : O(g)"
-  show "O(g) <= f +o O(g)"
-  proof -
-    from a have "-f : O(g)" by auto
-    then have "-f +o O(g) <= O(g)" by (elim bigo_plus_absorb_lemma1)
-    then have "f +o (-f +o O(g)) <= f +o O(g)" by auto
-    also have "f +o (-f +o O(g)) = O(g)"
-      by (simp add: set_plus_rearranges)
-    finally show ?thesis .
-  qed
-qed
+lemma bigo_plus_absorb_lemma2: "f : O(g) \<Longrightarrow> O(g) \<le> f +o O(g)"
+by (metis (no_types) bigo_minus bigo_plus_absorb_lemma1 right_minus
+          set_plus_mono_b set_plus_rearrange2 set_zero_plus subsetI)
 
 lemma bigo_plus_absorb [simp]: "f : O(g) \<Longrightarrow> f +o O(g) = O(g)"
 by (metis bigo_plus_absorb_lemma1 bigo_plus_absorb_lemma2 order_eq_iff)
 
-lemma bigo_plus_absorb2 [intro]: "f : O(g) \<Longrightarrow> A <= O(g) \<Longrightarrow> f +o A <= O(g)"
-  apply (subgoal_tac "f +o A <= f +o O(g)")
-  apply force+
-done
+lemma bigo_plus_absorb2 [intro]: "f : O(g) \<Longrightarrow> A <= O(g) \<Longrightarrow> f +o A \<le> O(g)"
+by (metis bigo_plus_absorb set_plus_mono)
 
 lemma bigo_add_commute_imp: "f : g +o O(h) \<Longrightarrow> g : f +o O(h)"
-  apply (subst set_minus_plus [symmetric])
-  apply (subgoal_tac "g - f = - (f - g)")
-  apply (erule ssubst)
-  apply (rule bigo_minus)
-  apply (subst set_minus_plus)
-  apply assumption
-  apply (simp add: diff_minus add_ac)
-done
+by (metis bigo_minus minus_diff_eq set_plus_imp_minus set_minus_plus)
 
 lemma bigo_add_commute: "(f : g +o O(h)) = (g : f +o O(h))"
-  apply (rule iffI)
-  apply (erule bigo_add_commute_imp)+
-done
+by (metis bigo_add_commute_imp)
 
 lemma bigo_const1: "(\<lambda>x. c) : O(\<lambda>x. 1)"
 by (auto simp add: bigo_def mult_ac)
 
-lemma (*bigo_const2 [intro]:*) "O(\<lambda>x. c) <= O(\<lambda>x. 1)"
+lemma bigo_const2 [intro]: "O(\<lambda>x. c) \<le> O(\<lambda>x. 1)"
 by (metis bigo_const1 bigo_elt_subset)
 
-lemma bigo_const2 [intro]: "O(\<lambda>x. c\<Colon>'b\<Colon>{linordered_idom,number_ring}) <= O(\<lambda>x. 1)"
-proof -
-  have "\<forall>u. (\<lambda>Q. u) \<in> O(\<lambda>Q. 1)" by (metis bigo_const1)
-  thus "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)" by (metis bigo_elt_subset)
-qed
-
 lemma bigo_const3: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow> (\<lambda>x. 1) : O(\<lambda>x. c)"
 apply (simp add: bigo_def)
 by (metis abs_eq_0 left_inverse order_refl)
 
 lemma bigo_const4: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow> O(\<lambda>x. 1) <= O(\<lambda>x. c)"
-by (rule bigo_elt_subset, rule bigo_const3, assumption)
+by (metis bigo_elt_subset bigo_const3)
 
 lemma bigo_const [simp]: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow>
     O(\<lambda>x. c) = O(\<lambda>x. 1)"
-by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption)
+by (metis bigo_const2 bigo_const4 equalityI)
 
 lemma bigo_const_mult1: "(\<lambda>x. c * f x) : O(f)"
-  apply (simp add: bigo_def abs_mult)
+apply (simp add: bigo_def abs_mult)
 by (metis le_less)
 
-lemma bigo_const_mult2: "O(\<lambda>x. c * f x) <= O(f)"
+lemma bigo_const_mult2: "O(\<lambda>x. c * f x) \<le> O(f)"
 by (rule bigo_elt_subset, rule bigo_const_mult1)
 
 lemma bigo_const_mult3: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow> f : O(\<lambda>x. c * f x)"
 apply (simp add: bigo_def)
-(* sledgehammer *)
-apply (rule_tac x = "abs(inverse c)" in exI)
-apply (simp only: abs_mult [symmetric] mult_assoc [symmetric])
-apply (subst left_inverse)
-by auto
+by (metis (no_types) abs_mult mult_assoc mult_1 order_refl left_inverse)
 
-lemma bigo_const_mult4: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow>
-    O(f) <= O(\<lambda>x. c * f x)"
-by (rule bigo_elt_subset, rule bigo_const_mult3, assumption)
+lemma bigo_const_mult4:
+"(c\<Colon>'a\<Colon>{linordered_field,number_ring}) \<noteq> 0 \<Longrightarrow> O(f) \<le> O(\<lambda>x. c * f x)"
+by (metis bigo_elt_subset bigo_const_mult3)
 
 lemma bigo_const_mult [simp]: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow>
     O(\<lambda>x. c * f x) = O(f)"
-by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4)
+by (metis equalityI bigo_const_mult2 bigo_const_mult4)
 
 lemma bigo_const_mult5 [simp]: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow>
     (\<lambda>x. c) *o O(f) = O(f)"
@@ -563,48 +480,36 @@
   apply (rule mult_left_mono)
   apply (erule spec)
   apply simp
-  apply(simp add: mult_ac)
+  apply (simp add: mult_ac)
 done
 
 lemma bigo_const_mult7 [intro]: "f =o O(g) \<Longrightarrow> (\<lambda>x. c * f x) =o O(g)"
-proof -
-  assume "f =o O(g)"
-  then have "(\<lambda>x. c) * f =o (\<lambda>x. c) *o O(g)"
-    by auto
-  also have "(\<lambda>x. c) * f = (\<lambda>x. c * f x)"
-    by (simp add: func_times)
-  also have "(\<lambda>x. c) *o O(g) <= O(g)"
-    by (auto del: subsetI)
-  finally show ?thesis .
-qed
+by (metis bigo_const_mult1 bigo_elt_subset order_less_le psubsetD)
 
 lemma bigo_compose1: "f =o O(g) \<Longrightarrow> (\<lambda>x. f(k x)) =o O(\<lambda>x. g(k x))"
 by (unfold bigo_def, auto)
 
-lemma bigo_compose2: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. f(k x)) =o (\<lambda>x. g(k x)) +o
-    O(\<lambda>x. h(k x))"
-  apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def
-      func_plus)
-  apply (erule bigo_compose1)
-done
+lemma bigo_compose2:
+"f =o g +o O(h) \<Longrightarrow> (\<lambda>x. f(k x)) =o (\<lambda>x. g(k x)) +o O(\<lambda>x. h(k x))"
+apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def func_plus)
+by (erule bigo_compose1)
 
 subsection {* Setsum *}
 
 lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 <= h x y \<Longrightarrow>
     \<exists>c. \<forall>x. \<forall>y \<in> A x. abs (f x y) <= c * (h x y) \<Longrightarrow>
       (\<lambda>x. SUM y : A x. f x y) =o O(\<lambda>x. SUM y : A x. h x y)"
-  apply (auto simp add: bigo_def)
-  apply (rule_tac x = "abs c" in exI)
-  apply (subst abs_of_nonneg) back back
-  apply (rule setsum_nonneg)
-  apply force
-  apply (subst setsum_right_distrib)
-  apply (rule allI)
-  apply (rule order_trans)
-  apply (rule setsum_abs)
-  apply (rule setsum_mono)
-apply (blast intro: order_trans mult_right_mono abs_ge_self)
-done
+apply (auto simp add: bigo_def)
+apply (rule_tac x = "abs c" in exI)
+apply (subst abs_of_nonneg) back back
+ apply (rule setsum_nonneg)
+ apply force
+apply (subst setsum_right_distrib)
+apply (rule allI)
+apply (rule order_trans)
+ apply (rule setsum_abs)
+apply (rule setsum_mono)
+by (metis abs_ge_self abs_mult_pos order_trans)
 
 lemma bigo_setsum1: "\<forall>x y. 0 <= h x y \<Longrightarrow>
     \<exists>c. \<forall>x y. abs (f x y) <= c * (h x y) \<Longrightarrow>
@@ -612,9 +517,10 @@
 by (metis (no_types) bigo_setsum_main)
 
 lemma bigo_setsum2: "\<forall>y. 0 <= h y \<Longrightarrow>
-    \<exists>c. \<forall>y. abs(f y) <= c * (h y) \<Longrightarrow>
+    \<exists>c. \<forall>y. abs (f y) <= c * (h y) \<Longrightarrow>
       (\<lambda>x. SUM y : A x. f y) =o O(\<lambda>x. SUM y : A x. h y)"
-by (rule bigo_setsum1, auto)
+apply (rule bigo_setsum1)
+by metis+
 
 lemma bigo_setsum3: "f =o O(h) \<Longrightarrow>
     (\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o
@@ -624,13 +530,7 @@
  apply (rule abs_ge_zero)
 apply (unfold bigo_def)
 apply (auto simp add: abs_mult)
-(* sledgehammer *)
-apply (rule_tac x = c in exI)
-apply (rule allI)+
-apply (subst mult_left_commute)
-apply (rule mult_left_mono)
- apply (erule spec)
-by (rule abs_ge_zero)
+by (metis abs_ge_zero mult_left_commute mult_left_mono)
 
 lemma bigo_setsum4: "f =o g +o O(h) \<Longrightarrow>
     (\<lambda>x. SUM y : A x. l x y * f(k x y)) =o
@@ -641,22 +541,19 @@
 apply (subst setsum_subtractf [symmetric])
 apply (subst right_diff_distrib [symmetric])
 apply (rule bigo_setsum3)
-apply (subst fun_diff_def [symmetric])
-by (erule set_plus_imp_minus)
+by (metis (lifting, no_types) fun_diff_def set_plus_imp_minus ext)
 
 lemma bigo_setsum5: "f =o O(h) \<Longrightarrow> \<forall>x y. 0 <= l x y \<Longrightarrow>
     \<forall>x. 0 <= h x \<Longrightarrow>
       (\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o
         O(\<lambda>x. SUM y : A x. (l x y) * h(k x y))"
-  apply (subgoal_tac "(\<lambda>x. SUM y : A x. (l x y) * h(k x y)) =
+apply (subgoal_tac "(\<lambda>x. SUM y : A x. (l x y) * h(k x y)) =
       (\<lambda>x. SUM y : A x. abs((l x y) * h(k x y)))")
-  apply (erule ssubst)
-  apply (erule bigo_setsum3)
-  apply (rule ext)
-  apply (rule setsum_cong2)
-  apply (thin_tac "f \<in> O(h)")
-apply (metis abs_of_nonneg zero_le_mult_iff)
-done
+ apply (erule ssubst)
+ apply (erule bigo_setsum3)
+apply (rule ext)
+apply (rule setsum_cong2)
+by (metis abs_of_nonneg zero_le_mult_iff)
 
 lemma bigo_setsum6: "f =o g +o O(h) \<Longrightarrow> \<forall>x y. 0 <= l x y \<Longrightarrow>
     \<forall>x. 0 <= h x \<Longrightarrow>
diff -r ded0390eceae -r 9ac0c64ad8e7 src/HOL/Metis_Examples/Type_Encodings.thy
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Jan 30 17:15:59 2012 +0100
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Jan 30 17:15:59 2012 +0100
@@ -67,7 +67,8 @@
       | tac (type_enc :: type_encs) st =
         st (* |> tap (fn _ => tracing (PolyML.makestring type_enc)) *)
            |> ((if null type_encs then all_tac else rtac @{thm fork} 1)
-               THEN Metis_Tactic.metis_tac [type_enc] "combinators" ctxt ths 1
+               THEN Metis_Tactic.metis_tac [type_enc]
+                    ATP_Problem_Generate.combsN ctxt ths 1
                THEN COND (has_fewer_prems 2) all_tac no_tac
                THEN tac type_encs)
   in tac end