# HG changeset patch
# User obua
# Date 1121782613 -7200
# Node ID 9ed940a1bebb71464bfe80866a52681300444c5b
# Parent  a51699621d22705c6c557feb2427b5f1a3b96547
proving bounds for real linear programs

diff -r a51699621d22 -r 9ed940a1bebb etc/settings
--- a/etc/settings	Tue Jul 19 14:59:11 2005 +0200
+++ b/etc/settings	Tue Jul 19 16:16:53 2005 +0200
@@ -225,3 +225,15 @@
 
 # HOL4 proof objects (cf. Isabelle/src/HOL/Import)
 HOL4_PROOFS="$PROOF_DIRS:$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
+
+# For configuring HOL/Matrix/cplex
+# First option: use the commercial cplex solver
+# LP_SOLVER_NAME=CPLEX
+# LP_SOLVER_PATH=cplex
+# Second option: use the open source glpk solver
+# LP_SOLVER_NAME=GLPK
+# LP_SOLVER_PATH=glpsol
+
+# toogles the detail of the error message in case of a cyclic definition
+DEFS_CHAIN_HISTORY=ON
+#DEFS_CHAIN_HISTORY=OFF
\ No newline at end of file
diff -r a51699621d22 -r 9ed940a1bebb src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jul 19 14:59:11 2005 +0200
+++ b/src/HOL/IsaMakefile	Tue Jul 19 16:16:53 2005 +0200
@@ -630,9 +630,23 @@
   Matrix/document/root.tex Matrix/ROOT.ML \
   Matrix/cplex/ROOT.ML Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
   Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
-  Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML
+  Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \
+  Matrix/cplex/MatrixLP.thy Matrix/cplex/MatrixLP.ML
 	@$(ISATOOL) usedir $(OUT)/HOL-Complex Matrix
 
+## HOL-Complex-Matrix
+
+#HOL-Complex-Matrix: HOL $(OUT)/HOL-Complex-Matrix
+#
+#$(OUT)/HOL-Complex-Matrix: $(OUT)/HOL-Complex \
+#  Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
+#  Matrix/document/root.tex Matrix/ROOT.ML \
+#  Matrix/cplex/ROOT.ML Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
+#  Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
+#  Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \
+#  Matrix/cplex/MatrixLP.thy Matrix/cplex/MatrixLP.ML
+#	@cd Matrix; $(ISATOOL) usedir -b -g true $(OUT)/HOL-Complex HOL-Complex-Matrix
+
 
 ## TLA
 
diff -r a51699621d22 -r 9ed940a1bebb src/HOL/Matrix/ROOT.ML
--- a/src/HOL/Matrix/ROOT.ML	Tue Jul 19 14:59:11 2005 +0200
+++ b/src/HOL/Matrix/ROOT.ML	Tue Jul 19 16:16:53 2005 +0200
@@ -3,6 +3,6 @@
 *)
 
 use_thy "SparseMatrix";
-cd "cplex"; use_thy "Cplex"; cd "..";
+cd "cplex"; use_thy "MatrixLP"; cd "..";
 
 
diff -r a51699621d22 -r 9ed940a1bebb src/HOL/Matrix/cplex/Cplex_tools.ML
--- a/src/HOL/Matrix/cplex/Cplex_tools.ML	Tue Jul 19 14:59:11 2005 +0200
+++ b/src/HOL/Matrix/cplex/Cplex_tools.ML	Tue Jul 19 16:16:53 2005 +0200
@@ -1191,7 +1191,7 @@
     case getenv "LP_SOLVER_NAME" of
 	"CPLEX" => solve_cplex prog
       | "GLPK" => solve_glpk prog
-      | _ => raise (Execute ("LP_SOLVER.NAME must be set to CPLEX or to GLPK"));
+      | _ => raise (Execute ("LP_SOLVER_NAME must be set to CPLEX or to GLPK"));
 		   
 end;
 
diff -r a51699621d22 -r 9ed940a1bebb src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
--- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML	Tue Jul 19 14:59:11 2005 +0200
+++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML	Tue Jul 19 16:16:53 2005 +0200
@@ -81,14 +81,16 @@
 val Cons_spvec_const = Const (term_Cons, spvec_elemT --> spvecT --> spvecT)
 val Cons_spmat_const = Const (term_Cons, spmat_elemT --> spmatT --> spmatT) 
 			 
-val float_const = Const (readterm "float", HOLogic.mk_prodT (HOLogic.intT, HOLogic.intT) --> HOLogic.realT)
+val float_const = Float.float_const
+
+(*val float_const = Const (readterm "float", HOLogic.mk_prodT (HOLogic.intT, HOLogic.intT) --> HOLogic.realT)*)
 		  
 val zero = IntInf.fromInt 0
 val minus_one = IntInf.fromInt ~1
 val two = IntInf.fromInt 2
 	  
-fun mk_intinf ty n =
-    let
+val mk_intinf = Float.mk_intinf
+(*    let
 	fun mk_bit n = if n = zero then HOLogic.false_const else HOLogic.true_const
 								 
 	fun bin_of n = 
@@ -104,20 +106,20 @@
 		end
     in 
 	HOLogic.number_of_const ty $ (bin_of n)
-    end
+    end*)
 
-fun mk_float (a,b) = 
-    float_const $ (HOLogic.mk_prod ((mk_intinf HOLogic.intT a), (mk_intinf HOLogic.intT b)))
+val mk_float  = Float.mk_float 
+(*    float_const $ (HOLogic.mk_prod ((mk_intinf HOLogic.intT a), (mk_intinf HOLogic.intT b)))*)
 
 fun float2cterm (a,b) = cterm_of sg (mk_float (a,b))
 
-fun approx_value_term prec f value = 
-    let
+fun approx_value_term prec f = Float.approx_float prec (fn (x, y) => (f x, f y))
+(*    let
 	val (flower, fupper) = ExactFloatingPoint.approx_decstr_by_bin prec value
 	val (flower, fupper) = (f flower, f fupper)
     in
 	(mk_float flower, mk_float fupper)
-    end
+    end*)
 
 fun approx_value prec pprt value = 
     let
diff -r a51699621d22 -r 9ed940a1bebb src/HOL/Matrix/cplex/MatrixLP.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Matrix/cplex/MatrixLP.ML	Tue Jul 19 16:16:53 2005 +0200
@@ -0,0 +1,117 @@
+(*  Title:      HOL/Matrix/cplex/MatrixLP.ML
+    ID:         $Id$
+    Author:     Steven Obua
+*)
+
+signature MATRIX_LP = 
+sig
+  val lp_dual_estimate_prt : string -> int -> thm 
+  val matrix_compute : cterm -> thm
+  val matrix_simplify : thm -> thm
+  val prove_bound : string -> int -> thm
+  val float2real : string * string -> Real.real
+end
+
+structure MatrixLP : MATRIX_LP =
+struct
+
+val sg = sign_of (theory "MatrixLP")
+
+fun inst_real thm = standard (Thm.instantiate ([(ctyp_of sg (TVar (hd (term_tvars (prop_of thm)))),
+						 ctyp_of sg HOLogic.realT)], []) thm)
+
+fun lp_dual_estimate_prt lptfile prec = 
+    let
+	val th = inst_real (thm "SparseMatrix.spm_mult_le_dual_prts_no_let")
+	val (y, (A1, A2), (c1, c2), b, (r1, r2)) = 
+	    let
+		open fspmlp
+		val l = load lptfile prec false
+	    in
+		(y l, A l, c l, b l, r12 l)
+	    end		
+	fun var s x = (cterm_of sg (Var ((s,0), FloatSparseMatrixBuilder.real_spmatT)), x)
+	val th = Thm.instantiate ([], [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2, 
+				       var "r1" r1, var "r2" r2, var "b" b]) th
+    in
+	th
+    end
+	 
+fun read_ct s = read_cterm sg (s, TypeInfer.logicT);
+    
+fun is_meta_eq th =
+    let
+	fun check ((Const ("==", _)) $ _ $ _) = true
+	  | check _ = false
+    in
+	check (concl_of th)
+    end
+    
+fun prep ths = (Library.filter is_meta_eq ths) @ (map (standard o mk_meta_eq) (Library.filter (not o is_meta_eq) ths))
+
+fun make ths = Compute.basic_make sg ths
+	  
+fun inst_tvar ty thm = 
+    let
+	val ord = prod_ord (prod_ord string_ord int_ord) (list_ord string_ord)
+	val v = TVar (hd (sort ord (term_tvars (prop_of thm))))
+    in	
+	standard (Thm.instantiate ([(ctyp_of sg v, ctyp_of sg ty)], []) thm)
+    end
+    
+fun inst_tvars [] thms = thms
+  | inst_tvars (ty::tys) thms = inst_tvars tys (map (inst_tvar ty) thms)
+				
+val matrix_compute =
+    let 
+	val spvecT = FloatSparseMatrixBuilder.real_spvecT
+	val spmatT = FloatSparseMatrixBuilder.real_spmatT
+	val spvecT_elem = HOLogic.mk_prodT (HOLogic.natT, HOLogic.realT)
+	val spmatT_elem = HOLogic.mk_prodT (HOLogic.natT, spvecT)
+	val case_compute = map thm ["list_case_compute", "list_case_compute_empty", "list_case_compute_cons"]
+	val ths = 
+	    prep (
+	    (inst_tvars [HOLogic.intT, HOLogic.natT] (thms "Let_compute")) 
+	    @ (inst_tvars [HOLogic.intT, HOLogic.intT] (thms "Let_compute"))
+	    @ (map (fn t => inst_tvar t (thm "If_True")) [HOLogic.intT, HOLogic.natT, HOLogic.realT, spvecT, spmatT, HOLogic.boolT])
+	    @ (map (fn t => inst_tvar t (thm "If_False")) [HOLogic.intT, HOLogic.natT, HOLogic.realT, spvecT, spmatT, HOLogic.boolT])
+	    @ (thms "MatrixLP.float_arith")
+	    @ (map (inst_tvar HOLogic.realT) (thms "MatrixLP.sparse_row_matrix_arith_simps"))
+	    @ (thms "MatrixLP.boolarith")
+	    @ (inst_tvars [HOLogic.natT, HOLogic.realT] [thm "fst_compute", thm "snd_compute"])
+	    @ (inst_tvars [HOLogic.natT, FloatSparseMatrixBuilder.real_spvecT] [thm "fst_compute", thm "snd_compute"])
+	    @ (inst_tvars [HOLogic.boolT, spmatT_elem] case_compute)
+	    @ (inst_tvars [HOLogic.boolT, spvecT_elem] case_compute)
+	    @ (inst_tvars [HOLogic.boolT, HOLogic.realT] case_compute)
+	    @ (inst_tvars [spvecT] (thms "MatrixLP.sorted_sp_simps"))
+	    @ (inst_tvars [HOLogic.realT] (thms "MatrixLP.sorted_sp_simps"))
+	    @ [thm "zero_eq_Numeral0_nat", thm "one_eq_Numeral1_nat"]
+	    @ (inst_tvars [HOLogic.intT] [thm "zero_eq_Numeral0_nring", thm "one_eq_Numeral1_nring"])
+	    @ (inst_tvars [HOLogic.realT] [thm "zero_eq_Numeral0_nring", thm "one_eq_Numeral1_nring"]))
+	    
+	val c = make ths
+    in
+	Compute.rewrite c
+    end
+
+fun matrix_simplify th = 
+    let
+	val simp_th = matrix_compute (cprop_of th)
+	val th = strip_shyps (equal_elim simp_th th)
+	fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th
+    in
+	removeTrue th
+    end
+
+fun prove_bound lptfile prec = 
+    let
+	val th = lp_dual_estimate_prt lptfile prec
+    in
+	matrix_simplify th
+    end
+
+fun realFromStr s = valOf (Real.fromString s)
+fun float2real (x,y) = (realFromStr x) * (Math.pow (2.0, realFromStr y))
+
+end
+
diff -r a51699621d22 -r 9ed940a1bebb src/HOL/Matrix/cplex/MatrixLP.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Matrix/cplex/MatrixLP.thy	Tue Jul 19 16:16:53 2005 +0200
@@ -0,0 +1,66 @@
+(*  Title:      HOL/Matrix/cplex/MatrixLP.thy
+    ID:         $Id$
+    Author:     Steven Obua
+*)
+
+theory MatrixLP 
+imports Cplex
+begin
+
+constdefs
+  list_case_compute :: "'b list \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b list \<Rightarrow> 'a) \<Rightarrow> 'a"
+  "list_case_compute l a f == list_case a f l"
+
+lemma list_case_compute: "list_case = (\<lambda> (a::'a) f (l::'b list). list_case_compute l a f)"
+  apply (rule ext)+
+  apply (simp add: list_case_compute_def)
+  done
+
+lemma list_case_compute_empty: "list_case_compute ([]::'b list) = (\<lambda> (a::'a) f. a)"
+  apply (rule ext)+
+  apply (simp add: list_case_compute_def)
+  done
+
+lemma list_case_compute_cons: "list_case_compute (u#v) = (\<lambda> (a::'a) f. (f (u::'b) v))"
+  apply (rule ext)+
+  apply (simp add: list_case_compute_def)
+  done
+
+lemma If_True: "(If True) = (\<lambda> x y. x)"
+  apply (rule ext)+
+  apply auto
+  done
+
+lemma If_False: "(If False) = (\<lambda> x y. y)"
+  apply (rule ext)+
+  apply auto
+  done
+
+lemma Let_compute: "Let (x::'a) f = ((f x)::'b)"
+  by (simp add: Let_def)
+
+lemma fst_compute: "fst (a::'a, b::'b) = a"
+  by auto
+
+lemma snd_compute: "snd (a::'a, b::'b) = b"
+  by auto
+
+lemma bool1: "(\<not> True) = False"  by blast
+lemma bool2: "(\<not> False) = True"  by blast
+lemma bool3: "((P\<Colon>bool) \<and> True) = P" by blast
+lemma bool4: "(True \<and> (P\<Colon>bool)) = P" by blast
+lemma bool5: "((P\<Colon>bool) \<and> False) = False" by blast
+lemma bool6: "(False \<and> (P\<Colon>bool)) = False" by blast
+lemma bool7: "((P\<Colon>bool) \<or> True) = True" by blast
+lemma bool8: "(True \<or> (P\<Colon>bool)) = True" by blast
+lemma bool9: "((P\<Colon>bool) \<or> False) = P" by blast
+lemma bool10: "(False \<or> (P\<Colon>bool)) = P" by blast
+lemmas boolarith = bool1 bool2 bool3 bool4 bool5 bool6 bool7 bool8 bool9 bool10
+
+lemmas float_arith = Float.arith
+lemmas sparse_row_matrix_arith_simps = SparseMatrix.sparse_row_matrix_arith_simps
+lemmas sorted_sp_simps = SparseMatrix.sorted_sp_simps
+lemmas fst_snd_conv = Product_Type.fst_conv Product_Type.snd_conv
+
+end
+
diff -r a51699621d22 -r 9ed940a1bebb src/HOL/Matrix/cplex/ROOT.ML
--- a/src/HOL/Matrix/cplex/ROOT.ML	Tue Jul 19 14:59:11 2005 +0200
+++ b/src/HOL/Matrix/cplex/ROOT.ML	Tue Jul 19 16:16:53 2005 +0200
@@ -2,4 +2,4 @@
     ID:         $Id$
 *)
 
-(*use_thy "Cplex";*)
\ No newline at end of file
+use_thy "MatrixLP";
\ No newline at end of file
diff -r a51699621d22 -r 9ed940a1bebb src/HOL/Real/Float.ML
--- a/src/HOL/Real/Float.ML	Tue Jul 19 14:59:11 2005 +0200
+++ b/src/HOL/Real/Float.ML	Tue Jul 19 16:16:53 2005 +0200
@@ -352,7 +352,7 @@
 
 fun mk_intinf ty n =
     let
-	fun mk_bit n = if n = zero then HOLogic.false_const else HOLogic.true_const
+	fun mk_bit n = if n = zero then HOLogic.B0_const else HOLogic.B1_const
 								 
 	fun bin_of n = 
 	    if n = zero then HOLogic.pls_const
@@ -373,8 +373,8 @@
     let
 	fun dest_bit n = 
 	    case n of 
-		Const ("False", _) => FloatArith.izero
-	      | Const ("True", _) => FloatArith.ione
+		Const ("Numeral.bit.B0", _) => FloatArith.izero
+	      | Const ("Numeral.bit.B1", _) => FloatArith.ione
 	      | _ => raise Dest_intinf
 			 
 	fun int_of n =