--- a/src/HOL/Archimedean_Field.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Archimedean_Field.thy Mon Jul 12 11:21:56 2010 +0200
@@ -143,7 +143,7 @@
definition
floor :: "'a::archimedean_field \<Rightarrow> int" where
- [code del]: "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
+ "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
notation (xsymbols)
floor ("\<lfloor>_\<rfloor>")
@@ -274,7 +274,7 @@
definition
ceiling :: "'a::archimedean_field \<Rightarrow> int" where
- [code del]: "ceiling x = - floor (- x)"
+ "ceiling x = - floor (- x)"
notation (xsymbols)
ceiling ("\<lceil>_\<rceil>")
--- a/src/HOL/Complete_Lattice.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Complete_Lattice.thy Mon Jul 12 11:21:56 2010 +0200
@@ -193,10 +193,10 @@
begin
definition
- Inf_fun_def [code del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
+ Inf_fun_def: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
definition
- Sup_fun_def [code del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
+ Sup_fun_def: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
instance proof
qed (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
@@ -457,7 +457,7 @@
notation (xsymbols)
Inter ("\<Inter>_" [90] 90)
-lemma Inter_eq [code del]:
+lemma Inter_eq:
"\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
proof (rule set_ext)
fix x
--- a/src/HOL/Complex.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Complex.thy Mon Jul 12 11:21:56 2010 +0200
@@ -281,7 +281,7 @@
definition dist_complex_def:
"dist x y = cmod (x - y)"
-definition open_complex_def [code del]:
+definition open_complex_def:
"open (S :: complex set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
lemmas cmod_def = complex_norm_def
--- a/src/HOL/Divides.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Divides.thy Mon Jul 12 11:21:56 2010 +0200
@@ -527,7 +527,7 @@
begin
definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
- [code del]: "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
+ "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
lemma divmod_nat_rel_divmod_nat:
"divmod_nat_rel m n (divmod_nat m n)"
--- a/src/HOL/Equiv_Relations.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Equiv_Relations.thy Mon Jul 12 11:21:56 2010 +0200
@@ -93,7 +93,7 @@
subsection {* Quotients *}
definition quotient :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set" (infixl "'/'/" 90) where
- [code del]: "A//r = (\<Union>x \<in> A. {r``{x}})" -- {* set of equiv classes *}
+ "A//r = (\<Union>x \<in> A. {r``{x}})" -- {* set of equiv classes *}
lemma quotientI: "x \<in> A ==> r``{x} \<in> A//r"
by (unfold quotient_def) blast
--- a/src/HOL/Finite_Set.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Finite_Set.thy Mon Jul 12 11:21:56 2010 +0200
@@ -589,7 +589,7 @@
inductive_cases empty_fold_graphE [elim!]: "fold_graph f z {} x"
definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" where
-[code del]: "fold f z A = (THE y. fold_graph f z A y)"
+ "fold f z A = (THE y. fold_graph f z A y)"
text{*A tempting alternative for the definiens is
@{term "if finite A then THE y. fold_graph f z A y else e"}.
--- a/src/HOL/Fun.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Fun.thy Mon Jul 12 11:21:56 2010 +0200
@@ -131,7 +131,7 @@
definition
bij_betw :: "('a => 'b) => 'a set => 'b set => bool" where -- "bijective"
- [code del]: "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
+ "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
definition
surj :: "('a => 'b) => bool" where
--- a/src/HOL/FunDef.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/FunDef.thy Mon Jul 12 11:21:56 2010 +0200
@@ -224,11 +224,11 @@
subsection {* Concrete orders for SCNP termination proofs *}
definition "pair_less = less_than <*lex*> less_than"
-definition [code del]: "pair_leq = pair_less^="
+definition "pair_leq = pair_less^="
definition "max_strict = max_ext pair_less"
-definition [code del]: "max_weak = max_ext pair_leq \<union> {({}, {})}"
-definition [code del]: "min_strict = min_ext pair_less"
-definition [code del]: "min_weak = min_ext pair_leq \<union> {({}, {})}"
+definition "max_weak = max_ext pair_leq \<union> {({}, {})}"
+definition "min_strict = min_ext pair_less"
+definition "min_weak = min_ext pair_leq \<union> {({}, {})}"
lemma wf_pair_less[simp]: "wf pair_less"
by (auto simp: pair_less_def)
--- a/src/HOL/HOL.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/HOL.thy Mon Jul 12 11:21:56 2010 +0200
@@ -1138,7 +1138,7 @@
*}
definition simp_implies :: "[prop, prop] => prop" (infixr "=simp=>" 1) where
- [code del]: "simp_implies \<equiv> op ==>"
+ "simp_implies \<equiv> op ==>"
lemma simp_impliesI:
assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Mon Jul 12 11:21:56 2010 +0200
@@ -42,7 +42,7 @@
definition
traverse :: "'a\<Colon>heap node \<Rightarrow> 'a list Heap"
where
-[code del]: "traverse = MREC (\<lambda>n. case n of Empty \<Rightarrow> return (Inl [])
+ "traverse = MREC (\<lambda>n. case n of Empty \<Rightarrow> return (Inl [])
| Node x r \<Rightarrow> (do tl \<leftarrow> Ref.lookup r;
return (Inr tl) done))
(\<lambda>n tl xs. case n of Empty \<Rightarrow> undefined
--- a/src/HOL/Int.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Int.thy Mon Jul 12 11:21:56 2010 +0200
@@ -18,7 +18,7 @@
subsection {* The equivalence relation underlying the integers *}
definition intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set" where
- [code del]: "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
+ "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
typedef (Integ)
int = "UNIV//intrel"
@@ -28,34 +28,34 @@
begin
definition
- Zero_int_def [code del]: "0 = Abs_Integ (intrel `` {(0, 0)})"
+ Zero_int_def: "0 = Abs_Integ (intrel `` {(0, 0)})"
definition
- One_int_def [code del]: "1 = Abs_Integ (intrel `` {(1, 0)})"
+ One_int_def: "1 = Abs_Integ (intrel `` {(1, 0)})"
definition
- add_int_def [code del]: "z + w = Abs_Integ
+ add_int_def: "z + w = Abs_Integ
(\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
intrel `` {(x + u, y + v)})"
definition
- minus_int_def [code del]:
+ minus_int_def:
"- z = Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
definition
- diff_int_def [code del]: "z - w = z + (-w \<Colon> int)"
+ diff_int_def: "z - w = z + (-w \<Colon> int)"
definition
- mult_int_def [code del]: "z * w = Abs_Integ
+ mult_int_def: "z * w = Abs_Integ
(\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.
intrel `` {(x*u + y*v, x*v + y*u)})"
definition
- le_int_def [code del]:
+ le_int_def:
"z \<le> w \<longleftrightarrow> (\<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w)"
definition
- less_int_def [code del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
+ less_int_def: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
definition
zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
@@ -283,7 +283,7 @@
begin
definition of_int :: "int \<Rightarrow> 'a" where
- [code del]: "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
+ "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
proof -
@@ -388,10 +388,8 @@
subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
-definition
- nat :: "int \<Rightarrow> nat"
-where
- [code del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
+definition nat :: "int \<Rightarrow> nat" where
+ "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
proof -
@@ -593,21 +591,17 @@
subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *}
-definition
- Pls :: int where
- [code del]: "Pls = 0"
-
-definition
- Min :: int where
- [code del]: "Min = - 1"
-
-definition
- Bit0 :: "int \<Rightarrow> int" where
- [code del]: "Bit0 k = k + k"
-
-definition
- Bit1 :: "int \<Rightarrow> int" where
- [code del]: "Bit1 k = 1 + k + k"
+definition Pls :: int where
+ "Pls = 0"
+
+definition Min :: int where
+ "Min = - 1"
+
+definition Bit0 :: "int \<Rightarrow> int" where
+ "Bit0 k = k + k"
+
+definition Bit1 :: "int \<Rightarrow> int" where
+ "Bit1 k = 1 + k + k"
class number = -- {* for numeric types: nat, int, real, \dots *}
fixes number_of :: "int \<Rightarrow> 'a"
@@ -630,13 +624,11 @@
-- {* Unfold all @{text let}s involving constants *}
unfolding Let_def ..
-definition
- succ :: "int \<Rightarrow> int" where
- [code del]: "succ k = k + 1"
-
-definition
- pred :: "int \<Rightarrow> int" where
- [code del]: "pred k = k - 1"
+definition succ :: "int \<Rightarrow> int" where
+ "succ k = k + 1"
+
+definition pred :: "int \<Rightarrow> int" where
+ "pred k = k - 1"
lemmas
max_number_of [simp] = max_def
@@ -952,8 +944,8 @@
instantiation int :: number_ring
begin
-definition int_number_of_def [code del]:
- "number_of w = (of_int w \<Colon> int)"
+definition
+ int_number_of_def: "number_of w = (of_int w \<Colon> int)"
instance proof
qed (simp only: int_number_of_def)
@@ -1274,7 +1266,7 @@
begin
definition Ints :: "'a set" where
- [code del]: "Ints = range of_int"
+ "Ints = range of_int"
notation (xsymbols)
Ints ("\<int>")
@@ -2233,7 +2225,8 @@
instantiation int :: eq
begin
-definition [code del]: "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
+definition
+ "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
instance by default (simp add: eq_int_def)
--- a/src/HOL/IsaMakefile Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/IsaMakefile Mon Jul 12 11:21:56 2010 +0200
@@ -1058,10 +1058,10 @@
$(SRC)/Tools/Compute_Oracle/compute.ML Matrix/ComputeFloat.thy \
Matrix/ComputeHOL.thy Matrix/ComputeNumeral.thy Tools/float_arith.ML \
Matrix/Matrix.thy Matrix/SparseMatrix.thy Matrix/LP.thy \
- Matrix/document/root.tex Matrix/ROOT.ML Matrix/cplex/Cplex.thy \
- Matrix/cplex/CplexMatrixConverter.ML Matrix/cplex/Cplex_tools.ML \
- Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \
- Matrix/cplex/matrixlp.ML
+ Matrix/document/root.tex Matrix/ROOT.ML Matrix/Cplex.thy \
+ Matrix/CplexMatrixConverter.ML Matrix/Cplex_tools.ML \
+ Matrix/FloatSparseMatrixBuilder.ML Matrix/fspmlp.ML \
+ Matrix/matrixlp.ML
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Matrix
--- a/src/HOL/Lattices.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Lattices.thy Mon Jul 12 11:21:56 2010 +0200
@@ -623,10 +623,10 @@
begin
definition
- inf_fun_eq [code del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
+ inf_fun_eq: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
definition
- sup_fun_eq [code del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
+ sup_fun_eq: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
instance proof
qed (simp_all add: le_fun_def inf_fun_eq sup_fun_eq)
--- a/src/HOL/Library/Char_ord.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Library/Char_ord.thy Mon Jul 12 11:21:56 2010 +0200
@@ -63,11 +63,11 @@
begin
definition
- char_less_eq_def [code del]: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
+ char_less_eq_def: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2)"
definition
- char_less_def [code del]: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
+ char_less_def: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
n1 < n2 \<or> n1 = n2 \<and> m1 < m2)"
instance
--- a/src/HOL/Library/ContNotDenum.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Library/ContNotDenum.thy Mon Jul 12 11:21:56 2010 +0200
@@ -402,7 +402,6 @@
(f (Suc n)) \<notin> e)
)"
-declare newInt.simps [code del]
subsubsection {* Properties *}
--- a/src/HOL/Library/Dlist.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Library/Dlist.thy Mon Jul 12 11:21:56 2010 +0200
@@ -23,7 +23,7 @@
text {* Formal, totalized constructor for @{typ "'a dlist"}: *}
definition Dlist :: "'a list \<Rightarrow> 'a dlist" where
- [code del]: "Dlist xs = Abs_dlist (remdups xs)"
+ "Dlist xs = Abs_dlist (remdups xs)"
lemma distinct_list_of_dlist [simp]:
"distinct (list_of_dlist dxs)"
--- a/src/HOL/Library/Enum.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Library/Enum.thy Mon Jul 12 11:21:56 2010 +0200
@@ -149,7 +149,7 @@
begin
definition
- [code del]: "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
+ "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
instance proof
show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)"
@@ -278,7 +278,7 @@
begin
definition
- [code del]: "enum = map (split Char) (product enum enum)"
+ "enum = map (split Char) (product enum enum)"
lemma enum_chars [code]:
"enum = chars"
--- a/src/HOL/Library/Fraction_Field.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Library/Fraction_Field.thy Mon Jul 12 11:21:56 2010 +0200
@@ -69,7 +69,7 @@
definition
Fract :: "'a::idom \<Rightarrow> 'a \<Rightarrow> 'a fract" where
- [code del]: "Fract a b = Abs_fract (fractrel `` {if b = 0 then (0, 1) else (a, b)})"
+ "Fract a b = Abs_fract (fractrel `` {if b = 0 then (0, 1) else (a, b)})"
code_datatype Fract
@@ -93,13 +93,13 @@
begin
definition
- Zero_fract_def [code, code_unfold]: "0 = Fract 0 1"
+ Zero_fract_def [code_unfold]: "0 = Fract 0 1"
definition
- One_fract_def [code, code_unfold]: "1 = Fract 1 1"
+ One_fract_def [code_unfold]: "1 = Fract 1 1"
definition
- add_fract_def [code del]:
+ add_fract_def:
"q + r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
fractrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})"
@@ -115,7 +115,7 @@
qed
definition
- minus_fract_def [code del]:
+ minus_fract_def:
"- q = Abs_fract (\<Union>x \<in> Rep_fract q. fractrel `` {(- fst x, snd x)})"
lemma minus_fract [simp, code]: "- Fract a b = Fract (- a) (b::'a::idom)"
@@ -129,7 +129,7 @@
by (cases "b = 0") (simp_all add: eq_fract)
definition
- diff_fract_def [code del]: "q - r = q + - (r::'a fract)"
+ diff_fract_def: "q - r = q + - (r::'a fract)"
lemma diff_fract [simp]:
assumes "b \<noteq> 0" and "d \<noteq> 0"
@@ -137,7 +137,7 @@
using assms by (simp add: diff_fract_def diff_minus)
definition
- mult_fract_def [code del]:
+ mult_fract_def:
"q * r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
fractrel``{(fst x * fst y, snd x * snd y)})"
@@ -236,7 +236,7 @@
begin
definition
- inverse_fract_def [code del]:
+ inverse_fract_def:
"inverse q = Abs_fract (\<Union>x \<in> Rep_fract q.
fractrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})"
@@ -250,7 +250,7 @@
qed
definition
- divide_fract_def [code del]: "q / r = q * inverse (r:: 'a fract)"
+ divide_fract_def: "q / r = q * inverse (r:: 'a fract)"
lemma divide_fract [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
by (simp add: divide_fract_def)
@@ -318,12 +318,12 @@
begin
definition
- le_fract_def [code del]:
+ le_fract_def:
"q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
{(fst x * snd y)*(snd x * snd y) \<le> (fst y * snd x)*(snd x * snd y)})"
definition
- less_fract_def [code del]: "z < (w::'a fract) \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z"
+ less_fract_def: "z < (w::'a fract) \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z"
lemma le_fract [simp]:
assumes "b \<noteq> 0" and "d \<noteq> 0"
--- a/src/HOL/Library/Fset.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Library/Fset.thy Mon Jul 12 11:21:56 2010 +0200
@@ -124,10 +124,10 @@
begin
definition Inf_fset :: "'a fset set \<Rightarrow> 'a fset" where
- [simp, code del]: "Inf_fset As = Fset (Inf (image member As))"
+ [simp]: "Inf_fset As = Fset (Inf (image member As))"
definition Sup_fset :: "'a fset set \<Rightarrow> 'a fset" where
- [simp, code del]: "Sup_fset As = Fset (Sup (image member As))"
+ [simp]: "Sup_fset As = Fset (Sup (image member As))"
instance proof
qed (auto simp add: le_fun_def le_bool_def)
--- a/src/HOL/Library/List_lexord.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Library/List_lexord.thy Mon Jul 12 11:21:56 2010 +0200
@@ -62,10 +62,10 @@
begin
definition
- [code del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
+ "(inf \<Colon> 'a list \<Rightarrow> _) = min"
definition
- [code del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
+ "(sup \<Colon> 'a list \<Rightarrow> _) = max"
instance
by intro_classes
--- a/src/HOL/Library/Multiset.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Jul 12 11:21:56 2010 +0200
@@ -978,11 +978,11 @@
subsubsection {* Well-foundedness *}
definition mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
- [code del]: "mult1 r = {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
+ "mult1 r = {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
(\<forall>b. b :# K --> (b, a) \<in> r)}"
definition mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
- [code del]: "mult r = (mult1 r)\<^sup>+"
+ "mult r = (mult1 r)\<^sup>+"
lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
by (simp add: mult1_def)
@@ -1498,7 +1498,7 @@
by auto
definition "ms_strict = mult pair_less"
-definition [code del]: "ms_weak = ms_strict \<union> Id"
+definition "ms_weak = ms_strict \<union> Id"
lemma ms_reduction_pair: "reduction_pair (ms_strict, ms_weak)"
unfolding reduction_pair_def ms_strict_def ms_weak_def pair_less_def
--- a/src/HOL/Library/Nat_Infinity.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy Mon Jul 12 11:21:56 2010 +0200
@@ -126,7 +126,7 @@
begin
definition
- [code del]: "m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | Fin m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | Fin n \<Rightarrow> Fin (m + n)))"
+ "m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | Fin m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | Fin n \<Rightarrow> Fin (m + n)))"
lemma plus_inat_simps [simp, code]:
"Fin m + Fin n = Fin (m + n)"
@@ -177,7 +177,7 @@
begin
definition
- times_inat_def [code del]:
+ times_inat_def:
"m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | Fin m \<Rightarrow>
(case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | Fin n \<Rightarrow> Fin (m * n)))"
@@ -238,11 +238,11 @@
begin
definition
- [code del]: "m \<le> n = (case n of Fin n1 \<Rightarrow> (case m of Fin m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False)
+ "m \<le> n = (case n of Fin n1 \<Rightarrow> (case m of Fin m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False)
| \<infinity> \<Rightarrow> True)"
definition
- [code del]: "m < n = (case m of Fin m1 \<Rightarrow> (case n of Fin n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
+ "m < n = (case m of Fin m1 \<Rightarrow> (case n of Fin n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
| \<infinity> \<Rightarrow> False)"
lemma inat_ord_simps [simp]:
--- a/src/HOL/Library/Option_ord.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Library/Option_ord.thy Mon Jul 12 11:21:56 2010 +0200
@@ -12,10 +12,10 @@
begin
definition less_eq_option where
- [code del]: "x \<le> y \<longleftrightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> x \<le> y))"
+ "x \<le> y \<longleftrightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> x \<le> y))"
definition less_option where
- [code del]: "x < y \<longleftrightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> x < y))"
+ "x < y \<longleftrightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> x < y))"
lemma less_eq_option_None [simp]: "None \<le> x"
by (simp add: less_eq_option_def)
--- a/src/HOL/Library/Polynomial.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Library/Polynomial.thy Mon Jul 12 11:21:56 2010 +0200
@@ -98,7 +98,7 @@
definition
pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
where
- [code del]: "pCons a p = Abs_poly (nat_case a (coeff p))"
+ "pCons a p = Abs_poly (nat_case a (coeff p))"
syntax
"_poly" :: "args \<Rightarrow> 'a poly" ("[:(_):]")
@@ -209,7 +209,7 @@
function
poly_rec :: "'b \<Rightarrow> ('a::zero \<Rightarrow> 'a poly \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a poly \<Rightarrow> 'b"
where
- poly_rec_pCons_eq_if [simp del, code del]:
+ poly_rec_pCons_eq_if [simp del]:
"poly_rec z f (pCons a p) = f a p (if p = 0 then z else poly_rec z f p)"
by (case_tac x, rename_tac q, case_tac q, auto)
@@ -266,7 +266,7 @@
begin
definition
- plus_poly_def [code del]:
+ plus_poly_def:
"p + q = Abs_poly (\<lambda>n. coeff p n + coeff q n)"
lemma Poly_add:
@@ -305,11 +305,11 @@
begin
definition
- uminus_poly_def [code del]:
+ uminus_poly_def:
"- p = Abs_poly (\<lambda>n. - coeff p n)"
definition
- minus_poly_def [code del]:
+ minus_poly_def:
"p - q = Abs_poly (\<lambda>n. coeff p n - coeff q n)"
lemma Poly_minus:
@@ -512,7 +512,7 @@
begin
definition
- times_poly_def [code del]:
+ times_poly_def:
"p * q = poly_rec 0 (\<lambda>a p pq. smult a q + pCons 0 pq) p"
lemma mult_poly_0_left: "(0::'a poly) * q = 0"
@@ -736,20 +736,16 @@
begin
definition
- [code del]:
- "x < y \<longleftrightarrow> pos_poly (y - x)"
+ "x < y \<longleftrightarrow> pos_poly (y - x)"
definition
- [code del]:
- "x \<le> y \<longleftrightarrow> x = y \<or> pos_poly (y - x)"
+ "x \<le> y \<longleftrightarrow> x = y \<or> pos_poly (y - x)"
definition
- [code del]:
- "abs (x::'a poly) = (if x < 0 then - x else x)"
+ "abs (x::'a poly) = (if x < 0 then - x else x)"
definition
- [code del]:
- "sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
+ "sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
instance proof
fix x y :: "'a poly"
@@ -818,7 +814,6 @@
definition
pdivmod_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
where
- [code del]:
"pdivmod_rel x y q r \<longleftrightarrow>
x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
@@ -943,10 +938,10 @@
begin
definition div_poly where
- [code del]: "x div y = (THE q. \<exists>r. pdivmod_rel x y q r)"
+ "x div y = (THE q. \<exists>r. pdivmod_rel x y q r)"
definition mod_poly where
- [code del]: "x mod y = (THE r. \<exists>q. pdivmod_rel x y q r)"
+ "x mod y = (THE r. \<exists>q. pdivmod_rel x y q r)"
lemma div_poly_eq:
"pdivmod_rel x y q r \<Longrightarrow> x div y = q"
@@ -1133,7 +1128,7 @@
by (relation "measure (\<lambda>(x, y). if y = 0 then 0 else Suc (degree y))")
(auto dest: degree_mod_less)
-declare poly_gcd.simps [simp del, code del]
+declare poly_gcd.simps [simp del]
lemma poly_gcd_dvd1 [iff]: "poly_gcd x y dvd x"
and poly_gcd_dvd2 [iff]: "poly_gcd x y dvd y"
@@ -1287,7 +1282,7 @@
definition
synthetic_divmod :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly \<times> 'a"
-where [code del]:
+where
"synthetic_divmod p c =
poly_rec (0, 0) (\<lambda>a p (q, r). (pCons r q, a + c * r)) p"
@@ -1442,7 +1437,6 @@
definition
order :: "'a::idom \<Rightarrow> 'a poly \<Rightarrow> nat"
where
- [code del]:
"order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)"
lemma coeff_linear_power:
@@ -1514,7 +1508,7 @@
instantiation poly :: ("{zero,eq}") eq
begin
-definition [code del]:
+definition
"eq_class.eq (p::'a poly) q \<longleftrightarrow> p = q"
instance
@@ -1574,7 +1568,7 @@
definition
pdivmod :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly"
where
- [code del]: "pdivmod x y = (x div y, x mod y)"
+ "pdivmod x y = (x div y, x mod y)"
lemma div_poly_code [code]: "x div y = fst (pdivmod x y)"
unfolding pdivmod_def by simp
--- a/src/HOL/Library/Product_ord.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Library/Product_ord.thy Mon Jul 12 11:21:56 2010 +0200
@@ -12,10 +12,10 @@
begin
definition
- prod_le_def [code del]: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x \<le> snd y"
+ prod_le_def: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x \<le> snd y"
definition
- prod_less_def [code del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x < snd y"
+ prod_less_def: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x < snd y"
instance ..
--- a/src/HOL/Library/Sublist_Order.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Library/Sublist_Order.thy Mon Jul 12 11:21:56 2010 +0200
@@ -26,7 +26,7 @@
| take: "ys \<le> xs \<Longrightarrow> x # ys \<le> x # xs"
definition
- [code del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
+ "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
instance proof qed
--- a/src/HOL/Library/Univ_Poly.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Library/Univ_Poly.thy Mon Jul 12 11:21:56 2010 +0200
@@ -71,7 +71,7 @@
definition (in semiring_0)
divides :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "divides" 70) where
- [code del]: "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
+ "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
--{*order of a polynomial*}
definition (in ring_1) order :: "'a => 'a list => nat" where
--- a/src/HOL/Lim.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Lim.thy Mon Jul 12 11:21:56 2010 +0200
@@ -23,7 +23,7 @@
definition
isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where
- [code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"
+ "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"
subsection {* Limits of Functions *}
--- a/src/HOL/Limits.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Limits.thy Mon Jul 12 11:21:56 2010 +0200
@@ -37,9 +37,8 @@
subsection {* Eventually *}
-definition
- eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a net \<Rightarrow> bool" where
- [code del]: "eventually P net \<longleftrightarrow> Rep_net net P"
+definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a net \<Rightarrow> bool" where
+ "eventually P net \<longleftrightarrow> Rep_net net P"
lemma eventually_Abs_net:
assumes "is_filter net" shows "eventually P (Abs_net net) = net P"
@@ -114,37 +113,29 @@
begin
definition
- le_net_def [code del]:
- "net \<le> net' \<longleftrightarrow> (\<forall>P. eventually P net' \<longrightarrow> eventually P net)"
+ le_net_def: "net \<le> net' \<longleftrightarrow> (\<forall>P. eventually P net' \<longrightarrow> eventually P net)"
definition
- less_net_def [code del]:
- "(net :: 'a net) < net' \<longleftrightarrow> net \<le> net' \<and> \<not> net' \<le> net"
+ less_net_def: "(net :: 'a net) < net' \<longleftrightarrow> net \<le> net' \<and> \<not> net' \<le> net"
definition
- top_net_def [code del]:
- "top = Abs_net (\<lambda>P. \<forall>x. P x)"
+ top_net_def: "top = Abs_net (\<lambda>P. \<forall>x. P x)"
definition
- bot_net_def [code del]:
- "bot = Abs_net (\<lambda>P. True)"
+ bot_net_def: "bot = Abs_net (\<lambda>P. True)"
definition
- sup_net_def [code del]:
- "sup net net' = Abs_net (\<lambda>P. eventually P net \<and> eventually P net')"
+ sup_net_def: "sup net net' = Abs_net (\<lambda>P. eventually P net \<and> eventually P net')"
definition
- inf_net_def [code del]:
- "inf a b = Abs_net
+ inf_net_def: "inf a b = Abs_net
(\<lambda>P. \<exists>Q R. eventually Q a \<and> eventually R b \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
definition
- Sup_net_def [code del]:
- "Sup A = Abs_net (\<lambda>P. \<forall>net\<in>A. eventually P net)"
+ Sup_net_def: "Sup A = Abs_net (\<lambda>P. \<forall>net\<in>A. eventually P net)"
definition
- Inf_net_def [code del]:
- "Inf A = Sup {x::'a net. \<forall>y\<in>A. x \<le> y}"
+ Inf_net_def: "Inf A = Sup {x::'a net. \<forall>y\<in>A. x \<le> y}"
lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)"
unfolding top_net_def
@@ -243,9 +234,7 @@
subsection {* Map function for nets *}
-definition
- netmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a net \<Rightarrow> 'b net"
-where [code del]:
+definition netmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a net \<Rightarrow> 'b net" where
"netmap f net = Abs_net (\<lambda>P. eventually (\<lambda>x. P (f x)) net)"
lemma eventually_netmap:
@@ -271,9 +260,7 @@
subsection {* Sequentially *}
-definition
- sequentially :: "nat net"
-where [code del]:
+definition sequentially :: "nat net" where
"sequentially = Abs_net (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
lemma eventually_sequentially:
@@ -302,19 +289,13 @@
subsection {* Standard Nets *}
-definition
- within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70)
-where [code del]:
+definition within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70) where
"net within S = Abs_net (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) net)"
-definition
- nhds :: "'a::topological_space \<Rightarrow> 'a net"
-where [code del]:
+definition nhds :: "'a::topological_space \<Rightarrow> 'a net" where
"nhds a = Abs_net (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
-definition
- at :: "'a::topological_space \<Rightarrow> 'a net"
-where [code del]:
+definition at :: "'a::topological_space \<Rightarrow> 'a net" where
"at a = nhds a within - {a}"
lemma eventually_within:
@@ -368,9 +349,8 @@
subsection {* Boundedness *}
-definition
- Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
- [code del]: "Bfun f net = (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) net)"
+definition Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
+ "Bfun f net = (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) net)"
lemma BfunI:
assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) net" shows "Bfun f net"
@@ -390,9 +370,8 @@
subsection {* Convergence to Zero *}
-definition
- Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
- [code del]: "Zfun f net = (\<forall>r>0. eventually (\<lambda>x. norm (f x) < r) net)"
+definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
+ "Zfun f net = (\<forall>r>0. eventually (\<lambda>x. norm (f x) < r) net)"
lemma ZfunI:
"(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) net) \<Longrightarrow> Zfun f net"
@@ -547,10 +526,8 @@
subsection {* Limits *}
-definition
- tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
- (infixr "--->" 55)
-where [code del]:
+definition tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
+ (infixr "--->" 55) where
"(f ---> l) net \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
ML {*
--- a/src/HOL/List.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/List.thy Mon Jul 12 11:21:56 2010 +0200
@@ -208,7 +208,7 @@
definition
list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
- [code del]: "list_all2 P xs ys =
+ "list_all2 P xs ys =
(length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"
definition
@@ -4206,7 +4206,7 @@
definition
set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set" where
- [code del]: "set_Cons A XS = {z. \<exists>x xs. z = x # xs \<and> x \<in> A \<and> xs \<in> XS}"
+ "set_Cons A XS = {z. \<exists>x xs. z = x # xs \<and> x \<in> A \<and> xs \<in> XS}"
lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
by (auto simp add: set_Cons_def)
@@ -4229,17 +4229,17 @@
primrec -- {*The lexicographic ordering for lists of the specified length*}
lexn :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a list \<times> 'a list) set" where
- [code del]: "lexn r 0 = {}"
- | [code del]: "lexn r (Suc n) = (prod_fun (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
+ "lexn r 0 = {}"
+ | "lexn r (Suc n) = (prod_fun (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
{(xs, ys). length xs = Suc n \<and> length ys = Suc n}"
definition
lex :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
- [code del]: "lex r = (\<Union>n. lexn r n)" -- {*Holds only between lists of the same length*}
+ "lex r = (\<Union>n. lexn r n)" -- {*Holds only between lists of the same length*}
definition
lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" where
- [code del]: "lenlex r = inv_image (less_than <*lex*> lex r) (\<lambda>xs. (length xs, xs))"
+ "lenlex r = inv_image (less_than <*lex*> lex r) (\<lambda>xs. (length xs, xs))"
-- {*Compares lists by their length and then lexicographically*}
lemma wf_lexn: "wf r ==> wf (lexn r n)"
@@ -4313,7 +4313,7 @@
definition
lexord :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
- [code del]: "lexord r = {(x,y ). \<exists> a v. y = x @ a # v \<or>
+ "lexord r = {(x,y ). \<exists> a v. y = x @ a # v \<or>
(\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
lemma lexord_Nil_left[simp]: "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Matrix/Cplex.thy Mon Jul 12 11:21:56 2010 +0200
@@ -0,0 +1,66 @@
+(* Title: HOL/Matrix/cplex/Cplex.thy
+ Author: Steven Obua
+*)
+
+theory Cplex
+imports SparseMatrix LP ComputeFloat ComputeNumeral
+uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML"
+ "fspmlp.ML" ("matrixlp.ML")
+begin
+
+lemma spm_mult_le_dual_prts:
+ assumes
+ "sorted_sparse_matrix A1"
+ "sorted_sparse_matrix A2"
+ "sorted_sparse_matrix c1"
+ "sorted_sparse_matrix c2"
+ "sorted_sparse_matrix y"
+ "sorted_sparse_matrix r1"
+ "sorted_sparse_matrix r2"
+ "sorted_spvec b"
+ "le_spmat [] y"
+ "sparse_row_matrix A1 \<le> A"
+ "A \<le> sparse_row_matrix A2"
+ "sparse_row_matrix c1 \<le> c"
+ "c \<le> sparse_row_matrix c2"
+ "sparse_row_matrix r1 \<le> x"
+ "x \<le> sparse_row_matrix r2"
+ "A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)"
+ shows
+ "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b)
+ (let s1 = diff_spmat c1 (mult_spmat y A2); s2 = diff_spmat c2 (mult_spmat y A1) in
+ add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2)) (add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2))
+ (add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1)) (mult_spmat (nprt_spmat s1) (nprt_spmat r1))))))"
+ apply (simp add: Let_def)
+ apply (insert assms)
+ apply (simp add: sparse_row_matrix_op_simps algebra_simps)
+ apply (rule mult_le_dual_prts[where A=A, simplified Let_def algebra_simps])
+ apply (auto)
+ done
+
+lemma spm_mult_le_dual_prts_no_let:
+ assumes
+ "sorted_sparse_matrix A1"
+ "sorted_sparse_matrix A2"
+ "sorted_sparse_matrix c1"
+ "sorted_sparse_matrix c2"
+ "sorted_sparse_matrix y"
+ "sorted_sparse_matrix r1"
+ "sorted_sparse_matrix r2"
+ "sorted_spvec b"
+ "le_spmat [] y"
+ "sparse_row_matrix A1 \<le> A"
+ "A \<le> sparse_row_matrix A2"
+ "sparse_row_matrix c1 \<le> c"
+ "c \<le> sparse_row_matrix c2"
+ "sparse_row_matrix r1 \<le> x"
+ "x \<le> sparse_row_matrix r2"
+ "A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)"
+ shows
+ "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b)
+ (mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))"
+ by (simp add: assms mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
+
+use "matrixlp.ML"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Matrix/CplexMatrixConverter.ML Mon Jul 12 11:21:56 2010 +0200
@@ -0,0 +1,128 @@
+(* Title: HOL/Matrix/cplex/CplexMatrixConverter.ML
+ Author: Steven Obua
+*)
+
+signature MATRIX_BUILDER =
+sig
+ type vector
+ type matrix
+
+ val empty_vector : vector
+ val empty_matrix : matrix
+
+ exception Nat_expected of int
+ val set_elem : vector -> int -> string -> vector
+ val set_vector : matrix -> int -> vector -> matrix
+end;
+
+signature CPLEX_MATRIX_CONVERTER =
+sig
+ structure cplex : CPLEX
+ structure matrix_builder : MATRIX_BUILDER
+ type vector = matrix_builder.vector
+ type matrix = matrix_builder.matrix
+ type naming = int * (int -> string) * (string -> int)
+
+ exception Converter of string
+
+ (* program must fulfill is_normed_cplexProg and must be an element of the image of elim_nonfree_bounds *)
+ (* convert_prog maximize c A b naming *)
+ val convert_prog : cplex.cplexProg -> bool * vector * matrix * vector * naming
+
+ (* results must be optimal, converts_results returns the optimal value as string and the solution as vector *)
+ (* convert_results results name2index *)
+ val convert_results : cplex.cplexResult -> (string -> int) -> string * vector
+end;
+
+functor MAKE_CPLEX_MATRIX_CONVERTER (structure cplex: CPLEX and matrix_builder: MATRIX_BUILDER) : CPLEX_MATRIX_CONVERTER =
+struct
+
+structure cplex = cplex
+structure matrix_builder = matrix_builder
+type matrix = matrix_builder.matrix
+type vector = matrix_builder.vector
+type naming = int * (int -> string) * (string -> int)
+
+open matrix_builder
+open cplex
+
+exception Converter of string;
+
+fun neg_term (cplexNeg t) = t
+ | neg_term (cplexSum ts) = cplexSum (map neg_term ts)
+ | neg_term t = cplexNeg t
+
+fun convert_prog (cplexProg (s, goal, constrs, bounds)) =
+ let
+ fun build_naming index i2s s2i [] = (index, i2s, s2i)
+ | build_naming index i2s s2i (cplexBounds (cplexNeg cplexInf, cplexLeq, cplexVar v, cplexLeq, cplexInf)::bounds)
+ = build_naming (index+1) (Inttab.update (index, v) i2s) (Symtab.update_new (v, index) s2i) bounds
+ | build_naming _ _ _ _ = raise (Converter "nonfree bound")
+
+ val (varcount, i2s_tab, s2i_tab) = build_naming 0 Inttab.empty Symtab.empty bounds
+
+ fun i2s i = case Inttab.lookup i2s_tab i of NONE => raise (Converter "index not found")
+ | SOME n => n
+ fun s2i s = case Symtab.lookup s2i_tab s of NONE => raise (Converter ("name not found: "^s))
+ | SOME i => i
+ fun num2str positive (cplexNeg t) = num2str (not positive) t
+ | num2str positive (cplexNum num) = if positive then num else "-"^num
+ | num2str _ _ = raise (Converter "term is not a (possibly signed) number")
+
+ fun setprod vec positive (cplexNeg t) = setprod vec (not positive) t
+ | setprod vec positive (cplexVar v) = set_elem vec (s2i v) (if positive then "1" else "-1")
+ | setprod vec positive (cplexProd (cplexNum num, cplexVar v)) =
+ set_elem vec (s2i v) (if positive then num else "-"^num)
+ | setprod _ _ _ = raise (Converter "term is not a normed product")
+
+ fun sum2vec (cplexSum ts) = fold (fn t => fn vec => setprod vec true t) ts empty_vector
+ | sum2vec t = setprod empty_vector true t
+
+ fun constrs2Ab j A b [] = (A, b)
+ | constrs2Ab j A b ((_, cplexConstr (cplexLeq, (t1,t2)))::cs) =
+ constrs2Ab (j+1) (set_vector A j (sum2vec t1)) (set_elem b j (num2str true t2)) cs
+ | constrs2Ab j A b ((_, cplexConstr (cplexGeq, (t1,t2)))::cs) =
+ constrs2Ab (j+1) (set_vector A j (sum2vec (neg_term t1))) (set_elem b j (num2str true (neg_term t2))) cs
+ | constrs2Ab j A b ((_, cplexConstr (cplexEq, (t1,t2)))::cs) =
+ constrs2Ab j A b ((NONE, cplexConstr (cplexLeq, (t1,t2)))::
+ (NONE, cplexConstr (cplexGeq, (t1, t2)))::cs)
+ | constrs2Ab _ _ _ _ = raise (Converter "no strict constraints allowed")
+
+ val (A, b) = constrs2Ab 0 empty_matrix empty_vector constrs
+
+ val (goal_maximize, goal_term) =
+ case goal of
+ (cplexMaximize t) => (true, t)
+ | (cplexMinimize t) => (false, t)
+ in
+ (goal_maximize, sum2vec goal_term, A, b, (varcount, i2s, s2i))
+ end
+
+fun convert_results (cplex.Optimal (opt, entries)) name2index =
+ let
+ fun setv (name, value) v = matrix_builder.set_elem v (name2index name) value
+ in
+ (opt, fold setv entries (matrix_builder.empty_vector))
+ end
+ | convert_results _ _ = raise (Converter "No optimal result")
+
+end;
+
+structure SimpleMatrixBuilder : MATRIX_BUILDER =
+struct
+type vector = (int * string) list
+type matrix = (int * vector) list
+
+val empty_matrix = []
+val empty_vector = []
+
+exception Nat_expected of int;
+
+fun set_elem v i s = v @ [(i, s)]
+
+fun set_vector m i v = m @ [(i, v)]
+
+end;
+
+structure SimpleCplexMatrixConverter =
+ MAKE_CPLEX_MATRIX_CONVERTER(structure cplex = Cplex and matrix_builder = SimpleMatrixBuilder);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Matrix/Cplex_tools.ML Mon Jul 12 11:21:56 2010 +0200
@@ -0,0 +1,1225 @@
+(* Title: HOL/Matrix/cplex/Cplex_tools.ML
+ Author: Steven Obua
+*)
+
+signature CPLEX =
+sig
+
+ datatype cplexTerm = cplexVar of string | cplexNum of string | cplexInf
+ | cplexNeg of cplexTerm
+ | cplexProd of cplexTerm * cplexTerm
+ | cplexSum of (cplexTerm list)
+
+ datatype cplexComp = cplexLe | cplexLeq | cplexEq | cplexGe | cplexGeq
+
+ datatype cplexGoal = cplexMinimize of cplexTerm
+ | cplexMaximize of cplexTerm
+
+ datatype cplexConstr = cplexConstr of cplexComp *
+ (cplexTerm * cplexTerm)
+
+ datatype cplexBounds = cplexBounds of cplexTerm * cplexComp * cplexTerm
+ * cplexComp * cplexTerm
+ | cplexBound of cplexTerm * cplexComp * cplexTerm
+
+ datatype cplexProg = cplexProg of string
+ * cplexGoal
+ * ((string option * cplexConstr)
+ list)
+ * cplexBounds list
+
+ datatype cplexResult = Unbounded
+ | Infeasible
+ | Undefined
+ | Optimal of string *
+ (((* name *) string *
+ (* value *) string) list)
+
+ datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
+
+ exception Load_cplexFile of string
+ exception Load_cplexResult of string
+ exception Save_cplexFile of string
+ exception Execute of string
+
+ val load_cplexFile : string -> cplexProg
+
+ val save_cplexFile : string -> cplexProg -> unit
+
+ val elim_nonfree_bounds : cplexProg -> cplexProg
+
+ val relax_strict_ineqs : cplexProg -> cplexProg
+
+ val is_normed_cplexProg : cplexProg -> bool
+
+ val get_solver : unit -> cplexSolver
+ val set_solver : cplexSolver -> unit
+ val solve : cplexProg -> cplexResult
+end;
+
+structure Cplex : CPLEX =
+struct
+
+datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
+
+val cplexsolver = Unsynchronized.ref SOLVER_DEFAULT;
+fun get_solver () = !cplexsolver;
+fun set_solver s = (cplexsolver := s);
+
+exception Load_cplexFile of string;
+exception Load_cplexResult of string;
+exception Save_cplexFile of string;
+
+datatype cplexTerm = cplexVar of string
+ | cplexNum of string
+ | cplexInf
+ | cplexNeg of cplexTerm
+ | cplexProd of cplexTerm * cplexTerm
+ | cplexSum of (cplexTerm list)
+datatype cplexComp = cplexLe | cplexLeq | cplexEq | cplexGe | cplexGeq
+datatype cplexGoal = cplexMinimize of cplexTerm | cplexMaximize of cplexTerm
+datatype cplexConstr = cplexConstr of cplexComp * (cplexTerm * cplexTerm)
+datatype cplexBounds = cplexBounds of cplexTerm * cplexComp * cplexTerm
+ * cplexComp * cplexTerm
+ | cplexBound of cplexTerm * cplexComp * cplexTerm
+datatype cplexProg = cplexProg of string
+ * cplexGoal
+ * ((string option * cplexConstr) list)
+ * cplexBounds list
+
+fun rev_cmp cplexLe = cplexGe
+ | rev_cmp cplexLeq = cplexGeq
+ | rev_cmp cplexGe = cplexLe
+ | rev_cmp cplexGeq = cplexLeq
+ | rev_cmp cplexEq = cplexEq
+
+fun the NONE = raise (Load_cplexFile "SOME expected")
+ | the (SOME x) = x;
+
+fun modulo_signed is_something (cplexNeg u) = is_something u
+ | modulo_signed is_something u = is_something u
+
+fun is_Num (cplexNum _) = true
+ | is_Num _ = false
+
+fun is_Inf cplexInf = true
+ | is_Inf _ = false
+
+fun is_Var (cplexVar _) = true
+ | is_Var _ = false
+
+fun is_Neg (cplexNeg x ) = true
+ | is_Neg _ = false
+
+fun is_normed_Prod (cplexProd (t1, t2)) =
+ (is_Num t1) andalso (is_Var t2)
+ | is_normed_Prod x = is_Var x
+
+fun is_normed_Sum (cplexSum ts) =
+ (ts <> []) andalso forall (modulo_signed is_normed_Prod) ts
+ | is_normed_Sum x = modulo_signed is_normed_Prod x
+
+fun is_normed_Constr (cplexConstr (c, (t1, t2))) =
+ (is_normed_Sum t1) andalso (modulo_signed is_Num t2)
+
+fun is_Num_or_Inf x = is_Inf x orelse is_Num x
+
+fun is_normed_Bounds (cplexBounds (t1, c1, t2, c2, t3)) =
+ (c1 = cplexLe orelse c1 = cplexLeq) andalso
+ (c2 = cplexLe orelse c2 = cplexLeq) andalso
+ is_Var t2 andalso
+ modulo_signed is_Num_or_Inf t1 andalso
+ modulo_signed is_Num_or_Inf t3
+ | is_normed_Bounds (cplexBound (t1, c, t2)) =
+ (is_Var t1 andalso (modulo_signed is_Num_or_Inf t2))
+ orelse
+ (c <> cplexEq andalso
+ is_Var t2 andalso (modulo_signed is_Num_or_Inf t1))
+
+fun term_of_goal (cplexMinimize x) = x
+ | term_of_goal (cplexMaximize x) = x
+
+fun is_normed_cplexProg (cplexProg (name, goal, constraints, bounds)) =
+ is_normed_Sum (term_of_goal goal) andalso
+ forall (fn (_,x) => is_normed_Constr x) constraints andalso
+ forall is_normed_Bounds bounds
+
+fun is_NL s = s = "\n"
+
+fun is_blank s = forall (fn c => c <> #"\n" andalso Char.isSpace c) (String.explode s)
+
+fun is_num a =
+ let
+ val b = String.explode a
+ fun num4 cs = forall Char.isDigit cs
+ fun num3 [] = true
+ | num3 (ds as (c::cs)) =
+ if c = #"+" orelse c = #"-" then
+ num4 cs
+ else
+ num4 ds
+ fun num2 [] = true
+ | num2 (c::cs) =
+ if c = #"e" orelse c = #"E" then num3 cs
+ else (Char.isDigit c) andalso num2 cs
+ fun num1 [] = true
+ | num1 (c::cs) =
+ if c = #"." then num2 cs
+ else if c = #"e" orelse c = #"E" then num3 cs
+ else (Char.isDigit c) andalso num1 cs
+ fun num [] = true
+ | num (c::cs) =
+ if c = #"." then num2 cs
+ else (Char.isDigit c) andalso num1 cs
+ in
+ num b
+ end
+
+fun is_delimiter s = s = "+" orelse s = "-" orelse s = ":"
+
+fun is_cmp s = s = "<" orelse s = ">" orelse s = "<="
+ orelse s = ">=" orelse s = "="
+
+fun is_symbol a =
+ let
+ val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}|~"
+ fun is_symbol_char c = Char.isAlphaNum c orelse
+ exists (fn d => d=c) symbol_char
+ fun is_symbol_start c = is_symbol_char c andalso
+ not (Char.isDigit c) andalso
+ not (c= #".")
+ val b = String.explode a
+ in
+ b <> [] andalso is_symbol_start (hd b) andalso
+ forall is_symbol_char b
+ end
+
+fun to_upper s = String.implode (map Char.toUpper (String.explode s))
+
+fun keyword x =
+ let
+ val a = to_upper x
+ in
+ if a = "BOUNDS" orelse a = "BOUND" then
+ SOME "BOUNDS"
+ else if a = "MINIMIZE" orelse a = "MINIMUM" orelse a = "MIN" then
+ SOME "MINIMIZE"
+ else if a = "MAXIMIZE" orelse a = "MAXIMUM" orelse a = "MAX" then
+ SOME "MAXIMIZE"
+ else if a = "ST" orelse a = "S.T." orelse a = "ST." then
+ SOME "ST"
+ else if a = "FREE" orelse a = "END" then
+ SOME a
+ else if a = "GENERAL" orelse a = "GENERALS" orelse a = "GEN" then
+ SOME "GENERAL"
+ else if a = "INTEGER" orelse a = "INTEGERS" orelse a = "INT" then
+ SOME "INTEGER"
+ else if a = "BINARY" orelse a = "BINARIES" orelse a = "BIN" then
+ SOME "BINARY"
+ else if a = "INF" orelse a = "INFINITY" then
+ SOME "INF"
+ else
+ NONE
+ end
+
+val TOKEN_ERROR = ~1
+val TOKEN_BLANK = 0
+val TOKEN_NUM = 1
+val TOKEN_DELIMITER = 2
+val TOKEN_SYMBOL = 3
+val TOKEN_LABEL = 4
+val TOKEN_CMP = 5
+val TOKEN_KEYWORD = 6
+val TOKEN_NL = 7
+
+(* tokenize takes a list of chars as argument and returns a list of
+ int * string pairs, each string representing a "cplex token",
+ and each int being one of TOKEN_NUM, TOKEN_DELIMITER, TOKEN_CMP
+ or TOKEN_SYMBOL *)
+fun tokenize s =
+ let
+ val flist = [(is_NL, TOKEN_NL),
+ (is_blank, TOKEN_BLANK),
+ (is_num, TOKEN_NUM),
+ (is_delimiter, TOKEN_DELIMITER),
+ (is_cmp, TOKEN_CMP),
+ (is_symbol, TOKEN_SYMBOL)]
+ fun match_helper [] s = (fn x => false, TOKEN_ERROR)
+ | match_helper (f::fs) s =
+ if ((fst f) s) then f else match_helper fs s
+ fun match s = match_helper flist s
+ fun tok s =
+ if s = "" then [] else
+ let
+ val h = String.substring (s,0,1)
+ val (f, j) = match h
+ fun len i =
+ if size s = i then i
+ else if f (String.substring (s,0,i+1)) then
+ len (i+1)
+ else i
+ in
+ if j < 0 then
+ (if h = "\\" then []
+ else raise (Load_cplexFile ("token expected, found: "
+ ^s)))
+ else
+ let
+ val l = len 1
+ val u = String.substring (s,0,l)
+ val v = String.extract (s,l,NONE)
+ in
+ if j = 0 then tok v else (j, u) :: tok v
+ end
+ end
+ in
+ tok s
+ end
+
+exception Tokenize of string;
+
+fun tokenize_general flist s =
+ let
+ fun match_helper [] s = raise (Tokenize s)
+ | match_helper (f::fs) s =
+ if ((fst f) s) then f else match_helper fs s
+ fun match s = match_helper flist s
+ fun tok s =
+ if s = "" then [] else
+ let
+ val h = String.substring (s,0,1)
+ val (f, j) = match h
+ fun len i =
+ if size s = i then i
+ else if f (String.substring (s,0,i+1)) then
+ len (i+1)
+ else i
+ val l = len 1
+ in
+ (j, String.substring (s,0,l)) :: tok (String.extract (s,l,NONE))
+ end
+ in
+ tok s
+ end
+
+fun load_cplexFile name =
+ let
+ val f = TextIO.openIn name
+ val ignore_NL = Unsynchronized.ref true
+ val rest = Unsynchronized.ref []
+
+ fun is_symbol s c = (fst c) = TOKEN_SYMBOL andalso (to_upper (snd c)) = s
+
+ fun readToken_helper () =
+ if length (!rest) > 0 then
+ let val u = hd (!rest) in
+ (
+ rest := tl (!rest);
+ SOME u
+ )
+ end
+ else
+ (case TextIO.inputLine f of
+ NONE => NONE
+ | SOME s =>
+ let val t = tokenize s in
+ if (length t >= 2 andalso
+ snd(hd (tl t)) = ":")
+ then
+ rest := (TOKEN_LABEL, snd (hd t)) :: (tl (tl t))
+ else if (length t >= 2) andalso is_symbol "SUBJECT" (hd (t))
+ andalso is_symbol "TO" (hd (tl t))
+ then
+ rest := (TOKEN_SYMBOL, "ST") :: (tl (tl t))
+ else
+ rest := t;
+ readToken_helper ()
+ end)
+
+ fun readToken_helper2 () =
+ let val c = readToken_helper () in
+ if c = NONE then NONE
+ else if !ignore_NL andalso fst (the c) = TOKEN_NL then
+ readToken_helper2 ()
+ else if fst (the c) = TOKEN_SYMBOL
+ andalso keyword (snd (the c)) <> NONE
+ then SOME (TOKEN_KEYWORD, the (keyword (snd (the c))))
+ else c
+ end
+
+ fun readToken () = readToken_helper2 ()
+
+ fun pushToken a = rest := (a::(!rest))
+
+ fun is_value token =
+ fst token = TOKEN_NUM orelse (fst token = TOKEN_KEYWORD
+ andalso snd token = "INF")
+
+ fun get_value token =
+ if fst token = TOKEN_NUM then
+ cplexNum (snd token)
+ else if fst token = TOKEN_KEYWORD andalso snd token = "INF"
+ then
+ cplexInf
+ else
+ raise (Load_cplexFile "num expected")
+
+ fun readTerm_Product only_num =
+ let val c = readToken () in
+ if c = NONE then NONE
+ else if fst (the c) = TOKEN_SYMBOL
+ then (
+ if only_num then (pushToken (the c); NONE)
+ else SOME (cplexVar (snd (the c)))
+ )
+ else if only_num andalso is_value (the c) then
+ SOME (get_value (the c))
+ else if is_value (the c) then
+ let val t1 = get_value (the c)
+ val d = readToken ()
+ in
+ if d = NONE then SOME t1
+ else if fst (the d) = TOKEN_SYMBOL then
+ SOME (cplexProd (t1, cplexVar (snd (the d))))
+ else
+ (pushToken (the d); SOME t1)
+ end
+ else (pushToken (the c); NONE)
+ end
+
+ fun readTerm_Signed only_signed only_num =
+ let
+ val c = readToken ()
+ in
+ if c = NONE then NONE
+ else
+ let val d = the c in
+ if d = (TOKEN_DELIMITER, "+") then
+ readTerm_Product only_num
+ else if d = (TOKEN_DELIMITER, "-") then
+ SOME (cplexNeg (the (readTerm_Product
+ only_num)))
+ else (pushToken d;
+ if only_signed then NONE
+ else readTerm_Product only_num)
+ end
+ end
+
+ fun readTerm_Sum first_signed =
+ let val c = readTerm_Signed first_signed false in
+ if c = NONE then [] else (the c)::(readTerm_Sum true)
+ end
+
+ fun readTerm () =
+ let val c = readTerm_Sum false in
+ if c = [] then NONE
+ else if tl c = [] then SOME (hd c)
+ else SOME (cplexSum c)
+ end
+
+ fun readLabeledTerm () =
+ let val c = readToken () in
+ if c = NONE then (NONE, NONE)
+ else if fst (the c) = TOKEN_LABEL then
+ let val t = readTerm () in
+ if t = NONE then
+ raise (Load_cplexFile ("term after label "^
+ (snd (the c))^
+ " expected"))
+ else (SOME (snd (the c)), t)
+ end
+ else (pushToken (the c); (NONE, readTerm ()))
+ end
+
+ fun readGoal () =
+ let
+ val g = readToken ()
+ in
+ if g = SOME (TOKEN_KEYWORD, "MAXIMIZE") then
+ cplexMaximize (the (snd (readLabeledTerm ())))
+ else if g = SOME (TOKEN_KEYWORD, "MINIMIZE") then
+ cplexMinimize (the (snd (readLabeledTerm ())))
+ else raise (Load_cplexFile "MAXIMIZE or MINIMIZE expected")
+ end
+
+ fun str2cmp b =
+ (case b of
+ "<" => cplexLe
+ | "<=" => cplexLeq
+ | ">" => cplexGe
+ | ">=" => cplexGeq
+ | "=" => cplexEq
+ | _ => raise (Load_cplexFile (b^" is no TOKEN_CMP")))
+
+ fun readConstraint () =
+ let
+ val t = readLabeledTerm ()
+ fun make_constraint b t1 t2 =
+ cplexConstr
+ (str2cmp b,
+ (t1, t2))
+ in
+ if snd t = NONE then NONE
+ else
+ let val c = readToken () in
+ if c = NONE orelse fst (the c) <> TOKEN_CMP
+ then raise (Load_cplexFile "TOKEN_CMP expected")
+ else
+ let val n = readTerm_Signed false true in
+ if n = NONE then
+ raise (Load_cplexFile "num expected")
+ else
+ SOME (fst t,
+ make_constraint (snd (the c))
+ (the (snd t))
+ (the n))
+ end
+ end
+ end
+
+ fun readST () =
+ let
+ fun readbody () =
+ let val t = readConstraint () in
+ if t = NONE then []
+ else if (is_normed_Constr (snd (the t))) then
+ (the t)::(readbody ())
+ else if (fst (the t) <> NONE) then
+ raise (Load_cplexFile
+ ("constraint '"^(the (fst (the t)))^
+ "'is not normed"))
+ else
+ raise (Load_cplexFile
+ "constraint is not normed")
+ end
+ in
+ if readToken () = SOME (TOKEN_KEYWORD, "ST")
+ then
+ readbody ()
+ else
+ raise (Load_cplexFile "ST expected")
+ end
+
+ fun readCmp () =
+ let val c = readToken () in
+ if c = NONE then NONE
+ else if fst (the c) = TOKEN_CMP then
+ SOME (str2cmp (snd (the c)))
+ else (pushToken (the c); NONE)
+ end
+
+ fun skip_NL () =
+ let val c = readToken () in
+ if c <> NONE andalso fst (the c) = TOKEN_NL then
+ skip_NL ()
+ else
+ (pushToken (the c); ())
+ end
+
+ fun is_var (cplexVar _) = true
+ | is_var _ = false
+
+ fun make_bounds c t1 t2 =
+ cplexBound (t1, c, t2)
+
+ fun readBound () =
+ let
+ val _ = skip_NL ()
+ val t1 = readTerm ()
+ in
+ if t1 = NONE then NONE
+ else
+ let
+ val c1 = readCmp ()
+ in
+ if c1 = NONE then
+ let
+ val c = readToken ()
+ in
+ if c = SOME (TOKEN_KEYWORD, "FREE") then
+ SOME (
+ cplexBounds (cplexNeg cplexInf,
+ cplexLeq,
+ the t1,
+ cplexLeq,
+ cplexInf))
+ else
+ raise (Load_cplexFile "FREE expected")
+ end
+ else
+ let
+ val t2 = readTerm ()
+ in
+ if t2 = NONE then
+ raise (Load_cplexFile "term expected")
+ else
+ let val c2 = readCmp () in
+ if c2 = NONE then
+ SOME (make_bounds (the c1)
+ (the t1)
+ (the t2))
+ else
+ SOME (
+ cplexBounds (the t1,
+ the c1,
+ the t2,
+ the c2,
+ the (readTerm())))
+ end
+ end
+ end
+ end
+
+ fun readBounds () =
+ let
+ fun makestring b = "?"
+ fun readbody () =
+ let
+ val b = readBound ()
+ in
+ if b = NONE then []
+ else if (is_normed_Bounds (the b)) then
+ (the b)::(readbody())
+ else (
+ raise (Load_cplexFile
+ ("bounds are not normed in: "^
+ (makestring (the b)))))
+ end
+ in
+ if readToken () = SOME (TOKEN_KEYWORD, "BOUNDS") then
+ readbody ()
+ else raise (Load_cplexFile "BOUNDS expected")
+ end
+
+ fun readEnd () =
+ if readToken () = SOME (TOKEN_KEYWORD, "END") then ()
+ else raise (Load_cplexFile "END expected")
+
+ val result_Goal = readGoal ()
+ val result_ST = readST ()
+ val _ = ignore_NL := false
+ val result_Bounds = readBounds ()
+ val _ = ignore_NL := true
+ val _ = readEnd ()
+ val _ = TextIO.closeIn f
+ in
+ cplexProg (name, result_Goal, result_ST, result_Bounds)
+ end
+
+fun save_cplexFile filename (cplexProg (name, goal, constraints, bounds)) =
+ let
+ val f = TextIO.openOut filename
+
+ fun basic_write s = TextIO.output(f, s)
+
+ val linebuf = Unsynchronized.ref ""
+ fun buf_flushline s =
+ (basic_write (!linebuf);
+ basic_write "\n";
+ linebuf := s)
+ fun buf_add s = linebuf := (!linebuf) ^ s
+
+ fun write s =
+ if (String.size s) + (String.size (!linebuf)) >= 250 then
+ buf_flushline (" "^s)
+ else
+ buf_add s
+
+ fun writeln s = (buf_add s; buf_flushline "")
+
+ fun write_term (cplexVar x) = write x
+ | write_term (cplexNum x) = write x
+ | write_term cplexInf = write "inf"
+ | write_term (cplexProd (cplexNum "1", b)) = write_term b
+ | write_term (cplexProd (a, b)) =
+ (write_term a; write " "; write_term b)
+ | write_term (cplexNeg x) = (write " - "; write_term x)
+ | write_term (cplexSum ts) = write_terms ts
+ and write_terms [] = ()
+ | write_terms (t::ts) =
+ (if (not (is_Neg t)) then write " + " else ();
+ write_term t; write_terms ts)
+
+ fun write_goal (cplexMaximize term) =
+ (writeln "MAXIMIZE"; write_term term; writeln "")
+ | write_goal (cplexMinimize term) =
+ (writeln "MINIMIZE"; write_term term; writeln "")
+
+ fun write_cmp cplexLe = write "<"
+ | write_cmp cplexLeq = write "<="
+ | write_cmp cplexEq = write "="
+ | write_cmp cplexGe = write ">"
+ | write_cmp cplexGeq = write ">="
+
+ fun write_constr (cplexConstr (cmp, (a,b))) =
+ (write_term a;
+ write " ";
+ write_cmp cmp;
+ write " ";
+ write_term b)
+
+ fun write_constraints [] = ()
+ | write_constraints (c::cs) =
+ (if (fst c <> NONE)
+ then
+ (write (the (fst c)); write ": ")
+ else
+ ();
+ write_constr (snd c);
+ writeln "";
+ write_constraints cs)
+
+ fun write_bounds [] = ()
+ | write_bounds ((cplexBounds (t1,c1,t2,c2,t3))::bs) =
+ ((if t1 = cplexNeg cplexInf andalso t3 = cplexInf
+ andalso (c1 = cplexLeq orelse c1 = cplexLe)
+ andalso (c2 = cplexLeq orelse c2 = cplexLe)
+ then
+ (write_term t2; write " free")
+ else
+ (write_term t1; write " "; write_cmp c1; write " ";
+ write_term t2; write " "; write_cmp c2; write " ";
+ write_term t3)
+ ); writeln ""; write_bounds bs)
+ | write_bounds ((cplexBound (t1, c, t2)) :: bs) =
+ (write_term t1; write " ";
+ write_cmp c; write " ";
+ write_term t2; writeln ""; write_bounds bs)
+
+ val _ = write_goal goal
+ val _ = (writeln ""; writeln "ST")
+ val _ = write_constraints constraints
+ val _ = (writeln ""; writeln "BOUNDS")
+ val _ = write_bounds bounds
+ val _ = (writeln ""; writeln "END")
+ val _ = TextIO.closeOut f
+ in
+ ()
+ end
+
+fun norm_Constr (constr as cplexConstr (c, (t1, t2))) =
+ if not (modulo_signed is_Num t2) andalso
+ modulo_signed is_Num t1
+ then
+ [cplexConstr (rev_cmp c, (t2, t1))]
+ else if (c = cplexLe orelse c = cplexLeq) andalso
+ (t1 = (cplexNeg cplexInf) orelse t2 = cplexInf)
+ then
+ []
+ else if (c = cplexGe orelse c = cplexGeq) andalso
+ (t1 = cplexInf orelse t2 = cplexNeg cplexInf)
+ then
+ []
+ else
+ [constr]
+
+fun bound2constr (cplexBounds (t1,c1,t2,c2,t3)) =
+ (norm_Constr(cplexConstr (c1, (t1, t2))))
+ @ (norm_Constr(cplexConstr (c2, (t2, t3))))
+ | bound2constr (cplexBound (t1, cplexEq, t2)) =
+ (norm_Constr(cplexConstr (cplexLeq, (t1, t2))))
+ @ (norm_Constr(cplexConstr (cplexLeq, (t2, t1))))
+ | bound2constr (cplexBound (t1, c1, t2)) =
+ norm_Constr(cplexConstr (c1, (t1,t2)))
+
+val emptyset = Symtab.empty
+
+fun singleton v = Symtab.update (v, ()) emptyset
+
+fun merge a b = Symtab.merge (op =) (a, b)
+
+fun mergemap f ts = fold (fn x => fn table => merge table (f x)) ts Symtab.empty
+
+fun diff a b = Symtab.fold (Symtab.delete_safe o fst) b a
+
+fun collect_vars (cplexVar v) = singleton v
+ | collect_vars (cplexNeg t) = collect_vars t
+ | collect_vars (cplexProd (t1, t2)) =
+ merge (collect_vars t1) (collect_vars t2)
+ | collect_vars (cplexSum ts) = mergemap collect_vars ts
+ | collect_vars _ = emptyset
+
+(* Eliminates all nonfree bounds from the linear program and produces an
+ equivalent program with only free bounds
+ IF for the input program P holds: is_normed_cplexProg P *)
+fun elim_nonfree_bounds (cplexProg (name, goal, constraints, bounds)) =
+ let
+ fun collect_constr_vars (_, cplexConstr (c, (t1,_))) =
+ (collect_vars t1)
+
+ val cvars = merge (collect_vars (term_of_goal goal))
+ (mergemap collect_constr_vars constraints)
+
+ fun collect_lower_bounded_vars
+ (cplexBounds (t1, c1, cplexVar v, c2, t3)) =
+ singleton v
+ | collect_lower_bounded_vars
+ (cplexBound (_, cplexLe, cplexVar v)) =
+ singleton v
+ | collect_lower_bounded_vars
+ (cplexBound (_, cplexLeq, cplexVar v)) =
+ singleton v
+ | collect_lower_bounded_vars
+ (cplexBound (cplexVar v, cplexGe,_)) =
+ singleton v
+ | collect_lower_bounded_vars
+ (cplexBound (cplexVar v, cplexGeq, _)) =
+ singleton v
+ | collect_lower_bounded_vars
+ (cplexBound (cplexVar v, cplexEq, _)) =
+ singleton v
+ | collect_lower_bounded_vars _ = emptyset
+
+ val lvars = mergemap collect_lower_bounded_vars bounds
+ val positive_vars = diff cvars lvars
+ val zero = cplexNum "0"
+
+ fun make_pos_constr v =
+ (NONE, cplexConstr (cplexGeq, ((cplexVar v), zero)))
+
+ fun make_free_bound v =
+ cplexBounds (cplexNeg cplexInf, cplexLeq,
+ cplexVar v, cplexLeq,
+ cplexInf)
+
+ val pos_constrs = rev (Symtab.fold
+ (fn (k, v) => cons (make_pos_constr k))
+ positive_vars [])
+ val bound_constrs = map (pair NONE)
+ (maps bound2constr bounds)
+ val constraints' = constraints @ pos_constrs @ bound_constrs
+ val bounds' = rev (Symtab.fold (fn (v, _) => cons (make_free_bound v)) cvars []);
+ in
+ cplexProg (name, goal, constraints', bounds')
+ end
+
+fun relax_strict_ineqs (cplexProg (name, goals, constrs, bounds)) =
+ let
+ fun relax cplexLe = cplexLeq
+ | relax cplexGe = cplexGeq
+ | relax x = x
+
+ fun relax_constr (n, cplexConstr(c, (t1, t2))) =
+ (n, cplexConstr(relax c, (t1, t2)))
+
+ fun relax_bounds (cplexBounds (t1, c1, t2, c2, t3)) =
+ cplexBounds (t1, relax c1, t2, relax c2, t3)
+ | relax_bounds (cplexBound (t1, c, t2)) =
+ cplexBound (t1, relax c, t2)
+ in
+ cplexProg (name,
+ goals,
+ map relax_constr constrs,
+ map relax_bounds bounds)
+ end
+
+datatype cplexResult = Unbounded
+ | Infeasible
+ | Undefined
+ | Optimal of string * ((string * string) list)
+
+fun is_separator x = forall (fn c => c = #"-") (String.explode x)
+
+fun is_sign x = (x = "+" orelse x = "-")
+
+fun is_colon x = (x = ":")
+
+fun is_resultsymbol a =
+ let
+ val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}|~-"
+ fun is_symbol_char c = Char.isAlphaNum c orelse
+ exists (fn d => d=c) symbol_char
+ fun is_symbol_start c = is_symbol_char c andalso
+ not (Char.isDigit c) andalso
+ not (c= #".") andalso
+ not (c= #"-")
+ val b = String.explode a
+ in
+ b <> [] andalso is_symbol_start (hd b) andalso
+ forall is_symbol_char b
+ end
+
+val TOKEN_SIGN = 100
+val TOKEN_COLON = 101
+val TOKEN_SEPARATOR = 102
+
+fun load_glpkResult name =
+ let
+ val flist = [(is_NL, TOKEN_NL),
+ (is_blank, TOKEN_BLANK),
+ (is_num, TOKEN_NUM),
+ (is_sign, TOKEN_SIGN),
+ (is_colon, TOKEN_COLON),
+ (is_cmp, TOKEN_CMP),
+ (is_resultsymbol, TOKEN_SYMBOL),
+ (is_separator, TOKEN_SEPARATOR)]
+
+ val tokenize = tokenize_general flist
+
+ val f = TextIO.openIn name
+
+ val rest = Unsynchronized.ref []
+
+ fun readToken_helper () =
+ if length (!rest) > 0 then
+ let val u = hd (!rest) in
+ (
+ rest := tl (!rest);
+ SOME u
+ )
+ end
+ else
+ (case TextIO.inputLine f of
+ NONE => NONE
+ | SOME s => (rest := tokenize s; readToken_helper()))
+
+ fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty)
+
+ fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest)))
+
+ fun readToken () =
+ let val t = readToken_helper () in
+ if is_tt t TOKEN_BLANK then
+ readToken ()
+ else if is_tt t TOKEN_NL then
+ let val t2 = readToken_helper () in
+ if is_tt t2 TOKEN_SIGN then
+ (pushToken (SOME (TOKEN_SEPARATOR, "-")); t)
+ else
+ (pushToken t2; t)
+ end
+ else if is_tt t TOKEN_SIGN then
+ let val t2 = readToken_helper () in
+ if is_tt t2 TOKEN_NUM then
+ (SOME (TOKEN_NUM, (snd (the t))^(snd (the t2))))
+ else
+ (pushToken t2; t)
+ end
+ else
+ t
+ end
+
+ fun readRestOfLine P =
+ let
+ val t = readToken ()
+ in
+ if is_tt t TOKEN_NL orelse t = NONE
+ then P
+ else readRestOfLine P
+ end
+
+ fun readHeader () =
+ let
+ fun readStatus () = readRestOfLine ("STATUS", snd (the (readToken ())))
+ fun readObjective () = readRestOfLine ("OBJECTIVE", snd (the (readToken (); readToken (); readToken ())))
+ val t1 = readToken ()
+ val t2 = readToken ()
+ in
+ if is_tt t1 TOKEN_SYMBOL andalso is_tt t2 TOKEN_COLON
+ then
+ case to_upper (snd (the t1)) of
+ "STATUS" => (readStatus ())::(readHeader ())
+ | "OBJECTIVE" => (readObjective())::(readHeader ())
+ | _ => (readRestOfLine (); readHeader ())
+ else
+ (pushToken t2; pushToken t1; [])
+ end
+
+ fun skip_until_sep () =
+ let val x = readToken () in
+ if is_tt x TOKEN_SEPARATOR then
+ readRestOfLine ()
+ else
+ skip_until_sep ()
+ end
+
+ fun load_value () =
+ let
+ val t1 = readToken ()
+ val t2 = readToken ()
+ in
+ if is_tt t1 TOKEN_NUM andalso is_tt t2 TOKEN_SYMBOL then
+ let
+ val t = readToken ()
+ val state = if is_tt t TOKEN_NL then readToken () else t
+ val _ = if is_tt state TOKEN_SYMBOL then () else raise (Load_cplexResult "state expected")
+ val k = readToken ()
+ in
+ if is_tt k TOKEN_NUM then
+ readRestOfLine (SOME (snd (the t2), snd (the k)))
+ else
+ raise (Load_cplexResult "number expected")
+ end
+ else
+ (pushToken t2; pushToken t1; NONE)
+ end
+
+ fun load_values () =
+ let val v = load_value () in
+ if v = NONE then [] else (the v)::(load_values ())
+ end
+
+ val header = readHeader ()
+
+ val result =
+ case AList.lookup (op =) header "STATUS" of
+ SOME "INFEASIBLE" => Infeasible
+ | SOME "UNBOUNDED" => Unbounded
+ | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
+ (skip_until_sep ();
+ skip_until_sep ();
+ load_values ()))
+ | _ => Undefined
+
+ val _ = TextIO.closeIn f
+ in
+ result
+ end
+ handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
+ | Option => raise (Load_cplexResult "Option")
+ | x => raise x
+
+fun load_cplexResult name =
+ let
+ val flist = [(is_NL, TOKEN_NL),
+ (is_blank, TOKEN_BLANK),
+ (is_num, TOKEN_NUM),
+ (is_sign, TOKEN_SIGN),
+ (is_colon, TOKEN_COLON),
+ (is_cmp, TOKEN_CMP),
+ (is_resultsymbol, TOKEN_SYMBOL)]
+
+ val tokenize = tokenize_general flist
+
+ val f = TextIO.openIn name
+
+ val rest = Unsynchronized.ref []
+
+ fun readToken_helper () =
+ if length (!rest) > 0 then
+ let val u = hd (!rest) in
+ (
+ rest := tl (!rest);
+ SOME u
+ )
+ end
+ else
+ (case TextIO.inputLine f of
+ NONE => NONE
+ | SOME s => (rest := tokenize s; readToken_helper()))
+
+ fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty)
+
+ fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest)))
+
+ fun readToken () =
+ let val t = readToken_helper () in
+ if is_tt t TOKEN_BLANK then
+ readToken ()
+ else if is_tt t TOKEN_SIGN then
+ let val t2 = readToken_helper () in
+ if is_tt t2 TOKEN_NUM then
+ (SOME (TOKEN_NUM, (snd (the t))^(snd (the t2))))
+ else
+ (pushToken t2; t)
+ end
+ else
+ t
+ end
+
+ fun readRestOfLine P =
+ let
+ val t = readToken ()
+ in
+ if is_tt t TOKEN_NL orelse t = NONE
+ then P
+ else readRestOfLine P
+ end
+
+ fun readHeader () =
+ let
+ fun readStatus () = readRestOfLine ("STATUS", snd (the (readToken ())))
+ fun readObjective () =
+ let
+ val t = readToken ()
+ in
+ if is_tt t TOKEN_SYMBOL andalso to_upper (snd (the t)) = "VALUE" then
+ readRestOfLine ("OBJECTIVE", snd (the (readToken())))
+ else
+ readRestOfLine ("OBJECTIVE_NAME", snd (the t))
+ end
+
+ val t = readToken ()
+ in
+ if is_tt t TOKEN_SYMBOL then
+ case to_upper (snd (the t)) of
+ "STATUS" => (readStatus ())::(readHeader ())
+ | "OBJECTIVE" => (readObjective ())::(readHeader ())
+ | "SECTION" => (pushToken t; [])
+ | _ => (readRestOfLine (); readHeader ())
+ else
+ (readRestOfLine (); readHeader ())
+ end
+
+ fun skip_nls () =
+ let val x = readToken () in
+ if is_tt x TOKEN_NL then
+ skip_nls ()
+ else
+ (pushToken x; ())
+ end
+
+ fun skip_paragraph () =
+ if is_tt (readToken ()) TOKEN_NL then
+ (if is_tt (readToken ()) TOKEN_NL then
+ skip_nls ()
+ else
+ skip_paragraph ())
+ else
+ skip_paragraph ()
+
+ fun load_value () =
+ let
+ val t1 = readToken ()
+ val t1 = if is_tt t1 TOKEN_SYMBOL andalso snd (the t1) = "A" then readToken () else t1
+ in
+ if is_tt t1 TOKEN_NUM then
+ let
+ val name = readToken ()
+ val status = readToken ()
+ val value = readToken ()
+ in
+ if is_tt name TOKEN_SYMBOL andalso
+ is_tt status TOKEN_SYMBOL andalso
+ is_tt value TOKEN_NUM
+ then
+ readRestOfLine (SOME (snd (the name), snd (the value)))
+ else
+ raise (Load_cplexResult "column line expected")
+ end
+ else
+ (pushToken t1; NONE)
+ end
+
+ fun load_values () =
+ let val v = load_value () in
+ if v = NONE then [] else (the v)::(load_values ())
+ end
+
+ val header = readHeader ()
+
+ val result =
+ case AList.lookup (op =) header "STATUS" of
+ SOME "INFEASIBLE" => Infeasible
+ | SOME "NONOPTIMAL" => Unbounded
+ | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
+ (skip_paragraph ();
+ skip_paragraph ();
+ skip_paragraph ();
+ skip_paragraph ();
+ skip_paragraph ();
+ load_values ()))
+ | _ => Undefined
+
+ val _ = TextIO.closeIn f
+ in
+ result
+ end
+ handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
+ | Option => raise (Load_cplexResult "Option")
+ | x => raise x
+
+exception Execute of string;
+
+fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s])));
+fun wrap s = "\""^s^"\"";
+
+fun solve_glpk prog =
+ let
+ val name = LargeInt.toString (Time.toMicroseconds (Time.now ()))
+ val lpname = tmp_file (name^".lp")
+ val resultname = tmp_file (name^".txt")
+ val _ = save_cplexFile lpname prog
+ val cplex_path = getenv "GLPK_PATH"
+ val cplex = if cplex_path = "" then "glpsol" else cplex_path
+ val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
+ val answer = #1 (bash_output command)
+ in
+ let
+ val result = load_glpkResult resultname
+ val _ = OS.FileSys.remove lpname
+ val _ = OS.FileSys.remove resultname
+ in
+ result
+ end
+ handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer))
+ | _ => raise (Execute answer)
+ end
+
+fun solve_cplex prog =
+ let
+ fun write_script s lp r =
+ let
+ val f = TextIO.openOut s
+ val _ = TextIO.output (f, "read\n"^lp^"\noptimize\nwrite\n"^r^"\nquit")
+ val _ = TextIO.closeOut f
+ in
+ ()
+ end
+
+ val name = LargeInt.toString (Time.toMicroseconds (Time.now ()))
+ val lpname = tmp_file (name^".lp")
+ val resultname = tmp_file (name^".txt")
+ val scriptname = tmp_file (name^".script")
+ val _ = save_cplexFile lpname prog
+ val cplex_path = getenv "CPLEX_PATH"
+ val cplex = if cplex_path = "" then "cplex" else cplex_path
+ val _ = write_script scriptname lpname resultname
+ val command = (wrap cplex)^" < "^(wrap scriptname)^" > /dev/null"
+ val answer = "return code "^(Int.toString (bash command))
+ in
+ let
+ val result = load_cplexResult resultname
+ val _ = OS.FileSys.remove lpname
+ val _ = OS.FileSys.remove resultname
+ val _ = OS.FileSys.remove scriptname
+ in
+ result
+ end
+ end
+
+fun solve prog =
+ case get_solver () of
+ SOLVER_DEFAULT =>
+ (case getenv "LP_SOLVER" of
+ "CPLEX" => solve_cplex prog
+ | "GLPK" => solve_glpk prog
+ | _ => raise (Execute ("LP_SOLVER must be set to CPLEX or to GLPK")))
+ | SOLVER_CPLEX => solve_cplex prog
+ | SOLVER_GLPK => solve_glpk prog
+
+end;
+
+(*
+val demofile = "/home/obua/flyspeck/kepler/LP/cplexPent2.lp45"
+val demoout = "/home/obua/flyspeck/kepler/LP/test.out"
+val demoresult = "/home/obua/flyspeck/kepler/LP/try/test2.sol"
+
+fun loadcplex () = Cplex.relax_strict_ineqs
+ (Cplex.load_cplexFile demofile)
+
+fun writecplex lp = Cplex.save_cplexFile demoout lp
+
+fun test () =
+ let
+ val lp = loadcplex ()
+ val lp2 = Cplex.elim_nonfree_bounds lp
+ in
+ writecplex lp2
+ end
+
+fun loadresult () = Cplex.load_cplexResult demoresult;
+*)
+
+(*val prog = Cplex.load_cplexFile "/home/obua/tmp/pent/graph_0.lpt";
+val _ = Cplex.solve prog;*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Matrix/FloatSparseMatrixBuilder.ML Mon Jul 12 11:21:56 2010 +0200
@@ -0,0 +1,284 @@
+(* Title: HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
+ Author: Steven Obua
+*)
+
+signature FLOAT_SPARSE_MATIRX_BUILDER =
+sig
+ include MATRIX_BUILDER
+
+ structure cplex : CPLEX
+
+ type float = Float.float
+ val approx_value : int -> (float -> float) -> string -> term * term
+ val approx_vector : int -> (float -> float) -> vector -> term * term
+ val approx_matrix : int -> (float -> float) -> matrix -> term * term
+
+ val mk_spvec_entry : int -> float -> term
+ val mk_spvec_entry' : int -> term -> term
+ val mk_spmat_entry : int -> term -> term
+ val spvecT: typ
+ val spmatT: typ
+
+ val v_elem_at : vector -> int -> string option
+ val m_elem_at : matrix -> int -> vector option
+ val v_only_elem : vector -> int option
+ val v_fold : (int * string -> 'a -> 'a) -> vector -> 'a -> 'a
+ val m_fold : (int * vector -> 'a -> 'a) -> matrix -> 'a -> 'a
+
+ val transpose_matrix : matrix -> matrix
+
+ val cut_vector : int -> vector -> vector
+ val cut_matrix : vector -> int option -> matrix -> matrix
+
+ val delete_matrix : int list -> matrix -> matrix
+ val cut_matrix' : int list -> matrix -> matrix
+ val delete_vector : int list -> vector -> vector
+ val cut_vector' : int list -> vector -> vector
+
+ val indices_of_matrix : matrix -> int list
+ val indices_of_vector : vector -> int list
+
+ (* cplexProg c A b *)
+ val cplexProg : vector -> matrix -> vector -> cplex.cplexProg * (string -> int)
+ (* dual_cplexProg c A b *)
+ val dual_cplexProg : vector -> matrix -> vector -> cplex.cplexProg * (string -> int)
+end;
+
+structure FloatSparseMatrixBuilder : FLOAT_SPARSE_MATIRX_BUILDER =
+struct
+
+type float = Float.float
+structure Inttab = Table(type key = int val ord = rev_order o int_ord);
+
+type vector = string Inttab.table
+type matrix = vector Inttab.table
+
+val spvec_elemT = HOLogic.mk_prodT (HOLogic.natT, HOLogic.realT);
+val spvecT = HOLogic.listT spvec_elemT;
+val spmat_elemT = HOLogic.mk_prodT (HOLogic.natT, spvecT);
+val spmatT = HOLogic.listT spmat_elemT;
+
+fun approx_value prec f =
+ FloatArith.approx_float prec (fn (x, y) => (f x, f y));
+
+fun mk_spvec_entry i f =
+ HOLogic.mk_prod (HOLogic.mk_number HOLogic.natT i, FloatArith.mk_float f);
+
+fun mk_spvec_entry' i x =
+ HOLogic.mk_prod (HOLogic.mk_number HOLogic.natT i, x);
+
+fun mk_spmat_entry i e =
+ HOLogic.mk_prod (HOLogic.mk_number HOLogic.natT i, e);
+
+fun approx_vector prec pprt vector =
+ let
+ fun app (index, s) (lower, upper) =
+ let
+ val (flower, fupper) = approx_value prec pprt s
+ val index = HOLogic.mk_number HOLogic.natT index
+ val elower = HOLogic.mk_prod (index, flower)
+ val eupper = HOLogic.mk_prod (index, fupper)
+ in (elower :: lower, eupper :: upper) end;
+ in
+ pairself (HOLogic.mk_list spvec_elemT) (Inttab.fold app vector ([], []))
+ end;
+
+fun approx_matrix prec pprt vector =
+ let
+ fun app (index, v) (lower, upper) =
+ let
+ val (flower, fupper) = approx_vector prec pprt v
+ val index = HOLogic.mk_number HOLogic.natT index
+ val elower = HOLogic.mk_prod (index, flower)
+ val eupper = HOLogic.mk_prod (index, fupper)
+ in (elower :: lower, eupper :: upper) end;
+ in
+ pairself (HOLogic.mk_list spmat_elemT) (Inttab.fold app vector ([], []))
+ end;
+
+exception Nat_expected of int;
+
+val zero_interval = approx_value 1 I "0"
+
+fun set_elem vector index str =
+ if index < 0 then
+ raise (Nat_expected index)
+ else if (approx_value 1 I str) = zero_interval then
+ vector
+ else
+ Inttab.update (index, str) vector
+
+fun set_vector matrix index vector =
+ if index < 0 then
+ raise (Nat_expected index)
+ else if Inttab.is_empty vector then
+ matrix
+ else
+ Inttab.update (index, vector) matrix
+
+val empty_matrix = Inttab.empty
+val empty_vector = Inttab.empty
+
+(* dual stuff *)
+
+structure cplex = Cplex
+
+fun transpose_matrix matrix =
+ let
+ fun upd j (i, s) =
+ Inttab.map_default (i, Inttab.empty) (Inttab.update (j, s));
+ fun updm (j, v) = Inttab.fold (upd j) v;
+ in Inttab.fold updm matrix empty_matrix end;
+
+exception No_name of string;
+
+exception Superfluous_constr_right_hand_sides
+
+fun cplexProg c A b =
+ let
+ val ytable = Unsynchronized.ref Inttab.empty
+ fun indexof s =
+ if String.size s = 0 then raise (No_name s)
+ else case Int.fromString (String.extract(s, 1, NONE)) of
+ SOME i => i | NONE => raise (No_name s)
+
+ fun nameof i =
+ let
+ val s = "x"^(Int.toString i)
+ val _ = Unsynchronized.change ytable (Inttab.update (i, s))
+ in
+ s
+ end
+
+ fun split_numstr s =
+ if String.isPrefix "-" s then (false,String.extract(s, 1, NONE))
+ else if String.isPrefix "+" s then (true, String.extract(s, 1, NONE))
+ else (true, s)
+
+ fun mk_term index s =
+ let
+ val (p, s) = split_numstr s
+ val prod = cplex.cplexProd (cplex.cplexNum s, cplex.cplexVar (nameof index))
+ in
+ if p then prod else cplex.cplexNeg prod
+ end
+
+ fun vec2sum vector =
+ cplex.cplexSum (Inttab.fold (fn (index, s) => fn list => (mk_term index s) :: list) vector [])
+
+ fun mk_constr index vector c =
+ let
+ val s = case Inttab.lookup c index of SOME s => s | NONE => "0"
+ val (p, s) = split_numstr s
+ val num = if p then cplex.cplexNum s else cplex.cplexNeg (cplex.cplexNum s)
+ in
+ (NONE, cplex.cplexConstr (cplex.cplexLeq, (vec2sum vector, num)))
+ end
+
+ fun delete index c = Inttab.delete index c handle Inttab.UNDEF _ => c
+
+ val (list, b) = Inttab.fold
+ (fn (index, v) => fn (list, c) => ((mk_constr index v c)::list, delete index c))
+ A ([], b)
+ val _ = if Inttab.is_empty b then () else raise Superfluous_constr_right_hand_sides
+
+ fun mk_free y = cplex.cplexBounds (cplex.cplexNeg cplex.cplexInf, cplex.cplexLeq,
+ cplex.cplexVar y, cplex.cplexLeq,
+ cplex.cplexInf)
+
+ val yvars = Inttab.fold (fn (i, y) => fn l => (mk_free y)::l) (!ytable) []
+
+ val prog = cplex.cplexProg ("original", cplex.cplexMaximize (vec2sum c), list, yvars)
+ in
+ (prog, indexof)
+ end
+
+
+fun dual_cplexProg c A b =
+ let
+ fun indexof s =
+ if String.size s = 0 then raise (No_name s)
+ else case Int.fromString (String.extract(s, 1, NONE)) of
+ SOME i => i | NONE => raise (No_name s)
+
+ fun nameof i = "y"^(Int.toString i)
+
+ fun split_numstr s =
+ if String.isPrefix "-" s then (false,String.extract(s, 1, NONE))
+ else if String.isPrefix "+" s then (true, String.extract(s, 1, NONE))
+ else (true, s)
+
+ fun mk_term index s =
+ let
+ val (p, s) = split_numstr s
+ val prod = cplex.cplexProd (cplex.cplexNum s, cplex.cplexVar (nameof index))
+ in
+ if p then prod else cplex.cplexNeg prod
+ end
+
+ fun vec2sum vector =
+ cplex.cplexSum (Inttab.fold (fn (index, s) => fn list => (mk_term index s)::list) vector [])
+
+ fun mk_constr index vector c =
+ let
+ val s = case Inttab.lookup c index of SOME s => s | NONE => "0"
+ val (p, s) = split_numstr s
+ val num = if p then cplex.cplexNum s else cplex.cplexNeg (cplex.cplexNum s)
+ in
+ (NONE, cplex.cplexConstr (cplex.cplexEq, (vec2sum vector, num)))
+ end
+
+ fun delete index c = Inttab.delete index c handle Inttab.UNDEF _ => c
+
+ val (list, c) = Inttab.fold
+ (fn (index, v) => fn (list, c) => ((mk_constr index v c)::list, delete index c))
+ (transpose_matrix A) ([], c)
+ val _ = if Inttab.is_empty c then () else raise Superfluous_constr_right_hand_sides
+
+ val prog = cplex.cplexProg ("dual", cplex.cplexMinimize (vec2sum b), list, [])
+ in
+ (prog, indexof)
+ end
+
+fun cut_vector size v =
+ let
+ val count = Unsynchronized.ref 0;
+ fun app (i, s) = if (!count < size) then
+ (count := !count +1 ; Inttab.update (i, s))
+ else I
+ in
+ Inttab.fold app v empty_vector
+ end
+
+fun cut_matrix vfilter vsize m =
+ let
+ fun app (i, v) =
+ if is_none (Inttab.lookup vfilter i) then I
+ else case vsize
+ of NONE => Inttab.update (i, v)
+ | SOME s => Inttab.update (i, cut_vector s v)
+ in Inttab.fold app m empty_matrix end
+
+fun v_elem_at v i = Inttab.lookup v i
+fun m_elem_at m i = Inttab.lookup m i
+
+fun v_only_elem v =
+ case Inttab.min_key v of
+ NONE => NONE
+ | SOME vmin => (case Inttab.max_key v of
+ NONE => SOME vmin
+ | SOME vmax => if vmin = vmax then SOME vmin else NONE)
+
+fun v_fold f = Inttab.fold f;
+fun m_fold f = Inttab.fold f;
+
+fun indices_of_vector v = Inttab.keys v
+fun indices_of_matrix m = Inttab.keys m
+fun delete_vector indices v = fold Inttab.delete indices v
+fun delete_matrix indices m = fold Inttab.delete indices m
+fun cut_matrix' indices m = fold (fn i => fn m => (case Inttab.lookup m i of NONE => m | SOME v => Inttab.update (i, v) m)) indices Inttab.empty
+fun cut_vector' indices v = fold (fn i => fn v => (case Inttab.lookup v i of NONE => v | SOME x => Inttab.update (i, x) v)) indices Inttab.empty
+
+
+
+end;
--- a/src/HOL/Matrix/Matrix.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Matrix/Matrix.thy Mon Jul 12 11:21:56 2010 +0200
@@ -776,7 +776,7 @@
instantiation matrix :: (zero) zero
begin
-definition zero_matrix_def [code del]: "0 = Abs_matrix (\<lambda>j i. 0)"
+definition zero_matrix_def: "0 = Abs_matrix (\<lambda>j i. 0)"
instance ..
@@ -1459,9 +1459,9 @@
instantiation matrix :: ("{lattice, zero}") lattice
begin
-definition [code del]: "inf = combine_matrix inf"
+definition "inf = combine_matrix inf"
-definition [code del]: "sup = combine_matrix sup"
+definition "sup = combine_matrix sup"
instance
by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def)
@@ -1472,7 +1472,7 @@
begin
definition
- plus_matrix_def [code del]: "A + B = combine_matrix (op +) A B"
+ plus_matrix_def: "A + B = combine_matrix (op +) A B"
instance ..
@@ -1482,7 +1482,7 @@
begin
definition
- minus_matrix_def [code del]: "- A = apply_matrix uminus A"
+ minus_matrix_def: "- A = apply_matrix uminus A"
instance ..
@@ -1492,7 +1492,7 @@
begin
definition
- diff_matrix_def [code del]: "A - B = combine_matrix (op -) A B"
+ diff_matrix_def: "A - B = combine_matrix (op -) A B"
instance ..
@@ -1502,7 +1502,7 @@
begin
definition
- times_matrix_def [code del]: "A * B = mult_matrix (op *) (op +) A B"
+ times_matrix_def: "A * B = mult_matrix (op *) (op +) A B"
instance ..
@@ -1512,7 +1512,7 @@
begin
definition
- abs_matrix_def [code del]: "abs (A \<Colon> 'a matrix) = sup A (- A)"
+ abs_matrix_def: "abs (A \<Colon> 'a matrix) = sup A (- A)"
instance ..
--- a/src/HOL/Matrix/ROOT.ML Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Matrix/ROOT.ML Mon Jul 12 11:21:56 2010 +0200
@@ -1,1 +1,2 @@
-use_thys ["SparseMatrix", "cplex/Cplex"];
+
+use_thy "Cplex";
--- a/src/HOL/Matrix/cplex/Cplex.thy Mon Jul 12 11:21:27 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,66 +0,0 @@
-(* Title: HOL/Matrix/cplex/Cplex.thy
- Author: Steven Obua
-*)
-
-theory Cplex
-imports SparseMatrix LP ComputeFloat ComputeNumeral
-uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML"
- "fspmlp.ML" ("matrixlp.ML")
-begin
-
-lemma spm_mult_le_dual_prts:
- assumes
- "sorted_sparse_matrix A1"
- "sorted_sparse_matrix A2"
- "sorted_sparse_matrix c1"
- "sorted_sparse_matrix c2"
- "sorted_sparse_matrix y"
- "sorted_sparse_matrix r1"
- "sorted_sparse_matrix r2"
- "sorted_spvec b"
- "le_spmat [] y"
- "sparse_row_matrix A1 \<le> A"
- "A \<le> sparse_row_matrix A2"
- "sparse_row_matrix c1 \<le> c"
- "c \<le> sparse_row_matrix c2"
- "sparse_row_matrix r1 \<le> x"
- "x \<le> sparse_row_matrix r2"
- "A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)"
- shows
- "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b)
- (let s1 = diff_spmat c1 (mult_spmat y A2); s2 = diff_spmat c2 (mult_spmat y A1) in
- add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2)) (add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2))
- (add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1)) (mult_spmat (nprt_spmat s1) (nprt_spmat r1))))))"
- apply (simp add: Let_def)
- apply (insert assms)
- apply (simp add: sparse_row_matrix_op_simps algebra_simps)
- apply (rule mult_le_dual_prts[where A=A, simplified Let_def algebra_simps])
- apply (auto)
- done
-
-lemma spm_mult_le_dual_prts_no_let:
- assumes
- "sorted_sparse_matrix A1"
- "sorted_sparse_matrix A2"
- "sorted_sparse_matrix c1"
- "sorted_sparse_matrix c2"
- "sorted_sparse_matrix y"
- "sorted_sparse_matrix r1"
- "sorted_sparse_matrix r2"
- "sorted_spvec b"
- "le_spmat [] y"
- "sparse_row_matrix A1 \<le> A"
- "A \<le> sparse_row_matrix A2"
- "sparse_row_matrix c1 \<le> c"
- "c \<le> sparse_row_matrix c2"
- "sparse_row_matrix r1 \<le> x"
- "x \<le> sparse_row_matrix r2"
- "A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)"
- shows
- "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b)
- (mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))"
- by (simp add: assms mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
-
-use "matrixlp.ML"
-
-end
--- a/src/HOL/Matrix/cplex/CplexMatrixConverter.ML Mon Jul 12 11:21:27 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,128 +0,0 @@
-(* Title: HOL/Matrix/cplex/CplexMatrixConverter.ML
- Author: Steven Obua
-*)
-
-signature MATRIX_BUILDER =
-sig
- type vector
- type matrix
-
- val empty_vector : vector
- val empty_matrix : matrix
-
- exception Nat_expected of int
- val set_elem : vector -> int -> string -> vector
- val set_vector : matrix -> int -> vector -> matrix
-end;
-
-signature CPLEX_MATRIX_CONVERTER =
-sig
- structure cplex : CPLEX
- structure matrix_builder : MATRIX_BUILDER
- type vector = matrix_builder.vector
- type matrix = matrix_builder.matrix
- type naming = int * (int -> string) * (string -> int)
-
- exception Converter of string
-
- (* program must fulfill is_normed_cplexProg and must be an element of the image of elim_nonfree_bounds *)
- (* convert_prog maximize c A b naming *)
- val convert_prog : cplex.cplexProg -> bool * vector * matrix * vector * naming
-
- (* results must be optimal, converts_results returns the optimal value as string and the solution as vector *)
- (* convert_results results name2index *)
- val convert_results : cplex.cplexResult -> (string -> int) -> string * vector
-end;
-
-functor MAKE_CPLEX_MATRIX_CONVERTER (structure cplex: CPLEX and matrix_builder: MATRIX_BUILDER) : CPLEX_MATRIX_CONVERTER =
-struct
-
-structure cplex = cplex
-structure matrix_builder = matrix_builder
-type matrix = matrix_builder.matrix
-type vector = matrix_builder.vector
-type naming = int * (int -> string) * (string -> int)
-
-open matrix_builder
-open cplex
-
-exception Converter of string;
-
-fun neg_term (cplexNeg t) = t
- | neg_term (cplexSum ts) = cplexSum (map neg_term ts)
- | neg_term t = cplexNeg t
-
-fun convert_prog (cplexProg (s, goal, constrs, bounds)) =
- let
- fun build_naming index i2s s2i [] = (index, i2s, s2i)
- | build_naming index i2s s2i (cplexBounds (cplexNeg cplexInf, cplexLeq, cplexVar v, cplexLeq, cplexInf)::bounds)
- = build_naming (index+1) (Inttab.update (index, v) i2s) (Symtab.update_new (v, index) s2i) bounds
- | build_naming _ _ _ _ = raise (Converter "nonfree bound")
-
- val (varcount, i2s_tab, s2i_tab) = build_naming 0 Inttab.empty Symtab.empty bounds
-
- fun i2s i = case Inttab.lookup i2s_tab i of NONE => raise (Converter "index not found")
- | SOME n => n
- fun s2i s = case Symtab.lookup s2i_tab s of NONE => raise (Converter ("name not found: "^s))
- | SOME i => i
- fun num2str positive (cplexNeg t) = num2str (not positive) t
- | num2str positive (cplexNum num) = if positive then num else "-"^num
- | num2str _ _ = raise (Converter "term is not a (possibly signed) number")
-
- fun setprod vec positive (cplexNeg t) = setprod vec (not positive) t
- | setprod vec positive (cplexVar v) = set_elem vec (s2i v) (if positive then "1" else "-1")
- | setprod vec positive (cplexProd (cplexNum num, cplexVar v)) =
- set_elem vec (s2i v) (if positive then num else "-"^num)
- | setprod _ _ _ = raise (Converter "term is not a normed product")
-
- fun sum2vec (cplexSum ts) = fold (fn t => fn vec => setprod vec true t) ts empty_vector
- | sum2vec t = setprod empty_vector true t
-
- fun constrs2Ab j A b [] = (A, b)
- | constrs2Ab j A b ((_, cplexConstr (cplexLeq, (t1,t2)))::cs) =
- constrs2Ab (j+1) (set_vector A j (sum2vec t1)) (set_elem b j (num2str true t2)) cs
- | constrs2Ab j A b ((_, cplexConstr (cplexGeq, (t1,t2)))::cs) =
- constrs2Ab (j+1) (set_vector A j (sum2vec (neg_term t1))) (set_elem b j (num2str true (neg_term t2))) cs
- | constrs2Ab j A b ((_, cplexConstr (cplexEq, (t1,t2)))::cs) =
- constrs2Ab j A b ((NONE, cplexConstr (cplexLeq, (t1,t2)))::
- (NONE, cplexConstr (cplexGeq, (t1, t2)))::cs)
- | constrs2Ab _ _ _ _ = raise (Converter "no strict constraints allowed")
-
- val (A, b) = constrs2Ab 0 empty_matrix empty_vector constrs
-
- val (goal_maximize, goal_term) =
- case goal of
- (cplexMaximize t) => (true, t)
- | (cplexMinimize t) => (false, t)
- in
- (goal_maximize, sum2vec goal_term, A, b, (varcount, i2s, s2i))
- end
-
-fun convert_results (cplex.Optimal (opt, entries)) name2index =
- let
- fun setv (name, value) v = matrix_builder.set_elem v (name2index name) value
- in
- (opt, fold setv entries (matrix_builder.empty_vector))
- end
- | convert_results _ _ = raise (Converter "No optimal result")
-
-end;
-
-structure SimpleMatrixBuilder : MATRIX_BUILDER =
-struct
-type vector = (int * string) list
-type matrix = (int * vector) list
-
-val empty_matrix = []
-val empty_vector = []
-
-exception Nat_expected of int;
-
-fun set_elem v i s = v @ [(i, s)]
-
-fun set_vector m i v = m @ [(i, v)]
-
-end;
-
-structure SimpleCplexMatrixConverter =
- MAKE_CPLEX_MATRIX_CONVERTER(structure cplex = Cplex and matrix_builder = SimpleMatrixBuilder);
--- a/src/HOL/Matrix/cplex/Cplex_tools.ML Mon Jul 12 11:21:27 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1225 +0,0 @@
-(* Title: HOL/Matrix/cplex/Cplex_tools.ML
- Author: Steven Obua
-*)
-
-signature CPLEX =
-sig
-
- datatype cplexTerm = cplexVar of string | cplexNum of string | cplexInf
- | cplexNeg of cplexTerm
- | cplexProd of cplexTerm * cplexTerm
- | cplexSum of (cplexTerm list)
-
- datatype cplexComp = cplexLe | cplexLeq | cplexEq | cplexGe | cplexGeq
-
- datatype cplexGoal = cplexMinimize of cplexTerm
- | cplexMaximize of cplexTerm
-
- datatype cplexConstr = cplexConstr of cplexComp *
- (cplexTerm * cplexTerm)
-
- datatype cplexBounds = cplexBounds of cplexTerm * cplexComp * cplexTerm
- * cplexComp * cplexTerm
- | cplexBound of cplexTerm * cplexComp * cplexTerm
-
- datatype cplexProg = cplexProg of string
- * cplexGoal
- * ((string option * cplexConstr)
- list)
- * cplexBounds list
-
- datatype cplexResult = Unbounded
- | Infeasible
- | Undefined
- | Optimal of string *
- (((* name *) string *
- (* value *) string) list)
-
- datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
-
- exception Load_cplexFile of string
- exception Load_cplexResult of string
- exception Save_cplexFile of string
- exception Execute of string
-
- val load_cplexFile : string -> cplexProg
-
- val save_cplexFile : string -> cplexProg -> unit
-
- val elim_nonfree_bounds : cplexProg -> cplexProg
-
- val relax_strict_ineqs : cplexProg -> cplexProg
-
- val is_normed_cplexProg : cplexProg -> bool
-
- val get_solver : unit -> cplexSolver
- val set_solver : cplexSolver -> unit
- val solve : cplexProg -> cplexResult
-end;
-
-structure Cplex : CPLEX =
-struct
-
-datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
-
-val cplexsolver = Unsynchronized.ref SOLVER_DEFAULT;
-fun get_solver () = !cplexsolver;
-fun set_solver s = (cplexsolver := s);
-
-exception Load_cplexFile of string;
-exception Load_cplexResult of string;
-exception Save_cplexFile of string;
-
-datatype cplexTerm = cplexVar of string
- | cplexNum of string
- | cplexInf
- | cplexNeg of cplexTerm
- | cplexProd of cplexTerm * cplexTerm
- | cplexSum of (cplexTerm list)
-datatype cplexComp = cplexLe | cplexLeq | cplexEq | cplexGe | cplexGeq
-datatype cplexGoal = cplexMinimize of cplexTerm | cplexMaximize of cplexTerm
-datatype cplexConstr = cplexConstr of cplexComp * (cplexTerm * cplexTerm)
-datatype cplexBounds = cplexBounds of cplexTerm * cplexComp * cplexTerm
- * cplexComp * cplexTerm
- | cplexBound of cplexTerm * cplexComp * cplexTerm
-datatype cplexProg = cplexProg of string
- * cplexGoal
- * ((string option * cplexConstr) list)
- * cplexBounds list
-
-fun rev_cmp cplexLe = cplexGe
- | rev_cmp cplexLeq = cplexGeq
- | rev_cmp cplexGe = cplexLe
- | rev_cmp cplexGeq = cplexLeq
- | rev_cmp cplexEq = cplexEq
-
-fun the NONE = raise (Load_cplexFile "SOME expected")
- | the (SOME x) = x;
-
-fun modulo_signed is_something (cplexNeg u) = is_something u
- | modulo_signed is_something u = is_something u
-
-fun is_Num (cplexNum _) = true
- | is_Num _ = false
-
-fun is_Inf cplexInf = true
- | is_Inf _ = false
-
-fun is_Var (cplexVar _) = true
- | is_Var _ = false
-
-fun is_Neg (cplexNeg x ) = true
- | is_Neg _ = false
-
-fun is_normed_Prod (cplexProd (t1, t2)) =
- (is_Num t1) andalso (is_Var t2)
- | is_normed_Prod x = is_Var x
-
-fun is_normed_Sum (cplexSum ts) =
- (ts <> []) andalso forall (modulo_signed is_normed_Prod) ts
- | is_normed_Sum x = modulo_signed is_normed_Prod x
-
-fun is_normed_Constr (cplexConstr (c, (t1, t2))) =
- (is_normed_Sum t1) andalso (modulo_signed is_Num t2)
-
-fun is_Num_or_Inf x = is_Inf x orelse is_Num x
-
-fun is_normed_Bounds (cplexBounds (t1, c1, t2, c2, t3)) =
- (c1 = cplexLe orelse c1 = cplexLeq) andalso
- (c2 = cplexLe orelse c2 = cplexLeq) andalso
- is_Var t2 andalso
- modulo_signed is_Num_or_Inf t1 andalso
- modulo_signed is_Num_or_Inf t3
- | is_normed_Bounds (cplexBound (t1, c, t2)) =
- (is_Var t1 andalso (modulo_signed is_Num_or_Inf t2))
- orelse
- (c <> cplexEq andalso
- is_Var t2 andalso (modulo_signed is_Num_or_Inf t1))
-
-fun term_of_goal (cplexMinimize x) = x
- | term_of_goal (cplexMaximize x) = x
-
-fun is_normed_cplexProg (cplexProg (name, goal, constraints, bounds)) =
- is_normed_Sum (term_of_goal goal) andalso
- forall (fn (_,x) => is_normed_Constr x) constraints andalso
- forall is_normed_Bounds bounds
-
-fun is_NL s = s = "\n"
-
-fun is_blank s = forall (fn c => c <> #"\n" andalso Char.isSpace c) (String.explode s)
-
-fun is_num a =
- let
- val b = String.explode a
- fun num4 cs = forall Char.isDigit cs
- fun num3 [] = true
- | num3 (ds as (c::cs)) =
- if c = #"+" orelse c = #"-" then
- num4 cs
- else
- num4 ds
- fun num2 [] = true
- | num2 (c::cs) =
- if c = #"e" orelse c = #"E" then num3 cs
- else (Char.isDigit c) andalso num2 cs
- fun num1 [] = true
- | num1 (c::cs) =
- if c = #"." then num2 cs
- else if c = #"e" orelse c = #"E" then num3 cs
- else (Char.isDigit c) andalso num1 cs
- fun num [] = true
- | num (c::cs) =
- if c = #"." then num2 cs
- else (Char.isDigit c) andalso num1 cs
- in
- num b
- end
-
-fun is_delimiter s = s = "+" orelse s = "-" orelse s = ":"
-
-fun is_cmp s = s = "<" orelse s = ">" orelse s = "<="
- orelse s = ">=" orelse s = "="
-
-fun is_symbol a =
- let
- val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}|~"
- fun is_symbol_char c = Char.isAlphaNum c orelse
- exists (fn d => d=c) symbol_char
- fun is_symbol_start c = is_symbol_char c andalso
- not (Char.isDigit c) andalso
- not (c= #".")
- val b = String.explode a
- in
- b <> [] andalso is_symbol_start (hd b) andalso
- forall is_symbol_char b
- end
-
-fun to_upper s = String.implode (map Char.toUpper (String.explode s))
-
-fun keyword x =
- let
- val a = to_upper x
- in
- if a = "BOUNDS" orelse a = "BOUND" then
- SOME "BOUNDS"
- else if a = "MINIMIZE" orelse a = "MINIMUM" orelse a = "MIN" then
- SOME "MINIMIZE"
- else if a = "MAXIMIZE" orelse a = "MAXIMUM" orelse a = "MAX" then
- SOME "MAXIMIZE"
- else if a = "ST" orelse a = "S.T." orelse a = "ST." then
- SOME "ST"
- else if a = "FREE" orelse a = "END" then
- SOME a
- else if a = "GENERAL" orelse a = "GENERALS" orelse a = "GEN" then
- SOME "GENERAL"
- else if a = "INTEGER" orelse a = "INTEGERS" orelse a = "INT" then
- SOME "INTEGER"
- else if a = "BINARY" orelse a = "BINARIES" orelse a = "BIN" then
- SOME "BINARY"
- else if a = "INF" orelse a = "INFINITY" then
- SOME "INF"
- else
- NONE
- end
-
-val TOKEN_ERROR = ~1
-val TOKEN_BLANK = 0
-val TOKEN_NUM = 1
-val TOKEN_DELIMITER = 2
-val TOKEN_SYMBOL = 3
-val TOKEN_LABEL = 4
-val TOKEN_CMP = 5
-val TOKEN_KEYWORD = 6
-val TOKEN_NL = 7
-
-(* tokenize takes a list of chars as argument and returns a list of
- int * string pairs, each string representing a "cplex token",
- and each int being one of TOKEN_NUM, TOKEN_DELIMITER, TOKEN_CMP
- or TOKEN_SYMBOL *)
-fun tokenize s =
- let
- val flist = [(is_NL, TOKEN_NL),
- (is_blank, TOKEN_BLANK),
- (is_num, TOKEN_NUM),
- (is_delimiter, TOKEN_DELIMITER),
- (is_cmp, TOKEN_CMP),
- (is_symbol, TOKEN_SYMBOL)]
- fun match_helper [] s = (fn x => false, TOKEN_ERROR)
- | match_helper (f::fs) s =
- if ((fst f) s) then f else match_helper fs s
- fun match s = match_helper flist s
- fun tok s =
- if s = "" then [] else
- let
- val h = String.substring (s,0,1)
- val (f, j) = match h
- fun len i =
- if size s = i then i
- else if f (String.substring (s,0,i+1)) then
- len (i+1)
- else i
- in
- if j < 0 then
- (if h = "\\" then []
- else raise (Load_cplexFile ("token expected, found: "
- ^s)))
- else
- let
- val l = len 1
- val u = String.substring (s,0,l)
- val v = String.extract (s,l,NONE)
- in
- if j = 0 then tok v else (j, u) :: tok v
- end
- end
- in
- tok s
- end
-
-exception Tokenize of string;
-
-fun tokenize_general flist s =
- let
- fun match_helper [] s = raise (Tokenize s)
- | match_helper (f::fs) s =
- if ((fst f) s) then f else match_helper fs s
- fun match s = match_helper flist s
- fun tok s =
- if s = "" then [] else
- let
- val h = String.substring (s,0,1)
- val (f, j) = match h
- fun len i =
- if size s = i then i
- else if f (String.substring (s,0,i+1)) then
- len (i+1)
- else i
- val l = len 1
- in
- (j, String.substring (s,0,l)) :: tok (String.extract (s,l,NONE))
- end
- in
- tok s
- end
-
-fun load_cplexFile name =
- let
- val f = TextIO.openIn name
- val ignore_NL = Unsynchronized.ref true
- val rest = Unsynchronized.ref []
-
- fun is_symbol s c = (fst c) = TOKEN_SYMBOL andalso (to_upper (snd c)) = s
-
- fun readToken_helper () =
- if length (!rest) > 0 then
- let val u = hd (!rest) in
- (
- rest := tl (!rest);
- SOME u
- )
- end
- else
- (case TextIO.inputLine f of
- NONE => NONE
- | SOME s =>
- let val t = tokenize s in
- if (length t >= 2 andalso
- snd(hd (tl t)) = ":")
- then
- rest := (TOKEN_LABEL, snd (hd t)) :: (tl (tl t))
- else if (length t >= 2) andalso is_symbol "SUBJECT" (hd (t))
- andalso is_symbol "TO" (hd (tl t))
- then
- rest := (TOKEN_SYMBOL, "ST") :: (tl (tl t))
- else
- rest := t;
- readToken_helper ()
- end)
-
- fun readToken_helper2 () =
- let val c = readToken_helper () in
- if c = NONE then NONE
- else if !ignore_NL andalso fst (the c) = TOKEN_NL then
- readToken_helper2 ()
- else if fst (the c) = TOKEN_SYMBOL
- andalso keyword (snd (the c)) <> NONE
- then SOME (TOKEN_KEYWORD, the (keyword (snd (the c))))
- else c
- end
-
- fun readToken () = readToken_helper2 ()
-
- fun pushToken a = rest := (a::(!rest))
-
- fun is_value token =
- fst token = TOKEN_NUM orelse (fst token = TOKEN_KEYWORD
- andalso snd token = "INF")
-
- fun get_value token =
- if fst token = TOKEN_NUM then
- cplexNum (snd token)
- else if fst token = TOKEN_KEYWORD andalso snd token = "INF"
- then
- cplexInf
- else
- raise (Load_cplexFile "num expected")
-
- fun readTerm_Product only_num =
- let val c = readToken () in
- if c = NONE then NONE
- else if fst (the c) = TOKEN_SYMBOL
- then (
- if only_num then (pushToken (the c); NONE)
- else SOME (cplexVar (snd (the c)))
- )
- else if only_num andalso is_value (the c) then
- SOME (get_value (the c))
- else if is_value (the c) then
- let val t1 = get_value (the c)
- val d = readToken ()
- in
- if d = NONE then SOME t1
- else if fst (the d) = TOKEN_SYMBOL then
- SOME (cplexProd (t1, cplexVar (snd (the d))))
- else
- (pushToken (the d); SOME t1)
- end
- else (pushToken (the c); NONE)
- end
-
- fun readTerm_Signed only_signed only_num =
- let
- val c = readToken ()
- in
- if c = NONE then NONE
- else
- let val d = the c in
- if d = (TOKEN_DELIMITER, "+") then
- readTerm_Product only_num
- else if d = (TOKEN_DELIMITER, "-") then
- SOME (cplexNeg (the (readTerm_Product
- only_num)))
- else (pushToken d;
- if only_signed then NONE
- else readTerm_Product only_num)
- end
- end
-
- fun readTerm_Sum first_signed =
- let val c = readTerm_Signed first_signed false in
- if c = NONE then [] else (the c)::(readTerm_Sum true)
- end
-
- fun readTerm () =
- let val c = readTerm_Sum false in
- if c = [] then NONE
- else if tl c = [] then SOME (hd c)
- else SOME (cplexSum c)
- end
-
- fun readLabeledTerm () =
- let val c = readToken () in
- if c = NONE then (NONE, NONE)
- else if fst (the c) = TOKEN_LABEL then
- let val t = readTerm () in
- if t = NONE then
- raise (Load_cplexFile ("term after label "^
- (snd (the c))^
- " expected"))
- else (SOME (snd (the c)), t)
- end
- else (pushToken (the c); (NONE, readTerm ()))
- end
-
- fun readGoal () =
- let
- val g = readToken ()
- in
- if g = SOME (TOKEN_KEYWORD, "MAXIMIZE") then
- cplexMaximize (the (snd (readLabeledTerm ())))
- else if g = SOME (TOKEN_KEYWORD, "MINIMIZE") then
- cplexMinimize (the (snd (readLabeledTerm ())))
- else raise (Load_cplexFile "MAXIMIZE or MINIMIZE expected")
- end
-
- fun str2cmp b =
- (case b of
- "<" => cplexLe
- | "<=" => cplexLeq
- | ">" => cplexGe
- | ">=" => cplexGeq
- | "=" => cplexEq
- | _ => raise (Load_cplexFile (b^" is no TOKEN_CMP")))
-
- fun readConstraint () =
- let
- val t = readLabeledTerm ()
- fun make_constraint b t1 t2 =
- cplexConstr
- (str2cmp b,
- (t1, t2))
- in
- if snd t = NONE then NONE
- else
- let val c = readToken () in
- if c = NONE orelse fst (the c) <> TOKEN_CMP
- then raise (Load_cplexFile "TOKEN_CMP expected")
- else
- let val n = readTerm_Signed false true in
- if n = NONE then
- raise (Load_cplexFile "num expected")
- else
- SOME (fst t,
- make_constraint (snd (the c))
- (the (snd t))
- (the n))
- end
- end
- end
-
- fun readST () =
- let
- fun readbody () =
- let val t = readConstraint () in
- if t = NONE then []
- else if (is_normed_Constr (snd (the t))) then
- (the t)::(readbody ())
- else if (fst (the t) <> NONE) then
- raise (Load_cplexFile
- ("constraint '"^(the (fst (the t)))^
- "'is not normed"))
- else
- raise (Load_cplexFile
- "constraint is not normed")
- end
- in
- if readToken () = SOME (TOKEN_KEYWORD, "ST")
- then
- readbody ()
- else
- raise (Load_cplexFile "ST expected")
- end
-
- fun readCmp () =
- let val c = readToken () in
- if c = NONE then NONE
- else if fst (the c) = TOKEN_CMP then
- SOME (str2cmp (snd (the c)))
- else (pushToken (the c); NONE)
- end
-
- fun skip_NL () =
- let val c = readToken () in
- if c <> NONE andalso fst (the c) = TOKEN_NL then
- skip_NL ()
- else
- (pushToken (the c); ())
- end
-
- fun is_var (cplexVar _) = true
- | is_var _ = false
-
- fun make_bounds c t1 t2 =
- cplexBound (t1, c, t2)
-
- fun readBound () =
- let
- val _ = skip_NL ()
- val t1 = readTerm ()
- in
- if t1 = NONE then NONE
- else
- let
- val c1 = readCmp ()
- in
- if c1 = NONE then
- let
- val c = readToken ()
- in
- if c = SOME (TOKEN_KEYWORD, "FREE") then
- SOME (
- cplexBounds (cplexNeg cplexInf,
- cplexLeq,
- the t1,
- cplexLeq,
- cplexInf))
- else
- raise (Load_cplexFile "FREE expected")
- end
- else
- let
- val t2 = readTerm ()
- in
- if t2 = NONE then
- raise (Load_cplexFile "term expected")
- else
- let val c2 = readCmp () in
- if c2 = NONE then
- SOME (make_bounds (the c1)
- (the t1)
- (the t2))
- else
- SOME (
- cplexBounds (the t1,
- the c1,
- the t2,
- the c2,
- the (readTerm())))
- end
- end
- end
- end
-
- fun readBounds () =
- let
- fun makestring b = "?"
- fun readbody () =
- let
- val b = readBound ()
- in
- if b = NONE then []
- else if (is_normed_Bounds (the b)) then
- (the b)::(readbody())
- else (
- raise (Load_cplexFile
- ("bounds are not normed in: "^
- (makestring (the b)))))
- end
- in
- if readToken () = SOME (TOKEN_KEYWORD, "BOUNDS") then
- readbody ()
- else raise (Load_cplexFile "BOUNDS expected")
- end
-
- fun readEnd () =
- if readToken () = SOME (TOKEN_KEYWORD, "END") then ()
- else raise (Load_cplexFile "END expected")
-
- val result_Goal = readGoal ()
- val result_ST = readST ()
- val _ = ignore_NL := false
- val result_Bounds = readBounds ()
- val _ = ignore_NL := true
- val _ = readEnd ()
- val _ = TextIO.closeIn f
- in
- cplexProg (name, result_Goal, result_ST, result_Bounds)
- end
-
-fun save_cplexFile filename (cplexProg (name, goal, constraints, bounds)) =
- let
- val f = TextIO.openOut filename
-
- fun basic_write s = TextIO.output(f, s)
-
- val linebuf = Unsynchronized.ref ""
- fun buf_flushline s =
- (basic_write (!linebuf);
- basic_write "\n";
- linebuf := s)
- fun buf_add s = linebuf := (!linebuf) ^ s
-
- fun write s =
- if (String.size s) + (String.size (!linebuf)) >= 250 then
- buf_flushline (" "^s)
- else
- buf_add s
-
- fun writeln s = (buf_add s; buf_flushline "")
-
- fun write_term (cplexVar x) = write x
- | write_term (cplexNum x) = write x
- | write_term cplexInf = write "inf"
- | write_term (cplexProd (cplexNum "1", b)) = write_term b
- | write_term (cplexProd (a, b)) =
- (write_term a; write " "; write_term b)
- | write_term (cplexNeg x) = (write " - "; write_term x)
- | write_term (cplexSum ts) = write_terms ts
- and write_terms [] = ()
- | write_terms (t::ts) =
- (if (not (is_Neg t)) then write " + " else ();
- write_term t; write_terms ts)
-
- fun write_goal (cplexMaximize term) =
- (writeln "MAXIMIZE"; write_term term; writeln "")
- | write_goal (cplexMinimize term) =
- (writeln "MINIMIZE"; write_term term; writeln "")
-
- fun write_cmp cplexLe = write "<"
- | write_cmp cplexLeq = write "<="
- | write_cmp cplexEq = write "="
- | write_cmp cplexGe = write ">"
- | write_cmp cplexGeq = write ">="
-
- fun write_constr (cplexConstr (cmp, (a,b))) =
- (write_term a;
- write " ";
- write_cmp cmp;
- write " ";
- write_term b)
-
- fun write_constraints [] = ()
- | write_constraints (c::cs) =
- (if (fst c <> NONE)
- then
- (write (the (fst c)); write ": ")
- else
- ();
- write_constr (snd c);
- writeln "";
- write_constraints cs)
-
- fun write_bounds [] = ()
- | write_bounds ((cplexBounds (t1,c1,t2,c2,t3))::bs) =
- ((if t1 = cplexNeg cplexInf andalso t3 = cplexInf
- andalso (c1 = cplexLeq orelse c1 = cplexLe)
- andalso (c2 = cplexLeq orelse c2 = cplexLe)
- then
- (write_term t2; write " free")
- else
- (write_term t1; write " "; write_cmp c1; write " ";
- write_term t2; write " "; write_cmp c2; write " ";
- write_term t3)
- ); writeln ""; write_bounds bs)
- | write_bounds ((cplexBound (t1, c, t2)) :: bs) =
- (write_term t1; write " ";
- write_cmp c; write " ";
- write_term t2; writeln ""; write_bounds bs)
-
- val _ = write_goal goal
- val _ = (writeln ""; writeln "ST")
- val _ = write_constraints constraints
- val _ = (writeln ""; writeln "BOUNDS")
- val _ = write_bounds bounds
- val _ = (writeln ""; writeln "END")
- val _ = TextIO.closeOut f
- in
- ()
- end
-
-fun norm_Constr (constr as cplexConstr (c, (t1, t2))) =
- if not (modulo_signed is_Num t2) andalso
- modulo_signed is_Num t1
- then
- [cplexConstr (rev_cmp c, (t2, t1))]
- else if (c = cplexLe orelse c = cplexLeq) andalso
- (t1 = (cplexNeg cplexInf) orelse t2 = cplexInf)
- then
- []
- else if (c = cplexGe orelse c = cplexGeq) andalso
- (t1 = cplexInf orelse t2 = cplexNeg cplexInf)
- then
- []
- else
- [constr]
-
-fun bound2constr (cplexBounds (t1,c1,t2,c2,t3)) =
- (norm_Constr(cplexConstr (c1, (t1, t2))))
- @ (norm_Constr(cplexConstr (c2, (t2, t3))))
- | bound2constr (cplexBound (t1, cplexEq, t2)) =
- (norm_Constr(cplexConstr (cplexLeq, (t1, t2))))
- @ (norm_Constr(cplexConstr (cplexLeq, (t2, t1))))
- | bound2constr (cplexBound (t1, c1, t2)) =
- norm_Constr(cplexConstr (c1, (t1,t2)))
-
-val emptyset = Symtab.empty
-
-fun singleton v = Symtab.update (v, ()) emptyset
-
-fun merge a b = Symtab.merge (op =) (a, b)
-
-fun mergemap f ts = fold (fn x => fn table => merge table (f x)) ts Symtab.empty
-
-fun diff a b = Symtab.fold (Symtab.delete_safe o fst) b a
-
-fun collect_vars (cplexVar v) = singleton v
- | collect_vars (cplexNeg t) = collect_vars t
- | collect_vars (cplexProd (t1, t2)) =
- merge (collect_vars t1) (collect_vars t2)
- | collect_vars (cplexSum ts) = mergemap collect_vars ts
- | collect_vars _ = emptyset
-
-(* Eliminates all nonfree bounds from the linear program and produces an
- equivalent program with only free bounds
- IF for the input program P holds: is_normed_cplexProg P *)
-fun elim_nonfree_bounds (cplexProg (name, goal, constraints, bounds)) =
- let
- fun collect_constr_vars (_, cplexConstr (c, (t1,_))) =
- (collect_vars t1)
-
- val cvars = merge (collect_vars (term_of_goal goal))
- (mergemap collect_constr_vars constraints)
-
- fun collect_lower_bounded_vars
- (cplexBounds (t1, c1, cplexVar v, c2, t3)) =
- singleton v
- | collect_lower_bounded_vars
- (cplexBound (_, cplexLe, cplexVar v)) =
- singleton v
- | collect_lower_bounded_vars
- (cplexBound (_, cplexLeq, cplexVar v)) =
- singleton v
- | collect_lower_bounded_vars
- (cplexBound (cplexVar v, cplexGe,_)) =
- singleton v
- | collect_lower_bounded_vars
- (cplexBound (cplexVar v, cplexGeq, _)) =
- singleton v
- | collect_lower_bounded_vars
- (cplexBound (cplexVar v, cplexEq, _)) =
- singleton v
- | collect_lower_bounded_vars _ = emptyset
-
- val lvars = mergemap collect_lower_bounded_vars bounds
- val positive_vars = diff cvars lvars
- val zero = cplexNum "0"
-
- fun make_pos_constr v =
- (NONE, cplexConstr (cplexGeq, ((cplexVar v), zero)))
-
- fun make_free_bound v =
- cplexBounds (cplexNeg cplexInf, cplexLeq,
- cplexVar v, cplexLeq,
- cplexInf)
-
- val pos_constrs = rev (Symtab.fold
- (fn (k, v) => cons (make_pos_constr k))
- positive_vars [])
- val bound_constrs = map (pair NONE)
- (maps bound2constr bounds)
- val constraints' = constraints @ pos_constrs @ bound_constrs
- val bounds' = rev (Symtab.fold (fn (v, _) => cons (make_free_bound v)) cvars []);
- in
- cplexProg (name, goal, constraints', bounds')
- end
-
-fun relax_strict_ineqs (cplexProg (name, goals, constrs, bounds)) =
- let
- fun relax cplexLe = cplexLeq
- | relax cplexGe = cplexGeq
- | relax x = x
-
- fun relax_constr (n, cplexConstr(c, (t1, t2))) =
- (n, cplexConstr(relax c, (t1, t2)))
-
- fun relax_bounds (cplexBounds (t1, c1, t2, c2, t3)) =
- cplexBounds (t1, relax c1, t2, relax c2, t3)
- | relax_bounds (cplexBound (t1, c, t2)) =
- cplexBound (t1, relax c, t2)
- in
- cplexProg (name,
- goals,
- map relax_constr constrs,
- map relax_bounds bounds)
- end
-
-datatype cplexResult = Unbounded
- | Infeasible
- | Undefined
- | Optimal of string * ((string * string) list)
-
-fun is_separator x = forall (fn c => c = #"-") (String.explode x)
-
-fun is_sign x = (x = "+" orelse x = "-")
-
-fun is_colon x = (x = ":")
-
-fun is_resultsymbol a =
- let
- val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}|~-"
- fun is_symbol_char c = Char.isAlphaNum c orelse
- exists (fn d => d=c) symbol_char
- fun is_symbol_start c = is_symbol_char c andalso
- not (Char.isDigit c) andalso
- not (c= #".") andalso
- not (c= #"-")
- val b = String.explode a
- in
- b <> [] andalso is_symbol_start (hd b) andalso
- forall is_symbol_char b
- end
-
-val TOKEN_SIGN = 100
-val TOKEN_COLON = 101
-val TOKEN_SEPARATOR = 102
-
-fun load_glpkResult name =
- let
- val flist = [(is_NL, TOKEN_NL),
- (is_blank, TOKEN_BLANK),
- (is_num, TOKEN_NUM),
- (is_sign, TOKEN_SIGN),
- (is_colon, TOKEN_COLON),
- (is_cmp, TOKEN_CMP),
- (is_resultsymbol, TOKEN_SYMBOL),
- (is_separator, TOKEN_SEPARATOR)]
-
- val tokenize = tokenize_general flist
-
- val f = TextIO.openIn name
-
- val rest = Unsynchronized.ref []
-
- fun readToken_helper () =
- if length (!rest) > 0 then
- let val u = hd (!rest) in
- (
- rest := tl (!rest);
- SOME u
- )
- end
- else
- (case TextIO.inputLine f of
- NONE => NONE
- | SOME s => (rest := tokenize s; readToken_helper()))
-
- fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty)
-
- fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest)))
-
- fun readToken () =
- let val t = readToken_helper () in
- if is_tt t TOKEN_BLANK then
- readToken ()
- else if is_tt t TOKEN_NL then
- let val t2 = readToken_helper () in
- if is_tt t2 TOKEN_SIGN then
- (pushToken (SOME (TOKEN_SEPARATOR, "-")); t)
- else
- (pushToken t2; t)
- end
- else if is_tt t TOKEN_SIGN then
- let val t2 = readToken_helper () in
- if is_tt t2 TOKEN_NUM then
- (SOME (TOKEN_NUM, (snd (the t))^(snd (the t2))))
- else
- (pushToken t2; t)
- end
- else
- t
- end
-
- fun readRestOfLine P =
- let
- val t = readToken ()
- in
- if is_tt t TOKEN_NL orelse t = NONE
- then P
- else readRestOfLine P
- end
-
- fun readHeader () =
- let
- fun readStatus () = readRestOfLine ("STATUS", snd (the (readToken ())))
- fun readObjective () = readRestOfLine ("OBJECTIVE", snd (the (readToken (); readToken (); readToken ())))
- val t1 = readToken ()
- val t2 = readToken ()
- in
- if is_tt t1 TOKEN_SYMBOL andalso is_tt t2 TOKEN_COLON
- then
- case to_upper (snd (the t1)) of
- "STATUS" => (readStatus ())::(readHeader ())
- | "OBJECTIVE" => (readObjective())::(readHeader ())
- | _ => (readRestOfLine (); readHeader ())
- else
- (pushToken t2; pushToken t1; [])
- end
-
- fun skip_until_sep () =
- let val x = readToken () in
- if is_tt x TOKEN_SEPARATOR then
- readRestOfLine ()
- else
- skip_until_sep ()
- end
-
- fun load_value () =
- let
- val t1 = readToken ()
- val t2 = readToken ()
- in
- if is_tt t1 TOKEN_NUM andalso is_tt t2 TOKEN_SYMBOL then
- let
- val t = readToken ()
- val state = if is_tt t TOKEN_NL then readToken () else t
- val _ = if is_tt state TOKEN_SYMBOL then () else raise (Load_cplexResult "state expected")
- val k = readToken ()
- in
- if is_tt k TOKEN_NUM then
- readRestOfLine (SOME (snd (the t2), snd (the k)))
- else
- raise (Load_cplexResult "number expected")
- end
- else
- (pushToken t2; pushToken t1; NONE)
- end
-
- fun load_values () =
- let val v = load_value () in
- if v = NONE then [] else (the v)::(load_values ())
- end
-
- val header = readHeader ()
-
- val result =
- case AList.lookup (op =) header "STATUS" of
- SOME "INFEASIBLE" => Infeasible
- | SOME "UNBOUNDED" => Unbounded
- | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
- (skip_until_sep ();
- skip_until_sep ();
- load_values ()))
- | _ => Undefined
-
- val _ = TextIO.closeIn f
- in
- result
- end
- handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
- | Option => raise (Load_cplexResult "Option")
- | x => raise x
-
-fun load_cplexResult name =
- let
- val flist = [(is_NL, TOKEN_NL),
- (is_blank, TOKEN_BLANK),
- (is_num, TOKEN_NUM),
- (is_sign, TOKEN_SIGN),
- (is_colon, TOKEN_COLON),
- (is_cmp, TOKEN_CMP),
- (is_resultsymbol, TOKEN_SYMBOL)]
-
- val tokenize = tokenize_general flist
-
- val f = TextIO.openIn name
-
- val rest = Unsynchronized.ref []
-
- fun readToken_helper () =
- if length (!rest) > 0 then
- let val u = hd (!rest) in
- (
- rest := tl (!rest);
- SOME u
- )
- end
- else
- (case TextIO.inputLine f of
- NONE => NONE
- | SOME s => (rest := tokenize s; readToken_helper()))
-
- fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty)
-
- fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest)))
-
- fun readToken () =
- let val t = readToken_helper () in
- if is_tt t TOKEN_BLANK then
- readToken ()
- else if is_tt t TOKEN_SIGN then
- let val t2 = readToken_helper () in
- if is_tt t2 TOKEN_NUM then
- (SOME (TOKEN_NUM, (snd (the t))^(snd (the t2))))
- else
- (pushToken t2; t)
- end
- else
- t
- end
-
- fun readRestOfLine P =
- let
- val t = readToken ()
- in
- if is_tt t TOKEN_NL orelse t = NONE
- then P
- else readRestOfLine P
- end
-
- fun readHeader () =
- let
- fun readStatus () = readRestOfLine ("STATUS", snd (the (readToken ())))
- fun readObjective () =
- let
- val t = readToken ()
- in
- if is_tt t TOKEN_SYMBOL andalso to_upper (snd (the t)) = "VALUE" then
- readRestOfLine ("OBJECTIVE", snd (the (readToken())))
- else
- readRestOfLine ("OBJECTIVE_NAME", snd (the t))
- end
-
- val t = readToken ()
- in
- if is_tt t TOKEN_SYMBOL then
- case to_upper (snd (the t)) of
- "STATUS" => (readStatus ())::(readHeader ())
- | "OBJECTIVE" => (readObjective ())::(readHeader ())
- | "SECTION" => (pushToken t; [])
- | _ => (readRestOfLine (); readHeader ())
- else
- (readRestOfLine (); readHeader ())
- end
-
- fun skip_nls () =
- let val x = readToken () in
- if is_tt x TOKEN_NL then
- skip_nls ()
- else
- (pushToken x; ())
- end
-
- fun skip_paragraph () =
- if is_tt (readToken ()) TOKEN_NL then
- (if is_tt (readToken ()) TOKEN_NL then
- skip_nls ()
- else
- skip_paragraph ())
- else
- skip_paragraph ()
-
- fun load_value () =
- let
- val t1 = readToken ()
- val t1 = if is_tt t1 TOKEN_SYMBOL andalso snd (the t1) = "A" then readToken () else t1
- in
- if is_tt t1 TOKEN_NUM then
- let
- val name = readToken ()
- val status = readToken ()
- val value = readToken ()
- in
- if is_tt name TOKEN_SYMBOL andalso
- is_tt status TOKEN_SYMBOL andalso
- is_tt value TOKEN_NUM
- then
- readRestOfLine (SOME (snd (the name), snd (the value)))
- else
- raise (Load_cplexResult "column line expected")
- end
- else
- (pushToken t1; NONE)
- end
-
- fun load_values () =
- let val v = load_value () in
- if v = NONE then [] else (the v)::(load_values ())
- end
-
- val header = readHeader ()
-
- val result =
- case AList.lookup (op =) header "STATUS" of
- SOME "INFEASIBLE" => Infeasible
- | SOME "NONOPTIMAL" => Unbounded
- | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
- (skip_paragraph ();
- skip_paragraph ();
- skip_paragraph ();
- skip_paragraph ();
- skip_paragraph ();
- load_values ()))
- | _ => Undefined
-
- val _ = TextIO.closeIn f
- in
- result
- end
- handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
- | Option => raise (Load_cplexResult "Option")
- | x => raise x
-
-exception Execute of string;
-
-fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s])));
-fun wrap s = "\""^s^"\"";
-
-fun solve_glpk prog =
- let
- val name = LargeInt.toString (Time.toMicroseconds (Time.now ()))
- val lpname = tmp_file (name^".lp")
- val resultname = tmp_file (name^".txt")
- val _ = save_cplexFile lpname prog
- val cplex_path = getenv "GLPK_PATH"
- val cplex = if cplex_path = "" then "glpsol" else cplex_path
- val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
- val answer = #1 (bash_output command)
- in
- let
- val result = load_glpkResult resultname
- val _ = OS.FileSys.remove lpname
- val _ = OS.FileSys.remove resultname
- in
- result
- end
- handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer))
- | _ => raise (Execute answer)
- end
-
-fun solve_cplex prog =
- let
- fun write_script s lp r =
- let
- val f = TextIO.openOut s
- val _ = TextIO.output (f, "read\n"^lp^"\noptimize\nwrite\n"^r^"\nquit")
- val _ = TextIO.closeOut f
- in
- ()
- end
-
- val name = LargeInt.toString (Time.toMicroseconds (Time.now ()))
- val lpname = tmp_file (name^".lp")
- val resultname = tmp_file (name^".txt")
- val scriptname = tmp_file (name^".script")
- val _ = save_cplexFile lpname prog
- val cplex_path = getenv "CPLEX_PATH"
- val cplex = if cplex_path = "" then "cplex" else cplex_path
- val _ = write_script scriptname lpname resultname
- val command = (wrap cplex)^" < "^(wrap scriptname)^" > /dev/null"
- val answer = "return code "^(Int.toString (bash command))
- in
- let
- val result = load_cplexResult resultname
- val _ = OS.FileSys.remove lpname
- val _ = OS.FileSys.remove resultname
- val _ = OS.FileSys.remove scriptname
- in
- result
- end
- end
-
-fun solve prog =
- case get_solver () of
- SOLVER_DEFAULT =>
- (case getenv "LP_SOLVER" of
- "CPLEX" => solve_cplex prog
- | "GLPK" => solve_glpk prog
- | _ => raise (Execute ("LP_SOLVER must be set to CPLEX or to GLPK")))
- | SOLVER_CPLEX => solve_cplex prog
- | SOLVER_GLPK => solve_glpk prog
-
-end;
-
-(*
-val demofile = "/home/obua/flyspeck/kepler/LP/cplexPent2.lp45"
-val demoout = "/home/obua/flyspeck/kepler/LP/test.out"
-val demoresult = "/home/obua/flyspeck/kepler/LP/try/test2.sol"
-
-fun loadcplex () = Cplex.relax_strict_ineqs
- (Cplex.load_cplexFile demofile)
-
-fun writecplex lp = Cplex.save_cplexFile demoout lp
-
-fun test () =
- let
- val lp = loadcplex ()
- val lp2 = Cplex.elim_nonfree_bounds lp
- in
- writecplex lp2
- end
-
-fun loadresult () = Cplex.load_cplexResult demoresult;
-*)
-
-(*val prog = Cplex.load_cplexFile "/home/obua/tmp/pent/graph_0.lpt";
-val _ = Cplex.solve prog;*)
--- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Mon Jul 12 11:21:27 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,284 +0,0 @@
-(* Title: HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
- Author: Steven Obua
-*)
-
-signature FLOAT_SPARSE_MATIRX_BUILDER =
-sig
- include MATRIX_BUILDER
-
- structure cplex : CPLEX
-
- type float = Float.float
- val approx_value : int -> (float -> float) -> string -> term * term
- val approx_vector : int -> (float -> float) -> vector -> term * term
- val approx_matrix : int -> (float -> float) -> matrix -> term * term
-
- val mk_spvec_entry : int -> float -> term
- val mk_spvec_entry' : int -> term -> term
- val mk_spmat_entry : int -> term -> term
- val spvecT: typ
- val spmatT: typ
-
- val v_elem_at : vector -> int -> string option
- val m_elem_at : matrix -> int -> vector option
- val v_only_elem : vector -> int option
- val v_fold : (int * string -> 'a -> 'a) -> vector -> 'a -> 'a
- val m_fold : (int * vector -> 'a -> 'a) -> matrix -> 'a -> 'a
-
- val transpose_matrix : matrix -> matrix
-
- val cut_vector : int -> vector -> vector
- val cut_matrix : vector -> int option -> matrix -> matrix
-
- val delete_matrix : int list -> matrix -> matrix
- val cut_matrix' : int list -> matrix -> matrix
- val delete_vector : int list -> vector -> vector
- val cut_vector' : int list -> vector -> vector
-
- val indices_of_matrix : matrix -> int list
- val indices_of_vector : vector -> int list
-
- (* cplexProg c A b *)
- val cplexProg : vector -> matrix -> vector -> cplex.cplexProg * (string -> int)
- (* dual_cplexProg c A b *)
- val dual_cplexProg : vector -> matrix -> vector -> cplex.cplexProg * (string -> int)
-end;
-
-structure FloatSparseMatrixBuilder : FLOAT_SPARSE_MATIRX_BUILDER =
-struct
-
-type float = Float.float
-structure Inttab = Table(type key = int val ord = rev_order o int_ord);
-
-type vector = string Inttab.table
-type matrix = vector Inttab.table
-
-val spvec_elemT = HOLogic.mk_prodT (HOLogic.natT, HOLogic.realT);
-val spvecT = HOLogic.listT spvec_elemT;
-val spmat_elemT = HOLogic.mk_prodT (HOLogic.natT, spvecT);
-val spmatT = HOLogic.listT spmat_elemT;
-
-fun approx_value prec f =
- FloatArith.approx_float prec (fn (x, y) => (f x, f y));
-
-fun mk_spvec_entry i f =
- HOLogic.mk_prod (HOLogic.mk_number HOLogic.natT i, FloatArith.mk_float f);
-
-fun mk_spvec_entry' i x =
- HOLogic.mk_prod (HOLogic.mk_number HOLogic.natT i, x);
-
-fun mk_spmat_entry i e =
- HOLogic.mk_prod (HOLogic.mk_number HOLogic.natT i, e);
-
-fun approx_vector prec pprt vector =
- let
- fun app (index, s) (lower, upper) =
- let
- val (flower, fupper) = approx_value prec pprt s
- val index = HOLogic.mk_number HOLogic.natT index
- val elower = HOLogic.mk_prod (index, flower)
- val eupper = HOLogic.mk_prod (index, fupper)
- in (elower :: lower, eupper :: upper) end;
- in
- pairself (HOLogic.mk_list spvec_elemT) (Inttab.fold app vector ([], []))
- end;
-
-fun approx_matrix prec pprt vector =
- let
- fun app (index, v) (lower, upper) =
- let
- val (flower, fupper) = approx_vector prec pprt v
- val index = HOLogic.mk_number HOLogic.natT index
- val elower = HOLogic.mk_prod (index, flower)
- val eupper = HOLogic.mk_prod (index, fupper)
- in (elower :: lower, eupper :: upper) end;
- in
- pairself (HOLogic.mk_list spmat_elemT) (Inttab.fold app vector ([], []))
- end;
-
-exception Nat_expected of int;
-
-val zero_interval = approx_value 1 I "0"
-
-fun set_elem vector index str =
- if index < 0 then
- raise (Nat_expected index)
- else if (approx_value 1 I str) = zero_interval then
- vector
- else
- Inttab.update (index, str) vector
-
-fun set_vector matrix index vector =
- if index < 0 then
- raise (Nat_expected index)
- else if Inttab.is_empty vector then
- matrix
- else
- Inttab.update (index, vector) matrix
-
-val empty_matrix = Inttab.empty
-val empty_vector = Inttab.empty
-
-(* dual stuff *)
-
-structure cplex = Cplex
-
-fun transpose_matrix matrix =
- let
- fun upd j (i, s) =
- Inttab.map_default (i, Inttab.empty) (Inttab.update (j, s));
- fun updm (j, v) = Inttab.fold (upd j) v;
- in Inttab.fold updm matrix empty_matrix end;
-
-exception No_name of string;
-
-exception Superfluous_constr_right_hand_sides
-
-fun cplexProg c A b =
- let
- val ytable = Unsynchronized.ref Inttab.empty
- fun indexof s =
- if String.size s = 0 then raise (No_name s)
- else case Int.fromString (String.extract(s, 1, NONE)) of
- SOME i => i | NONE => raise (No_name s)
-
- fun nameof i =
- let
- val s = "x"^(Int.toString i)
- val _ = Unsynchronized.change ytable (Inttab.update (i, s))
- in
- s
- end
-
- fun split_numstr s =
- if String.isPrefix "-" s then (false,String.extract(s, 1, NONE))
- else if String.isPrefix "+" s then (true, String.extract(s, 1, NONE))
- else (true, s)
-
- fun mk_term index s =
- let
- val (p, s) = split_numstr s
- val prod = cplex.cplexProd (cplex.cplexNum s, cplex.cplexVar (nameof index))
- in
- if p then prod else cplex.cplexNeg prod
- end
-
- fun vec2sum vector =
- cplex.cplexSum (Inttab.fold (fn (index, s) => fn list => (mk_term index s) :: list) vector [])
-
- fun mk_constr index vector c =
- let
- val s = case Inttab.lookup c index of SOME s => s | NONE => "0"
- val (p, s) = split_numstr s
- val num = if p then cplex.cplexNum s else cplex.cplexNeg (cplex.cplexNum s)
- in
- (NONE, cplex.cplexConstr (cplex.cplexLeq, (vec2sum vector, num)))
- end
-
- fun delete index c = Inttab.delete index c handle Inttab.UNDEF _ => c
-
- val (list, b) = Inttab.fold
- (fn (index, v) => fn (list, c) => ((mk_constr index v c)::list, delete index c))
- A ([], b)
- val _ = if Inttab.is_empty b then () else raise Superfluous_constr_right_hand_sides
-
- fun mk_free y = cplex.cplexBounds (cplex.cplexNeg cplex.cplexInf, cplex.cplexLeq,
- cplex.cplexVar y, cplex.cplexLeq,
- cplex.cplexInf)
-
- val yvars = Inttab.fold (fn (i, y) => fn l => (mk_free y)::l) (!ytable) []
-
- val prog = cplex.cplexProg ("original", cplex.cplexMaximize (vec2sum c), list, yvars)
- in
- (prog, indexof)
- end
-
-
-fun dual_cplexProg c A b =
- let
- fun indexof s =
- if String.size s = 0 then raise (No_name s)
- else case Int.fromString (String.extract(s, 1, NONE)) of
- SOME i => i | NONE => raise (No_name s)
-
- fun nameof i = "y"^(Int.toString i)
-
- fun split_numstr s =
- if String.isPrefix "-" s then (false,String.extract(s, 1, NONE))
- else if String.isPrefix "+" s then (true, String.extract(s, 1, NONE))
- else (true, s)
-
- fun mk_term index s =
- let
- val (p, s) = split_numstr s
- val prod = cplex.cplexProd (cplex.cplexNum s, cplex.cplexVar (nameof index))
- in
- if p then prod else cplex.cplexNeg prod
- end
-
- fun vec2sum vector =
- cplex.cplexSum (Inttab.fold (fn (index, s) => fn list => (mk_term index s)::list) vector [])
-
- fun mk_constr index vector c =
- let
- val s = case Inttab.lookup c index of SOME s => s | NONE => "0"
- val (p, s) = split_numstr s
- val num = if p then cplex.cplexNum s else cplex.cplexNeg (cplex.cplexNum s)
- in
- (NONE, cplex.cplexConstr (cplex.cplexEq, (vec2sum vector, num)))
- end
-
- fun delete index c = Inttab.delete index c handle Inttab.UNDEF _ => c
-
- val (list, c) = Inttab.fold
- (fn (index, v) => fn (list, c) => ((mk_constr index v c)::list, delete index c))
- (transpose_matrix A) ([], c)
- val _ = if Inttab.is_empty c then () else raise Superfluous_constr_right_hand_sides
-
- val prog = cplex.cplexProg ("dual", cplex.cplexMinimize (vec2sum b), list, [])
- in
- (prog, indexof)
- end
-
-fun cut_vector size v =
- let
- val count = Unsynchronized.ref 0;
- fun app (i, s) = if (!count < size) then
- (count := !count +1 ; Inttab.update (i, s))
- else I
- in
- Inttab.fold app v empty_vector
- end
-
-fun cut_matrix vfilter vsize m =
- let
- fun app (i, v) =
- if is_none (Inttab.lookup vfilter i) then I
- else case vsize
- of NONE => Inttab.update (i, v)
- | SOME s => Inttab.update (i, cut_vector s v)
- in Inttab.fold app m empty_matrix end
-
-fun v_elem_at v i = Inttab.lookup v i
-fun m_elem_at m i = Inttab.lookup m i
-
-fun v_only_elem v =
- case Inttab.min_key v of
- NONE => NONE
- | SOME vmin => (case Inttab.max_key v of
- NONE => SOME vmin
- | SOME vmax => if vmin = vmax then SOME vmin else NONE)
-
-fun v_fold f = Inttab.fold f;
-fun m_fold f = Inttab.fold f;
-
-fun indices_of_vector v = Inttab.keys v
-fun indices_of_matrix m = Inttab.keys m
-fun delete_vector indices v = fold Inttab.delete indices v
-fun delete_matrix indices m = fold Inttab.delete indices m
-fun cut_matrix' indices m = fold (fn i => fn m => (case Inttab.lookup m i of NONE => m | SOME v => Inttab.update (i, v) m)) indices Inttab.empty
-fun cut_vector' indices v = fold (fn i => fn v => (case Inttab.lookup v i of NONE => v | SOME x => Inttab.update (i, x) v)) indices Inttab.empty
-
-
-
-end;
--- a/src/HOL/Matrix/cplex/fspmlp.ML Mon Jul 12 11:21:27 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,322 +0,0 @@
-(* Title: HOL/Matrix/cplex/fspmlp.ML
- Author: Steven Obua
-*)
-
-signature FSPMLP =
-sig
- type linprog
- type vector = FloatSparseMatrixBuilder.vector
- type matrix = FloatSparseMatrixBuilder.matrix
-
- val y : linprog -> term
- val A : linprog -> term * term
- val b : linprog -> term
- val c : linprog -> term * term
- val r12 : linprog -> term * term
-
- exception Load of string
-
- val load : string -> int -> bool -> linprog
-end
-
-structure Fspmlp : FSPMLP =
-struct
-
-type vector = FloatSparseMatrixBuilder.vector
-type matrix = FloatSparseMatrixBuilder.matrix
-
-type linprog = term * (term * term) * term * (term * term) * (term * term)
-
-fun y (c1, c2, c3, c4, _) = c1
-fun A (c1, c2, c3, c4, _) = c2
-fun b (c1, c2, c3, c4, _) = c3
-fun c (c1, c2, c3, c4, _) = c4
-fun r12 (c1, c2, c3, c4, c6) = c6
-
-structure CplexFloatSparseMatrixConverter =
-MAKE_CPLEX_MATRIX_CONVERTER(structure cplex = Cplex and matrix_builder = FloatSparseMatrixBuilder);
-
-datatype bound_type = LOWER | UPPER
-
-fun intbound_ord ((i1: int, b1),(i2,b2)) =
- if i1 < i2 then LESS
- else if i1 = i2 then
- (if b1 = b2 then EQUAL else if b1=LOWER then LESS else GREATER)
- else GREATER
-
-structure Inttab = Table(type key = int val ord = (rev_order o int_ord));
-
-structure VarGraph = Table(type key = int*bound_type val ord = intbound_ord);
-(* key -> (float option) * (int -> (float * (((float * float) * key) list)))) *)
-(* dest_key -> (sure_bound * (row_index -> (row_bound * (((coeff_lower * coeff_upper) * src_key) list)))) *)
-
-exception Internal of string;
-
-fun add_row_bound g dest_key row_index row_bound =
- let
- val x =
- case VarGraph.lookup g dest_key of
- NONE => (NONE, Inttab.update (row_index, (row_bound, [])) Inttab.empty)
- | SOME (sure_bound, f) =>
- (sure_bound,
- case Inttab.lookup f row_index of
- NONE => Inttab.update (row_index, (row_bound, [])) f
- | SOME _ => raise (Internal "add_row_bound"))
- in
- VarGraph.update (dest_key, x) g
- end
-
-fun update_sure_bound g (key as (_, btype)) bound =
- let
- val x =
- case VarGraph.lookup g key of
- NONE => (SOME bound, Inttab.empty)
- | SOME (NONE, f) => (SOME bound, f)
- | SOME (SOME old_bound, f) =>
- (SOME ((case btype of
- UPPER => Float.min
- | LOWER => Float.max)
- old_bound bound), f)
- in
- VarGraph.update (key, x) g
- end
-
-fun get_sure_bound g key =
- case VarGraph.lookup g key of
- NONE => NONE
- | SOME (sure_bound, _) => sure_bound
-
-(*fun get_row_bound g key row_index =
- case VarGraph.lookup g key of
- NONE => NONE
- | SOME (sure_bound, f) =>
- (case Inttab.lookup f row_index of
- NONE => NONE
- | SOME (row_bound, _) => (sure_bound, row_bound))*)
-
-fun add_edge g src_key dest_key row_index coeff =
- case VarGraph.lookup g dest_key of
- NONE => raise (Internal "add_edge: dest_key not found")
- | SOME (sure_bound, f) =>
- (case Inttab.lookup f row_index of
- NONE => raise (Internal "add_edge: row_index not found")
- | SOME (row_bound, sources) =>
- VarGraph.update (dest_key, (sure_bound, Inttab.update (row_index, (row_bound, (coeff, src_key) :: sources)) f)) g)
-
-fun split_graph g =
- let
- fun split (key, (sure_bound, _)) (r1, r2) = case sure_bound
- of NONE => (r1, r2)
- | SOME bound => (case key
- of (u, UPPER) => (r1, Inttab.update (u, bound) r2)
- | (u, LOWER) => (Inttab.update (u, bound) r1, r2))
- in VarGraph.fold split g (Inttab.empty, Inttab.empty) end
-
-fun it2list t = Inttab.fold cons t [];
-
-(* If safe is true, termination is guaranteed, but the sure bounds may be not optimal (relative to the algorithm).
- If safe is false, termination is not guaranteed, but on termination the sure bounds are optimal (relative to the algorithm) *)
-fun propagate_sure_bounds safe names g =
- let
- (* returns NONE if no new sure bound could be calculated, otherwise the new sure bound is returned *)
- fun calc_sure_bound_from_sources g (key as (_, btype)) =
- let
- fun mult_upper x (lower, upper) =
- if Float.sign x = LESS then
- Float.mult x lower
- else
- Float.mult x upper
-
- fun mult_lower x (lower, upper) =
- if Float.sign x = LESS then
- Float.mult x upper
- else
- Float.mult x lower
-
- val mult_btype = case btype of UPPER => mult_upper | LOWER => mult_lower
-
- fun calc_sure_bound (row_index, (row_bound, sources)) sure_bound =
- let
- fun add_src_bound (coeff, src_key) sum =
- case sum of
- NONE => NONE
- | SOME x =>
- (case get_sure_bound g src_key of
- NONE => NONE
- | SOME src_sure_bound => SOME (Float.add x (mult_btype src_sure_bound coeff)))
- in
- case fold add_src_bound sources (SOME row_bound) of
- NONE => sure_bound
- | new_sure_bound as (SOME new_bound) =>
- (case sure_bound of
- NONE => new_sure_bound
- | SOME old_bound =>
- SOME (case btype of
- UPPER => Float.min old_bound new_bound
- | LOWER => Float.max old_bound new_bound))
- end
- in
- case VarGraph.lookup g key of
- NONE => NONE
- | SOME (sure_bound, f) =>
- let
- val x = Inttab.fold calc_sure_bound f sure_bound
- in
- if x = sure_bound then NONE else x
- end
- end
-
- fun propagate (key, _) (g, b) =
- case calc_sure_bound_from_sources g key of
- NONE => (g,b)
- | SOME bound => (update_sure_bound g key bound,
- if safe then
- case get_sure_bound g key of
- NONE => true
- | _ => b
- else
- true)
-
- val (g, b) = VarGraph.fold propagate g (g, false)
- in
- if b then propagate_sure_bounds safe names g else g
- end
-
-exception Load of string;
-
-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
- val empty = Inttab.empty
-
- fun instab t i x = Inttab.update (i, x) t
-
- fun isnegstr x = String.isPrefix "-" x
- fun negstr x = if isnegstr x then String.extract (x, 1, NONE) else "-"^x
-
- fun test_1 (lower, upper) =
- if lower = upper then
- (if Float.eq (lower, (~1, 0)) then ~1
- else if Float.eq (lower, (1, 0)) then 1
- else 0)
- else 0
-
- fun calcr (row_index, a) g =
- let
- val b = FloatSparseMatrixBuilder.v_elem_at b row_index
- val (_, b2) = FloatArith.approx_decstr_by_bin prec (case b of NONE => "0" | SOME b => b)
- val approx_a = FloatSparseMatrixBuilder.v_fold (fn (i, s) => fn l =>
- (i, FloatArith.approx_decstr_by_bin prec s)::l) a []
-
- fun fold_dest_nodes (dest_index, dest_value) g =
- let
- val dest_test = test_1 dest_value
- in
- if dest_test = 0 then
- g
- else let
- val (dest_key as (_, dest_btype), row_bound) =
- if dest_test = ~1 then
- ((dest_index, LOWER), Float.neg b2)
- else
- ((dest_index, UPPER), b2)
-
- fun fold_src_nodes (src_index, src_value as (src_lower, src_upper)) g =
- if src_index = dest_index then g
- else
- let
- val coeff = case dest_btype of
- UPPER => (Float.neg src_upper, Float.neg src_lower)
- | LOWER => src_value
- in
- if Float.sign src_lower = LESS then
- add_edge g (src_index, UPPER) dest_key row_index coeff
- else
- add_edge g (src_index, LOWER) dest_key row_index coeff
- end
- in
- fold fold_src_nodes approx_a (add_row_bound g dest_key row_index row_bound)
- end
- end
- in
- case approx_a of
- [] => g
- | [(u, a)] =>
- let
- val atest = test_1 a
- in
- if atest = ~1 then
- update_sure_bound g (u, LOWER) (Float.neg b2)
- else if atest = 1 then
- update_sure_bound g (u, UPPER) b2
- else
- g
- end
- | _ => fold fold_dest_nodes approx_a g
- 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
-
- fun add_row_entry m index f vname value =
- let
- val v = (case value of
- SOME value => FloatSparseMatrixBuilder.mk_spvec_entry 0 value
- | NONE => FloatSparseMatrixBuilder.mk_spvec_entry' 0 (f $ (Var ((vname,0), HOLogic.realT))))
- val vec = cons_spvec v empty_spvec
- in
- cons_spmat (FloatSparseMatrixBuilder.mk_spmat_entry index vec) m
- end
-
- fun abs_estimate i r1 r2 =
- if i = 0 then
- let val e = empty_spmat in (e, e) end
- else
- let
- val index = xlen-i
- val (r12_1, r12_2) = abs_estimate (i-1) r1 r2
- val b1 = Inttab.lookup r1 index
- val b2 = Inttab.lookup r2 index
- in
- (add_row_entry r12_1 index @{term "lbound :: real => real"} ((names index)^"l") b1,
- add_row_entry r12_2 index @{term "ubound :: real => real"} ((names index)^"u") b2)
- end
-
- val (r1, r2) = abs_estimate xlen r1 r2
-
- in
- (r1, r2)
- end
-
-fun load filename prec safe_propagation =
- let
- 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 (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
- val results = Cplex.solve dualprog
- val (optimal,v) = CplexFloatSparseMatrixConverter.convert_results results indexof
- (*val A = FloatSparseMatrixBuilder.cut_matrix v NONE A*)
- fun id x = x
- val v = FloatSparseMatrixBuilder.set_vector FloatSparseMatrixBuilder.empty_matrix 0 v
- val b = FloatSparseMatrixBuilder.transpose_matrix (FloatSparseMatrixBuilder.set_vector FloatSparseMatrixBuilder.empty_matrix 0 b)
- val c = FloatSparseMatrixBuilder.set_vector FloatSparseMatrixBuilder.empty_matrix 0 c
- val (y1, _) = FloatSparseMatrixBuilder.approx_matrix prec Float.positive_part v
- val A = FloatSparseMatrixBuilder.approx_matrix prec id A
- val (_,b2) = FloatSparseMatrixBuilder.approx_matrix prec id b
- val c = FloatSparseMatrixBuilder.approx_matrix prec id c
- in
- (y1, A, b2, c, (r1, r2))
- end handle CplexFloatSparseMatrixConverter.Converter s => (raise (Load ("Converter: "^s)))
-
-end
--- a/src/HOL/Matrix/cplex/matrixlp.ML Mon Jul 12 11:21:27 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,100 +0,0 @@
-(* Title: HOL/Matrix/cplex/matrixlp.ML
- Author: Steven Obua
-*)
-
-signature MATRIX_LP =
-sig
- val lp_dual_estimate_prt : string -> int -> thm
- val lp_dual_estimate_prt_primitive :
- cterm * (cterm * cterm) * (cterm * cterm) * cterm * (cterm * cterm) -> 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
-
-fun inst_real thm =
- let val certT = ctyp_of (Thm.theory_of_thm thm) in
- Drule.export_without_context (Thm.instantiate
- ([(certT (TVar (hd (OldTerm.term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
- end
-
-local
-
-val cert = cterm_of @{theory}
-
-in
-
-fun lp_dual_estimate_prt_primitive (y, (A1, A2), (c1, c2), b, (r1, r2)) =
- let
- val th = inst_real @{thm "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
- in th end
-
-fun lp_dual_estimate_prt lptfile prec =
- let
- val certificate =
- let
- 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)
- end
- in
- lp_dual_estimate_prt_primitive certificate
- end
-
-end
-
-fun prep ths = ComputeHOL.prep_thms ths
-
-fun inst_tvar ty thm =
- let
- val certT = Thm.ctyp_of (Thm.theory_of_thm thm);
- val ord = prod_ord (prod_ord string_ord int_ord) (list_ord string_ord)
- val v = TVar (hd (sort ord (OldTerm.term_tvars (prop_of thm))))
- in
- Drule.export_without_context (Thm.instantiate ([(certT v, certT ty)], []) thm)
- end
-
-fun inst_tvars [] thms = thms
- | inst_tvars (ty::tys) thms = inst_tvars tys (map (inst_tvar ty) thms)
-
-local
- val ths = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_list_case" "ComputeHOL.compute_let"
- "ComputeHOL.compute_if" "ComputeFloat.arith" "SparseMatrix.sparse_row_matrix_arith_simps"
- "ComputeHOL.compute_bool" "ComputeHOL.compute_pair"
- "SparseMatrix.sorted_sp_simps" "ComputeNumeral.number_norm"
- "ComputeNumeral.natnorm"};
- val computer = PCompute.make Compute.SML @{theory} ths []
-in
-
-fun matrix_compute c = hd (PCompute.rewrite computer [c])
-
-end
-
-fun matrix_simplify th =
- let
- val simp_th = matrix_compute (cprop_of th)
- val th = Thm.strip_shyps (Thm.equal_elim simp_th th)
- fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle _ => th (* FIXME avoid handle _ *)
- in
- removeTrue th
- end
-
-fun prove_bound lptfile prec =
- let
- val th = lp_dual_estimate_prt lptfile prec
- in
- matrix_simplify th
- end
-
-val realFromStr = the o Real.fromString;
-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/fspmlp.ML Mon Jul 12 11:21:56 2010 +0200
@@ -0,0 +1,322 @@
+(* Title: HOL/Matrix/cplex/fspmlp.ML
+ Author: Steven Obua
+*)
+
+signature FSPMLP =
+sig
+ type linprog
+ type vector = FloatSparseMatrixBuilder.vector
+ type matrix = FloatSparseMatrixBuilder.matrix
+
+ val y : linprog -> term
+ val A : linprog -> term * term
+ val b : linprog -> term
+ val c : linprog -> term * term
+ val r12 : linprog -> term * term
+
+ exception Load of string
+
+ val load : string -> int -> bool -> linprog
+end
+
+structure Fspmlp : FSPMLP =
+struct
+
+type vector = FloatSparseMatrixBuilder.vector
+type matrix = FloatSparseMatrixBuilder.matrix
+
+type linprog = term * (term * term) * term * (term * term) * (term * term)
+
+fun y (c1, c2, c3, c4, _) = c1
+fun A (c1, c2, c3, c4, _) = c2
+fun b (c1, c2, c3, c4, _) = c3
+fun c (c1, c2, c3, c4, _) = c4
+fun r12 (c1, c2, c3, c4, c6) = c6
+
+structure CplexFloatSparseMatrixConverter =
+MAKE_CPLEX_MATRIX_CONVERTER(structure cplex = Cplex and matrix_builder = FloatSparseMatrixBuilder);
+
+datatype bound_type = LOWER | UPPER
+
+fun intbound_ord ((i1: int, b1),(i2,b2)) =
+ if i1 < i2 then LESS
+ else if i1 = i2 then
+ (if b1 = b2 then EQUAL else if b1=LOWER then LESS else GREATER)
+ else GREATER
+
+structure Inttab = Table(type key = int val ord = (rev_order o int_ord));
+
+structure VarGraph = Table(type key = int*bound_type val ord = intbound_ord);
+(* key -> (float option) * (int -> (float * (((float * float) * key) list)))) *)
+(* dest_key -> (sure_bound * (row_index -> (row_bound * (((coeff_lower * coeff_upper) * src_key) list)))) *)
+
+exception Internal of string;
+
+fun add_row_bound g dest_key row_index row_bound =
+ let
+ val x =
+ case VarGraph.lookup g dest_key of
+ NONE => (NONE, Inttab.update (row_index, (row_bound, [])) Inttab.empty)
+ | SOME (sure_bound, f) =>
+ (sure_bound,
+ case Inttab.lookup f row_index of
+ NONE => Inttab.update (row_index, (row_bound, [])) f
+ | SOME _ => raise (Internal "add_row_bound"))
+ in
+ VarGraph.update (dest_key, x) g
+ end
+
+fun update_sure_bound g (key as (_, btype)) bound =
+ let
+ val x =
+ case VarGraph.lookup g key of
+ NONE => (SOME bound, Inttab.empty)
+ | SOME (NONE, f) => (SOME bound, f)
+ | SOME (SOME old_bound, f) =>
+ (SOME ((case btype of
+ UPPER => Float.min
+ | LOWER => Float.max)
+ old_bound bound), f)
+ in
+ VarGraph.update (key, x) g
+ end
+
+fun get_sure_bound g key =
+ case VarGraph.lookup g key of
+ NONE => NONE
+ | SOME (sure_bound, _) => sure_bound
+
+(*fun get_row_bound g key row_index =
+ case VarGraph.lookup g key of
+ NONE => NONE
+ | SOME (sure_bound, f) =>
+ (case Inttab.lookup f row_index of
+ NONE => NONE
+ | SOME (row_bound, _) => (sure_bound, row_bound))*)
+
+fun add_edge g src_key dest_key row_index coeff =
+ case VarGraph.lookup g dest_key of
+ NONE => raise (Internal "add_edge: dest_key not found")
+ | SOME (sure_bound, f) =>
+ (case Inttab.lookup f row_index of
+ NONE => raise (Internal "add_edge: row_index not found")
+ | SOME (row_bound, sources) =>
+ VarGraph.update (dest_key, (sure_bound, Inttab.update (row_index, (row_bound, (coeff, src_key) :: sources)) f)) g)
+
+fun split_graph g =
+ let
+ fun split (key, (sure_bound, _)) (r1, r2) = case sure_bound
+ of NONE => (r1, r2)
+ | SOME bound => (case key
+ of (u, UPPER) => (r1, Inttab.update (u, bound) r2)
+ | (u, LOWER) => (Inttab.update (u, bound) r1, r2))
+ in VarGraph.fold split g (Inttab.empty, Inttab.empty) end
+
+fun it2list t = Inttab.fold cons t [];
+
+(* If safe is true, termination is guaranteed, but the sure bounds may be not optimal (relative to the algorithm).
+ If safe is false, termination is not guaranteed, but on termination the sure bounds are optimal (relative to the algorithm) *)
+fun propagate_sure_bounds safe names g =
+ let
+ (* returns NONE if no new sure bound could be calculated, otherwise the new sure bound is returned *)
+ fun calc_sure_bound_from_sources g (key as (_, btype)) =
+ let
+ fun mult_upper x (lower, upper) =
+ if Float.sign x = LESS then
+ Float.mult x lower
+ else
+ Float.mult x upper
+
+ fun mult_lower x (lower, upper) =
+ if Float.sign x = LESS then
+ Float.mult x upper
+ else
+ Float.mult x lower
+
+ val mult_btype = case btype of UPPER => mult_upper | LOWER => mult_lower
+
+ fun calc_sure_bound (row_index, (row_bound, sources)) sure_bound =
+ let
+ fun add_src_bound (coeff, src_key) sum =
+ case sum of
+ NONE => NONE
+ | SOME x =>
+ (case get_sure_bound g src_key of
+ NONE => NONE
+ | SOME src_sure_bound => SOME (Float.add x (mult_btype src_sure_bound coeff)))
+ in
+ case fold add_src_bound sources (SOME row_bound) of
+ NONE => sure_bound
+ | new_sure_bound as (SOME new_bound) =>
+ (case sure_bound of
+ NONE => new_sure_bound
+ | SOME old_bound =>
+ SOME (case btype of
+ UPPER => Float.min old_bound new_bound
+ | LOWER => Float.max old_bound new_bound))
+ end
+ in
+ case VarGraph.lookup g key of
+ NONE => NONE
+ | SOME (sure_bound, f) =>
+ let
+ val x = Inttab.fold calc_sure_bound f sure_bound
+ in
+ if x = sure_bound then NONE else x
+ end
+ end
+
+ fun propagate (key, _) (g, b) =
+ case calc_sure_bound_from_sources g key of
+ NONE => (g,b)
+ | SOME bound => (update_sure_bound g key bound,
+ if safe then
+ case get_sure_bound g key of
+ NONE => true
+ | _ => b
+ else
+ true)
+
+ val (g, b) = VarGraph.fold propagate g (g, false)
+ in
+ if b then propagate_sure_bounds safe names g else g
+ end
+
+exception Load of string;
+
+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
+ val empty = Inttab.empty
+
+ fun instab t i x = Inttab.update (i, x) t
+
+ fun isnegstr x = String.isPrefix "-" x
+ fun negstr x = if isnegstr x then String.extract (x, 1, NONE) else "-"^x
+
+ fun test_1 (lower, upper) =
+ if lower = upper then
+ (if Float.eq (lower, (~1, 0)) then ~1
+ else if Float.eq (lower, (1, 0)) then 1
+ else 0)
+ else 0
+
+ fun calcr (row_index, a) g =
+ let
+ val b = FloatSparseMatrixBuilder.v_elem_at b row_index
+ val (_, b2) = FloatArith.approx_decstr_by_bin prec (case b of NONE => "0" | SOME b => b)
+ val approx_a = FloatSparseMatrixBuilder.v_fold (fn (i, s) => fn l =>
+ (i, FloatArith.approx_decstr_by_bin prec s)::l) a []
+
+ fun fold_dest_nodes (dest_index, dest_value) g =
+ let
+ val dest_test = test_1 dest_value
+ in
+ if dest_test = 0 then
+ g
+ else let
+ val (dest_key as (_, dest_btype), row_bound) =
+ if dest_test = ~1 then
+ ((dest_index, LOWER), Float.neg b2)
+ else
+ ((dest_index, UPPER), b2)
+
+ fun fold_src_nodes (src_index, src_value as (src_lower, src_upper)) g =
+ if src_index = dest_index then g
+ else
+ let
+ val coeff = case dest_btype of
+ UPPER => (Float.neg src_upper, Float.neg src_lower)
+ | LOWER => src_value
+ in
+ if Float.sign src_lower = LESS then
+ add_edge g (src_index, UPPER) dest_key row_index coeff
+ else
+ add_edge g (src_index, LOWER) dest_key row_index coeff
+ end
+ in
+ fold fold_src_nodes approx_a (add_row_bound g dest_key row_index row_bound)
+ end
+ end
+ in
+ case approx_a of
+ [] => g
+ | [(u, a)] =>
+ let
+ val atest = test_1 a
+ in
+ if atest = ~1 then
+ update_sure_bound g (u, LOWER) (Float.neg b2)
+ else if atest = 1 then
+ update_sure_bound g (u, UPPER) b2
+ else
+ g
+ end
+ | _ => fold fold_dest_nodes approx_a g
+ 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
+
+ fun add_row_entry m index f vname value =
+ let
+ val v = (case value of
+ SOME value => FloatSparseMatrixBuilder.mk_spvec_entry 0 value
+ | NONE => FloatSparseMatrixBuilder.mk_spvec_entry' 0 (f $ (Var ((vname,0), HOLogic.realT))))
+ val vec = cons_spvec v empty_spvec
+ in
+ cons_spmat (FloatSparseMatrixBuilder.mk_spmat_entry index vec) m
+ end
+
+ fun abs_estimate i r1 r2 =
+ if i = 0 then
+ let val e = empty_spmat in (e, e) end
+ else
+ let
+ val index = xlen-i
+ val (r12_1, r12_2) = abs_estimate (i-1) r1 r2
+ val b1 = Inttab.lookup r1 index
+ val b2 = Inttab.lookup r2 index
+ in
+ (add_row_entry r12_1 index @{term "lbound :: real => real"} ((names index)^"l") b1,
+ add_row_entry r12_2 index @{term "ubound :: real => real"} ((names index)^"u") b2)
+ end
+
+ val (r1, r2) = abs_estimate xlen r1 r2
+
+ in
+ (r1, r2)
+ end
+
+fun load filename prec safe_propagation =
+ let
+ 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 (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
+ val results = Cplex.solve dualprog
+ val (optimal,v) = CplexFloatSparseMatrixConverter.convert_results results indexof
+ (*val A = FloatSparseMatrixBuilder.cut_matrix v NONE A*)
+ fun id x = x
+ val v = FloatSparseMatrixBuilder.set_vector FloatSparseMatrixBuilder.empty_matrix 0 v
+ val b = FloatSparseMatrixBuilder.transpose_matrix (FloatSparseMatrixBuilder.set_vector FloatSparseMatrixBuilder.empty_matrix 0 b)
+ val c = FloatSparseMatrixBuilder.set_vector FloatSparseMatrixBuilder.empty_matrix 0 c
+ val (y1, _) = FloatSparseMatrixBuilder.approx_matrix prec Float.positive_part v
+ val A = FloatSparseMatrixBuilder.approx_matrix prec id A
+ val (_,b2) = FloatSparseMatrixBuilder.approx_matrix prec id b
+ val c = FloatSparseMatrixBuilder.approx_matrix prec id c
+ in
+ (y1, A, b2, c, (r1, r2))
+ end handle CplexFloatSparseMatrixConverter.Converter s => (raise (Load ("Converter: "^s)))
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Matrix/matrixlp.ML Mon Jul 12 11:21:56 2010 +0200
@@ -0,0 +1,100 @@
+(* Title: HOL/Matrix/cplex/matrixlp.ML
+ Author: Steven Obua
+*)
+
+signature MATRIX_LP =
+sig
+ val lp_dual_estimate_prt : string -> int -> thm
+ val lp_dual_estimate_prt_primitive :
+ cterm * (cterm * cterm) * (cterm * cterm) * cterm * (cterm * cterm) -> 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
+
+fun inst_real thm =
+ let val certT = ctyp_of (Thm.theory_of_thm thm) in
+ Drule.export_without_context (Thm.instantiate
+ ([(certT (TVar (hd (OldTerm.term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
+ end
+
+local
+
+val cert = cterm_of @{theory}
+
+in
+
+fun lp_dual_estimate_prt_primitive (y, (A1, A2), (c1, c2), b, (r1, r2)) =
+ let
+ val th = inst_real @{thm "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
+ in th end
+
+fun lp_dual_estimate_prt lptfile prec =
+ let
+ val certificate =
+ let
+ 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)
+ end
+ in
+ lp_dual_estimate_prt_primitive certificate
+ end
+
+end
+
+fun prep ths = ComputeHOL.prep_thms ths
+
+fun inst_tvar ty thm =
+ let
+ val certT = Thm.ctyp_of (Thm.theory_of_thm thm);
+ val ord = prod_ord (prod_ord string_ord int_ord) (list_ord string_ord)
+ val v = TVar (hd (sort ord (OldTerm.term_tvars (prop_of thm))))
+ in
+ Drule.export_without_context (Thm.instantiate ([(certT v, certT ty)], []) thm)
+ end
+
+fun inst_tvars [] thms = thms
+ | inst_tvars (ty::tys) thms = inst_tvars tys (map (inst_tvar ty) thms)
+
+local
+ val ths = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_list_case" "ComputeHOL.compute_let"
+ "ComputeHOL.compute_if" "ComputeFloat.arith" "SparseMatrix.sparse_row_matrix_arith_simps"
+ "ComputeHOL.compute_bool" "ComputeHOL.compute_pair"
+ "SparseMatrix.sorted_sp_simps" "ComputeNumeral.number_norm"
+ "ComputeNumeral.natnorm"};
+ val computer = PCompute.make Compute.SML @{theory} ths []
+in
+
+fun matrix_compute c = hd (PCompute.rewrite computer [c])
+
+end
+
+fun matrix_simplify th =
+ let
+ val simp_th = matrix_compute (cprop_of th)
+ val th = Thm.strip_shyps (Thm.equal_elim simp_th th)
+ fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle _ => th (* FIXME avoid handle _ *)
+ in
+ removeTrue th
+ end
+
+fun prove_bound lptfile prec =
+ let
+ val th = lp_dual_estimate_prt lptfile prec
+ in
+ matrix_simplify th
+ end
+
+val realFromStr = the o Real.fromString;
+fun float2real (x, y) = realFromStr x * Math.pow (2.0, realFromStr y);
+
+end
--- a/src/HOL/NSA/HDeriv.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/NSA/HDeriv.thy Mon Jul 12 11:21:56 2010 +0200
@@ -26,7 +26,7 @@
definition
increment :: "[real=>real,real,hypreal] => hypreal" where
- [code del]: "increment f x h = (@inc. f NSdifferentiable x &
+ "increment f x h = (@inc. f NSdifferentiable x &
inc = ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x))"
--- a/src/HOL/NSA/HLim.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/NSA/HLim.thy Mon Jul 12 11:21:56 2010 +0200
@@ -16,18 +16,18 @@
definition
NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where
- [code del]: "f -- a --NS> L =
+ "f -- a --NS> L =
(\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
definition
isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
--{*NS definition dispenses with limit notions*}
- [code del]: "isNSCont f a = (\<forall>y. y @= star_of a -->
+ "isNSCont f a = (\<forall>y. y @= star_of a -->
( *f* f) y @= star_of (f a))"
definition
isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
- [code del]: "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
+ "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
subsection {* Limits of Functions *}
--- a/src/HOL/NSA/HLog.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/NSA/HLog.thy Mon Jul 12 11:21:56 2010 +0200
@@ -20,11 +20,11 @@
definition
powhr :: "[hypreal,hypreal] => hypreal" (infixr "powhr" 80) where
- [transfer_unfold, code del]: "x powhr a = starfun2 (op powr) x a"
+ [transfer_unfold]: "x powhr a = starfun2 (op powr) x a"
definition
hlog :: "[hypreal,hypreal] => hypreal" where
- [transfer_unfold, code del]: "hlog a x = starfun2 log a x"
+ [transfer_unfold]: "hlog a x = starfun2 log a x"
lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
by (simp add: powhr_def starfun2_star_n)
--- a/src/HOL/NSA/HSEQ.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/NSA/HSEQ.thy Mon Jul 12 11:21:56 2010 +0200
@@ -16,7 +16,7 @@
NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
("((_)/ ----NS> (_))" [60, 60] 60) where
--{*Nonstandard definition of convergence of sequence*}
- [code del]: "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
+ "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
definition
nslim :: "(nat => 'a::real_normed_vector) => 'a" where
@@ -31,12 +31,12 @@
definition
NSBseq :: "(nat => 'a::real_normed_vector) => bool" where
--{*Nonstandard definition for bounded sequence*}
- [code del]: "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
+ "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
definition
NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where
--{*Nonstandard definition*}
- [code del]: "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
+ "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
subsection {* Limits of Sequences *}
--- a/src/HOL/NSA/HSeries.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/NSA/HSeries.thy Mon Jul 12 11:21:56 2010 +0200
@@ -13,7 +13,7 @@
definition
sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" where
- [code del]: "sumhr =
+ "sumhr =
(%(M,N,f). starfun2 (%m n. setsum f {m..<n}) M N)"
definition
@@ -22,7 +22,7 @@
definition
NSsummable :: "(nat=>real) => bool" where
- [code del]: "NSsummable f = (\<exists>s. f NSsums s)"
+ "NSsummable f = (\<exists>s. f NSsums s)"
definition
NSsuminf :: "(nat=>real) => real" where
--- a/src/HOL/NSA/HyperDef.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/NSA/HyperDef.thy Mon Jul 12 11:21:56 2010 +0200
@@ -45,7 +45,7 @@
begin
definition
- star_scaleR_def [transfer_unfold, code del]: "scaleR r \<equiv> *f* (scaleR r)"
+ star_scaleR_def [transfer_unfold]: "scaleR r \<equiv> *f* (scaleR r)"
instance ..
@@ -111,7 +111,7 @@
definition
of_hypreal :: "hypreal \<Rightarrow> 'a::real_algebra_1 star" where
- [transfer_unfold, code del]: "of_hypreal = *f* of_real"
+ [transfer_unfold]: "of_hypreal = *f* of_real"
lemma Standard_of_hypreal [simp]:
"r \<in> Standard \<Longrightarrow> of_hypreal r \<in> Standard"
@@ -435,7 +435,7 @@
subsection{*Powers with Hypernatural Exponents*}
definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
- hyperpow_def [transfer_unfold, code del]: "R pow N = ( *f2* op ^) R N"
+ hyperpow_def [transfer_unfold]: "R pow N = ( *f2* op ^) R N"
(* hypernatural powers of hyperreals *)
lemma Standard_hyperpow [simp]:
--- a/src/HOL/NSA/HyperNat.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/NSA/HyperNat.thy Mon Jul 12 11:21:56 2010 +0200
@@ -19,7 +19,7 @@
definition
hSuc :: "hypnat => hypnat" where
- hSuc_def [transfer_unfold, code del]: "hSuc = *f* Suc"
+ hSuc_def [transfer_unfold]: "hSuc = *f* Suc"
subsection{*Properties Transferred from Naturals*}
@@ -366,7 +366,7 @@
definition
of_hypnat :: "hypnat \<Rightarrow> 'a::semiring_1_cancel star" where
- of_hypnat_def [transfer_unfold, code del]: "of_hypnat = *f* of_nat"
+ of_hypnat_def [transfer_unfold]: "of_hypnat = *f* of_nat"
lemma of_hypnat_0 [simp]: "of_hypnat 0 = 0"
by transfer (rule of_nat_0)
--- a/src/HOL/NSA/NSA.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/NSA/NSA.thy Mon Jul 12 11:21:56 2010 +0200
@@ -15,15 +15,15 @@
definition
Infinitesimal :: "('a::real_normed_vector) star set" where
- [code del]: "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
+ "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
definition
HFinite :: "('a::real_normed_vector) star set" where
- [code del]: "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
+ "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
definition
HInfinite :: "('a::real_normed_vector) star set" where
- [code del]: "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
+ "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
definition
approx :: "['a::real_normed_vector star, 'a star] => bool" (infixl "@=" 50) where
@@ -56,7 +56,7 @@
definition
scaleHR :: "real star \<Rightarrow> 'a star \<Rightarrow> 'a::real_normed_vector star" where
- [transfer_unfold, code del]: "scaleHR = starfun2 scaleR"
+ [transfer_unfold]: "scaleHR = starfun2 scaleR"
lemma Standard_hnorm [simp]: "x \<in> Standard \<Longrightarrow> hnorm x \<in> Standard"
by (simp add: hnorm_def)
--- a/src/HOL/NSA/NSCA.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/NSA/NSCA.thy Mon Jul 12 11:21:56 2010 +0200
@@ -16,7 +16,7 @@
definition --{* standard part map*}
stc :: "hcomplex => hcomplex" where
- [code del]: "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
+ "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
subsection{*Closure Laws for SComplex, the Standard Complex Numbers*}
--- a/src/HOL/NSA/NSComplex.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/NSA/NSComplex.thy Mon Jul 12 11:21:56 2010 +0200
@@ -25,11 +25,11 @@
definition
hRe :: "hcomplex => hypreal" where
- [code del]: "hRe = *f* Re"
+ "hRe = *f* Re"
definition
hIm :: "hcomplex => hypreal" where
- [code del]: "hIm = *f* Im"
+ "hIm = *f* Im"
(*------ imaginary unit ----------*)
@@ -42,22 +42,22 @@
definition
hcnj :: "hcomplex => hcomplex" where
- [code del]: "hcnj = *f* cnj"
+ "hcnj = *f* cnj"
(*------------ Argand -------------*)
definition
hsgn :: "hcomplex => hcomplex" where
- [code del]: "hsgn = *f* sgn"
+ "hsgn = *f* sgn"
definition
harg :: "hcomplex => hypreal" where
- [code del]: "harg = *f* arg"
+ "harg = *f* arg"
definition
(* abbreviation for (cos a + i sin a) *)
hcis :: "hypreal => hcomplex" where
- [code del]:"hcis = *f* cis"
+ "hcis = *f* cis"
(*----- injection from hyperreals -----*)
@@ -68,16 +68,16 @@
definition
(* abbreviation for r*(cos a + i sin a) *)
hrcis :: "[hypreal, hypreal] => hcomplex" where
- [code del]: "hrcis = *f2* rcis"
+ "hrcis = *f2* rcis"
(*------------ e ^ (x + iy) ------------*)
definition
hexpi :: "hcomplex => hcomplex" where
- [code del]: "hexpi = *f* expi"
+ "hexpi = *f* expi"
definition
HComplex :: "[hypreal,hypreal] => hcomplex" where
- [code del]: "HComplex = *f2* Complex"
+ "HComplex = *f2* Complex"
lemmas hcomplex_defs [transfer_unfold] =
hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def
--- a/src/HOL/NSA/Star.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/NSA/Star.thy Mon Jul 12 11:21:56 2010 +0200
@@ -17,12 +17,12 @@
definition
InternalSets :: "'a star set set" where
- [code del]: "InternalSets = {X. \<exists>As. X = *sn* As}"
+ "InternalSets = {X. \<exists>As. X = *sn* As}"
definition
(* nonstandard extension of function *)
is_starext :: "['a star => 'a star, 'a => 'a] => bool" where
- [code del]: "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
+ "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
definition
@@ -32,7 +32,7 @@
definition
InternalFuns :: "('a star => 'b star) set" where
- [code del]:"InternalFuns = {X. \<exists>F. X = *fn* F}"
+ "InternalFuns = {X. \<exists>F. X = *fn* F}"
(*--------------------------------------------------------
--- a/src/HOL/NSA/StarDef.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/NSA/StarDef.thy Mon Jul 12 11:21:56 2010 +0200
@@ -290,7 +290,7 @@
subsection {* Internal predicates *}
definition unstar :: "bool star \<Rightarrow> bool" where
- [code del]: "unstar b \<longleftrightarrow> b = star_of True"
+ "unstar b \<longleftrightarrow> b = star_of True"
lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)"
by (simp add: unstar_def star_of_def star_n_eq_iff)
@@ -431,7 +431,7 @@
begin
definition
- star_zero_def [code del]: "0 \<equiv> star_of 0"
+ star_zero_def: "0 \<equiv> star_of 0"
instance ..
@@ -441,7 +441,7 @@
begin
definition
- star_one_def [code del]: "1 \<equiv> star_of 1"
+ star_one_def: "1 \<equiv> star_of 1"
instance ..
@@ -451,7 +451,7 @@
begin
definition
- star_add_def [code del]: "(op +) \<equiv> *f2* (op +)"
+ star_add_def: "(op +) \<equiv> *f2* (op +)"
instance ..
@@ -461,7 +461,7 @@
begin
definition
- star_mult_def [code del]: "(op *) \<equiv> *f2* (op *)"
+ star_mult_def: "(op *) \<equiv> *f2* (op *)"
instance ..
@@ -471,7 +471,7 @@
begin
definition
- star_minus_def [code del]: "uminus \<equiv> *f* uminus"
+ star_minus_def: "uminus \<equiv> *f* uminus"
instance ..
@@ -481,7 +481,7 @@
begin
definition
- star_diff_def [code del]: "(op -) \<equiv> *f2* (op -)"
+ star_diff_def: "(op -) \<equiv> *f2* (op -)"
instance ..
--- a/src/HOL/Nat.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Nat.thy Mon Jul 12 11:21:56 2010 +0200
@@ -48,7 +48,7 @@
instantiation nat :: zero
begin
-definition Zero_nat_def [code del]:
+definition Zero_nat_def:
"0 = Abs_Nat Zero_Rep"
instance ..
@@ -1362,9 +1362,8 @@
context semiring_1
begin
-definition
- Nats :: "'a set" where
- [code del]: "Nats = range of_nat"
+definition Nats :: "'a set" where
+ "Nats = range of_nat"
notation (xsymbols)
Nats ("\<nat>")
--- a/src/HOL/Number_Theory/Primes.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Number_Theory/Primes.thy Mon Jul 12 11:21:56 2010 +0200
@@ -45,7 +45,7 @@
definition
prime_nat :: "nat \<Rightarrow> bool"
where
- [code del]: "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
+ "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
instance proof qed
@@ -58,7 +58,7 @@
definition
prime_int :: "int \<Rightarrow> bool"
where
- [code del]: "prime_int p = prime (nat p)"
+ "prime_int p = prime (nat p)"
instance proof qed
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy Mon Jul 12 11:21:56 2010 +0200
@@ -17,7 +17,7 @@
definition
is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
- [code del]: "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
+ "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
(\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
text {* Uniqueness *}
--- a/src/HOL/Old_Number_Theory/Primes.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Primes.thy Mon Jul 12 11:21:56 2010 +0200
@@ -15,7 +15,7 @@
definition
prime :: "nat \<Rightarrow> bool" where
- [code del]: "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
+ "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
lemma two_is_prime: "prime 2"
--- a/src/HOL/Orderings.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Orderings.thy Mon Jul 12 11:21:56 2010 +0200
@@ -264,10 +264,10 @@
text {* min/max *}
definition (in ord) min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
- [code del]: "min a b = (if a \<le> b then a else b)"
+ "min a b = (if a \<le> b then a else b)"
definition (in ord) max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
- [code del]: "max a b = (if a \<le> b then b else a)"
+ "max a b = (if a \<le> b then b else a)"
lemma min_le_iff_disj:
"min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
@@ -1196,10 +1196,10 @@
begin
definition
- le_bool_def [code del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
+ le_bool_def: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
definition
- less_bool_def [code del]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
+ less_bool_def: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
definition
top_bool_eq: "top = True"
@@ -1244,10 +1244,10 @@
begin
definition
- le_fun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
+ le_fun_def: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
definition
- less_fun_def [code del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
+ less_fun_def: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
instance ..
--- a/src/HOL/Predicate.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Predicate.thy Mon Jul 12 11:21:56 2010 +0200
@@ -408,10 +408,10 @@
"P \<squnion> Q = Pred (eval P \<squnion> eval Q)"
definition
- [code del]: "\<Sqinter>A = Pred (INFI A eval)"
+ "\<Sqinter>A = Pred (INFI A eval)"
definition
- [code del]: "\<Squnion>A = Pred (SUPR A eval)"
+ "\<Squnion>A = Pred (SUPR A eval)"
definition
"- P = Pred (- eval P)"
@@ -873,7 +873,7 @@
definition the :: "'a pred => 'a"
where
- [code del]: "the A = (THE x. eval A x)"
+ "the A = (THE x. eval A x)"
lemma the_eq[code]: "the A = singleton (\<lambda>x. not_unique A) A"
by (auto simp add: the_def singleton_def not_unique_def)
--- a/src/HOL/Product_Type.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Product_Type.thy Mon Jul 12 11:21:56 2010 +0200
@@ -829,7 +829,7 @@
*}
definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
- [code del]: "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
+ "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
lemma prod_fun [simp, code]: "prod_fun f g (a, b) = (f a, g b)"
by (simp add: prod_fun_def)
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Mon Jul 12 11:21:56 2010 +0200
@@ -42,7 +42,7 @@
"(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_int_raw"
definition
- minus_int_def [code del]: "z - w = z + (-w\<Colon>int)"
+ minus_int_def: "z - w = z + (-w\<Colon>int)"
fun
times_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -61,7 +61,7 @@
le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_int_raw"
definition
- less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
+ less_int_def: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
definition
zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
--- a/src/HOL/RealDef.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/RealDef.thy Mon Jul 12 11:21:56 2010 +0200
@@ -1498,8 +1498,6 @@
subsection{*Numerals and Arithmetic*}
-declare number_of_real_def [code del]
-
lemma [code_unfold_post]:
"number_of k = real_of_int (number_of k)"
unfolding number_of_is_id number_of_real_def ..
--- a/src/HOL/RealVector.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/RealVector.thy Mon Jul 12 11:21:56 2010 +0200
@@ -305,9 +305,8 @@
subsection {* The Set of Real Numbers *}
-definition
- Reals :: "'a::real_algebra_1 set" where
- [code del]: "Reals = range of_real"
+definition Reals :: "'a::real_algebra_1 set" where
+ "Reals = range of_real"
notation (xsymbols)
Reals ("\<real>")
@@ -786,7 +785,7 @@
definition dist_real_def:
"dist x y = \<bar>x - y\<bar>"
-definition open_real_def [code del]:
+definition open_real_def:
"open (S :: real set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
instance
--- a/src/HOL/Recdef.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Recdef.thy Mon Jul 12 11:21:56 2010 +0200
@@ -38,7 +38,7 @@
definition
wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" where
- [code del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
+ "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
subsection{*Well-Founded Recursion*}
--- a/src/HOL/Rings.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Rings.thy Mon Jul 12 11:21:56 2010 +0200
@@ -96,7 +96,7 @@
begin
definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where
- [code del]: "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
+ "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"
unfolding dvd_def ..
--- a/src/HOL/SEQ.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/SEQ.thy Mon Jul 12 11:21:56 2010 +0200
@@ -31,7 +31,7 @@
definition
Bseq :: "(nat => 'a::real_normed_vector) => bool" where
--{*Standard definition for bounded sequence*}
- [code del]: "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
+ "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
definition
monoseq :: "(nat=>real)=>bool" where
@@ -39,27 +39,27 @@
The use of disjunction here complicates proofs considerably.
One alternative is to add a Boolean argument to indicate the direction.
Another is to develop the notions of increasing and decreasing first.*}
- [code del]: "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
+ "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
definition
incseq :: "(nat=>real)=>bool" where
--{*Increasing sequence*}
- [code del]: "incseq X = (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)"
+ "incseq X = (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)"
definition
decseq :: "(nat=>real)=>bool" where
--{*Increasing sequence*}
- [code del]: "decseq X = (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
+ "decseq X = (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
definition
subseq :: "(nat => nat) => bool" where
--{*Definition of subsequence*}
- [code del]: "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
+ "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
definition
Cauchy :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
--{*Standard definition of the Cauchy condition*}
- [code del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
+ "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
subsection {* Bounded Sequences *}
--- a/src/HOL/Set.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Set.thy Mon Jul 12 11:21:56 2010 +0200
@@ -1574,7 +1574,7 @@
subsubsection {* Inverse image of a function *}
definition vimage :: "('a => 'b) => 'b set => 'a set" (infixr "-`" 90) where
- [code del]: "f -` B == {x. f x : B}"
+ "f -` B == {x. f x : B}"
lemma vimage_eq [simp]: "(a : f -` B) = (f a : B)"
by (unfold vimage_def) blast
@@ -1657,7 +1657,7 @@
subsubsection {* Getting the Contents of a Singleton Set *}
definition contents :: "'a set \<Rightarrow> 'a" where
- [code del]: "contents X = (THE x. X = {x})"
+ "contents X = (THE x. X = {x})"
lemma contents_eq [simp]: "contents {x} = x"
by (simp add: contents_def)
--- a/src/HOL/SupInf.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/SupInf.thy Mon Jul 12 11:21:56 2010 +0200
@@ -9,7 +9,7 @@
instantiation real :: Sup
begin
definition
- Sup_real_def [code del]: "Sup X == (LEAST z::real. \<forall>x\<in>X. x\<le>z)"
+ Sup_real_def: "Sup X == (LEAST z::real. \<forall>x\<in>X. x\<le>z)"
instance ..
end
@@ -17,7 +17,7 @@
instantiation real :: Inf
begin
definition
- Inf_real_def [code del]: "Inf (X::real set) == - (Sup (uminus ` X))"
+ Inf_real_def: "Inf (X::real set) == - (Sup (uminus ` X))"
instance ..
end
--- a/src/HOL/Wellfounded.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/Wellfounded.thy Mon Jul 12 11:21:56 2010 +0200
@@ -682,9 +682,8 @@
text{* Lexicographic combinations *}
-definition
- lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" (infixr "<*lex*>" 80) where
- [code del]: "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
+definition lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" (infixr "<*lex*>" 80) where
+ "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"
apply (unfold wf_def lex_prod_def)
@@ -819,10 +818,8 @@
by (force elim!: max_ext.cases)
-definition
- min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set"
-where
- [code del]: "min_ext r = {(X, Y) | X Y. X \<noteq> {} \<and> (\<forall>y \<in> Y. (\<exists>x \<in> X. (x, y) \<in> r))}"
+definition min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" where
+ "min_ext r = {(X, Y) | X Y. X \<noteq> {} \<and> (\<forall>y \<in> Y. (\<exists>x \<in> X. (x, y) \<in> r))}"
lemma min_ext_wf:
assumes "wf r"
--- a/src/HOL/ex/Dedekind_Real.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy Mon Jul 12 11:21:56 2010 +0200
@@ -19,7 +19,7 @@
definition
cut :: "rat set => bool" where
- [code del]: "cut A = ({} \<subset> A &
+ "cut A = ({} \<subset> A &
A < {r. 0 < r} &
(\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
@@ -49,7 +49,7 @@
definition
psup :: "preal set => preal" where
- [code del]: "psup P = Abs_preal (\<Union>X \<in> P. Rep_preal X)"
+ "psup P = Abs_preal (\<Union>X \<in> P. Rep_preal X)"
definition
add_set :: "[rat set,rat set] => rat set" where
@@ -57,7 +57,7 @@
definition
diff_set :: "[rat set,rat set] => rat set" where
- [code del]: "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
+ "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
definition
mult_set :: "[rat set,rat set] => rat set" where
@@ -65,17 +65,17 @@
definition
inverse_set :: "rat set => rat set" where
- [code del]: "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
+ "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
instantiation preal :: "{ord, plus, minus, times, inverse, one}"
begin
definition
- preal_less_def [code del]:
+ preal_less_def:
"R < S == Rep_preal R < Rep_preal S"
definition
- preal_le_def [code del]:
+ preal_le_def:
"R \<le> S == Rep_preal R \<subseteq> Rep_preal S"
definition
@@ -1162,7 +1162,7 @@
definition
realrel :: "((preal * preal) * (preal * preal)) set" where
- [code del]: "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
+ "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
typedef (Real) real = "UNIV//realrel"
by (auto simp add: quotient_def)
@@ -1170,46 +1170,46 @@
definition
(** these don't use the overloaded "real" function: users don't see them **)
real_of_preal :: "preal => real" where
- [code del]: "real_of_preal m = Abs_Real (realrel `` {(m + 1, 1)})"
+ "real_of_preal m = Abs_Real (realrel `` {(m + 1, 1)})"
instantiation real :: "{zero, one, plus, minus, uminus, times, inverse, ord, abs, sgn}"
begin
definition
- real_zero_def [code del]: "0 = Abs_Real(realrel``{(1, 1)})"
+ real_zero_def: "0 = Abs_Real(realrel``{(1, 1)})"
definition
- real_one_def [code del]: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
+ real_one_def: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
definition
- real_add_def [code del]: "z + w =
+ real_add_def: "z + w =
contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
{ Abs_Real(realrel``{(x+u, y+v)}) })"
definition
- real_minus_def [code del]: "- r = contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
+ real_minus_def: "- r = contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
definition
- real_diff_def [code del]: "r - (s::real) = r + - s"
+ real_diff_def: "r - (s::real) = r + - s"
definition
- real_mult_def [code del]:
+ real_mult_def:
"z * w =
contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
{ Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
definition
- real_inverse_def [code del]: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
+ real_inverse_def: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
definition
- real_divide_def [code del]: "R / (S::real) = R * inverse S"
+ real_divide_def: "R / (S::real) = R * inverse S"
definition
- real_le_def [code del]: "z \<le> (w::real) \<longleftrightarrow>
+ real_le_def: "z \<le> (w::real) \<longleftrightarrow>
(\<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Real z & (u,v) \<in> Rep_Real w)"
definition
- real_less_def [code del]: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
+ real_less_def: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
definition
real_abs_def: "abs (r::real) = (if r < 0 then - r else r)"
@@ -1656,7 +1656,7 @@
begin
definition
- real_number_of_def [code del]: "(number_of w :: real) = of_int w"
+ real_number_of_def: "(number_of w :: real) = of_int w"
instance
by intro_classes (simp add: real_number_of_def)
--- a/src/HOL/ex/Gauge_Integration.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/ex/Gauge_Integration.thy Mon Jul 12 11:21:56 2010 +0200
@@ -28,7 +28,7 @@
definition
gauge :: "[real set, real => real] => bool" where
- [code del]: "gauge E g = (\<forall>x\<in>E. 0 < g(x))"
+ "gauge E g = (\<forall>x\<in>E. 0 < g(x))"
subsection {* Gauge-fine divisions *}
@@ -259,7 +259,7 @@
definition
Integral :: "[(real*real),real=>real,real] => bool" where
- [code del]: "Integral = (%(a,b) f k. \<forall>e > 0.
+ "Integral = (%(a,b) f k. \<forall>e > 0.
(\<exists>\<delta>. gauge {a .. b} \<delta> &
(\<forall>D. fine \<delta> (a,b) D -->
\<bar>rsum D f - k\<bar> < e)))"
--- a/src/HOL/ex/Numeral.thy Mon Jul 12 11:21:27 2010 +0200
+++ b/src/HOL/ex/Numeral.thy Mon Jul 12 11:21:56 2010 +0200
@@ -106,16 +106,16 @@
begin
definition plus_num :: "num \<Rightarrow> num \<Rightarrow> num" where
- [code del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
+ "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
definition times_num :: "num \<Rightarrow> num \<Rightarrow> num" where
- [code del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
+ "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
definition less_eq_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
- [code del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
+ "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
definition less_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
- [code del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
+ "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
instance ..
@@ -761,10 +761,10 @@
lemmas [code_unfold] = Pls_def [symmetric] Mns_def [symmetric]
definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
- [simp, code del]: "sub m n = (of_num m - of_num n)"
+ [simp]: "sub m n = (of_num m - of_num n)"
definition dup :: "int \<Rightarrow> int" where
- [code del]: "dup k = 2 * k"
+ "dup k = 2 * k"
lemma Dig_sub [code]:
"sub One One = 0"