src/HOL/Matrix/LP.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 23477 f4b83f03cac9
child 29667 53103fc8ffa3
permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:      HOL/Matrix/LP.thy
     2     ID:         $Id$
     3     Author:     Steven Obua
     4 *)
     5 
     6 theory LP 
     7 imports Main
     8 begin
     9 
    10 lemma linprog_dual_estimate:
    11   assumes
    12   "A * x \<le> (b::'a::lordered_ring)"
    13   "0 \<le> y"
    14   "abs (A - A') \<le> \<delta>A"
    15   "b \<le> b'"
    16   "abs (c - c') \<le> \<delta>c"
    17   "abs x \<le> r"
    18   shows
    19   "c * x \<le> y * b' + (y * \<delta>A + abs (y * A' - c') + \<delta>c) * r"
    20 proof -
    21   from prems have 1: "y * b <= y * b'" by (simp add: mult_left_mono)
    22   from prems have 2: "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
    23   have 3: "y * (A * x) = c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x" by (simp add: ring_simps)  
    24   from 1 2 3 have 4: "c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x <= y * b'" by simp
    25   have 5: "c * x <= y * b' + abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"
    26     by (simp only: 4 estimate_by_abs)  
    27   have 6: "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <= abs (y * (A - A') + (y * A' - c') + (c'-c)) * abs x"
    28     by (simp add: abs_le_mult)
    29   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"
    30     by(rule abs_triangle_ineq [THEN mult_right_mono]) simp
    31   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"
    32     by (simp add: abs_triangle_ineq mult_right_mono)    
    33   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"
    34     by (simp add: abs_le_mult mult_right_mono)  
    35   have 10: "c'-c = -(c-c')" by (simp add: ring_simps)
    36   have 11: "abs (c'-c) = abs (c-c')" 
    37     by (subst 10, subst abs_minus_cancel, simp)
    38   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"
    39     by (simp add: 11 prems mult_right_mono)
    40   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"
    41     by (simp add: prems mult_right_mono mult_left_mono)  
    42   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"
    43     apply (rule mult_left_mono)
    44     apply (simp add: prems)
    45     apply (rule_tac add_mono[of "0::'a" _ "0", simplified])+
    46     apply (rule mult_left_mono[of "0" "\<delta>A", simplified])
    47     apply (simp_all)
    48     apply (rule order_trans[where y="abs (A-A')"], simp_all add: prems)
    49     apply (rule order_trans[where y="abs (c-c')"], simp_all add: prems)
    50     done    
    51   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"     
    52     by (simp)
    53   show ?thesis 
    54     apply (rule_tac le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
    55     apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified prems]])
    56     done
    57 qed
    58 
    59 lemma le_ge_imp_abs_diff_1:
    60   assumes
    61   "A1 <= (A::'a::lordered_ring)"
    62   "A <= A2" 
    63   shows "abs (A-A1) <= A2-A1"
    64 proof -
    65   have "0 <= A - A1"    
    66   proof -
    67     have 1: "A - A1 = A + (- A1)" by simp
    68     show ?thesis by (simp only: 1 add_right_mono[of A1 A "-A1", simplified, simplified prems])
    69   qed
    70   then have "abs (A-A1) = A-A1" by (rule abs_of_nonneg)
    71   with prems show "abs (A-A1) <= (A2-A1)" by simp
    72 qed
    73 
    74 lemma mult_le_prts:
    75   assumes
    76   "a1 <= (a::'a::lordered_ring)"
    77   "a <= a2"
    78   "b1 <= b"
    79   "b <= b2"
    80   shows
    81   "a * b <= pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1"
    82 proof - 
    83   have "a * b = (pprt a + nprt a) * (pprt b + nprt b)" 
    84     apply (subst prts[symmetric])+
    85     apply simp
    86     done
    87   then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
    88     by (simp add: ring_simps)
    89   moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
    90     by (simp_all add: prems mult_mono)
    91   moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
    92   proof -
    93     have "pprt a * nprt b <= pprt a * nprt b2"
    94       by (simp add: mult_left_mono prems)
    95     moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
    96       by (simp add: mult_right_mono_neg prems)
    97     ultimately show ?thesis
    98       by simp
    99   qed
   100   moreover have "nprt a * pprt b <= nprt a2 * pprt b1"
   101   proof - 
   102     have "nprt a * pprt b <= nprt a2 * pprt b"
   103       by (simp add: mult_right_mono prems)
   104     moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
   105       by (simp add: mult_left_mono_neg prems)
   106     ultimately show ?thesis
   107       by simp
   108   qed
   109   moreover have "nprt a * nprt b <= nprt a1 * nprt b1"
   110   proof -
   111     have "nprt a * nprt b <= nprt a * nprt b1"
   112       by (simp add: mult_left_mono_neg prems)
   113     moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
   114       by (simp add: mult_right_mono_neg prems)
   115     ultimately show ?thesis
   116       by simp
   117   qed
   118   ultimately show ?thesis
   119     by - (rule add_mono | simp)+
   120 qed
   121     
   122 lemma mult_le_dual_prts: 
   123   assumes
   124   "A * x \<le> (b::'a::lordered_ring)"
   125   "0 \<le> y"
   126   "A1 \<le> A"
   127   "A \<le> A2"
   128   "c1 \<le> c"
   129   "c \<le> c2"
   130   "r1 \<le> x"
   131   "x \<le> r2"
   132   shows
   133   "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)"
   134   (is "_ <= _ + ?C")
   135 proof -
   136   from prems have "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
   137   moreover have "y * (A * x) = c * x + (y * A - c) * x" by (simp add: ring_simps)  
   138   ultimately have "c * x + (y * A - c) * x <= y * b" by simp
   139   then have "c * x <= y * b - (y * A - c) * x" by (simp add: le_diff_eq)
   140   then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: ring_simps)
   141   have s2: "c - y * A <= c2 - y * A1"
   142     by (simp add: diff_def prems add_mono mult_left_mono)
   143   have s1: "c1 - y * A2 <= c - y * A"
   144     by (simp add: diff_def prems add_mono mult_left_mono)
   145   have prts: "(c - y * A) * x <= ?C"
   146     apply (simp add: Let_def)
   147     apply (rule mult_le_prts)
   148     apply (simp_all add: prems s1 s2)
   149     done
   150   then have "y * b + (c - y * A) * x <= y * b + ?C"
   151     by simp
   152   with cx show ?thesis
   153     by(simp only:)
   154 qed
   155 
   156 end