# HG changeset patch # User griff # Date 1333442706 -32400 # Node ID b75ce48a93ee2dce30f7d7ff9eb8f90b0c96e08f # Parent 07f4bf913230f9797c0183b09ea176fbc520b4c8 dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q" diff -r 07f4bf913230 -r b75ce48a93ee src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Tue Apr 03 17:26:30 2012 +0900 +++ b/src/HOL/Quotient.thy Tue Apr 03 17:45:06 2012 +0900 @@ -717,9 +717,9 @@ apply (rule QuotientI) apply (simp add: o_def Quotient_abs_rep [OF R2] Quotient_abs_rep [OF R1]) apply simp - apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI) + apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI) apply (rule Quotient_rep_reflp [OF R1]) - apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI [rotated]) + apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI [rotated]) apply (rule Quotient_rep_reflp [OF R1]) apply (rule Rep1) apply (rule Quotient_rep_reflp [OF R2]) @@ -730,8 +730,8 @@ apply (erule Quotient_refl1 [OF R1]) apply (drule Quotient_refl1 [OF R2], drule Rep1) apply (subgoal_tac "R1 r (Rep1 (Abs1 x))") - apply (rule_tac b="Rep1 (Abs1 x)" in pred_compI, assumption) - apply (erule pred_compI) + apply (rule_tac b="Rep1 (Abs1 x)" in relcomppI, assumption) + apply (erule relcomppI) apply (erule Quotient_symp [OF R1, THEN sympD]) apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2]) apply (rule conjI, erule Quotient_refl1 [OF R1]) @@ -744,8 +744,8 @@ apply (erule Quotient_refl1 [OF R1]) apply (drule Quotient_refl2 [OF R2], drule Rep1) apply (subgoal_tac "R1 s (Rep1 (Abs1 y))") - apply (rule_tac b="Rep1 (Abs1 y)" in pred_compI, assumption) - apply (erule pred_compI) + apply (rule_tac b="Rep1 (Abs1 y)" in relcomppI, assumption) + apply (erule relcomppI) apply (erule Quotient_symp [OF R1, THEN sympD]) apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2]) apply (rule conjI, erule Quotient_refl2 [OF R1]) @@ -761,11 +761,11 @@ apply (erule Quotient_refl1 [OF R1]) apply (rename_tac a b c d) apply simp - apply (rule_tac b="Rep1 (Abs1 r)" in pred_compI) + apply (rule_tac b="Rep1 (Abs1 r)" in relcomppI) apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2]) apply (rule conjI, erule Quotient_refl1 [OF R1]) apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1]) - apply (rule_tac b="Rep1 (Abs1 s)" in pred_compI [rotated]) + apply (rule_tac b="Rep1 (Abs1 s)" in relcomppI [rotated]) apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2]) apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1]) apply (erule Quotient_refl2 [OF R1]) diff -r 07f4bf913230 -r b75ce48a93ee src/HOL/Quotient_Examples/FSet.thy --- a/src/HOL/Quotient_Examples/FSet.thy Tue Apr 03 17:26:30 2012 +0900 +++ b/src/HOL/Quotient_Examples/FSet.thy Tue Apr 03 17:45:06 2012 +0900 @@ -140,7 +140,7 @@ next assume a: "(list_all2 R OOO op \) r s" then have b: "map Abs r \ map Abs s" - proof (elim pred_compE) + proof (elim relcomppE) fix b ba assume c: "list_all2 R r b" assume d: "b \ ba" @@ -165,11 +165,11 @@ have y: "list_all2 R (map Rep (map Abs s)) s" by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_all2_refl'[OF e, of s]]) have c: "(op \ OO list_all2 R) (map Rep (map Abs r)) s" - by (rule pred_compI) (rule b, rule y) + by (rule relcomppI) (rule b, rule y) have z: "list_all2 R r (map Rep (map Abs r))" by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_all2_refl'[OF e, of r]]) then show "(list_all2 R OOO op \) r s" - using a c pred_compI by simp + using a c relcomppI by simp qed qed @@ -360,7 +360,7 @@ quotient_definition "concat_fset :: ('a fset) fset \ 'a fset" is concat -proof (elim pred_compE) +proof (elim relcomppE) fix a b ba bb assume a: "list_all2 op \ a ba" with list_symp [OF list_eq_symp] have a': "list_all2 op \ ba a" by (rule sympE) @@ -397,9 +397,9 @@ lemma Cons_rsp2 [quot_respect]: shows "(op \ ===> list_all2 op \ OOO op \ ===> list_all2 op \ OOO op \) Cons Cons" apply (auto intro!: fun_relI) - apply (rule_tac b="x # b" in pred_compI) + apply (rule_tac b="x # b" in relcomppI) apply auto - apply (rule_tac b="x # ba" in pred_compI) + apply (rule_tac b="x # ba" in relcomppI) apply auto done @@ -453,7 +453,7 @@ assumes "(R1 ===> R2 ===> R3) C C" and "(R4 ===> R5 ===> R6) C C" shows "(R1 OOO R4 ===> R2 OOO R5 ===> R3 OOO R6) C C" by (auto intro!: fun_relI) - (metis (full_types) assms fun_relE pred_compI) + (metis (full_types) assms fun_relE relcomppI) lemma append_rsp2 [quot_respect]: "(list_all2 op \ OOO op \ ===> list_all2 op \ OOO op \ ===> list_all2 op \ OOO op \) append append" @@ -479,7 +479,7 @@ by (induct y ya rule: list_induct2') (simp_all, metis apply_rsp' list_eq_def) show "(list_all2 op \ OOO op \) (map f xa) (map f' ya)" - by (metis a b c list_eq_def pred_compI) + by (metis a b c list_eq_def relcomppI) qed lemma map_prs2 [quot_preserve]: diff -r 07f4bf913230 -r b75ce48a93ee src/HOL/Relation.thy --- a/src/HOL/Relation.thy Tue Apr 03 17:26:30 2012 +0900 +++ b/src/HOL/Relation.thy Tue Apr 03 17:45:06 2012 +0900 @@ -512,10 +512,9 @@ where relcompI [intro]: "(a, b) \ r \ (b, c) \ s \ (a, c) \ r O s" -abbreviation pred_comp (infixr "OO" 75) where - "pred_comp \ relcompp" +notation relcompp (infixr "OO" 75) -lemmas pred_compI = relcompp.intros +lemmas relcomppI = relcompp.intros text {* For historic reasons, the elimination rules are not wholly corresponding. @@ -523,14 +522,12 @@ *} inductive_cases relcompEpair: "(a, c) \ r O s" -inductive_cases pred_compE [elim!]: "(r OO s) a c" +inductive_cases relcomppE [elim!]: "(r OO s) a c" lemma relcompE [elim!]: "xz \ r O s \ (\x y z. xz = (x, z) \ (x, y) \ r \ (y, z) \ s \ P) \ P" by (cases xz) (simp, erule relcompEpair, iprover) -lemmas pred_comp_relcomp_eq = relcompp_relcomp_eq - lemma R_O_Id [simp]: "R O Id = R" by fast @@ -543,7 +540,7 @@ "{} O R = {}" by blast -lemma pred_comp_bot1 [simp]: +lemma relcompp_bot1 [simp]: "\ OO R = \" by (fact relcomp_empty1 [to_pred]) @@ -551,7 +548,7 @@ "R O {} = {}" by blast -lemma pred_comp_bot2 [simp]: +lemma relcompp_bot2 [simp]: "R OO \ = \" by (fact relcomp_empty2 [to_pred]) @@ -560,7 +557,7 @@ by blast -lemma pred_comp_assoc: +lemma relcompp_assoc: "(r OO s) OO t = r OO (s OO t)" by (fact O_assoc [to_pred]) @@ -568,7 +565,7 @@ "trans r \ r O r \ r" by (unfold trans_def) blast -lemma transp_pred_comp_less_eq: +lemma transp_relcompp_less_eq: "transp r \ r OO r \ r " by (fact trans_O_subset [to_pred]) @@ -576,7 +573,7 @@ "r' \ r \ s' \ s \ r' O s' \ r O s" by blast -lemma pred_comp_mono: +lemma relcompp_mono: "r' \ r \ s' \ s \ r' OO s' \ r OO s " by (fact relcomp_mono [to_pred]) @@ -588,7 +585,7 @@ "R O (S \ T) = (R O S) \ (R O T)" by auto -lemma pred_comp_distrib [simp]: +lemma relcompp_distrib [simp]: "R OO (S \ T) = R OO S \ R OO T" by (fact relcomp_distrib [to_pred]) @@ -596,7 +593,7 @@ "(S \ T) O R = (S O R) \ (T O R)" by auto -lemma pred_comp_distrib2 [simp]: +lemma relcompp_distrib2 [simp]: "(S \ T) OO R = S OO R \ T OO R" by (fact relcomp_distrib2 [to_pred]) @@ -679,9 +676,9 @@ lemma converse_relcomp: "(r O s)^-1 = s^-1 O r^-1" by blast -lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1" - by (iprover intro: order_antisym conversepI pred_compI - elim: pred_compE dest: conversepD) +lemma converse_relcompp: "(r OO s)^--1 = s^--1 OO r^--1" + by (iprover intro: order_antisym conversepI relcomppI + elim: relcomppE dest: conversepD) lemma converse_Int: "(r \ s)^-1 = r^-1 \ s^-1" by blast