src/HOL/Library/Product_Vector.thy
changeset 44066 d74182c93f04
parent 37678 0040bafffdef
child 44126 ce44e70d0c47
equal deleted inserted replaced
44065:eb64ffccfc75 44066:d74182c93f04
    26   unfolding scaleR_prod_def by simp
    26   unfolding scaleR_prod_def by simp
    27 
    27 
    28 instance proof
    28 instance proof
    29   fix a b :: real and x y :: "'a \<times> 'b"
    29   fix a b :: real and x y :: "'a \<times> 'b"
    30   show "scaleR a (x + y) = scaleR a x + scaleR a y"
    30   show "scaleR a (x + y) = scaleR a x + scaleR a y"
    31     by (simp add: expand_prod_eq scaleR_right_distrib)
    31     by (simp add: prod_eq_iff scaleR_right_distrib)
    32   show "scaleR (a + b) x = scaleR a x + scaleR b x"
    32   show "scaleR (a + b) x = scaleR a x + scaleR b x"
    33     by (simp add: expand_prod_eq scaleR_left_distrib)
    33     by (simp add: prod_eq_iff scaleR_left_distrib)
    34   show "scaleR a (scaleR b x) = scaleR (a * b) x"
    34   show "scaleR a (scaleR b x) = scaleR (a * b) x"
    35     by (simp add: expand_prod_eq)
    35     by (simp add: prod_eq_iff)
    36   show "scaleR 1 x = x"
    36   show "scaleR 1 x = x"
    37     by (simp add: expand_prod_eq)
    37     by (simp add: prod_eq_iff)
    38 qed
    38 qed
    39 
    39 
    40 end
    40 end
    41 
    41 
    42 subsection {* Product is a topological space *}
    42 subsection {* Product is a topological space *}
   172 unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge2)
   172 unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge2)
   173 
   173 
   174 instance proof
   174 instance proof
   175   fix x y :: "'a \<times> 'b"
   175   fix x y :: "'a \<times> 'b"
   176   show "dist x y = 0 \<longleftrightarrow> x = y"
   176   show "dist x y = 0 \<longleftrightarrow> x = y"
   177     unfolding dist_prod_def expand_prod_eq by simp
   177     unfolding dist_prod_def prod_eq_iff by simp
   178 next
   178 next
   179   fix x y z :: "'a \<times> 'b"
   179   fix x y z :: "'a \<times> 'b"
   180   show "dist x y \<le> dist x z + dist y z"
   180   show "dist x y \<le> dist x z + dist y z"
   181     unfolding dist_prod_def
   181     unfolding dist_prod_def
   182     by (intro order_trans [OF _ real_sqrt_sum_squares_triangle_ineq]
   182     by (intro order_trans [OF _ real_sqrt_sum_squares_triangle_ineq]
   371   fix r :: real and x y :: "'a \<times> 'b"
   371   fix r :: real and x y :: "'a \<times> 'b"
   372   show "0 \<le> norm x"
   372   show "0 \<le> norm x"
   373     unfolding norm_prod_def by simp
   373     unfolding norm_prod_def by simp
   374   show "norm x = 0 \<longleftrightarrow> x = 0"
   374   show "norm x = 0 \<longleftrightarrow> x = 0"
   375     unfolding norm_prod_def
   375     unfolding norm_prod_def
   376     by (simp add: expand_prod_eq)
   376     by (simp add: prod_eq_iff)
   377   show "norm (x + y) \<le> norm x + norm y"
   377   show "norm (x + y) \<le> norm x + norm y"
   378     unfolding norm_prod_def
   378     unfolding norm_prod_def
   379     apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq])
   379     apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq])
   380     apply (simp add: add_mono power_mono norm_triangle_ineq)
   380     apply (simp add: add_mono power_mono norm_triangle_ineq)
   381     done
   381     done
   421     by (simp add: right_distrib)
   421     by (simp add: right_distrib)
   422   show "0 \<le> inner x x"
   422   show "0 \<le> inner x x"
   423     unfolding inner_prod_def
   423     unfolding inner_prod_def
   424     by (intro add_nonneg_nonneg inner_ge_zero)
   424     by (intro add_nonneg_nonneg inner_ge_zero)
   425   show "inner x x = 0 \<longleftrightarrow> x = 0"
   425   show "inner x x = 0 \<longleftrightarrow> x = 0"
   426     unfolding inner_prod_def expand_prod_eq
   426     unfolding inner_prod_def prod_eq_iff
   427     by (simp add: add_nonneg_eq_0_iff)
   427     by (simp add: add_nonneg_eq_0_iff)
   428   show "norm x = sqrt (inner x x)"
   428   show "norm x = sqrt (inner x x)"
   429     unfolding norm_prod_def inner_prod_def
   429     unfolding norm_prod_def inner_prod_def
   430     by (simp add: power2_norm_eq_inner)
   430     by (simp add: power2_norm_eq_inner)
   431 qed
   431 qed