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>
*)
header {* \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) = \<Union>{α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) = \<Union>(α2`f`α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