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