--- 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
--- 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
--- 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 "..";
--- 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;
--- 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
--- /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
+
--- /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
+
--- 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
--- 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 =