Theory Collections.Algos

(*  Title:       Isabelle Collections Framework
    Author:      Peter Lammich <lammich at in.tum.de>
    Maintainer:  Peter Lammich <lammich at in.tum.de>
*)
section ‹\isaheader{More Generic Algorithms}›
theory Algos
imports 
  "../spec/SetSpec"
  "../spec/MapSpec"
  "../spec/ListSpec"
begin
text_raw ‹\label{thy:Algos}›
     

subsection "Injective Map to Naturals"

text "Whether a set is an initial segment of the natural numbers"
definition inatseg :: "nat set ⇒ bool" 
  where "inatseg s == ∃k. s = {i::nat. i<k}"

lemma inatseg_simps[simp]:
  "inatseg {}"
  "inatseg {0}"
  by (unfold inatseg_def)
    auto

text "Compute an injective map from objects into an initial 
    segment of the natural numbers"
locale map_to_nat_loc = 
  s: StdSet s_ops +
  m: StdMap m_ops
  for s_ops :: "('x,'s,'more1) set_ops_scheme"
  and m_ops :: "('x,nat,'m,'more2) map_ops_scheme"
begin

  definition map_to_nat 
    :: "'s ⇒ 'm" where
    "map_to_nat s ==
      snd (s.iterate s (λx (c,m). (c+1,m.update x c m)) (0,m.empty ()))"

  lemma map_to_nat_correct:
    assumes INV[simp]: "s.invar s"
    shows 
      ― ‹All elements have got a number›
      "dom (m.α (map_to_nat s)) = s.α s" (is ?T1) and
      ― ‹No two elements got the same number›
      [rule_format]: "inj_on (m.α (map_to_nat s)) (s.α s)" (is ?T2) and
      ― ‹Numbering is inatseg›
      [rule_format]: "inatseg (ran (m.α (map_to_nat s)))" (is ?T3) and
      ― ‹The result satisfies the map invariant›
      "m.invar (map_to_nat s)" (is ?T4)
    proof -
      have i_aux: "!!m S S' k v. ⟦inj_on m S; S' = insert k S; v∉ran m⟧ 
                                 ⟹ inj_on (m(k↦v)) S'"
        apply (rule inj_onI)
        apply (simp split: if_split_asm)
        apply (simp add: ran_def)
        apply (simp add: ran_def)
        apply blast
        apply (blast dest: inj_onD)
        done

      have "?T1 ∧ ?T2 ∧ ?T3 ∧ ?T4"
        apply (unfold map_to_nat_def)
        apply (rule_tac I="λit (c,m). 
          m.invar m ∧ 
          dom (m.α m) = s.α s - it ∧ 
          inj_on (m.α m) (s.α s - it) ∧ 
          (ran (m.α m) = {i. i<c})
          " in s.iterate_rule_P)
        apply simp
        apply (simp add: m.empty_correct)
        apply (case_tac σ)
        apply (simp add: m.empty_correct m.update_correct)
        apply (intro conjI)
        apply blast
        apply clarify
        apply (rule_tac m2="m.α ba" and 
                        k2=x and v2=aa and 
                        S'2="(s.α s - (it - {x}))" and 
                        S2="(s.α s - it)" 
                        in i_aux)
        apply auto [3]
        apply auto [1]
        apply (case_tac σ)
        apply (auto simp add: inatseg_def)
        done
      thus ?T1 ?T2 ?T3 ?T4 by auto
    qed
  
end

subsection "Map from Set"
text "Build a map using a set of keys and a function to compute the values."

locale it_dom_fun_to_map_loc =
  s: StdSet s_ops
+ m: StdMap m_ops 
  for s_ops :: "('k,'s,'more1) set_ops_scheme"
  and m_ops :: "('k,'v,'m,'more2) map_ops_scheme"
begin

  definition it_dom_fun_to_map ::
    "'s ⇒ ('k ⇒ 'v) ⇒ 'm"
    where "it_dom_fun_to_map s f == 
           s.iterate s (λk m. m.update_dj k (f k) m) (m.empty ())"

  lemma it_dom_fun_to_map_correct:
    assumes INV: "s.invar s"
    shows "m.α (it_dom_fun_to_map s f) k 
      = (if k ∈ s.α s then Some (f k) else None)" (is ?G1)
    and "m.invar (it_dom_fun_to_map s f)" (is ?G2)
  proof -
    have "m.α (it_dom_fun_to_map s f) k 
      = (if k ∈ s.α s then Some (f k) else None) ∧
      m.invar (it_dom_fun_to_map s f)"
      unfolding it_dom_fun_to_map_def
      apply (rule s.iterate_rule_P[where 
        I = "λit res. m.invar res 
        ∧ (∀k. m.α res k = (if (k ∈ (s.α s) - it) then Some (f k) else None))"
        ])
        apply (simp add: INV)

        apply (simp add: m.empty_correct)

        apply (subgoal_tac "x∉dom (m.α σ)")

        apply (auto simp: INV m.empty_correct m.update_dj_correct) []

        apply auto [2]
      done
    thus ?G1 and ?G2
      by auto
  qed

end


locale set_to_list_defs_loc =
  s: StdSetDefs s_ops
+ l: StdListDefs l_ops
  for s_ops :: "('x,'s,'more1) set_ops_scheme"
  and l_ops :: "('x,'l,'more2) list_ops_scheme"
begin
  definition "g_set_to_listl s ≡ s.iterate s l.appendl (l.empty ())"
  definition "g_set_to_listr s ≡ s.iterate s l.appendr (l.empty ())"
end

locale set_to_list_loc = set_to_list_defs_loc s_ops l_ops
+ s: StdSet s_ops
+ l: StdList l_ops
  for s_ops :: "('x,'s,'more1) set_ops_scheme"
  and l_ops :: "('x,'l,'more2) list_ops_scheme"
begin
  lemma g_set_to_listl_correct: 
    assumes I: "s.invar s"
    shows "List.set (l.α (g_set_to_listl s)) = s.α s"
    and "l.invar (g_set_to_listl s)"
    and "distinct (l.α (g_set_to_listl s))"
    using I apply -
    unfolding g_set_to_listl_def
    apply (rule_tac I="λit σ. l.invar σ ∧ List.set (l.α σ) = it 
      ∧ distinct (l.α σ)" 
      in s.iterate_rule_insert_P, auto simp: l.correct)+
    done

  lemma g_set_to_listr_correct: 
    assumes I: "s.invar s"
    shows "List.set (l.α (g_set_to_listr s)) = s.α s"
    and "l.invar (g_set_to_listr s)"
    and "distinct (l.α (g_set_to_listr s))"
    using I apply -
    unfolding g_set_to_listr_def
    apply (rule_tac I="λit σ. l.invar σ ∧ List.set (l.α σ) = it
      ∧ distinct (l.α σ)" 
      in s.iterate_rule_insert_P, auto simp: l.correct)+
    done

end

end