context-based treatment of generalization; also handling TFrees in axiom clauses
authorpaulson
Tue Oct 09 18:14:00 2007 +0200 (2007-10-09)
changeset 24937340523598914
parent 24936 68a36883f0ad
child 24938 a220317465b4
context-based treatment of generalization; also handling TFrees in axiom clauses
src/HOL/MetisExamples/BigO.thy
src/HOL/MetisExamples/set.thy
src/HOL/Tools/meson.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_clause.ML
src/HOL/Tools/res_hol_clause.ML
src/HOL/Tools/res_reconstruct.ML
     1.1 --- a/src/HOL/MetisExamples/BigO.thy	Tue Oct 09 17:11:20 2007 +0200
     1.2 +++ b/src/HOL/MetisExamples/BigO.thy	Tue Oct 09 18:14:00 2007 +0200
     1.3 @@ -40,149 +40,64 @@
     1.4    apply (case_tac "c = 0", simp)
     1.5    apply (rule_tac x = "1" in exI, simp)
     1.6    apply (rule_tac x = "abs c" in exI, auto)
     1.7 -(*hand-modified to give 'a sort ordered_idom and X3 type 'a*)
     1.8  proof (neg_clausify)
     1.9  fix c x
    1.10 -assume 0: "\<And>A. \<bar>h A\<bar> \<le> c * \<bar>f A\<bar>"
    1.11 -assume 1: "c \<noteq> (0\<Colon>'a::ordered_idom)"
    1.12 -assume 2: "\<not> \<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>"
    1.13 -have 3: "\<And>X1 X3. \<bar>h X3\<bar> < X1 \<or> \<not> c * \<bar>f X3\<bar> < X1"
    1.14 -  by (metis order_le_less_trans 0)
    1.15 -have 4: "\<And>X3. (1\<Colon>'a) * X3 \<le> X3 \<or> \<not> (1\<Colon>'a) \<le> (1\<Colon>'a)"
    1.16 -  by (metis mult_le_cancel_right2)
    1.17 -have 5: "\<And>X3. (1\<Colon>'a) * X3 \<le> X3"
    1.18 -  by (metis 4 order_refl)
    1.19 -have 6: "\<And>X3. \<bar>0\<Colon>'a\<bar> = \<bar>X3\<bar> * (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (0\<Colon>'a)"
    1.20 -  by (metis abs_mult_pos mult_cancel_right1)
    1.21 -have 7: "\<bar>0\<Colon>'a\<bar> = (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (0\<Colon>'a)"
    1.22 -  by (metis 6 mult_cancel_right1)
    1.23 -have 8: "\<bar>0\<Colon>'a\<bar> = (0\<Colon>'a)"
    1.24 -  by (metis 7 order_refl)
    1.25 -have 9: "\<not> (0\<Colon>'a) < (0\<Colon>'a)"
    1.26 -  by (metis abs_not_less_zero 8)
    1.27 -have 10: "\<bar>(1\<Colon>'a) * (0\<Colon>'a)\<bar> = - ((1\<Colon>'a) * (0\<Colon>'a))"
    1.28 -  by (metis abs_of_nonpos 5)
    1.29 -have 11: "(0\<Colon>'a) = - ((1\<Colon>'a) * (0\<Colon>'a))"
    1.30 -  by (metis 10 mult_cancel_right1 8)
    1.31 -have 12: "(0\<Colon>'a) = - (0\<Colon>'a)"
    1.32 -  by (metis 11 mult_cancel_right1)
    1.33 -have 13: "\<And>X3. \<bar>X3\<bar> = X3 \<or> X3 \<le> (0\<Colon>'a)"
    1.34 -  by (metis abs_of_nonneg linorder_linear)
    1.35 -have 14: "c \<le> (0\<Colon>'a) \<or> \<not> \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
    1.36 -  by (metis 2 13)
    1.37 -have 15: "c \<le> (0\<Colon>'a)"
    1.38 -  by (metis 14 0)
    1.39 -have 16: "c = (0\<Colon>'a) \<or> c < (0\<Colon>'a)"
    1.40 -  by (metis linorder_antisym_conv2 15)
    1.41 -have 17: "\<bar>c\<bar> = - c"
    1.42 -  by (metis abs_of_nonpos 15)
    1.43 -have 18: "c < (0\<Colon>'a)"
    1.44 -  by (metis 16 1)
    1.45 -have 19: "\<not> \<bar>h x\<bar> \<le> - c * \<bar>f x\<bar>"
    1.46 -  by (metis 2 17)
    1.47 -have 20: "\<And>X3. X3 * (1\<Colon>'a) = X3"
    1.48 -  by (metis mult_cancel_right1 AC_mult.f.commute)
    1.49 -have 21: "\<And>X3. (0\<Colon>'a) \<le> X3 * X3"
    1.50 -  by (metis zero_le_square AC_mult.f.commute)
    1.51 -have 22: "(0\<Colon>'a) \<le> (1\<Colon>'a)"
    1.52 -  by (metis 21 mult_cancel_left1)
    1.53 -have 23: "\<And>X3. (0\<Colon>'a) = X3 \<or> (0\<Colon>'a) \<noteq> - X3"
    1.54 -  by (metis neg_equal_iff_equal 12)
    1.55 -have 24: "\<And>X3. (0\<Colon>'a) = - X3 \<or> X3 \<noteq> (0\<Colon>'a)"
    1.56 -  by (metis 23 minus_equation_iff)
    1.57 -have 25: "\<And>X3. \<bar>0\<Colon>'a\<bar> = \<bar>X3\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
    1.58 -  by metis
    1.59 -have 26: "\<And>X3. (0\<Colon>'a) = \<bar>X3\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
    1.60 -  by (metis 8)
    1.61 -have 27: "\<And>X1 X3. (0\<Colon>'a) * \<bar>X1\<bar> = \<bar>X3 * X1\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
    1.62 -  by (metis abs_mult 26)
    1.63 -have 28: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
    1.64 -  by (metis 27 mult_cancel_left1)
    1.65 -have 29: "\<And>X1 X3. (0\<Colon>'a) = X3 * X1 \<or> (0\<Colon>'a) < (0\<Colon>'a) \<or> X3 \<noteq> (0\<Colon>'a)"
    1.66 -  by (metis zero_less_abs_iff 28)
    1.67 -have 30: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> X3 \<noteq> (0\<Colon>'a)"
    1.68 -  by (metis 29 9)
    1.69 -have 31: "\<And>X1 X3. (0\<Colon>'a) = X1 * X3 \<or> X3 \<noteq> (0\<Colon>'a)"
    1.70 -  by (metis AC_mult.f.commute 30)
    1.71 -have 32: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<bar>X1\<bar> \<noteq> (0\<Colon>'a)"
    1.72 -  by (metis abs_mult 31)
    1.73 -have 33: "\<And>X3::'a. \<bar>X3 * X3\<bar> = X3 * X3"
    1.74 -  by (metis abs_mult_self abs_mult)
    1.75 -have 34: "\<And>X3. (0\<Colon>'a) \<le> \<bar>X3\<bar> \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
    1.76 -  by (metis abs_ge_zero abs_mult_pos 20)
    1.77 -have 35: "\<And>X3. (0\<Colon>'a) \<le> \<bar>X3\<bar>"
    1.78 -  by (metis 34 22)
    1.79 -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)"
    1.80 -  by (metis abs_eq_0 abs_mult_pos 20)
    1.81 -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)"
    1.82 -  by (metis 36 20)
    1.83 -have 38: "\<And>X3. X3 = (0\<Colon>'a) \<or> \<bar>X3\<bar> \<noteq> (0\<Colon>'a)"
    1.84 -  by (metis 37 22)
    1.85 -have 39: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> \<bar>X1\<bar> \<noteq> (0\<Colon>'a)"
    1.86 -  by (metis 38 32)
    1.87 -have 40: "\<And>X3::'a. \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar> \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
    1.88 -  by (metis abs_idempotent abs_mult_pos 20)
    1.89 -have 41: "\<And>X3::'a. \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar>"
    1.90 -  by (metis 40 22)
    1.91 -have 42: "\<And>X3. \<not> \<bar>X3\<bar> < (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
    1.92 -  by (metis abs_not_less_zero abs_mult_pos 20)
    1.93 -have 43: "\<And>X3. \<not> \<bar>X3\<bar> < (0\<Colon>'a)"
    1.94 -  by (metis 42 22)
    1.95 -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)"
    1.96 -  by (metis abs_le_zero_iff abs_mult_pos 20)
    1.97 -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)"
    1.98 -  by (metis 44 20)
    1.99 -have 46: "\<And>X3. X3 = (0\<Colon>'a) \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a)"
   1.100 -  by (metis 45 22)
   1.101 -have 47: "\<And>X3. X3 * X3 = (0\<Colon>'a) \<or> \<not> X3 * X3 \<le> (0\<Colon>'a)"
   1.102 -  by (metis 46 33)
   1.103 -have 48: "\<And>X3. X3 * X3 = (0\<Colon>'a) \<or> \<not> X3 \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> X3"
   1.104 -  by (metis 47 mult_le_0_iff)
   1.105 -have 49: "\<And>X3. \<bar>X3\<bar> = (0\<Colon>'a) \<or> \<not> X3 \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> X3"
   1.106 -  by (metis mult_eq_0_iff abs_mult_self 48)
   1.107 -have 50: "\<And>X1 X3.
   1.108 -   (0\<Colon>'a) * \<bar>X1\<bar> = \<bar>\<bar>X3 * X1\<bar>\<bar> \<or>
   1.109 -   \<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>"
   1.110 -  by (metis abs_mult_pos abs_mult 49)
   1.111 -have 51: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> \<not> X1 \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> X1"
   1.112 -  by (metis 39 49)
   1.113 -have 52: "\<And>X1 X3.
   1.114 -   (0\<Colon>'a) = \<bar>\<bar>X3 * X1\<bar>\<bar> \<or>
   1.115 -   \<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>"
   1.116 -  by (metis 50 mult_cancel_left1)
   1.117 -have 53: "\<And>X1 X3.
   1.118 -   (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>"
   1.119 -  by (metis 52 41)
   1.120 -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>"
   1.121 -  by (metis 53 35)
   1.122 -have 55: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a)"
   1.123 -  by (metis 54 35)
   1.124 -have 56: "\<And>X1 X3. \<bar>X1 * X3\<bar> = (0\<Colon>'a) \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a)"
   1.125 -  by (metis 55 AC_mult.f.commute)
   1.126 -have 57: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> \<not> \<bar>X1\<bar> \<le> (0\<Colon>'a)"
   1.127 -  by (metis 38 56)
   1.128 -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>"
   1.129 -  by (metis 0 51)
   1.130 -have 59: "\<And>X3. \<bar>h X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> \<bar>f X3\<bar> \<le> (0\<Colon>'a)"
   1.131 -  by (metis 58 35)
   1.132 -have 60: "\<And>X3. \<bar>h X3\<bar> \<le> (0\<Colon>'a) \<or> (0\<Colon>'a) < \<bar>f X3\<bar>"
   1.133 -  by (metis 59 linorder_not_le)
   1.134 -have 61: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> (0\<Colon>'a) < \<bar>X1\<bar>"
   1.135 -  by (metis 57 linorder_not_le)
   1.136 -have 62: "(0\<Colon>'a) < \<bar>\<bar>f x\<bar>\<bar> \<or> \<not> \<bar>h x\<bar> \<le> (0\<Colon>'a)"
   1.137 -  by (metis 19 61)
   1.138 -have 63: "(0\<Colon>'a) < \<bar>f x\<bar> \<or> \<not> \<bar>h x\<bar> \<le> (0\<Colon>'a)"
   1.139 -  by (metis 62 41)
   1.140 -have 64: "(0\<Colon>'a) < \<bar>f x\<bar>"
   1.141 -  by (metis 63 60)
   1.142 -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>"
   1.143 -  by (metis 3 mult_less_0_iff)
   1.144 -have 66: "\<And>X3. \<bar>h X3\<bar> < (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) < \<bar>f X3\<bar>"
   1.145 -  by (metis 65 18)
   1.146 -have 67: "\<And>X3. \<not> (0\<Colon>'a) < \<bar>f X3\<bar>"
   1.147 -  by (metis 66 43)
   1.148 +have 0: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<bar>X1 * X2\<bar> = \<bar>X2 * X1\<bar>"
   1.149 +  by (metis abs_mult mult_commute)
   1.150 +have 1: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
   1.151 +   X1 \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or> \<bar>X2\<bar> * X1 = \<bar>X2 * X1\<bar>"
   1.152 +  by (metis abs_mult_pos linorder_linear)
   1.153 +have 2: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
   1.154 +   \<not> (0\<Colon>'a\<Colon>ordered_idom) < X1 * X2 \<or>
   1.155 +   \<not> (0\<Colon>'a\<Colon>ordered_idom) \<le> X2 \<or> \<not> X1 \<le> (0\<Colon>'a\<Colon>ordered_idom)"
   1.156 +  by (metis linorder_not_less mult_nonneg_nonpos2)
   1.157 +assume 3: "\<And>x\<Colon>'b\<Colon>type.
   1.158 +   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>
   1.159 +   \<le> (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
   1.160 +assume 4: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
   1.161 +  \<le> \<bar>c\<Colon>'a\<Colon>ordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
   1.162 +have 5: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
   1.163 +  \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
   1.164 +  by (metis 4 abs_mult)
   1.165 +have 6: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
   1.166 +   \<not> X1 \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or> X1 \<le> \<bar>X2\<bar>"
   1.167 +  by (metis abs_ge_zero xt1(6))
   1.168 +have 7: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
   1.169 +   X1 \<le> \<bar>X2\<bar> \<or> (0\<Colon>'a\<Colon>ordered_idom) < X1"
   1.170 +  by (metis not_leE 6)
   1.171 +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>"
   1.172 +  by (metis 5 7)
   1.173 +have 9: "\<And>X1\<Colon>'a\<Colon>ordered_idom.
   1.174 +   \<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar> \<le> X1 \<or>
   1.175 +   (0\<Colon>'a\<Colon>ordered_idom) < X1"
   1.176 +  by (metis 8 order_less_le_trans)
   1.177 +have 10: "(0\<Colon>'a\<Colon>ordered_idom)
   1.178 +< (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
   1.179 +  by (metis 3 9)
   1.180 +have 11: "\<not> (c\<Colon>'a\<Colon>ordered_idom) \<le> (0\<Colon>'a\<Colon>ordered_idom)"
   1.181 +  by (metis abs_ge_zero 2 10)
   1.182 +have 12: "\<And>X1\<Colon>'a\<Colon>ordered_idom. (c\<Colon>'a\<Colon>ordered_idom) * \<bar>X1\<bar> = \<bar>X1 * c\<bar>"
   1.183 +  by (metis mult_commute 1 11)
   1.184 +have 13: "\<And>X1\<Colon>'b\<Colon>type.
   1.185 +   - (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1
   1.186 +   \<le> (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1\<bar>"
   1.187 +  by (metis 3 abs_le_D2)
   1.188 +have 14: "\<And>X1\<Colon>'b\<Colon>type.
   1.189 +   - (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1
   1.190 +   \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1\<bar>"
   1.191 +  by (metis 0 12 13)
   1.192 +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>"
   1.193 +  by (metis abs_mult abs_mult_pos abs_ge_zero)
   1.194 +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"
   1.195 +  by (metis xt1(6) abs_ge_self)
   1.196 +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>"
   1.197 +  by (metis 16 abs_le_D1)
   1.198 +have 18: "\<And>X1\<Colon>'b\<Colon>type.
   1.199 +   (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1
   1.200 +   \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1\<bar>"
   1.201 +  by (metis 17 3 15)
   1.202  show "False"
   1.203 -  by (metis 67 64)
   1.204 +  by (metis abs_le_iff 5 18 14)
   1.205  qed
   1.206  
   1.207  lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
   1.208 @@ -195,76 +110,34 @@
   1.209  ML{*ResReconstruct.modulus:=2*}
   1.210  proof (neg_clausify)
   1.211  fix c x
   1.212 -assume 0: "\<And>A. \<bar>h A\<bar> \<le> c * \<bar>f A\<bar>"
   1.213 -assume 1: "c \<noteq> (0\<Colon>'a::ordered_idom)"
   1.214 -assume 2: "\<not> \<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>"
   1.215 -have 3: "\<And>X3. (1\<Colon>'a) * X3 \<le> X3"
   1.216 -  by (metis mult_le_cancel_right2 order_refl order_refl)
   1.217 -have 4: "\<bar>0\<Colon>'a\<bar> = (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (0\<Colon>'a)"
   1.218 -  by (metis abs_mult_pos mult_cancel_right1 mult_cancel_right1)
   1.219 -have 5: "\<not> (0\<Colon>'a) < (0\<Colon>'a)"
   1.220 -  by (metis abs_not_less_zero 4 order_refl)
   1.221 -have 6: "(0\<Colon>'a) = - ((1\<Colon>'a) * (0\<Colon>'a))"
   1.222 -  by (metis abs_of_nonpos 3 mult_cancel_right1 4 order_refl)
   1.223 -have 7: "\<And>X3. \<bar>X3\<bar> = X3 \<or> X3 \<le> (0\<Colon>'a)"
   1.224 -  by (metis abs_of_nonneg linorder_linear)
   1.225 -have 8: "c \<le> (0\<Colon>'a)"
   1.226 -  by (metis 2 7 0)
   1.227 -have 9: "\<bar>c\<bar> = - c"
   1.228 -  by (metis abs_of_nonpos 8)
   1.229 -have 10: "\<not> \<bar>h x\<bar> \<le> - c * \<bar>f x\<bar>"
   1.230 -  by (metis 2 9)
   1.231 -have 11: "\<And>X3. X3 * (1\<Colon>'a) = X3"
   1.232 -  by (metis mult_cancel_right1 AC_mult.f.commute)
   1.233 -have 12: "(0\<Colon>'a) \<le> (1\<Colon>'a)"
   1.234 -  by (metis zero_le_square AC_mult.f.commute mult_cancel_left1)
   1.235 -have 13: "\<And>X3. (0\<Colon>'a) = - X3 \<or> X3 \<noteq> (0\<Colon>'a)"
   1.236 -  by (metis neg_equal_iff_equal 6 mult_cancel_right1 minus_equation_iff)
   1.237 -have 14: "\<And>X3. (0\<Colon>'a) = \<bar>X3\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
   1.238 -  by (metis abs_minus_cancel 13 4 order_refl)
   1.239 -have 15: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
   1.240 -  by (metis abs_mult 14 mult_cancel_left1)
   1.241 -have 16: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> X3 \<noteq> (0\<Colon>'a)"
   1.242 -  by (metis zero_less_abs_iff 15 5)
   1.243 -have 17: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<bar>X1\<bar> \<noteq> (0\<Colon>'a)"
   1.244 -  by (metis abs_mult AC_mult.f.commute 16)
   1.245 -have 18: "\<And>X3. (0\<Colon>'a) \<le> \<bar>X3\<bar>"
   1.246 -  by (metis abs_ge_zero abs_mult_pos 11 12)
   1.247 -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)"
   1.248 -  by (metis abs_eq_0 abs_mult_pos 11)
   1.249 -have 20: "\<And>X3. X3 = (0\<Colon>'a) \<or> \<bar>X3\<bar> \<noteq> (0\<Colon>'a)"
   1.250 -  by (metis 19 11 12)
   1.251 -have 21: "\<And>X3::'a. \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar> \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
   1.252 -  by (metis abs_idempotent abs_mult_pos 11)
   1.253 -have 22: "\<And>X3. \<not> \<bar>X3\<bar> < (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
   1.254 -  by (metis abs_not_less_zero abs_mult_pos 11)
   1.255 -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)"
   1.256 -  by (metis abs_le_zero_iff abs_mult_pos 11 11)
   1.257 -have 24: "\<And>X3. X3 * X3 = (0\<Colon>'a) \<or> \<not> X3 * X3 \<le> (0\<Colon>'a)"
   1.258 -  by (metis 23 12 abs_mult_self abs_mult AC_mult.f.commute)
   1.259 -have 25: "\<And>X3. \<bar>X3\<bar> = (0\<Colon>'a) \<or> \<not> X3 \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> X3"
   1.260 -  by (metis mult_eq_0_iff abs_mult_self 24 mult_le_0_iff)
   1.261 -have 26: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> \<not> X1 \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> X1"
   1.262 -  by (metis 20 17 25)
   1.263 -have 27: "\<And>X1 X3.
   1.264 -   (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>"
   1.265 -  by (metis abs_mult_pos abs_mult 25 mult_cancel_left1 21 12)
   1.266 -have 28: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a)"
   1.267 -  by (metis 27 18 18)
   1.268 -have 29: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> \<not> \<bar>X1\<bar> \<le> (0\<Colon>'a)"
   1.269 -  by (metis 20 28 AC_mult.f.commute)
   1.270 -have 30: "\<And>X3. \<bar>h X3\<bar> \<le> (0\<Colon>'a) \<or> \<not> \<bar>f X3\<bar> \<le> (0\<Colon>'a)"
   1.271 -  by (metis 0 26 18)
   1.272 -have 31: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> (0\<Colon>'a) < \<bar>X1\<bar>"
   1.273 -  by (metis 29 linorder_not_le)
   1.274 -have 32: "(0\<Colon>'a) < \<bar>f x\<bar> \<or> \<not> \<bar>h x\<bar> \<le> (0\<Colon>'a)"
   1.275 -  by (metis 10 31 21 12)
   1.276 -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>"
   1.277 -  by (metis order_le_less_trans 0 mult_less_0_iff)
   1.278 -have 34: "\<And>X3. \<not> (0\<Colon>'a) < \<bar>f X3\<bar>"
   1.279 -  by (metis 33 linorder_antisym_conv2 8 1 22 12)
   1.280 +have 0: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<bar>X1 * X2\<bar> = \<bar>X2 * X1\<bar>"
   1.281 +  by (metis abs_mult mult_commute)
   1.282 +assume 1: "\<And>x\<Colon>'b\<Colon>type.
   1.283 +   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>
   1.284 +   \<le> (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
   1.285 +assume 2: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
   1.286 +  \<le> \<bar>c\<Colon>'a\<Colon>ordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
   1.287 +have 3: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
   1.288 +  \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
   1.289 +  by (metis 2 abs_mult)
   1.290 +have 4: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
   1.291 +   \<not> X1 \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or> X1 \<le> \<bar>X2\<bar>"
   1.292 +  by (metis abs_ge_zero xt1(6))
   1.293 +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>"
   1.294 +  by (metis not_leE 4 3)
   1.295 +have 6: "(0\<Colon>'a\<Colon>ordered_idom)
   1.296 +< (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
   1.297 +  by (metis 1 order_less_le_trans 5)
   1.298 +have 7: "\<And>X1\<Colon>'a\<Colon>ordered_idom. (c\<Colon>'a\<Colon>ordered_idom) * \<bar>X1\<bar> = \<bar>X1 * c\<bar>"
   1.299 +  by (metis abs_ge_zero linorder_not_less mult_nonneg_nonpos2 6 linorder_linear abs_mult_pos mult_commute)
   1.300 +have 8: "\<And>X1\<Colon>'b\<Colon>type.
   1.301 +   - (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1
   1.302 +   \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1\<bar>"
   1.303 +  by (metis 0 7 abs_le_D2 1)
   1.304 +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>"
   1.305 +  by (metis abs_ge_self xt1(6) abs_le_D1)
   1.306  show "False"
   1.307 -  by (metis 34 32 30 linorder_not_le)
   1.308 +  by (metis 8 abs_ge_zero abs_mult_pos abs_mult 1 9 3 abs_le_iff)
   1.309  qed
   1.310  
   1.311  lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
   1.312 @@ -277,133 +150,24 @@
   1.313  ML{*ResReconstruct.modulus:=3*}
   1.314  proof (neg_clausify)
   1.315  fix c x
   1.316 -assume 0: "\<And>A\<Colon>'b\<Colon>type.
   1.317 -   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) A\<bar>
   1.318 -   \<le> (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) A\<bar>"
   1.319 -assume 1: "(c\<Colon>'a\<Colon>ordered_idom) \<noteq> (0\<Colon>'a\<Colon>ordered_idom)"
   1.320 -assume 2: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
   1.321 +assume 0: "\<And>x\<Colon>'b\<Colon>type.
   1.322 +   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>
   1.323 +   \<le> (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
   1.324 +assume 1: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
   1.325    \<le> \<bar>c\<Colon>'a\<Colon>ordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
   1.326 -have 3: "\<And>X3\<Colon>'a\<Colon>ordered_idom. (1\<Colon>'a\<Colon>ordered_idom) * X3 \<le> X3"
   1.327 -  by (metis mult_le_cancel_right2 order_refl order_refl)
   1.328 -have 4: "\<bar>0\<Colon>'a\<Colon>ordered_idom\<bar> = (0\<Colon>'a\<Colon>ordered_idom)"
   1.329 -  by (metis abs_mult_pos mult_cancel_right1 mult_cancel_right1 order_refl)
   1.330 -have 5: "(0\<Colon>'a\<Colon>ordered_idom) = - ((1\<Colon>'a\<Colon>ordered_idom) * (0\<Colon>'a\<Colon>ordered_idom))"
   1.331 -  by (metis abs_of_nonpos 3 mult_cancel_right1 4)
   1.332 -have 6: "(c\<Colon>'a\<Colon>ordered_idom) \<le> (0\<Colon>'a\<Colon>ordered_idom)"
   1.333 -  by (metis 2 abs_of_nonneg linorder_linear 0)
   1.334 -have 7: "(c\<Colon>'a\<Colon>ordered_idom) < (0\<Colon>'a\<Colon>ordered_idom)"
   1.335 -  by (metis linorder_antisym_conv2 6 1)
   1.336 -have 8: "\<And>X3\<Colon>'a\<Colon>ordered_idom. X3 * (1\<Colon>'a\<Colon>ordered_idom) = X3"
   1.337 -  by (metis mult_cancel_right1 AC_mult.f.commute)
   1.338 -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"
   1.339 -  by (metis neg_equal_iff_equal 5 mult_cancel_right1)
   1.340 -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)"
   1.341 -  by (metis abs_minus_cancel 9 minus_equation_iff 4)
   1.342 -have 11: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X3\<Colon>'a\<Colon>ordered_idom.
   1.343 -   (0\<Colon>'a\<Colon>ordered_idom) * \<bar>X1\<bar> = \<bar>X3 * X1\<bar> \<or> X3 \<noteq> (0\<Colon>'a\<Colon>ordered_idom)"
   1.344 -  by (metis abs_mult 10)
   1.345 -have 12: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X3\<Colon>'a\<Colon>ordered_idom.
   1.346 -   X3 * X1 = (0\<Colon>'a\<Colon>ordered_idom) \<or> X3 \<noteq> (0\<Colon>'a\<Colon>ordered_idom)"
   1.347 -  by (metis zero_less_abs_iff 11 mult_cancel_left1 abs_not_less_zero 4)
   1.348 -have 13: "\<And>X3\<Colon>'a\<Colon>ordered_idom. \<bar>X3 * X3\<bar> = X3 * X3"
   1.349 -  by (metis abs_mult_self abs_mult AC_mult.f.commute)
   1.350 -have 14: "\<And>X3\<Colon>'a\<Colon>ordered_idom. (0\<Colon>'a\<Colon>ordered_idom) \<le> \<bar>X3\<bar>"
   1.351 -  by (metis abs_ge_zero abs_mult_pos 8 zero_le_square AC_mult.f.commute mult_cancel_left1)
   1.352 -have 15: "\<And>X3\<Colon>'a\<Colon>ordered_idom.
   1.353 -   X3 = (0\<Colon>'a\<Colon>ordered_idom) \<or>
   1.354 -   \<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)"
   1.355 -  by (metis abs_eq_0 abs_mult_pos 8 8)
   1.356 -have 16: "\<And>X3\<Colon>'a\<Colon>ordered_idom.
   1.357 -   \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar> \<or> \<not> (0\<Colon>'a\<Colon>ordered_idom) \<le> (1\<Colon>'a\<Colon>ordered_idom)"
   1.358 -  by (metis abs_idempotent abs_mult_pos 8)
   1.359 -have 17: "\<And>X3\<Colon>'a\<Colon>ordered_idom. \<not> \<bar>X3\<bar> < (0\<Colon>'a\<Colon>ordered_idom)"
   1.360 -  by (metis abs_not_less_zero abs_mult_pos 8 zero_le_square AC_mult.f.commute mult_cancel_left1)
   1.361 -have 18: "\<And>X3\<Colon>'a\<Colon>ordered_idom.
   1.362 -   X3 = (0\<Colon>'a\<Colon>ordered_idom) \<or>
   1.363 -   \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or>
   1.364 -   \<not> (0\<Colon>'a\<Colon>ordered_idom) \<le> (1\<Colon>'a\<Colon>ordered_idom)"
   1.365 -  by (metis abs_le_zero_iff abs_mult_pos 8 8)
   1.366 -have 19: "\<And>X3\<Colon>'a\<Colon>ordered_idom.
   1.367 -   X3 * X3 = (0\<Colon>'a\<Colon>ordered_idom) \<or>
   1.368 -   \<not> X3 \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or> \<not> (0\<Colon>'a\<Colon>ordered_idom) \<le> X3"
   1.369 -  by (metis 18 zero_le_square AC_mult.f.commute mult_cancel_left1 13 mult_le_0_iff)
   1.370 -have 20: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X3\<Colon>'a\<Colon>ordered_idom.
   1.371 -   X3 * X1 = (0\<Colon>'a\<Colon>ordered_idom) \<or>
   1.372 -   \<not> X1 \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or> \<not> (0\<Colon>'a\<Colon>ordered_idom) \<le> X1"
   1.373 -  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)
   1.374 -have 21: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X3\<Colon>'a\<Colon>ordered_idom.
   1.375 -   (0\<Colon>'a\<Colon>ordered_idom) = \<bar>X3 * X1\<bar> \<or>
   1.376 -   \<not> \<bar>X3\<bar> \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or> \<not> (0\<Colon>'a\<Colon>ordered_idom) \<le> \<bar>X3\<bar>"
   1.377 -  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)
   1.378 -have 22: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X3\<Colon>'a\<Colon>ordered_idom.
   1.379 -   X3 * X1 = (0\<Colon>'a\<Colon>ordered_idom) \<or> \<not> \<bar>X1\<bar> \<le> (0\<Colon>'a\<Colon>ordered_idom)"
   1.380 -  by (metis 15 zero_le_square AC_mult.f.commute mult_cancel_left1 21 14 AC_mult.f.commute)
   1.381 -have 23: "\<And>X3\<Colon>'b\<Colon>type.
   1.382 -   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X3\<bar> \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or>
   1.383 -   (0\<Colon>'a\<Colon>ordered_idom) < \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X3\<bar>"
   1.384 -  by (metis 0 20 14 linorder_not_le)
   1.385 -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>
   1.386 -\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar> \<le> (0\<Colon>'a\<Colon>ordered_idom)"
   1.387 -  by (metis 2 abs_of_nonpos 6 22 linorder_not_le 16 zero_le_square AC_mult.f.commute mult_cancel_left1)
   1.388 -have 25: "\<And>X3\<Colon>'b\<Colon>type.
   1.389 -   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X3\<bar> < (0\<Colon>'a\<Colon>ordered_idom) \<or>
   1.390 -   \<not> (0\<Colon>'a\<Colon>ordered_idom) < \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X3\<bar>"
   1.391 -  by (metis order_le_less_trans 0 mult_less_0_iff 7)
   1.392 +have 2: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
   1.393 +   X1 \<le> \<bar>X2\<bar> \<or> (0\<Colon>'a\<Colon>ordered_idom) < X1"
   1.394 +  by (metis abs_ge_zero xt1(6) not_leE)
   1.395 +have 3: "\<not> (c\<Colon>'a\<Colon>ordered_idom) \<le> (0\<Colon>'a\<Colon>ordered_idom)"
   1.396 +  by (metis abs_ge_zero mult_nonneg_nonpos2 linorder_not_less order_less_le_trans 1 abs_mult 2 0)
   1.397 +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>"
   1.398 +  by (metis abs_ge_zero abs_mult_pos abs_mult)
   1.399 +have 5: "\<And>X1\<Colon>'b\<Colon>type.
   1.400 +   (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1
   1.401 +   \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1\<bar>"
   1.402 +  by (metis 4 0 xt1(6) abs_ge_self abs_le_D1)
   1.403  show "False"
   1.404 -  by (metis 25 17 24 23)
   1.405 -qed
   1.406 -
   1.407 -lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
   1.408 -    ALL x. (abs (h x)) <= (c * (abs (f x))))
   1.409 -      = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
   1.410 -  apply auto
   1.411 -  apply (case_tac "c = 0", simp)
   1.412 -  apply (rule_tac x = "1" in exI, simp)
   1.413 -  apply (rule_tac x = "abs c" in exI, auto);
   1.414 -ML{*ResReconstruct.modulus:=4*}
   1.415 -ML{*ResReconstruct.recon_sorts:=false*}
   1.416 -proof (neg_clausify)
   1.417 -fix c x
   1.418 -assume 0: "\<And>A. \<bar>h A\<bar> \<le> c * \<bar>f A\<bar>"
   1.419 -assume 1: "c \<noteq> (0\<Colon>'a)"
   1.420 -assume 2: "\<not> \<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>"
   1.421 -have 3: "\<And>X3. (1\<Colon>'a) * X3 \<le> X3"
   1.422 -  by (metis mult_le_cancel_right2 order_refl order_refl)
   1.423 -have 4: "\<not> (0\<Colon>'a) < (0\<Colon>'a)"
   1.424 -  by (metis abs_not_less_zero abs_mult_pos mult_cancel_right1 mult_cancel_right1 order_refl)
   1.425 -have 5: "c \<le> (0\<Colon>'a)"
   1.426 -  by (metis 2 abs_of_nonneg linorder_linear 0)
   1.427 -have 6: "\<not> \<bar>h x\<bar> \<le> - c * \<bar>f x\<bar>"
   1.428 -  by (metis 2 abs_of_nonpos 5)
   1.429 -have 7: "(0\<Colon>'a) \<le> (1\<Colon>'a)"
   1.430 -  by (metis zero_le_square AC_mult.f.commute mult_cancel_left1)
   1.431 -have 8: "\<And>X3. (0\<Colon>'a) = \<bar>X3\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
   1.432 -  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)
   1.433 -have 9: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> X3 \<noteq> (0\<Colon>'a)"
   1.434 -  by (metis abs_mult 8 mult_cancel_left1)
   1.435 -have 10: "\<And>X1 X3. (0\<Colon>'a) = \<bar>X3 * X1\<bar> \<or> \<bar>X1\<bar> \<noteq> (0\<Colon>'a)"
   1.436 -  by (metis abs_mult AC_mult.f.commute zero_less_abs_iff 9 4)
   1.437 -have 11: "\<And>X3. (0\<Colon>'a) \<le> \<bar>X3\<bar>"
   1.438 -  by (metis abs_ge_zero abs_mult_pos mult_cancel_right1 AC_mult.f.commute 7)
   1.439 -have 12: "\<And>X3. X3 = (0\<Colon>'a) \<or> \<bar>X3\<bar> \<noteq> (0\<Colon>'a)"
   1.440 -  by (metis abs_eq_0 abs_mult_pos mult_cancel_right1 AC_mult.f.commute mult_cancel_right1 AC_mult.f.commute 7)
   1.441 -have 13: "\<And>X3. \<not> \<bar>X3\<bar> < (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> (1\<Colon>'a)"
   1.442 -  by (metis abs_not_less_zero abs_mult_pos mult_cancel_right1 AC_mult.f.commute)
   1.443 -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)"
   1.444 -  by (metis abs_le_zero_iff abs_mult_pos mult_cancel_right1 AC_mult.f.commute mult_cancel_right1 AC_mult.f.commute)
   1.445 -have 15: "\<And>X3. \<bar>X3\<bar> = (0\<Colon>'a) \<or> \<not> X3 \<le> (0\<Colon>'a) \<or> \<not> (0\<Colon>'a) \<le> X3"
   1.446 -  by (metis mult_eq_0_iff abs_mult_self 14 7 abs_mult_self abs_mult AC_mult.f.commute mult_le_0_iff)
   1.447 -have 16: "\<And>X1 X3.
   1.448 -   (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>"
   1.449 -  by (metis abs_mult_pos abs_mult 15 mult_cancel_left1 abs_idempotent abs_mult_pos mult_cancel_right1 AC_mult.f.commute 7)
   1.450 -have 17: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> \<not> \<bar>X1\<bar> \<le> (0\<Colon>'a)"
   1.451 -  by (metis 12 16 11 11 AC_mult.f.commute)
   1.452 -have 18: "\<And>X1 X3. X3 * X1 = (0\<Colon>'a) \<or> (0\<Colon>'a) < \<bar>X1\<bar>"
   1.453 -  by (metis 17 linorder_not_le)
   1.454 -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>"
   1.455 -  by (metis order_le_less_trans 0 mult_less_0_iff)
   1.456 -show "False"
   1.457 -  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)
   1.458 +  by (metis abs_mult mult_commute 3 abs_mult_pos linorder_linear 0 abs_le_D2 5 1 abs_le_iff)
   1.459  qed
   1.460  
   1.461  
   1.462 @@ -474,14 +238,12 @@
   1.463    apply(auto simp add: bigo_def)
   1.464  proof (neg_clausify)
   1.465  fix x
   1.466 -assume 0: "\<And>mes_pSG\<Colon>'b\<Colon>ordered_idom.
   1.467 -   \<not> \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) mes_pSG)\<bar>
   1.468 -     \<le> mes_pSG * \<bar>f (x mes_pSG)\<bar>"
   1.469 -have 1: "\<And>X3\<Colon>'b. X3 \<le> (1\<Colon>'b) * X3 \<or> \<not> (1\<Colon>'b) \<le> (1\<Colon>'b)"
   1.470 -  by (metis Ring_and_Field.mult_le_cancel_right1 order_refl)
   1.471 -have 2: "\<And>X3\<Colon>'b. X3 \<le> (1\<Colon>'b) * X3"
   1.472 -  by (metis 1 order_refl)
   1.473 -show 3: "False"
   1.474 +assume 0: "\<And>xa. \<not> \<bar>f (x xa)\<bar> \<le> xa * \<bar>f (x xa)\<bar>"
   1.475 +have 1: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2 \<or> \<not> (1\<Colon>'b) \<le> (1\<Colon>'b)"
   1.476 +  by (metis mult_le_cancel_right1 order_eq_iff)
   1.477 +have 2: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2"
   1.478 +  by (metis order_eq_iff 1)
   1.479 +show "False"
   1.480    by (metis 0 2)
   1.481  qed
   1.482  
   1.483 @@ -490,15 +252,11 @@
   1.484    apply (auto simp add: bigo_def func_zero)
   1.485  proof (neg_clausify)
   1.486  fix x
   1.487 -assume 0: "\<And>mes_mVM\<Colon>'b\<Colon>ordered_idom.
   1.488 -   \<not> (0\<Colon>'b\<Colon>ordered_idom)
   1.489 -     \<le> mes_mVM *
   1.490 -       \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom)
   1.491 -         ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) mes_mVM)\<bar>"
   1.492 -have 1: "(0\<Colon>'b\<Colon>ordered_idom) < (0\<Colon>'b\<Colon>ordered_idom)"
   1.493 -  by (metis 0 Ring_and_Field.mult_le_cancel_left1)
   1.494 -show 2: "False"
   1.495 -  by (metis Orderings.linorder_class.neq_iff 1)
   1.496 +assume 0: "\<And>xa. \<not> (0\<Colon>'b) \<le> xa * \<bar>g (x xa)\<bar>"
   1.497 +have 1: "\<not> (0\<Colon>'b) \<le> (0\<Colon>'b)"
   1.498 +  by (metis 0 mult_eq_0_iff)
   1.499 +show "False"
   1.500 +  by (metis 1 linorder_neq_iff linorder_antisym_conv1)
   1.501  qed
   1.502  
   1.503  lemma bigo_zero2: "O(%x.0) = {%x.0}"
   1.504 @@ -637,70 +395,48 @@
   1.505  (*Version 2: single-step proof*)
   1.506  proof (neg_clausify)
   1.507  fix x
   1.508 -assume 0: "\<And>mes_mbt\<Colon>'a.
   1.509 -   (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) mes_mbt
   1.510 -   \<le> (c\<Colon>'b\<Colon>ordered_idom) * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) mes_mbt"
   1.511 -assume 1: "\<And>mes_mbs\<Colon>'b\<Colon>ordered_idom.
   1.512 -   \<not> (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) mes_mbs)
   1.513 -     \<le> mes_mbs * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x mes_mbs)\<bar>"
   1.514 -have 2: "\<And>X3\<Colon>'a.
   1.515 -   (c\<Colon>'b\<Colon>ordered_idom) * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) X3 =
   1.516 -   (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) X3 \<or>
   1.517 -   \<not> c * g X3 \<le> f X3"
   1.518 -  by (metis Lattices.min_max.less_eq_less_inf.antisym_intro 0)
   1.519 -have 3: "\<And>X3\<Colon>'b\<Colon>ordered_idom.
   1.520 -   \<not> (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>X3\<bar>)
   1.521 -     \<le> \<bar>X3 * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X3\<bar>)\<bar>"
   1.522 -  by (metis 1 Ring_and_Field.abs_mult)
   1.523 -have 4: "\<And>X3\<Colon>'b\<Colon>ordered_idom. (1\<Colon>'b\<Colon>ordered_idom) * X3 = X3"
   1.524 -  by (metis Ring_and_Field.mult_cancel_left2 Finite_Set.AC_mult.f.commute)
   1.525 -have 5: "\<And>X3\<Colon>'b\<Colon>ordered_idom. X3 * (1\<Colon>'b\<Colon>ordered_idom) = X3"
   1.526 -  by (metis Ring_and_Field.mult_cancel_right2 Finite_Set.AC_mult.f.commute)
   1.527 -have 6: "\<And>X3\<Colon>'b\<Colon>ordered_idom. \<bar>X3\<bar> * \<bar>X3\<bar> = X3 * X3"
   1.528 -  by (metis Ring_and_Field.abs_mult_self Finite_Set.AC_mult.f.commute)
   1.529 -have 7: "\<And>X3\<Colon>'b\<Colon>ordered_idom. (0\<Colon>'b\<Colon>ordered_idom) \<le> X3 * X3"
   1.530 -  by (metis Ring_and_Field.zero_le_square Finite_Set.AC_mult.f.commute)
   1.531 -have 8: "(0\<Colon>'b\<Colon>ordered_idom) \<le> (1\<Colon>'b\<Colon>ordered_idom)"
   1.532 -  by (metis 7 Ring_and_Field.mult_cancel_left2)
   1.533 -have 9: "\<And>X3\<Colon>'b\<Colon>ordered_idom. X3 * X3 = \<bar>X3 * X3\<bar>"
   1.534 -  by (metis Ring_and_Field.abs_mult 6)
   1.535 -have 10: "\<bar>1\<Colon>'b\<Colon>ordered_idom\<bar> = (1\<Colon>'b\<Colon>ordered_idom)"
   1.536 -  by (metis 9 4)
   1.537 -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>"
   1.538 -  by (metis Ring_and_Field.abs_mult OrderedGroup.abs_idempotent 5)
   1.539 -have 12: "\<And>X3\<Colon>'b\<Colon>ordered_idom. \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar>"
   1.540 -  by (metis 11 10 5)
   1.541 -have 13: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom.
   1.542 -   X3 * (1\<Colon>'b\<Colon>ordered_idom) \<le> X1 \<or>
   1.543 -   \<not> \<bar>X3\<bar> \<le> X1 \<or> \<not> (0\<Colon>'b\<Colon>ordered_idom) \<le> (1\<Colon>'b\<Colon>ordered_idom)"
   1.544 -  by (metis OrderedGroup.abs_le_D1 Ring_and_Field.abs_mult_pos 5)
   1.545 -have 14: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom.
   1.546 -   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)"
   1.547 -  by (metis 13 5)
   1.548 -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"
   1.549 -  by (metis 14 8)
   1.550 -have 16: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. X3 \<le> X1 \<or> X1 \<le> \<bar>X3\<bar>"
   1.551 -  by (metis 15 Orderings.linorder_class.less_eq_less.linear)
   1.552 -have 17: "\<And>X3\<Colon>'b\<Colon>ordered_idom.
   1.553 -   X3 * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>X3\<bar>)
   1.554 -   \<le> (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X3\<bar>)"
   1.555 -  by (metis 3 16)
   1.556 -have 18: "(c\<Colon>'b\<Colon>ordered_idom) *
   1.557 -(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>c\<bar>) =
   1.558 -(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>c\<bar>)"
   1.559 -  by (metis 2 17)
   1.560 -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>"
   1.561 -  by (metis 15 Ring_and_Field.abs_le_mult Ring_and_Field.abs_mult)
   1.562 -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>"
   1.563 -  by (metis 19 12 12)
   1.564 -have 21: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. X3 * X1 \<le> \<bar>X3\<bar> * \<bar>X1\<bar>"
   1.565 -  by (metis 15 20)
   1.566 -have 22: "(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom)
   1.567 - ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>c\<Colon>'b\<Colon>ordered_idom\<bar>)
   1.568 -\<le> \<bar>c\<bar> * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>c\<bar>)\<bar>"
   1.569 -  by (metis 21 18)
   1.570 -show 23: "False"
   1.571 -  by (metis 22 1)
   1.572 +assume 0: "\<And>x. f x \<le> c * g x"
   1.573 +assume 1: "\<And>xa. \<not> f (x xa) \<le> xa * \<bar>g (x xa)\<bar>"
   1.574 +have 2: "\<And>X3. c * g X3 = f X3 \<or> \<not> c * g X3 \<le> f X3"
   1.575 +  by (metis 0 order_antisym_conv)
   1.576 +have 3: "\<And>X3. \<not> f (x \<bar>X3\<bar>) \<le> \<bar>X3 * g (x \<bar>X3\<bar>)\<bar>"
   1.577 +  by (metis 1 abs_mult)
   1.578 +have 4: "\<And>X1 X3\<Colon>'b\<Colon>ordered_idom. X3 \<le> X1 \<or> X1 \<le> \<bar>X3\<bar>"
   1.579 +  by (metis linorder_linear abs_le_D1)
   1.580 +have 5: "\<And>X3::'b. \<bar>X3\<bar> * \<bar>X3\<bar> = X3 * X3"
   1.581 +  by (metis abs_mult_self AC_mult.f.commute)
   1.582 +have 6: "\<And>X3. \<not> X3 * X3 < (0\<Colon>'b\<Colon>ordered_idom)"
   1.583 +  by (metis not_square_less_zero AC_mult.f.commute)
   1.584 +have 7: "\<And>X1 X3::'b. \<bar>X1\<bar> * \<bar>X3\<bar> = \<bar>X3 * X1\<bar>"
   1.585 +  by (metis abs_mult AC_mult.f.commute)
   1.586 +have 8: "\<And>X3::'b. X3 * X3 = \<bar>X3 * X3\<bar>"
   1.587 +  by (metis abs_mult 5)
   1.588 +have 9: "\<And>X3. X3 * g (x \<bar>X3\<bar>) \<le> f (x \<bar>X3\<bar>)"
   1.589 +  by (metis 3 4)
   1.590 +have 10: "c * g (x \<bar>c\<bar>) = f (x \<bar>c\<bar>)"
   1.591 +  by (metis 2 9)
   1.592 +have 11: "\<And>X3::'b. \<bar>X3\<bar> * \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar> * \<bar>X3\<bar>"
   1.593 +  by (metis abs_idempotent abs_mult 8)
   1.594 +have 12: "\<And>X3::'b. \<bar>X3 * \<bar>X3\<bar>\<bar> = \<bar>X3\<bar> * \<bar>X3\<bar>"
   1.595 +  by (metis AC_mult.f.commute 7 11)
   1.596 +have 13: "\<And>X3::'b. \<bar>X3 * \<bar>X3\<bar>\<bar> = X3 * X3"
   1.597 +  by (metis 8 7 12)
   1.598 +have 14: "\<And>X3. X3 \<le> \<bar>X3\<bar> \<or> X3 < (0\<Colon>'b)"
   1.599 +  by (metis abs_ge_self abs_le_D1 abs_if)
   1.600 +have 15: "\<And>X3. X3 \<le> \<bar>X3\<bar> \<or> \<bar>X3\<bar> < (0\<Colon>'b)"
   1.601 +  by (metis abs_ge_self abs_le_D1 abs_if)
   1.602 +have 16: "\<And>X3. X3 * X3 < (0\<Colon>'b) \<or> X3 * \<bar>X3\<bar> \<le> X3 * X3"
   1.603 +  by (metis 15 13)
   1.604 +have 17: "\<And>X3::'b. X3 * \<bar>X3\<bar> \<le> X3 * X3"
   1.605 +  by (metis 16 6)
   1.606 +have 18: "\<And>X3. X3 \<le> \<bar>X3\<bar> \<or> \<not> X3 < (0\<Colon>'b)"
   1.607 +  by (metis mult_le_cancel_left 17)
   1.608 +have 19: "\<And>X3::'b. X3 \<le> \<bar>X3\<bar>"
   1.609 +  by (metis 18 14)
   1.610 +have 20: "\<not> f (x \<bar>c\<bar>) \<le> \<bar>f (x \<bar>c\<bar>)\<bar>"
   1.611 +  by (metis 3 10)
   1.612 +show "False"
   1.613 +  by (metis 20 19)
   1.614  qed
   1.615  
   1.616  
   1.617 @@ -781,16 +517,11 @@
   1.618    apply auto
   1.619  proof (neg_clausify)
   1.620  fix x
   1.621 -assume 0: "!!mes_o43::'b::ordered_idom.
   1.622 -   ~ abs ((f::'a::type => 'b::ordered_idom)
   1.623 -           ((x::'b::ordered_idom => 'a::type) mes_o43))
   1.624 -     <= mes_o43 * abs (f (x mes_o43))"
   1.625 -have 1: "!!X3::'b::ordered_idom.
   1.626 -   X3 <= (1::'b::ordered_idom) * X3 |
   1.627 -   ~ (1::'b::ordered_idom) <= (1::'b::ordered_idom)"
   1.628 -  by (metis mult_le_cancel_right1 order_refl)
   1.629 -have 2: "!!X3::'b::ordered_idom. X3 <= (1::'b::ordered_idom) * X3"
   1.630 -  by (metis 1 order_refl)
   1.631 +assume 0: "\<And>xa. \<not> \<bar>f (x xa)\<bar> \<le> xa * \<bar>f (x xa)\<bar>"
   1.632 +have 1: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2 \<or> \<not> (1\<Colon>'b) \<le> (1\<Colon>'b)"
   1.633 +  by (metis mult_le_cancel_right1 order_eq_iff)
   1.634 +have 2: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2"
   1.635 +  by (metis order_eq_iff 1)
   1.636  show "False"
   1.637    by (metis 0 2)
   1.638  qed
   1.639 @@ -801,15 +532,11 @@
   1.640    apply auto
   1.641  proof (neg_clausify)
   1.642  fix x
   1.643 -assume 0: "\<And>mes_o4C\<Colon>'b\<Colon>ordered_idom.
   1.644 -   \<not> \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) mes_o4C)\<bar>
   1.645 -     \<le> mes_o4C * \<bar>f (x mes_o4C)\<bar>"
   1.646 -have 1: "\<And>X3\<Colon>'b\<Colon>ordered_idom.
   1.647 -   X3 \<le> (1\<Colon>'b\<Colon>ordered_idom) * X3 \<or>
   1.648 -   \<not> (1\<Colon>'b\<Colon>ordered_idom) \<le> (1\<Colon>'b\<Colon>ordered_idom)"
   1.649 -  by (metis mult_le_cancel_right1 order_refl)
   1.650 -have 2: "\<And>X3\<Colon>'b\<Colon>ordered_idom. X3 \<le> (1\<Colon>'b\<Colon>ordered_idom) * X3"
   1.651 -  by (metis 1 order_refl)
   1.652 +assume 0: "\<And>xa. \<not> \<bar>f (x xa)\<bar> \<le> xa * \<bar>f (x xa)\<bar>"
   1.653 +have 1: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2 \<or> \<not> (1\<Colon>'b) \<le> (1\<Colon>'b)"
   1.654 +  by (metis mult_le_cancel_right1 order_eq_iff)
   1.655 +have 2: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2"
   1.656 +  by (metis order_eq_iff 1)
   1.657  show "False"
   1.658    by (metis 0 2)
   1.659  qed
   1.660 @@ -1144,17 +871,14 @@
   1.661  
   1.662  ML{*ResAtp.problem_name := "BigO__bigo_const_mult1"*}
   1.663  lemma bigo_const_mult1: "(%x. c * f x) : O(f)"
   1.664 -  apply (simp add: bigo_def abs_mult) 
   1.665 +  apply (simp add: bigo_def abs_mult)
   1.666  proof (neg_clausify)
   1.667  fix x
   1.668 -assume 0: "\<And>mes_vAL\<Colon>'b.
   1.669 -   \<not> \<bar>c\<Colon>'b\<bar> *
   1.670 -     \<bar>(f\<Colon>'a \<Rightarrow> 'b) ((x\<Colon>'b \<Rightarrow> 'a) mes_vAL)\<bar>
   1.671 -     \<le> mes_vAL * \<bar>f (x mes_vAL)\<bar>"
   1.672 -have 1: "\<And>Y\<Colon>'b. Y \<le> Y"
   1.673 -  by (metis order_refl)
   1.674 -show 2: "False"
   1.675 -  by (metis 0 1)
   1.676 +assume 0: "\<And>xa. \<not> \<bar>c\<bar> * \<bar>f (x xa)\<bar> \<le> xa * \<bar>f (x xa)\<bar>"
   1.677 +have 1: "\<And>X2. \<not> \<bar>c * f (x X2)\<bar> \<le> X2 * \<bar>f (x X2)\<bar>"
   1.678 +  by (metis 0 abs_mult)
   1.679 +show "False"
   1.680 +  by (metis 1 abs_le_mult)
   1.681  qed
   1.682  
   1.683  lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"
   1.684 @@ -1435,16 +1159,8 @@
   1.685  lemma bigo_lesso1: "ALL x. f x <= g x ==> f <o g =o O(h)"
   1.686    apply (unfold lesso_def)
   1.687    apply (subgoal_tac "(%x. max (f x - g x) 0) = 0")
   1.688 -(*
   1.689 -?? abstractions don't work: abstraction function gets the wrong type?
   1.690 -proof (neg_clausify)
   1.691 -assume 0: "llabs_subgoal_1 f g = 0"
   1.692 -assume 1: "llabs_subgoal_1 f g \<notin> O(h)"
   1.693 -show "False"
   1.694 -  by (metis 1 0 bigo_zero)
   1.695 -*)
   1.696 -  apply (erule ssubst)
   1.697 -  apply (rule bigo_zero)
   1.698 +(*??Translation of TSTP raised an exception: Type unification failed: Variable ?'X2.0::type not of sort ord*)
   1.699 +apply (metis bigo_zero ord_class.max)
   1.700    apply (unfold func_zero)
   1.701    apply (rule ext)
   1.702    apply (simp split: split_max)
     2.1 --- a/src/HOL/MetisExamples/set.thy	Tue Oct 09 17:11:20 2007 +0200
     2.2 +++ b/src/HOL/MetisExamples/set.thy	Tue Oct 09 18:14:00 2007 +0200
     2.3 @@ -33,7 +33,7 @@
     2.4  assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
     2.5  assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
     2.6  assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
     2.7 -assume 5: "\<And>A. ((\<not> Y \<subseteq> A \<or> \<not> Z \<subseteq> A) \<or> X \<subseteq> A) \<or> X = Y \<union> Z"
     2.8 +assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
     2.9  have 6: "sup Y Z = X \<or> Y \<subseteq> X"
    2.10    by (metis 0 sup_set_eq)
    2.11  have 7: "sup Y Z = X \<or> Z \<subseteq> X"
    2.12 @@ -103,7 +103,7 @@
    2.13  assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
    2.14  assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
    2.15  assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
    2.16 -assume 5: "\<And>A. ((\<not> Y \<subseteq> A \<or> \<not> Z \<subseteq> A) \<or> X \<subseteq> A) \<or> X = Y \<union> Z"
    2.17 +assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
    2.18  have 6: "sup Y Z = X \<or> Y \<subseteq> X"
    2.19    by (metis 0 sup_set_eq)
    2.20  have 7: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
    2.21 @@ -146,7 +146,7 @@
    2.22  assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
    2.23  assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
    2.24  assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
    2.25 -assume 5: "\<And>A. ((\<not> Y \<subseteq> A \<or> \<not> Z \<subseteq> A) \<or> X \<subseteq> A) \<or> X = Y \<union> Z"
    2.26 +assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
    2.27  have 6: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
    2.28    by (metis 3 sup_set_eq)
    2.29  have 7: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
    2.30 @@ -181,7 +181,7 @@
    2.31  assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
    2.32  assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
    2.33  assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
    2.34 -assume 5: "\<And>A. ((\<not> Y \<subseteq> A \<or> \<not> Z \<subseteq> A) \<or> X \<subseteq> A) \<or> X = Y \<union> Z"
    2.35 +assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
    2.36  have 6: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
    2.37    by (metis 4 sup_set_eq)
    2.38  have 7: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
    2.39 @@ -221,9 +221,9 @@
    2.40  proof (neg_clausify)
    2.41  fix x xa
    2.42  assume 0: "f (g x) = x"
    2.43 -assume 1: "\<And>A. A = x \<or> f (g A) \<noteq> A"
    2.44 -assume 2: "\<And>A. g (f (xa A)) = xa A \<or> g (f A) \<noteq> A"
    2.45 -assume 3: "\<And>A. g (f A) \<noteq> A \<or> xa A \<noteq> A"
    2.46 +assume 1: "\<And>y. y = x \<or> f (g y) \<noteq> y"
    2.47 +assume 2: "\<And>x. g (f (xa x)) = xa x \<or> g (f x) \<noteq> x"
    2.48 +assume 3: "\<And>x. g (f x) \<noteq> x \<or> xa x \<noteq> x"
    2.49  have 4: "\<And>X1. g (f X1) \<noteq> X1 \<or> g x \<noteq> X1"
    2.50    by (metis 3 1 2)
    2.51  show "False"
    2.52 @@ -243,8 +243,8 @@
    2.53  lemma singleton_example_2:
    2.54       "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
    2.55  proof (neg_clausify)
    2.56 -assume 0: "\<And>A. \<not> S \<subseteq> {A}"
    2.57 -assume 1: "\<And>A. A \<notin> S \<or> \<Union>S \<subseteq> A"
    2.58 +assume 0: "\<And>x. \<not> S \<subseteq> {x}"
    2.59 +assume 1: "\<And>x. x \<notin> S \<or> \<Union>S \<subseteq> x"
    2.60  have 2: "\<And>X3. X3 = \<Union>S \<or> \<not> X3 \<subseteq> \<Union>S \<or> X3 \<notin> S"
    2.61    by (metis set_eq_subset 1)
    2.62  have 3: "\<And>X3. S \<subseteq> insert (\<Union>S) X3"
     3.1 --- a/src/HOL/Tools/meson.ML	Tue Oct 09 17:11:20 2007 +0200
     3.2 +++ b/src/HOL/Tools/meson.ML	Tue Oct 09 18:14:00 2007 +0200
     3.3 @@ -6,9 +6,6 @@
     3.4  The MESON resolution proof procedure for HOL.
     3.5  
     3.6  When making clauses, avoids using the rewriter -- instead uses RS recursively
     3.7 -
     3.8 -NEED TO SORT LITERALS BY # OF VARS, USING ==>I/E.  ELIMINATES NEED FOR
     3.9 -FUNCTION nodups -- if done to goal clauses too!
    3.10  *)
    3.11  
    3.12  signature MESON =
    3.13 @@ -18,9 +15,8 @@
    3.14    val flexflex_first_order: thm -> thm
    3.15    val size_of_subgoals: thm -> int
    3.16    val too_many_clauses: term -> bool
    3.17 -  val make_cnf: thm list -> thm -> thm list
    3.18 +  val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
    3.19    val finish_cnf: thm list -> thm list
    3.20 -  val generalize: thm -> thm
    3.21    val make_nnf: thm -> thm
    3.22    val make_nnf1: thm -> thm
    3.23    val skolemize: thm -> thm
    3.24 @@ -102,10 +98,15 @@
    3.25          in  th'  end
    3.26          handle THM _ => th;
    3.27  
    3.28 -(*raises exception if no rules apply -- unlike RL*)
    3.29 +(*Forward proof while preserving bound variables names*)
    3.30 +fun rename_bvs_RS th rl =
    3.31 +  let val th' = th RS rl
    3.32 +  in  Thm.rename_boundvars (concl_of th') (concl_of th) th' end;
    3.33 +
    3.34 +(*raises exception if no rules apply*)
    3.35  fun tryres (th, rls) =
    3.36    let fun tryall [] = raise THM("tryres", 0, th::rls)
    3.37 -        | tryall (rl::rls) = (th RS rl handle THM _ => tryall rls)
    3.38 +        | tryall (rl::rls) = (rename_bvs_RS th rl handle THM _ => tryall rls)
    3.39    in  tryall rls  end;
    3.40  
    3.41  (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
    3.42 @@ -208,6 +209,32 @@
    3.43    handle TERM _ => th;  (*probably dest_Trueprop on a weird theorem*)
    3.44  
    3.45  
    3.46 +(*** Removal of duplicate literals ***)
    3.47 +
    3.48 +(*Forward proof, passing extra assumptions as theorems to the tactic*)
    3.49 +fun forward_res2 nf hyps st =
    3.50 +  case Seq.pull
    3.51 +        (REPEAT
    3.52 +         (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
    3.53 +         st)
    3.54 +  of SOME(th,_) => th
    3.55 +   | NONE => raise THM("forward_res2", 0, [st]);
    3.56 +
    3.57 +(*Remove duplicates in P|Q by assuming ~P in Q
    3.58 +  rls (initially []) accumulates assumptions of the form P==>False*)
    3.59 +fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
    3.60 +    handle THM _ => tryres(th,rls)
    3.61 +    handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),
    3.62 +                           [disj_FalseD1, disj_FalseD2, asm_rl])
    3.63 +    handle THM _ => th;
    3.64 +
    3.65 +(*Remove duplicate literals, if there are any*)
    3.66 +fun nodups th =
    3.67 +  if has_duplicates (op =) (literals (prop_of th))
    3.68 +    then nodups_aux [] th
    3.69 +    else th;
    3.70 +
    3.71 +
    3.72  (*** The basic CNF transformation ***)
    3.73  
    3.74  val max_clauses = 40;
    3.75 @@ -243,11 +270,19 @@
    3.76  fun too_many_clauses t = nclauses t >= max_clauses;
    3.77  
    3.78  (*Replaces universally quantified variables by FREE variables -- because
    3.79 -  assumptions may not contain scheme variables.  Later, we call "generalize". *)
    3.80 -fun freeze_spec th =
    3.81 -  let val newname = gensym "mes_"
    3.82 -      val spec' = read_instantiate [("x", newname)] spec
    3.83 -  in  th RS spec'  end;
    3.84 +  assumptions may not contain scheme variables.  Later, generalize using Variable.export. *)
    3.85 +local  
    3.86 +  val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))));
    3.87 +  val spec_varT = #T (Thm.rep_cterm spec_var);
    3.88 +  fun name_of (Const ("All", _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
    3.89 +in  
    3.90 +  fun freeze_spec th ctxt =
    3.91 +    let
    3.92 +      val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
    3.93 +      val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (concl_of th))] ctxt;
    3.94 +      val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec;
    3.95 +    in (th RS spec', ctxt') end
    3.96 +end;
    3.97  
    3.98  (*Used with METAHYPS below. There is one assumption, which gets bound to prem
    3.99    and then normalized via function nf. The normal form is given to resolve_tac,
   3.100 @@ -268,16 +303,18 @@
   3.101  (*Conjunctive normal form, adding clauses from th in front of ths (for foldr).
   3.102    Strips universal quantifiers and breaks up conjunctions.
   3.103    Eliminates existential quantifiers using skoths: Skolemization theorems.*)
   3.104 -fun cnf skoths (th,ths) =
   3.105 -  let fun cnf_aux (th,ths) =
   3.106 +fun cnf skoths ctxt (th,ths) =
   3.107 +  let val ctxtr = ref ctxt
   3.108 +      fun cnf_aux (th,ths) =
   3.109          if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
   3.110          else if not (has_conns ["All","Ex","op &"] (prop_of th))
   3.111 -        then th::ths (*no work to do, terminate*)
   3.112 +        then nodups th :: ths (*no work to do, terminate*)
   3.113          else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
   3.114              Const ("op &", _) => (*conjunction*)
   3.115                  cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
   3.116            | Const ("All", _) => (*universal quantifier*)
   3.117 -                cnf_aux (freeze_spec th, ths)
   3.118 +                let val (th',ctxt') = freeze_spec th (!ctxtr)
   3.119 +                in  ctxtr := ctxt'; cnf_aux (th', ths) end
   3.120            | Const ("Ex", _) =>
   3.121                (*existential quantifier: Insert Skolem functions*)
   3.122                cnf_aux (apply_skolem_ths (th,skoths), ths)
   3.123 @@ -288,62 +325,18 @@
   3.124                    (METAHYPS (resop cnf_nil) 1) THEN
   3.125                     (fn st' => st' |> METAHYPS (resop cnf_nil) 1)
   3.126                in  Seq.list_of (tac (th RS disj_forward)) @ ths  end
   3.127 -          | _ => (*no work to do*) th::ths
   3.128 +          | _ => nodups th :: ths  (*no work to do*)
   3.129        and cnf_nil th = cnf_aux (th,[])
   3.130 -  in
   3.131 -    if too_many_clauses (concl_of th)
   3.132 -    then (Output.debug (fn () => ("cnf is ignoring: " ^ string_of_thm th)); ths)
   3.133 -    else cnf_aux (th,ths)
   3.134 -  end;
   3.135 -
   3.136 -fun all_names (Const ("all", _) $ Abs(x,_,P)) = x :: all_names P
   3.137 -  | all_names _ = [];
   3.138 +      val cls = 
   3.139 +	    if too_many_clauses (concl_of th)
   3.140 +	    then (Output.debug (fn () => ("cnf is ignoring: " ^ string_of_thm th)); ths)
   3.141 +	    else cnf_aux (th,ths)
   3.142 +  in  (cls, !ctxtr)  end;
   3.143  
   3.144 -fun new_names n [] = []
   3.145 -  | new_names n (x::xs) =
   3.146 -      if String.isPrefix "mes_" x then (x, radixstring(26,"A",n)) :: new_names (n+1) xs
   3.147 -      else new_names n xs;
   3.148 -
   3.149 -(*The gensym names are ugly, so don't let the user see them. When forall_elim_vars
   3.150 -  is called, it will ensure that no name clauses ensue.*)
   3.151 -fun nice_names th =
   3.152 -  let val old_names = all_names (prop_of th)
   3.153 -  in  Drule.rename_bvars (new_names 0 old_names) th  end;
   3.154 -
   3.155 -(*Convert all suitable free variables to schematic variables,
   3.156 -  but don't discharge assumptions.*)
   3.157 -fun generalize th = Thm.varifyT (forall_elim_vars 0 (nice_names (forall_intr_frees th)));
   3.158 -
   3.159 -fun make_cnf skoths th = cnf skoths (th, []);
   3.160 +fun make_cnf skoths th ctxt = cnf skoths ctxt (th, []);
   3.161  
   3.162  (*Generalization, removal of redundant equalities, removal of tautologies.*)
   3.163 -fun finish_cnf ths = filter (not o is_taut) (map (refl_clause o generalize) ths);
   3.164 -
   3.165 -
   3.166 -(**** Removal of duplicate literals ****)
   3.167 -
   3.168 -(*Forward proof, passing extra assumptions as theorems to the tactic*)
   3.169 -fun forward_res2 nf hyps st =
   3.170 -  case Seq.pull
   3.171 -        (REPEAT
   3.172 -         (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
   3.173 -         st)
   3.174 -  of SOME(th,_) => th
   3.175 -   | NONE => raise THM("forward_res2", 0, [st]);
   3.176 -
   3.177 -(*Remove duplicates in P|Q by assuming ~P in Q
   3.178 -  rls (initially []) accumulates assumptions of the form P==>False*)
   3.179 -fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
   3.180 -    handle THM _ => tryres(th,rls)
   3.181 -    handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),
   3.182 -                           [disj_FalseD1, disj_FalseD2, asm_rl])
   3.183 -    handle THM _ => th;
   3.184 -
   3.185 -(*Remove duplicate literals, if there are any*)
   3.186 -fun nodups th =
   3.187 -  if has_duplicates (op =) (literals (prop_of th))
   3.188 -    then nodups_aux [] th
   3.189 -    else th;
   3.190 +fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);
   3.191  
   3.192  
   3.193  (**** Generation of contrapositives ****)
   3.194 @@ -530,13 +523,16 @@
   3.195      handle THM _ =>
   3.196          skolemize (forward_res skolemize
   3.197                     (tryres (th, [conj_forward, disj_forward, all_forward])))
   3.198 -    handle THM _ => forward_res skolemize (th RS ex_forward);
   3.199 +    handle THM _ => forward_res skolemize (rename_bvs_RS th ex_forward);
   3.200  
   3.201 +fun add_clauses (th,cls) =
   3.202 +  let val ctxt0 = Variable.thm_context th
   3.203 +      val (cnfs,ctxt) = make_cnf [] th ctxt0
   3.204 +  in Variable.export ctxt ctxt0 cnfs @ cls end;
   3.205  
   3.206  (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   3.207    The resulting clauses are HOL disjunctions.*)
   3.208 -fun make_clauses ths =
   3.209 -    (sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths)));
   3.210 +fun make_clauses ths = sort_clauses (foldr add_clauses [] ths);
   3.211  
   3.212  (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
   3.213  fun make_horns ths =
     4.1 --- a/src/HOL/Tools/metis_tools.ML	Tue Oct 09 17:11:20 2007 +0200
     4.2 +++ b/src/HOL/Tools/metis_tools.ML	Tue Oct 09 18:14:00 2007 +0200
     4.3 @@ -97,18 +97,32 @@
     4.4          let val (lits, types_sorts) = ResHolClause.literals_of_term thy t
     4.5          in  (map (hol_literal_to_fol isFO) lits, types_sorts) end;
     4.6  
     4.7 -  fun metis_of_typeLit (ResClause.LTVar (s,x))  = metis_lit false s [Metis.Term.Var x]
     4.8 -    | metis_of_typeLit (ResClause.LTFree (s,x)) = metis_lit true  s [Metis.Term.Fn(x,[])];
     4.9 +  (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
    4.10 +  fun metis_of_typeLit pos (ResClause.LTVar (s,x))  = metis_lit pos s [Metis.Term.Var x]
    4.11 +    | metis_of_typeLit pos (ResClause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
    4.12  
    4.13 -  fun metis_of_tfree tf = Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit tf));
    4.14 +  fun default_sort ctxt (ResClause.FOLTVar _, _) = false
    4.15 +    | default_sort ctxt (ResClause.FOLTFree x, ss) = (ss = Option.getOpt (Variable.def_sort ctxt (x,~1), []));
    4.16  
    4.17 -  fun hol_thm_to_fol ctxt isFO th =
    4.18 +  fun metis_of_tfree tf = 
    4.19 +    Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf));
    4.20 +
    4.21 +  fun hol_thm_to_fol is_conjecture ctxt isFO th =
    4.22      let val thy = ProofContext.theory_of ctxt
    4.23          val (mlits, types_sorts) =
    4.24                 (literals_of_hol_thm thy isFO o HOLogic.dest_Trueprop o prop_of) th
    4.25 -        val (tvar_lits,tfree_lits) = ResClause.add_typs_aux types_sorts
    4.26 -        val tlits = if Config.get ctxt type_lits then map metis_of_typeLit tvar_lits else []
    4.27 -    in  (Metis.Thm.axiom (Metis.LiteralSet.fromList(tlits@mlits)), tfree_lits)  end;
    4.28 +    in  
    4.29 +        if is_conjecture then
    4.30 +            (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), ResClause.add_typs types_sorts) 
    4.31 +        else
    4.32 +          let val tylits = ResClause.add_typs 
    4.33 +                             (filter (not o default_sort ctxt) types_sorts)
    4.34 +              val mtylits = if Config.get ctxt type_lits 
    4.35 +                            then map (metis_of_typeLit false) tylits else []
    4.36 +          in
    4.37 +            (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [])
    4.38 +          end
    4.39 +    end;
    4.40  
    4.41    (* ARITY CLAUSE *)
    4.42  
    4.43 @@ -118,8 +132,9 @@
    4.44          metis_lit false (ResClause.make_type_class c) [Metis.Term.Var str];
    4.45  
    4.46    (*TrueI is returned as the Isabelle counterpart because there isn't any.*)
    4.47 -  fun arity_cls (ResClause.ArityClause{kind,conclLit,premLits,...}) =
    4.48 -    (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
    4.49 +  fun arity_cls (ResClause.ArityClause{conclLit,premLits,...}) =
    4.50 +    (TrueI, 
    4.51 +     Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
    4.52  
    4.53    (* CLASSREL CLAUSE *)
    4.54  
    4.55 @@ -460,9 +475,6 @@
    4.56    val comb_C = cnf_th ResHolClause.comb_C;
    4.57    val comb_S = cnf_th ResHolClause.comb_S;
    4.58  
    4.59 -  fun dest_Arity (ResClause.ArityClause{premLits,...}) =
    4.60 -        map ResClause.class_of_arityLit premLits;
    4.61 -
    4.62    fun type_ext thy tms =
    4.63      let val subs = ResAtp.tfree_classes_of_terms tms
    4.64          val supers = ResAtp.tvar_classes_of_terms tms
    4.65 @@ -489,16 +501,17 @@
    4.66          | in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
    4.67      in  c=pred orelse exists in_mterm tm_list  end;
    4.68  
    4.69 +  (*Extract TFree constraints from context to include as conjecture clauses*)
    4.70 +  fun init_tfrees ctxt =
    4.71 +    let fun add ((a,i),s) ys = if i = ~1 then (ResClause.FOLTFree a,s) :: ys else ys
    4.72 +    in  ResClause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
    4.73 +
    4.74    (*transform isabelle clause to metis clause *)
    4.75 -  fun add_thm ctxt (ith, {isFO, axioms, tfrees}) : logic_map =
    4.76 -    let val (mth, tfree_lits) = hol_thm_to_fol ctxt isFO ith
    4.77 -        fun add_tfree (tf, axs) =
    4.78 -              if member (op=) tfrees tf then axs
    4.79 -              else (metis_of_tfree tf, TrueI) :: axs
    4.80 -        val new_axioms = foldl add_tfree [] tfree_lits
    4.81 +  fun add_thm is_conjecture ctxt (ith, {isFO, axioms, tfrees}) : logic_map =
    4.82 +    let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt isFO ith
    4.83      in
    4.84         {isFO = isFO,
    4.85 -        axioms = (mth, Meson.make_meta_clause ith) :: (new_axioms @ axioms),
    4.86 +        axioms = (mth, Meson.make_meta_clause ith) :: axioms,
    4.87          tfrees = tfree_lits union tfrees}
    4.88      end;
    4.89  
    4.90 @@ -509,11 +522,19 @@
    4.91                            axioms = (mth, ith) :: axioms,
    4.92                            tfrees = tfrees}
    4.93  
    4.94 +  (*Insert non-logical axioms corresponding to all accumulated TFrees*)
    4.95 +  fun add_tfrees {isFO, axioms, tfrees} : logic_map =
    4.96 +       {isFO = isFO,
    4.97 +        axioms = (map (fn tf => (metis_of_tfree tf, TrueI)) (distinct op= tfrees)) @ axioms,
    4.98 +        tfrees = tfrees};
    4.99 +        
   4.100    (* Function to generate metis clauses, including comb and type clauses *)
   4.101    fun build_map mode thy ctxt cls ths =
   4.102      let val isFO = (mode = ResAtp.Fol) orelse
   4.103                      (mode <> ResAtp.Hol andalso ResAtp.is_fol_thms (cls @ ths))
   4.104 -        val lmap = foldl (add_thm ctxt) {isFO = isFO, axioms = [], tfrees = []} (cls @ ths)
   4.105 +        val lmap0 = foldl (add_thm true ctxt) 
   4.106 +                          {isFO = isFO, axioms = [], tfrees = init_tfrees ctxt} cls
   4.107 +        val lmap = foldl (add_thm false ctxt) (add_tfrees lmap0) ths
   4.108          val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
   4.109          fun used c = exists (Metis.LiteralSet.exists (const_in_metis c)) clause_lists
   4.110          (*Now check for the existence of certain combinators*)
   4.111 @@ -524,7 +545,7 @@
   4.112          val thS   = if used "c_COMBS" then [comb_S] else []
   4.113          val thEQ  = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else []
   4.114          val lmap' = if isFO then lmap 
   4.115 -                    else foldl (add_thm ctxt) lmap (thEQ @ thS @ thC @ thB @ thK @ thI)
   4.116 +                    else foldl (add_thm false ctxt) lmap (thEQ @ thS @ thC @ thB @ thK @ thI)
   4.117      in
   4.118          add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap'
   4.119      end;
   4.120 @@ -550,7 +571,7 @@
   4.121          val {isFO,axioms,tfrees} = build_map mode thy ctxt cls ths
   4.122          val _ = if null tfrees then ()
   4.123                  else (Output.debug (fn () => "TFREE CLAUSES");
   4.124 -                      app (fn tf => Output.debug (fn _ => ResClause.tptp_of_typeLit tf)) tfrees)
   4.125 +                      app (fn tf => Output.debug (fn _ => ResClause.tptp_of_typeLit true tf)) tfrees)
   4.126          val _ = Output.debug (fn () => "CLAUSES GIVEN TO METIS")
   4.127          val thms = map #1 axioms
   4.128          val _ = app (fn th => Output.debug (fn () => Metis.Thm.toString th)) thms
     5.1 --- a/src/HOL/Tools/res_axioms.ML	Tue Oct 09 17:11:20 2007 +0200
     5.2 +++ b/src/HOL/Tools/res_axioms.ML	Tue Oct 09 18:14:00 2007 +0200
     5.3 @@ -8,7 +8,6 @@
     5.4  signature RES_AXIOMS =
     5.5  sig
     5.6    val cnf_axiom: thm -> thm list
     5.7 -  val meta_cnf_axiom: thm -> thm list
     5.8    val pairname: thm -> string * thm
     5.9    val multi_base_blacklist: string list 
    5.10    val skolem_thm: thm -> thm list
    5.11 @@ -294,13 +293,14 @@
    5.12      transfer (Theory.deref atp_linkup_thy_ref) th handle THM _ => th;
    5.13  
    5.14  (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
    5.15 -fun to_nnf th =
    5.16 -    th |> transfer_to_ATP_Linkup
    5.17 -       |> transform_elim |> zero_var_indexes |> freeze_thm
    5.18 -       |> Conv.fconv_rule ObjectLogic.atomize |> Meson.make_nnf |> strip_lambdas ~1;
    5.19 +fun to_nnf th ctxt0 =
    5.20 +  let val th1 = th |> transfer_to_ATP_Linkup |> transform_elim |> zero_var_indexes
    5.21 +      val ((_,[th2]),ctxt) = Variable.import_thms false [th1] ctxt0
    5.22 +      val th3 = th2 |> Conv.fconv_rule ObjectLogic.atomize |> Meson.make_nnf |> strip_lambdas ~1
    5.23 +  in  (th3, ctxt)  end;
    5.24  
    5.25  (*Generate Skolem functions for a theorem supplied in nnf*)
    5.26 -fun skolem_of_nnf s th =
    5.27 +fun assume_skolem_of_def s th =
    5.28    map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
    5.29  
    5.30  fun assert_lambda_free ths msg =
    5.31 @@ -321,27 +321,32 @@
    5.32  
    5.33  (*Skolemize a named theorem, with Skolem functions as additional premises.*)
    5.34  fun skolem_thm th =
    5.35 -  let val nnfth = to_nnf th and s = fake_name th
    5.36 -  in  Meson.make_cnf (skolem_of_nnf s nnfth) nnfth |>  map combinators |> Meson.finish_cnf
    5.37 -  end
    5.38 +  let val ctxt0 = Variable.thm_context th
    5.39 +      val (nnfth,ctxt1) = to_nnf th ctxt0 and s = fake_name th
    5.40 +      val (cnfs,ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1
    5.41 +  in  cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf  end
    5.42    handle THM _ => [];
    5.43  
    5.44  (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
    5.45    It returns a modified theory, unless skolemization fails.*)
    5.46  fun skolem thy th =
    5.47 +  let val ctxt0 = Variable.thm_context th
    5.48 +  in
    5.49       Option.map
    5.50 -        (fn nnfth =>
    5.51 +        (fn (nnfth,ctxt1) =>
    5.52            let val _ = Output.debug (fn () => "skolemizing " ^ name_or_string th ^ ": ")
    5.53                val _ = Output.debug (fn () => string_of_thm nnfth)
    5.54                val s = fake_name th
    5.55                val (thy',defs) = declare_skofuns s nnfth thy
    5.56 -              val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth
    5.57 +              val (cnfs,ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1
    5.58                val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded")
    5.59 -              val cnfs' = map combinators cnfs
    5.60 -          in (map Goal.close_result (Meson.finish_cnf cnfs'), thy') end
    5.61 +              val cnfs' = cnfs |> map combinators |> Variable.export ctxt2 ctxt0 
    5.62 +                               |> Meson.finish_cnf |> map Goal.close_result
    5.63 +          in (cnfs', thy') end
    5.64            handle Clausify_failure thy_e => ([],thy_e)
    5.65          )
    5.66 -      (try to_nnf th);
    5.67 +      (try (to_nnf th) ctxt0)
    5.68 +  end;
    5.69  
    5.70  (*The cache prevents repeated clausification of a theorem, and also repeated declaration of
    5.71    Skolem functions.*)
    5.72 @@ -529,12 +534,8 @@
    5.73  
    5.74  val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac];
    5.75  
    5.76 -(*finish_cnf removes tautologies and functional reflexivity axioms, but by calling Thm.varifyT
    5.77 -  it can introduce TVars, which are useless in conjecture clauses.*)
    5.78 -val no_tvars = null o term_tvars o prop_of;
    5.79 -
    5.80 -val neg_clausify =
    5.81 -  filter no_tvars o Meson.finish_cnf o map combinators o Meson.make_clauses;
    5.82 +fun neg_clausify sts =
    5.83 +  sts |> Meson.make_clauses |> map combinators |> Meson.finish_cnf;
    5.84  
    5.85  fun neg_conjecture_clauses st0 n =
    5.86    let val st = Seq.hd (neg_skolemize_tac n st0)
     6.1 --- a/src/HOL/Tools/res_clause.ML	Tue Oct 09 17:11:20 2007 +0200
     6.2 +++ b/src/HOL/Tools/res_clause.ML	Tue Oct 09 18:14:00 2007 +0200
     6.3 @@ -32,7 +32,6 @@
     6.4    val make_fixed_type_const : string -> string
     6.5    val make_type_class : string -> string
     6.6    datatype kind = Axiom | Conjecture
     6.7 -  val name_of_kind : kind -> string
     6.8    type axiom_name = string
     6.9    datatype typ_var = FOLTVar of indexname | FOLTFree of string
    6.10    datatype fol_type =
    6.11 @@ -44,20 +43,15 @@
    6.12    val mk_typ_var_sort: typ -> typ_var * sort
    6.13    exception CLAUSE of string * term
    6.14    val isMeta : string -> bool
    6.15 -  val add_typs_aux : (typ_var * string list) list -> type_literal list * type_literal list
    6.16 +  val add_typs : (typ_var * string list) list -> type_literal list
    6.17    val get_tvar_strs: (typ_var * sort) list -> string list
    6.18    datatype arLit =
    6.19        TConsLit of class * string * string list
    6.20      | TVarLit of class * string
    6.21    datatype arityClause = ArityClause of
    6.22 -   {axiom_name: axiom_name,
    6.23 -    kind: kind,
    6.24 -    conclLit: arLit,
    6.25 -    premLits: arLit list}
    6.26 +   {axiom_name: axiom_name, conclLit: arLit, premLits: arLit list}
    6.27    datatype classrelClause = ClassrelClause of
    6.28 -   {axiom_name: axiom_name,
    6.29 -    subclass: class,
    6.30 -    superclass: class}
    6.31 +   {axiom_name: axiom_name, subclass: class, superclass: class}
    6.32    val make_classrel_clauses: theory -> class list -> class list -> classrelClause list
    6.33    val make_arity_clauses: theory -> string list -> class list -> class list * arityClause list
    6.34    val add_type_sort_preds: (typ_var * string list) * int Symtab.table -> int Symtab.table
    6.35 @@ -69,8 +63,8 @@
    6.36    val init_functab: int Symtab.table
    6.37    val writeln_strs: TextIO.outstream -> string list -> unit
    6.38    val dfg_sign: bool -> string -> string
    6.39 -  val dfg_of_typeLit: type_literal -> string
    6.40 -  val gen_dfg_cls: int * string * string * string * string list -> string
    6.41 +  val dfg_of_typeLit: bool -> type_literal -> string
    6.42 +  val gen_dfg_cls: int * string * kind * string list * string list * string list -> string
    6.43    val string_of_preds: (string * Int.int) list -> string
    6.44    val string_of_funcs: (string * int) list -> string
    6.45    val string_of_symbols: string -> string -> string
    6.46 @@ -80,8 +74,8 @@
    6.47    val dfg_classrelClause: classrelClause -> string
    6.48    val dfg_arity_clause: arityClause -> string
    6.49    val tptp_sign: bool -> string -> string
    6.50 -  val tptp_of_typeLit : type_literal -> string
    6.51 -  val gen_tptp_cls : int * string * kind * string list -> string
    6.52 +  val tptp_of_typeLit : bool -> type_literal -> string
    6.53 +  val gen_tptp_cls : int * string * kind * string list * string list -> string
    6.54    val tptp_tfree_clause : string -> string
    6.55    val tptp_arity_clause : arityClause -> string
    6.56    val tptp_classrelClause : classrelClause -> string
    6.57 @@ -236,9 +230,6 @@
    6.58  
    6.59  datatype kind = Axiom | Conjecture;
    6.60  
    6.61 -fun name_of_kind Axiom = "axiom"
    6.62 -  | name_of_kind Conjecture = "negated_conjecture";
    6.63 -
    6.64  type axiom_name = string;
    6.65  
    6.66  (**** Isabelle FOL clauses ****)
    6.67 @@ -296,18 +287,8 @@
    6.68  fun pred_of_sort (LTVar (s,ty)) = (s,1)
    6.69    | pred_of_sort (LTFree (s,ty)) = (s,1)
    6.70  
    6.71 -(*Given a list of sorted type variables, return two separate lists.
    6.72 -  The first is for TVars, the second for TFrees.*)
    6.73 -fun add_typs_aux [] = ([],[])
    6.74 -  | add_typs_aux ((FOLTVar indx, s) :: tss) =
    6.75 -      let val vs = sorts_on_typs (FOLTVar indx, s)
    6.76 -          val (vss,fss) = add_typs_aux tss
    6.77 -      in  (vs union vss, fss)  end
    6.78 -  | add_typs_aux ((FOLTFree x, s) :: tss) =
    6.79 -      let val fs = sorts_on_typs (FOLTFree x, s)
    6.80 -          val (vss,fss) = add_typs_aux tss
    6.81 -      in  (vss, fs union fss)  end;
    6.82 -
    6.83 +(*Given a list of sorted type variables, return a list of type literals.*)
    6.84 +fun add_typs tss = foldl (op union) [] (map sorts_on_typs tss);
    6.85  
    6.86  (** make axiom and conjecture clauses. **)
    6.87  
    6.88 @@ -327,7 +308,6 @@
    6.89  
    6.90  datatype arityClause =
    6.91           ArityClause of {axiom_name: axiom_name,
    6.92 -                         kind: kind,
    6.93                           conclLit: arLit,
    6.94                           premLits: arLit list};
    6.95  
    6.96 @@ -344,7 +324,7 @@
    6.97     let val tvars = gen_TVars (length args)
    6.98         val tvars_srts = ListPair.zip (tvars,args)
    6.99     in
   6.100 -      ArityClause {axiom_name = axiom_name, kind = Axiom,
   6.101 +      ArityClause {axiom_name = axiom_name, 
   6.102                     conclLit = TConsLit (cls, make_fixed_type_const tcons, tvars),
   6.103                     premLits = map TVarLit (union_all(map pack_sort tvars_srts))}
   6.104     end;
   6.105 @@ -478,17 +458,21 @@
   6.106  fun dfg_sign true s = s
   6.107    | dfg_sign false s = "not(" ^ s ^ ")"
   6.108  
   6.109 -fun dfg_of_typeLit (LTVar (s,ty)) = "not(" ^ s ^ "(" ^ ty ^ "))"
   6.110 -  | dfg_of_typeLit (LTFree (s,ty)) = s ^ "(" ^ ty ^ ")";
   6.111 +fun dfg_of_typeLit pos (LTVar (s,ty))  = dfg_sign pos (s ^ "(" ^ ty ^ ")")
   6.112 +  | dfg_of_typeLit pos (LTFree (s,ty)) = dfg_sign pos (s ^ "(" ^ ty ^ ")");
   6.113  
   6.114  (*Enclose the clause body by quantifiers, if necessary*)
   6.115  fun dfg_forall [] body = body
   6.116    | dfg_forall vars body = "forall([" ^ commas vars ^ "],\n" ^ body ^ ")"
   6.117  
   6.118 -fun gen_dfg_cls (cls_id, ax_name, knd, lits, vars) =
   6.119 -    "clause( %(" ^ knd ^ ")\n" ^
   6.120 -    dfg_forall vars ("or(" ^ lits ^ ")") ^ ",\n" ^
   6.121 -    string_of_clausename (cls_id,ax_name) ^  ").\n\n";
   6.122 +fun gen_dfg_cls (cls_id, ax_name, Axiom, lits, tylits, vars) =
   6.123 +      "clause( %(axiom)\n" ^
   6.124 +      dfg_forall vars ("or(" ^ commas (tylits@lits) ^ ")") ^ ",\n" ^
   6.125 +      string_of_clausename (cls_id,ax_name) ^  ").\n\n"
   6.126 +  | gen_dfg_cls (cls_id, ax_name, Conjecture, lits, _, vars) =
   6.127 +      "clause( %(negated_conjecture)\n" ^
   6.128 +      dfg_forall vars ("or(" ^ commas lits ^ ")") ^ ",\n" ^
   6.129 +      string_of_clausename (cls_id,ax_name) ^  ").\n\n";
   6.130  
   6.131  fun string_of_arity (name, num) =  "(" ^ name ^ "," ^ Int.toString num ^ ")"
   6.132  
   6.133 @@ -523,11 +507,11 @@
   6.134  
   6.135  fun string_of_ar axiom_name = arclause_prefix ^ ascii_of axiom_name;
   6.136  
   6.137 -fun dfg_arity_clause (ArityClause{axiom_name,kind,conclLit,premLits,...}) =
   6.138 +fun dfg_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) =
   6.139    let val TConsLit (_,_,tvars) = conclLit
   6.140        val lits = map dfg_of_arLit (conclLit :: premLits)
   6.141    in
   6.142 -      "clause( %(" ^ name_of_kind kind ^ ")\n" ^
   6.143 +      "clause( %(axiom)\n" ^
   6.144        dfg_forall tvars ("or( " ^ commas lits ^ ")") ^ ",\n" ^
   6.145        string_of_ar axiom_name ^ ").\n\n"
   6.146    end;
   6.147 @@ -539,12 +523,15 @@
   6.148  fun tptp_sign true s = s
   6.149    | tptp_sign false s = "~ " ^ s
   6.150  
   6.151 -fun tptp_of_typeLit (LTVar (s,ty))  = tptp_sign false (s ^ "(" ^ ty ^ ")")
   6.152 -  | tptp_of_typeLit (LTFree (s,ty)) = tptp_sign true  (s ^ "(" ^ ty ^ ")");
   6.153 +fun tptp_of_typeLit pos (LTVar (s,ty))  = tptp_sign pos (s ^ "(" ^ ty ^ ")")
   6.154 +  | tptp_of_typeLit pos (LTFree (s,ty)) = tptp_sign pos  (s ^ "(" ^ ty ^ ")");
   6.155  
   6.156 -fun gen_tptp_cls (cls_id,ax_name,knd,lits) =
   6.157 -    "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^
   6.158 -    name_of_kind knd ^ "," ^ tptp_pack lits ^ ").\n";
   6.159 +fun gen_tptp_cls (cls_id,ax_name,Axiom,lits,tylits) =
   6.160 +      "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ ",axiom," ^ 
   6.161 +               tptp_pack (tylits@lits) ^ ").\n"
   6.162 +  | gen_tptp_cls (cls_id,ax_name,Conjecture,lits,_) =
   6.163 +      "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ ",negated_conjecture," ^ 
   6.164 +               tptp_pack lits ^ ").\n";
   6.165  
   6.166  fun tptp_tfree_clause tfree_lit =
   6.167      "cnf(" ^ "tfree_tcs," ^ "negated_conjecture" ^ "," ^ tptp_pack[tfree_lit] ^ ").\n";
   6.168 @@ -554,8 +541,8 @@
   6.169    | tptp_of_arLit (TVarLit (c,str)) =
   6.170        tptp_sign false (make_type_class c ^ "(" ^ str ^ ")")
   6.171  
   6.172 -fun tptp_arity_clause (ArityClause{axiom_name,kind,conclLit,premLits,...}) =
   6.173 -  "cnf(" ^ string_of_ar axiom_name ^ "," ^ name_of_kind kind ^ "," ^
   6.174 +fun tptp_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) =
   6.175 +  "cnf(" ^ string_of_ar axiom_name ^ ",axiom," ^
   6.176    tptp_pack (map tptp_of_arLit (conclLit :: premLits)) ^ ").\n";
   6.177  
   6.178  fun tptp_classrelLits sub sup =
     7.1 --- a/src/HOL/Tools/res_hol_clause.ML	Tue Oct 09 17:11:20 2007 +0200
     7.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Tue Oct 09 18:14:00 2007 +0200
     7.3 @@ -97,9 +97,7 @@
     7.4                      th: thm,
     7.5                      kind: RC.kind,
     7.6                      literals: literal list,
     7.7 -                    ctypes_sorts: (RC.typ_var * Term.sort) list,
     7.8 -                    ctvar_type_literals: RC.type_literal list,
     7.9 -                    ctfree_type_literals: RC.type_literal list};
    7.10 +                    ctypes_sorts: (RC.typ_var * Term.sort) list};
    7.11  
    7.12  
    7.13  (*********************************************************************)
    7.14 @@ -177,15 +175,12 @@
    7.15  (* making axiom and conjecture clauses *)
    7.16  fun make_clause thy (clause_id,axiom_name,kind,th) =
    7.17      let val (lits,ctypes_sorts) = literals_of_term thy (prop_of th)
    7.18 -        val (ctvar_lits,ctfree_lits) = RC.add_typs_aux ctypes_sorts
    7.19      in
    7.20          if forall isFalse lits
    7.21          then error "Problem too trivial for resolution (empty clause)"
    7.22          else
    7.23              Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind,
    7.24 -                    literals = lits, ctypes_sorts = ctypes_sorts,
    7.25 -                    ctvar_type_literals = ctvar_lits,
    7.26 -                    ctfree_type_literals = ctfree_lits}
    7.27 +                    literals = lits, ctypes_sorts = ctypes_sorts}
    7.28      end;
    7.29  
    7.30  
    7.31 @@ -302,34 +297,24 @@
    7.32  
    7.33  (*Given a clause, returns its literals paired with a list of literals concerning TFrees;
    7.34    the latter should only occur in conjecture clauses.*)
    7.35 -fun tptp_type_lits (Clause cls) =
    7.36 -    let val lits = map tptp_literal (#literals cls)
    7.37 -        val ctvar_lits_strs = map RC.tptp_of_typeLit (#ctvar_type_literals cls)
    7.38 -        val ctfree_lits = map RC.tptp_of_typeLit (#ctfree_type_literals cls)
    7.39 -    in
    7.40 -        (ctvar_lits_strs @ lits, ctfree_lits)
    7.41 -    end;
    7.42 +fun tptp_type_lits pos (Clause{literals, ctypes_sorts, ...}) =
    7.43 +      (map tptp_literal literals, 
    7.44 +       map (RC.tptp_of_typeLit pos) (RC.add_typs ctypes_sorts));
    7.45  
    7.46  fun clause2tptp (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
    7.47 -    let val (lits,ctfree_lits) = tptp_type_lits cls
    7.48 -        val cls_str = RC.gen_tptp_cls(clause_id,axiom_name,kind,lits)
    7.49 -    in
    7.50 -        (cls_str,ctfree_lits)
    7.51 -    end;
    7.52 +  let val (lits,tylits) = tptp_type_lits (kind = RC.Conjecture) cls
    7.53 +  in
    7.54 +      (RC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits)
    7.55 +  end;
    7.56  
    7.57  
    7.58  (*** dfg format ***)
    7.59  
    7.60  fun dfg_literal (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate pred);
    7.61  
    7.62 -fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) =
    7.63 -  let val lits = map dfg_literal literals
    7.64 -      val (tvar_lits,tfree_lits) = RC.add_typs_aux ctypes_sorts
    7.65 -      val tvar_lits_strs = map RC.dfg_of_typeLit tvar_lits
    7.66 -      val tfree_lits = map RC.dfg_of_typeLit tfree_lits
    7.67 -  in
    7.68 -      (tvar_lits_strs @ lits, tfree_lits)
    7.69 -  end;
    7.70 +fun dfg_type_lits pos (Clause{literals, ctypes_sorts, ...}) =
    7.71 +      (map dfg_literal literals, 
    7.72 +       map (RC.dfg_of_typeLit pos) (RC.add_typs ctypes_sorts));
    7.73  
    7.74  fun get_uvars (CombConst _) vars = vars
    7.75    | get_uvars (CombVar(v,_)) vars = (v::vars)
    7.76 @@ -340,13 +325,13 @@
    7.77  fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals);
    7.78  
    7.79  fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
    7.80 -    let val (lits,tfree_lits) = dfg_clause_aux cls
    7.81 -        val vars = dfg_vars cls
    7.82 -        val tvars = RC.get_tvar_strs ctypes_sorts
    7.83 -        val knd = RC.name_of_kind kind
    7.84 -        val lits_str = commas lits
    7.85 -        val cls_str = RC.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars)
    7.86 -    in (cls_str, tfree_lits) end;
    7.87 +  let val (lits,tylits) = dfg_type_lits (kind = RC.Conjecture) cls
    7.88 +      val vars = dfg_vars cls
    7.89 +      val tvars = RC.get_tvar_strs ctypes_sorts
    7.90 +  in
    7.91 +      (RC.gen_dfg_cls(clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
    7.92 +  end;
    7.93 +
    7.94  
    7.95  (** For DFG format: accumulate function and predicate declarations **)
    7.96  
    7.97 @@ -509,7 +494,6 @@
    7.98      end;
    7.99  
   7.100  
   7.101 -
   7.102  (* dfg format *)
   7.103  
   7.104  fun dfg_write_file thy isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
     8.1 --- a/src/HOL/Tools/res_reconstruct.ML	Tue Oct 09 17:11:20 2007 +0200
     8.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Tue Oct 09 18:14:00 2007 +0200
     8.3 @@ -404,7 +404,7 @@
     8.4    | add_nonnull_prfline ((lno, t, deps), lines) = (lno, t, deps) :: lines
     8.5  and delete_dep lno lines = foldr add_nonnull_prfline [] (map (replace_deps (lno, [])) lines);
     8.6  
     8.7 -fun bad_free (Free (a,_)) = String.isPrefix "llabs_" a orelse String.isPrefix "sko_" a
     8.8 +fun bad_free (Free (a,_)) = String.isPrefix "sko_" a
     8.9    | bad_free _ = false;
    8.10  
    8.11  (*TVars are forbidden in goals. Also, we don't want lines with <2 dependencies.
    8.12 @@ -414,11 +414,11 @@
    8.13    phase may delete some dependencies, hence this phase comes later.*)
    8.14  fun add_wanted_prfline ((lno, t, []), (nlines, lines)) =
    8.15        (nlines, (lno, t, []) :: lines)   (*conjecture clauses must be kept*)
    8.16 -  | add_wanted_prfline (line, (nlines, [])) = (nlines, [line])   (*final line must be kept*)
    8.17    | add_wanted_prfline ((lno, t, deps), (nlines, lines)) =
    8.18        if eq_types t orelse not (null (term_tvars t)) orelse
    8.19 -         length deps < 2 orelse nlines mod !modulus <> 0 orelse
    8.20 -         exists bad_free (term_frees t)
    8.21 +         exists bad_free (term_frees t) orelse
    8.22 +         (not (null lines) andalso   (*final line can't be deleted for these reasons*)
    8.23 +          (length deps < 2 orelse nlines mod !modulus <> 0))   
    8.24        then (nlines+1, map (replace_deps (lno, deps)) lines) (*Delete line*)
    8.25        else (nlines+1, (lno, t, deps) :: lines);
    8.26