header {* \isaheader{Indices of Sets} *}
theory SetIndex
imports
"../common/Misc"
"../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 \<rightharpoonup> '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.
*}
-- "Lookup"
definition idx_lookup :: "_ => _ => 'i => 'm => 't" where
"idx_lookup mlookup tempty i m == case mlookup i m of None => (tempty ()) | Some s => s"
locale index_env =
m: map_lookup mα minvar mlookup +
t: set_empty tα tinvar tempty
for mα :: "'m => 'i \<rightharpoonup> 't" and minvar mlookup
and tα :: "'t => 'x set" and tinvar tempty
begin
-- "Mapping indices to abstract indices"
definition ci_α' where
"ci_α' ci i == case mα ci i of None => None | Some s => Some (tα s)"
definition "ci_α == im_α o ci_α'"
definition ci_invar where
"ci_invar ci == minvar ci ∧ (∀i s. mα ci i = Some s --> tinvar s)"
lemma ci_impl_minvar: "ci_invar m ==> minvar 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 (unfold is_index_def index_map_def ci_α_def)
(simp add: index_map_correct)
abbreviation "lookup == idx_lookup mlookup tempty"
lemma lookup_invar': "ci_invar m ==> tinvar (lookup i m)"
apply (unfold ci_invar_def idx_lookup_def)
apply (auto split: option.split simp add: m.lookup_correct t.empty_correct)
done
lemma lookup_correct:
assumes I[simp, intro!]: "is_index f s idx"
shows
"tα (lookup i idx) = index f s i"
"tinvar (lookup i idx)"
proof -
case goal2 thus ?case using I by (simp add: is_index_def lookup_invar')
next
case goal1
have [simp, intro!]: "minvar idx"
using ci_impl_minvar[OF is_index_invar[OF I]]
by simp
thus ?case
proof (cases "mlookup 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: idx_lookup_def None t.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 "… = tα si" by (simp add: ci_α_def ci_α'_def im_α_def)
finally show ?thesis by (simp add: idx_lookup_def Some t.empty_correct)
qed
qed
end
-- "Building indices"
definition idx_build_stepfun :: "
('i => 'm \<rightharpoonup> 't) =>
('i => 't => 'm => 'm) =>
(unit => 't) =>
('x => 't => 't) =>
('x => 'i) => 'x => 'm => 'm" where
"idx_build_stepfun mlookup mupdate tempty tinsert f x m ==
let i=f x in
(case mlookup i m of
None => mupdate i (tinsert x (tempty ())) m |
Some s => mupdate i (tinsert x s) m
)"
definition idx_build :: "
(unit => 'm) =>
('i => 'm \<rightharpoonup> 't) =>
('i => 't => 'm => 'm) =>
(unit => 't) =>
('x => 't => 't) =>
('s => ('x,'m) set_iterator) =>
('x => 'i) => 's => 'm" where
"idx_build mempty mlookup mupdate tempty tinsert siterate f s
== siterate s (λ_. True)
(idx_build_stepfun mlookup mupdate tempty tinsert f)
(mempty ())"
locale idx_build_env =
index_env mα minvar mlookup tα tinvar tempty +
m: map_empty mα minvar mempty +
m: map_update mα minvar mupdate +
t: set_ins tα tinvar tinsert +
s: set_iteratei sα sinvar siterate
for mα :: "'m => 'i \<rightharpoonup> 't" and minvar mempty mlookup mupdate
and tα :: "'t => 'x set" and tinvar tempty tinsert
and sα :: "'s => 'x set" and sinvar
and siterate :: "'s => ('x,'m) set_iterator"
begin
abbreviation "idx_build_stepfun' == idx_build_stepfun mlookup mupdate tempty tinsert"
abbreviation "idx_build' ==
idx_build mempty mlookup mupdate tempty tinsert siterate"
lemma idx_build_correct':
assumes I: "sinvar s"
shows "ci_α' (idx_build' f s) = index_map f (sα s)" (is ?T1) and
[simp]: "ci_invar (idx_build' f s)" (is ?T2)
proof -
have "sinvar s ==>
ci_α' (idx_build' f s) = index_map f (sα s) ∧ ci_invar (idx_build' f s)"
apply (unfold idx_build_def)
apply (rule_tac
I="λit m. ci_α' m = index_map f (sα s - it) ∧ ci_invar m"
in 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
t.empty_correct t.ins_correct Let_def
split: option.split) [1]
apply (rule ext)
proof -
case (goal1 x it m i)
hence INV[simp, intro!]: "minvar m" by (simp add: ci_invar_def)
from goal1 have
INVS[simp, intro]: "!!q s. mα m q = Some s ==> tinvar s"
by (simp add: ci_invar_def)
show ?case proof (cases "i=f x")
case True[simp]
show ?thesis proof (cases "mα m (f x)")
case None[simp]
hence "idx_build_stepfun' f x m = mupdate i (tinsert x (tempty ())) m"
apply (unfold idx_build_stepfun_def)
apply (simp add: m.update_correct m.lookup_correct t.empty_correct)
done
hence "ci_α' (idx_build_stepfun' f x m) i = Some {x}"
by (simp add: m.update_correct
t.ins_correct t.empty_correct ci_α'_def)
also {
have "None = ci_α' m (f x)"
by (simp add: ci_α'_def)
also from goal1(4) have "… = index_map f (sα s - it) i" by simp
finally have E: "{xa ∈ sα s - it. f xa = i} = {}"
by (simp add: index_map_def index_def split: split_if_asm)
moreover have
"{xa ∈ sα s - (it - {x}). f xa = i}
= {xa ∈ sα s - it. f xa = i} ∪ {x}"
using goal1(2,3) by auto
ultimately have "Some {x} = index_map f (sα s - (it - {x})) i"
by (unfold index_map_def index_def) auto
} finally show ?thesis .
next
case (Some ss)[simp]
hence [simp, intro!]: "tinvar ss" by (simp del: Some)
hence "idx_build_stepfun' f x m = mupdate (f x) (tinsert 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 (tα ss))"
by (simp add: m.update_correct t.ins_correct ci_α'_def)
also {
have "Some (tα ss) = ci_α' m (f x)"
by (simp add: ci_α'_def)
also from goal1(4) have "… = index_map f (sα s - it) i" by simp
finally have E: "{xa ∈ sα s - it. f xa = i} = tα ss"
by (simp add: index_map_def index_def split: split_if_asm)
moreover have
"{xa ∈ sα s - (it - {x}). f xa = i}
= {xa ∈ sα s - it. f xa = i} ∪ {x}"
using goal1(2,3) by auto
ultimately have
"Some (insert x (tα ss)) = index_map f (sα s - (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
t.ins_correct t.empty_correct C)
done
also from goal1(4) have "ci_α' m i = index_map f (sα s - it) i" by simp
also have
"{xa ∈ sα s - (it - {x}). f xa = i} = {xa ∈ sα s - it. f xa = i}"
using goal1(2,3) C by auto
hence "index_map f (sα s - it) i = index_map f (sα s - (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_correct:
"sinvar s ==> is_index f (sα s) (idx_build' f s)"
by (simp add: idx_build_correct' index_map_correct ci_α_def is_index_def)
end
subsubsection "Exported Correctness Lemmas and Definitions"
text {*
In order to allow simpler use, we
make the correctness lemmas visible outside the locale.
We also export the @{const [source] index_env.is_index} predicate.
*}
definition idx_invar
:: "('m => 'k \<rightharpoonup> 't) => ('m => bool)
=> ('t => 'v set) => ('t => bool)
=> ('v => 'k) => ('v set) => 'm => bool"
where
"idx_invar mα minvar tα tinvar == index_env.is_index mα minvar tα tinvar"
lemma idx_build_correct:
assumes "map_empty mα minvar mempty"
assumes "map_lookup mα minvar mlookup"
assumes "map_update mα minvar mupdate"
assumes "set_empty tα tinvar tempty"
assumes "set_ins tα tinvar tinsert"
assumes "set_iteratei sα sinvar siterate"
constrains mα :: "'m => 'i \<rightharpoonup> 't"
constrains tα :: "'t => 'x set"
constrains sα :: "'s => 'x set"
constrains siterate :: "'s => ('x,'m) set_iterator"
assumes INV: "sinvar S"
shows "idx_invar mα minvar tα tinvar f (sα S) (idx_build mempty mlookup mupdate tempty tinsert siterate f S)"
proof -
interpret m: map_empty mα minvar mempty by fact
interpret m: map_lookup mα minvar mlookup by fact
interpret m: map_update mα minvar mupdate by fact
interpret s: set_empty tα tinvar tempty by fact
interpret s: set_ins tα tinvar tinsert by fact
interpret t: set_iteratei sα sinvar siterate by fact
interpret idx_build_env
mα minvar mempty mlookup mupdate
tα tinvar tempty tinsert
sα sinvar siterate
by unfold_locales
from idx_build_correct[OF INV] show ?thesis
by (unfold idx_invar_def idx_build_def)
qed
lemma idx_lookup_correct:
assumes "map_lookup mα minvar mlookup"
assumes "set_empty tα tinvar tempty"
assumes INV: "idx_invar mα minvar tα tinvar f S idx"
shows "tα (idx_lookup mlookup tempty k idx) = index f S k" (is ?T1)
"tinvar (idx_lookup mlookup tempty k idx)" (is ?T2)
proof -
interpret m: map_lookup mα minvar mlookup by fact
interpret s: set_empty tα tinvar tempty by fact
interpret index_env
mα minvar mlookup
tα tinvar tempty
by unfold_locales
from lookup_correct[OF INV[unfolded idx_invar_def], of k] show ?T1 ?T2
by (simp_all add: idx_invar_def idx_lookup_def)
qed
end