src/HOL/Library/Set_Algebras.thy
 changeset 47443 aeff49a3369b parent 44890 22f665a2e91c child 47444 d21c95af2df7
```     1.1 --- a/src/HOL/Library/Set_Algebras.thy	Thu Apr 12 13:47:21 2012 +0200
1.2 +++ b/src/HOL/Library/Set_Algebras.thy	Thu Apr 12 19:58:59 2012 +0200
1.3 @@ -14,11 +14,53 @@
1.4    comments at the top of theory @{text BigO}.
1.5  *}
1.6
1.7 -definition set_plus :: "'a::plus set \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "\<oplus>" 65) where
1.8 -  "A \<oplus> B = {c. \<exists>a\<in>A. \<exists>b\<in>B. c = a + b}"
1.9 +instantiation set :: (plus) plus
1.10 +begin
1.11 +
1.12 +definition plus_set :: "'a::plus set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
1.13 +  set_plus_def: "A + B = {c. \<exists>a\<in>A. \<exists>b\<in>B. c = a + b}"
1.14 +
1.15 +instance ..
1.16 +
1.17 +end
1.18 +
1.19 +instantiation set :: (times) times
1.20 +begin
1.21 +
1.22 +definition times_set :: "'a::times set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
1.23 +  set_times_def: "A * B = {c. \<exists>a\<in>A. \<exists>b\<in>B. c = a * b}"
1.24 +
1.25 +instance ..
1.26 +
1.27 +end
1.28 +
1.29 +
1.30 +text {* Legacy syntax: *}
1.31
1.32 -definition set_times :: "'a::times set \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "\<otimes>" 70) where
1.33 -  "A \<otimes> B = {c. \<exists>a\<in>A. \<exists>b\<in>B. c = a * b}"
1.34 +abbreviation (input) set_plus :: "'a::plus set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "\<oplus>" 65) where
1.35 +  "A \<oplus> B \<equiv> A + B"
1.36 +abbreviation (input) set_times :: "'a::times set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "\<otimes>" 70) where
1.37 +  "A \<otimes> B \<equiv> A * B"
1.38 +
1.39 +instantiation set :: (zero) zero
1.40 +begin
1.41 +
1.42 +definition
1.43 +  set_zero[simp]: "0::('a::zero)set == {0}"
1.44 +
1.45 +instance ..
1.46 +
1.47 +end
1.48 +
1.49 +instantiation set :: (one) one
1.50 +begin
1.51 +
1.52 +definition
1.53 +  set_one[simp]: "1::('a::one)set == {1}"
1.54 +
1.55 +instance ..
1.56 +
1.57 +end
1.58
1.59  definition elt_set_plus :: "'a::plus \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "+o" 70) where
1.60    "a +o B = {c. \<exists>b\<in>B. c = a + b}"
1.61 @@ -29,96 +71,29 @@
1.62  abbreviation (input) elt_set_eq :: "'a \<Rightarrow> 'a set \<Rightarrow> bool"  (infix "=o" 50) where
1.63    "x =o A \<equiv> x \<in> A"
1.64
1.65 -interpretation set_add!: semigroup "set_plus :: 'a::semigroup_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
1.67 -
1.68 -interpretation set_add!: abel_semigroup "set_plus :: 'a::ab_semigroup_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
1.72
1.73 -interpretation set_add!: monoid "set_plus :: 'a::monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" proof
1.75 -
1.76 -interpretation set_add!: comm_monoid "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" proof
1.78 -
1.79 -definition listsum_set :: "('a::monoid_add set) list \<Rightarrow> 'a set" where
1.80 -  "listsum_set = monoid_add.listsum set_plus {0}"
1.83
1.85 -  "monoid_add.listsum set_plus {0::'a} = listsum_set"
1.86 -proof -
1.87 -  show "class.monoid_add set_plus {0::'a}" proof
1.89 -  then interpret set_add!: monoid_add "set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" .
1.90 -  show "monoid_add.listsum set_plus {0::'a} = listsum_set"
1.91 -    by (simp only: listsum_set_def)
1.92 -qed
1.94 +by default (simp_all add: set_plus_def)
1.95
1.96 -definition setsum_set :: "('b \<Rightarrow> ('a::comm_monoid_add) set) \<Rightarrow> 'b set \<Rightarrow> 'a set" where
1.97 -  "setsum_set f A = (if finite A then fold_image set_plus f {0} A else {0})"
1.98 -
1.100 -  comm_monoid_big "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" setsum_set
1.101 -proof
1.102 -qed (fact setsum_set_def)
1.104 +by default (simp_all add: set_plus_def)
1.105
1.107 -  "monoid_add.listsum set_plus {0::'a} = listsum_set"
1.108 -  and "comm_monoid_add.setsum set_plus {0::'a} = setsum_set"
1.109 -proof -
1.110 -  show "class.comm_monoid_add (set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set) {0}" proof
1.112 -  then interpret set_add!: comm_monoid_add "set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" .
1.113 -  show "monoid_add.listsum set_plus {0::'a} = listsum_set"
1.114 -    by (simp only: listsum_set_def)
1.115 -  show "comm_monoid_add.setsum set_plus {0::'a} = setsum_set"
1.117 -qed
1.118 +instance set :: (semigroup_mult) semigroup_mult
1.119 +by default (force simp add: set_times_def mult.assoc)
1.120
1.121 -interpretation set_mult!: semigroup "set_times :: 'a::semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
1.122 -qed (force simp add: set_times_def mult.assoc)
1.123 -
1.124 -interpretation set_mult!: abel_semigroup "set_times :: 'a::ab_semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
1.125 -qed (force simp add: set_times_def mult.commute)
1.126 -
1.127 -interpretation set_mult!: monoid "set_times :: 'a::monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" proof
1.129 -
1.130 -interpretation set_mult!: comm_monoid "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" proof
1.132 -
1.133 -definition power_set :: "nat \<Rightarrow> ('a::monoid_mult set) \<Rightarrow> 'a set" where
1.134 -  "power_set n A = power.power {1} set_times A n"
1.135 +instance set :: (ab_semigroup_mult) ab_semigroup_mult
1.136 +by default (force simp add: set_times_def mult.commute)
1.137
1.138 -interpretation set_mult!: monoid_mult "{1}" "set_times :: 'a::monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
1.139 -  "power.power {1} set_times = (\<lambda>A n. power_set n A)"
1.140 -proof -
1.141 -  show "class.monoid_mult {1} (set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set)" proof
1.142 -  qed (simp_all add: set_mult.assoc)
1.143 -  show "power.power {1} set_times = (\<lambda>A n. power_set n A)"
1.144 -    by (simp add: power_set_def)
1.145 -qed
1.146 -
1.147 -definition setprod_set :: "('b \<Rightarrow> ('a::comm_monoid_mult) set) \<Rightarrow> 'b set \<Rightarrow> 'a set" where
1.148 -  "setprod_set f A = (if finite A then fold_image set_times f {1} A else {1})"
1.149 +instance set :: (monoid_mult) monoid_mult
1.150 +by default (simp_all add: set_times_def)
1.151
1.152 -interpretation set_mult!:
1.153 -  comm_monoid_big "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" setprod_set
1.154 -proof
1.155 -qed (fact setprod_set_def)
1.156 -
1.157 -interpretation set_mult!: comm_monoid_mult "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" where
1.158 -  "power.power {1} set_times = (\<lambda>A n. power_set n A)"
1.159 -  and "comm_monoid_mult.setprod set_times {1::'a} = setprod_set"
1.160 -proof -
1.161 -  show "class.comm_monoid_mult (set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set) {1}" proof
1.162 -  qed (simp_all add: set_mult.commute)
1.163 -  then interpret set_mult!: comm_monoid_mult "set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" .
1.164 -  show "power.power {1} set_times = (\<lambda>A n. power_set n A)"
1.165 -    by (simp add: power_set_def)
1.166 -  show "comm_monoid_mult.setprod set_times {1::'a} = setprod_set"
1.167 -    by (simp add: set_mult.setprod_def setprod_set_def fun_eq_iff)
1.168 -qed
1.169 +instance set :: (comm_monoid_mult) comm_monoid_mult
1.170 +by default (simp_all add: set_times_def)
1.171
1.172  lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \<oplus> D"
1.173    by (auto simp add: set_plus_def)
1.174 @@ -358,6 +333,11 @@
1.175    fixes S T :: "'n::semigroup_add set" shows "S \<oplus> T = (\<lambda>(x, y). x + y) ` (S \<times> T)"
1.176    unfolding set_plus_def by (fastforce simp: image_iff)
1.177
1.178 +text {* Legacy syntax: *}
1.179 +
1.180 +abbreviation (input) setsum_set :: "('b \<Rightarrow> ('a::comm_monoid_add) set) \<Rightarrow> 'b set \<Rightarrow> 'a set" where
1.181 +   "setsum_set == setsum"
1.182 +
1.183  lemma set_setsum_alt:
1.184    assumes fin: "finite I"
1.185    shows "setsum_set S I = {setsum s I |s. \<forall>i\<in>I. s i \<in> S i}"
```