# HG changeset patch
# User krauss
# Date 1334253539 -7200
# Node ID aeff49a3369b85ed56c2da13840179bce0d3828f
# Parent  11a0aa6cc677e84c97ba0a2e098b59b9e6b38f32
backported Set_Algebras to use type classes (basically reverting b3e8d5ec721d from 2008)

diff -r 11a0aa6cc677 -r aeff49a3369b src/HOL/Library/Set_Algebras.thy
--- a/src/HOL/Library/Set_Algebras.thy	Thu Apr 12 13:47:21 2012 +0200
+++ b/src/HOL/Library/Set_Algebras.thy	Thu Apr 12 19:58:59 2012 +0200
@@ -14,11 +14,53 @@
   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}"
+instantiation set :: (plus) plus
+begin
+
+definition plus_set :: "'a::plus set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+  set_plus_def: "A + B = {c. \<exists>a\<in>A. \<exists>b\<in>B. c = a + b}"
+
+instance ..
+
+end
+
+instantiation set :: (times) times
+begin
+
+definition times_set :: "'a::times set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+  set_times_def: "A * B = {c. \<exists>a\<in>A. \<exists>b\<in>B. c = a * b}"
+
+instance ..
+
+end
+
+
+text {* Legacy syntax: *}
 
-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}"
+abbreviation (input) set_plus :: "'a::plus set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "\<oplus>" 65) where
+  "A \<oplus> B \<equiv> A + B"
+abbreviation (input) set_times :: "'a::times set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "\<otimes>" 70) where
+  "A \<otimes> B \<equiv> A * B"
+
+instantiation set :: (zero) zero
+begin
+
+definition
+  set_zero[simp]: "0::('a::zero)set == {0}"
+
+instance ..
+
+end
+ 
+instantiation set :: (one) one
+begin
+
+definition
+  set_one[simp]: "1::('a::one)set == {1}"
+
+instance ..
+
+end
 
 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}"
@@ -29,96 +71,29 @@
 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)
+instance set :: (semigroup_add) semigroup_add
+by default (force simp add: set_plus_def add.assoc)
 
-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}"
+instance set :: (ab_semigroup_add) ab_semigroup_add
+by default (force simp add: set_plus_def add.commute)
 
-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
+instance set :: (monoid_add) monoid_add
+by default (simp_all add: set_plus_def)
 
-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)
+instance set :: (comm_monoid_add) comm_monoid_add
+by default (simp_all add: set_plus_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 fun_eq_iff)
-qed
+instance set :: (semigroup_mult) semigroup_mult
+by default (force simp add: set_times_def mult.assoc)
 
-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"
+instance set :: (ab_semigroup_mult) ab_semigroup_mult
+by default (force simp add: set_times_def mult.commute)
 
-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})"
+instance set :: (monoid_mult) monoid_mult
+by default (simp_all add: set_times_def)
 
-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 fun_eq_iff)
-qed
+instance set :: (comm_monoid_mult) comm_monoid_mult
+by default (simp_all add: set_times_def)
 
 lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \<oplus> D"
   by (auto simp add: set_plus_def)
@@ -358,6 +333,11 @@
   fixes S T :: "'n::semigroup_add set" shows "S \<oplus> T = (\<lambda>(x, y). x + y) ` (S \<times> T)"
   unfolding set_plus_def by (fastforce simp: image_iff)
 
+text {* Legacy syntax: *}
+
+abbreviation (input) setsum_set :: "('b \<Rightarrow> ('a::comm_monoid_add) set) \<Rightarrow> 'b set \<Rightarrow> 'a set" where
+   "setsum_set == setsum"
+
 lemma set_setsum_alt:
   assumes fin: "finite I"
   shows "setsum_set S I = {setsum s I |s. \<forall>i\<in>I. s i \<in> S i}"