equal
deleted
inserted
replaced
38 (\<lambda>k m. m(k := None)) (\<lambda>k m. m(k := None))" |
38 (\<lambda>k m. m(k := None)) (\<lambda>k m. m(k := None))" |
39 by transfer_prover |
39 by transfer_prover |
40 |
40 |
41 lemma is_none_parametric [transfer_rule]: |
41 lemma is_none_parametric [transfer_rule]: |
42 "(rel_option A ===> HOL.eq) Option.is_none Option.is_none" |
42 "(rel_option A ===> HOL.eq) Option.is_none Option.is_none" |
43 by (auto simp add: is_none_def rel_fun_def rel_option_iff split: option.split) |
43 by (auto simp add: Option.is_none_def rel_fun_def rel_option_iff split: option.split) |
44 |
44 |
45 lemma dom_parametric: |
45 lemma dom_parametric: |
46 assumes [transfer_rule]: "bi_total A" |
46 assumes [transfer_rule]: "bi_total A" |
47 shows "((A ===> rel_option B) ===> rel_set A) dom dom" |
47 shows "((A ===> rel_option B) ===> rel_set A) dom dom" |
48 unfolding dom_def [abs_def] is_none_def [symmetric] by transfer_prover |
48 unfolding dom_def [abs_def] Option.is_none_def [symmetric] by transfer_prover |
49 |
49 |
50 lemma map_of_parametric [transfer_rule]: |
50 lemma map_of_parametric [transfer_rule]: |
51 assumes [transfer_rule]: "bi_unique R1" |
51 assumes [transfer_rule]: "bi_unique R1" |
52 shows "(list_all2 (rel_prod R1 R2) ===> R1 ===> rel_option R2) map_of map_of" |
52 shows "(list_all2 (rel_prod R1 R2) ===> R1 ===> rel_option R2) map_of map_of" |
53 unfolding map_of_def by transfer_prover |
53 unfolding map_of_def by transfer_prover |
221 "lookup empty k = None" |
221 "lookup empty k = None" |
222 by transfer simp |
222 by transfer simp |
223 |
223 |
224 lemma keys_is_none_rep [code_unfold]: |
224 lemma keys_is_none_rep [code_unfold]: |
225 "k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))" |
225 "k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))" |
226 by transfer (auto simp add: is_none_def) |
226 by transfer (auto simp add: Option.is_none_def) |
227 |
227 |
228 lemma update_update: |
228 lemma update_update: |
229 "update k v (update k w m) = update k v m" |
229 "update k v (update k w m) = update k v m" |
230 "k \<noteq> l \<Longrightarrow> update k v (update l w m) = update l w (update k v m)" |
230 "k \<noteq> l \<Longrightarrow> update k v (update l w m) = update l w (update k v m)" |
231 by (transfer, simp add: fun_upd_twist)+ |
231 by (transfer, simp add: fun_upd_twist)+ |