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