Theory Collections.SetIndex
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
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