equal
deleted
inserted
replaced
457 |
457 |
458 lemma Ex_transfer [transfer_rule]: |
458 lemma Ex_transfer [transfer_rule]: |
459 assumes "bi_total A" |
459 assumes "bi_total A" |
460 shows "((A ===> op =) ===> op =) Ex Ex" |
460 shows "((A ===> op =) ===> op =) Ex Ex" |
461 using assms unfolding bi_total_def rel_fun_def by fast |
461 using assms unfolding bi_total_def rel_fun_def by fast |
|
462 |
|
463 lemma Ex1_parametric [transfer_rule]: |
|
464 assumes [transfer_rule]: "bi_unique A" "bi_total A" |
|
465 shows "((A ===> op =) ===> op =) Ex1 Ex1" |
|
466 unfolding Ex1_def[abs_def] by transfer_prover |
462 |
467 |
463 declare If_transfer [transfer_rule] |
468 declare If_transfer [transfer_rule] |
464 |
469 |
465 lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let" |
470 lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let" |
466 unfolding rel_fun_def by simp |
471 unfolding rel_fun_def by simp |