src/HOL/Set.thy
 changeset 32683 7c1fe854ca6a parent 32456 341c83339aeb child 32888 ae17e72aac80
```     1.1 --- a/src/HOL/Set.thy	Fri Sep 18 14:09:38 2009 +0200
1.2 +++ b/src/HOL/Set.thy	Sat Sep 19 07:38:03 2009 +0200
1.3 @@ -652,8 +652,8 @@
1.4
1.5  subsubsection {* Binary union -- Un *}
1.6
1.7 -definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
1.8 -  sup_set_eq [symmetric]: "A Un B = sup A B"
1.9 +abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
1.10 +  "op Un \<equiv> sup"
1.11
1.12  notation (xsymbols)
1.13    union  (infixl "\<union>" 65)
1.14 @@ -663,7 +663,7 @@
1.15
1.16  lemma Un_def:
1.17    "A \<union> B = {x. x \<in> A \<or> x \<in> B}"
1.18 -  by (simp add: sup_fun_eq sup_bool_eq sup_set_eq [symmetric] Collect_def mem_def)
1.19 +  by (simp add: sup_fun_eq sup_bool_eq Collect_def mem_def)
1.20
1.21  lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
1.22    by (unfold Un_def) blast
1.23 @@ -689,15 +689,13 @@
1.24    by (simp add: Collect_def mem_def insert_compr Un_def)
1.25
1.26  lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
1.27 -  apply (fold sup_set_eq)
1.28 -  apply (erule mono_sup)
1.29 -  done
1.30 +  by (fact mono_sup)
1.31
1.32
1.33  subsubsection {* Binary intersection -- Int *}
1.34
1.35 -definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
1.36 -  inf_set_eq [symmetric]: "A Int B = inf A B"
1.37 +abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
1.38 +  "op Int \<equiv> inf"
1.39
1.40  notation (xsymbols)
1.41    inter  (infixl "\<inter>" 70)
1.42 @@ -707,7 +705,7 @@
1.43
1.44  lemma Int_def:
1.45    "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
1.46 -  by (simp add: inf_fun_eq inf_bool_eq inf_set_eq [symmetric] Collect_def mem_def)
1.47 +  by (simp add: inf_fun_eq inf_bool_eq Collect_def mem_def)
1.48
1.49  lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
1.50    by (unfold Int_def) blast
1.51 @@ -725,9 +723,7 @@
1.52    by simp
1.53
1.54  lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
1.55 -  apply (fold inf_set_eq)
1.56 -  apply (erule mono_inf)
1.57 -  done
1.58 +  by (fact mono_inf)
1.59
1.60
1.61  subsubsection {* Set difference *}
```