1.1 --- a/src/HOLCF/LowerPD.thy	Fri Nov 26 18:07:00 2010 +0100
     1.2 +++ b/src/HOLCF/LowerPD.thy	Fri Nov 26 14:10:34 2010 -0800
     1.3 @@ -195,7 +195,7 @@
     1.4  apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
     1.5  done
     1.6  
     1.7 -lemma lower_plus_below_iff:
     1.8 +lemma lower_plus_below_iff [simp]:
     1.9    "xs +\<flat> ys \<sqsubseteq> zs \<longleftrightarrow> xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs"
    1.10  apply safe
    1.11  apply (erule below_trans [OF lower_plus_below1])
    1.12 @@ -203,7 +203,7 @@
    1.13  apply (erule (1) lower_plus_least)
    1.14  done
    1.15  
    1.16 -lemma lower_unit_below_plus_iff:
    1.17 +lemma lower_unit_below_plus_iff [simp]:
    1.18    "{x}\<flat> \<sqsubseteq> ys +\<flat> zs \<longleftrightarrow> {x}\<flat> \<sqsubseteq> ys \<or> {x}\<flat> \<sqsubseteq> zs"
    1.19  apply (induct x rule: compact_basis.principal_induct, simp)
    1.20  apply (induct ys rule: lower_pd.principal_induct, simp)
    1.21 @@ -328,7 +328,7 @@
    1.22  apply (erule lower_le_induct, safe)
    1.23  apply (simp add: monofun_cfun)
    1.24  apply (simp add: rev_below_trans [OF lower_plus_below1])
    1.25 -apply (simp add: lower_plus_below_iff)
    1.26 +apply simp
    1.27  done
    1.28  
    1.29  definition
    1.30 @@ -389,14 +389,14 @@
    1.31  apply default
    1.32  apply (induct_tac x rule: lower_pd_induct, simp_all add: ep_pair.e_inverse)
    1.33  apply (induct_tac y rule: lower_pd_induct)
    1.34 -apply (simp_all add: ep_pair.e_p_below monofun_cfun)
    1.35 +apply (simp_all add: ep_pair.e_p_below monofun_cfun del: lower_plus_below_iff)
    1.36  done
    1.37  
    1.38  lemma deflation_lower_map: "deflation d \<Longrightarrow> deflation (lower_map\<cdot>d)"
    1.39  apply default
    1.40  apply (induct_tac x rule: lower_pd_induct, simp_all add: deflation.idem)
    1.41  apply (induct_tac x rule: lower_pd_induct)
    1.42 -apply (simp_all add: deflation.below monofun_cfun)
    1.43 +apply (simp_all add: deflation.below monofun_cfun del: lower_plus_below_iff)
    1.44  done
    1.45  
    1.46  (* FIXME: long proof! *)

     2.1 --- a/src/HOLCF/UpperPD.thy	Fri Nov 26 18:07:00 2010 +0100
     2.2 +++ b/src/HOLCF/UpperPD.thy	Fri Nov 26 14:10:34 2010 -0800
     2.3 @@ -193,7 +193,7 @@
     2.4  apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
     2.5  done
     2.6  
     2.7 -lemma upper_below_plus_iff:
     2.8 +lemma upper_below_plus_iff [simp]:
     2.9    "xs \<sqsubseteq> ys +\<sharp> zs \<longleftrightarrow> xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs"
    2.10  apply safe
    2.11  apply (erule below_trans [OF _ upper_plus_below1])
    2.12 @@ -201,7 +201,7 @@
    2.13  apply (erule (1) upper_plus_greatest)
    2.14  done
    2.15  
    2.16 -lemma upper_plus_below_unit_iff:
    2.17 +lemma upper_plus_below_unit_iff [simp]:
    2.18    "xs +\<sharp> ys \<sqsubseteq> {z}\<sharp> \<longleftrightarrow> xs \<sqsubseteq> {z}\<sharp> \<or> ys \<sqsubseteq> {z}\<sharp>"
    2.19  apply (induct xs rule: upper_pd.principal_induct, simp)
    2.20  apply (induct ys rule: upper_pd.principal_induct, simp)
    2.21 @@ -323,7 +323,7 @@
    2.22  apply (erule upper_le_induct, safe)
    2.23  apply (simp add: monofun_cfun)
    2.24  apply (simp add: below_trans [OF upper_plus_below1])
    2.25 -apply (simp add: upper_below_plus_iff)
    2.26 +apply simp
    2.27  done
    2.28  
    2.29  definition
    2.30 @@ -384,14 +384,14 @@
    2.31  apply default
    2.32  apply (induct_tac x rule: upper_pd_induct, simp_all add: ep_pair.e_inverse)
    2.33  apply (induct_tac y rule: upper_pd_induct)
    2.34 -apply (simp_all add: ep_pair.e_p_below monofun_cfun)
    2.35 +apply (simp_all add: ep_pair.e_p_below monofun_cfun del: upper_below_plus_iff)
    2.36  done
    2.37  
    2.38  lemma deflation_upper_map: "deflation d \<Longrightarrow> deflation (upper_map\<cdot>d)"
    2.39  apply default
    2.40  apply (induct_tac x rule: upper_pd_induct, simp_all add: deflation.idem)
    2.41  apply (induct_tac x rule: upper_pd_induct)
    2.42 -apply (simp_all add: deflation.below monofun_cfun)
    2.43 +apply (simp_all add: deflation.below monofun_cfun del: upper_below_plus_iff)
    2.44  done
    2.45  
    2.46  (* FIXME: long proof! *)