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.66 -qed (force simp add: set_plus_def add.assoc)
    1.67 -
    1.68 -interpretation set_add!: abel_semigroup "set_plus :: 'a::ab_semigroup_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
    1.69 -qed (force simp add: set_plus_def add.commute)
    1.70 +instance set :: (semigroup_add) semigroup_add
    1.71 +by default (force simp add: set_plus_def add.assoc)
    1.72  
    1.73 -interpretation set_add!: monoid "set_plus :: 'a::monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" proof
    1.74 -qed (simp_all add: set_plus_def)
    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.77 -qed (simp add: set_plus_def)
    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.81 +instance set :: (ab_semigroup_add) ab_semigroup_add
    1.82 +by default (force simp add: set_plus_def add.commute)
    1.83  
    1.84 -interpretation set_add!: monoid_add "set_plus :: 'a::monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" where
    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.88 -  qed (simp_all add: set_add.assoc)
    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.93 +instance set :: (monoid_add) monoid_add
    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.99 -interpretation set_add!:
   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.103 +instance set :: (comm_monoid_add) comm_monoid_add
   1.104 +by default (simp_all add: set_plus_def)
   1.105  
   1.106 -interpretation set_add!: comm_monoid_add "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" where
   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.111 -  qed (simp_all add: set_add.commute)
   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.116 -    by (simp add: set_add.setsum_def setsum_set_def fun_eq_iff)
   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.128 -qed (simp_all add: set_times_def)
   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.131 -qed (simp add: set_times_def)
   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}"