1(* Title: ZF/Trancl.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1992 University of Cambridge 4*) 5 6section\<open>Relations: Their General Properties and Transitive Closure\<close> 7 8theory Trancl imports Fixedpt Perm begin 9 10definition 11 refl :: "[i,i]=>o" where 12 "refl(A,r) == (\<forall>x\<in>A. <x,x> \<in> r)" 13 14definition 15 irrefl :: "[i,i]=>o" where 16 "irrefl(A,r) == \<forall>x\<in>A. <x,x> \<notin> r" 17 18definition 19 sym :: "i=>o" where 20 "sym(r) == \<forall>x y. <x,y>: r \<longrightarrow> <y,x>: r" 21 22definition 23 asym :: "i=>o" where 24 "asym(r) == \<forall>x y. <x,y>:r \<longrightarrow> ~ <y,x>:r" 25 26definition 27 antisym :: "i=>o" where 28 "antisym(r) == \<forall>x y.<x,y>:r \<longrightarrow> <y,x>:r \<longrightarrow> x=y" 29 30definition 31 trans :: "i=>o" where 32 "trans(r) == \<forall>x y z. <x,y>: r \<longrightarrow> <y,z>: r \<longrightarrow> <x,z>: r" 33 34definition 35 trans_on :: "[i,i]=>o" ("trans[_]'(_')") where 36 "trans[A](r) == \<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. 37 <x,y>: r \<longrightarrow> <y,z>: r \<longrightarrow> <x,z>: r" 38 39definition 40 rtrancl :: "i=>i" ("(_^*)" [100] 100) (*refl/transitive closure*) where 41 "r^* == lfp(field(r)*field(r), %s. id(field(r)) \<union> (r O s))" 42 43definition 44 trancl :: "i=>i" ("(_^+)" [100] 100) (*transitive closure*) where 45 "r^+ == r O r^*" 46 47definition 48 equiv :: "[i,i]=>o" where 49 "equiv(A,r) == r \<subseteq> A*A & refl(A,r) & sym(r) & trans(r)" 50 51 52subsection\<open>General properties of relations\<close> 53 54subsubsection\<open>irreflexivity\<close> 55 56lemma irreflI: 57 "[| !!x. x \<in> A ==> <x,x> \<notin> r |] ==> irrefl(A,r)" 58by (simp add: irrefl_def) 59 60lemma irreflE: "[| irrefl(A,r); x \<in> A |] ==> <x,x> \<notin> r" 61by (simp add: irrefl_def) 62 63subsubsection\<open>symmetry\<close> 64 65lemma symI: 66 "[| !!x y.<x,y>: r ==> <y,x>: r |] ==> sym(r)" 67by (unfold sym_def, blast) 68 69lemma symE: "[| sym(r); <x,y>: r |] ==> <y,x>: r" 70by (unfold sym_def, blast) 71 72subsubsection\<open>antisymmetry\<close> 73 74lemma antisymI: 75 "[| !!x y.[| <x,y>: r; <y,x>: r |] ==> x=y |] ==> antisym(r)" 76by (simp add: antisym_def, blast) 77 78lemma antisymE: "[| antisym(r); <x,y>: r; <y,x>: r |] ==> x=y" 79by (simp add: antisym_def, blast) 80 81subsubsection\<open>transitivity\<close> 82 83lemma transD: "[| trans(r); <a,b>:r; <b,c>:r |] ==> <a,c>:r" 84by (unfold trans_def, blast) 85 86lemma trans_onD: 87 "[| trans[A](r); <a,b>:r; <b,c>:r; a \<in> A; b \<in> A; c \<in> A |] ==> <a,c>:r" 88by (unfold trans_on_def, blast) 89 90lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)" 91by (unfold trans_def trans_on_def, blast) 92 93lemma trans_on_imp_trans: "[|trans[A](r); r \<subseteq> A*A|] ==> trans(r)" 94by (simp add: trans_on_def trans_def, blast) 95 96 97subsection\<open>Transitive closure of a relation\<close> 98 99lemma rtrancl_bnd_mono: 100 "bnd_mono(field(r)*field(r), %s. id(field(r)) \<union> (r O s))" 101by (rule bnd_monoI, blast+) 102 103lemma rtrancl_mono: "r<=s ==> r^* \<subseteq> s^*" 104apply (unfold rtrancl_def) 105apply (rule lfp_mono) 106apply (rule rtrancl_bnd_mono)+ 107apply blast 108done 109 110(* @{term"r^* = id(field(r)) \<union> ( r O r^* )"} *) 111lemmas rtrancl_unfold = 112 rtrancl_bnd_mono [THEN rtrancl_def [THEN def_lfp_unfold]] 113 114(** The relation rtrancl **) 115 116(* @{term"r^* \<subseteq> field(r) * field(r)"} *) 117lemmas rtrancl_type = rtrancl_def [THEN def_lfp_subset] 118 119lemma relation_rtrancl: "relation(r^*)" 120apply (simp add: relation_def) 121apply (blast dest: rtrancl_type [THEN subsetD]) 122done 123 124(*Reflexivity of rtrancl*) 125lemma rtrancl_refl: "[| a \<in> field(r) |] ==> <a,a> \<in> r^*" 126apply (rule rtrancl_unfold [THEN ssubst]) 127apply (erule idI [THEN UnI1]) 128done 129 130(*Closure under composition with r *) 131lemma rtrancl_into_rtrancl: "[| <a,b> \<in> r^*; <b,c> \<in> r |] ==> <a,c> \<in> r^*" 132apply (rule rtrancl_unfold [THEN ssubst]) 133apply (rule compI [THEN UnI2], assumption, assumption) 134done 135 136(*rtrancl of r contains all pairs in r *) 137lemma r_into_rtrancl: "<a,b> \<in> r ==> <a,b> \<in> r^*" 138by (rule rtrancl_refl [THEN rtrancl_into_rtrancl], blast+) 139 140(*The premise ensures that r consists entirely of pairs*) 141lemma r_subset_rtrancl: "relation(r) ==> r \<subseteq> r^*" 142by (simp add: relation_def, blast intro: r_into_rtrancl) 143 144lemma rtrancl_field: "field(r^*) = field(r)" 145by (blast intro: r_into_rtrancl dest!: rtrancl_type [THEN subsetD]) 146 147 148(** standard induction rule **) 149 150lemma rtrancl_full_induct [case_names initial step, consumes 1]: 151 "[| <a,b> \<in> r^*; 152 !!x. x \<in> field(r) ==> P(<x,x>); 153 !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |] ==> P(<x,z>) |] 154 ==> P(<a,b>)" 155by (erule def_induct [OF rtrancl_def rtrancl_bnd_mono], blast) 156 157(*nice induction rule. 158 Tried adding the typing hypotheses y,z \<in> field(r), but these 159 caused expensive case splits!*) 160lemma rtrancl_induct [case_names initial step, induct set: rtrancl]: 161 "[| <a,b> \<in> r^*; 162 P(a); 163 !!y z.[| <a,y> \<in> r^*; <y,z> \<in> r; P(y) |] ==> P(z) 164 |] ==> P(b)" 165(*by induction on this formula*) 166apply (subgoal_tac "\<forall>y. <a,b> = <a,y> \<longrightarrow> P (y) ") 167(*now solve first subgoal: this formula is sufficient*) 168apply (erule spec [THEN mp], rule refl) 169(*now do the induction*) 170apply (erule rtrancl_full_induct, blast+) 171done 172 173(*transitivity of transitive closure!! -- by induction.*) 174lemma trans_rtrancl: "trans(r^*)" 175apply (unfold trans_def) 176apply (intro allI impI) 177apply (erule_tac b = z in rtrancl_induct, assumption) 178apply (blast intro: rtrancl_into_rtrancl) 179done 180 181lemmas rtrancl_trans = trans_rtrancl [THEN transD] 182 183(*elimination of rtrancl -- by induction on a special formula*) 184lemma rtranclE: 185 "[| <a,b> \<in> r^*; (a=b) ==> P; 186 !!y.[| <a,y> \<in> r^*; <y,b> \<in> r |] ==> P |] 187 ==> P" 188apply (subgoal_tac "a = b | (\<exists>y. <a,y> \<in> r^* & <y,b> \<in> r) ") 189(*see HOL/trancl*) 190apply blast 191apply (erule rtrancl_induct, blast+) 192done 193 194 195(**** The relation trancl ****) 196 197(*Transitivity of r^+ is proved by transitivity of r^* *) 198lemma trans_trancl: "trans(r^+)" 199apply (unfold trans_def trancl_def) 200apply (blast intro: rtrancl_into_rtrancl 201 trans_rtrancl [THEN transD, THEN compI]) 202done 203 204lemmas trans_on_trancl = trans_trancl [THEN trans_imp_trans_on] 205 206lemmas trancl_trans = trans_trancl [THEN transD] 207 208(** Conversions between trancl and rtrancl **) 209 210lemma trancl_into_rtrancl: "<a,b> \<in> r^+ ==> <a,b> \<in> r^*" 211apply (unfold trancl_def) 212apply (blast intro: rtrancl_into_rtrancl) 213done 214 215(*r^+ contains all pairs in r *) 216lemma r_into_trancl: "<a,b> \<in> r ==> <a,b> \<in> r^+" 217apply (unfold trancl_def) 218apply (blast intro!: rtrancl_refl) 219done 220 221(*The premise ensures that r consists entirely of pairs*) 222lemma r_subset_trancl: "relation(r) ==> r \<subseteq> r^+" 223by (simp add: relation_def, blast intro: r_into_trancl) 224 225 226(*intro rule by definition: from r^* and r *) 227lemma rtrancl_into_trancl1: "[| <a,b> \<in> r^*; <b,c> \<in> r |] ==> <a,c> \<in> r^+" 228by (unfold trancl_def, blast) 229 230(*intro rule from r and r^* *) 231lemma rtrancl_into_trancl2: 232 "[| <a,b> \<in> r; <b,c> \<in> r^* |] ==> <a,c> \<in> r^+" 233apply (erule rtrancl_induct) 234 apply (erule r_into_trancl) 235apply (blast intro: r_into_trancl trancl_trans) 236done 237 238(*Nice induction rule for trancl*) 239lemma trancl_induct [case_names initial step, induct set: trancl]: 240 "[| <a,b> \<in> r^+; 241 !!y. [| <a,y> \<in> r |] ==> P(y); 242 !!y z.[| <a,y> \<in> r^+; <y,z> \<in> r; P(y) |] ==> P(z) 243 |] ==> P(b)" 244apply (rule compEpair) 245apply (unfold trancl_def, assumption) 246(*by induction on this formula*) 247apply (subgoal_tac "\<forall>z. <y,z> \<in> r \<longrightarrow> P (z) ") 248(*now solve first subgoal: this formula is sufficient*) 249 apply blast 250apply (erule rtrancl_induct) 251apply (blast intro: rtrancl_into_trancl1)+ 252done 253 254(*elimination of r^+ -- NOT an induction rule*) 255lemma tranclE: 256 "[| <a,b> \<in> r^+; 257 <a,b> \<in> r ==> P; 258 !!y.[| <a,y> \<in> r^+; <y,b> \<in> r |] ==> P 259 |] ==> P" 260apply (subgoal_tac "<a,b> \<in> r | (\<exists>y. <a,y> \<in> r^+ & <y,b> \<in> r) ") 261apply blast 262apply (rule compEpair) 263apply (unfold trancl_def, assumption) 264apply (erule rtranclE) 265apply (blast intro: rtrancl_into_trancl1)+ 266done 267 268lemma trancl_type: "r^+ \<subseteq> field(r)*field(r)" 269apply (unfold trancl_def) 270apply (blast elim: rtrancl_type [THEN subsetD, THEN SigmaE2]) 271done 272 273lemma relation_trancl: "relation(r^+)" 274apply (simp add: relation_def) 275apply (blast dest: trancl_type [THEN subsetD]) 276done 277 278lemma trancl_subset_times: "r \<subseteq> A * A ==> r^+ \<subseteq> A * A" 279by (insert trancl_type [of r], blast) 280 281lemma trancl_mono: "r<=s ==> r^+ \<subseteq> s^+" 282by (unfold trancl_def, intro comp_mono rtrancl_mono) 283 284lemma trancl_eq_r: "[|relation(r); trans(r)|] ==> r^+ = r" 285apply (rule equalityI) 286 prefer 2 apply (erule r_subset_trancl, clarify) 287apply (frule trancl_type [THEN subsetD], clarify) 288apply (erule trancl_induct, assumption) 289apply (blast dest: transD) 290done 291 292 293(** Suggested by Sidi Ould Ehmety **) 294 295lemma rtrancl_idemp [simp]: "(r^*)^* = r^*" 296apply (rule equalityI, auto) 297 prefer 2 298 apply (frule rtrancl_type [THEN subsetD]) 299 apply (blast intro: r_into_rtrancl ) 300txt\<open>converse direction\<close> 301apply (frule rtrancl_type [THEN subsetD], clarify) 302apply (erule rtrancl_induct) 303apply (simp add: rtrancl_refl rtrancl_field) 304apply (blast intro: rtrancl_trans) 305done 306 307lemma rtrancl_subset: "[| R \<subseteq> S; S \<subseteq> R^* |] ==> S^* = R^*" 308apply (drule rtrancl_mono) 309apply (drule rtrancl_mono, simp_all, blast) 310done 311 312lemma rtrancl_Un_rtrancl: 313 "[| relation(r); relation(s) |] ==> (r^* \<union> s^*)^* = (r \<union> s)^*" 314apply (rule rtrancl_subset) 315apply (blast dest: r_subset_rtrancl) 316apply (blast intro: rtrancl_mono [THEN subsetD]) 317done 318 319(*** "converse" laws by Sidi Ould Ehmety ***) 320 321(** rtrancl **) 322 323lemma rtrancl_converseD: "<x,y>:converse(r)^* ==> <x,y>:converse(r^*)" 324apply (rule converseI) 325apply (frule rtrancl_type [THEN subsetD]) 326apply (erule rtrancl_induct) 327apply (blast intro: rtrancl_refl) 328apply (blast intro: r_into_rtrancl rtrancl_trans) 329done 330 331lemma rtrancl_converseI: "<x,y>:converse(r^*) ==> <x,y>:converse(r)^*" 332apply (drule converseD) 333apply (frule rtrancl_type [THEN subsetD]) 334apply (erule rtrancl_induct) 335apply (blast intro: rtrancl_refl) 336apply (blast intro: r_into_rtrancl rtrancl_trans) 337done 338 339lemma rtrancl_converse: "converse(r)^* = converse(r^*)" 340apply (safe intro!: equalityI) 341apply (frule rtrancl_type [THEN subsetD]) 342apply (safe dest!: rtrancl_converseD intro!: rtrancl_converseI) 343done 344 345(** trancl **) 346 347lemma trancl_converseD: "<a, b>:converse(r)^+ ==> <a, b>:converse(r^+)" 348apply (erule trancl_induct) 349apply (auto intro: r_into_trancl trancl_trans) 350done 351 352lemma trancl_converseI: "<x,y>:converse(r^+) ==> <x,y>:converse(r)^+" 353apply (drule converseD) 354apply (erule trancl_induct) 355apply (auto intro: r_into_trancl trancl_trans) 356done 357 358lemma trancl_converse: "converse(r)^+ = converse(r^+)" 359apply (safe intro!: equalityI) 360apply (frule trancl_type [THEN subsetD]) 361apply (safe dest!: trancl_converseD intro!: trancl_converseI) 362done 363 364lemma converse_trancl_induct [case_names initial step, consumes 1]: 365"[| <a, b>:r^+; !!y. <y, b> :r ==> P(y); 366 !!y z. [| <y, z> \<in> r; <z, b> \<in> r^+; P(z) |] ==> P(y) |] 367 ==> P(a)" 368apply (drule converseI) 369apply (simp (no_asm_use) add: trancl_converse [symmetric]) 370apply (erule trancl_induct) 371apply (auto simp add: trancl_converse) 372done 373 374end 375