author wenzelm Wed, 08 Mar 2017 10:50:59 +0100 changeset 65151 a7394aa4d21c parent 65150 fa299b4e50c3 child 65152 a920012ae16a
tuned proofs;
```--- 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

@@ -11,7 +11,7 @@

lemma add_inf_distrib_left: "a + inf b c = inf (a + b) (a + c)"
apply (rule antisym)
apply (rule add_le_imp_le_left [of "uminus a"])
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 (rule add_le_imp_le_left [of "uminus a"])
+   apply (simp only: add.assoc [symmetric], simp)
apply (rule le_supI)
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)"])
-  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 @@

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" _])
-    done
+  assume ?lhs
+  show ?rhs
next
-  assume ?r
-  then show ?l
-    apply -
-    apply (rule add_le_imp_le_right[of _ "b" _])
-    apply simp
-    done
+  assume ?rhs
+  show ?lhs
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"
-  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"
-    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 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

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)
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