src/HOL/Transitive_Closure.ML
changeset 10213 01c2744a3786
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Transitive_Closure.ML	Thu Oct 12 18:44:35 2000 +0200
     1.3 @@ -0,0 +1,402 @@
     1.4 +(*  Title:      HOL/Transitive_Closure
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +Theorems about the transitive closure of a relation
    1.10 +*)
    1.11 +
    1.12 +(** The relation rtrancl **)
    1.13 +
    1.14 +section "^*";
    1.15 +
    1.16 +Goal "mono(%s. Id Un (r O s))";
    1.17 +by (rtac monoI 1);
    1.18 +by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1));
    1.19 +qed "rtrancl_fun_mono";
    1.20 +
    1.21 +bind_thm ("rtrancl_unfold", rtrancl_fun_mono RS (rtrancl_def RS def_lfp_unfold));
    1.22 +
    1.23 +(*Reflexivity of rtrancl*)
    1.24 +Goal "(a,a) : r^*";
    1.25 +by (stac rtrancl_unfold 1);
    1.26 +by (Blast_tac 1);
    1.27 +qed "rtrancl_refl";
    1.28 +
    1.29 +Addsimps [rtrancl_refl];
    1.30 +AddSIs   [rtrancl_refl];
    1.31 +
    1.32 +
    1.33 +(*Closure under composition with r*)
    1.34 +Goal "[| (a,b) : r^*;  (b,c) : r |] ==> (a,c) : r^*";
    1.35 +by (stac rtrancl_unfold 1);
    1.36 +by (Blast_tac 1);
    1.37 +qed "rtrancl_into_rtrancl";
    1.38 +
    1.39 +(*rtrancl of r contains r*)
    1.40 +Goal "!!p. p : r ==> p : r^*";
    1.41 +by (split_all_tac 1);
    1.42 +by (etac (rtrancl_refl RS rtrancl_into_rtrancl) 1);
    1.43 +qed "r_into_rtrancl";
    1.44 +
    1.45 +AddIs [r_into_rtrancl];
    1.46 +
    1.47 +(*monotonicity of rtrancl*)
    1.48 +Goalw [rtrancl_def] "r <= s ==> r^* <= s^*";
    1.49 +by (REPEAT(ares_tac [lfp_mono,Un_mono,comp_mono,subset_refl] 1));
    1.50 +qed "rtrancl_mono";
    1.51 +
    1.52 +(** standard induction rule **)
    1.53 +
    1.54 +val major::prems = Goal 
    1.55 +  "[| (a,b) : r^*; \
    1.56 +\     !!x. P(x,x); \
    1.57 +\     !!x y z.[| P(x,y); (x,y): r^*; (y,z): r |]  ==>  P(x,z) |] \
    1.58 +\  ==>  P(a,b)";
    1.59 +by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_lfp_induct) 1);
    1.60 +by (blast_tac (claset() addIs prems) 1);
    1.61 +qed "rtrancl_full_induct";
    1.62 +
    1.63 +(*nice induction rule*)
    1.64 +val major::prems = Goal
    1.65 +    "[| (a::'a,b) : r^*;    \
    1.66 +\       P(a); \
    1.67 +\       !!y z.[| (a,y) : r^*;  (y,z) : r;  P(y) |] ==> P(z) |]  \
    1.68 +\     ==> P(b)";
    1.69 +(*by induction on this formula*)
    1.70 +by (subgoal_tac "! y. (a::'a,b) = (a,y) --> P(y)" 1);
    1.71 +(*now solve first subgoal: this formula is sufficient*)
    1.72 +by (Blast_tac 1);
    1.73 +(*now do the induction*)
    1.74 +by (resolve_tac [major RS rtrancl_full_induct] 1);
    1.75 +by (blast_tac (claset() addIs prems) 1);
    1.76 +by (blast_tac (claset() addIs prems) 1);
    1.77 +qed "rtrancl_induct";
    1.78 +
    1.79 +bind_thm ("rtrancl_induct2", split_rule
    1.80 +  (read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] rtrancl_induct));
    1.81 +
    1.82 +(*transitivity of transitive closure!! -- by induction.*)
    1.83 +Goalw [trans_def] "trans(r^*)";
    1.84 +by Safe_tac;
    1.85 +by (eres_inst_tac [("b","z")] rtrancl_induct 1);
    1.86 +by (ALLGOALS(blast_tac (claset() addIs [rtrancl_into_rtrancl])));
    1.87 +qed "trans_rtrancl";
    1.88 +
    1.89 +bind_thm ("rtrancl_trans", trans_rtrancl RS transD);
    1.90 +
    1.91 +
    1.92 +(*elimination of rtrancl -- by induction on a special formula*)
    1.93 +val major::prems = Goal
    1.94 +    "[| (a::'a,b) : r^*;  (a = b) ==> P;        \
    1.95 +\       !!y.[| (a,y) : r^*; (y,b) : r |] ==> P  \
    1.96 +\    |] ==> P";
    1.97 +by (subgoal_tac "(a::'a) = b  | (? y. (a,y) : r^* & (y,b) : r)" 1);
    1.98 +by (rtac (major RS rtrancl_induct) 2);
    1.99 +by (blast_tac (claset() addIs prems) 2);
   1.100 +by (blast_tac (claset() addIs prems) 2);
   1.101 +by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
   1.102 +qed "rtranclE";
   1.103 +
   1.104 +bind_thm ("rtrancl_into_rtrancl2", r_into_rtrancl RS rtrancl_trans);
   1.105 +
   1.106 +(*** More r^* equations and inclusions ***)
   1.107 +
   1.108 +Goal "(r^*)^* = r^*";
   1.109 +by Auto_tac;
   1.110 +by (etac rtrancl_induct 1);
   1.111 +by (rtac rtrancl_refl 1);
   1.112 +by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   1.113 +qed "rtrancl_idemp";
   1.114 +Addsimps [rtrancl_idemp];
   1.115 +
   1.116 +Goal "R^* O R^* = R^*";
   1.117 +by (rtac set_ext 1);
   1.118 +by (split_all_tac 1);
   1.119 +by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   1.120 +qed "rtrancl_idemp_self_comp";
   1.121 +Addsimps [rtrancl_idemp_self_comp];
   1.122 +
   1.123 +Goal "r <= s^* ==> r^* <= s^*";
   1.124 +by (dtac rtrancl_mono 1);
   1.125 +by (Asm_full_simp_tac 1);
   1.126 +qed "rtrancl_subset_rtrancl";
   1.127 +
   1.128 +Goal "[| R <= S; S <= R^* |] ==> S^* = R^*";
   1.129 +by (dtac rtrancl_mono 1);
   1.130 +by (dtac rtrancl_mono 1);
   1.131 +by (Asm_full_simp_tac 1);
   1.132 +by (Blast_tac 1);
   1.133 +qed "rtrancl_subset";
   1.134 +
   1.135 +Goal "(R^* Un S^*)^* = (R Un S)^*";
   1.136 +by (blast_tac (claset() addSIs [rtrancl_subset]
   1.137 +                        addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
   1.138 +qed "rtrancl_Un_rtrancl";
   1.139 +
   1.140 +Goal "(R^=)^* = R^*";
   1.141 +by (blast_tac (claset() addSIs [rtrancl_subset] addIs [r_into_rtrancl]) 1);
   1.142 +qed "rtrancl_reflcl";
   1.143 +Addsimps [rtrancl_reflcl];
   1.144 +
   1.145 +Goal "(r - Id)^* = r^*";
   1.146 +by (rtac sym 1);
   1.147 +by (rtac rtrancl_subset 1);
   1.148 + by (Blast_tac 1);
   1.149 +by (Clarify_tac 1);
   1.150 +by (rename_tac "a b" 1);
   1.151 +by (case_tac "a=b" 1);
   1.152 + by (Blast_tac 1);
   1.153 +by (blast_tac (claset() addSIs [r_into_rtrancl]) 1);
   1.154 +qed "rtrancl_r_diff_Id";
   1.155 +
   1.156 +Goal "(x,y) : (r^-1)^* ==> (y,x) : r^*";
   1.157 +by (etac rtrancl_induct 1);
   1.158 +by (rtac rtrancl_refl 1);
   1.159 +by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   1.160 +qed "rtrancl_converseD";
   1.161 +
   1.162 +Goal "(y,x) : r^* ==> (x,y) : (r^-1)^*";
   1.163 +by (etac rtrancl_induct 1);
   1.164 +by (rtac rtrancl_refl 1);
   1.165 +by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   1.166 +qed "rtrancl_converseI";
   1.167 +
   1.168 +Goal "(r^-1)^* = (r^*)^-1";
   1.169 +(*blast_tac fails: the split_all_tac wrapper must be called to convert
   1.170 +  the set element to a pair*)
   1.171 +by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI]));
   1.172 +qed "rtrancl_converse";
   1.173 +
   1.174 +val major::prems = Goal
   1.175 +    "[| (a,b) : r^*; P(b); \
   1.176 +\       !!y z.[| (y,z) : r;  (z,b) : r^*;  P(z) |] ==> P(y) |]  \
   1.177 +\     ==> P(a)";
   1.178 +by (rtac (major RS rtrancl_converseI RS rtrancl_induct) 1);
   1.179 +by (resolve_tac prems 1);
   1.180 +by (blast_tac (claset() addIs prems addSDs[rtrancl_converseD])1);
   1.181 +qed "converse_rtrancl_induct";
   1.182 +
   1.183 +bind_thm ("converse_rtrancl_induct2", split_rule
   1.184 +  (read_instantiate [("a","(ax,ay)"),("b","(bx,by)")]converse_rtrancl_induct));
   1.185 +
   1.186 +val major::prems = Goal
   1.187 + "[| (x,z):r^*; \
   1.188 +\    x=z ==> P; \
   1.189 +\    !!y. [| (x,y):r; (y,z):r^* |] ==> P \
   1.190 +\ |] ==> P";
   1.191 +by (subgoal_tac "x = z  | (? y. (x,y) : r & (y,z) : r^*)" 1);
   1.192 +by (rtac (major RS converse_rtrancl_induct) 2);
   1.193 +by (blast_tac (claset() addIs prems) 2);
   1.194 +by (blast_tac (claset() addIs prems) 2);
   1.195 +by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
   1.196 +qed "converse_rtranclE";
   1.197 +
   1.198 +bind_thm ("converse_rtranclE2", split_rule
   1.199 +  (read_instantiate [("x","(xa,xb)"), ("z","(za,zb)")] converse_rtranclE));
   1.200 +
   1.201 +Goal "r O r^* = r^* O r";
   1.202 +by (blast_tac (claset() addEs [rtranclE, converse_rtranclE] 
   1.203 +	               addIs [rtrancl_into_rtrancl, rtrancl_into_rtrancl2]) 1);
   1.204 +qed "r_comp_rtrancl_eq";
   1.205 +
   1.206 +
   1.207 +(**** The relation trancl ****)
   1.208 +
   1.209 +section "^+";
   1.210 +
   1.211 +Goalw [trancl_def] "[| p:r^+; r <= s |] ==> p:s^+";
   1.212 +by (blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1);
   1.213 +qed "trancl_mono";
   1.214 +
   1.215 +(** Conversions between trancl and rtrancl **)
   1.216 +
   1.217 +Goalw [trancl_def]
   1.218 +    "!!p. p : r^+ ==> p : r^*";
   1.219 +by (split_all_tac 1);
   1.220 +by (etac compEpair 1);
   1.221 +by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1));
   1.222 +qed "trancl_into_rtrancl";
   1.223 +
   1.224 +(*r^+ contains r*)
   1.225 +Goalw [trancl_def]
   1.226 +   "!!p. p : r ==> p : r^+";
   1.227 +by (split_all_tac 1);
   1.228 +by (REPEAT (ares_tac [prem,compI,rtrancl_refl] 1));
   1.229 +qed "r_into_trancl";
   1.230 +AddIs [r_into_trancl];
   1.231 +
   1.232 +(*intro rule by definition: from rtrancl and r*)
   1.233 +Goalw [trancl_def] "[| (a,b) : r^*;  (b,c) : r |]   ==>  (a,c) : r^+";
   1.234 +by Auto_tac;
   1.235 +qed "rtrancl_into_trancl1";
   1.236 +
   1.237 +(*intro rule from r and rtrancl*)
   1.238 +Goal "[| (a,b) : r;  (b,c) : r^* |]   ==>  (a,c) : r^+";
   1.239 +by (etac rtranclE 1);
   1.240 +by (blast_tac (claset() addIs [r_into_trancl]) 1);
   1.241 +by (rtac (rtrancl_trans RS rtrancl_into_trancl1) 1);
   1.242 +by (REPEAT (ares_tac [r_into_rtrancl] 1));
   1.243 +qed "rtrancl_into_trancl2";
   1.244 +
   1.245 +(*Nice induction rule for trancl*)
   1.246 +val major::prems = Goal
   1.247 +  "[| (a,b) : r^+;                                      \
   1.248 +\     !!y.  [| (a,y) : r |] ==> P(y);                   \
   1.249 +\     !!y z.[| (a,y) : r^+;  (y,z) : r;  P(y) |] ==> P(z)       \
   1.250 +\  |] ==> P(b)";
   1.251 +by (rtac (rewrite_rule [trancl_def] major  RS  compEpair) 1);
   1.252 +(*by induction on this formula*)
   1.253 +by (subgoal_tac "ALL z. (y,z) : r --> P(z)" 1);
   1.254 +(*now solve first subgoal: this formula is sufficient*)
   1.255 +by (Blast_tac 1);
   1.256 +by (etac rtrancl_induct 1);
   1.257 +by (ALLGOALS (blast_tac (claset() addIs (rtrancl_into_trancl1::prems))));
   1.258 +qed "trancl_induct";
   1.259 +
   1.260 +(*Another induction rule for trancl, incorporating transitivity.*)
   1.261 +val major::prems = Goal
   1.262 + "[| (x,y) : r^+; \
   1.263 +\    !!x y. (x,y) : r ==> P x y; \
   1.264 +\    !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z \
   1.265 +\ |] ==> P x y";
   1.266 +by (blast_tac (claset() addIs ([r_into_trancl,major RS trancl_induct]@prems))1);
   1.267 +qed "trancl_trans_induct";
   1.268 +
   1.269 +(*elimination of r^+ -- NOT an induction rule*)
   1.270 +val major::prems = Goal
   1.271 +    "[| (a::'a,b) : r^+;  \
   1.272 +\       (a,b) : r ==> P; \
   1.273 +\       !!y.[| (a,y) : r^+;  (y,b) : r |] ==> P  \
   1.274 +\    |] ==> P";
   1.275 +by (subgoal_tac "(a::'a,b) : r | (? y. (a,y) : r^+  &  (y,b) : r)" 1);
   1.276 +by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1));
   1.277 +by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
   1.278 +by (etac rtranclE 1);
   1.279 +by (Blast_tac 1);
   1.280 +by (blast_tac (claset() addSIs [rtrancl_into_trancl1]) 1);
   1.281 +qed "tranclE";
   1.282 +
   1.283 +(*Transitivity of r^+.
   1.284 +  Proved by unfolding since it uses transitivity of rtrancl. *)
   1.285 +Goalw [trancl_def] "trans(r^+)";
   1.286 +by (rtac transI 1);
   1.287 +by (REPEAT (etac compEpair 1));
   1.288 +by (rtac (rtrancl_into_rtrancl RS (rtrancl_trans RS compI)) 1);
   1.289 +by (REPEAT (assume_tac 1));
   1.290 +qed "trans_trancl";
   1.291 +
   1.292 +bind_thm ("trancl_trans", trans_trancl RS transD);
   1.293 +
   1.294 +Goalw [trancl_def] "[| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+";
   1.295 +by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   1.296 +qed "rtrancl_trancl_trancl";
   1.297 +
   1.298 +(* "[| (a,b) : r;  (b,c) : r^+ |]   ==>  (a,c) : r^+" *)
   1.299 +bind_thm ("trancl_into_trancl2", [trans_trancl, r_into_trancl] MRS transD);
   1.300 +
   1.301 +(* primitive recursion for trancl over finite relations: *)
   1.302 +Goal "(insert (y,x) r)^+ = r^+ Un {(a,b). (a,y):r^* & (x,b):r^*}";
   1.303 +by (rtac equalityI 1);
   1.304 + by (rtac subsetI 1);
   1.305 + by (split_all_tac 1);
   1.306 + by (etac trancl_induct 1);
   1.307 +  by (blast_tac (claset() addIs [r_into_trancl]) 1);
   1.308 + by (blast_tac (claset() addIs
   1.309 +     [rtrancl_into_trancl1,trancl_into_rtrancl,r_into_trancl,trancl_trans]) 1);
   1.310 +by (rtac subsetI 1);
   1.311 +by (blast_tac (claset() addIs
   1.312 +     [rtrancl_into_trancl2, rtrancl_trancl_trancl,
   1.313 +      impOfSubs rtrancl_mono, trancl_mono]) 1);
   1.314 +qed "trancl_insert";
   1.315 +
   1.316 +Goalw [trancl_def] "(r^-1)^+ = (r^+)^-1";
   1.317 +by (simp_tac (simpset() addsimps [rtrancl_converse,converse_comp]) 1);
   1.318 +by (simp_tac (simpset() addsimps [rtrancl_converse RS sym,
   1.319 +				  r_comp_rtrancl_eq]) 1);
   1.320 +qed "trancl_converse";
   1.321 +
   1.322 +Goal "(x,y) : (r^+)^-1 ==> (x,y) : (r^-1)^+";
   1.323 +by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1);
   1.324 +qed "trancl_converseI";
   1.325 +
   1.326 +Goal "(x,y) : (r^-1)^+ ==> (x,y) : (r^+)^-1";
   1.327 +by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1);
   1.328 +qed "trancl_converseD";
   1.329 +
   1.330 +val major::prems = Goal
   1.331 +    "[| (a,b) : r^+; !!y. (y,b) : r ==> P(y); \
   1.332 +\       !!y z.[| (y,z) : r;  (z,b) : r^+;  P(z) |] ==> P(y) |]  \
   1.333 +\     ==> P(a)";
   1.334 +by (rtac ((major RS converseI RS trancl_converseI) RS trancl_induct) 1);
   1.335 + by (resolve_tac prems 1);
   1.336 + by (etac converseD 1);
   1.337 +by (blast_tac (claset() addIs prems addSDs [trancl_converseD])1);
   1.338 +qed "converse_trancl_induct";
   1.339 +
   1.340 +Goal "(x,y):R^+ ==> ? z. (x,z):R & (z,y):R^*";
   1.341 +be converse_trancl_induct 1;
   1.342 +by Auto_tac;
   1.343 +by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   1.344 +qed "tranclD";
   1.345 +
   1.346 +(*Unused*)
   1.347 +Goal "r^-1 Int r^+ = {} ==> (x, x) ~: r^+";
   1.348 +by (subgoal_tac "!y. (x, y) : r^+ --> x~=y" 1);
   1.349 +by (Fast_tac 1);
   1.350 +by (strip_tac 1);
   1.351 +by (etac trancl_induct 1);
   1.352 +by (auto_tac (claset() addIs [r_into_trancl], simpset()));
   1.353 +qed "irrefl_tranclI";
   1.354 +
   1.355 +Goal "!!X. [| !x. (x, x) ~: r^+; (x,y) : r |] ==> x ~= y";
   1.356 +by (blast_tac (claset() addDs [r_into_trancl]) 1);
   1.357 +qed "irrefl_trancl_rD";
   1.358 +
   1.359 +Goal "[| (a,b) : r^*;  r <= A <*> A |] ==> a=b | a:A";
   1.360 +by (etac rtrancl_induct 1);
   1.361 +by Auto_tac;
   1.362 +val lemma = result();
   1.363 +
   1.364 +Goalw [trancl_def] "r <= A <*> A ==> r^+ <= A <*> A";
   1.365 +by (blast_tac (claset() addSDs [lemma]) 1);
   1.366 +qed "trancl_subset_Sigma";
   1.367 +
   1.368 +
   1.369 +Goal "(r^+)^= = r^*";
   1.370 +by Safe_tac;
   1.371 +by  (etac trancl_into_rtrancl 1);
   1.372 +by (blast_tac (claset() addEs [rtranclE] addDs [rtrancl_into_trancl1]) 1);
   1.373 +qed "reflcl_trancl";
   1.374 +Addsimps[reflcl_trancl];
   1.375 +
   1.376 +Goal "(r^=)^+ = r^*";
   1.377 +by Safe_tac;
   1.378 +by  (dtac trancl_into_rtrancl 1);
   1.379 +by  (Asm_full_simp_tac 1);
   1.380 +by (etac rtranclE 1);
   1.381 +by  Safe_tac;
   1.382 +by  (rtac r_into_trancl 1);
   1.383 +by  (Simp_tac 1);
   1.384 +by (rtac rtrancl_into_trancl1 1);
   1.385 +by (etac (rtrancl_reflcl RS equalityD2 RS subsetD) 1);
   1.386 +by (Fast_tac 1);
   1.387 +qed "trancl_reflcl";
   1.388 +Addsimps[trancl_reflcl];
   1.389 +
   1.390 +Goal "{}^+ = {}";
   1.391 +by (auto_tac (claset() addEs [trancl_induct], simpset()));
   1.392 +qed "trancl_empty";
   1.393 +Addsimps[trancl_empty];
   1.394 +
   1.395 +Goal "{}^* = Id";
   1.396 +by (rtac (reflcl_trancl RS subst) 1);
   1.397 +by (Simp_tac 1);
   1.398 +qed "rtrancl_empty";
   1.399 +Addsimps[rtrancl_empty];
   1.400 +
   1.401 +Goal "(a,b):R^* ==> a=b | a~=b & (a,b):R^+";
   1.402 +by(force_tac (claset(), simpset() addsimps [reflcl_trancl RS sym] 
   1.403 +				  delsimps [reflcl_trancl]) 1);
   1.404 +qed "rtranclD";
   1.405 +