Theory Collections.SetIteratorCollectionsGA
section ‹General Algorithms for Iterators over Finite Sets›
theory SetIteratorCollectionsGA
imports
"../spec/SetSpec"
"../spec/MapSpec"
begin
subsection ‹Iterate add to Set›
definition iterate_add_to_set where
"iterate_add_to_set s ins (it::('x,'x_set) set_iterator) =
it (λ_. True) (λx σ. ins x σ) s"
lemma iterate_add_to_set_correct :
assumes ins_OK: "set_ins α invar ins"
assumes s_OK: "invar s"
assumes it: "set_iterator it S0"
shows "α (iterate_add_to_set s ins it) = S0 ∪ α s ∧ invar (iterate_add_to_set s ins it)"
unfolding iterate_add_to_set_def
apply (rule set_iterator_no_cond_rule_insert_P [OF it,
where ?I="λS σ. α σ = S ∪ α s ∧ invar σ"])
apply (insert ins_OK s_OK)
apply (simp_all add: set_ins_def)
done
lemma iterate_add_to_set_dj_correct :
assumes ins_dj_OK: "set_ins_dj α invar ins_dj"
assumes s_OK: "invar s"
assumes it: "set_iterator it S0"
assumes dj: "S0 ∩ α s = {}"
shows "α (iterate_add_to_set s ins_dj it) = S0 ∪ α s ∧ invar (iterate_add_to_set s ins_dj it)"
unfolding iterate_add_to_set_def
apply (rule set_iterator_no_cond_rule_insert_P [OF it,
where ?I="λS σ. α σ = S ∪ α s ∧ invar σ"])
apply (insert ins_dj_OK s_OK dj)
apply (simp_all add: set_ins_dj_def set_eq_iff)
done
subsection ‹Iterator to Set›
definition iterate_to_set where
"iterate_to_set emp ins_dj (it::('x,'x_set) set_iterator) =
iterate_add_to_set (emp ()) ins_dj it"
lemma iterate_to_set_alt_def[code] :
"iterate_to_set emp ins_dj (it::('x,'x_set) set_iterator) =
it (λ_. True) (λx σ. ins_dj x σ) (emp ())"
unfolding iterate_to_set_def iterate_add_to_set_def by simp
lemma iterate_to_set_correct :
assumes ins_dj_OK: "set_ins_dj α invar ins_dj"
assumes emp_OK: "set_empty α invar emp"
assumes it: "set_iterator it S0"
shows "α (iterate_to_set emp ins_dj it) = S0 ∧ invar (iterate_to_set emp ins_dj it)"
unfolding iterate_to_set_def
using iterate_add_to_set_dj_correct [OF ins_dj_OK _ it, of "emp ()"] emp_OK
by (simp add: set_empty_def)
subsection ‹Iterate image/filter add to Set›
text ‹Iterators only visit element once. Therefore the image operations makes sense for
filters only if an injective function is used. However, when adding to a set using
non-injective functions is fine.›
lemma iterate_image_filter_add_to_set_correct :
assumes ins_OK: "set_ins α invar ins"
assumes s_OK: "invar s"
assumes it: "set_iterator it S0"
shows "α (iterate_add_to_set s ins (set_iterator_image_filter f it)) =
{b . ∃a. a ∈ S0 ∧ f a = Some b} ∪ α s ∧
invar (iterate_add_to_set s ins (set_iterator_image_filter f it))"
unfolding iterate_add_to_set_def set_iterator_image_filter_def
apply (rule set_iterator_no_cond_rule_insert_P [OF it,
where ?I="λS σ. α σ = {b . ∃a. a ∈ S ∧ f a = Some b} ∪ α s ∧ invar σ"])
apply (insert ins_OK s_OK)
apply (simp_all add: set_ins_def split: option.split)
apply auto
done
lemma iterate_image_filter_to_set_correct :
assumes ins_OK: "set_ins α invar ins"
assumes emp_OK: "set_empty α invar emp"
assumes it: "set_iterator it S0"
shows "α (iterate_to_set emp ins (set_iterator_image_filter f it)) =
{b . ∃a. a ∈ S0 ∧ f a = Some b} ∧
invar (iterate_to_set emp ins (set_iterator_image_filter f it))"
unfolding iterate_to_set_def
using iterate_image_filter_add_to_set_correct [OF ins_OK _ it, of "emp ()" f] emp_OK
by (simp add: set_empty_def)
text‹For completeness lets also consider injective versions.›
lemma iterate_inj_image_filter_add_to_set_correct :
assumes ins_dj_OK: "set_ins_dj α invar ins"
assumes s_OK: "invar s"
assumes it: "set_iterator it S0"
assumes dj: "{y. ∃x. x ∈ S0 ∧ f x = Some y} ∩ α s = {}"
assumes f_inj_on: "inj_on f (S0 ∩ dom f)"
shows "α (iterate_add_to_set s ins (set_iterator_image_filter f it)) =
{b . ∃a. a ∈ S0 ∧ f a = Some b} ∪ α s ∧
invar (iterate_add_to_set s ins (set_iterator_image_filter f it))"
proof -
from set_iterator_image_filter_correct [OF it f_inj_on]
have it_f: "set_iterator (set_iterator_image_filter f it)
{y. ∃x. x ∈ S0 ∧ f x = Some y}" by simp
from iterate_add_to_set_dj_correct [OF ins_dj_OK, OF s_OK it_f dj]
show ?thesis by auto
qed
lemma iterate_inj_image_filter_to_set_correct :
assumes ins_OK: "set_ins_dj α invar ins"
assumes emp_OK: "set_empty α invar emp"
assumes it: "set_iterator it S0"
assumes f_inj_on: "inj_on f (S0 ∩ dom f)"
shows "α (iterate_to_set emp ins (set_iterator_image_filter f it)) =
{b . ∃a. a ∈ S0 ∧ f a = Some b} ∧
invar (iterate_to_set emp ins (set_iterator_image_filter f it))"
unfolding iterate_to_set_def
using iterate_inj_image_filter_add_to_set_correct [OF ins_OK _ it _ f_inj_on, of "emp ()"] emp_OK
by (simp add: set_empty_def)
subsection ‹Iterate diff Set›
definition iterate_diff_set where
"iterate_diff_set s del (it::('x,'x_set) set_iterator) =
it (λ_. True) (λx σ. del x σ) s"
lemma iterate_diff_correct :
assumes del_OK: "set_delete α invar del"
assumes s_OK: "invar s"
assumes it: "set_iterator it S0"
shows "α (iterate_diff_set s del it) = α s - S0 ∧ invar (iterate_diff_set s del it)"
unfolding iterate_diff_set_def
apply (rule set_iterator_no_cond_rule_insert_P [OF it,
where ?I="λS σ. α σ = α s - S ∧ invar σ"])
apply (insert del_OK s_OK)
apply (auto simp add: set_delete_def set_eq_iff)
done
subsection ‹Iterate add to Map›
definition iterate_add_to_map where
"iterate_add_to_map m update (it::('k × 'v,'kv_map) set_iterator) =
it (λ_. True) (λ(k,v) σ. update k v σ) m"
lemma iterate_add_to_map_correct :
assumes upd_OK: "map_update α invar upd"
assumes m_OK: "invar m"
assumes it: "map_iterator it M"
shows "α (iterate_add_to_map m upd it) = α m ++ M ∧ invar (iterate_add_to_map m upd it)"
using assms
unfolding iterate_add_to_map_def
apply (rule_tac map_iterator_no_cond_rule_insert_P [OF it,
where ?I="λd σ. (α σ = α m ++ M |` d) ∧ invar σ"])
apply (simp_all add: map_update_def restrict_map_insert)
done
lemma iterate_add_to_map_dj_correct :
assumes upd_OK: "map_update_dj α invar upd"
assumes m_OK: "invar m"
assumes it: "map_iterator it M"
assumes dj: "dom M ∩ dom (α m) = {}"
shows "α (iterate_add_to_map m upd it) = α m ++ M ∧ invar (iterate_add_to_map m upd it)"
using assms
unfolding iterate_add_to_map_def
apply (rule_tac map_iterator_no_cond_rule_insert_P [OF it,
where ?I="λd σ. (α σ = α m ++ M |` d) ∧ invar σ"])
apply (simp_all add: map_update_dj_def restrict_map_insert set_eq_iff)
done
subsection ‹Iterator to Map›
definition iterate_to_map where
"iterate_to_map emp upd_dj (it::('k × 'v,'kv_map) set_iterator) =
iterate_add_to_map (emp ()) upd_dj it"
lemma iterate_to_map_alt_def[code] :
"iterate_to_map emp upd_dj it =
it (λ_. True) (λ(k, v) σ. upd_dj k v σ) (emp ())"
unfolding iterate_to_map_def iterate_add_to_map_def by simp
lemma iterate_to_map_correct :
assumes upd_dj_OK: "map_update_dj α invar upd_dj"
assumes emp_OK: "map_empty α invar emp"
assumes it: "map_iterator it M"
shows "α (iterate_to_map emp upd_dj it) = M ∧ invar (iterate_to_map emp upd_dj it)"
unfolding iterate_to_map_def
using iterate_add_to_map_dj_correct [OF upd_dj_OK _ it, of "emp ()"] emp_OK
by (simp add: map_empty_def)
end