Theory SetGA

(*  Title:       Isabelle Collections Library
    Author:      Peter Lammich <peter dot lammich at uni-muenster.de>
    Maintainer:  Peter Lammich <peter dot lammich at uni-muenster.de>
*)
(*
  Changes since submission on 2009-11-26:

  2009-12-10: OrderedSet, algorithms for iterators, min, max, to_sorted_list

*)

section ‹\isaheader{Generic Algorithms for Sets}›
theory SetGA
imports "../spec/SetSpec" SetIteratorCollectionsGA
begin
text_raw ‹\label{thy:SetGA}›

subsection ‹Generic Set Algorithms›

locale g_set_xx_defs_loc = 
  s1: StdSetDefs ops1 + s2: StdSetDefs ops2
  for ops1 :: "('x,'s1,'more1) set_ops_scheme"
  and ops2 :: "('x,'s2,'more2) set_ops_scheme"
begin
  definition "g_copy s ≡ s1.iterate s s2.ins_dj (s2.empty ())"
  definition "g_filter P s1 ≡ s1.iterate s1 
    (λx σ. if P x then s2.ins_dj x σ else σ) 
    (s2.empty ())"

  definition "g_union s1 s2 ≡ s1.iterate s1 s2.ins s2"
  definition "g_diff s1 s2 ≡ s2.iterate s2 s1.delete s1"

  definition g_union_list where
    "g_union_list l =
      foldl (λs s'. g_union s' s) (s2.empty ()) l"

  definition "g_union_dj s1 s2 ≡ s1.iterate s1 s2.ins_dj s2"

  definition "g_disjoint_witness s1 s2 ≡
    s1.sel s1 (λx. s2.memb x s2)"

  definition "g_disjoint s1 s2 ≡
    s1.ball s1 (λx. ¬s2.memb x s2)"
end

locale g_set_xx_loc = g_set_xx_defs_loc ops1 ops2 +
  s1: StdSet ops1 + s2: StdSet ops2
  for ops1 :: "('x,'s1,'more1) set_ops_scheme"
  and ops2 :: "('x,'s2,'more2) set_ops_scheme"
begin
  lemma g_copy_alt: 
    "g_copy s = iterate_to_set s2.empty s2.ins_dj (s1.iteratei s)"
    unfolding iterate_to_set_alt_def g_copy_def ..

  lemma g_copy_impl: "set_copy s1.α s1.invar s2.α s2.invar g_copy" 
  proof -

    have LIS: 
      "set_ins_dj s2.α s2.invar s2.ins_dj" 
      "set_empty s2.α s2.invar s2.empty"
      by unfold_locales

    from iterate_to_set_correct[OF LIS s1.iteratei_correct]
    show ?thesis
      apply unfold_locales
      unfolding g_copy_alt
      by simp_all
  qed

  lemma g_filter_impl: "set_filter s1.α s1.invar s2.α s2.invar g_filter"
  proof
    fix s P
    assume "s1.invar s"
    hence "s2.α (g_filter P s) = {e ∈ s1.α s. P e} ∧
      s2.invar (g_filter P s)" (is "?G1 ∧ ?G2")
      unfolding g_filter_def
      apply (rule_tac I="λit σ. s2.invar σ ∧ s2.α σ = {e ∈ it. P e}" 
        in s1.iterate_rule_insert_P)
      by (auto simp add: s2.empty_correct s2.ins_dj_correct)
    thus ?G1 ?G2 by auto
  qed

  lemma g_union_alt: 
    "g_union s1 s2 = iterate_add_to_set s2 s2.ins (s1.iteratei s1)"
    unfolding iterate_add_to_set_def g_union_def ..

  lemma g_diff_alt:
    "g_diff s1 s2 = iterate_diff_set s1 s1.delete (s2.iteratei s2)"
    unfolding g_diff_def iterate_diff_set_def ..

  lemma g_union_impl:
    "set_union s1.α s1.invar s2.α s2.invar s2.α s2.invar g_union"
  proof -
    have LIS: "set_ins s2.α s2.invar s2.ins" by unfold_locales
    from iterate_add_to_set_correct[OF LIS _ s1.iteratei_correct]
    show ?thesis
      apply unfold_locales
      unfolding g_union_alt
      by simp_all
  qed

  lemma g_diff_impl:
    "set_diff s1.α s1.invar s2.α s2.invar g_diff"
  proof -
    have LIS: "set_delete s1.α s1.invar s1.delete" by unfold_locales
    from iterate_diff_correct[OF LIS _ s2.iteratei_correct]
    show ?thesis
      apply unfold_locales
      unfolding g_diff_alt
      by simp_all
  qed

  lemma g_union_list_impl:
    shows "set_union_list s1.α s1.invar s2.α s2.invar g_union_list"
  proof
    fix l
    note correct = s2.empty_correct set_union.union_correct[OF g_union_impl]

    assume "∀s1∈set l. s1.invar s1"
    hence aux: "⋀s. s2.invar s ⟹
           s2.α (foldl (λs s'. g_union s' s) s l) 
           = ⋃{s1.α s1 |s1. s1 ∈ set l} ∪ s2.α s ∧
           s2.invar (foldl (λs s'. g_union s' s) s l)"
      by (induct l) (auto simp add: correct)

    from aux [of "s2.empty ()"]
    show "s2.α (g_union_list l) = ⋃{s1.α s1 |s1. s1 ∈ set l}"
         "s2.invar (g_union_list l)"
      unfolding g_union_list_def
      by (simp_all add: correct)
  qed

  lemma g_union_dj_impl:
    "set_union_dj s1.α s1.invar s2.α s2.invar s2.α s2.invar g_union_dj"
  proof
    fix s1 s2
    assume I: 
      "s1.invar s1" 
      "s2.invar s2"
    assume DJ: "s1.α s1 ∩ s2.α s2 = {}"

    have "s2.α (g_union_dj s1 s2) 
      = s1.α s1 ∪ s2.α s2
      ∧ s2.invar (g_union_dj s1 s2)" (is "?G1 ∧ ?G2")
      unfolding g_union_dj_def

      apply (rule_tac I="λit σ. s2.invar σ ∧ s2.α σ = it ∪ s2.α s2" 
        in s1.iterate_rule_insert_P)
      using DJ
      apply (simp_all add: I)
      apply (subgoal_tac "x∉s2.α σ")
      apply (simp add: s2.ins_dj_correct I)
      apply auto
      done
    thus ?G1 ?G2 by auto
  qed

  lemma g_disjoint_witness_impl: 
    "set_disjoint_witness s1.α s1.invar s2.α s2.invar g_disjoint_witness"
  proof -
    show ?thesis
      apply unfold_locales
      unfolding g_disjoint_witness_def
      by (auto dest: s1.sel'_noneD s1.sel'_someD simp: s2.memb_correct)
  qed

  lemma g_disjoint_impl: 
    "set_disjoint s1.α s1.invar s2.α s2.invar g_disjoint"
  proof -
    show ?thesis
      apply unfold_locales
      unfolding g_disjoint_def
      by (auto simp: s2.memb_correct s1.ball_correct)
  qed
end

sublocale g_set_xx_loc < 
  set_copy s1.α s1.invar s2.α s2.invar g_copy by (rule g_copy_impl)

sublocale g_set_xx_loc < 
  set_filter s1.α s1.invar s2.α s2.invar g_filter by (rule g_filter_impl)

sublocale g_set_xx_loc < 
  set_union s1.α s1.invar s2.α s2.invar s2.α s2.invar g_union 
  by (rule g_union_impl)

sublocale g_set_xx_loc < 
  set_union_dj s1.α s1.invar s2.α s2.invar s2.α s2.invar g_union_dj 
  by (rule g_union_dj_impl)

sublocale g_set_xx_loc < 
  set_diff s1.α s1.invar s2.α s2.invar g_diff 
  by (rule g_diff_impl)

sublocale g_set_xx_loc < 
  set_disjoint_witness s1.α s1.invar s2.α s2.invar g_disjoint_witness
  by (rule g_disjoint_witness_impl)

sublocale g_set_xx_loc < 
  set_disjoint s1.α s1.invar s2.α s2.invar g_disjoint by (rule g_disjoint_impl)




(*sublocale StdBasicSetDefs < g_set_xx: g_set_xx_defs_loc ops ops .
sublocale StdBasicSet < g_set_xx: g_set_xx_loc ops ops
  by unfold_locales
*)

locale g_set_xxx_defs_loc =
  s1: StdSetDefs ops1 +
  s2: StdSetDefs ops2 +
  s3: StdSetDefs ops3
  for ops1 :: "('x,'s1,'more1) set_ops_scheme"
  and ops2 :: "('x,'s2,'more2) set_ops_scheme"
  and ops3 :: "('x,'s3,'more3) set_ops_scheme"
begin
  definition "g_inter s1 s2 ≡
    s1.iterate s1 (λx s. if s2.memb x s2 then s3.ins_dj x s else s) 
      (s3.empty ())"
end

locale g_set_xxx_loc = g_set_xxx_defs_loc ops1 ops2 ops3 +
  s1: StdSet ops1 +
  s2: StdSet ops2 +
  s3: StdSet ops3
  for ops1 :: "('x,'s1,'more1) set_ops_scheme"
  and ops2 :: "('x,'s2,'more2) set_ops_scheme"
  and ops3 :: "('x,'s3,'more3) set_ops_scheme"
begin
  lemma g_inter_impl: "set_inter s1.α s1.invar s2.α s2.invar s3.α s3.invar
    g_inter"
  proof
    fix s1 s2
    assume I: 
      "s1.invar s1" 
      "s2.invar s2"
    have "s3.α (g_inter s1 s2) = s1.α s1 ∩ s2.α s2 ∧ s3.invar (g_inter s1 s2)"
      unfolding g_inter_def
      apply (rule_tac I="λit σ. s3.α σ = it ∩ s2.α s2 ∧ s3.invar σ" 
        in s1.iterate_rule_insert_P) 
      apply (simp_all add: I s3.empty_correct s3.ins_dj_correct s2.memb_correct)
      done
    thus "s3.α (g_inter s1 s2) = s1.α s1 ∩ s2.α s2" 
      and "s3.invar (g_inter s1 s2)" by auto
  qed
end    

sublocale g_set_xxx_loc 
  < set_inter s1.α s1.invar s2.α s2.invar s3.α s3.invar g_inter
  by (rule g_inter_impl)


(*sublocale StdBasicSetDefs < g_set_xxx: g_set_xxx_defs_loc ops ops ops .
sublocale StdBasicSet < g_set_xxx: g_set_xxx_loc ops ops ops
  by unfold_locales
*)

locale g_set_xy_defs_loc = 
  s1: StdSet ops1 + s2: StdSet ops2
  for ops1 :: "('x1,'s1,'more1) set_ops_scheme"
  and ops2 :: "('x2,'s2,'more2) set_ops_scheme"
begin
  definition "g_image_filter f s ≡ 
    s1.iterate s 
      (λx res. case f x of Some v ⇒ s2.ins v res | _ ⇒ res) 
      (s2.empty ())"

  definition "g_image f s ≡ 
    s1.iterate s (λx res. s2.ins (f x) res) (s2.empty ())"

  definition "g_inj_image_filter f s ≡ 
    s1.iterate s 
      (λx res. case f x of Some v ⇒ s2.ins_dj v res | _ ⇒ res) 
      (s2.empty ())"

  definition "g_inj_image f s ≡ 
    s1.iterate s (λx res. s2.ins_dj (f x) res) (s2.empty ())"

end

locale g_set_xy_loc = g_set_xy_defs_loc ops1 ops2 +
  s1: StdSet ops1 + s2: StdSet ops2
  for ops1 :: "('x1,'s1,'more1) set_ops_scheme"
  and ops2 :: "('x2,'s2,'more2) set_ops_scheme"
begin
  lemma g_image_filter_impl: 
    "set_image_filter s1.α s1.invar s2.α s2.invar g_image_filter"
  proof
    fix f s
    assume I: "s1.invar s"
    have A: "g_image_filter f s == 
         iterate_to_set s2.empty s2.ins 
           (set_iterator_image_filter f (s1.iteratei s))"
      unfolding g_image_filter_def 
        iterate_to_set_alt_def set_iterator_image_filter_def
      by simp
    
    have ins: "set_ins s2.α s2.invar s2.ins"
      and emp: "set_empty s2.α s2.invar s2.empty" by unfold_locales

    from iterate_image_filter_to_set_correct[OF ins emp s1.iteratei_correct]
    show "s2.α (g_image_filter f s) =
          {b. ∃a∈s1.α s. f a = Some b}"
         "s2.invar (g_image_filter f s)"
      unfolding A using I by auto
  qed

  lemma g_image_alt: "g_image f s = g_image_filter (Some o f) s"
    unfolding g_image_def g_image_filter_def
    by auto

  lemma g_image_impl: "set_image s1.α s1.invar s2.α s2.invar g_image" 
  proof -
    interpret set_image_filter s1.α s1.invar s2.α s2.invar g_image_filter 
      by (rule g_image_filter_impl)

    show ?thesis
      apply unfold_locales
      unfolding g_image_alt
      by (auto simp add: image_filter_correct)
  qed

  lemma g_inj_image_filter_impl: 
    "set_inj_image_filter s1.α s1.invar s2.α s2.invar g_inj_image_filter"
  proof
    fix f::"'x1 ⇀ 'x2" and s
    assume I: "s1.invar s" and INJ: "inj_on f (s1.α s ∩ dom f)"
    have A: "g_inj_image_filter f s == 
         iterate_to_set s2.empty s2.ins_dj 
           (set_iterator_image_filter f (s1.iteratei s))"
      unfolding g_inj_image_filter_def 
        iterate_to_set_alt_def set_iterator_image_filter_def
      by simp
    
    have ins_dj: "set_ins_dj s2.α s2.invar s2.ins_dj"
      and emp: "set_empty s2.α s2.invar s2.empty" by unfold_locales


    from set_iterator_image_filter_correct[OF s1.iteratei_correct[OF I] INJ]
    have iti_s1_filter: "set_iterator 
      (set_iterator_image_filter f (s1.iteratei s))
      {y. ∃x. x ∈ s1.α s ∧ f x = Some y}"
      by simp

    from iterate_to_set_correct[OF ins_dj emp, OF iti_s1_filter]
    show "s2.α (g_inj_image_filter f s) =
          {b. ∃a∈s1.α s. f a = Some b}"
         "s2.invar (g_inj_image_filter f s)"
      unfolding A by auto
  qed


  lemma g_inj_image_alt: "g_inj_image f s = g_inj_image_filter (Some o f) s"
    unfolding g_inj_image_def g_inj_image_filter_def
    by auto

  lemma g_inj_image_impl: 
    "set_inj_image s1.α s1.invar s2.α s2.invar g_inj_image" 
  proof -
    interpret set_inj_image_filter 
      s1.α s1.invar s2.α s2.invar g_inj_image_filter 
      by (rule g_inj_image_filter_impl)

    have AUX: "⋀S f. inj_on f S ⟹ inj_on (Some ∘ f) (S ∩ dom (Some ∘ f))"
      by (auto intro!: inj_onI dest: inj_onD)
      
    show ?thesis
      apply unfold_locales
      unfolding g_inj_image_alt
      by (auto simp add: inj_image_filter_correct AUX)

  qed

end

sublocale g_set_xy_loc < set_image_filter s1.α s1.invar s2.α s2.invar 
  g_image_filter by (rule g_image_filter_impl)

sublocale g_set_xy_loc < set_image s1.α s1.invar s2.α s2.invar 
  g_image by (rule g_image_impl)

sublocale g_set_xy_loc < set_inj_image s1.α s1.invar s2.α s2.invar 
  g_inj_image by (rule g_inj_image_impl)

locale g_set_xyy_defs_loc = 
  s0: StdSetDefs ops0 + 
  g_set_xx_defs_loc ops1 ops2
  for ops0 :: "('x0,'s0,'more0) set_ops_scheme"
  and ops1 :: "('x,'s1,'more1) set_ops_scheme"
  and ops2 :: "('x,'s2,'more2) set_ops_scheme"
begin
  definition g_Union_image
    :: "('x0 ⇒ 's1) ⇒ 's0 ⇒ 's2"
    where "g_Union_image f S 
    == s0.iterate S (λx res. g_union (f x) res) (s2.empty ())"
end

locale g_set_xyy_loc = g_set_xyy_defs_loc ops0 ops1 ops2 +
  s0: StdSet ops0 + 
  g_set_xx_loc ops1 ops2
  for ops0 :: "('x0,'s0,'more0) set_ops_scheme"
  and ops1 :: "('x,'s1,'more1) set_ops_scheme"
  and ops2 :: "('x,'s2,'more2) set_ops_scheme"
begin

  lemma g_Union_image_impl:
    "set_Union_image s0.α s0.invar s1.α s1.invar s2.α s2.invar g_Union_image"
  proof -
    {
      fix s f
      have "⟦s0.invar s; ⋀x. x ∈ s0.α s ⟹ s1.invar (f x)⟧ ⟹ 
        s2.α (g_Union_image f s) = ⋃(s1.α ` f ` s0.α s) 
        ∧ s2.invar (g_Union_image f s)"
        apply (unfold g_Union_image_def)
        apply (rule_tac I="λit res. s2.invar res 
          ∧ s2.α res = ⋃(s1.α`f`(s0.α s - it))" in s0.iterate_rule_P)
        apply (fastforce simp add: s2.empty_correct union_correct)+
        done
    }
    thus ?thesis
      apply unfold_locales
      apply auto
      done
  qed
end

sublocale g_set_xyy_loc < 
  set_Union_image s0.α s0.invar s1.α s1.invar s2.α s2.invar g_Union_image
  by (rule g_Union_image_impl)

subsection ‹Default Set Operations›

record ('x,'s) set_basic_ops = 
  bset_op_α :: "'s ⇒ 'x set"
  bset_op_invar :: "'s ⇒ bool"
  bset_op_empty :: "unit ⇒ 's"
  bset_op_memb :: "'x ⇒ 's ⇒ bool"
  bset_op_ins :: "'x ⇒ 's ⇒ 's"
  bset_op_ins_dj :: "'x ⇒ 's ⇒ 's"
  bset_op_delete :: "'x ⇒ 's ⇒ 's"
  bset_op_list_it :: "('x,'s) set_list_it"

record ('x,'s) oset_basic_ops = "('x::linorder,'s) set_basic_ops" +
  bset_op_ordered_list_it :: "'s ⇒ ('x,'x list) set_iterator"
  bset_op_rev_list_it :: "'s ⇒ ('x,'x list) set_iterator"

locale StdBasicSetDefs = 
  poly_set_iteratei_defs "bset_op_list_it ops"
  for ops :: "('x,'s,'more) set_basic_ops_scheme"
begin
  abbreviation α where "α == bset_op_α ops"
  abbreviation invar where "invar == bset_op_invar ops"
  abbreviation empty where "empty == bset_op_empty ops"
  abbreviation memb where "memb == bset_op_memb ops"
  abbreviation ins where "ins == bset_op_ins ops"
  abbreviation ins_dj where "ins_dj == bset_op_ins_dj ops"
  abbreviation delete where "delete == bset_op_delete ops"
  abbreviation list_it where "list_it ≡ bset_op_list_it ops"
end

locale StdBasicOSetDefs = StdBasicSetDefs ops
  + poly_set_iterateoi_defs "bset_op_ordered_list_it ops"
  + poly_set_rev_iterateoi_defs "bset_op_rev_list_it ops"
  for ops :: "('x::linorder,'s,'more) oset_basic_ops_scheme"
begin
  abbreviation "ordered_list_it ≡ bset_op_ordered_list_it ops"
  abbreviation "rev_list_it ≡ bset_op_rev_list_it ops"
end

locale StdBasicSet = StdBasicSetDefs 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
  for ops :: "('x,'s,'more) set_basic_ops_scheme"
begin

  lemmas correct[simp] = 
    empty_correct
    memb_correct
    ins_correct
    ins_dj_correct
    delete_correct

end

locale StdBasicOSet =
  StdBasicOSetDefs ops +
  StdBasicSet ops +
  poly_set_iterateoi α invar ordered_list_it +
  poly_set_rev_iterateoi α invar rev_list_it
  for ops :: "('x::linorder,'s,'more) oset_basic_ops_scheme"
begin
end

context StdBasicSetDefs
begin
  definition "g_sng x ≡ ins x (empty ())"
  definition "g_isEmpty s ≡ iteratei s (λc. c) (λ_ _. False) True"
  definition "g_sel' s P ≡ iteratei s ((=) None) 
    (λx _. if P x then Some x else None) None"

  definition "g_ball s P ≡ iteratei s (λc. c) (λx σ. P x) True"
  definition "g_bex s P ≡ iteratei s (λc. ¬c) (λx σ. P x) False"
  definition "g_size s ≡ iteratei s (λ_. True) (λx n . Suc n) 0"
  definition "g_size_abort m s ≡ iteratei s (λσ. σ < m) (λx. Suc) 0"
  definition "g_isSng s ≡ (iteratei s (λσ. σ < 2) (λx. Suc) 0 = 1)"

  definition "g_union s1 s2 ≡ iterate s1 ins s2"
  definition "g_diff s1 s2 ≡ iterate s2 delete s1"

  definition "g_subset s1 s2 ≡ g_ball s1 (λx. memb x s2)"

  definition "g_equal s1 s2 ≡ g_subset s1 s2 ∧ g_subset s2 s1"

  definition "g_to_list s ≡ iterate s (#) []"

  fun g_from_list_aux where
    "g_from_list_aux accs [] = accs" |
    "g_from_list_aux accs (x#l) = g_from_list_aux (ins x accs) l"
    ― ‹Tail recursive version›

  definition "g_from_list l == g_from_list_aux (empty ()) l"

  definition "g_inter s1 s2 ≡
    iterate s1 (λx s. if memb x s2 then ins_dj x s else s) 
      (empty ())"

  definition "g_union_dj s1 s2 ≡ iterate s1 ins_dj s2"
  definition "g_filter P s ≡ iterate s 
    (λx σ. if P x then ins_dj x σ else σ) 
    (empty ())"

  definition "g_disjoint_witness s1 s2 ≡ g_sel' s1 (λx. memb x s2)"
  definition "g_disjoint s1 s2 ≡ g_ball s1 (λx. ¬memb x s2)"

  definition dflt_ops
    where [icf_rec_def]: "dflt_ops ≡ ⦇
      set_op_α = α, 
      set_op_invar = invar, 
      set_op_empty = empty, 
      set_op_memb = memb, 
      set_op_ins = ins, 
      set_op_ins_dj = ins_dj, 
      set_op_delete = delete, 
      set_op_list_it = list_it, 
      set_op_sng = g_sng ,
      set_op_isEmpty = g_isEmpty ,
      set_op_isSng = g_isSng ,
      set_op_ball = g_ball ,
      set_op_bex = g_bex ,
      set_op_size = g_size ,
      set_op_size_abort = g_size_abort ,
      set_op_union = g_union ,
      set_op_union_dj = g_union_dj ,
      set_op_diff = g_diff ,
      set_op_filter = g_filter ,
      set_op_inter = g_inter ,
      set_op_subset = g_subset ,
      set_op_equal = g_equal ,
      set_op_disjoint = g_disjoint ,
      set_op_disjoint_witness = g_disjoint_witness ,
      set_op_sel = g_sel' ,
      set_op_to_list = g_to_list ,
      set_op_from_list = g_from_list
    ⦈"

  local_setup ‹Locale_Code.lc_decl_del @{term dflt_ops}›
end

context StdBasicSet
begin
  lemma g_sng_impl: "set_sng α invar g_sng"
    apply unfold_locales 
    unfolding g_sng_def
    apply (auto simp: ins_correct empty_correct)
    done

  lemma g_ins_dj_impl: "set_ins_dj α invar ins"
    by unfold_locales (auto simp: ins_correct)

  lemma g_isEmpty_impl: "set_isEmpty α invar g_isEmpty"
  proof 
    fix s assume I: "invar s"
    have A: "g_isEmpty s = iterate_is_empty (iteratei s)"
      unfolding g_isEmpty_def iterate_is_empty_def ..
    from iterate_is_empty_correct[OF iteratei_correct[OF I]]
    show "g_isEmpty s ⟷ α s = {}" unfolding A .
  qed

  lemma g_sel'_impl: "set_sel' α invar g_sel'"
  proof -
    have A: "⋀s P. g_sel' s P = iterate_sel_no_map (iteratei s) P"
      unfolding g_sel'_def iterate_sel_no_map_alt_def 
      apply (rule arg_cong[where f="iteratei", THEN cong, THEN cong, THEN cong])
      by auto

    show ?thesis
      unfolding set_sel'_def A
      using iterate_sel_no_map_correct[OF iteratei_correct]
      apply (simp add: Bex_def Ball_def)
      apply (metis option.exhaust)
      done
  qed
   
  lemma g_ball_alt: "g_ball s P = iterate_ball (iteratei s) P"
    unfolding g_ball_def iterate_ball_def by (simp add: id_def)
  lemma g_bex_alt: "g_bex s P = iterate_bex (iteratei s) P"
    unfolding g_bex_def iterate_bex_def ..

  lemma g_ball_impl: "set_ball α invar g_ball"
    apply unfold_locales
    unfolding g_ball_alt
    apply (rule iterate_ball_correct)
    by (rule iteratei_correct)

  lemma g_bex_impl: "set_bex α invar g_bex"
    apply unfold_locales
    unfolding g_bex_alt
    apply (rule iterate_bex_correct)
    by (rule iteratei_correct)

  lemma g_size_alt: "g_size s = iterate_size (iteratei s)"
    unfolding g_size_def iterate_size_def ..
  lemma g_size_abort_alt: "g_size_abort m s = iterate_size_abort (iteratei s) m"
    unfolding g_size_abort_def iterate_size_abort_def ..

  lemma g_size_impl: "set_size α invar g_size"
    apply unfold_locales
    unfolding g_size_alt
    apply (rule conjunct1[OF iterate_size_correct])
    by (rule iteratei_correct)

  lemma g_size_abort_impl: "set_size_abort α invar g_size_abort"
    apply unfold_locales
    unfolding g_size_abort_alt
    apply (rule conjunct1[OF iterate_size_abort_correct])
    by (rule iteratei_correct)

  lemma g_isSng_alt: "g_isSng s = iterate_is_sng (iteratei s)"
    unfolding g_isSng_def iterate_is_sng_def iterate_size_abort_def ..

  lemma g_isSng_impl: "set_isSng α invar g_isSng"
    apply unfold_locales
    unfolding g_isSng_alt
    apply (drule iterate_is_sng_correct[OF iteratei_correct])
    apply (simp add: card_Suc_eq)
    done

  lemma g_union_impl: "set_union α invar α invar α invar g_union"
    unfolding g_union_def[abs_def]
    apply unfold_locales
    apply (rule_tac I="λit σ. invar σ ∧ α σ = it ∪ α s2" 
      in iterate_rule_insert_P, simp_all)+
    done

  lemma g_diff_impl: "set_diff α invar α invar g_diff"
    unfolding g_diff_def[abs_def]
    apply (unfold_locales)
    apply (rule_tac I="λit σ. invar σ ∧ α σ = α s1 - it" 
      in iterate_rule_insert_P, auto)+
    done

  lemma g_subset_impl: "set_subset α invar α invar g_subset"
  proof -
    interpret set_ball α invar g_ball by (rule g_ball_impl)

    show ?thesis 
      apply unfold_locales
      unfolding g_subset_def
      by (auto simp add: ball_correct memb_correct)
  qed

  lemma g_equal_impl: "set_equal α invar α invar g_equal"
  proof -
    interpret set_subset α invar α invar g_subset by (rule g_subset_impl)

    show ?thesis 
      apply unfold_locales
      unfolding g_equal_def
      by (auto simp add: subset_correct)
  qed

  lemma g_to_list_impl: "set_to_list α invar g_to_list"
  proof 
    fix s 
    assume I: "invar s"
    have A: "g_to_list s = iterate_to_list (iteratei s)"
      unfolding g_to_list_def iterate_to_list_def ..
    
    from iterate_to_list_correct [OF iteratei_correct[OF I]]
    show "set (g_to_list s) = α s" and "distinct (g_to_list s)"
      unfolding A
      by auto
  qed

  lemma g_from_list_impl: "list_to_set α invar g_from_list"
  proof -
    { ― ‹Show a generalized lemma›
      fix l accs
      have "invar accs ⟹ α (g_from_list_aux accs l) = set l ∪ α accs 
            ∧ invar (g_from_list_aux accs l)"
        by (induct l arbitrary: accs)
           (auto simp add: ins_correct)
    } thus ?thesis
      apply (unfold_locales)
      apply (unfold g_from_list_def)
      apply (auto simp add: empty_correct)
      done
  qed

  lemma g_inter_impl: "set_inter α invar α invar α invar g_inter"
    unfolding g_inter_def[abs_def]
    apply unfold_locales
    apply (rule_tac I="λit σ. invar σ ∧ α σ = it ∩ α s2" 
      in iterate_rule_insert_P, auto) []
    apply (rule_tac I="λit σ. invar σ ∧ α σ = it ∩ α s2" 
      in iterate_rule_insert_P, auto)
    done

  lemma g_union_dj_impl: "set_union_dj α invar α invar α invar g_union_dj"
    unfolding g_union_dj_def[abs_def]
    apply unfold_locales
    apply (rule_tac I="λit σ. invar σ ∧ α σ = it ∪ α s2" 
      in iterate_rule_insert_P)
    apply simp
    apply simp
    apply (subgoal_tac "x∉α σ")
    apply simp
    apply blast
    apply simp
    apply (rule_tac I="λit σ. invar σ ∧ α σ = it ∪ α s2" 
      in iterate_rule_insert_P)
    apply simp
    apply simp
    apply (subgoal_tac "x∉α σ")
    apply simp
    apply blast
    apply simp
    done

  lemma g_filter_impl: "set_filter α invar α invar g_filter"
    unfolding g_filter_def[abs_def]
    apply (unfold_locales)
    apply (rule_tac I="λit σ. invar σ ∧ α σ = it ∩ Collect P" 
      in iterate_rule_insert_P, auto)
    apply (rule_tac I="λit σ. invar σ ∧ α σ = it ∩ Collect P" 
      in iterate_rule_insert_P, auto)
    done

  lemma g_disjoint_witness_impl: "set_disjoint_witness 
    α invar α invar g_disjoint_witness"
  proof -
    interpret set_sel' α invar g_sel' by (rule g_sel'_impl)
    show ?thesis
      unfolding g_disjoint_witness_def[abs_def]
      apply unfold_locales
      by (auto dest: sel'_noneD sel'_someD simp: memb_correct)
  qed

  lemma g_disjoint_impl: "set_disjoint 
    α invar α invar g_disjoint"
  proof -
    interpret set_ball α invar g_ball by (rule g_ball_impl)
    show ?thesis
      apply unfold_locales
      unfolding g_disjoint_def
      by (auto simp: memb_correct ball_correct)
  qed

end

context StdBasicSet
begin
  lemma dflt_ops_impl: "StdSet dflt_ops"
    apply (rule StdSet_intro)
    apply icf_locales
    apply (simp_all add: icf_rec_unf)
    apply (rule g_sng_impl g_isEmpty_impl g_isSng_impl g_ball_impl 
      g_bex_impl g_size_impl g_size_abort_impl g_union_impl g_union_dj_impl
      g_diff_impl g_filter_impl g_inter_impl
      g_subset_impl g_equal_impl g_disjoint_impl
      g_disjoint_witness_impl g_sel'_impl g_to_list_impl
      g_from_list_impl
    )+
    done
end

context StdBasicOSetDefs
begin
  definition "g_min s P ≡ iterateoi s (λx. x = None) 
    (λx _. if P x then Some x else None) None"
  definition "g_max s P ≡ rev_iterateoi s (λx. x = None)
    (λx _. if P x then Some x else None) None"

  definition "g_to_sorted_list s ≡ rev_iterateo s (#) []"
  definition "g_to_rev_list s ≡ iterateo s (#) []"

  definition dflt_oops :: "('x::linorder,'s) oset_ops" 
    where [icf_rec_def]:
    "dflt_oops ≡ set_ops.extend 
      dflt_ops
      ⦇ 
        set_op_ordered_list_it = ordered_list_it,
        set_op_rev_list_it = rev_list_it,
        set_op_min = g_min,
        set_op_max = g_max,
        set_op_to_sorted_list = g_to_sorted_list,
        set_op_to_rev_list = g_to_rev_list
      ⦈"
  local_setup ‹Locale_Code.lc_decl_del @{term dflt_oops}›

end

context StdBasicOSet
begin
  lemma g_min_impl: "set_min α invar g_min"
  proof 
    fix s P

    assume I: "invar s"
  
    from iterateoi_correct[OF I]
    have iti': "set_iterator_linord (iterateoi s) (α s)" by simp
    note sel_correct = iterate_sel_no_map_linord_correct[OF iti', of P]

    have A: "g_min s P = iterate_sel_no_map (iterateoi s) P"
      unfolding g_min_def iterate_sel_no_map_def iterate_sel_def by simp
  
    { fix x
      assume "x∈α s" "P x"
      with sel_correct 
      show "g_min s P ∈ Some ` {x∈α s. P x}" and "the (g_min s P) ≤ x"
        unfolding A by auto
    }

    { assume "{x∈α s. P x} = {}"        
       with sel_correct show "g_min s P = None"
        unfolding A by auto
    }
  qed

  lemma g_max_impl: "set_max α invar g_max"
  proof 
    fix s P

    assume I: "invar s"
  
    from rev_iterateoi_correct[OF I]
    have iti': "set_iterator_rev_linord (rev_iterateoi s) (α s)" by simp
    note sel_correct = iterate_sel_no_map_rev_linord_correct[OF iti', of P]

    have A: "g_max s P = iterate_sel_no_map (rev_iterateoi s) P"
      unfolding g_max_def iterate_sel_no_map_def iterate_sel_def by simp
  
    { fix x
      assume "x∈α s" "P x"
      with sel_correct 
      show "g_max s P ∈ Some ` {x∈α s. P x}" and "the (g_max s P) ≥ x"
        unfolding A by auto
    }

    { assume "{x∈α s. P x} = {}"        
       with sel_correct show "g_max s P = None"
        unfolding A by auto
    }
  qed

  lemma g_to_sorted_list_impl: "set_to_sorted_list α invar g_to_sorted_list"
  proof 
    fix s
    assume I: "invar s"
    note iti = rev_iterateoi_correct[OF I]
    from iterate_to_list_rev_linord_correct[OF iti]
    show "sorted (g_to_sorted_list s)" 
         "distinct (g_to_sorted_list s)"
         "set (g_to_sorted_list s) = α s" 
      unfolding g_to_sorted_list_def iterate_to_list_def by simp_all
  qed

  lemma g_to_rev_list_impl: "set_to_rev_list α invar g_to_rev_list"
  proof 
    fix s
    assume I: "invar s"
    note iti = iterateoi_correct[OF I]
    from iterate_to_list_linord_correct[OF iti]
    show "sorted (rev (g_to_rev_list s))" 
         "distinct (g_to_rev_list s)"
         "set (g_to_rev_list s) = α s" 
      unfolding g_to_rev_list_def iterate_to_list_def 
      by (simp_all)
  qed

  lemma dflt_oops_impl: "StdOSet dflt_oops"
  proof -
    interpret aux: StdSet dflt_ops by (rule dflt_ops_impl)

    show ?thesis
      apply (rule StdOSet_intro)
      apply icf_locales
      apply (simp_all add: icf_rec_unf)
      apply (rule g_min_impl)
      apply (rule g_max_impl)
      apply (rule g_to_sorted_list_impl)
      apply (rule g_to_rev_list_impl)
      done
  qed

end

subsection "More Generic Set Algorithms"
text ‹
  These algorithms do not have a function specification in a locale, but
  their specification is done  ad-hoc in the correctness lemma.
›

subsubsection "Image and Filter of Cartesian Product"

locale image_filter_cp_defs_loc =
  s1: StdSetDefs ops1 +
  s2: StdSetDefs ops2 +
  s3: StdSetDefs ops3
  for ops1 :: "('x,'s1,'more1) set_ops_scheme"
  and ops2 :: "('y,'s2,'more2) set_ops_scheme"
  and ops3 :: "('z,'s3,'more3) set_ops_scheme"
begin

  definition "image_filter_cartesian_product f s1 s2 ==
    s1.iterate s1 (λx res.
      s2.iterate s2 (λy res.
        case (f (x, y)) of 
          None ⇒ res
        | Some z ⇒ (s3.ins z res)
      ) res
    ) (s3.empty ())"

  lemma image_filter_cartesian_product_alt:
    "image_filter_cartesian_product f s1 s2 ==
     iterate_to_set s3.empty s3.ins (set_iterator_image_filter f (
       set_iterator_product (s1.iteratei s1) (λ_. s2.iteratei s2)))"
    unfolding image_filter_cartesian_product_def iterate_to_set_alt_def
      set_iterator_image_filter_def set_iterator_product_def 
    by simp

  definition image_filter_cp where
    "image_filter_cp f P s1 s2 ≡
     image_filter_cartesian_product 
      (λxy. if P xy then Some (f xy) else None) s1 s2"

end

locale image_filter_cp_loc = image_filter_cp_defs_loc ops1 ops2 ops3 +
  s1: StdSet ops1 +
  s2: StdSet ops2 +
  s3: StdSet ops3
  for ops1 :: "('x,'s1,'more1) set_ops_scheme"
  and ops2 :: "('y,'s2,'more2) set_ops_scheme"
  and ops3 :: "('z,'s3,'more3) set_ops_scheme"
begin

  lemma image_filter_cartesian_product_correct:
    fixes f :: "'x × 'y ⇀ 'z"
    assumes I[simp, intro!]: "s1.invar s1" "s2.invar s2"
    shows "s3.α (image_filter_cartesian_product f s1 s2) 
     = { z | x y z. f (x,y) = Some z ∧ x∈s1.α s1 ∧ y∈s2.α s2 }" (is ?T1)
    "s3.invar (image_filter_cartesian_product f s1 s2)" (is ?T2)
  proof -
    from set_iterator_product_correct 
      [OF s1.iteratei_correct[OF I(1)] s2.iteratei_correct[OF I(2)]]
      have it_s12: "set_iterator 
        (set_iterator_product (s1.iteratei s1) (λ_. s2.iteratei s2))
        (s1.α s1 × s2.α s2)" 
        by simp

      have LIS: 
        "set_ins s3.α s3.invar s3.ins" 
        "set_empty s3.α s3.invar s3.empty"
        by unfold_locales
  
      from iterate_image_filter_to_set_correct[OF LIS it_s12, of f]
      show ?T1 ?T2
        unfolding image_filter_cartesian_product_alt by auto
  qed

  lemma image_filter_cp_correct:
    assumes I: "s1.invar s1" "s2.invar s2"
    shows 
    "s3.α (image_filter_cp f P s1 s2) 
     = { f (x, y) | x y. P (x, y) ∧ x∈s1.α s1 ∧ y∈s2.α s2 }" (is ?T1)
    "s3.invar (image_filter_cp f P s1 s2)" (is ?T2)
  proof -
    from image_filter_cartesian_product_correct [OF I]
    show "?T1" "?T2"
      unfolding image_filter_cp_def
      by auto
  qed

end

locale inj_image_filter_cp_defs_loc =
  s1: StdSetDefs ops1 +
  s2: StdSetDefs ops2 +
  s3: StdSetDefs ops3
  for ops1 :: "('x,'s1,'more1) set_ops_scheme"
  and ops2 :: "('y,'s2,'more2) set_ops_scheme"
  and ops3 :: "('z,'s3,'more3) set_ops_scheme"
begin

  definition "inj_image_filter_cartesian_product f s1 s2 ==
    s1.iterate s1 (λx res.
      s2.iterate s2 (λy res.
        case (f (x, y)) of 
          None ⇒ res
        | Some z ⇒ (s3.ins_dj z res)
      ) res
    ) (s3.empty ())"

  lemma inj_image_filter_cartesian_product_alt:
    "inj_image_filter_cartesian_product f s1 s2 ==
     iterate_to_set s3.empty s3.ins_dj (set_iterator_image_filter f (
       set_iterator_product (s1.iteratei s1) (λ_. s2.iteratei s2)))"
    unfolding inj_image_filter_cartesian_product_def iterate_to_set_alt_def
      set_iterator_image_filter_def set_iterator_product_def 
    by simp

  definition inj_image_filter_cp where
    "inj_image_filter_cp f P s1 s2 ≡
     inj_image_filter_cartesian_product 
      (λxy. if P xy then Some (f xy) else None) s1 s2"

end

locale inj_image_filter_cp_loc = inj_image_filter_cp_defs_loc ops1 ops2 ops3 +
  s1: StdSet ops1 +
  s2: StdSet ops2 +
  s3: StdSet ops3
  for ops1 :: "('x,'s1,'more1) set_ops_scheme"
  and ops2 :: "('y,'s2,'more2) set_ops_scheme"
  and ops3 :: "('z,'s3,'more3) set_ops_scheme"
begin

  lemma inj_image_filter_cartesian_product_correct:
    fixes f :: "'x × 'y ⇀ 'z"
    assumes I[simp, intro!]: "s1.invar s1" "s2.invar s2"
    assumes INJ: "inj_on f (s1.α s1 × s2.α s2 ∩ dom f)"
    shows "s3.α (inj_image_filter_cartesian_product f s1 s2) 
     = { z | x y z. f (x,y) = Some z ∧ x∈s1.α s1 ∧ y∈s2.α s2 }" (is ?T1)
    "s3.invar (inj_image_filter_cartesian_product f s1 s2)" (is ?T2)
  proof -
    from set_iterator_product_correct 
      [OF s1.iteratei_correct[OF I(1)] s2.iteratei_correct[OF I(2)]]
      have it_s12: "set_iterator 
        (set_iterator_product (s1.iteratei s1) (λ_. s2.iteratei s2))
        (s1.α s1 × s2.α s2)" 
        by simp

      have LIS: 
        "set_ins_dj s3.α s3.invar s3.ins_dj" 
        "set_empty s3.α s3.invar s3.empty"
        by unfold_locales
  
      from iterate_inj_image_filter_to_set_correct[OF LIS it_s12 INJ]
      show ?T1 ?T2
        unfolding inj_image_filter_cartesian_product_alt by auto
  qed

  lemma inj_image_filter_cp_correct:
    assumes I: "s1.invar s1" "s2.invar s2"
    assumes INJ: "inj_on f {x∈s1.α s1 × s2.α s2. P x}"
    shows 
    "s3.α (inj_image_filter_cp f P s1 s2) 
     = { f (x, y) | x y. P (x, y) ∧ x∈s1.α s1 ∧ y∈s2.α s2 }" (is ?T1)
    "s3.invar (inj_image_filter_cp f P s1 s2)" (is ?T2)
  proof -
    let ?f = "λxy. if P xy then Some (f xy) else None"
    from INJ have INJ': "inj_on ?f (s1.α s1 × s2.α s2 ∩ dom ?f)"
      by (force intro!: inj_onI dest: inj_onD split: if_split_asm)

    from inj_image_filter_cartesian_product_correct [OF I INJ']
    show "?T1" "?T2"
      unfolding inj_image_filter_cp_def
      by auto
  qed

end


subsubsection "Cartesian Product"

locale cart_defs_loc = inj_image_filter_cp_defs_loc ops1 ops2 ops3
  for ops1 :: "('x,'s1,'more1) set_ops_scheme"
  and ops2 :: "('y,'s2,'more2) set_ops_scheme"
  and ops3 :: "('x×'y,'s3,'more3) set_ops_scheme"
begin

  definition "cart s1 s2 ≡
    s1.iterate s1 
      (λx. s2.iterate s2 (λy res. s3.ins_dj (x,y) res)) 
      (s3.empty ())"

  lemma cart_alt: "cart s1 s2 == 
    inj_image_filter_cartesian_product Some s1 s2"
    unfolding cart_def inj_image_filter_cartesian_product_def
    by simp

end

locale cart_loc = cart_defs_loc ops1 ops2 ops3 
  + inj_image_filter_cp_loc ops1 ops2 ops3
  for ops1 :: "('x,'s1,'more1) set_ops_scheme"
  and ops2 :: "('y,'s2,'more2) set_ops_scheme"
  and ops3 :: "('x×'y,'s3,'more3) set_ops_scheme"
begin

  lemma cart_correct:
    assumes I[simp, intro!]: "s1.invar s1" "s2.invar s2"
    shows "s3.α (cart s1 s2) 
           = s1.α s1 × s2.α s2" (is ?T1)
    "s3.invar (cart s1 s2)" (is ?T2)
    unfolding cart_alt
    by (auto simp add: 
      inj_image_filter_cartesian_product_correct[OF I, where f=Some])

end


subsection ‹Generic Algorithms outside basic-set›
text ‹
  In this section, we present some generic algorithms that are not
  formulated in terms of basic-set. They are useful for setting up 
  some data structures.
›

subsection ‹Image (by image-filter)›
definition "iflt_image iflt f s == iflt (λx. Some (f x)) s"

lemma iflt_image_correct:
  assumes "set_image_filter α1 invar1 α2 invar2 iflt"
  shows "set_image α1 invar1 α2 invar2 (iflt_image iflt)"
proof -
  interpret set_image_filter α1 invar1 α2 invar2 iflt by fact
  show ?thesis
    apply (unfold_locales)
    apply (unfold iflt_image_def)
    apply (auto simp add: image_filter_correct)
    done
qed

subsection‹Injective Image-Filter (by image-filter)›

definition [code_unfold]: "iflt_inj_image = iflt_image"

lemma iflt_inj_image_correct:
  assumes "set_inj_image_filter α1 invar1 α2 invar2 iflt"
  shows "set_inj_image α1 invar1 α2 invar2 (iflt_inj_image iflt)"
proof -
  interpret set_inj_image_filter α1 invar1 α2 invar2 iflt by fact

  show ?thesis
    apply (unfold_locales)
    apply (unfold iflt_image_def iflt_inj_image_def)
    apply (subst inj_image_filter_correct)
    apply (auto simp add: dom_const intro: inj_onI dest: inj_onD)
    apply (subst inj_image_filter_correct)
    apply (auto simp add: dom_const intro: inj_onI dest: inj_onD)
    done
qed


subsection‹Filter (by image-filter)›
definition "iflt_filter iflt P s == iflt (λx. if P x then Some x else None) s"

lemma iflt_filter_correct:
  fixes α1 :: "'s1 ⇒ 'a set"
  fixes α2 :: "'s2 ⇒ 'a set"
  assumes "set_inj_image_filter α1 invar1 α2 invar2 iflt"
  shows "set_filter α1 invar1 α2 invar2 (iflt_filter iflt)"
proof (rule set_filter.intro)
  fix s P
  assume invar_s: "invar1 s"
  interpret S: set_inj_image_filter α1 invar1 α2 invar2 iflt by fact

  let ?f' = "λx::'a. if P x then Some x else None"
  have inj_f': "inj_on ?f' (α1 s ∩ dom ?f')"
    by (simp add: inj_on_def Ball_def domIff)
  note correct' = S.inj_image_filter_correct [OF invar_s inj_f',
    folded iflt_filter_def]

  show "invar2 (iflt_filter iflt P s)"
       "α2 (iflt_filter iflt P s) = {e ∈ α1 s. P e}"
    by (auto simp add: correct')
qed

end