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