src/HOL/OrderedGroup.thy
changeset 22452 8a86fd2a1bf0
parent 22422 ee19cdb07528
child 22482 8fc3d7237e03
     1.1 --- a/src/HOL/OrderedGroup.thy	Fri Mar 16 21:32:07 2007 +0100
     1.2 +++ b/src/HOL/OrderedGroup.thy	Fri Mar 16 21:32:08 2007 +0100
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  (*  Title:   HOL/OrderedGroup.thy
     1.6      ID:      $Id$
     1.7      Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel,
     1.8 @@ -8,7 +7,7 @@
     1.9  header {* Ordered Groups *}
    1.10  
    1.11  theory OrderedGroup
    1.12 -imports LOrder
    1.13 +imports Lattices
    1.14  uses "~~/src/Provers/Arith/abel_cancel.ML"
    1.15  begin
    1.16  
    1.17 @@ -204,7 +203,7 @@
    1.18  instance pordered_cancel_ab_semigroup_add \<subseteq> pordered_ab_semigroup_add ..
    1.19  
    1.20  class pordered_ab_semigroup_add_imp_le = pordered_cancel_ab_semigroup_add +
    1.21 -  assumes add_le_imp_le_left: "c \<^loc>+ a \<sqsubseteq> c + b \<Longrightarrow> a \<sqsubseteq> b"
    1.22 +  assumes add_le_imp_le_left: "c \<^loc>+ a \<sqsubseteq> c \<^loc>+ b \<Longrightarrow> a \<sqsubseteq> b"
    1.23  
    1.24  class pordered_ab_group_add = ab_group_add + pordered_ab_semigroup_add
    1.25  
    1.26 @@ -565,13 +564,19 @@
    1.27  lemma le_iff_diff_le_0: "(a \<le> b) = (a-b \<le> (0::'a::pordered_ab_group_add))"
    1.28  by (simp add: compare_rls)
    1.29  
    1.30 +
    1.31  subsection {* Lattice Ordered (Abelian) Groups *}
    1.32  
    1.33 -axclass lordered_ab_group_meet < pordered_ab_group_add, meet_semilorder
    1.34 +class lordered_ab_group_meet = pordered_ab_group_add + lower_semilattice
    1.35 +
    1.36 +class lordered_ab_group_join = pordered_ab_group_add + upper_semilattice
    1.37  
    1.38 -axclass lordered_ab_group_join < pordered_ab_group_add, join_semilorder
    1.39 +class lordered_ab_group = pordered_ab_group_add + lattice
    1.40  
    1.41 -lemma add_inf_distrib_left: "a + (inf b c) = inf (a + b) (a + (c::'a::{pordered_ab_group_add, meet_semilorder}))"
    1.42 +instance lordered_ab_group \<subseteq> lordered_ab_group_meet by default
    1.43 +instance lordered_ab_group \<subseteq> lordered_ab_group_join by default
    1.44 +
    1.45 +lemma add_inf_distrib_left: "a + inf b c = inf (a + b) (a + (c::'a::{pordered_ab_group_add, lower_semilattice}))"
    1.46  apply (rule order_antisym)
    1.47  apply (simp_all add: le_infI)
    1.48  apply (rule add_le_imp_le_left [of "-a"])
    1.49 @@ -580,7 +585,7 @@
    1.50  apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+
    1.51  done
    1.52  
    1.53 -lemma add_sup_distrib_left: "a + (sup b c) = sup (a + b) (a+ (c::'a::{pordered_ab_group_add, join_semilorder}))" 
    1.54 +lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a+ (c::'a::{pordered_ab_group_add, upper_semilattice}))" 
    1.55  apply (rule order_antisym)
    1.56  apply (rule add_le_imp_le_left [of "-a"])
    1.57  apply (simp only: add_assoc[symmetric], simp)
    1.58 @@ -590,55 +595,53 @@
    1.59  apply (simp_all)
    1.60  done
    1.61  
    1.62 -lemma is_join_neg_inf: "is_join (% (a::'a::{pordered_ab_group_add, meet_semilorder}) b. - (inf (-a) (-b)))"
    1.63 -apply (auto simp add: is_join_def)
    1.64 -apply (rule_tac c="inf (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_inf_distrib_left)
    1.65 -apply (rule_tac c="inf (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_inf_distrib_left)
    1.66 -apply (subst neg_le_iff_le[symmetric]) 
    1.67 -apply (simp add: le_infI)
    1.68 -done
    1.69 -
    1.70 -lemma is_meet_neg_sup: "is_meet (% (a::'a::{pordered_ab_group_add, join_semilorder}) b. - (sup (-a) (-b)))"
    1.71 -apply (auto simp add: is_meet_def)
    1.72 -apply (rule_tac c="sup (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_sup_distrib_left)
    1.73 -apply (rule_tac c="sup (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_sup_distrib_left)
    1.74 -apply (subst neg_le_iff_le[symmetric]) 
    1.75 -apply (simp add: le_supI)
    1.76 -done
    1.77 -
    1.78 -axclass lordered_ab_group \<subseteq> pordered_ab_group_add, lorder
    1.79 -
    1.80 -instance lordered_ab_group_join \<subseteq> lordered_ab_group
    1.81 -proof
    1.82 -  show "? m. is_meet (m::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_join))" by (blast intro: is_meet_neg_sup)
    1.83 -qed
    1.84 -
    1.85 -instance lordered_ab_group_meet \<subseteq> lordered_ab_group
    1.86 -proof 
    1.87 -  show "? j. is_join (j::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_meet))" by (blast intro: is_join_neg_inf)
    1.88 -qed
    1.89 -
    1.90 -lemma add_inf_distrib_right: "(inf a b) + (c::'a::lordered_ab_group) = inf (a+c) (b+c)"
    1.91 +lemma add_inf_distrib_right: "inf a b + (c::'a::lordered_ab_group) = inf (a+c) (b+c)"
    1.92  proof -
    1.93 -  have "c + (inf a b) = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left)
    1.94 +  have "c + inf a b = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left)
    1.95    thus ?thesis by (simp add: add_commute)
    1.96  qed
    1.97  
    1.98 -lemma add_sup_distrib_right: "(sup a b) + (c::'a::lordered_ab_group) = sup (a+c) (b+c)"
    1.99 +lemma add_sup_distrib_right: "sup a b + (c::'a::lordered_ab_group) = sup (a+c) (b+c)"
   1.100  proof -
   1.101 -  have "c + (sup a b) = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left)
   1.102 +  have "c + sup a b = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left)
   1.103    thus ?thesis by (simp add: add_commute)
   1.104  qed
   1.105  
   1.106  lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
   1.107  
   1.108 -lemma sup_eq_neg_inf: "sup a (b::'a::lordered_ab_group) = - inf (-a) (-b)"
   1.109 -by (simp add: is_join_unique[OF is_join_join is_join_neg_inf])
   1.110 +lemma inf_eq_neg_sup: "inf a (b\<Colon>'a\<Colon>lordered_ab_group) = - sup (-a) (-b)"
   1.111 +proof (rule inf_unique)
   1.112 +  fix a b :: 'a
   1.113 +  show "- sup (-a) (-b) \<le> a" by (rule add_le_imp_le_right [of _ "sup (-a) (-b)"])
   1.114 +    (simp, simp add: add_sup_distrib_left)
   1.115 +next
   1.116 +  fix a b :: 'a
   1.117 +  show "- sup (-a) (-b) \<le> b" by (rule add_le_imp_le_right [of _ "sup (-a) (-b)"])
   1.118 +    (simp, simp add: add_sup_distrib_left)
   1.119 +next
   1.120 +  fix a b c :: 'a
   1.121 +  assume "a \<le> b" "a \<le> c"
   1.122 +  then show "a \<le> - sup (-b) (-c)" by (subst neg_le_iff_le [symmetric])
   1.123 +    (simp add: le_supI)
   1.124 +qed
   1.125 +  
   1.126 +lemma sup_eq_neg_inf: "sup a (b\<Colon>'a\<Colon>lordered_ab_group) = - inf (-a) (-b)"
   1.127 +proof (rule sup_unique)
   1.128 +  fix a b :: 'a
   1.129 +  show "a \<le> - inf (-a) (-b)" by (rule add_le_imp_le_right [of _ "inf (-a) (-b)"])
   1.130 +    (simp, simp add: add_inf_distrib_left)
   1.131 +next
   1.132 +  fix a b :: 'a
   1.133 +  show "b \<le> - inf (-a) (-b)" by (rule add_le_imp_le_right [of _ "inf (-a) (-b)"])
   1.134 +    (simp, simp add: add_inf_distrib_left)
   1.135 +next
   1.136 +  fix a b c :: 'a
   1.137 +  assume "a \<le> c" "b \<le> c"
   1.138 +  then show "- inf (-a) (-b) \<le> c" by (subst neg_le_iff_le [symmetric])
   1.139 +    (simp add: le_infI)
   1.140 +qed
   1.141  
   1.142 -lemma inf_eq_neg_sup: "inf a (b::'a::lordered_ab_group) = - sup (-a) (-b)"
   1.143 -by (simp add: is_meet_unique[OF is_meet_meet is_meet_neg_sup])
   1.144 -
   1.145 -lemma add_eq_inf_sup: "a + b = (sup a b) + (inf a (b::'a::lordered_ab_group))"
   1.146 +lemma add_eq_inf_sup: "a + b = sup a b + inf a (b\<Colon>'a\<Colon>lordered_ab_group)"
   1.147  proof -
   1.148    have "0 = - inf 0 (a-b) + inf (a-b) 0" by (simp add: inf_commute)
   1.149    hence "0 = sup 0 (b-a) + inf (a-b) 0" by (simp add: inf_eq_neg_sup)
   1.150 @@ -761,8 +764,8 @@
   1.151    with a show ?thesis by simp 
   1.152  qed
   1.153  
   1.154 -axclass lordered_ab_group_abs \<subseteq> lordered_ab_group
   1.155 -  abs_lattice: "abs x = sup x (-x)"
   1.156 +class lordered_ab_group_abs = lordered_ab_group +
   1.157 +  assumes abs_lattice: "abs x = sup x (uminus x)"
   1.158  
   1.159  lemma abs_zero[simp]: "abs 0 = (0::'a::lordered_ab_group_abs)"
   1.160  by (simp add: abs_lattice)
   1.161 @@ -786,7 +789,7 @@
   1.162  proof -
   1.163    note b = add_le_cancel_right[of a a "-a",symmetric,simplified]
   1.164    have c: "a + a = 0 \<Longrightarrow> -a = a" by (rule add_right_imp_eq[of _ a], simp)
   1.165 -  show ?thesis by (auto simp add: max_def b linorder_not_less join_max)
   1.166 +  show ?thesis by (auto simp add: max_def b linorder_not_less sup_max)
   1.167  qed
   1.168  
   1.169  lemma abs_if_lattice: "\<bar>a\<bar> = (if a < 0 then -a else (a::'a::{lordered_ab_group_abs, linorder}))"
   1.170 @@ -1131,8 +1134,6 @@
   1.171  val le_iff_diff_le_0 = thm "le_iff_diff_le_0";
   1.172  val add_inf_distrib_left = thm "add_inf_distrib_left";
   1.173  val add_sup_distrib_left = thm "add_sup_distrib_left";
   1.174 -val is_join_neg_inf = thm "is_join_neg_inf";
   1.175 -val is_meet_neg_sup = thm "is_meet_neg_sup";
   1.176  val add_sup_distrib_right = thm "add_sup_distrib_right";
   1.177  val add_inf_distrib_right = thm "add_inf_distrib_right";
   1.178  val add_sup_inf_distribs = thms "add_sup_inf_distribs";