diff -r 3c886fe611b8 -r f738e6dbd844 src/HOL/HOLCF/Compact_Basis.thy
--- a/src/HOL/HOLCF/Compact_Basis.thy Sat Mar 23 17:11:06 2013 +0100
+++ b/src/HOL/HOLCF/Compact_Basis.thy Sat Mar 23 20:50:39 2013 +0100
@@ -96,20 +96,23 @@
definition
fold_pd ::
"('a compact_basis \ 'b::type) \ ('b \ 'b \ 'b) \ 'a pd_basis \ 'b"
- where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
+ where "fold_pd g f t = semilattice_set.F f (g ` Rep_pd_basis t)"
lemma fold_pd_PDUnit:
- assumes "class.ab_semigroup_idem_mult f"
+ assumes "semilattice f"
shows "fold_pd g f (PDUnit x) = g x"
-unfolding fold_pd_def Rep_PDUnit by simp
+proof -
+ from assms interpret semilattice_set f by (rule semilattice_set.intro)
+ show ?thesis by (simp add: fold_pd_def Rep_PDUnit)
+qed
lemma fold_pd_PDPlus:
- assumes "class.ab_semigroup_idem_mult f"
+ assumes "semilattice f"
shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
proof -
- interpret ab_semigroup_idem_mult f by fact
- show ?thesis unfolding fold_pd_def Rep_PDPlus
- by (simp add: image_Un fold1_Un2)
+ from assms interpret semilattice_set f by (rule semilattice_set.intro)
+ show ?thesis by (simp add: image_Un fold_pd_def Rep_PDPlus union)
qed
end
+