|
16873
|
1 |
(* Title: HOL/Matrix/cplex/MatrixLP.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Steven Obua
|
|
|
4 |
*)
|
|
|
5 |
|
|
|
6 |
theory MatrixLP
|
|
23174
|
7 |
imports Cplex "~~/src/Tools/Compute_Oracle/Compute_Oracle"
|
|
20782
|
8 |
uses ("matrixlp.ML")
|
|
16873
|
9 |
begin
|
|
|
10 |
|
|
|
11 |
constdefs
|
|
|
12 |
list_case_compute :: "'b list \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b list \<Rightarrow> 'a) \<Rightarrow> 'a"
|
|
|
13 |
"list_case_compute l a f == list_case a f l"
|
|
|
14 |
|
|
|
15 |
lemma list_case_compute: "list_case = (\<lambda> (a::'a) f (l::'b list). list_case_compute l a f)"
|
|
|
16 |
apply (rule ext)+
|
|
|
17 |
apply (simp add: list_case_compute_def)
|
|
|
18 |
done
|
|
|
19 |
|
|
|
20 |
lemma list_case_compute_empty: "list_case_compute ([]::'b list) = (\<lambda> (a::'a) f. a)"
|
|
|
21 |
apply (rule ext)+
|
|
|
22 |
apply (simp add: list_case_compute_def)
|
|
|
23 |
done
|
|
|
24 |
|
|
|
25 |
lemma list_case_compute_cons: "list_case_compute (u#v) = (\<lambda> (a::'a) f. (f (u::'b) v))"
|
|
|
26 |
apply (rule ext)+
|
|
|
27 |
apply (simp add: list_case_compute_def)
|
|
|
28 |
done
|
|
|
29 |
|
|
|
30 |
lemma If_True: "(If True) = (\<lambda> x y. x)"
|
|
|
31 |
apply (rule ext)+
|
|
|
32 |
apply auto
|
|
|
33 |
done
|
|
|
34 |
|
|
|
35 |
lemma If_False: "(If False) = (\<lambda> x y. y)"
|
|
|
36 |
apply (rule ext)+
|
|
|
37 |
apply auto
|
|
|
38 |
done
|
|
|
39 |
|
|
|
40 |
lemma Let_compute: "Let (x::'a) f = ((f x)::'b)"
|
|
|
41 |
by (simp add: Let_def)
|
|
|
42 |
|
|
|
43 |
lemma fst_compute: "fst (a::'a, b::'b) = a"
|
|
|
44 |
by auto
|
|
|
45 |
|
|
|
46 |
lemma snd_compute: "snd (a::'a, b::'b) = b"
|
|
|
47 |
by auto
|
|
|
48 |
|
|
|
49 |
lemma bool1: "(\<not> True) = False" by blast
|
|
|
50 |
lemma bool2: "(\<not> False) = True" by blast
|
|
|
51 |
lemma bool3: "((P\<Colon>bool) \<and> True) = P" by blast
|
|
|
52 |
lemma bool4: "(True \<and> (P\<Colon>bool)) = P" by blast
|
|
|
53 |
lemma bool5: "((P\<Colon>bool) \<and> False) = False" by blast
|
|
|
54 |
lemma bool6: "(False \<and> (P\<Colon>bool)) = False" by blast
|
|
|
55 |
lemma bool7: "((P\<Colon>bool) \<or> True) = True" by blast
|
|
|
56 |
lemma bool8: "(True \<or> (P\<Colon>bool)) = True" by blast
|
|
|
57 |
lemma bool9: "((P\<Colon>bool) \<or> False) = P" by blast
|
|
|
58 |
lemma bool10: "(False \<or> (P\<Colon>bool)) = P" by blast
|
|
|
59 |
lemmas boolarith = bool1 bool2 bool3 bool4 bool5 bool6 bool7 bool8 bool9 bool10
|
|
|
60 |
|
|
|
61 |
lemmas float_arith = Float.arith
|
|
|
62 |
lemmas sparse_row_matrix_arith_simps = SparseMatrix.sparse_row_matrix_arith_simps
|
|
|
63 |
lemmas sorted_sp_simps = SparseMatrix.sorted_sp_simps
|
|
|
64 |
lemmas fst_snd_conv = Product_Type.fst_conv Product_Type.snd_conv
|
|
|
65 |
|
|
20782
|
66 |
use "matrixlp.ML"
|
|
|
67 |
|
|
16873
|
68 |
end
|