src/HOL/Matrix/LinProg.thy

first version of matrices for HOL/Isabelle

(*  Title:      HOL/Matrix/LinProg.thy
    ID:         $Id$
    Author:     Steven Obua
    License:    2004 Technische Universität München
*)

theory LinProg = Matrix:

lemma linprog_by_duality_approx_general:
  assumes
  fmuladdprops:
  "! a b c d. a <= b & c <= d \<longrightarrow> fadd a c <= fadd b d"
  "! c a b. 0 <= c & a <= b \<longrightarrow> fmul c a <= fmul c b"
  "! a. fmul 0 a = 0"  
  "! a. fmul a 0 = 0"
  "fadd 0 0 = 0" 
  "associative fadd"
  "commutative fadd"
  "associative fmul"
  "distributive fmul fadd"
  and specificprops:
  "mult_matrix fmul fadd (combine_matrix fadd A dA) x <= (b::('a::{order, zero}) matrix)"
  "mult_matrix fmul fadd y A = c"
  "0 <= y"
  shows
  "combine_matrix fadd (mult_matrix fmul fadd c x) (mult_matrix fmul fadd (mult_matrix fmul fadd y dA) x) 
  <= mult_matrix fmul fadd y b"
proof -
  let ?mul = "mult_matrix fmul fadd"
  let ?add = "combine_matrix fadd"
  let ?t1 = "?mul y (?mul (?add A dA) x)"
  have a: "?t1 <= ?mul y b" by (rule le_left_mult, simp_all!)
  have b: "?t1 = ?mul (?mul y (?add A dA)) x" by (simp! add: mult_matrix_assoc_simple[THEN sym])
  have assoc: "associative ?add" by (simp! add: combine_matrix_assoc)
  have r_distr: "r_distributive ?mul ?add" 
    apply (rule r_distributive_matrix)
    by (simp! add: distributive_def)+
  have l_distr: "l_distributive ?mul ?add"
    apply (rule l_distributive_matrix)
    by (simp! add: distributive_def)+
  have c:"?mul y (?add A dA) = ?add (?mul y A) (?mul y dA)"
    by (insert r_distr, simp add: r_distributive_def)
  have d:"?mul (?add (?mul y A) (?mul y dA)) x = ?add (?mul (?mul y A) x) (?mul (?mul y dA) x)"
    by (insert l_distr, simp add: l_distributive_def)
  have e:"\<dots> = ?add (?mul c x) (?mul (?mul y dA) x)" by (simp!)
  from a b c d e show "?add (?mul c x) (?mul (?mul y dA) x) <= ?mul y b" by simp
qed

lemma linprog_by_duality_approx:
  assumes
  "(A + dA) * x <= (b::('a::pordered_matrix_element) matrix)"
  "y * A = c"
  "0 <= y"
  shows
  "c * x  + (y * dA) * x <= y * b"
apply (simp add: times_matrix_def plus_matrix_def)
apply (rule linprog_by_duality_approx_general)
apply (simp_all)
apply (simp_all add: associative_def matrix_add_assoc matrix_mult_assoc)
apply (simp_all add: commutative_def matrix_add_commute)
apply (simp_all add: distributive_def l_distributive_def r_distributive_def matrix_left_distrib matrix_right_distrib)
apply (simp_all! add: plus_matrix_def times_matrix_def)
apply (simp add: pordered_add)
apply (simp add: pordered_mult_left)
done

lemma linprog_by_duality:
  assumes
  "A * x <= (b::('a::pordered_g_semiring) matrix)"
  "y * A = c"
  "0 <= y"
  shows
  "c * x  <= y * b"
proof -
  have a:"(A + 0) * x <= b" by (simp!)
  have b:"c * x + (y*0)*x <= y * b" by (rule linprog_by_duality_approx, simp_all!) 
  show "c * x <= y*b" by (insert b, simp)
qed

end