src/HOL/Matrix/Matrix.thy
changeset 22422 ee19cdb07528
parent 21312 1d39091a3208
child 22452 8a86fd2a1bf0
     1.1 --- a/src/HOL/Matrix/Matrix.thy	Tue Mar 06 16:40:32 2007 +0100
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Fri Mar 09 08:45:50 2007 +0100
     1.3 @@ -7,23 +7,21 @@
     1.4  imports MatrixGeneral
     1.5  begin
     1.6  
     1.7 -instance matrix :: (minus) minus ..
     1.8 +instance matrix :: ("{plus, zero}") plus
     1.9 +  plus_matrix_def: "A + B \<equiv> combine_matrix (op +) A B" ..
    1.10  
    1.11 -instance matrix :: (plus) plus ..
    1.12 -
    1.13 -instance matrix :: ("{plus,times}") times ..
    1.14 +instance matrix :: ("{minus, zero}") minus
    1.15 +  minus_matrix_def: "- A \<equiv> apply_matrix uminus A"
    1.16 +  diff_matrix_def: "A - B \<equiv> combine_matrix (op -) A B" ..
    1.17  
    1.18 -defs (overloaded)
    1.19 -  plus_matrix_def: "A + B == combine_matrix (op +) A B"
    1.20 -  diff_matrix_def: "A - B == combine_matrix (op -) A B"
    1.21 -  minus_matrix_def: "- A == apply_matrix uminus A"
    1.22 -  times_matrix_def: "A * B == mult_matrix (op *) (op +) A B"
    1.23 +instance matrix :: ("{plus, times, zero}") times
    1.24 +  times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" ..
    1.25  
    1.26 -lemma is_meet_combine_matrix_meet: "is_meet (combine_matrix meet)"
    1.27 -  by (simp_all add: is_meet_def le_matrix_def meet_left_le meet_right_le le_meetI)
    1.28 +lemma is_meet_combine_matrix_meet: "is_meet (combine_matrix inf)"
    1.29 +  by (simp_all add: is_meet_def le_matrix_def inf_le1 inf_le2 le_infI)
    1.30  
    1.31 -lemma is_join_combine_matrix_join: "is_join (combine_matrix join)"
    1.32 -  by (simp_all add: is_join_def le_matrix_def join_left_le join_right_le join_leI)
    1.33 +lemma is_join_combine_matrix_join: "is_join (combine_matrix sup)"
    1.34 +  by (simp_all add: is_join_def le_matrix_def sup_ge1 sup_ge2 le_supI)
    1.35  
    1.36  instance matrix :: (lordered_ab_group) lordered_ab_group_meet
    1.37  proof 
    1.38 @@ -58,7 +56,7 @@
    1.39  qed
    1.40  
    1.41  defs (overloaded)
    1.42 -  abs_matrix_def: "abs (A::('a::lordered_ab_group) matrix) == join A (- A)"
    1.43 +  abs_matrix_def: "abs (A::('a::lordered_ab_group) matrix) == sup A (- A)"
    1.44  
    1.45  instance matrix :: (lordered_ring) lordered_ring
    1.46  proof
    1.47 @@ -78,7 +76,7 @@
    1.48      apply (rule r_distributive_matrix[simplified r_distributive_def, THEN spec, THEN spec, THEN spec])
    1.49      apply (simp_all add: associative_def commutative_def ring_eq_simps)
    1.50      done  
    1.51 -  show "abs A = join A (-A)" 
    1.52 +  show "abs A = sup A (-A)" 
    1.53      by (simp add: abs_matrix_def)
    1.54    assume a: "A \<le> B"
    1.55    assume b: "0 \<le> C"
    1.56 @@ -102,7 +100,6 @@
    1.57  apply (simp add: times_matrix_def)
    1.58  apply (simp add: Rep_mult_matrix)
    1.59  done
    1.60 - 
    1.61  
    1.62  lemma apply_matrix_add: "! x y. f (x+y) = (f x) + (f y) \<Longrightarrow> f 0 = (0::'a) \<Longrightarrow> apply_matrix f ((a::('a::lordered_ab_group) matrix) + b) = (apply_matrix f a) + (apply_matrix f b)"
    1.63  apply (subst Rep_matrix_inject[symmetric])
    1.64 @@ -122,9 +119,9 @@
    1.65  lemma ncols_mult: "ncols ((A::('a::lordered_ring) matrix) * B) <= ncols B"
    1.66  by (simp add: times_matrix_def mult_ncols)
    1.67  
    1.68 -constdefs
    1.69 -  one_matrix :: "nat \<Rightarrow> ('a::{zero,one}) matrix"
    1.70 -  "one_matrix n == Abs_matrix (% j i. if j = i & j < n then 1 else 0)"
    1.71 +definition
    1.72 +  one_matrix :: "nat \<Rightarrow> ('a::{zero,one}) matrix" where
    1.73 +  "one_matrix n = Abs_matrix (% j i. if j = i & j < n then 1 else 0)"
    1.74  
    1.75  lemma Rep_one_matrix[simp]: "Rep_matrix (one_matrix n) j i = (if (j = i & j < n) then 1 else 0)"
    1.76  apply (simp add: one_matrix_def)
    1.77 @@ -289,13 +286,13 @@
    1.78  lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group)) x y = - (Rep_matrix A x y)"
    1.79    by (simp add: minus_matrix_def)
    1.80  
    1.81 -lemma join_matrix: "join (A::('a::lordered_ring) matrix) B = combine_matrix join A B"  
    1.82 -  apply (insert join_unique[of "(combine_matrix join)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_join_combine_matrix_join])
    1.83 +lemma join_matrix: "sup (A::('a::lordered_ring) matrix) B = combine_matrix sup A B"  
    1.84 +  apply (insert join_unique[of "(combine_matrix sup)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_join_combine_matrix_join])
    1.85    apply (simp)
    1.86    done
    1.87  
    1.88 -lemma meet_matrix: "meet (A::('a::lordered_ring) matrix) B = combine_matrix meet A B"
    1.89 -  apply (insert meet_unique[of "(combine_matrix meet)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_meet_combine_matrix_meet])
    1.90 +lemma meet_matrix: "inf (A::('a::lordered_ring) matrix) B = combine_matrix inf A B"
    1.91 +  apply (insert meet_unique[of "(combine_matrix inf)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_meet_combine_matrix_meet])
    1.92    apply (simp)
    1.93    done
    1.94