Theory SetIteratorCollectionsGA

theory SetIteratorCollectionsGA
imports SetSpec MapSpec
(*  Title:       General Algorithms for Iterators
    Author:      Thomas Tuerk <tuerk@in.tum.de>
    Maintainer:  Thomas Tuerk <tuerk@in.tum.de>
*)
header {* 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