src/HOL/Quotient_Examples/FSet.thy
changeset 47434 b75ce48a93ee
parent 47198 cfd8ff62eab1
child 47435 e1b761c216ac
     1.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Tue Apr 03 17:26:30 2012 +0900
     1.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Tue Apr 03 17:45:06 2012 +0900
     1.3 @@ -140,7 +140,7 @@
     1.4    next
     1.5      assume a: "(list_all2 R OOO op \<approx>) r s"
     1.6      then have b: "map Abs r \<approx> map Abs s"
     1.7 -    proof (elim pred_compE)
     1.8 +    proof (elim relcomppE)
     1.9        fix b ba
    1.10        assume c: "list_all2 R r b"
    1.11        assume d: "b \<approx> ba"
    1.12 @@ -165,11 +165,11 @@
    1.13      have y: "list_all2 R (map Rep (map Abs s)) s"
    1.14        by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_all2_refl'[OF e, of s]])
    1.15      have c: "(op \<approx> OO list_all2 R) (map Rep (map Abs r)) s"
    1.16 -      by (rule pred_compI) (rule b, rule y)
    1.17 +      by (rule relcomppI) (rule b, rule y)
    1.18      have z: "list_all2 R r (map Rep (map Abs r))"
    1.19        by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_all2_refl'[OF e, of r]])
    1.20      then show "(list_all2 R OOO op \<approx>) r s"
    1.21 -      using a c pred_compI by simp
    1.22 +      using a c relcomppI by simp
    1.23    qed
    1.24  qed
    1.25  
    1.26 @@ -360,7 +360,7 @@
    1.27  quotient_definition
    1.28    "concat_fset :: ('a fset) fset \<Rightarrow> 'a fset"
    1.29    is concat 
    1.30 -proof (elim pred_compE)
    1.31 +proof (elim relcomppE)
    1.32  fix a b ba bb
    1.33    assume a: "list_all2 op \<approx> a ba"
    1.34    with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE)
    1.35 @@ -397,9 +397,9 @@
    1.36  lemma Cons_rsp2 [quot_respect]:
    1.37    shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
    1.38    apply (auto intro!: fun_relI)
    1.39 -  apply (rule_tac b="x # b" in pred_compI)
    1.40 +  apply (rule_tac b="x # b" in relcomppI)
    1.41    apply auto
    1.42 -  apply (rule_tac b="x # ba" in pred_compI)
    1.43 +  apply (rule_tac b="x # ba" in relcomppI)
    1.44    apply auto
    1.45    done
    1.46  
    1.47 @@ -453,7 +453,7 @@
    1.48    assumes "(R1 ===> R2 ===> R3) C C" and "(R4 ===> R5 ===> R6) C C"
    1.49    shows "(R1 OOO R4 ===> R2 OOO R5 ===> R3 OOO R6) C C"
    1.50    by (auto intro!: fun_relI)
    1.51 -     (metis (full_types) assms fun_relE pred_compI)
    1.52 +     (metis (full_types) assms fun_relE relcomppI)
    1.53  
    1.54  lemma append_rsp2 [quot_respect]:
    1.55    "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"
    1.56 @@ -479,7 +479,7 @@
    1.57      by (induct y ya rule: list_induct2')
    1.58         (simp_all, metis apply_rsp' list_eq_def)
    1.59    show "(list_all2 op \<approx> OOO op \<approx>) (map f xa) (map f' ya)"
    1.60 -    by (metis a b c list_eq_def pred_compI)
    1.61 +    by (metis a b c list_eq_def relcomppI)
    1.62  qed
    1.63  
    1.64  lemma map_prs2 [quot_preserve]: