Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
be explicit about Finite_Set.fold
authorhaftmann
Tue, 27 Dec 2011 09:45:10 +0100
changeset 45994 38a46e029784
parent 45993 3ca49a4bcc9f
child 46002 b319f1b0c634
be explicit about Finite_Set.fold
src/HOL/Library/Saturated.thy file | annotate | diff | comparison | revisions
src/HOL/Multivariate_Analysis/Integration.thy file | annotate | diff | comparison | revisions
src/HOL/Quotient_Examples/FSet.thy file | annotate | diff | comparison | revisions 
--- 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 \<in> A"
-  ultimately have "fold min top A \<le> min x top" by (rule min_max.fold_inf_le_inf)
+  ultimately have "Finite_Set.fold min top A \<le> min x top" by (rule min_max.fold_inf_le_inf)
   then show "Inf A \<le> x" by (simp add: Inf_sat_def)
 next
   fix z :: "'a sat"
   fix A :: "'a sat set"
   note finite
   moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
-  ultimately have "min z top \<le> fold min top A" by (blast intro: min_max.inf_le_fold_inf)
+  ultimately have "min z top \<le> Finite_Set.fold min top A" by (blast intro: min_max.inf_le_fold_inf)
   then show "z \<le> 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 \<in> A"
-  ultimately have "max x bot \<le> fold max bot A" by (rule min_max.sup_le_fold_sup)
+  ultimately have "max x bot \<le> Finite_Set.fold max bot A" by (rule min_max.sup_le_fold_sup)
   then show "x \<le> Sup A" by (simp add: Sup_sat_def)
 next
   fix z :: "'a sat"
   fix A :: "'a sat set"
   note finite
   moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
-  ultimately have "fold max bot A \<le> max z bot" by (blast intro: min_max.fold_sup_le_sup)
+  ultimately have "Finite_Set.fold max bot A \<le> max z bot" by (blast intro: min_max.fold_sup_le_sup)
   then show "Sup A \<le> z" by (simp add: Sup_sat_def max_def bot_unique)
 qed
 
--- 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\<in>s \<and> f x \<noteq> neutral opp}"
-definition "fold' opp e s \<equiv> (if finite s then fold opp e s else e)"
+definition "fold' opp e s \<equiv> (if finite s then Finite_Set.fold opp e s else e)"
 definition "iterate opp s f \<equiv> fold' (\<lambda>x a. opp (f x) a) (neutral opp) (support opp f s)"
 
 lemma support_subset[intro]:"support opp f s \<subseteq> s" unfolding support_def by auto
--- 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 {*
isabelle