Theory Rtrancl_On
theory Rtrancl_On
imports Main
begin
section ‹Reflexive-Transitive Closure on a Domain›
text ‹
In this section we introduce a variant of the reflexive-transitive closure
of a relation which is useful to formalize the reachability relation on
digraphs.
›
inductive_set
rtrancl_on :: "'a set ⇒ 'a rel ⇒ 'a rel"
for F :: "'a set" and r :: "'a rel"
where
rtrancl_on_refl [intro!, Pure.intro!, simp]: "a ∈ F ⟹ (a, a) ∈ rtrancl_on F r"
| rtrancl_on_into_rtrancl_on [Pure.intro]:
"(a, b) ∈ rtrancl_on F r ⟹ (b, c) ∈ r ⟹ c ∈ F
⟹ (a, c) ∈ rtrancl_on F r"
definition symcl :: "'a rel ⇒ 'a rel" (‹(_⇧s)› [1000] 999) where
"symcl R = R ∪ (λ(a,b). (b,a)) ` R"
lemma in_rtrancl_on_in_F:
assumes "(a,b) ∈ rtrancl_on F r" shows "a ∈ F" "b ∈ F"
using assms by induct auto
lemma rtrancl_on_induct[consumes 1, case_names base step, induct set: rtrancl_on]:
assumes "(a, b) ∈ rtrancl_on F r"
and "a ∈ F ⟹ P a"
"⋀y z. ⟦(a, y) ∈ rtrancl_on F r; (y,z) ∈ r; y ∈ F; z ∈ F; P y⟧ ⟹ P z"
shows "P b"
using assms by (induct a b) (auto dest: in_rtrancl_on_in_F)
lemma rtrancl_on_trans:
assumes "(a,b) ∈ rtrancl_on F r" "(b,c) ∈ rtrancl_on F r" shows "(a,c) ∈ rtrancl_on F r"
using assms(2,1)
by induct (auto intro: rtrancl_on_into_rtrancl_on)
lemma converse_rtrancl_on_into_rtrancl_on:
assumes "(a,b) ∈ r" "(b, c) ∈ rtrancl_on F r" "a ∈ F"
shows "(a, c) ∈ rtrancl_on F r"
proof -
have "b ∈ F" using ‹(b,c) ∈ _› by (rule in_rtrancl_on_in_F)
show ?thesis
apply (rule rtrancl_on_trans)
apply (rule rtrancl_on_into_rtrancl_on)
apply (rule rtrancl_on_refl)
by fact+
qed
lemma rtrancl_on_converseI:
assumes "(y, x) ∈ rtrancl_on F r" shows "(x, y) ∈ rtrancl_on F (r¯)"
using assms
proof induct
case (step a b)
then have "(b,b) ∈ rtrancl_on F (r¯)" "(b,a) ∈ r¯" by auto
then show ?case using step
by (metis rtrancl_on_trans rtrancl_on_into_rtrancl_on)
qed auto
theorem rtrancl_on_converseD:
assumes "(y, x) ∈ rtrancl_on F (r¯)" shows "(x, y) ∈ rtrancl_on F r"
using assms by - (drule rtrancl_on_converseI, simp)
lemma converse_rtrancl_on_induct[consumes 1, case_names base step, induct set: rtrancl_on]:
assumes major: "(a, b) ∈ rtrancl_on F r"
and cases: "b ∈ F ⟹ P b"
"⋀x y. ⟦(x,y) ∈ r; (y,b) ∈ rtrancl_on F r; x ∈ F; y ∈ F; P y⟧ ⟹ P x"
shows "P a"
using rtrancl_on_converseI[OF major] cases
by induct (auto intro: rtrancl_on_converseD)
lemma converse_rtrancl_on_cases:
assumes "(a, b) ∈ rtrancl_on F r"
obtains (base) "a = b" "b ∈ F"
| (step) c where "(a,c) ∈ r" "(c,b) ∈ rtrancl_on F r"
using assms by induct auto
lemma rtrancl_on_sym:
assumes "sym r" shows "sym (rtrancl_on F r)"
using assms by (auto simp: sym_conv_converse_eq intro: symI dest: rtrancl_on_converseI)
lemma rtrancl_on_mono:
assumes "s ⊆ r" "F ⊆ G" "(a,b) ∈ rtrancl_on F s" shows "(a,b) ∈ rtrancl_on G r"
using assms(3,1,2)
proof induct
case (step x y) show ?case
using step assms by (intro converse_rtrancl_on_into_rtrancl_on[OF _ step(5)]) auto
qed auto
lemma rtrancl_consistent_rtrancl_on:
assumes "(a,b) ∈ r⇧*"
and "a ∈ F" "b ∈ F"
and consistent: "⋀a b. ⟦ a ∈ F; (a,b) ∈ r ⟧ ⟹ b ∈ F"
shows "(a,b) ∈ rtrancl_on F r"
using assms(1-3)
proof (induction rule: converse_rtrancl_induct)
case (step y z) then have "z ∈ F" by (rule_tac consistent) simp
with step have "(z,b) ∈ rtrancl_on F r" by simp
with step.prems ‹(y,z) ∈ r› ‹z ∈ F› show ?case
using converse_rtrancl_on_into_rtrancl_on
by metis
qed simp
lemma rtrancl_on_rtranclI:
"(a,b) ∈ rtrancl_on F r ⟹ (a,b) ∈ r⇧*"
by (induct rule: rtrancl_on_induct) simp_all
lemma rtrancl_on_sub_rtrancl:
"rtrancl_on F r ⊆ r^*"
using rtrancl_on_rtranclI
by auto
end