Theory SetIndex

(*  Title:       Isabelle Collections Library
    Author:      Peter Lammich <peter dot lammich at uni-muenster.de>
    Maintainer:  Peter Lammich <peter dot lammich at uni-muenster.de>
*)
section ‹\isaheader{Indices of Sets}›
theory SetIndex
imports 
  "../spec/MapSpec"
  "../spec/SetSpec"
begin
text_raw ‹\label{thy:SetIndex}›

text ‹
  This theory defines an indexing operation that builds an index from a set 
  and an indexing function. 

  Here, index is a map from indices to all values of the set with that index.
›

subsection "Indexing by Function"

definition index :: "('a ⇒ 'i) ⇒ 'a set ⇒ 'i ⇒ 'a set"
  where "index f s i == { x∈s . f x = i }"

lemma indexI: "⟦ x∈s; f x = i ⟧ ⟹ x∈index f s i" by (unfold index_def) auto
lemma indexD: 
  "x∈index f s i ⟹ x∈s"
  "x∈index f s i ⟹ f x = i"
  by (unfold index_def) auto

lemma index_iff[simp]: "x∈index f s i ⟷ x∈s ∧ f x = i" by (simp add: index_def)
 
subsection "Indexing by Map"

definition index_map :: "('a ⇒ 'i) ⇒ 'a set ⇒ 'i ⇀ 'a set"
  where "index_map f s i == let s=index f s i in if s={} then None else Some s"

definition im_α where "im_α im i == case im i of None ⇒ {} | Some s ⇒ s"

lemma index_map_correct: "im_α (index_map f s) = index f s"
  apply (rule ext)
  apply (unfold index_def index_map_def im_α_def)
  apply auto
  done

subsection "Indexing by Maps and Sets from the Isabelle Collections Framework"
text ‹
  In this theory, we define the generic algorithm as constants outside any locale,
  but prove the correctness lemmas inside a locale that assumes correctness of all
  prerequisite functions.
  Finally, we export the correctness lemmas from the locale.
›

locale index_loc = 
  m: StdMap m_ops +
  s: StdSet s_ops
  for m_ops :: "('i,'s,'m,'more1) map_ops_scheme"
  and s_ops :: "('x,'s,'more2) set_ops_scheme"
begin
  ― ‹Mapping indices to abstract indices›
  definition ci_α' where
    "ci_α' ci i == case m.α ci i of None ⇒ None | Some s ⇒ Some (s.α s)"

  definition "ci_α == im_α ∘ ci_α'"

  definition ci_invar where
    "ci_invar ci == m.invar ci ∧ (∀i s. m.α ci i = Some s ⟶ s.invar s)"

  lemma ci_impl_minvar: "ci_invar m ⟹ m.invar m" by (unfold ci_invar_def) auto

  definition is_index :: "('x ⇒ 'i) ⇒ 'x set ⇒ 'm ⇒ bool"
  where
    "is_index f s idx == ci_invar idx ∧ ci_α' idx = index_map f s"

  lemma is_index_invar: "is_index f s idx ⟹ ci_invar idx" 
    by (simp add: is_index_def)

  lemma is_index_correct: "is_index f s idx ⟹ ci_α idx = index f s"
    by (simp only: is_index_def index_map_def ci_α_def)
       (simp add: index_map_correct)

  definition lookup :: "'i ⇒ 'm ⇒ 's" where
    "lookup i m == case m.lookup i m of None ⇒ (s.empty ()) | Some s ⇒ s"

  lemma lookup_invar': "ci_invar m ⟹ s.invar (lookup i m)"
    apply (unfold ci_invar_def lookup_def)
    apply (auto split: option.split simp add: m.lookup_correct s.empty_correct)
    done

  lemma lookup_correct:
    assumes I[simp, intro!]: "is_index f s idx"
    shows 
      "s.α (lookup i idx) = index f s i"
      "s.invar (lookup i idx)"
  proof goal_cases
    case 2 thus ?case using I by (simp add: is_index_def lookup_invar')
  next
    case 1 
    have [simp, intro!]: "m.invar idx" 
      using ci_impl_minvar[OF is_index_invar[OF I]] 
      by simp
    thus ?case 
    proof (cases "m.lookup i idx")
      case None
      hence [simp]: "m.α idx i = None" by (simp add: m.lookup_correct)
      from is_index_correct[OF I] have "index f s i = ci_α idx i" by simp
      also have "… = {}" by (simp add: ci_α_def ci_α'_def im_α_def)
      finally show ?thesis by (simp add: lookup_def None s.empty_correct)
    next
      case (Some si)
      hence [simp]: "m.α idx i = Some si" by (simp add: m.lookup_correct)
      from is_index_correct[OF I] have "index f s i = ci_α idx i" by simp
      also have "… = s.α si" by (simp add: ci_α_def ci_α'_def im_α_def)
      finally show ?thesis by (simp add: lookup_def Some s.empty_correct)
    qed
  qed

end

locale build_index_loc = index_loc m_ops s_ops +
  t: StdSet t_ops
  for m_ops :: "('i,'s,'m,'more1) map_ops_scheme"
  and s_ops :: "('x,'s,'more3) set_ops_scheme"
  and t_ops :: "('x,'t,'more2) set_ops_scheme"
begin

  text "Building indices"
  definition idx_build_stepfun :: "('x ⇒ 'i) ⇒ 'x ⇒ 'm ⇒ 'm" where
    "idx_build_stepfun f x m == 
      let i=f x in
        (case m.lookup i m of
          None ⇒ m.update i (s.ins x (s.empty ())) m |
          Some s ⇒ m.update i (s.ins x s) m
      )"

  definition idx_build :: "('x ⇒ 'i) ⇒ 't ⇒ 'm" where
    "idx_build f t == t.iterate t (idx_build_stepfun f) (m.empty ())"

  lemma idx_build_correct:
    assumes I: "t.invar t"
    shows "ci_α' (idx_build f t) = index_map f (t.α t)" (is ?T1) and
    [simp]: "ci_invar (idx_build f t)" (is ?T2)
  proof -
    have "t.invar t ⟹ 
      ci_α' (idx_build f t) = index_map f (t.α t) ∧ ci_invar (idx_build f t)"
      apply (unfold idx_build_def)
      apply (rule_tac 
          I="λit m. ci_α' m = index_map f (t.α t - it) ∧ ci_invar m" 
          in t.iterate_rule_P)
      apply assumption
      apply (simp add: ci_invar_def m.empty_correct)
      apply (rule ext)
      apply (unfold ci_α'_def index_map_def index_def)[1]
      apply (simp add: m.empty_correct)
      defer
      apply simp
      apply (rule conjI)
      defer
      apply (unfold idx_build_stepfun_def)[1]
      apply (auto 
        simp add: ci_invar_def m.update_correct m.lookup_correct 
                  s.empty_correct s.ins_correct Let_def 
        split: option.split) [1]
        
      apply (rule ext)
    proof goal_cases
      case prems: (1 x it m i)
      hence INV[simp, intro!]: "m.invar m" by (simp add: ci_invar_def)
      from prems have 
        INVS[simp, intro]: "!!q s. m.α m q = Some s ⟹ s.invar s" 
        by (simp add: ci_invar_def)
      
      show ?case proof (cases "i=f x")
        case [simp]: True
        show ?thesis proof (cases "m.α m (f x)")
          case [simp]: None
          hence "idx_build_stepfun f x m = m.update i (s.ins x (s.empty ())) m"
            apply (unfold idx_build_stepfun_def) 
            apply (simp add: m.update_correct m.lookup_correct s.empty_correct)
            done
          hence "ci_α' (idx_build_stepfun f x m) i = Some {x}"
            by (simp add: m.update_correct 
                          s.ins_correct s.empty_correct ci_α'_def)
          also {
            have "None = ci_α' m (f x)" 
              by (simp add: ci_α'_def)
            also from prems(4) have "… = index_map f (t.α t - it) i" by simp
            finally have E: "{xa ∈ t.α t - it. f xa = i} = {}" 
              by (simp add: index_map_def index_def split: if_split_asm)
            moreover have 
              "{xa ∈ t.α t - (it - {x}). f xa = i} 
               = {xa ∈ t.α t - it. f xa = i} ∪ {x}"
              using prems(2,3) by auto
            ultimately have "Some {x} = index_map f (t.α t - (it - {x})) i"
              by (unfold index_map_def index_def) auto
          } finally show ?thesis .
        next
          case [simp]: (Some ss)
          hence [simp, intro!]: "s.invar ss" by (simp del: Some)
          hence "idx_build_stepfun f x m = m.update (f x) (s.ins x ss) m"
            by (unfold idx_build_stepfun_def) 
               (simp add: m.update_correct m.lookup_correct)
          hence "ci_α' (idx_build_stepfun f x m) i = Some (insert x (s.α ss))"
            by (simp add: m.update_correct s.ins_correct ci_α'_def)
          also {
              have "Some (s.α ss) = ci_α' m (f x)" 
                by (simp add: ci_α'_def)
            also from prems(4) have "… = index_map f (t.α t - it) i" by simp
            finally have E: "{xa ∈ t.α t - it. f xa = i} = s.α ss" 
              by (simp add: index_map_def index_def split: if_split_asm)
            moreover have 
              "{xa ∈ t.α t - (it - {x}). f xa = i} 
               = {xa ∈ t.α t - it. f xa = i} ∪ {x}"
              using prems(2,3) by auto
            ultimately have 
              "Some (insert x (s.α ss)) = index_map f (t.α t - (it - {x})) i"
              by (unfold index_map_def index_def) auto
          }
          finally show ?thesis .
        qed
      next
        case False hence C: "i≠f x" "f x≠i" by simp_all
        have "ci_α' (idx_build_stepfun f x m) i = ci_α' m i"
          apply (unfold ci_α'_def idx_build_stepfun_def)
          apply (simp 
            split: option.split_asm option.split 
            add: Let_def m.lookup_correct m.update_correct 
                 s.ins_correct s.empty_correct C)
          done
        also from prems(4) have "ci_α' m i = index_map f (t.α t - it) i" 
          by simp
        also have 
          "{xa ∈ t.α t - (it - {x}). f xa = i} = {xa ∈ t.α t - it. f xa = i}"
          using prems(2,3) C by auto
        hence "index_map f (t.α t - it) i = index_map f (t.α t - (it-{x})) i"
          by (unfold index_map_def index_def) simp
        finally show ?thesis .
      qed
    qed
    with I show ?T1 ?T2 by auto
  qed

  lemma idx_build_is_index: 
    "t.invar t ⟹ is_index f (t.α t) (idx_build f t)"
    by (simp add: idx_build_correct index_map_correct ci_α_def is_index_def)

end

end