be explicit about Finite_Set.fold
authorhaftmann
Tue Dec 27 09:45:10 2011 +0100 (2011-12-27)
changeset 4599438a46e029784
parent 45993 3ca49a4bcc9f
child 46002 b319f1b0c634
be explicit about Finite_Set.fold
src/HOL/Library/Saturated.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Quotient_Examples/FSet.thy
     1.1 --- a/src/HOL/Library/Saturated.thy	Tue Dec 27 09:15:26 2011 +0100
     1.2 +++ b/src/HOL/Library/Saturated.thy	Tue Dec 27 09:45:10 2011 +0100
     1.3 @@ -215,38 +215,38 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  "Inf (A :: 'a sat set) = fold min top A"
     1.8 +  "Inf (A :: 'a sat set) = Finite_Set.fold min top A"
     1.9  
    1.10  definition
    1.11 -  "Sup (A :: 'a sat set) = fold max bot A"
    1.12 +  "Sup (A :: 'a sat set) = Finite_Set.fold max bot A"
    1.13  
    1.14  instance proof
    1.15    fix x :: "'a sat"
    1.16    fix A :: "'a sat set"
    1.17    note finite
    1.18    moreover assume "x \<in> A"
    1.19 -  ultimately have "fold min top A \<le> min x top" by (rule min_max.fold_inf_le_inf)
    1.20 +  ultimately have "Finite_Set.fold min top A \<le> min x top" by (rule min_max.fold_inf_le_inf)
    1.21    then show "Inf A \<le> x" by (simp add: Inf_sat_def)
    1.22  next
    1.23    fix z :: "'a sat"
    1.24    fix A :: "'a sat set"
    1.25    note finite
    1.26    moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
    1.27 -  ultimately have "min z top \<le> fold min top A" by (blast intro: min_max.inf_le_fold_inf)
    1.28 +  ultimately have "min z top \<le> Finite_Set.fold min top A" by (blast intro: min_max.inf_le_fold_inf)
    1.29    then show "z \<le> Inf A" by (simp add: Inf_sat_def min_def)
    1.30  next
    1.31    fix x :: "'a sat"
    1.32    fix A :: "'a sat set"
    1.33    note finite
    1.34    moreover assume "x \<in> A"
    1.35 -  ultimately have "max x bot \<le> fold max bot A" by (rule min_max.sup_le_fold_sup)
    1.36 +  ultimately have "max x bot \<le> Finite_Set.fold max bot A" by (rule min_max.sup_le_fold_sup)
    1.37    then show "x \<le> Sup A" by (simp add: Sup_sat_def)
    1.38  next
    1.39    fix z :: "'a sat"
    1.40    fix A :: "'a sat set"
    1.41    note finite
    1.42    moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
    1.43 -  ultimately have "fold max bot A \<le> max z bot" by (blast intro: min_max.fold_sup_le_sup)
    1.44 +  ultimately have "Finite_Set.fold max bot A \<le> max z bot" by (blast intro: min_max.fold_sup_le_sup)
    1.45    then show "Sup A \<le> z" by (simp add: Sup_sat_def max_def bot_unique)
    1.46  qed
    1.47  
     2.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Dec 27 09:15:26 2011 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Dec 27 09:45:10 2011 +0100
     2.3 @@ -1814,7 +1814,7 @@
     2.4    unfolding monoidal_def forall_option neutral_lifted[OF assms] using monoidal_ac[OF assms] by auto
     2.5  
     2.6  definition "support opp f s = {x. x\<in>s \<and> f x \<noteq> neutral opp}"
     2.7 -definition "fold' opp e s \<equiv> (if finite s then fold opp e s else e)"
     2.8 +definition "fold' opp e s \<equiv> (if finite s then Finite_Set.fold opp e s else e)"
     2.9  definition "iterate opp s f \<equiv> fold' (\<lambda>x a. opp (f x) a) (neutral opp) (support opp f s)"
    2.10  
    2.11  lemma support_subset[intro]:"support opp f s \<subseteq> s" unfolding support_def by auto
     3.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Tue Dec 27 09:15:26 2011 +0100
     3.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Tue Dec 27 09:45:10 2011 +0100
     3.3 @@ -6,7 +6,7 @@
     3.4  *)
     3.5  
     3.6  theory FSet
     3.7 -imports "~~/src/HOL/Library/Quotient_List"
     3.8 +imports "~~/src/HOL/Library/Multiset" "~~/src/HOL/Library/Quotient_List"
     3.9  begin
    3.10  
    3.11  text {*