Theory RTranCl

(*  ID:         $Id: RTranCl.thy,v 1.1 2006/01/04 13:44:04 nipkow Exp $
    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)}*"}. *}

consts RTranCl :: "('a => 'a list) => ('a * 'a) set"
syntax "in_set" :: "'a => ('a => 'a list) => 'a => bool"
      ("_ [_]-> _" [55,0,55] 50)
translations "g [succs]-> g'" => "g' ∈ set (succs g)"
syntax "in_RTranCl" :: "'a => ('a => 'a list) => 'a => bool"
       ("_ [_]->* _" [55,0,55] 50)
translations "g [succs]->* g'" == "(g,g') ∈ RTranCl succs"

inductive "RTranCl succs"
intros
  refl: "g [succs]->* g"
  succs: "g [succs]-> g' ==> g' [succs]->* g'' ==> g [succs]->* g''"

lemmas RTranCl1 = RTranCl.succs[OF _ RTranCl.refl]

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 "P g" "g' ∈ set(succs g)" "(g', g'') ∈ RTranCl succs" 
      and IH: "P g' ==> P g''"
    have "P g'" by (rule s)
    then show "P g''" by (rule IH)
  qed
qed

constdefs
 invariant :: "('a => bool) => ('a => 'a list) => bool"
"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 inv_RTranCl_subset:
assumes inv: "invariant P succs" and f: "(!!g. P g ==> (g,f g) ∈ RTranCl succs)"
shows "invariant P (%g. [f g])"
proof(clarsimp simp:invariant_def)
  fix g assume "P g"
  from f[OF `P g`] show "P(f g)"
    by induct (auto intro!: `P g` elim!: invariantE[OF inv])
qed

lemma inv_comp_map:
 "invariant P succs ==> (!!g. P g ==> P(f g)) ==> invariant P (map f o succs)"
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_subset: "(!!g. set(f g) ⊆ set(h g)) ==>
  (s,g) : RTranCl f ==> (s,g) : RTranCl h"
apply(erule RTranCl.induct)
apply(rule RTranCl.intros)
apply(blast intro: RTranCl.intros)
done

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

lemma RTranCl_rev_succs: 
 "(g, g') ∈ RTranCl succs ==> g'' ∈ set (succs g') ==> (g, g'') ∈ RTranCl succs"
proof (induct rule: RTranCl.induct)
  fix g assume "g'' ∈ set (succs g)" 
  moreover have "(g'', g'') ∈ RTranCl succs" by (rule RTranCl.refl)
  ultimately show "(g, g'') ∈ RTranCl succs" by (rule RTranCl.succs)
next
  fix g h' h'' assume "h' ∈ set (succs g)" 
  moreover assume "(h', h'') ∈ RTranCl succs" and "g'' ∈ set (succs h'')"
   and IH: "g'' ∈ set (succs h'') ==> (h', g'') ∈ RTranCl succs"
  have "(h', g'') ∈ RTranCl succs" by (rule IH)
  ultimately show "(g, g'') ∈ RTranCl succs" by (rule RTranCl.succs)
qed

lemma RTranCl_compose:
assumes "(g,g') ∈ RTranCl succs"
shows "(g',g'') ∈ RTranCl succs ==> (g,g'') ∈ RTranCl succs"
using prems(1)
proof (induct rule: RTranCl_induct)
  case refl show ?case by assumption
next
  case succs thus ?case by(blast intro:RTranCl.succs)
qed


lemma RTranCl_map_comp_subset:
assumes inv: "invariant P succs"
and f: "(!!g. P g ==> (g,f g) ∈ RTranCl succs)"
and a: "(s,g) ∈ RTranCl (map f o succs)"
shows "P s ==> (s,g) ∈ RTranCl succs"
using a
proof(induct rule: RTranCl_induct)
  case refl thus ?case by(fast intro: RTranCl.refl)
next
  case (succs g g')
  then obtain g'' where "g'' ∈ set(succs g)"  "g' = f g''" by auto
  moreover then have "P g''"
    using RTranCl_inv[OF inv, OF succs(2)] succs(3) inv by(simp add:invariant_def)
  ultimately show ?case by(blast intro:RTranCl_compose RTranCl.succs f succs(2-3))
qed


end