src/HOL/Quotient.thy
changeset 47308 9caab698dbe4
parent 47105 e64ffc96a49f
child 47361 87c0eaf04bad
child 47435 e1b761c216ac
     1.1 --- a/src/HOL/Quotient.thy	Tue Apr 03 14:09:37 2012 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Tue Apr 03 16:26:48 2012 +0200
     1.3 @@ -5,11 +5,10 @@
     1.4  header {* Definition of Quotient Types *}
     1.5  
     1.6  theory Quotient
     1.7 -imports Plain Hilbert_Choice Equiv_Relations
     1.8 +imports Plain Hilbert_Choice Equiv_Relations Lifting
     1.9  keywords
    1.10 -  "print_quotmaps" "print_quotients" "print_quotconsts" :: diag and
    1.11 +  "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and
    1.12    "quotient_type" :: thy_goal and "/" and
    1.13 -  "setup_lifting" :: thy_decl and
    1.14    "quotient_definition" :: thy_goal
    1.15  uses
    1.16    ("Tools/Quotient/quotient_info.ML")
    1.17 @@ -53,37 +52,6 @@
    1.18    shows "x \<in> Respects R \<longleftrightarrow> R x x"
    1.19    unfolding Respects_def by simp
    1.20  
    1.21 -subsection {* Function map and function relation *}
    1.22 -
    1.23 -notation map_fun (infixr "--->" 55)
    1.24 -
    1.25 -lemma map_fun_id:
    1.26 -  "(id ---> id) = id"
    1.27 -  by (simp add: fun_eq_iff)
    1.28 -
    1.29 -definition
    1.30 -  fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool" (infixr "===>" 55)
    1.31 -where
    1.32 -  "fun_rel R1 R2 = (\<lambda>f g. \<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
    1.33 -
    1.34 -lemma fun_relI [intro]:
    1.35 -  assumes "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
    1.36 -  shows "(R1 ===> R2) f g"
    1.37 -  using assms by (simp add: fun_rel_def)
    1.38 -
    1.39 -lemma fun_relE:
    1.40 -  assumes "(R1 ===> R2) f g" and "R1 x y"
    1.41 -  obtains "R2 (f x) (g y)"
    1.42 -  using assms by (simp add: fun_rel_def)
    1.43 -
    1.44 -lemma fun_rel_eq:
    1.45 -  shows "((op =) ===> (op =)) = (op =)"
    1.46 -  by (auto simp add: fun_eq_iff elim: fun_relE)
    1.47 -
    1.48 -lemma fun_rel_eq_rel:
    1.49 -  shows "((op =) ===> R) = (\<lambda>f g. \<forall>x. R (f x) (g x))"
    1.50 -  by (simp add: fun_rel_def)
    1.51 -
    1.52  subsection {* set map (vimage) and set relation *}
    1.53  
    1.54  definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
    1.55 @@ -106,155 +74,169 @@
    1.56  subsection {* Quotient Predicate *}
    1.57  
    1.58  definition
    1.59 -  "Quotient R Abs Rep \<longleftrightarrow>
    1.60 +  "Quotient3 R Abs Rep \<longleftrightarrow>
    1.61       (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. R (Rep a) (Rep a)) \<and>
    1.62       (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s)"
    1.63  
    1.64 -lemma QuotientI:
    1.65 +lemma Quotient3I:
    1.66    assumes "\<And>a. Abs (Rep a) = a"
    1.67      and "\<And>a. R (Rep a) (Rep a)"
    1.68      and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s"
    1.69 -  shows "Quotient R Abs Rep"
    1.70 -  using assms unfolding Quotient_def by blast
    1.71 +  shows "Quotient3 R Abs Rep"
    1.72 +  using assms unfolding Quotient3_def by blast
    1.73  
    1.74 -lemma Quotient_abs_rep:
    1.75 -  assumes a: "Quotient R Abs Rep"
    1.76 +lemma Quotient3_abs_rep:
    1.77 +  assumes a: "Quotient3 R Abs Rep"
    1.78    shows "Abs (Rep a) = a"
    1.79    using a
    1.80 -  unfolding Quotient_def
    1.81 +  unfolding Quotient3_def
    1.82    by simp
    1.83  
    1.84 -lemma Quotient_rep_reflp:
    1.85 -  assumes a: "Quotient R Abs Rep"
    1.86 +lemma Quotient3_rep_reflp:
    1.87 +  assumes a: "Quotient3 R Abs Rep"
    1.88    shows "R (Rep a) (Rep a)"
    1.89    using a
    1.90 -  unfolding Quotient_def
    1.91 +  unfolding Quotient3_def
    1.92    by blast
    1.93  
    1.94 -lemma Quotient_rel:
    1.95 -  assumes a: "Quotient R Abs Rep"
    1.96 +lemma Quotient3_rel:
    1.97 +  assumes a: "Quotient3 R Abs Rep"
    1.98    shows "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
    1.99    using a
   1.100 -  unfolding Quotient_def
   1.101 +  unfolding Quotient3_def
   1.102    by blast
   1.103  
   1.104 -lemma Quotient_refl1: 
   1.105 -  assumes a: "Quotient R Abs Rep" 
   1.106 +lemma Quotient3_refl1: 
   1.107 +  assumes a: "Quotient3 R Abs Rep" 
   1.108    shows "R r s \<Longrightarrow> R r r"
   1.109 -  using a unfolding Quotient_def 
   1.110 +  using a unfolding Quotient3_def 
   1.111    by fast
   1.112  
   1.113 -lemma Quotient_refl2: 
   1.114 -  assumes a: "Quotient R Abs Rep" 
   1.115 +lemma Quotient3_refl2: 
   1.116 +  assumes a: "Quotient3 R Abs Rep" 
   1.117    shows "R r s \<Longrightarrow> R s s"
   1.118 -  using a unfolding Quotient_def 
   1.119 +  using a unfolding Quotient3_def 
   1.120    by fast
   1.121  
   1.122 -lemma Quotient_rel_rep:
   1.123 -  assumes a: "Quotient R Abs Rep"
   1.124 +lemma Quotient3_rel_rep:
   1.125 +  assumes a: "Quotient3 R Abs Rep"
   1.126    shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
   1.127    using a
   1.128 -  unfolding Quotient_def
   1.129 +  unfolding Quotient3_def
   1.130    by metis
   1.131  
   1.132 -lemma Quotient_rep_abs:
   1.133 -  assumes a: "Quotient R Abs Rep"
   1.134 +lemma Quotient3_rep_abs:
   1.135 +  assumes a: "Quotient3 R Abs Rep"
   1.136    shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
   1.137 -  using a unfolding Quotient_def
   1.138 +  using a unfolding Quotient3_def
   1.139 +  by blast
   1.140 +
   1.141 +lemma Quotient3_rel_abs:
   1.142 +  assumes a: "Quotient3 R Abs Rep"
   1.143 +  shows "R r s \<Longrightarrow> Abs r = Abs s"
   1.144 +  using a unfolding Quotient3_def
   1.145    by blast
   1.146  
   1.147 -lemma Quotient_rel_abs:
   1.148 -  assumes a: "Quotient R Abs Rep"
   1.149 -  shows "R r s \<Longrightarrow> Abs r = Abs s"
   1.150 -  using a unfolding Quotient_def
   1.151 -  by blast
   1.152 -
   1.153 -lemma Quotient_symp:
   1.154 -  assumes a: "Quotient R Abs Rep"
   1.155 +lemma Quotient3_symp:
   1.156 +  assumes a: "Quotient3 R Abs Rep"
   1.157    shows "symp R"
   1.158 -  using a unfolding Quotient_def using sympI by metis
   1.159 +  using a unfolding Quotient3_def using sympI by metis
   1.160  
   1.161 -lemma Quotient_transp:
   1.162 -  assumes a: "Quotient R Abs Rep"
   1.163 +lemma Quotient3_transp:
   1.164 +  assumes a: "Quotient3 R Abs Rep"
   1.165    shows "transp R"
   1.166 -  using a unfolding Quotient_def using transpI by metis
   1.167 +  using a unfolding Quotient3_def using transpI by (metis (full_types))
   1.168  
   1.169 -lemma identity_quotient:
   1.170 -  shows "Quotient (op =) id id"
   1.171 -  unfolding Quotient_def id_def
   1.172 +lemma Quotient3_part_equivp:
   1.173 +  assumes a: "Quotient3 R Abs Rep"
   1.174 +  shows "part_equivp R"
   1.175 +by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp a part_equivpI)
   1.176 +
   1.177 +lemma identity_quotient3:
   1.178 +  shows "Quotient3 (op =) id id"
   1.179 +  unfolding Quotient3_def id_def
   1.180    by blast
   1.181  
   1.182 -lemma fun_quotient:
   1.183 -  assumes q1: "Quotient R1 abs1 rep1"
   1.184 -  and     q2: "Quotient R2 abs2 rep2"
   1.185 -  shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
   1.186 +lemma fun_quotient3:
   1.187 +  assumes q1: "Quotient3 R1 abs1 rep1"
   1.188 +  and     q2: "Quotient3 R2 abs2 rep2"
   1.189 +  shows "Quotient3 (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
   1.190  proof -
   1.191 -  have "\<And>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
   1.192 -    using q1 q2 by (simp add: Quotient_def fun_eq_iff)
   1.193 +  have "\<And>a.(rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
   1.194 +    using q1 q2 by (simp add: Quotient3_def fun_eq_iff)
   1.195    moreover
   1.196 -  have "\<And>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
   1.197 +  have "\<And>a.(R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
   1.198      by (rule fun_relI)
   1.199 -      (insert q1 q2 Quotient_rel_abs [of R1 abs1 rep1] Quotient_rel_rep [of R2 abs2 rep2],
   1.200 -        simp (no_asm) add: Quotient_def, simp)
   1.201 +      (insert q1 q2 Quotient3_rel_abs [of R1 abs1 rep1] Quotient3_rel_rep [of R2 abs2 rep2],
   1.202 +        simp (no_asm) add: Quotient3_def, simp)
   1.203 +  
   1.204    moreover
   1.205 -  have "\<And>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
   1.206 +  {
   1.207 +  fix r s
   1.208 +  have "(R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
   1.209          (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"
   1.210 -    apply(auto simp add: fun_rel_def fun_eq_iff)
   1.211 -    using q1 q2 unfolding Quotient_def
   1.212 -    apply(metis)
   1.213 -    using q1 q2 unfolding Quotient_def
   1.214 -    apply(metis)
   1.215 -    using q1 q2 unfolding Quotient_def
   1.216 -    apply(metis)
   1.217 -    using q1 q2 unfolding Quotient_def
   1.218 -    apply(metis)
   1.219 -    done
   1.220 -  ultimately
   1.221 -  show "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
   1.222 -    unfolding Quotient_def by blast
   1.223 +  proof -
   1.224 +    
   1.225 +    have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) r r" unfolding fun_rel_def
   1.226 +      using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] 
   1.227 +      by (metis (full_types) part_equivp_def)
   1.228 +    moreover have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) s s" unfolding fun_rel_def
   1.229 +      using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] 
   1.230 +      by (metis (full_types) part_equivp_def)
   1.231 +    moreover have "(R1 ===> R2) r s \<Longrightarrow> (rep1 ---> abs2) r  = (rep1 ---> abs2) s"
   1.232 +      apply(auto simp add: fun_rel_def fun_eq_iff) using q1 q2 unfolding Quotient3_def by metis
   1.233 +    moreover have "((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
   1.234 +        (rep1 ---> abs2) r  = (rep1 ---> abs2) s) \<Longrightarrow> (R1 ===> R2) r s"
   1.235 +      apply(auto simp add: fun_rel_def fun_eq_iff) using q1 q2 unfolding Quotient3_def 
   1.236 +    by (metis map_fun_apply)
   1.237 +  
   1.238 +    ultimately show ?thesis by blast
   1.239 + qed
   1.240 + }
   1.241 + ultimately show ?thesis by (intro Quotient3I) (assumption+)
   1.242  qed
   1.243  
   1.244  lemma abs_o_rep:
   1.245 -  assumes a: "Quotient R Abs Rep"
   1.246 +  assumes a: "Quotient3 R Abs Rep"
   1.247    shows "Abs o Rep = id"
   1.248    unfolding fun_eq_iff
   1.249 -  by (simp add: Quotient_abs_rep[OF a])
   1.250 +  by (simp add: Quotient3_abs_rep[OF a])
   1.251  
   1.252  lemma equals_rsp:
   1.253 -  assumes q: "Quotient R Abs Rep"
   1.254 +  assumes q: "Quotient3 R Abs Rep"
   1.255    and     a: "R xa xb" "R ya yb"
   1.256    shows "R xa ya = R xb yb"
   1.257 -  using a Quotient_symp[OF q] Quotient_transp[OF q]
   1.258 +  using a Quotient3_symp[OF q] Quotient3_transp[OF q]
   1.259    by (blast elim: sympE transpE)
   1.260  
   1.261  lemma lambda_prs:
   1.262 -  assumes q1: "Quotient R1 Abs1 Rep1"
   1.263 -  and     q2: "Quotient R2 Abs2 Rep2"
   1.264 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
   1.265 +  and     q2: "Quotient3 R2 Abs2 Rep2"
   1.266    shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
   1.267    unfolding fun_eq_iff
   1.268 -  using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
   1.269 +  using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
   1.270    by simp
   1.271  
   1.272  lemma lambda_prs1:
   1.273 -  assumes q1: "Quotient R1 Abs1 Rep1"
   1.274 -  and     q2: "Quotient R2 Abs2 Rep2"
   1.275 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
   1.276 +  and     q2: "Quotient3 R2 Abs2 Rep2"
   1.277    shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
   1.278    unfolding fun_eq_iff
   1.279 -  using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
   1.280 +  using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
   1.281    by simp
   1.282  
   1.283  lemma rep_abs_rsp:
   1.284 -  assumes q: "Quotient R Abs Rep"
   1.285 +  assumes q: "Quotient3 R Abs Rep"
   1.286    and     a: "R x1 x2"
   1.287    shows "R x1 (Rep (Abs x2))"
   1.288 -  using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]
   1.289 +  using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q]
   1.290    by metis
   1.291  
   1.292  lemma rep_abs_rsp_left:
   1.293 -  assumes q: "Quotient R Abs Rep"
   1.294 +  assumes q: "Quotient3 R Abs Rep"
   1.295    and     a: "R x1 x2"
   1.296    shows "R (Rep (Abs x1)) x2"
   1.297 -  using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]
   1.298 +  using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q]
   1.299    by metis
   1.300  
   1.301  text{*
   1.302 @@ -264,24 +246,19 @@
   1.303    will be provable; which is why we need to use @{text apply_rsp} and
   1.304    not the primed version *}
   1.305  
   1.306 -lemma apply_rsp:
   1.307 +lemma apply_rspQ3:
   1.308    fixes f g::"'a \<Rightarrow> 'c"
   1.309 -  assumes q: "Quotient R1 Abs1 Rep1"
   1.310 +  assumes q: "Quotient3 R1 Abs1 Rep1"
   1.311    and     a: "(R1 ===> R2) f g" "R1 x y"
   1.312    shows "R2 (f x) (g y)"
   1.313    using a by (auto elim: fun_relE)
   1.314  
   1.315 -lemma apply_rsp':
   1.316 -  assumes a: "(R1 ===> R2) f g" "R1 x y"
   1.317 -  shows "R2 (f x) (g y)"
   1.318 -  using a by (auto elim: fun_relE)
   1.319 -
   1.320 -lemma apply_rsp'':
   1.321 -  assumes "Quotient R Abs Rep"
   1.322 +lemma apply_rspQ3'':
   1.323 +  assumes "Quotient3 R Abs Rep"
   1.324    and "(R ===> S) f f"
   1.325    shows "S (f (Rep x)) (f (Rep x))"
   1.326  proof -
   1.327 -  from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp)
   1.328 +  from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient3_rep_reflp)
   1.329    then show ?thesis using assms(2) by (auto intro: apply_rsp')
   1.330  qed
   1.331  
   1.332 @@ -393,29 +370,29 @@
   1.333    "x \<in> p \<Longrightarrow> Babs p m x = m x"
   1.334  
   1.335  lemma babs_rsp:
   1.336 -  assumes q: "Quotient R1 Abs1 Rep1"
   1.337 +  assumes q: "Quotient3 R1 Abs1 Rep1"
   1.338    and     a: "(R1 ===> R2) f g"
   1.339    shows      "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
   1.340    apply (auto simp add: Babs_def in_respects fun_rel_def)
   1.341    apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
   1.342    using a apply (simp add: Babs_def fun_rel_def)
   1.343    apply (simp add: in_respects fun_rel_def)
   1.344 -  using Quotient_rel[OF q]
   1.345 +  using Quotient3_rel[OF q]
   1.346    by metis
   1.347  
   1.348  lemma babs_prs:
   1.349 -  assumes q1: "Quotient R1 Abs1 Rep1"
   1.350 -  and     q2: "Quotient R2 Abs2 Rep2"
   1.351 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
   1.352 +  and     q2: "Quotient3 R2 Abs2 Rep2"
   1.353    shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f"
   1.354    apply (rule ext)
   1.355    apply (simp add:)
   1.356    apply (subgoal_tac "Rep1 x \<in> Respects R1")
   1.357 -  apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
   1.358 -  apply (simp add: in_respects Quotient_rel_rep[OF q1])
   1.359 +  apply (simp add: Babs_def Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
   1.360 +  apply (simp add: in_respects Quotient3_rel_rep[OF q1])
   1.361    done
   1.362  
   1.363  lemma babs_simp:
   1.364 -  assumes q: "Quotient R1 Abs Rep"
   1.365 +  assumes q: "Quotient3 R1 Abs Rep"
   1.366    shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)"
   1.367    apply(rule iffI)
   1.368    apply(simp_all only: babs_rsp[OF q])
   1.369 @@ -423,7 +400,7 @@
   1.370    apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
   1.371    apply(metis Babs_def)
   1.372    apply (simp add: in_respects)
   1.373 -  using Quotient_rel[OF q]
   1.374 +  using Quotient3_rel[OF q]
   1.375    by metis
   1.376  
   1.377  (* If a user proves that a particular functional relation
   1.378 @@ -451,15 +428,15 @@
   1.379  
   1.380  (* 2 lemmas needed for cleaning of quantifiers *)
   1.381  lemma all_prs:
   1.382 -  assumes a: "Quotient R absf repf"
   1.383 +  assumes a: "Quotient3 R absf repf"
   1.384    shows "Ball (Respects R) ((absf ---> id) f) = All f"
   1.385 -  using a unfolding Quotient_def Ball_def in_respects id_apply comp_def map_fun_def
   1.386 +  using a unfolding Quotient3_def Ball_def in_respects id_apply comp_def map_fun_def
   1.387    by metis
   1.388  
   1.389  lemma ex_prs:
   1.390 -  assumes a: "Quotient R absf repf"
   1.391 +  assumes a: "Quotient3 R absf repf"
   1.392    shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
   1.393 -  using a unfolding Quotient_def Bex_def in_respects id_apply comp_def map_fun_def
   1.394 +  using a unfolding Quotient3_def Bex_def in_respects id_apply comp_def map_fun_def
   1.395    by metis
   1.396  
   1.397  subsection {* @{text Bex1_rel} quantifier *}
   1.398 @@ -508,7 +485,7 @@
   1.399    done
   1.400  
   1.401  lemma bex1_rel_rsp:
   1.402 -  assumes a: "Quotient R absf repf"
   1.403 +  assumes a: "Quotient3 R absf repf"
   1.404    shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)"
   1.405    apply (simp add: fun_rel_def)
   1.406    apply clarify
   1.407 @@ -520,7 +497,7 @@
   1.408  
   1.409  
   1.410  lemma ex1_prs:
   1.411 -  assumes a: "Quotient R absf repf"
   1.412 +  assumes a: "Quotient3 R absf repf"
   1.413    shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f"
   1.414  apply (simp add:)
   1.415  apply (subst Bex1_rel_def)
   1.416 @@ -535,7 +512,7 @@
   1.417    apply (rule_tac x="absf x" in exI)
   1.418    apply (simp)
   1.419    apply rule+
   1.420 -  using a unfolding Quotient_def
   1.421 +  using a unfolding Quotient3_def
   1.422    apply metis
   1.423   apply rule+
   1.424   apply (erule_tac x="x" in ballE)
   1.425 @@ -548,10 +525,10 @@
   1.426   apply (rule_tac x="repf x" in exI)
   1.427   apply (simp only: in_respects)
   1.428    apply rule
   1.429 - apply (metis Quotient_rel_rep[OF a])
   1.430 -using a unfolding Quotient_def apply (simp)
   1.431 + apply (metis Quotient3_rel_rep[OF a])
   1.432 +using a unfolding Quotient3_def apply (simp)
   1.433  apply rule+
   1.434 -using a unfolding Quotient_def in_respects
   1.435 +using a unfolding Quotient3_def in_respects
   1.436  apply metis
   1.437  done
   1.438  
   1.439 @@ -587,7 +564,7 @@
   1.440  subsection {* Various respects and preserve lemmas *}
   1.441  
   1.442  lemma quot_rel_rsp:
   1.443 -  assumes a: "Quotient R Abs Rep"
   1.444 +  assumes a: "Quotient3 R Abs Rep"
   1.445    shows "(R ===> R ===> op =) R R"
   1.446    apply(rule fun_relI)+
   1.447    apply(rule equals_rsp[OF a])
   1.448 @@ -595,12 +572,12 @@
   1.449    done
   1.450  
   1.451  lemma o_prs:
   1.452 -  assumes q1: "Quotient R1 Abs1 Rep1"
   1.453 -  and     q2: "Quotient R2 Abs2 Rep2"
   1.454 -  and     q3: "Quotient R3 Abs3 Rep3"
   1.455 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
   1.456 +  and     q2: "Quotient3 R2 Abs2 Rep2"
   1.457 +  and     q3: "Quotient3 R3 Abs3 Rep3"
   1.458    shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) op \<circ> = op \<circ>"
   1.459    and   "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) op \<circ> = op \<circ>"
   1.460 -  using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]
   1.461 +  using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] Quotient3_abs_rep[OF q3]
   1.462    by (simp_all add: fun_eq_iff)
   1.463  
   1.464  lemma o_rsp:
   1.465 @@ -609,26 +586,26 @@
   1.466    by (force elim: fun_relE)+
   1.467  
   1.468  lemma cond_prs:
   1.469 -  assumes a: "Quotient R absf repf"
   1.470 +  assumes a: "Quotient3 R absf repf"
   1.471    shows "absf (if a then repf b else repf c) = (if a then b else c)"
   1.472 -  using a unfolding Quotient_def by auto
   1.473 +  using a unfolding Quotient3_def by auto
   1.474  
   1.475  lemma if_prs:
   1.476 -  assumes q: "Quotient R Abs Rep"
   1.477 +  assumes q: "Quotient3 R Abs Rep"
   1.478    shows "(id ---> Rep ---> Rep ---> Abs) If = If"
   1.479 -  using Quotient_abs_rep[OF q]
   1.480 +  using Quotient3_abs_rep[OF q]
   1.481    by (auto simp add: fun_eq_iff)
   1.482  
   1.483  lemma if_rsp:
   1.484 -  assumes q: "Quotient R Abs Rep"
   1.485 +  assumes q: "Quotient3 R Abs Rep"
   1.486    shows "(op = ===> R ===> R ===> R) If If"
   1.487    by force
   1.488  
   1.489  lemma let_prs:
   1.490 -  assumes q1: "Quotient R1 Abs1 Rep1"
   1.491 -  and     q2: "Quotient R2 Abs2 Rep2"
   1.492 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
   1.493 +  and     q2: "Quotient3 R2 Abs2 Rep2"
   1.494    shows "(Rep2 ---> (Abs2 ---> Rep1) ---> Abs1) Let = Let"
   1.495 -  using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
   1.496 +  using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
   1.497    by (auto simp add: fun_eq_iff)
   1.498  
   1.499  lemma let_rsp:
   1.500 @@ -640,9 +617,9 @@
   1.501    by auto
   1.502  
   1.503  lemma id_prs:
   1.504 -  assumes a: "Quotient R Abs Rep"
   1.505 +  assumes a: "Quotient3 R Abs Rep"
   1.506    shows "(Rep ---> Abs) id = id"
   1.507 -  by (simp add: fun_eq_iff Quotient_abs_rep [OF a])
   1.508 +  by (simp add: fun_eq_iff Quotient3_abs_rep [OF a])
   1.509  
   1.510  
   1.511  locale quot_type =
   1.512 @@ -673,8 +650,8 @@
   1.513    by (metis assms exE_some equivp[simplified part_equivp_def])
   1.514  
   1.515  lemma Quotient:
   1.516 -  shows "Quotient R abs rep"
   1.517 -  unfolding Quotient_def abs_def rep_def
   1.518 +  shows "Quotient3 R abs rep"
   1.519 +  unfolding Quotient3_def abs_def rep_def
   1.520    proof (intro conjI allI)
   1.521      fix a r s
   1.522      show x: "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)" proof -
   1.523 @@ -703,149 +680,114 @@
   1.524  
   1.525  subsection {* Quotient composition *}
   1.526  
   1.527 -lemma OOO_quotient:
   1.528 +lemma OOO_quotient3:
   1.529    fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   1.530    fixes Abs1 :: "'a \<Rightarrow> 'b" and Rep1 :: "'b \<Rightarrow> 'a"
   1.531    fixes Abs2 :: "'b \<Rightarrow> 'c" and Rep2 :: "'c \<Rightarrow> 'b"
   1.532    fixes R2' :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   1.533    fixes R2 :: "'b \<Rightarrow> 'b \<Rightarrow> bool"
   1.534 -  assumes R1: "Quotient R1 Abs1 Rep1"
   1.535 -  assumes R2: "Quotient R2 Abs2 Rep2"
   1.536 +  assumes R1: "Quotient3 R1 Abs1 Rep1"
   1.537 +  assumes R2: "Quotient3 R2 Abs2 Rep2"
   1.538    assumes Abs1: "\<And>x y. R2' x y \<Longrightarrow> R1 x x \<Longrightarrow> R1 y y \<Longrightarrow> R2 (Abs1 x) (Abs1 y)"
   1.539    assumes Rep1: "\<And>x y. R2 x y \<Longrightarrow> R2' (Rep1 x) (Rep1 y)"
   1.540 -  shows "Quotient (R1 OO R2' OO R1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
   1.541 -apply (rule QuotientI)
   1.542 -   apply (simp add: o_def Quotient_abs_rep [OF R2] Quotient_abs_rep [OF R1])
   1.543 +  shows "Quotient3 (R1 OO R2' OO R1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
   1.544 +apply (rule Quotient3I)
   1.545 +   apply (simp add: o_def Quotient3_abs_rep [OF R2] Quotient3_abs_rep [OF R1])
   1.546    apply simp
   1.547    apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI)
   1.548 -   apply (rule Quotient_rep_reflp [OF R1])
   1.549 +   apply (rule Quotient3_rep_reflp [OF R1])
   1.550    apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI [rotated])
   1.551 -   apply (rule Quotient_rep_reflp [OF R1])
   1.552 +   apply (rule Quotient3_rep_reflp [OF R1])
   1.553    apply (rule Rep1)
   1.554 -  apply (rule Quotient_rep_reflp [OF R2])
   1.555 +  apply (rule Quotient3_rep_reflp [OF R2])
   1.556   apply safe
   1.557      apply (rename_tac x y)
   1.558      apply (drule Abs1)
   1.559 -      apply (erule Quotient_refl2 [OF R1])
   1.560 -     apply (erule Quotient_refl1 [OF R1])
   1.561 -    apply (drule Quotient_refl1 [OF R2], drule Rep1)
   1.562 +      apply (erule Quotient3_refl2 [OF R1])
   1.563 +     apply (erule Quotient3_refl1 [OF R1])
   1.564 +    apply (drule Quotient3_refl1 [OF R2], drule Rep1)
   1.565      apply (subgoal_tac "R1 r (Rep1 (Abs1 x))")
   1.566       apply (rule_tac b="Rep1 (Abs1 x)" in pred_compI, assumption)
   1.567       apply (erule pred_compI)
   1.568 -     apply (erule Quotient_symp [OF R1, THEN sympD])
   1.569 -    apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
   1.570 -    apply (rule conjI, erule Quotient_refl1 [OF R1])
   1.571 -    apply (rule conjI, rule Quotient_rep_reflp [OF R1])
   1.572 -    apply (subst Quotient_abs_rep [OF R1])
   1.573 -    apply (erule Quotient_rel_abs [OF R1])
   1.574 +     apply (erule Quotient3_symp [OF R1, THEN sympD])
   1.575 +    apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
   1.576 +    apply (rule conjI, erule Quotient3_refl1 [OF R1])
   1.577 +    apply (rule conjI, rule Quotient3_rep_reflp [OF R1])
   1.578 +    apply (subst Quotient3_abs_rep [OF R1])
   1.579 +    apply (erule Quotient3_rel_abs [OF R1])
   1.580     apply (rename_tac x y)
   1.581     apply (drule Abs1)
   1.582 -     apply (erule Quotient_refl2 [OF R1])
   1.583 -    apply (erule Quotient_refl1 [OF R1])
   1.584 -   apply (drule Quotient_refl2 [OF R2], drule Rep1)
   1.585 +     apply (erule Quotient3_refl2 [OF R1])
   1.586 +    apply (erule Quotient3_refl1 [OF R1])
   1.587 +   apply (drule Quotient3_refl2 [OF R2], drule Rep1)
   1.588     apply (subgoal_tac "R1 s (Rep1 (Abs1 y))")
   1.589      apply (rule_tac b="Rep1 (Abs1 y)" in pred_compI, assumption)
   1.590      apply (erule pred_compI)
   1.591 -    apply (erule Quotient_symp [OF R1, THEN sympD])
   1.592 -   apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
   1.593 -   apply (rule conjI, erule Quotient_refl2 [OF R1])
   1.594 -   apply (rule conjI, rule Quotient_rep_reflp [OF R1])
   1.595 -   apply (subst Quotient_abs_rep [OF R1])
   1.596 -   apply (erule Quotient_rel_abs [OF R1, THEN sym])
   1.597 +    apply (erule Quotient3_symp [OF R1, THEN sympD])
   1.598 +   apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
   1.599 +   apply (rule conjI, erule Quotient3_refl2 [OF R1])
   1.600 +   apply (rule conjI, rule Quotient3_rep_reflp [OF R1])
   1.601 +   apply (subst Quotient3_abs_rep [OF R1])
   1.602 +   apply (erule Quotient3_rel_abs [OF R1, THEN sym])
   1.603    apply simp
   1.604 -  apply (rule Quotient_rel_abs [OF R2])
   1.605 -  apply (rule Quotient_rel_abs [OF R1, THEN ssubst], assumption)
   1.606 -  apply (rule Quotient_rel_abs [OF R1, THEN subst], assumption)
   1.607 +  apply (rule Quotient3_rel_abs [OF R2])
   1.608 +  apply (rule Quotient3_rel_abs [OF R1, THEN ssubst], assumption)
   1.609 +  apply (rule Quotient3_rel_abs [OF R1, THEN subst], assumption)
   1.610    apply (erule Abs1)
   1.611 -   apply (erule Quotient_refl2 [OF R1])
   1.612 -  apply (erule Quotient_refl1 [OF R1])
   1.613 +   apply (erule Quotient3_refl2 [OF R1])
   1.614 +  apply (erule Quotient3_refl1 [OF R1])
   1.615   apply (rename_tac a b c d)
   1.616   apply simp
   1.617   apply (rule_tac b="Rep1 (Abs1 r)" in pred_compI)
   1.618 -  apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
   1.619 -  apply (rule conjI, erule Quotient_refl1 [OF R1])
   1.620 -  apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
   1.621 +  apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
   1.622 +  apply (rule conjI, erule Quotient3_refl1 [OF R1])
   1.623 +  apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1])
   1.624   apply (rule_tac b="Rep1 (Abs1 s)" in pred_compI [rotated])
   1.625 -  apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
   1.626 -  apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
   1.627 -  apply (erule Quotient_refl2 [OF R1])
   1.628 +  apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
   1.629 +  apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1])
   1.630 +  apply (erule Quotient3_refl2 [OF R1])
   1.631   apply (rule Rep1)
   1.632   apply (drule Abs1)
   1.633 -   apply (erule Quotient_refl2 [OF R1])
   1.634 -  apply (erule Quotient_refl1 [OF R1])
   1.635 +   apply (erule Quotient3_refl2 [OF R1])
   1.636 +  apply (erule Quotient3_refl1 [OF R1])
   1.637   apply (drule Abs1)
   1.638 -  apply (erule Quotient_refl2 [OF R1])
   1.639 - apply (erule Quotient_refl1 [OF R1])
   1.640 - apply (drule Quotient_rel_abs [OF R1])
   1.641 - apply (drule Quotient_rel_abs [OF R1])
   1.642 - apply (drule Quotient_rel_abs [OF R1])
   1.643 - apply (drule Quotient_rel_abs [OF R1])
   1.644 +  apply (erule Quotient3_refl2 [OF R1])
   1.645 + apply (erule Quotient3_refl1 [OF R1])
   1.646 + apply (drule Quotient3_rel_abs [OF R1])
   1.647 + apply (drule Quotient3_rel_abs [OF R1])
   1.648 + apply (drule Quotient3_rel_abs [OF R1])
   1.649 + apply (drule Quotient3_rel_abs [OF R1])
   1.650   apply simp
   1.651 - apply (rule Quotient_rel[symmetric, OF R2, THEN iffD2])
   1.652 + apply (rule Quotient3_rel[symmetric, OF R2, THEN iffD2])
   1.653   apply simp
   1.654  done
   1.655  
   1.656 -lemma OOO_eq_quotient:
   1.657 +lemma OOO_eq_quotient3:
   1.658    fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   1.659    fixes Abs1 :: "'a \<Rightarrow> 'b" and Rep1 :: "'b \<Rightarrow> 'a"
   1.660    fixes Abs2 :: "'b \<Rightarrow> 'c" and Rep2 :: "'c \<Rightarrow> 'b"
   1.661 -  assumes R1: "Quotient R1 Abs1 Rep1"
   1.662 -  assumes R2: "Quotient op= Abs2 Rep2"
   1.663 -  shows "Quotient (R1 OOO op=) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
   1.664 +  assumes R1: "Quotient3 R1 Abs1 Rep1"
   1.665 +  assumes R2: "Quotient3 op= Abs2 Rep2"
   1.666 +  shows "Quotient3 (R1 OOO op=) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
   1.667  using assms
   1.668 -by (rule OOO_quotient) auto
   1.669 +by (rule OOO_quotient3) auto
   1.670  
   1.671  subsection {* Invariant *}
   1.672  
   1.673 -definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
   1.674 -  where "invariant R = (\<lambda>x y. R x \<and> x = y)"
   1.675 -
   1.676 -lemma invariant_to_eq:
   1.677 -  assumes "invariant P x y"
   1.678 -  shows "x = y"
   1.679 -using assms by (simp add: invariant_def)
   1.680 -
   1.681 -lemma fun_rel_eq_invariant:
   1.682 -  shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
   1.683 -by (auto simp add: invariant_def fun_rel_def)
   1.684 -
   1.685 -lemma invariant_same_args:
   1.686 -  shows "invariant P x x \<equiv> P x"
   1.687 -using assms by (auto simp add: invariant_def)
   1.688 -
   1.689 -lemma copy_type_to_Quotient:
   1.690 +lemma copy_type_to_Quotient3:
   1.691    assumes "type_definition Rep Abs UNIV"
   1.692 -  shows "Quotient (op =) Abs Rep"
   1.693 +  shows "Quotient3 (op =) Abs Rep"
   1.694  proof -
   1.695    interpret type_definition Rep Abs UNIV by fact
   1.696 -  from Abs_inject Rep_inverse show ?thesis by (auto intro!: QuotientI)
   1.697 +  from Abs_inject Rep_inverse show ?thesis by (auto intro!: Quotient3I)
   1.698  qed
   1.699  
   1.700 -lemma copy_type_to_equivp:
   1.701 -  fixes Abs :: "'a \<Rightarrow> 'b"
   1.702 -  and Rep :: "'b \<Rightarrow> 'a"
   1.703 -  assumes "type_definition Rep Abs (UNIV::'a set)"
   1.704 -  shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)"
   1.705 -by (rule identity_equivp)
   1.706 -
   1.707 -lemma invariant_type_to_Quotient:
   1.708 +lemma invariant_type_to_Quotient3:
   1.709    assumes "type_definition Rep Abs {x. P x}"
   1.710 -  shows "Quotient (invariant P) Abs Rep"
   1.711 +  shows "Quotient3 (Lifting.invariant P) Abs Rep"
   1.712  proof -
   1.713    interpret type_definition Rep Abs "{x. P x}" by fact
   1.714 -  from Rep Abs_inject Rep_inverse show ?thesis by (auto intro!: QuotientI simp: invariant_def)
   1.715 -qed
   1.716 -
   1.717 -lemma invariant_type_to_part_equivp:
   1.718 -  assumes "type_definition Rep Abs {x. P x}"
   1.719 -  shows "part_equivp (invariant P)"
   1.720 -proof (intro part_equivpI)
   1.721 -  interpret type_definition Rep Abs "{x. P x}" by fact
   1.722 -  show "\<exists>x. invariant P x x" using Rep by (auto simp: invariant_def)
   1.723 -next
   1.724 -  show "symp (invariant P)" by (auto intro: sympI simp: invariant_def)
   1.725 -next
   1.726 -  show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
   1.727 +  from Rep Abs_inject Rep_inverse show ?thesis by (auto intro!: Quotient3I simp: invariant_def)
   1.728  qed
   1.729  
   1.730  subsection {* ML setup *}
   1.731 @@ -855,9 +797,9 @@
   1.732  use "Tools/Quotient/quotient_info.ML"
   1.733  setup Quotient_Info.setup
   1.734  
   1.735 -declare [[map "fun" = (fun_rel, fun_quotient)]]
   1.736 +declare [[mapQ3 "fun" = (fun_rel, fun_quotient3)]]
   1.737  
   1.738 -lemmas [quot_thm] = fun_quotient
   1.739 +lemmas [quot_thm] = fun_quotient3
   1.740  lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp
   1.741  lemmas [quot_preserve] = if_prs o_prs let_prs id_prs
   1.742  lemmas [quot_equiv] = identity_equivp
   1.743 @@ -960,6 +902,4 @@
   1.744    map_fun (infixr "--->" 55) and
   1.745    fun_rel (infixr "===>" 55)
   1.746  
   1.747 -hide_const (open) invariant
   1.748 -
   1.749  end