src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy
changeset 56166 9a241bc276cd
parent 55413 a8e96847523c
child 56188 0268784f60da
     1.1 --- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Sat Mar 15 16:54:32 2014 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Sun Mar 16 18:09:04 2014 +0100
     1.3 @@ -39,10 +39,12 @@
     1.4    hence "\<And>i. (\<lambda>x. x \<bullet> i) ` X \<noteq> {}" by simp
     1.5    thus "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X" "(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z"
     1.6      by (auto simp: eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def
     1.7 +      simp del: Inf_class.Inf_image_eq Sup_class.Sup_image_eq
     1.8        intro!: cInf_greatest cSup_least)
     1.9  qed (force intro!: cInf_lower cSup_upper
    1.10        simp: bdd_below_def bdd_above_def preorder_class.bdd_below_def preorder_class.bdd_above_def
    1.11 -        eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def)+
    1.12 +        eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def
    1.13 +      simp del: Inf_class.Inf_image_eq Sup_class.Sup_image_eq)+
    1.14  
    1.15  lemma inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)"
    1.16    and inner_Basis_sup_left: "i \<in> Basis \<Longrightarrow> sup x y \<bullet> i = sup (x \<bullet> i) (y \<bullet> i)"
    1.17 @@ -51,7 +53,7 @@
    1.18  
    1.19  lemma inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x:X. f x) \<bullet> i = (INF x:X. f x \<bullet> i)"
    1.20    and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x:X. f x) \<bullet> i = (SUP x:X. f x \<bullet> i)"
    1.21 -  by (simp_all add: INF_def SUP_def eucl_Sup eucl_Inf)
    1.22 +  using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: comp_def)
    1.23  
    1.24  lemma abs_inner: "i \<in> Basis \<Longrightarrow> abs x \<bullet> i = abs (x \<bullet> i)"
    1.25    by (auto simp: eucl_abs)
    1.26 @@ -87,7 +89,7 @@
    1.27    shows "Sup s = X"
    1.28    using assms
    1.29    unfolding eucl_Sup euclidean_representation_setsum
    1.30 -  by (auto simp: Sup_class.SUP_def intro!: conditionally_complete_lattice_class.cSup_eq_maximum)
    1.31 +  by (auto simp: Sup_class.SUP_def simp del: Sup_class.Sup_image_eq intro!: conditionally_complete_lattice_class.cSup_eq_maximum)
    1.32  
    1.33  lemma Inf_eq_minimum_componentwise:
    1.34    assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b"
    1.35 @@ -96,7 +98,7 @@
    1.36    shows "Inf s = X"
    1.37    using assms
    1.38    unfolding eucl_Inf euclidean_representation_setsum
    1.39 -  by (auto simp: Inf_class.INF_def intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
    1.40 +  by (auto simp: Inf_class.INF_def simp del: Inf_class.Inf_image_eq intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
    1.41  
    1.42  end
    1.43  
    1.44 @@ -115,10 +117,11 @@
    1.45        and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b"
    1.46      by auto
    1.47    hence "Inf ?proj = x \<bullet> b"
    1.48 -    by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
    1.49 +    by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum simp del: Inf_class.Inf_image_eq)
    1.50    hence "x \<bullet> b = Inf X \<bullet> b"
    1.51 -    by (auto simp: eucl_Inf Inf_class.INF_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis`
    1.52 -      setsum_delta cong: if_cong)
    1.53 +    by (auto simp: eucl_Inf Inf_class.INF_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis` setsum_delta
    1.54 +      simp del: Inf_class.Inf_image_eq
    1.55 +      cong: if_cong)
    1.56    with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Inf X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> x \<bullet> b \<le> y \<bullet> b)" by blast
    1.57  qed
    1.58  
    1.59 @@ -137,10 +140,10 @@
    1.60        and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b"
    1.61      by auto
    1.62    hence "Sup ?proj = x \<bullet> b"
    1.63 -    by (auto intro!: cSup_eq_maximum)
    1.64 +    by (auto intro!: cSup_eq_maximum simp del: Sup_image_eq)
    1.65    hence "x \<bullet> b = Sup X \<bullet> b"
    1.66 -    by (auto simp: eucl_Sup[where 'a='a] SUP_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis`
    1.67 -      setsum_delta cong: if_cong)
    1.68 +    by (auto simp: eucl_Sup[where 'a='a] SUP_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis` setsum_delta
    1.69 +      simp del: Sup_image_eq cong: if_cong)
    1.70    with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Sup X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> y \<bullet> b \<le> x \<bullet> b)" by blast
    1.71  qed
    1.72  
    1.73 @@ -715,7 +718,7 @@
    1.74  lemma diameter_closed_interval:
    1.75    fixes a b::"'a::ordered_euclidean_space"
    1.76    shows "a \<le> b \<Longrightarrow> diameter {a..b} = dist a b"
    1.77 -  by (force simp add: diameter_def SUP_def intro!: cSup_eq_maximum setL2_mono
    1.78 +  by (force simp add: diameter_def SUP_def simp del: Sup_image_eq intro!: cSup_eq_maximum setL2_mono
    1.79       simp: euclidean_dist_l2[where 'a='a] eucl_le[where 'a='a] dist_norm)
    1.80  
    1.81  text {* Intervals in general, including infinite and mixtures of open and closed. *}