Theory Collections.SetIterator
section ‹\isaheader{Iterators over Finite Sets}›
theory SetIterator
imports
Automatic_Refinement.Misc
Automatic_Refinement.Foldi
begin
text ‹When reasoning about finite sets, it is often handy to be able to iterate over the elements
of the set. If the finite set is represented by a list, the @{term fold} operation can be used.
For general finite sets, the order of elements is not fixed though. Therefore, nondeterministic
iterators are introduced in this theory.›
subsection ‹General Iterators›
type_synonym ('x,'σ) set_iterator = "('σ⇒bool) ⇒ ('x⇒'σ⇒'σ) ⇒ 'σ ⇒ 'σ"
locale set_iterator_genord =
fixes iti::"('x,'σ) set_iterator"
and S0::"'x set"
and R::"'x ⇒ 'x ⇒ bool"
assumes foldli_transform:
"∃l0. distinct l0 ∧ S0 = set l0 ∧ sorted_wrt R l0 ∧ iti = foldli l0"
begin
text ‹Let's prove some trivial lemmata to show that the formalisation agrees with
the view of iterators described above.›
lemma set_iterator_weaken_R :
"(⋀x y. ⟦x ∈ S0; y ∈ S0; R x y⟧ ⟹ R' x y) ⟹
set_iterator_genord iti S0 R'"
by (metis set_iterator_genord.intro foldli_transform sorted_wrt_mono_rel)
lemma finite_S0 :
shows "finite S0"
by (metis finite_set foldli_transform)
lemma iti_stop_rule_cond :
assumes not_c: "¬(c σ)"
shows "iti c f σ = σ"
proof -
from foldli_transform obtain l0 where l0_props:
"iti c = foldli l0 c" by blast
with foldli_not_cond [of c σ l0 f, OF not_c]
show ?thesis by simp
qed
lemma iti_stop_rule_emp :
assumes S0_emp: "S0 = {}"
shows "iti c f σ = σ"
proof -
from foldli_transform obtain l0 where l0_props:
"S0 = set l0" "iti c = foldli l0 c" by blast
with foldli.simps(1) [of c f σ] S0_emp
show ?thesis by simp
qed
text ‹Reducing everything to folding is cumbersome. Let's
define a few high-level inference rules.›
lemma iteratei_rule_P:
assumes
"I S0 σ0"
"⋀S σ x. ⟦ c σ; x ∈ S; I S σ; S ⊆ S0;
∀y∈S - {x}. R x y; ∀y∈S0 - S. R y x⟧
⟹ I (S - {x}) (f x σ)"
"⋀σ. I {} σ ⟹ P σ"
"⋀σ S. ⟦ S ⊆ S0; S ≠ {}; ¬ c σ; I S σ;
∀x∈S. ∀y∈S0-S. R y x ⟧ ⟹ P σ"
shows "P (iti c f σ0)"
proof -
{ fix P I σ0 f
assume
I: "I S0 σ0" and
R: "⋀S σ x. ⟦c σ; x ∈ S; I S σ; S ⊆ S0; ∀y∈S-{x}. R x y⟧ ⟹ I (S - {x}) (f x σ)" and
C1: "I {} (iti c f σ0) ⟹ P" and
C2:"⋀S. ⟦S ⊆ S0; S ≠ {}; ¬ c (iti c f σ0); I S (iti c f σ0)⟧ ⟹ P"
from foldli_transform obtain l0 where l0_props:
"distinct l0" "S0 = set l0" "sorted_wrt R l0" "iti c = foldli l0 c" by auto
from I R
have "I {} (iti c f σ0) ∨
(∃S. S ⊆ S0 ∧ S ≠ {} ∧
¬ (c (iti c f σ0)) ∧
I S (iti c f σ0))"
unfolding l0_props using l0_props(1,3)
proof (induct l0 arbitrary: σ0)
case Nil thus ?case by simp
next
case (Cons x l0)
note ind_hyp = Cons(1)
note I_x_l0 = Cons(2)
note step = Cons(3)
from Cons(4) have dist_l0: "distinct l0" and x_nin_l0: "x ∉ set l0" by simp_all
from Cons(5) have R_l0: "∀y∈set l0. R x y" and
sort_l0: "sorted_wrt R l0" by simp_all
show ?case
proof (cases "c σ0")
case False
with I_x_l0 show ?thesis
apply (rule_tac disjI2)
apply (rule_tac exI[where x="set (x # l0)"])
apply (simp)
done
next
case True note c_σ0 = this
from step[of σ0 x "set (x # l0)"] I_x_l0 R_l0 c_σ0 x_nin_l0
have step': "I (set l0) (f x σ0)"
by (simp_all add: Ball_def)
from ind_hyp [OF step' step dist_l0 sort_l0]
have "I {} (foldli l0 c f (f x σ0)) ∨
(∃S. S ⊆ set l0 ∧ S ≠ {} ∧
¬ c (foldli l0 c f (f x σ0)) ∧ I S (foldli l0 c f (f x σ0)))"
by (fastforce)
thus ?thesis
by (simp add: c_σ0 subset_iff) metis
qed
qed
with C1 C2 have "P" by blast
} note aux = this
from assms
show ?thesis
apply (rule_tac aux [of "λS σ. I S σ ∧ (∀x∈S. ∀y∈S0-S. R y x)" σ0 f])
apply auto
done
qed
text ‹Instead of removing elements one by one from the invariant, adding them is sometimes more natural.›
lemma iteratei_rule_insert_P:
assumes pre :
"I {} σ0"
"⋀S σ x. ⟦ c σ; x ∈ S0 - S; I S σ; S ⊆ S0; ∀y∈(S0 - S) - {x}. R x y;
∀y∈S. R y x⟧
⟹ I (insert x S) (f x σ)"
"⋀σ. I S0 σ ⟹ P σ"
"⋀σ S. ⟦ S ⊆ S0; S ≠ S0;
¬ (c σ); I S σ; ∀x∈S0-S. ∀y∈S. R y x ⟧ ⟹ P σ"
shows "P (iti c f σ0)"
proof -
let ?I' = "λS σ. I (S0 - S) σ"
have pre1:
"!!σ S. ⟦ S ⊆ S0; S ≠ {}; ¬ (c σ); ?I' S σ;
∀x∈S. ∀y∈S0-S. R y x⟧ ⟹ P σ"
proof -
fix S σ
assume AA:
"S ⊆ S0" "S ≠ {}"
"¬ (c σ)"
"?I' S σ" "∀x∈S. ∀y∈S0-S. R y x"
with pre(4) [of "S0 - S"]
show "P σ" by auto
qed
have pre2 :"⋀x S σ. ⟦c σ; x ∈ S; S ⊆ S0; ?I' S σ; ∀y∈S - {x}. R x y; ∀y∈S0-S. R y x ⟧ ⟹ ?I' (S - {x}) (f x σ)"
proof -
fix x S σ
assume AA : "c σ" "x ∈ S" "S ⊆ S0" "?I' S σ" "∀y∈S - {x}. R x y" "∀y∈S0 - S. R y x"
from AA(2) AA(3) have "S0 - (S - {x}) = insert x (S0 - S)" "S0 - (S0 - S) = S" by auto
moreover
note pre(2) [of σ x "S0 - S"] AA
ultimately show "?I' (S - {x}) (f x σ)"
by auto
qed
show "P (iti c f σ0)"
apply (rule iteratei_rule_P [of ?I' σ0 c f P])
apply (simp add: pre)
apply (rule pre2) apply simp_all
apply (simp add: pre(3))
apply (simp add: pre1)
done
qed
text ‹Show that iti without interruption is related to fold›
lemma iti_fold:
assumes lc_f: "comp_fun_commute f"
shows "iti (λ_. True) f σ0 = Finite_Set.fold f σ0 S0"
proof (rule iteratei_rule_insert_P [where I = "λX σ'. σ' = Finite_Set.fold f σ0 X"])
fix S σ x
assume "x ∈ S0 - S" "S ⊆ S0" and σ_eq: "σ = Finite_Set.fold f σ0 S"
from finite_S0 ‹S ⊆ S0› have fin_S: "finite S" by (metis finite_subset)
from ‹x ∈ S0 - S› have x_nin_S: "x ∉ S" by simp
interpret comp_fun_commute: comp_fun_commute f
by (fact lc_f)
note fold_eq = comp_fun_commute.fold_insert [OF fin_S x_nin_S]
show "f x σ = Finite_Set.fold f σ0 (insert x S)"
by (simp add: fold_eq σ_eq)
qed simp_all
end
subsection ‹Iterators over Maps›
type_synonym ('k,'v,'σ) map_iterator = "('k×'v,'σ) set_iterator"
text ‹Iterator over the key-value pairs of a finite map are called iterators over maps.›
abbreviation "map_iterator_genord it m R ≡ set_iterator_genord it (map_to_set m) R"
subsection ‹Unordered Iterators›
text ‹Often one does not care about the order in which the elements are processed.
Therefore, the selection function can be set to not impose any further restrictings.
This leads to considerably simpler theorems.›
definition "set_iterator it S0 ≡ set_iterator_genord it S0 (λ_ _. True)"
abbreviation "map_iterator it m ≡ set_iterator it (map_to_set m)"
lemma set_iterator_intro :
"set_iterator_genord it S0 R ⟹ set_iterator it S0"
unfolding set_iterator_def
apply (rule set_iterator_genord.set_iterator_weaken_R [where R = R])
apply simp_all
done
lemma set_iterator_no_cond_rule_P:
"⟦ set_iterator it S0;
I S0 σ0;
!!S σ x. ⟦ x ∈ S; I S σ; S ⊆ S0 ⟧ ⟹ I (S - {x}) (f x σ);
!!σ. I {} σ ⟹ P σ
⟧ ⟹ P (it (λ_. True) f σ0)"
unfolding set_iterator_def
using set_iterator_genord.iteratei_rule_P [of it S0 "λ_ _. True" I σ0 "λ_. True" f P]
by simp
lemma set_iterator_no_cond_rule_insert_P:
"⟦ set_iterator it S0;
I {} σ0;
!!S σ x. ⟦ x ∈ S0 - S; I S σ; S ⊆ S0 ⟧ ⟹ I (insert x S) (f x σ);
!!σ. I S0 σ ⟹ P σ
⟧ ⟹ P (it (λ_. True) f σ0)"
unfolding set_iterator_def
using set_iterator_genord.iteratei_rule_insert_P [of it S0 "λ_ _. True" I σ0 "λ_. True" f P]
by simp
lemma set_iterator_rule_P:
"⟦ set_iterator it S0;
I S0 σ0;
!!S σ x. ⟦ c σ; x ∈ S; I S σ; S ⊆ S0 ⟧ ⟹ I (S - {x}) (f x σ);
!!σ. I {} σ ⟹ P σ;
!!σ S. S ⊆ S0 ⟹ S ≠ {} ⟹ ¬ c σ ⟹ I S σ ⟹ P σ
⟧ ⟹ P (it c f σ0)"
unfolding set_iterator_def
using set_iterator_genord.iteratei_rule_P [of it S0 "λ_ _. True" I σ0 c f P]
by simp
lemma set_iterator_rule_insert_P:
"⟦ set_iterator it S0;
I {} σ0;
!!S σ x. ⟦ c σ; x ∈ S0 - S; I S σ; S ⊆ S0 ⟧ ⟹ I (insert x S) (f x σ);
!!σ. I S0 σ ⟹ P σ;
!!σ S. S ⊆ S0 ⟹ S ≠ S0 ⟹ ¬ c σ ⟹ I S σ ⟹ P σ
⟧ ⟹ P (it c f σ0)"
unfolding set_iterator_def
using set_iterator_genord.iteratei_rule_insert_P [of it S0 "λ_ _. True" I σ0 c f P]
by simp
text‹The following rules is adapted for maps. Instead of a set of key-value pairs the invariant
now only sees the keys.›
lemma map_iterator_genord_rule_P:
assumes "map_iterator_genord it m R"
and I0: "I (dom m) σ0"
and IP: "!!k v it σ. ⟦ c σ; k ∈ it; m k = Some v; it ⊆ dom m; I it σ;
∀k' v'. k' ∈ it-{k} ∧ m k' = Some v' ⟶ R (k, v) (k', v');
∀k' v'. k' ∉ it ∧ m k' = Some v' ⟶ R (k', v') (k, v)⟧ ⟹
I (it - {k}) (f (k, v) σ)"
and IF: "!!σ. I {} σ ⟹ P σ"
and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ {}; ¬ c σ; I it σ;
∀k v k' v'. k ∉ it ∧ m k = Some v ∧ k' ∈ it ∧ m k' = Some v' ⟶
R (k, v) (k', v') ⟧ ⟹ P σ"
shows "P (it c f σ0)"
proof (rule set_iterator_genord.iteratei_rule_P [of it "map_to_set m" R "λS σ. I (fst ` S) σ" σ0 c f P])
show "map_iterator_genord it m R" by fact
next
show "I (fst ` map_to_set m) σ0" using I0 by (simp add: map_to_set_dom[symmetric])
next
fix σ
assume "I (fst ` {}) σ"
with IF show "P σ" by simp
next
fix σ S
assume "S ⊆ map_to_set m" "S ≠ {}" "¬ c σ" "I (fst ` S) σ"
and R_prop: "∀x∈S. ∀y∈map_to_set m - S. R y x"
let ?S' = "fst ` S"
show "P σ"
proof (rule II [where it = ?S'])
from ‹S ⊆ map_to_set m›
show "?S' ⊆ dom m"
unfolding map_to_set_dom
by auto
next
from ‹S ≠ {}› show "?S' ≠ {}" by auto
next
show "¬ (c σ)" by fact
next
show "I (fst ` S) σ" by fact
next
show "∀k v k' v'.
k ∉ fst ` S ∧
m k = Some v ∧
k' ∈ fst ` S ∧ m k' = Some v' ⟶
R (k, v) (k', v')"
proof (intro allI impI, elim conjE )
fix k v k' v'
assume pre_k: "k ∉ fst ` S" "m k = Some v"
assume pre_k': "k' ∈ fst ` S" "m k' = Some v'"
from ‹S ⊆ map_to_set m› pre_k'
have kv'_in: "(k', v') ∈ S"
unfolding map_to_set_def by auto
from ‹S ⊆ map_to_set m› pre_k
have kv_in: "(k, v) ∈ map_to_set m - S"
unfolding map_to_set_def
by (auto simp add: image_iff)
from R_prop kv_in kv'_in
show "R (k, v) (k',v')" by simp
qed
qed
next
fix σ S kv
assume "S ⊆ map_to_set m" "kv ∈ S" "c σ" and I_S': "I (fst ` S) σ" and
R_S: "∀kv'∈S - {kv}. R kv kv'" and
R_not_S: "∀kv'∈map_to_set m - S. R kv' kv"
let ?S' = "fst ` S"
obtain k v where kv_eq[simp]: "kv = (k, v)" by (rule prod.exhaust)
have "I (fst ` S - {k}) (f (k, v) σ)"
proof (rule IP)
show "c σ" by fact
next
from ‹kv ∈ S› show "k ∈ ?S'" by (auto simp add: image_iff Bex_def)
next
from ‹kv ∈ S› ‹S ⊆ map_to_set m›
have "kv ∈ map_to_set m" by auto
thus m_k_eq: "m k = Some v" unfolding map_to_set_def by simp
next
from ‹S ⊆ map_to_set m›
show S'_subset: "?S' ⊆ dom m"
unfolding map_to_set_dom
by auto
next
show "I (fst ` S) σ" by fact
next
from ‹S ⊆ map_to_set m› ‹kv ∈ S›
have S_simp: "{(k', v'). k' ∈ (fst ` S) - {k} ∧ m k' = Some v'} = S - {kv}"
unfolding map_to_set_def subset_iff
apply (auto simp add: image_iff Bex_def)
apply (metis option.inject)
done
from R_S[unfolded S_simp[symmetric]] R_not_S
show "∀k' v'. k' ∈ fst ` S - {k} ∧ m k' = Some v' ⟶
R (k, v) (k', v') "
by simp
next
from ‹S ⊆ map_to_set m› R_not_S
show "∀k' v'. k' ∉ fst ` S ∧ m k' = Some v' ⟶ R (k', v') (k, v)"
apply (simp add: Ball_def map_to_set_def subset_iff image_iff)
apply metis
done
qed
moreover
from ‹S ⊆ map_to_set m› ‹kv ∈ S›
have "fst ` (S - {kv}) = fst ` S - {k}"
apply (simp add: set_eq_iff image_iff Bex_def map_to_set_def subset_iff)
apply (metis option.inject)
done
ultimately show "I (fst ` (S - {kv})) (f kv σ)" by simp
qed
lemma map_iterator_genord_rule_insert_P:
assumes "map_iterator_genord it m R"
and I0: "I {} σ0"
and IP: "!!k v it σ. ⟦ c σ; k ∈ dom m - it; m k = Some v; it ⊆ dom m; I it σ;
∀k' v'. k' ∈ (dom m - it) - {k} ∧ m k' = Some v' ⟶ R (k, v) (k', v');
∀k' v'. k' ∈ it ∧ m k' = Some v' ⟶
R (k', v') (k, v)⟧ ⟹ I (insert k it) (f (k, v) σ)"
and IF: "!!σ. I (dom m) σ ⟹ P σ"
and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ dom m; ¬ c σ; I it σ;
∀k v k' v'. k ∈ it ∧ m k = Some v ∧ k' ∉ it ∧ m k' = Some v' ⟶
R (k, v) (k', v') ⟧ ⟹ P σ"
shows "P (it c f σ0)"
proof (rule map_iterator_genord_rule_P [of it m R "λS σ. I (dom m - S) σ"])
show "map_iterator_genord it m R" by fact
next
show "I (dom m - dom m) σ0" using I0 by simp
next
fix σ
assume "I (dom m - {}) σ"
with IF show "P σ" by simp
next
fix σ it
assume assms: "it ⊆ dom m" "it ≠ {}" "¬ c σ" "I (dom m - it) σ"
"∀k v k' v'. k ∉ it ∧ m k = Some v ∧ k' ∈ it ∧ m k' = Some v' ⟶
R (k, v) (k', v')"
from assms have "dom m - it ≠ dom m" by auto
with II[of "dom m - it" σ] assms
show "P σ"
apply (simp add: subset_iff dom_def)
apply (metis option.simps(2))
done
next
fix k v it σ
assume assms: "c σ" "k ∈ it" "m k = Some v" "it ⊆ dom m" "I (dom m - it) σ"
"∀k' v'. k' ∈ it - {k} ∧ m k' = Some v' ⟶ R (k, v) (k', v')"
"∀k' v'. k' ∉ it ∧ m k' = Some v' ⟶ R (k', v') (k, v)"
hence "insert k (dom m - it) = (dom m - (it - {k}))" "dom m - (dom m - it) = it" by auto
with assms IP[of σ k "dom m - it" v]
show "I (dom m - (it - {k})) (f (k, v) σ)" by (simp_all add: subset_iff)
qed
lemma map_iterator_rule_P:
assumes "map_iterator it m"
and I0: "I (dom m) σ0"
and IP: "!!k v it σ. ⟦ c σ; k ∈ it; m k = Some v; it ⊆ dom m; I it σ ⟧ ⟹ I (it - {k}) (f (k, v) σ)"
and IF: "!!σ. I {} σ ⟹ P σ"
and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ {}; ¬ c σ; I it σ ⟧ ⟹ P σ"
shows "P (it c f σ0)"
using assms map_iterator_genord_rule_P[of it m "λ_ _. True" I σ0 c f P]
unfolding set_iterator_def
by simp
lemma map_iterator_rule_insert_P:
assumes "map_iterator it m"
and I0: "I {} σ0"
and IP: "!!k v it σ. ⟦ c σ; k ∈ dom m - it; m k = Some v; it ⊆ dom m; I it σ ⟧ ⟹ I (insert k it) (f (k, v) σ)"
and IF: "!!σ. I (dom m) σ ⟹ P σ"
and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ dom m; ¬ c σ; I it σ ⟧ ⟹ P σ"
shows "P (it c f σ0)"
using assms map_iterator_genord_rule_insert_P[of it m "λ_ _. True" I σ0 c f P]
unfolding set_iterator_def
by simp
lemma map_iterator_no_cond_rule_P:
assumes "map_iterator it m"
and I0: "I (dom m) σ0"
and IP: "!!k v it σ. ⟦ k ∈ it; m k = Some v; it ⊆ dom m; I it σ ⟧ ⟹ I (it - {k}) (f (k, v) σ)"
and IF: "!!σ. I {} σ ⟹ P σ"
shows "P (it (λ_. True) f σ0)"
using assms map_iterator_genord_rule_P[of it m "λ_ _. True" I σ0 "λ_. True" f P]
unfolding set_iterator_def
by simp
lemma map_iterator_no_cond_rule_insert_P:
assumes "map_iterator it m"
and I0: "I {} σ0"
and IP: "!!k v it σ. ⟦ k ∈ dom m - it; m k = Some v; it ⊆ dom m; I it σ ⟧ ⟹ I (insert k it) (f (k, v) σ)"
and IF: "!!σ. I (dom m) σ ⟹ P σ"
shows "P (it (λ_. True) f σ0)"
using assms map_iterator_genord_rule_insert_P[of it m "λ_ _. True" I σ0 "λ_. True" f P]
unfolding set_iterator_def
by simp
subsection ‹Ordered Iterators›
text ‹Selecting according to a linear order is another case that is interesting.
Ordered iterators over maps, i.\,e.\ iterators over key-value pairs,
use an order on the keys.›
context linorder begin
definition "set_iterator_linord it S0
≡ set_iterator_genord it S0 (≤)"
definition "set_iterator_rev_linord it S0
≡ set_iterator_genord it S0 (≥)"
definition "set_iterator_map_linord it S0 ≡
set_iterator_genord it S0 (λ(k,_) (k',_). k≤k')"
definition "set_iterator_map_rev_linord it S0 ≡
set_iterator_genord it S0 (λ(k,_) (k',_). k≥k')"
abbreviation "map_iterator_linord it m ≡
set_iterator_map_linord it (map_to_set m)"
abbreviation "map_iterator_rev_linord it m ≡
set_iterator_map_rev_linord it (map_to_set m)"
lemma set_iterator_linord_rule_P:
"⟦ set_iterator_linord it S0;
I S0 σ0;
!!S σ x. ⟦ c σ; x ∈ S; I S σ; S ⊆ S0; ⋀x'. x' ∈ S0-S ⟹ x' ≤ x; ⋀x'. x' ∈ S ⟹ x ≤ x'⟧ ⟹ I (S - {x}) (f x σ);
!!σ. I {} σ ⟹ P σ;
!!σ S. S ⊆ S0 ⟹ S ≠ {} ⟹ (⋀x x'. ⟦x ∈ S; x' ∈ S0-S⟧ ⟹ x' ≤ x) ⟹ ¬ c σ ⟹ I S σ ⟹ P σ
⟧ ⟹ P (it c f σ0)"
unfolding set_iterator_linord_def
apply (rule set_iterator_genord.iteratei_rule_P [of it S0 "(≤)" I σ0 c f P])
apply (simp_all add: Ball_def)
apply (metis order_refl)
done
lemma set_iterator_linord_rule_insert_P:
"⟦ set_iterator_linord it S0;
I {} σ0;
!!S σ x. ⟦ c σ; x ∈ S0 - S; I S σ; S ⊆ S0; ⋀x'. x' ∈ S ⟹ x' ≤ x; ⋀x'. x' ∈ S0 - S ⟹ x ≤ x'⟧ ⟹ I (insert x S) (f x σ);
!!σ. I S0 σ ⟹ P σ;
!!σ S. S ⊆ S0 ⟹ S ≠ S0 ⟹ (⋀x x'. ⟦x ∈ S0-S; x' ∈ S⟧ ⟹ x' ≤ x) ⟹ ¬ c σ ⟹ I S σ ⟹ P σ
⟧ ⟹ P (it c f σ0)"
unfolding set_iterator_linord_def
apply (rule set_iterator_genord.iteratei_rule_insert_P [of it S0 "(≤)" I σ0 c f P])
apply (simp_all add: Ball_def)
apply (metis order_refl)
done
lemma set_iterator_rev_linord_rule_P:
"⟦ set_iterator_rev_linord it S0;
I S0 σ0;
!!S σ x. ⟦ c σ; x ∈ S; I S σ; S ⊆ S0; ⋀x'. x' ∈ S0-S ⟹ x ≤ x'; ⋀x'. x' ∈ S ⟹ x' ≤ x⟧ ⟹ I (S - {x}) (f x σ);
!!σ. I {} σ ⟹ P σ;
!!σ S. S ⊆ S0 ⟹ S ≠ {} ⟹ (⋀x x'. ⟦x ∈ S; x' ∈ S0-S⟧ ⟹ x ≤ x') ⟹ ¬ c σ ⟹ I S σ ⟹ P σ
⟧ ⟹ P (it c f σ0)"
unfolding set_iterator_rev_linord_def
apply (rule set_iterator_genord.iteratei_rule_P [of it S0 "(≥)" I σ0 c f P])
apply (simp_all add: Ball_def)
apply (metis order_refl)
done
lemma set_iterator_rev_linord_rule_insert_P:
"⟦ set_iterator_rev_linord it S0;
I {} σ0;
!!S σ x. ⟦ c σ; x ∈ S0 - S; I S σ; S ⊆ S0; ⋀x'. x' ∈ S ⟹ x ≤ x'; ⋀x'. x' ∈ S0 - S ⟹ x' ≤ x⟧ ⟹ I (insert x S) (f x σ);
!!σ. I S0 σ ⟹ P σ;
!!σ S. S ⊆ S0 ⟹ S ≠ S0 ⟹ (⋀x x'. ⟦x ∈ S0-S; x' ∈ S⟧ ⟹ x ≤ x') ⟹ ¬ c σ ⟹ I S σ ⟹ P σ
⟧ ⟹ P (it c f σ0)"
unfolding set_iterator_rev_linord_def
apply (rule set_iterator_genord.iteratei_rule_insert_P [of it S0 "(≥)" I σ0 c f P])
apply (simp_all add: Ball_def)
apply (metis order_refl)
done
lemma set_iterator_map_linord_rule_P:
"⟦ set_iterator_map_linord it S0;
I S0 σ0;
!!S σ k v. ⟦ c σ; (k, v) ∈ S; I S σ; S ⊆ S0; ⋀k' v'. (k', v') ∈ S0-S ⟹ k' ≤ k;
⋀k' v'. (k', v') ∈ S ⟹ k ≤ k'⟧ ⟹ I (S - {(k,v)}) (f (k,v) σ);
!!σ. I {} σ ⟹ P σ;
!!σ S. S ⊆ S0 ⟹ S ≠ {} ⟹ (⋀k v k' v'. ⟦(k, v) ∈ S0-S; (k', v') ∈ S⟧ ⟹ k ≤ k') ⟹
¬ c σ ⟹ I S σ ⟹ P σ
⟧ ⟹ P (it c f σ0)"
unfolding set_iterator_map_linord_def
apply (rule set_iterator_genord.iteratei_rule_P
[of it S0 "(λ(k,_) (k',_). k ≤ k')" I σ0 c f P])
apply simp_all
apply (auto simp add: Ball_def)
apply (metis order_refl)
apply metis
done
lemma set_iterator_map_linord_rule_insert_P:
"⟦ set_iterator_map_linord it S0;
I {} σ0;
!!S σ k v. ⟦ c σ; (k, v) ∈ S0 - S; I S σ; S ⊆ S0; ⋀k' v'. (k', v') ∈ S ⟹ k' ≤ k;
⋀k' v'. (k',v') ∈ S0 - S ⟹ k ≤ k'⟧ ⟹ I (insert (k,v) S) (f (k,v) σ);
!!σ. I S0 σ ⟹ P σ;
!!σ S. S ⊆ S0 ⟹ S ≠ S0 ⟹ (⋀k v k' v'. ⟦(k, v) ∈ S; (k', v') ∈ S0-S⟧ ⟹ k ≤ k') ⟹
¬ c σ ⟹ I S σ ⟹ P σ
⟧ ⟹ P (it c f σ0)"
unfolding set_iterator_map_linord_def
apply (rule set_iterator_genord.iteratei_rule_insert_P
[of it S0 "(λ(k,_) (k',_). k ≤ k')" I σ0 c f P])
apply simp_all
apply (auto simp add: Ball_def)
apply (metis order_refl)
apply metis
done
lemma set_iterator_map_rev_linord_rule_P:
"⟦ set_iterator_map_rev_linord it S0;
I S0 σ0;
!!S σ k v. ⟦ c σ; (k, v) ∈ S; I S σ; S ⊆ S0; ⋀k' v'. (k', v') ∈ S0-S ⟹ k ≤ k';
⋀k' v'. (k', v') ∈ S ⟹ k' ≤ k⟧ ⟹ I (S - {(k,v)}) (f (k,v) σ);
!!σ. I {} σ ⟹ P σ;
!!σ S. S ⊆ S0 ⟹ S ≠ {} ⟹ (⋀k v k' v'. ⟦(k, v) ∈ S0-S; (k', v') ∈ S⟧ ⟹ k' ≤ k) ⟹
¬ c σ ⟹ I S σ ⟹ P σ
⟧ ⟹ P (it c f σ0)"
unfolding set_iterator_map_rev_linord_def
apply (rule set_iterator_genord.iteratei_rule_P
[of it S0 "(λ(k,_) (k',_). k ≥ k')" I σ0 c f P])
apply simp_all
apply (auto simp add: Ball_def)
apply (metis order_refl)
apply metis
done
lemma set_iterator_map_rev_linord_rule_insert_P:
"⟦ set_iterator_map_rev_linord it S0;
I {} σ0;
!!S σ k v. ⟦ c σ; (k, v) ∈ S0 - S; I S σ; S ⊆ S0; ⋀k' v'. (k', v') ∈ S ⟹ k ≤ k';
⋀k' v'. (k',v') ∈ S0 - S ⟹ k' ≤ k⟧ ⟹ I (insert (k,v) S) (f (k,v) σ);
!!σ. I S0 σ ⟹ P σ;
!!σ S. S ⊆ S0 ⟹ S ≠ S0 ⟹ (⋀k v k' v'. ⟦(k, v) ∈ S; (k', v') ∈ S0-S⟧ ⟹ k' ≤ k) ⟹
¬ c σ ⟹ I S σ ⟹ P σ
⟧ ⟹ P (it c f σ0)"
unfolding set_iterator_map_rev_linord_def
apply (rule set_iterator_genord.iteratei_rule_insert_P
[of it S0 "(λ(k,_) (k',_). k ≥ k')" I σ0 c f P])
apply simp_all
apply (auto simp add: Ball_def)
apply (metis order_refl)
apply metis
done
lemma map_iterator_linord_rule_P:
assumes "map_iterator_linord it m"
and I0: "I (dom m) σ0"
and IP: "!!k v it σ. ⟦ c σ; k ∈ it; m k = Some v; it ⊆ dom m; I it σ;
⋀k'. k' ∈ it ⟹ k ≤ k';
⋀k'. k' ∈ (dom m)-it ⟹ k' ≤ k⟧ ⟹ I (it - {k}) (f (k, v) σ)"
and IF: "!!σ. I {} σ ⟹ P σ"
and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ {}; ¬ c σ; I it σ;
⋀k k'. ⟦k ∈ (dom m)-it; k' ∈ it⟧ ⟹ k ≤ k'⟧ ⟹ P σ"
shows "P (it c f σ0)"
using assms
unfolding set_iterator_map_linord_def
by (rule map_iterator_genord_rule_P) auto
lemma map_iterator_linord_rule_insert_P:
assumes "map_iterator_linord it m"
and I0: "I {} σ0"
and IP: "!!k v it σ. ⟦ c σ; k ∈ dom m - it; m k = Some v; it ⊆ dom m; I it σ;
⋀k'. k' ∈ (dom m - it) ⟹ k ≤ k';
⋀k'. k' ∈ it ⟹ k' ≤ k ⟧ ⟹ I (insert k it) (f (k, v) σ)"
and IF: "!!σ. I (dom m) σ ⟹ P σ"
and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ dom m; ¬ c σ; I it σ;
⋀k k'. ⟦k ∈ it; k' ∈ (dom m)-it⟧ ⟹ k ≤ k'⟧ ⟹ P σ"
shows "P (it c f σ0)"
using assms
unfolding set_iterator_map_linord_def
by (rule map_iterator_genord_rule_insert_P) auto
lemma map_iterator_rev_linord_rule_P:
assumes "map_iterator_rev_linord it m"
and I0: "I (dom m) σ0"
and IP: "!!k v it σ. ⟦ c σ; k ∈ it; m k = Some v; it ⊆ dom m; I it σ;
⋀k'. k' ∈ it ⟹ k' ≤ k;
⋀k'. k' ∈ (dom m)-it ⟹ k ≤ k'⟧ ⟹ I (it - {k}) (f (k, v) σ)"
and IF: "!!σ. I {} σ ⟹ P σ"
and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ {}; ¬ c σ; I it σ;
⋀k k'. ⟦k ∈ (dom m)-it; k' ∈ it⟧ ⟹ k' ≤ k⟧ ⟹ P σ"
shows "P (it c f σ0)"
using assms
unfolding set_iterator_map_rev_linord_def
by (rule map_iterator_genord_rule_P) auto
lemma map_iterator_rev_linord_rule_insert_P:
assumes "map_iterator_rev_linord it m"
and I0: "I {} σ0"
and IP: "!!k v it σ. ⟦ c σ; k ∈ dom m - it; m k = Some v; it ⊆ dom m; I it σ;
⋀k'. k' ∈ (dom m - it) ⟹ k' ≤ k;
⋀k'. k' ∈ it ⟹ k ≤ k'⟧ ⟹ I (insert k it) (f (k, v) σ)"
and IF: "!!σ. I (dom m) σ ⟹ P σ"
and II: "!!σ it. ⟦ it ⊆ dom m; it ≠ dom m; ¬ c σ; I it σ;
⋀k k'. ⟦k ∈ it; k' ∈ (dom m)-it⟧ ⟹ k' ≤ k⟧ ⟹ P σ"
shows "P (it c f σ0)"
using assms
unfolding set_iterator_map_rev_linord_def
by (rule map_iterator_genord_rule_insert_P) auto
end
subsection ‹Conversions to foldli›
lemma set_iterator_genord_foldli_conv :
"set_iterator_genord iti S R ⟷
(∃l0. distinct l0 ∧ S = set l0 ∧ sorted_wrt R l0 ∧ iti = foldli l0)"
unfolding set_iterator_genord_def by simp
lemma set_iterator_genord_I [intro] :
"⟦distinct l0; S = set l0; sorted_wrt R l0; iti = foldli l0⟧ ⟹
set_iterator_genord iti S R" unfolding set_iterator_genord_foldli_conv
by blast
lemma set_iterator_foldli_conv :
"set_iterator iti S ⟷
(∃l0. distinct l0 ∧ S = set l0 ∧ iti = foldli l0)"
unfolding set_iterator_def set_iterator_genord_def by simp
lemma set_iterator_I [intro] :
"⟦distinct l0; S = set l0; iti = foldli l0⟧ ⟹
set_iterator iti S"
unfolding set_iterator_foldli_conv
by blast
context linorder begin
lemma set_iterator_linord_foldli_conv :
"set_iterator_linord iti S ⟷
(∃l0. distinct l0 ∧ S = set l0 ∧ sorted l0 ∧ iti = foldli l0)"
unfolding set_iterator_linord_def set_iterator_genord_def by simp
lemma set_iterator_linord_I [intro] :
"⟦distinct l0; S = set l0; sorted l0; iti = foldli l0⟧ ⟹
set_iterator_linord iti S"
unfolding set_iterator_linord_foldli_conv
by blast
lemma set_iterator_rev_linord_foldli_conv :
"set_iterator_rev_linord iti S ⟷
(∃l0. distinct l0 ∧ S = set l0 ∧ sorted (rev l0) ∧ iti = foldli l0)"
unfolding set_iterator_rev_linord_def set_iterator_genord_def by simp
lemma set_iterator_rev_linord_I [intro] :
"⟦distinct l0; S = set l0; sorted (rev l0); iti = foldli l0⟧ ⟹
set_iterator_rev_linord iti S"
unfolding set_iterator_rev_linord_foldli_conv
by blast
end
lemma map_iterator_genord_foldli_conv :
"map_iterator_genord iti m R ⟷
(∃(l0::('k × 'v) list). distinct (map fst l0) ∧ m = map_of l0 ∧ sorted_wrt R l0 ∧ iti = foldli l0)"
proof -
{ fix l0 :: "('k × 'v) list"
assume dist: "distinct l0"
have "(map_to_set m = set l0) ⟷
(distinct (map fst l0) ∧
m = map_of l0)"
proof (cases "distinct (map fst l0)")
case True thus ?thesis by (metis map_of_map_to_set)
next
case False note not_dist_fst = this
with dist have "~(inj_on fst (set l0))" by (simp add: distinct_map)
hence "set l0 ≠ map_to_set m"
by (rule_tac notI) (simp add: map_to_set_def inj_on_def)
with not_dist_fst show ?thesis by simp
qed
}
thus ?thesis
unfolding set_iterator_genord_def distinct_map
by metis
qed
lemma map_iterator_genord_I [intro] :
"⟦distinct (map fst l0); m = map_of l0; sorted_wrt R l0; iti = foldli l0⟧ ⟹
map_iterator_genord iti m R"
unfolding map_iterator_genord_foldli_conv
by blast
lemma map_iterator_foldli_conv :
"map_iterator iti m ⟷
(∃l0. distinct (map fst l0) ∧ m = map_of l0 ∧ iti = foldli l0)"
unfolding set_iterator_def map_iterator_genord_foldli_conv
by simp
lemma map_iterator_I [intro] :
"⟦distinct (map fst l0); m = map_of l0; iti = foldli l0⟧ ⟹
map_iterator iti m"
unfolding map_iterator_foldli_conv
by blast
context linorder begin
lemma sorted_wrt_keys_map_fst:
"sorted_wrt (λ(k,_) (k',_). R k k') l = sorted_wrt R (map fst l)"
by (induct l) auto
lemma map_iterator_linord_foldli_conv :
"map_iterator_linord iti m ⟷
(∃l0. distinct (map fst l0) ∧ m = map_of l0 ∧ sorted (map fst l0) ∧ iti = foldli l0)"
unfolding set_iterator_map_linord_def map_iterator_genord_foldli_conv
by (simp add: sorted_wrt_keys_map_fst)
lemma map_iterator_linord_I [intro] :
"⟦distinct (map fst l0); m = map_of l0; sorted (map fst l0); iti = foldli l0⟧ ⟹
map_iterator_linord iti m"
unfolding map_iterator_linord_foldli_conv
by blast
lemma map_iterator_rev_linord_foldli_conv :
"map_iterator_rev_linord iti m ⟷
(∃l0. distinct (map fst l0) ∧ m = map_of l0 ∧ sorted (rev (map fst l0)) ∧ iti = foldli l0)"
unfolding set_iterator_map_rev_linord_def map_iterator_genord_foldli_conv
by (simp add: sorted_wrt_keys_map_fst)
lemma map_iterator_rev_linord_I [intro] :
"⟦distinct (map fst l0); m = map_of l0; sorted (rev (map fst l0)); iti = foldli l0⟧ ⟹
map_iterator_rev_linord iti m"
unfolding map_iterator_rev_linord_foldli_conv
by blast
end
end