equal
deleted
inserted
replaced
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" |
46 shows "(list_all2 (prod_rel R1 R2) ===> R1 ===> rel_option R2) map_of map_of" |
46 shows "(list_all2 (rel_prod R1 R2) ===> R1 ===> rel_option R2) map_of map_of" |
47 unfolding map_of_def by transfer_prover |
47 unfolding map_of_def by transfer_prover |
48 |
48 |
49 lemma tabulate_transfer: |
49 lemma tabulate_transfer: |
50 assumes [transfer_rule]: "bi_unique A" |
50 assumes [transfer_rule]: "bi_unique A" |
51 shows "(list_all2 A ===> (A ===> B) ===> A ===> rel_option B) |
51 shows "(list_all2 A ===> (A ===> B) ===> A ===> rel_option B) |