Quelle  RTranCl.thy

(*  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
  of type @{typ"'a ==> 'a list"}. Instead of defining the closure
  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