# Theory Trancl

Up to index of Isabelle/ZF

theory Trancl
imports Fixedpt Perm
`(*  Title:      ZF/Trancl.thy    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory    Copyright   1992  University of Cambridge*)header{*Relations: Their General Properties and Transitive Closure*}theory Trancl imports Fixedpt Perm begindefinition  refl     :: "[i,i]=>o"  where    "refl(A,r) == (∀x∈A. <x,x> ∈ r)"definition  irrefl   :: "[i,i]=>o"  where    "irrefl(A,r) == ∀x∈A. <x,x> ∉ r"definition  sym      :: "i=>o"  where    "sym(r) == ∀x y. <x,y>: r --> <y,x>: r"definition  asym     :: "i=>o"  where    "asym(r) == ∀x y. <x,y>:r --> ~ <y,x>:r"definition  antisym  :: "i=>o"  where    "antisym(r) == ∀x y.<x,y>:r --> <y,x>:r --> x=y"definition  trans    :: "i=>o"  where    "trans(r) == ∀x y z. <x,y>: r --> <y,z>: r --> <x,z>: r"definition  trans_on :: "[i,i]=>o"  ("trans[_]'(_')")  where    "trans[A](r) == ∀x∈A. ∀y∈A. ∀z∈A.                          <x,y>: r --> <y,z>: r --> <x,z>: r"definition  rtrancl :: "i=>i"  ("(_^*)" [100] 100)  (*refl/transitive closure*)  where    "r^* == lfp(field(r)*field(r), %s. id(field(r)) ∪ (r O s))"definition  trancl  :: "i=>i"  ("(_^+)" [100] 100)  (*transitive closure*)  where    "r^+ == r O r^*"definition  equiv    :: "[i,i]=>o"  where    "equiv(A,r) == r ⊆ A*A & refl(A,r) & sym(r) & trans(r)"subsection{*General properties of relations*}subsubsection{*irreflexivity*}lemma irreflI:    "[| !!x. x ∈ A ==> <x,x> ∉ r |] ==> irrefl(A,r)"by (simp add: irrefl_def)lemma irreflE: "[| irrefl(A,r);  x ∈ A |] ==>  <x,x> ∉ r"by (simp add: irrefl_def)subsubsection{*symmetry*}lemma symI:     "[| !!x y.<x,y>: r ==> <y,x>: r |] ==> sym(r)"by (unfold sym_def, blast)lemma symE: "[| sym(r); <x,y>: r |]  ==>  <y,x>: r"by (unfold sym_def, blast)subsubsection{*antisymmetry*}lemma antisymI:     "[| !!x y.[| <x,y>: r;  <y,x>: r |] ==> x=y |] ==> antisym(r)"by (simp add: antisym_def, blast)lemma antisymE: "[| antisym(r); <x,y>: r;  <y,x>: r |]  ==>  x=y"by (simp add: antisym_def, blast)subsubsection{*transitivity*}lemma transD: "[| trans(r);  <a,b>:r;  <b,c>:r |] ==> <a,c>:r"by (unfold trans_def, blast)lemma trans_onD:    "[| trans[A](r);  <a,b>:r;  <b,c>:r;  a ∈ A;  b ∈ A;  c ∈ A |] ==> <a,c>:r"by (unfold trans_on_def, blast)lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)"by (unfold trans_def trans_on_def, blast)lemma trans_on_imp_trans: "[|trans[A](r); r ⊆ A*A|] ==> trans(r)";by (simp add: trans_on_def trans_def, blast)subsection{*Transitive closure of a relation*}lemma rtrancl_bnd_mono:     "bnd_mono(field(r)*field(r), %s. id(field(r)) ∪ (r O s))"by (rule bnd_monoI, blast+)lemma rtrancl_mono: "r<=s ==> r^* ⊆ s^*"apply (unfold rtrancl_def)apply (rule lfp_mono)apply (rule rtrancl_bnd_mono)+apply blastdone(* @{term"r^* = id(field(r)) ∪ ( r O r^* )"}    *)lemmas rtrancl_unfold =     rtrancl_bnd_mono [THEN rtrancl_def [THEN def_lfp_unfold]](** The relation rtrancl **)(*  @{term"r^* ⊆ field(r) * field(r)"}  *)lemmas rtrancl_type = rtrancl_def [THEN def_lfp_subset]lemma relation_rtrancl: "relation(r^*)"apply (simp add: relation_def)apply (blast dest: rtrancl_type [THEN subsetD])done(*Reflexivity of rtrancl*)lemma rtrancl_refl: "[| a ∈ field(r) |] ==> <a,a> ∈ r^*"apply (rule rtrancl_unfold [THEN ssubst])apply (erule idI [THEN UnI1])done(*Closure under composition with r  *)lemma rtrancl_into_rtrancl: "[| <a,b> ∈ r^*;  <b,c> ∈ r |] ==> <a,c> ∈ r^*"apply (rule rtrancl_unfold [THEN ssubst])apply (rule compI [THEN UnI2], assumption, assumption)done(*rtrancl of r contains all pairs in r  *)lemma r_into_rtrancl: "<a,b> ∈ r ==> <a,b> ∈ r^*"by (rule rtrancl_refl [THEN rtrancl_into_rtrancl], blast+)(*The premise ensures that r consists entirely of pairs*)lemma r_subset_rtrancl: "relation(r) ==> r ⊆ r^*"by (simp add: relation_def, blast intro: r_into_rtrancl)lemma rtrancl_field: "field(r^*) = field(r)"by (blast intro: r_into_rtrancl dest!: rtrancl_type [THEN subsetD])(** standard induction rule **)lemma rtrancl_full_induct [case_names initial step, consumes 1]:  "[| <a,b> ∈ r^*;      !!x. x ∈ field(r) ==> P(<x,x>);      !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |]  ==>  P(<x,z>) |]   ==>  P(<a,b>)"by (erule def_induct [OF rtrancl_def rtrancl_bnd_mono], blast)(*nice induction rule.  Tried adding the typing hypotheses y,z ∈ field(r), but these  caused expensive case splits!*)lemma rtrancl_induct [case_names initial step, induct set: rtrancl]:  "[| <a,b> ∈ r^*;      P(a);      !!y z.[| <a,y> ∈ r^*;  <y,z> ∈ r;  P(y) |] ==> P(z)   |] ==> P(b)"(*by induction on this formula*)apply (subgoal_tac "∀y. <a,b> = <a,y> --> P (y) ")(*now solve first subgoal: this formula is sufficient*)apply (erule spec [THEN mp], rule refl)(*now do the induction*)apply (erule rtrancl_full_induct, blast+)done(*transitivity of transitive closure!! -- by induction.*)lemma trans_rtrancl: "trans(r^*)"apply (unfold trans_def)apply (intro allI impI)apply (erule_tac b = z in rtrancl_induct, assumption)apply (blast intro: rtrancl_into_rtrancl)donelemmas rtrancl_trans = trans_rtrancl [THEN transD](*elimination of rtrancl -- by induction on a special formula*)lemma rtranclE:    "[| <a,b> ∈ r^*;  (a=b) ==> P;        !!y.[| <a,y> ∈ r^*;   <y,b> ∈ r |] ==> P |]     ==> P"apply (subgoal_tac "a = b | (∃y. <a,y> ∈ r^* & <y,b> ∈ r) ")(*see HOL/trancl*)apply blastapply (erule rtrancl_induct, blast+)done(**** The relation trancl ****)(*Transitivity of r^+ is proved by transitivity of r^*  *)lemma trans_trancl: "trans(r^+)"apply (unfold trans_def trancl_def)apply (blast intro: rtrancl_into_rtrancl                    trans_rtrancl [THEN transD, THEN compI])donelemmas trans_on_trancl = trans_trancl [THEN trans_imp_trans_on]lemmas trancl_trans = trans_trancl [THEN transD](** Conversions between trancl and rtrancl **)lemma trancl_into_rtrancl: "<a,b> ∈ r^+ ==> <a,b> ∈ r^*"apply (unfold trancl_def)apply (blast intro: rtrancl_into_rtrancl)done(*r^+ contains all pairs in r  *)lemma r_into_trancl: "<a,b> ∈ r ==> <a,b> ∈ r^+"apply (unfold trancl_def)apply (blast intro!: rtrancl_refl)done(*The premise ensures that r consists entirely of pairs*)lemma r_subset_trancl: "relation(r) ==> r ⊆ r^+"by (simp add: relation_def, blast intro: r_into_trancl)(*intro rule by definition: from r^* and r  *)lemma rtrancl_into_trancl1: "[| <a,b> ∈ r^*;  <b,c> ∈ r |]   ==>  <a,c> ∈ r^+"by (unfold trancl_def, blast)(*intro rule from r and r^*  *)lemma rtrancl_into_trancl2:    "[| <a,b> ∈ r;  <b,c> ∈ r^* |]   ==>  <a,c> ∈ r^+"apply (erule rtrancl_induct) apply (erule r_into_trancl)apply (blast intro: r_into_trancl trancl_trans)done(*Nice induction rule for trancl*)lemma trancl_induct [case_names initial step, induct set: trancl]:  "[| <a,b> ∈ r^+;      !!y.  [| <a,y> ∈ r |] ==> P(y);      !!y z.[| <a,y> ∈ r^+;  <y,z> ∈ r;  P(y) |] ==> P(z)   |] ==> P(b)"apply (rule compEpair)apply (unfold trancl_def, assumption)(*by induction on this formula*)apply (subgoal_tac "∀z. <y,z> ∈ r --> P (z) ")(*now solve first subgoal: this formula is sufficient*) apply blastapply (erule rtrancl_induct)apply (blast intro: rtrancl_into_trancl1)+done(*elimination of r^+ -- NOT an induction rule*)lemma tranclE:    "[| <a,b> ∈ r^+;        <a,b> ∈ r ==> P;        !!y.[| <a,y> ∈ r^+; <y,b> ∈ r |] ==> P     |] ==> P"apply (subgoal_tac "<a,b> ∈ r | (∃y. <a,y> ∈ r^+ & <y,b> ∈ r) ")apply blastapply (rule compEpair)apply (unfold trancl_def, assumption)apply (erule rtranclE)apply (blast intro: rtrancl_into_trancl1)+donelemma trancl_type: "r^+ ⊆ field(r)*field(r)"apply (unfold trancl_def)apply (blast elim: rtrancl_type [THEN subsetD, THEN SigmaE2])donelemma relation_trancl: "relation(r^+)"apply (simp add: relation_def)apply (blast dest: trancl_type [THEN subsetD])donelemma trancl_subset_times: "r ⊆ A * A ==> r^+ ⊆ A * A"by (insert trancl_type [of r], blast)lemma trancl_mono: "r<=s ==> r^+ ⊆ s^+"by (unfold trancl_def, intro comp_mono rtrancl_mono)lemma trancl_eq_r: "[|relation(r); trans(r)|] ==> r^+ = r"apply (rule equalityI) prefer 2 apply (erule r_subset_trancl, clarify)apply (frule trancl_type [THEN subsetD], clarify)apply (erule trancl_induct, assumption)apply (blast dest: transD)done(** Suggested by Sidi Ould Ehmety **)lemma rtrancl_idemp [simp]: "(r^*)^* = r^*"apply (rule equalityI, auto) prefer 2 apply (frule rtrancl_type [THEN subsetD]) apply (blast intro: r_into_rtrancl )txt{*converse direction*}apply (frule rtrancl_type [THEN subsetD], clarify)apply (erule rtrancl_induct)apply (simp add: rtrancl_refl rtrancl_field)apply (blast intro: rtrancl_trans)donelemma rtrancl_subset: "[| R ⊆ S; S ⊆ R^* |] ==> S^* = R^*"apply (drule rtrancl_mono)apply (drule rtrancl_mono, simp_all, blast)donelemma rtrancl_Un_rtrancl:     "[| relation(r); relation(s) |] ==> (r^* ∪ s^*)^* = (r ∪ s)^*"apply (rule rtrancl_subset)apply (blast dest: r_subset_rtrancl)apply (blast intro: rtrancl_mono [THEN subsetD])done(*** "converse" laws by Sidi Ould Ehmety ***)(** rtrancl **)lemma rtrancl_converseD: "<x,y>:converse(r)^* ==> <x,y>:converse(r^*)"apply (rule converseI)apply (frule rtrancl_type [THEN subsetD])apply (erule rtrancl_induct)apply (blast intro: rtrancl_refl)apply (blast intro: r_into_rtrancl rtrancl_trans)donelemma rtrancl_converseI: "<x,y>:converse(r^*) ==> <x,y>:converse(r)^*"apply (drule converseD)apply (frule rtrancl_type [THEN subsetD])apply (erule rtrancl_induct)apply (blast intro: rtrancl_refl)apply (blast intro: r_into_rtrancl rtrancl_trans)donelemma rtrancl_converse: "converse(r)^* = converse(r^*)"apply (safe intro!: equalityI)apply (frule rtrancl_type [THEN subsetD])apply (safe dest!: rtrancl_converseD intro!: rtrancl_converseI)done(** trancl **)lemma trancl_converseD: "<a, b>:converse(r)^+ ==> <a, b>:converse(r^+)"apply (erule trancl_induct)apply (auto intro: r_into_trancl trancl_trans)donelemma trancl_converseI: "<x,y>:converse(r^+) ==> <x,y>:converse(r)^+"apply (drule converseD)apply (erule trancl_induct)apply (auto intro: r_into_trancl trancl_trans)donelemma trancl_converse: "converse(r)^+ = converse(r^+)"apply (safe intro!: equalityI)apply (frule trancl_type [THEN subsetD])apply (safe dest!: trancl_converseD intro!: trancl_converseI)donelemma converse_trancl_induct [case_names initial step, consumes 1]:"[| <a, b>:r^+; !!y. <y, b> :r ==> P(y);      !!y z. [| <y, z> ∈ r; <z, b> ∈ r^+; P(z) |] ==> P(y) |]       ==> P(a)"apply (drule converseI)apply (simp (no_asm_use) add: trancl_converse [symmetric])apply (erule trancl_induct)apply (auto simp add: trancl_converse)doneend`