consolidated names of theorems on composition;
generalized former theorem UN_o;
comp_assoc orients to the right, as is more common

--- a/NEWS	Mon Oct 08 11:37:03 2012 +0200
+++ b/NEWS	Mon Oct 08 12:03:49 2012 +0200
@@ -62,6 +62,8 @@
 
 *** HOL ***
 
+* Theorem UN_o generalized to SUP_comp.  INCOMPATIBILITY.
+
 * Class "comm_monoid_diff" formalises properties of bounded
 subtraction, with natural numbers and multisets as typical instances.
 

--- a/src/Doc/Codegen/Further.thy	Mon Oct 08 11:37:03 2012 +0200
+++ b/src/Doc/Codegen/Further.thy	Mon Oct 08 12:03:49 2012 +0200
@@ -166,7 +166,7 @@
 lemma %quote powers_power:
   "powers xs \<circ> power x = power x \<circ> powers xs"
   by (induct xs)
-    (simp_all del: o_apply id_apply add: o_assoc [symmetric],
+    (simp_all del: o_apply id_apply add: comp_assoc,
       simp del: o_apply add: o_assoc power_commute)
 
 lemma %quote powers_rev:

--- a/src/HOL/Finite_Set.thy	Mon Oct 08 11:37:03 2012 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Oct 08 12:03:49 2012 +0200
@@ -793,7 +793,7 @@
         with Suc have hyp: "f y ^^ h y \<circ> f x = f x \<circ> f y ^^ h y"
           by auto
         from Suc h_def have "g y = Suc (h y)" by simp
-        then show ?case by (simp add: o_assoc [symmetric] hyp)
+        then show ?case by (simp add: comp_assoc hyp)
           (simp add: o_assoc comp_fun_commute)
       qed
       def h \<equiv> "\<lambda>z. if z = x then g x - 1 else g z"
@@ -803,7 +803,7 @@
       with False h_def have hyp2: "f y ^^ g y \<circ> f x ^^ h x = f x ^^ h x \<circ> f y ^^ g y" by simp
       from Suc h_def have "g x = Suc (h x)" by simp
       then show ?case by (simp del: funpow.simps add: funpow_Suc_right o_assoc hyp2)
-        (simp add: o_assoc [symmetric] hyp1)
+        (simp add: comp_assoc hyp1)
     qed
   qed
 qed
@@ -1507,7 +1507,7 @@
   assumes "finite A"
   shows "f x \<circ> F A = F A \<circ> f x"
   using assms by (induct A)
-    (simp, simp del: o_apply add: o_assoc, simp del: o_apply add: o_assoc [symmetric] comp_fun_commute)
+    (simp, simp del: o_apply add: o_assoc, simp del: o_apply add: comp_assoc comp_fun_commute)
 
 lemma commute_left_comp':
   assumes "finite A"
@@ -1518,14 +1518,14 @@
   assumes "finite A" and "finite B"
   shows "F B \<circ> F A = F A \<circ> F B"
   using assms by (induct A)
-    (simp_all add: o_assoc, simp add: o_assoc [symmetric] comp_fun_commute')
+    (simp_all add: o_assoc, simp add: comp_assoc comp_fun_commute')
 
 lemma commute_left_comp'':
   assumes "finite A" and "finite B"
   shows "F B \<circ> (F A \<circ> g) = F A \<circ> (F B \<circ> g)"
   using assms by (simp add: o_assoc comp_fun_commute'')
 
-lemmas comp_fun_commutes = o_assoc [symmetric] comp_fun_commute commute_left_comp
+lemmas comp_fun_commutes = comp_assoc comp_fun_commute commute_left_comp
   comp_fun_commute' commute_left_comp' comp_fun_commute'' commute_left_comp''
 
 lemma union_inter:

--- a/src/HOL/Fun.thy	Mon Oct 08 11:37:03 2012 +0200
+++ b/src/HOL/Fun.thy	Mon Oct 08 12:03:49 2012 +0200
@@ -41,34 +41,41 @@
 notation (HTML output)
   comp  (infixl "\<circ>" 55)
 
-lemma o_apply [simp]: "(f o g) x = f (g x)"
-by (simp add: comp_def)
-
-lemma o_assoc: "f o (g o h) = f o g o h"
-by (simp add: comp_def)
+lemma comp_apply [simp]: "(f o g) x = f (g x)"
+  by (simp add: comp_def)
 
-lemma id_o [simp]: "id o g = g"
-by (simp add: comp_def)
+lemma comp_assoc: "(f o g) o h = f o (g o h)"
+  by (simp add: fun_eq_iff)
 
-lemma o_id [simp]: "f o id = f"
-by (simp add: comp_def)
+lemma id_comp [simp]: "id o g = g"
+  by (simp add: fun_eq_iff)
 
-lemma o_eq_dest:
+lemma comp_id [simp]: "f o id = f"
+  by (simp add: fun_eq_iff)
+
+lemma comp_eq_dest:
   "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
-  by (simp only: comp_def) (fact fun_cong)
+  by (simp add: fun_eq_iff)
 
-lemma o_eq_elim:
+lemma comp_eq_elim:
   "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
-  by (erule meta_mp) (fact o_eq_dest) 
+  by (simp add: fun_eq_iff) 
 
-lemma image_compose: "(f o g) ` r = f`(g`r)"
-by (simp add: comp_def, blast)
-
-lemma vimage_compose: "(g \<circ> f) -` x = f -` (g -` x)"
+lemma image_comp:
+  "(f o g) ` r = f ` (g ` r)"
   by auto
 
-lemma UN_o: "UNION A (g o f) = UNION (f`A) g"
-by (unfold comp_def, blast)
+lemma vimage_comp:
+  "(g \<circ> f) -` x = f -` (g -` x)"
+  by auto
+
+lemma INF_comp:
+  "INFI A (g \<circ> f) = INFI (f ` A) g"
+  by (simp add: INF_def image_comp)
+
+lemma SUP_comp:
+  "SUPR A (g \<circ> f) = SUPR (f ` A) g"
+  by (simp add: SUP_def image_comp)
 
 
 subsection {* The Forward Composition Operator @{text fcomp} *}
@@ -735,10 +742,6 @@
   by (rule the_inv_into_f_f)
 
 
-text{*compatibility*}
-lemmas o_def = comp_def
-
-
 subsection {* Cantor's Paradox *}
 
 lemma Cantors_paradox [no_atp]:
@@ -806,7 +809,19 @@
   by (simp_all add: fun_eq_iff)
 
 enriched_type vimage
-  by (simp_all add: fun_eq_iff vimage_compose)
+  by (simp_all add: fun_eq_iff vimage_comp)
+
+text {* Legacy theorem names *}
+
+lemmas o_def = comp_def
+lemmas o_apply = comp_apply
+lemmas o_assoc = comp_assoc [symmetric]
+lemmas id_o = id_comp
+lemmas o_id = comp_id
+lemmas o_eq_dest = comp_eq_dest
+lemmas o_eq_elim = comp_eq_elim
+lemmas image_compose = image_comp
+lemmas vimage_compose = vimage_comp
 
 end
 

--- a/src/HOL/Hilbert_Choice.thy	Mon Oct 08 11:37:03 2012 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Mon Oct 08 12:03:49 2012 +0200
@@ -144,7 +144,7 @@
 by (simp add: inj_iff)
 
 lemma o_inv_o_cancel[simp]: "inj f ==> g o inv f o f = g"
-by (simp add: o_assoc[symmetric])
+by (simp add: comp_assoc)
 
 lemma inv_into_image_cancel[simp]:
   "inj_on f A ==> S <= A ==> inv_into A f ` f ` S = S"

--- a/src/HOL/Library/Permutations.thy	Mon Oct 08 11:37:03 2012 +0200
+++ b/src/HOL/Library/Permutations.thy	Mon Oct 08 12:03:49 2012 +0200
@@ -292,7 +292,7 @@
   next
     case (comp_Suc n p a b m q)
     have th: "Suc n + m = Suc (n + m)" by arith
-    show ?case unfolding th o_assoc[symmetric]
+    show ?case unfolding th comp_assoc
       apply (rule swapidseq.comp_Suc) using comp_Suc.hyps(2)[OF comp_Suc.prems]  comp_Suc.hyps(3) by blast+
 qed
 
@@ -302,7 +302,7 @@
 lemma swapidseq_endswap: "swapidseq n p \<Longrightarrow> a \<noteq> b ==> swapidseq (Suc n) (p o Fun.swap a b id)"
   apply (induct n p rule: swapidseq.induct)
   using swapidseq_swap[of a b]
-  by (auto simp add: o_assoc[symmetric] intro: swapidseq.comp_Suc)
+  by (auto simp add: comp_assoc intro: swapidseq.comp_Suc)
 
 lemma swapidseq_inverse_exists: "swapidseq n p ==> \<exists>q. swapidseq n q \<and> p o q = id \<and> q o p = id"
 proof(induct n p rule: swapidseq.induct)
@@ -418,7 +418,7 @@
     have th2: "swapidseq (n - 1) (Fun.swap a z id o q)" "n \<noteq> 0" by blast+
     have th: "Suc n - 1 = Suc (n - 1)" using th2(2) by auto
     have ?case unfolding cdqm(2) H o_assoc th
-      apply (simp only: Suc_not_Zero simp_thms o_assoc[symmetric])
+      apply (simp only: Suc_not_Zero simp_thms comp_assoc)
       apply (rule comp_Suc)
       using th2 H apply blast+
       done}
@@ -734,7 +734,7 @@
 apply (rule permutes_compose)
 using q apply auto
 apply (rule_tac x = "x o inv q" in exI)
-by (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o o_assoc[symmetric])
+by (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o comp_assoc)
 
 lemma permutes_in_seg: "p permutes {1 ..n} \<Longrightarrow> i \<in> {1..n} ==> 1 <= p i \<and> p i <= n"
 
@@ -770,7 +770,7 @@
   proof-
     fix p r
     assume "p permutes S" and r:"r permutes S" and rp: "q \<circ> p = q \<circ> r"
-    hence "inv q o q o p = inv q o q o r" by (simp add: o_assoc[symmetric])
+    hence "inv q o q o p = inv q o q o r" by (simp add: comp_assoc)
     with permutes_inj[OF q, unfolded inj_iff]
 
     show "p = r" by simp

--- a/src/HOL/List.thy	Mon Oct 08 11:37:03 2012 +0200
+++ b/src/HOL/List.thy	Mon Oct 08 12:03:49 2012 +0200
@@ -2398,7 +2398,7 @@
   assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
     and x: "x \<in> set xs"
   shows "fold f xs = fold f (remove1 x xs) \<circ> f x"
-  using assms by (induct xs) (auto simp add: o_assoc [symmetric])
+  using assms by (induct xs) (auto simp add: comp_assoc)
 
 lemma fold_cong [fundef_cong]:
   "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)

--- a/src/HOL/Word/Misc_Typedef.thy	Mon Oct 08 11:37:03 2012 +0200
+++ b/src/HOL/Word/Misc_Typedef.thy	Mon Oct 08 12:03:49 2012 +0200
@@ -102,7 +102,7 @@
   "norm o norm = norm ==> (fr o norm = norm o fr) = 
     (norm o fr o norm = fr o norm & norm o fr o norm = norm o fr)"
   apply safe
-    apply (simp_all add: o_assoc [symmetric])
+    apply (simp_all add: comp_assoc)
    apply (simp_all add: o_assoc)
   done
 
@@ -192,7 +192,7 @@
   apply (fold eq_norm')
   apply safe
    prefer 2
-   apply (simp add: o_assoc [symmetric])
+   apply (simp add: comp_assoc)
   apply (rule ext)
   apply (drule fun_cong)
   apply simp
@@ -208,7 +208,7 @@
    apply (rule fns3 [THEN iffD1])
      prefer 3
      apply (rule fns2 [THEN iffD1])
-       apply (simp_all add: o_assoc [symmetric])
+       apply (simp_all add: comp_assoc)
    apply (simp_all add: o_assoc)
   done