# HG changeset patch
# User haftmann
# Date 1282319310 -7200
# Node ID 86fc906dcd86b2d67a29f036a375983696148c95
# Parent  d6cb7e625d7572931fe2a1422a28137d99d78887
split and enriched theory SetsAndFunctions

diff -r d6cb7e625d75 -r 86fc906dcd86 NEWS
--- a/NEWS	Fri Aug 20 17:46:56 2010 +0200
+++ b/NEWS	Fri Aug 20 17:48:30 2010 +0200
@@ -35,6 +35,10 @@
 
 *** HOL ***
 
+* Theory SetsAndFunctions has been split into Function_Algebras and Set_Algebras;
+canonical names for instance definitions for functions; various improvements.
+INCOMPATIBILITY.
+
 * Records: logical foundation type for records do not carry a '_type' suffix
 any longer.  INCOMPATIBILITY.
 
diff -r d6cb7e625d75 -r 86fc906dcd86 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Aug 20 17:46:56 2010 +0200
+++ b/src/HOL/IsaMakefile	Fri Aug 20 17:48:30 2010 +0200
@@ -408,6 +408,7 @@
   Library/Executable_Set.thy Library/Float.thy				\
   Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
   Library/FrechetDeriv.thy Library/Fset.thy Library/FuncSet.thy		\
+  Library/Function_Algebras.thy						\
   Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy		\
   Library/Indicator_Function.thy Library/Infinite_Set.thy		\
   Library/Inner_Product.thy Library/Kleene_Algebra.thy			\
@@ -428,8 +429,8 @@
   Library/Quotient_Product.thy Library/Quotient_Sum.thy			\
   Library/Quotient_Syntax.thy Library/Quotient_Type.thy			\
   Library/RBT.thy Library/RBT_Impl.thy Library/README.html		\
-  Library/State_Monad.thy Library/Ramsey.thy Library/Reflection.thy	\
-  Library/SML_Quickcheck.thy Library/SetsAndFunctions.thy		\
+  Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy	\
+  Library/Reflection.thy Library/SML_Quickcheck.thy 			\
   Library/Sublist_Order.thy Library/Sum_Of_Squares.thy			\
   Library/Sum_Of_Squares/sos_wrapper.ML					\
   Library/Sum_Of_Squares/sum_of_squares.ML				\
diff -r d6cb7e625d75 -r 86fc906dcd86 src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Fri Aug 20 17:46:56 2010 +0200
+++ b/src/HOL/Library/BigO.thy	Fri Aug 20 17:48:30 2010 +0200
@@ -5,7 +5,7 @@
 header {* Big O notation *}
 
 theory BigO
-imports Complex_Main SetsAndFunctions
+imports Complex_Main Function_Algebras Set_Algebras
 begin
 
 text {*
diff -r d6cb7e625d75 -r 86fc906dcd86 src/HOL/Library/Function_Algebras.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Function_Algebras.thy	Fri Aug 20 17:48:30 2010 +0200
@@ -0,0 +1,207 @@
+(*  Title:      HOL/Library/Function_Algebras.thy
+    Author:     Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
+*)
+
+header {* Pointwise instantiation of functions to algebra type classes *}
+
+theory Function_Algebras
+imports Main
+begin
+
+text {* Pointwise operations *}
+
+instantiation "fun" :: (type, plus) plus
+begin
+
+definition
+  "f + g = (\<lambda>x. f x + g x)"
+
+instance ..
+
+end
+
+instantiation "fun" :: (type, zero) zero
+begin
+
+definition
+  "0 = (\<lambda>x. 0)"
+
+instance ..
+
+end
+
+instantiation "fun" :: (type, times) times
+begin
+
+definition
+  "f * g = (\<lambda>x. f x * g x)"
+
+instance ..
+
+end
+
+instantiation "fun" :: (type, one) one
+begin
+
+definition
+  "1 = (\<lambda>x. 1)"
+
+instance ..
+
+end
+
+
+text {* Additive structures *}
+
+instance "fun" :: (type, semigroup_add) semigroup_add proof
+qed (simp add: plus_fun_def add.assoc)
+
+instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add proof
+qed (simp_all add: plus_fun_def expand_fun_eq)
+
+instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add proof
+qed (simp add: plus_fun_def add.commute)
+
+instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add proof
+qed simp
+
+instance "fun" :: (type, monoid_add) monoid_add proof
+qed (simp_all add: plus_fun_def zero_fun_def)
+
+instance "fun" :: (type, comm_monoid_add) comm_monoid_add proof
+qed simp
+
+instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add ..
+
+instance "fun" :: (type, group_add) group_add proof
+qed (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
+
+instance "fun" :: (type, ab_group_add) ab_group_add proof
+qed (simp_all add: diff_minus)
+
+
+text {* Multiplicative structures *}
+
+instance "fun" :: (type, semigroup_mult) semigroup_mult proof
+qed (simp add: times_fun_def mult.assoc)
+
+instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult proof
+qed (simp add: times_fun_def mult.commute)
+
+instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult proof
+qed (simp add: times_fun_def)
+
+instance "fun" :: (type, monoid_mult) monoid_mult proof
+qed (simp_all add: times_fun_def one_fun_def)
+
+instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult proof
+qed simp
+
+
+text {* Misc *}
+
+instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
+
+instance "fun" :: (type, mult_zero) mult_zero proof
+qed (simp_all add: zero_fun_def times_fun_def)
+
+instance "fun" :: (type, mult_mono) mult_mono proof
+qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
+
+instance "fun" :: (type, mult_mono1) mult_mono1 proof
+qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_mono1)
+
+instance "fun" :: (type, zero_neq_one) zero_neq_one proof
+qed (simp add: zero_fun_def one_fun_def expand_fun_eq)
+
+
+text {* Ring structures *}
+
+instance "fun" :: (type, semiring) semiring proof
+qed (simp_all add: plus_fun_def times_fun_def algebra_simps)
+
+instance "fun" :: (type, comm_semiring) comm_semiring proof
+qed (simp add: plus_fun_def times_fun_def algebra_simps)
+
+instance "fun" :: (type, semiring_0) semiring_0 ..
+
+instance "fun" :: (type, comm_semiring_0) comm_semiring_0 ..
+
+instance "fun" :: (type, semiring_0_cancel) semiring_0_cancel ..
+
+instance "fun" :: (type, comm_semiring_0_cancel) comm_semiring_0_cancel ..
+
+instance "fun" :: (type, semiring_1) semiring_1 ..
+
+lemma of_nat_fun:
+  shows "of_nat n = (\<lambda>x::'a. of_nat n)"
+proof -
+  have comp: "comp = (\<lambda>f g x. f (g x))"
+    by (rule ext)+ simp
+  have plus_fun: "plus = (\<lambda>f g x. f x + g x)"
+    by (rule ext, rule ext) (fact plus_fun_def)
+  have "of_nat n = (comp (plus (1::'b)) ^^ n) (\<lambda>x::'a. 0)"
+    by (simp add: of_nat_def plus_fun zero_fun_def one_fun_def comp)
+  also have "... = comp ((plus 1) ^^ n) (\<lambda>x::'a. 0)"
+    by (simp only: comp_funpow)
+  finally show ?thesis by (simp add: of_nat_def comp)
+qed
+
+instance "fun" :: (type, comm_semiring_1) comm_semiring_1 ..
+
+instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
+
+instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel ..
+
+instance "fun" :: (type, semiring_char_0) semiring_char_0 proof
+  from inj_of_nat have "inj (\<lambda>n (x::'a). of_nat n :: 'b)"
+    by (rule inj_fun)
+  then have "inj (\<lambda>n. of_nat n :: 'a \<Rightarrow> 'b)"
+    by (simp add: of_nat_fun)
+  then show "inj (of_nat :: nat \<Rightarrow> 'a \<Rightarrow> 'b)" .
+qed
+
+instance "fun" :: (type, ring) ring ..
+
+instance "fun" :: (type, comm_ring) comm_ring ..
+
+instance "fun" :: (type, ring_1) ring_1 ..
+
+instance "fun" :: (type, comm_ring_1) comm_ring_1 ..
+
+instance "fun" :: (type, ring_char_0) ring_char_0 ..
+
+
+text {* Ordereded structures *}
+
+instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add proof
+qed (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
+
+instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
+
+instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le proof
+qed (simp add: plus_fun_def le_fun_def)
+
+instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
+
+instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
+
+instance "fun" :: (type, ordered_semiring) ordered_semiring ..
+
+instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring ..
+
+instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
+
+instance "fun" :: (type, ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
+
+instance "fun" :: (type, ordered_ring) ordered_ring ..
+
+instance "fun" :: (type, ordered_comm_ring) ordered_comm_ring ..
+
+
+lemmas func_plus = plus_fun_def
+lemmas func_zero = zero_fun_def
+lemmas func_times = times_fun_def
+lemmas func_one = one_fun_def
+
+end
diff -r d6cb7e625d75 -r 86fc906dcd86 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Fri Aug 20 17:46:56 2010 +0200
+++ b/src/HOL/Library/Library.thy	Fri Aug 20 17:48:30 2010 +0200
@@ -22,6 +22,7 @@
   FrechetDeriv
   Fset
   FuncSet
+  Function_Algebras
   Fundamental_Theorem_Algebra
   Indicator_Function
   Infinite_Set
@@ -54,6 +55,7 @@
   Ramsey
   Reflection
   RBT
+  Set_Algebras
   SML_Quickcheck
   State_Monad
   Sum_Of_Squares
diff -r d6cb7e625d75 -r 86fc906dcd86 src/HOL/Library/Set_Algebras.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Set_Algebras.thy	Fri Aug 20 17:48:30 2010 +0200
@@ -0,0 +1,357 @@
+(*  Title:      HOL/Library/Set_Algebras.thy
+    Author:     Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
+*)
+
+header {* Algebraic operations on sets *}
+
+theory Set_Algebras
+imports Main
+begin
+
+text {*
+  This library lifts operations like addition and muliplication to
+  sets.  It was designed to support asymptotic calculations. See the
+  comments at the top of theory @{text BigO}.
+*}
+
+definition set_plus :: "'a::plus set \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "\<oplus>" 65) where
+  "A \<oplus> B = {c. \<exists>a\<in>A. \<exists>b\<in>B. c = a + b}"
+
+definition set_times :: "'a::times set \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "\<otimes>" 70) where
+  "A \<otimes> B = {c. \<exists>a\<in>A. \<exists>b\<in>B. c = a * b}"
+
+definition elt_set_plus :: "'a::plus \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "+o" 70) where
+  "a +o B = {c. \<exists>b\<in>B. c = a + b}"
+
+definition elt_set_times :: "'a::times \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "*o" 80) where
+  "a *o B = {c. \<exists>b\<in>B. c = a * b}"
+
+abbreviation (input) elt_set_eq :: "'a \<Rightarrow> 'a set \<Rightarrow> bool"  (infix "=o" 50) where
+  "x =o A \<equiv> x \<in> A"
+
+interpretation set_add!: semigroup "set_plus :: 'a::semigroup_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
+qed (force simp add: set_plus_def add.assoc)
+
+interpretation set_add!: abel_semigroup "set_plus :: 'a::ab_semigroup_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
+qed (force simp add: set_plus_def add.commute)
+
+interpretation set_add!: monoid "set_plus :: 'a::monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" proof
+qed (simp_all add: set_plus_def)
+
+interpretation set_add!: comm_monoid "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" proof
+qed (simp add: set_plus_def)
+
+definition listsum_set :: "('a::monoid_add set) list \<Rightarrow> 'a set" where
+  "listsum_set = monoid_add.listsum set_plus {0}"
+
+interpretation set_add!: monoid_add "set_plus :: 'a::monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" where
+  "monoid_add.listsum set_plus {0::'a} = listsum_set"
+proof -
+  show "class.monoid_add set_plus {0::'a}" proof
+  qed (simp_all add: set_add.assoc)
+  then interpret set_add!: monoid_add "set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" .
+  show "monoid_add.listsum set_plus {0::'a} = listsum_set"
+    by (simp only: listsum_set_def)
+qed
+
+definition setsum_set :: "('b \<Rightarrow> ('a::comm_monoid_add) set) \<Rightarrow> 'b set \<Rightarrow> 'a set" where
+  "setsum_set f A = (if finite A then fold_image set_plus f {0} A else {0})"
+
+interpretation set_add!:
+  comm_monoid_big "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" setsum_set 
+proof
+qed (fact setsum_set_def)
+
+interpretation set_add!: comm_monoid_add "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" where
+  "monoid_add.listsum set_plus {0::'a} = listsum_set"
+  and "comm_monoid_add.setsum set_plus {0::'a} = setsum_set"
+proof -
+  show "class.comm_monoid_add (set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set) {0}" proof
+  qed (simp_all add: set_add.commute)
+  then interpret set_add!: comm_monoid_add "set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" .
+  show "monoid_add.listsum set_plus {0::'a} = listsum_set"
+    by (simp only: listsum_set_def)
+  show "comm_monoid_add.setsum set_plus {0::'a} = setsum_set"
+    by (simp add: set_add.setsum_def setsum_set_def expand_fun_eq)
+qed
+
+interpretation set_mult!: semigroup "set_times :: 'a::semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
+qed (force simp add: set_times_def mult.assoc)
+
+interpretation set_mult!: abel_semigroup "set_times :: 'a::ab_semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
+qed (force simp add: set_times_def mult.commute)
+
+interpretation set_mult!: monoid "set_times :: 'a::monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" proof
+qed (simp_all add: set_times_def)
+
+interpretation set_mult!: comm_monoid "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" proof
+qed (simp add: set_times_def)
+
+definition power_set :: "nat \<Rightarrow> ('a::monoid_mult set) \<Rightarrow> 'a set" where
+  "power_set n A = power.power {1} set_times A n"
+
+interpretation set_mult!: monoid_mult "{1}" "set_times :: 'a::monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+  "power.power {1} set_times = (\<lambda>A n. power_set n A)"
+proof -
+  show "class.monoid_mult {1} (set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set)" proof
+  qed (simp_all add: set_mult.assoc)
+  show "power.power {1} set_times = (\<lambda>A n. power_set n A)"
+    by (simp add: power_set_def)
+qed
+
+definition setprod_set :: "('b \<Rightarrow> ('a::comm_monoid_mult) set) \<Rightarrow> 'b set \<Rightarrow> 'a set" where
+  "setprod_set f A = (if finite A then fold_image set_times f {1} A else {1})"
+
+interpretation set_mult!:
+  comm_monoid_big "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" setprod_set 
+proof
+qed (fact setprod_set_def)
+
+interpretation set_mult!: comm_monoid_mult "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" where
+  "power.power {1} set_times = (\<lambda>A n. power_set n A)"
+  and "comm_monoid_mult.setprod set_times {1::'a} = setprod_set"
+proof -
+  show "class.comm_monoid_mult (set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set) {1}" proof
+  qed (simp_all add: set_mult.commute)
+  then interpret set_mult!: comm_monoid_mult "set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" .
+  show "power.power {1} set_times = (\<lambda>A n. power_set n A)"
+    by (simp add: power_set_def)
+  show "comm_monoid_mult.setprod set_times {1::'a} = setprod_set"
+    by (simp add: set_mult.setprod_def setprod_set_def expand_fun_eq)
+qed
+
+lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \<oplus> D"
+  by (auto simp add: set_plus_def)
+
+lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
+  by (auto simp add: elt_set_plus_def)
+
+lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) \<oplus>
+    (b +o D) = (a + b) +o (C \<oplus> D)"
+  apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
+   apply (rule_tac x = "ba + bb" in exI)
+  apply (auto simp add: add_ac)
+  apply (rule_tac x = "aa + a" in exI)
+  apply (auto simp add: add_ac)
+  done
+
+lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) =
+    (a + b) +o C"
+  by (auto simp add: elt_set_plus_def add_assoc)
+
+lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) \<oplus> C =
+    a +o (B \<oplus> C)"
+  apply (auto simp add: elt_set_plus_def set_plus_def)
+   apply (blast intro: add_ac)
+  apply (rule_tac x = "a + aa" in exI)
+  apply (rule conjI)
+   apply (rule_tac x = "aa" in bexI)
+    apply auto
+  apply (rule_tac x = "ba" in bexI)
+   apply (auto simp add: add_ac)
+  done
+
+theorem set_plus_rearrange4: "C \<oplus> ((a::'a::comm_monoid_add) +o D) =
+    a +o (C \<oplus> D)"
+  apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus_def add_ac)
+   apply (rule_tac x = "aa + ba" in exI)
+   apply (auto simp add: add_ac)
+  done
+
+theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
+  set_plus_rearrange3 set_plus_rearrange4
+
+lemma set_plus_mono [intro!]: "C <= D ==> a +o C <= a +o D"
+  by (auto simp add: elt_set_plus_def)
+
+lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==>
+    C \<oplus> E <= D \<oplus> F"
+  by (auto simp add: set_plus_def)
+
+lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C \<oplus> D"
+  by (auto simp add: elt_set_plus_def set_plus_def)
+
+lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==>
+    a +o D <= D \<oplus> C"
+  by (auto simp add: elt_set_plus_def set_plus_def add_ac)
+
+lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C \<oplus> D"
+  apply (subgoal_tac "a +o B <= a +o D")
+   apply (erule order_trans)
+   apply (erule set_plus_mono3)
+  apply (erule set_plus_mono)
+  done
+
+lemma set_plus_mono_b: "C <= D ==> x : a +o C
+    ==> x : a +o D"
+  apply (frule set_plus_mono)
+  apply auto
+  done
+
+lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C \<oplus> E ==>
+    x : D \<oplus> F"
+  apply (frule set_plus_mono2)
+   prefer 2
+   apply force
+  apply assumption
+  done
+
+lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C \<oplus> D"
+  apply (frule set_plus_mono3)
+  apply auto
+  done
+
+lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==>
+    x : a +o D ==> x : D \<oplus> C"
+  apply (frule set_plus_mono4)
+  apply auto
+  done
+
+lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C"
+  by (auto simp add: elt_set_plus_def)
+
+lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A \<oplus> B"
+  apply (auto intro!: subsetI simp add: set_plus_def)
+  apply (rule_tac x = 0 in bexI)
+   apply (rule_tac x = x in bexI)
+    apply (auto simp add: add_ac)
+  done
+
+lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C"
+  by (auto simp add: elt_set_plus_def add_ac diff_minus)
+
+lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C"
+  apply (auto simp add: elt_set_plus_def add_ac diff_minus)
+  apply (subgoal_tac "a = (a + - b) + b")
+   apply (rule bexI, assumption, assumption)
+  apply (auto simp add: add_ac)
+  done
+
+lemma set_minus_plus: "((a::'a::ab_group_add) - b : C) = (a : b +o C)"
+  by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus,
+    assumption)
+
+lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C \<otimes> D"
+  by (auto simp add: set_times_def)
+
+lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
+  by (auto simp add: elt_set_times_def)
+
+lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) \<otimes>
+    (b *o D) = (a * b) *o (C \<otimes> D)"
+  apply (auto simp add: elt_set_times_def set_times_def)
+   apply (rule_tac x = "ba * bb" in exI)
+   apply (auto simp add: mult_ac)
+  apply (rule_tac x = "aa * a" in exI)
+  apply (auto simp add: mult_ac)
+  done
+
+lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) =
+    (a * b) *o C"
+  by (auto simp add: elt_set_times_def mult_assoc)
+
+lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) \<otimes> C =
+    a *o (B \<otimes> C)"
+  apply (auto simp add: elt_set_times_def set_times_def)
+   apply (blast intro: mult_ac)
+  apply (rule_tac x = "a * aa" in exI)
+  apply (rule conjI)
+   apply (rule_tac x = "aa" in bexI)
+    apply auto
+  apply (rule_tac x = "ba" in bexI)
+   apply (auto simp add: mult_ac)
+  done
+
+theorem set_times_rearrange4: "C \<otimes> ((a::'a::comm_monoid_mult) *o D) =
+    a *o (C \<otimes> D)"
+  apply (auto intro!: subsetI simp add: elt_set_times_def set_times_def
+    mult_ac)
+   apply (rule_tac x = "aa * ba" in exI)
+   apply (auto simp add: mult_ac)
+  done
+
+theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
+  set_times_rearrange3 set_times_rearrange4
+
+lemma set_times_mono [intro]: "C <= D ==> a *o C <= a *o D"
+  by (auto simp add: elt_set_times_def)
+
+lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==>
+    C \<otimes> E <= D \<otimes> F"
+  by (auto simp add: set_times_def)
+
+lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C \<otimes> D"
+  by (auto simp add: elt_set_times_def set_times_def)
+
+lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==>
+    a *o D <= D \<otimes> C"
+  by (auto simp add: elt_set_times_def set_times_def mult_ac)
+
+lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C \<otimes> D"
+  apply (subgoal_tac "a *o B <= a *o D")
+   apply (erule order_trans)
+   apply (erule set_times_mono3)
+  apply (erule set_times_mono)
+  done
+
+lemma set_times_mono_b: "C <= D ==> x : a *o C
+    ==> x : a *o D"
+  apply (frule set_times_mono)
+  apply auto
+  done
+
+lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C \<otimes> E ==>
+    x : D \<otimes> F"
+  apply (frule set_times_mono2)
+   prefer 2
+   apply force
+  apply assumption
+  done
+
+lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C \<otimes> D"
+  apply (frule set_times_mono3)
+  apply auto
+  done
+
+lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==>
+    x : a *o D ==> x : D \<otimes> C"
+  apply (frule set_times_mono4)
+  apply auto
+  done
+
+lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C"
+  by (auto simp add: elt_set_times_def)
+
+lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)=
+    (a * b) +o (a *o C)"
+  by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs)
+
+lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B \<oplus> C) =
+    (a *o B) \<oplus> (a *o C)"
+  apply (auto simp add: set_plus_def elt_set_times_def ring_distribs)
+   apply blast
+  apply (rule_tac x = "b + bb" in exI)
+  apply (auto simp add: ring_distribs)
+  done
+
+lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) \<otimes> D <=
+    a *o D \<oplus> C \<otimes> D"
+  apply (auto intro!: subsetI simp add:
+    elt_set_plus_def elt_set_times_def set_times_def
+    set_plus_def ring_distribs)
+  apply auto
+  done
+
+theorems set_times_plus_distribs =
+  set_times_plus_distrib
+  set_times_plus_distrib2
+
+lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==>
+    - a : C"
+  by (auto simp add: elt_set_times_def)
+
+lemma set_neg_intro2: "(a::'a::ring_1) : C ==>
+    - a : (- 1) *o C"
+  by (auto simp add: elt_set_times_def)
+
+end
diff -r d6cb7e625d75 -r 86fc906dcd86 src/HOL/Library/SetsAndFunctions.thy
--- a/src/HOL/Library/SetsAndFunctions.thy	Fri Aug 20 17:46:56 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,373 +0,0 @@
-(*  Title:      HOL/Library/SetsAndFunctions.thy
-    Author:     Jeremy Avigad and Kevin Donnelly
-*)
-
-header {* Operations on sets and functions *}
-
-theory SetsAndFunctions
-imports Main
-begin
-
-text {*
-This library lifts operations like addition and muliplication to sets and
-functions of appropriate types. It was designed to support asymptotic
-calculations. See the comments at the top of theory @{text BigO}.
-*}
-
-subsection {* Basic definitions *}
-
-definition
-  set_plus :: "('a::plus) set => 'a set => 'a set"  (infixl "\<oplus>" 65) where
-  "A \<oplus> B == {c. EX a:A. EX b:B. c = a + b}"
-
-instantiation "fun" :: (type, plus) plus
-begin
-
-definition
-  func_plus: "f + g == (%x. f x + g x)"
-
-instance ..
-
-end
-
-definition
-  set_times :: "('a::times) set => 'a set => 'a set"  (infixl "\<otimes>" 70) where
-  "A \<otimes> B == {c. EX a:A. EX b:B. c = a * b}"
-
-instantiation "fun" :: (type, times) times
-begin
-
-definition
-  func_times: "f * g == (%x. f x * g x)"
-
-instance ..
-
-end
-
-
-instantiation "fun" :: (type, zero) zero
-begin
-
-definition
-  func_zero: "0::(('a::type) => ('b::zero)) == %x. 0"
-
-instance ..
-
-end
-
-instantiation "fun" :: (type, one) one
-begin
-
-definition
-  func_one: "1::(('a::type) => ('b::one)) == %x. 1"
-
-instance ..
-
-end
-
-definition
-  elt_set_plus :: "'a::plus => 'a set => 'a set"  (infixl "+o" 70) where
-  "a +o B = {c. EX b:B. c = a + b}"
-
-definition
-  elt_set_times :: "'a::times => 'a set => 'a set"  (infixl "*o" 80) where
-  "a *o B = {c. EX b:B. c = a * b}"
-
-abbreviation (input)
-  elt_set_eq :: "'a => 'a set => bool"  (infix "=o" 50) where
-  "x =o A == x : A"
-
-instance "fun" :: (type,semigroup_add)semigroup_add
-  by default (auto simp add: func_plus add_assoc)
-
-instance "fun" :: (type,comm_monoid_add)comm_monoid_add
-  by default (auto simp add: func_zero func_plus add_ac)
-
-instance "fun" :: (type,ab_group_add)ab_group_add
-  apply default
-   apply (simp add: fun_Compl_def func_plus func_zero)
-  apply (simp add: fun_Compl_def func_plus fun_diff_def diff_minus)
-  done
-
-instance "fun" :: (type,semigroup_mult)semigroup_mult
-  apply default
-  apply (auto simp add: func_times mult_assoc)
-  done
-
-instance "fun" :: (type,comm_monoid_mult)comm_monoid_mult
-  apply default
-   apply (auto simp add: func_one func_times mult_ac)
-  done
-
-instance "fun" :: (type,comm_ring_1)comm_ring_1
-  apply default
-   apply (auto simp add: func_plus func_times fun_Compl_def fun_diff_def
-     func_one func_zero algebra_simps)
-  apply (drule fun_cong)
-  apply simp
-  done
-
-interpretation set_semigroup_add: semigroup_add "op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"
-  apply default
-  apply (unfold set_plus_def)
-  apply (force simp add: add_assoc)
-  done
-
-interpretation set_semigroup_mult: semigroup_mult "op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"
-  apply default
-  apply (unfold set_times_def)
-  apply (force simp add: mult_assoc)
-  done
-
-interpretation set_comm_monoid_add: comm_monoid_add "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set" "{0}"
-  apply default
-   apply (unfold set_plus_def)
-   apply (force simp add: add_ac)
-  apply force
-  done
-
-interpretation set_comm_monoid_mult: comm_monoid_mult "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set" "{1}"
-  apply default
-   apply (unfold set_times_def)
-   apply (force simp add: mult_ac)
-  apply force
-  done
-
-
-subsection {* Basic properties *}
-
-lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \<oplus> D"
-  by (auto simp add: set_plus_def)
-
-lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
-  by (auto simp add: elt_set_plus_def)
-
-lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) \<oplus>
-    (b +o D) = (a + b) +o (C \<oplus> D)"
-  apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
-   apply (rule_tac x = "ba + bb" in exI)
-  apply (auto simp add: add_ac)
-  apply (rule_tac x = "aa + a" in exI)
-  apply (auto simp add: add_ac)
-  done
-
-lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) =
-    (a + b) +o C"
-  by (auto simp add: elt_set_plus_def add_assoc)
-
-lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) \<oplus> C =
-    a +o (B \<oplus> C)"
-  apply (auto simp add: elt_set_plus_def set_plus_def)
-   apply (blast intro: add_ac)
-  apply (rule_tac x = "a + aa" in exI)
-  apply (rule conjI)
-   apply (rule_tac x = "aa" in bexI)
-    apply auto
-  apply (rule_tac x = "ba" in bexI)
-   apply (auto simp add: add_ac)
-  done
-
-theorem set_plus_rearrange4: "C \<oplus> ((a::'a::comm_monoid_add) +o D) =
-    a +o (C \<oplus> D)"
-  apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus_def add_ac)
-   apply (rule_tac x = "aa + ba" in exI)
-   apply (auto simp add: add_ac)
-  done
-
-theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
-  set_plus_rearrange3 set_plus_rearrange4
-
-lemma set_plus_mono [intro!]: "C <= D ==> a +o C <= a +o D"
-  by (auto simp add: elt_set_plus_def)
-
-lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==>
-    C \<oplus> E <= D \<oplus> F"
-  by (auto simp add: set_plus_def)
-
-lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C \<oplus> D"
-  by (auto simp add: elt_set_plus_def set_plus_def)
-
-lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==>
-    a +o D <= D \<oplus> C"
-  by (auto simp add: elt_set_plus_def set_plus_def add_ac)
-
-lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C \<oplus> D"
-  apply (subgoal_tac "a +o B <= a +o D")
-   apply (erule order_trans)
-   apply (erule set_plus_mono3)
-  apply (erule set_plus_mono)
-  done
-
-lemma set_plus_mono_b: "C <= D ==> x : a +o C
-    ==> x : a +o D"
-  apply (frule set_plus_mono)
-  apply auto
-  done
-
-lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C \<oplus> E ==>
-    x : D \<oplus> F"
-  apply (frule set_plus_mono2)
-   prefer 2
-   apply force
-  apply assumption
-  done
-
-lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C \<oplus> D"
-  apply (frule set_plus_mono3)
-  apply auto
-  done
-
-lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==>
-    x : a +o D ==> x : D \<oplus> C"
-  apply (frule set_plus_mono4)
-  apply auto
-  done
-
-lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C"
-  by (auto simp add: elt_set_plus_def)
-
-lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A \<oplus> B"
-  apply (auto intro!: subsetI simp add: set_plus_def)
-  apply (rule_tac x = 0 in bexI)
-   apply (rule_tac x = x in bexI)
-    apply (auto simp add: add_ac)
-  done
-
-lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C"
-  by (auto simp add: elt_set_plus_def add_ac diff_minus)
-
-lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C"
-  apply (auto simp add: elt_set_plus_def add_ac diff_minus)
-  apply (subgoal_tac "a = (a + - b) + b")
-   apply (rule bexI, assumption, assumption)
-  apply (auto simp add: add_ac)
-  done
-
-lemma set_minus_plus: "((a::'a::ab_group_add) - b : C) = (a : b +o C)"
-  by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus,
-    assumption)
-
-lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C \<otimes> D"
-  by (auto simp add: set_times_def)
-
-lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
-  by (auto simp add: elt_set_times_def)
-
-lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) \<otimes>
-    (b *o D) = (a * b) *o (C \<otimes> D)"
-  apply (auto simp add: elt_set_times_def set_times_def)
-   apply (rule_tac x = "ba * bb" in exI)
-   apply (auto simp add: mult_ac)
-  apply (rule_tac x = "aa * a" in exI)
-  apply (auto simp add: mult_ac)
-  done
-
-lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) =
-    (a * b) *o C"
-  by (auto simp add: elt_set_times_def mult_assoc)
-
-lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) \<otimes> C =
-    a *o (B \<otimes> C)"
-  apply (auto simp add: elt_set_times_def set_times_def)
-   apply (blast intro: mult_ac)
-  apply (rule_tac x = "a * aa" in exI)
-  apply (rule conjI)
-   apply (rule_tac x = "aa" in bexI)
-    apply auto
-  apply (rule_tac x = "ba" in bexI)
-   apply (auto simp add: mult_ac)
-  done
-
-theorem set_times_rearrange4: "C \<otimes> ((a::'a::comm_monoid_mult) *o D) =
-    a *o (C \<otimes> D)"
-  apply (auto intro!: subsetI simp add: elt_set_times_def set_times_def
-    mult_ac)
-   apply (rule_tac x = "aa * ba" in exI)
-   apply (auto simp add: mult_ac)
-  done
-
-theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
-  set_times_rearrange3 set_times_rearrange4
-
-lemma set_times_mono [intro]: "C <= D ==> a *o C <= a *o D"
-  by (auto simp add: elt_set_times_def)
-
-lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==>
-    C \<otimes> E <= D \<otimes> F"
-  by (auto simp add: set_times_def)
-
-lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C \<otimes> D"
-  by (auto simp add: elt_set_times_def set_times_def)
-
-lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==>
-    a *o D <= D \<otimes> C"
-  by (auto simp add: elt_set_times_def set_times_def mult_ac)
-
-lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C \<otimes> D"
-  apply (subgoal_tac "a *o B <= a *o D")
-   apply (erule order_trans)
-   apply (erule set_times_mono3)
-  apply (erule set_times_mono)
-  done
-
-lemma set_times_mono_b: "C <= D ==> x : a *o C
-    ==> x : a *o D"
-  apply (frule set_times_mono)
-  apply auto
-  done
-
-lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C \<otimes> E ==>
-    x : D \<otimes> F"
-  apply (frule set_times_mono2)
-   prefer 2
-   apply force
-  apply assumption
-  done
-
-lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C \<otimes> D"
-  apply (frule set_times_mono3)
-  apply auto
-  done
-
-lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==>
-    x : a *o D ==> x : D \<otimes> C"
-  apply (frule set_times_mono4)
-  apply auto
-  done
-
-lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C"
-  by (auto simp add: elt_set_times_def)
-
-lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)=
-    (a * b) +o (a *o C)"
-  by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs)
-
-lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B \<oplus> C) =
-    (a *o B) \<oplus> (a *o C)"
-  apply (auto simp add: set_plus_def elt_set_times_def ring_distribs)
-   apply blast
-  apply (rule_tac x = "b + bb" in exI)
-  apply (auto simp add: ring_distribs)
-  done
-
-lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) \<otimes> D <=
-    a *o D \<oplus> C \<otimes> D"
-  apply (auto intro!: subsetI simp add:
-    elt_set_plus_def elt_set_times_def set_times_def
-    set_plus_def ring_distribs)
-  apply auto
-  done
-
-theorems set_times_plus_distribs =
-  set_times_plus_distrib
-  set_times_plus_distrib2
-
-lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==>
-    - a : C"
-  by (auto simp add: elt_set_times_def)
-
-lemma set_neg_intro2: "(a::'a::ring_1) : C ==>
-    - a : (- 1) *o C"
-  by (auto simp add: elt_set_times_def)
-
-end
diff -r d6cb7e625d75 -r 86fc906dcd86 src/HOL/Metis_Examples/BigO.thy
--- a/src/HOL/Metis_Examples/BigO.thy	Fri Aug 20 17:46:56 2010 +0200
+++ b/src/HOL/Metis_Examples/BigO.thy	Fri Aug 20 17:48:30 2010 +0200
@@ -7,7 +7,7 @@
 header {* Big O notation *}
 
 theory BigO
-imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Main SetsAndFunctions 
+imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Main Function_Algebras Set_Algebras
 begin
 
 subsection {* Definitions *}
diff -r d6cb7e625d75 -r 86fc906dcd86 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Fri Aug 20 17:46:56 2010 +0200
+++ b/src/HOL/Tools/meson.ML	Fri Aug 20 17:48:30 2010 +0200
@@ -411,7 +411,7 @@
       (fn (c,T) => not(is_conn c) andalso exists has_bool (binder_types T));
 
 (*A higher-order instance of a first-order constant? Example is the definition of
-  one, 1, at a function type in theory SetsAndFunctions.*)
+  one, 1, at a function type in theory Function_Algebras.*)
 fun higher_inst_const thy (c,T) =
   case binder_types T of
       [] => false (*not a function type, OK*)