split and enriched theory SetsAndFunctions
authorhaftmann
Fri Aug 20 17:48:30 2010 +0200 (2010-08-20)
changeset 3862286fc906dcd86
parent 38621 d6cb7e625d75
child 38623 08a789ef8044
split and enriched theory SetsAndFunctions
NEWS
src/HOL/IsaMakefile
src/HOL/Library/BigO.thy
src/HOL/Library/Function_Algebras.thy
src/HOL/Library/Library.thy
src/HOL/Library/Set_Algebras.thy
src/HOL/Library/SetsAndFunctions.thy
src/HOL/Metis_Examples/BigO.thy
src/HOL/Tools/meson.ML
     1.1 --- a/NEWS	Fri Aug 20 17:46:56 2010 +0200
     1.2 +++ b/NEWS	Fri Aug 20 17:48:30 2010 +0200
     1.3 @@ -35,6 +35,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Theory SetsAndFunctions has been split into Function_Algebras and Set_Algebras;
     1.8 +canonical names for instance definitions for functions; various improvements.
     1.9 +INCOMPATIBILITY.
    1.10 +
    1.11  * Records: logical foundation type for records do not carry a '_type' suffix
    1.12  any longer.  INCOMPATIBILITY.
    1.13  
     2.1 --- a/src/HOL/IsaMakefile	Fri Aug 20 17:46:56 2010 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Fri Aug 20 17:48:30 2010 +0200
     2.3 @@ -408,6 +408,7 @@
     2.4    Library/Executable_Set.thy Library/Float.thy				\
     2.5    Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
     2.6    Library/FrechetDeriv.thy Library/Fset.thy Library/FuncSet.thy		\
     2.7 +  Library/Function_Algebras.thy						\
     2.8    Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy		\
     2.9    Library/Indicator_Function.thy Library/Infinite_Set.thy		\
    2.10    Library/Inner_Product.thy Library/Kleene_Algebra.thy			\
    2.11 @@ -428,8 +429,8 @@
    2.12    Library/Quotient_Product.thy Library/Quotient_Sum.thy			\
    2.13    Library/Quotient_Syntax.thy Library/Quotient_Type.thy			\
    2.14    Library/RBT.thy Library/RBT_Impl.thy Library/README.html		\
    2.15 -  Library/State_Monad.thy Library/Ramsey.thy Library/Reflection.thy	\
    2.16 -  Library/SML_Quickcheck.thy Library/SetsAndFunctions.thy		\
    2.17 +  Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy	\
    2.18 +  Library/Reflection.thy Library/SML_Quickcheck.thy 			\
    2.19    Library/Sublist_Order.thy Library/Sum_Of_Squares.thy			\
    2.20    Library/Sum_Of_Squares/sos_wrapper.ML					\
    2.21    Library/Sum_Of_Squares/sum_of_squares.ML				\
     3.1 --- a/src/HOL/Library/BigO.thy	Fri Aug 20 17:46:56 2010 +0200
     3.2 +++ b/src/HOL/Library/BigO.thy	Fri Aug 20 17:48:30 2010 +0200
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* Big O notation *}
     3.5  
     3.6  theory BigO
     3.7 -imports Complex_Main SetsAndFunctions
     3.8 +imports Complex_Main Function_Algebras Set_Algebras
     3.9  begin
    3.10  
    3.11  text {*
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/Function_Algebras.thy	Fri Aug 20 17:48:30 2010 +0200
     4.3 @@ -0,0 +1,207 @@
     4.4 +(*  Title:      HOL/Library/Function_Algebras.thy
     4.5 +    Author:     Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
     4.6 +*)
     4.7 +
     4.8 +header {* Pointwise instantiation of functions to algebra type classes *}
     4.9 +
    4.10 +theory Function_Algebras
    4.11 +imports Main
    4.12 +begin
    4.13 +
    4.14 +text {* Pointwise operations *}
    4.15 +
    4.16 +instantiation "fun" :: (type, plus) plus
    4.17 +begin
    4.18 +
    4.19 +definition
    4.20 +  "f + g = (\<lambda>x. f x + g x)"
    4.21 +
    4.22 +instance ..
    4.23 +
    4.24 +end
    4.25 +
    4.26 +instantiation "fun" :: (type, zero) zero
    4.27 +begin
    4.28 +
    4.29 +definition
    4.30 +  "0 = (\<lambda>x. 0)"
    4.31 +
    4.32 +instance ..
    4.33 +
    4.34 +end
    4.35 +
    4.36 +instantiation "fun" :: (type, times) times
    4.37 +begin
    4.38 +
    4.39 +definition
    4.40 +  "f * g = (\<lambda>x. f x * g x)"
    4.41 +
    4.42 +instance ..
    4.43 +
    4.44 +end
    4.45 +
    4.46 +instantiation "fun" :: (type, one) one
    4.47 +begin
    4.48 +
    4.49 +definition
    4.50 +  "1 = (\<lambda>x. 1)"
    4.51 +
    4.52 +instance ..
    4.53 +
    4.54 +end
    4.55 +
    4.56 +
    4.57 +text {* Additive structures *}
    4.58 +
    4.59 +instance "fun" :: (type, semigroup_add) semigroup_add proof
    4.60 +qed (simp add: plus_fun_def add.assoc)
    4.61 +
    4.62 +instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add proof
    4.63 +qed (simp_all add: plus_fun_def expand_fun_eq)
    4.64 +
    4.65 +instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add proof
    4.66 +qed (simp add: plus_fun_def add.commute)
    4.67 +
    4.68 +instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add proof
    4.69 +qed simp
    4.70 +
    4.71 +instance "fun" :: (type, monoid_add) monoid_add proof
    4.72 +qed (simp_all add: plus_fun_def zero_fun_def)
    4.73 +
    4.74 +instance "fun" :: (type, comm_monoid_add) comm_monoid_add proof
    4.75 +qed simp
    4.76 +
    4.77 +instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add ..
    4.78 +
    4.79 +instance "fun" :: (type, group_add) group_add proof
    4.80 +qed (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
    4.81 +
    4.82 +instance "fun" :: (type, ab_group_add) ab_group_add proof
    4.83 +qed (simp_all add: diff_minus)
    4.84 +
    4.85 +
    4.86 +text {* Multiplicative structures *}
    4.87 +
    4.88 +instance "fun" :: (type, semigroup_mult) semigroup_mult proof
    4.89 +qed (simp add: times_fun_def mult.assoc)
    4.90 +
    4.91 +instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult proof
    4.92 +qed (simp add: times_fun_def mult.commute)
    4.93 +
    4.94 +instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult proof
    4.95 +qed (simp add: times_fun_def)
    4.96 +
    4.97 +instance "fun" :: (type, monoid_mult) monoid_mult proof
    4.98 +qed (simp_all add: times_fun_def one_fun_def)
    4.99 +
   4.100 +instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult proof
   4.101 +qed simp
   4.102 +
   4.103 +
   4.104 +text {* Misc *}
   4.105 +
   4.106 +instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
   4.107 +
   4.108 +instance "fun" :: (type, mult_zero) mult_zero proof
   4.109 +qed (simp_all add: zero_fun_def times_fun_def)
   4.110 +
   4.111 +instance "fun" :: (type, mult_mono) mult_mono proof
   4.112 +qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
   4.113 +
   4.114 +instance "fun" :: (type, mult_mono1) mult_mono1 proof
   4.115 +qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_mono1)
   4.116 +
   4.117 +instance "fun" :: (type, zero_neq_one) zero_neq_one proof
   4.118 +qed (simp add: zero_fun_def one_fun_def expand_fun_eq)
   4.119 +
   4.120 +
   4.121 +text {* Ring structures *}
   4.122 +
   4.123 +instance "fun" :: (type, semiring) semiring proof
   4.124 +qed (simp_all add: plus_fun_def times_fun_def algebra_simps)
   4.125 +
   4.126 +instance "fun" :: (type, comm_semiring) comm_semiring proof
   4.127 +qed (simp add: plus_fun_def times_fun_def algebra_simps)
   4.128 +
   4.129 +instance "fun" :: (type, semiring_0) semiring_0 ..
   4.130 +
   4.131 +instance "fun" :: (type, comm_semiring_0) comm_semiring_0 ..
   4.132 +
   4.133 +instance "fun" :: (type, semiring_0_cancel) semiring_0_cancel ..
   4.134 +
   4.135 +instance "fun" :: (type, comm_semiring_0_cancel) comm_semiring_0_cancel ..
   4.136 +
   4.137 +instance "fun" :: (type, semiring_1) semiring_1 ..
   4.138 +
   4.139 +lemma of_nat_fun:
   4.140 +  shows "of_nat n = (\<lambda>x::'a. of_nat n)"
   4.141 +proof -
   4.142 +  have comp: "comp = (\<lambda>f g x. f (g x))"
   4.143 +    by (rule ext)+ simp
   4.144 +  have plus_fun: "plus = (\<lambda>f g x. f x + g x)"
   4.145 +    by (rule ext, rule ext) (fact plus_fun_def)
   4.146 +  have "of_nat n = (comp (plus (1::'b)) ^^ n) (\<lambda>x::'a. 0)"
   4.147 +    by (simp add: of_nat_def plus_fun zero_fun_def one_fun_def comp)
   4.148 +  also have "... = comp ((plus 1) ^^ n) (\<lambda>x::'a. 0)"
   4.149 +    by (simp only: comp_funpow)
   4.150 +  finally show ?thesis by (simp add: of_nat_def comp)
   4.151 +qed
   4.152 +
   4.153 +instance "fun" :: (type, comm_semiring_1) comm_semiring_1 ..
   4.154 +
   4.155 +instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
   4.156 +
   4.157 +instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel ..
   4.158 +
   4.159 +instance "fun" :: (type, semiring_char_0) semiring_char_0 proof
   4.160 +  from inj_of_nat have "inj (\<lambda>n (x::'a). of_nat n :: 'b)"
   4.161 +    by (rule inj_fun)
   4.162 +  then have "inj (\<lambda>n. of_nat n :: 'a \<Rightarrow> 'b)"
   4.163 +    by (simp add: of_nat_fun)
   4.164 +  then show "inj (of_nat :: nat \<Rightarrow> 'a \<Rightarrow> 'b)" .
   4.165 +qed
   4.166 +
   4.167 +instance "fun" :: (type, ring) ring ..
   4.168 +
   4.169 +instance "fun" :: (type, comm_ring) comm_ring ..
   4.170 +
   4.171 +instance "fun" :: (type, ring_1) ring_1 ..
   4.172 +
   4.173 +instance "fun" :: (type, comm_ring_1) comm_ring_1 ..
   4.174 +
   4.175 +instance "fun" :: (type, ring_char_0) ring_char_0 ..
   4.176 +
   4.177 +
   4.178 +text {* Ordereded structures *}
   4.179 +
   4.180 +instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add proof
   4.181 +qed (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
   4.182 +
   4.183 +instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
   4.184 +
   4.185 +instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le proof
   4.186 +qed (simp add: plus_fun_def le_fun_def)
   4.187 +
   4.188 +instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
   4.189 +
   4.190 +instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
   4.191 +
   4.192 +instance "fun" :: (type, ordered_semiring) ordered_semiring ..
   4.193 +
   4.194 +instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring ..
   4.195 +
   4.196 +instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
   4.197 +
   4.198 +instance "fun" :: (type, ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
   4.199 +
   4.200 +instance "fun" :: (type, ordered_ring) ordered_ring ..
   4.201 +
   4.202 +instance "fun" :: (type, ordered_comm_ring) ordered_comm_ring ..
   4.203 +
   4.204 +
   4.205 +lemmas func_plus = plus_fun_def
   4.206 +lemmas func_zero = zero_fun_def
   4.207 +lemmas func_times = times_fun_def
   4.208 +lemmas func_one = one_fun_def
   4.209 +
   4.210 +end
     5.1 --- a/src/HOL/Library/Library.thy	Fri Aug 20 17:46:56 2010 +0200
     5.2 +++ b/src/HOL/Library/Library.thy	Fri Aug 20 17:48:30 2010 +0200
     5.3 @@ -22,6 +22,7 @@
     5.4    FrechetDeriv
     5.5    Fset
     5.6    FuncSet
     5.7 +  Function_Algebras
     5.8    Fundamental_Theorem_Algebra
     5.9    Indicator_Function
    5.10    Infinite_Set
    5.11 @@ -54,6 +55,7 @@
    5.12    Ramsey
    5.13    Reflection
    5.14    RBT
    5.15 +  Set_Algebras
    5.16    SML_Quickcheck
    5.17    State_Monad
    5.18    Sum_Of_Squares
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Library/Set_Algebras.thy	Fri Aug 20 17:48:30 2010 +0200
     6.3 @@ -0,0 +1,357 @@
     6.4 +(*  Title:      HOL/Library/Set_Algebras.thy
     6.5 +    Author:     Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
     6.6 +*)
     6.7 +
     6.8 +header {* Algebraic operations on sets *}
     6.9 +
    6.10 +theory Set_Algebras
    6.11 +imports Main
    6.12 +begin
    6.13 +
    6.14 +text {*
    6.15 +  This library lifts operations like addition and muliplication to
    6.16 +  sets.  It was designed to support asymptotic calculations. See the
    6.17 +  comments at the top of theory @{text BigO}.
    6.18 +*}
    6.19 +
    6.20 +definition set_plus :: "'a::plus set \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "\<oplus>" 65) where
    6.21 +  "A \<oplus> B = {c. \<exists>a\<in>A. \<exists>b\<in>B. c = a + b}"
    6.22 +
    6.23 +definition set_times :: "'a::times set \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "\<otimes>" 70) where
    6.24 +  "A \<otimes> B = {c. \<exists>a\<in>A. \<exists>b\<in>B. c = a * b}"
    6.25 +
    6.26 +definition elt_set_plus :: "'a::plus \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "+o" 70) where
    6.27 +  "a +o B = {c. \<exists>b\<in>B. c = a + b}"
    6.28 +
    6.29 +definition elt_set_times :: "'a::times \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "*o" 80) where
    6.30 +  "a *o B = {c. \<exists>b\<in>B. c = a * b}"
    6.31 +
    6.32 +abbreviation (input) elt_set_eq :: "'a \<Rightarrow> 'a set \<Rightarrow> bool"  (infix "=o" 50) where
    6.33 +  "x =o A \<equiv> x \<in> A"
    6.34 +
    6.35 +interpretation set_add!: semigroup "set_plus :: 'a::semigroup_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
    6.36 +qed (force simp add: set_plus_def add.assoc)
    6.37 +
    6.38 +interpretation set_add!: abel_semigroup "set_plus :: 'a::ab_semigroup_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
    6.39 +qed (force simp add: set_plus_def add.commute)
    6.40 +
    6.41 +interpretation set_add!: monoid "set_plus :: 'a::monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" proof
    6.42 +qed (simp_all add: set_plus_def)
    6.43 +
    6.44 +interpretation set_add!: comm_monoid "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" proof
    6.45 +qed (simp add: set_plus_def)
    6.46 +
    6.47 +definition listsum_set :: "('a::monoid_add set) list \<Rightarrow> 'a set" where
    6.48 +  "listsum_set = monoid_add.listsum set_plus {0}"
    6.49 +
    6.50 +interpretation set_add!: monoid_add "set_plus :: 'a::monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" where
    6.51 +  "monoid_add.listsum set_plus {0::'a} = listsum_set"
    6.52 +proof -
    6.53 +  show "class.monoid_add set_plus {0::'a}" proof
    6.54 +  qed (simp_all add: set_add.assoc)
    6.55 +  then interpret set_add!: monoid_add "set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" .
    6.56 +  show "monoid_add.listsum set_plus {0::'a} = listsum_set"
    6.57 +    by (simp only: listsum_set_def)
    6.58 +qed
    6.59 +
    6.60 +definition setsum_set :: "('b \<Rightarrow> ('a::comm_monoid_add) set) \<Rightarrow> 'b set \<Rightarrow> 'a set" where
    6.61 +  "setsum_set f A = (if finite A then fold_image set_plus f {0} A else {0})"
    6.62 +
    6.63 +interpretation set_add!:
    6.64 +  comm_monoid_big "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" setsum_set 
    6.65 +proof
    6.66 +qed (fact setsum_set_def)
    6.67 +
    6.68 +interpretation set_add!: comm_monoid_add "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" where
    6.69 +  "monoid_add.listsum set_plus {0::'a} = listsum_set"
    6.70 +  and "comm_monoid_add.setsum set_plus {0::'a} = setsum_set"
    6.71 +proof -
    6.72 +  show "class.comm_monoid_add (set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set) {0}" proof
    6.73 +  qed (simp_all add: set_add.commute)
    6.74 +  then interpret set_add!: comm_monoid_add "set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" .
    6.75 +  show "monoid_add.listsum set_plus {0::'a} = listsum_set"
    6.76 +    by (simp only: listsum_set_def)
    6.77 +  show "comm_monoid_add.setsum set_plus {0::'a} = setsum_set"
    6.78 +    by (simp add: set_add.setsum_def setsum_set_def expand_fun_eq)
    6.79 +qed
    6.80 +
    6.81 +interpretation set_mult!: semigroup "set_times :: 'a::semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
    6.82 +qed (force simp add: set_times_def mult.assoc)
    6.83 +
    6.84 +interpretation set_mult!: abel_semigroup "set_times :: 'a::ab_semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
    6.85 +qed (force simp add: set_times_def mult.commute)
    6.86 +
    6.87 +interpretation set_mult!: monoid "set_times :: 'a::monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" proof
    6.88 +qed (simp_all add: set_times_def)
    6.89 +
    6.90 +interpretation set_mult!: comm_monoid "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" proof
    6.91 +qed (simp add: set_times_def)
    6.92 +
    6.93 +definition power_set :: "nat \<Rightarrow> ('a::monoid_mult set) \<Rightarrow> 'a set" where
    6.94 +  "power_set n A = power.power {1} set_times A n"
    6.95 +
    6.96 +interpretation set_mult!: monoid_mult "{1}" "set_times :: 'a::monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    6.97 +  "power.power {1} set_times = (\<lambda>A n. power_set n A)"
    6.98 +proof -
    6.99 +  show "class.monoid_mult {1} (set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set)" proof
   6.100 +  qed (simp_all add: set_mult.assoc)
   6.101 +  show "power.power {1} set_times = (\<lambda>A n. power_set n A)"
   6.102 +    by (simp add: power_set_def)
   6.103 +qed
   6.104 +
   6.105 +definition setprod_set :: "('b \<Rightarrow> ('a::comm_monoid_mult) set) \<Rightarrow> 'b set \<Rightarrow> 'a set" where
   6.106 +  "setprod_set f A = (if finite A then fold_image set_times f {1} A else {1})"
   6.107 +
   6.108 +interpretation set_mult!:
   6.109 +  comm_monoid_big "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" setprod_set 
   6.110 +proof
   6.111 +qed (fact setprod_set_def)
   6.112 +
   6.113 +interpretation set_mult!: comm_monoid_mult "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" where
   6.114 +  "power.power {1} set_times = (\<lambda>A n. power_set n A)"
   6.115 +  and "comm_monoid_mult.setprod set_times {1::'a} = setprod_set"
   6.116 +proof -
   6.117 +  show "class.comm_monoid_mult (set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set) {1}" proof
   6.118 +  qed (simp_all add: set_mult.commute)
   6.119 +  then interpret set_mult!: comm_monoid_mult "set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" .
   6.120 +  show "power.power {1} set_times = (\<lambda>A n. power_set n A)"
   6.121 +    by (simp add: power_set_def)
   6.122 +  show "comm_monoid_mult.setprod set_times {1::'a} = setprod_set"
   6.123 +    by (simp add: set_mult.setprod_def setprod_set_def expand_fun_eq)
   6.124 +qed
   6.125 +
   6.126 +lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \<oplus> D"
   6.127 +  by (auto simp add: set_plus_def)
   6.128 +
   6.129 +lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
   6.130 +  by (auto simp add: elt_set_plus_def)
   6.131 +
   6.132 +lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) \<oplus>
   6.133 +    (b +o D) = (a + b) +o (C \<oplus> D)"
   6.134 +  apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
   6.135 +   apply (rule_tac x = "ba + bb" in exI)
   6.136 +  apply (auto simp add: add_ac)
   6.137 +  apply (rule_tac x = "aa + a" in exI)
   6.138 +  apply (auto simp add: add_ac)
   6.139 +  done
   6.140 +
   6.141 +lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) =
   6.142 +    (a + b) +o C"
   6.143 +  by (auto simp add: elt_set_plus_def add_assoc)
   6.144 +
   6.145 +lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) \<oplus> C =
   6.146 +    a +o (B \<oplus> C)"
   6.147 +  apply (auto simp add: elt_set_plus_def set_plus_def)
   6.148 +   apply (blast intro: add_ac)
   6.149 +  apply (rule_tac x = "a + aa" in exI)
   6.150 +  apply (rule conjI)
   6.151 +   apply (rule_tac x = "aa" in bexI)
   6.152 +    apply auto
   6.153 +  apply (rule_tac x = "ba" in bexI)
   6.154 +   apply (auto simp add: add_ac)
   6.155 +  done
   6.156 +
   6.157 +theorem set_plus_rearrange4: "C \<oplus> ((a::'a::comm_monoid_add) +o D) =
   6.158 +    a +o (C \<oplus> D)"
   6.159 +  apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus_def add_ac)
   6.160 +   apply (rule_tac x = "aa + ba" in exI)
   6.161 +   apply (auto simp add: add_ac)
   6.162 +  done
   6.163 +
   6.164 +theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
   6.165 +  set_plus_rearrange3 set_plus_rearrange4
   6.166 +
   6.167 +lemma set_plus_mono [intro!]: "C <= D ==> a +o C <= a +o D"
   6.168 +  by (auto simp add: elt_set_plus_def)
   6.169 +
   6.170 +lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==>
   6.171 +    C \<oplus> E <= D \<oplus> F"
   6.172 +  by (auto simp add: set_plus_def)
   6.173 +
   6.174 +lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C \<oplus> D"
   6.175 +  by (auto simp add: elt_set_plus_def set_plus_def)
   6.176 +
   6.177 +lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==>
   6.178 +    a +o D <= D \<oplus> C"
   6.179 +  by (auto simp add: elt_set_plus_def set_plus_def add_ac)
   6.180 +
   6.181 +lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C \<oplus> D"
   6.182 +  apply (subgoal_tac "a +o B <= a +o D")
   6.183 +   apply (erule order_trans)
   6.184 +   apply (erule set_plus_mono3)
   6.185 +  apply (erule set_plus_mono)
   6.186 +  done
   6.187 +
   6.188 +lemma set_plus_mono_b: "C <= D ==> x : a +o C
   6.189 +    ==> x : a +o D"
   6.190 +  apply (frule set_plus_mono)
   6.191 +  apply auto
   6.192 +  done
   6.193 +
   6.194 +lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C \<oplus> E ==>
   6.195 +    x : D \<oplus> F"
   6.196 +  apply (frule set_plus_mono2)
   6.197 +   prefer 2
   6.198 +   apply force
   6.199 +  apply assumption
   6.200 +  done
   6.201 +
   6.202 +lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C \<oplus> D"
   6.203 +  apply (frule set_plus_mono3)
   6.204 +  apply auto
   6.205 +  done
   6.206 +
   6.207 +lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==>
   6.208 +    x : a +o D ==> x : D \<oplus> C"
   6.209 +  apply (frule set_plus_mono4)
   6.210 +  apply auto
   6.211 +  done
   6.212 +
   6.213 +lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C"
   6.214 +  by (auto simp add: elt_set_plus_def)
   6.215 +
   6.216 +lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A \<oplus> B"
   6.217 +  apply (auto intro!: subsetI simp add: set_plus_def)
   6.218 +  apply (rule_tac x = 0 in bexI)
   6.219 +   apply (rule_tac x = x in bexI)
   6.220 +    apply (auto simp add: add_ac)
   6.221 +  done
   6.222 +
   6.223 +lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C"
   6.224 +  by (auto simp add: elt_set_plus_def add_ac diff_minus)
   6.225 +
   6.226 +lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C"
   6.227 +  apply (auto simp add: elt_set_plus_def add_ac diff_minus)
   6.228 +  apply (subgoal_tac "a = (a + - b) + b")
   6.229 +   apply (rule bexI, assumption, assumption)
   6.230 +  apply (auto simp add: add_ac)
   6.231 +  done
   6.232 +
   6.233 +lemma set_minus_plus: "((a::'a::ab_group_add) - b : C) = (a : b +o C)"
   6.234 +  by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus,
   6.235 +    assumption)
   6.236 +
   6.237 +lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C \<otimes> D"
   6.238 +  by (auto simp add: set_times_def)
   6.239 +
   6.240 +lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
   6.241 +  by (auto simp add: elt_set_times_def)
   6.242 +
   6.243 +lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) \<otimes>
   6.244 +    (b *o D) = (a * b) *o (C \<otimes> D)"
   6.245 +  apply (auto simp add: elt_set_times_def set_times_def)
   6.246 +   apply (rule_tac x = "ba * bb" in exI)
   6.247 +   apply (auto simp add: mult_ac)
   6.248 +  apply (rule_tac x = "aa * a" in exI)
   6.249 +  apply (auto simp add: mult_ac)
   6.250 +  done
   6.251 +
   6.252 +lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) =
   6.253 +    (a * b) *o C"
   6.254 +  by (auto simp add: elt_set_times_def mult_assoc)
   6.255 +
   6.256 +lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) \<otimes> C =
   6.257 +    a *o (B \<otimes> C)"
   6.258 +  apply (auto simp add: elt_set_times_def set_times_def)
   6.259 +   apply (blast intro: mult_ac)
   6.260 +  apply (rule_tac x = "a * aa" in exI)
   6.261 +  apply (rule conjI)
   6.262 +   apply (rule_tac x = "aa" in bexI)
   6.263 +    apply auto
   6.264 +  apply (rule_tac x = "ba" in bexI)
   6.265 +   apply (auto simp add: mult_ac)
   6.266 +  done
   6.267 +
   6.268 +theorem set_times_rearrange4: "C \<otimes> ((a::'a::comm_monoid_mult) *o D) =
   6.269 +    a *o (C \<otimes> D)"
   6.270 +  apply (auto intro!: subsetI simp add: elt_set_times_def set_times_def
   6.271 +    mult_ac)
   6.272 +   apply (rule_tac x = "aa * ba" in exI)
   6.273 +   apply (auto simp add: mult_ac)
   6.274 +  done
   6.275 +
   6.276 +theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
   6.277 +  set_times_rearrange3 set_times_rearrange4
   6.278 +
   6.279 +lemma set_times_mono [intro]: "C <= D ==> a *o C <= a *o D"
   6.280 +  by (auto simp add: elt_set_times_def)
   6.281 +
   6.282 +lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==>
   6.283 +    C \<otimes> E <= D \<otimes> F"
   6.284 +  by (auto simp add: set_times_def)
   6.285 +
   6.286 +lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C \<otimes> D"
   6.287 +  by (auto simp add: elt_set_times_def set_times_def)
   6.288 +
   6.289 +lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==>
   6.290 +    a *o D <= D \<otimes> C"
   6.291 +  by (auto simp add: elt_set_times_def set_times_def mult_ac)
   6.292 +
   6.293 +lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C \<otimes> D"
   6.294 +  apply (subgoal_tac "a *o B <= a *o D")
   6.295 +   apply (erule order_trans)
   6.296 +   apply (erule set_times_mono3)
   6.297 +  apply (erule set_times_mono)
   6.298 +  done
   6.299 +
   6.300 +lemma set_times_mono_b: "C <= D ==> x : a *o C
   6.301 +    ==> x : a *o D"
   6.302 +  apply (frule set_times_mono)
   6.303 +  apply auto
   6.304 +  done
   6.305 +
   6.306 +lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C \<otimes> E ==>
   6.307 +    x : D \<otimes> F"
   6.308 +  apply (frule set_times_mono2)
   6.309 +   prefer 2
   6.310 +   apply force
   6.311 +  apply assumption
   6.312 +  done
   6.313 +
   6.314 +lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C \<otimes> D"
   6.315 +  apply (frule set_times_mono3)
   6.316 +  apply auto
   6.317 +  done
   6.318 +
   6.319 +lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==>
   6.320 +    x : a *o D ==> x : D \<otimes> C"
   6.321 +  apply (frule set_times_mono4)
   6.322 +  apply auto
   6.323 +  done
   6.324 +
   6.325 +lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C"
   6.326 +  by (auto simp add: elt_set_times_def)
   6.327 +
   6.328 +lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)=
   6.329 +    (a * b) +o (a *o C)"
   6.330 +  by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs)
   6.331 +
   6.332 +lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B \<oplus> C) =
   6.333 +    (a *o B) \<oplus> (a *o C)"
   6.334 +  apply (auto simp add: set_plus_def elt_set_times_def ring_distribs)
   6.335 +   apply blast
   6.336 +  apply (rule_tac x = "b + bb" in exI)
   6.337 +  apply (auto simp add: ring_distribs)
   6.338 +  done
   6.339 +
   6.340 +lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) \<otimes> D <=
   6.341 +    a *o D \<oplus> C \<otimes> D"
   6.342 +  apply (auto intro!: subsetI simp add:
   6.343 +    elt_set_plus_def elt_set_times_def set_times_def
   6.344 +    set_plus_def ring_distribs)
   6.345 +  apply auto
   6.346 +  done
   6.347 +
   6.348 +theorems set_times_plus_distribs =
   6.349 +  set_times_plus_distrib
   6.350 +  set_times_plus_distrib2
   6.351 +
   6.352 +lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==>
   6.353 +    - a : C"
   6.354 +  by (auto simp add: elt_set_times_def)
   6.355 +
   6.356 +lemma set_neg_intro2: "(a::'a::ring_1) : C ==>
   6.357 +    - a : (- 1) *o C"
   6.358 +  by (auto simp add: elt_set_times_def)
   6.359 +
   6.360 +end
     7.1 --- a/src/HOL/Library/SetsAndFunctions.thy	Fri Aug 20 17:46:56 2010 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,373 +0,0 @@
     7.4 -(*  Title:      HOL/Library/SetsAndFunctions.thy
     7.5 -    Author:     Jeremy Avigad and Kevin Donnelly
     7.6 -*)
     7.7 -
     7.8 -header {* Operations on sets and functions *}
     7.9 -
    7.10 -theory SetsAndFunctions
    7.11 -imports Main
    7.12 -begin
    7.13 -
    7.14 -text {*
    7.15 -This library lifts operations like addition and muliplication to sets and
    7.16 -functions of appropriate types. It was designed to support asymptotic
    7.17 -calculations. See the comments at the top of theory @{text BigO}.
    7.18 -*}
    7.19 -
    7.20 -subsection {* Basic definitions *}
    7.21 -
    7.22 -definition
    7.23 -  set_plus :: "('a::plus) set => 'a set => 'a set"  (infixl "\<oplus>" 65) where
    7.24 -  "A \<oplus> B == {c. EX a:A. EX b:B. c = a + b}"
    7.25 -
    7.26 -instantiation "fun" :: (type, plus) plus
    7.27 -begin
    7.28 -
    7.29 -definition
    7.30 -  func_plus: "f + g == (%x. f x + g x)"
    7.31 -
    7.32 -instance ..
    7.33 -
    7.34 -end
    7.35 -
    7.36 -definition
    7.37 -  set_times :: "('a::times) set => 'a set => 'a set"  (infixl "\<otimes>" 70) where
    7.38 -  "A \<otimes> B == {c. EX a:A. EX b:B. c = a * b}"
    7.39 -
    7.40 -instantiation "fun" :: (type, times) times
    7.41 -begin
    7.42 -
    7.43 -definition
    7.44 -  func_times: "f * g == (%x. f x * g x)"
    7.45 -
    7.46 -instance ..
    7.47 -
    7.48 -end
    7.49 -
    7.50 -
    7.51 -instantiation "fun" :: (type, zero) zero
    7.52 -begin
    7.53 -
    7.54 -definition
    7.55 -  func_zero: "0::(('a::type) => ('b::zero)) == %x. 0"
    7.56 -
    7.57 -instance ..
    7.58 -
    7.59 -end
    7.60 -
    7.61 -instantiation "fun" :: (type, one) one
    7.62 -begin
    7.63 -
    7.64 -definition
    7.65 -  func_one: "1::(('a::type) => ('b::one)) == %x. 1"
    7.66 -
    7.67 -instance ..
    7.68 -
    7.69 -end
    7.70 -
    7.71 -definition
    7.72 -  elt_set_plus :: "'a::plus => 'a set => 'a set"  (infixl "+o" 70) where
    7.73 -  "a +o B = {c. EX b:B. c = a + b}"
    7.74 -
    7.75 -definition
    7.76 -  elt_set_times :: "'a::times => 'a set => 'a set"  (infixl "*o" 80) where
    7.77 -  "a *o B = {c. EX b:B. c = a * b}"
    7.78 -
    7.79 -abbreviation (input)
    7.80 -  elt_set_eq :: "'a => 'a set => bool"  (infix "=o" 50) where
    7.81 -  "x =o A == x : A"
    7.82 -
    7.83 -instance "fun" :: (type,semigroup_add)semigroup_add
    7.84 -  by default (auto simp add: func_plus add_assoc)
    7.85 -
    7.86 -instance "fun" :: (type,comm_monoid_add)comm_monoid_add
    7.87 -  by default (auto simp add: func_zero func_plus add_ac)
    7.88 -
    7.89 -instance "fun" :: (type,ab_group_add)ab_group_add
    7.90 -  apply default
    7.91 -   apply (simp add: fun_Compl_def func_plus func_zero)
    7.92 -  apply (simp add: fun_Compl_def func_plus fun_diff_def diff_minus)
    7.93 -  done
    7.94 -
    7.95 -instance "fun" :: (type,semigroup_mult)semigroup_mult
    7.96 -  apply default
    7.97 -  apply (auto simp add: func_times mult_assoc)
    7.98 -  done
    7.99 -
   7.100 -instance "fun" :: (type,comm_monoid_mult)comm_monoid_mult
   7.101 -  apply default
   7.102 -   apply (auto simp add: func_one func_times mult_ac)
   7.103 -  done
   7.104 -
   7.105 -instance "fun" :: (type,comm_ring_1)comm_ring_1
   7.106 -  apply default
   7.107 -   apply (auto simp add: func_plus func_times fun_Compl_def fun_diff_def
   7.108 -     func_one func_zero algebra_simps)
   7.109 -  apply (drule fun_cong)
   7.110 -  apply simp
   7.111 -  done
   7.112 -
   7.113 -interpretation set_semigroup_add: semigroup_add "op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"
   7.114 -  apply default
   7.115 -  apply (unfold set_plus_def)
   7.116 -  apply (force simp add: add_assoc)
   7.117 -  done
   7.118 -
   7.119 -interpretation set_semigroup_mult: semigroup_mult "op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"
   7.120 -  apply default
   7.121 -  apply (unfold set_times_def)
   7.122 -  apply (force simp add: mult_assoc)
   7.123 -  done
   7.124 -
   7.125 -interpretation set_comm_monoid_add: comm_monoid_add "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set" "{0}"
   7.126 -  apply default
   7.127 -   apply (unfold set_plus_def)
   7.128 -   apply (force simp add: add_ac)
   7.129 -  apply force
   7.130 -  done
   7.131 -
   7.132 -interpretation set_comm_monoid_mult: comm_monoid_mult "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set" "{1}"
   7.133 -  apply default
   7.134 -   apply (unfold set_times_def)
   7.135 -   apply (force simp add: mult_ac)
   7.136 -  apply force
   7.137 -  done
   7.138 -
   7.139 -
   7.140 -subsection {* Basic properties *}
   7.141 -
   7.142 -lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \<oplus> D"
   7.143 -  by (auto simp add: set_plus_def)
   7.144 -
   7.145 -lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
   7.146 -  by (auto simp add: elt_set_plus_def)
   7.147 -
   7.148 -lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) \<oplus>
   7.149 -    (b +o D) = (a + b) +o (C \<oplus> D)"
   7.150 -  apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
   7.151 -   apply (rule_tac x = "ba + bb" in exI)
   7.152 -  apply (auto simp add: add_ac)
   7.153 -  apply (rule_tac x = "aa + a" in exI)
   7.154 -  apply (auto simp add: add_ac)
   7.155 -  done
   7.156 -
   7.157 -lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) =
   7.158 -    (a + b) +o C"
   7.159 -  by (auto simp add: elt_set_plus_def add_assoc)
   7.160 -
   7.161 -lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) \<oplus> C =
   7.162 -    a +o (B \<oplus> C)"
   7.163 -  apply (auto simp add: elt_set_plus_def set_plus_def)
   7.164 -   apply (blast intro: add_ac)
   7.165 -  apply (rule_tac x = "a + aa" in exI)
   7.166 -  apply (rule conjI)
   7.167 -   apply (rule_tac x = "aa" in bexI)
   7.168 -    apply auto
   7.169 -  apply (rule_tac x = "ba" in bexI)
   7.170 -   apply (auto simp add: add_ac)
   7.171 -  done
   7.172 -
   7.173 -theorem set_plus_rearrange4: "C \<oplus> ((a::'a::comm_monoid_add) +o D) =
   7.174 -    a +o (C \<oplus> D)"
   7.175 -  apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus_def add_ac)
   7.176 -   apply (rule_tac x = "aa + ba" in exI)
   7.177 -   apply (auto simp add: add_ac)
   7.178 -  done
   7.179 -
   7.180 -theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
   7.181 -  set_plus_rearrange3 set_plus_rearrange4
   7.182 -
   7.183 -lemma set_plus_mono [intro!]: "C <= D ==> a +o C <= a +o D"
   7.184 -  by (auto simp add: elt_set_plus_def)
   7.185 -
   7.186 -lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==>
   7.187 -    C \<oplus> E <= D \<oplus> F"
   7.188 -  by (auto simp add: set_plus_def)
   7.189 -
   7.190 -lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C \<oplus> D"
   7.191 -  by (auto simp add: elt_set_plus_def set_plus_def)
   7.192 -
   7.193 -lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==>
   7.194 -    a +o D <= D \<oplus> C"
   7.195 -  by (auto simp add: elt_set_plus_def set_plus_def add_ac)
   7.196 -
   7.197 -lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C \<oplus> D"
   7.198 -  apply (subgoal_tac "a +o B <= a +o D")
   7.199 -   apply (erule order_trans)
   7.200 -   apply (erule set_plus_mono3)
   7.201 -  apply (erule set_plus_mono)
   7.202 -  done
   7.203 -
   7.204 -lemma set_plus_mono_b: "C <= D ==> x : a +o C
   7.205 -    ==> x : a +o D"
   7.206 -  apply (frule set_plus_mono)
   7.207 -  apply auto
   7.208 -  done
   7.209 -
   7.210 -lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C \<oplus> E ==>
   7.211 -    x : D \<oplus> F"
   7.212 -  apply (frule set_plus_mono2)
   7.213 -   prefer 2
   7.214 -   apply force
   7.215 -  apply assumption
   7.216 -  done
   7.217 -
   7.218 -lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C \<oplus> D"
   7.219 -  apply (frule set_plus_mono3)
   7.220 -  apply auto
   7.221 -  done
   7.222 -
   7.223 -lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==>
   7.224 -    x : a +o D ==> x : D \<oplus> C"
   7.225 -  apply (frule set_plus_mono4)
   7.226 -  apply auto
   7.227 -  done
   7.228 -
   7.229 -lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C"
   7.230 -  by (auto simp add: elt_set_plus_def)
   7.231 -
   7.232 -lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A \<oplus> B"
   7.233 -  apply (auto intro!: subsetI simp add: set_plus_def)
   7.234 -  apply (rule_tac x = 0 in bexI)
   7.235 -   apply (rule_tac x = x in bexI)
   7.236 -    apply (auto simp add: add_ac)
   7.237 -  done
   7.238 -
   7.239 -lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C"
   7.240 -  by (auto simp add: elt_set_plus_def add_ac diff_minus)
   7.241 -
   7.242 -lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C"
   7.243 -  apply (auto simp add: elt_set_plus_def add_ac diff_minus)
   7.244 -  apply (subgoal_tac "a = (a + - b) + b")
   7.245 -   apply (rule bexI, assumption, assumption)
   7.246 -  apply (auto simp add: add_ac)
   7.247 -  done
   7.248 -
   7.249 -lemma set_minus_plus: "((a::'a::ab_group_add) - b : C) = (a : b +o C)"
   7.250 -  by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus,
   7.251 -    assumption)
   7.252 -
   7.253 -lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C \<otimes> D"
   7.254 -  by (auto simp add: set_times_def)
   7.255 -
   7.256 -lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
   7.257 -  by (auto simp add: elt_set_times_def)
   7.258 -
   7.259 -lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) \<otimes>
   7.260 -    (b *o D) = (a * b) *o (C \<otimes> D)"
   7.261 -  apply (auto simp add: elt_set_times_def set_times_def)
   7.262 -   apply (rule_tac x = "ba * bb" in exI)
   7.263 -   apply (auto simp add: mult_ac)
   7.264 -  apply (rule_tac x = "aa * a" in exI)
   7.265 -  apply (auto simp add: mult_ac)
   7.266 -  done
   7.267 -
   7.268 -lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) =
   7.269 -    (a * b) *o C"
   7.270 -  by (auto simp add: elt_set_times_def mult_assoc)
   7.271 -
   7.272 -lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) \<otimes> C =
   7.273 -    a *o (B \<otimes> C)"
   7.274 -  apply (auto simp add: elt_set_times_def set_times_def)
   7.275 -   apply (blast intro: mult_ac)
   7.276 -  apply (rule_tac x = "a * aa" in exI)
   7.277 -  apply (rule conjI)
   7.278 -   apply (rule_tac x = "aa" in bexI)
   7.279 -    apply auto
   7.280 -  apply (rule_tac x = "ba" in bexI)
   7.281 -   apply (auto simp add: mult_ac)
   7.282 -  done
   7.283 -
   7.284 -theorem set_times_rearrange4: "C \<otimes> ((a::'a::comm_monoid_mult) *o D) =
   7.285 -    a *o (C \<otimes> D)"
   7.286 -  apply (auto intro!: subsetI simp add: elt_set_times_def set_times_def
   7.287 -    mult_ac)
   7.288 -   apply (rule_tac x = "aa * ba" in exI)
   7.289 -   apply (auto simp add: mult_ac)
   7.290 -  done
   7.291 -
   7.292 -theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
   7.293 -  set_times_rearrange3 set_times_rearrange4
   7.294 -
   7.295 -lemma set_times_mono [intro]: "C <= D ==> a *o C <= a *o D"
   7.296 -  by (auto simp add: elt_set_times_def)
   7.297 -
   7.298 -lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==>
   7.299 -    C \<otimes> E <= D \<otimes> F"
   7.300 -  by (auto simp add: set_times_def)
   7.301 -
   7.302 -lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C \<otimes> D"
   7.303 -  by (auto simp add: elt_set_times_def set_times_def)
   7.304 -
   7.305 -lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==>
   7.306 -    a *o D <= D \<otimes> C"
   7.307 -  by (auto simp add: elt_set_times_def set_times_def mult_ac)
   7.308 -
   7.309 -lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C \<otimes> D"
   7.310 -  apply (subgoal_tac "a *o B <= a *o D")
   7.311 -   apply (erule order_trans)
   7.312 -   apply (erule set_times_mono3)
   7.313 -  apply (erule set_times_mono)
   7.314 -  done
   7.315 -
   7.316 -lemma set_times_mono_b: "C <= D ==> x : a *o C
   7.317 -    ==> x : a *o D"
   7.318 -  apply (frule set_times_mono)
   7.319 -  apply auto
   7.320 -  done
   7.321 -
   7.322 -lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C \<otimes> E ==>
   7.323 -    x : D \<otimes> F"
   7.324 -  apply (frule set_times_mono2)
   7.325 -   prefer 2
   7.326 -   apply force
   7.327 -  apply assumption
   7.328 -  done
   7.329 -
   7.330 -lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C \<otimes> D"
   7.331 -  apply (frule set_times_mono3)
   7.332 -  apply auto
   7.333 -  done
   7.334 -
   7.335 -lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==>
   7.336 -    x : a *o D ==> x : D \<otimes> C"
   7.337 -  apply (frule set_times_mono4)
   7.338 -  apply auto
   7.339 -  done
   7.340 -
   7.341 -lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C"
   7.342 -  by (auto simp add: elt_set_times_def)
   7.343 -
   7.344 -lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)=
   7.345 -    (a * b) +o (a *o C)"
   7.346 -  by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs)
   7.347 -
   7.348 -lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B \<oplus> C) =
   7.349 -    (a *o B) \<oplus> (a *o C)"
   7.350 -  apply (auto simp add: set_plus_def elt_set_times_def ring_distribs)
   7.351 -   apply blast
   7.352 -  apply (rule_tac x = "b + bb" in exI)
   7.353 -  apply (auto simp add: ring_distribs)
   7.354 -  done
   7.355 -
   7.356 -lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) \<otimes> D <=
   7.357 -    a *o D \<oplus> C \<otimes> D"
   7.358 -  apply (auto intro!: subsetI simp add:
   7.359 -    elt_set_plus_def elt_set_times_def set_times_def
   7.360 -    set_plus_def ring_distribs)
   7.361 -  apply auto
   7.362 -  done
   7.363 -
   7.364 -theorems set_times_plus_distribs =
   7.365 -  set_times_plus_distrib
   7.366 -  set_times_plus_distrib2
   7.367 -
   7.368 -lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==>
   7.369 -    - a : C"
   7.370 -  by (auto simp add: elt_set_times_def)
   7.371 -
   7.372 -lemma set_neg_intro2: "(a::'a::ring_1) : C ==>
   7.373 -    - a : (- 1) *o C"
   7.374 -  by (auto simp add: elt_set_times_def)
   7.375 -
   7.376 -end
     8.1 --- a/src/HOL/Metis_Examples/BigO.thy	Fri Aug 20 17:46:56 2010 +0200
     8.2 +++ b/src/HOL/Metis_Examples/BigO.thy	Fri Aug 20 17:48:30 2010 +0200
     8.3 @@ -7,7 +7,7 @@
     8.4  header {* Big O notation *}
     8.5  
     8.6  theory BigO
     8.7 -imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Main SetsAndFunctions 
     8.8 +imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Main Function_Algebras Set_Algebras
     8.9  begin
    8.10  
    8.11  subsection {* Definitions *}
     9.1 --- a/src/HOL/Tools/meson.ML	Fri Aug 20 17:46:56 2010 +0200
     9.2 +++ b/src/HOL/Tools/meson.ML	Fri Aug 20 17:48:30 2010 +0200
     9.3 @@ -411,7 +411,7 @@
     9.4        (fn (c,T) => not(is_conn c) andalso exists has_bool (binder_types T));
     9.5  
     9.6  (*A higher-order instance of a first-order constant? Example is the definition of
     9.7 -  one, 1, at a function type in theory SetsAndFunctions.*)
     9.8 +  one, 1, at a function type in theory Function_Algebras.*)
     9.9  fun higher_inst_const thy (c,T) =
    9.10    case binder_types T of
    9.11        [] => false (*not a function type, OK*)