header {* 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_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 (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"])
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 (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_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