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 +