76 |
76 |
77 lemma Quotient_rep_abs: "R r r \<Longrightarrow> R (Rep (Abs r)) r" |
77 lemma Quotient_rep_abs: "R r r \<Longrightarrow> R (Rep (Abs r)) r" |
78 using a unfolding Quotient_def |
78 using a unfolding Quotient_def |
79 by blast |
79 by blast |
80 |
80 |
81 lemma Quotient_rep_abs_eq: "R t t \<Longrightarrow> R \<le> op= \<Longrightarrow> Rep (Abs t) = t" |
81 lemma Quotient_rep_abs_eq: "R t t \<Longrightarrow> R \<le> (=) \<Longrightarrow> Rep (Abs t) = t" |
82 using a unfolding Quotient_def |
82 using a unfolding Quotient_def |
83 by blast |
83 by blast |
84 |
84 |
85 lemma Quotient_rep_abs_fold_unmap: |
85 lemma Quotient_rep_abs_fold_unmap: |
86 assumes "x' \<equiv> Abs x" and "R x x" and "Rep x' \<equiv> Rep' x'" |
86 assumes "x' \<equiv> Abs x" and "R x x" and "Rep x' \<equiv> Rep' x'" |
116 lemma Quotient_part_equivp: "part_equivp R" |
116 lemma Quotient_part_equivp: "part_equivp R" |
117 by (metis Quotient_rep_reflp Quotient_symp Quotient_transp part_equivpI) |
117 by (metis Quotient_rep_reflp Quotient_symp Quotient_transp part_equivpI) |
118 |
118 |
119 end |
119 end |
120 |
120 |
121 lemma identity_quotient: "Quotient (op =) id id (op =)" |
121 lemma identity_quotient: "Quotient (=) id id (=)" |
122 unfolding Quotient_def by simp |
122 unfolding Quotient_def by simp |
123 |
123 |
124 text \<open>TODO: Use one of these alternatives as the real definition.\<close> |
124 text \<open>TODO: Use one of these alternatives as the real definition.\<close> |
125 |
125 |
126 lemma Quotient_alt_def: |
126 lemma Quotient_alt_def: |
215 unfolding Respects_def by simp |
215 unfolding Respects_def by simp |
216 |
216 |
217 lemma UNIV_typedef_to_Quotient: |
217 lemma UNIV_typedef_to_Quotient: |
218 assumes "type_definition Rep Abs UNIV" |
218 assumes "type_definition Rep Abs UNIV" |
219 and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" |
219 and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" |
220 shows "Quotient (op =) Abs Rep T" |
220 shows "Quotient (=) Abs Rep T" |
221 proof - |
221 proof - |
222 interpret type_definition Rep Abs UNIV by fact |
222 interpret type_definition Rep Abs UNIV by fact |
223 from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis |
223 from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis |
224 by (fastforce intro!: QuotientI fun_eq_iff) |
224 by (fastforce intro!: QuotientI fun_eq_iff) |
225 qed |
225 qed |
226 |
226 |
227 lemma UNIV_typedef_to_equivp: |
227 lemma UNIV_typedef_to_equivp: |
228 fixes Abs :: "'a \<Rightarrow> 'b" |
228 fixes Abs :: "'a \<Rightarrow> 'b" |
229 and Rep :: "'b \<Rightarrow> 'a" |
229 and Rep :: "'b \<Rightarrow> 'a" |
230 assumes "type_definition Rep Abs (UNIV::'a set)" |
230 assumes "type_definition Rep Abs (UNIV::'a set)" |
231 shows "equivp (op= ::'a\<Rightarrow>'a\<Rightarrow>bool)" |
231 shows "equivp ((=) ::'a\<Rightarrow>'a\<Rightarrow>bool)" |
232 by (rule identity_equivp) |
232 by (rule identity_equivp) |
233 |
233 |
234 lemma typedef_to_Quotient: |
234 lemma typedef_to_Quotient: |
235 assumes "type_definition Rep Abs S" |
235 assumes "type_definition Rep Abs S" |
236 and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" |
236 and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" |
282 using 1 unfolding Quotient_alt_def right_unique_def by metis |
282 using 1 unfolding Quotient_alt_def right_unique_def by metis |
283 |
283 |
284 lemma Quotient_right_total: "right_total T" |
284 lemma Quotient_right_total: "right_total T" |
285 using 1 unfolding Quotient_alt_def right_total_def by metis |
285 using 1 unfolding Quotient_alt_def right_total_def by metis |
286 |
286 |
287 lemma Quotient_rel_eq_transfer: "(T ===> T ===> op =) R (op =)" |
287 lemma Quotient_rel_eq_transfer: "(T ===> T ===> (=)) R (=)" |
288 using 1 unfolding Quotient_alt_def rel_fun_def by simp |
288 using 1 unfolding Quotient_alt_def rel_fun_def by simp |
289 |
289 |
290 lemma Quotient_abs_induct: |
290 lemma Quotient_abs_induct: |
291 assumes "\<And>y. R y y \<Longrightarrow> P (Abs y)" shows "P x" |
291 assumes "\<And>y. R y y \<Longrightarrow> P (Abs y)" shows "P x" |
292 using 1 assms unfolding Quotient_def by metis |
292 using 1 assms unfolding Quotient_def by metis |
304 using 1 2 unfolding Quotient_alt_def left_total_def reflp_def by auto |
304 using 1 2 unfolding Quotient_alt_def left_total_def reflp_def by auto |
305 |
305 |
306 lemma Quotient_bi_total: "bi_total T" |
306 lemma Quotient_bi_total: "bi_total T" |
307 using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto |
307 using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto |
308 |
308 |
309 lemma Quotient_id_abs_transfer: "(op = ===> T) (\<lambda>x. x) Abs" |
309 lemma Quotient_id_abs_transfer: "((=) ===> T) (\<lambda>x. x) Abs" |
310 using 1 2 unfolding Quotient_alt_def reflp_def rel_fun_def by simp |
310 using 1 2 unfolding Quotient_alt_def reflp_def rel_fun_def by simp |
311 |
311 |
312 lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x" |
312 lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x" |
313 using 1 2 unfolding Quotient_alt_def reflp_def by metis |
313 using 1 2 unfolding Quotient_alt_def reflp_def by metis |
314 |
314 |
364 shows "left_total T" |
364 shows "left_total T" |
365 using r_R Quotient_cr_rel[OF q] unfolding left_total_def by (auto elim: reflpE) |
365 using r_R Quotient_cr_rel[OF q] unfolding left_total_def by (auto elim: reflpE) |
366 |
366 |
367 lemma Quotient_composition_ge_eq: |
367 lemma Quotient_composition_ge_eq: |
368 assumes "left_total T" |
368 assumes "left_total T" |
369 assumes "R \<ge> op=" |
369 assumes "R \<ge> (=)" |
370 shows "(T OO R OO T\<inverse>\<inverse>) \<ge> op=" |
370 shows "(T OO R OO T\<inverse>\<inverse>) \<ge> (=)" |
371 using assms unfolding left_total_def by fast |
371 using assms unfolding left_total_def by fast |
372 |
372 |
373 lemma Quotient_composition_le_eq: |
373 lemma Quotient_composition_le_eq: |
374 assumes "left_unique T" |
374 assumes "left_unique T" |
375 assumes "R \<le> op=" |
375 assumes "R \<le> (=)" |
376 shows "(T OO R OO T\<inverse>\<inverse>) \<le> op=" |
376 shows "(T OO R OO T\<inverse>\<inverse>) \<le> (=)" |
377 using assms unfolding left_unique_def by blast |
377 using assms unfolding left_unique_def by blast |
378 |
378 |
379 lemma eq_onp_le_eq: |
379 lemma eq_onp_le_eq: |
380 "eq_onp P \<le> op=" unfolding eq_onp_def by blast |
380 "eq_onp P \<le> (=)" unfolding eq_onp_def by blast |
381 |
381 |
382 lemma reflp_ge_eq: |
382 lemma reflp_ge_eq: |
383 "reflp R \<Longrightarrow> R \<ge> op=" unfolding reflp_def by blast |
383 "reflp R \<Longrightarrow> R \<ge> (=)" unfolding reflp_def by blast |
384 |
384 |
385 text \<open>Proving a parametrized correspondence relation\<close> |
385 text \<open>Proving a parametrized correspondence relation\<close> |
386 |
386 |
387 definition POS :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where |
387 definition POS :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where |
388 "POS A B \<equiv> A \<le> B" |
388 "POS A B \<equiv> A \<le> B" |
389 |
389 |
390 definition NEG :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where |
390 definition NEG :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where |
391 "NEG A B \<equiv> B \<le> A" |
391 "NEG A B \<equiv> B \<le> A" |
392 |
392 |
393 lemma pos_OO_eq: |
393 lemma pos_OO_eq: |
394 shows "POS (A OO op=) A" |
394 shows "POS (A OO (=)) A" |
395 unfolding POS_def OO_def by blast |
395 unfolding POS_def OO_def by blast |
396 |
396 |
397 lemma pos_eq_OO: |
397 lemma pos_eq_OO: |
398 shows "POS (op= OO A) A" |
398 shows "POS ((=) OO A) A" |
399 unfolding POS_def OO_def by blast |
399 unfolding POS_def OO_def by blast |
400 |
400 |
401 lemma neg_OO_eq: |
401 lemma neg_OO_eq: |
402 shows "NEG (A OO op=) A" |
402 shows "NEG (A OO (=)) A" |
403 unfolding NEG_def OO_def by auto |
403 unfolding NEG_def OO_def by auto |
404 |
404 |
405 lemma neg_eq_OO: |
405 lemma neg_eq_OO: |
406 shows "NEG (op= OO A) A" |
406 shows "NEG ((=) OO A) A" |
407 unfolding NEG_def OO_def by blast |
407 unfolding NEG_def OO_def by blast |
408 |
408 |
409 lemma POS_trans: |
409 lemma POS_trans: |
410 assumes "POS A B" |
410 assumes "POS A B" |
411 assumes "POS B C" |
411 assumes "POS B C" |
485 |
485 |
486 subsection \<open>Domains\<close> |
486 subsection \<open>Domains\<close> |
487 |
487 |
488 lemma composed_equiv_rel_eq_onp: |
488 lemma composed_equiv_rel_eq_onp: |
489 assumes "left_unique R" |
489 assumes "left_unique R" |
490 assumes "(R ===> op=) P P'" |
490 assumes "(R ===> (=)) P P'" |
491 assumes "Domainp R = P''" |
491 assumes "Domainp R = P''" |
492 shows "(R OO eq_onp P' OO R\<inverse>\<inverse>) = eq_onp (inf P'' P)" |
492 shows "(R OO eq_onp P' OO R\<inverse>\<inverse>) = eq_onp (inf P'' P)" |
493 using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def rel_fun_def eq_onp_def |
493 using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def rel_fun_def eq_onp_def |
494 fun_eq_iff by blast |
494 fun_eq_iff by blast |
495 |
495 |
496 lemma composed_equiv_rel_eq_eq_onp: |
496 lemma composed_equiv_rel_eq_eq_onp: |
497 assumes "left_unique R" |
497 assumes "left_unique R" |
498 assumes "Domainp R = P" |
498 assumes "Domainp R = P" |
499 shows "(R OO op= OO R\<inverse>\<inverse>) = eq_onp P" |
499 shows "(R OO (=) OO R\<inverse>\<inverse>) = eq_onp P" |
500 using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def eq_onp_def |
500 using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def eq_onp_def |
501 fun_eq_iff is_equality_def by metis |
501 fun_eq_iff is_equality_def by metis |
502 |
502 |
503 lemma pcr_Domainp_par_left_total: |
503 lemma pcr_Domainp_par_left_total: |
504 assumes "Domainp B = P" |
504 assumes "Domainp B = P" |
505 assumes "left_total A" |
505 assumes "left_total A" |
506 assumes "(A ===> op=) P' P" |
506 assumes "(A ===> (=)) P' P" |
507 shows "Domainp (A OO B) = P'" |
507 shows "Domainp (A OO B) = P'" |
508 using assms |
508 using assms |
509 unfolding Domainp_iff[abs_def] OO_def bi_unique_def left_total_def rel_fun_def |
509 unfolding Domainp_iff[abs_def] OO_def bi_unique_def left_total_def rel_fun_def |
510 by (fast intro: fun_eq_iff) |
510 by (fast intro: fun_eq_iff) |
511 |
511 |
512 lemma pcr_Domainp_par: |
512 lemma pcr_Domainp_par: |
513 assumes "Domainp B = P2" |
513 assumes "Domainp B = P2" |
514 assumes "Domainp A = P1" |
514 assumes "Domainp A = P1" |
515 assumes "(A ===> op=) P2' P2" |
515 assumes "(A ===> (=)) P2' P2" |
516 shows "Domainp (A OO B) = (inf P1 P2')" |
516 shows "Domainp (A OO B) = (inf P1 P2')" |
517 using assms unfolding rel_fun_def Domainp_iff[abs_def] OO_def |
517 using assms unfolding rel_fun_def Domainp_iff[abs_def] OO_def |
518 by (fast intro: fun_eq_iff) |
518 by (fast intro: fun_eq_iff) |
519 |
519 |
520 definition rel_pred_comp :: "('a => 'b => bool) => ('b => bool) => 'a => bool" |
520 definition rel_pred_comp :: "('a => 'b => bool) => ('b => bool) => 'a => bool" |