# HG changeset patch # User haftmann # Date 1349690629 -7200 # Node ID 13aa6d8268ecc712aa97a6b56c92aba7c02cecf1 # Parent 1e1611fd32df12e3df347398d07630add8abcd23 consolidated names of theorems on composition; generalized former theorem UN_o; comp_assoc orients to the right, as is more common diff -r 1e1611fd32df -r 13aa6d8268ec NEWS --- 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. diff -r 1e1611fd32df -r 13aa6d8268ec src/Doc/Codegen/Further.thy --- 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 \ power x = power x \ 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: diff -r 1e1611fd32df -r 13aa6d8268ec src/HOL/Finite_Set.thy --- 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 \ f x = f x \ 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 \ "\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 \ f x ^^ h x = f x ^^ h x \ 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 \ F A = F A \ 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 \ F A = F A \ 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 \ (F A \ g) = F A \ (F B \ 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: diff -r 1e1611fd32df -r 13aa6d8268ec src/HOL/Fun.thy --- 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 "\" 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 \ 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 \ ((\v. a (b v) = c (d v)) \ R) \ 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 \ 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 \ f) -` x = f -` (g -` x)" + by auto + +lemma INF_comp: + "INFI A (g \ f) = INFI (f ` A) g" + by (simp add: INF_def image_comp) + +lemma SUP_comp: + "SUPR A (g \ 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 diff -r 1e1611fd32df -r 13aa6d8268ec src/HOL/Hilbert_Choice.thy --- 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" diff -r 1e1611fd32df -r 13aa6d8268ec src/HOL/Library/Permutations.thy --- 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 \ a \ 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 ==> \q. swapidseq n q \ p o q = id \ 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 \ 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} \ i \ {1..n} ==> 1 <= p i \ p i <= n" @@ -770,7 +770,7 @@ proof- fix p r assume "p permutes S" and r:"r permutes S" and rp: "q \ p = q \ 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 diff -r 1e1611fd32df -r 13aa6d8268ec src/HOL/List.thy --- 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: "\x y. x \ set xs \ y \ set xs \ f x \ f y = f y \ f x" and x: "x \ set xs" shows "fold f xs = fold f (remove1 x xs) \ 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 \ xs = ys \ (\x. x \ set xs \ f x = g x) diff -r 1e1611fd32df -r 13aa6d8268ec src/HOL/Word/Misc_Typedef.thy --- 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