Theory RTranCl

(*  Author:  Gertrud Bauer, Tobias Nipkow  *)

section ‹Transitive Closure of Successor List Function›

theory RTranCl
imports Main
begin

text‹The reflexive transitive closure of a relation induced by a
function of type @{typ"'a ⇒ 'a list"}. Instead of defining the closure
again it would have been simpler to take @{term"{(x,y) . y ∈ set(f x)}⇧*"}.›

abbreviation (input)
  in_set :: "'a ⇒ ('a ⇒ 'b list) ⇒ 'b ⇒ bool" (‹_ [_]→ _› [55,0,55] 50) where
  "g [succs]→ g' == g' ∈ set (succs g)"

inductive_set
  RTranCl :: "('a ⇒ 'a list) ⇒ ('a * 'a) set"
  and in_RTranCl :: "'a ⇒ ('a ⇒ 'a list) ⇒ 'a ⇒ bool"
    (‹_ [_]→* _› [55,0,55] 50)
  for succs :: "'a ⇒ 'a list"
where
  "g [succs]→* g' ≡ (g,g') ∈ RTranCl succs"
| refl: "g [succs]→* g"
| succs: "g [succs]→ g' ⟹ g' [succs]→* g'' ⟹ g [succs]→* g''"

inductive_cases RTranCl_elim: "(h,h') : RTranCl succs"

lemma RTranCl_induct(*<*) [induct set: RTranCl, consumes 1, case_names refl succs] (*>*):
 "(h, h') ∈ RTranCl succs ⟹ 
  P h ⟹ 
  (⋀g g'. g' ∈ set (succs g) ⟹ P g ⟹ P g') ⟹ 
  P h'"
proof -
  assume s: "⋀g g'. g' ∈ set (succs g) ⟹ P g ⟹ P g'"
  assume "(h, h') ∈ RTranCl succs" "P h"
  then show "P h'"
  proof (induct rule: RTranCl.induct)
    fix g assume "P g" then show "P g" . 
  next
    fix g g' g''
    assume IH: "P g' ⟹ P g''"
    assume "g' ∈ set(succs g)" "P g"
    then have "P g'" by (rule s)
    then show "P g''" by (rule IH)
  qed
qed

definition invariant :: "('a ⇒ bool) ⇒ ('a ⇒ 'a list) ⇒ bool" where
"invariant P succs ≡ ∀g g'. g' ∈ set(succs g) ⟶ P g ⟶ P g'"

lemma invariantE:
  "invariant P succs  ⟹ g [succs]→ g' ⟹ P g ⟹ P g'"
by(simp add:invariant_def)

lemma inv_subset:
 "invariant P f ⟹ (⋀g. P g ⟹ set(f' g) ⊆ set(f g)) ⟹ invariant P f'"
by(auto simp:invariant_def)

lemma RTranCl_inv:
  "invariant P succs ⟹ (g,g') ∈ RTranCl succs ⟹ P g ⟹ P g'"
by (erule RTranCl_induct)(auto simp:invariant_def)

lemma RTranCl_subset2:
assumes a: "(s,g) : RTranCl f"
shows "(⋀g. (s,g) ∈ RTranCl f ⟹ set(f g) ⊆ set(h g)) ⟹ (s,g) : RTranCl h"
using a
proof (induct rule: RTranCl.induct)
  case refl show ?case by(rule RTranCl.intros)
next
  case succs thus ?case by(blast intro: RTranCl.intros)
qed

end