1(* Title: HOL/Quotient.thy 2 Author: Cezary Kaliszyk and Christian Urban 3*) 4 5section \<open>Definition of Quotient Types\<close> 6 7theory Quotient 8imports Lifting 9keywords 10 "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and 11 "quotient_type" :: thy_goal and "/" and 12 "quotient_definition" :: thy_goal 13begin 14 15text \<open> 16 Basic definition for equivalence relations 17 that are represented by predicates. 18\<close> 19 20text \<open>Composition of Relations\<close> 21 22abbreviation 23 rel_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" (infixr "OOO" 75) 24where 25 "r1 OOO r2 \<equiv> r1 OO r2 OO r1" 26 27lemma eq_comp_r: 28 shows "((=) OOO R) = R" 29 by (auto simp add: fun_eq_iff) 30 31context includes lifting_syntax 32begin 33 34subsection \<open>Quotient Predicate\<close> 35 36definition 37 "Quotient3 R Abs Rep \<longleftrightarrow> 38 (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. R (Rep a) (Rep a)) \<and> 39 (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s)" 40 41lemma Quotient3I: 42 assumes "\<And>a. Abs (Rep a) = a" 43 and "\<And>a. R (Rep a) (Rep a)" 44 and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s" 45 shows "Quotient3 R Abs Rep" 46 using assms unfolding Quotient3_def by blast 47 48context 49 fixes R Abs Rep 50 assumes a: "Quotient3 R Abs Rep" 51begin 52 53lemma Quotient3_abs_rep: 54 "Abs (Rep a) = a" 55 using a 56 unfolding Quotient3_def 57 by simp 58 59lemma Quotient3_rep_reflp: 60 "R (Rep a) (Rep a)" 61 using a 62 unfolding Quotient3_def 63 by blast 64 65lemma Quotient3_rel: 66 "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" \<comment> \<open>orientation does not loop on rewriting\<close> 67 using a 68 unfolding Quotient3_def 69 by blast 70 71lemma Quotient3_refl1: 72 "R r s \<Longrightarrow> R r r" 73 using a unfolding Quotient3_def 74 by fast 75 76lemma Quotient3_refl2: 77 "R r s \<Longrightarrow> R s s" 78 using a unfolding Quotient3_def 79 by fast 80 81lemma Quotient3_rel_rep: 82 "R (Rep a) (Rep b) \<longleftrightarrow> a = b" 83 using a 84 unfolding Quotient3_def 85 by metis 86 87lemma Quotient3_rep_abs: 88 "R r r \<Longrightarrow> R (Rep (Abs r)) r" 89 using a unfolding Quotient3_def 90 by blast 91 92lemma Quotient3_rel_abs: 93 "R r s \<Longrightarrow> Abs r = Abs s" 94 using a unfolding Quotient3_def 95 by blast 96 97lemma Quotient3_symp: 98 "symp R" 99 using a unfolding Quotient3_def using sympI by metis 100 101lemma Quotient3_transp: 102 "transp R" 103 using a unfolding Quotient3_def using transpI by (metis (full_types)) 104 105lemma Quotient3_part_equivp: 106 "part_equivp R" 107 by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp part_equivpI) 108 109lemma abs_o_rep: 110 "Abs \<circ> Rep = id" 111 unfolding fun_eq_iff 112 by (simp add: Quotient3_abs_rep) 113 114lemma equals_rsp: 115 assumes b: "R xa xb" "R ya yb" 116 shows "R xa ya = R xb yb" 117 using b Quotient3_symp Quotient3_transp 118 by (blast elim: sympE transpE) 119 120lemma rep_abs_rsp: 121 assumes b: "R x1 x2" 122 shows "R x1 (Rep (Abs x2))" 123 using b Quotient3_rel Quotient3_abs_rep Quotient3_rep_reflp 124 by metis 125 126lemma rep_abs_rsp_left: 127 assumes b: "R x1 x2" 128 shows "R (Rep (Abs x1)) x2" 129 using b Quotient3_rel Quotient3_abs_rep Quotient3_rep_reflp 130 by metis 131 132end 133 134lemma identity_quotient3: 135 "Quotient3 (=) id id" 136 unfolding Quotient3_def id_def 137 by blast 138 139lemma fun_quotient3: 140 assumes q1: "Quotient3 R1 abs1 rep1" 141 and q2: "Quotient3 R2 abs2 rep2" 142 shows "Quotient3 (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" 143proof - 144 have "\<And>a.(rep1 ---> abs2) ((abs1 ---> rep2) a) = a" 145 using q1 q2 by (simp add: Quotient3_def fun_eq_iff) 146 moreover 147 have "\<And>a.(R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" 148 by (rule rel_funI) 149 (insert q1 q2 Quotient3_rel_abs [of R1 abs1 rep1] Quotient3_rel_rep [of R2 abs2 rep2], 150 simp (no_asm) add: Quotient3_def, simp) 151 152 moreover 153 { 154 fix r s 155 have "(R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and> 156 (rep1 ---> abs2) r = (rep1 ---> abs2) s)" 157 proof - 158 159 have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) r r" unfolding rel_fun_def 160 using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] 161 by (metis (full_types) part_equivp_def) 162 moreover have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) s s" unfolding rel_fun_def 163 using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] 164 by (metis (full_types) part_equivp_def) 165 moreover have "(R1 ===> R2) r s \<Longrightarrow> (rep1 ---> abs2) r = (rep1 ---> abs2) s" 166 apply(auto simp add: rel_fun_def fun_eq_iff) using q1 q2 unfolding Quotient3_def by metis 167 moreover have "((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and> 168 (rep1 ---> abs2) r = (rep1 ---> abs2) s) \<Longrightarrow> (R1 ===> R2) r s" 169 apply(auto simp add: rel_fun_def fun_eq_iff) using q1 q2 unfolding Quotient3_def 170 by (metis map_fun_apply) 171 172 ultimately show ?thesis by blast 173 qed 174 } 175 ultimately show ?thesis by (intro Quotient3I) (assumption+) 176qed 177 178lemma lambda_prs: 179 assumes q1: "Quotient3 R1 Abs1 Rep1" 180 and q2: "Quotient3 R2 Abs2 Rep2" 181 shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)" 182 unfolding fun_eq_iff 183 using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] 184 by simp 185 186lemma lambda_prs1: 187 assumes q1: "Quotient3 R1 Abs1 Rep1" 188 and q2: "Quotient3 R2 Abs2 Rep2" 189 shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)" 190 unfolding fun_eq_iff 191 using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] 192 by simp 193 194text\<open> 195 In the following theorem R1 can be instantiated with anything, 196 but we know some of the types of the Rep and Abs functions; 197 so by solving Quotient assumptions we can get a unique R1 that 198 will be provable; which is why we need to use \<open>apply_rsp\<close> and 199 not the primed version\<close> 200 201lemma apply_rspQ3: 202 fixes f g::"'a \<Rightarrow> 'c" 203 assumes q: "Quotient3 R1 Abs1 Rep1" 204 and a: "(R1 ===> R2) f g" "R1 x y" 205 shows "R2 (f x) (g y)" 206 using a by (auto elim: rel_funE) 207 208lemma apply_rspQ3'': 209 assumes "Quotient3 R Abs Rep" 210 and "(R ===> S) f f" 211 shows "S (f (Rep x)) (f (Rep x))" 212proof - 213 from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient3_rep_reflp) 214 then show ?thesis using assms(2) by (auto intro: apply_rsp') 215qed 216 217subsection \<open>lemmas for regularisation of ball and bex\<close> 218 219lemma ball_reg_eqv: 220 fixes P :: "'a \<Rightarrow> bool" 221 assumes a: "equivp R" 222 shows "Ball (Respects R) P = (All P)" 223 using a 224 unfolding equivp_def 225 by (auto simp add: in_respects) 226 227lemma bex_reg_eqv: 228 fixes P :: "'a \<Rightarrow> bool" 229 assumes a: "equivp R" 230 shows "Bex (Respects R) P = (Ex P)" 231 using a 232 unfolding equivp_def 233 by (auto simp add: in_respects) 234 235lemma ball_reg_right: 236 assumes a: "\<And>x. x \<in> R \<Longrightarrow> P x \<longrightarrow> Q x" 237 shows "All P \<longrightarrow> Ball R Q" 238 using a by fast 239 240lemma bex_reg_left: 241 assumes a: "\<And>x. x \<in> R \<Longrightarrow> Q x \<longrightarrow> P x" 242 shows "Bex R Q \<longrightarrow> Ex P" 243 using a by fast 244 245lemma ball_reg_left: 246 assumes a: "equivp R" 247 shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P" 248 using a by (metis equivp_reflp in_respects) 249 250lemma bex_reg_right: 251 assumes a: "equivp R" 252 shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P" 253 using a by (metis equivp_reflp in_respects) 254 255lemma ball_reg_eqv_range: 256 fixes P::"'a \<Rightarrow> bool" 257 and x::"'a" 258 assumes a: "equivp R2" 259 shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))" 260 apply(rule iffI) 261 apply(rule allI) 262 apply(drule_tac x="\<lambda>y. f x" in bspec) 263 apply(simp add: in_respects rel_fun_def) 264 apply(rule impI) 265 using a equivp_reflp_symp_transp[of "R2"] 266 apply (auto elim: equivpE reflpE) 267 done 268 269lemma bex_reg_eqv_range: 270 assumes a: "equivp R2" 271 shows "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))" 272 apply(auto) 273 apply(rule_tac x="\<lambda>y. f x" in bexI) 274 apply(simp) 275 apply(simp add: Respects_def in_respects rel_fun_def) 276 apply(rule impI) 277 using a equivp_reflp_symp_transp[of "R2"] 278 apply (auto elim: equivpE reflpE) 279 done 280 281(* Next four lemmas are unused *) 282lemma all_reg: 283 assumes a: "\<forall>x :: 'a. (P x \<longrightarrow> Q x)" 284 and b: "All P" 285 shows "All Q" 286 using a b by fast 287 288lemma ex_reg: 289 assumes a: "\<forall>x :: 'a. (P x \<longrightarrow> Q x)" 290 and b: "Ex P" 291 shows "Ex Q" 292 using a b by fast 293 294lemma ball_reg: 295 assumes a: "\<forall>x :: 'a. (x \<in> R \<longrightarrow> P x \<longrightarrow> Q x)" 296 and b: "Ball R P" 297 shows "Ball R Q" 298 using a b by fast 299 300lemma bex_reg: 301 assumes a: "\<forall>x :: 'a. (x \<in> R \<longrightarrow> P x \<longrightarrow> Q x)" 302 and b: "Bex R P" 303 shows "Bex R Q" 304 using a b by fast 305 306 307lemma ball_all_comm: 308 assumes "\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)" 309 shows "(\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y)" 310 using assms by auto 311 312lemma bex_ex_comm: 313 assumes "(\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)" 314 shows "(\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y)" 315 using assms by auto 316 317subsection \<open>Bounded abstraction\<close> 318 319definition 320 Babs :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" 321where 322 "x \<in> p \<Longrightarrow> Babs p m x = m x" 323 324lemma babs_rsp: 325 assumes q: "Quotient3 R1 Abs1 Rep1" 326 and a: "(R1 ===> R2) f g" 327 shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)" 328 apply (auto simp add: Babs_def in_respects rel_fun_def) 329 apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1") 330 using a apply (simp add: Babs_def rel_fun_def) 331 apply (simp add: in_respects rel_fun_def) 332 using Quotient3_rel[OF q] 333 by metis 334 335lemma babs_prs: 336 assumes q1: "Quotient3 R1 Abs1 Rep1" 337 and q2: "Quotient3 R2 Abs2 Rep2" 338 shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f" 339 apply (rule ext) 340 apply (simp add:) 341 apply (subgoal_tac "Rep1 x \<in> Respects R1") 342 apply (simp add: Babs_def Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) 343 apply (simp add: in_respects Quotient3_rel_rep[OF q1]) 344 done 345 346lemma babs_simp: 347 assumes q: "Quotient3 R1 Abs Rep" 348 shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)" 349 apply(rule iffI) 350 apply(simp_all only: babs_rsp[OF q]) 351 apply(auto simp add: Babs_def rel_fun_def) 352 apply(metis Babs_def in_respects Quotient3_rel[OF q]) 353 done 354 355(* If a user proves that a particular functional relation 356 is an equivalence this may be useful in regularising *) 357lemma babs_reg_eqv: 358 shows "equivp R \<Longrightarrow> Babs (Respects R) P = P" 359 by (simp add: fun_eq_iff Babs_def in_respects equivp_reflp) 360 361 362(* 3 lemmas needed for proving repabs_inj *) 363lemma ball_rsp: 364 assumes a: "(R ===> (=)) f g" 365 shows "Ball (Respects R) f = Ball (Respects R) g" 366 using a by (auto simp add: Ball_def in_respects elim: rel_funE) 367 368lemma bex_rsp: 369 assumes a: "(R ===> (=)) f g" 370 shows "(Bex (Respects R) f = Bex (Respects R) g)" 371 using a by (auto simp add: Bex_def in_respects elim: rel_funE) 372 373lemma bex1_rsp: 374 assumes a: "(R ===> (=)) f g" 375 shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)" 376 using a by (auto elim: rel_funE simp add: Ex1_def in_respects) 377 378(* 2 lemmas needed for cleaning of quantifiers *) 379lemma all_prs: 380 assumes a: "Quotient3 R absf repf" 381 shows "Ball (Respects R) ((absf ---> id) f) = All f" 382 using a unfolding Quotient3_def Ball_def in_respects id_apply comp_def map_fun_def 383 by metis 384 385lemma ex_prs: 386 assumes a: "Quotient3 R absf repf" 387 shows "Bex (Respects R) ((absf ---> id) f) = Ex f" 388 using a unfolding Quotient3_def Bex_def in_respects id_apply comp_def map_fun_def 389 by metis 390 391subsection \<open>\<open>Bex1_rel\<close> quantifier\<close> 392 393definition 394 Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" 395where 396 "Bex1_rel R P \<longleftrightarrow> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))" 397 398lemma bex1_rel_aux: 399 "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R x\<rbrakk> \<Longrightarrow> Bex1_rel R y" 400 unfolding Bex1_rel_def 401 by (metis in_respects) 402 403lemma bex1_rel_aux2: 404 "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R y\<rbrakk> \<Longrightarrow> Bex1_rel R x" 405 unfolding Bex1_rel_def 406 by (metis in_respects) 407 408lemma bex1_rel_rsp: 409 assumes a: "Quotient3 R absf repf" 410 shows "((R ===> (=)) ===> (=)) (Bex1_rel R) (Bex1_rel R)" 411 unfolding rel_fun_def by (metis bex1_rel_aux bex1_rel_aux2) 412 413lemma ex1_prs: 414 assumes "Quotient3 R absf repf" 415 shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f" 416 apply (auto simp: Bex1_rel_def Respects_def) 417 apply (metis Quotient3_def assms) 418 apply (metis (full_types) Quotient3_def assms) 419 by (meson Quotient3_rel assms) 420 421lemma bex1_bexeq_reg: 422 shows "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))" 423 by (auto simp add: Ex1_def Bex1_rel_def Bex_def Ball_def in_respects) 424 425lemma bex1_bexeq_reg_eqv: 426 assumes a: "equivp R" 427 shows "(\<exists>!x. P x) \<longrightarrow> Bex1_rel R P" 428 using equivp_reflp[OF a] 429 by (metis (full_types) Bex1_rel_def in_respects) 430 431subsection \<open>Various respects and preserve lemmas\<close> 432 433lemma quot_rel_rsp: 434 assumes a: "Quotient3 R Abs Rep" 435 shows "(R ===> R ===> (=)) R R" 436 apply(rule rel_funI)+ 437 by (meson assms equals_rsp) 438 439lemma o_prs: 440 assumes q1: "Quotient3 R1 Abs1 Rep1" 441 and q2: "Quotient3 R2 Abs2 Rep2" 442 and q3: "Quotient3 R3 Abs3 Rep3" 443 shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) (\<circ>) = (\<circ>)" 444 and "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) (\<circ>) = (\<circ>)" 445 using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] Quotient3_abs_rep[OF q3] 446 by (simp_all add: fun_eq_iff) 447 448lemma o_rsp: 449 "((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) (\<circ>) (\<circ>)" 450 "((=) ===> (R1 ===> (=)) ===> R1 ===> (=)) (\<circ>) (\<circ>)" 451 by (force elim: rel_funE)+ 452 453lemma cond_prs: 454 assumes a: "Quotient3 R absf repf" 455 shows "absf (if a then repf b else repf c) = (if a then b else c)" 456 using a unfolding Quotient3_def by auto 457 458lemma if_prs: 459 assumes q: "Quotient3 R Abs Rep" 460 shows "(id ---> Rep ---> Rep ---> Abs) If = If" 461 using Quotient3_abs_rep[OF q] 462 by (auto simp add: fun_eq_iff) 463 464lemma if_rsp: 465 assumes q: "Quotient3 R Abs Rep" 466 shows "((=) ===> R ===> R ===> R) If If" 467 by force 468 469lemma let_prs: 470 assumes q1: "Quotient3 R1 Abs1 Rep1" 471 and q2: "Quotient3 R2 Abs2 Rep2" 472 shows "(Rep2 ---> (Abs2 ---> Rep1) ---> Abs1) Let = Let" 473 using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] 474 by (auto simp add: fun_eq_iff) 475 476lemma let_rsp: 477 shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let" 478 by (force elim: rel_funE) 479 480lemma id_rsp: 481 shows "(R ===> R) id id" 482 by auto 483 484lemma id_prs: 485 assumes a: "Quotient3 R Abs Rep" 486 shows "(Rep ---> Abs) id = id" 487 by (simp add: fun_eq_iff Quotient3_abs_rep [OF a]) 488 489end 490 491locale quot_type = 492 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 493 and Abs :: "'a set \<Rightarrow> 'b" 494 and Rep :: "'b \<Rightarrow> 'a set" 495 assumes equivp: "part_equivp R" 496 and rep_prop: "\<And>y. \<exists>x. R x x \<and> Rep y = Collect (R x)" 497 and rep_inverse: "\<And>x. Abs (Rep x) = x" 498 and abs_inverse: "\<And>c. (\<exists>x. ((R x x) \<and> (c = Collect (R x)))) \<Longrightarrow> (Rep (Abs c)) = c" 499 and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)" 500begin 501 502definition 503 abs :: "'a \<Rightarrow> 'b" 504where 505 "abs x = Abs (Collect (R x))" 506 507definition 508 rep :: "'b \<Rightarrow> 'a" 509where 510 "rep a = (SOME x. x \<in> Rep a)" 511 512lemma some_collect: 513 assumes "R r r" 514 shows "R (SOME x. x \<in> Collect (R r)) = R r" 515 apply simp 516 by (metis assms exE_some equivp[simplified part_equivp_def]) 517 518lemma Quotient: 519 shows "Quotient3 R abs rep" 520 unfolding Quotient3_def abs_def rep_def 521 proof (intro conjI allI) 522 fix a r s 523 show x: "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)" proof - 524 obtain x where r: "R x x" and rep: "Rep a = Collect (R x)" using rep_prop[of a] by auto 525 have "R (SOME x. x \<in> Rep a) x" using r rep some_collect by metis 526 then have "R x (SOME x. x \<in> Rep a)" using part_equivp_symp[OF equivp] by fast 527 then show "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)" 528 using part_equivp_transp[OF equivp] by (metis \<open>R (SOME x. x \<in> Rep a) x\<close>) 529 qed 530 have "Collect (R (SOME x. x \<in> Rep a)) = (Rep a)" by (metis some_collect rep_prop) 531 then show "Abs (Collect (R (SOME x. x \<in> Rep a))) = a" using rep_inverse by auto 532 have "R r r \<Longrightarrow> R s s \<Longrightarrow> Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" 533 proof - 534 assume "R r r" and "R s s" 535 then have "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> Collect (R r) = Collect (R s)" 536 by (metis abs_inverse) 537 also have "Collect (R r) = Collect (R s) \<longleftrightarrow> (\<lambda>A x. x \<in> A) (Collect (R r)) = (\<lambda>A x. x \<in> A) (Collect (R s))" 538 by rule simp_all 539 finally show "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" by simp 540 qed 541 then show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (Collect (R r)) = Abs (Collect (R s)))" 542 using equivp[simplified part_equivp_def] by metis 543 qed 544 545end 546 547subsection \<open>Quotient composition\<close> 548 549 550lemma OOO_quotient3: 551 fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 552 fixes Abs1 :: "'a \<Rightarrow> 'b" and Rep1 :: "'b \<Rightarrow> 'a" 553 fixes Abs2 :: "'b \<Rightarrow> 'c" and Rep2 :: "'c \<Rightarrow> 'b" 554 fixes R2' :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 555 fixes R2 :: "'b \<Rightarrow> 'b \<Rightarrow> bool" 556 assumes R1: "Quotient3 R1 Abs1 Rep1" 557 assumes R2: "Quotient3 R2 Abs2 Rep2" 558 assumes Abs1: "\<And>x y. R2' x y \<Longrightarrow> R1 x x \<Longrightarrow> R1 y y \<Longrightarrow> R2 (Abs1 x) (Abs1 y)" 559 assumes Rep1: "\<And>x y. R2 x y \<Longrightarrow> R2' (Rep1 x) (Rep1 y)" 560 shows "Quotient3 (R1 OO R2' OO R1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)" 561proof - 562 have *: "(R1 OOO R2') r r \<and> (R1 OOO R2') s s \<and> (Abs2 \<circ> Abs1) r = (Abs2 \<circ> Abs1) s 563 \<longleftrightarrow> (R1 OOO R2') r s" for r s 564 apply safe 565 subgoal for a b c d 566 apply simp 567 apply (rule_tac b="Rep1 (Abs1 r)" in relcomppI) 568 using Quotient3_refl1 R1 rep_abs_rsp apply fastforce 569 apply (rule_tac b="Rep1 (Abs1 s)" in relcomppI) 570 apply (metis (full_types) Rep1 Abs1 Quotient3_rel R2 Quotient3_refl1 [OF R1] Quotient3_refl2 [OF R1] Quotient3_rel_abs [OF R1]) 571 by (metis Quotient3_rel R1 rep_abs_rsp_left) 572 subgoal for x y 573 apply (drule Abs1) 574 apply (erule Quotient3_refl2 [OF R1]) 575 apply (erule Quotient3_refl1 [OF R1]) 576 apply (drule Quotient3_refl1 [OF R2], drule Rep1) 577 by (metis (full_types) Quotient3_def R1 relcompp.relcompI) 578 subgoal for x y 579 apply (drule Abs1) 580 apply (erule Quotient3_refl2 [OF R1]) 581 apply (erule Quotient3_refl1 [OF R1]) 582 apply (drule Quotient3_refl2 [OF R2], drule Rep1) 583 by (metis (full_types) Quotient3_def R1 relcompp.relcompI) 584 subgoal for x y 585 by simp (metis (full_types) Abs1 Quotient3_rel R1 R2) 586 done 587 show ?thesis 588 apply (rule Quotient3I) 589 using * apply (simp_all add: o_def Quotient3_abs_rep [OF R2] Quotient3_abs_rep [OF R1]) 590 apply (metis Quotient3_rep_reflp R1 R2 Rep1 relcompp.relcompI) 591 done 592qed 593 594lemma OOO_eq_quotient3: 595 fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 596 fixes Abs1 :: "'a \<Rightarrow> 'b" and Rep1 :: "'b \<Rightarrow> 'a" 597 fixes Abs2 :: "'b \<Rightarrow> 'c" and Rep2 :: "'c \<Rightarrow> 'b" 598 assumes R1: "Quotient3 R1 Abs1 Rep1" 599 assumes R2: "Quotient3 (=) Abs2 Rep2" 600 shows "Quotient3 (R1 OOO (=)) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)" 601using assms 602by (rule OOO_quotient3) auto 603 604subsection \<open>Quotient3 to Quotient\<close> 605 606lemma Quotient3_to_Quotient: 607assumes "Quotient3 R Abs Rep" 608and "T \<equiv> \<lambda>x y. R x x \<and> Abs x = y" 609shows "Quotient R Abs Rep T" 610using assms unfolding Quotient3_def by (intro QuotientI) blast+ 611 612lemma Quotient3_to_Quotient_equivp: 613assumes q: "Quotient3 R Abs Rep" 614and T_def: "T \<equiv> \<lambda>x y. Abs x = y" 615and eR: "equivp R" 616shows "Quotient R Abs Rep T" 617proof (intro QuotientI) 618 fix a 619 show "Abs (Rep a) = a" using q by(rule Quotient3_abs_rep) 620next 621 fix a 622 show "R (Rep a) (Rep a)" using q by(rule Quotient3_rep_reflp) 623next 624 fix r s 625 show "R r s = (R r r \<and> R s s \<and> Abs r = Abs s)" using q by(rule Quotient3_rel[symmetric]) 626next 627 show "T = (\<lambda>x y. R x x \<and> Abs x = y)" using T_def equivp_reflp[OF eR] by simp 628qed 629 630subsection \<open>ML setup\<close> 631 632text \<open>Auxiliary data for the quotient package\<close> 633 634named_theorems quot_equiv "equivalence relation theorems" 635 and quot_respect "respectfulness theorems" 636 and quot_preserve "preservation theorems" 637 and id_simps "identity simp rules for maps" 638 and quot_thm "quotient theorems" 639ML_file "Tools/Quotient/quotient_info.ML" 640 641declare [[mapQ3 "fun" = (rel_fun, fun_quotient3)]] 642 643lemmas [quot_thm] = fun_quotient3 644lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp 645lemmas [quot_preserve] = if_prs o_prs let_prs id_prs 646lemmas [quot_equiv] = identity_equivp 647 648 649text \<open>Lemmas about simplifying id's.\<close> 650lemmas [id_simps] = 651 id_def[symmetric] 652 map_fun_id 653 id_apply 654 id_o 655 o_id 656 eq_comp_r 657 vimage_id 658 659text \<open>Translation functions for the lifting process.\<close> 660ML_file "Tools/Quotient/quotient_term.ML" 661 662 663text \<open>Definitions of the quotient types.\<close> 664ML_file "Tools/Quotient/quotient_type.ML" 665 666 667text \<open>Definitions for quotient constants.\<close> 668ML_file "Tools/Quotient/quotient_def.ML" 669 670 671text \<open> 672 An auxiliary constant for recording some information 673 about the lifted theorem in a tactic. 674\<close> 675definition 676 Quot_True :: "'a \<Rightarrow> bool" 677where 678 "Quot_True x \<longleftrightarrow> True" 679 680lemma 681 shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P" 682 and QT_ex: "Quot_True (Ex P) \<Longrightarrow> Quot_True P" 683 and QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P" 684 and QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))" 685 and QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)" 686 by (simp_all add: Quot_True_def ext) 687 688lemma QT_imp: "Quot_True a \<equiv> Quot_True b" 689 by (simp add: Quot_True_def) 690 691context includes lifting_syntax 692begin 693 694text \<open>Tactics for proving the lifted theorems\<close> 695ML_file "Tools/Quotient/quotient_tacs.ML" 696 697end 698 699subsection \<open>Methods / Interface\<close> 700 701method_setup lifting = 702 \<open>Attrib.thms >> (fn thms => fn ctxt => 703 SIMPLE_METHOD' (Quotient_Tacs.lift_tac ctxt [] thms))\<close> 704 \<open>lift theorems to quotient types\<close> 705 706method_setup lifting_setup = 707 \<open>Attrib.thm >> (fn thm => fn ctxt => 708 SIMPLE_METHOD' (Quotient_Tacs.lift_procedure_tac ctxt [] thm))\<close> 709 \<open>set up the three goals for the quotient lifting procedure\<close> 710 711method_setup descending = 712 \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_tac ctxt []))\<close> 713 \<open>decend theorems to the raw level\<close> 714 715method_setup descending_setup = 716 \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_procedure_tac ctxt []))\<close> 717 \<open>set up the three goals for the decending theorems\<close> 718 719method_setup partiality_descending = 720 \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_tac ctxt []))\<close> 721 \<open>decend theorems to the raw level\<close> 722 723method_setup partiality_descending_setup = 724 \<open>Scan.succeed (fn ctxt => 725 SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_procedure_tac ctxt []))\<close> 726 \<open>set up the three goals for the decending theorems\<close> 727 728method_setup regularize = 729 \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.regularize_tac ctxt))\<close> 730 \<open>prove the regularization goals from the quotient lifting procedure\<close> 731 732method_setup injection = 733 \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.all_injection_tac ctxt))\<close> 734 \<open>prove the rep/abs injection goals from the quotient lifting procedure\<close> 735 736method_setup cleaning = 737 \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.clean_tac ctxt))\<close> 738 \<open>prove the cleaning goals from the quotient lifting procedure\<close> 739 740attribute_setup quot_lifted = 741 \<open>Scan.succeed Quotient_Tacs.lifted_attrib\<close> 742 \<open>lift theorems to quotient types\<close> 743 744no_notation 745 rel_conj (infixr "OOO" 75) 746 747end 748 749