consolidated names of theorems on composition;
authorhaftmann
Mon Oct 08 12:03:49 2012 +0200 (2012-10-08)
changeset 4973913aa6d8268ec
parent 49738 1e1611fd32df
child 49740 6f02b893dd87
consolidated names of theorems on composition;
generalized former theorem UN_o;
comp_assoc orients to the right, as is more common
NEWS
src/Doc/Codegen/Further.thy
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Library/Permutations.thy
src/HOL/List.thy
src/HOL/Word/Misc_Typedef.thy
     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 -
    4.10 -lemma o_assoc: "f o (g o h) = f o g o h"
    4.11 -by (simp add: comp_def)
    4.12 +lemma comp_apply [simp]: "(f o g) x = f (g x)"
    4.13 +  by (simp add: comp_def)
    4.14  
    4.15 -lemma id_o [simp]: "id o g = g"
    4.16 -by (simp add: comp_def)
    4.17 +lemma comp_assoc: "(f o g) o h = f o (g o h)"
    4.18 +  by (simp add: fun_eq_iff)
    4.19  
    4.20 -lemma o_id [simp]: "f o id = f"
    4.21 -by (simp add: comp_def)
    4.22 +lemma id_comp [simp]: "id o g = g"
    4.23 +  by (simp add: fun_eq_iff)
    4.24  
    4.25 -lemma o_eq_dest:
    4.26 +lemma comp_id [simp]: "f o id = f"
    4.27 +  by (simp add: fun_eq_iff)
    4.28 +
    4.29 +lemma comp_eq_dest:
    4.30    "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
    4.31 -  by (simp only: comp_def) (fact fun_cong)
    4.32 +  by (simp add: fun_eq_iff)
    4.33  
    4.34 -lemma o_eq_elim:
    4.35 +lemma comp_eq_elim:
    4.36    "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
    4.37 -  by (erule meta_mp) (fact o_eq_dest) 
    4.38 +  by (simp add: fun_eq_iff) 
    4.39  
    4.40 -lemma image_compose: "(f o g) ` r = f`(g`r)"
    4.41 -by (simp add: comp_def, blast)
    4.42 -
    4.43 -lemma vimage_compose: "(g \<circ> f) -` x = f -` (g -` x)"
    4.44 +lemma image_comp:
    4.45 +  "(f o g) ` r = f ` (g ` r)"
    4.46    by auto
    4.47  
    4.48 -lemma UN_o: "UNION A (g o f) = UNION (f`A) g"
    4.49 -by (unfold comp_def, blast)
    4.50 +lemma vimage_comp:
    4.51 +  "(g \<circ> f) -` x = f -` (g -` x)"
    4.52 +  by auto
    4.53 +
    4.54 +lemma INF_comp:
    4.55 +  "INFI A (g \<circ> f) = INFI (f ` A) g"
    4.56 +  by (simp add: INF_def image_comp)
    4.57 +
    4.58 +lemma SUP_comp:
    4.59 +  "SUPR A (g \<circ> f) = SUPR (f ` A) g"
    4.60 +  by (simp add: SUP_def image_comp)
    4.61  
    4.62  
    4.63  subsection {* The Forward Composition Operator @{text fcomp} *}
    4.64 @@ -735,10 +742,6 @@
    4.65    by (rule the_inv_into_f_f)
    4.66  
    4.67  
    4.68 -text{*compatibility*}
    4.69 -lemmas o_def = comp_def
    4.70 -
    4.71 -
    4.72  subsection {* Cantor's Paradox *}
    4.73  
    4.74  lemma Cantors_paradox [no_atp]:
    4.75 @@ -806,7 +809,19 @@
    4.76    by (simp_all add: fun_eq_iff)
    4.77  
    4.78  enriched_type vimage
    4.79 -  by (simp_all add: fun_eq_iff vimage_compose)
    4.80 +  by (simp_all add: fun_eq_iff vimage_comp)
    4.81 +
    4.82 +text {* Legacy theorem names *}
    4.83 +
    4.84 +lemmas o_def = comp_def
    4.85 +lemmas o_apply = comp_apply
    4.86 +lemmas o_assoc = comp_assoc [symmetric]
    4.87 +lemmas id_o = id_comp
    4.88 +lemmas o_id = comp_id
    4.89 +lemmas o_eq_dest = comp_eq_dest
    4.90 +lemmas o_eq_elim = comp_eq_elim
    4.91 +lemmas image_compose = image_comp
    4.92 +lemmas vimage_compose = vimage_comp
    4.93  
    4.94  end
    4.95  
     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