1.1 --- a/NEWS Mon Oct 08 11:37:03 2012 +0200
1.2 +++ b/NEWS Mon Oct 08 12:03:49 2012 +0200
1.3 @@ -62,6 +62,8 @@
1.4
1.5 *** HOL ***
1.6
1.7 +* Theorem UN_o generalized to SUP_comp. INCOMPATIBILITY.
1.8 +
1.9 * Class "comm_monoid_diff" formalises properties of bounded
1.10 subtraction, with natural numbers and multisets as typical instances.
1.11
2.1 --- a/src/Doc/Codegen/Further.thy Mon Oct 08 11:37:03 2012 +0200
2.2 +++ b/src/Doc/Codegen/Further.thy Mon Oct 08 12:03:49 2012 +0200
2.3 @@ -166,7 +166,7 @@
2.4 lemma %quote powers_power:
2.5 "powers xs \<circ> power x = power x \<circ> powers xs"
2.6 by (induct xs)
2.7 - (simp_all del: o_apply id_apply add: o_assoc [symmetric],
2.8 + (simp_all del: o_apply id_apply add: comp_assoc,
2.9 simp del: o_apply add: o_assoc power_commute)
2.10
2.11 lemma %quote powers_rev:
3.1 --- a/src/HOL/Finite_Set.thy Mon Oct 08 11:37:03 2012 +0200
3.2 +++ b/src/HOL/Finite_Set.thy Mon Oct 08 12:03:49 2012 +0200
3.3 @@ -793,7 +793,7 @@
3.4 with Suc have hyp: "f y ^^ h y \<circ> f x = f x \<circ> f y ^^ h y"
3.5 by auto
3.6 from Suc h_def have "g y = Suc (h y)" by simp
3.7 - then show ?case by (simp add: o_assoc [symmetric] hyp)
3.8 + then show ?case by (simp add: comp_assoc hyp)
3.9 (simp add: o_assoc comp_fun_commute)
3.10 qed
3.11 def h \<equiv> "\<lambda>z. if z = x then g x - 1 else g z"
3.12 @@ -803,7 +803,7 @@
3.13 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
3.14 from Suc h_def have "g x = Suc (h x)" by simp
3.15 then show ?case by (simp del: funpow.simps add: funpow_Suc_right o_assoc hyp2)
3.16 - (simp add: o_assoc [symmetric] hyp1)
3.17 + (simp add: comp_assoc hyp1)
3.18 qed
3.19 qed
3.20 qed
3.21 @@ -1507,7 +1507,7 @@
3.22 assumes "finite A"
3.23 shows "f x \<circ> F A = F A \<circ> f x"
3.24 using assms by (induct A)
3.25 - (simp, simp del: o_apply add: o_assoc, simp del: o_apply add: o_assoc [symmetric] comp_fun_commute)
3.26 + (simp, simp del: o_apply add: o_assoc, simp del: o_apply add: comp_assoc comp_fun_commute)
3.27
3.28 lemma commute_left_comp':
3.29 assumes "finite A"
3.30 @@ -1518,14 +1518,14 @@
3.31 assumes "finite A" and "finite B"
3.32 shows "F B \<circ> F A = F A \<circ> F B"
3.33 using assms by (induct A)
3.34 - (simp_all add: o_assoc, simp add: o_assoc [symmetric] comp_fun_commute')
3.35 + (simp_all add: o_assoc, simp add: comp_assoc comp_fun_commute')
3.36
3.37 lemma commute_left_comp'':
3.38 assumes "finite A" and "finite B"
3.39 shows "F B \<circ> (F A \<circ> g) = F A \<circ> (F B \<circ> g)"
3.40 using assms by (simp add: o_assoc comp_fun_commute'')
3.41
3.42 -lemmas comp_fun_commutes = o_assoc [symmetric] comp_fun_commute commute_left_comp
3.43 +lemmas comp_fun_commutes = comp_assoc comp_fun_commute commute_left_comp
3.44 comp_fun_commute' commute_left_comp' comp_fun_commute'' commute_left_comp''
3.45
3.46 lemma union_inter:
4.1 --- a/src/HOL/Fun.thy Mon Oct 08 11:37:03 2012 +0200
4.2 +++ b/src/HOL/Fun.thy Mon Oct 08 12:03:49 2012 +0200
4.3 @@ -41,34 +41,41 @@
4.4 notation (HTML output)
4.5 comp (infixl "\<circ>" 55)
4.6
4.7 -lemma o_apply [simp]: "(f o g) x = f (g x)"
4.8 -by (simp add: comp_def)
4.9 +lemma comp_apply [simp]: "(f o g) x = f (g x)"
4.10 + by (simp add: comp_def)
4.11
4.12 -lemma o_assoc: "f o (g o h) = f o g o h"
4.13 -by (simp add: comp_def)
4.14 +lemma comp_assoc: "(f o g) o h = f o (g o h)"
4.15 + by (simp add: fun_eq_iff)
4.16
4.17 -lemma id_o [simp]: "id o g = g"
4.18 -by (simp add: comp_def)
4.19 +lemma id_comp [simp]: "id o g = g"
4.20 + by (simp add: fun_eq_iff)
4.21
4.22 -lemma o_id [simp]: "f o id = f"
4.23 -by (simp add: comp_def)
4.24 +lemma comp_id [simp]: "f o id = f"
4.25 + by (simp add: fun_eq_iff)
4.26
4.27 -lemma o_eq_dest:
4.28 +lemma comp_eq_dest:
4.29 "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
4.30 - by (simp only: comp_def) (fact fun_cong)
4.31 + by (simp add: fun_eq_iff)
4.32
4.33 -lemma o_eq_elim:
4.34 +lemma comp_eq_elim:
4.35 "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
4.36 - by (erule meta_mp) (fact o_eq_dest)
4.37 + by (simp add: fun_eq_iff)
4.38
4.39 -lemma image_compose: "(f o g) ` r = f`(g`r)"
4.40 -by (simp add: comp_def, blast)
4.41 -
4.42 -lemma vimage_compose: "(g \<circ> f) -` x = f -` (g -` x)"
4.43 +lemma image_comp:
4.44 + "(f o g) ` r = f ` (g ` r)"
4.45 by auto
4.46
4.47 -lemma UN_o: "UNION A (g o f) = UNION (f`A) g"
4.48 -by (unfold comp_def, blast)
4.49 +lemma vimage_comp:
4.50 + "(g \<circ> f) -` x = f -` (g -` x)"
4.51 + by auto
4.52 +
4.53 +lemma INF_comp:
4.54 + "INFI A (g \<circ> f) = INFI (f ` A) g"
4.55 + by (simp add: INF_def image_comp)
4.56 +
4.57 +lemma SUP_comp:
4.58 + "SUPR A (g \<circ> f) = SUPR (f ` A) g"
4.59 + by (simp add: SUP_def image_comp)
4.60
4.61
4.62 subsection {* The Forward Composition Operator @{text fcomp} *}
4.63 @@ -735,10 +742,6 @@
4.64 by (rule the_inv_into_f_f)
4.65
4.66
4.67 -text{*compatibility*}
4.68 -lemmas o_def = comp_def
4.69 -
4.70 -
4.71 subsection {* Cantor's Paradox *}
4.72
4.73 lemma Cantors_paradox [no_atp]:
4.74 @@ -806,7 +809,19 @@
4.75 by (simp_all add: fun_eq_iff)
4.76
4.77 enriched_type vimage
4.78 - by (simp_all add: fun_eq_iff vimage_compose)
4.79 + by (simp_all add: fun_eq_iff vimage_comp)
4.80 +
4.81 +text {* Legacy theorem names *}
4.82 +
4.83 +lemmas o_def = comp_def
4.84 +lemmas o_apply = comp_apply
4.85 +lemmas o_assoc = comp_assoc [symmetric]
4.86 +lemmas id_o = id_comp
4.87 +lemmas o_id = comp_id
4.88 +lemmas o_eq_dest = comp_eq_dest
4.89 +lemmas o_eq_elim = comp_eq_elim
4.90 +lemmas image_compose = image_comp
4.91 +lemmas vimage_compose = vimage_comp
4.92
4.93 end
4.94
5.1 --- a/src/HOL/Hilbert_Choice.thy Mon Oct 08 11:37:03 2012 +0200
5.2 +++ b/src/HOL/Hilbert_Choice.thy Mon Oct 08 12:03:49 2012 +0200
5.3 @@ -144,7 +144,7 @@
5.4 by (simp add: inj_iff)
5.5
5.6 lemma o_inv_o_cancel[simp]: "inj f ==> g o inv f o f = g"
5.7 -by (simp add: o_assoc[symmetric])
5.8 +by (simp add: comp_assoc)
5.9
5.10 lemma inv_into_image_cancel[simp]:
5.11 "inj_on f A ==> S <= A ==> inv_into A f ` f ` S = S"
6.1 --- a/src/HOL/Library/Permutations.thy Mon Oct 08 11:37:03 2012 +0200
6.2 +++ b/src/HOL/Library/Permutations.thy Mon Oct 08 12:03:49 2012 +0200
6.3 @@ -292,7 +292,7 @@
6.4 next
6.5 case (comp_Suc n p a b m q)
6.6 have th: "Suc n + m = Suc (n + m)" by arith
6.7 - show ?case unfolding th o_assoc[symmetric]
6.8 + show ?case unfolding th comp_assoc
6.9 apply (rule swapidseq.comp_Suc) using comp_Suc.hyps(2)[OF comp_Suc.prems] comp_Suc.hyps(3) by blast+
6.10 qed
6.11
6.12 @@ -302,7 +302,7 @@
6.13 lemma swapidseq_endswap: "swapidseq n p \<Longrightarrow> a \<noteq> b ==> swapidseq (Suc n) (p o Fun.swap a b id)"
6.14 apply (induct n p rule: swapidseq.induct)
6.15 using swapidseq_swap[of a b]
6.16 - by (auto simp add: o_assoc[symmetric] intro: swapidseq.comp_Suc)
6.17 + by (auto simp add: comp_assoc intro: swapidseq.comp_Suc)
6.18
6.19 lemma swapidseq_inverse_exists: "swapidseq n p ==> \<exists>q. swapidseq n q \<and> p o q = id \<and> q o p = id"
6.20 proof(induct n p rule: swapidseq.induct)
6.21 @@ -418,7 +418,7 @@
6.22 have th2: "swapidseq (n - 1) (Fun.swap a z id o q)" "n \<noteq> 0" by blast+
6.23 have th: "Suc n - 1 = Suc (n - 1)" using th2(2) by auto
6.24 have ?case unfolding cdqm(2) H o_assoc th
6.25 - apply (simp only: Suc_not_Zero simp_thms o_assoc[symmetric])
6.26 + apply (simp only: Suc_not_Zero simp_thms comp_assoc)
6.27 apply (rule comp_Suc)
6.28 using th2 H apply blast+
6.29 done}
6.30 @@ -734,7 +734,7 @@
6.31 apply (rule permutes_compose)
6.32 using q apply auto
6.33 apply (rule_tac x = "x o inv q" in exI)
6.34 -by (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o o_assoc[symmetric])
6.35 +by (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o comp_assoc)
6.36
6.37 lemma permutes_in_seg: "p permutes {1 ..n} \<Longrightarrow> i \<in> {1..n} ==> 1 <= p i \<and> p i <= n"
6.38
6.39 @@ -770,7 +770,7 @@
6.40 proof-
6.41 fix p r
6.42 assume "p permutes S" and r:"r permutes S" and rp: "q \<circ> p = q \<circ> r"
6.43 - hence "inv q o q o p = inv q o q o r" by (simp add: o_assoc[symmetric])
6.44 + hence "inv q o q o p = inv q o q o r" by (simp add: comp_assoc)
6.45 with permutes_inj[OF q, unfolded inj_iff]
6.46
6.47 show "p = r" by simp
7.1 --- a/src/HOL/List.thy Mon Oct 08 11:37:03 2012 +0200
7.2 +++ b/src/HOL/List.thy Mon Oct 08 12:03:49 2012 +0200
7.3 @@ -2398,7 +2398,7 @@
7.4 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"
7.5 and x: "x \<in> set xs"
7.6 shows "fold f xs = fold f (remove1 x xs) \<circ> f x"
7.7 - using assms by (induct xs) (auto simp add: o_assoc [symmetric])
7.8 + using assms by (induct xs) (auto simp add: comp_assoc)
7.9
7.10 lemma fold_cong [fundef_cong]:
7.11 "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)
8.1 --- a/src/HOL/Word/Misc_Typedef.thy Mon Oct 08 11:37:03 2012 +0200
8.2 +++ b/src/HOL/Word/Misc_Typedef.thy Mon Oct 08 12:03:49 2012 +0200
8.3 @@ -102,7 +102,7 @@
8.4 "norm o norm = norm ==> (fr o norm = norm o fr) =
8.5 (norm o fr o norm = fr o norm & norm o fr o norm = norm o fr)"
8.6 apply safe
8.7 - apply (simp_all add: o_assoc [symmetric])
8.8 + apply (simp_all add: comp_assoc)
8.9 apply (simp_all add: o_assoc)
8.10 done
8.11
8.12 @@ -192,7 +192,7 @@
8.13 apply (fold eq_norm')
8.14 apply safe
8.15 prefer 2
8.16 - apply (simp add: o_assoc [symmetric])
8.17 + apply (simp add: comp_assoc)
8.18 apply (rule ext)
8.19 apply (drule fun_cong)
8.20 apply simp
8.21 @@ -208,7 +208,7 @@
8.22 apply (rule fns3 [THEN iffD1])
8.23 prefer 3
8.24 apply (rule fns2 [THEN iffD1])
8.25 - apply (simp_all add: o_assoc [symmetric])
8.26 + apply (simp_all add: comp_assoc)
8.27 apply (simp_all add: o_assoc)
8.28 done
8.29