dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
authorgriff
Tue Apr 03 17:45:06 2012 +0900 (2012-04-03)
changeset 47434b75ce48a93ee
parent 47433 07f4bf913230
child 47435 e1b761c216ac
dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
src/HOL/Quotient.thy
src/HOL/Quotient_Examples/FSet.thy
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Quotient.thy	Tue Apr 03 17:26:30 2012 +0900
     1.2 +++ b/src/HOL/Quotient.thy	Tue Apr 03 17:45:06 2012 +0900
     1.3 @@ -717,9 +717,9 @@
     1.4  apply (rule QuotientI)
     1.5     apply (simp add: o_def Quotient_abs_rep [OF R2] Quotient_abs_rep [OF R1])
     1.6    apply simp
     1.7 -  apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI)
     1.8 +  apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI)
     1.9     apply (rule Quotient_rep_reflp [OF R1])
    1.10 -  apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI [rotated])
    1.11 +  apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI [rotated])
    1.12     apply (rule Quotient_rep_reflp [OF R1])
    1.13    apply (rule Rep1)
    1.14    apply (rule Quotient_rep_reflp [OF R2])
    1.15 @@ -730,8 +730,8 @@
    1.16       apply (erule Quotient_refl1 [OF R1])
    1.17      apply (drule Quotient_refl1 [OF R2], drule Rep1)
    1.18      apply (subgoal_tac "R1 r (Rep1 (Abs1 x))")
    1.19 -     apply (rule_tac b="Rep1 (Abs1 x)" in pred_compI, assumption)
    1.20 -     apply (erule pred_compI)
    1.21 +     apply (rule_tac b="Rep1 (Abs1 x)" in relcomppI, assumption)
    1.22 +     apply (erule relcomppI)
    1.23       apply (erule Quotient_symp [OF R1, THEN sympD])
    1.24      apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
    1.25      apply (rule conjI, erule Quotient_refl1 [OF R1])
    1.26 @@ -744,8 +744,8 @@
    1.27      apply (erule Quotient_refl1 [OF R1])
    1.28     apply (drule Quotient_refl2 [OF R2], drule Rep1)
    1.29     apply (subgoal_tac "R1 s (Rep1 (Abs1 y))")
    1.30 -    apply (rule_tac b="Rep1 (Abs1 y)" in pred_compI, assumption)
    1.31 -    apply (erule pred_compI)
    1.32 +    apply (rule_tac b="Rep1 (Abs1 y)" in relcomppI, assumption)
    1.33 +    apply (erule relcomppI)
    1.34      apply (erule Quotient_symp [OF R1, THEN sympD])
    1.35     apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
    1.36     apply (rule conjI, erule Quotient_refl2 [OF R1])
    1.37 @@ -761,11 +761,11 @@
    1.38    apply (erule Quotient_refl1 [OF R1])
    1.39   apply (rename_tac a b c d)
    1.40   apply simp
    1.41 - apply (rule_tac b="Rep1 (Abs1 r)" in pred_compI)
    1.42 + apply (rule_tac b="Rep1 (Abs1 r)" in relcomppI)
    1.43    apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
    1.44    apply (rule conjI, erule Quotient_refl1 [OF R1])
    1.45    apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
    1.46 - apply (rule_tac b="Rep1 (Abs1 s)" in pred_compI [rotated])
    1.47 + apply (rule_tac b="Rep1 (Abs1 s)" in relcomppI [rotated])
    1.48    apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
    1.49    apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
    1.50    apply (erule Quotient_refl2 [OF R1])
     2.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Tue Apr 03 17:26:30 2012 +0900
     2.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Tue Apr 03 17:45:06 2012 +0900
     2.3 @@ -140,7 +140,7 @@
     2.4    next
     2.5      assume a: "(list_all2 R OOO op \<approx>) r s"
     2.6      then have b: "map Abs r \<approx> map Abs s"
     2.7 -    proof (elim pred_compE)
     2.8 +    proof (elim relcomppE)
     2.9        fix b ba
    2.10        assume c: "list_all2 R r b"
    2.11        assume d: "b \<approx> ba"
    2.12 @@ -165,11 +165,11 @@
    2.13      have y: "list_all2 R (map Rep (map Abs s)) s"
    2.14        by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_all2_refl'[OF e, of s]])
    2.15      have c: "(op \<approx> OO list_all2 R) (map Rep (map Abs r)) s"
    2.16 -      by (rule pred_compI) (rule b, rule y)
    2.17 +      by (rule relcomppI) (rule b, rule y)
    2.18      have z: "list_all2 R r (map Rep (map Abs r))"
    2.19        by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_all2_refl'[OF e, of r]])
    2.20      then show "(list_all2 R OOO op \<approx>) r s"
    2.21 -      using a c pred_compI by simp
    2.22 +      using a c relcomppI by simp
    2.23    qed
    2.24  qed
    2.25  
    2.26 @@ -360,7 +360,7 @@
    2.27  quotient_definition
    2.28    "concat_fset :: ('a fset) fset \<Rightarrow> 'a fset"
    2.29    is concat 
    2.30 -proof (elim pred_compE)
    2.31 +proof (elim relcomppE)
    2.32  fix a b ba bb
    2.33    assume a: "list_all2 op \<approx> a ba"
    2.34    with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE)
    2.35 @@ -397,9 +397,9 @@
    2.36  lemma Cons_rsp2 [quot_respect]:
    2.37    shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
    2.38    apply (auto intro!: fun_relI)
    2.39 -  apply (rule_tac b="x # b" in pred_compI)
    2.40 +  apply (rule_tac b="x # b" in relcomppI)
    2.41    apply auto
    2.42 -  apply (rule_tac b="x # ba" in pred_compI)
    2.43 +  apply (rule_tac b="x # ba" in relcomppI)
    2.44    apply auto
    2.45    done
    2.46  
    2.47 @@ -453,7 +453,7 @@
    2.48    assumes "(R1 ===> R2 ===> R3) C C" and "(R4 ===> R5 ===> R6) C C"
    2.49    shows "(R1 OOO R4 ===> R2 OOO R5 ===> R3 OOO R6) C C"
    2.50    by (auto intro!: fun_relI)
    2.51 -     (metis (full_types) assms fun_relE pred_compI)
    2.52 +     (metis (full_types) assms fun_relE relcomppI)
    2.53  
    2.54  lemma append_rsp2 [quot_respect]:
    2.55    "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"
    2.56 @@ -479,7 +479,7 @@
    2.57      by (induct y ya rule: list_induct2')
    2.58         (simp_all, metis apply_rsp' list_eq_def)
    2.59    show "(list_all2 op \<approx> OOO op \<approx>) (map f xa) (map f' ya)"
    2.60 -    by (metis a b c list_eq_def pred_compI)
    2.61 +    by (metis a b c list_eq_def relcomppI)
    2.62  qed
    2.63  
    2.64  lemma map_prs2 [quot_preserve]:
     3.1 --- a/src/HOL/Relation.thy	Tue Apr 03 17:26:30 2012 +0900
     3.2 +++ b/src/HOL/Relation.thy	Tue Apr 03 17:45:06 2012 +0900
     3.3 @@ -512,10 +512,9 @@
     3.4  where
     3.5    relcompI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s"
     3.6  
     3.7 -abbreviation pred_comp (infixr "OO" 75) where
     3.8 -  "pred_comp \<equiv> relcompp"
     3.9 +notation relcompp (infixr "OO" 75)
    3.10  
    3.11 -lemmas pred_compI = relcompp.intros
    3.12 +lemmas relcomppI = relcompp.intros
    3.13  
    3.14  text {*
    3.15    For historic reasons, the elimination rules are not wholly corresponding.
    3.16 @@ -523,14 +522,12 @@
    3.17  *}
    3.18  
    3.19  inductive_cases relcompEpair: "(a, c) \<in> r O s"
    3.20 -inductive_cases pred_compE [elim!]: "(r OO s) a c"
    3.21 +inductive_cases relcomppE [elim!]: "(r OO s) a c"
    3.22  
    3.23  lemma relcompE [elim!]: "xz \<in> r O s \<Longrightarrow>
    3.24    (\<And>x y z. xz = (x, z) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> s  \<Longrightarrow> P) \<Longrightarrow> P"
    3.25    by (cases xz) (simp, erule relcompEpair, iprover)
    3.26  
    3.27 -lemmas pred_comp_relcomp_eq = relcompp_relcomp_eq
    3.28 -
    3.29  lemma R_O_Id [simp]:
    3.30    "R O Id = R"
    3.31    by fast
    3.32 @@ -543,7 +540,7 @@
    3.33    "{} O R = {}"
    3.34    by blast
    3.35  
    3.36 -lemma pred_comp_bot1 [simp]:
    3.37 +lemma relcompp_bot1 [simp]:
    3.38    "\<bottom> OO R = \<bottom>"
    3.39    by (fact relcomp_empty1 [to_pred])
    3.40  
    3.41 @@ -551,7 +548,7 @@
    3.42    "R O {} = {}"
    3.43    by blast
    3.44  
    3.45 -lemma pred_comp_bot2 [simp]:
    3.46 +lemma relcompp_bot2 [simp]:
    3.47    "R OO \<bottom> = \<bottom>"
    3.48    by (fact relcomp_empty2 [to_pred])
    3.49  
    3.50 @@ -560,7 +557,7 @@
    3.51    by blast
    3.52  
    3.53  
    3.54 -lemma pred_comp_assoc:
    3.55 +lemma relcompp_assoc:
    3.56    "(r OO s) OO t = r OO (s OO t)"
    3.57    by (fact O_assoc [to_pred])
    3.58  
    3.59 @@ -568,7 +565,7 @@
    3.60    "trans r \<Longrightarrow> r O r \<subseteq> r"
    3.61    by (unfold trans_def) blast
    3.62  
    3.63 -lemma transp_pred_comp_less_eq:
    3.64 +lemma transp_relcompp_less_eq:
    3.65    "transp r \<Longrightarrow> r OO r \<le> r "
    3.66    by (fact trans_O_subset [to_pred])
    3.67  
    3.68 @@ -576,7 +573,7 @@
    3.69    "r' \<subseteq> r \<Longrightarrow> s' \<subseteq> s \<Longrightarrow> r' O s' \<subseteq> r O s"
    3.70    by blast
    3.71  
    3.72 -lemma pred_comp_mono:
    3.73 +lemma relcompp_mono:
    3.74    "r' \<le> r \<Longrightarrow> s' \<le> s \<Longrightarrow> r' OO s' \<le> r OO s "
    3.75    by (fact relcomp_mono [to_pred])
    3.76  
    3.77 @@ -588,7 +585,7 @@
    3.78    "R O (S \<union> T) = (R O S) \<union> (R O T)" 
    3.79    by auto
    3.80  
    3.81 -lemma pred_comp_distrib [simp]:
    3.82 +lemma relcompp_distrib [simp]:
    3.83    "R OO (S \<squnion> T) = R OO S \<squnion> R OO T"
    3.84    by (fact relcomp_distrib [to_pred])
    3.85  
    3.86 @@ -596,7 +593,7 @@
    3.87    "(S \<union> T) O R = (S O R) \<union> (T O R)"
    3.88    by auto
    3.89  
    3.90 -lemma pred_comp_distrib2 [simp]:
    3.91 +lemma relcompp_distrib2 [simp]:
    3.92    "(S \<squnion> T) OO R = S OO R \<squnion> T OO R"
    3.93    by (fact relcomp_distrib2 [to_pred])
    3.94  
    3.95 @@ -679,9 +676,9 @@
    3.96  lemma converse_relcomp: "(r O s)^-1 = s^-1 O r^-1"
    3.97    by blast
    3.98  
    3.99 -lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
   3.100 -  by (iprover intro: order_antisym conversepI pred_compI
   3.101 -    elim: pred_compE dest: conversepD)
   3.102 +lemma converse_relcompp: "(r OO s)^--1 = s^--1 OO r^--1"
   3.103 +  by (iprover intro: order_antisym conversepI relcomppI
   3.104 +    elim: relcomppE dest: conversepD)
   3.105  
   3.106  lemma converse_Int: "(r \<inter> s)^-1 = r^-1 \<inter> s^-1"
   3.107    by blast