Theory Collections.SetIteratorCollectionsGA

(*  Title:       General Algorithms for Iterators
    Author:      Thomas Tuerk <tuerk@in.tum.de>
    Maintainer:  Thomas Tuerk <tuerk@in.tum.de>
*)
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