290 |
290 |
291 lemma Quotient_abs_induct: |
291 lemma Quotient_abs_induct: |
292 assumes "\<And>y. R y y \<Longrightarrow> P (Abs y)" shows "P x" |
292 assumes "\<And>y. R y y \<Longrightarrow> P (Abs y)" shows "P x" |
293 using 1 assms unfolding Quotient_def by metis |
293 using 1 assms unfolding Quotient_def by metis |
294 |
294 |
295 lemma Quotient_All_transfer: |
|
296 "((T ===> op =) ===> op =) (Ball (Respects R)) All" |
|
297 unfolding fun_rel_def Respects_def Quotient_cr_rel [OF 1] |
|
298 by (auto, metis Quotient_abs_induct) |
|
299 |
|
300 lemma Quotient_Ex_transfer: |
|
301 "((T ===> op =) ===> op =) (Bex (Respects R)) Ex" |
|
302 unfolding fun_rel_def Respects_def Quotient_cr_rel [OF 1] |
|
303 by (auto, metis Quotient_rep_reflp [OF 1] Quotient_abs_rep [OF 1]) |
|
304 |
|
305 lemma Quotient_forall_transfer: |
|
306 "((T ===> op =) ===> op =) (transfer_bforall (\<lambda>x. R x x)) transfer_forall" |
|
307 using Quotient_All_transfer |
|
308 unfolding transfer_forall_def transfer_bforall_def |
|
309 Ball_def [abs_def] in_respects . |
|
310 |
|
311 end |
295 end |
312 |
296 |
313 text {* Generating transfer rules for total quotients. *} |
297 text {* Generating transfer rules for total quotients. *} |
314 |
298 |
315 context |
299 context |
353 using T_def type Quotient_right_total typedef_to_Quotient |
337 using T_def type Quotient_right_total typedef_to_Quotient |
354 by blast |
338 by blast |
355 |
339 |
356 lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep" |
340 lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep" |
357 unfolding fun_rel_def T_def by simp |
341 unfolding fun_rel_def T_def by simp |
358 |
|
359 lemma typedef_All_transfer: "((T ===> op =) ===> op =) (Ball A) All" |
|
360 unfolding T_def fun_rel_def |
|
361 by (metis type_definition.Rep [OF type] |
|
362 type_definition.Abs_inverse [OF type]) |
|
363 |
|
364 lemma typedef_Ex_transfer: "((T ===> op =) ===> op =) (Bex A) Ex" |
|
365 unfolding T_def fun_rel_def |
|
366 by (metis type_definition.Rep [OF type] |
|
367 type_definition.Abs_inverse [OF type]) |
|
368 |
|
369 lemma typedef_forall_transfer: |
|
370 "((T ===> op =) ===> op =) |
|
371 (transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall" |
|
372 unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric] |
|
373 by (rule typedef_All_transfer) |
|
374 |
342 |
375 end |
343 end |
376 |
344 |
377 text {* Generating the correspondence rule for a constant defined with |
345 text {* Generating the correspondence rule for a constant defined with |
378 @{text "lift_definition"}. *} |
346 @{text "lift_definition"}. *} |
538 apply (subst all_comm) |
506 apply (subst all_comm) |
539 apply (subst all_conj_distrib[symmetric]) |
507 apply (subst all_conj_distrib[symmetric]) |
540 apply (intro choice) |
508 apply (intro choice) |
541 by metis |
509 by metis |
542 |
510 |
|
511 subsection {* Domains *} |
|
512 |
|
513 lemma pcr_Domainp_par_left_total: |
|
514 assumes "Domainp B = P" |
|
515 assumes "left_total A" |
|
516 assumes "(A ===> op=) P' P" |
|
517 shows "Domainp (A OO B) = P'" |
|
518 using assms |
|
519 unfolding Domainp_iff[abs_def] OO_def bi_unique_def left_total_def fun_rel_def |
|
520 by (fast intro: fun_eq_iff) |
|
521 |
|
522 lemma pcr_Domainp_par: |
|
523 assumes "Domainp B = P2" |
|
524 assumes "Domainp A = P1" |
|
525 assumes "(A ===> op=) P2' P2" |
|
526 shows "Domainp (A OO B) = (inf P1 P2')" |
|
527 using assms unfolding fun_rel_def Domainp_iff[abs_def] OO_def |
|
528 by (fast intro: fun_eq_iff) |
|
529 |
|
530 definition rel_pred_comp :: "('a => 'b => bool) => ('b => bool) => 'a => bool" (infixr "OP" 75) |
|
531 where "rel_pred_comp R P \<equiv> \<lambda>x. \<exists>y. R x y \<and> P y" |
|
532 |
|
533 lemma pcr_Domainp: |
|
534 assumes "Domainp B = P" |
|
535 shows "Domainp (A OO B) = (A OP P)" |
|
536 using assms unfolding rel_pred_comp_def by blast |
|
537 |
|
538 lemma pcr_Domainp_total: |
|
539 assumes "bi_total B" |
|
540 assumes "Domainp A = P" |
|
541 shows "Domainp (A OO B) = P" |
|
542 using assms unfolding bi_total_def |
|
543 by fast |
|
544 |
|
545 lemma Quotient_to_Domainp: |
|
546 assumes "Quotient R Abs Rep T" |
|
547 shows "Domainp T = (\<lambda>x. R x x)" |
|
548 by (simp add: Domainp_iff[abs_def] Quotient_cr_rel[OF assms]) |
|
549 |
|
550 lemma invariant_to_Domainp: |
|
551 assumes "Quotient (Lifting.invariant P) Abs Rep T" |
|
552 shows "Domainp T = P" |
|
553 by (simp add: invariant_def Domainp_iff[abs_def] Quotient_cr_rel[OF assms]) |
|
554 |
543 subsection {* ML setup *} |
555 subsection {* ML setup *} |
544 |
556 |
545 ML_file "Tools/Lifting/lifting_util.ML" |
557 ML_file "Tools/Lifting/lifting_util.ML" |
546 |
558 |
547 ML_file "Tools/Lifting/lifting_info.ML" |
559 ML_file "Tools/Lifting/lifting_info.ML" |