Theory Collections.CollectionsV1
section ‹Backwards Compatibility for Version 1›
theory CollectionsV1
imports Collections
begin
text ‹
This theory defines some stuff to establish (partial) backwards
compatibility with ICF Version 1.
›
attribute_setup locale_witness_add = ‹
Scan.succeed (Locale.witness_add)
› "Add witness for locale instantiation. HACK, use
sublocale or interpretation whereever possible!"
subsection ‹Iterators›
text ‹We define all the monomorphic iterator locales›
subsubsection "Set"
locale set_iteratei = finite_set α invar for α :: "'s ⇒ 'x set" and invar +
fixes iteratei :: "'s ⇒ ('x, 'σ) set_iterator"
assumes iteratei_rule: "invar S ⟹ set_iterator (iteratei S) (α S)"
begin
lemma iteratei_rule_P:
"⟦
invar S;
I (α S) σ0;
!!x it σ. ⟦ c σ; x ∈ it; it ⊆ α S; I it σ ⟧ ⟹ I (it - {x}) (f x σ);
!!σ. I {} σ ⟹ P σ;
!!σ it. ⟦ it ⊆ α S; it ≠ {}; ¬ c σ; I it σ ⟧ ⟹ P σ
⟧ ⟹ P (iteratei S c f σ0)"
apply (rule set_iterator_rule_P [OF iteratei_rule, of S I σ0 c f P])
apply simp_all
done
lemma iteratei_rule_insert_P:
"⟦
invar S;
I {} σ0;
!!x it σ. ⟦ c σ; x ∈ α S - it; it ⊆ α S; I it σ ⟧ ⟹ I (insert x it) (f x σ);
!!σ. I (α S) σ ⟹ P σ;
!!σ it. ⟦ it ⊆ α S; it ≠ α S; ¬ c σ; I it σ ⟧ ⟹ P σ
⟧ ⟹ P (iteratei S c f σ0)"
apply (rule set_iterator_rule_insert_P [OF iteratei_rule, of S I σ0 c f P])
apply simp_all
done
text ‹Versions without break condition.›
lemma iterate_rule_P:
"⟦
invar S;
I (α S) σ0;
!!x it σ. ⟦ x ∈ it; it ⊆ α S; I it σ ⟧ ⟹ I (it - {x}) (f x σ);
!!σ. I {} σ ⟹ P σ
⟧ ⟹ P (iteratei S (λ_. True) f σ0)"
apply (rule set_iterator_no_cond_rule_P [OF iteratei_rule, of S I σ0 f P])
apply simp_all
done
lemma iterate_rule_insert_P:
"⟦
invar S;
I {} σ0;
!!x it σ. ⟦ x ∈ α S - it; it ⊆ α S; I it σ ⟧ ⟹ I (insert x it) (f x σ);
!!σ. I (α S) σ ⟹ P σ
⟧ ⟹ P (iteratei S (λ_. True) f σ0)"
apply (rule set_iterator_no_cond_rule_insert_P [OF iteratei_rule, of S I σ0 f P])
apply simp_all
done
end
lemma set_iteratei_I :
assumes "⋀s. invar s ⟹ set_iterator (iti s) (α s)"
shows "set_iteratei α invar iti"
proof
fix s
assume invar_s: "invar s"
from assms(1)[OF invar_s] show it_OK: "set_iterator (iti s) (α s)" .
from set_iterator_genord.finite_S0 [OF it_OK[unfolded set_iterator_def]]
show "finite (α s)" .
qed
locale set_iterateoi = ordered_finite_set α invar
for α :: "'s ⇒ ('u::linorder) set" and invar
+
fixes iterateoi :: "'s ⇒ ('u,'σ) set_iterator"
assumes iterateoi_rule:
"invar s ⟹ set_iterator_linord (iterateoi s) (α s)"
begin
lemma iterateoi_rule_P[case_names minv inv0 inv_pres i_complete i_inter]:
assumes MINV: "invar m"
assumes I0: "I (α m) σ0"
assumes IP: "!!k it σ. ⟦
c σ;
k ∈ it;
∀j∈it. k≤j;
∀j∈α m - it. j≤k;
it ⊆ α m;
I it σ
⟧ ⟹ I (it - {k}) (f k σ)"
assumes IF: "!!σ. I {} σ ⟹ P σ"
assumes II: "!!σ it. ⟦
it ⊆ α m;
it ≠ {};
¬ c σ;
I it σ;
∀k∈it. ∀j∈α m - it. j≤k
⟧ ⟹ P σ"
shows "P (iterateoi m c f σ0)"
using set_iterator_linord_rule_P [OF iterateoi_rule, OF MINV, of I σ0 c f P,
OF I0 _ IF] IP II
by simp
lemma iterateo_rule_P[case_names minv inv0 inv_pres i_complete]:
assumes MINV: "invar m"
assumes I0: "I ((α m)) σ0"
assumes IP: "!!k it σ. ⟦ k ∈ it; ∀j∈it. k≤j; ∀j∈(α m) - it. j≤k; it ⊆ (α m); I it σ ⟧
⟹ I (it - {k}) (f k σ)"
assumes IF: "!!σ. I {} σ ⟹ P σ"
shows "P (iterateoi m (λ_. True) f σ0)"
apply (rule iterateoi_rule_P [where I = I])
apply (simp_all add: assms)
done
end
lemma set_iterateoi_I :
assumes "⋀s. invar s ⟹ set_iterator_linord (itoi s) (α s)"
shows "set_iterateoi α invar itoi"
proof
fix s
assume invar_s: "invar s"
from assms(1)[OF invar_s] show it_OK: "set_iterator_linord (itoi s) (α s)" .
from set_iterator_genord.finite_S0 [OF it_OK[unfolded set_iterator_linord_def]]
show "finite (α s)" by simp
qed
locale set_reverse_iterateoi = ordered_finite_set α invar
for α :: "'s ⇒ ('u::linorder) set" and invar
+
fixes reverse_iterateoi :: "'s ⇒ ('u,'σ) set_iterator"
assumes reverse_iterateoi_rule: "
invar m ⟹ set_iterator_rev_linord (reverse_iterateoi m) (α m)"
begin
lemma reverse_iterateoi_rule_P[case_names minv inv0 inv_pres i_complete i_inter]:
assumes MINV: "invar m"
assumes I0: "I ((α m)) σ0"
assumes IP: "!!k it σ. ⟦
c σ;
k ∈ it;
∀j∈it. k≥j;
∀j∈(α m) - it. j≥k;
it ⊆ (α m);
I it σ
⟧ ⟹ I (it - {k}) (f k σ)"
assumes IF: "!!σ. I {} σ ⟹ P σ"
assumes II: "!!σ it. ⟦
it ⊆ (α m);
it ≠ {};
¬ c σ;
I it σ;
∀k∈it. ∀j∈(α m) - it. j≥k
⟧ ⟹ P σ"
shows "P (reverse_iterateoi m c f σ0)"
using set_iterator_rev_linord_rule_P [OF reverse_iterateoi_rule, OF MINV, of I σ0 c f P,
OF I0 _ IF] IP II
by simp
lemma reverse_iterateo_rule_P[case_names minv inv0 inv_pres i_complete]:
assumes MINV: "invar m"
assumes I0: "I ((α m)) σ0"
assumes IP: "!!k it σ. ⟦
k ∈ it;
∀j∈it. k≥j;
∀j∈ (α m) - it. j≥k;
it ⊆ (α m);
I it σ
⟧ ⟹ I (it - {k}) (f k σ)"
assumes IF: "!!σ. I {} σ ⟹ P σ"
shows "P (reverse_iterateoi m (λ_. True) f σ0)"
apply (rule reverse_iterateoi_rule_P [where I = I])
apply (simp_all add: assms)
done
end
lemma set_reverse_iterateoi_I :
assumes "⋀s. invar s ⟹ set_iterator_rev_linord (itoi s) (α s)"
shows "set_reverse_iterateoi α invar itoi"
proof
fix s
assume invar_s: "invar s"
from assms(1)[OF invar_s] show it_OK: "set_iterator_rev_linord (itoi s) (α s)" .
from set_iterator_genord.finite_S0 [OF it_OK[unfolded set_iterator_rev_linord_def]]
show "finite (α s)" by simp
qed
lemma (in poly_set_iteratei) v1_iteratei_impl:
"set_iteratei α invar iteratei"
by unfold_locales (rule iteratei_correct)
lemma (in poly_set_iterateoi) v1_iterateoi_impl:
"set_iterateoi α invar iterateoi"
by unfold_locales (rule iterateoi_correct)
lemma (in poly_set_rev_iterateoi) v1_reverse_iterateoi_impl:
"set_reverse_iterateoi α invar rev_iterateoi"
by unfold_locales (rule rev_iterateoi_correct)
declare (in poly_set_iteratei) v1_iteratei_impl[locale_witness_add]
declare (in poly_set_iterateoi) v1_iterateoi_impl[locale_witness_add]
declare (in poly_set_rev_iterateoi)
v1_reverse_iterateoi_impl[locale_witness_add]
subsubsection "Map"
locale map_iteratei = finite_map α invar for α :: "'s ⇒ 'u ⇀ 'v" and invar +
fixes iteratei :: "'s ⇒ ('u × 'v,'σ) set_iterator"
assumes iteratei_rule: "invar m ⟹ map_iterator (iteratei m) (α m)"
begin
lemma iteratei_rule_P:
assumes "invar 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 (iteratei m c f σ0)"
using map_iterator_rule_P [OF iteratei_rule, of m I σ0 c f P]
by (simp_all add: assms)
lemma iteratei_rule_insert_P:
assumes
"invar m"
"I {} σ0"
"!!k v it σ. ⟦ c σ; k ∈ (dom (α m) - it); α m k = Some v; it ⊆ dom (α m); I it σ ⟧
⟹ I (insert k it) (f (k, v) σ)"
"!!σ. I (dom (α m)) σ ⟹ P σ"
"!!σ it. ⟦ it ⊆ dom (α m); it ≠ dom (α m);
¬ (c σ);
I it σ ⟧ ⟹ P σ"
shows "P (iteratei m c f σ0)"
using map_iterator_rule_insert_P [OF iteratei_rule, of m I σ0 c f P]
by (simp_all add: assms)
lemma iterate_rule_P:
"⟦
invar m;
I (dom (α m)) σ0;
!!k v it σ. ⟦ k ∈ it; α m k = Some v; it ⊆ dom (α m); I it σ ⟧
⟹ I (it - {k}) (f (k, v) σ);
!!σ. I {} σ ⟹ P σ
⟧ ⟹ P (iteratei m (λ_. True) f σ0)"
using iteratei_rule_P [of m I σ0 "λ_. True" f P]
by fast
lemma iterate_rule_insert_P:
"⟦
invar m;
I {} σ0;
!!k v it σ. ⟦ k ∈ (dom (α m) - it); α m k = Some v; it ⊆ dom (α m); I it σ ⟧
⟹ I (insert k it) (f (k, v) σ);
!!σ. I (dom (α m)) σ ⟹ P σ
⟧ ⟹ P (iteratei m (λ_. True) f σ0)"
using iteratei_rule_insert_P [of m I σ0 "λ_. True" f P]
by fast
end
lemma map_iteratei_I :
assumes "⋀m. invar m ⟹ map_iterator (iti m) (α m)"
shows "map_iteratei α invar iti"
proof
fix m
assume invar_m: "invar m"
from assms(1)[OF invar_m] show it_OK: "map_iterator (iti m) (α m)" .
from set_iterator_genord.finite_S0 [OF it_OK[unfolded set_iterator_def]]
show "finite (dom (α m))" by (simp add: finite_map_to_set)
qed
locale map_iterateoi = ordered_finite_map α invar
for α :: "'s ⇒ ('u::linorder) ⇀ 'v" and invar
+
fixes iterateoi :: "'s ⇒ ('u × 'v,'σ) set_iterator"
assumes iterateoi_rule: "
invar m ⟹ map_iterator_linord (iterateoi m) (α m)"
begin
lemma iterateoi_rule_P[case_names minv inv0 inv_pres i_complete i_inter]:
assumes MINV: "invar m"
assumes I0: "I (dom (α m)) σ0"
assumes IP: "!!k v it σ. ⟦
c σ;
k ∈ it;
∀j∈it. k≤j;
∀j∈dom (α m) - it. j≤k;
α m k = Some v;
it ⊆ dom (α m);
I it σ
⟧ ⟹ I (it - {k}) (f (k, v) σ)"
assumes IF: "!!σ. I {} σ ⟹ P σ"
assumes II: "!!σ it. ⟦
it ⊆ dom (α m);
it ≠ {};
¬ c σ;
I it σ;
∀k∈it. ∀j∈dom (α m) - it. j≤k
⟧ ⟹ P σ"
shows "P (iterateoi m c f σ0)"
using map_iterator_linord_rule_P [OF iterateoi_rule, of m I σ0 c f P] assms
by simp
lemma iterateo_rule_P[case_names minv inv0 inv_pres i_complete]:
assumes MINV: "invar m"
assumes I0: "I (dom (α m)) σ0"
assumes IP: "!!k v it σ. ⟦ k ∈ it; ∀j∈it. k≤j; ∀j∈dom (α m) - it. j≤k; α m k = Some v; it ⊆ dom (α m); I it σ ⟧
⟹ I (it - {k}) (f (k, v) σ)"
assumes IF: "!!σ. I {} σ ⟹ P σ"
shows "P (iterateoi m (λ_. True) f σ0)"
using map_iterator_linord_rule_P [OF iterateoi_rule, of m I σ0 "λ_. True" f P] assms
by simp
end
lemma map_iterateoi_I :
assumes "⋀m. invar m ⟹ map_iterator_linord (itoi m) (α m)"
shows "map_iterateoi α invar itoi"
proof
fix m
assume invar_m: "invar m"
from assms(1)[OF invar_m] show it_OK: "map_iterator_linord (itoi m) (α m)" .
from set_iterator_genord.finite_S0 [OF it_OK[unfolded set_iterator_map_linord_def]]
show "finite (dom (α m))" by (simp add: finite_map_to_set)
qed
locale map_reverse_iterateoi = ordered_finite_map α invar
for α :: "'s ⇒ ('u::linorder) ⇀ 'v" and invar
+
fixes reverse_iterateoi :: "'s ⇒ ('u × 'v,'σ) set_iterator"
assumes reverse_iterateoi_rule: "
invar m ⟹ map_iterator_rev_linord (reverse_iterateoi m) (α m)"
begin
lemma reverse_iterateoi_rule_P[case_names minv inv0 inv_pres i_complete i_inter]:
assumes MINV: "invar m"
assumes I0: "I (dom (α m)) σ0"
assumes IP: "!!k v it σ. ⟦
c σ;
k ∈ it;
∀j∈it. k≥j;
∀j∈dom (α m) - it. j≥k;
α m k = Some v;
it ⊆ dom (α m);
I it σ
⟧ ⟹ I (it - {k}) (f (k, v) σ)"
assumes IF: "!!σ. I {} σ ⟹ P σ"
assumes II: "!!σ it. ⟦
it ⊆ dom (α m);
it ≠ {};
¬ c σ;
I it σ;
∀k∈it. ∀j∈dom (α m) - it. j≥k
⟧ ⟹ P σ"
shows "P (reverse_iterateoi m c f σ0)"
using map_iterator_rev_linord_rule_P [OF reverse_iterateoi_rule, of m I σ0 c f P] assms
by simp
lemma reverse_iterateo_rule_P[case_names minv inv0 inv_pres i_complete]:
assumes MINV: "invar m"
assumes I0: "I (dom (α m)) σ0"
assumes IP: "!!k v it σ. ⟦
k ∈ it;
∀j∈it. k≥j;
∀j∈dom (α m) - it. j≥k;
α m k = Some v;
it ⊆ dom (α m);
I it σ
⟧ ⟹ I (it - {k}) (f (k, v) σ)"
assumes IF: "!!σ. I {} σ ⟹ P σ"
shows "P (reverse_iterateoi m (λ_. True) f σ0)"
using map_iterator_rev_linord_rule_P[OF reverse_iterateoi_rule, of m I σ0 "λ_. True" f P] assms
by simp
end
lemma map_reverse_iterateoi_I :
assumes "⋀m. invar m ⟹ map_iterator_rev_linord (ritoi m) (α m)"
shows "map_reverse_iterateoi α invar ritoi"
proof
fix m
assume invar_m: "invar m"
from assms(1)[OF invar_m] show it_OK: "map_iterator_rev_linord (ritoi m) (α m)" .
from set_iterator_genord.finite_S0 [OF it_OK[unfolded set_iterator_map_rev_linord_def]]
show "finite (dom (α m))" by (simp add: finite_map_to_set)
qed
lemma (in poly_map_iteratei) v1_iteratei_impl:
"map_iteratei α invar iteratei"
by unfold_locales (rule iteratei_correct)
lemma (in poly_map_iterateoi) v1_iterateoi_impl:
"map_iterateoi α invar iterateoi"
by unfold_locales (rule iterateoi_correct)
lemma (in poly_map_rev_iterateoi) v1_reverse_iterateoi_impl:
"map_reverse_iterateoi α invar rev_iterateoi"
by unfold_locales (rule rev_iterateoi_correct)
declare (in poly_map_iteratei) v1_iteratei_impl[locale_witness_add]
declare (in poly_map_iterateoi) v1_iterateoi_impl[locale_witness_add]
declare (in poly_map_rev_iterateoi)
v1_reverse_iterateoi_impl[locale_witness_add]
subsection ‹Concrete Operation Names›
text ‹We define abbreviations to recover the ‹xx_op›-names›