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;