# HG changeset patch
# User wenzelm
# Date 1488966659 -3600
# Node ID a7394aa4d21ce6276ae6b5e724e293ba9c0ba6de
# Parent  fa299b4e50c38d343fc26a5d9f6d89af3c1325f9
tuned proofs;

diff -r fa299b4e50c3 -r a7394aa4d21c src/HOL/Library/Lattice_Algebras.thy
--- a/src/HOL/Library/Lattice_Algebras.thy	Wed Mar 08 10:29:40 2017 +0100
+++ b/src/HOL/Library/Lattice_Algebras.thy	Wed Mar 08 10:50:59 2017 +0100
@@ -3,7 +3,7 @@
 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
@@ -11,7 +11,7 @@
 
 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
@@ -31,11 +31,11 @@
 
 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)"
@@ -80,9 +80,8 @@
   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)"
@@ -121,12 +120,12 @@
 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"
@@ -146,21 +145,15 @@
   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)
@@ -182,7 +175,7 @@
   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
@@ -195,7 +188,7 @@
   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
 
@@ -206,14 +199,14 @@
   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
 
@@ -238,49 +231,11 @@
 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 -
@@ -302,7 +257,10 @@
     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 -
@@ -405,7 +363,7 @@
     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
@@ -606,15 +564,13 @@
 
 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