Moved stuff from Ring_and_Field to Matrix
authorobua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 194049bf2cdc9e8e8
parent 19403 5c15cd397a82
child 19405 a551256aba15
Moved stuff from Ring_and_Field to Matrix
src/HOL/IsaMakefile
src/HOL/Matrix/SparseMatrix.thy
src/HOL/Matrix/cplex/MatrixLP.ML
src/HOL/Matrix/cplex/fspmlp.ML
src/HOL/OrderedGroup.thy
src/HOL/Ring_and_Field.thy
src/HOL/Wellfounded_Relations.thy
     1.1 --- a/src/HOL/IsaMakefile	Mon Apr 10 14:37:23 2006 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Apr 10 16:00:34 2006 +0200
     1.3 @@ -672,7 +672,7 @@
     1.4  HOL-Complex-Matrix: HOL-Complex $(OUT)/HOL-Complex-Matrix
     1.5  
     1.6  $(OUT)/HOL-Complex-Matrix: $(OUT)/HOL-Complex \
     1.7 -  Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
     1.8 +  Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy Matrix/LP.thy \
     1.9    Matrix/document/root.tex Matrix/ROOT.ML \
    1.10    Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
    1.11    Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
     2.1 --- a/src/HOL/Matrix/SparseMatrix.thy	Mon Apr 10 14:37:23 2006 +0200
     2.2 +++ b/src/HOL/Matrix/SparseMatrix.thy	Mon Apr 10 16:00:34 2006 +0200
     2.3 @@ -3,7 +3,7 @@
     2.4      Author:     Steven Obua
     2.5  *)
     2.6  
     2.7 -theory SparseMatrix imports Matrix begin
     2.8 +theory SparseMatrix imports Matrix LP begin
     2.9  
    2.10  types 
    2.11    'a spvec = "(nat * 'a) list"
     3.1 --- a/src/HOL/Matrix/cplex/MatrixLP.ML	Mon Apr 10 14:37:23 2006 +0200
     3.2 +++ b/src/HOL/Matrix/cplex/MatrixLP.ML	Mon Apr 10 16:00:34 2006 +0200
     3.3 @@ -6,6 +6,7 @@
     3.4  signature MATRIX_LP = 
     3.5  sig
     3.6    val lp_dual_estimate_prt : string -> int -> thm 
     3.7 +  val lp_dual_estimate_prt_primitive : cterm * (cterm * cterm) * (cterm * cterm) * cterm * (cterm * cterm) -> thm
     3.8    val matrix_compute : cterm -> thm
     3.9    val matrix_simplify : thm -> thm
    3.10    val prove_bound : string -> int -> thm
    3.11 @@ -20,21 +21,27 @@
    3.12  fun inst_real thm = standard (Thm.instantiate ([(ctyp_of sg (TVar (hd (term_tvars (prop_of thm)))),
    3.13  						 ctyp_of sg HOLogic.realT)], []) thm)
    3.14  
    3.15 +fun lp_dual_estimate_prt_primitive (y, (A1, A2), (c1, c2), b, (r1, r2)) = 
    3.16 +    let
    3.17 +	val th = inst_real (thm "SparseMatrix.spm_mult_le_dual_prts_no_let")
    3.18 +	fun var s x = (cterm_of sg (Var ((s,0), FloatSparseMatrixBuilder.real_spmatT)), x)
    3.19 +	val th = Thm.instantiate ([], [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2, 
    3.20 +				       var "r1" r1, var "r2" r2, var "b" b]) th
    3.21 +    in
    3.22 +	th
    3.23 +    end
    3.24 +
    3.25  fun lp_dual_estimate_prt lptfile prec = 
    3.26      let
    3.27 -	val th = inst_real (thm "SparseMatrix.spm_mult_le_dual_prts_no_let")
    3.28 -	val (y, (A1, A2), (c1, c2), b, (r1, r2)) = 
    3.29 +	val certificate = 
    3.30  	    let
    3.31  		open fspmlp
    3.32  		val l = load lptfile prec false
    3.33  	    in
    3.34  		(y l, A l, c l, b l, r12 l)
    3.35  	    end		
    3.36 -	fun var s x = (cterm_of sg (Var ((s,0), FloatSparseMatrixBuilder.real_spmatT)), x)
    3.37 -	val th = Thm.instantiate ([], [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2, 
    3.38 -				       var "r1" r1, var "r2" r2, var "b" b]) th
    3.39      in
    3.40 -	th
    3.41 +	lp_dual_estimate_prt_primitive certificate
    3.42      end
    3.43  	 
    3.44  fun read_ct s = read_cterm sg (s, TypeInfer.logicT);
     4.1 --- a/src/HOL/Matrix/cplex/fspmlp.ML	Mon Apr 10 14:37:23 2006 +0200
     4.2 +++ b/src/HOL/Matrix/cplex/fspmlp.ML	Mon Apr 10 16:00:34 2006 +0200
     4.3 @@ -6,6 +6,8 @@
     4.4  signature FSPMLP = 
     4.5  sig
     4.6      type linprog
     4.7 +    type vector = FloatSparseMatrixBuilder.vector
     4.8 +    type matrix = FloatSparseMatrixBuilder.matrix
     4.9  
    4.10      val y : linprog -> cterm
    4.11      val A : linprog -> cterm * cterm
    4.12 @@ -22,6 +24,9 @@
    4.13  structure fspmlp : FSPMLP = 
    4.14  struct
    4.15  
    4.16 +type vector = FloatSparseMatrixBuilder.vector
    4.17 +type matrix = FloatSparseMatrixBuilder.matrix
    4.18 +
    4.19  type linprog = cterm * (cterm * cterm) * cterm * (cterm * cterm) * cterm * (cterm * cterm)
    4.20  
    4.21  fun y (c1, c2, c3, c4, c5, _) = c1
    4.22 @@ -314,6 +319,7 @@
    4.23  	val c = FloatSparseMatrixBuilder.approx_matrix prec id c
    4.24      in
    4.25  	(y1, A, b2, c, r, (r1, r2))
    4.26 -    end handle CplexFloatSparseMatrixConverter.Converter s => (raise (Load ("Converter: "^s)))
    4.27 +    end handle CplexFloatSparseMatrixConverter.Converter s => (raise (Load ("Converter: "^s)))	
    4.28 +
    4.29  
    4.30  end
     5.1 --- a/src/HOL/OrderedGroup.thy	Mon Apr 10 14:37:23 2006 +0200
     5.2 +++ b/src/HOL/OrderedGroup.thy	Mon Apr 10 16:00:34 2006 +0200
     5.3 @@ -854,6 +854,12 @@
     5.4  lemma nprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> nprt a <= nprt b"
     5.5    by (simp add: le_def_meet nprt_def meet_aci)
     5.6  
     5.7 +lemma pprt_neg: "pprt (-x) = - nprt x"
     5.8 +  by (simp add: pprt_def nprt_def)
     5.9 +
    5.10 +lemma nprt_neg: "nprt (-x) = - pprt x"
    5.11 +  by (simp add: pprt_def nprt_def)
    5.12 +
    5.13  lemma iff2imp: "(A=B) \<Longrightarrow> (A \<Longrightarrow> B)"
    5.14  by (simp)
    5.15  
    5.16 @@ -1029,6 +1035,8 @@
    5.17  declare diff_le_0_iff_le [simp]
    5.18  
    5.19  
    5.20 +
    5.21 +
    5.22  ML {*
    5.23  val add_zero_left = thm"add_0";
    5.24  val add_zero_right = thm"add_0_right";
     6.1 --- a/src/HOL/Ring_and_Field.thy	Mon Apr 10 14:37:23 2006 +0200
     6.2 +++ b/src/HOL/Ring_and_Field.thy	Mon Apr 10 16:00:34 2006 +0200
     6.3 @@ -1932,71 +1932,7 @@
     6.4    apply (simp add: order_less_imp_le);
     6.5  done;
     6.6  
     6.7 -subsection {* Miscellaneous *}
     6.8 -
     6.9 -lemma linprog_dual_estimate:
    6.10 -  assumes
    6.11 -  "A * x \<le> (b::'a::lordered_ring)"
    6.12 -  "0 \<le> y"
    6.13 -  "abs (A - A') \<le> \<delta>A"
    6.14 -  "b \<le> b'"
    6.15 -  "abs (c - c') \<le> \<delta>c"
    6.16 -  "abs x \<le> r"
    6.17 -  shows
    6.18 -  "c * x \<le> y * b' + (y * \<delta>A + abs (y * A' - c') + \<delta>c) * r"
    6.19 -proof -
    6.20 -  from prems have 1: "y * b <= y * b'" by (simp add: mult_left_mono)
    6.21 -  from prems have 2: "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
    6.22 -  have 3: "y * (A * x) = c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x" by (simp add: ring_eq_simps)  
    6.23 -  from 1 2 3 have 4: "c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x <= y * b'" by simp
    6.24 -  have 5: "c * x <= y * b' + abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"
    6.25 -    by (simp only: 4 estimate_by_abs)  
    6.26 -  have 6: "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <= abs (y * (A - A') + (y * A' - c') + (c'-c)) * abs x"
    6.27 -    by (simp add: abs_le_mult)
    6.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"
    6.29 -    by(rule abs_triangle_ineq [THEN mult_right_mono]) simp
    6.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"
    6.31 -    by (simp add: abs_triangle_ineq mult_right_mono)    
    6.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"
    6.33 -    by (simp add: abs_le_mult mult_right_mono)  
    6.34 -  have 10: "c'-c = -(c-c')" by (simp add: ring_eq_simps)
    6.35 -  have 11: "abs (c'-c) = abs (c-c')" 
    6.36 -    by (subst 10, subst abs_minus_cancel, simp)
    6.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"
    6.38 -    by (simp add: 11 prems mult_right_mono)
    6.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"
    6.40 -    by (simp add: prems mult_right_mono mult_left_mono)  
    6.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"
    6.42 -    apply (rule mult_left_mono)
    6.43 -    apply (simp add: prems)
    6.44 -    apply (rule_tac add_mono[of "0::'a" _ "0", simplified])+
    6.45 -    apply (rule mult_left_mono[of "0" "\<delta>A", simplified])
    6.46 -    apply (simp_all)
    6.47 -    apply (rule order_trans[where y="abs (A-A')"], simp_all add: prems)
    6.48 -    apply (rule order_trans[where y="abs (c-c')"], simp_all add: prems)
    6.49 -    done    
    6.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"     
    6.51 -    by (simp)
    6.52 -  show ?thesis 
    6.53 -    apply (rule_tac le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
    6.54 -    apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified prems]])
    6.55 -    done
    6.56 -qed
    6.57 -
    6.58 -lemma le_ge_imp_abs_diff_1:
    6.59 -  assumes
    6.60 -  "A1 <= (A::'a::lordered_ring)"
    6.61 -  "A <= A2" 
    6.62 -  shows "abs (A-A1) <= A2-A1"
    6.63 -proof -
    6.64 -  have "0 <= A - A1"    
    6.65 -  proof -
    6.66 -    have 1: "A - A1 = A + (- A1)" by simp
    6.67 -    show ?thesis by (simp only: 1 add_right_mono[of A1 A "-A1", simplified, simplified prems])
    6.68 -  qed
    6.69 -  then have "abs (A-A1) = A-A1" by (rule abs_of_nonneg)
    6.70 -  with prems show "abs (A-A1) <= (A2-A1)" by simp
    6.71 -qed
    6.72 +subsection {* Bounds of products via negative and positive Part *}
    6.73  
    6.74  lemma mult_le_prts:
    6.75    assumes
    6.76 @@ -2045,39 +1981,23 @@
    6.77    ultimately show ?thesis
    6.78      by - (rule add_mono | simp)+
    6.79  qed
    6.80 -    
    6.81 -lemma mult_le_dual_prts: 
    6.82 +
    6.83 +lemma mult_ge_prts:
    6.84    assumes
    6.85 -  "A * x \<le> (b::'a::lordered_ring)"
    6.86 -  "0 \<le> y"
    6.87 -  "A1 \<le> A"
    6.88 -  "A \<le> A2"
    6.89 -  "c1 \<le> c"
    6.90 -  "c \<le> c2"
    6.91 -  "r1 \<le> x"
    6.92 -  "x \<le> r2"
    6.93 +  "a1 <= (a::'a::lordered_ring)"
    6.94 +  "a <= a2"
    6.95 +  "b1 <= b"
    6.96 +  "b <= b2"
    6.97    shows
    6.98 -  "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)"
    6.99 -  (is "_ <= _ + ?C")
   6.100 -proof -
   6.101 -  from prems have "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
   6.102 -  moreover have "y * (A * x) = c * x + (y * A - c) * x" by (simp add: ring_eq_simps)  
   6.103 -  ultimately have "c * x + (y * A - c) * x <= y * b" by simp
   6.104 -  then have "c * x <= y * b - (y * A - c) * x" by (simp add: le_diff_eq)
   6.105 -  then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: ring_eq_simps)
   6.106 -  have s2: "c - y * A <= c2 - y * A1"
   6.107 -    by (simp add: diff_def prems add_mono mult_left_mono)
   6.108 -  have s1: "c1 - y * A2 <= c - y * A"
   6.109 -    by (simp add: diff_def prems add_mono mult_left_mono)
   6.110 -  have prts: "(c - y * A) * x <= ?C"
   6.111 -    apply (simp add: Let_def)
   6.112 -    apply (rule mult_le_prts)
   6.113 -    apply (simp_all add: prems s1 s2)
   6.114 -    done
   6.115 -  then have "y * b + (c - y * A) * x <= y * b + ?C"
   6.116 -    by simp
   6.117 -  with cx show ?thesis
   6.118 -    by(simp only:)
   6.119 +  "a * b >= nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1"
   6.120 +proof - 
   6.121 +  from prems have a1:"- a2 <= -a" by auto
   6.122 +  from prems have a2: "-a <= -a1" by auto
   6.123 +  from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 prems(3) prems(4), simplified nprt_neg pprt_neg] 
   6.124 +  have le: "- (a * b) <= - nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1" by simp  
   6.125 +  then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"
   6.126 +    by (simp only: minus_le_iff)
   6.127 +  then show ?thesis by simp
   6.128  qed
   6.129  
   6.130  ML {*
     7.1 --- a/src/HOL/Wellfounded_Relations.thy	Mon Apr 10 14:37:23 2006 +0200
     7.2 +++ b/src/HOL/Wellfounded_Relations.thy	Mon Apr 10 16:00:34 2006 +0200
     7.3 @@ -116,13 +116,11 @@
     7.4  apply (drule spec, erule mp, blast) 
     7.5  done
     7.6  
     7.7 -
     7.8  text{*Transitivity of WF combinators.*}
     7.9  lemma trans_lex_prod [intro!]: 
    7.10      "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
    7.11  by (unfold trans_def lex_prod_def, blast) 
    7.12  
    7.13 -
    7.14  subsubsection{*Wellfoundedness of proper subset on finite sets.*}
    7.15  lemma wf_finite_psubset: "wf(finite_psubset)"
    7.16  apply (unfold finite_psubset_def)