src/HOL/Quotient.thy
 changeset 54867 c21a2465cac1 parent 54555 e8c5e95d338b child 55945 e96383acecf9
```     1.1 --- a/src/HOL/Quotient.thy	Wed Dec 25 22:35:29 2013 +0100
1.2 +++ b/src/HOL/Quotient.thy	Thu Dec 26 22:47:49 2013 +0100
1.3 @@ -46,75 +46,94 @@
1.4    shows "Quotient3 R Abs Rep"
1.5    using assms unfolding Quotient3_def by blast
1.6
1.7 -lemma Quotient3_abs_rep:
1.8 +context
1.9 +  fixes R Abs Rep
1.10    assumes a: "Quotient3 R Abs Rep"
1.11 -  shows "Abs (Rep a) = a"
1.12 +begin
1.13 +
1.14 +lemma Quotient3_abs_rep:
1.15 +  "Abs (Rep a) = a"
1.16    using a
1.17    unfolding Quotient3_def
1.18    by simp
1.19
1.20  lemma Quotient3_rep_reflp:
1.21 -  assumes a: "Quotient3 R Abs Rep"
1.22 -  shows "R (Rep a) (Rep a)"
1.23 +  "R (Rep a) (Rep a)"
1.24    using a
1.25    unfolding Quotient3_def
1.26    by blast
1.27
1.28  lemma Quotient3_rel:
1.29 -  assumes a: "Quotient3 R Abs Rep"
1.30 -  shows "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
1.31 +  "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
1.32    using a
1.33    unfolding Quotient3_def
1.34    by blast
1.35
1.36  lemma Quotient3_refl1:
1.37 -  assumes a: "Quotient3 R Abs Rep"
1.38 -  shows "R r s \<Longrightarrow> R r r"
1.39 +  "R r s \<Longrightarrow> R r r"
1.40    using a unfolding Quotient3_def
1.41    by fast
1.42
1.43  lemma Quotient3_refl2:
1.44 -  assumes a: "Quotient3 R Abs Rep"
1.45 -  shows "R r s \<Longrightarrow> R s s"
1.46 +  "R r s \<Longrightarrow> R s s"
1.47    using a unfolding Quotient3_def
1.48    by fast
1.49
1.50  lemma Quotient3_rel_rep:
1.51 -  assumes a: "Quotient3 R Abs Rep"
1.52 -  shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
1.53 +  "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
1.54    using a
1.55    unfolding Quotient3_def
1.56    by metis
1.57
1.58  lemma Quotient3_rep_abs:
1.59 -  assumes a: "Quotient3 R Abs Rep"
1.60 -  shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
1.61 +  "R r r \<Longrightarrow> R (Rep (Abs r)) r"
1.62    using a unfolding Quotient3_def
1.63    by blast
1.64
1.65  lemma Quotient3_rel_abs:
1.66 -  assumes a: "Quotient3 R Abs Rep"
1.67 -  shows "R r s \<Longrightarrow> Abs r = Abs s"
1.68 +  "R r s \<Longrightarrow> Abs r = Abs s"
1.69    using a unfolding Quotient3_def
1.70    by blast
1.71
1.72  lemma Quotient3_symp:
1.73 -  assumes a: "Quotient3 R Abs Rep"
1.74 -  shows "symp R"
1.75 +  "symp R"
1.76    using a unfolding Quotient3_def using sympI by metis
1.77
1.78  lemma Quotient3_transp:
1.79 -  assumes a: "Quotient3 R Abs Rep"
1.80 -  shows "transp R"
1.81 +  "transp R"
1.82    using a unfolding Quotient3_def using transpI by (metis (full_types))
1.83
1.84  lemma Quotient3_part_equivp:
1.85 -  assumes a: "Quotient3 R Abs Rep"
1.86 -  shows "part_equivp R"
1.87 -by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp a part_equivpI)
1.88 +  "part_equivp R"
1.89 +  by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp part_equivpI)
1.90 +
1.91 +lemma abs_o_rep:
1.92 +  "Abs o Rep = id"
1.93 +  unfolding fun_eq_iff
1.94 +  by (simp add: Quotient3_abs_rep)
1.95 +
1.96 +lemma equals_rsp:
1.97 +  assumes b: "R xa xb" "R ya yb"
1.98 +  shows "R xa ya = R xb yb"
1.99 +  using b Quotient3_symp Quotient3_transp
1.100 +  by (blast elim: sympE transpE)
1.101 +
1.102 +lemma rep_abs_rsp:
1.103 +  assumes b: "R x1 x2"
1.104 +  shows "R x1 (Rep (Abs x2))"
1.105 +  using b Quotient3_rel Quotient3_abs_rep Quotient3_rep_reflp
1.106 +  by metis
1.107 +
1.108 +lemma rep_abs_rsp_left:
1.109 +  assumes b: "R x1 x2"
1.110 +  shows "R (Rep (Abs x1)) x2"
1.111 +  using b Quotient3_rel Quotient3_abs_rep Quotient3_rep_reflp
1.112 +  by metis
1.113 +
1.114 +end
1.115
1.116  lemma identity_quotient3:
1.117 -  shows "Quotient3 (op =) id id"
1.118 +  "Quotient3 (op =) id id"
1.119    unfolding Quotient3_def id_def
1.120    by blast
1.121
1.122 @@ -157,19 +176,6 @@
1.123   ultimately show ?thesis by (intro Quotient3I) (assumption+)
1.124  qed
1.125
1.126 -lemma abs_o_rep:
1.127 -  assumes a: "Quotient3 R Abs Rep"
1.128 -  shows "Abs o Rep = id"
1.129 -  unfolding fun_eq_iff
1.130 -  by (simp add: Quotient3_abs_rep[OF a])
1.131 -
1.132 -lemma equals_rsp:
1.133 -  assumes q: "Quotient3 R Abs Rep"
1.134 -  and     a: "R xa xb" "R ya yb"
1.135 -  shows "R xa ya = R xb yb"
1.136 -  using a Quotient3_symp[OF q] Quotient3_transp[OF q]
1.137 -  by (blast elim: sympE transpE)
1.138 -
1.139  lemma lambda_prs:
1.140    assumes q1: "Quotient3 R1 Abs1 Rep1"
1.141    and     q2: "Quotient3 R2 Abs2 Rep2"
1.142 @@ -186,20 +192,6 @@
1.143    using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
1.144    by simp
1.145
1.146 -lemma rep_abs_rsp:
1.147 -  assumes q: "Quotient3 R Abs Rep"
1.148 -  and     a: "R x1 x2"
1.149 -  shows "R x1 (Rep (Abs x2))"
1.150 -  using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q]
1.151 -  by metis
1.152 -
1.153 -lemma rep_abs_rsp_left:
1.154 -  assumes q: "Quotient3 R Abs Rep"
1.155 -  and     a: "R x1 x2"
1.156 -  shows "R (Rep (Abs x1)) x2"
1.157 -  using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q]
1.158 -  by metis
1.159 -
1.160  text{*
1.161    In the following theorem R1 can be instantiated with anything,
1.162    but we know some of the types of the Rep and Abs functions;
```