src/HOL/Library/Lattice_Algebras.thy

 (*  Author:     Steven Obua, TU Muenchen *)
 
 section \<open>Various algebraic structures combined with a lattice\<close>
 
 theory Lattice_Algebras
-imports Complex_Main
+  imports Complex_Main
 begin
 
 class semilattice_inf_ab_group_add = ordered_ab_group_add + semilattice_inf
 begin
 
 lemma add_inf_distrib_left: "a + inf b c = inf (a + b) (a + c)"
   apply (rule antisym)
-  apply (simp_all add: le_infI)
+   apply (simp_all add: le_infI)
   apply (rule add_le_imp_le_left [of "uminus a"])
   apply (simp only: add.assoc [symmetric], simp add: diff_le_eq add.commute)
   done
 
 lemma add_inf_distrib_right: "inf a b + c = inf (a + c) (b + c)"

 class semilattice_sup_ab_group_add = ordered_ab_group_add + semilattice_sup
 begin
 
 lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a + c)"
   apply (rule antisym)
-  apply (rule add_le_imp_le_left [of "uminus a"])
-  apply (simp only: add.assoc [symmetric], simp)
-  apply (simp add: le_diff_eq add.commute)
+   apply (rule add_le_imp_le_left [of "uminus a"])
+   apply (simp only: add.assoc [symmetric], simp)
+   apply (simp add: le_diff_eq add.commute)
   apply (rule le_supI)
-  apply (rule add_le_imp_le_left [of "a"], simp only: add.assoc[symmetric], simp)+
+   apply (rule add_le_imp_le_left [of "a"], simp only: add.assoc[symmetric], simp)+
   done
 
 lemma add_sup_distrib_right: "sup a b + c = sup (a + c) (b + c)"
 proof -
   have "c + sup a b = sup (c+a) (c+b)"

     by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"])
       (simp, simp add: add_inf_distrib_left)
   show "b \<le> - inf (- a) (- b)"
     by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"])
       (simp, simp add: add_inf_distrib_left)
-  assume "a \<le> c" "b \<le> c"
-  then show "- inf (- a) (- b) \<le> c"
-    by (subst neg_le_iff_le [symmetric]) (simp add: le_infI)
+  show "- inf (- a) (- b) \<le> c" if "a \<le> c" "b \<le> c"
+    using that by (subst neg_le_iff_le [symmetric]) (simp add: le_infI)
 qed
 
 lemma neg_inf_eq_sup: "- inf a b = sup (- a) (- b)"
   by (simp add: inf_eq_neg_sup)
 

   where "pprt x = sup x 0"
 
 lemma pprt_neg: "pprt (- x) = - nprt x"
 proof -
   have "sup (- x) 0 = sup (- x) (- 0)"
-    unfolding minus_zero ..
+    by (simp only: minus_zero)
   also have "\<dots> = - inf x 0"
-    unfolding neg_inf_eq_sup ..
+    by (simp only: neg_inf_eq_sup)
   finally have "sup (- x) 0 = - inf x 0" .
   then show ?thesis
-    unfolding pprt_def nprt_def .
+    by (simp only: pprt_def nprt_def)
 qed
 
 lemma nprt_neg: "nprt (- x) = - pprt x"
 proof -
   from pprt_neg have "pprt (- (- x)) = - nprt (- x)" .

 
 lemma nprt_le_zero[simp]: "nprt a \<le> 0"
   by (simp add: nprt_def)
 
 lemma le_eq_neg: "a \<le> - b \<longleftrightarrow> a + b \<le> 0"
-  (is "?l = ?r")
+  (is "?lhs = ?rhs")
 proof
-  assume ?l
-  then show ?r
-    apply -
-    apply (rule add_le_imp_le_right[of _ "uminus b" _])
-    apply (simp add: add.assoc)
-    done
+  assume ?lhs
+  show ?rhs
+    by (rule add_le_imp_le_right[of _ "uminus b" _]) (simp add: add.assoc \<open>?lhs\<close>)
 next
-  assume ?r
-  then show ?l
-    apply -
-    apply (rule add_le_imp_le_right[of _ "b" _])
-    apply simp
-    done
+  assume ?rhs
+  show ?lhs
+    by (rule add_le_imp_le_right[of _ "b" _]) (simp add: \<open>?rhs\<close>)
 qed
 
 lemma pprt_0[simp]: "pprt 0 = 0" by (simp add: pprt_def)
 lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
 

 
 lemma sup_0_imp_0:
   assumes "sup a (- a) = 0"
   shows "a = 0"
 proof -
-  have p: "0 \<le> a" if "sup a (- a) = 0" for a :: 'a
+  have pos: "0 \<le> a" if "sup a (- a) = 0" for a :: 'a
   proof -
     from that have "sup a (- a) + a = a"
       by simp
     then have "sup (a + a) 0 = a"
       by (simp add: add_sup_distrib_right)

     then show ?thesis
       by (blast intro: order_trans inf_sup_ord)
   qed
   from assms have **: "sup (-a) (-(-a)) = 0"
     by (simp add: sup_commute)
-  from p[OF assms] p[OF **] show "a = 0"
+  from pos[OF assms] pos[OF **] show "a = 0"
     by simp
 qed
 
 lemma inf_0_imp_0: "inf a (- a) = 0 \<Longrightarrow> a = 0"
   apply (simp add: inf_eq_neg_sup)
   apply (simp add: sup_commute)
   apply (erule sup_0_imp_0)
   done
 
 lemma inf_0_eq_0 [simp, no_atp]: "inf a (- a) = 0 \<longleftrightarrow> a = 0"
-  apply rule
-  apply (erule inf_0_imp_0)
+  apply (rule iffI)
+   apply (erule inf_0_imp_0)
   apply simp
   done
 
 lemma sup_0_eq_0 [simp, no_atp]: "sup a (- a) = 0 \<longleftrightarrow> a = 0"
-  apply rule
-  apply (erule sup_0_imp_0)
+  apply (rule iffI)
+   apply (erule sup_0_imp_0)
   apply simp
   done
 
 lemma zero_le_double_add_iff_zero_le_single_add [simp]: "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
   (is "?lhs \<longleftrightarrow> ?rhs")

   show ?lhs if ?rhs
     by (simp add: add_mono[OF that that, simplified])
 qed
 
 lemma double_zero [simp]: "a + a = 0 \<longleftrightarrow> a = 0"
-  (is "?lhs \<longleftrightarrow> ?rhs")
-proof
-  show ?rhs if ?lhs
-  proof -
-    from that have "a + a + - a = - a"
-      by simp
-    then have "a + (a + - a) = - a"
-      by (simp only: add.assoc)
-    then have a: "- a = a"
-      by simp
-    show ?thesis
-      apply (rule antisym)
-      apply (unfold neg_le_iff_le [symmetric, of a])
-      unfolding a
-      apply simp
-      unfolding zero_le_double_add_iff_zero_le_single_add [symmetric, of a]
-      unfolding that
-      unfolding le_less
-      apply simp_all
-      done
-  qed
-  show ?lhs if ?rhs
-    using that by simp
-qed
+  using add_nonneg_eq_0_iff eq_iff by auto
 
 lemma zero_less_double_add_iff_zero_less_single_add [simp]: "0 < a + a \<longleftrightarrow> 0 < a"
-proof (cases "a = 0")
-  case True
-  then show ?thesis by auto
-next
-  case False
-  then show ?thesis
-    unfolding less_le
-    apply simp
-    apply rule
-    apply clarify
-    apply rule
-    apply assumption
-    apply (rule notI)
-    unfolding double_zero [symmetric, of a]
-    apply blast
-    done
-qed
+  by (meson le_less_trans less_add_same_cancel2 less_le_not_le
+      zero_le_double_add_iff_zero_le_single_add)
 
 lemma double_add_le_zero_iff_single_add_le_zero [simp]: "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
 proof -
   have "a + a \<le> 0 \<longleftrightarrow> 0 \<le> - (a + a)"
     by (subst le_minus_iff) simp

     by (simp only: minus_add_distrib zero_less_double_add_iff_zero_less_single_add) simp
   ultimately show ?thesis
     by blast
 qed
 
-declare neg_inf_eq_sup [simp] neg_sup_eq_inf [simp] diff_inf_eq_sup [simp] diff_sup_eq_inf [simp]
+declare neg_inf_eq_sup [simp]
+  and neg_sup_eq_inf [simp]
+  and diff_inf_eq_sup [simp]
+  and diff_sup_eq_inf [simp]
 
 lemma le_minus_self_iff: "a \<le> - a \<longleftrightarrow> a \<le> 0"
 proof -
   from add_le_cancel_left [of "uminus a" "plus a a" zero]
   have "a \<le> - a \<longleftrightarrow> a + a \<le> 0"

     have e: "- a - b = - (a + b)"
       by simp
     from a d e have "\<bar>a + b\<bar> \<le> sup ?m ?n"
       apply -
       apply (drule abs_leI)
-      apply (simp_all only: algebra_simps minus_add)
+       apply (simp_all only: algebra_simps minus_add)
       apply (metis add_uminus_conv_diff d sup_commute uminus_add_conv_diff)
       done
     with g[symmetric] show ?thesis by simp
   qed
 qed

     by (simp add: algebra_simps)
 qed
 
 instance int :: lattice_ring
 proof
-  fix k :: int
-  show "\<bar>k\<bar> = sup k (- k)"
+  show "\<bar>k\<bar> = sup k (- k)" for k :: int
     by (auto simp add: sup_int_def)
 qed
 
 instance real :: lattice_ring
 proof
-  fix a :: real
-  show "\<bar>a\<bar> = sup a (- a)"
+  show "\<bar>a\<bar> = sup a (- a)" for a :: real
     by (auto simp add: sup_real_def)
 qed
 
 end