Session Collections

Theory Sorted_List_Operations

section ‹\isaheader{Operations on sorted Lists}›
theory Sorted_List_Operations
imports Main Automatic_Refinement.Misc
begin 

fun inter_sorted :: "'a::{linorder} list  'a list  'a list" where
   "inter_sorted [] l2 = []"
 | "inter_sorted l1 [] = []"
 | "inter_sorted (x1 # l1) (x2 # l2) =
    (if (x1 < x2) then (inter_sorted l1 (x2 # l2)) else 
     (if (x1 = x2) then x1 # (inter_sorted l1 l2) else inter_sorted (x1 # l1) l2))"

lemma inter_sorted_correct :
assumes l1_OK: "distinct l1  sorted l1"
assumes l2_OK: "distinct l2  sorted l2"
shows "distinct (inter_sorted l1 l2)  sorted (inter_sorted l1 l2)  
       set (inter_sorted l1 l2) = set l1  set l2"
using assms
proof (induct l1 arbitrary: l2) 
  case Nil thus ?case by simp
next
  case (Cons x1 l1 l2) 
  note x1_l1_props = Cons(2)
  note l2_props = Cons(3)

  from x1_l1_props have l1_props: "distinct l1  sorted l1"
                    and x1_nin_l1: "x1  set l1"
                    and x1_le: "x. x  set l1  x1  x"
    by (simp_all add: Ball_def)

  note ind_hyp_l1 = Cons(1)[OF l1_props]

  show ?case
  using l2_props 
  proof (induct l2)
    case Nil with x1_l1_props show ?case by simp
  next
    case (Cons x2 l2)
    note x2_l2_props = Cons(2)
    from x2_l2_props have l2_props: "distinct l2  sorted l2"
                    and x2_nin_l2: "x2  set l2"
                    and x2_le: "x. x  set l2  x2  x"
    by (simp_all add: Ball_def)

    note ind_hyp_l2 = Cons(1)[OF l2_props]
    show ?case
    proof (cases "x1 < x2")
      case True note x1_less_x2 = this

      from ind_hyp_l1[OF x2_l2_props] x1_less_x2 x1_nin_l1 x1_le x2_le
      show ?thesis
        apply (auto simp add: Ball_def)
        apply (metis linorder_not_le)
      done
    next
      case False note x2_le_x1 = this
      
      show ?thesis
      proof (cases "x1 = x2")
        case True note x1_eq_x2 = this

        from ind_hyp_l1[OF l2_props] x1_le x2_le x2_nin_l2 x1_eq_x2 x1_nin_l1
        show ?thesis by (simp add: x1_eq_x2 Ball_def)
      next
        case False note x1_neq_x2 = this
        with x2_le_x1 have x2_less_x1 : "x2 < x1" by auto

        from ind_hyp_l2 x2_le_x1 x1_neq_x2 x2_le x2_nin_l2 x1_le
        show ?thesis 
          apply (auto simp add: x2_less_x1 Ball_def)
          apply (metis linorder_not_le x2_less_x1)
        done
      qed
    qed
  qed
qed

fun diff_sorted :: "'a::{linorder} list  'a list  'a list" where
   "diff_sorted [] l2 = []"
 | "diff_sorted l1 [] = l1"
 | "diff_sorted (x1 # l1) (x2 # l2) =
    (if (x1 < x2) then x1 # (diff_sorted l1 (x2 # l2)) else 
     (if (x1 = x2) then (diff_sorted l1 l2) else diff_sorted (x1 # l1) l2))"

lemma diff_sorted_correct :
assumes l1_OK: "distinct l1  sorted l1"
assumes l2_OK: "distinct l2  sorted l2"
shows "distinct (diff_sorted l1 l2)  sorted (diff_sorted l1 l2)  
       set (diff_sorted l1 l2) = set l1 - set l2"
using assms
proof (induct l1 arbitrary: l2) 
  case Nil thus ?case by simp
next
  case (Cons x1 l1 l2) 
  note x1_l1_props = Cons(2)
  note l2_props = Cons(3)

  from x1_l1_props have l1_props: "distinct l1  sorted l1"
                    and x1_nin_l1: "x1  set l1"
                    and x1_le: "x. x  set l1  x1  x"
    by (simp_all add: Ball_def)

  note ind_hyp_l1 = Cons(1)[OF l1_props]

  show ?case
  using l2_props 
  proof (induct l2)
    case Nil with x1_l1_props show ?case by simp
  next
    case (Cons x2 l2)
    note x2_l2_props = Cons(2)
    from x2_l2_props have l2_props: "distinct l2  sorted l2"
                    and x2_nin_l2: "x2  set l2"
                    and x2_le: "x. x  set l2  x2  x"
    by (simp_all add: Ball_def)

    note ind_hyp_l2 = Cons(1)[OF l2_props]
    show ?case
    proof (cases "x1 < x2")
      case True note x1_less_x2 = this

      from ind_hyp_l1[OF x2_l2_props] x1_less_x2 x1_nin_l1 x1_le x2_le
      show ?thesis
        apply simp
        apply (simp add: Ball_def set_eq_iff)
        apply (metis linorder_not_le order_less_imp_not_eq2)
      done
    next
      case False note x2_le_x1 = this
      
      show ?thesis
      proof (cases "x1 = x2")
        case True note x1_eq_x2 = this

        from ind_hyp_l1[OF l2_props] x1_le x2_le x2_nin_l2 x1_eq_x2 x1_nin_l1
        show ?thesis by (simp add: x1_eq_x2 Ball_def)
      next
        case False note x1_neq_x2 = this
        with x2_le_x1 have x2_less_x1 : "x2 < x1" by auto

        from x2_less_x1 x1_le have x2_nin_l1: "x2  set l1"
           by (metis linorder_not_less)

        from ind_hyp_l2 x1_le x2_nin_l1
        show ?thesis 
          apply (simp add: x2_less_x1 x1_neq_x2 x2_le_x1 x1_nin_l1 Ball_def set_eq_iff)
          apply (metis x1_neq_x2)
        done
      qed
    qed
  qed
qed

fun subset_sorted :: "'a::{linorder} list  'a list  bool" where
   "subset_sorted [] l2 = True"
 | "subset_sorted (x1 # l1) [] = False"
 | "subset_sorted (x1 # l1) (x2 # l2) =
    (if (x1 < x2) then False else 
     (if (x1 = x2) then (subset_sorted l1 l2) else subset_sorted (x1 # l1) l2))"

lemma subset_sorted_correct :
assumes l1_OK: "distinct l1  sorted l1"
assumes l2_OK: "distinct l2  sorted l2"
shows "subset_sorted l1 l2  set l1  set l2"
using assms
proof (induct l1 arbitrary: l2) 
  case Nil thus ?case by simp
next
  case (Cons x1 l1 l2) 
  note x1_l1_props = Cons(2)
  note l2_props = Cons(3)

  from x1_l1_props have l1_props: "distinct l1  sorted l1"
                    and x1_nin_l1: "x1  set l1"
                    and x1_le: "x. x  set l1  x1  x"
    by (simp_all add: Ball_def)

  note ind_hyp_l1 = Cons(1)[OF l1_props]

  show ?case
  using l2_props 
  proof (induct l2)
    case Nil with x1_l1_props show ?case by simp
  next
    case (Cons x2 l2)
    note x2_l2_props = Cons(2)
    from x2_l2_props have l2_props: "distinct l2  sorted l2"
                    and x2_nin_l2: "x2  set l2"
                    and x2_le: "x. x  set l2  x2  x"
    by (simp_all add: Ball_def)

    note ind_hyp_l2 = Cons(1)[OF l2_props]
    show ?case
    proof (cases "x1 < x2")
      case True note x1_less_x2 = this

      from ind_hyp_l1[OF x2_l2_props] x1_less_x2 x1_nin_l1 x1_le x2_le
      show ?thesis
        apply (auto simp add: Ball_def)
        apply (metis linorder_not_le)
      done
    next
      case False note x2_le_x1 = this
      
      show ?thesis
      proof (cases "x1 = x2")
        case True note x1_eq_x2 = this

        from ind_hyp_l1[OF l2_props] x1_le x2_le x2_nin_l2 x1_eq_x2 x1_nin_l1
        show ?thesis 
          apply (simp add: subset_iff x1_eq_x2 Ball_def)
          apply metis
        done
      next
        case False note x1_neq_x2 = this
        with x2_le_x1 have x2_less_x1 : "x2 < x1" by auto

        from ind_hyp_l2 x2_le_x1 x1_neq_x2 x2_le x2_nin_l2 x1_le
        show ?thesis 
          apply (simp add: subset_iff x2_less_x1 Ball_def)
          apply (metis linorder_not_le x2_less_x1)
        done
      qed
    qed
  qed
qed

lemma set_eq_sorted_correct :
  assumes l1_OK: "distinct l1  sorted l1"
  assumes l2_OK: "distinct l2  sorted l2"
  shows "l1 = l2  set l1 = set l2"
  using assms
proof -
  have l12_eq: "l1 = l2  subset_sorted l1 l2  subset_sorted l2 l1"
  proof (induct l1 arbitrary: l2)
    case Nil thus ?case by (cases l2) auto
  next
    case (Cons x1 l1')
    note ind_hyp = Cons(1)

    show ?case
    proof (cases l2)
      case Nil thus ?thesis by simp
    next
      case (Cons x2 l2')
      thus ?thesis by (simp add: ind_hyp)
    qed
  qed
  also have "  ((set l1  set l2)  (set l2  set l1))"
    using subset_sorted_correct[OF l1_OK l2_OK] subset_sorted_correct[OF l2_OK l1_OK]
    by simp
  also have "  set l1 = set l2" by auto
  finally show ?thesis .
qed

fun memb_sorted where
   "memb_sorted [] x = False"
 | "memb_sorted (y # xs) x =
    (if (y < x) then memb_sorted xs x else (x = y))"

lemma memb_sorted_correct :
  "sorted xs  memb_sorted xs x  x  set xs"
by (induct xs) (auto simp add: Ball_def)


fun insertion_sort where
   "insertion_sort x [] = [x]"
 | "insertion_sort x (y # xs) =
    (if (y < x) then y # insertion_sort x xs else 
     (if (x = y) then y # xs else x # y # xs))"

lemma insertion_sort_correct :
  "sorted xs  distinct xs 
   distinct (insertion_sort x xs)  
   sorted (insertion_sort x xs) 
   set (insertion_sort x xs) = set (x # xs)"
by (induct xs) (auto simp add: Ball_def)

fun delete_sorted where
   "delete_sorted x [] = []"
 | "delete_sorted x (y # xs) =
    (if (y < x) then y # delete_sorted x xs else 
     (if (x = y) then xs else y # xs))"

lemma delete_sorted_correct :
  "sorted xs  distinct xs 
   distinct (delete_sorted x xs)  
   sorted (delete_sorted x xs) 
   set (delete_sorted x xs) = set xs - {x}"
apply (induct xs) 
apply simp
apply (simp add: Ball_def set_eq_iff)
apply (metis order_less_le)
done

end

Theory HashCode

(*  Title:       Isabelle Collections Library
    Author:      Peter Lammich <peter dot lammich at uni-muenster.de>
                 Philipp Meyer <meyerphi@in.tum.de>
*)
section ‹\isaheader {The hashable Typeclass}›
theory HashCode
imports 
  Native_Word.Uint32 
begin

text_raw ‹\label{thy:HashCode}›

text ‹
  In this theory a typeclass of hashable types is established.
  For hashable types, there is a function hashcode›, that
  maps any entity of this type to an unsigned 32 bit word value.

  This theory defines the hashable typeclass and provides instantiations
  for a couple of standard types.
›

type_synonym
  hashcode = "uint32"

definition "nat_of_hashcode  nat_of_uint32"
definition "int_of_hashcode  int_of_uint32"
definition "integer_of_hashcode  integer_of_uint32"

class hashable =
  fixes hashcode :: "'a  hashcode"
  and def_hashmap_size :: "'a itself  nat"
  assumes def_hashmap_size: "1 < def_hashmap_size TYPE('a)"
begin
  definition bounded_hashcode :: "uint32  'a  uint32" where
    "bounded_hashcode n x = (hashcode x) mod n"
 
  lemma bounded_hashcode_bounds: "1 < n  bounded_hashcode n a < n"
    unfolding bounded_hashcode_def
    by (transfer, simp add: word_less_def uint_mod)

  definition bounded_hashcode_nat :: "nat  'a  nat" where
    "bounded_hashcode_nat n x = nat_of_hashcode (hashcode x) mod n"

  lemma bounded_hashcode_nat_bounds: "1 < n  bounded_hashcode_nat n a < n"
    unfolding bounded_hashcode_nat_def
    by transfer simp
end

instantiation unit :: hashable
begin
  definition [simp]: "hashcode (u :: unit) = 0"
  definition "def_hashmap_size = (λ_ :: unit itself. 2)"
  instance
    by (intro_classes)(simp_all add: def_hashmap_size_unit_def)
end

instantiation bool :: hashable
begin
  definition [simp]: "hashcode (b :: bool) = (if b then 1 else 0)"
  definition "def_hashmap_size = (λ_ :: bool itself. 2)"
  instance by (intro_classes)(simp_all add: def_hashmap_size_bool_def)
end

instantiation "int" :: hashable
begin
  definition [simp]: "hashcode (i :: int) = uint32_of_int i"
  definition "def_hashmap_size = (λ_ :: int itself. 16)"
  instance by(intro_classes)(simp_all add: def_hashmap_size_int_def)
end

instantiation "integer" :: hashable
begin
  definition [simp]: "hashcode (i :: integer) = Uint32 i"
  definition "def_hashmap_size = (λ_ :: integer itself. 16)"
  instance by(intro_classes)(simp_all add: def_hashmap_size_integer_def)
end

instantiation "nat" :: hashable
begin
  definition [simp]: "hashcode (n :: nat) = uint32_of_int (int n)"
  definition "def_hashmap_size = (λ_ :: nat itself. 16)"
  instance by(intro_classes)(simp_all add: def_hashmap_size_nat_def)
end

instantiation char :: hashable
begin
  definition [simp]: "hashcode (c :: char) == uint32_of_int (of_char c)"
  definition "def_hashmap_size = (λ_ :: char itself. 32)"
  instance by(intro_classes)(simp_all add: def_hashmap_size_char_def)
end

instantiation prod :: (hashable, hashable) hashable
begin
  definition "hashcode x == (hashcode (fst x) * 33 + hashcode (snd x))"
  definition "def_hashmap_size = (λ_ :: ('a × 'b) itself. def_hashmap_size TYPE('a) + def_hashmap_size TYPE('b))"
  instance using def_hashmap_size[where ?'a="'a"] def_hashmap_size[where ?'a="'b"]
    by(intro_classes)(simp_all add: def_hashmap_size_prod_def)
end

instantiation sum :: (hashable, hashable) hashable
begin
  definition "hashcode x == (case x of Inl a  2 * hashcode a | Inr b  2 * hashcode b + 1)"
  definition "def_hashmap_size = (λ_ :: ('a + 'b) itself. def_hashmap_size TYPE('a) + def_hashmap_size TYPE('b))"
  instance using def_hashmap_size[where ?'a="'a"] def_hashmap_size[where ?'a="'b"]
    by(intro_classes)(simp_all add: bounded_hashcode_bounds def_hashmap_size_sum_def split: sum.split)
end

instantiation list :: (hashable) hashable
begin
  definition "hashcode = foldl (λh x. h * 33 + hashcode x) 5381"
  definition "def_hashmap_size = (λ_ :: 'a list itself. 2 * def_hashmap_size TYPE('a))"
  instance
  proof
    from def_hashmap_size[where ?'a = "'a"]
    show "1 < def_hashmap_size TYPE('a list)"
      by(simp add: def_hashmap_size_list_def)
  qed
end

instantiation option :: (hashable) hashable
begin
  definition "hashcode opt = (case opt of None  0 | Some a  hashcode a + 1)"
  definition "def_hashmap_size = (λ_ :: 'a option itself. def_hashmap_size TYPE('a) + 1)"
  instance using def_hashmap_size[where ?'a = "'a"]
    by(intro_classes)(simp_all add: def_hashmap_size_option_def split: option.split)
end

lemma hashcode_option_simps [simp]:
  "hashcode None = 0"
  "hashcode (Some a) = 1 + hashcode a"
  by(simp_all add: hashcode_option_def)

lemma bounded_hashcode_option_simps [simp]:
  "bounded_hashcode n None = 0"
  "bounded_hashcode n (Some a) = (hashcode a + 1) mod n"
  by (simp_all add: bounded_hashcode_def ac_simps)

(*
lemma bounded_hashcode_option_simps [simp]:
  "bounded_hashcode n None = 0"
  "bounded_hashcode n (Some a) = (bounded_hashcode n a + 1) mod n"
  apply (simp_all add: bounded_hashcode_def, transfer, simp_all add: word_mod_def)
  apply (simp_all add: algebra_simps mod_add_right_eq)
*)

instantiation String.literal :: hashable
begin

definition hashcode_literal :: "String.literal  uint32" 
  where "hashcode_literal s = hashcode (String.explode s)"

definition def_hashmap_size_literal  :: "String.literal itself  nat"
  where "def_hashmap_size_literal _ = 10"

instance
  by standard (simp_all only: def_hashmap_size_literal_def)

end


hide_type (open) word

end

Theory Code_Target_ICF

section ‹Default Code Generator Setup for the Isabelle Collection Framework›
theory Code_Target_ICF
imports   
  "HOL-Library.Code_Target_Numeral"
  Native_Word.Code_Target_Bits_Int
begin

end

Theory SetIterator

(*  Title:       Iterators over Finite Sets
    Author:      Thomas Tuerk <tuerk@in.tum.de>
    Maintainer:  Thomas Tuerk <tuerk@in.tum.de>
*)
section ‹\isaheader{Iterators over Finite Sets}›
theory SetIterator
imports 
  Automatic_Refinement.Misc 
  Automatic_Refinement.Foldi 
  (*"../../Refine_Monadic/Refine_Monadic"*)
begin

text ‹When reasoning about finite sets, it is often handy to be able to iterate over the elements
  of the set. If the finite set is represented by a list, the @{term fold} operation can be used.
  For general finite sets, the order of elements is not fixed though. Therefore, nondeterministic
  iterators are introduced in this theory.›

subsection ‹General Iterators›

type_synonym ('x,) set_iterator = "(bool)  ('x)    "

locale set_iterator_genord =
  fixes iti::"('x,) set_iterator" 
    and S0::"'x set" 
    and R::"'x  'x  bool"
  assumes foldli_transform:
    "l0. distinct l0  S0 = set l0  sorted_wrt R l0  iti = foldli l0"
begin
  text ‹Let's prove some trivial lemmata to show that the formalisation agrees with
          the view of iterators described above.›
  lemma set_iterator_weaken_R :
    "(x y. x  S0; y  S0; R x y  R' x y)  
             set_iterator_genord iti S0 R'"
    by (metis set_iterator_genord.intro foldli_transform sorted_wrt_mono_rel)

  lemma finite_S0 :
    shows "finite S0"
    by (metis finite_set foldli_transform)

  lemma iti_stop_rule_cond :
    assumes not_c: "¬(c σ)"
    shows "iti c f σ = σ"
  proof -
    from foldli_transform obtain l0 where l0_props:
      "iti c = foldli l0 c" by blast
    with foldli_not_cond [of c σ l0 f, OF not_c]
    show ?thesis by simp
  qed

  lemma iti_stop_rule_emp :
    assumes S0_emp: "S0 = {}"
    shows "iti c f σ = σ"
  proof -
    from foldli_transform obtain l0 where l0_props:
      "S0 = set l0" "iti c = foldli l0 c" by blast
    with foldli.simps(1) [of c f σ] S0_emp
    show ?thesis by simp
  qed

  text ‹Reducing everything to folding is cumbersome. Let's
          define a few high-level inference rules.›

  lemma iteratei_rule_P:
    assumes 
      "I S0 σ0"
      "S σ x.  c σ; x  S; I S σ; S  S0; 
                 yS - {x}. R x y; yS0 - S. R y x 
                  I (S - {x}) (f x σ)"
      "σ. I {} σ  P σ"
      "σ S.  S  S0; S  {}; ¬ c σ; I S σ;
               xS. yS0-S. R y x   P σ"
    shows "P (iti c f σ0)"
  proof -
    { fix P I σ0 f
      assume
        I: "I S0 σ0" and 
        R: "S σ x. c σ; x  S; I S σ; S  S0; yS-{x}. R x y  I (S - {x}) (f x σ)" and
        C1: "I {} (iti c f σ0)  P" and
        C2:"S. S  S0; S  {}; ¬ c (iti c f σ0); I S (iti c f σ0)  P"

      from foldli_transform obtain l0 where l0_props:
         "distinct l0" "S0 = set l0" "sorted_wrt R l0"  "iti c = foldli l0 c" by auto

      from I R  
      have "I {} (iti c f σ0)  
          (S. S  S0  S  {}  
               ¬ (c (iti c f σ0))  
               I S (iti c f σ0))" 
        unfolding l0_props using l0_props(1,3)
      proof (induct l0 arbitrary: σ0)
        case Nil thus ?case by simp
      next
        case (Cons x l0)
        note ind_hyp = Cons(1)
        note I_x_l0 = Cons(2)
        note step = Cons(3)
        from Cons(4) have dist_l0: "distinct l0" and x_nin_l0: "x  set l0" by simp_all
        from Cons(5) have R_l0: "yset l0. R x y" and 
                          sort_l0: "sorted_wrt R l0" by simp_all

        show ?case
        proof (cases "c σ0")
          case False
          with I_x_l0 show ?thesis
            apply (rule_tac disjI2)
            apply (rule_tac exI[where x="set (x # l0)"])
            apply (simp)
          done
        next
          case True note c_σ0 = this

          from step[of σ0 x "set (x # l0)"] I_x_l0 R_l0 c_σ0 x_nin_l0
          have step': "I (set l0) (f x σ0)"
            by (simp_all add: Ball_def)

          from ind_hyp [OF step' step dist_l0 sort_l0]
          have "I {} (foldli l0 c f (f x σ0))  
                (S. S  set l0  S  {} 
                ¬ c (foldli l0 c f (f x σ0))  I S (foldli l0 c f (f x σ0)))" 
            by (fastforce)
          thus ?thesis
            by (simp add: c_σ0 subset_iff) metis
        qed
      qed
      with C1 C2 have "P" by blast
    } note aux = this

    from assms
    show ?thesis 
      apply (rule_tac aux [of "λS σ. I S σ  (xS. yS0-S. R y x)" σ0 f])
      apply auto
    done
  qed

  text ‹Instead of removing elements one by one from the invariant, adding them is sometimes more natural.›
  lemma iteratei_rule_insert_P:
  assumes pre :
      "I {} σ0"
      "S σ x.  c σ; x  S0 - S; I S σ; S  S0; y(S0 - S) - {x}. R x y;
                 yS. R y x 
                   I (insert x S) (f x σ)"
      "σ. I S0 σ  P σ"
      "σ S.  S  S0; S  S0; 
              ¬ (c σ); I S σ; xS0-S. yS. R y x   P σ"
  shows "P (iti c f σ0)"
  proof -
    let ?I' = "λS σ. I (S0 - S) σ"

    have pre1: 
      "!!σ S.  S  S0; S  {}; ¬ (c σ); ?I' S σ;
             xS. yS0-S. R y x  P σ"
    proof -
      fix S σ
      assume AA: 
        "S  S0" "S  {}"
        "¬ (c σ)" 
        "?I' S σ" "xS. yS0-S. R y x"
      with pre(4) [of "S0 - S"]
      show "P σ" by auto
    qed

    have pre2 :"x S σ. c σ; x  S; S  S0; ?I' S σ; yS - {x}. R x y; yS0-S. R y x   ?I' (S - {x}) (f x σ)"
    proof -
      fix x S σ
      assume AA : "c σ" "x  S" "S  S0" "?I' S σ" "yS - {x}. R x y" "yS0 - S. R y x" 

      from AA(2) AA(3) have "S0 - (S - {x}) = insert x (S0 - S)" "S0 - (S0 - S) = S" by auto
      moreover 
      note pre(2) [of σ x "S0 - S"] AA
      ultimately show "?I' (S - {x}) (f x σ)"
        by auto
    qed

    show "P (iti c f σ0)" 
      apply (rule iteratei_rule_P [of ?I' σ0 c f P])
      apply (simp add: pre)
      apply (rule pre2) apply simp_all
      apply (simp add: pre(3))
      apply (simp add: pre1)
    done
  qed

  text ‹Show that iti without interruption is related to fold›
  lemma iti_fold: 
  assumes lc_f: "comp_fun_commute f"
    shows "iti (λ_. True) f σ0 = Finite_Set.fold f σ0 S0"
  proof (rule iteratei_rule_insert_P [where I = "λX σ'. σ' = Finite_Set.fold f σ0 X"])
    fix S σ x
    assume "x  S0 - S" "S  S0" and σ_eq: "σ = Finite_Set.fold f σ0 S"
    from finite_S0 S  S0 have fin_S: "finite S" by (metis finite_subset)
    from x  S0 - S have x_nin_S: "x  S" by simp
    note fold_eq = comp_fun_commute.fold_insert [OF lc_f fin_S x_nin_S]

    show "f x σ = Finite_Set.fold f σ0 (insert x S)" 
      by (simp add: fold_eq σ_eq)
  qed simp_all
end


subsection ‹Iterators over Maps›

type_synonym ('k,'v,) map_iterator = "('k×'v,) set_iterator"

text ‹Iterator over the key-value pairs of a finite map are called iterators over maps.›
abbreviation "map_iterator_genord it m R  set_iterator_genord it (map_to_set m) R"

subsection ‹Unordered Iterators›

text ‹Often one does not care about the order in which the elements are processed. 
        Therefore, the selection function can be set to not impose any further restrictings.
        This leads to considerably simpler theorems.›

definition "set_iterator it S0  set_iterator_genord it S0 (λ_ _. True)"
abbreviation "map_iterator it m  set_iterator it (map_to_set m)"

lemma set_iterator_intro :
    "set_iterator_genord it S0 R  set_iterator it S0"
unfolding set_iterator_def
apply (rule set_iterator_genord.set_iterator_weaken_R [where R = R])
apply simp_all
done

lemma set_iterator_no_cond_rule_P:
" set_iterator it S0;
   I S0 σ0;
   !!S σ x.  x  S; I S σ; S  S0   I (S - {x}) (f x σ);
   !!σ. I {} σ  P σ
   P (it (λ_. True) f σ0)"
unfolding set_iterator_def
using set_iterator_genord.iteratei_rule_P [of it S0 "λ_ _. True" I σ0 "λ_. True" f P]
by simp 

lemma set_iterator_no_cond_rule_insert_P:
" set_iterator it S0;
   I {} σ0;
   !!S σ x.  x  S0 - S; I S σ; S  S0    I (insert x S) (f x σ);
   !!σ. I S0 σ  P σ
   P (it (λ_. True) f σ0)"
unfolding set_iterator_def
using set_iterator_genord.iteratei_rule_insert_P [of it S0 "λ_ _. True" I σ0 "λ_. True" f P]
by simp 

lemma set_iterator_rule_P:
" set_iterator it S0;
   I S0 σ0;
   !!S σ x.  c σ; x  S; I S σ; S  S0   I (S - {x}) (f x σ);
   !!σ. I {} σ  P σ;
   !!σ S. S  S0  S  {}  ¬ c σ  I S σ  P σ
   P (it c f σ0)"
unfolding set_iterator_def
using set_iterator_genord.iteratei_rule_P [of it S0 "λ_ _. True" I σ0 c f P]
by simp 

lemma set_iterator_rule_insert_P:
" set_iterator it S0;
   I {} σ0;
   !!S σ x.  c σ; x  S0 - S; I S σ; S  S0    I (insert x S) (f x σ);
   !!σ. I S0 σ  P σ;
   !!σ S. S  S0  S  S0  ¬ c σ  I S σ  P σ
   P (it c f σ0)"
unfolding set_iterator_def
using set_iterator_genord.iteratei_rule_insert_P [of it S0 "λ_ _. True" I σ0 c f P]
by simp  


text‹The following rules is adapted for maps. Instead of a set of key-value pairs the invariant
       now only sees the keys.›
lemma map_iterator_genord_rule_P:
  assumes "map_iterator_genord it m R"
      and I0: "I (dom m) σ0"
      and IP: "!!k v it σ.  c σ; k  it; m k = Some v; it  dom m; I it σ; 
                             k' v'. k'  it-{k}  m k' = Some v'  R (k, v) (k', v');
                             k' v'. k'  it  m k' = Some v'  R (k', v') (k, v)  
                            I (it - {k}) (f (k, v) σ)"
      and IF: "!!σ. I {} σ  P σ"
      and II: "!!σ it.  it  dom m; it  {}; ¬ c σ; I it σ;
                         k v k' v'. k  it  m k = Some v  k'  it  m k' = Some v'  
                                     R (k, v) (k', v')   P σ"
  shows "P (it c f σ0)"
proof (rule set_iterator_genord.iteratei_rule_P [of it "map_to_set m" R "λS σ. I (fst ` S) σ" σ0 c f P])
  show "map_iterator_genord it m R" by fact
next
  show "I (fst ` map_to_set m) σ0" using I0 by (simp add: map_to_set_dom[symmetric])
next
  fix σ
  assume "I (fst ` {}) σ"
  with IF show "P σ" by simp
next
  fix σ S
  assume "S  map_to_set m" "S  {}" "¬ c σ" "I (fst ` S) σ"  
         and R_prop: "xS. ymap_to_set m - S. R y x"
  let ?S' = "fst ` S"

  show "P σ"
  proof (rule II [where it = ?S'])
    from S  map_to_set m
    show "?S'  dom m"
      unfolding map_to_set_dom
      by auto
  next
    from S  {} show "?S'  {}" by auto
  next
    show "¬ (c σ)" by fact
  next
    show "I (fst ` S) σ" by fact
  next
    show "k v k' v'.
       k  fst ` S 
       m k = Some v 
       k'  fst ` S  m k' = Some v' 
       R (k, v) (k', v')" 
    proof (intro allI impI, elim conjE )
      fix k v k' v'
      assume pre_k: "k  fst ` S" "m k = Some v"
      assume pre_k': "k'  fst ` S" "m k' = Some v'"

      from S  map_to_set m pre_k' 
      have kv'_in: "(k', v')  S"
        unfolding map_to_set_def by auto

      from S  map_to_set m pre_k
      have kv_in: "(k, v)  map_to_set m - S"
        unfolding map_to_set_def 
        by (auto simp add: image_iff)

      from R_prop kv_in kv'_in
      show "R (k, v) (k',v')" by simp
    qed
  qed
next
  fix σ S kv
  assume "S  map_to_set m" "kv  S" "c σ" and I_S': "I (fst ` S) σ" and 
         R_S: "kv'S - {kv}. R kv kv'" and
         R_not_S: "kv'map_to_set m - S. R kv' kv"
  let ?S' = "fst ` S" 
  obtain k v where kv_eq[simp]: "kv = (k, v)" by (rule prod.exhaust)

  have "I (fst ` S - {k}) (f (k, v) σ)"
  proof (rule IP)
    show "c σ" by fact
  next
    from kv  S show "k  ?S'" by (auto simp add: image_iff Bex_def)
  next
    from kv  S S  map_to_set m 
    have "kv  map_to_set m" by auto
    thus m_k_eq: "m k = Some v" unfolding map_to_set_def by simp
  next
    from S  map_to_set m
    show S'_subset: "?S'  dom m"
      unfolding map_to_set_dom
      by auto
  next
    show "I (fst ` S) σ" by fact
  next
    from S  map_to_set m kv  S
    have S_simp: "{(k', v'). k'  (fst ` S) - {k}  m k' = Some v'} = S - {kv}"
      unfolding map_to_set_def subset_iff
      apply (auto simp add: image_iff Bex_def)
      apply (metis option.inject)
    done

    from R_S[unfolded S_simp[symmetric]] R_not_S
    show "k' v'. k'  fst ` S - {k}  m k' = Some v' 
                  R (k, v) (k', v') " 
      by simp
  next
    from S  map_to_set m R_not_S
    show "k' v'. k'  fst ` S  m k' = Some v'  R (k', v') (k, v)" 
      apply (simp add: Ball_def map_to_set_def subset_iff image_iff)
      apply metis
    done
  qed

  moreover 
    from S  map_to_set m kv  S
    have "fst ` (S - {kv}) = fst ` S - {k}"
      apply (simp add: set_eq_iff image_iff Bex_def map_to_set_def subset_iff)
      apply (metis option.inject)
    done

  ultimately show "I (fst ` (S - {kv})) (f kv σ)" by simp
qed

lemma map_iterator_genord_rule_insert_P:
  assumes "map_iterator_genord it m R"
      and I0: "I {} σ0"
      and IP: "!!k v it σ.  c σ; k  dom m - it; m k = Some v; it  dom m; I it σ; 
                             k' v'. k'  (dom m - it) - {k}  m k' = Some v'  R (k, v) (k', v');
                             k' v'. k'  it  m k' = Some v'  
                               R (k', v') (k, v)  I (insert k it) (f (k, v) σ)"
      and IF: "!!σ. I (dom m) σ  P σ"
      and II: "!!σ it.  it  dom m; it  dom m; ¬ c σ; I it σ;
                         k v k' v'. k  it  m k = Some v  k'  it  m k' = Some v'  
                                     R (k, v) (k', v')   P σ"
  shows "P (it c f σ0)"
proof (rule map_iterator_genord_rule_P [of it m R "λS σ. I (dom m - S) σ"])
  show "map_iterator_genord it m R" by fact
next
  show "I (dom m - dom m) σ0" using I0 by simp
next
  fix σ
  assume "I (dom m - {}) σ"
  with IF show "P σ" by simp
next
  fix σ it
  assume assms: "it  dom m" "it  {}" "¬ c σ" "I (dom m - it) σ"
                "k v k' v'. k  it  m k = Some v  k'  it  m k' = Some v' 
                             R (k, v) (k', v')"
  from assms have "dom m - it  dom m" by auto
  with II[of "dom m - it" σ] assms
  show "P σ" 
    apply (simp add: subset_iff dom_def)
    apply (metis option.simps(2))
  done
next
  fix k v it σ
  assume assms: "c σ" "k  it" "m k = Some v" "it  dom m" "I (dom m - it) σ"
                "k' v'. k'  it - {k}  m k' = Some v'  R (k, v) (k', v')"
                "k' v'. k'  it  m k' = Some v'  R (k', v') (k, v)"

  hence "insert k (dom m - it) = (dom m - (it - {k}))" "dom m - (dom m - it) = it" by auto
  with assms IP[of σ k "dom m - it" v]
  show "I (dom m - (it - {k})) (f (k, v) σ)" by (simp_all add: subset_iff)
qed

lemma map_iterator_rule_P:
  assumes "map_iterator it m"
      and I0: "I (dom m) σ0"
      and IP: "!!k v it σ.  c σ; k  it; m k = Some v; it  dom m; I it σ   I (it - {k}) (f (k, v) σ)"
      and IF: "!!σ. I {} σ  P σ"
      and II: "!!σ it.  it  dom m; it  {}; ¬ c σ; I it σ   P σ"
  shows "P (it c f σ0)"
using assms map_iterator_genord_rule_P[of it m "λ_ _. True" I σ0 c f P]
unfolding set_iterator_def
by simp

lemma map_iterator_rule_insert_P:
  assumes "map_iterator it m"
      and I0: "I {} σ0"
      and IP: "!!k v it σ.  c σ; k  dom m - it; m k = Some v; it  dom m; I it σ   I (insert k it) (f (k, v) σ)"
      and IF: "!!σ. I (dom m) σ  P σ"
      and II: "!!σ it.  it  dom m; it  dom m; ¬ c σ; I it σ   P σ"
  shows "P (it c f σ0)"
using assms map_iterator_genord_rule_insert_P[of it m "λ_ _. True" I σ0 c f P]
unfolding set_iterator_def
by simp

lemma map_iterator_no_cond_rule_P:
  assumes "map_iterator it m"
      and I0: "I (dom m) σ0"
      and IP: "!!k v it σ.  k  it; m k = Some v; it  dom m; I it σ   I (it - {k}) (f (k, v) σ)"
      and IF: "!!σ. I {} σ  P σ"
  shows "P (it (λ_. True) f σ0)"
using assms map_iterator_genord_rule_P[of it m "λ_ _. True" I σ0 "λ_. True" f P]
unfolding set_iterator_def
by simp

lemma map_iterator_no_cond_rule_insert_P:
  assumes "map_iterator it m"
      and I0: "I {} σ0"
      and IP: "!!k v it σ.  k  dom m - it; m k = Some v; it  dom m; I it σ   I (insert k it) (f (k, v) σ)"
      and IF: "!!σ. I (dom m) σ  P σ"
  shows "P (it (λ_. True) f σ0)"
using assms map_iterator_genord_rule_insert_P[of it m "λ_ _. True" I σ0 "λ_. True" f P]
unfolding set_iterator_def
by simp


subsection ‹Ordered Iterators›

text ‹Selecting according to a linear order is another case that is interesting. 
 Ordered iterators over maps, i.\,e.\ iterators over key-value pairs,
 use an order on the keys.›

context linorder begin
  definition "set_iterator_linord it S0 
     set_iterator_genord it S0 (≤)"
  definition "set_iterator_rev_linord it S0 
     set_iterator_genord it S0 (≥)"
  definition "set_iterator_map_linord it S0  
     set_iterator_genord it S0 (λ(k,_) (k',_). kk')"
  definition "set_iterator_map_rev_linord it S0  
     set_iterator_genord it S0 (λ(k,_) (k',_). kk')"
  abbreviation "map_iterator_linord it m  
    set_iterator_map_linord it (map_to_set m)"
  abbreviation "map_iterator_rev_linord it m  
    set_iterator_map_rev_linord it (map_to_set m)"

  lemma set_iterator_linord_rule_P:
  " set_iterator_linord it S0;
     I S0 σ0;
     !!S σ x.  c σ; x  S; I S σ; S  S0; x'. x'  S0-S  x'  x; x'. x'  S  x  x'  I (S - {x}) (f x σ);
     !!σ. I {} σ  P σ;
     !!σ S. S  S0  S  {}  (x x'. x  S; x'  S0-S  x'  x)  ¬ c σ  I S σ  P σ
     P (it c f σ0)"
  unfolding set_iterator_linord_def
  apply (rule set_iterator_genord.iteratei_rule_P [of it S0 "(≤)" I σ0 c f P])
  apply (simp_all add: Ball_def)
  apply (metis order_refl)
  done

  lemma set_iterator_linord_rule_insert_P:
  " set_iterator_linord it S0;
     I {} σ0;
     !!S σ x.  c σ; x  S0 - S; I S σ; S  S0; x'. x'  S  x'  x; x'. x'  S0 - S  x  x'   I (insert x S) (f x σ);
     !!σ. I S0 σ  P σ;
     !!σ S. S  S0  S  S0  (x x'. x  S0-S; x'  S  x'  x)  ¬ c σ  I S σ  P σ
     P (it c f σ0)"
  unfolding set_iterator_linord_def
  apply (rule set_iterator_genord.iteratei_rule_insert_P [of it S0 "(≤)" I σ0 c f P])
  apply (simp_all add: Ball_def)
  apply (metis order_refl)
  done

  lemma set_iterator_rev_linord_rule_P:
  " set_iterator_rev_linord it S0;
     I S0 σ0;
     !!S σ x.  c σ; x  S; I S σ; S  S0; x'. x'  S0-S  x  x'; x'. x'  S  x'  x  I (S - {x}) (f x σ);
     !!σ. I {} σ  P σ;
     !!σ S. S  S0  S  {}  (x x'. x  S; x'  S0-S  x  x')  ¬ c σ  I S σ  P σ
     P (it c f σ0)"
  unfolding set_iterator_rev_linord_def
  apply (rule set_iterator_genord.iteratei_rule_P [of it S0 "(≥)" I σ0 c f P])
  apply (simp_all add: Ball_def)
  apply (metis order_refl)
  done

  lemma set_iterator_rev_linord_rule_insert_P:
  " set_iterator_rev_linord it S0;
     I {} σ0;
     !!S σ x.  c σ; x  S0 - S; I S σ; S  S0; x'. x'  S  x  x'; x'. x'  S0 - S  x'  x   I (insert x S) (f x σ);
     !!σ. I S0 σ  P σ;
     !!σ S. S  S0  S  S0   (x x'. x  S0-S; x'  S  x  x')  ¬ c σ  I S σ  P σ
     P (it c f σ0)"
  unfolding set_iterator_rev_linord_def
  apply (rule set_iterator_genord.iteratei_rule_insert_P [of it S0 "(≥)" I σ0 c f P])
  apply (simp_all add: Ball_def)
  apply (metis order_refl)
  done


  lemma set_iterator_map_linord_rule_P:
  " set_iterator_map_linord it S0;
     I S0 σ0;
     !!S σ k v.  c σ; (k, v)  S; I S σ; S  S0; k' v'. (k', v')  S0-S  k'  k;
                  k' v'. (k', v')  S  k  k'  I (S - {(k,v)}) (f (k,v) σ);
     !!σ. I {} σ  P σ;
     !!σ S. S  S0  S  {}  (k v k' v'. (k, v)  S0-S; (k', v')  S  k  k') 
         ¬ c σ  I S σ  P σ
     P (it c f σ0)"
  unfolding set_iterator_map_linord_def
  apply (rule set_iterator_genord.iteratei_rule_P 
    [of it S0 "(λ(k,_) (k',_). k  k')" I σ0 c f P])
  apply simp_all
  apply (auto simp add: Ball_def)
  apply (metis order_refl)
  apply metis
  done

  lemma set_iterator_map_linord_rule_insert_P:
  " set_iterator_map_linord it S0;
     I {} σ0;
     !!S σ k v.  c σ; (k, v)  S0 - S; I S σ; S  S0; k' v'. (k', v')  S  k'  k;
                  k' v'. (k',v')  S0 - S  k  k'   I (insert (k,v) S) (f (k,v) σ);
     !!σ. I S0 σ  P σ;
     !!σ S. S  S0  S  S0  (k v k' v'. (k, v)  S; (k', v')  S0-S  k  k') 
            ¬ c σ  I S σ  P σ
     P (it c f σ0)"
  unfolding set_iterator_map_linord_def
  apply (rule set_iterator_genord.iteratei_rule_insert_P 
    [of it S0 "(λ(k,_) (k',_). k  k')" I σ0 c f P])
  apply simp_all
  apply (auto simp add: Ball_def)
  apply (metis order_refl)
  apply metis
  done

  lemma set_iterator_map_rev_linord_rule_P:
  " set_iterator_map_rev_linord it S0;
     I S0 σ0;
     !!S σ k v.  c σ; (k, v)  S; I S σ; S  S0; k' v'. (k', v')  S0-S  k  k';
                  k' v'. (k', v')  S  k'  k  I (S - {(k,v)}) (f (k,v) σ);
     !!σ. I {} σ  P σ;
     !!σ S. S  S0  S  {}  (k v k' v'. (k, v)  S0-S; (k', v')  S  k'  k)  
            ¬ c σ  I S σ  P σ
     P (it c f σ0)"
  unfolding set_iterator_map_rev_linord_def
  apply (rule set_iterator_genord.iteratei_rule_P 
    [of it S0 "(λ(k,_) (k',_). k  k')" I σ0 c f P])
  apply simp_all
  apply (auto simp add: Ball_def)
  apply (metis order_refl)
  apply metis
  done

  lemma set_iterator_map_rev_linord_rule_insert_P:
  " set_iterator_map_rev_linord it S0;
     I {} σ0;
     !!S σ k v.  c σ; (k, v)  S0 - S; I S σ; S  S0; k' v'. (k', v')  S  k  k';
                 k' v'. (k',v')  S0 - S  k'  k   I (insert (k,v) S) (f (k,v) σ);
     !!σ. I S0 σ  P σ;
     !!σ S. S  S0  S  S0  (k v k' v'. (k, v)  S; (k', v')  S0-S  k'  k)  
            ¬ c σ  I S σ  P σ
     P (it c f σ0)"
  unfolding set_iterator_map_rev_linord_def
  apply (rule set_iterator_genord.iteratei_rule_insert_P 
    [of it S0 "(λ(k,_) (k',_). k  k')" I σ0 c f P])
  apply simp_all
  apply (auto simp add: Ball_def)
  apply (metis order_refl)
  apply metis
  done


  lemma map_iterator_linord_rule_P:
    assumes "map_iterator_linord it m"
        and I0: "I (dom m) σ0"
        and IP: "!!k v it σ.  c σ; k  it; m k = Some v; it  dom m; I it σ;
                 k'. k'  it  k  k'; 
                 k'. k'  (dom m)-it  k'  k  I (it - {k}) (f (k, v) σ)"
        and IF: "!!σ. I {} σ  P σ"
        and II: "!!σ it.  it  dom m; it  {}; ¬ c σ; I it σ;
                  k k'. k  (dom m)-it; k'  it  k  k'  P σ"
    shows "P (it c f σ0)"
  using assms
  unfolding set_iterator_map_linord_def
  by (rule map_iterator_genord_rule_P) auto

  lemma map_iterator_linord_rule_insert_P:
    assumes "map_iterator_linord it m"
        and I0: "I {} σ0"
        and IP: "!!k v it σ.  c σ; k  dom m - it; m k = Some v; it  dom m; I it σ;
                 k'. k'  (dom m - it)  k  k'; 
                 k'. k'  it  k'  k   I (insert k it) (f (k, v) σ)"
        and IF: "!!σ. I (dom m) σ  P σ"
        and II: "!!σ it.  it  dom m; it  dom m; ¬ c σ; I it σ;
                  k k'. k  it; k'  (dom m)-it  k  k'  P σ"
    shows "P (it c f σ0)"
  using assms
  unfolding set_iterator_map_linord_def
  by (rule map_iterator_genord_rule_insert_P) auto

  lemma map_iterator_rev_linord_rule_P:
    assumes "map_iterator_rev_linord it m"
        and I0: "I (dom m) σ0"
        and IP: "!!k v it σ.  c σ; k  it; m k = Some v; it  dom m; I it σ;
                 k'. k'  it  k'  k; 
                 k'. k'  (dom m)-it  k  k'  I (it - {k}) (f (k, v) σ)"
        and IF: "!!σ. I {} σ  P σ"
        and II: "!!σ it.  it  dom m; it  {}; ¬ c σ; I it σ;
                  k k'. k  (dom m)-it; k'  it  k'  k  P σ"
    shows "P (it c f σ0)"
  using assms
  unfolding set_iterator_map_rev_linord_def
  by (rule map_iterator_genord_rule_P) auto

  lemma map_iterator_rev_linord_rule_insert_P:
    assumes "map_iterator_rev_linord it m"
        and I0: "I {} σ0"
        and IP: "!!k v it σ.  c σ; k  dom m - it; m k = Some v; it  dom m; I it σ;
                 k'. k'  (dom m - it)  k'  k; 
                 k'. k'  it  k  k'  I (insert k it) (f (k, v) σ)"
        and IF: "!!σ. I (dom m) σ  P σ"
        and II: "!!σ it.  it  dom m; it  dom m; ¬ c σ; I it σ;
                  k k'. k  it; k'  (dom m)-it  k'  k  P σ"
    shows "P (it c f σ0)"
  using assms
  unfolding set_iterator_map_rev_linord_def
  by (rule map_iterator_genord_rule_insert_P) auto
end

subsection ‹Conversions to foldli›

lemma set_iterator_genord_foldli_conv :
  "set_iterator_genord iti S R 
   (l0. distinct l0  S = set l0  sorted_wrt R l0  iti = foldli l0)"
unfolding set_iterator_genord_def by simp

lemma set_iterator_genord_I [intro] :
  "distinct l0; S = set l0; sorted_wrt R l0; iti = foldli l0 
   set_iterator_genord iti S R" unfolding set_iterator_genord_foldli_conv
   by blast

lemma set_iterator_foldli_conv :
  "set_iterator iti S 
   (l0. distinct l0  S = set l0  iti = foldli l0)"
unfolding set_iterator_def set_iterator_genord_def by simp

lemma set_iterator_I [intro] :
  "distinct l0; S = set l0; iti = foldli l0 
   set_iterator iti S" 
   unfolding set_iterator_foldli_conv
   by blast

context linorder begin
  lemma set_iterator_linord_foldli_conv :
    "set_iterator_linord iti S 
     (l0. distinct l0  S = set l0  sorted l0  iti = foldli l0)"
  unfolding set_iterator_linord_def set_iterator_genord_def by (simp add: sorted_sorted_wrt)

  lemma set_iterator_linord_I [intro] :
    "distinct l0; S = set l0; sorted l0; iti = foldli l0 
     set_iterator_linord iti S" 
     unfolding set_iterator_linord_foldli_conv
     by blast

  lemma set_iterator_rev_linord_foldli_conv :
    "set_iterator_rev_linord iti S 
     (l0. distinct l0  S = set l0  sorted (rev l0)  iti = foldli l0)"
  unfolding set_iterator_rev_linord_def set_iterator_genord_def by simp

  lemma set_iterator_rev_linord_I [intro] :
    "distinct l0; S = set l0; sorted (rev l0); iti = foldli l0 
     set_iterator_rev_linord iti S" 
     unfolding set_iterator_rev_linord_foldli_conv
     by blast
end


lemma map_iterator_genord_foldli_conv :
  "map_iterator_genord iti m R 
   ((l0::('k × 'v) list). distinct (map fst l0)  m = map_of l0  sorted_wrt R l0  iti = foldli l0)"
proof -
  { fix l0 :: "('k × 'v) list"
    assume dist: "distinct l0"
    have "(map_to_set m = set l0) 
          (distinct (map fst l0) 
           m = map_of l0)"
    proof (cases "distinct (map fst l0)")
      case True thus ?thesis by (metis map_of_map_to_set)
    next
      case False note not_dist_fst = this

      with dist have "~(inj_on fst (set l0))" by (simp add: distinct_map)
      hence "set l0  map_to_set m"
        by (rule_tac notI) (simp add: map_to_set_def inj_on_def)
      with not_dist_fst show ?thesis by simp
    qed
  } 
  thus ?thesis
    unfolding set_iterator_genord_def distinct_map
    by metis
qed

lemma map_iterator_genord_I [intro] :
  "distinct (map fst l0); m = map_of l0; sorted_wrt R l0; iti = foldli l0 
   map_iterator_genord iti m R" 
   unfolding map_iterator_genord_foldli_conv
   by blast

lemma map_iterator_foldli_conv :
  "map_iterator iti m 
   (l0. distinct (map fst l0)  m = map_of l0  iti = foldli l0)"
unfolding set_iterator_def map_iterator_genord_foldli_conv 
by simp

lemma map_iterator_I [intro] :
  "distinct (map fst l0); m = map_of l0; iti = foldli l0 
   map_iterator iti m" 
   unfolding map_iterator_foldli_conv
   by blast

context linorder begin

  lemma sorted_wrt_keys_map_fst:
    "sorted_wrt (λ(k,_) (k',_). R k k') l = sorted_wrt R (map fst l)"
    by (induct l) auto

  lemma map_iterator_linord_foldli_conv :
    "map_iterator_linord iti m 
     (l0. distinct (map fst l0)  m = map_of l0  sorted (map fst l0)  iti = foldli l0)"
  unfolding set_iterator_map_linord_def map_iterator_genord_foldli_conv
  by (simp add: sorted_wrt_keys_map_fst sorted_sorted_wrt)

  lemma map_iterator_linord_I [intro] :
    "distinct (map fst l0); m = map_of l0; sorted (map fst l0); iti = foldli l0 
     map_iterator_linord iti m" 
     unfolding map_iterator_linord_foldli_conv
     by blast

  lemma map_iterator_rev_linord_foldli_conv :
    "map_iterator_rev_linord iti m 
     (l0. distinct (map fst l0)  m = map_of l0  sorted (rev (map fst l0))  iti = foldli l0)"
  unfolding set_iterator_map_rev_linord_def map_iterator_genord_foldli_conv 
  by (simp add: sorted_wrt_keys_map_fst)

  lemma map_iterator_rev_linord_I [intro] :
    "distinct (map fst l0); m = map_of l0; sorted (rev (map fst l0)); iti = foldli l0 
     map_iterator_rev_linord iti m" 
     unfolding map_iterator_rev_linord_foldli_conv
     by blast

end

end

Theory SetIteratorOperations

(*  Title:       Operations on Iterators over Finite Sets
    Author:      Thomas Tuerk <tuerk@in.tum.de>
    Maintainer:  Thomas Tuerk <tuerk@in.tum.de>
*)
section ‹Operations on Set Iterators›
theory SetIteratorOperations
imports Main SetIterator
begin

text‹Many operations on sets can be lifted to iterators over sets. This theory tries to introduce
the most useful such operations.›

subsection ‹Empty set›

text ‹Iterators over empty sets and singleton sets are very easy to define.›
definition set_iterator_emp :: "('a,) set_iterator" where
  "set_iterator_emp c f σ0 = σ0"

lemma set_iterator_emp_foldli_conv :
  "set_iterator_emp = foldli []"
by (simp add: fun_eq_iff set_iterator_emp_def)

lemma set_iterator_genord_emp_correct :
  "set_iterator_genord set_iterator_emp {} R"
apply (rule set_iterator_genord.intro)
apply (rule exI[where x="[]"])
apply (simp add: set_iterator_emp_foldli_conv)
done

lemma set_iterator_emp_correct :
  "set_iterator set_iterator_emp {}"
using set_iterator_intro [OF set_iterator_genord_emp_correct] .

lemma (in linorder) set_iterator_linord_emp_correct :
  "set_iterator_linord set_iterator_emp {}"
unfolding set_iterator_linord_def
by (fact set_iterator_genord_emp_correct) 

lemma (in linorder) set_iterator_rev_linord_emp_correct :
  "set_iterator_rev_linord set_iterator_emp {}"
unfolding set_iterator_rev_linord_def
by (fact set_iterator_genord_emp_correct) 

lemma (in linorder) map_iterator_linord_emp_correct :
  "map_iterator_linord set_iterator_emp Map.empty"
  "set_iterator_map_linord set_iterator_emp {}"
unfolding set_iterator_map_linord_def
by (simp_all add: set_iterator_genord_emp_correct map_to_set_def) 

lemma (in linorder) map_iterator_rev_linord_emp_correct :
  "map_iterator_rev_linord set_iterator_emp Map.empty"
  "set_iterator_map_rev_linord set_iterator_emp {}"
unfolding set_iterator_map_rev_linord_def
by (simp_all add: set_iterator_genord_emp_correct map_to_set_def) 


subsection‹Singleton Sets›

definition set_iterator_sng :: "'a  ('a,) set_iterator" where
  "set_iterator_sng x c f σ0 = (if c σ0 then f x σ0 else σ0)"

lemma set_iterator_sng_foldli_conv :
  "set_iterator_sng x = foldli [x]"
by (simp add: fun_eq_iff set_iterator_sng_def)

lemma set_iterator_genord_sng_correct :
  "set_iterator_genord (set_iterator_sng (x::'a)) {x} R"
apply (rule set_iterator_genord.intro)
apply (rule exI[where x="[x]"])
apply (simp add: set_iterator_sng_foldli_conv)
done

lemma set_iterator_sng_correct :
  "set_iterator (set_iterator_sng x) {x}"
unfolding set_iterator_def
by (rule set_iterator_genord_sng_correct)

lemma (in linorder) set_iterator_linord_sng_correct :
  "set_iterator_linord (set_iterator_sng x) {x}"
unfolding set_iterator_linord_def
by (simp add: set_iterator_genord_sng_correct) 

lemma (in linorder) set_iterator_rev_linord_sng_correct :
  "set_iterator_rev_linord (set_iterator_sng x) {x}"
unfolding set_iterator_rev_linord_def
by (simp add: set_iterator_genord_sng_correct) 

lemma (in linorder) map_iterator_linord_sng_correct :
  "map_iterator_linord (set_iterator_sng (k,v)) (Map.empty (k  v))"
unfolding set_iterator_map_linord_def
by (simp add: set_iterator_genord_sng_correct) 

lemma (in linorder) map_iterator_rev_linord_sng_correct :
  "map_iterator_rev_linord (set_iterator_sng (k,v)) (Map.empty (k  v))"
unfolding set_iterator_map_rev_linord_def
by (simp add: set_iterator_genord_sng_correct) 


subsection ‹Union›

text ‹Iterators over disjoint sets can be combined by first iterating over one and then the
other set. The result is an iterator over the union of the original sets.›

definition set_iterator_union ::
    "('a,) set_iterator  ('a, ) set_iterator  ('a,) set_iterator" where
  "set_iterator_union it_a it_b  λc f σ0. (it_b c f (it_a c f σ0))"

lemma set_iterator_union_foldli_conv :
  "set_iterator_union (foldli as) (foldli bs) = foldli (as @ bs)"
by (simp add: fun_eq_iff set_iterator_union_def foldli_append)

lemma set_iterator_genord_union_correct :
  fixes it_a :: "('a,) set_iterator"
  fixes it_b :: "('a,) set_iterator"
  fixes R S_a S_b
  assumes it_a: "set_iterator_genord it_a S_a R"
  assumes it_b: "set_iterator_genord it_b S_b R"
  assumes dist_Sab: "S_a  S_b = {}"
  assumes R_OK: "a b. a  S_a; b  S_b  R a b"
  shows "set_iterator_genord (set_iterator_union it_a it_b) (S_a  S_b) R"
proof -
  from it_a obtain as where 
    dist_as: "distinct as" and S_a_eq: "S_a = set as" and 
    sorted_as: "sorted_wrt R as" and it_a_eq: "it_a = foldli as"
  unfolding set_iterator_genord_foldli_conv by blast

  from it_b obtain bs where 
    dist_bs: "distinct bs" and S_b_eq: "S_b = set bs" and 
    sorted_bs: "sorted_wrt R bs" and it_b_eq: "it_b = foldli bs"
  unfolding set_iterator_genord_foldli_conv by blast

  show ?thesis
  proof (rule set_iterator_genord_I [of "as @ bs"])
    from dist_Sab S_a_eq S_b_eq dist_as dist_bs
    show "distinct (as @ bs)" by simp
  next
    from S_a_eq S_b_eq 
    show "S_a  S_b = set (as @ bs)" by simp
  next
    from sorted_as sorted_bs R_OK S_a_eq S_b_eq
    show "sorted_wrt R (as @ bs)"
      by (simp add: sorted_wrt_append Ball_def)
  next
    show "set_iterator_union it_a it_b = (foldli (as @ bs))"
      unfolding it_a_eq it_b_eq set_iterator_union_foldli_conv by simp
  qed
qed

lemma set_iterator_union_emp [simp] :
  "set_iterator_union (set_iterator_emp) it = it"
  "set_iterator_union it (set_iterator_emp) = it"
unfolding set_iterator_emp_def set_iterator_union_def
by simp_all

lemma set_iterator_union_correct :
  assumes it_a: "set_iterator it_a S_a"
  assumes it_b: "set_iterator it_b S_b"
  assumes dist_Sab: "S_a  S_b = {}"
  shows "set_iterator (set_iterator_union it_a it_b) (S_a  S_b)"
proof -
  note res' = set_iterator_genord_union_correct [OF it_a[unfolded set_iterator_def] 
                                                    it_b[unfolded set_iterator_def] dist_Sab]
  from set_iterator_intro [OF res']
  show ?thesis by simp
qed

lemma (in linorder) set_iterator_linord_union_correct :
  assumes it_a: "set_iterator_linord it_a S_a"
  assumes it_b: "set_iterator_linord it_b S_b"
  assumes ord_Sab: "a b. a  S_a; b  S_b  a < b"
  shows "set_iterator_linord (set_iterator_union it_a it_b) (S_a  S_b)"
unfolding set_iterator_linord_def
apply (rule_tac set_iterator_genord_union_correct[
   OF it_a[unfolded set_iterator_linord_def] it_b[unfolded set_iterator_linord_def]])
apply (insert ord_Sab)
apply auto
apply (metis less_le_not_le ord_Sab)
done

lemma (in linorder) set_iterator_rev_linord_union_correct :
  assumes it_a: "set_iterator_rev_linord it_a S_a"
  assumes it_b: "set_iterator_rev_linord it_b S_b"
  assumes ord_Sab: "a b. a  S_a; b  S_b  a > b"
  shows "set_iterator_rev_linord (set_iterator_union it_a it_b) (S_a  S_b)"
unfolding set_iterator_rev_linord_def
apply (rule_tac set_iterator_genord_union_correct[
   OF it_a[unfolded set_iterator_rev_linord_def] it_b[unfolded set_iterator_rev_linord_def]])
apply (insert ord_Sab)
apply auto
apply (metis less_le_not_le ord_Sab)
done

lemma (in linorder) map_iterator_linord_union_correct :
  assumes it_a: "set_iterator_map_linord it_a S_a"
  assumes it_b: "set_iterator_map_linord it_b S_b"
  assumes ord_Sab: "kv kv'. kv  S_a; kv'  S_b  fst kv < fst kv'"
  shows "set_iterator_map_linord (set_iterator_union it_a it_b) (S_a  S_b)"
  unfolding set_iterator_map_linord_def
  apply (rule set_iterator_genord_union_correct [OF 
    it_a[unfolded set_iterator_map_linord_def] 
    it_b[unfolded set_iterator_map_linord_def]])
  apply (insert ord_Sab)
  apply auto
  apply (metis less_le_not_le)
done

lemma (in linorder) map_iterator_rev_linord_union_correct :
  assumes it_a: "set_iterator_map_rev_linord it_a S_a"
  assumes it_b: "set_iterator_map_rev_linord it_b S_b"
  assumes ord_Sab: "kv kv'. kv  S_a; kv'  S_b  fst kv > fst kv'"
  shows "set_iterator_map_rev_linord (set_iterator_union it_a it_b) (S_a  S_b)"
  unfolding set_iterator_map_rev_linord_def
  apply (rule set_iterator_genord_union_correct [OF 
    it_a[unfolded set_iterator_map_rev_linord_def] 
    it_b[unfolded set_iterator_map_rev_linord_def]])
  apply (insert ord_Sab)
  apply auto
  apply (metis less_le_not_le)
done


subsection ‹Product›

definition set_iterator_product :: 
    "('a,) set_iterator  ('a  ('b,) set_iterator)  ('a × 'b ,) set_iterator" where
  "set_iterator_product it_a it_b  λc f σ0.
    it_a c (
      λa σ. it_b a c (λb σ. f (a,b) σ) σ
    ) σ0"


lemma set_iterator_product_foldli_conv: 
  "set_iterator_product (foldli as) (λa. foldli (bs a)) =
   foldli (concat (map (λa. map (λb. (a, b)) (bs a)) as))"
apply (induct as)
  apply (simp add: set_iterator_product_def)
apply (simp add: set_iterator_product_def foldli_append foldli_map o_def fun_eq_iff)
done

lemma set_iterator_product_it_b_cong: 
assumes it_a_OK: "set_iterator it_a S_a"
    and it_b_b': "a. a  S_a  it_b a = it_b' a"
shows "set_iterator_product it_a it_b =
       set_iterator_product it_a it_b'"
proof -
  from it_a_OK obtain as where 
    dist_as: "distinct as" and S_a_eq: "S_a = set as" and 
    it_a_eq: "it_a = foldli as"
  unfolding set_iterator_foldli_conv by blast
  
  from it_b_b'[unfolded S_a_eq]
  show ?thesis unfolding it_a_eq
    by (induct as) 
       (simp_all add: set_iterator_product_def it_b_b' fun_eq_iff)
qed

definition set_iterator_product_order ::
  "('a  'a  bool)  ('a  'b  'b  bool) 
   ('a × 'b)  ('a × 'b)  bool" where
  "set_iterator_product_order R_a R_b ab ab' 
   (if (fst ab = fst ab') then R_b (fst ab) (snd ab) (snd ab') else
                               R_a (fst ab) (fst ab'))"

lemma set_iterator_genord_product_correct :
  fixes it_a :: "('a,) set_iterator"
  fixes it_b :: "'a  ('b,) set_iterator" 
  assumes it_a: "set_iterator_genord it_a S_a R_a"
  assumes it_b: "a. a  S_a  set_iterator_genord (it_b a) (S_b a) (R_b a)"
  shows "set_iterator_genord (set_iterator_product it_a it_b) (Sigma S_a S_b) 
             (set_iterator_product_order R_a R_b)"
proof -
  from it_a obtain as where 
    dist_as: "distinct as" and S_a_eq: "S_a = set as" and 
    sorted_as: "sorted_wrt R_a as" and it_a_eq: "it_a = foldli as"
  unfolding set_iterator_genord_foldli_conv by blast

  from it_b obtain bs where 
    dist_bs: "a. a  set as  distinct (bs a)" and S_b_eq: "a. a  set as   S_b a = set (bs a)" and 
    sorted_bs: "a. a  set as  sorted_wrt (R_b a) (bs a)" and 
    it_b_eq: "a. a  set as  it_b a = foldli (bs a)"
  unfolding set_iterator_genord_foldli_conv by (metis S_a_eq)

  let ?abs = "concat (map (λa. map (λb. (a, b)) (bs a)) as)"

  show ?thesis
  proof (rule set_iterator_genord_I[of ?abs])
    from set_iterator_product_it_b_cong[of it_a S_a it_b, 
       OF set_iterator_intro[OF it_a] it_b_eq] it_a_eq S_a_eq
    have "set_iterator_product it_a it_b =
          set_iterator_product (foldli as) (λa. foldli (bs a))" by simp
    thus "set_iterator_product it_a it_b = foldli ?abs"
      by (simp add: set_iterator_product_foldli_conv)
  next
    show "distinct ?abs"
    using dist_as dist_bs[unfolded S_a_eq]
    by (induct as) 
       (simp_all add: distinct_map inj_on_def dist_bs set_eq_iff image_iff)
  next
    show "Sigma S_a S_b = set ?abs" 
      unfolding S_a_eq using S_b_eq
      by (induct as) auto  
  next
    from sorted_as sorted_bs dist_as     
    show "sorted_wrt
           (set_iterator_product_order R_a R_b)
           (concat (map (λa. map (Pair a) (bs a)) as))"
    proof (induct as rule: list.induct)
      case Nil thus ?case by simp
    next
      case (Cons a as)
      from Cons(2) have R_a_as: "a'. a'  set as  R_a a a'" and
                        sorted_as: "sorted_wrt R_a as" by simp_all
      from Cons(3) have sorted_bs_a: "sorted_wrt (R_b a) (bs a)" 
                    and sorted_bs_as: "a. a  set as  sorted_wrt (R_b a) (bs a)" by simp_all
      from Cons(4) have dist_as: "distinct as" and a_nin_as: "a  set as" by simp_all
      note ind_hyp = Cons(1)[OF sorted_as sorted_bs_as dist_as]
      
      define bs_a where "bs_a = bs a"
      from sorted_bs_a
      have sorted_prod_a : "sorted_wrt (set_iterator_product_order R_a R_b) (map (Pair a) (bs a))"
        unfolding bs_a_def[symmetric]
        apply (induct bs_a rule: list.induct) 
        apply (simp_all add: set_iterator_product_order_def Ball_def image_iff)
      done

      show ?case
        apply (simp add: sorted_wrt_append ind_hyp sorted_prod_a)
        apply (simp add: set_iterator_product_order_def R_a_as a_nin_as)
      done
    qed
  qed
qed

lemma set_iterator_product_correct :
  assumes it_a: "set_iterator it_a S_a"
  assumes it_b: "a. a  S_a  set_iterator (it_b a) (S_b a)"
  shows "set_iterator (set_iterator_product it_a it_b) (Sigma S_a S_b)"
proof -
  note res' = set_iterator_genord_product_correct [OF it_a[unfolded set_iterator_def], 
     of it_b S_b "λ_ _ _. True", OF it_b[unfolded set_iterator_def]]
  note res = set_iterator_intro [OF res']
  thus ?thesis by simp
qed


subsection ‹Filter and Image›

text ‹Filtering and applying an injective function on iterators is easily defineable as well.
  In contrast to sets the function really has to be injective, because an iterator guarentees to
  visit each element only once.›

definition set_iterator_image_filter ::
    "('a  'b option)  ('a,) set_iterator  ('b,) set_iterator" where
  "set_iterator_image_filter g it  λc f σ0. (it c
     (λx σ. (case (g x) of Some x'  f x' σ | None  σ)) σ0)"

lemma set_iterator_image_filter_foldli_conv :
  "set_iterator_image_filter g (foldli xs) =
   foldli (List.map_filter g xs)"
by (induct xs) (auto simp add: List.map_filter_def set_iterator_image_filter_def fun_eq_iff)  

lemma set_iterator_genord_image_filter_correct :
  fixes it :: "('a,) set_iterator"
  fixes g :: "'a  'b option"
  assumes it_OK: "set_iterator_genord it S R"
  assumes g_inj_on: "inj_on g (S  dom g)"
  assumes R'_prop: "x y x' y'. x  S; g x = Some x'; y  S; g y = Some y'; R x y  R' x' y'"
  shows "set_iterator_genord (set_iterator_image_filter g it) {y. x. x  S  g x = Some y} R'"
proof -
  from it_OK obtain xs where 
    dist_xs: "distinct xs" and S_eq: "S = set xs" and 
    sorted_xs: "sorted_wrt R xs" and it_eq: "it = foldli xs"
  unfolding set_iterator_genord_foldli_conv by blast

  show ?thesis
  proof (rule set_iterator_genord_I [of "List.map_filter g xs"])
    show "set_iterator_image_filter g it =
          foldli (List.map_filter g xs)"
      unfolding it_eq  set_iterator_image_filter_foldli_conv by simp
  next
    from dist_xs g_inj_on[unfolded S_eq]
    show "distinct (List.map_filter g xs)"
      apply (induct xs)
      apply (simp add: List.map_filter_simps) 
      apply (simp add: List.map_filter_def image_iff inj_on_def Ball_def dom_def)
      apply (metis not_Some_eq option.sel)
    done
  next
    show "{y. x. x  S  g x = Some y} =
          set (List.map_filter g xs)"
      unfolding S_eq set_map_filter by simp
  next
    from sorted_xs R'_prop[unfolded S_eq]
    show "sorted_wrt R' (List.map_filter g xs)"
    proof (induct xs rule: list.induct)
      case Nil thus ?case by (simp add: List.map_filter_simps) 
    next
      case (Cons x xs)
      note sort_x_xs = Cons(2)
      note R'_x_xs = Cons(3)

      from Cons have ind_hyp: "sorted_wrt R' (List.map_filter g xs)" by auto

      show ?case
        apply (cases "g x")  
        apply (simp add: List.map_filter_simps ind_hyp)
        apply (simp add: List.map_filter_simps set_map_filter Ball_def ind_hyp)
        apply (insert R'_x_xs[of x] sort_x_xs)
        apply (simp add: Ball_def)
        apply metis
      done
    qed
  qed
qed


lemma set_iterator_image_filter_correct :
  fixes it :: "('a,) set_iterator"
  fixes g :: "'a  'b option"
  assumes it_OK: "set_iterator it S"
  assumes g_inj_on: "inj_on g (S  dom g)"
  shows "set_iterator (set_iterator_image_filter g it) {y. x. x  S  g x = Some y}"
proof -
  note res' = set_iterator_genord_image_filter_correct [OF it_OK[unfolded set_iterator_def], 
     of g "λ_ _. True"]
  note res = set_iterator_intro [OF res']
  with g_inj_on show ?thesis by simp 
qed


text ‹Special definitions for only filtering or only appling a function are handy.›
definition set_iterator_filter ::
    "('a  bool)  ('a,) set_iterator  ('a,) set_iterator" where
  "set_iterator_filter P  set_iterator_image_filter (λx. if P x then Some x else None)"

lemma set_iterator_filter_foldli_conv :
  "set_iterator_filter P (foldli xs) = foldli (filter P xs)"
  apply (simp add: set_iterator_filter_def set_iterator_image_filter_foldli_conv)
  apply (rule cong) apply simp
  apply (induct xs)
  apply (simp_all add: List.map_filter_def)
done

lemma set_iterator_filter_alt_def [code] : 
  "set_iterator_filter P it = (λc f. it c (λ(x::'a) (σ::'b). if P x then f x σ else σ))"
proof -
  have "f. (λ(x::'a) (σ::'b).
             case if P x then Some x else None of None  σ
             | Some x'  f x' σ) =
            (λx σ. if P x then f x σ else σ)"
     by auto
  thus ?thesis 
    unfolding set_iterator_filter_def
              set_iterator_image_filter_def[abs_def]
    by simp
qed

lemma set_iterator_genord_filter_correct :
  fixes it :: "('a,) set_iterator"
  assumes it_OK: "set_iterator_genord it S R"
  shows "set_iterator_genord (set_iterator_filter P it) {x. x  S  P x} R"
proof -
  let ?g = "λx. if P x then Some x else None"
  have in_dom_g: "x. x  dom ?g  P x" unfolding dom_def by auto

  from set_iterator_genord_image_filter_correct [OF it_OK, of ?g R, folded set_iterator_filter_def]
  show ?thesis
    by (simp add: if_split_eq1 inj_on_def Ball_def in_dom_g)
qed

lemma set_iterator_filter_correct :
  assumes it_OK: "set_iterator it S"
  shows "set_iterator (set_iterator_filter P it) {x. x  S  P x}"
proof -
  note res' = set_iterator_genord_filter_correct [OF it_OK[unfolded set_iterator_def], 
    of P]
  note res = set_iterator_intro [OF res']
  thus ?thesis by simp
qed

lemma (in linorder) set_iterator_linord_filter_correct :
  assumes it_OK: "set_iterator_linord it S"
  shows "set_iterator_linord (set_iterator_filter P it) {x. x  S  P x}"
using assms
unfolding set_iterator_linord_def
by (rule set_iterator_genord_filter_correct)

lemma (in linorder) set_iterator_rev_linord_filter_correct :
  assumes it_OK: "set_iterator_rev_linord it S"
  shows "set_iterator_rev_linord (set_iterator_filter P it) {x. x  S  P x}"
using assms
unfolding set_iterator_rev_linord_def
by (rule set_iterator_genord_filter_correct)

definition set_iterator_image ::
    "('a  'b)  ('a,) set_iterator  ('b,) set_iterator" where
  "set_iterator_image g  set_iterator_image_filter (λx. Some (g x))"

lemma set_iterator_image_foldli_conv :
  "set_iterator_image g (foldli xs) = foldli (map g xs)"
  apply (simp add: set_iterator_image_def set_iterator_image_filter_foldli_conv)
  apply (rule cong) apply simp
  apply (induct xs)
  apply (simp_all add: List.map_filter_def)
done

lemma set_iterator_image_alt_def [code] : 
  "set_iterator_image g it = (λc f. it c (λx. f (g x)))"
unfolding set_iterator_image_def
          set_iterator_image_filter_def[abs_def]
by simp

lemma set_iterator_genord_image_correct :
  fixes it :: "('a,) set_iterator"
  assumes it_OK: "set_iterator_genord it S R"
  assumes g_inj: "inj_on g S"
  assumes R'_prop: "x y. x  S; y  S; R x y  R' (g x) (g y)"
  shows "set_iterator_genord (set_iterator_image g it) (g ` S) R'"
proof -
  let ?g = "λx. Some (g x)"
  have set_eq: "S. {y . x. x  S  ?g x = Some y} = g ` S" by auto

  show ?thesis
    apply (rule set_iterator_genord_image_filter_correct [OF it_OK, of ?g R', 
     folded set_iterator_image_def set_eq[symmetric]])
    apply (insert g_inj, simp add: inj_on_def) []
    apply (insert R'_prop, auto)
  done
qed

lemma set_iterator_image_correct :
  assumes it_OK: "set_iterator it S"
  assumes g_inj: "inj_on g S"
  assumes S'_OK: "S' = g ` S"
  shows "set_iterator (set_iterator_image g it) S'"
proof -
  note res' = set_iterator_genord_image_correct [OF it_OK[unfolded set_iterator_def] g_inj, 
    of "λ_ _. True"]
  note res = set_iterator_intro [OF res', folded S'_OK]
  thus ?thesis by simp
qed



subsection ‹Construction from list (foldli)›

text ‹Iterators correspond by definition to iteration over distinct lists. They fix an order 
 in which the elements are visited. Therefore, it is trivial to construct an iterator from a 
 distinct list.›

lemma set_iterator_genord_foldli_correct :
"distinct xs  sorted_wrt R xs  set_iterator_genord (foldli xs) (set xs) R"
by (rule set_iterator_genord_I[of xs]) (simp_all)

lemma set_iterator_foldli_correct :
"distinct xs  set_iterator (foldli xs) (set xs)"
by (rule set_iterator_I[of xs]) (simp_all)

lemma (in linorder) set_iterator_linord_foldli_correct :
assumes dist_xs: "distinct xs"
assumes sorted_xs: "sorted xs"
shows "set_iterator_linord (foldli xs) (set xs)"
using assms
by (rule_tac set_iterator_linord_I[of xs]) (simp_all)


lemma (in linorder) set_iterator_rev_linord_foldli_correct :
assumes dist_xs: "distinct xs"
assumes sorted_xs: "sorted (rev xs)"
shows "set_iterator_rev_linord (foldli xs) (set xs)"
using assms
by (rule_tac set_iterator_rev_linord_I[of xs]) (simp_all)


lemma map_iterator_genord_foldli_correct :
"distinct (map fst xs)  sorted_wrt R xs  map_iterator_genord (foldli xs) (map_of xs) R"
by (rule map_iterator_genord_I[of xs]) simp_all

lemma map_iterator_foldli_correct :
"distinct (map fst xs)  map_iterator (foldli xs) (map_of xs)"
by (rule map_iterator_I[of xs]) (simp_all)

lemma (in linorder) map_iterator_linord_foldli_correct :
assumes dist_xs: "distinct (map fst xs)"
assumes sorted_xs: "sorted (map fst xs)"
shows "map_iterator_linord (foldli xs) (map_of xs)"
using assms
by (rule_tac map_iterator_linord_I[of xs]) (simp_all)


lemma (in linorder) map_iterator_rev_linord_foldli_correct :
assumes dist_xs: "distinct (map fst xs)"
assumes sorted_xs: "sorted (rev (map fst xs))"
shows "map_iterator_rev_linord (foldli xs) (map_of xs)"
using assms
by (rule_tac map_iterator_rev_linord_I[of xs]) (simp_all)


subsection ‹Construction from list (foldri)›

lemma set_iterator_genord_foldri_correct :
"distinct xs  sorted_wrt R (rev xs)  set_iterator_genord (foldri xs) (set xs) R"
by (rule set_iterator_genord_I[of "rev xs"]) (simp_all add: foldri_def)

lemma set_iterator_foldri_correct :
"distinct xs  set_iterator (foldri xs) (set xs)"
by (rule set_iterator_I[of "rev xs"]) (simp_all add: foldri_def)

lemma (in linorder) set_iterator_linord_foldri_correct :
assumes dist_xs: "distinct xs"
assumes sorted_xs: "sorted (rev xs)"
shows "set_iterator_linord (foldri xs) (set xs)"
using assms
by (rule_tac set_iterator_linord_I[of "rev xs"]) (simp_all add: foldri_def)

lemma (in linorder) set_iterator_rev_linord_foldri_correct :
assumes dist_xs: "distinct xs"
assumes sorted_xs: "sorted xs"
shows "set_iterator_rev_linord (foldri xs) (set xs)"
using assms
by (rule_tac set_iterator_rev_linord_I[of "rev xs"]) (simp_all add: foldri_def)

lemma map_iterator_genord_foldri_correct :
"distinct (map fst xs)  sorted_wrt R (rev xs)  map_iterator_genord (foldri xs) (map_of xs) R"
by (rule map_iterator_genord_I[of "rev xs"]) 
   (simp_all add: rev_map[symmetric] foldri_def)

lemma map_iterator_foldri_correct :
"distinct (map fst xs)  map_iterator (foldri xs) (map_of xs)"
by (rule map_iterator_I[of "rev xs"]) 
   (simp_all add: rev_map[symmetric] foldri_def)

lemma (in linorder) map_iterator_linord_foldri_correct :
assumes dist_xs: "distinct (map fst xs)"
assumes sorted_xs: "sorted (rev (map fst xs))"
shows "map_iterator_linord (foldri xs) (map_of xs)"
using assms
by (rule_tac map_iterator_linord_I[of "rev xs"]) 
   (simp_all add: rev_map[symmetric] foldri_def)

lemma (in linorder) map_iterator_rev_linord_foldri_correct :
assumes dist_xs: "distinct (map fst xs)"
assumes sorted_xs: "sorted (map fst xs)"
shows "map_iterator_rev_linord (foldri xs) (map_of xs)"
using assms
by (rule_tac map_iterator_rev_linord_I[of "rev xs"]) 
   (simp_all add: rev_map[symmetric] foldri_def)


subsection ‹Iterators over Maps›

text ‹In the following iterator over the key-value pairs of a finite map are called
 iterators over maps. Operations for such iterators are presented.›

subsubsection‹Domain Iterator›

text ‹One very simple such operation is iterating over only the keys of the map.›

definition map_iterator_dom where
  "map_iterator_dom it = set_iterator_image fst it"

lemma map_iterator_dom_foldli_conv :
  "map_iterator_dom (foldli kvs) = foldli (map fst kvs)"
unfolding map_iterator_dom_def set_iterator_image_foldli_conv by simp

lemma map_iterator_genord_dom_correct :
  assumes it_OK: "map_iterator_genord it m R"
  assumes R'_prop: "k v k' v'. m k = Some v; m k' = Some v'; R (k, v) (k', v')  R' k k'"
  shows "set_iterator_genord (map_iterator_dom it) (dom m) R'"
proof -
  have pre1: "inj_on fst (map_to_set m)" 
     unfolding inj_on_def map_to_set_def by simp

  from set_iterator_genord_image_correct[OF it_OK pre1, of R'] R'_prop
  show ?thesis
    unfolding map_iterator_dom_def map_to_set_dom[symmetric]
    by (auto simp add: map_to_set_def)
qed

lemma map_iterator_dom_correct :
  assumes it_OK: "map_iterator it m"
  shows "set_iterator (map_iterator_dom it) (dom m)"
using assms
unfolding set_iterator_def 
apply (rule_tac map_iterator_genord_dom_correct)
apply simp_all
done

lemma (in linorder) map_iterator_linord_dom_correct :
  assumes it_OK: "map_iterator_linord it m"
  shows "set_iterator_linord (map_iterator_dom it) (dom m)"
using assms
unfolding set_iterator_linord_def set_iterator_map_linord_def  
apply (rule_tac map_iterator_genord_dom_correct)
apply assumption
apply auto
done

lemma (in linorder) map_iterator_rev_linord_dom_correct :
  assumes it_OK: "map_iterator_rev_linord it m"
  shows "set_iterator_rev_linord (map_iterator_dom it) (dom m)"
using assms
unfolding set_iterator_rev_linord_def set_iterator_map_rev_linord_def
apply (rule_tac map_iterator_genord_dom_correct)
apply assumption
apply auto
done


subsubsection‹Domain Iterator with Filter›

text ‹More complex is iterating over only the keys such that the key-value pairs satisfy some
        property.›

definition map_iterator_dom_filter ::
    "('a × 'b  bool)  ('a × 'b,) set_iterator  ('a,) set_iterator" where
  "map_iterator_dom_filter P it  set_iterator_image_filter 
     (λxy. if P xy then Some (fst xy) else None) it"

lemma map_iterator_dom_filter_alt_def [code] :
  "map_iterator_dom_filter P it = 
   (λc f. it c (λkv σ. if P kv then f (fst kv) σ else σ))"
unfolding map_iterator_dom_filter_def set_iterator_image_filter_def
apply (rule ext)
apply (rule ext)
apply (rule arg_cong2[where f="it"])
apply (simp)
apply (simp add: fun_eq_iff split: option.splits)
done

lemma map_iterator_genord_dom_filter_correct :
  fixes it :: "('a × 'b, ) set_iterator"
  assumes it_OK: "set_iterator_genord it (map_to_set m) R"
  assumes R'_prop: "k1 v1 k2 v2.
      m k1 = Some v1; P (k1, v1);
       m k2 = Some v2; P (k2, v2); R (k1, v1) (k2, v2)  R' k1 k2"
  shows "set_iterator_genord (map_iterator_dom_filter P it) {k . v. m k = Some v  P (k, v)} R'"
proof - 
  define g where "g xy = (if P xy then Some (fst xy) else None)" for xy :: "'a × 'b"

  note set_iterator_genord_image_filter_correct [OF it_OK, of g R']

  have g_eq_Some: "kv k. g kv = Some k  ((k = fst kv)  P kv)"
    unfolding g_def by (auto split: prod.splits option.splits)

  have "x1 x2 y. x1  map_to_set m  x2  map_to_set m 
                  g x1 = Some y  g x2 = Some y  x1 = x2"
  proof -
    fix x1 x2 y
    assume x1_in: "x1  map_to_set m"
       and x2_in: "x2  map_to_set m"
       and g1_eq: "g x1 = Some y" 
       and g2_eq: "g x2 = Some y"

    obtain k1 v1 where x1_eq[simp] : "x1 = (k1, v1)" by (rule prod.exhaust)
    obtain k2 v2 where x2_eq[simp] : "x2 = (k2, v2)" by (rule prod.exhaust)

    from g1_eq g2_eq g_eq_Some have k1_eq: "k1 = k2" by simp 
    with x1_in x2_in have v1_eq: "v1 = v2"
      unfolding map_to_set_def by simp
    from k1_eq v1_eq show "x1 = x2" by simp
  qed
  hence g_inj_on: "inj_on g (map_to_set m  dom g)"
    unfolding inj_on_def dom_def by auto

  have g_eq_Some: "x y. (g x = Some y)  (P x  y = (fst x))"
    unfolding g_def by auto

  have "set_iterator_genord (set_iterator_image_filter g it)
            {y. x. x  map_to_set m  g x = Some y} R'" 
    apply (rule set_iterator_genord_image_filter_correct [OF it_OK, of g R', OF g_inj_on])
    apply (insert R'_prop) 
    apply (auto simp add: g_eq_Some map_to_set_def)
  done
  thus ?thesis
    unfolding map_iterator_dom_filter_def g_def[symmetric]
    by (simp add: g_eq_Some map_to_set_def)
qed

lemma map_iterator_dom_filter_correct :
  assumes it_OK: "map_iterator it m"
  shows "set_iterator (map_iterator_dom_filter P it) {k. v. m k = Some v  P (k, v)}"
using assms
unfolding set_iterator_def
apply (rule_tac map_iterator_genord_dom_filter_correct)
apply simp_all
done

lemma (in linorder) map_iterator_linord_dom_filter_correct :
  assumes it_OK: "map_iterator_linord it m"
  shows "set_iterator_linord (map_iterator_dom_filter P it) {k. v. m k = Some v  P (k, v)}"
using assms
unfolding set_iterator_map_linord_def set_iterator_linord_def 
apply (rule_tac map_iterator_genord_dom_filter_correct 
  [where R = "λ(k,_) (k',_). kk'"])
apply (simp_all add: set_iterator_def)
done

lemma (in linorder) set_iterator_rev_linord_map_filter_correct :
  assumes it_OK: "map_iterator_rev_linord it m"
  shows "set_iterator_rev_linord (map_iterator_dom_filter P it) 
  {k. v. m k = Some v  P (k, v)}"
using assms
unfolding set_iterator_map_rev_linord_def set_iterator_rev_linord_def 
apply (rule_tac map_iterator_genord_dom_filter_correct 
  [where R = "λ(k,_) (k',_). kk'"])
apply (simp_all add: set_iterator_def)
done


subsubsection‹Product for Maps›

definition map_iterator_product where
  "map_iterator_product it_a it_b =
   set_iterator_image (λkvv'. (fst (fst kvv'), snd kvv')) 
    (set_iterator_product it_a (λkv. it_b (snd kv)))"

lemma map_iterator_product_foldli_conv :
"map_iterator_product (foldli as) (λa. foldli (bs a)) = 
 foldli (concat (map (λ(k, v). map (Pair k) (bs v)) as))"
unfolding map_iterator_product_def set_iterator_product_foldli_conv set_iterator_image_foldli_conv
by (simp add: map_concat o_def split_def) 

lemma map_iterator_product_alt_def [code] :
  "map_iterator_product it_a it_b = 
   (λc f. it_a c (λa. it_b (snd a) c (λb. f (fst a, b))))"
unfolding map_iterator_product_def set_iterator_product_def set_iterator_image_alt_def
by simp

lemma map_iterator_genord_product_correct :
  fixes it_a :: "(('k × 'v),) set_iterator"
  fixes it_b :: "'v  ('e,) set_iterator" 
  fixes S_a S_b R_a R_b m
  assumes it_a: "map_iterator_genord it_a m R_a"
  assumes it_b: "k v. m k = Some v  set_iterator_genord (it_b v) (S_b v) (R_b v)"
  assumes R'_prop: "k v u k' v' u'.
       m k = Some v 
       u  S_b v 
       m k' = Some v' 
       u'  S_b v' 
       if k = k' then R_b v u u'
       else R_a (k, v) (k', v') 
       R_ab (k, u) (k', u')"
  shows "set_iterator_genord (map_iterator_product it_a it_b) 
     {(k, e) . (v. m k = Some v  e  S_b v)} R_ab"
proof -
  from it_b have it_b': "kv. kv  map_to_set m 
       set_iterator_genord (it_b (snd kv)) (S_b (snd kv)) (R_b (snd kv))"
    unfolding map_to_set_def by (case_tac kv, simp)

  have "(x{(k, v). m k = Some v}. yS_b (snd x). {(x, y)}) = {((k,v), e) . 
          (m k = Some v)  e  S_b v}" by (auto)
  with set_iterator_genord_product_correct [OF it_a, of "λkv. it_b (snd kv)" 
    "λkv. S_b (snd kv)" "λkv. R_b (snd kv)", OF it_b']
  have it_ab': "set_iterator_genord (set_iterator_product it_a (λkv. it_b (snd kv)))
      {((k,v), e) . (m k = Some v)  e  S_b v}
      (set_iterator_product_order R_a
        (λkv. R_b (snd kv)))"
     (is "set_iterator_genord ?it_ab' ?S_ab' ?R_ab'")
    unfolding map_to_set_def
    by (simp add: Sigma_def)

  let ?g = "λkvv'. (fst (fst kvv'), snd kvv')"
  have inj_g: "inj_on ?g ?S_ab'"
    unfolding inj_on_def by simp

  have R_ab_OK: "x y.
      x  {((k, v), e). m k = Some v  e  S_b v} 
      y  {((k, v), e). m k = Some v  e  S_b v} 
      set_iterator_product_order R_a (λkv. R_b (snd kv)) x y 
      R_ab (fst (fst x), snd x) (fst (fst y), snd y)"
    apply (simp add: set_iterator_product_order_def)
    apply clarify
    apply (simp)
    apply (unfold fst_conv snd_conv)
    apply (metis R'_prop option.inject)
  done

  have "(?g ` {((k, v), e). m k = Some v  e  S_b v}) = {(k, e). v. m k = Some v  e  S_b v}" 
    by (simp add: image_iff set_eq_iff)
  with set_iterator_genord_image_correct [OF it_ab' inj_g, of R_ab, OF R_ab_OK]
  show ?thesis 
    by (simp add: map_iterator_product_def)
qed

lemma map_iterator_product_correct :
  assumes it_a: "map_iterator it_a m"
  assumes it_b: "k v. m k = Some v  set_iterator (it_b v) (S_b v)"
  shows "set_iterator (map_iterator_product it_a it_b) 
         {(k, e) . (v. m k = Some v  e  S_b v)}"
proof -
  note res' = map_iterator_genord_product_correct [OF it_a[unfolded set_iterator_def], 
     of it_b S_b "λ_ _ _. True"]
  note res = set_iterator_intro [OF res']
  with it_b show ?thesis unfolding set_iterator_def by simp
qed

  
subsubsection‹Key Filter›

definition map_iterator_key_filter ::
    "('a  bool)  ('a × 'b,) set_iterator  ('a × 'b,) set_iterator" where
  "map_iterator_key_filter P  set_iterator_filter (P  fst)"

lemma map_iterator_key_filter_foldli_conv :
  "map_iterator_key_filter P (foldli kvs) =  foldli (filter (λ(k, v). P k) kvs)"
unfolding map_iterator_key_filter_def set_iterator_filter_foldli_conv o_def split_def 
by simp

lemma map_iterator_key_filter_alt_def [code] :
  "map_iterator_key_filter P it = (λc f. it c (λx σ. if P (fst x) then f x σ else σ))"
unfolding map_iterator_key_filter_def set_iterator_filter_alt_def
  set_iterator_image_filter_def by simp

lemma map_iterator_genord_key_filter_correct :
  fixes it :: "('a × 'b, ) set_iterator"
  assumes it_OK: "map_iterator_genord it m R"
  shows "map_iterator_genord (map_iterator_key_filter P it) (m |` {k . P k}) R"
proof - 
  from set_iterator_genord_filter_correct [OF it_OK, of "P  fst", 
    folded map_iterator_key_filter_def] 
  have step1: "set_iterator_genord (map_iterator_key_filter P it)
                  {x  map_to_set m. (P  fst) x} R" 
    by simp

  have "{x  map_to_set m. (P  fst) x} = map_to_set (m |` {k . P k})"
    unfolding map_to_set_def restrict_map_def
    by (auto split: if_splits)
  with step1 show ?thesis by simp
qed

lemma map_iterator_key_filter_correct :
  assumes it_OK: "map_iterator it m"
  shows "set_iterator (map_iterator_key_filter P it) (map_to_set (m |` {k . P k}))"
using assms
unfolding set_iterator_def
apply (rule_tac map_iterator_genord_key_filter_correct)
apply simp_all
done

end


Theory Proper_Iterator

section ‹Proper Iterators›
theory Proper_Iterator
imports 
  SetIteratorOperations 
  Automatic_Refinement.Refine_Lib
begin
  text ‹
    Proper iterators provide a way to obtain polymorphic iterators even
    inside locale contexts.

    For this purpose, an iterator that converts the set to a list is fixed
    inside the locale, and polymorphic iterators are described by folding
    over the generated list.

    In order to ensure efficiency, it is shown that folding over the generated
    list is equivalent to directly iterating over the set, and this equivalence
    is set up as a code preprocessing rule.
›

  subsection ‹Proper Iterators›

  text ‹A proper iterator can be expressed as a fold over a list, where
    the list does only depend on the set. In particular, it does not depend
    on the type of the state. We express this by the following definition, 
    using two iterators with different types:›

  definition proper_it 
    :: "('x,'σ1) set_iterator  ('x,'σ2) set_iterator  bool"
    where "proper_it it it'  (l. it=foldli l  it'=foldli l)"

  lemma proper_itI[intro?]:
    fixes it :: "('x,'σ1) set_iterator" 
    and it' :: "('x,'σ2) set_iterator"
    assumes "it=foldli l  it'=foldli l"
    shows "proper_it it it'"
    using assms unfolding proper_it_def by auto

  lemma proper_itE:
    fixes it :: "('x,'σ1) set_iterator" 
    and it' :: "('x,'σ2) set_iterator"
    assumes "proper_it it it'"
    obtains l where "it=foldli l" and "it'=foldli l"
    using assms unfolding proper_it_def by auto

  lemma proper_it_parE:
    fixes it :: "'a  ('x,'σ1) set_iterator" 
    and it' :: "'a  ('x,'σ2) set_iterator"
    assumes "x. proper_it (it x) (it' x)"
    obtains f where "it = (λx. foldli (f x))" and "it' = (λx. foldli (f x))"
    using assms unfolding proper_it_def
    by metis

  definition 
    proper_it'
    where "proper_it' it it'  s. proper_it (it s) (it' s)"

  lemma proper_it'I:
    "s. proper_it (it s) (it' s)  proper_it' it it'"
    unfolding proper_it'_def by blast

  lemma proper_it'D:
    "proper_it' it it'  proper_it (it s) (it' s)"
    unfolding proper_it'_def by blast





  subsubsection ‹Properness Preservation›
  ML structure Icf_Proper_Iterator = struct

      structure icf_proper_iteratorI = Named_Thms
        ( val name = @{binding icf_proper_iteratorI_raw}
          val description = "ICF (internal): Rules to show properness of iterators" )

      val get = icf_proper_iteratorI.get
  
      fun add_thm thm = icf_proper_iteratorI.add_thm thm
  
      val add = Thm.declaration_attribute add_thm

      fun del_thm thm = icf_proper_iteratorI.del_thm thm

      val del = Thm.declaration_attribute del_thm

      val setup = I
        #> icf_proper_iteratorI.setup
        #> Attrib.setup @{binding icf_proper_iteratorI} 
          (Attrib.add_del add del) 
          ("ICF: Rules to show properness of iterators")
        #> Global_Theory.add_thms_dynamic (@{binding icf_proper_iteratorI}, 
             get o Context.proof_of
            )
        
  
    end
  setup Icf_Proper_Iterator.setup

  lemma proper_iterator_trigger: 
    "proper_it it it'  proper_it it it'"
    "proper_it' itf itf'  proper_it' itf itf'" .

  declaration Tagged_Solver.declare_solver @{thms proper_iterator_trigger} 
      @{binding proper_iterator} "Proper iterator solver"
      (fn ctxt => REPEAT_ALL_NEW (resolve_tac ctxt (Icf_Proper_Iterator.get ctxt)))

  lemma pi_foldli[icf_proper_iteratorI]: 
    "proper_it (foldli l :: ('a,) set_iterator) (foldli l)"
    unfolding proper_it_def 
    by auto

  lemma pi_foldri[icf_proper_iteratorI]: 
    "proper_it (foldri l :: ('a,) set_iterator) (foldri l)"
    unfolding proper_it_def foldri_def by auto

  lemma pi'_foldli[icf_proper_iteratorI]: 
    "proper_it' (foldli o tsl) (foldli o tsl)"
    apply (clarsimp simp add: proper_it'_def)
    apply (tagged_solver)
    done

  lemma pi'_foldri[icf_proper_iteratorI]: 
    "proper_it' (foldri o tsl) (foldri o tsl)"
    apply (clarsimp simp add: proper_it'_def)
    apply (tagged_solver)
    done

  text ‹Iterator combinators preserve properness›
  lemma pi_emp[icf_proper_iteratorI]: 
    "proper_it set_iterator_emp set_iterator_emp"
    unfolding proper_it_def set_iterator_emp_def[abs_def]
    by (auto intro!: ext exI[where x="[]"])

  lemma pi_sng[icf_proper_iteratorI]:
    "proper_it (set_iterator_sng x) (set_iterator_sng x)"
    unfolding proper_it_def set_iterator_sng_def[abs_def]
    by (auto intro!: ext exI[where x="[x]"])

  lemma pi_union[icf_proper_iteratorI]:
    assumes PA: "proper_it it_a it_a'"
    assumes PB: "proper_it it_b it_b'"
    shows "proper_it (set_iterator_union it_a it_b)
      (set_iterator_union it_a' it_b')"
    unfolding set_iterator_union_def
    apply (rule proper_itE[OF PA])
    apply (rule proper_itE[OF PB])
    apply (rule_tac l="l@la" in proper_itI)
    apply simp
    apply (intro conjI ext)
    apply (simp_all add: foldli_append)
    done

  lemma pi_product[icf_proper_iteratorI]:
    fixes it_a :: "('a,'σa) set_iterator"
    fixes it_b :: "'a  ('b,'σa) set_iterator"
    assumes PA: "proper_it it_a it_a'"
    and PB: "x. proper_it (it_b x) (it_b' x)"
    shows "proper_it (set_iterator_product it_a it_b)
      (set_iterator_product it_a' it_b')"
  proof -
    from PB have PB': "x. proper_it (it_b x) (it_b' x)" ..
    show ?thesis
      unfolding proper_it_def
      apply (rule proper_itE[OF PA])
      apply (rule proper_it_parE[OF PB'])
      apply (auto simp add: set_iterator_product_foldli_conv)
      done
  qed

  lemma pi_image_filter[icf_proper_iteratorI]:
    fixes it :: "('x,'σ1) set_iterator" 
    and it' :: "('x,'σ2) set_iterator"
    and g :: "'x  'y option"
    assumes P: "proper_it it it'"
    shows "proper_it (set_iterator_image_filter g it) 
      (set_iterator_image_filter g it')"
    unfolding proper_it_def
    apply (rule proper_itE[OF P])
    apply (auto simp: set_iterator_image_filter_foldli_conv)
    done

  lemma pi_filter[icf_proper_iteratorI]:
    assumes P: "proper_it it it'"
    shows "proper_it (set_iterator_filter P it) 
      (set_iterator_filter P it')"
    unfolding proper_it_def
    apply (rule proper_itE[OF P])
    by (auto simp: set_iterator_filter_foldli_conv)

  lemma pi_image[icf_proper_iteratorI]:
    assumes P: "proper_it it it'"
    shows "proper_it (set_iterator_image g it) 
      (set_iterator_image g it')"
    unfolding proper_it_def
    apply (rule proper_itE[OF P])
    by (auto simp: set_iterator_image_foldli_conv)

  lemma pi_dom[icf_proper_iteratorI]:
    assumes P: "proper_it it it'"
    shows "proper_it (map_iterator_dom it) 
      (map_iterator_dom it')"
    unfolding proper_it_def
    apply (rule proper_itE[OF P])
    by (auto simp: map_iterator_dom_foldli_conv)

  lemma set_iterator_product_eq2:
    assumes "aset la. itb a = itb' a"
    shows "set_iterator_product (foldli la) itb
    = set_iterator_product (foldli la) itb'"
  proof (intro ext)
    fix c f σ
    show "set_iterator_product (foldli la) itb c f σ
      = set_iterator_product (foldli la) itb' c f σ"
      using assms
      unfolding set_iterator_product_def
      apply (induct la arbitrary: σ)
      apply (auto)
      done
  qed


subsubsection ‹Optimizing Folds›
  text ‹
    Using an iterator to create a list. The optimizations will
    match the pattern foldli (it_to_list it s)›
  definition "it_to_list it s  (it s) (λ_. True) (λx l. l@[x]) []"

  lemma map_it_to_list_genord_correct:
    assumes A: "map_iterator_genord (it s) m (λ(k,_) (k',_). R k k')"
    shows "map_of (it_to_list it s) = m
       distinct (map fst (it_to_list it s))
       sorted_wrt R ((map fst (it_to_list it s)))"
    unfolding it_to_list_def
    apply (rule map_iterator_genord_rule_insert_P[OF A, where I="
      λit l. map_of l = m |` it 
         distinct (map fst l) 
         sorted_wrt R ((map fst l))
      "])
    apply auto
    apply (auto simp: restrict_map_def) []
    apply (metis Some_eq_map_of_iff restrict_map_eq(2))
    apply (auto simp add: sorted_wrt_append)
    by (metis (lifting) restrict_map_eq(2) weak_map_of_SomeI)

  lemma (in linorder) map_it_to_list_linord_correct:
    assumes A: "map_iterator_linord (it s) m"
    shows "map_of (it_to_list it s) = m
       distinct (map fst (it_to_list it s))
       sorted ((map fst (it_to_list it s)))"
    using map_it_to_list_genord_correct[where it=it,
      OF A[unfolded set_iterator_map_linord_def]]
    by (simp add: sorted_sorted_wrt)

  lemma (in linorder) map_it_to_list_rev_linord_correct:
    assumes A: "map_iterator_rev_linord (it s) m"
    shows "map_of (it_to_list it s) = m
       distinct (map fst (it_to_list it s))
       sorted (rev (map fst (it_to_list it s)))"
    using map_it_to_list_genord_correct[where it=it,
      OF A[unfolded set_iterator_map_rev_linord_def]]
    by simp

 
end

Theory It_to_It

theory It_to_It
imports 
  Proper_Iterator
begin

  lemma proper_it_fold: 
    "proper_it it it'  foldli (it (λ_. True) (λx l. l@[x]) []) = it'"
    unfolding proper_it_def by auto
  lemma proper_it_unfold: 
    "proper_it it it'  it' = foldli (it (λ_. True) (λx l. l@[x]) [])"
    unfolding proper_it_def by auto


  text ‹The following constant converts an iterator over list-state
    to an iterator over arbitrary state›
  definition it_to_it :: "('x,'x list) set_iterator  ('x,) set_iterator"
    where [code del]: "it_to_it it 
     (foldli (it (λ_. True) (λx l. l@[x]) []))"

  lemma pi_it_to_it[icf_proper_iteratorI]: "proper_it (it_to_it I) (it_to_it I)"
    unfolding it_to_it_def by (rule pi_foldli)
  text ‹In case of a proper iterator, it is equivalent to direct iteration›
  lemma it_to_it_fold: "proper_it it (it'::('x,) set_iterator) 
     it_to_it it = it'"
    unfolding it_to_it_def
    by (simp add: proper_it_fold)

  lemma it_to_it_map_fold:
    assumes P: "proper_it it it'"
    shows "it_to_it (λc f. it c (f  f')) = (λc f. it' c (f o f'))"
    apply (rule proper_itE[OF P])
    unfolding it_to_it_def
    apply (intro ext)
    apply (simp add: foldli_foldl map_by_foldl foldli_map)
    done

  lemma it_to_it_fold': "proper_it' it (it'::'s  ('x,) set_iterator) 
     it_to_it (it s) = (it' s)"
    by (drule proper_it'D) (rule it_to_it_fold)

  lemma it_to_it_map_fold':
    assumes P: "proper_it' it it'"
    shows "it_to_it (λc f. it s c (f  f')) = (λc f. it' s c (f o f'))"
    using P[THEN proper_it'D] by (rule it_to_it_map_fold)

  text ‹This locale wraps up the setup of a proper iterator for use
    with it_to_it›.›
  locale proper_it_loc =
    fixes it :: "'s  ('x,'x list) set_iterator"
    and it' :: "'s  ('x,) set_iterator"
    assumes proper': "proper_it' it it'"
  begin
    lemma proper: "proper_it (it s) (it' s)"
      using proper' by (rule proper_it'D)

    lemmas it_to_it_code_unfold[code_unfold] = it_to_it_fold[OF proper]
  end

  subsubsection ‹Correctness›
  text ‹The polymorphic iterator is a valid iterator again.›
  lemma it_to_it_genord_correct: 
    assumes "set_iterator_genord (it::('x,'x list) set_iterator) S R" 
    shows "set_iterator_genord ((it_to_it it)::('x,) set_iterator) S R"
  proof -
    interpret set_iterator_genord it S R by fact

    show ?thesis
      apply (unfold_locales)
      unfolding it_to_it_def
      using foldli_transform
      by auto
  qed

  lemma it_to_it_linord_correct: 
    assumes "set_iterator_linord (it::('x::linorder,'x list) set_iterator) S" 
    shows "set_iterator_linord ((it_to_it it)::('x,) set_iterator) S"
    using assms
    unfolding set_iterator_linord_def
    by (rule it_to_it_genord_correct)

  lemma it_to_it_rev_linord_correct: 
    assumes "set_iterator_rev_linord (it::('x::linorder,'x list) set_iterator) S"
    shows "set_iterator_rev_linord ((it_to_it it)::('x,) set_iterator) S"
    using assms
    unfolding set_iterator_rev_linord_def
    by (rule it_to_it_genord_correct)

  lemma it_to_it_correct: 
    assumes "set_iterator (it::('x,'x list) set_iterator) S" 
    shows "set_iterator ((it_to_it it)::('x,) set_iterator) S"
    using assms
    unfolding set_iterator_def
    by (rule it_to_it_genord_correct)

  lemma it_to_it_map_genord_correct:
    assumes "map_iterator_genord (it::('u,'v,('u×'v) list) map_iterator) S R" 
    shows "map_iterator_genord ((it_to_it it)::('u,'v,) map_iterator) S R"
    using assms by (rule it_to_it_genord_correct)

  lemma it_to_it_map_linord_correct:
    assumes "map_iterator_linord (it::('u::linorder,'v,('u×'v) list) map_iterator) S" 
    shows "map_iterator_linord ((it_to_it it)::('u,'v,) map_iterator) S"
    using assms unfolding set_iterator_map_linord_def by (rule it_to_it_genord_correct)

  lemma it_to_it_map_rev_linord_correct:
    assumes 
      "map_iterator_rev_linord (it::('u::linorder,'v,('u×'v) list) map_iterator) S" 
    shows "map_iterator_rev_linord ((it_to_it it)::('u,'v,) map_iterator) S"
    using assms unfolding set_iterator_map_rev_linord_def 
    by (rule it_to_it_genord_correct)

  lemma it_to_it_map_correct:
    assumes "map_iterator (it::('u,'v,('u×'v) list) map_iterator) S" 
    shows "map_iterator ((it_to_it it)::('u,'v,) map_iterator) S"
    using assms by (rule it_to_it_correct)






end

Theory SetIteratorGA

(*  Title:       General Algorithms for Iterators
    Author:      Thomas Tuerk <tuerk@in.tum.de>
    Maintainer:  Thomas Tuerk <tuerk@in.tum.de>
*)
section ‹General Algorithms for Iterators over Finite Sets›
theory SetIteratorGA
imports Main SetIteratorOperations
begin

subsection ‹Quantification›

definition iterate_ball where
    "iterate_ball (it::('x,bool) set_iterator) P = it id (λx σ. P x) True"

lemma iterate_ball_correct :
assumes it: "set_iterator it S0"
shows "iterate_ball it P = (xS0. P x)"
unfolding iterate_ball_def
apply (rule set_iterator_rule_P [OF it,
            where I = "λS σ. σ = (xS0-S. P x)"])
apply auto
done

definition iterate_bex where
    "iterate_bex (it::('x,bool) set_iterator) P = it (λσ. ¬σ) (λx σ. P x) False"

lemma iterate_bex_correct :
assumes it: "set_iterator it S0"
shows "iterate_bex it P = (xS0. P x)"
unfolding iterate_bex_def
apply (rule set_iterator_rule_P [OF it, where I = "λS σ. σ = (xS0-S. P x)"])
apply auto
done

subsection ‹Iterator to List›

definition iterate_to_list where
    "iterate_to_list (it::('x,'x list) set_iterator) = it (λ_. True) (λx σ. x # σ) []"

lemma iterate_to_list_foldli [simp] :
  "iterate_to_list (foldli xs) = rev xs"
unfolding iterate_to_list_def
by (induct xs rule: rev_induct, simp_all add: foldli_snoc) 

lemma iterate_to_list_genord_correct :
assumes it: "set_iterator_genord it S0 R"
shows "set (iterate_to_list it) = S0  distinct (iterate_to_list it) 
       sorted_wrt R (rev (iterate_to_list it))"
using it unfolding set_iterator_genord_foldli_conv by auto

lemma iterate_to_list_correct :
assumes it: "set_iterator it S0"
shows "set (iterate_to_list it) = S0  distinct (iterate_to_list it)"
using iterate_to_list_genord_correct [OF it[unfolded set_iterator_def]]
by simp

lemma (in linorder) iterate_to_list_linord_correct :
fixes S0 :: "'a set"
assumes it_OK: "set_iterator_linord it S0"
shows "set (iterate_to_list it) = S0  distinct (iterate_to_list it) 
       sorted (rev (iterate_to_list it))"
using it_OK unfolding set_iterator_linord_foldli_conv by auto

lemma (in linorder) iterate_to_list_rev_linord_correct :
fixes S0 :: "'a set"
assumes it_OK: "set_iterator_rev_linord it S0"
shows "set (iterate_to_list it) = S0  distinct (iterate_to_list it) 
       sorted (iterate_to_list it)"
using it_OK unfolding set_iterator_rev_linord_foldli_conv by auto

lemma (in linorder) iterate_to_list_map_linord_correct :
assumes it_OK: "map_iterator_linord it m"
shows "map_of (iterate_to_list it) = m  distinct (map fst (iterate_to_list it)) 
       sorted (map fst (rev (iterate_to_list it)))"
using it_OK unfolding map_iterator_linord_foldli_conv 
by clarify (simp add: rev_map[symmetric])

lemma (in linorder) iterate_to_list_map_rev_linord_correct :
assumes it_OK: "map_iterator_rev_linord it m"
shows "map_of (iterate_to_list it) = m  distinct (map fst (iterate_to_list it)) 
       sorted (map fst (iterate_to_list it))"
using it_OK unfolding map_iterator_rev_linord_foldli_conv 
by clarify (simp add: rev_map[symmetric])


subsection ‹Size›

lemma set_iterator_finite :
assumes it: "set_iterator it S0"
shows "finite S0"
using set_iterator_genord.finite_S0 [OF it[unfolded set_iterator_def]] .

lemma map_iterator_finite :
assumes it: "map_iterator it m"
shows "finite (dom m)"
using set_iterator_genord.finite_S0 [OF it[unfolded set_iterator_def]]
by (simp add: finite_map_to_set) 

definition iterate_size where
    "iterate_size (it::('x,nat) set_iterator) = it (λ_. True) (λx σ. Suc σ) 0"

lemma iterate_size_correct :
assumes it: "set_iterator it S0"
shows "iterate_size it = card S0  finite S0"
unfolding iterate_size_def
apply (rule_tac set_iterator_rule_insert_P [OF it, 
    where I = "λS σ. σ = card S  finite S"])
apply auto
done

definition iterate_size_abort where
  "iterate_size_abort (it::('x,nat) set_iterator) n = it (λσ. σ < n) (λx σ. Suc σ) 0"

lemma iterate_size_abort_correct :
assumes it: "set_iterator it S0"
shows "iterate_size_abort it n = (min n (card S0))  finite S0"
unfolding iterate_size_abort_def
proof (rule set_iterator_rule_insert_P [OF it,
   where I = "λS σ. σ = (min n (card S))  finite S"], goal_cases)
  case (4 σ S)
  assume "S  S0" "S  S0" "¬ σ < n" "σ = min n (card S)  finite S" 

  from σ = min n (card S)  finite S ¬ σ < n 
  have "σ = n" "n  card S"
    by (auto simp add: min_less_iff_disj)

  note fin_S0 = set_iterator_genord.finite_S0 [OF it[unfolded set_iterator_def]]
  from card_mono [OF fin_S0 S  S0] have "card S  card S0" .
  
  with σ = n n  card S fin_S0
  show "σ = min n (card S0)  finite S0" by simp
qed simp_all

subsection ‹Emptyness Check›

definition iterate_is_empty_by_size where
    "iterate_is_empty_by_size it = (iterate_size_abort it 1 = 0)"

lemma iterate_is_empty_by_size_correct :
assumes it: "set_iterator it S0"
shows "iterate_is_empty_by_size it = (S0 = {})"
using iterate_size_abort_correct[OF it, of 1]
unfolding iterate_is_empty_by_size_def
by (cases "card S0") auto

definition iterate_is_empty where
    "iterate_is_empty (it::('x,bool) set_iterator) = (it (λb. b) (λ_ _. False) True)"

lemma iterate_is_empty_correct :
assumes it: "set_iterator it S0"
shows "iterate_is_empty it = (S0 = {})"
unfolding iterate_is_empty_def
apply (rule set_iterator_rule_insert_P [OF it,
   where I = "λS σ. σ  S = {}"])
apply auto
done

subsection ‹Check for singleton Sets›

definition iterate_is_sng where
    "iterate_is_sng it = (iterate_size_abort it 2 = 1)"

lemma iterate_is_sng_correct :
assumes it: "set_iterator it S0"
shows "iterate_is_sng it = (card S0 = 1)"
using iterate_size_abort_correct[OF it, of 2]
unfolding iterate_is_sng_def
apply (cases "card S0", simp, rename_tac n')
apply (case_tac n')
apply auto
done

subsection ‹Selection›

definition iterate_sel where
    "iterate_sel (it::('x,'y option) set_iterator) f = it (λσ. σ = None) (λx σ. f x) None"

lemma iterate_sel_genord_correct :
assumes it_OK: "set_iterator_genord it S0 R"
shows "iterate_sel it f = None  (xS0. (f x = None))"
      "iterate_sel it f = Some y  (x  S0. f x = Some y  (x'  S0-{x}. y. f x' = Some y'  R x x'))"
proof -
  show "iterate_sel it f = None  (xS0. (f x = None))"
    unfolding iterate_sel_def
    apply (rule_tac set_iterator_genord.iteratei_rule_insert_P [OF it_OK, 
       where I = "λS σ. (σ = None)  (xS. (f x = None))"])
    apply auto
  done
next
  have "iterate_sel it f = Some y  (x  S0. f x = Some y  (x'  S0-{x}. y'. f x' = Some y'  R x x'))"
    unfolding iterate_sel_def
    apply (rule_tac set_iterator_genord.iteratei_rule_insert_P [OF it_OK, 
       where I = "λS σ. (y. σ = Some y  (x  S. f x = Some y  (x'  S-{x}.y'. f x' = Some y'  R x x'))) 
                        ((σ = None)  (xS. f x = None))"])
    apply simp
    apply (auto simp add: Bex_def subset_iff Ball_def)
    apply metis
  done
  moreover assume "iterate_sel it f = Some y" 
  finally show "(x  S0. f x = Some y  (x'  S0-{x}. y. f x' = Some y'  R x x'))" by blast
qed


definition iterate_sel_no_map where
    "iterate_sel_no_map it P = iterate_sel it (λx. if P x then Some x else None)" 
lemmas iterate_sel_no_map_alt_def = iterate_sel_no_map_def[unfolded iterate_sel_def, code]

lemma iterate_sel_no_map_genord_correct :
assumes it_OK: "set_iterator_genord it S0 R"
shows "iterate_sel_no_map it P = None  (xS0. ¬(P x))"
      "iterate_sel_no_map it P = Some x  (x  S0  P x  (x'  S0-{x}. P x'  R x x'))"
unfolding iterate_sel_no_map_def
using iterate_sel_genord_correct[OF it_OK, of "λx. if P x then Some x else None"]
apply (simp_all add: Bex_def)
apply (metis option.inject option.simps(2)) 
done

lemma iterate_sel_no_map_correct :
assumes it_OK: "set_iterator it S0"
shows "iterate_sel_no_map it P = None  (xS0. ¬(P x))"
      "iterate_sel_no_map it P = Some x  x  S0  P x"
proof -
  note iterate_sel_no_map_genord_correct [OF it_OK[unfolded set_iterator_def], of P]
  thus "iterate_sel_no_map it P = None  (xS0. ¬(P x))"
       "iterate_sel_no_map it P = Some x  x  S0  P x"
    by simp_all
qed

lemma (in linorder) iterate_sel_no_map_linord_correct :
assumes it_OK: "set_iterator_linord it S0"
shows "iterate_sel_no_map it P = None  (xS0. ¬(P x))"
      "iterate_sel_no_map it P = Some x  (x  S0  P x  (x'S0. P x'  x  x'))"
proof -
  note iterate_sel_no_map_genord_correct [OF it_OK[unfolded set_iterator_linord_def], of P]
  thus "iterate_sel_no_map it P = None  (xS0. ¬(P x))"
       "iterate_sel_no_map it P = Some x  (x  S0  P x  (x'S0. P x'  x  x'))"
    by auto
qed

lemma (in linorder) iterate_sel_no_map_rev_linord_correct :
assumes it_OK: "set_iterator_rev_linord it S0"
shows "iterate_sel_no_map it P = None  (xS0. ¬(P x))"
      "iterate_sel_no_map it P = Some x  (x  S0  P x  (x'S0. P x'  x'  x))"
proof -
  note iterate_sel_no_map_genord_correct [OF it_OK[unfolded set_iterator_rev_linord_def], of P]
  thus "iterate_sel_no_map it P = None  (xS0. ¬(P x))"
       "iterate_sel_no_map it P = Some x  (x  S0  P x  (x'S0. P x'  x'  x))"
    by auto
qed


lemma iterate_sel_no_map_map_correct :
assumes it_OK: "map_iterator it m"
shows "iterate_sel_no_map it P = None  (k v. m k = Some v  ¬(P (k, v)))"
      "iterate_sel_no_map it P = Some (k, v)  (m k = Some v  P (k, v))"
proof -
  note iterate_sel_no_map_genord_correct [OF it_OK[unfolded set_iterator_def], of P]
  thus "iterate_sel_no_map it P = None  (k v. m k = Some v  ¬(P (k, v)))"
       "iterate_sel_no_map it P = Some (k, v)  (m k = Some v  P (k, v))"
    by (auto simp add: map_to_set_def)
qed

lemma (in linorder) iterate_sel_no_map_map_linord_correct :
assumes it_OK: "map_iterator_linord it m"
shows "iterate_sel_no_map it P = None  (k v. m k = Some v  ¬(P (k, v)))"
      "iterate_sel_no_map it P = Some (k, v)  (m k = Some v  P (k, v)  (k' v' . m k' = Some v' 
           P (k', v')  k  k'))"
proof -
  note iterate_sel_no_map_genord_correct [OF it_OK[unfolded set_iterator_map_linord_def], of P]
  thus "iterate_sel_no_map it P = None  (k v. m k = Some v  ¬(P (k, v)))"
       "iterate_sel_no_map it P = Some (k, v)  (m k = Some v  P (k, v)  (k' v' . m k' = Some v' 
           P (k', v')  k  k'))"
    apply (auto simp add: map_to_set_def Ball_def) 
  done
qed

lemma (in linorder) iterate_sel_no_map_map_rev_linord_correct :
assumes it_OK: "map_iterator_rev_linord it m"
shows "iterate_sel_no_map it P = None  (k v. m k = Some v  ¬(P (k, v)))"
      "iterate_sel_no_map it P = Some (k, v)  (m k = Some v  P (k, v)  (k' v' . m k' = Some v' 
           P (k', v')  k'  k))"
proof -
  note iterate_sel_no_map_genord_correct [OF it_OK[unfolded set_iterator_map_rev_linord_def], of P]
  thus "iterate_sel_no_map it P = None  (k v. m k = Some v  ¬(P (k, v)))"
       "iterate_sel_no_map it P = Some (k, v)  (m k = Some v  P (k, v)  (k' v' . m k' = Some v' 
           P (k', v')  k'  k))"
    apply (auto simp add: map_to_set_def Ball_def) 
  done
qed


subsection ‹Creating ordered iterators›

text ‹One can transform an iterator into an ordered one by converting it to list, 
        sorting this list and then converting back to an iterator. In general, this brute-force
        method is inefficient, though.›

definition iterator_to_ordered_iterator where
  "iterator_to_ordered_iterator sort_fun it =
   foldli (sort_fun (iterate_to_list it))"

lemma iterator_to_ordered_iterator_correct :
assumes sort_fun_OK: "l. sorted_wrt R (sort_fun l)  mset (sort_fun l) = mset l"
    and it_OK: "set_iterator it S0"
shows "set_iterator_genord (iterator_to_ordered_iterator sort_fun it) S0 R"
proof -
  define l where "l = iterate_to_list it"
  have l_props: "set l = S0" "distinct l" 
    using iterate_to_list_correct [OF it_OK, folded l_def] by simp_all

  with sort_fun_OK[of l] have sort_l_props:
    "sorted_wrt R (sort_fun l)"
    "set (sort_fun l) = S0" "distinct (sort_fun l)"
    apply (simp_all)
    apply (metis set_mset_mset)
    apply (metis distinct_count_atmost_1 set_mset_mset)
  done

  show ?thesis
    apply (rule set_iterator_genord_I[of "sort_fun l"])
    apply (simp_all add: sort_l_props iterator_to_ordered_iterator_def l_def[symmetric])
  done
qed


definition iterator_to_ordered_iterator_quicksort where
  "iterator_to_ordered_iterator_quicksort R it =
   iterator_to_ordered_iterator (quicksort_by_rel R []) it"

lemmas iterator_to_ordered_iterator_quicksort_code[code] =
  iterator_to_ordered_iterator_quicksort_def[unfolded iterator_to_ordered_iterator_def]

lemma iterator_to_ordered_iterator_quicksort_correct :
assumes lin : "x y. (R x y)  (R y x)"
    and trans_R: "x y z. R x y  R y z  R x z"
    and it_OK: "set_iterator it S0"
shows "set_iterator_genord (iterator_to_ordered_iterator_quicksort R it) S0 R"
unfolding iterator_to_ordered_iterator_quicksort_def
apply (rule iterator_to_ordered_iterator_correct [OF _ it_OK])
apply (simp_all add: sorted_wrt_quicksort_by_rel[OF lin trans_R])
done

definition iterator_to_ordered_iterator_mergesort where
  "iterator_to_ordered_iterator_mergesort R it =
   iterator_to_ordered_iterator (mergesort_by_rel R) it"

lemmas iterator_to_ordered_iterator_mergesort_code[code] =
  iterator_to_ordered_iterator_mergesort_def[unfolded iterator_to_ordered_iterator_def]

lemma iterator_to_ordered_iterator_mergesort_correct :
assumes lin : "x y. (R x y)  (R y x)"
    and trans_R: "x y z. R x y  R y z  R x z"
    and it_OK: "set_iterator it S0"
shows "set_iterator_genord (iterator_to_ordered_iterator_mergesort R it) S0 R"
unfolding iterator_to_ordered_iterator_mergesort_def
apply (rule iterator_to_ordered_iterator_correct [OF _ it_OK])
apply (simp_all add: sorted_wrt_mergesort_by_rel[OF lin trans_R])
done

end


Theory Gen_Iterator

section ‹\isaheader{Iterators}›
theory Gen_Iterator
imports Refine_Monadic.Refine_Monadic Proper_Iterator
begin
  text ‹
    Iterators are realized by to-list functions followed by folding.
    A post-optimization step then replaces these constructions by
    real iterators.›

  lemma param_it_to_list[param]: "(it_to_list,it_to_list) 
    (Rs  (Ra  bool_rel)  
    (Rb  Rblist_rel  Rblist_rel)  Rclist_rel  Rd)  Rs  Rd"
    unfolding it_to_list_def[abs_def]
    by parametricity


  definition key_rel :: "('k  'k  bool)  ('k×'v)  ('k×'v)  bool"
    where "key_rel R a b  R (fst a) (fst b)"

  lemma key_rel_UNIV[simp]: "key_rel (λ_ _. True) = (λ_ _. True)"
    unfolding key_rel_def[abs_def] by auto

  subsection ‹Setup for Autoref›
  text ‹Default pattern rules for it_to_sorted_list›
  definition "set_to_sorted_list R S  it_to_sorted_list R S"
  lemma set_to_sorted_list_itype[autoref_itype]: 
    "set_to_sorted_list R ::i Iii_set i Iii_listii_nres" 
    by simp

context begin interpretation autoref_syn .
  lemma set_to_sorted_list_pat[autoref_op_pat]: 
    "it_to_sorted_list R S  OP (set_to_sorted_list R) S"
    unfolding set_to_sorted_list_def[abs_def] by auto
end

  definition "map_to_sorted_list R M 
     it_to_sorted_list (key_rel R) (map_to_set M)"
  lemma map_to_sorted_list_itype[autoref_itype]:
    "map_to_sorted_list R ::i Rk,Rvii_map i Rk,Rvii_prodii_listii_nres"
    by simp

context begin interpretation autoref_syn .
  lemma map_to_sorted_list_pat[autoref_op_pat]:
    "it_to_sorted_list (key_rel R) (map_to_set M) 
       OP (map_to_sorted_list R) M"
    "it_to_sorted_list (λ_ _. True) (map_to_set M) 
       OP (map_to_sorted_list (λ_ _. True)) M"
    unfolding map_to_sorted_list_def[abs_def] by auto
end

  subsection ‹Set iterators›
  (*definition "is_set_to_sorted_list_deprecated ordR Rk Rs tsl ≡ ∀s s'.
    (s,s')∈⟨Rk⟩Rs ⟶ 
      (RETURN (tsl s),it_to_sorted_list ordR s')∈⟨⟨Rk⟩list_rel⟩nres_rel"
    *)

  definition "is_set_to_sorted_list ordR Rk Rs tsl  s s'.
    (s,s')RkRs 
       ( l'. (tsl s,l')Rklist_rel 
             RETURN l'  it_to_sorted_list ordR s')"

  definition "is_set_to_list  is_set_to_sorted_list (λ_ _. True)"


  lemma is_set_to_sorted_listE:
    assumes "is_set_to_sorted_list ordR Rk Rs tsl"
    assumes "(s,s')RkRs"
    obtains l' where "(tsl s,l')Rklist_rel" 
    and "RETURN l'  it_to_sorted_list ordR s'"
    using assms unfolding is_set_to_sorted_list_def by blast

  (* TODO: Move *)
  lemma it_to_sorted_list_weaken: 
    "RR'  it_to_sorted_list R s  it_to_sorted_list R' s"
    unfolding it_to_sorted_list_def
    by (auto intro!: sorted_wrt_mono_rel[where P=R])

  lemma set_to_list_by_set_to_sorted_list[autoref_ga_rules]:
    assumes "GEN_ALGO_tag (is_set_to_sorted_list ordR Rk Rs tsl)"
    shows "is_set_to_list Rk Rs tsl"
    using assms
    unfolding is_set_to_list_def is_set_to_sorted_list_def autoref_tag_defs
    apply (safe)
    apply (drule spec, drule spec, drule (1) mp)
    apply (elim exE conjE)
    apply (rule exI, rule conjI, assumption)
    apply (rule order_trans, assumption)
    apply (rule it_to_sorted_list_weaken)
    by blast


  definition "det_fold_set R c f σ result  
    l. distinct l  sorted_wrt R l  foldli l c f σ = result (set l)"

  lemma det_fold_setI[intro?]:
    assumes "l. distinct l; sorted_wrt R l 
       foldli l c f σ = result (set l)"
    shows "det_fold_set R c f σ result"
    using assms unfolding det_fold_set_def by auto

  text ‹Template lemma for generic algorithm using set iterator›
  lemma det_fold_sorted_set:
    assumes 1: "det_fold_set ordR c' f' σ' result"
    assumes 2: "is_set_to_sorted_list ordR Rk Rs tsl"
    assumes SREF[param]: "(s,s')RkRs"
    assumes [param]:  "(c,c')Id"
    assumes [param]: "(f,f')Rk    "
    assumes [param]: "(σ,σ')"
    shows "(foldli (tsl s) c f σ, result s')  "
  proof -
    obtain tsl' where
      [param]: "(tsl s,tsl')  Rklist_rel" 
      and IT: "RETURN tsl'  it_to_sorted_list ordR s'"
      using 2 SREF
      by (rule is_set_to_sorted_listE)
    
    have "(foldli (tsl s) c f σ, foldli tsl' c' f' σ')  "
      by parametricity
    also have "foldli tsl' c' f' σ' = result s'"
      using 1 IT 
      unfolding det_fold_set_def it_to_sorted_list_def
      by simp
    finally show ?thesis .
  qed

  lemma det_fold_set:
    assumes "det_fold_set (λ_ _. True) c' f' σ' result"
    assumes "is_set_to_list Rk Rs tsl"
    assumes "(s,s')RkRs"
    assumes "(c,c')Id"
    assumes "(f,f')Rk    "
    assumes "(σ,σ')"
    shows "(foldli (tsl s) c f σ, result s')  "
    using assms
    unfolding  is_set_to_list_def
    by (rule det_fold_sorted_set)

  subsection ‹Map iterators›

  text ‹Build relation on keys›
  
  (*definition "is_map_to_sorted_list_deprecated ordR Rk Rv Rm tsl ≡ ∀m m'.
    (m,m')∈⟨Rk,Rv⟩Rm ⟶ 
      (RETURN (tsl m),it_to_sorted_list (key_rel ordR) (map_to_set m'))
      ∈⟨⟨⟨Rk,Rv⟩prod_rel⟩list_rel⟩nres_rel"*)

  definition "is_map_to_sorted_list ordR Rk Rv Rm tsl  m m'.
    (m,m')Rk,RvRm  (
      l'. (tsl m,l')Rk,Rvprod_rellist_rel
         RETURN l'  it_to_sorted_list (key_rel ordR) (map_to_set m'))"

  definition "is_map_to_list Rk Rv Rm tsl 
     is_map_to_sorted_list (λ_ _. True) Rk Rv Rm tsl"

  lemma is_map_to_sorted_listE:
    assumes "is_map_to_sorted_list ordR Rk Rv Rm tsl"
    assumes "(m,m')Rk,RvRm"
    obtains l' where "(tsl m,l')Rk,Rvprod_rellist_rel" 
    and "RETURN l'  it_to_sorted_list (key_rel ordR) (map_to_set m')"
    using assms unfolding is_map_to_sorted_list_def by blast

  lemma map_to_list_by_map_to_sorted_list[autoref_ga_rules]:
    assumes "GEN_ALGO_tag (is_map_to_sorted_list ordR Rk Rv Rm tsl)"
    shows "is_map_to_list Rk Rv Rm tsl"
    using assms
    unfolding is_map_to_list_def is_map_to_sorted_list_def autoref_tag_defs
    apply (safe)
    apply (drule spec, drule spec, drule (1) mp)
    apply (elim exE conjE)
    apply (rule exI, rule conjI, assumption)
    apply (rule order_trans, assumption)
    apply (rule it_to_sorted_list_weaken)
    unfolding key_rel_def[abs_def]
    by blast

  definition "det_fold_map R c f σ result  
    l. distinct (map fst l)  sorted_wrt (key_rel R) l 
       foldli l c f σ = result (map_of l)"

  lemma det_fold_mapI[intro?]:
    assumes "l. distinct (map fst l); sorted_wrt (key_rel R) l 
       foldli l c f σ = result (map_of l)"
    shows "det_fold_map R c f σ result"
    using assms unfolding det_fold_map_def by auto

  lemma det_fold_map_aux:
    assumes 1: "distinct (map fst l); sorted_wrt (key_rel R) l 
       foldli l c f σ = result (map_of l)"
    assumes 2: "RETURN l  it_to_sorted_list (key_rel R) (map_to_set m)"
    shows "foldli l c f σ = result m"
  proof -
    from 2 have "distinct l" and "set l = map_to_set m" 
      and SORTED: "sorted_wrt (key_rel R) l"
      unfolding it_to_sorted_list_def by simp_all
    hence "(k,v)set l. (k',v')set l. k=k'  v=v'"
      apply simp
      unfolding map_to_set_def
      apply auto
      done
    with ‹distinct l have DF: "distinct (map fst l)"
      apply (induct l)
      apply simp
      apply force
      done
    with ‹set l = map_to_set m have [simp]: "m = map_of l"
      by (metis map_of_map_to_set)
      
    from 1[OF DF SORTED] show ?thesis by simp
  qed
    
  text ‹Template lemma for generic algorithm using map iterator›
  lemma det_fold_sorted_map:
    assumes 1: "det_fold_map ordR c' f' σ' result"
    assumes 2: "is_map_to_sorted_list ordR Rk Rv Rm tsl"
    assumes MREF[param]: "(m,m')Rk,RvRm"
    assumes [param]:  "(c,c')Id"
    assumes [param]: "(f,f')Rk,Rvprod_rel    "
    assumes [param]: "(σ,σ')"
    shows "(foldli (tsl m) c f σ, result m')  "
  proof -
    obtain tsl' where
      [param]: "(tsl m,tsl')  Rk,Rvprod_rellist_rel" 
      and IT: "RETURN tsl'  it_to_sorted_list (key_rel ordR) (map_to_set m')"
      using 2 MREF by (rule is_map_to_sorted_listE)
    
    have "(foldli (tsl m) c f σ, foldli tsl' c' f' σ')  "
      by parametricity
    also have "foldli tsl' c' f' σ' = result m'"
      using det_fold_map_aux[of tsl' ordR c' f' σ' result] 1 IT
      unfolding det_fold_map_def
      by clarsimp
    finally show ?thesis .
  qed

  lemma det_fold_map:
    assumes "det_fold_map (λ_ _. True) c' f' σ' result"
    assumes "is_map_to_list Rk Rv Rm tsl"
    assumes "(m,m')Rk,RvRm"
    assumes "(c,c')Id"
    assumes "(f,f')Rk,Rvprod_rel    "
    assumes "(σ,σ')"
    shows "(foldli (tsl m) c f σ, result m')  "
    using assms
    unfolding is_map_to_list_def
    by (rule det_fold_sorted_map)

lemma set_to_sorted_list_by_tsl[autoref_rules]:
  assumes "MINOR_PRIO_TAG (- 11)"
  assumes TSL: "SIDE_GEN_ALGO (is_set_to_sorted_list R Rk Rs tsl)"
  shows "(λs. RETURN (tsl s), set_to_sorted_list R) 
     RkRs  Rklist_relnres_rel"
proof (intro fun_relI nres_relI)
  fix s s'
  assume "(s,s')RkRs"
  with TSL obtain l' where 
    R1: "(tsl s, l')  Rklist_rel" 
      and R2: "RETURN l'  set_to_sorted_list R s'"
    unfolding is_set_to_sorted_list_def set_to_sorted_list_def autoref_tag_defs
    by blast
  
  have "RETURN (tsl s)  (Rklist_rel) (RETURN l')"
    by (rule RETURN_refine) fact
  also note R2
  finally show "RETURN (tsl s)   (Rklist_rel) (set_to_sorted_list R s')" .
qed

lemma set_to_list_by_tsl[autoref_rules]:
  assumes "MINOR_PRIO_TAG (- 10)"
  assumes TSL: "SIDE_GEN_ALGO (is_set_to_list Rk Rs tsl)"
  shows "(λs. RETURN (tsl s), set_to_sorted_list (λ_ _. True)) 
     RkRs  Rklist_relnres_rel"
  using assms(2-) unfolding is_set_to_list_def
  by (rule set_to_sorted_list_by_tsl[OF PRIO_TAGI])

lemma map_to_sorted_list_by_tsl[autoref_rules]:
  assumes "MINOR_PRIO_TAG (- 11)"
  assumes TSL: "SIDE_GEN_ALGO (is_map_to_sorted_list R Rk Rv Rs tsl)"
  shows "(λs. RETURN (tsl s), map_to_sorted_list R) 
     Rk,RvRs  Rk,Rvprod_rellist_relnres_rel"
proof (intro fun_relI nres_relI)
  fix s s'
  assume "(s,s')Rk,RvRs"
  with TSL obtain l' where 
    R1: "(tsl s, l')  Rk,Rvprod_rellist_rel" 
      and R2: "RETURN l'  map_to_sorted_list R s'"
    unfolding is_map_to_sorted_list_def map_to_sorted_list_def autoref_tag_defs
    by blast
  
  have "RETURN (tsl s)  (Rk,Rvprod_rellist_rel) (RETURN l')"
    apply (rule RETURN_refine)
    by fact
  also note R2
  finally show 
    "RETURN (tsl s)   (Rk,Rvprod_rellist_rel) (map_to_sorted_list R s')" .
qed

lemma map_to_list_by_tsl[autoref_rules]:
  assumes "MINOR_PRIO_TAG (- 10)"
  assumes TSL: "SIDE_GEN_ALGO (is_map_to_list Rk Rv Rs tsl)"
  shows "(λs. RETURN (tsl s), map_to_sorted_list (λ_ _. True)) 
     Rk,RvRs  Rk,Rvprod_rellist_relnres_rel"
  using assms(2-) unfolding is_map_to_list_def
  by (rule map_to_sorted_list_by_tsl[OF PRIO_TAGI])


(*lemma dres_it_FOREACH_it_simp[iterator_simps]: 
  "dres_it_FOREACH (λs. dRETURN (i s)) s c f σ 
    = foldli (i s) (case_dres False False c) (λx s. s ⤜ f x) (dRETURN σ)"
  unfolding dres_it_FOREACH_def
  by simp
*)

text ‹
  TODO/FIXME: 
    * Integrate mono-prover properly into solver-infrastructure,
        i.e. tag a mono-goal.
    * Tag iterators, such that, for the mono-prover, we can just convert
        a proper iterator back to its foldli-equivalent!
›
lemma proper_it_mono_dres_pair:
  assumes PR: "proper_it' it it'"
  assumes A: "k v x. f k v x  f' k v x"
  shows "
    it' s (case_dres False False c) (λ(k,v) s. s  f k v) σ
     it' s (case_dres False False c) (λ(k,v) s. s  f' k v) σ" (is "?a  ?b")
proof -
  from proper_itE[OF PR[THEN proper_it'D]] obtain l where 
    A_FMT: 
      "?a = foldli l (case_dres False False c) (λ(k,v) s. s  f k v) σ" 
        (is "_ = ?a'")
    and B_FMT: 
      "?b = foldli l (case_dres False False c) (λ(k,v) s. s  f' k v) σ" 
        (is "_ = ?b'")
    by metis
  
  from A have A': "kv x. case_prod f kv x  case_prod f' kv x"
    by auto

  note A_FMT
  also have 
    "?a' = foldli l (case_dres False False c) (λkv s. s  case_prod f kv) σ"
    apply (fo_rule fun_cong)
    apply (fo_rule arg_cong)
    by auto
  also note foldli_mono_dres[OF A']
  also have 
    "foldli l (case_dres False False c) (λkv s. s  case_prod f' kv) σ = ?b'"
    apply (fo_rule fun_cong)
    apply (fo_rule arg_cong)
    by auto
  also note B_FMT[symmetric]
  finally show ?thesis .
qed

lemma proper_it_mono_dres_pair_flat:
  assumes PR: "proper_it' it it'"
  assumes A: "k v x. flat_ge (f k v x) (f' k v x)"
  shows "
    flat_ge (it' s (case_dres False False c) (λ(k,v) s. s  f k v) σ)
      (it' s (case_dres False False c) (λ(k,v) s. s  f' k v) σ)" 
      (is "flat_ge ?a ?b")
proof -
  from proper_itE[OF PR[THEN proper_it'D]] obtain l where 
    A_FMT: 
      "?a = foldli l (case_dres False False c) (λ(k,v) s. s  f k v) σ" 
        (is "_ = ?a'")
    and B_FMT: 
      "?b = foldli l (case_dres False False c) (λ(k,v) s. s  f' k v) σ" 
        (is "_ = ?b'")
    by metis
  
  from A have A': "kv x. flat_ge (case_prod f kv x) (case_prod f' kv x)"
    by auto

  note A_FMT
  also have 
    "?a' = foldli l (case_dres False False c) (λkv s. s  case_prod f kv) σ"
    apply (fo_rule fun_cong)
    apply (fo_rule arg_cong)
    by auto
  also note foldli_mono_dres_flat[OF A']
  also have 
    "foldli l (case_dres False False c) (λkv s. s  case_prod f' kv) σ = ?b'"
    apply (fo_rule fun_cong)
    apply (fo_rule arg_cong)
    by auto
  also note B_FMT[symmetric]
  finally show ?thesis .
qed

    
lemma proper_it_mono_dres:
  assumes PR: "proper_it' it it'"
  assumes A: "kv x. f kv x  f' kv x"
  shows "
    it' s (case_dres False False c) (λkv s. s  f kv) σ
     it' s (case_dres False False c) (λkv s. s  f' kv) σ"
  apply (rule proper_itE[OF PR[THEN proper_it'D[where s=s]]])
  apply (erule_tac t="it' s" in ssubst)
  apply (rule foldli_mono_dres[OF A])
  done

lemma proper_it_mono_dres_flat:
  assumes PR: "proper_it' it it'"
  assumes A: "kv x. flat_ge (f kv x) (f' kv x)"
  shows "
    flat_ge (it' s (case_dres False False c) (λkv s. s  f kv) σ)
      (it' s (case_dres False False c) (λkv s. s  f' kv) σ)"
  apply (rule proper_itE[OF PR[THEN proper_it'D[where s=s]]])
  apply (erule_tac t="it' s" in ssubst)
  apply (rule foldli_mono_dres_flat[OF A])
  done

lemma pi'_dom[icf_proper_iteratorI]: "proper_it' it it' 
   proper_it' (map_iterator_dom o it) (map_iterator_dom o it')"
  apply (rule proper_it'I)
  apply (simp add: comp_def)
  apply (rule icf_proper_iteratorI)
  apply (erule proper_it'D)
  done

lemma proper_it_mono_dres_dom:
  assumes PR: "proper_it' it it'"
  assumes A: "kv x. f kv x  f' kv x"
  shows "
    (map_iterator_dom o it') s (case_dres False False c) (λkv s. s  f kv) σ
     
    (map_iterator_dom o it') s (case_dres False False c) (λkv s. s  f' kv) σ"
  
  apply (rule proper_it_mono_dres)
  apply (rule icf_proper_iteratorI)
  by fact+

lemma proper_it_mono_dres_dom_flat:
  assumes PR: "proper_it' it it'"
  assumes A: "kv x. flat_ge (f kv x) (f' kv x)"
  shows "flat_ge 
    ((map_iterator_dom o it') s (case_dres False False c) (λkv s. s  f kv) σ)
    ((map_iterator_dom o it') s (case_dres False False c) (λkv s. s  f' kv) σ)"
  apply (rule proper_it_mono_dres_flat)
  apply (rule icf_proper_iteratorI)
  by fact+


(* TODO/FIXME: Hack! Mono-prover should be able to find proper-iterators itself
*)
lemmas proper_it_monos = 
  proper_it_mono_dres_pair proper_it_mono_dres_pair_flat
  proper_it_mono_dres proper_it_mono_dres_flat
  proper_it_mono_dres_dom proper_it_mono_dres_dom_flat

(* TODO: Conceptually, this leads to some kind of bundles: 
  Each bundle has a list of processors, that are invoked for every registered
  theorem. *)


attribute_setup "proper_it" = ‹
  Scan.succeed (Thm.declaration_attribute (fn thm => fn context => 
    let
      val mono_thms = map_filter (try (curry (RS) thm)) @{thms proper_it_monos}
      (*val mono_thms = map (fn mt => thm RS mt) @{thms proper_it_monos}*)
      val context = context 
        |> Icf_Proper_Iterator.add_thm thm
        |> fold Refine_Mono_Prover.add_mono_thm mono_thms
    in
      context
    end
  ))
  "Proper iterator declaration"

end

Theory Idx_Iterator

section ‹\isaheader{Iterator by get and size }›
theory Idx_Iterator
imports
  SetIterator
  Automatic_Refinement.Automatic_Refinement
begin

fun idx_iteratei_aux 
  :: "('s  nat  'a)  nat  nat  's  (bool)  ('a   )    "
where
  "idx_iteratei_aux get sz i l c f σ = (
    if i=0  ¬ c σ then σ
    else idx_iteratei_aux get sz (i - 1) l c f (f (get l (sz-i)) σ)
  )"

declare idx_iteratei_aux.simps[simp del]

lemma idx_iteratei_aux_simps[simp]:
  "i=0  idx_iteratei_aux get sz i l c f σ = σ"
  "¬c σ  idx_iteratei_aux get sz i l c f σ = σ"
  "i0; c σ  idx_iteratei_aux get sz i l c f σ = idx_iteratei_aux get sz (i - 1) l c f (f (get l (sz-i)) σ)"
  apply -
  apply (subst idx_iteratei_aux.simps, simp)+
  done

definition "idx_iteratei get sz l c f σ == idx_iteratei_aux get (sz l) (sz l) l c f σ"

lemma idx_iteratei_eq_foldli:
  assumes sz: "(sz, length)  arel  nat_rel"
  assumes get: "(get, (!))  arel  nat_rel  Id"
  assumes "(s,s')  arel"
  shows "(idx_iteratei get sz s, foldli s')  Id" 
proof-
  have size_correct: "s s'. (s,s')  arel  sz s = length s'"
      using sz[param_fo] by simp
  have get_correct: "s s' n. (s,s')  arel  get s n = s' ! n"
      using get[param_fo] by simp
  {
    fix n l
    assume A: "Suc n  length l"
    hence B: "length l - Suc n < length l" by simp
    from A have [simp]: "Suc (length l - Suc n) = length l - n" by simp
    from Cons_nth_drop_Suc[OF B, simplified] have 
      "drop (length l - Suc n) l = l!(length l - Suc n)#drop (length l - n) l" 
      by simp
  } note drop_aux=this

  {
    fix s s' c f σ i
    assume "(s,s')  arel" "isz s"
    hence "idx_iteratei_aux get (sz s) i s c f σ = foldli (drop (sz s - i) s') c f σ"
    proof (induct i arbitrary: σ)
      case 0 with size_correct[of s] show ?case by simp
    next
      case (Suc n)
      note S = Suc.prems(1)
      show ?case proof (cases "c σ")
        case False thus ?thesis by simp
      next
        case [simp, intro!]: True
        show ?thesis using Suc
            by (simp add: size_correct[OF S] get_correct[OF S] drop_aux)
      qed
    qed
  } note aux=this

  show ?thesis
    unfolding idx_iteratei_def[abs_def]
    by (simp, intro ext, simp add: aux[OF (s,s')  arel])
qed


text ‹Misc.›

lemma idx_iteratei_aux_nth_conv_foldli_drop:
  fixes xs :: "'b list"
  assumes "i  length xs"
  shows "idx_iteratei_aux (!) (length xs) i xs c f σ = foldli (drop (length xs - i) xs) c f σ"
using assms
proof(induct get"(!) :: 'b list  nat  'b" sz"length xs" i xs c f σ rule: idx_iteratei_aux.induct)
  case (1 i l c f σ)
  show ?case
  proof(cases "i = 0  ¬ c σ")
    case True thus ?thesis
      by(subst idx_iteratei_aux.simps)(auto)
  next
    case False
    hence i: "i > 0" and c: "c σ" by auto
    hence "idx_iteratei_aux (!) (length l) i l c f σ = idx_iteratei_aux (!) (length l) (i - 1) l c f (f (l ! (length l - i)) σ)"
      by(subst idx_iteratei_aux.simps) simp
    also have " = foldli (drop (length l - (i - 1)) l) c f (f (l ! (length l - i)) σ)"
      using i  length l i c by -(rule 1, auto)
    also from i  length l i
    have "drop (length l - i) l = (l ! (length l - i)) # drop (length l - (i - 1)) l"
      apply (subst Cons_nth_drop_Suc[symmetric])
      apply simp_all
      done
    hence "foldli (drop (length l - (i - 1)) l) c f (f (l ! (length l - i)) σ) = foldli (drop (length l - i) l) c f σ"
      using c by simp
    finally show ?thesis .
  qed
qed

lemma idx_iteratei_nth_length_conv_foldli: "idx_iteratei nth length = foldli"
by(rule ext)+(simp add: idx_iteratei_def idx_iteratei_aux_nth_conv_foldli_drop)
end

Theory Iterator

theory Iterator
imports 
  It_to_It 
  SetIteratorOperations 
  SetIteratorGA 
  Proper_Iterator
  Gen_Iterator
  Idx_Iterator
begin

  text ‹Folding over a list created by a proper iterator can be replaced
    by a single iteration›
  lemma proper_it_to_list_opt[refine_transfer_post_subst]:
    assumes PR: "proper_it' it it'"
    shows "foldli o it_to_list it  it'"
  proof (rule eq_reflection, intro ext)
    fix s c f σ
    
    obtain l where "it s = foldli l" and "it' s = foldli l"
      by (rule proper_itE[OF PR[THEN proper_it'D[where s=s]]])
    thus "(foldli o it_to_list it) s c f σ = it' s c f σ"
      by (simp add: comp_def it_to_list_def)
  qed

  lemma iterator_cnv_to_comp[refine_transfer_post_simp]:
    "foldli (it_to_list it x) = (foldli o it_to_list it) x"
    by auto

  declare idx_iteratei_eq_foldli[autoref_rules]

end

Theory RBT_add

(*  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{Additions to RB-Trees}›
theory RBT_add
imports 
  "HOL-Library.RBT_Impl" 
  "../Iterator/Iterator"
begin
text_raw ‹\label{thy:RBT_add}›

lemma tlt_trans: "l  u; uv  l  v"
  by (induct l) auto

lemma trt_trans: " uv; v«|r   u«|r"
  by (induct r) auto

lemmas tlt_trans' = tlt_trans[OF _ less_imp_le]
lemmas trt_trans' = trt_trans[OF less_imp_le]

primrec rm_iterateoi 
  :: "('k,'v) RBT_Impl.rbt  ('k × 'v, ) set_iterator"
  where
  "rm_iterateoi RBT_Impl.Empty c f σ = σ" |
  "rm_iterateoi (RBT_Impl.Branch col l k v r) c f σ = (
    if (c σ) then
      let σ' = rm_iterateoi l c f σ in
        if (c σ') then
          rm_iterateoi r c f (f (k, v) σ')
        else σ'
    else 
      σ
  )"

lemma rm_iterateoi_abort :
  "¬(c σ)  rm_iterateoi t c f σ = σ"
by (cases t) auto

lemma rm_iterateoi_alt_def :
  "rm_iterateoi RBT_Impl.Empty = set_iterator_emp"
  "rm_iterateoi (RBT_Impl.Branch col l k v r) = 
   set_iterator_union (rm_iterateoi l)
     (set_iterator_union (set_iterator_sng (k, v)) (rm_iterateoi r))"
by (simp_all add: fun_eq_iff set_iterator_emp_def rm_iterateoi_abort
                  set_iterator_union_def set_iterator_sng_def Let_def)
declare rm_iterateoi.simps[simp del]


primrec rm_reverse_iterateoi 
  :: "('k,'v) RBT_Impl.rbt  ('k × 'v, ) set_iterator"
  where
  "rm_reverse_iterateoi RBT_Impl.Empty c f σ = σ" |
  "rm_reverse_iterateoi (Branch col l k v r) c f σ = (
    if (c σ) then
      let σ' = rm_reverse_iterateoi r c f σ in
        if (c σ') then
          rm_reverse_iterateoi l c f (f (k, v) σ')
        else σ'
    else 
      σ
  )"

lemma rm_reverse_iterateoi_abort :
  "¬(c σ)  rm_reverse_iterateoi t c f σ = σ"
by (cases t) auto

lemma rm_reverse_iterateoi_alt_def :
  "rm_reverse_iterateoi RBT_Impl.Empty = set_iterator_emp"
  "rm_reverse_iterateoi (RBT_Impl.Branch col l k v r) = 
   set_iterator_union (rm_reverse_iterateoi r)
     (set_iterator_union (set_iterator_sng (k, v)) (rm_reverse_iterateoi l))"
by (simp_all add: fun_eq_iff set_iterator_emp_def rm_reverse_iterateoi_abort
                  set_iterator_union_def set_iterator_sng_def Let_def)
declare rm_reverse_iterateoi.simps[simp del]

(*
lemma finite_dom_lookup [simp, intro!]: "finite (dom (RBT.lookup t))"
by(simp add: RBT.lookup_def)


instantiation rbt :: ("{equal, linorder}", equal) equal begin

definition "equal_class.equal (r :: ('a, 'b) rbt) r' == RBT.impl_of r = RBT.impl_of r'"

instance
proof
qed (simp add: equal_rbt_def RBT.impl_of_inject)

end
*)

lemma (in linorder) map_to_set_lookup_entries: 
   "rbt_sorted t  map_to_set (rbt_lookup t) = set (RBT_Impl.entries t)"
  using map_of_entries[symmetric,of t]
  by (simp add: distinct_entries map_to_set_map_of)

lemma (in linorder) rm_iterateoi_correct:
  fixes t::"('a, 'v) RBT_Impl.rbt"
  assumes is_sort: "rbt_sorted t"
  defines "it  
  RBT_add.rm_iterateoi::(('a, 'v) RBT_Impl.rbt  ('a × 'v, ) set_iterator)"
  shows "map_iterator_linord (it t) (rbt_lookup t)"
  using is_sort
proof (induct t)
  case Empty
  show ?case unfolding it_def 
    by (simp add: rm_iterateoi_alt_def 
      map_iterator_linord_emp_correct rbt_lookup_Empty)
next
  case (Branch c l k v r)
  note is_sort_t = Branch(3)

  from Branch(1) is_sort_t have 
    l_it: "map_iterator_linord (it l) (rbt_lookup l)" by simp
  from Branch(2) is_sort_t have 
    r_it: "map_iterator_linord (it r) (rbt_lookup r)" by simp
  note kv_it = map_iterator_linord_sng_correct[of k v]

  have kv_r_it : "set_iterator_map_linord
     (set_iterator_union (set_iterator_sng (k, v)) (it r))
     (map_to_set [k  v]  map_to_set (rbt_lookup r))"
  proof (rule map_iterator_linord_union_correct [OF kv_it r_it])
    fix kv kv'
    assume pre: "kv  map_to_set [k  v]" "kv'  map_to_set (rbt_lookup r)"
    obtain k' v' where kv'_eq[simp]: "kv' = (k', v')" by (rule prod.exhaust)
 
    from pre is_sort_t show "fst kv < fst kv'" 
      apply (simp add: map_to_set_lookup_entries split: prod.splits)
      apply (metis entry_in_tree_keys rbt_greater_prop)
      done
  qed

  have l_kv_r_it : "set_iterator_map_linord (it (Branch c l k v r))
     (map_to_set (rbt_lookup l) 
       (map_to_set [k  v]  map_to_set (rbt_lookup r)))"
    unfolding it_def rm_iterateoi_alt_def
    unfolding it_def[symmetric]
  proof (rule map_iterator_linord_union_correct [OF l_it kv_r_it])
    fix kv1 kv2
    assume pre: "kv1  map_to_set (rbt_lookup l)" 
                "kv2  map_to_set [k  v]  map_to_set (rbt_lookup r)" 

    obtain k1 v1 where kv1_eq[simp]: "kv1 = (k1, v1)" by (rule prod.exhaust)
    obtain k2 v2 where kv2_eq[simp]: "kv2 = (k2, v2)" by (rule prod.exhaust)

    from pre is_sort_t show "fst kv1 < fst kv2" 
      apply (simp add: map_to_set_lookup_entries split: prod.splits)
      by (metis (lifting) map_of_entries neqE option.simps(3) 
        ord.rbt_lookup_rbt_greater ord.rbt_lookup_rbt_less rbt_greater_trans 
        rbt_less_trans weak_map_of_SomeI)
  qed
  
  from is_sort_t
  have map_eq: "map_to_set (rbt_lookup l) 
     (map_to_set [k  v]  map_to_set (rbt_lookup r)) =
        map_to_set (rbt_lookup (Branch c l k v r))" 
    by (simp add: set_eq_iff map_to_set_lookup_entries)
  
  from l_kv_r_it[unfolded map_eq]
  show ?case .
qed

lemma (in linorder) rm_reverse_iterateoi_correct:
  fixes t::"('a, 'v) RBT_Impl.rbt"
  assumes is_sort: "rbt_sorted t"
  defines "it  RBT_add.rm_reverse_iterateoi
    ::(('a, 'v) RBT_Impl.rbt  ('a × 'v, ) set_iterator)"
  shows "map_iterator_rev_linord (it t) (rbt_lookup t)"
  using is_sort
proof (induct t)
  case Empty
  show ?case unfolding it_def 
    by (simp add: rm_reverse_iterateoi_alt_def 
      map_iterator_rev_linord_emp_correct rbt_lookup_Empty)
next
  case (Branch c l k v r)
  note is_sort_t = Branch(3)

  from Branch(1) is_sort_t have 
    l_it: "map_iterator_rev_linord (it l) (rbt_lookup l)" by simp
  from Branch(2) is_sort_t have 
    r_it: "map_iterator_rev_linord (it r) (rbt_lookup r)" by simp
  note kv_it = map_iterator_rev_linord_sng_correct[of k v]

  have kv_l_it : "set_iterator_map_rev_linord
     (set_iterator_union (set_iterator_sng (k, v)) (it l))
     (map_to_set [k  v]  map_to_set (rbt_lookup l))"
  proof (rule map_iterator_rev_linord_union_correct [OF kv_it l_it])
    fix kv kv'
    assume pre: "kv  map_to_set [k  v]" "kv'  map_to_set (rbt_lookup l)"
    obtain k' v' where kv'_eq[simp]: "kv' = (k', v')" by (rule prod.exhaust)
 
    from pre is_sort_t show "fst kv > fst kv'" 
      apply (simp add: map_to_set_lookup_entries split: prod.splits)
      apply (metis entry_in_tree_keys rbt_less_prop)
   done
  qed

  have r_kv_l_it : "set_iterator_map_rev_linord (it (Branch c l k v r))
     (map_to_set (rbt_lookup r) 
       (map_to_set [k  v]  map_to_set (rbt_lookup l)))"
    unfolding it_def rm_reverse_iterateoi_alt_def
    unfolding it_def[symmetric]
  proof (rule map_iterator_rev_linord_union_correct [OF r_it kv_l_it])
    fix kv1 kv2
    assume pre: "kv1  map_to_set (rbt_lookup r)" 
                "kv2  map_to_set [k  v]  map_to_set (rbt_lookup l)" 

    obtain k1 v1 where kv1_eq[simp]: "kv1 = (k1, v1)" by (rule prod.exhaust)
    obtain k2 v2 where kv2_eq[simp]: "kv2 = (k2, v2)" by (rule prod.exhaust)

    from pre is_sort_t show "fst kv1 > fst kv2" 
      apply (simp add: map_to_set_lookup_entries split: prod.splits)
      by (metis (mono_tags) entry_in_tree_keys neq_iff option.simps(3) 
        ord.rbt_greater_prop ord.rbt_lookup_rbt_less rbt_less_trans 
        rbt_lookup_in_tree)
  qed
  
  from is_sort_t
  have map_eq: "map_to_set (rbt_lookup r) 
     (map_to_set [k  v]  map_to_set (rbt_lookup l)) =
        map_to_set (rbt_lookup (Branch c l k v r))" 
    by (auto simp add: set_eq_iff map_to_set_lookup_entries)

  from r_kv_l_it[unfolded map_eq]
  show ?case .
qed

lemma pi_rm[icf_proper_iteratorI]: 
  "proper_it (RBT_add.rm_iterateoi t) (RBT_add.rm_iterateoi t)"
  by (induct t) (simp_all add: rm_iterateoi_alt_def icf_proper_iteratorI)

lemma pi_rm_rev[icf_proper_iteratorI]: 
  "proper_it (RBT_add.rm_reverse_iterateoi t) (RBT_add.rm_reverse_iterateoi t)"
  by (induct t) (simp_all add: rm_reverse_iterateoi_alt_def 
    icf_proper_iteratorI)

primrec bheight_aux :: "('a,'b) RBT_Impl.rbt  nat  nat"
where
  "acc. bheight_aux RBT_Impl.Empty acc = acc"
| "acc. bheight_aux (RBT_Impl.Branch c lt k v rt) acc = 
     bheight_aux lt (case c of RBT_Impl.B  Suc acc | RBT_Impl.R  acc)"

lemma bheight_aux_eq: "bheight_aux t a = bheight t + a"
  by (induct t arbitrary: a) (auto split: RBT_Impl.color.split)

definition [code_unfold]: "rbt_bheight t  bheight_aux t 0"
lemma "rbt_bheight t = bheight t"
  unfolding rbt_bheight_def by (simp add: bheight_aux_eq)

(*definition "black_height t ≡ rbt_bheight (RBT.impl_of t)"*)

end

Theory Dlist_add

section ‹\isaheader{Additions to Distinct Lists}›
theory Dlist_add 
  imports 
  "HOL-Library.Dlist" 
  Automatic_Refinement.Misc
  "../Iterator/SetIteratorOperations" 
begin

primrec dlist_remove1' :: "'a  'a list  'a list  'a list"
where
  "dlist_remove1' x z [] = z"
| "dlist_remove1' x z (y # ys) 
  = (if x = y then z @ ys else dlist_remove1' x (y # z) ys)"

definition dlist_remove' :: "'a  'a dlist  'a dlist"
where "dlist_remove' a xs = Dlist (dlist_remove1' a [] (list_of_dlist xs))"

lemma distinct_remove1': "distinct (xs @ ys)  
  distinct (dlist_remove1' x xs ys)"
  by(induct ys arbitrary: xs) simp_all

lemma set_dlist_remove1': "distinct ys  
  set (dlist_remove1' x xs ys) = set xs  (set ys - {x})"
  by(induct ys arbitrary: xs) auto

lemma list_of_dlist_remove' [simp, code abstract]:
  "list_of_dlist (dlist_remove' a xs) = dlist_remove1' a [] (list_of_dlist xs)"
by(simp add: dlist_remove'_def distinct_remove1')

lemma dlist_remove'_correct: 
  "y  set (list_of_dlist (dlist_remove' x xs)) 
   (if x = y then False else y  set (list_of_dlist xs))"
  by(simp add: dlist_remove'_def 
    Dlist.member_def List.member_def set_dlist_remove1')

definition dlist_iteratei :: "'a dlist  ('a, 'b) set_iterator"
  where "dlist_iteratei xs = foldli (list_of_dlist xs)"

lemma dlist_iteratei_correct:
  "set_iterator (dlist_iteratei xs) (set (list_of_dlist xs))"
using distinct_list_of_dlist[of xs] 
      set_