header {* \isaheader{More Generic Algorithms} *}
theory Algos
imports
"../common/Misc"
"../spec/SetSpec"
"../spec/MapSpec"
"../spec/ListSpec"
begin
text_raw {*\label{thy:Algos}*}
subsection "Injective Map to Naturals"
-- "Compute an injective map from objects into an initial
segment of the natural numbers"
definition map_to_nat
:: "('s => ('x,nat × 'm) set_iterator) =>
(unit => 'm) => ('x => nat => 'm => 'm) =>
's => 'm" where
"map_to_nat iterate1 empty2 update2 s ==
snd (iterate1 s (λ_. True) (λx (c,m). (c+1,update2 x c m)) (0,empty2 ()))"
-- "Whether a set is an initial segment of the natural numbers"
definition inatseg :: "nat set => bool"
where "inatseg s == ∃k. s = {i::nat. i<k}"
lemma inatseg_simps[simp]:
"inatseg {}"
"inatseg {0}"
by (unfold inatseg_def)
auto
lemma map_to_nat_correct:
fixes α1 :: "'s => 'x set"
fixes α2 :: "'m => 'x \<rightharpoonup> nat"
assumes "set_iteratei α1 invar1 iterate1"
assumes "map_empty α2 invar2 empty2"
assumes "map_update α2 invar2 update2"
assumes INV[simp]: "invar1 s"
defines "nm == map_to_nat iterate1 empty2 update2 s"
shows
-- "All elements have got a number"
"dom (α2 nm) = α1 s" (is ?T1) and
-- "No two elements got the same number"
[rule_format]: "inj_on (α2 nm) (α1 s)" (is ?T2) and
-- "Numbering is inatseg"
[rule_format]: "inatseg (ran (α2 nm))" (is ?T3) and
-- "The result satisfies the map invariant"
"invar2 nm" (is ?T4)
proof -
interpret s1: set_iteratei α1 invar1 iterate1 by fact
interpret m2: map_empty α2 invar2 empty2 by fact
interpret m2: map_update α2 invar2 update2 by fact
have i_aux: "!!m S S' k v. [|inj_on m S; S' = insert k S; v∉ran m|]
==> inj_on (m(k\<mapsto>v)) S'"
apply (rule inj_onI)
apply (simp split: split_if_asm)
apply (simp add: ran_def)
apply (simp add: ran_def)
apply blast
apply (blast dest: inj_onD)
done
have "?T1 ∧ ?T2 ∧ ?T3 ∧ ?T4"
apply (unfold nm_def map_to_nat_def)
apply (rule_tac I="λit (c,m).
invar2 m ∧
dom (α2 m) = α1 s - it ∧
inj_on (α2 m) (α1 s - it) ∧
(ran (α2 m) = {i. i<c})
" in s1.iterate_rule_P)
apply simp
apply (simp add: m2.empty_correct)
apply (case_tac σ)
apply (simp add: m2.empty_correct m2.update_correct)
apply (intro conjI)
apply blast
apply clarify
apply (rule_tac m="α2 ba" and
k=x and v=aa and
S'="(α1 s - (it - {x}))" and
S="(α1 s - it)"
in i_aux)
apply auto [3]
apply auto [1]
apply (case_tac σ)
apply (auto simp add: inatseg_def)
done
thus ?T1 ?T2 ?T3 ?T4 by auto
qed
subsection "Set to List(-interface)"
subsubsection "Converting Set to List by Enqueue"
definition it_set_to_List_enq :: "('s => ('a,'f) set_iterator) =>
(unit => 'f) => ('a=>'f=>'f) => 's => 'f"
where "it_set_to_List_enq iterate emp enq S == iterate S (λ_. True) (λx F. enq x F) (emp ())"
lemma it_set_to_List_enq_correct:
assumes "set_iteratei α invar iterate"
assumes "list_empty αl invarl emp"
assumes "list_enqueue αl invarl enq"
assumes [simp]: "invar S"
shows
"set (αl (it_set_to_List_enq iterate emp enq S)) = α S" (is ?T1)
"invarl (it_set_to_List_enq iterate emp enq S)" (is ?T2)
"distinct (αl (it_set_to_List_enq iterate emp enq S))" (is ?T3)
proof -
interpret set_iteratei α invar iterate by fact
interpret list_empty αl invarl emp by fact
interpret list_enqueue αl invarl enq by fact
have "?T1 ∧ ?T2 ∧ ?T3"
apply (unfold it_set_to_List_enq_def)
apply (rule_tac
I="λit F. set (αl F) = α S - it ∧ invarl F ∧ distinct (αl F)"
in iterate_rule_P)
apply (auto simp add: enqueue_correct empty_correct)
done
thus ?T1 ?T2 ?T3 by auto
qed
subsubsection "Converting Set to List by Push"
definition it_set_to_List_push :: "('s => ('a,'f) set_iterator) =>
(unit => 'f) => ('a=>'f=>'f) => 's => 'f"
where "it_set_to_List_push iterate emp push S == iterate S (λ_. True) (λx F. push x F) (emp ())"
lemma it_set_to_List_push_correct:
assumes "set_iteratei α invar iterate"
assumes "list_empty αl invarl emp"
assumes "list_push αl invarl push"
assumes [simp]: "invar S"
shows
"set (αl (it_set_to_List_push iterate emp push S)) = α S" (is ?T1)
"invarl (it_set_to_List_push iterate emp push S)" (is ?T2)
"distinct (αl (it_set_to_List_push iterate emp push S))" (is ?T3)
proof -
interpret set_iteratei α invar iterate by fact
interpret list_empty αl invarl emp by fact
interpret list_push αl invarl push by fact
have "?T1 ∧ ?T2 ∧ ?T3"
apply (unfold it_set_to_List_push_def)
apply (rule_tac
I="λit F. set (αl F) = α S - it ∧ invarl F ∧ distinct (αl F)"
in iterate_rule_P)
apply (auto simp add: push_correct empty_correct)
done
thus ?T1 ?T2 ?T3 by auto
qed
subsection "Map from Set"
-- "Build a map using a set of keys and a function to compute the values."
definition it_dom_fun_to_map ::
"('s => ('k,'m) set_iterator) =>
('k => 'v => 'm => 'm) => (unit => 'm) => 's => ('k => 'v) => 'm"
where "it_dom_fun_to_map s_it up_dj emp s f ==
s_it s (λ_. True) (λk m. up_dj k (f k) m) (emp ())"
lemma it_dom_fun_to_map_correct:
fixes α1 :: "'m => 'k => 'v option"
fixes α2 :: "'s => 'k set"
assumes s_it: "set_iteratei α2 invar2 s_it"
assumes m_up: "map_update_dj α1 invar1 up_dj"
assumes m_emp: "map_empty α1 invar1 emp"
assumes INV: "invar2 s"
shows "α1 (it_dom_fun_to_map s_it up_dj emp s f) k = (if k ∈ α2 s then Some (f k) else None)"
and "invar1 (it_dom_fun_to_map s_it up_dj emp s f)"
proof -
interpret s_it: set_iteratei α2 invar2 s_it using s_it .
interpret m: map_update_dj α1 invar1 up_dj using m_up .
interpret m: map_empty α1 invar1 emp using m_emp .
have "α1 (it_dom_fun_to_map s_it up_dj emp s f) k = (if k ∈ α2 s then Some (f k) else None) ∧
invar1 (it_dom_fun_to_map s_it up_dj emp s f)"
unfolding it_dom_fun_to_map_def
apply (rule s_it.iterate_rule_P[where
I = "λit res. invar1 res ∧ (∀k. α1 res k = (if (k ∈ (α2 s) - it) then Some (f k) else None))"
])
apply (simp add: INV)
apply (simp add: m.empty_correct)
apply (subgoal_tac "x∉dom (α1 σ)")
apply (auto simp: INV m.empty_correct m.update_dj_correct) []
apply auto
done
thus "α1 (it_dom_fun_to_map s_it up_dj emp s f) k = (if k ∈ α2 s then Some (f k) else None)"
and "invar1 (it_dom_fun_to_map s_it up_dj emp s f)"
by auto
qed
end