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