src/HOL/Transitive_Closure.ML
author nipkow
Thu Oct 12 18:44:35 2000 +0200 (2000-10-12)
changeset 10213 01c2744a3786
permissions -rw-r--r--
*** empty log message ***
     1 (*  Title:      HOL/Transitive_Closure
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 Theorems about the transitive closure of a relation
     7 *)
     8 
     9 (** The relation rtrancl **)
    10 
    11 section "^*";
    12 
    13 Goal "mono(%s. Id Un (r O s))";
    14 by (rtac monoI 1);
    15 by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1));
    16 qed "rtrancl_fun_mono";
    17 
    18 bind_thm ("rtrancl_unfold", rtrancl_fun_mono RS (rtrancl_def RS def_lfp_unfold));
    19 
    20 (*Reflexivity of rtrancl*)
    21 Goal "(a,a) : r^*";
    22 by (stac rtrancl_unfold 1);
    23 by (Blast_tac 1);
    24 qed "rtrancl_refl";
    25 
    26 Addsimps [rtrancl_refl];
    27 AddSIs   [rtrancl_refl];
    28 
    29 
    30 (*Closure under composition with r*)
    31 Goal "[| (a,b) : r^*;  (b,c) : r |] ==> (a,c) : r^*";
    32 by (stac rtrancl_unfold 1);
    33 by (Blast_tac 1);
    34 qed "rtrancl_into_rtrancl";
    35 
    36 (*rtrancl of r contains r*)
    37 Goal "!!p. p : r ==> p : r^*";
    38 by (split_all_tac 1);
    39 by (etac (rtrancl_refl RS rtrancl_into_rtrancl) 1);
    40 qed "r_into_rtrancl";
    41 
    42 AddIs [r_into_rtrancl];
    43 
    44 (*monotonicity of rtrancl*)
    45 Goalw [rtrancl_def] "r <= s ==> r^* <= s^*";
    46 by (REPEAT(ares_tac [lfp_mono,Un_mono,comp_mono,subset_refl] 1));
    47 qed "rtrancl_mono";
    48 
    49 (** standard induction rule **)
    50 
    51 val major::prems = Goal 
    52   "[| (a,b) : r^*; \
    53 \     !!x. P(x,x); \
    54 \     !!x y z.[| P(x,y); (x,y): r^*; (y,z): r |]  ==>  P(x,z) |] \
    55 \  ==>  P(a,b)";
    56 by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_lfp_induct) 1);
    57 by (blast_tac (claset() addIs prems) 1);
    58 qed "rtrancl_full_induct";
    59 
    60 (*nice induction rule*)
    61 val major::prems = Goal
    62     "[| (a::'a,b) : r^*;    \
    63 \       P(a); \
    64 \       !!y z.[| (a,y) : r^*;  (y,z) : r;  P(y) |] ==> P(z) |]  \
    65 \     ==> P(b)";
    66 (*by induction on this formula*)
    67 by (subgoal_tac "! y. (a::'a,b) = (a,y) --> P(y)" 1);
    68 (*now solve first subgoal: this formula is sufficient*)
    69 by (Blast_tac 1);
    70 (*now do the induction*)
    71 by (resolve_tac [major RS rtrancl_full_induct] 1);
    72 by (blast_tac (claset() addIs prems) 1);
    73 by (blast_tac (claset() addIs prems) 1);
    74 qed "rtrancl_induct";
    75 
    76 bind_thm ("rtrancl_induct2", split_rule
    77   (read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] rtrancl_induct));
    78 
    79 (*transitivity of transitive closure!! -- by induction.*)
    80 Goalw [trans_def] "trans(r^*)";
    81 by Safe_tac;
    82 by (eres_inst_tac [("b","z")] rtrancl_induct 1);
    83 by (ALLGOALS(blast_tac (claset() addIs [rtrancl_into_rtrancl])));
    84 qed "trans_rtrancl";
    85 
    86 bind_thm ("rtrancl_trans", trans_rtrancl RS transD);
    87 
    88 
    89 (*elimination of rtrancl -- by induction on a special formula*)
    90 val major::prems = Goal
    91     "[| (a::'a,b) : r^*;  (a = b) ==> P;        \
    92 \       !!y.[| (a,y) : r^*; (y,b) : r |] ==> P  \
    93 \    |] ==> P";
    94 by (subgoal_tac "(a::'a) = b  | (? y. (a,y) : r^* & (y,b) : r)" 1);
    95 by (rtac (major RS rtrancl_induct) 2);
    96 by (blast_tac (claset() addIs prems) 2);
    97 by (blast_tac (claset() addIs prems) 2);
    98 by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
    99 qed "rtranclE";
   100 
   101 bind_thm ("rtrancl_into_rtrancl2", r_into_rtrancl RS rtrancl_trans);
   102 
   103 (*** More r^* equations and inclusions ***)
   104 
   105 Goal "(r^*)^* = r^*";
   106 by Auto_tac;
   107 by (etac rtrancl_induct 1);
   108 by (rtac rtrancl_refl 1);
   109 by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   110 qed "rtrancl_idemp";
   111 Addsimps [rtrancl_idemp];
   112 
   113 Goal "R^* O R^* = R^*";
   114 by (rtac set_ext 1);
   115 by (split_all_tac 1);
   116 by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   117 qed "rtrancl_idemp_self_comp";
   118 Addsimps [rtrancl_idemp_self_comp];
   119 
   120 Goal "r <= s^* ==> r^* <= s^*";
   121 by (dtac rtrancl_mono 1);
   122 by (Asm_full_simp_tac 1);
   123 qed "rtrancl_subset_rtrancl";
   124 
   125 Goal "[| R <= S; S <= R^* |] ==> S^* = R^*";
   126 by (dtac rtrancl_mono 1);
   127 by (dtac rtrancl_mono 1);
   128 by (Asm_full_simp_tac 1);
   129 by (Blast_tac 1);
   130 qed "rtrancl_subset";
   131 
   132 Goal "(R^* Un S^*)^* = (R Un S)^*";
   133 by (blast_tac (claset() addSIs [rtrancl_subset]
   134                         addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
   135 qed "rtrancl_Un_rtrancl";
   136 
   137 Goal "(R^=)^* = R^*";
   138 by (blast_tac (claset() addSIs [rtrancl_subset] addIs [r_into_rtrancl]) 1);
   139 qed "rtrancl_reflcl";
   140 Addsimps [rtrancl_reflcl];
   141 
   142 Goal "(r - Id)^* = r^*";
   143 by (rtac sym 1);
   144 by (rtac rtrancl_subset 1);
   145  by (Blast_tac 1);
   146 by (Clarify_tac 1);
   147 by (rename_tac "a b" 1);
   148 by (case_tac "a=b" 1);
   149  by (Blast_tac 1);
   150 by (blast_tac (claset() addSIs [r_into_rtrancl]) 1);
   151 qed "rtrancl_r_diff_Id";
   152 
   153 Goal "(x,y) : (r^-1)^* ==> (y,x) : r^*";
   154 by (etac rtrancl_induct 1);
   155 by (rtac rtrancl_refl 1);
   156 by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   157 qed "rtrancl_converseD";
   158 
   159 Goal "(y,x) : r^* ==> (x,y) : (r^-1)^*";
   160 by (etac rtrancl_induct 1);
   161 by (rtac rtrancl_refl 1);
   162 by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   163 qed "rtrancl_converseI";
   164 
   165 Goal "(r^-1)^* = (r^*)^-1";
   166 (*blast_tac fails: the split_all_tac wrapper must be called to convert
   167   the set element to a pair*)
   168 by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI]));
   169 qed "rtrancl_converse";
   170 
   171 val major::prems = Goal
   172     "[| (a,b) : r^*; P(b); \
   173 \       !!y z.[| (y,z) : r;  (z,b) : r^*;  P(z) |] ==> P(y) |]  \
   174 \     ==> P(a)";
   175 by (rtac (major RS rtrancl_converseI RS rtrancl_induct) 1);
   176 by (resolve_tac prems 1);
   177 by (blast_tac (claset() addIs prems addSDs[rtrancl_converseD])1);
   178 qed "converse_rtrancl_induct";
   179 
   180 bind_thm ("converse_rtrancl_induct2", split_rule
   181   (read_instantiate [("a","(ax,ay)"),("b","(bx,by)")]converse_rtrancl_induct));
   182 
   183 val major::prems = Goal
   184  "[| (x,z):r^*; \
   185 \    x=z ==> P; \
   186 \    !!y. [| (x,y):r; (y,z):r^* |] ==> P \
   187 \ |] ==> P";
   188 by (subgoal_tac "x = z  | (? y. (x,y) : r & (y,z) : r^*)" 1);
   189 by (rtac (major RS converse_rtrancl_induct) 2);
   190 by (blast_tac (claset() addIs prems) 2);
   191 by (blast_tac (claset() addIs prems) 2);
   192 by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
   193 qed "converse_rtranclE";
   194 
   195 bind_thm ("converse_rtranclE2", split_rule
   196   (read_instantiate [("x","(xa,xb)"), ("z","(za,zb)")] converse_rtranclE));
   197 
   198 Goal "r O r^* = r^* O r";
   199 by (blast_tac (claset() addEs [rtranclE, converse_rtranclE] 
   200 	               addIs [rtrancl_into_rtrancl, rtrancl_into_rtrancl2]) 1);
   201 qed "r_comp_rtrancl_eq";
   202 
   203 
   204 (**** The relation trancl ****)
   205 
   206 section "^+";
   207 
   208 Goalw [trancl_def] "[| p:r^+; r <= s |] ==> p:s^+";
   209 by (blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1);
   210 qed "trancl_mono";
   211 
   212 (** Conversions between trancl and rtrancl **)
   213 
   214 Goalw [trancl_def]
   215     "!!p. p : r^+ ==> p : r^*";
   216 by (split_all_tac 1);
   217 by (etac compEpair 1);
   218 by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1));
   219 qed "trancl_into_rtrancl";
   220 
   221 (*r^+ contains r*)
   222 Goalw [trancl_def]
   223    "!!p. p : r ==> p : r^+";
   224 by (split_all_tac 1);
   225 by (REPEAT (ares_tac [prem,compI,rtrancl_refl] 1));
   226 qed "r_into_trancl";
   227 AddIs [r_into_trancl];
   228 
   229 (*intro rule by definition: from rtrancl and r*)
   230 Goalw [trancl_def] "[| (a,b) : r^*;  (b,c) : r |]   ==>  (a,c) : r^+";
   231 by Auto_tac;
   232 qed "rtrancl_into_trancl1";
   233 
   234 (*intro rule from r and rtrancl*)
   235 Goal "[| (a,b) : r;  (b,c) : r^* |]   ==>  (a,c) : r^+";
   236 by (etac rtranclE 1);
   237 by (blast_tac (claset() addIs [r_into_trancl]) 1);
   238 by (rtac (rtrancl_trans RS rtrancl_into_trancl1) 1);
   239 by (REPEAT (ares_tac [r_into_rtrancl] 1));
   240 qed "rtrancl_into_trancl2";
   241 
   242 (*Nice induction rule for trancl*)
   243 val major::prems = Goal
   244   "[| (a,b) : r^+;                                      \
   245 \     !!y.  [| (a,y) : r |] ==> P(y);                   \
   246 \     !!y z.[| (a,y) : r^+;  (y,z) : r;  P(y) |] ==> P(z)       \
   247 \  |] ==> P(b)";
   248 by (rtac (rewrite_rule [trancl_def] major  RS  compEpair) 1);
   249 (*by induction on this formula*)
   250 by (subgoal_tac "ALL z. (y,z) : r --> P(z)" 1);
   251 (*now solve first subgoal: this formula is sufficient*)
   252 by (Blast_tac 1);
   253 by (etac rtrancl_induct 1);
   254 by (ALLGOALS (blast_tac (claset() addIs (rtrancl_into_trancl1::prems))));
   255 qed "trancl_induct";
   256 
   257 (*Another induction rule for trancl, incorporating transitivity.*)
   258 val major::prems = Goal
   259  "[| (x,y) : r^+; \
   260 \    !!x y. (x,y) : r ==> P x y; \
   261 \    !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z \
   262 \ |] ==> P x y";
   263 by (blast_tac (claset() addIs ([r_into_trancl,major RS trancl_induct]@prems))1);
   264 qed "trancl_trans_induct";
   265 
   266 (*elimination of r^+ -- NOT an induction rule*)
   267 val major::prems = Goal
   268     "[| (a::'a,b) : r^+;  \
   269 \       (a,b) : r ==> P; \
   270 \       !!y.[| (a,y) : r^+;  (y,b) : r |] ==> P  \
   271 \    |] ==> P";
   272 by (subgoal_tac "(a::'a,b) : r | (? y. (a,y) : r^+  &  (y,b) : r)" 1);
   273 by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1));
   274 by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
   275 by (etac rtranclE 1);
   276 by (Blast_tac 1);
   277 by (blast_tac (claset() addSIs [rtrancl_into_trancl1]) 1);
   278 qed "tranclE";
   279 
   280 (*Transitivity of r^+.
   281   Proved by unfolding since it uses transitivity of rtrancl. *)
   282 Goalw [trancl_def] "trans(r^+)";
   283 by (rtac transI 1);
   284 by (REPEAT (etac compEpair 1));
   285 by (rtac (rtrancl_into_rtrancl RS (rtrancl_trans RS compI)) 1);
   286 by (REPEAT (assume_tac 1));
   287 qed "trans_trancl";
   288 
   289 bind_thm ("trancl_trans", trans_trancl RS transD);
   290 
   291 Goalw [trancl_def] "[| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+";
   292 by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   293 qed "rtrancl_trancl_trancl";
   294 
   295 (* "[| (a,b) : r;  (b,c) : r^+ |]   ==>  (a,c) : r^+" *)
   296 bind_thm ("trancl_into_trancl2", [trans_trancl, r_into_trancl] MRS transD);
   297 
   298 (* primitive recursion for trancl over finite relations: *)
   299 Goal "(insert (y,x) r)^+ = r^+ Un {(a,b). (a,y):r^* & (x,b):r^*}";
   300 by (rtac equalityI 1);
   301  by (rtac subsetI 1);
   302  by (split_all_tac 1);
   303  by (etac trancl_induct 1);
   304   by (blast_tac (claset() addIs [r_into_trancl]) 1);
   305  by (blast_tac (claset() addIs
   306      [rtrancl_into_trancl1,trancl_into_rtrancl,r_into_trancl,trancl_trans]) 1);
   307 by (rtac subsetI 1);
   308 by (blast_tac (claset() addIs
   309      [rtrancl_into_trancl2, rtrancl_trancl_trancl,
   310       impOfSubs rtrancl_mono, trancl_mono]) 1);
   311 qed "trancl_insert";
   312 
   313 Goalw [trancl_def] "(r^-1)^+ = (r^+)^-1";
   314 by (simp_tac (simpset() addsimps [rtrancl_converse,converse_comp]) 1);
   315 by (simp_tac (simpset() addsimps [rtrancl_converse RS sym,
   316 				  r_comp_rtrancl_eq]) 1);
   317 qed "trancl_converse";
   318 
   319 Goal "(x,y) : (r^+)^-1 ==> (x,y) : (r^-1)^+";
   320 by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1);
   321 qed "trancl_converseI";
   322 
   323 Goal "(x,y) : (r^-1)^+ ==> (x,y) : (r^+)^-1";
   324 by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1);
   325 qed "trancl_converseD";
   326 
   327 val major::prems = Goal
   328     "[| (a,b) : r^+; !!y. (y,b) : r ==> P(y); \
   329 \       !!y z.[| (y,z) : r;  (z,b) : r^+;  P(z) |] ==> P(y) |]  \
   330 \     ==> P(a)";
   331 by (rtac ((major RS converseI RS trancl_converseI) RS trancl_induct) 1);
   332  by (resolve_tac prems 1);
   333  by (etac converseD 1);
   334 by (blast_tac (claset() addIs prems addSDs [trancl_converseD])1);
   335 qed "converse_trancl_induct";
   336 
   337 Goal "(x,y):R^+ ==> ? z. (x,z):R & (z,y):R^*";
   338 be converse_trancl_induct 1;
   339 by Auto_tac;
   340 by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   341 qed "tranclD";
   342 
   343 (*Unused*)
   344 Goal "r^-1 Int r^+ = {} ==> (x, x) ~: r^+";
   345 by (subgoal_tac "!y. (x, y) : r^+ --> x~=y" 1);
   346 by (Fast_tac 1);
   347 by (strip_tac 1);
   348 by (etac trancl_induct 1);
   349 by (auto_tac (claset() addIs [r_into_trancl], simpset()));
   350 qed "irrefl_tranclI";
   351 
   352 Goal "!!X. [| !x. (x, x) ~: r^+; (x,y) : r |] ==> x ~= y";
   353 by (blast_tac (claset() addDs [r_into_trancl]) 1);
   354 qed "irrefl_trancl_rD";
   355 
   356 Goal "[| (a,b) : r^*;  r <= A <*> A |] ==> a=b | a:A";
   357 by (etac rtrancl_induct 1);
   358 by Auto_tac;
   359 val lemma = result();
   360 
   361 Goalw [trancl_def] "r <= A <*> A ==> r^+ <= A <*> A";
   362 by (blast_tac (claset() addSDs [lemma]) 1);
   363 qed "trancl_subset_Sigma";
   364 
   365 
   366 Goal "(r^+)^= = r^*";
   367 by Safe_tac;
   368 by  (etac trancl_into_rtrancl 1);
   369 by (blast_tac (claset() addEs [rtranclE] addDs [rtrancl_into_trancl1]) 1);
   370 qed "reflcl_trancl";
   371 Addsimps[reflcl_trancl];
   372 
   373 Goal "(r^=)^+ = r^*";
   374 by Safe_tac;
   375 by  (dtac trancl_into_rtrancl 1);
   376 by  (Asm_full_simp_tac 1);
   377 by (etac rtranclE 1);
   378 by  Safe_tac;
   379 by  (rtac r_into_trancl 1);
   380 by  (Simp_tac 1);
   381 by (rtac rtrancl_into_trancl1 1);
   382 by (etac (rtrancl_reflcl RS equalityD2 RS subsetD) 1);
   383 by (Fast_tac 1);
   384 qed "trancl_reflcl";
   385 Addsimps[trancl_reflcl];
   386 
   387 Goal "{}^+ = {}";
   388 by (auto_tac (claset() addEs [trancl_induct], simpset()));
   389 qed "trancl_empty";
   390 Addsimps[trancl_empty];
   391 
   392 Goal "{}^* = Id";
   393 by (rtac (reflcl_trancl RS subst) 1);
   394 by (Simp_tac 1);
   395 qed "rtrancl_empty";
   396 Addsimps[rtrancl_empty];
   397 
   398 Goal "(a,b):R^* ==> a=b | a~=b & (a,b):R^+";
   399 by(force_tac (claset(), simpset() addsimps [reflcl_trancl RS sym] 
   400 				  delsimps [reflcl_trancl]) 1);
   401 qed "rtranclD";
   402