src/HOL/HOLCF/Compact_Basis.thy
 changeset 51489 f738e6dbd844 parent 49834 b27bbb021df1 child 58880 0baae4311a9f
```     1.1 --- a/src/HOL/HOLCF/Compact_Basis.thy	Sat Mar 23 17:11:06 2013 +0100
1.2 +++ b/src/HOL/HOLCF/Compact_Basis.thy	Sat Mar 23 20:50:39 2013 +0100
1.3 @@ -96,20 +96,23 @@
1.4  definition
1.5    fold_pd ::
1.6      "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
1.7 -  where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
1.8 +  where "fold_pd g f t = semilattice_set.F f (g ` Rep_pd_basis t)"
1.9
1.10  lemma fold_pd_PDUnit:
1.11 -  assumes "class.ab_semigroup_idem_mult f"
1.12 +  assumes "semilattice f"
1.13    shows "fold_pd g f (PDUnit x) = g x"
1.14 -unfolding fold_pd_def Rep_PDUnit by simp
1.15 +proof -
1.16 +  from assms interpret semilattice_set f by (rule semilattice_set.intro)
1.17 +  show ?thesis by (simp add: fold_pd_def Rep_PDUnit)
1.18 +qed
1.19
1.20  lemma fold_pd_PDPlus:
1.21 -  assumes "class.ab_semigroup_idem_mult f"
1.22 +  assumes "semilattice f"
1.23    shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
1.24  proof -
1.25 -  interpret ab_semigroup_idem_mult f by fact
1.26 -  show ?thesis unfolding fold_pd_def Rep_PDPlus
1.27 -    by (simp add: image_Un fold1_Un2)
1.28 +  from assms interpret semilattice_set f by (rule semilattice_set.intro)
1.29 +  show ?thesis by (simp add: image_Un fold_pd_def Rep_PDPlus union)
1.30  qed
1.31
1.32  end
1.33 +
```