src/HOL/Metis_Examples/BigO.thy
changeset 35028 108662d50512
parent 33027 9cf389429f6d
child 35050 9f841f20dca6
     1.1 --- a/src/HOL/Metis_Examples/BigO.thy	Fri Feb 05 14:33:31 2010 +0100
     1.2 +++ b/src/HOL/Metis_Examples/BigO.thy	Fri Feb 05 14:33:50 2010 +0100
     1.3 @@ -12,11 +12,11 @@
     1.4  
     1.5  subsection {* Definitions *}
     1.6  
     1.7 -definition bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set"    ("(1O'(_'))") where
     1.8 +definition bigo :: "('a => 'b::linordered_idom) => ('a => 'b) set"    ("(1O'(_'))") where
     1.9    "O(f::('a => 'b)) ==   {h. EX c. ALL x. abs (h x) <= c * abs (f x)}"
    1.10  
    1.11  declare [[ atp_problem_prefix = "BigO__bigo_pos_const" ]]
    1.12 -lemma bigo_pos_const: "(EX (c::'a::ordered_idom). 
    1.13 +lemma bigo_pos_const: "(EX (c::'a::linordered_idom). 
    1.14      ALL x. (abs (h x)) <= (c * (abs (f x))))
    1.15        = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
    1.16    apply auto
    1.17 @@ -30,7 +30,7 @@
    1.18  
    1.19  declare [[sledgehammer_modulus = 1]]
    1.20  
    1.21 -lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
    1.22 +lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). 
    1.23      ALL x. (abs (h x)) <= (c * (abs (f x))))
    1.24        = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
    1.25    apply auto
    1.26 @@ -39,59 +39,59 @@
    1.27    apply (rule_tac x = "abs c" in exI, auto)
    1.28  proof (neg_clausify)
    1.29  fix c x
    1.30 -have 0: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<bar>X1 * X2\<bar> = \<bar>X2 * X1\<bar>"
    1.31 +have 0: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom. \<bar>X1 * X2\<bar> = \<bar>X2 * X1\<bar>"
    1.32    by (metis abs_mult mult_commute)
    1.33 -have 1: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
    1.34 -   X1 \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or> \<bar>X2\<bar> * X1 = \<bar>X2 * X1\<bar>"
    1.35 +have 1: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
    1.36 +   X1 \<le> (0\<Colon>'a\<Colon>linordered_idom) \<or> \<bar>X2\<bar> * X1 = \<bar>X2 * X1\<bar>"
    1.37    by (metis abs_mult_pos linorder_linear)
    1.38 -have 2: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
    1.39 -   \<not> (0\<Colon>'a\<Colon>ordered_idom) < X1 * X2 \<or>
    1.40 -   \<not> (0\<Colon>'a\<Colon>ordered_idom) \<le> X2 \<or> \<not> X1 \<le> (0\<Colon>'a\<Colon>ordered_idom)"
    1.41 +have 2: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
    1.42 +   \<not> (0\<Colon>'a\<Colon>linordered_idom) < X1 * X2 \<or>
    1.43 +   \<not> (0\<Colon>'a\<Colon>linordered_idom) \<le> X2 \<or> \<not> X1 \<le> (0\<Colon>'a\<Colon>linordered_idom)"
    1.44    by (metis linorder_not_less mult_nonneg_nonpos2)
    1.45  assume 3: "\<And>x\<Colon>'b\<Colon>type.
    1.46 -   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>
    1.47 -   \<le> (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
    1.48 -assume 4: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
    1.49 -  \<le> \<bar>c\<Colon>'a\<Colon>ordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
    1.50 -have 5: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
    1.51 -  \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
    1.52 +   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>
    1.53 +   \<le> (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
    1.54 +assume 4: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
    1.55 +  \<le> \<bar>c\<Colon>'a\<Colon>linordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
    1.56 +have 5: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
    1.57 +  \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
    1.58    by (metis 4 abs_mult)
    1.59 -have 6: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
    1.60 -   \<not> X1 \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or> X1 \<le> \<bar>X2\<bar>"
    1.61 +have 6: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
    1.62 +   \<not> X1 \<le> (0\<Colon>'a\<Colon>linordered_idom) \<or> X1 \<le> \<bar>X2\<bar>"
    1.63    by (metis abs_ge_zero xt1(6))
    1.64 -have 7: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
    1.65 -   X1 \<le> \<bar>X2\<bar> \<or> (0\<Colon>'a\<Colon>ordered_idom) < X1"
    1.66 +have 7: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
    1.67 +   X1 \<le> \<bar>X2\<bar> \<or> (0\<Colon>'a\<Colon>linordered_idom) < X1"
    1.68    by (metis not_leE 6)
    1.69 -have 8: "(0\<Colon>'a\<Colon>ordered_idom) < \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
    1.70 +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>"
    1.71    by (metis 5 7)
    1.72 -have 9: "\<And>X1\<Colon>'a\<Colon>ordered_idom.
    1.73 -   \<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar> \<le> X1 \<or>
    1.74 -   (0\<Colon>'a\<Colon>ordered_idom) < X1"
    1.75 +have 9: "\<And>X1\<Colon>'a\<Colon>linordered_idom.
    1.76 +   \<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar> \<le> X1 \<or>
    1.77 +   (0\<Colon>'a\<Colon>linordered_idom) < X1"
    1.78    by (metis 8 order_less_le_trans)
    1.79 -have 10: "(0\<Colon>'a\<Colon>ordered_idom)
    1.80 -< (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
    1.81 +have 10: "(0\<Colon>'a\<Colon>linordered_idom)
    1.82 +< (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
    1.83    by (metis 3 9)
    1.84 -have 11: "\<not> (c\<Colon>'a\<Colon>ordered_idom) \<le> (0\<Colon>'a\<Colon>ordered_idom)"
    1.85 +have 11: "\<not> (c\<Colon>'a\<Colon>linordered_idom) \<le> (0\<Colon>'a\<Colon>linordered_idom)"
    1.86    by (metis abs_ge_zero 2 10)
    1.87 -have 12: "\<And>X1\<Colon>'a\<Colon>ordered_idom. (c\<Colon>'a\<Colon>ordered_idom) * \<bar>X1\<bar> = \<bar>X1 * c\<bar>"
    1.88 +have 12: "\<And>X1\<Colon>'a\<Colon>linordered_idom. (c\<Colon>'a\<Colon>linordered_idom) * \<bar>X1\<bar> = \<bar>X1 * c\<bar>"
    1.89    by (metis mult_commute 1 11)
    1.90  have 13: "\<And>X1\<Colon>'b\<Colon>type.
    1.91 -   - (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1
    1.92 -   \<le> (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1\<bar>"
    1.93 +   - (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1
    1.94 +   \<le> (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1\<bar>"
    1.95    by (metis 3 abs_le_D2)
    1.96  have 14: "\<And>X1\<Colon>'b\<Colon>type.
    1.97 -   - (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1
    1.98 -   \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1\<bar>"
    1.99 +   - (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1
   1.100 +   \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1\<bar>"
   1.101    by (metis 0 12 13)
   1.102 -have 15: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<bar>X1 * \<bar>X2\<bar>\<bar> = \<bar>X1 * X2\<bar>"
   1.103 +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>"
   1.104    by (metis abs_mult abs_mult_pos abs_ge_zero)
   1.105 -have 16: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. X1 \<le> \<bar>X2\<bar> \<or> \<not> X1 \<le> X2"
   1.106 +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"
   1.107    by (metis xt1(6) abs_ge_self)
   1.108 -have 17: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<not> \<bar>X1\<bar> \<le> X2 \<or> X1 \<le> \<bar>X2\<bar>"
   1.109 +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>"
   1.110    by (metis 16 abs_le_D1)
   1.111  have 18: "\<And>X1\<Colon>'b\<Colon>type.
   1.112 -   (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1
   1.113 -   \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1\<bar>"
   1.114 +   (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1
   1.115 +   \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1\<bar>"
   1.116    by (metis 17 3 15)
   1.117  show "False"
   1.118    by (metis abs_le_iff 5 18 14)
   1.119 @@ -99,7 +99,7 @@
   1.120  
   1.121  declare [[sledgehammer_modulus = 2]]
   1.122  
   1.123 -lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
   1.124 +lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). 
   1.125      ALL x. (abs (h x)) <= (c * (abs (f x))))
   1.126        = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
   1.127    apply auto
   1.128 @@ -108,31 +108,31 @@
   1.129    apply (rule_tac x = "abs c" in exI, auto);
   1.130  proof (neg_clausify)
   1.131  fix c x
   1.132 -have 0: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<bar>X1 * X2\<bar> = \<bar>X2 * X1\<bar>"
   1.133 +have 0: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom. \<bar>X1 * X2\<bar> = \<bar>X2 * X1\<bar>"
   1.134    by (metis abs_mult mult_commute)
   1.135  assume 1: "\<And>x\<Colon>'b\<Colon>type.
   1.136 -   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>
   1.137 -   \<le> (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
   1.138 -assume 2: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
   1.139 -  \<le> \<bar>c\<Colon>'a\<Colon>ordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
   1.140 -have 3: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
   1.141 -  \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
   1.142 +   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>
   1.143 +   \<le> (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
   1.144 +assume 2: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
   1.145 +  \<le> \<bar>c\<Colon>'a\<Colon>linordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
   1.146 +have 3: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
   1.147 +  \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
   1.148    by (metis 2 abs_mult)
   1.149 -have 4: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
   1.150 -   \<not> X1 \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or> X1 \<le> \<bar>X2\<bar>"
   1.151 +have 4: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
   1.152 +   \<not> X1 \<le> (0\<Colon>'a\<Colon>linordered_idom) \<or> X1 \<le> \<bar>X2\<bar>"
   1.153    by (metis abs_ge_zero xt1(6))
   1.154 -have 5: "(0\<Colon>'a\<Colon>ordered_idom) < \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
   1.155 +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>"
   1.156    by (metis not_leE 4 3)
   1.157 -have 6: "(0\<Colon>'a\<Colon>ordered_idom)
   1.158 -< (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
   1.159 +have 6: "(0\<Colon>'a\<Colon>linordered_idom)
   1.160 +< (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
   1.161    by (metis 1 order_less_le_trans 5)
   1.162 -have 7: "\<And>X1\<Colon>'a\<Colon>ordered_idom. (c\<Colon>'a\<Colon>ordered_idom) * \<bar>X1\<bar> = \<bar>X1 * c\<bar>"
   1.163 +have 7: "\<And>X1\<Colon>'a\<Colon>linordered_idom. (c\<Colon>'a\<Colon>linordered_idom) * \<bar>X1\<bar> = \<bar>X1 * c\<bar>"
   1.164    by (metis abs_ge_zero linorder_not_less mult_nonneg_nonpos2 6 linorder_linear abs_mult_pos mult_commute)
   1.165  have 8: "\<And>X1\<Colon>'b\<Colon>type.
   1.166 -   - (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1
   1.167 -   \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1\<bar>"
   1.168 +   - (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1
   1.169 +   \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1\<bar>"
   1.170    by (metis 0 7 abs_le_D2 1)
   1.171 -have 9: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<not> \<bar>X1\<bar> \<le> X2 \<or> X1 \<le> \<bar>X2\<bar>"
   1.172 +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>"
   1.173    by (metis abs_ge_self xt1(6) abs_le_D1)
   1.174  show "False"
   1.175    by (metis 8 abs_ge_zero abs_mult_pos abs_mult 1 9 3 abs_le_iff)
   1.176 @@ -140,7 +140,7 @@
   1.177  
   1.178  declare [[sledgehammer_modulus = 3]]
   1.179  
   1.180 -lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
   1.181 +lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). 
   1.182      ALL x. (abs (h x)) <= (c * (abs (f x))))
   1.183        = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
   1.184    apply auto
   1.185 @@ -150,20 +150,20 @@
   1.186  proof (neg_clausify)
   1.187  fix c x
   1.188  assume 0: "\<And>x\<Colon>'b\<Colon>type.
   1.189 -   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>
   1.190 -   \<le> (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
   1.191 -assume 1: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
   1.192 -  \<le> \<bar>c\<Colon>'a\<Colon>ordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
   1.193 -have 2: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
   1.194 -   X1 \<le> \<bar>X2\<bar> \<or> (0\<Colon>'a\<Colon>ordered_idom) < X1"
   1.195 +   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>
   1.196 +   \<le> (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
   1.197 +assume 1: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
   1.198 +  \<le> \<bar>c\<Colon>'a\<Colon>linordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
   1.199 +have 2: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
   1.200 +   X1 \<le> \<bar>X2\<bar> \<or> (0\<Colon>'a\<Colon>linordered_idom) < X1"
   1.201    by (metis abs_ge_zero xt1(6) not_leE)
   1.202 -have 3: "\<not> (c\<Colon>'a\<Colon>ordered_idom) \<le> (0\<Colon>'a\<Colon>ordered_idom)"
   1.203 +have 3: "\<not> (c\<Colon>'a\<Colon>linordered_idom) \<le> (0\<Colon>'a\<Colon>linordered_idom)"
   1.204    by (metis abs_ge_zero mult_nonneg_nonpos2 linorder_not_less order_less_le_trans 1 abs_mult 2 0)
   1.205 -have 4: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<bar>X1 * \<bar>X2\<bar>\<bar> = \<bar>X1 * X2\<bar>"
   1.206 +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>"
   1.207    by (metis abs_ge_zero abs_mult_pos abs_mult)
   1.208  have 5: "\<And>X1\<Colon>'b\<Colon>type.
   1.209 -   (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1
   1.210 -   \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1\<bar>"
   1.211 +   (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1
   1.212 +   \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1\<bar>"
   1.213    by (metis 4 0 xt1(6) abs_ge_self abs_le_D1)
   1.214  show "False"
   1.215    by (metis abs_mult mult_commute 3 abs_mult_pos linorder_linear 0 abs_le_D2 5 1 abs_le_iff)
   1.216 @@ -172,7 +172,7 @@
   1.217  
   1.218  declare [[sledgehammer_modulus = 1]]
   1.219  
   1.220 -lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
   1.221 +lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). 
   1.222      ALL x. (abs (h x)) <= (c * (abs (f x))))
   1.223        = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
   1.224    apply auto
   1.225 @@ -181,7 +181,7 @@
   1.226    apply (rule_tac x = "abs c" in exI, auto);
   1.227  proof (neg_clausify)
   1.228  fix c x  (*sort/type constraint inserted by hand!*)
   1.229 -have 0: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2. \<bar>X1 * \<bar>X2\<bar>\<bar> = \<bar>X1 * X2\<bar>"
   1.230 +have 0: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2. \<bar>X1 * \<bar>X2\<bar>\<bar> = \<bar>X1 * X2\<bar>"
   1.231    by (metis abs_ge_zero abs_mult_pos abs_mult)
   1.232  assume 1: "\<And>A. \<bar>h A\<bar> \<le> c * \<bar>f A\<bar>"
   1.233  have 2: "\<And>X1 X2. \<not> \<bar>X1\<bar> \<le> X2 \<or> (0\<Colon>'a) \<le> X2"
   1.234 @@ -383,11 +383,11 @@
   1.235    by (metis 0 order_antisym_conv)
   1.236  have 3: "\<And>X3. \<not> f (x \<bar>X3\<bar>) \<le> \<bar>X3 * g (x \<bar>X3\<bar>)\<bar>"
   1.237    by (metis 1 abs_mult)
   1.238 -have 4: "\<And>X1 X3\<Colon>'b\<Colon>ordered_idom. X3 \<le> X1 \<or> X1 \<le> \<bar>X3\<bar>"
   1.239 +have 4: "\<And>X1 X3\<Colon>'b\<Colon>linordered_idom. X3 \<le> X1 \<or> X1 \<le> \<bar>X3\<bar>"
   1.240    by (metis linorder_linear abs_le_D1)
   1.241  have 5: "\<And>X3::'b. \<bar>X3\<bar> * \<bar>X3\<bar> = X3 * X3"
   1.242    by (metis abs_mult_self)
   1.243 -have 6: "\<And>X3. \<not> X3 * X3 < (0\<Colon>'b\<Colon>ordered_idom)"
   1.244 +have 6: "\<And>X3. \<not> X3 * X3 < (0\<Colon>'b\<Colon>linordered_idom)"
   1.245    by (metis not_square_less_zero)
   1.246  have 7: "\<And>X1 X3::'b. \<bar>X1\<bar> * \<bar>X3\<bar> = \<bar>X3 * X1\<bar>"
   1.247    by (metis abs_mult mult_commute)
   1.248 @@ -438,26 +438,26 @@
   1.249  proof (neg_clausify)
   1.250  fix x
   1.251  assume 0: "\<And>A\<Colon>'a\<Colon>type.
   1.252 -   (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) A
   1.253 -   \<le> (c\<Colon>'b\<Colon>ordered_idom) * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) A"
   1.254 -assume 1: "\<And>A\<Colon>'b\<Colon>ordered_idom.
   1.255 -   \<not> (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a\<Colon>type) A)
   1.256 -     \<le> A * \<bar>(g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) (x A)\<bar>"
   1.257 +   (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) A
   1.258 +   \<le> (c\<Colon>'b\<Colon>linordered_idom) * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) A"
   1.259 +assume 1: "\<And>A\<Colon>'b\<Colon>linordered_idom.
   1.260 +   \<not> (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) ((x\<Colon>'b\<Colon>linordered_idom \<Rightarrow> 'a\<Colon>type) A)
   1.261 +     \<le> A * \<bar>(g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) (x A)\<bar>"
   1.262  have 2: "\<And>X2\<Colon>'a\<Colon>type.
   1.263 -   \<not> (c\<Colon>'b\<Colon>ordered_idom) * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) X2
   1.264 -     < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) X2"
   1.265 +   \<not> (c\<Colon>'b\<Colon>linordered_idom) * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) X2
   1.266 +     < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) X2"
   1.267    by (metis 0 linorder_not_le)
   1.268 -have 3: "\<And>X2\<Colon>'b\<Colon>ordered_idom.
   1.269 -   \<not> (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a\<Colon>type) \<bar>X2\<bar>)
   1.270 -     \<le> \<bar>X2 * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X2\<bar>)\<bar>"
   1.271 +have 3: "\<And>X2\<Colon>'b\<Colon>linordered_idom.
   1.272 +   \<not> (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) ((x\<Colon>'b\<Colon>linordered_idom \<Rightarrow> 'a\<Colon>type) \<bar>X2\<bar>)
   1.273 +     \<le> \<bar>X2 * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) (x \<bar>X2\<bar>)\<bar>"
   1.274    by (metis abs_mult 1)
   1.275 -have 4: "\<And>X2\<Colon>'b\<Colon>ordered_idom.
   1.276 -   \<bar>X2 * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a\<Colon>type) \<bar>X2\<bar>)\<bar>
   1.277 -   < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X2\<bar>)"
   1.278 +have 4: "\<And>X2\<Colon>'b\<Colon>linordered_idom.
   1.279 +   \<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>
   1.280 +   < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) (x \<bar>X2\<bar>)"
   1.281    by (metis 3 linorder_not_less)
   1.282 -have 5: "\<And>X2\<Colon>'b\<Colon>ordered_idom.
   1.283 -   X2 * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a\<Colon>type) \<bar>X2\<bar>)
   1.284 -   < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X2\<bar>)"
   1.285 +have 5: "\<And>X2\<Colon>'b\<Colon>linordered_idom.
   1.286 +   X2 * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) ((x\<Colon>'b\<Colon>linordered_idom \<Rightarrow> 'a\<Colon>type) \<bar>X2\<bar>)
   1.287 +   < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) (x \<bar>X2\<bar>)"
   1.288    by (metis abs_less_iff 4)
   1.289  show "False"
   1.290    by (metis 2 5)
   1.291 @@ -603,54 +603,54 @@
   1.292    just been done*)
   1.293  proof (neg_clausify)
   1.294  fix a c b ca x
   1.295 -assume 0: "(0\<Colon>'b\<Colon>ordered_idom) < (c\<Colon>'b\<Colon>ordered_idom)"
   1.296 -assume 1: "\<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x\<Colon>'a)\<bar>
   1.297 -\<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>"
   1.298 -assume 2: "\<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x\<Colon>'a)\<bar>
   1.299 -\<le> (ca\<Colon>'b\<Colon>ordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>"
   1.300 -assume 3: "\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x\<Colon>'a)\<bar> *
   1.301 -  \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>
   1.302 -  \<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar> *
   1.303 -    ((ca\<Colon>'b\<Colon>ordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>)"
   1.304 -have 4: "\<bar>c\<Colon>'b\<Colon>ordered_idom\<bar> = c"
   1.305 +assume 0: "(0\<Colon>'b\<Colon>linordered_idom) < (c\<Colon>'b\<Colon>linordered_idom)"
   1.306 +assume 1: "\<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar>
   1.307 +\<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>"
   1.308 +assume 2: "\<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar>
   1.309 +\<le> (ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>"
   1.310 +assume 3: "\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar> *
   1.311 +  \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>
   1.312 +  \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> *
   1.313 +    ((ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>)"
   1.314 +have 4: "\<bar>c\<Colon>'b\<Colon>linordered_idom\<bar> = c"
   1.315    by (metis OrderedGroup.abs_of_pos 0)
   1.316 -have 5: "\<And>X1\<Colon>'b\<Colon>ordered_idom. (c\<Colon>'b\<Colon>ordered_idom) * \<bar>X1\<bar> = \<bar>c * X1\<bar>"
   1.317 +have 5: "\<And>X1\<Colon>'b\<Colon>linordered_idom. (c\<Colon>'b\<Colon>linordered_idom) * \<bar>X1\<bar> = \<bar>c * X1\<bar>"
   1.318    by (metis Ring_and_Field.abs_mult 4)
   1.319 -have 6: "(0\<Colon>'b\<Colon>ordered_idom) = (1\<Colon>'b\<Colon>ordered_idom) \<or>
   1.320 -(0\<Colon>'b\<Colon>ordered_idom) < (1\<Colon>'b\<Colon>ordered_idom)"
   1.321 -  by (metis OrderedGroup.abs_not_less_zero Ring_and_Field.abs_one Ring_and_Field.linorder_neqE_ordered_idom)
   1.322 -have 7: "(0\<Colon>'b\<Colon>ordered_idom) < (1\<Colon>'b\<Colon>ordered_idom)"
   1.323 +have 6: "(0\<Colon>'b\<Colon>linordered_idom) = (1\<Colon>'b\<Colon>linordered_idom) \<or>
   1.324 +(0\<Colon>'b\<Colon>linordered_idom) < (1\<Colon>'b\<Colon>linordered_idom)"
   1.325 +  by (metis OrderedGroup.abs_not_less_zero Ring_and_Field.abs_one Ring_and_Field.linorder_neqE_linordered_idom)
   1.326 +have 7: "(0\<Colon>'b\<Colon>linordered_idom) < (1\<Colon>'b\<Colon>linordered_idom)"
   1.327    by (metis 6 Ring_and_Field.one_neq_zero)
   1.328 -have 8: "\<bar>1\<Colon>'b\<Colon>ordered_idom\<bar> = (1\<Colon>'b\<Colon>ordered_idom)"
   1.329 +have 8: "\<bar>1\<Colon>'b\<Colon>linordered_idom\<bar> = (1\<Colon>'b\<Colon>linordered_idom)"
   1.330    by (metis OrderedGroup.abs_of_pos 7)
   1.331 -have 9: "\<And>X1\<Colon>'b\<Colon>ordered_idom. (0\<Colon>'b\<Colon>ordered_idom) \<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>X1\<bar>"
   1.332 +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>"
   1.333    by (metis OrderedGroup.abs_ge_zero 5)
   1.334 -have 10: "\<And>X1\<Colon>'b\<Colon>ordered_idom. X1 * (1\<Colon>'b\<Colon>ordered_idom) = X1"
   1.335 +have 10: "\<And>X1\<Colon>'b\<Colon>linordered_idom. X1 * (1\<Colon>'b\<Colon>linordered_idom) = X1"
   1.336    by (metis Ring_and_Field.mult_cancel_right2 mult_commute)
   1.337 -have 11: "\<And>X1\<Colon>'b\<Colon>ordered_idom. \<bar>\<bar>X1\<bar>\<bar> = \<bar>X1\<bar> * \<bar>1\<Colon>'b\<Colon>ordered_idom\<bar>"
   1.338 +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>"
   1.339    by (metis Ring_and_Field.abs_mult OrderedGroup.abs_idempotent 10)
   1.340 -have 12: "\<And>X1\<Colon>'b\<Colon>ordered_idom. \<bar>\<bar>X1\<bar>\<bar> = \<bar>X1\<bar>"
   1.341 +have 12: "\<And>X1\<Colon>'b\<Colon>linordered_idom. \<bar>\<bar>X1\<bar>\<bar> = \<bar>X1\<bar>"
   1.342    by (metis 11 8 10)
   1.343 -have 13: "\<And>X1\<Colon>'b\<Colon>ordered_idom. (0\<Colon>'b\<Colon>ordered_idom) \<le> \<bar>X1\<bar>"
   1.344 +have 13: "\<And>X1\<Colon>'b\<Colon>linordered_idom. (0\<Colon>'b\<Colon>linordered_idom) \<le> \<bar>X1\<bar>"
   1.345    by (metis OrderedGroup.abs_ge_zero 12)
   1.346 -have 14: "\<not> (0\<Colon>'b\<Colon>ordered_idom)
   1.347 -  \<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x\<Colon>'a)\<bar> \<or>
   1.348 -\<not> (0\<Colon>'b\<Colon>ordered_idom) \<le> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar> \<or>
   1.349 -\<not> \<bar>b x\<bar> \<le> (ca\<Colon>'b\<Colon>ordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar> \<or>
   1.350 -\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar> \<le> c * \<bar>f x\<bar>"
   1.351 +have 14: "\<not> (0\<Colon>'b\<Colon>linordered_idom)
   1.352 +  \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar> \<or>
   1.353 +\<not> (0\<Colon>'b\<Colon>linordered_idom) \<le> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<or>
   1.354 +\<not> \<bar>b x\<bar> \<le> (ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<or>
   1.355 +\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<le> c * \<bar>f x\<bar>"
   1.356    by (metis 3 Ring_and_Field.mult_mono)
   1.357 -have 15: "\<not> (0\<Colon>'b\<Colon>ordered_idom) \<le> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x\<Colon>'a)\<bar> \<or>
   1.358 -\<not> \<bar>b x\<bar> \<le> (ca\<Colon>'b\<Colon>ordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar> \<or>
   1.359 -\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>
   1.360 -  \<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>"
   1.361 +have 15: "\<not> (0\<Colon>'b\<Colon>linordered_idom) \<le> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar> \<or>
   1.362 +\<not> \<bar>b x\<bar> \<le> (ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<or>
   1.363 +\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>
   1.364 +  \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>"
   1.365    by (metis 14 9)
   1.366 -have 16: "\<not> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x\<Colon>'a)\<bar>
   1.367 -  \<le> (ca\<Colon>'b\<Colon>ordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar> \<or>
   1.368 -\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>
   1.369 -  \<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>"
   1.370 +have 16: "\<not> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar>
   1.371 +  \<le> (ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<or>
   1.372 +\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>
   1.373 +  \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>"
   1.374    by (metis 15 13)
   1.375 -have 17: "\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x\<Colon>'a)\<bar>
   1.376 -  \<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>"
   1.377 +have 17: "\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar>
   1.378 +  \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>"
   1.379    by (metis 16 2)
   1.380  show 18: "False"
   1.381    by (metis 17 1)
   1.382 @@ -682,7 +682,7 @@
   1.383  
   1.384  
   1.385  lemma bigo_mult5: "ALL x. f x ~= 0 ==>
   1.386 -    O(f * g) <= (f::'a => ('b::ordered_field)) *o O(g)"
   1.387 +    O(f * g) <= (f::'a => ('b::linordered_field)) *o O(g)"
   1.388  proof -
   1.389    assume "ALL x. f x ~= 0"
   1.390    show "O(f * g) <= f *o O(g)"
   1.391 @@ -712,14 +712,14 @@
   1.392  
   1.393  declare [[ atp_problem_prefix = "BigO__bigo_mult6" ]]
   1.394  lemma bigo_mult6: "ALL x. f x ~= 0 ==>
   1.395 -    O(f * g) = (f::'a => ('b::ordered_field)) *o O(g)"
   1.396 +    O(f * g) = (f::'a => ('b::linordered_field)) *o O(g)"
   1.397  by (metis bigo_mult2 bigo_mult5 order_antisym)
   1.398  
   1.399  (*proof requires relaxing relevance: 2007-01-25*)
   1.400  declare [[ atp_problem_prefix = "BigO__bigo_mult7" ]]
   1.401    declare bigo_mult6 [simp]
   1.402  lemma bigo_mult7: "ALL x. f x ~= 0 ==>
   1.403 -    O(f * g) <= O(f::'a => ('b::ordered_field)) \<otimes> O(g)"
   1.404 +    O(f * g) <= O(f::'a => ('b::linordered_field)) \<otimes> O(g)"
   1.405  (*sledgehammer*)
   1.406    apply (subst bigo_mult6)
   1.407    apply assumption
   1.408 @@ -731,7 +731,7 @@
   1.409  declare [[ atp_problem_prefix = "BigO__bigo_mult8" ]]
   1.410    declare bigo_mult7[intro!]
   1.411  lemma bigo_mult8: "ALL x. f x ~= 0 ==>
   1.412 -    O(f * g) = O(f::'a => ('b::ordered_field)) \<otimes> O(g)"
   1.413 +    O(f * g) = O(f::'a => ('b::linordered_field)) \<otimes> O(g)"
   1.414  by (metis bigo_mult bigo_mult7 order_antisym_conv)
   1.415  
   1.416  lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)"
   1.417 @@ -810,11 +810,11 @@
   1.418  lemma (*bigo_const2 [intro]:*) "O(%x. c) <= O(%x. 1)"
   1.419  by (metis bigo_const1 bigo_elt_subset);
   1.420  
   1.421 -lemma bigo_const2 [intro]: "O(%x. c::'b::ordered_idom) <= O(%x. 1)";
   1.422 +lemma bigo_const2 [intro]: "O(%x. c::'b::linordered_idom) <= O(%x. 1)";
   1.423  (*??FAILS because the two occurrences of COMBK have different polymorphic types
   1.424  proof (neg_clausify)
   1.425 -assume 0: "\<not> O(COMBK (c\<Colon>'b\<Colon>ordered_idom)) \<subseteq> O(COMBK (1\<Colon>'b\<Colon>ordered_idom))"
   1.426 -have 1: "COMBK (c\<Colon>'b\<Colon>ordered_idom) \<notin> O(COMBK (1\<Colon>'b\<Colon>ordered_idom))"
   1.427 +assume 0: "\<not> O(COMBK (c\<Colon>'b\<Colon>linordered_idom)) \<subseteq> O(COMBK (1\<Colon>'b\<Colon>linordered_idom))"
   1.428 +have 1: "COMBK (c\<Colon>'b\<Colon>linordered_idom) \<notin> O(COMBK (1\<Colon>'b\<Colon>linordered_idom))"
   1.429  apply (rule notI) 
   1.430  apply (rule 0 [THEN notE]) 
   1.431  apply (rule bigo_elt_subset) 
   1.432 @@ -830,26 +830,26 @@
   1.433  done
   1.434  
   1.435  declare [[ atp_problem_prefix = "BigO__bigo_const3" ]]
   1.436 -lemma bigo_const3: "(c::'a::ordered_field) ~= 0 ==> (%x. 1) : O(%x. c)"
   1.437 +lemma bigo_const3: "(c::'a::linordered_field) ~= 0 ==> (%x. 1) : O(%x. c)"
   1.438  apply (simp add: bigo_def)
   1.439  proof (neg_clausify)
   1.440 -assume 0: "(c\<Colon>'a\<Colon>ordered_field) \<noteq> (0\<Colon>'a\<Colon>ordered_field)"
   1.441 -assume 1: "\<And>A\<Colon>'a\<Colon>ordered_field. \<not> (1\<Colon>'a\<Colon>ordered_field) \<le> A * \<bar>c\<Colon>'a\<Colon>ordered_field\<bar>"
   1.442 -have 2: "(0\<Colon>'a\<Colon>ordered_field) = \<bar>c\<Colon>'a\<Colon>ordered_field\<bar> \<or>
   1.443 -\<not> (1\<Colon>'a\<Colon>ordered_field) \<le> (1\<Colon>'a\<Colon>ordered_field)"
   1.444 +assume 0: "(c\<Colon>'a\<Colon>linordered_field) \<noteq> (0\<Colon>'a\<Colon>linordered_field)"
   1.445 +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>"
   1.446 +have 2: "(0\<Colon>'a\<Colon>linordered_field) = \<bar>c\<Colon>'a\<Colon>linordered_field\<bar> \<or>
   1.447 +\<not> (1\<Colon>'a\<Colon>linordered_field) \<le> (1\<Colon>'a\<Colon>linordered_field)"
   1.448    by (metis 1 field_inverse)
   1.449 -have 3: "\<bar>c\<Colon>'a\<Colon>ordered_field\<bar> = (0\<Colon>'a\<Colon>ordered_field)"
   1.450 +have 3: "\<bar>c\<Colon>'a\<Colon>linordered_field\<bar> = (0\<Colon>'a\<Colon>linordered_field)"
   1.451    by (metis linorder_neq_iff linorder_antisym_conv1 2)
   1.452 -have 4: "(0\<Colon>'a\<Colon>ordered_field) = (c\<Colon>'a\<Colon>ordered_field)"
   1.453 +have 4: "(0\<Colon>'a\<Colon>linordered_field) = (c\<Colon>'a\<Colon>linordered_field)"
   1.454    by (metis 3 abs_eq_0)
   1.455  show "False"
   1.456    by (metis 0 4)
   1.457  qed
   1.458  
   1.459 -lemma bigo_const4: "(c::'a::ordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)"
   1.460 +lemma bigo_const4: "(c::'a::linordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)"
   1.461  by (rule bigo_elt_subset, rule bigo_const3, assumption)
   1.462  
   1.463 -lemma bigo_const [simp]: "(c::'a::ordered_field) ~= 0 ==> 
   1.464 +lemma bigo_const [simp]: "(c::'a::linordered_field) ~= 0 ==> 
   1.465      O(%x. c) = O(%x. 1)"
   1.466  by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption)
   1.467  
   1.468 @@ -858,9 +858,9 @@
   1.469    apply (simp add: bigo_def abs_mult)
   1.470  proof (neg_clausify)
   1.471  fix x
   1.472 -assume 0: "\<And>xa\<Colon>'b\<Colon>ordered_idom.
   1.473 -   \<not> \<bar>c\<Colon>'b\<Colon>ordered_idom\<bar> *
   1.474 -     \<bar>(f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a\<Colon>type) xa)\<bar>
   1.475 +assume 0: "\<And>xa\<Colon>'b\<Colon>linordered_idom.
   1.476 +   \<not> \<bar>c\<Colon>'b\<Colon>linordered_idom\<bar> *
   1.477 +     \<bar>(f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) ((x\<Colon>'b\<Colon>linordered_idom \<Rightarrow> 'a\<Colon>type) xa)\<bar>
   1.478       \<le> xa * \<bar>f (x xa)\<bar>"
   1.479  show "False"
   1.480    by (metis linorder_neq_iff linorder_antisym_conv1 0)
   1.481 @@ -870,7 +870,7 @@
   1.482  by (rule bigo_elt_subset, rule bigo_const_mult1)
   1.483  
   1.484  declare [[ atp_problem_prefix = "BigO__bigo_const_mult3" ]]
   1.485 -lemma bigo_const_mult3: "(c::'a::ordered_field) ~= 0 ==> f : O(%x. c * f x)"
   1.486 +lemma bigo_const_mult3: "(c::'a::linordered_field) ~= 0 ==> f : O(%x. c * f x)"
   1.487    apply (simp add: bigo_def)
   1.488  (*sledgehammer [no luck]*); 
   1.489    apply (rule_tac x = "abs(inverse c)" in exI)
   1.490 @@ -879,16 +879,16 @@
   1.491  apply (auto ); 
   1.492  done
   1.493  
   1.494 -lemma bigo_const_mult4: "(c::'a::ordered_field) ~= 0 ==> 
   1.495 +lemma bigo_const_mult4: "(c::'a::linordered_field) ~= 0 ==> 
   1.496      O(f) <= O(%x. c * f x)"
   1.497  by (rule bigo_elt_subset, rule bigo_const_mult3, assumption)
   1.498  
   1.499 -lemma bigo_const_mult [simp]: "(c::'a::ordered_field) ~= 0 ==> 
   1.500 +lemma bigo_const_mult [simp]: "(c::'a::linordered_field) ~= 0 ==> 
   1.501      O(%x. c * f x) = O(f)"
   1.502  by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4)
   1.503  
   1.504  declare [[ atp_problem_prefix = "BigO__bigo_const_mult5" ]]
   1.505 -lemma bigo_const_mult5 [simp]: "(c::'a::ordered_field) ~= 0 ==> 
   1.506 +lemma bigo_const_mult5 [simp]: "(c::'a::linordered_field) ~= 0 ==> 
   1.507      (%x. c) *o O(f) = O(f)"
   1.508    apply (auto del: subsetI)
   1.509    apply (rule order_trans)
   1.510 @@ -1057,7 +1057,7 @@
   1.511    apply assumption+
   1.512  done
   1.513    
   1.514 -lemma bigo_useful_const_mult: "(c::'a::ordered_field) ~= 0 ==> 
   1.515 +lemma bigo_useful_const_mult: "(c::'a::linordered_field) ~= 0 ==> 
   1.516      (%x. c) * f =o O(h) ==> f =o O(h)"
   1.517    apply (rule subsetD)
   1.518    apply (subgoal_tac "(%x. 1 / c) *o O(h) <= O(h)")
   1.519 @@ -1100,7 +1100,7 @@
   1.520  subsection {* Less than or equal to *}
   1.521  
   1.522  constdefs 
   1.523 -  lesso :: "('a => 'b::ordered_idom) => ('a => 'b) => ('a => 'b)"
   1.524 +  lesso :: "('a => 'b::linordered_idom) => ('a => 'b) => ('a => 'b)"
   1.525        (infixl "<o" 70)
   1.526    "f <o g == (%x. max (f x - g x) 0)"
   1.527  
   1.528 @@ -1165,7 +1165,7 @@
   1.529  proof (neg_clausify)
   1.530  fix x
   1.531  assume 0: "\<And>A. k A \<le> f A"
   1.532 -have 1: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X2. \<not> max X1 X2 < X1"
   1.533 +have 1: "\<And>(X1\<Colon>'b\<Colon>linordered_idom) X2. \<not> max X1 X2 < X1"
   1.534    by (metis linorder_not_less le_maxI1)  (*sort inserted by hand*)
   1.535  assume 2: "(0\<Colon>'b) \<le> k x - g x"
   1.536  have 3: "\<not> k x - g x < (0\<Colon>'b)"
   1.537 @@ -1206,7 +1206,7 @@
   1.538  apply (metis abs_ge_zero linorder_linear min_max.sup_absorb1 min_max.sup_commute)
   1.539  done
   1.540  
   1.541 -lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::ordered_field) ==>
   1.542 +lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::linordered_field) ==>
   1.543      g =o h +o O(k) ==> f <o h =o O(k)"
   1.544    apply (unfold lesso_def)
   1.545    apply (drule set_plus_imp_minus)