src/HOL/Matrix_LP/LP.thy
 author blanchet Tue Nov 07 15:16:42 2017 +0100 (21 months ago) changeset 67022 49309fe530fd parent 66453 cc19f7ca2ed6 permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
```     1 (*  Title:      HOL/Matrix_LP/LP.thy
```
```     2     Author:     Steven Obua
```
```     3 *)
```
```     4
```
```     5 theory LP
```
```     6 imports Main "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   "\<bar>A - A'\<bar> \<le> \<delta>_A"
```
```    23   "b \<le> b'"
```
```    24   "\<bar>c - c'\<bar> \<le> \<delta>_c"
```
```    25   "\<bar>x\<bar> \<le> r"
```
```    26   shows
```
```    27   "c * x \<le> y * b' + (y * \<delta>_A + \<bar>y * A' - c'\<bar> + \<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' + \<bar>(y * (A - A') + (y * A' - c') + (c'-c)) * x\<bar>"
```
```    34     by (simp only: 4 estimate_by_abs)
```
```    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>"
```
```    36     by (simp add: abs_le_mult)
```
```    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>"
```
```    38     by(rule abs_triangle_ineq [THEN mult_right_mono]) simp
```
```    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>"
```
```    40     by (simp add: abs_triangle_ineq mult_right_mono)
```
```    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>"
```
```    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: "\<bar>c'-c\<bar> = \<bar>c-c'\<bar>"
```
```    45     by (subst 10, subst abs_minus_cancel, simp)
```
```    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>"
```
```    47     by (simp add: 11 assms mult_right_mono)
```
```    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>"
```
```    49     by (simp add: assms mult_right_mono mult_left_mono)
```
```    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"
```
```    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="\<bar>A-A'\<bar>"], simp_all add: assms)
```
```    57     apply (rule order_trans[where y="\<bar>c-c'\<bar>"], simp_all add: assms)
```
```    58     done
```
```    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"
```
```    60     by (simp)
```
```    61   show ?thesis
```
```    62     apply (rule le_add_right_mono[of _ _ "\<bar>(y * (A - A') + (y * A' - c') + (c'-c)) * x\<bar>"])
```
```    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 "\<bar>A-A1\<bar> <= 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 "\<bar>A-A1\<bar> = A-A1" by (rule abs_of_nonneg)
```
```    78   with assms show "\<bar>A-A1\<bar> <= (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
```