(* 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
lemmas RTranCl1:
g' ∈ set (succs g) ==> g [succs]->* g'
lemmas RTranCl1:
g' ∈ set (succs g) ==> g [succs]->* g'
lemmas RTranCl_elim:
[| h [succs]->* h'; h' = h ==> P; !!g'. [| g' ∈ set (succs h); g' [succs]->* h' |] ==> P |] ==> P
lemma RTranCl_induct:
[| h [succs]->* h'; P h; !!g g'. [| g' ∈ set (succs g); P g |] ==> P g' |] ==> P h'
lemma invariantE:
[| invariant P succs; g' ∈ set (succs g); P g |] ==> P g'
lemma inv_subset:
[| invariant P f; !!g. P g ==> set (f' g) ⊆ set (f g) |] ==> invariant P f'
lemma inv_RTranCl_subset:
[| invariant P succs; !!g. P g ==> g [succs]->* f g |] ==> invariant P (λg. [f g])
lemma inv_comp_map:
[| invariant P succs; !!g. P g ==> P (f g) |] ==> invariant P (map f o succs)
lemma RTranCl_inv:
[| invariant P succs; g [succs]->* g'; P g |] ==> P g'
lemma RTranCl_subset:
[| !!g. set (f g) ⊆ set (h g); s [f]->* g |] ==> s [h]->* g
lemma RTranCl_subset2:
[| s [f]->* g; !!g. s [f]->* g ==> set (f g) ⊆ set (h g) |] ==> s [h]->* g
lemma RTranCl_rev_succs:
[| g [succs]->* g'; g'' ∈ set (succs g') |] ==> g [succs]->* g''
lemma RTranCl_compose:
[| g [succs]->* g'; g' [succs]->* g'' |] ==> g [succs]->* g''
lemma RTranCl_map_comp_subset:
[| invariant P succs; !!g. P g ==> g [succs]->* f g; s [map f o succs]->* g; P s |] ==> s [succs]->* g