(* 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