src/HOLCF/LowerPD.thy
changeset 29990 b11793ea15a3
parent 29672 07f3da9fd2a0
child 30729 461ee3e49ad3
     1.1 --- a/src/HOLCF/LowerPD.thy	Thu Feb 19 05:50:26 2009 -0800
     1.2 +++ b/src/HOLCF/LowerPD.thy	Thu Feb 19 06:47:06 2009 -0800
     1.3 @@ -245,22 +245,25 @@
     1.4  apply (simp add: PDPlus_commute)
     1.5  done
     1.6  
     1.7 -lemma lower_plus_absorb: "xs +\<flat> xs = xs"
     1.8 +lemma lower_plus_absorb [simp]: "xs +\<flat> xs = xs"
     1.9  apply (induct xs rule: lower_pd.principal_induct, simp)
    1.10  apply (simp add: PDPlus_absorb)
    1.11  done
    1.12  
    1.13 -interpretation aci_lower_plus!: ab_semigroup_idem_mult "op +\<flat>"
    1.14 -  proof qed (rule lower_plus_assoc lower_plus_commute lower_plus_absorb)+
    1.15 +lemma lower_plus_left_commute: "xs +\<flat> (ys +\<flat> zs) = ys +\<flat> (xs +\<flat> zs)"
    1.16 +by (rule mk_left_commute [of "op +\<flat>", OF lower_plus_assoc lower_plus_commute])
    1.17  
    1.18 -lemma lower_plus_left_commute: "xs +\<flat> (ys +\<flat> zs) = ys +\<flat> (xs +\<flat> zs)"
    1.19 -by (rule aci_lower_plus.mult_left_commute)
    1.20 +lemma lower_plus_left_absorb [simp]: "xs +\<flat> (xs +\<flat> ys) = xs +\<flat> ys"
    1.21 +by (simp only: lower_plus_assoc [symmetric] lower_plus_absorb)
    1.22  
    1.23 -lemma lower_plus_left_absorb: "xs +\<flat> (xs +\<flat> ys) = xs +\<flat> ys"
    1.24 -by (rule aci_lower_plus.mult_left_idem)
    1.25 -(*
    1.26 -lemmas lower_plus_aci = aci_lower_plus.mult_ac_idem
    1.27 -*)
    1.28 +text {* Useful for @{text "simp add: lower_plus_ac"} *}
    1.29 +lemmas lower_plus_ac =
    1.30 +  lower_plus_assoc lower_plus_commute lower_plus_left_commute
    1.31 +
    1.32 +text {* Useful for @{text "simp only: lower_plus_aci"} *}
    1.33 +lemmas lower_plus_aci =
    1.34 +  lower_plus_ac lower_plus_absorb lower_plus_left_absorb
    1.35 +
    1.36  lemma lower_plus_less1: "xs \<sqsubseteq> xs +\<flat> ys"
    1.37  apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
    1.38  apply (simp add: PDPlus_lower_less)
    1.39 @@ -315,14 +318,8 @@
    1.40    lower_plus_less_iff
    1.41    lower_unit_less_plus_iff
    1.42  
    1.43 -lemma fooble:
    1.44 -  fixes f :: "'a::po \<Rightarrow> 'b::po"
    1.45 -  assumes f: "\<And>x y. f x \<sqsubseteq> f y \<longleftrightarrow> x \<sqsubseteq> y"
    1.46 -  shows "f x = f y \<longleftrightarrow> x = y"
    1.47 -unfolding po_eq_conv by (simp add: f)
    1.48 -
    1.49  lemma lower_unit_eq_iff [simp]: "{x}\<flat> = {y}\<flat> \<longleftrightarrow> x = y"
    1.50 -by (rule lower_unit_less_iff [THEN fooble])
    1.51 +by (simp add: po_eq_conv)
    1.52  
    1.53  lemma lower_unit_strict [simp]: "{\<bottom>}\<flat> = \<bottom>"
    1.54  unfolding inst_lower_pd_pcpo Rep_compact_bot [symmetric] by simp
    1.55 @@ -399,7 +396,7 @@
    1.56  apply unfold_locales
    1.57  apply (simp add: lower_plus_assoc)
    1.58  apply (simp add: lower_plus_commute)
    1.59 -apply (simp add: lower_plus_absorb eta_cfun)
    1.60 +apply (simp add: eta_cfun)
    1.61  done
    1.62  
    1.63  lemma lower_bind_basis_simps [simp]: