equal
deleted
inserted
replaced
35 lemma [transfer_rule]: "(rel_option A ===> op=) equal_None equal_None" |
35 lemma [transfer_rule]: "(rel_option A ===> op=) equal_None equal_None" |
36 unfolding fun_rel_def rel_option_iff equal_None_def by (auto split: option.split) |
36 unfolding fun_rel_def rel_option_iff equal_None_def by (auto split: option.split) |
37 |
37 |
38 lemma dom_transfer: |
38 lemma dom_transfer: |
39 assumes [transfer_rule]: "bi_total A" |
39 assumes [transfer_rule]: "bi_total A" |
40 shows "((A ===> rel_option B) ===> set_rel A) dom dom" |
40 shows "((A ===> rel_option B) ===> rel_set A) dom dom" |
41 unfolding dom_def[abs_def] equal_None_def[symmetric] |
41 unfolding dom_def[abs_def] equal_None_def[symmetric] |
42 by transfer_prover |
42 by transfer_prover |
43 |
43 |
44 lemma map_of_transfer [transfer_rule]: |
44 lemma map_of_transfer [transfer_rule]: |
45 assumes [transfer_rule]: "bi_unique R1" |
45 assumes [transfer_rule]: "bi_unique R1" |