# HG changeset patch
# User huffman
# Date 1290809434 28800
# Node ID a292fc5157f886e153251c652d6dabf47793069e
# Parent  88f2955a111e0971250875b1fc13a0644a9ee718
declare more simp rules for powerdomains

diff -r 88f2955a111e -r a292fc5157f8 src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Fri Nov 26 18:07:00 2010 +0100
+++ b/src/HOLCF/LowerPD.thy	Fri Nov 26 14:10:34 2010 -0800
@@ -195,7 +195,7 @@
 apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
 done
 
-lemma lower_plus_below_iff:
+lemma lower_plus_below_iff [simp]:
   "xs +\<flat> ys \<sqsubseteq> zs \<longleftrightarrow> xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs"
 apply safe
 apply (erule below_trans [OF lower_plus_below1])
@@ -203,7 +203,7 @@
 apply (erule (1) lower_plus_least)
 done
 
-lemma lower_unit_below_plus_iff:
+lemma lower_unit_below_plus_iff [simp]:
   "{x}\<flat> \<sqsubseteq> ys +\<flat> zs \<longleftrightarrow> {x}\<flat> \<sqsubseteq> ys \<or> {x}\<flat> \<sqsubseteq> zs"
 apply (induct x rule: compact_basis.principal_induct, simp)
 apply (induct ys rule: lower_pd.principal_induct, simp)
@@ -328,7 +328,7 @@
 apply (erule lower_le_induct, safe)
 apply (simp add: monofun_cfun)
 apply (simp add: rev_below_trans [OF lower_plus_below1])
-apply (simp add: lower_plus_below_iff)
+apply simp
 done
 
 definition
@@ -389,14 +389,14 @@
 apply default
 apply (induct_tac x rule: lower_pd_induct, simp_all add: ep_pair.e_inverse)
 apply (induct_tac y rule: lower_pd_induct)
-apply (simp_all add: ep_pair.e_p_below monofun_cfun)
+apply (simp_all add: ep_pair.e_p_below monofun_cfun del: lower_plus_below_iff)
 done
 
 lemma deflation_lower_map: "deflation d \<Longrightarrow> deflation (lower_map\<cdot>d)"
 apply default
 apply (induct_tac x rule: lower_pd_induct, simp_all add: deflation.idem)
 apply (induct_tac x rule: lower_pd_induct)
-apply (simp_all add: deflation.below monofun_cfun)
+apply (simp_all add: deflation.below monofun_cfun del: lower_plus_below_iff)
 done
 
 (* FIXME: long proof! *)
diff -r 88f2955a111e -r a292fc5157f8 src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Fri Nov 26 18:07:00 2010 +0100
+++ b/src/HOLCF/UpperPD.thy	Fri Nov 26 14:10:34 2010 -0800
@@ -193,7 +193,7 @@
 apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
 done
 
-lemma upper_below_plus_iff:
+lemma upper_below_plus_iff [simp]:
   "xs \<sqsubseteq> ys +\<sharp> zs \<longleftrightarrow> xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs"
 apply safe
 apply (erule below_trans [OF _ upper_plus_below1])
@@ -201,7 +201,7 @@
 apply (erule (1) upper_plus_greatest)
 done
 
-lemma upper_plus_below_unit_iff:
+lemma upper_plus_below_unit_iff [simp]:
   "xs +\<sharp> ys \<sqsubseteq> {z}\<sharp> \<longleftrightarrow> xs \<sqsubseteq> {z}\<sharp> \<or> ys \<sqsubseteq> {z}\<sharp>"
 apply (induct xs rule: upper_pd.principal_induct, simp)
 apply (induct ys rule: upper_pd.principal_induct, simp)
@@ -323,7 +323,7 @@
 apply (erule upper_le_induct, safe)
 apply (simp add: monofun_cfun)
 apply (simp add: below_trans [OF upper_plus_below1])
-apply (simp add: upper_below_plus_iff)
+apply simp
 done
 
 definition
@@ -384,14 +384,14 @@
 apply default
 apply (induct_tac x rule: upper_pd_induct, simp_all add: ep_pair.e_inverse)
 apply (induct_tac y rule: upper_pd_induct)
-apply (simp_all add: ep_pair.e_p_below monofun_cfun)
+apply (simp_all add: ep_pair.e_p_below monofun_cfun del: upper_below_plus_iff)
 done
 
 lemma deflation_upper_map: "deflation d \<Longrightarrow> deflation (upper_map\<cdot>d)"
 apply default
 apply (induct_tac x rule: upper_pd_induct, simp_all add: deflation.idem)
 apply (induct_tac x rule: upper_pd_induct)
-apply (simp_all add: deflation.below monofun_cfun)
+apply (simp_all add: deflation.below monofun_cfun del: upper_below_plus_iff)
 done
 
 (* FIXME: long proof! *)