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 = (∀x∈S0. P x)"
unfolding iterate_ball_def
apply (rule set_iterator_rule_P [OF it,
            where I = "λS σ. σ = (∀x∈S0-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 = (∃x∈S0. P x)"
unfolding iterate_bex_def
apply (rule set_iterator_rule_P [OF it, where I = "λS σ. σ = (∃x∈S0-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 ⟷ (∀x∈S0. (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 ⟷ (∀x∈S0. (f x = None))"
    unfolding iterate_sel_def
    apply (rule_tac set_iterator_genord.iteratei_rule_insert_P [OF it_OK, 
       where I = "λS σ. (σ = None) ⟷ (∀x∈S. (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) ⟷ (∀x∈S. 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 ⟷ (∀x∈S0. ¬(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 ⟷ (∀x∈S0. ¬(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 ⟷ (∀x∈S0. ¬(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 ⟷ (∀x∈S0. ¬(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 ⟷ (∀x∈S0. ¬(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 ⟷ (∀x∈S0. ¬(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 ⟷ (∀x∈S0. ¬(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