# HG changeset patch
# User paulson
# Date 1191946440 -7200
# Node ID 34052359891452d8ceaaaf694a1d9dde2881c2e7
# Parent  68a36883f0ad1ead64a3c820153762146c2023d4
context-based treatment of generalization; also handling TFrees in axiom clauses

diff -r 68a36883f0ad -r 340523598914 src/HOL/MetisExamples/BigO.thy
--- a/src/HOL/MetisExamples/BigO.thy	Tue Oct 09 17:11:20 2007 +0200
+++ b/src/HOL/MetisExamples/BigO.thy	Tue Oct 09 18:14:00 2007 +0200
@@ -40,149 +40,64 @@
   apply (case_tac "c = 0", simp)
   apply (rule_tac x = "1" in exI, simp)
   apply (rule_tac x = "abs c" in exI, auto)
-(*hand-modified to give 'a sort ordered_idom and X3 type 'a*)
 proof (neg_clausify)
 fix c x
-assume 0: "\<And>A. \<bar>h A\<bar> \<le> c * \<bar>f A\<bar>"
-assume 1: "c \<noteq> (0\<Colon>'a::ordered_idom)"
-assume 2: "\<not> \<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>"
-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)
-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)"
-  by (metis abs_mult_pos mult_cancel_right1)
-have 7: "\<bar>0\<Colon>'a\<bar> = (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (0\<Colon>'a)"
-  by (metis 6 mult_cancel_right1)
-have 8: "\<bar>0\<Colon>'a\<bar> = (0\<Colon>'a)"
-  by (metis 7 order_refl)
-have 9: "\<not> (0\<Colon>'a) < (0\<Colon>'a)"
-  by (metis abs_not_less_zero 8)
-have 10: "\<bar>(1\<Colon>'a) * (0\<Colon>'a)\<bar> = - ((1\<Colon>'a) * (0\<Colon>'a))"
-  by (metis abs_of_nonpos 5)
-have 11: "(0\<Colon>'a) = - ((1\<Colon>'a) * (0\<Colon>'a))"
-  by (metis 10 mult_cancel_right1 8)
-have 12: "(0\<Colon>'a) = - (0\<Colon>'a)"
-  by (metis 11 mult_cancel_right1)
-have 13: "\<And>X3. \<bar>X3\<bar> = X3 \<or> X3 \<le> (0\<Colon>'a)"
-  by (metis abs_of_nonneg linorder_linear)
-have 14: "c \<le> (0\<Colon>'a) \<or> \<not> \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
-  by (metis 2 13)
-have 15: "c \<le> (0\<Colon>'a)"
-  by (metis 14 0)
-have 16: "c = (0\<Colon>'a) \<or> c < (0\<Colon>'a)"
-  by (metis linorder_antisym_conv2 15)
-have 17: "\<bar>c\<bar> = - c"
-  by (metis abs_of_nonpos 15)
-have 18: "c < (0\<Colon>'a)"
-  by (metis 16 1)
-have 19: "\<not> \<bar>h x\<bar> \<le> - c * \<bar>f x\<bar>"
-  by (metis 2 17)
-have 20: "\<And>X3. X3 * (1\<Colon>'a) = X3"
-  by (metis mult_cancel_right1 AC_mult.f.commute)
-have 21: "\<And>X3. (0\<Colon>'a) \<le> X3 * X3"
-  by (metis zero_le_square AC_mult.f.commute)
-have 22: "(0\<Colon>'a) \<le> (1\<Colon>'a)"
-  by (metis 21 mult_cancel_left1)
-have 23: "\<And>X3. (0\<Colon>'a) = X3 \<or> (0\<Colon>'a) \<noteq> - X3"
-  by (metis neg_equal_iff_equal 12)
-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
-have 26: "\<And>X3. (0\<Colon>'a) = \<bar>X3\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
-  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)"
-  by (metis 27 mult_cancel_left1)
-have 29: "\<And>X1 X3. (0\<Colon>'a) = X3 * X1 \<or> (0\<Colon>'a) < (0\<Colon>'a) \<or> X3 \<noteq> (0\<Colon>'a)"
-  by (metis zero_less_abs_iff 28)
-have 30: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> X3 \<noteq> (0\<Colon>'a)"
-  by (metis 29 9)
-have 31: "\<And>X1 X3. (0\<Colon>'a) = X1 * X3 \<or> X3 \<noteq> (0\<Colon>'a)"
-  by (metis AC_mult.f.commute 30)
-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)
-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>"
-  by (metis 34 22)
-have 36: "\<And>X3. X3 * (1\<Colon>'a) = (0\<Colon>'a) \<or> \<bar>X3\<bar> \<noteq> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
-  by (metis abs_eq_0 abs_mult_pos 20)
-have 37: "\<And>X3. X3 = (0\<Colon>'a) \<or> \<bar>X3\<bar> \<noteq> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
-  by (metis 36 20)
-have 38: "\<And>X3. X3 = (0\<Colon>'a) \<or> \<bar>X3\<bar> \<noteq> (0\<Colon>'a)"
-  by (metis 37 22)
-have 39: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> \<bar>X1\<bar> \<noteq> (0\<Colon>'a)"
-  by (metis 38 32)
-have 40: "\<And>X3::'a. \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar> \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
-  by (metis abs_idempotent abs_mult_pos 20)
-have 41: "\<And>X3::'a. \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar>"
-  by (metis 40 22)
-have 42: "\<And>X3. \<not> \<bar>X3\<bar> < (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
-  by (metis abs_not_less_zero abs_mult_pos 20)
-have 43: "\<And>X3. \<not> \<bar>X3\<bar> < (0\<Colon>'a)"
-  by (metis 42 22)
-have 44: "\<And>X3. X3 * (1\<Colon>'a) = (0\<Colon>'a) \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
-  by (metis abs_le_zero_iff abs_mult_pos 20)
-have 45: "\<And>X3. X3 = (0\<Colon>'a) \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
-  by (metis 44 20)
-have 46: "\<And>X3. X3 = (0\<Colon>'a) \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a)"
-  by (metis 45 22)
-have 47: "\<And>X3. X3 * X3 = (0\<Colon>'a) \<or> \<not> X3 * X3 \<le> (0\<Colon>'a)"
-  by (metis 46 33)
-have 48: "\<And>X3. X3 * X3 = (0\<Colon>'a) \<or> \<not> X3 \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> X3"
-  by (metis 47 mult_le_0_iff)
-have 49: "\<And>X3. \<bar>X3\<bar> = (0\<Colon>'a) \<or> \<not> X3 \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> X3"
-  by (metis mult_eq_0_iff abs_mult_self 48)
-have 50: "\<And>X1 X3.
-   (0\<Colon>'a) * \<bar>X1\<bar> = \<bar>\<bar>X3 * X1\<bar>\<bar> \<or>
-   \<not> (0\<Colon>'a) \<le> \<bar>X1\<bar> \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> \<bar>X3\<bar>"
-  by (metis abs_mult_pos abs_mult 49)
-have 51: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> \<not> X1 \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> X1"
-  by (metis 39 49)
-have 52: "\<And>X1 X3.
-   (0\<Colon>'a) = \<bar>\<bar>X3 * X1\<bar>\<bar> \<or>
-   \<not> (0\<Colon>'a) \<le> \<bar>X1\<bar> \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> \<bar>X3\<bar>"
-  by (metis 50 mult_cancel_left1)
-have 53: "\<And>X1 X3.
-   (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<not> (0\<Colon>'a) \<le> \<bar>X1\<bar> \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> \<bar>X3\<bar>"
-  by (metis 52 41)
-have 54: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> \<bar>X3\<bar>"
-  by (metis 53 35)
-have 55: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a)"
-  by (metis 54 35)
-have 56: "\<And>X1 X3. \<bar>X1 * X3\<bar> = (0\<Colon>'a) \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a)"
-  by (metis 55 AC_mult.f.commute)
-have 57: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> \<not> \<bar>X1\<bar> \<le> (0\<Colon>'a)"
-  by (metis 38 56)
-have 58: "\<And>X3. \<bar>h X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> \<bar>f X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> \<bar>f X3\<bar>"
-  by (metis 0 51)
-have 59: "\<And>X3. \<bar>h X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> \<bar>f X3\<bar> \<le> (0\<Colon>'a)"
-  by (metis 58 35)
-have 60: "\<And>X3. \<bar>h X3\<bar> \<le> (0\<Colon>'a) \<or> (0\<Colon>'a) < \<bar>f X3\<bar>"
-  by (metis 59 linorder_not_le)
-have 61: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> (0\<Colon>'a) < \<bar>X1\<bar>"
-  by (metis 57 linorder_not_le)
-have 62: "(0\<Colon>'a) < \<bar>\<bar>f x\<bar>\<bar> \<or> \<not> \<bar>h x\<bar> \<le> (0\<Colon>'a)"
-  by (metis 19 61)
-have 63: "(0\<Colon>'a) < \<bar>f x\<bar> \<or> \<not> \<bar>h x\<bar> \<le> (0\<Colon>'a)"
-  by (metis 62 41)
-have 64: "(0\<Colon>'a) < \<bar>f x\<bar>"
-  by (metis 63 60)
-have 65: "\<And>X3. \<bar>h X3\<bar> < (0\<Colon>'a) \<or> \<not> c < (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) < \<bar>f X3\<bar>"
-  by (metis 3 mult_less_0_iff)
-have 66: "\<And>X3. \<bar>h X3\<bar> < (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) < \<bar>f X3\<bar>"
-  by (metis 65 18)
-have 67: "\<And>X3. \<not> (0\<Colon>'a) < \<bar>f X3\<bar>"
-  by (metis 66 43)
+have 0: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<bar>X1 * X2\<bar> = \<bar>X2 * X1\<bar>"
+  by (metis abs_mult mult_commute)
+have 1: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
+   X1 \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or> \<bar>X2\<bar> * X1 = \<bar>X2 * X1\<bar>"
+  by (metis abs_mult_pos linorder_linear)
+have 2: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
+   \<not> (0\<Colon>'a\<Colon>ordered_idom) < X1 * X2 \<or>
+   \<not> (0\<Colon>'a\<Colon>ordered_idom) \<le> X2 \<or> \<not> X1 \<le> (0\<Colon>'a\<Colon>ordered_idom)"
+  by (metis linorder_not_less mult_nonneg_nonpos2)
+assume 3: "\<And>x\<Colon>'b\<Colon>type.
+   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>
+   \<le> (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
+assume 4: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
+  \<le> \<bar>c\<Colon>'a\<Colon>ordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
+have 5: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
+  \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
+  by (metis 4 abs_mult)
+have 6: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
+   \<not> X1 \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or> X1 \<le> \<bar>X2\<bar>"
+  by (metis abs_ge_zero xt1(6))
+have 7: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
+   X1 \<le> \<bar>X2\<bar> \<or> (0\<Colon>'a\<Colon>ordered_idom) < X1"
+  by (metis not_leE 6)
+have 8: "(0\<Colon>'a\<Colon>ordered_idom) < \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
+  by (metis 5 7)
+have 9: "\<And>X1\<Colon>'a\<Colon>ordered_idom.
+   \<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar> \<le> X1 \<or>
+   (0\<Colon>'a\<Colon>ordered_idom) < X1"
+  by (metis 8 order_less_le_trans)
+have 10: "(0\<Colon>'a\<Colon>ordered_idom)
+< (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
+  by (metis 3 9)
+have 11: "\<not> (c\<Colon>'a\<Colon>ordered_idom) \<le> (0\<Colon>'a\<Colon>ordered_idom)"
+  by (metis abs_ge_zero 2 10)
+have 12: "\<And>X1\<Colon>'a\<Colon>ordered_idom. (c\<Colon>'a\<Colon>ordered_idom) * \<bar>X1\<bar> = \<bar>X1 * c\<bar>"
+  by (metis mult_commute 1 11)
+have 13: "\<And>X1\<Colon>'b\<Colon>type.
+   - (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1
+   \<le> (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1\<bar>"
+  by (metis 3 abs_le_D2)
+have 14: "\<And>X1\<Colon>'b\<Colon>type.
+   - (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1
+   \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1\<bar>"
+  by (metis 0 12 13)
+have 15: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<bar>X1 * \<bar>X2\<bar>\<bar> = \<bar>X1 * X2\<bar>"
+  by (metis abs_mult abs_mult_pos abs_ge_zero)
+have 16: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. X1 \<le> \<bar>X2\<bar> \<or> \<not> X1 \<le> X2"
+  by (metis xt1(6) abs_ge_self)
+have 17: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<not> \<bar>X1\<bar> \<le> X2 \<or> X1 \<le> \<bar>X2\<bar>"
+  by (metis 16 abs_le_D1)
+have 18: "\<And>X1\<Colon>'b\<Colon>type.
+   (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1
+   \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1\<bar>"
+  by (metis 17 3 15)
 show "False"
-  by (metis 67 64)
+  by (metis abs_le_iff 5 18 14)
 qed
 
 lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
@@ -195,76 +110,34 @@
 ML{*ResReconstruct.modulus:=2*}
 proof (neg_clausify)
 fix c x
-assume 0: "\<And>A. \<bar>h A\<bar> \<le> c * \<bar>f A\<bar>"
-assume 1: "c \<noteq> (0\<Colon>'a::ordered_idom)"
-assume 2: "\<not> \<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>"
-have 3: "\<And>X3. (1\<Colon>'a) * X3 \<le> X3"
-  by (metis mult_le_cancel_right2 order_refl order_refl)
-have 4: "\<bar>0\<Colon>'a\<bar> = (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (0\<Colon>'a)"
-  by (metis abs_mult_pos mult_cancel_right1 mult_cancel_right1)
-have 5: "\<not> (0\<Colon>'a) < (0\<Colon>'a)"
-  by (metis abs_not_less_zero 4 order_refl)
-have 6: "(0\<Colon>'a) = - ((1\<Colon>'a) * (0\<Colon>'a))"
-  by (metis abs_of_nonpos 3 mult_cancel_right1 4 order_refl)
-have 7: "\<And>X3. \<bar>X3\<bar> = X3 \<or> X3 \<le> (0\<Colon>'a)"
-  by (metis abs_of_nonneg linorder_linear)
-have 8: "c \<le> (0\<Colon>'a)"
-  by (metis 2 7 0)
-have 9: "\<bar>c\<bar> = - c"
-  by (metis abs_of_nonpos 8)
-have 10: "\<not> \<bar>h x\<bar> \<le> - c * \<bar>f x\<bar>"
-  by (metis 2 9)
-have 11: "\<And>X3. X3 * (1\<Colon>'a) = X3"
-  by (metis mult_cancel_right1 AC_mult.f.commute)
-have 12: "(0\<Colon>'a) \<le> (1\<Colon>'a)"
-  by (metis zero_le_square AC_mult.f.commute mult_cancel_left1)
-have 13: "\<And>X3. (0\<Colon>'a) = - X3 \<or> X3 \<noteq> (0\<Colon>'a)"
-  by (metis neg_equal_iff_equal 6 mult_cancel_right1 minus_equation_iff)
-have 14: "\<And>X3. (0\<Colon>'a) = \<bar>X3\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
-  by (metis abs_minus_cancel 13 4 order_refl)
-have 15: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
-  by (metis abs_mult 14 mult_cancel_left1)
-have 16: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> X3 \<noteq> (0\<Colon>'a)"
-  by (metis zero_less_abs_iff 15 5)
-have 17: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<bar>X1\<bar> \<noteq> (0\<Colon>'a)"
-  by (metis abs_mult AC_mult.f.commute 16)
-have 18: "\<And>X3. (0\<Colon>'a) \<le> \<bar>X3\<bar>"
-  by (metis abs_ge_zero abs_mult_pos 11 12)
-have 19: "\<And>X3. X3 * (1\<Colon>'a) = (0\<Colon>'a) \<or> \<bar>X3\<bar> \<noteq> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
-  by (metis abs_eq_0 abs_mult_pos 11)
-have 20: "\<And>X3. X3 = (0\<Colon>'a) \<or> \<bar>X3\<bar> \<noteq> (0\<Colon>'a)"
-  by (metis 19 11 12)
-have 21: "\<And>X3::'a. \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar> \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
-  by (metis abs_idempotent abs_mult_pos 11)
-have 22: "\<And>X3. \<not> \<bar>X3\<bar> < (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
-  by (metis abs_not_less_zero abs_mult_pos 11)
-have 23: "\<And>X3. X3 = (0\<Colon>'a) \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
-  by (metis abs_le_zero_iff abs_mult_pos 11 11)
-have 24: "\<And>X3. X3 * X3 = (0\<Colon>'a) \<or> \<not> X3 * X3 \<le> (0\<Colon>'a)"
-  by (metis 23 12 abs_mult_self abs_mult AC_mult.f.commute)
-have 25: "\<And>X3. \<bar>X3\<bar> = (0\<Colon>'a) \<or> \<not> X3 \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> X3"
-  by (metis mult_eq_0_iff abs_mult_self 24 mult_le_0_iff)
-have 26: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> \<not> X1 \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> X1"
-  by (metis 20 17 25)
-have 27: "\<And>X1 X3.
-   (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<not> (0\<Colon>'a) \<le> \<bar>X1\<bar> \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> \<bar>X3\<bar>"
-  by (metis abs_mult_pos abs_mult 25 mult_cancel_left1 21 12)
-have 28: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a)"
-  by (metis 27 18 18)
-have 29: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> \<not> \<bar>X1\<bar> \<le> (0\<Colon>'a)"
-  by (metis 20 28 AC_mult.f.commute)
-have 30: "\<And>X3. \<bar>h X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> \<bar>f X3\<bar> \<le> (0\<Colon>'a)"
-  by (metis 0 26 18)
-have 31: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> (0\<Colon>'a) < \<bar>X1\<bar>"
-  by (metis 29 linorder_not_le)
-have 32: "(0\<Colon>'a) < \<bar>f x\<bar> \<or> \<not> \<bar>h x\<bar> \<le> (0\<Colon>'a)"
-  by (metis 10 31 21 12)
-have 33: "\<And>X3. \<bar>h X3\<bar> < (0\<Colon>'a) \<or> \<not> c < (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) < \<bar>f X3\<bar>"
-  by (metis order_le_less_trans 0 mult_less_0_iff)
-have 34: "\<And>X3. \<not> (0\<Colon>'a) < \<bar>f X3\<bar>"
-  by (metis 33 linorder_antisym_conv2 8 1 22 12)
+have 0: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<bar>X1 * X2\<bar> = \<bar>X2 * X1\<bar>"
+  by (metis abs_mult mult_commute)
+assume 1: "\<And>x\<Colon>'b\<Colon>type.
+   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>
+   \<le> (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
+assume 2: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
+  \<le> \<bar>c\<Colon>'a\<Colon>ordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
+have 3: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
+  \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
+  by (metis 2 abs_mult)
+have 4: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
+   \<not> X1 \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or> X1 \<le> \<bar>X2\<bar>"
+  by (metis abs_ge_zero xt1(6))
+have 5: "(0\<Colon>'a\<Colon>ordered_idom) < \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
+  by (metis not_leE 4 3)
+have 6: "(0\<Colon>'a\<Colon>ordered_idom)
+< (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
+  by (metis 1 order_less_le_trans 5)
+have 7: "\<And>X1\<Colon>'a\<Colon>ordered_idom. (c\<Colon>'a\<Colon>ordered_idom) * \<bar>X1\<bar> = \<bar>X1 * c\<bar>"
+  by (metis abs_ge_zero linorder_not_less mult_nonneg_nonpos2 6 linorder_linear abs_mult_pos mult_commute)
+have 8: "\<And>X1\<Colon>'b\<Colon>type.
+   - (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1
+   \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1\<bar>"
+  by (metis 0 7 abs_le_D2 1)
+have 9: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<not> \<bar>X1\<bar> \<le> X2 \<or> X1 \<le> \<bar>X2\<bar>"
+  by (metis abs_ge_self xt1(6) abs_le_D1)
 show "False"
-  by (metis 34 32 30 linorder_not_le)
+  by (metis 8 abs_ge_zero abs_mult_pos abs_mult 1 9 3 abs_le_iff)
 qed
 
 lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
@@ -277,133 +150,24 @@
 ML{*ResReconstruct.modulus:=3*}
 proof (neg_clausify)
 fix c x
-assume 0: "\<And>A\<Colon>'b\<Colon>type.
-   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) A\<bar>
-   \<le> (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) A\<bar>"
-assume 1: "(c\<Colon>'a\<Colon>ordered_idom) \<noteq> (0\<Colon>'a\<Colon>ordered_idom)"
-assume 2: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
+assume 0: "\<And>x\<Colon>'b\<Colon>type.
+   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>
+   \<le> (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
+assume 1: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
   \<le> \<bar>c\<Colon>'a\<Colon>ordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
-have 3: "\<And>X3\<Colon>'a\<Colon>ordered_idom. (1\<Colon>'a\<Colon>ordered_idom) * X3 \<le> X3"
-  by (metis mult_le_cancel_right2 order_refl order_refl)
-have 4: "\<bar>0\<Colon>'a\<Colon>ordered_idom\<bar> = (0\<Colon>'a\<Colon>ordered_idom)"
-  by (metis abs_mult_pos mult_cancel_right1 mult_cancel_right1 order_refl)
-have 5: "(0\<Colon>'a\<Colon>ordered_idom) = - ((1\<Colon>'a\<Colon>ordered_idom) * (0\<Colon>'a\<Colon>ordered_idom))"
-  by (metis abs_of_nonpos 3 mult_cancel_right1 4)
-have 6: "(c\<Colon>'a\<Colon>ordered_idom) \<le> (0\<Colon>'a\<Colon>ordered_idom)"
-  by (metis 2 abs_of_nonneg linorder_linear 0)
-have 7: "(c\<Colon>'a\<Colon>ordered_idom) < (0\<Colon>'a\<Colon>ordered_idom)"
-  by (metis linorder_antisym_conv2 6 1)
-have 8: "\<And>X3\<Colon>'a\<Colon>ordered_idom. X3 * (1\<Colon>'a\<Colon>ordered_idom) = X3"
-  by (metis mult_cancel_right1 AC_mult.f.commute)
-have 9: "\<And>X3\<Colon>'a\<Colon>ordered_idom. (0\<Colon>'a\<Colon>ordered_idom) = X3 \<or> (0\<Colon>'a\<Colon>ordered_idom) \<noteq> - X3"
-  by (metis neg_equal_iff_equal 5 mult_cancel_right1)
-have 10: "\<And>X3\<Colon>'a\<Colon>ordered_idom. (0\<Colon>'a\<Colon>ordered_idom) = \<bar>X3\<bar> \<or> X3 \<noteq> (0\<Colon>'a\<Colon>ordered_idom)"
-  by (metis abs_minus_cancel 9 minus_equation_iff 4)
-have 11: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X3\<Colon>'a\<Colon>ordered_idom.
-   (0\<Colon>'a\<Colon>ordered_idom) * \<bar>X1\<bar> = \<bar>X3 * X1\<bar> \<or> X3 \<noteq> (0\<Colon>'a\<Colon>ordered_idom)"
-  by (metis abs_mult 10)
-have 12: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X3\<Colon>'a\<Colon>ordered_idom.
-   X3 * X1 = (0\<Colon>'a\<Colon>ordered_idom) \<or> X3 \<noteq> (0\<Colon>'a\<Colon>ordered_idom)"
-  by (metis zero_less_abs_iff 11 mult_cancel_left1 abs_not_less_zero 4)
-have 13: "\<And>X3\<Colon>'a\<Colon>ordered_idom. \<bar>X3 * X3\<bar> = X3 * X3"
-  by (metis abs_mult_self abs_mult AC_mult.f.commute)
-have 14: "\<And>X3\<Colon>'a\<Colon>ordered_idom. (0\<Colon>'a\<Colon>ordered_idom) \<le> \<bar>X3\<bar>"
-  by (metis abs_ge_zero abs_mult_pos 8 zero_le_square AC_mult.f.commute mult_cancel_left1)
-have 15: "\<And>X3\<Colon>'a\<Colon>ordered_idom.
-   X3 = (0\<Colon>'a\<Colon>ordered_idom) \<or>
-   \<bar>X3\<bar> \<noteq> (0\<Colon>'a\<Colon>ordered_idom) \<or> \<not> (0\<Colon>'a\<Colon>ordered_idom) \<le> (1\<Colon>'a\<Colon>ordered_idom)"
-  by (metis abs_eq_0 abs_mult_pos 8 8)
-have 16: "\<And>X3\<Colon>'a\<Colon>ordered_idom.
-   \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar> \<or> \<not> (0\<Colon>'a\<Colon>ordered_idom) \<le> (1\<Colon>'a\<Colon>ordered_idom)"
-  by (metis abs_idempotent abs_mult_pos 8)
-have 17: "\<And>X3\<Colon>'a\<Colon>ordered_idom. \<not> \<bar>X3\<bar> < (0\<Colon>'a\<Colon>ordered_idom)"
-  by (metis abs_not_less_zero abs_mult_pos 8 zero_le_square AC_mult.f.commute mult_cancel_left1)
-have 18: "\<And>X3\<Colon>'a\<Colon>ordered_idom.
-   X3 = (0\<Colon>'a\<Colon>ordered_idom) \<or>
-   \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or>
-   \<not> (0\<Colon>'a\<Colon>ordered_idom) \<le> (1\<Colon>'a\<Colon>ordered_idom)"
-  by (metis abs_le_zero_iff abs_mult_pos 8 8)
-have 19: "\<And>X3\<Colon>'a\<Colon>ordered_idom.
-   X3 * X3 = (0\<Colon>'a\<Colon>ordered_idom) \<or>
-   \<not> X3 \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or> \<not> (0\<Colon>'a\<Colon>ordered_idom) \<le> X3"
-  by (metis 18 zero_le_square AC_mult.f.commute mult_cancel_left1 13 mult_le_0_iff)
-have 20: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X3\<Colon>'a\<Colon>ordered_idom.
-   X3 * X1 = (0\<Colon>'a\<Colon>ordered_idom) \<or>
-   \<not> X1 \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or> \<not> (0\<Colon>'a\<Colon>ordered_idom) \<le> X1"
-  by (metis 15 zero_le_square AC_mult.f.commute mult_cancel_left1 abs_mult AC_mult.f.commute 12 mult_eq_0_iff abs_mult_self 19)
-have 21: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X3\<Colon>'a\<Colon>ordered_idom.
-   (0\<Colon>'a\<Colon>ordered_idom) = \<bar>X3 * X1\<bar> \<or>
-   \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or> \<not> (0\<Colon>'a\<Colon>ordered_idom) \<le> \<bar>X3\<bar>"
-  by (metis abs_mult_pos abs_mult mult_eq_0_iff abs_mult_self 19 mult_cancel_left1 16 zero_le_square AC_mult.f.commute mult_cancel_left1 14)
-have 22: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X3\<Colon>'a\<Colon>ordered_idom.
-   X3 * X1 = (0\<Colon>'a\<Colon>ordered_idom) \<or> \<not> \<bar>X1\<bar> \<le> (0\<Colon>'a\<Colon>ordered_idom)"
-  by (metis 15 zero_le_square AC_mult.f.commute mult_cancel_left1 21 14 AC_mult.f.commute)
-have 23: "\<And>X3\<Colon>'b\<Colon>type.
-   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X3\<bar> \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or>
-   (0\<Colon>'a\<Colon>ordered_idom) < \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X3\<bar>"
-  by (metis 0 20 14 linorder_not_le)
-have 24: "(0\<Colon>'a\<Colon>ordered_idom) < \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar> \<or>
-\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar> \<le> (0\<Colon>'a\<Colon>ordered_idom)"
-  by (metis 2 abs_of_nonpos 6 22 linorder_not_le 16 zero_le_square AC_mult.f.commute mult_cancel_left1)
-have 25: "\<And>X3\<Colon>'b\<Colon>type.
-   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X3\<bar> < (0\<Colon>'a\<Colon>ordered_idom) \<or>
-   \<not> (0\<Colon>'a\<Colon>ordered_idom) < \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X3\<bar>"
-  by (metis order_le_less_trans 0 mult_less_0_iff 7)
+have 2: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
+   X1 \<le> \<bar>X2\<bar> \<or> (0\<Colon>'a\<Colon>ordered_idom) < X1"
+  by (metis abs_ge_zero xt1(6) not_leE)
+have 3: "\<not> (c\<Colon>'a\<Colon>ordered_idom) \<le> (0\<Colon>'a\<Colon>ordered_idom)"
+  by (metis abs_ge_zero mult_nonneg_nonpos2 linorder_not_less order_less_le_trans 1 abs_mult 2 0)
+have 4: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<bar>X1 * \<bar>X2\<bar>\<bar> = \<bar>X1 * X2\<bar>"
+  by (metis abs_ge_zero abs_mult_pos abs_mult)
+have 5: "\<And>X1\<Colon>'b\<Colon>type.
+   (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1
+   \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1\<bar>"
+  by (metis 4 0 xt1(6) abs_ge_self abs_le_D1)
 show "False"
-  by (metis 25 17 24 23)
-qed
-
-lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
-    ALL x. (abs (h x)) <= (c * (abs (f x))))
-      = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
-  apply auto
-  apply (case_tac "c = 0", simp)
-  apply (rule_tac x = "1" in exI, simp)
-  apply (rule_tac x = "abs c" in exI, auto);
-ML{*ResReconstruct.modulus:=4*}
-ML{*ResReconstruct.recon_sorts:=false*}
-proof (neg_clausify)
-fix c x
-assume 0: "\<And>A. \<bar>h A\<bar> \<le> c * \<bar>f A\<bar>"
-assume 1: "c \<noteq> (0\<Colon>'a)"
-assume 2: "\<not> \<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>"
-have 3: "\<And>X3. (1\<Colon>'a) * X3 \<le> X3"
-  by (metis mult_le_cancel_right2 order_refl order_refl)
-have 4: "\<not> (0\<Colon>'a) < (0\<Colon>'a)"
-  by (metis abs_not_less_zero abs_mult_pos mult_cancel_right1 mult_cancel_right1 order_refl)
-have 5: "c \<le> (0\<Colon>'a)"
-  by (metis 2 abs_of_nonneg linorder_linear 0)
-have 6: "\<not> \<bar>h x\<bar> \<le> - c * \<bar>f x\<bar>"
-  by (metis 2 abs_of_nonpos 5)
-have 7: "(0\<Colon>'a) \<le> (1\<Colon>'a)"
-  by (metis zero_le_square AC_mult.f.commute mult_cancel_left1)
-have 8: "\<And>X3. (0\<Colon>'a) = \<bar>X3\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
-  by (metis abs_minus_cancel neg_equal_iff_equal abs_of_nonpos 3 mult_cancel_right1 abs_mult_pos mult_cancel_right1 mult_cancel_right1 order_refl mult_cancel_right1 minus_equation_iff abs_mult_pos mult_cancel_right1 mult_cancel_right1 order_refl)
-have 9: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
-  by (metis abs_mult 8 mult_cancel_left1)
-have 10: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<bar>X1\<bar> \<noteq> (0\<Colon>'a)"
-  by (metis abs_mult AC_mult.f.commute zero_less_abs_iff 9 4)
-have 11: "\<And>X3. (0\<Colon>'a) \<le> \<bar>X3\<bar>"
-  by (metis abs_ge_zero abs_mult_pos mult_cancel_right1 AC_mult.f.commute 7)
-have 12: "\<And>X3. X3 = (0\<Colon>'a) \<or> \<bar>X3\<bar> \<noteq> (0\<Colon>'a)"
-  by (metis abs_eq_0 abs_mult_pos mult_cancel_right1 AC_mult.f.commute mult_cancel_right1 AC_mult.f.commute 7)
-have 13: "\<And>X3. \<not> \<bar>X3\<bar> < (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
-  by (metis abs_not_less_zero abs_mult_pos mult_cancel_right1 AC_mult.f.commute)
-have 14: "\<And>X3. X3 = (0\<Colon>'a) \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
-  by (metis abs_le_zero_iff abs_mult_pos mult_cancel_right1 AC_mult.f.commute mult_cancel_right1 AC_mult.f.commute)
-have 15: "\<And>X3. \<bar>X3\<bar> = (0\<Colon>'a) \<or> \<not> X3 \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> X3"
-  by (metis mult_eq_0_iff abs_mult_self 14 7 abs_mult_self abs_mult AC_mult.f.commute mult_le_0_iff)
-have 16: "\<And>X1 X3.
-   (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<not> (0\<Colon>'a) \<le> \<bar>X1\<bar> \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> \<bar>X3\<bar>"
-  by (metis abs_mult_pos abs_mult 15 mult_cancel_left1 abs_idempotent abs_mult_pos mult_cancel_right1 AC_mult.f.commute 7)
-have 17: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> \<not> \<bar>X1\<bar> \<le> (0\<Colon>'a)"
-  by (metis 12 16 11 11 AC_mult.f.commute)
-have 18: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> (0\<Colon>'a) < \<bar>X1\<bar>"
-  by (metis 17 linorder_not_le)
-have 19: "\<And>X3. \<bar>h X3\<bar> < (0\<Colon>'a) \<or> \<not> c < (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) < \<bar>f X3\<bar>"
-  by (metis order_le_less_trans 0 mult_less_0_iff)
-show "False"
-  by (metis 19 linorder_antisym_conv2 5 1 13 7 6 18 abs_idempotent abs_mult_pos mult_cancel_right1 AC_mult.f.commute 7 0 12 10 15 11 linorder_not_le)
+  by (metis abs_mult mult_commute 3 abs_mult_pos linorder_linear 0 abs_le_D2 5 1 abs_le_iff)
 qed
 
 
@@ -474,14 +238,12 @@
   apply(auto simp add: bigo_def)
 proof (neg_clausify)
 fix x
-assume 0: "\<And>mes_pSG\<Colon>'b\<Colon>ordered_idom.
-   \<not> \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) mes_pSG)\<bar>
-     \<le> mes_pSG * \<bar>f (x mes_pSG)\<bar>"
-have 1: "\<And>X3\<Colon>'b. X3 \<le> (1\<Colon>'b) * X3 \<or> \<not> (1\<Colon>'b) \<le> (1\<Colon>'b)"
-  by (metis Ring_and_Field.mult_le_cancel_right1 order_refl)
-have 2: "\<And>X3\<Colon>'b. X3 \<le> (1\<Colon>'b) * X3"
-  by (metis 1 order_refl)
-show 3: "False"
+assume 0: "\<And>xa. \<not> \<bar>f (x xa)\<bar> \<le> xa * \<bar>f (x xa)\<bar>"
+have 1: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2 \<or> \<not> (1\<Colon>'b) \<le> (1\<Colon>'b)"
+  by (metis mult_le_cancel_right1 order_eq_iff)
+have 2: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2"
+  by (metis order_eq_iff 1)
+show "False"
   by (metis 0 2)
 qed
 
@@ -490,15 +252,11 @@
   apply (auto simp add: bigo_def func_zero)
 proof (neg_clausify)
 fix x
-assume 0: "\<And>mes_mVM\<Colon>'b\<Colon>ordered_idom.
-   \<not> (0\<Colon>'b\<Colon>ordered_idom)
-     \<le> mes_mVM *
-       \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom)
-         ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) mes_mVM)\<bar>"
-have 1: "(0\<Colon>'b\<Colon>ordered_idom) < (0\<Colon>'b\<Colon>ordered_idom)"
-  by (metis 0 Ring_and_Field.mult_le_cancel_left1)
-show 2: "False"
-  by (metis Orderings.linorder_class.neq_iff 1)
+assume 0: "\<And>xa. \<not> (0\<Colon>'b) \<le> xa * \<bar>g (x xa)\<bar>"
+have 1: "\<not> (0\<Colon>'b) \<le> (0\<Colon>'b)"
+  by (metis 0 mult_eq_0_iff)
+show "False"
+  by (metis 1 linorder_neq_iff linorder_antisym_conv1)
 qed
 
 lemma bigo_zero2: "O(%x.0) = {%x.0}"
@@ -637,70 +395,48 @@
 (*Version 2: single-step proof*)
 proof (neg_clausify)
 fix x
-assume 0: "\<And>mes_mbt\<Colon>'a.
-   (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) mes_mbt
-   \<le> (c\<Colon>'b\<Colon>ordered_idom) * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) mes_mbt"
-assume 1: "\<And>mes_mbs\<Colon>'b\<Colon>ordered_idom.
-   \<not> (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) mes_mbs)
-     \<le> mes_mbs * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x mes_mbs)\<bar>"
-have 2: "\<And>X3\<Colon>'a.
-   (c\<Colon>'b\<Colon>ordered_idom) * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) X3 =
-   (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) X3 \<or>
-   \<not> c * g X3 \<le> f X3"
-  by (metis Lattices.min_max.less_eq_less_inf.antisym_intro 0)
-have 3: "\<And>X3\<Colon>'b\<Colon>ordered_idom.
-   \<not> (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>X3\<bar>)
-     \<le> \<bar>X3 * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X3\<bar>)\<bar>"
-  by (metis 1 Ring_and_Field.abs_mult)
-have 4: "\<And>X3\<Colon>'b\<Colon>ordered_idom. (1\<Colon>'b\<Colon>ordered_idom) * X3 = X3"
-  by (metis Ring_and_Field.mult_cancel_left2 Finite_Set.AC_mult.f.commute)
-have 5: "\<And>X3\<Colon>'b\<Colon>ordered_idom. X3 * (1\<Colon>'b\<Colon>ordered_idom) = X3"
-  by (metis Ring_and_Field.mult_cancel_right2 Finite_Set.AC_mult.f.commute)
-have 6: "\<And>X3\<Colon>'b\<Colon>ordered_idom. \<bar>X3\<bar> * \<bar>X3\<bar> = X3 * X3"
-  by (metis Ring_and_Field.abs_mult_self Finite_Set.AC_mult.f.commute)
-have 7: "\<And>X3\<Colon>'b\<Colon>ordered_idom. (0\<Colon>'b\<Colon>ordered_idom) \<le> X3 * X3"
-  by (metis Ring_and_Field.zero_le_square Finite_Set.AC_mult.f.commute)
-have 8: "(0\<Colon>'b\<Colon>ordered_idom) \<le> (1\<Colon>'b\<Colon>ordered_idom)"
-  by (metis 7 Ring_and_Field.mult_cancel_left2)
-have 9: "\<And>X3\<Colon>'b\<Colon>ordered_idom. X3 * X3 = \<bar>X3 * X3\<bar>"
-  by (metis Ring_and_Field.abs_mult 6)
-have 10: "\<bar>1\<Colon>'b\<Colon>ordered_idom\<bar> = (1\<Colon>'b\<Colon>ordered_idom)"
-  by (metis 9 4)
-have 11: "\<And>X3\<Colon>'b\<Colon>ordered_idom. \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar> * \<bar>1\<Colon>'b\<Colon>ordered_idom\<bar>"
-  by (metis Ring_and_Field.abs_mult OrderedGroup.abs_idempotent 5)
-have 12: "\<And>X3\<Colon>'b\<Colon>ordered_idom. \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar>"
-  by (metis 11 10 5)
-have 13: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom.
-   X3 * (1\<Colon>'b\<Colon>ordered_idom) \<le> X1 \<or>
-   \<not> \<bar>X3\<bar> \<le> X1 \<or> \<not> (0\<Colon>'b\<Colon>ordered_idom) \<le> (1\<Colon>'b\<Colon>ordered_idom)"
-  by (metis OrderedGroup.abs_le_D1 Ring_and_Field.abs_mult_pos 5)
-have 14: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom.
-   X3 \<le> X1 \<or> \<not> \<bar>X3\<bar> \<le> X1 \<or> \<not> (0\<Colon>'b\<Colon>ordered_idom) \<le> (1\<Colon>'b\<Colon>ordered_idom)"
-  by (metis 13 5)
-have 15: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. X3 \<le> X1 \<or> \<not> \<bar>X3\<bar> \<le> X1"
-  by (metis 14 8)
-have 16: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. X3 \<le> X1 \<or> X1 \<le> \<bar>X3\<bar>"
-  by (metis 15 Orderings.linorder_class.less_eq_less.linear)
-have 17: "\<And>X3\<Colon>'b\<Colon>ordered_idom.
-   X3 * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>X3\<bar>)
-   \<le> (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X3\<bar>)"
-  by (metis 3 16)
-have 18: "(c\<Colon>'b\<Colon>ordered_idom) *
-(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>c\<bar>) =
-(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>c\<bar>)"
-  by (metis 2 17)
-have 19: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. \<bar>X3 * X1\<bar> \<le> \<bar>\<bar>X3\<bar>\<bar> * \<bar>\<bar>X1\<bar>\<bar>"
-  by (metis 15 Ring_and_Field.abs_le_mult Ring_and_Field.abs_mult)
-have 20: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. \<bar>X3 * X1\<bar> \<le> \<bar>X3\<bar> * \<bar>X1\<bar>"
-  by (metis 19 12 12)
-have 21: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. X3 * X1 \<le> \<bar>X3\<bar> * \<bar>X1\<bar>"
-  by (metis 15 20)
-have 22: "(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom)
- ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>c\<Colon>'b\<Colon>ordered_idom\<bar>)
-\<le> \<bar>c\<bar> * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>c\<bar>)\<bar>"
-  by (metis 21 18)
-show 23: "False"
-  by (metis 22 1)
+assume 0: "\<And>x. f x \<le> c * g x"
+assume 1: "\<And>xa. \<not> f (x xa) \<le> xa * \<bar>g (x xa)\<bar>"
+have 2: "\<And>X3. c * g X3 = f X3 \<or> \<not> c * g X3 \<le> f X3"
+  by (metis 0 order_antisym_conv)
+have 3: "\<And>X3. \<not> f (x \<bar>X3\<bar>) \<le> \<bar>X3 * g (x \<bar>X3\<bar>)\<bar>"
+  by (metis 1 abs_mult)
+have 4: "\<And>X1 X3\<Colon>'b\<Colon>ordered_idom. X3 \<le> X1 \<or> X1 \<le> \<bar>X3\<bar>"
+  by (metis linorder_linear abs_le_D1)
+have 5: "\<And>X3::'b. \<bar>X3\<bar> * \<bar>X3\<bar> = X3 * X3"
+  by (metis abs_mult_self AC_mult.f.commute)
+have 6: "\<And>X3. \<not> X3 * X3 < (0\<Colon>'b\<Colon>ordered_idom)"
+  by (metis not_square_less_zero AC_mult.f.commute)
+have 7: "\<And>X1 X3::'b. \<bar>X1\<bar> * \<bar>X3\<bar> = \<bar>X3 * X1\<bar>"
+  by (metis abs_mult AC_mult.f.commute)
+have 8: "\<And>X3::'b. X3 * X3 = \<bar>X3 * X3\<bar>"
+  by (metis abs_mult 5)
+have 9: "\<And>X3. X3 * g (x \<bar>X3\<bar>) \<le> f (x \<bar>X3\<bar>)"
+  by (metis 3 4)
+have 10: "c * g (x \<bar>c\<bar>) = f (x \<bar>c\<bar>)"
+  by (metis 2 9)
+have 11: "\<And>X3::'b. \<bar>X3\<bar> * \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar> * \<bar>X3\<bar>"
+  by (metis abs_idempotent abs_mult 8)
+have 12: "\<And>X3::'b. \<bar>X3 * \<bar>X3\<bar>\<bar> = \<bar>X3\<bar> * \<bar>X3\<bar>"
+  by (metis AC_mult.f.commute 7 11)
+have 13: "\<And>X3::'b. \<bar>X3 * \<bar>X3\<bar>\<bar> = X3 * X3"
+  by (metis 8 7 12)
+have 14: "\<And>X3. X3 \<le> \<bar>X3\<bar> \<or> X3 < (0\<Colon>'b)"
+  by (metis abs_ge_self abs_le_D1 abs_if)
+have 15: "\<And>X3. X3 \<le> \<bar>X3\<bar> \<or> \<bar>X3\<bar> < (0\<Colon>'b)"
+  by (metis abs_ge_self abs_le_D1 abs_if)
+have 16: "\<And>X3. X3 * X3 < (0\<Colon>'b) \<or> X3 * \<bar>X3\<bar> \<le> X3 * X3"
+  by (metis 15 13)
+have 17: "\<And>X3::'b. X3 * \<bar>X3\<bar> \<le> X3 * X3"
+  by (metis 16 6)
+have 18: "\<And>X3. X3 \<le> \<bar>X3\<bar> \<or> \<not> X3 < (0\<Colon>'b)"
+  by (metis mult_le_cancel_left 17)
+have 19: "\<And>X3::'b. X3 \<le> \<bar>X3\<bar>"
+  by (metis 18 14)
+have 20: "\<not> f (x \<bar>c\<bar>) \<le> \<bar>f (x \<bar>c\<bar>)\<bar>"
+  by (metis 3 10)
+show "False"
+  by (metis 20 19)
 qed
 
 
@@ -781,16 +517,11 @@
   apply auto
 proof (neg_clausify)
 fix x
-assume 0: "!!mes_o43::'b::ordered_idom.
-   ~ abs ((f::'a::type => 'b::ordered_idom)
-           ((x::'b::ordered_idom => 'a::type) mes_o43))
-     <= mes_o43 * abs (f (x mes_o43))"
-have 1: "!!X3::'b::ordered_idom.
-   X3 <= (1::'b::ordered_idom) * X3 |
-   ~ (1::'b::ordered_idom) <= (1::'b::ordered_idom)"
-  by (metis mult_le_cancel_right1 order_refl)
-have 2: "!!X3::'b::ordered_idom. X3 <= (1::'b::ordered_idom) * X3"
-  by (metis 1 order_refl)
+assume 0: "\<And>xa. \<not> \<bar>f (x xa)\<bar> \<le> xa * \<bar>f (x xa)\<bar>"
+have 1: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2 \<or> \<not> (1\<Colon>'b) \<le> (1\<Colon>'b)"
+  by (metis mult_le_cancel_right1 order_eq_iff)
+have 2: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2"
+  by (metis order_eq_iff 1)
 show "False"
   by (metis 0 2)
 qed
@@ -801,15 +532,11 @@
   apply auto
 proof (neg_clausify)
 fix x
-assume 0: "\<And>mes_o4C\<Colon>'b\<Colon>ordered_idom.
-   \<not> \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) mes_o4C)\<bar>
-     \<le> mes_o4C * \<bar>f (x mes_o4C)\<bar>"
-have 1: "\<And>X3\<Colon>'b\<Colon>ordered_idom.
-   X3 \<le> (1\<Colon>'b\<Colon>ordered_idom) * X3 \<or>
-   \<not> (1\<Colon>'b\<Colon>ordered_idom) \<le> (1\<Colon>'b\<Colon>ordered_idom)"
-  by (metis mult_le_cancel_right1 order_refl)
-have 2: "\<And>X3\<Colon>'b\<Colon>ordered_idom. X3 \<le> (1\<Colon>'b\<Colon>ordered_idom) * X3"
-  by (metis 1 order_refl)
+assume 0: "\<And>xa. \<not> \<bar>f (x xa)\<bar> \<le> xa * \<bar>f (x xa)\<bar>"
+have 1: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2 \<or> \<not> (1\<Colon>'b) \<le> (1\<Colon>'b)"
+  by (metis mult_le_cancel_right1 order_eq_iff)
+have 2: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2"
+  by (metis order_eq_iff 1)
 show "False"
   by (metis 0 2)
 qed
@@ -1144,17 +871,14 @@
 
 ML{*ResAtp.problem_name := "BigO__bigo_const_mult1"*}
 lemma bigo_const_mult1: "(%x. c * f x) : O(f)"
-  apply (simp add: bigo_def abs_mult) 
+  apply (simp add: bigo_def abs_mult)
 proof (neg_clausify)
 fix x
-assume 0: "\<And>mes_vAL\<Colon>'b.
-   \<not> \<bar>c\<Colon>'b\<bar> *
-     \<bar>(f\<Colon>'a \<Rightarrow> 'b) ((x\<Colon>'b \<Rightarrow> 'a) mes_vAL)\<bar>
-     \<le> mes_vAL * \<bar>f (x mes_vAL)\<bar>"
-have 1: "\<And>Y\<Colon>'b. Y \<le> Y"
-  by (metis order_refl)
-show 2: "False"
-  by (metis 0 1)
+assume 0: "\<And>xa. \<not> \<bar>c\<bar> * \<bar>f (x xa)\<bar> \<le> xa * \<bar>f (x xa)\<bar>"
+have 1: "\<And>X2. \<not> \<bar>c * f (x X2)\<bar> \<le> X2 * \<bar>f (x X2)\<bar>"
+  by (metis 0 abs_mult)
+show "False"
+  by (metis 1 abs_le_mult)
 qed
 
 lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"
@@ -1435,16 +1159,8 @@
 lemma bigo_lesso1: "ALL x. f x <= g x ==> f <o g =o O(h)"
   apply (unfold lesso_def)
   apply (subgoal_tac "(%x. max (f x - g x) 0) = 0")
-(*
-?? abstractions don't work: abstraction function gets the wrong type?
-proof (neg_clausify)
-assume 0: "llabs_subgoal_1 f g = 0"
-assume 1: "llabs_subgoal_1 f g \<notin> O(h)"
-show "False"
-  by (metis 1 0 bigo_zero)
-*)
-  apply (erule ssubst)
-  apply (rule bigo_zero)
+(*??Translation of TSTP raised an exception: Type unification failed: Variable ?'X2.0::type not of sort ord*)
+apply (metis bigo_zero ord_class.max)
   apply (unfold func_zero)
   apply (rule ext)
   apply (simp split: split_max)
diff -r 68a36883f0ad -r 340523598914 src/HOL/MetisExamples/set.thy
--- a/src/HOL/MetisExamples/set.thy	Tue Oct 09 17:11:20 2007 +0200
+++ b/src/HOL/MetisExamples/set.thy	Tue Oct 09 18:14:00 2007 +0200
@@ -33,7 +33,7 @@
 assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
 assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
 assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 5: "\<And>A. ((\<not> Y \<subseteq> A \<or> \<not> Z \<subseteq> A) \<or> X \<subseteq> A) \<or> X = Y \<union> Z"
+assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
 have 6: "sup Y Z = X \<or> Y \<subseteq> X"
   by (metis 0 sup_set_eq)
 have 7: "sup Y Z = X \<or> Z \<subseteq> X"
@@ -103,7 +103,7 @@
 assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
 assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
 assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 5: "\<And>A. ((\<not> Y \<subseteq> A \<or> \<not> Z \<subseteq> A) \<or> X \<subseteq> A) \<or> X = Y \<union> Z"
+assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
 have 6: "sup Y Z = X \<or> Y \<subseteq> X"
   by (metis 0 sup_set_eq)
 have 7: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
@@ -146,7 +146,7 @@
 assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
 assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
 assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 5: "\<And>A. ((\<not> Y \<subseteq> A \<or> \<not> Z \<subseteq> A) \<or> X \<subseteq> A) \<or> X = Y \<union> Z"
+assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
 have 6: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
   by (metis 3 sup_set_eq)
 have 7: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
@@ -181,7 +181,7 @@
 assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
 assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
 assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 5: "\<And>A. ((\<not> Y \<subseteq> A \<or> \<not> Z \<subseteq> A) \<or> X \<subseteq> A) \<or> X = Y \<union> Z"
+assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
 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"
@@ -221,9 +221,9 @@
 proof (neg_clausify)
 fix x xa
 assume 0: "f (g x) = x"
-assume 1: "\<And>A. A = x \<or> f (g A) \<noteq> A"
-assume 2: "\<And>A. g (f (xa A)) = xa A \<or> g (f A) \<noteq> A"
-assume 3: "\<And>A. g (f A) \<noteq> A \<or> xa A \<noteq> A"
+assume 1: "\<And>y. y = x \<or> f (g y) \<noteq> y"
+assume 2: "\<And>x. g (f (xa x)) = xa x \<or> g (f x) \<noteq> x"
+assume 3: "\<And>x. g (f x) \<noteq> x \<or> xa x \<noteq> x"
 have 4: "\<And>X1. g (f X1) \<noteq> X1 \<or> g x \<noteq> X1"
   by (metis 3 1 2)
 show "False"
@@ -243,8 +243,8 @@
 lemma singleton_example_2:
      "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
 proof (neg_clausify)
-assume 0: "\<And>A. \<not> S \<subseteq> {A}"
-assume 1: "\<And>A. A \<notin> S \<or> \<Union>S \<subseteq> A"
+assume 0: "\<And>x. \<not> S \<subseteq> {x}"
+assume 1: "\<And>x. x \<notin> S \<or> \<Union>S \<subseteq> x"
 have 2: "\<And>X3. X3 = \<Union>S \<or> \<not> X3 \<subseteq> \<Union>S \<or> X3 \<notin> S"
   by (metis set_eq_subset 1)
 have 3: "\<And>X3. S \<subseteq> insert (\<Union>S) X3"
diff -r 68a36883f0ad -r 340523598914 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Tue Oct 09 17:11:20 2007 +0200
+++ b/src/HOL/Tools/meson.ML	Tue Oct 09 18:14:00 2007 +0200
@@ -6,9 +6,6 @@
 The MESON resolution proof procedure for HOL.
 
 When making clauses, avoids using the rewriter -- instead uses RS recursively
-
-NEED TO SORT LITERALS BY # OF VARS, USING ==>I/E.  ELIMINATES NEED FOR
-FUNCTION nodups -- if done to goal clauses too!
 *)
 
 signature MESON =
@@ -18,9 +15,8 @@
   val flexflex_first_order: thm -> thm
   val size_of_subgoals: thm -> int
   val too_many_clauses: term -> bool
-  val make_cnf: thm list -> thm -> thm list
+  val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
   val finish_cnf: thm list -> thm list
-  val generalize: thm -> thm
   val make_nnf: thm -> thm
   val make_nnf1: thm -> thm
   val skolemize: thm -> thm
@@ -102,10 +98,15 @@
         in  th'  end
         handle THM _ => th;
 
-(*raises exception if no rules apply -- unlike RL*)
+(*Forward proof while preserving bound variables names*)
+fun rename_bvs_RS th rl =
+  let val th' = th RS rl
+  in  Thm.rename_boundvars (concl_of th') (concl_of th) th' end;
+
+(*raises exception if no rules apply*)
 fun tryres (th, rls) =
   let fun tryall [] = raise THM("tryres", 0, th::rls)
-        | tryall (rl::rls) = (th RS rl handle THM _ => tryall rls)
+        | tryall (rl::rls) = (rename_bvs_RS th rl handle THM _ => tryall rls)
   in  tryall rls  end;
 
 (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
@@ -208,6 +209,32 @@
   handle TERM _ => th;  (*probably dest_Trueprop on a weird theorem*)
 
 
+(*** Removal of duplicate literals ***)
+
+(*Forward proof, passing extra assumptions as theorems to the tactic*)
+fun forward_res2 nf hyps st =
+  case Seq.pull
+        (REPEAT
+         (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
+         st)
+  of SOME(th,_) => th
+   | NONE => raise THM("forward_res2", 0, [st]);
+
+(*Remove duplicates in P|Q by assuming ~P in Q
+  rls (initially []) accumulates assumptions of the form P==>False*)
+fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
+    handle THM _ => tryres(th,rls)
+    handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),
+                           [disj_FalseD1, disj_FalseD2, asm_rl])
+    handle THM _ => th;
+
+(*Remove duplicate literals, if there are any*)
+fun nodups th =
+  if has_duplicates (op =) (literals (prop_of th))
+    then nodups_aux [] th
+    else th;
+
+
 (*** The basic CNF transformation ***)
 
 val max_clauses = 40;
@@ -243,11 +270,19 @@
 fun too_many_clauses t = nclauses t >= max_clauses;
 
 (*Replaces universally quantified variables by FREE variables -- because
-  assumptions may not contain scheme variables.  Later, we call "generalize". *)
-fun freeze_spec th =
-  let val newname = gensym "mes_"
-      val spec' = read_instantiate [("x", newname)] spec
-  in  th RS spec'  end;
+  assumptions may not contain scheme variables.  Later, generalize using Variable.export. *)
+local  
+  val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))));
+  val spec_varT = #T (Thm.rep_cterm spec_var);
+  fun name_of (Const ("All", _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
+in  
+  fun freeze_spec th ctxt =
+    let
+      val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
+      val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (concl_of th))] ctxt;
+      val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec;
+    in (th RS spec', ctxt') end
+end;
 
 (*Used with METAHYPS below. There is one assumption, which gets bound to prem
   and then normalized via function nf. The normal form is given to resolve_tac,
@@ -268,16 +303,18 @@
 (*Conjunctive normal form, adding clauses from th in front of ths (for foldr).
   Strips universal quantifiers and breaks up conjunctions.
   Eliminates existential quantifiers using skoths: Skolemization theorems.*)
-fun cnf skoths (th,ths) =
-  let fun cnf_aux (th,ths) =
+fun cnf skoths ctxt (th,ths) =
+  let val ctxtr = ref ctxt
+      fun cnf_aux (th,ths) =
         if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
         else if not (has_conns ["All","Ex","op &"] (prop_of th))
-        then th::ths (*no work to do, terminate*)
+        then nodups th :: ths (*no work to do, terminate*)
         else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
             Const ("op &", _) => (*conjunction*)
                 cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
           | Const ("All", _) => (*universal quantifier*)
-                cnf_aux (freeze_spec th, ths)
+                let val (th',ctxt') = freeze_spec th (!ctxtr)
+                in  ctxtr := ctxt'; cnf_aux (th', ths) end
           | Const ("Ex", _) =>
               (*existential quantifier: Insert Skolem functions*)
               cnf_aux (apply_skolem_ths (th,skoths), ths)
@@ -288,62 +325,18 @@
                   (METAHYPS (resop cnf_nil) 1) THEN
                    (fn st' => st' |> METAHYPS (resop cnf_nil) 1)
               in  Seq.list_of (tac (th RS disj_forward)) @ ths  end
-          | _ => (*no work to do*) th::ths
+          | _ => nodups th :: ths  (*no work to do*)
       and cnf_nil th = cnf_aux (th,[])
-  in
-    if too_many_clauses (concl_of th)
-    then (Output.debug (fn () => ("cnf is ignoring: " ^ string_of_thm th)); ths)
-    else cnf_aux (th,ths)
-  end;
-
-fun all_names (Const ("all", _) $ Abs(x,_,P)) = x :: all_names P
-  | all_names _ = [];
+      val cls = 
+	    if too_many_clauses (concl_of th)
+	    then (Output.debug (fn () => ("cnf is ignoring: " ^ string_of_thm th)); ths)
+	    else cnf_aux (th,ths)
+  in  (cls, !ctxtr)  end;
 
-fun new_names n [] = []
-  | new_names n (x::xs) =
-      if String.isPrefix "mes_" x then (x, radixstring(26,"A",n)) :: new_names (n+1) xs
-      else new_names n xs;
-
-(*The gensym names are ugly, so don't let the user see them. When forall_elim_vars
-  is called, it will ensure that no name clauses ensue.*)
-fun nice_names th =
-  let val old_names = all_names (prop_of th)
-  in  Drule.rename_bvars (new_names 0 old_names) th  end;
-
-(*Convert all suitable free variables to schematic variables,
-  but don't discharge assumptions.*)
-fun generalize th = Thm.varifyT (forall_elim_vars 0 (nice_names (forall_intr_frees th)));
-
-fun make_cnf skoths th = cnf skoths (th, []);
+fun make_cnf skoths th ctxt = cnf skoths ctxt (th, []);
 
 (*Generalization, removal of redundant equalities, removal of tautologies.*)
-fun finish_cnf ths = filter (not o is_taut) (map (refl_clause o generalize) ths);
-
-
-(**** Removal of duplicate literals ****)
-
-(*Forward proof, passing extra assumptions as theorems to the tactic*)
-fun forward_res2 nf hyps st =
-  case Seq.pull
-        (REPEAT
-         (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
-         st)
-  of SOME(th,_) => th
-   | NONE => raise THM("forward_res2", 0, [st]);
-
-(*Remove duplicates in P|Q by assuming ~P in Q
-  rls (initially []) accumulates assumptions of the form P==>False*)
-fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
-    handle THM _ => tryres(th,rls)
-    handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),
-                           [disj_FalseD1, disj_FalseD2, asm_rl])
-    handle THM _ => th;
-
-(*Remove duplicate literals, if there are any*)
-fun nodups th =
-  if has_duplicates (op =) (literals (prop_of th))
-    then nodups_aux [] th
-    else th;
+fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);
 
 
 (**** Generation of contrapositives ****)
@@ -530,13 +523,16 @@
     handle THM _ =>
         skolemize (forward_res skolemize
                    (tryres (th, [conj_forward, disj_forward, all_forward])))
-    handle THM _ => forward_res skolemize (th RS ex_forward);
+    handle THM _ => forward_res skolemize (rename_bvs_RS th ex_forward);
 
+fun add_clauses (th,cls) =
+  let val ctxt0 = Variable.thm_context th
+      val (cnfs,ctxt) = make_cnf [] th ctxt0
+  in Variable.export ctxt ctxt0 cnfs @ cls end;
 
 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   The resulting clauses are HOL disjunctions.*)
-fun make_clauses ths =
-    (sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths)));
+fun make_clauses ths = sort_clauses (foldr add_clauses [] ths);
 
 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
 fun make_horns ths =
diff -r 68a36883f0ad -r 340523598914 src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Tue Oct 09 17:11:20 2007 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Tue Oct 09 18:14:00 2007 +0200
@@ -97,18 +97,32 @@
         let val (lits, types_sorts) = ResHolClause.literals_of_term thy t
         in  (map (hol_literal_to_fol isFO) lits, types_sorts) end;
 
-  fun metis_of_typeLit (ResClause.LTVar (s,x))  = metis_lit false s [Metis.Term.Var x]
-    | metis_of_typeLit (ResClause.LTFree (s,x)) = metis_lit true  s [Metis.Term.Fn(x,[])];
+  (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
+  fun metis_of_typeLit pos (ResClause.LTVar (s,x))  = metis_lit pos s [Metis.Term.Var x]
+    | metis_of_typeLit pos (ResClause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
 
-  fun metis_of_tfree tf = Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit tf));
+  fun default_sort ctxt (ResClause.FOLTVar _, _) = false
+    | default_sort ctxt (ResClause.FOLTFree x, ss) = (ss = Option.getOpt (Variable.def_sort ctxt (x,~1), []));
 
-  fun hol_thm_to_fol ctxt isFO th =
+  fun metis_of_tfree tf = 
+    Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf));
+
+  fun hol_thm_to_fol is_conjecture ctxt isFO th =
     let val thy = ProofContext.theory_of ctxt
         val (mlits, types_sorts) =
                (literals_of_hol_thm thy isFO o HOLogic.dest_Trueprop o prop_of) th
-        val (tvar_lits,tfree_lits) = ResClause.add_typs_aux types_sorts
-        val tlits = if Config.get ctxt type_lits then map metis_of_typeLit tvar_lits else []
-    in  (Metis.Thm.axiom (Metis.LiteralSet.fromList(tlits@mlits)), tfree_lits)  end;
+    in  
+        if is_conjecture then
+            (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), ResClause.add_typs types_sorts) 
+        else
+          let val tylits = ResClause.add_typs 
+                             (filter (not o default_sort ctxt) types_sorts)
+              val mtylits = if Config.get ctxt type_lits 
+                            then map (metis_of_typeLit false) tylits else []
+          in
+            (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [])
+          end
+    end;
 
   (* ARITY CLAUSE *)
 
@@ -118,8 +132,9 @@
         metis_lit false (ResClause.make_type_class c) [Metis.Term.Var str];
 
   (*TrueI is returned as the Isabelle counterpart because there isn't any.*)
-  fun arity_cls (ResClause.ArityClause{kind,conclLit,premLits,...}) =
-    (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
+  fun arity_cls (ResClause.ArityClause{conclLit,premLits,...}) =
+    (TrueI, 
+     Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
 
   (* CLASSREL CLAUSE *)
 
@@ -460,9 +475,6 @@
   val comb_C = cnf_th ResHolClause.comb_C;
   val comb_S = cnf_th ResHolClause.comb_S;
 
-  fun dest_Arity (ResClause.ArityClause{premLits,...}) =
-        map ResClause.class_of_arityLit premLits;
-
   fun type_ext thy tms =
     let val subs = ResAtp.tfree_classes_of_terms tms
         val supers = ResAtp.tvar_classes_of_terms tms
@@ -489,16 +501,17 @@
         | in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
     in  c=pred orelse exists in_mterm tm_list  end;
 
+  (*Extract TFree constraints from context to include as conjecture clauses*)
+  fun init_tfrees ctxt =
+    let fun add ((a,i),s) ys = if i = ~1 then (ResClause.FOLTFree a,s) :: ys else ys
+    in  ResClause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
+
   (*transform isabelle clause to metis clause *)
-  fun add_thm ctxt (ith, {isFO, axioms, tfrees}) : logic_map =
-    let val (mth, tfree_lits) = hol_thm_to_fol ctxt isFO ith
-        fun add_tfree (tf, axs) =
-              if member (op=) tfrees tf then axs
-              else (metis_of_tfree tf, TrueI) :: axs
-        val new_axioms = foldl add_tfree [] tfree_lits
+  fun add_thm is_conjecture ctxt (ith, {isFO, axioms, tfrees}) : logic_map =
+    let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt isFO ith
     in
        {isFO = isFO,
-        axioms = (mth, Meson.make_meta_clause ith) :: (new_axioms @ axioms),
+        axioms = (mth, Meson.make_meta_clause ith) :: axioms,
         tfrees = tfree_lits union tfrees}
     end;
 
@@ -509,11 +522,19 @@
                           axioms = (mth, ith) :: axioms,
                           tfrees = tfrees}
 
+  (*Insert non-logical axioms corresponding to all accumulated TFrees*)
+  fun add_tfrees {isFO, axioms, tfrees} : logic_map =
+       {isFO = isFO,
+        axioms = (map (fn tf => (metis_of_tfree tf, TrueI)) (distinct op= tfrees)) @ axioms,
+        tfrees = tfrees};
+        
   (* Function to generate metis clauses, including comb and type clauses *)
   fun build_map mode thy ctxt cls ths =
     let val isFO = (mode = ResAtp.Fol) orelse
                     (mode <> ResAtp.Hol andalso ResAtp.is_fol_thms (cls @ ths))
-        val lmap = foldl (add_thm ctxt) {isFO = isFO, axioms = [], tfrees = []} (cls @ ths)
+        val lmap0 = foldl (add_thm true ctxt) 
+                          {isFO = isFO, axioms = [], tfrees = init_tfrees ctxt} cls
+        val lmap = foldl (add_thm false ctxt) (add_tfrees lmap0) ths
         val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
         fun used c = exists (Metis.LiteralSet.exists (const_in_metis c)) clause_lists
         (*Now check for the existence of certain combinators*)
@@ -524,7 +545,7 @@
         val thS   = if used "c_COMBS" then [comb_S] else []
         val thEQ  = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else []
         val lmap' = if isFO then lmap 
-                    else foldl (add_thm ctxt) lmap (thEQ @ thS @ thC @ thB @ thK @ thI)
+                    else foldl (add_thm false ctxt) lmap (thEQ @ thS @ thC @ thB @ thK @ thI)
     in
         add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap'
     end;
@@ -550,7 +571,7 @@
         val {isFO,axioms,tfrees} = build_map mode thy ctxt cls ths
         val _ = if null tfrees then ()
                 else (Output.debug (fn () => "TFREE CLAUSES");
-                      app (fn tf => Output.debug (fn _ => ResClause.tptp_of_typeLit tf)) tfrees)
+                      app (fn tf => Output.debug (fn _ => ResClause.tptp_of_typeLit true tf)) tfrees)
         val _ = Output.debug (fn () => "CLAUSES GIVEN TO METIS")
         val thms = map #1 axioms
         val _ = app (fn th => Output.debug (fn () => Metis.Thm.toString th)) thms
diff -r 68a36883f0ad -r 340523598914 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Tue Oct 09 17:11:20 2007 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Tue Oct 09 18:14:00 2007 +0200
@@ -8,7 +8,6 @@
 signature RES_AXIOMS =
 sig
   val cnf_axiom: thm -> thm list
-  val meta_cnf_axiom: thm -> thm list
   val pairname: thm -> string * thm
   val multi_base_blacklist: string list 
   val skolem_thm: thm -> thm list
@@ -294,13 +293,14 @@
     transfer (Theory.deref atp_linkup_thy_ref) th handle THM _ => th;
 
 (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
-fun to_nnf th =
-    th |> transfer_to_ATP_Linkup
-       |> transform_elim |> zero_var_indexes |> freeze_thm
-       |> Conv.fconv_rule ObjectLogic.atomize |> Meson.make_nnf |> strip_lambdas ~1;
+fun to_nnf th ctxt0 =
+  let val th1 = th |> transfer_to_ATP_Linkup |> transform_elim |> zero_var_indexes
+      val ((_,[th2]),ctxt) = Variable.import_thms false [th1] ctxt0
+      val th3 = th2 |> Conv.fconv_rule ObjectLogic.atomize |> Meson.make_nnf |> strip_lambdas ~1
+  in  (th3, ctxt)  end;
 
 (*Generate Skolem functions for a theorem supplied in nnf*)
-fun skolem_of_nnf s th =
+fun assume_skolem_of_def s th =
   map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
 
 fun assert_lambda_free ths msg =
@@ -321,27 +321,32 @@
 
 (*Skolemize a named theorem, with Skolem functions as additional premises.*)
 fun skolem_thm th =
-  let val nnfth = to_nnf th and s = fake_name th
-  in  Meson.make_cnf (skolem_of_nnf s nnfth) nnfth |>  map combinators |> Meson.finish_cnf
-  end
+  let val ctxt0 = Variable.thm_context th
+      val (nnfth,ctxt1) = to_nnf th ctxt0 and s = fake_name th
+      val (cnfs,ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1
+  in  cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf  end
   handle THM _ => [];
 
 (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
   It returns a modified theory, unless skolemization fails.*)
 fun skolem thy th =
+  let val ctxt0 = Variable.thm_context th
+  in
      Option.map
-        (fn nnfth =>
+        (fn (nnfth,ctxt1) =>
           let val _ = Output.debug (fn () => "skolemizing " ^ name_or_string th ^ ": ")
               val _ = Output.debug (fn () => string_of_thm nnfth)
               val s = fake_name th
               val (thy',defs) = declare_skofuns s nnfth thy
-              val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth
+              val (cnfs,ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1
               val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded")
-              val cnfs' = map combinators cnfs
-          in (map Goal.close_result (Meson.finish_cnf cnfs'), thy') end
+              val cnfs' = cnfs |> map combinators |> Variable.export ctxt2 ctxt0 
+                               |> Meson.finish_cnf |> map Goal.close_result
+          in (cnfs', thy') end
           handle Clausify_failure thy_e => ([],thy_e)
         )
-      (try to_nnf th);
+      (try (to_nnf th) ctxt0)
+  end;
 
 (*The cache prevents repeated clausification of a theorem, and also repeated declaration of
   Skolem functions.*)
@@ -529,12 +534,8 @@
 
 val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac];
 
-(*finish_cnf removes tautologies and functional reflexivity axioms, but by calling Thm.varifyT
-  it can introduce TVars, which are useless in conjecture clauses.*)
-val no_tvars = null o term_tvars o prop_of;
-
-val neg_clausify =
-  filter no_tvars o Meson.finish_cnf o map combinators o Meson.make_clauses;
+fun neg_clausify sts =
+  sts |> Meson.make_clauses |> map combinators |> Meson.finish_cnf;
 
 fun neg_conjecture_clauses st0 n =
   let val st = Seq.hd (neg_skolemize_tac n st0)
diff -r 68a36883f0ad -r 340523598914 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Tue Oct 09 17:11:20 2007 +0200
+++ b/src/HOL/Tools/res_clause.ML	Tue Oct 09 18:14:00 2007 +0200
@@ -32,7 +32,6 @@
   val make_fixed_type_const : string -> string
   val make_type_class : string -> string
   datatype kind = Axiom | Conjecture
-  val name_of_kind : kind -> string
   type axiom_name = string
   datatype typ_var = FOLTVar of indexname | FOLTFree of string
   datatype fol_type =
@@ -44,20 +43,15 @@
   val mk_typ_var_sort: typ -> typ_var * sort
   exception CLAUSE of string * term
   val isMeta : string -> bool
-  val add_typs_aux : (typ_var * string list) list -> type_literal list * type_literal list
+  val add_typs : (typ_var * string list) list -> type_literal list
   val get_tvar_strs: (typ_var * sort) list -> string list
   datatype arLit =
       TConsLit of class * string * string list
     | TVarLit of class * string
   datatype arityClause = ArityClause of
-   {axiom_name: axiom_name,
-    kind: kind,
-    conclLit: arLit,
-    premLits: arLit list}
+   {axiom_name: axiom_name, conclLit: arLit, premLits: arLit list}
   datatype classrelClause = ClassrelClause of
-   {axiom_name: axiom_name,
-    subclass: class,
-    superclass: class}
+   {axiom_name: axiom_name, subclass: class, superclass: class}
   val make_classrel_clauses: theory -> class list -> class list -> classrelClause list
   val make_arity_clauses: theory -> string list -> class list -> class list * arityClause list
   val add_type_sort_preds: (typ_var * string list) * int Symtab.table -> int Symtab.table
@@ -69,8 +63,8 @@
   val init_functab: int Symtab.table
   val writeln_strs: TextIO.outstream -> string list -> unit
   val dfg_sign: bool -> string -> string
-  val dfg_of_typeLit: type_literal -> string
-  val gen_dfg_cls: int * string * string * string * string list -> string
+  val dfg_of_typeLit: bool -> type_literal -> string
+  val gen_dfg_cls: int * string * kind * string list * string list * string list -> string
   val string_of_preds: (string * Int.int) list -> string
   val string_of_funcs: (string * int) list -> string
   val string_of_symbols: string -> string -> string
@@ -80,8 +74,8 @@
   val dfg_classrelClause: classrelClause -> string
   val dfg_arity_clause: arityClause -> string
   val tptp_sign: bool -> string -> string
-  val tptp_of_typeLit : type_literal -> string
-  val gen_tptp_cls : int * string * kind * string list -> string
+  val tptp_of_typeLit : bool -> type_literal -> string
+  val gen_tptp_cls : int * string * kind * string list * string list -> string
   val tptp_tfree_clause : string -> string
   val tptp_arity_clause : arityClause -> string
   val tptp_classrelClause : classrelClause -> string
@@ -236,9 +230,6 @@
 
 datatype kind = Axiom | Conjecture;
 
-fun name_of_kind Axiom = "axiom"
-  | name_of_kind Conjecture = "negated_conjecture";
-
 type axiom_name = string;
 
 (**** Isabelle FOL clauses ****)
@@ -296,18 +287,8 @@
 fun pred_of_sort (LTVar (s,ty)) = (s,1)
   | pred_of_sort (LTFree (s,ty)) = (s,1)
 
-(*Given a list of sorted type variables, return two separate lists.
-  The first is for TVars, the second for TFrees.*)
-fun add_typs_aux [] = ([],[])
-  | add_typs_aux ((FOLTVar indx, s) :: tss) =
-      let val vs = sorts_on_typs (FOLTVar indx, s)
-          val (vss,fss) = add_typs_aux tss
-      in  (vs union vss, fss)  end
-  | add_typs_aux ((FOLTFree x, s) :: tss) =
-      let val fs = sorts_on_typs (FOLTFree x, s)
-          val (vss,fss) = add_typs_aux tss
-      in  (vss, fs union fss)  end;
-
+(*Given a list of sorted type variables, return a list of type literals.*)
+fun add_typs tss = foldl (op union) [] (map sorts_on_typs tss);
 
 (** make axiom and conjecture clauses. **)
 
@@ -327,7 +308,6 @@
 
 datatype arityClause =
          ArityClause of {axiom_name: axiom_name,
-                         kind: kind,
                          conclLit: arLit,
                          premLits: arLit list};
 
@@ -344,7 +324,7 @@
    let val tvars = gen_TVars (length args)
        val tvars_srts = ListPair.zip (tvars,args)
    in
-      ArityClause {axiom_name = axiom_name, kind = Axiom,
+      ArityClause {axiom_name = axiom_name, 
                    conclLit = TConsLit (cls, make_fixed_type_const tcons, tvars),
                    premLits = map TVarLit (union_all(map pack_sort tvars_srts))}
    end;
@@ -478,17 +458,21 @@
 fun dfg_sign true s = s
   | dfg_sign false s = "not(" ^ s ^ ")"
 
-fun dfg_of_typeLit (LTVar (s,ty)) = "not(" ^ s ^ "(" ^ ty ^ "))"
-  | dfg_of_typeLit (LTFree (s,ty)) = s ^ "(" ^ ty ^ ")";
+fun dfg_of_typeLit pos (LTVar (s,ty))  = dfg_sign pos (s ^ "(" ^ ty ^ ")")
+  | dfg_of_typeLit pos (LTFree (s,ty)) = dfg_sign pos (s ^ "(" ^ ty ^ ")");
 
 (*Enclose the clause body by quantifiers, if necessary*)
 fun dfg_forall [] body = body
   | dfg_forall vars body = "forall([" ^ commas vars ^ "],\n" ^ body ^ ")"
 
-fun gen_dfg_cls (cls_id, ax_name, knd, lits, vars) =
-    "clause( %(" ^ knd ^ ")\n" ^
-    dfg_forall vars ("or(" ^ lits ^ ")") ^ ",\n" ^
-    string_of_clausename (cls_id,ax_name) ^  ").\n\n";
+fun gen_dfg_cls (cls_id, ax_name, Axiom, lits, tylits, vars) =
+      "clause( %(axiom)\n" ^
+      dfg_forall vars ("or(" ^ commas (tylits@lits) ^ ")") ^ ",\n" ^
+      string_of_clausename (cls_id,ax_name) ^  ").\n\n"
+  | gen_dfg_cls (cls_id, ax_name, Conjecture, lits, _, vars) =
+      "clause( %(negated_conjecture)\n" ^
+      dfg_forall vars ("or(" ^ commas lits ^ ")") ^ ",\n" ^
+      string_of_clausename (cls_id,ax_name) ^  ").\n\n";
 
 fun string_of_arity (name, num) =  "(" ^ name ^ "," ^ Int.toString num ^ ")"
 
@@ -523,11 +507,11 @@
 
 fun string_of_ar axiom_name = arclause_prefix ^ ascii_of axiom_name;
 
-fun dfg_arity_clause (ArityClause{axiom_name,kind,conclLit,premLits,...}) =
+fun dfg_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) =
   let val TConsLit (_,_,tvars) = conclLit
       val lits = map dfg_of_arLit (conclLit :: premLits)
   in
-      "clause( %(" ^ name_of_kind kind ^ ")\n" ^
+      "clause( %(axiom)\n" ^
       dfg_forall tvars ("or( " ^ commas lits ^ ")") ^ ",\n" ^
       string_of_ar axiom_name ^ ").\n\n"
   end;
@@ -539,12 +523,15 @@
 fun tptp_sign true s = s
   | tptp_sign false s = "~ " ^ s
 
-fun tptp_of_typeLit (LTVar (s,ty))  = tptp_sign false (s ^ "(" ^ ty ^ ")")
-  | tptp_of_typeLit (LTFree (s,ty)) = tptp_sign true  (s ^ "(" ^ ty ^ ")");
+fun tptp_of_typeLit pos (LTVar (s,ty))  = tptp_sign pos (s ^ "(" ^ ty ^ ")")
+  | tptp_of_typeLit pos (LTFree (s,ty)) = tptp_sign pos  (s ^ "(" ^ ty ^ ")");
 
-fun gen_tptp_cls (cls_id,ax_name,knd,lits) =
-    "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^
-    name_of_kind knd ^ "," ^ tptp_pack lits ^ ").\n";
+fun gen_tptp_cls (cls_id,ax_name,Axiom,lits,tylits) =
+      "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ ",axiom," ^ 
+               tptp_pack (tylits@lits) ^ ").\n"
+  | gen_tptp_cls (cls_id,ax_name,Conjecture,lits,_) =
+      "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ ",negated_conjecture," ^ 
+               tptp_pack lits ^ ").\n";
 
 fun tptp_tfree_clause tfree_lit =
     "cnf(" ^ "tfree_tcs," ^ "negated_conjecture" ^ "," ^ tptp_pack[tfree_lit] ^ ").\n";
@@ -554,8 +541,8 @@
   | tptp_of_arLit (TVarLit (c,str)) =
       tptp_sign false (make_type_class c ^ "(" ^ str ^ ")")
 
-fun tptp_arity_clause (ArityClause{axiom_name,kind,conclLit,premLits,...}) =
-  "cnf(" ^ string_of_ar axiom_name ^ "," ^ name_of_kind kind ^ "," ^
+fun tptp_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) =
+  "cnf(" ^ string_of_ar axiom_name ^ ",axiom," ^
   tptp_pack (map tptp_of_arLit (conclLit :: premLits)) ^ ").\n";
 
 fun tptp_classrelLits sub sup =
diff -r 68a36883f0ad -r 340523598914 src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Tue Oct 09 17:11:20 2007 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML	Tue Oct 09 18:14:00 2007 +0200
@@ -97,9 +97,7 @@
                     th: thm,
                     kind: RC.kind,
                     literals: literal list,
-                    ctypes_sorts: (RC.typ_var * Term.sort) list,
-                    ctvar_type_literals: RC.type_literal list,
-                    ctfree_type_literals: RC.type_literal list};
+                    ctypes_sorts: (RC.typ_var * Term.sort) list};
 
 
 (*********************************************************************)
@@ -177,15 +175,12 @@
 (* making axiom and conjecture clauses *)
 fun make_clause thy (clause_id,axiom_name,kind,th) =
     let val (lits,ctypes_sorts) = literals_of_term thy (prop_of th)
-        val (ctvar_lits,ctfree_lits) = RC.add_typs_aux ctypes_sorts
     in
         if forall isFalse lits
         then error "Problem too trivial for resolution (empty clause)"
         else
             Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind,
-                    literals = lits, ctypes_sorts = ctypes_sorts,
-                    ctvar_type_literals = ctvar_lits,
-                    ctfree_type_literals = ctfree_lits}
+                    literals = lits, ctypes_sorts = ctypes_sorts}
     end;
 
 
@@ -302,34 +297,24 @@
 
 (*Given a clause, returns its literals paired with a list of literals concerning TFrees;
   the latter should only occur in conjecture clauses.*)
-fun tptp_type_lits (Clause cls) =
-    let val lits = map tptp_literal (#literals cls)
-        val ctvar_lits_strs = map RC.tptp_of_typeLit (#ctvar_type_literals cls)
-        val ctfree_lits = map RC.tptp_of_typeLit (#ctfree_type_literals cls)
-    in
-        (ctvar_lits_strs @ lits, ctfree_lits)
-    end;
+fun tptp_type_lits pos (Clause{literals, ctypes_sorts, ...}) =
+      (map tptp_literal literals, 
+       map (RC.tptp_of_typeLit pos) (RC.add_typs ctypes_sorts));
 
 fun clause2tptp (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
-    let val (lits,ctfree_lits) = tptp_type_lits cls
-        val cls_str = RC.gen_tptp_cls(clause_id,axiom_name,kind,lits)
-    in
-        (cls_str,ctfree_lits)
-    end;
+  let val (lits,tylits) = tptp_type_lits (kind = RC.Conjecture) cls
+  in
+      (RC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits)
+  end;
 
 
 (*** dfg format ***)
 
 fun dfg_literal (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate pred);
 
-fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) =
-  let val lits = map dfg_literal literals
-      val (tvar_lits,tfree_lits) = RC.add_typs_aux ctypes_sorts
-      val tvar_lits_strs = map RC.dfg_of_typeLit tvar_lits
-      val tfree_lits = map RC.dfg_of_typeLit tfree_lits
-  in
-      (tvar_lits_strs @ lits, tfree_lits)
-  end;
+fun dfg_type_lits pos (Clause{literals, ctypes_sorts, ...}) =
+      (map dfg_literal literals, 
+       map (RC.dfg_of_typeLit pos) (RC.add_typs ctypes_sorts));
 
 fun get_uvars (CombConst _) vars = vars
   | get_uvars (CombVar(v,_)) vars = (v::vars)
@@ -340,13 +325,13 @@
 fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals);
 
 fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
-    let val (lits,tfree_lits) = dfg_clause_aux cls
-        val vars = dfg_vars cls
-        val tvars = RC.get_tvar_strs ctypes_sorts
-        val knd = RC.name_of_kind kind
-        val lits_str = commas lits
-        val cls_str = RC.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars)
-    in (cls_str, tfree_lits) end;
+  let val (lits,tylits) = dfg_type_lits (kind = RC.Conjecture) cls
+      val vars = dfg_vars cls
+      val tvars = RC.get_tvar_strs ctypes_sorts
+  in
+      (RC.gen_dfg_cls(clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
+  end;
+
 
 (** For DFG format: accumulate function and predicate declarations **)
 
@@ -509,7 +494,6 @@
     end;
 
 
-
 (* dfg format *)
 
 fun dfg_write_file thy isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
diff -r 68a36883f0ad -r 340523598914 src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Tue Oct 09 17:11:20 2007 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Tue Oct 09 18:14:00 2007 +0200
@@ -404,7 +404,7 @@
   | add_nonnull_prfline ((lno, t, deps), lines) = (lno, t, deps) :: lines
 and delete_dep lno lines = foldr add_nonnull_prfline [] (map (replace_deps (lno, [])) lines);
 
-fun bad_free (Free (a,_)) = String.isPrefix "llabs_" a orelse String.isPrefix "sko_" a
+fun bad_free (Free (a,_)) = String.isPrefix "sko_" a
   | bad_free _ = false;
 
 (*TVars are forbidden in goals. Also, we don't want lines with <2 dependencies.
@@ -414,11 +414,11 @@
   phase may delete some dependencies, hence this phase comes later.*)
 fun add_wanted_prfline ((lno, t, []), (nlines, lines)) =
       (nlines, (lno, t, []) :: lines)   (*conjecture clauses must be kept*)
-  | add_wanted_prfline (line, (nlines, [])) = (nlines, [line])   (*final line must be kept*)
   | add_wanted_prfline ((lno, t, deps), (nlines, lines)) =
       if eq_types t orelse not (null (term_tvars t)) orelse
-         length deps < 2 orelse nlines mod !modulus <> 0 orelse
-         exists bad_free (term_frees t)
+         exists bad_free (term_frees t) orelse
+         (not (null lines) andalso   (*final line can't be deleted for these reasons*)
+          (length deps < 2 orelse nlines mod !modulus <> 0))   
       then (nlines+1, map (replace_deps (lno, deps)) lines) (*Delete line*)
       else (nlines+1, (lno, t, deps) :: lines);