--- a/src/HOL/Matrix/cplex/Cplex.thy Mon Jul 09 17:38:40 2007 +0200
+++ b/src/HOL/Matrix/cplex/Cplex.thy Mon Jul 09 17:39:55 2007 +0200
@@ -4,7 +4,7 @@
*)
theory Cplex
-imports FloatSparseMatrix
+imports FloatSparseMatrix "~~/src/HOL/Tools/ComputeNumeral"
uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML" "fspmlp.ML"
begin
--- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Mon Jul 09 17:38:40 2007 +0200
+++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Mon Jul 09 17:39:55 2007 +0200
@@ -69,7 +69,7 @@
val eupper = HOLogic.mk_prod (index, fupper)
in (elower :: lower, eupper :: upper) end;
in
- pairself (HOLogic.mk_list spvecT) (Inttab.fold app vector ([], []))
+ pairself (HOLogic.mk_list spvec_elemT) (Inttab.fold app vector ([], []))
end;
fun approx_matrix prec pprt vector =
@@ -82,7 +82,7 @@
val eupper = HOLogic.mk_prod (index, fupper)
in (elower :: lower, eupper :: upper) end;
in
- pairself (HOLogic.mk_list spmatT) (Inttab.fold app vector ([], []))
+ pairself (HOLogic.mk_list spmat_elemT) (Inttab.fold app vector ([], []))
end;
exception Nat_expected of int;
--- a/src/HOL/Matrix/cplex/MatrixLP.thy Mon Jul 09 17:38:40 2007 +0200
+++ b/src/HOL/Matrix/cplex/MatrixLP.thy Mon Jul 09 17:39:55 2007 +0200
@@ -4,65 +4,7 @@
*)
theory MatrixLP
-imports Cplex "~~/src/Tools/Compute_Oracle/Compute_Oracle"
-uses ("matrixlp.ML")
+imports Cplex
+uses "matrixlp.ML"
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
-
-use "matrixlp.ML"
-
end
--- a/src/HOL/Matrix/cplex/fspmlp.ML Mon Jul 09 17:38:40 2007 +0200
+++ b/src/HOL/Matrix/cplex/fspmlp.ML Mon Jul 09 17:39:55 2007 +0200
@@ -187,14 +187,10 @@
exception Load of string;
-(*val empty_spvec = @ {term "Nil :: (nat * real) list"};
-fun cons_spvec x xs = @ {term "Cons :: nat * real => nat * real => (nat * real) list"} $ x $ xs;
-val empty_spmat = @ {term "Nil :: (nat * (nat * real) list) list"};
-fun cons_spmat x xs = @ {term "Cons :: nat * (nat * real) list => (nat * (nat * real) list) list => (nat * (nat * real) list) list"} $ x $ xs;*)
-val empty_spvec = Bound 0
-fun cons_spvec x xs = Bound 0
-val empty_spmat = Bound 0
-fun cons_spmat x xs = Bound 0
+val empty_spvec = @{term "Nil :: real spvec"};
+fun cons_spvec x xs = @{term "Cons :: nat * real => real spvec => real spvec"} $ x $ xs;
+val empty_spmat = @{term "Nil :: real spmat"};
+fun cons_spmat x xs = @{term "Cons :: nat * real spvec => real spmat => real spmat"} $ x $ xs;
fun calcr safe_propagation xlen names prec A b =
let
@@ -267,9 +263,10 @@
end
val g = FloatSparseMatrixBuilder.m_fold calcr A VarGraph.empty
+
val g = propagate_sure_bounds safe_propagation names g
- val (r1, r2) = split_graph g
+ val (r1, r2) = split_graph g
fun add_row_entry m index value =
let
@@ -292,7 +289,9 @@
in
(add_row_entry r i' abs_max, (add_row_entry r12_1 i' b1, add_row_entry r12_2 i' b2))
end
+
val (r, (r1, r2)) = abs_estimate xlen r1 r2
+
in
(r, (r1, r2))
end
@@ -302,7 +301,7 @@
val prog = Cplex.load_cplexFile filename
val prog = Cplex.elim_nonfree_bounds prog
val prog = Cplex.relax_strict_ineqs prog
- val (maximize, c, A, b, (xlen, names, _)) = CplexFloatSparseMatrixConverter.convert_prog prog
+ val (maximize, c, A, b, (xlen, names, _)) = CplexFloatSparseMatrixConverter.convert_prog prog
val (r, (r1, r2)) = calcr safe_propagation xlen names prec A b
val _ = if maximize then () else raise Load "sorry, cannot handle minimization problems"
val (dualprog, indexof) = FloatSparseMatrixBuilder.dual_cplexProg c A b
--- a/src/HOL/Matrix/cplex/matrixlp.ML Mon Jul 09 17:38:40 2007 +0200
+++ b/src/HOL/Matrix/cplex/matrixlp.ML Mon Jul 09 17:39:55 2007 +0200
@@ -23,12 +23,15 @@
([(certT (TVar (hd (term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
end
-val spm_mult_le_dual_prts_no_let = thm "SparseMatrix.spm_mult_le_dual_prts_no_let";
-val cert = cterm_of (Thm.theory_of_thm spm_mult_le_dual_prts_no_let);
+local
+
+val cert = cterm_of @{theory "Cplex"}
+
+in
fun lp_dual_estimate_prt_primitive (y, (A1, A2), (c1, c2), b, (r1, r2)) =
let
- val th = inst_real spm_mult_le_dual_prts_no_let
+ val th = inst_real @{thm "SparseMatrix.spm_mult_le_dual_prts_no_let"}
fun var s x = (cert (Var ((s,0), FloatSparseMatrixBuilder.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
@@ -41,21 +44,15 @@
open Fspmlp
val l = load lptfile prec false
in
- (y l |> cert, A l |> pairself cert, c l |> pairself cert, b l |> cert, r12 l |> pairself cert)
+ (y l |> cert, A l |> pairself cert, c l |> pairself cert, b l |> cert, r12 l |> pairself cert)
end
in
lp_dual_estimate_prt_primitive certificate
end
-fun is_meta_eq th =
- let
- fun check ((Const ("==", _)) $ _ $ _) = true
- | check _ = false
- in
- check (concl_of th)
- end
+end
-fun prep ths = filter is_meta_eq ths @ map (standard o mk_meta_eq) (filter_out is_meta_eq ths)
+fun prep ths = ComputeHOL.prep_thms ths
fun inst_tvar ty thm =
let
@@ -69,38 +66,27 @@
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.spvecT
- val spmatT = FloatSparseMatrixBuilder.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.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"]))
+local
+ val matrix_lemmas = [
+ "ComputeHOL.compute_list_case",
+ "ComputeHOL.compute_let",
+ "ComputeHOL.compute_if",
+ "Float.arith",
+ "SparseMatrix.sparse_row_matrix_arith_simps",
+ "ComputeHOL.compute_bool",
+ "ComputeHOL.compute_pair",
+ "SparseMatrix.sorted_sp_simps",
+ "ComputeNumeral.number_norm",
+ "ComputeNumeral.natnorm"]
+ fun get_thms n = ComputeHOL.prep_thms (PureThy.get_thms @{theory "Cplex"} (Name n))
+ val ths = List.concat (map get_thms matrix_lemmas)
+ val computer = PCompute.make Compute.SML @{theory "Cplex"} ths []
+in
- val c = Compute.basic_make (the_context ()) ths
- in
- Compute.rewrite c
- end
+fun matrix_compute c = hd (PCompute.rewrite computer [c])
+end
+
fun matrix_simplify th =
let
val simp_th = matrix_compute (cprop_of th)