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