# HG changeset patch # User haftmann # Date 1324975510 -3600 # Node ID 38a46e02978443270bc89ce0760b9db2d1a2ddb1 # Parent 3ca49a4bcc9f4a2cd3eacd403e07216f0bda8765 be explicit about Finite_Set.fold diff -r 3ca49a4bcc9f -r 38a46e029784 src/HOL/Library/Saturated.thy --- a/src/HOL/Library/Saturated.thy Tue Dec 27 09:15:26 2011 +0100 +++ b/src/HOL/Library/Saturated.thy Tue Dec 27 09:45:10 2011 +0100 @@ -215,38 +215,38 @@ begin definition - "Inf (A :: 'a sat set) = fold min top A" + "Inf (A :: 'a sat set) = Finite_Set.fold min top A" definition - "Sup (A :: 'a sat set) = fold max bot A" + "Sup (A :: 'a sat set) = Finite_Set.fold max bot A" instance proof fix x :: "'a sat" fix A :: "'a sat set" note finite moreover assume "x \ A" - ultimately have "fold min top A \ min x top" by (rule min_max.fold_inf_le_inf) + ultimately have "Finite_Set.fold min top A \ min x top" by (rule min_max.fold_inf_le_inf) then show "Inf A \ x" by (simp add: Inf_sat_def) next fix z :: "'a sat" fix A :: "'a sat set" note finite moreover assume z: "\x. x \ A \ z \ x" - ultimately have "min z top \ fold min top A" by (blast intro: min_max.inf_le_fold_inf) + ultimately have "min z top \ Finite_Set.fold min top A" by (blast intro: min_max.inf_le_fold_inf) then show "z \ Inf A" by (simp add: Inf_sat_def min_def) next fix x :: "'a sat" fix A :: "'a sat set" note finite moreover assume "x \ A" - ultimately have "max x bot \ fold max bot A" by (rule min_max.sup_le_fold_sup) + ultimately have "max x bot \ Finite_Set.fold max bot A" by (rule min_max.sup_le_fold_sup) then show "x \ Sup A" by (simp add: Sup_sat_def) next fix z :: "'a sat" fix A :: "'a sat set" note finite moreover assume z: "\x. x \ A \ x \ z" - ultimately have "fold max bot A \ max z bot" by (blast intro: min_max.fold_sup_le_sup) + ultimately have "Finite_Set.fold max bot A \ max z bot" by (blast intro: min_max.fold_sup_le_sup) then show "Sup A \ z" by (simp add: Sup_sat_def max_def bot_unique) qed diff -r 3ca49a4bcc9f -r 38a46e029784 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Dec 27 09:15:26 2011 +0100 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Dec 27 09:45:10 2011 +0100 @@ -1814,7 +1814,7 @@ unfolding monoidal_def forall_option neutral_lifted[OF assms] using monoidal_ac[OF assms] by auto definition "support opp f s = {x. x\s \ f x \ neutral opp}" -definition "fold' opp e s \ (if finite s then fold opp e s else e)" +definition "fold' opp e s \ (if finite s then Finite_Set.fold opp e s else e)" definition "iterate opp s f \ fold' (\x a. opp (f x) a) (neutral opp) (support opp f s)" lemma support_subset[intro]:"support opp f s \ s" unfolding support_def by auto diff -r 3ca49a4bcc9f -r 38a46e029784 src/HOL/Quotient_Examples/FSet.thy --- a/src/HOL/Quotient_Examples/FSet.thy Tue Dec 27 09:15:26 2011 +0100 +++ b/src/HOL/Quotient_Examples/FSet.thy Tue Dec 27 09:45:10 2011 +0100 @@ -6,7 +6,7 @@ *) theory FSet -imports "~~/src/HOL/Library/Quotient_List" +imports "~~/src/HOL/Library/Multiset" "~~/src/HOL/Library/Quotient_List" begin text {*