theory RTrancl2
imports
"Transitive-Closure-II.RTrancl"
"Collections.RBTSetImpl"
begin
subsection ‹Instantiation using list operations›
text ‹It follows an implementation based on lists.
Here, the working list algorithm is implemented outside the locale so that
it can be used for code generation. In general, it is not terminating,
therefore we use partial\_function instead of function.›
partial_function(tailrec) mk_rtrancl_set_main where
[code]: "mk_rtrancl_set_main r todo fin = (case todo of [] ⇒ fin
| Cons a tod ⇒
(if rs.memb a fin then mk_rtrancl_set_main r tod fin
else mk_rtrancl_set_main r (r a @ tod) (rs.ins_dj a fin)))"
definition mk_rtrancl_set where
"mk_rtrancl_set r init ≡ mk_rtrancl_set_main r init (rs.empty ())"
locale subsumption_set =
fixes r :: "'a ⇒ 'a list"
sublocale subsumption_set ⊆ subsumption r "op =" set
by (unfold_locales, auto)
locale relation_subsumption_set = subsumption_set r for r :: "'a :: linorder ⇒ 'a list" +
assumes rtrancl_fin: "⋀ a. finite {b. (a,b) ∈ { (a,b) . b ∈ set (r a)}^*}"
abbreviation(input) sel_list where "sel_list x ≡ case x of Cons h t ⇒ (h,t)"
sublocale subsumption_set ⊆ subsumption_impl r "op =" set sel_list append length
proof(unfold_locales, rule finite_set)
fix b a c
assume "set b ≠ {}" and "sel_list b = (a,c)"
thus "set b = insert a (set c) ∧ length c < length b"
by (cases b, auto)
qed auto
sublocale relation_subsumption_set ⊆ relation_subsumption_impl r "op =" set sel_list append length
by (unfold_locales, rule rtrancl_fin)
context relation_subsumption_set
begin
text ‹The main equivalence proof between the generic work list algorithm
and the one operating on sets›
lemma mk_rtrancl_set_main: "rs.α fins = fin ⟹ rs.α (mk_rtrancl_set_main r todo fins) = mk_rtrancl_main todo fin"
proof (induct todo fin arbitrary: fins rule: mk_rtrancl_main.induct)
case (1 todo fin fins)
note simp = mk_rtrancl_set_main.simps[of _ todo fins] mk_rtrancl_main.simps[of todo fin]
show ?case (is "?l = ?r")
proof (cases todo)
case Nil
show ?thesis unfolding simp unfolding Nil using 1(3) by simp
next
case (Cons a tod)
show ?thesis
proof (cases "a ∈ fin")
case True
from True have l: "?l = rs.α (mk_rtrancl_set_main r tod fins)"
unfolding simp unfolding Cons using 1(3) by (simp add: rs.correct)
from True have r: "?r = mk_rtrancl_main tod fin"
unfolding simp unfolding Cons by auto
show ?thesis unfolding l r
by (rule 1(1), insert 1(2,3) Cons True, auto)
next
case False
from False have l: "?l = rs.α (mk_rtrancl_set_main r (r a @ tod) (rs.ins_dj a fins))"
unfolding simp unfolding Cons using 1(3) by (simp add: rs.correct)
from False have r: "?r = mk_rtrancl_main (r a @ tod) (insert a fin)"
unfolding simp unfolding Cons by auto
show ?thesis unfolding l r
by (rule 1(2), insert False Cons 1(3), auto simp: rs.correct)
qed
qed
qed
lemma mk_rtrancl_set: "rs.α (mk_rtrancl_set r init) = mk_rtrancl init"
unfolding mk_rtrancl_set_def mk_rtrancl_def
by (rule mk_rtrancl_set_main, simp add: rs.correct)
end
end