equal
deleted
inserted
replaced
31 by transfer_prover |
31 by transfer_prover |
32 |
32 |
33 definition equal_None :: "'a option \<Rightarrow> bool" where "equal_None x \<equiv> x = None" |
33 definition equal_None :: "'a option \<Rightarrow> bool" where "equal_None x \<equiv> x = None" |
34 |
34 |
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 rel_fun_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) ===> rel_set 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] |
53 by transfer_prover |
53 by transfer_prover |
54 |
54 |
55 lemma bulkload_transfer: |
55 lemma bulkload_transfer: |
56 "(list_all2 A ===> op= ===> rel_option A) |
56 "(list_all2 A ===> op= ===> rel_option A) |
57 (\<lambda>xs k. if k < length xs then Some (xs ! k) else None) (\<lambda>xs k. if k < length xs then Some (xs ! k) else None)" |
57 (\<lambda>xs k. if k < length xs then Some (xs ! k) else None) (\<lambda>xs k. if k < length xs then Some (xs ! k) else None)" |
58 unfolding fun_rel_def |
58 unfolding rel_fun_def |
59 apply clarsimp |
59 apply clarsimp |
60 apply (erule list_all2_induct) |
60 apply (erule list_all2_induct) |
61 apply simp |
61 apply simp |
62 apply (case_tac xa) |
62 apply (case_tac xa) |
63 apply simp |
63 apply simp |