src/HOL/Matrix_LP/LP.thy
author wenzelm
Wed, 26 Oct 2016 15:14:17 +0200
changeset 64406 492de9062cd2
parent 62390 842917225d56
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
more specific hardware information: relevant for ultimate Mac OS X version;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47455
26315a545e26 updated headers;
wenzelm
parents: 46988
diff changeset
     1
(*  Title:      HOL/Matrix_LP/LP.thy
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
     2
    Author:     Steven Obua
e4f382a270ad added LP.thy
obua
parents:
diff changeset
     3
*)
e4f382a270ad added LP.thy
obua
parents:
diff changeset
     4
e4f382a270ad added LP.thy
obua
parents:
diff changeset
     5
theory LP 
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 37884
diff changeset
     6
imports Main "~~/src/HOL/Library/Lattice_Algebras"
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
     7
begin
e4f382a270ad added LP.thy
obua
parents:
diff changeset
     8
37884
314a88278715 discontinued pretending that abel_cancel is logic-independent; cleaned up junk
haftmann
parents: 35032
diff changeset
     9
lemma le_add_right_mono: 
314a88278715 discontinued pretending that abel_cancel is logic-independent; cleaned up junk
haftmann
parents: 35032
diff changeset
    10
  assumes 
314a88278715 discontinued pretending that abel_cancel is logic-independent; cleaned up junk
haftmann
parents: 35032
diff changeset
    11
  "a <= b + (c::'a::ordered_ab_group_add)"
314a88278715 discontinued pretending that abel_cancel is logic-independent; cleaned up junk
haftmann
parents: 35032
diff changeset
    12
  "c <= d"    
314a88278715 discontinued pretending that abel_cancel is logic-independent; cleaned up junk
haftmann
parents: 35032
diff changeset
    13
  shows "a <= b + d"
314a88278715 discontinued pretending that abel_cancel is logic-independent; cleaned up junk
haftmann
parents: 35032
diff changeset
    14
  apply (rule_tac order_trans[where y = "b+c"])
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 41413
diff changeset
    15
  apply (simp_all add: assms)
37884
314a88278715 discontinued pretending that abel_cancel is logic-independent; cleaned up junk
haftmann
parents: 35032
diff changeset
    16
  done
314a88278715 discontinued pretending that abel_cancel is logic-independent; cleaned up junk
haftmann
parents: 35032
diff changeset
    17
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    18
lemma linprog_dual_estimate:
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    19
  assumes
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 32491
diff changeset
    20
  "A * x \<le> (b::'a::lattice_ring)"
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    21
  "0 \<le> y"
61945
1135b8de26c3 more symbols;
wenzelm
parents: 54230
diff changeset
    22
  "\<bar>A - A'\<bar> \<le> \<delta>_A"
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    23
  "b \<le> b'"
61945
1135b8de26c3 more symbols;
wenzelm
parents: 54230
diff changeset
    24
  "\<bar>c - c'\<bar> \<le> \<delta>_c"
1135b8de26c3 more symbols;
wenzelm
parents: 54230
diff changeset
    25
  "\<bar>x\<bar> \<le> r"
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    26
  shows
61945
1135b8de26c3 more symbols;
wenzelm
parents: 54230
diff changeset
    27
  "c * x \<le> y * b' + (y * \<delta>_A + \<bar>y * A' - c'\<bar> + \<delta>_c) * r"
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    28
proof -
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 41413
diff changeset
    29
  from assms have 1: "y * b <= y * b'" by (simp add: mult_left_mono)
efa734d9b221 eliminated global prems;
wenzelm
parents: 41413
diff changeset
    30
  from assms have 2: "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 23477
diff changeset
    31
  have 3: "y * (A * x) = c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x" by (simp add: algebra_simps)  
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    32
  from 1 2 3 have 4: "c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x <= y * b'" by simp
61945
1135b8de26c3 more symbols;
wenzelm
parents: 54230
diff changeset
    33
  have 5: "c * x <= y * b' + \<bar>(y * (A - A') + (y * A' - c') + (c'-c)) * x\<bar>"
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    34
    by (simp only: 4 estimate_by_abs)  
61945
1135b8de26c3 more symbols;
wenzelm
parents: 54230
diff changeset
    35
  have 6: "\<bar>(y * (A - A') + (y * A' - c') + (c'-c)) * x\<bar> <= \<bar>y * (A - A') + (y * A' - c') + (c'-c)\<bar> * \<bar>x\<bar>"
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    36
    by (simp add: abs_le_mult)
61945
1135b8de26c3 more symbols;
wenzelm
parents: 54230
diff changeset
    37
  have 7: "(\<bar>y * (A - A') + (y * A' - c') + (c'-c)\<bar>) * \<bar>x\<bar> <= (\<bar>y * (A-A') + (y*A'-c')\<bar> + \<bar>c' - c\<bar>) * \<bar>x\<bar>"
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    38
    by(rule abs_triangle_ineq [THEN mult_right_mono]) simp
61945
1135b8de26c3 more symbols;
wenzelm
parents: 54230
diff changeset
    39
  have 8: "(\<bar>y * (A-A') + (y*A'-c')\<bar> + \<bar>c' - c\<bar>) * \<bar>x\<bar> <= (\<bar>y * (A-A')\<bar> + \<bar>y*A'-c'\<bar> + \<bar>c' - c\<bar>) * \<bar>x\<bar>"
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    40
    by (simp add: abs_triangle_ineq mult_right_mono)    
61945
1135b8de26c3 more symbols;
wenzelm
parents: 54230
diff changeset
    41
  have 9: "(\<bar>y * (A-A')\<bar> + \<bar>y*A'-c'\<bar> + \<bar>c'-c\<bar>) * \<bar>x\<bar> <= (\<bar>y\<bar> * \<bar>A-A'\<bar> + \<bar>y*A'-c'\<bar> + \<bar>c'-c\<bar>) * \<bar>x\<bar>"
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    42
    by (simp add: abs_le_mult mult_right_mono)  
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 23477
diff changeset
    43
  have 10: "c'-c = -(c-c')" by (simp add: algebra_simps)
61945
1135b8de26c3 more symbols;
wenzelm
parents: 54230
diff changeset
    44
  have 11: "\<bar>c'-c\<bar> = \<bar>c-c'\<bar>"
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    45
    by (subst 10, subst abs_minus_cancel, simp)
61945
1135b8de26c3 more symbols;
wenzelm
parents: 54230
diff changeset
    46
  have 12: "(\<bar>y\<bar> * \<bar>A-A'\<bar> + \<bar>y*A'-c'\<bar> + \<bar>c'-c\<bar>) * \<bar>x\<bar> <= (\<bar>y\<bar> * \<bar>A-A'\<bar> + \<bar>y*A'-c'\<bar> + \<delta>_c) * \<bar>x\<bar>"
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 41413
diff changeset
    47
    by (simp add: 11 assms mult_right_mono)
61945
1135b8de26c3 more symbols;
wenzelm
parents: 54230
diff changeset
    48
  have 13: "(\<bar>y\<bar> * \<bar>A-A'\<bar> + \<bar>y*A'-c'\<bar> + \<delta>_c) * \<bar>x\<bar> <= (\<bar>y\<bar> * \<delta>_A + \<bar>y*A'-c'\<bar> + \<delta>_c) * \<bar>x\<bar>"
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 41413
diff changeset
    49
    by (simp add: assms mult_right_mono mult_left_mono)  
61945
1135b8de26c3 more symbols;
wenzelm
parents: 54230
diff changeset
    50
  have r: "(\<bar>y\<bar> * \<delta>_A + \<bar>y*A'-c'\<bar> + \<delta>_c) * \<bar>x\<bar> <= (\<bar>y\<bar> * \<delta>_A + \<bar>y*A'-c'\<bar> + \<delta>_c) * r"
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    51
    apply (rule mult_left_mono)
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 41413
diff changeset
    52
    apply (simp add: assms)
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    53
    apply (rule_tac add_mono[of "0::'a" _ "0", simplified])+
50252
4aa34bd43228 eliminated slightly odd identifiers;
wenzelm
parents: 47455
diff changeset
    54
    apply (rule mult_left_mono[of "0" "\<delta>_A", simplified])
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    55
    apply (simp_all)
61945
1135b8de26c3 more symbols;
wenzelm
parents: 54230
diff changeset
    56
    apply (rule order_trans[where y="\<bar>A-A'\<bar>"], simp_all add: assms)
1135b8de26c3 more symbols;
wenzelm
parents: 54230
diff changeset
    57
    apply (rule order_trans[where y="\<bar>c-c'\<bar>"], simp_all add: assms)
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    58
    done    
61945
1135b8de26c3 more symbols;
wenzelm
parents: 54230
diff changeset
    59
  from 6 7 8 9 12 13 r have 14: "\<bar>(y * (A - A') + (y * A' - c') + (c'-c)) * x\<bar> <= (\<bar>y\<bar> * \<delta>_A + \<bar>y*A'-c'\<bar> + \<delta>_c) * r"
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    60
    by (simp)
37884
314a88278715 discontinued pretending that abel_cancel is logic-independent; cleaned up junk
haftmann
parents: 35032
diff changeset
    61
  show ?thesis
61945
1135b8de26c3 more symbols;
wenzelm
parents: 54230
diff changeset
    62
    apply (rule le_add_right_mono[of _ _ "\<bar>(y * (A - A') + (y * A' - c') + (c'-c)) * x\<bar>"])
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 41413
diff changeset
    63
    apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified assms]])
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    64
    done
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    65
qed
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    66
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    67
lemma le_ge_imp_abs_diff_1:
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    68
  assumes
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 32491
diff changeset
    69
  "A1 <= (A::'a::lattice_ring)"
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    70
  "A <= A2" 
61945
1135b8de26c3 more symbols;
wenzelm
parents: 54230
diff changeset
    71
  shows "\<bar>A-A1\<bar> <= A2-A1"
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    72
proof -
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    73
  have "0 <= A - A1"    
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    74
  proof -
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 50252
diff changeset
    75
    from assms add_right_mono [of A1 A "- A1"] show ?thesis by simp
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    76
  qed
61945
1135b8de26c3 more symbols;
wenzelm
parents: 54230
diff changeset
    77
  then have "\<bar>A-A1\<bar> = A-A1" by (rule abs_of_nonneg)
1135b8de26c3 more symbols;
wenzelm
parents: 54230
diff changeset
    78
  with assms show "\<bar>A-A1\<bar> <= (A2-A1)" by simp
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    79
qed
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    80
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    81
lemma mult_le_prts:
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    82
  assumes
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 32491
diff changeset
    83
  "a1 <= (a::'a::lattice_ring)"
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    84
  "a <= a2"
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    85
  "b1 <= b"
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    86
  "b <= b2"
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    87
  shows
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    88
  "a * b <= pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1"
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    89
proof - 
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    90
  have "a * b = (pprt a + nprt a) * (pprt b + nprt b)" 
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    91
    apply (subst prts[symmetric])+
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    92
    apply simp
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    93
    done
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    94
  then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 23477
diff changeset
    95
    by (simp add: algebra_simps)
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    96
  moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 41413
diff changeset
    97
    by (simp_all add: assms mult_mono)
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    98
  moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
e4f382a270ad added LP.thy
obua
parents:
diff changeset
    99
  proof -
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   100
    have "pprt a * nprt b <= pprt a * nprt b2"
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 41413
diff changeset
   101
      by (simp add: mult_left_mono assms)
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   102
    moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 41413
diff changeset
   103
      by (simp add: mult_right_mono_neg assms)
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   104
    ultimately show ?thesis
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   105
      by simp
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   106
  qed
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   107
  moreover have "nprt a * pprt b <= nprt a2 * pprt b1"
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   108
  proof - 
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   109
    have "nprt a * pprt b <= nprt a2 * pprt b"
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 41413
diff changeset
   110
      by (simp add: mult_right_mono assms)
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   111
    moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 41413
diff changeset
   112
      by (simp add: mult_left_mono_neg assms)
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   113
    ultimately show ?thesis
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   114
      by simp
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   115
  qed
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   116
  moreover have "nprt a * nprt b <= nprt a1 * nprt b1"
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   117
  proof -
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   118
    have "nprt a * nprt b <= nprt a * nprt b1"
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 41413
diff changeset
   119
      by (simp add: mult_left_mono_neg assms)
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   120
    moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 41413
diff changeset
   121
      by (simp add: mult_right_mono_neg assms)
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   122
    ultimately show ?thesis
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   123
      by simp
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   124
  qed
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   125
  ultimately show ?thesis
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   126
    by - (rule add_mono | simp)+
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   127
qed
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   128
    
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   129
lemma mult_le_dual_prts: 
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   130
  assumes
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 32491
diff changeset
   131
  "A * x \<le> (b::'a::lattice_ring)"
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   132
  "0 \<le> y"
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   133
  "A1 \<le> A"
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   134
  "A \<le> A2"
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   135
  "c1 \<le> c"
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   136
  "c \<le> c2"
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   137
  "r1 \<le> x"
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   138
  "x \<le> r2"
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   139
  shows
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   140
  "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)"
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   141
  (is "_ <= _ + ?C")
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   142
proof -
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 41413
diff changeset
   143
  from assms have "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 23477
diff changeset
   144
  moreover have "y * (A * x) = c * x + (y * A - c) * x" by (simp add: algebra_simps)  
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   145
  ultimately have "c * x + (y * A - c) * x <= y * b" by simp
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   146
  then have "c * x <= y * b - (y * A - c) * x" by (simp add: le_diff_eq)
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 23477
diff changeset
   147
  then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: algebra_simps)
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   148
  have s2: "c - y * A <= c2 - y * A1"
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 50252
diff changeset
   149
    by (simp add: assms add_mono mult_left_mono algebra_simps)
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   150
  have s1: "c1 - y * A2 <= c - y * A"
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 50252
diff changeset
   151
    by (simp add: assms add_mono mult_left_mono algebra_simps)
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   152
  have prts: "(c - y * A) * x <= ?C"
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   153
    apply (simp add: Let_def)
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   154
    apply (rule mult_le_prts)
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 41413
diff changeset
   155
    apply (simp_all add: assms s1 s2)
19453
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   156
    done
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   157
  then have "y * b + (c - y * A) * x <= y * b + ?C"
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   158
    by simp
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   159
  with cx show ?thesis
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   160
    by(simp only:)
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   161
qed
e4f382a270ad added LP.thy
obua
parents:
diff changeset
   162
62390
842917225d56 more canonical names
nipkow
parents: 61945
diff changeset
   163
end