# HG changeset patch
# User blanchet
# Date 1272541311 -7200
# Node ID f91c7198281110151244aa1c581ae10dd5bf4ad3
# Parent  45c1870f234fba7857397b31b0ed8c291de8f5eb
redo more Metis/Sledgehammer example

diff -r 45c1870f234f -r f91c71982811 src/HOL/Metis_Examples/BigO.thy
--- a/src/HOL/Metis_Examples/BigO.thy	Thu Apr 29 12:21:20 2010 +0200
+++ b/src/HOL/Metis_Examples/BigO.thy	Thu Apr 29 13:41:51 2010 +0200
@@ -23,7 +23,7 @@
   apply (case_tac "c = 0", simp)
   apply (rule_tac x = "1" in exI, simp)
   apply (rule_tac x = "abs c" in exI, auto)
-  apply (metis abs_ge_minus_self abs_ge_zero abs_minus_cancel abs_of_nonneg equation_minus_iff Orderings.xt1(6) abs_mult)
+  apply (metis abs_ge_zero abs_of_nonneg Orderings.xt1(6) abs_mult)
   done
 
 (*** Now various verions with an increasing shrink factor ***)
@@ -37,64 +37,25 @@
   apply (case_tac "c = 0", simp)
   apply (rule_tac x = "1" in exI, simp)
   apply (rule_tac x = "abs c" in exI, auto)
-proof (neg_clausify)
-fix c x
-have 0: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom. \<bar>X1 * X2\<bar> = \<bar>X2 * X1\<bar>"
-  by (metis abs_mult mult_commute)
-have 1: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
-   X1 \<le> (0\<Colon>'a\<Colon>linordered_idom) \<or> \<bar>X2\<bar> * X1 = \<bar>X2 * X1\<bar>"
-  by (metis abs_mult_pos linorder_linear)
-have 2: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
-   \<not> (0\<Colon>'a\<Colon>linordered_idom) < X1 * X2 \<or>
-   \<not> (0\<Colon>'a\<Colon>linordered_idom) \<le> X2 \<or> \<not> X1 \<le> (0\<Colon>'a\<Colon>linordered_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>linordered_idom) x\<bar>
-   \<le> (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
-assume 4: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
-  \<le> \<bar>c\<Colon>'a\<Colon>linordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
-have 5: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
-  \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
-  by (metis 4 abs_mult)
-have 6: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
-   \<not> X1 \<le> (0\<Colon>'a\<Colon>linordered_idom) \<or> X1 \<le> \<bar>X2\<bar>"
-  by (metis abs_ge_zero xt1(6))
-have 7: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
-   X1 \<le> \<bar>X2\<bar> \<or> (0\<Colon>'a\<Colon>linordered_idom) < X1"
-  by (metis not_leE 6)
-have 8: "(0\<Colon>'a\<Colon>linordered_idom) < \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
-  by (metis 5 7)
-have 9: "\<And>X1\<Colon>'a\<Colon>linordered_idom.
-   \<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar> \<le> X1 \<or>
-   (0\<Colon>'a\<Colon>linordered_idom) < X1"
-  by (metis 8 order_less_le_trans)
-have 10: "(0\<Colon>'a\<Colon>linordered_idom)
-< (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
-  by (metis 3 9)
-have 11: "\<not> (c\<Colon>'a\<Colon>linordered_idom) \<le> (0\<Colon>'a\<Colon>linordered_idom)"
-  by (metis abs_ge_zero 2 10)
-have 12: "\<And>X1\<Colon>'a\<Colon>linordered_idom. (c\<Colon>'a\<Colon>linordered_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>linordered_idom) X1
-   \<le> (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_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>linordered_idom) X1
-   \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1\<bar>"
-  by (metis 0 12 13)
-have 15: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_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>linordered_idom) X2\<Colon>'a\<Colon>linordered_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>linordered_idom) X2\<Colon>'a\<Colon>linordered_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>linordered_idom) X1
-   \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1\<bar>"
-  by (metis 17 3 15)
-show "False"
-  by (metis abs_le_iff 5 18 14)
+proof -
+  fix c :: 'a and x :: 'b
+  assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
+  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_ge_zero)
+  have F2: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+  have F3: "\<forall>x\<^isub>1 x\<^isub>3. x\<^isub>3 \<le> \<bar>h x\<^isub>1\<bar> \<longrightarrow> x\<^isub>3 \<le> c * \<bar>f x\<^isub>1\<bar>" by (metis A1 order_trans)
+  have F4: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
+    by (metis abs_mult)
+  have F5: "\<forall>x\<^isub>3 x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^isub>1 \<longrightarrow> \<bar>x\<^isub>3 * x\<^isub>1\<bar> = \<bar>x\<^isub>3\<bar> * x\<^isub>1"
+    by (metis abs_mult_pos)
+  hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = \<bar>1\<bar> * x\<^isub>1" by (metis F2)
+  hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F2 abs_one)
+  hence "\<forall>x\<^isub>3. 0 \<le> \<bar>h x\<^isub>3\<bar> \<longrightarrow> \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" by (metis F3)
+  hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" by (metis F1)
+  hence "\<forall>x\<^isub>3. (0\<Colon>'a) \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F5)
+  hence "\<forall>x\<^isub>3. (0\<Colon>'a) \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F4)
+  hence "\<forall>x\<^isub>3. c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F1)
+  hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1)
+  thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4)
 qed
 
 sledgehammer_params [shrink_factor = 2]
@@ -106,36 +67,17 @@
   apply (case_tac "c = 0", simp)
   apply (rule_tac x = "1" in exI, simp)
   apply (rule_tac x = "abs c" in exI, auto);
-proof (neg_clausify)
-fix c x
-have 0: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_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>linordered_idom) x\<bar>
-   \<le> (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
-assume 2: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
-  \<le> \<bar>c\<Colon>'a\<Colon>linordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
-have 3: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
-  \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
-  by (metis 2 abs_mult)
-have 4: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
-   \<not> X1 \<le> (0\<Colon>'a\<Colon>linordered_idom) \<or> X1 \<le> \<bar>X2\<bar>"
-  by (metis abs_ge_zero xt1(6))
-have 5: "(0\<Colon>'a\<Colon>linordered_idom) < \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
-  by (metis not_leE 4 3)
-have 6: "(0\<Colon>'a\<Colon>linordered_idom)
-< (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
-  by (metis 1 order_less_le_trans 5)
-have 7: "\<And>X1\<Colon>'a\<Colon>linordered_idom. (c\<Colon>'a\<Colon>linordered_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>linordered_idom) X1
-   \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1\<bar>"
-  by (metis 0 7 abs_le_D2 1)
-have 9: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_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 8 abs_ge_zero abs_mult_pos abs_mult 1 9 3 abs_le_iff)
+proof -
+  fix c :: 'a and x :: 'b
+  assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
+  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+  have F2: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
+    by (metis abs_mult)
+  have "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_mult_pos abs_one)
+  hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" by (metis A1 abs_ge_zero order_trans)
+  hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F2 abs_mult_pos)
+  hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero)
+  thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2)
 qed
 
 sledgehammer_params [shrink_factor = 3]
@@ -146,30 +88,17 @@
   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);
-proof (neg_clausify)
-fix c x
-assume 0: "\<And>x\<Colon>'b\<Colon>type.
-   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>
-   \<le> (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
-assume 1: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
-  \<le> \<bar>c\<Colon>'a\<Colon>linordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
-have 2: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
-   X1 \<le> \<bar>X2\<bar> \<or> (0\<Colon>'a\<Colon>linordered_idom) < X1"
-  by (metis abs_ge_zero xt1(6) not_leE)
-have 3: "\<not> (c\<Colon>'a\<Colon>linordered_idom) \<le> (0\<Colon>'a\<Colon>linordered_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>linordered_idom) X2\<Colon>'a\<Colon>linordered_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>linordered_idom) X1
-   \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1\<bar>"
-  by (metis 4 0 xt1(6) abs_ge_self abs_le_D1)
-show "False"
-  by (metis abs_mult mult_commute 3 abs_mult_pos linorder_linear 0 abs_le_D2 5 1 abs_le_iff)
+  apply (rule_tac x = "abs c" in exI, auto)
+proof -
+  fix c :: 'a and x :: 'b
+  assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
+  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+  have F2: "\<forall>x\<^isub>3 x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^isub>1 \<longrightarrow> \<bar>x\<^isub>3 * x\<^isub>1\<bar> = \<bar>x\<^isub>3\<bar> * x\<^isub>1" by (metis abs_mult_pos)
+  hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_one)
+  hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F2 A1 abs_ge_zero order_trans)
+  thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_mult abs_ge_zero)
 qed
 
-
 sledgehammer_params [shrink_factor = 4]
 
 lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). 
@@ -178,33 +107,18 @@
   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);
-proof (neg_clausify)
-fix c x  (*sort/type constraint inserted by hand!*)
-have 0: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2. \<bar>X1 * \<bar>X2\<bar>\<bar> = \<bar>X1 * X2\<bar>"
-  by (metis abs_ge_zero abs_mult_pos abs_mult)
-assume 1: "\<And>A. \<bar>h A\<bar> \<le> c * \<bar>f A\<bar>"
-have 2: "\<And>X1 X2. \<not> \<bar>X1\<bar> \<le> X2 \<or> (0\<Colon>'a) \<le> X2"
-  by (metis abs_ge_zero order_trans)
-have 3: "\<And>X1. (0\<Colon>'a) \<le> c * \<bar>f X1\<bar>"
-  by (metis 1 2)
-have 4: "\<And>X1. c * \<bar>f X1\<bar> = \<bar>c * f X1\<bar>"
-  by (metis 0 abs_of_nonneg 3)
-have 5: "\<And>X1. - h X1 \<le> c * \<bar>f X1\<bar>"
-  by (metis 1 abs_le_D2)
-have 6: "\<And>X1. - h X1 \<le> \<bar>c * f X1\<bar>"
-  by (metis 4 5)
-have 7: "\<And>X1. h X1 \<le> c * \<bar>f X1\<bar>"
-  by (metis 1 abs_le_D1)
-have 8: "\<And>X1. h X1 \<le> \<bar>c * f X1\<bar>"
-  by (metis 4 7)
-assume 9: "\<not> \<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>"
-have 10: "\<not> \<bar>h x\<bar> \<le> \<bar>c * f x\<bar>"
-  by (metis abs_mult 9)
-show "False"
-  by (metis 6 8 10 abs_leI)
+  apply (rule_tac x = "abs c" in exI, auto)
+proof -
+  fix c :: 'a and x :: 'b
+  assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
+  have "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+  hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>"
+    by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one)
+  hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero abs_mult_pos abs_mult)
+  thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult)
 qed
 
+sledgehammer_params [shrink_factor = 1]
 
 lemma bigo_alt_def: "O(f) = 
     {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"
@@ -230,29 +144,13 @@
 
 declare [[ atp_problem_prefix = "BigO__bigo_refl" ]]
 lemma bigo_refl [intro]: "f : O(f)"
-  apply(auto simp add: bigo_def)
-proof (neg_clausify)
-fix x
-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
+apply (auto simp add: bigo_def)
+by (metis class_semiring.mul_1 order_refl)
 
 declare [[ atp_problem_prefix = "BigO__bigo_zero" ]]
 lemma bigo_zero: "0 : O(g)"
-  apply (auto simp add: bigo_def func_zero)
-proof (neg_clausify)
-fix x
-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
+apply (auto simp add: bigo_def func_zero)
+by (metis class_semiring.mul_0 order_refl)
 
 lemma bigo_zero2: "O(%x.0) = {%x.0}"
   apply (auto simp add: bigo_def) 
@@ -365,103 +263,36 @@
 lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> 
     f : O(g)" 
   apply (auto simp add: bigo_def)
-(*Version 1: one-shot proof*)
+(* Version 1: one-line proof *)
   apply (metis abs_le_D1 linorder_class.not_less  order_less_le  Orderings.xt1(12)  abs_mult)
   done
 
 lemma (*bigo_bounded_alt:*) "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> 
-    f : O(g)" 
-  apply (auto simp add: bigo_def)
-(*Version 2: single-step proof*)
-proof (neg_clausify)
-fix x
-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>linordered_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)
-have 6: "\<And>X3. \<not> X3 * X3 < (0\<Colon>'b\<Colon>linordered_idom)"
-  by (metis not_square_less_zero)
-have 7: "\<And>X1 X3::'b. \<bar>X1\<bar> * \<bar>X3\<bar> = \<bar>X3 * X1\<bar>"
-  by (metis abs_mult mult_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 mult_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)
+    f : O(g)"
+apply (auto simp add: bigo_def)
+(* Version 2: structured proof *)
+proof -
+  assume "\<forall>x. f x \<le> c * g x"
+  thus "\<exists>c. \<forall>x. f x \<le> c * \<bar>g x\<bar>" by (metis abs_mult abs_ge_self order_trans)
 qed
 
+text{*So here is the easier (and more natural) problem using transitivity*}
+declare [[ atp_problem_prefix = "BigO__bigo_bounded_alt_trans" ]]
+lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" 
+apply (auto simp add: bigo_def)
+(* Version 1: one-line proof *)
+by (metis abs_ge_self abs_mult order_trans)
 
 text{*So here is the easier (and more natural) problem using transitivity*}
 declare [[ atp_problem_prefix = "BigO__bigo_bounded_alt_trans" ]]
 lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" 
   apply (auto simp add: bigo_def)
-  (*Version 1: one-shot proof*) 
-  apply (metis Orderings.leD Orderings.leI abs_ge_self abs_le_D1 abs_mult abs_of_nonneg order_le_less)
-  done
-
-text{*So here is the easier (and more natural) problem using transitivity*}
-declare [[ atp_problem_prefix = "BigO__bigo_bounded_alt_trans" ]]
-lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" 
-  apply (auto simp add: bigo_def)
-(*Version 2: single-step proof*)
-proof (neg_clausify)
-fix x
-assume 0: "\<And>A\<Colon>'a\<Colon>type.
-   (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) A
-   \<le> (c\<Colon>'b\<Colon>linordered_idom) * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) A"
-assume 1: "\<And>A\<Colon>'b\<Colon>linordered_idom.
-   \<not> (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) ((x\<Colon>'b\<Colon>linordered_idom \<Rightarrow> 'a\<Colon>type) A)
-     \<le> A * \<bar>(g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) (x A)\<bar>"
-have 2: "\<And>X2\<Colon>'a\<Colon>type.
-   \<not> (c\<Colon>'b\<Colon>linordered_idom) * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) X2
-     < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) X2"
-  by (metis 0 linorder_not_le)
-have 3: "\<And>X2\<Colon>'b\<Colon>linordered_idom.
-   \<not> (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) ((x\<Colon>'b\<Colon>linordered_idom \<Rightarrow> 'a\<Colon>type) \<bar>X2\<bar>)
-     \<le> \<bar>X2 * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) (x \<bar>X2\<bar>)\<bar>"
-  by (metis abs_mult 1)
-have 4: "\<And>X2\<Colon>'b\<Colon>linordered_idom.
-   \<bar>X2 * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) ((x\<Colon>'b\<Colon>linordered_idom \<Rightarrow> 'a\<Colon>type) \<bar>X2\<bar>)\<bar>
-   < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) (x \<bar>X2\<bar>)"
-  by (metis 3 linorder_not_less)
-have 5: "\<And>X2\<Colon>'b\<Colon>linordered_idom.
-   X2 * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) ((x\<Colon>'b\<Colon>linordered_idom \<Rightarrow> 'a\<Colon>type) \<bar>X2\<bar>)
-   < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) (x \<bar>X2\<bar>)"
-  by (metis abs_less_iff 4)
-show "False"
-  by (metis 2 5)
+(* Version 2: structured proof *)
+proof -
+  assume "\<forall>x. f x \<le> c * g x"
+  thus "\<exists>c. \<forall>x. f x \<le> c * \<bar>g x\<bar>" by (metis abs_mult abs_ge_self order_trans)
 qed
 
-
 lemma bigo_bounded: "ALL x. 0 <= f x ==> ALL x. f x <= g x ==> 
     f : O(g)" 
   apply (erule bigo_bounded_alt [of f 1 g])
@@ -471,63 +302,37 @@
 declare [[ atp_problem_prefix = "BigO__bigo_bounded2" ]]
 lemma bigo_bounded2: "ALL x. lb x <= f x ==> ALL x. f x <= lb x + g x ==>
     f : lb +o O(g)"
-  apply (rule set_minus_imp_plus)
-  apply (rule bigo_bounded)
-  apply (auto simp add: diff_minus fun_Compl_def func_plus)
-  prefer 2
-  apply (drule_tac x = x in spec)+ 
-  apply arith (*not clear that it's provable otherwise*) 
-proof (neg_clausify)
-fix x
-assume 0: "\<And>y. lb y \<le> f y"
-assume 1: "\<not> (0\<Colon>'b) \<le> f x + - lb x"
-have 2: "\<And>X3. (0\<Colon>'b) + X3 = X3"
-  by (metis diff_eq_eq right_minus_eq)
-have 3: "\<not> (0\<Colon>'b) \<le> f x - lb x"
-  by (metis 1 diff_minus)
-have 4: "\<not> (0\<Colon>'b) + lb x \<le> f x"
-  by (metis 3 le_diff_eq)
-show "False"
-  by (metis 4 2 0)
+apply (rule set_minus_imp_plus)
+apply (rule bigo_bounded)
+ apply (auto simp add: diff_minus fun_Compl_def func_plus)
+ prefer 2
+ apply (drule_tac x = x in spec)+
+ apply (metis add_right_mono class_semiring.semiring_rules(24) diff_add_cancel diff_minus_eq_add le_less order_trans)
+proof -
+  fix x :: 'a
+  assume "\<forall>x. lb x \<le> f x"
+  thus "(0\<Colon>'b) \<le> f x + - lb x" by (metis not_leE diff_minus less_iff_diff_less_0 less_le_not_le)
 qed
 
 declare [[ atp_problem_prefix = "BigO__bigo_abs" ]]
 lemma bigo_abs: "(%x. abs(f x)) =o O(f)" 
-  apply (unfold bigo_def)
-  apply auto
-proof (neg_clausify)
-fix x
-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
+apply (unfold bigo_def)
+apply auto
+by (metis class_semiring.mul_1 order_refl)
 
 declare [[ atp_problem_prefix = "BigO__bigo_abs2" ]]
 lemma bigo_abs2: "f =o O(%x. abs(f x))"
-  apply (unfold bigo_def)
-  apply auto
-proof (neg_clausify)
-fix x
-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
+apply (unfold bigo_def)
+apply auto
+by (metis class_semiring.mul_1 order_refl)
  
 lemma bigo_abs3: "O(f) = O(%x. abs(f x))"
-  apply (rule equalityI)
-  apply (rule bigo_elt_subset)
-  apply (rule bigo_abs2)
-  apply (rule bigo_elt_subset)
-  apply (rule bigo_abs)
-done
+proof -
+  have F1: "\<forall>v u. u \<in> O(v) \<longrightarrow> O(u) \<subseteq> O(v)" by (metis bigo_elt_subset)
+  have F2: "\<forall>u. (\<lambda>R. \<bar>u R\<bar>) \<in> O(u)" by (metis bigo_abs)
+  have "\<forall>u. u \<in> O(\<lambda>R. \<bar>u R\<bar>)" by (metis bigo_abs2)
+  thus "O(f) = O(\<lambda>x. \<bar>f x\<bar>)" using F1 F2 by auto
+qed 
 
 lemma bigo_abs4: "f =o g +o O(h) ==> 
     (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)"
@@ -597,63 +402,9 @@
   abs_mult mult_pos_pos)
   apply (erule ssubst) 
   apply (subst abs_mult)
-(*not qute BigO__bigo_mult_simpler_1 (a hard problem!) as abs_mult has
-  just been done*)
-proof (neg_clausify)
-fix a c b ca x
-assume 0: "(0\<Colon>'b\<Colon>linordered_idom) < (c\<Colon>'b\<Colon>linordered_idom)"
-assume 1: "\<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar>
-\<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>"
-assume 2: "\<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar>
-\<le> (ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>"
-assume 3: "\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar> *
-  \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>
-  \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> *
-    ((ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>)"
-have 4: "\<bar>c\<Colon>'b\<Colon>linordered_idom\<bar> = c"
-  by (metis abs_of_pos 0)
-have 5: "\<And>X1\<Colon>'b\<Colon>linordered_idom. (c\<Colon>'b\<Colon>linordered_idom) * \<bar>X1\<bar> = \<bar>c * X1\<bar>"
-  by (metis abs_mult 4)
-have 6: "(0\<Colon>'b\<Colon>linordered_idom) = (1\<Colon>'b\<Colon>linordered_idom) \<or>
-(0\<Colon>'b\<Colon>linordered_idom) < (1\<Colon>'b\<Colon>linordered_idom)"
-  by (metis abs_not_less_zero abs_one linorder_neqE_linordered_idom)
-have 7: "(0\<Colon>'b\<Colon>linordered_idom) < (1\<Colon>'b\<Colon>linordered_idom)"
-  by (metis 6 one_neq_zero)
-have 8: "\<bar>1\<Colon>'b\<Colon>linordered_idom\<bar> = (1\<Colon>'b\<Colon>linordered_idom)"
-  by (metis abs_of_pos 7)
-have 9: "\<And>X1\<Colon>'b\<Colon>linordered_idom. (0\<Colon>'b\<Colon>linordered_idom) \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>X1\<bar>"
-  by (metis abs_ge_zero 5)
-have 10: "\<And>X1\<Colon>'b\<Colon>linordered_idom. X1 * (1\<Colon>'b\<Colon>linordered_idom) = X1"
-  by (metis mult_cancel_right2 mult_commute)
-have 11: "\<And>X1\<Colon>'b\<Colon>linordered_idom. \<bar>\<bar>X1\<bar>\<bar> = \<bar>X1\<bar> * \<bar>1\<Colon>'b\<Colon>linordered_idom\<bar>"
-  by (metis abs_mult abs_idempotent 10)
-have 12: "\<And>X1\<Colon>'b\<Colon>linordered_idom. \<bar>\<bar>X1\<bar>\<bar> = \<bar>X1\<bar>"
-  by (metis 11 8 10)
-have 13: "\<And>X1\<Colon>'b\<Colon>linordered_idom. (0\<Colon>'b\<Colon>linordered_idom) \<le> \<bar>X1\<bar>"
-  by (metis abs_ge_zero 12)
-have 14: "\<not> (0\<Colon>'b\<Colon>linordered_idom)
-  \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar> \<or>
-\<not> (0\<Colon>'b\<Colon>linordered_idom) \<le> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<or>
-\<not> \<bar>b x\<bar> \<le> (ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<or>
-\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<le> c * \<bar>f x\<bar>"
-  by (metis 3 mult_mono)
-have 15: "\<not> (0\<Colon>'b\<Colon>linordered_idom) \<le> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar> \<or>
-\<not> \<bar>b x\<bar> \<le> (ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<or>
-\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>
-  \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>"
-  by (metis 14 9)
-have 16: "\<not> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar>
-  \<le> (ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<or>
-\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>
-  \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>"
-  by (metis 15 13)
-have 17: "\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar>
-  \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>"
-  by (metis 16 2)
-show 18: "False"
-  by (metis 17 1)
-qed
-
+(* not quite as hard as BigO__bigo_mult_simpler_1 (a hard problem!) since
+   abs_mult has just been done *)
+by (metis abs_ge_zero mult_mono')
 
 declare [[ atp_problem_prefix = "BigO__bigo_mult2" ]]
 lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)"
@@ -672,7 +423,7 @@
 
 declare [[ atp_problem_prefix = "BigO__bigo_mult3" ]]
 lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)"
-by (metis bigo_mult set_times_intro subset_iff)
+by (metis bigo_mult set_rev_mp set_times_intro)
 
 declare [[ atp_problem_prefix = "BigO__bigo_mult4" ]]
 lemma bigo_mult4 [intro]:"f : k +o O(h) ==> g * f : (g * k) +o O(g * h)"
@@ -809,40 +560,16 @@
 by (metis bigo_const1 bigo_elt_subset);
 
 lemma bigo_const2 [intro]: "O(%x. c::'b::linordered_idom) <= O(%x. 1)";
-(*??FAILS because the two occurrences of COMBK have different polymorphic types
-proof (neg_clausify)
-assume 0: "\<not> O(COMBK (c\<Colon>'b\<Colon>linordered_idom)) \<subseteq> O(COMBK (1\<Colon>'b\<Colon>linordered_idom))"
-have 1: "COMBK (c\<Colon>'b\<Colon>linordered_idom) \<notin> O(COMBK (1\<Colon>'b\<Colon>linordered_idom))"
-apply (rule notI) 
-apply (rule 0 [THEN notE]) 
-apply (rule bigo_elt_subset) 
-apply assumption; 
-sorry
-  by (metis 0 bigo_elt_subset)  loops??
-show "False"
-  by (metis 1 bigo_const1)
+(* "thus" had to be replaced by "show" with an explicit reference to "F1" *)
+proof -
+  have F1: "\<forall>u. (\<lambda>Q. u) \<in> O(\<lambda>Q. 1)" by (metis bigo_const1)
+  show "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)" by (metis F1 bigo_elt_subset)
 qed
-*)
-  apply (rule bigo_elt_subset)
-  apply (rule bigo_const1)
-done
 
 declare [[ atp_problem_prefix = "BigO__bigo_const3" ]]
 lemma bigo_const3: "(c::'a::linordered_field) ~= 0 ==> (%x. 1) : O(%x. c)"
 apply (simp add: bigo_def)
-proof (neg_clausify)
-assume 0: "(c\<Colon>'a\<Colon>linordered_field) \<noteq> (0\<Colon>'a\<Colon>linordered_field)"
-assume 1: "\<And>A\<Colon>'a\<Colon>linordered_field. \<not> (1\<Colon>'a\<Colon>linordered_field) \<le> A * \<bar>c\<Colon>'a\<Colon>linordered_field\<bar>"
-have 2: "(0\<Colon>'a\<Colon>linordered_field) = \<bar>c\<Colon>'a\<Colon>linordered_field\<bar> \<or>
-\<not> (1\<Colon>'a\<Colon>linordered_field) \<le> (1\<Colon>'a\<Colon>linordered_field)"
-  by (metis 1 field_inverse)
-have 3: "\<bar>c\<Colon>'a\<Colon>linordered_field\<bar> = (0\<Colon>'a\<Colon>linordered_field)"
-  by (metis linorder_neq_iff linorder_antisym_conv1 2)
-have 4: "(0\<Colon>'a\<Colon>linordered_field) = (c\<Colon>'a\<Colon>linordered_field)"
-  by (metis 3 abs_eq_0)
-show "False"
-  by (metis 0 4)
-qed
+by (metis abs_eq_0 left_inverse order_refl)
 
 lemma bigo_const4: "(c::'a::linordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)"
 by (rule bigo_elt_subset, rule bigo_const3, assumption)
@@ -854,15 +581,7 @@
 declare [[ atp_problem_prefix = "BigO__bigo_const_mult1" ]]
 lemma bigo_const_mult1: "(%x. c * f x) : O(f)"
   apply (simp add: bigo_def abs_mult)
-proof (neg_clausify)
-fix x
-assume 0: "\<And>xa\<Colon>'b\<Colon>linordered_idom.
-   \<not> \<bar>c\<Colon>'b\<Colon>linordered_idom\<bar> *
-     \<bar>(f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) ((x\<Colon>'b\<Colon>linordered_idom \<Rightarrow> 'a\<Colon>type) xa)\<bar>
-     \<le> xa * \<bar>f (x xa)\<bar>"
-show "False"
-  by (metis linorder_neq_iff linorder_antisym_conv1 0)
-qed
+by (metis le_less)
 
 lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"
 by (rule bigo_elt_subset, rule bigo_const_mult1)
@@ -870,7 +589,7 @@
 declare [[ atp_problem_prefix = "BigO__bigo_const_mult3" ]]
 lemma bigo_const_mult3: "(c::'a::linordered_field) ~= 0 ==> f : O(%x. c * f x)"
   apply (simp add: bigo_def)
-(*sledgehammer [no luck]*); 
+(*sledgehammer [no luck]*)
   apply (rule_tac x = "abs(inverse c)" in exI)
   apply (simp only: abs_mult [symmetric] mult_assoc [symmetric])
 apply (subst left_inverse) 
@@ -1132,15 +851,17 @@
 
 declare [[ atp_problem_prefix = "BigO__bigo_lesso1" ]]
 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")
-(*??Translation of TSTP raised an exception: Type unification failed: Variable ?'X2.0::type not of sort ord*)
-apply (metis bigo_zero)
+apply (unfold lesso_def)
+apply (subgoal_tac "(%x. max (f x - g x) 0) = 0")
+proof -
+  assume "(\<lambda>x. max (f x - g x) 0) = 0"
+  thus "(\<lambda>x. max (f x - g x) 0) \<in> O(h)" by (metis bigo_zero)
+next
+  show "\<forall>x\<Colon>'a. f x \<le> g x \<Longrightarrow> (\<lambda>x\<Colon>'a. max (f x - g x) (0\<Colon>'b)) = (0\<Colon>'a \<Rightarrow> 'b)"
   apply (unfold func_zero)
   apply (rule ext)
-  apply (simp split: split_max)
-done
-
+  by (simp split: split_max)
+qed
 
 declare [[ atp_problem_prefix = "BigO__bigo_lesso2" ]]
 lemma bigo_lesso2: "f =o g +o O(h) ==>
@@ -1156,8 +877,9 @@
 apply (erule thin_rl)
 (*sledgehammer*);  
   apply (case_tac "0 <= k x - g x")
-  prefer 2 (*re-order subgoals because I don't know what to put after a structured proof*)
-   apply (metis abs_ge_zero abs_minus_commute linorder_linear min_max.sup_absorb1 min_max.sup_commute)
+(* apply (metis abs_le_iff add_le_imp_le_right diff_minus le_less
+                le_max_iff_disj min_max.le_supE min_max.sup_absorb2
+                min_max.sup_commute) *)
 proof (neg_clausify)
 fix x
 assume 0: "\<And>A. k A \<le> f A"
@@ -1177,6 +899,11 @@
   by (metis 5 abs_minus_commute 7 min_max.sup_commute 6)
 show "False"
   by (metis min_max.sup_commute min_max.inf_commute min_max.sup_inf_absorb min_max.le_iff_inf 0 max_diff_distrib_left 1 linorder_not_le 8)
+next
+  show "\<And>x\<Colon>'a.
+       \<lbrakk>\<forall>x\<Colon>'a. (0\<Colon>'b) \<le> k x; \<forall>x\<Colon>'a. k x \<le> f x; \<not> (0\<Colon>'b) \<le> k x - g x\<rbrakk>
+       \<Longrightarrow> max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>"
+    by (metis abs_ge_zero le_cases min_max.sup_absorb2)
 qed
 
 declare [[ atp_problem_prefix = "BigO__bigo_lesso3" ]]