src/HOL/Matrix/cplex/MatrixLP.thy
changeset 23665 825bea0266db
parent 23174 3913451b0418
     1.1 --- a/src/HOL/Matrix/cplex/MatrixLP.thy	Mon Jul 09 17:38:40 2007 +0200
     1.2 +++ b/src/HOL/Matrix/cplex/MatrixLP.thy	Mon Jul 09 17:39:55 2007 +0200
     1.3 @@ -4,65 +4,7 @@
     1.4  *)
     1.5  
     1.6  theory MatrixLP 
     1.7 -imports Cplex "~~/src/Tools/Compute_Oracle/Compute_Oracle"
     1.8 -uses ("matrixlp.ML")
     1.9 +imports Cplex 
    1.10 +uses "matrixlp.ML"
    1.11  begin
    1.12 -
    1.13 -constdefs
    1.14 -  list_case_compute :: "'b list \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b list \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.15 -  "list_case_compute l a f == list_case a f l"
    1.16 -
    1.17 -lemma list_case_compute: "list_case = (\<lambda> (a::'a) f (l::'b list). list_case_compute l a f)"
    1.18 -  apply (rule ext)+
    1.19 -  apply (simp add: list_case_compute_def)
    1.20 -  done
    1.21 -
    1.22 -lemma list_case_compute_empty: "list_case_compute ([]::'b list) = (\<lambda> (a::'a) f. a)"
    1.23 -  apply (rule ext)+
    1.24 -  apply (simp add: list_case_compute_def)
    1.25 -  done
    1.26 -
    1.27 -lemma list_case_compute_cons: "list_case_compute (u#v) = (\<lambda> (a::'a) f. (f (u::'b) v))"
    1.28 -  apply (rule ext)+
    1.29 -  apply (simp add: list_case_compute_def)
    1.30 -  done
    1.31 -
    1.32 -lemma If_True: "(If True) = (\<lambda> x y. x)"
    1.33 -  apply (rule ext)+
    1.34 -  apply auto
    1.35 -  done
    1.36 -
    1.37 -lemma If_False: "(If False) = (\<lambda> x y. y)"
    1.38 -  apply (rule ext)+
    1.39 -  apply auto
    1.40 -  done
    1.41 -
    1.42 -lemma Let_compute: "Let (x::'a) f = ((f x)::'b)"
    1.43 -  by (simp add: Let_def)
    1.44 -
    1.45 -lemma fst_compute: "fst (a::'a, b::'b) = a"
    1.46 -  by auto
    1.47 -
    1.48 -lemma snd_compute: "snd (a::'a, b::'b) = b"
    1.49 -  by auto
    1.50 -
    1.51 -lemma bool1: "(\<not> True) = False"  by blast
    1.52 -lemma bool2: "(\<not> False) = True"  by blast
    1.53 -lemma bool3: "((P\<Colon>bool) \<and> True) = P" by blast
    1.54 -lemma bool4: "(True \<and> (P\<Colon>bool)) = P" by blast
    1.55 -lemma bool5: "((P\<Colon>bool) \<and> False) = False" by blast
    1.56 -lemma bool6: "(False \<and> (P\<Colon>bool)) = False" by blast
    1.57 -lemma bool7: "((P\<Colon>bool) \<or> True) = True" by blast
    1.58 -lemma bool8: "(True \<or> (P\<Colon>bool)) = True" by blast
    1.59 -lemma bool9: "((P\<Colon>bool) \<or> False) = P" by blast
    1.60 -lemma bool10: "(False \<or> (P\<Colon>bool)) = P" by blast
    1.61 -lemmas boolarith = bool1 bool2 bool3 bool4 bool5 bool6 bool7 bool8 bool9 bool10
    1.62 -
    1.63 -lemmas float_arith = Float.arith
    1.64 -lemmas sparse_row_matrix_arith_simps = SparseMatrix.sparse_row_matrix_arith_simps
    1.65 -lemmas sorted_sp_simps = SparseMatrix.sorted_sp_simps
    1.66 -lemmas fst_snd_conv = Product_Type.fst_conv Product_Type.snd_conv
    1.67 -
    1.68 -use "matrixlp.ML"
    1.69 -
    1.70  end