src/HOL/Library/Lattice_Algebras.thy
changeset 57512 cc97b347b301
parent 56228 0f6dc7512023
child 57862 8f074e6e22fc
     1.1 --- a/src/HOL/Library/Lattice_Algebras.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Library/Lattice_Algebras.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4    apply (rule antisym)
     1.5    apply (simp_all add: le_infI)
     1.6    apply (rule add_le_imp_le_left [of "uminus a"])
     1.7 -  apply (simp only: add_assoc [symmetric], simp add: diff_le_eq add.commute)
     1.8 +  apply (simp only: add.assoc [symmetric], simp add: diff_le_eq add.commute)
     1.9    done
    1.10  
    1.11  lemma add_inf_distrib_right: "inf a b + c = inf (a + c) (b + c)"
    1.12 @@ -21,7 +21,7 @@
    1.13    have "c + inf a b = inf (c + a) (c + b)"
    1.14      by (simp add: add_inf_distrib_left)
    1.15    then show ?thesis
    1.16 -    by (simp add: add_commute)
    1.17 +    by (simp add: add.commute)
    1.18  qed
    1.19  
    1.20  end
    1.21 @@ -32,10 +32,10 @@
    1.22  lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a + c)"
    1.23    apply (rule antisym)
    1.24    apply (rule add_le_imp_le_left [of "uminus a"])
    1.25 -  apply (simp only: add_assoc [symmetric], simp)
    1.26 +  apply (simp only: add.assoc [symmetric], simp)
    1.27    apply (simp add: le_diff_eq add.commute)
    1.28    apply (rule le_supI)
    1.29 -  apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+
    1.30 +  apply (rule add_le_imp_le_left [of "a"], simp only: add.assoc[symmetric], simp)+
    1.31    done
    1.32  
    1.33  lemma add_sup_distrib_right: "sup a b + c = sup (a + c) (b + c)"
    1.34 @@ -43,7 +43,7 @@
    1.35    have "c + sup a b = sup (c+a) (c+b)"
    1.36      by (simp add: add_sup_distrib_left)
    1.37    then show ?thesis
    1.38 -    by (simp add: add_commute)
    1.39 +    by (simp add: add.commute)
    1.40  qed
    1.41  
    1.42  end
    1.43 @@ -151,7 +151,7 @@
    1.44    then show ?r
    1.45      apply -
    1.46      apply (rule add_le_imp_le_right[of _ "uminus b" _])
    1.47 -    apply (simp add: add_assoc)
    1.48 +    apply (simp add: add.assoc)
    1.49      done
    1.50  next
    1.51    assume ?r
    1.52 @@ -243,7 +243,7 @@
    1.53    then have "a + a + - a = - a"
    1.54      by simp
    1.55    then have "a + (a + - a) = - a"
    1.56 -    by (simp only: add_assoc)
    1.57 +    by (simp only: add.assoc)
    1.58    then have a: "- a = a"
    1.59      by simp
    1.60    show "a = 0"
    1.61 @@ -309,7 +309,7 @@
    1.62  proof -
    1.63    from add_le_cancel_left [of "uminus a" "plus a a" zero]
    1.64    have "a \<le> - a \<longleftrightarrow> a + a \<le> 0"
    1.65 -    by (simp add: add_assoc[symmetric])
    1.66 +    by (simp add: add.assoc[symmetric])
    1.67    then show ?thesis
    1.68      by simp
    1.69  qed
    1.70 @@ -318,7 +318,7 @@
    1.71  proof -
    1.72    from add_le_cancel_left [of "uminus a" zero "plus a a"]
    1.73    have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a"
    1.74 -    by (simp add: add_assoc[symmetric])
    1.75 +    by (simp add: add.assoc[symmetric])
    1.76    then show ?thesis
    1.77      by simp
    1.78  qed