--- 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.
--- 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 \
--- 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 {*
--- /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
--- 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
--- /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
--- 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
--- 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 *}
--- 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*)