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