Theory RTranCl

(*  Author:  Gertrud Bauer, Tobias Nipkow  *)

header {* 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