src/HOL/OrderedGroup.thy
changeset 32075 e8e0fb5da77a
parent 32010 cb1a1c94b4cd
parent 32064 53ca12ff305d
child 32436 10cd49e0c067
     1.1 --- a/src/HOL/OrderedGroup.thy	Sat Jul 18 22:53:02 2009 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Mon Jul 20 08:32:07 2009 +0200
     1.3 @@ -1075,16 +1075,16 @@
     1.4  lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
     1.5  
     1.6  lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
     1.7 -by (simp add: pprt_def le_iff_sup sup_ACI)
     1.8 +by (simp add: pprt_def le_iff_sup sup_aci)
     1.9  
    1.10  lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
    1.11 -by (simp add: nprt_def le_iff_inf inf_ACI)
    1.12 +by (simp add: nprt_def le_iff_inf inf_aci)
    1.13  
    1.14  lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
    1.15 -by (simp add: pprt_def le_iff_sup sup_ACI)
    1.16 +by (simp add: pprt_def le_iff_sup sup_aci)
    1.17  
    1.18  lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
    1.19 -by (simp add: nprt_def le_iff_inf inf_ACI)
    1.20 +by (simp add: nprt_def le_iff_inf inf_aci)
    1.21  
    1.22  lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
    1.23  proof -
    1.24 @@ -1120,7 +1120,7 @@
    1.25    assume "0 <= a + a"
    1.26    hence a:"inf (a+a) 0 = 0" by (simp add: le_iff_inf inf_commute)
    1.27    have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_")
    1.28 -    by (simp add: add_sup_inf_distribs inf_ACI)
    1.29 +    by (simp add: add_sup_inf_distribs inf_aci)
    1.30    hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
    1.31    hence "inf a 0 = 0" by (simp only: add_right_cancel)
    1.32    then show "0 <= a" by (simp add: le_iff_inf inf_commute)    
    1.33 @@ -1206,10 +1206,10 @@
    1.34  by (simp add: le_iff_inf nprt_def inf_commute)
    1.35  
    1.36  lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
    1.37 -by (simp add: le_iff_sup pprt_def sup_ACI sup_assoc [symmetric, of a])
    1.38 +by (simp add: le_iff_sup pprt_def sup_aci sup_assoc [symmetric, of a])
    1.39  
    1.40  lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
    1.41 -by (simp add: le_iff_inf nprt_def inf_ACI inf_assoc [symmetric, of a])
    1.42 +by (simp add: le_iff_inf nprt_def inf_aci inf_assoc [symmetric, of a])
    1.43  
    1.44  end
    1.45  
    1.46 @@ -1230,7 +1230,7 @@
    1.47    then have "0 \<le> sup a (- a)" unfolding abs_lattice .
    1.48    then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1)
    1.49    then show ?thesis
    1.50 -    by (simp add: add_sup_inf_distribs sup_ACI
    1.51 +    by (simp add: add_sup_inf_distribs sup_aci
    1.52        pprt_def nprt_def diff_minus abs_lattice)
    1.53  qed
    1.54  
    1.55 @@ -1254,7 +1254,7 @@
    1.56    show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
    1.57    proof -
    1.58      have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
    1.59 -      by (simp add: abs_lattice add_sup_inf_distribs sup_ACI diff_minus)
    1.60 +      by (simp add: abs_lattice add_sup_inf_distribs sup_aci diff_minus)
    1.61      have a:"a+b <= sup ?m ?n" by (simp)
    1.62      have b:"-a-b <= ?n" by (simp) 
    1.63      have c:"?n <= sup ?m ?n" by (simp)