Theory SetIteratorGA

(*  Title:       General Algorithms for Iterators
    Author:      Thomas Tuerk <tuerk@in.tum.de>
    Maintainer:  Thomas Tuerk <tuerk@in.tum.de>
*)
header {* General Algorithms for Iterators over Finite Sets *}
theory SetIteratorGA
imports Main SetIterator 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_by_rel 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 iterate_to_list_linord_correct :
fixes S0 :: "('a::{linorder}) 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 iterate_to_list_rev_linord_correct :
fixes S0 :: "('a::{linorder}) 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 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 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"])
  case (goal4 σ 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 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 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 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) 
    apply (metis order_refl)
  done
qed

lemma 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) 
    apply (metis order_refl)
  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_by_rel R (sort_fun l) ∧ multiset_of (sort_fun l) = multiset_of l"
    and it_OK: "set_iterator it S0"
shows "set_iterator_genord (iterator_to_ordered_iterator sort_fun it) S0 R"
proof -
  def 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_by_rel R (sort_fun l)"
    "set (sort_fun l) = S0" "distinct (sort_fun l)"
    apply (simp_all)
    apply (metis set_of_multiset_of)
    apply (metis distinct_count_atmost_1 set_of_multiset_of)
  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_by_rel_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_by_rel_mergesort_by_rel[OF lin trans_R])
done

end