Theory Rtrancl_On

(* Title:  Rtrancl_On.thy
   Author: Lars Noschinski, TU München
   Author: René Neumann, TU München
*)

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