# Theory SetSpec

(*  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{Specification of Sets}›
theory SetSpec
imports ICF_Spec_Base
begin
text_raw‹\label{thy:SetSpec}›

(*@intf Set
@abstype 'a set
Sets
*)

text ‹
This theory specifies set operations by means of a mapping to
HOL's standard sets.
›

(* Drop some notation that gets in the way here*)
(*no_notation member (infixl "mem" 55)*)
notation insert ("set'_ins")

type_synonym ('x,'s) set_α = "'s ⇒ 'x set"
type_synonym ('x,'s) set_invar = "'s ⇒ bool"
locale set =
― ‹Abstraction to set›
fixes α :: "'s ⇒ 'x set"
― ‹Invariant›
fixes invar :: "'s ⇒ bool"

locale set_no_invar = set +
assumes invar[simp, intro!]: "⋀s. invar s"

subsection "Basic Set Functions"

subsubsection "Empty set"

locale set_empty = set +
constrains α :: "'s ⇒ 'x set"
fixes empty :: "unit ⇒ 's"
assumes empty_correct:
"α (empty ()) = {}"
"invar (empty ())"

subsubsection "Membership Query"

locale set_memb = set +
constrains α :: "'s ⇒ 'x set"
fixes memb :: "'x ⇒ 's ⇒ bool"
assumes memb_correct:
"invar s ⟹ memb x s ⟷ x ∈ α s"

subsubsection "Insertion of Element"

locale set_ins = set +
constrains α :: "'s ⇒ 'x set"
fixes ins :: "'x ⇒ 's ⇒ 's"
assumes ins_correct:
"invar s ⟹ α (ins x s) = set_ins x (α s)"
"invar s ⟹ invar (ins x s)"

subsubsection "Disjoint Insert"

locale set_ins_dj = set +
constrains α :: "'s ⇒ 'x set"
fixes ins_dj :: "'x ⇒ 's ⇒ 's"
assumes ins_dj_correct:
"⟦invar s; x∉α s⟧ ⟹ α (ins_dj x s) = set_ins x (α s)"
"⟦invar s; x∉α s⟧ ⟹ invar (ins_dj x s)"

subsubsection "Deletion of Single Element"

locale set_delete = set +
constrains α :: "'s ⇒ 'x set"
fixes delete :: "'x ⇒ 's ⇒ 's"
assumes delete_correct:
"invar s ⟹ α (delete x s) = α s - {x}"
"invar s ⟹ invar (delete x s)"

subsubsection "Emptiness Check"

locale set_isEmpty = set +
constrains α :: "'s ⇒ 'x set"
fixes isEmpty :: "'s ⇒ bool"
assumes isEmpty_correct:
"invar s ⟹ isEmpty s ⟷ α s = {}"

subsubsection "Bounded Quantifiers"

locale set_ball = set +
constrains α :: "'s ⇒ 'x set"
fixes ball :: "'s ⇒ ('x ⇒ bool) ⇒ bool"
assumes ball_correct: "invar S ⟹ ball S P ⟷ (∀x∈α S. P x)"

locale set_bex = set +
constrains α :: "'s ⇒ 'x set"
fixes bex :: "'s ⇒ ('x ⇒ bool) ⇒ bool"
assumes bex_correct: "invar S ⟹ bex S P ⟷ (∃x∈α S. P x)"

subsubsection "Finite Set"
locale finite_set = set +
assumes finite[simp, intro!]: "invar s ⟹ finite (α s)"

subsubsection "Size"

locale set_size = finite_set +
constrains α :: "'s ⇒ 'x set"
fixes size :: "'s ⇒ nat"
assumes size_correct:
"invar s ⟹ size s = card (α s)"

locale set_size_abort = finite_set +
constrains α :: "'s ⇒ 'x set"
fixes size_abort :: "nat ⇒ 's ⇒ nat"
assumes size_abort_correct:
"invar s ⟹ size_abort m s = min m (card (α s))"

subsubsection "Singleton sets"

locale set_sng = set +
constrains α :: "'s ⇒ 'x set"
fixes sng :: "'x ⇒ 's"
assumes sng_correct:
"α (sng x) = {x}"
"invar (sng x)"

locale set_isSng = set +
constrains α :: "'s ⇒ 'x set"
fixes isSng :: "'s ⇒ bool"
assumes isSng_correct:
"invar s ⟹ isSng s ⟷ (∃e. α s = {e})"
begin
lemma isSng_correct_exists1 :
"invar s ⟹ (isSng s ⟷ (∃!e. (e ∈ α s)))"
by (auto simp add: isSng_correct)

lemma isSng_correct_card :
"invar s ⟹ (isSng s ⟷ (card (α s) = 1))"
by (auto simp add: isSng_correct card_Suc_eq)
end

subsection "Iterators"
text ‹
An iterator applies a
function to a state and all the elements of the set.
The function is applied in any order. Proofs over the iteration are
done by establishing invariants over the iteration.
Iterators may have a break-condition, that interrupts the iteration before
the last element has been visited.
›

(* Deprecated *)
(*
locale set_iteratei = finite_set +
constrains α :: "'s ⇒ 'x set"
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
*)

type_synonym ('x,'s) set_list_it
= "'s ⇒ ('x,'x list) set_iterator"
locale poly_set_iteratei_defs =
fixes list_it :: "'s ⇒ ('x,'x list) set_iterator"
begin
definition iteratei :: "'s ⇒ ('x,'σ) set_iterator"
where "iteratei S ≡ it_to_it (list_it S)"
(*local_setup {* Locale_Code.lc_decl_del @{term iteratei} *}*)

abbreviation "iterate s ≡ iteratei s (λ_. True)"
end

locale poly_set_iteratei =
finite_set + poly_set_iteratei_defs list_it
for list_it :: "'s ⇒ ('x,'x list) set_iterator" +
constrains α :: "'s ⇒ 'x set"
assumes list_it_correct: "invar s ⟹ set_iterator (list_it s) (α s)"
begin
lemma iteratei_correct: "invar S ⟹ set_iterator (iteratei S) (α S)"
unfolding iteratei_def
apply (rule it_to_it_correct)
by (rule list_it_correct)

lemma pi_iteratei[icf_proper_iteratorI]:
"proper_it (iteratei S) (iteratei S)"
unfolding iteratei_def
by (intro icf_proper_iteratorI)

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_correct, 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_correct, 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_correct, 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_correct,
of S I σ0 f P])
apply simp_all
done

end

subsection "More Set Operations"

subsubsection "Copy"
locale set_copy = s1: set α1 invar1 + s2: set α2 invar2
for α1 :: "'s1 ⇒ 'a set" and invar1
and α2 :: "'s2 ⇒ 'a set" and invar2
+
fixes copy :: "'s1 ⇒ 's2"
assumes copy_correct:
"invar1 s1 ⟹ α2 (copy s1) = α1 s1"
"invar1 s1 ⟹ invar2 (copy s1)"

subsubsection "Union"

locale set_union = s1: set α1 invar1 + s2: set α2 invar2 + s3: set α3 invar3
for α1 :: "'s1 ⇒ 'a set" and invar1
and α2 :: "'s2 ⇒ 'a set" and invar2
and α3 :: "'s3 ⇒ 'a set" and invar3
+
fixes union :: "'s1 ⇒ 's2 ⇒ 's3"
assumes union_correct:
"invar1 s1 ⟹ invar2 s2 ⟹ α3 (union s1 s2) = α1 s1 ∪ α2 s2"
"invar1 s1 ⟹ invar2 s2 ⟹ invar3 (union s1 s2)"

locale set_union_dj =
s1: set α1 invar1 + s2: set α2 invar2 + s3: set α3 invar3
for α1 :: "'s1 ⇒ 'a set" and invar1
and α2 :: "'s2 ⇒ 'a set" and invar2
and α3 :: "'s3 ⇒ 'a set" and invar3
+
fixes union_dj :: "'s1 ⇒ 's2 ⇒ 's3"
assumes union_dj_correct:
"⟦invar1 s1; invar2 s2; α1 s1 ∩ α2 s2 = {}⟧ ⟹ α3 (union_dj s1 s2) = α1 s1 ∪ α2 s2"
"⟦invar1 s1; invar2 s2; α1 s1 ∩ α2 s2 = {}⟧ ⟹ invar3 (union_dj s1 s2)"

locale set_union_list = s1: set α1 invar1 + s2: set α2 invar2
for α1 :: "'s1 ⇒ 'a set" and invar1
and α2 :: "'s2 ⇒ 'a set" and invar2
+
fixes union_list :: "'s1 list ⇒ 's2"
assumes union_list_correct:
"∀s1∈set l. invar1 s1 ⟹ α2 (union_list l) = ⋃{α1 s1 |s1. s1 ∈ set l}"
"∀s1∈set l. invar1 s1 ⟹ invar2 (union_list l)"

subsubsection "Difference"

locale set_diff = s1: set α1 invar1 + s2: set α2 invar2
for α1 :: "'s1 ⇒ 'a set" and invar1
and α2 :: "'s2 ⇒ 'a set" and invar2
+
fixes diff :: "'s1 ⇒ 's2 ⇒ 's1"
assumes diff_correct:
"invar1 s1 ⟹ invar2 s2 ⟹ α1 (diff s1 s2) = α1 s1 - α2 s2"
"invar1 s1 ⟹ invar2 s2 ⟹ invar1 (diff s1 s2)"

subsubsection "Intersection"

locale set_inter = s1: set α1 invar1 + s2: set α2 invar2 + s3: set α3 invar3
for α1 :: "'s1 ⇒ 'a set" and invar1
and α2 :: "'s2 ⇒ 'a set" and invar2
and α3 :: "'s3 ⇒ 'a set" and invar3
+
fixes inter :: "'s1 ⇒ 's2 ⇒ 's3"
assumes inter_correct:
"invar1 s1 ⟹ invar2 s2 ⟹ α3 (inter s1 s2) = α1 s1 ∩ α2 s2"
"invar1 s1 ⟹ invar2 s2 ⟹ invar3 (inter s1 s2)"

subsubsection "Subset"

locale set_subset = s1: set α1 invar1 + s2: set α2 invar2
for α1 :: "'s1 ⇒ 'a set" and invar1
and α2 :: "'s2 ⇒ 'a set" and invar2
+
fixes subset :: "'s1 ⇒ 's2 ⇒ bool"
assumes subset_correct:
"invar1 s1 ⟹ invar2 s2 ⟹ subset s1 s2 ⟷ α1 s1 ⊆ α2 s2"

subsubsection "Equal"

locale set_equal = s1: set α1 invar1 + s2: set α2 invar2
for α1 :: "'s1 ⇒ 'a set" and invar1
and α2 :: "'s2 ⇒ 'a set" and invar2
+
fixes equal :: "'s1 ⇒ 's2 ⇒ bool"
assumes equal_correct:
"invar1 s1 ⟹ invar2 s2 ⟹ equal s1 s2 ⟷ α1 s1 = α2 s2"

subsubsection "Image and Filter"

locale set_image_filter = s1: set α1 invar1 + s2: set α2 invar2
for α1 :: "'s1 ⇒ 'a set" and invar1
and α2 :: "'s2 ⇒ 'b set" and invar2
+
fixes image_filter :: "('a ⇒ 'b option) ⇒ 's1 ⇒ 's2"
assumes image_filter_correct_aux:
"invar1 s ⟹ α2 (image_filter f s) = { b . ∃a∈α1 s. f a = Some b }"
"invar1 s ⟹ invar2 (image_filter f s)"
begin
― ‹This special form will be checked first by the simplifier:›
lemma image_filter_correct_aux2:
"invar1 s ⟹
α2 (image_filter (λx. if P x then (Some (f x)) else None) s)
= f  {x∈α1 s. P x}"
by (auto simp add: image_filter_correct_aux)

lemmas image_filter_correct =
image_filter_correct_aux2 image_filter_correct_aux

end

locale set_inj_image_filter = s1: set α1 invar1 + s2: set α2 invar2
for α1 :: "'s1 ⇒ 'a set" and invar1
and α2 :: "'s2 ⇒ 'b set" and invar2
+
fixes inj_image_filter :: "('a ⇒ 'b option) ⇒ 's1 ⇒ 's2"
assumes inj_image_filter_correct:
"⟦invar1 s; inj_on f (α1 s ∩ dom f)⟧ ⟹ α2 (inj_image_filter f s) = { b . ∃a∈α1 s. f a = Some b }"
"⟦invar1 s; inj_on f (α1 s ∩ dom f)⟧ ⟹ invar2 (inj_image_filter f s)"

subsubsection "Image"

locale set_image = s1: set α1 invar1 + s2: set α2 invar2
for α1 :: "'s1 ⇒ 'a set" and invar1
and α2 :: "'s2 ⇒ 'b set" and invar2
+
fixes image :: "('a ⇒ 'b) ⇒ 's1 ⇒ 's2"
assumes image_correct:
"invar1 s ⟹ α2 (image f s) = fα1 s"
"invar1 s ⟹ invar2 (image f s)"

locale set_inj_image = s1: set α1 invar1 + s2: set α2 invar2
for α1 :: "'s1 ⇒ 'a set" and invar1
and α2 :: "'s2 ⇒ 'b set" and invar2
+
fixes inj_image :: "('a ⇒ 'b) ⇒ 's1 ⇒ 's2"
assumes inj_image_correct:
"⟦invar1 s; inj_on f (α1 s)⟧ ⟹ α2 (inj_image f s) = fα1 s"
"⟦invar1 s; inj_on f (α1 s)⟧ ⟹ invar2 (inj_image f s)"

subsubsection "Filter"

locale set_filter = s1: set α1 invar1 + s2: set α2 invar2
for α1 :: "'s1 ⇒ 'a set" and invar1
and α2 :: "'s2 ⇒ 'a set" and invar2
+
fixes filter :: "('a ⇒ bool) ⇒ 's1 ⇒ 's2"
assumes filter_correct:
"invar1 s ⟹ α2 (filter P s) = {e. e ∈ α1 s ∧ P e}"
"invar1 s ⟹ invar2 (filter P s)"

subsubsection "Union of Set of Sets"

locale set_Union_image =
s1: set α1 invar1 + s2: set α2 invar2 + s3: set α3 invar3
for α1 :: "'s1 ⇒ 'a set" and invar1
and α2 :: "'s2 ⇒ 'b set" and invar2
and α3 :: "'s3 ⇒ 'b set" and invar3
+
fixes Union_image :: "('a ⇒ 's2) ⇒ 's1 ⇒ 's3"
assumes Union_image_correct:
"⟦ invar1 s; !!x. x∈α1 s ⟹ invar2 (f x) ⟧ ⟹
α3 (Union_image f s) = ⋃(α2fα1 s)"
"⟦ invar1 s; !!x. x∈α1 s ⟹ invar2 (f x) ⟧ ⟹ invar3 (Union_image f s)"

subsubsection "Disjointness Check"

locale set_disjoint = s1: set α1 invar1 + s2: set α2 invar2
for α1 :: "'s1 ⇒ 'a set" and invar1
and α2 :: "'s2 ⇒ 'a set" and invar2
+
fixes disjoint :: "'s1 ⇒ 's2 ⇒ bool"
assumes disjoint_correct:
"invar1 s1 ⟹ invar2 s2 ⟹ disjoint s1 s2 ⟷ α1 s1 ∩ α2 s2 = {}"

subsubsection "Disjointness Check With Witness"

locale set_disjoint_witness = s1: set α1 invar1 + s2: set α2 invar2
for α1 :: "'s1 ⇒ 'a set" and invar1
and α2 :: "'s2 ⇒ 'a set" and invar2
+
fixes disjoint_witness :: "'s1 ⇒ 's2 ⇒ 'a option"
assumes disjoint_witness_correct:
"⟦invar1 s1; invar2 s2⟧
⟹ disjoint_witness s1 s2 = None ⟹ α1 s1 ∩ α2 s2 = {}"
"⟦invar1 s1; invar2 s2; disjoint_witness s1 s2 = Some a⟧
⟹ a∈α1 s1 ∩ α2 s2"
begin
lemma disjoint_witness_None: "⟦invar1 s1; invar2 s2⟧
⟹ disjoint_witness s1 s2 = None ⟷ α1 s1 ∩ α2 s2 = {}"
by (case_tac "disjoint_witness s1 s2")
(auto dest: disjoint_witness_correct)

lemma disjoint_witnessI: "⟦
invar1 s1;
invar2 s2;
α1 s1 ∩ α2 s2 ≠ {};
!!a. ⟦disjoint_witness s1 s2 = Some a⟧ ⟹ P
⟧ ⟹ P"
by (case_tac "disjoint_witness s1 s2")
(auto dest: disjoint_witness_correct)

end

subsubsection "Selection of Element"

locale set_sel = set +
constrains α :: "'s ⇒ 'x set"
fixes sel :: "'s ⇒ ('x ⇒ 'r option) ⇒ 'r option"
assumes selE:
"⟦ invar s; x∈α s; f x = Some r;
!!x r. ⟦sel s f = Some r; x∈α s; f x = Some r ⟧ ⟹ Q
⟧ ⟹ Q"
assumes selI: "⟦invar s; ∀x∈α s. f x = None ⟧ ⟹ sel s f = None"
begin

lemma sel_someD:
"⟦ invar s; sel s f = Some r; !!x. ⟦x∈α s; f x = Some r⟧ ⟹ P ⟧ ⟹ P"
apply (cases "∃x∈α s. ∃r. f x = Some r")
apply (safe)
apply (erule_tac f=f and x=x in selE)
apply auto
apply (drule (1) selI)
apply simp
done

lemma sel_noneD:
"⟦ invar s; sel s f = None; x∈α s ⟧ ⟹ f x = None"
apply (cases "∃x∈α s. ∃r. f x = Some r")
apply (safe)
apply (erule_tac f=f and x=xa in selE)
apply auto
done
end

― ‹Selection of element (without mapping)›
locale set_sel' = set +
constrains α :: "'s ⇒ 'x set"
fixes sel' :: "'s ⇒ ('x ⇒ bool) ⇒ 'x option"
assumes sel'E:
"⟦ invar s; x∈α s; P x;
!!x. ⟦sel' s P = Some x; x∈α s; P x ⟧ ⟹ Q
⟧ ⟹ Q"
assumes sel'I: "⟦invar s; ∀x∈α s. ¬ P x ⟧ ⟹ sel' s P = None"
begin

lemma sel'_someD:
"⟦ invar s; sel' s P = Some x ⟧ ⟹ x∈α s ∧ P x"
apply (cases "∃x∈α s. P x")
apply (safe)
apply (erule_tac P=P and x=xa in sel'E)
apply auto
apply (erule_tac P=P and x=xa in sel'E)
apply auto
apply (drule (1) sel'I)
apply simp
apply (drule (1) sel'I)
apply simp
done

lemma sel'_noneD:
"⟦ invar s; sel' s P = None; x∈α s ⟧ ⟹ ¬P x"
apply (cases "∃x∈α s. P x")
apply (safe)
apply (erule_tac P=P and x=xa in sel'E)
apply auto
done
end

subsubsection "Conversion of Set to List"

locale set_to_list = set +
constrains α :: "'s ⇒ 'x set"
fixes to_list :: "'s ⇒ 'x list"
assumes to_list_correct:
"invar s ⟹ set (to_list s) = α s"
"invar s ⟹ distinct (to_list s)"

subsubsection "Conversion of List to Set"

locale list_to_set = set +
constrains α :: "'s ⇒ 'x set"
fixes to_set :: "'x list ⇒ 's"
assumes to_set_correct:
"α (to_set l) = set l"
"invar (to_set l)"

subsection "Ordered Sets"

locale ordered_set = set α invar
for α :: "'s ⇒ ('u::linorder) set" and invar

locale ordered_finite_set = finite_set α invar + ordered_set α invar
for α :: "'s ⇒ ('u::linorder) set" and invar

subsubsection "Ordered Iteration"
(* Deprecated *)
(*  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

(* Deprecated *)
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
*)

locale poly_set_iterateoi_defs =
fixes olist_it :: "'s ⇒ ('x,'x list) set_iterator"
begin
definition iterateoi :: "'s ⇒ ('x,'σ) set_iterator"
where "iterateoi S ≡ it_to_it (olist_it S)"
(*local_setup {* Locale_Code.lc_decl_del @{term iterateoi} *}*)

abbreviation "iterateo s ≡ iterateoi s (λ_. True)"
end

locale poly_set_iterateoi =
finite_set α invar + poly_set_iterateoi_defs list_ordered_it
for α :: "'s ⇒ 'x::linorder set"
and invar
and list_ordered_it :: "'s ⇒ ('x,'x list) set_iterator" +
assumes list_ordered_it_correct: "invar x
⟹ set_iterator_linord (list_ordered_it x) (α x)"
begin
lemma iterateoi_correct:
"invar S ⟹ set_iterator_linord (iterateoi S) (α S)"
unfolding iterateoi_def
apply (rule it_to_it_linord_correct)
by (rule list_ordered_it_correct)

lemma pi_iterateoi[icf_proper_iteratorI]:
"proper_it (iterateoi S) (iterateoi S)"
unfolding iterateoi_def
by (intro icf_proper_iteratorI)

lemma iterateoi_rule_P[case_names minv inv0 inv_pres i_complete i_inter]:
assumes MINV: "invar s"
assumes I0: "I (α s) σ0"
assumes IP: "!!k it σ. ⟦
c σ;
k ∈ it;
∀j∈it. k≤j;
∀j∈α s - it. j≤k;
it ⊆ α s;
I it σ
⟧ ⟹ I (it - {k}) (f k σ)"
assumes IF: "!!σ. I {} σ ⟹ P σ"
assumes II: "!!σ it. ⟦
it ⊆ α s;
it ≠ {};
¬ c σ;
I it σ;
∀k∈it. ∀j∈α s - it. j≤k
⟧ ⟹ P σ"
shows "P (iterateoi s c f σ0)"
using set_iterator_linord_rule_P [OF iterateoi_correct,
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 s"
assumes I0: "I ((α s)) σ0"
assumes IP: "!!k it σ. ⟦ k ∈ it; ∀j∈it. k≤j;
∀j∈(α s) - it. j≤k; it ⊆ (α s); I it σ ⟧
⟹ I (it - {k}) (f k σ)"
assumes IF: "!!σ. I {} σ ⟹ P σ"
shows "P (iterateo s f σ0)"
apply (rule iterateoi_rule_P [where I = I])
apply (simp_all add: assms)
done
end

locale poly_set_rev_iterateoi_defs =
fixes list_rev_it :: "'s ⇒ ('x::linorder,'x list) set_iterator"
begin
definition rev_iterateoi :: "'s ⇒ ('x,'σ) set_iterator"
where "rev_iterateoi S ≡ it_to_it (list_rev_it S)"
(*local_setup {* Locale_Code.lc_decl_del @{term rev_iterateoi} *}*)

abbreviation "rev_iterateo m ≡ rev_iterateoi m (λ_. True)"
abbreviation "reverse_iterateoi ≡ rev_iterateoi"
abbreviation "reverse_iterateo ≡ rev_iterateo"
end

locale poly_set_rev_iterateoi =
finite_set α invar + poly_set_rev_iterateoi_defs list_rev_it
for α :: "'s ⇒ 'x::linorder set"
and invar
and list_rev_it :: "'s ⇒ ('x,'x list) set_iterator" +
assumes list_rev_it_correct:
"invar s ⟹ set_iterator_rev_linord (list_rev_it s) (α s)"
begin
lemma rev_iterateoi_correct:
"invar S ⟹ set_iterator_rev_linord (rev_iterateoi S) (α S)"
unfolding rev_iterateoi_def
apply (rule it_to_it_rev_linord_correct)
by (rule list_rev_it_correct)

lemma pi_rev_iterateoi[icf_proper_iteratorI]:
"proper_it (rev_iterateoi S) (rev_iterateoi S)"
unfolding rev_iterateoi_def
by (intro icf_proper_iteratorI)

lemma rev_iterateoi_rule_P[case_names minv inv0 inv_pres i_complete i_inter]:
assumes MINV: "invar s"
assumes I0: "I ((α s)) σ0"
assumes IP: "!!k it σ. ⟦
c σ;
k ∈ it;
∀j∈it. k≥j;
∀j∈(α s) - it. j≥k;
it ⊆ (α s);
I it σ
⟧ ⟹ I (it - {k}) (f k σ)"
assumes IF: "!!σ. I {} σ ⟹ P σ"
assumes II: "!!σ it. ⟦
it ⊆ (α s);
it ≠ {};
¬ c σ;
I it σ;
∀k∈it. ∀j∈(α s) - it. j≥k
⟧ ⟹ P σ"
shows "P (rev_iterateoi s c f σ0)"
using set_iterator_rev_linord_rule_P [OF rev_iterateoi_correct,
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 s"
assumes I0: "I ((α s)) σ0"
assumes IP: "!!k it σ. ⟦
k ∈ it;
∀j∈it. k≥j;
∀j∈ (α s) - it. j≥k;
it ⊆ (α s);
I it σ
⟧ ⟹ I (it - {k}) (f k σ)"
assumes IF: "!!σ. I {} σ ⟹ P σ"
shows "P (rev_iterateo s f σ0)"
apply (rule rev_iterateoi_rule_P [where I = I])
apply (simp_all add: assms)
done

end

subsubsection "Minimal and Maximal Element"

locale set_min = ordered_set +
constrains α :: "'s ⇒ 'u::linorder set"
fixes min :: "'s ⇒ ('u ⇒ bool) ⇒ 'u option"
assumes min_correct:
"⟦ invar s; x∈α s; P x ⟧ ⟹ min s P ∈ Some  {x∈α s. P x}"
"⟦ invar s; x∈α s; P x ⟧ ⟹ (the (min s P)) ≤ x"
"⟦ invar s; {x∈α s. P x} = {} ⟧ ⟹ min s P = None"
begin
lemma minE:
assumes A: "invar s" "x∈α s" "P x"
obtains x' where
"min s P = Some x'" "x'∈α s" "P x'" "∀x∈α s. P x ⟶ x' ≤ x"
proof -
from min_correct(1)[of s x P, OF A] have
MIS: "min s P ∈ Some  {x ∈ α s. P x}" .
then obtain x' where KV: "min s P = Some x'" "x'∈α s" "P x'"
by auto
show thesis
apply (rule that[OF KV])
apply (clarify)
apply (drule (1) min_correct(2)[OF ‹invar s›])
apply (simp add: KV(1))
done
qed

lemmas minI = min_correct(3)

lemma min_Some:
"⟦ invar s; min s P = Some x ⟧ ⟹ x∈α s"
"⟦ invar s; min s P = Some x ⟧ ⟹ P x"
"⟦ invar s; min s P = Some x; x'∈α s; P x'⟧ ⟹ x≤x'"
apply -
apply (cases "{x ∈ α s. P x} = {}")
apply (drule (1) min_correct(3))
apply simp
apply simp
apply (erule exE)
apply clarify
apply (drule (2) min_correct(1)[of s _ P])
apply auto [1]

apply (cases "{x ∈ α s. P x} = {}")
apply (drule (1) min_correct(3))
apply simp
apply simp
apply (erule exE)
apply clarify
apply (drule (2) min_correct(1)[of s _ P])
apply auto [1]

apply (drule (2) min_correct(2)[where P=P])
apply auto
done

lemma min_None:
"⟦ invar s; min s P = None ⟧ ⟹ {x∈α s. P x} = {}"
apply (cases "{x∈α s. P x} = {}")
apply simp
apply simp
apply (erule exE)
apply clarify
apply (drule (2) min_correct(1)[where P=P])
apply auto
done

end

locale set_max = ordered_set +
constrains α :: "'s ⇒ 'u::linorder set"
fixes max :: "'s ⇒ ('u ⇒ bool) ⇒ 'u option"
assumes max_correct:
"⟦ invar s; x∈α s; P x ⟧ ⟹ max s P ∈ Some  {x∈α s. P x}"
"⟦ invar s; x∈α s; P x ⟧ ⟹ the (max s P) ≥ x"
"⟦ invar s; {x∈α s. P x} = {} ⟧ ⟹ max s P = None"
begin
lemma maxE:
assumes A: "invar s" "x∈α s" "P x"
obtains x' where
"max s P = Some x'" "x'∈α s" "P x'" "∀x∈α s. P x ⟶ x' ≥ x"
proof -
from max_correct(1)[where P=P, OF A] have
MIS: "max s P ∈ Some  {x∈α s. P x}" .
then obtain x' where KV: "max s P = Some x'" "x'∈ α s" "P x'"
by auto
show thesis
apply (rule that[OF KV])
apply (clarify)
apply (drule (1) max_correct(2)[OF ‹invar s›])
apply (simp add: KV(1))
done
qed

lemmas maxI = max_correct(3)

lemma max_Some:
"⟦ invar s; max s P = Some x ⟧ ⟹ x∈α s"
"⟦ invar s; max s P = Some x ⟧ ⟹ P x"
"⟦ invar s; max s P = Some x; x'∈α s; P x'⟧ ⟹ x≥x'"
apply -
apply (cases "{x∈α s. P x} = {}")
apply (drule (1) max_correct(3))
apply simp
apply simp
apply (erule exE)
apply clarify
apply (drule (2) max_correct(1)[of s _ P])
apply auto [1]

apply (cases "{x∈α s. P x} = {}")
apply (drule (1) max_correct(3))
apply simp
apply simp
apply (erule exE)
apply clarify
apply (drule (2) max_correct(1)[of s _ P])
apply auto [1]

apply (drule (1) max_correct(2)[where P=P])
apply auto
done

lemma max_None:
"⟦ invar s; max s P = None ⟧ ⟹ {x∈α s. P x} = {}"
apply (cases "{x∈α s. P x} = {}")
apply simp
apply simp
apply (erule exE)
apply clarify
apply (drule (1) max_correct(1)[where P=P])
apply auto
done

end

subsection "Conversion to List"
locale set_to_sorted_list = ordered_set +
constrains α :: "'s ⇒ 'x::linorder set"
fixes to_sorted_list :: "'s ⇒ 'x list"
assumes to_sorted_list_correct:
"invar s ⟹ set (to_sorted_list s) = α s"
"invar s ⟹ distinct (to_sorted_list s)"
"invar s ⟹ sorted (to_sorted_list s)"

locale set_to_rev_list = ordered_set +
constrains α :: "'s ⇒ 'x::linorder set"
fixes to_rev_list :: "'s ⇒ 'x list"
assumes to_rev_list_correct:
"invar s ⟹ set (to_rev_list s) = α s"
"invar s ⟹ distinct (to_rev_list s)"
"invar s ⟹ sorted (rev (to_rev_list s))"

subsection "Record Based Interface"
record ('x,'s) set_ops =
set_op_α :: "'s ⇒ 'x set"
set_op_invar :: "'s ⇒ bool"
set_op_empty :: "unit ⇒ 's"
set_op_memb :: "'x ⇒ 's ⇒ bool"
set_op_ins :: "'x ⇒ 's ⇒ 's"
set_op_ins_dj :: "'x ⇒ 's ⇒ 's"
set_op_delete :: "'x ⇒ 's ⇒ 's"
set_op_list_it :: "('x,'s) set_list_it"
set_op_sng :: "'x ⇒ 's"
set_op_isEmpty :: "'s ⇒ bool"
set_op_isSng :: "'s ⇒ bool"
set_op_ball :: "'s ⇒ ('x ⇒ bool) ⇒ bool"
set_op_bex :: "'s ⇒ ('x ⇒ bool) ⇒ bool"
set_op_size :: "'s ⇒ nat"
set_op_size_abort :: "nat ⇒ 's ⇒ nat"
set_op_union :: "'s ⇒ 's ⇒ 's"
set_op_union_dj :: "'s ⇒ 's ⇒ 's"
set_op_diff :: "'s ⇒ 's ⇒ 's"
set_op_filter :: "('x ⇒ bool) ⇒ 's ⇒ 's"
set_op_inter :: "'s ⇒ 's ⇒ 's"
set_op_subset :: "'s ⇒ 's ⇒ bool"
set_op_equal :: "'s ⇒ 's ⇒ bool"
set_op_disjoint :: "'s ⇒ 's ⇒ bool"
set_op_disjoint_witness :: "'s ⇒ 's ⇒ 'x option"
set_op_sel :: "'s ⇒ ('x ⇒ bool) ⇒ 'x option" ― ‹Version without mapping›
set_op_to_list :: "'s ⇒ 'x list"
set_op_from_list :: "'x list ⇒ 's"

locale StdSetDefs =
poly_set_iteratei_defs "set_op_list_it ops"
for ops :: "('x,'s,'more) set_ops_scheme"
begin
abbreviation α where "α == set_op_α ops"
abbreviation invar where "invar == set_op_invar ops"
abbreviation empty where "empty == set_op_empty ops"
abbreviation memb where "memb == set_op_memb ops"
abbreviation ins where "ins == set_op_ins ops"
abbreviation ins_dj where "ins_dj == set_op_ins_dj ops"
abbreviation delete where "delete == set_op_delete ops"
abbreviation list_it where "list_it ≡ set_op_list_it ops"
abbreviation sng where "sng == set_op_sng ops"
abbreviation isEmpty where "isEmpty == set_op_isEmpty ops"
abbreviation isSng where "isSng == set_op_isSng ops"
abbreviation ball where "ball == set_op_ball ops"
abbreviation bex where "bex == set_op_bex ops"
abbreviation size where "size == set_op_size ops"
abbreviation size_abort where "size_abort == set_op_size_abort ops"
abbreviation union where "union == set_op_union ops"
abbreviation union_dj where "union_dj == set_op_union_dj ops"
abbreviation diff where "diff == set_op_diff ops"
abbreviation filter where "filter == set_op_filter ops"
abbreviation inter where "inter == set_op_inter ops"
abbreviation subset where "subset == set_op_subset ops"
abbreviation equal where "equal == set_op_equal ops"
abbreviation disjoint where "disjoint == set_op_disjoint ops"
abbreviation disjoint_witness
where "disjoint_witness == set_op_disjoint_witness ops"
abbreviation sel where "sel == set_op_sel ops"
abbreviation to_list where "to_list == set_op_to_list ops"
abbreviation from_list where "from_list == set_op_from_list ops"
end

locale StdSet = StdSetDefs ops +
set α invar +
set_empty α invar empty +
set_memb α invar memb +
set_ins α invar ins +
set_ins_dj α invar ins_dj +
set_delete α invar delete +
poly_set_iteratei α invar list_it +
set_sng α invar sng +
set_isEmpty α invar isEmpty +
set_isSng α invar isSng +
set_ball α invar ball +
set_bex α invar bex +
set_size α invar size +
set_size_abort α invar size_abort +
set_union α invar α invar α invar union +
set_union_dj α invar α invar α invar union_dj +
set_diff α invar α invar diff +
set_filter α invar α invar filter +
set_inter α invar α invar α invar inter +
set_subset α invar α invar subset +
set_equal α invar α invar equal +
set_disjoint α invar α invar disjoint +
set_disjoint_witness α invar α invar disjoint_witness +
set_sel' α invar sel +
set_to_list α invar to_list +
list_to_set α invar from_list
for ops :: "('x,'s,'more) set_ops_scheme"
begin

lemmas correct =
empty_correct
sng_correct
memb_correct
ins_correct
ins_dj_correct
delete_correct
isEmpty_correct
isSng_correct
ball_correct
bex_correct
size_correct
size_abort_correct
union_correct
union_dj_correct
diff_correct
filter_correct
inter_correct
subset_correct
equal_correct
disjoint_correct
disjoint_witness_correct
to_list_correct
to_set_correct

end

lemmas StdSet_intro = StdSet.intro[rem_dup_prems]

locale StdSet_no_invar = StdSet + set_no_invar α invar

record ('x,'s) oset_ops = "('x::linorder,'s) set_ops" +
set_op_ordered_list_it :: "'s ⇒ ('x,'x list) set_iterator"
set_op_rev_list_it :: "'s ⇒ ('x,'x list) set_iterator"
set_op_min :: "'s ⇒ ('x ⇒ bool) ⇒ 'x option"
set_op_max :: "'s ⇒ ('x ⇒ bool) ⇒ 'x option"
set_op_to_sorted_list :: "'s ⇒ 'x list"
set_op_to_rev_list :: "'s ⇒ 'x list"

locale StdOSetDefs = StdSetDefs ops
+ poly_set_iterateoi_defs "set_op_ordered_list_it ops"
+ poly_set_rev_iterateoi_defs "set_op_rev_list_it ops"
for ops :: "('x::linorder,'s,'more) oset_ops_scheme"
begin
abbreviation "ordered_list_it ≡ set_op_ordered_list_it ops"
abbreviation "rev_list_it ≡ set_op_rev_list_it ops"
abbreviation min where "min == set_op_min ops"
abbreviation max where "max == set_op_max ops"
abbreviation to_sorted_list where
"to_sorted_list ≡ set_op_to_sorted_list ops"
abbreviation to_rev_list where "to_rev_list ≡ set_op_to_rev_list ops"
end

locale StdOSet =
StdOSetDefs ops +
StdSet ops +
poly_set_iterateoi α invar ordered_list_it +
poly_set_rev_iterateoi α invar rev_list_it +
set_min α invar min +
set_max α invar max +
set_to_sorted_list α invar to_sorted_list +
set_to_rev_list α invar to_rev_list
for ops :: "('x::linorder,'s,'more) oset_ops_scheme"
begin
end

lemmas StdOSet_intro =
StdOSet.intro[OF StdSet_intro, rem_dup_prems]

no_notation insert ("set'_ins")
(*notation member (infixl "mem" 55)*)

end
`