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