src/HOL/Ring_and_Field.thy
changeset 19404 9bf2cdc9e8e8
parent 18649 bb99c2e705ca
child 20496 23eb6034c06d
     1.1 --- a/src/HOL/Ring_and_Field.thy	Mon Apr 10 14:37:23 2006 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Mon Apr 10 16:00:34 2006 +0200
     1.3 @@ -1932,71 +1932,7 @@
     1.4    apply (simp add: order_less_imp_le);
     1.5  done;
     1.6  
     1.7 -subsection {* Miscellaneous *}
     1.8 -
     1.9 -lemma linprog_dual_estimate:
    1.10 -  assumes
    1.11 -  "A * x \<le> (b::'a::lordered_ring)"
    1.12 -  "0 \<le> y"
    1.13 -  "abs (A - A') \<le> \<delta>A"
    1.14 -  "b \<le> b'"
    1.15 -  "abs (c - c') \<le> \<delta>c"
    1.16 -  "abs x \<le> r"
    1.17 -  shows
    1.18 -  "c * x \<le> y * b' + (y * \<delta>A + abs (y * A' - c') + \<delta>c) * r"
    1.19 -proof -
    1.20 -  from prems have 1: "y * b <= y * b'" by (simp add: mult_left_mono)
    1.21 -  from prems have 2: "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
    1.22 -  have 3: "y * (A * x) = c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x" by (simp add: ring_eq_simps)  
    1.23 -  from 1 2 3 have 4: "c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x <= y * b'" by simp
    1.24 -  have 5: "c * x <= y * b' + abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"
    1.25 -    by (simp only: 4 estimate_by_abs)  
    1.26 -  have 6: "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <= abs (y * (A - A') + (y * A' - c') + (c'-c)) * abs x"
    1.27 -    by (simp add: abs_le_mult)
    1.28 -  have 7: "(abs (y * (A - A') + (y * A' - c') + (c'-c))) * abs x <= (abs (y * (A-A') + (y*A'-c')) + abs(c'-c)) * abs x"
    1.29 -    by(rule abs_triangle_ineq [THEN mult_right_mono]) simp
    1.30 -  have 8: " (abs (y * (A-A') + (y*A'-c')) + abs(c'-c)) * abs x <=  (abs (y * (A-A')) + abs (y*A'-c') + abs(c'-c)) * abs x"
    1.31 -    by (simp add: abs_triangle_ineq mult_right_mono)    
    1.32 -  have 9: "(abs (y * (A-A')) + abs (y*A'-c') + abs(c'-c)) * abs x <= (abs y * abs (A-A') + abs (y*A'-c') + abs (c'-c)) * abs x"
    1.33 -    by (simp add: abs_le_mult mult_right_mono)  
    1.34 -  have 10: "c'-c = -(c-c')" by (simp add: ring_eq_simps)
    1.35 -  have 11: "abs (c'-c) = abs (c-c')" 
    1.36 -    by (subst 10, subst abs_minus_cancel, simp)
    1.37 -  have 12: "(abs y * abs (A-A') + abs (y*A'-c') + abs (c'-c)) * abs x <= (abs y * abs (A-A') + abs (y*A'-c') + \<delta>c) * abs x"
    1.38 -    by (simp add: 11 prems mult_right_mono)
    1.39 -  have 13: "(abs y * abs (A-A') + abs (y*A'-c') + \<delta>c) * abs x <= (abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * abs x"
    1.40 -    by (simp add: prems mult_right_mono mult_left_mono)  
    1.41 -  have r: "(abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * abs x <=  (abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * r"
    1.42 -    apply (rule mult_left_mono)
    1.43 -    apply (simp add: prems)
    1.44 -    apply (rule_tac add_mono[of "0::'a" _ "0", simplified])+
    1.45 -    apply (rule mult_left_mono[of "0" "\<delta>A", simplified])
    1.46 -    apply (simp_all)
    1.47 -    apply (rule order_trans[where y="abs (A-A')"], simp_all add: prems)
    1.48 -    apply (rule order_trans[where y="abs (c-c')"], simp_all add: prems)
    1.49 -    done    
    1.50 -  from 6 7 8 9 12 13 r have 14:" abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <=(abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * r"     
    1.51 -    by (simp)
    1.52 -  show ?thesis 
    1.53 -    apply (rule_tac le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
    1.54 -    apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified prems]])
    1.55 -    done
    1.56 -qed
    1.57 -
    1.58 -lemma le_ge_imp_abs_diff_1:
    1.59 -  assumes
    1.60 -  "A1 <= (A::'a::lordered_ring)"
    1.61 -  "A <= A2" 
    1.62 -  shows "abs (A-A1) <= A2-A1"
    1.63 -proof -
    1.64 -  have "0 <= A - A1"    
    1.65 -  proof -
    1.66 -    have 1: "A - A1 = A + (- A1)" by simp
    1.67 -    show ?thesis by (simp only: 1 add_right_mono[of A1 A "-A1", simplified, simplified prems])
    1.68 -  qed
    1.69 -  then have "abs (A-A1) = A-A1" by (rule abs_of_nonneg)
    1.70 -  with prems show "abs (A-A1) <= (A2-A1)" by simp
    1.71 -qed
    1.72 +subsection {* Bounds of products via negative and positive Part *}
    1.73  
    1.74  lemma mult_le_prts:
    1.75    assumes
    1.76 @@ -2045,39 +1981,23 @@
    1.77    ultimately show ?thesis
    1.78      by - (rule add_mono | simp)+
    1.79  qed
    1.80 -    
    1.81 -lemma mult_le_dual_prts: 
    1.82 +
    1.83 +lemma mult_ge_prts:
    1.84    assumes
    1.85 -  "A * x \<le> (b::'a::lordered_ring)"
    1.86 -  "0 \<le> y"
    1.87 -  "A1 \<le> A"
    1.88 -  "A \<le> A2"
    1.89 -  "c1 \<le> c"
    1.90 -  "c \<le> c2"
    1.91 -  "r1 \<le> x"
    1.92 -  "x \<le> r2"
    1.93 +  "a1 <= (a::'a::lordered_ring)"
    1.94 +  "a <= a2"
    1.95 +  "b1 <= b"
    1.96 +  "b <= b2"
    1.97    shows
    1.98 -  "c * x \<le> y * b + (let s1 = c1 - y * A2; s2 = c2 - y * A1 in pprt s2 * pprt r2 + pprt s1 * nprt r2 + nprt s2 * pprt r1 + nprt s1 * nprt r1)"
    1.99 -  (is "_ <= _ + ?C")
   1.100 -proof -
   1.101 -  from prems have "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
   1.102 -  moreover have "y * (A * x) = c * x + (y * A - c) * x" by (simp add: ring_eq_simps)  
   1.103 -  ultimately have "c * x + (y * A - c) * x <= y * b" by simp
   1.104 -  then have "c * x <= y * b - (y * A - c) * x" by (simp add: le_diff_eq)
   1.105 -  then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: ring_eq_simps)
   1.106 -  have s2: "c - y * A <= c2 - y * A1"
   1.107 -    by (simp add: diff_def prems add_mono mult_left_mono)
   1.108 -  have s1: "c1 - y * A2 <= c - y * A"
   1.109 -    by (simp add: diff_def prems add_mono mult_left_mono)
   1.110 -  have prts: "(c - y * A) * x <= ?C"
   1.111 -    apply (simp add: Let_def)
   1.112 -    apply (rule mult_le_prts)
   1.113 -    apply (simp_all add: prems s1 s2)
   1.114 -    done
   1.115 -  then have "y * b + (c - y * A) * x <= y * b + ?C"
   1.116 -    by simp
   1.117 -  with cx show ?thesis
   1.118 -    by(simp only:)
   1.119 +  "a * b >= nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1"
   1.120 +proof - 
   1.121 +  from prems have a1:"- a2 <= -a" by auto
   1.122 +  from prems have a2: "-a <= -a1" by auto
   1.123 +  from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 prems(3) prems(4), simplified nprt_neg pprt_neg] 
   1.124 +  have le: "- (a * b) <= - nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1" by simp  
   1.125 +  then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"
   1.126 +    by (simp only: minus_le_iff)
   1.127 +  then show ?thesis by simp
   1.128  qed
   1.129  
   1.130  ML {*