author paulson Tue Oct 09 18:14:00 2007 +0200 (2007-10-09) changeset 24937 340523598914 parent 24936 68a36883f0ad child 24938 a220317465b4
context-based treatment of generalization; also handling TFrees in axiom clauses
 src/HOL/MetisExamples/BigO.thy file | annotate | diff | revisions src/HOL/MetisExamples/set.thy file | annotate | diff | revisions src/HOL/Tools/meson.ML file | annotate | diff | revisions src/HOL/Tools/metis_tools.ML file | annotate | diff | revisions src/HOL/Tools/res_axioms.ML file | annotate | diff | revisions src/HOL/Tools/res_clause.ML file | annotate | diff | revisions src/HOL/Tools/res_hol_clause.ML file | annotate | diff | revisions src/HOL/Tools/res_reconstruct.ML file | annotate | diff | revisions
```     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.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.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.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.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
```