header {* \isaheader{More Generic Algorithms} *}
theory Algos
imports
"../spec/SetSpec"
"../spec/MapSpec"
"../spec/ListSpec"
begin
text_raw {*\label{thy:Algos}*}
subsection "Injective Map to Naturals"
text "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
text "Compute an injective map from objects into an initial
segment of the natural numbers"
locale map_to_nat_loc =
s!: StdSet s_ops +
m!: StdMap m_ops
for s_ops :: "('x,'s,'more1) set_ops_scheme"
and m_ops :: "('x,nat,'m,'more2) map_ops_scheme"
begin
definition map_to_nat
:: "'s => 'm" where
"map_to_nat s ==
snd (s.iterate s (λx (c,m). (c+1,m.update x c m)) (0,m.empty ()))"
lemma map_to_nat_correct:
assumes INV[simp]: "s.invar s"
shows
-- "All elements have got a number"
"dom (m.α (map_to_nat s)) = s.α s" (is ?T1) and
-- "No two elements got the same number"
[rule_format]: "inj_on (m.α (map_to_nat s)) (s.α s)" (is ?T2) and
-- "Numbering is inatseg"
[rule_format]: "inatseg (ran (m.α (map_to_nat s)))" (is ?T3) and
-- "The result satisfies the map invariant"
"m.invar (map_to_nat s)" (is ?T4)
proof -
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 map_to_nat_def)
apply (rule_tac I="λit (c,m).
m.invar m ∧
dom (m.α m) = s.α s - it ∧
inj_on (m.α m) (s.α s - it) ∧
(ran (m.α m) = {i. i<c})
" in s.iterate_rule_P)
apply simp
apply (simp add: m.empty_correct)
apply (case_tac σ)
apply (simp add: m.empty_correct m.update_correct)
apply (intro conjI)
apply blast
apply clarify
apply (rule_tac m="m.α ba" and
k=x and v=aa and
S'="(s.α s - (it - {x}))" and
S="(s.α 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
end
subsection "Map from Set"
text "Build a map using a set of keys and a function to compute the values."
locale it_dom_fun_to_map_loc =
s!: StdSet s_ops
+ m!: StdMap m_ops
for s_ops :: "('k,'s,'more1) set_ops_scheme"
and m_ops :: "('k,'v,'m,'more2) map_ops_scheme"
begin
definition it_dom_fun_to_map ::
"'s => ('k => 'v) => 'm"
where "it_dom_fun_to_map s f ==
s.iterate s (λk m. m.update_dj k (f k) m) (m.empty ())"
lemma it_dom_fun_to_map_correct:
assumes INV: "s.invar s"
shows "m.α (it_dom_fun_to_map s f) k
= (if k ∈ s.α s then Some (f k) else None)" (is ?G1)
and "m.invar (it_dom_fun_to_map s f)" (is ?G2)
proof -
have "m.α (it_dom_fun_to_map s f) k
= (if k ∈ s.α s then Some (f k) else None) ∧
m.invar (it_dom_fun_to_map s f)"
unfolding it_dom_fun_to_map_def
apply (rule s.iterate_rule_P[where
I = "λit res. m.invar res
∧ (∀k. m.α res k = (if (k ∈ (s.α s) - it) then Some (f k) else None))"
])
apply (simp add: INV)
apply (simp add: m.empty_correct)
apply (subgoal_tac "x∉dom (m.α σ)")
apply (auto simp: INV m.empty_correct m.update_dj_correct) []
apply auto [2]
done
thus ?G1 and ?G2
by auto
qed
end
locale set_to_list_defs_loc =
s!: StdSetDefs s_ops
+ l!: StdListDefs l_ops
for s_ops :: "('x,'s,'more1) set_ops_scheme"
and l_ops :: "('x,'l,'more2) list_ops_scheme"
begin
definition "g_set_to_listl s ≡ s.iterate s l.appendl (l.empty ())"
definition "g_set_to_listr s ≡ s.iterate s l.appendr (l.empty ())"
end
locale set_to_list_loc = set_to_list_defs_loc s_ops l_ops
+ s!: StdSet s_ops
+ l!: StdList l_ops
for s_ops :: "('x,'s,'more1) set_ops_scheme"
and l_ops :: "('x,'l,'more2) list_ops_scheme"
begin
lemma g_set_to_listl_correct:
assumes I: "s.invar s"
shows "List.set (l.α (g_set_to_listl s)) = s.α s"
and "l.invar (g_set_to_listl s)"
and "distinct (l.α (g_set_to_listl s))"
using I apply -
unfolding g_set_to_listl_def
apply (rule_tac I="λit σ. l.invar σ ∧ List.set (l.α σ) = it
∧ distinct (l.α σ)"
in s.iterate_rule_insert_P, auto simp: l.correct)+
done
lemma g_set_to_listr_correct:
assumes I: "s.invar s"
shows "List.set (l.α (g_set_to_listr s)) = s.α s"
and "l.invar (g_set_to_listr s)"
and "distinct (l.α (g_set_to_listr s))"
using I apply -
unfolding g_set_to_listr_def
apply (rule_tac I="λit σ. l.invar σ ∧ List.set (l.α σ) = it
∧ distinct (l.α σ)"
in s.iterate_rule_insert_P, auto simp: l.correct)+
done
end
end