Transitive_Closure turned into new-style theory;
authorwenzelm
Fri Jan 26 00:15:36 2001 +0100 (2001-01-26)
changeset 109800a45f2efaaec
parent 10979 3da4543034e7
child 10981 8d37c8befbe6
Transitive_Closure turned into new-style theory;
src/HOL/IsaMakefile
src/HOL/Transitive_Closure.thy
src/HOL/Transitive_Closure_lemmas.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Jan 26 00:14:25 2001 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jan 26 00:15:36 2001 +0100
     1.3 @@ -97,7 +97,7 @@
     1.4    Tools/inductive_package.ML Tools/meson.ML Tools/numeral_syntax.ML \
     1.5    Tools/primrec_package.ML Tools/recdef_package.ML \
     1.6    Tools/record_package.ML Tools/svc_funcs.ML Tools/typedef_package.ML \
     1.7 -  Transitive_Closure.ML Transitive_Closure.thy Wellfounded_Recursion.ML \
     1.8 +  Transitive_Closure.thy Transitive_Closure_lemmas.ML Wellfounded_Recursion.ML \
     1.9    Wellfounded_Recursion.thy Wellfounded_Relations.ML \
    1.10    Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \
    1.11    equalities.ML equalities.thy hologic.ML meson_lemmas.ML mono.ML \
     2.1 --- a/src/HOL/Transitive_Closure.thy	Fri Jan 26 00:14:25 2001 +0100
     2.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Jan 26 00:15:36 2001 +0100
     2.3 @@ -13,7 +13,8 @@
     2.4  to be atomic.
     2.5  *)
     2.6  
     2.7 -Transitive_Closure = Lfp + Relation + 
     2.8 +theory Transitive_Closure = Lfp + Relation
     2.9 +files ("Transitive_Closure_lemmas.ML"):
    2.10  
    2.11  constdefs
    2.12    rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^*)" [1000] 999)
    2.13 @@ -32,4 +33,6 @@
    2.14    trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>+)" [1000] 999)
    2.15    "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>=)" [1000] 999)
    2.16  
    2.17 +use "Transitive_Closure_lemmas.ML"
    2.18 +
    2.19  end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Transitive_Closure_lemmas.ML	Fri Jan 26 00:15:36 2001 +0100
     3.3 @@ -0,0 +1,406 @@
     3.4 +(*  Title:      HOL/Transitive_Closure_lemmas.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1992  University of Cambridge
     3.8 +
     3.9 +Theorems about the transitive closure of a relation
    3.10 +*)
    3.11 +
    3.12 +val rtrancl_def = thm "rtrancl_def";
    3.13 +val trancl_def = thm "trancl_def";
    3.14 +
    3.15 +
    3.16 +(** The relation rtrancl **)
    3.17 +
    3.18 +section "^*";
    3.19 +
    3.20 +Goal "mono(%s. Id Un (r O s))";
    3.21 +by (rtac monoI 1);
    3.22 +by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1));
    3.23 +qed "rtrancl_fun_mono";
    3.24 +
    3.25 +bind_thm ("rtrancl_unfold", rtrancl_fun_mono RS (rtrancl_def RS def_lfp_unfold));
    3.26 +
    3.27 +(*Reflexivity of rtrancl*)
    3.28 +Goal "(a,a) : r^*";
    3.29 +by (stac rtrancl_unfold 1);
    3.30 +by (Blast_tac 1);
    3.31 +qed "rtrancl_refl";
    3.32 +
    3.33 +Addsimps [rtrancl_refl];
    3.34 +AddSIs   [rtrancl_refl];
    3.35 +
    3.36 +
    3.37 +(*Closure under composition with r*)
    3.38 +Goal "[| (a,b) : r^*;  (b,c) : r |] ==> (a,c) : r^*";
    3.39 +by (stac rtrancl_unfold 1);
    3.40 +by (Blast_tac 1);
    3.41 +qed "rtrancl_into_rtrancl";
    3.42 +
    3.43 +(*rtrancl of r contains r*)
    3.44 +Goal "!!p. p : r ==> p : r^*";
    3.45 +by (split_all_tac 1);
    3.46 +by (etac (rtrancl_refl RS rtrancl_into_rtrancl) 1);
    3.47 +qed "r_into_rtrancl";
    3.48 +
    3.49 +AddIs [r_into_rtrancl];
    3.50 +
    3.51 +(*monotonicity of rtrancl*)
    3.52 +Goalw [rtrancl_def] "r <= s ==> r^* <= s^*";
    3.53 +by (REPEAT(ares_tac [lfp_mono,Un_mono,comp_mono,subset_refl] 1));
    3.54 +qed "rtrancl_mono";
    3.55 +
    3.56 +(** standard induction rule **)
    3.57 +
    3.58 +val major::prems = Goal 
    3.59 +  "[| (a,b) : r^*; \
    3.60 +\     !!x. P(x,x); \
    3.61 +\     !!x y z.[| P(x,y); (x,y): r^*; (y,z): r |]  ==>  P(x,z) |] \
    3.62 +\  ==>  P(a,b)";
    3.63 +by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_lfp_induct) 1);
    3.64 +by (blast_tac (claset() addIs prems) 1);
    3.65 +qed "rtrancl_full_induct";
    3.66 +
    3.67 +(*nice induction rule*)
    3.68 +val major::prems = Goal
    3.69 +    "[| (a::'a,b) : r^*;    \
    3.70 +\       P(a); \
    3.71 +\       !!y z.[| (a,y) : r^*;  (y,z) : r;  P(y) |] ==> P(z) |]  \
    3.72 +\     ==> P(b)";
    3.73 +(*by induction on this formula*)
    3.74 +by (subgoal_tac "! y. (a::'a,b) = (a,y) --> P(y)" 1);
    3.75 +(*now solve first subgoal: this formula is sufficient*)
    3.76 +by (Blast_tac 1);
    3.77 +(*now do the induction*)
    3.78 +by (resolve_tac [major RS rtrancl_full_induct] 1);
    3.79 +by (blast_tac (claset() addIs prems) 1);
    3.80 +by (blast_tac (claset() addIs prems) 1);
    3.81 +qed "rtrancl_induct";
    3.82 +
    3.83 +bind_thm ("rtrancl_induct2", split_rule
    3.84 +  (read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] rtrancl_induct));
    3.85 +
    3.86 +(*transitivity of transitive closure!! -- by induction.*)
    3.87 +Goalw [trans_def] "trans(r^*)";
    3.88 +by Safe_tac;
    3.89 +by (eres_inst_tac [("b","z")] rtrancl_induct 1);
    3.90 +by (ALLGOALS(blast_tac (claset() addIs [rtrancl_into_rtrancl])));
    3.91 +qed "trans_rtrancl";
    3.92 +
    3.93 +bind_thm ("rtrancl_trans", trans_rtrancl RS transD);
    3.94 +
    3.95 +
    3.96 +(*elimination of rtrancl -- by induction on a special formula*)
    3.97 +val major::prems = Goal
    3.98 +    "[| (a::'a,b) : r^*;  (a = b) ==> P;        \
    3.99 +\       !!y.[| (a,y) : r^*; (y,b) : r |] ==> P  \
   3.100 +\    |] ==> P";
   3.101 +by (subgoal_tac "(a::'a) = b  | (? y. (a,y) : r^* & (y,b) : r)" 1);
   3.102 +by (rtac (major RS rtrancl_induct) 2);
   3.103 +by (blast_tac (claset() addIs prems) 2);
   3.104 +by (blast_tac (claset() addIs prems) 2);
   3.105 +by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
   3.106 +qed "rtranclE";
   3.107 +
   3.108 +bind_thm ("rtrancl_into_rtrancl2", r_into_rtrancl RS rtrancl_trans);
   3.109 +
   3.110 +(*** More r^* equations and inclusions ***)
   3.111 +
   3.112 +Goal "(r^*)^* = r^*";
   3.113 +by Auto_tac;
   3.114 +by (etac rtrancl_induct 1);
   3.115 +by (rtac rtrancl_refl 1);
   3.116 +by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   3.117 +qed "rtrancl_idemp";
   3.118 +Addsimps [rtrancl_idemp];
   3.119 +
   3.120 +Goal "R^* O R^* = R^*";
   3.121 +by (rtac set_ext 1);
   3.122 +by (split_all_tac 1);
   3.123 +by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   3.124 +qed "rtrancl_idemp_self_comp";
   3.125 +Addsimps [rtrancl_idemp_self_comp];
   3.126 +
   3.127 +Goal "r <= s^* ==> r^* <= s^*";
   3.128 +by (dtac rtrancl_mono 1);
   3.129 +by (Asm_full_simp_tac 1);
   3.130 +qed "rtrancl_subset_rtrancl";
   3.131 +
   3.132 +Goal "[| R <= S; S <= R^* |] ==> S^* = R^*";
   3.133 +by (dtac rtrancl_mono 1);
   3.134 +by (dtac rtrancl_mono 1);
   3.135 +by (Asm_full_simp_tac 1);
   3.136 +by (Blast_tac 1);
   3.137 +qed "rtrancl_subset";
   3.138 +
   3.139 +Goal "(R^* Un S^*)^* = (R Un S)^*";
   3.140 +by (blast_tac (claset() addSIs [rtrancl_subset]
   3.141 +                        addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
   3.142 +qed "rtrancl_Un_rtrancl";
   3.143 +
   3.144 +Goal "(R^=)^* = R^*";
   3.145 +by (blast_tac (claset() addSIs [rtrancl_subset] addIs [r_into_rtrancl]) 1);
   3.146 +qed "rtrancl_reflcl";
   3.147 +Addsimps [rtrancl_reflcl];
   3.148 +
   3.149 +Goal "(r - Id)^* = r^*";
   3.150 +by (rtac sym 1);
   3.151 +by (rtac rtrancl_subset 1);
   3.152 + by (Blast_tac 1);
   3.153 +by (Clarify_tac 1);
   3.154 +by (rename_tac "a b" 1);
   3.155 +by (case_tac "a=b" 1);
   3.156 + by (Blast_tac 1);
   3.157 +by (blast_tac (claset() addSIs [r_into_rtrancl]) 1);
   3.158 +qed "rtrancl_r_diff_Id";
   3.159 +
   3.160 +Goal "(x,y) : (r^-1)^* ==> (y,x) : r^*";
   3.161 +by (etac rtrancl_induct 1);
   3.162 +by (rtac rtrancl_refl 1);
   3.163 +by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   3.164 +qed "rtrancl_converseD";
   3.165 +
   3.166 +Goal "(y,x) : r^* ==> (x,y) : (r^-1)^*";
   3.167 +by (etac rtrancl_induct 1);
   3.168 +by (rtac rtrancl_refl 1);
   3.169 +by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   3.170 +qed "rtrancl_converseI";
   3.171 +
   3.172 +Goal "(r^-1)^* = (r^*)^-1";
   3.173 +(*blast_tac fails: the split_all_tac wrapper must be called to convert
   3.174 +  the set element to a pair*)
   3.175 +by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI]));
   3.176 +qed "rtrancl_converse";
   3.177 +
   3.178 +val major::prems = Goal
   3.179 +    "[| (a,b) : r^*; P(b); \
   3.180 +\       !!y z.[| (y,z) : r;  (z,b) : r^*;  P(z) |] ==> P(y) |]  \
   3.181 +\     ==> P(a)";
   3.182 +by (rtac (major RS rtrancl_converseI RS rtrancl_induct) 1);
   3.183 +by (resolve_tac prems 1);
   3.184 +by (blast_tac (claset() addIs prems addSDs[rtrancl_converseD])1);
   3.185 +qed "converse_rtrancl_induct";
   3.186 +
   3.187 +bind_thm ("converse_rtrancl_induct2", split_rule
   3.188 +  (read_instantiate [("a","(ax,ay)"),("b","(bx,by)")]converse_rtrancl_induct));
   3.189 +
   3.190 +val major::prems = Goal
   3.191 + "[| (x,z):r^*; \
   3.192 +\    x=z ==> P; \
   3.193 +\    !!y. [| (x,y):r; (y,z):r^* |] ==> P \
   3.194 +\ |] ==> P";
   3.195 +by (subgoal_tac "x = z  | (? y. (x,y) : r & (y,z) : r^*)" 1);
   3.196 +by (rtac (major RS converse_rtrancl_induct) 2);
   3.197 +by (blast_tac (claset() addIs prems) 2);
   3.198 +by (blast_tac (claset() addIs prems) 2);
   3.199 +by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
   3.200 +qed "converse_rtranclE";
   3.201 +
   3.202 +bind_thm ("converse_rtranclE2", split_rule
   3.203 +  (read_instantiate [("x","(xa,xb)"), ("z","(za,zb)")] converse_rtranclE));
   3.204 +
   3.205 +Goal "r O r^* = r^* O r";
   3.206 +by (blast_tac (claset() addEs [rtranclE, converse_rtranclE] 
   3.207 +	               addIs [rtrancl_into_rtrancl, rtrancl_into_rtrancl2]) 1);
   3.208 +qed "r_comp_rtrancl_eq";
   3.209 +
   3.210 +
   3.211 +(**** The relation trancl ****)
   3.212 +
   3.213 +section "^+";
   3.214 +
   3.215 +Goalw [trancl_def] "[| p:r^+; r <= s |] ==> p:s^+";
   3.216 +by (blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1);
   3.217 +qed "trancl_mono";
   3.218 +
   3.219 +(** Conversions between trancl and rtrancl **)
   3.220 +
   3.221 +Goalw [trancl_def]
   3.222 +    "!!p. p : r^+ ==> p : r^*";
   3.223 +by (split_all_tac 1);
   3.224 +by (etac compEpair 1);
   3.225 +by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1));
   3.226 +qed "trancl_into_rtrancl";
   3.227 +
   3.228 +(*r^+ contains r*)
   3.229 +Goalw [trancl_def]
   3.230 +   "!!p. p : r ==> p : r^+";
   3.231 +by (split_all_tac 1);
   3.232 +by (REPEAT (ares_tac [prem,compI,rtrancl_refl] 1));
   3.233 +qed "r_into_trancl";
   3.234 +AddIs [r_into_trancl];
   3.235 +
   3.236 +(*intro rule by definition: from rtrancl and r*)
   3.237 +Goalw [trancl_def] "[| (a,b) : r^*;  (b,c) : r |]   ==>  (a,c) : r^+";
   3.238 +by Auto_tac;
   3.239 +qed "rtrancl_into_trancl1";
   3.240 +
   3.241 +(*intro rule from r and rtrancl*)
   3.242 +Goal "[| (a,b) : r;  (b,c) : r^* |]   ==>  (a,c) : r^+";
   3.243 +by (etac rtranclE 1);
   3.244 +by (blast_tac (claset() addIs [r_into_trancl]) 1);
   3.245 +by (rtac (rtrancl_trans RS rtrancl_into_trancl1) 1);
   3.246 +by (REPEAT (ares_tac [r_into_rtrancl] 1));
   3.247 +qed "rtrancl_into_trancl2";
   3.248 +
   3.249 +(*Nice induction rule for trancl*)
   3.250 +val major::prems = Goal
   3.251 +  "[| (a,b) : r^+;                                      \
   3.252 +\     !!y.  [| (a,y) : r |] ==> P(y);                   \
   3.253 +\     !!y z.[| (a,y) : r^+;  (y,z) : r;  P(y) |] ==> P(z)       \
   3.254 +\  |] ==> P(b)";
   3.255 +by (rtac (rewrite_rule [trancl_def] major  RS  compEpair) 1);
   3.256 +(*by induction on this formula*)
   3.257 +by (subgoal_tac "ALL z. (y,z) : r --> P(z)" 1);
   3.258 +(*now solve first subgoal: this formula is sufficient*)
   3.259 +by (Blast_tac 1);
   3.260 +by (etac rtrancl_induct 1);
   3.261 +by (ALLGOALS (blast_tac (claset() addIs (rtrancl_into_trancl1::prems))));
   3.262 +qed "trancl_induct";
   3.263 +
   3.264 +(*Another induction rule for trancl, incorporating transitivity.*)
   3.265 +val major::prems = Goal
   3.266 + "[| (x,y) : r^+; \
   3.267 +\    !!x y. (x,y) : r ==> P x y; \
   3.268 +\    !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z \
   3.269 +\ |] ==> P x y";
   3.270 +by (blast_tac (claset() addIs ([r_into_trancl,major RS trancl_induct]@prems))1);
   3.271 +qed "trancl_trans_induct";
   3.272 +
   3.273 +(*elimination of r^+ -- NOT an induction rule*)
   3.274 +val major::prems = Goal
   3.275 +    "[| (a::'a,b) : r^+;  \
   3.276 +\       (a,b) : r ==> P; \
   3.277 +\       !!y.[| (a,y) : r^+;  (y,b) : r |] ==> P  \
   3.278 +\    |] ==> P";
   3.279 +by (subgoal_tac "(a::'a,b) : r | (? y. (a,y) : r^+  &  (y,b) : r)" 1);
   3.280 +by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1));
   3.281 +by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
   3.282 +by (etac rtranclE 1);
   3.283 +by (Blast_tac 1);
   3.284 +by (blast_tac (claset() addSIs [rtrancl_into_trancl1]) 1);
   3.285 +qed "tranclE";
   3.286 +
   3.287 +(*Transitivity of r^+.
   3.288 +  Proved by unfolding since it uses transitivity of rtrancl. *)
   3.289 +Goalw [trancl_def] "trans(r^+)";
   3.290 +by (rtac transI 1);
   3.291 +by (REPEAT (etac compEpair 1));
   3.292 +by (rtac (rtrancl_into_rtrancl RS (rtrancl_trans RS compI)) 1);
   3.293 +by (REPEAT (assume_tac 1));
   3.294 +qed "trans_trancl";
   3.295 +
   3.296 +bind_thm ("trancl_trans", trans_trancl RS transD);
   3.297 +
   3.298 +Goalw [trancl_def] "[| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+";
   3.299 +by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   3.300 +qed "rtrancl_trancl_trancl";
   3.301 +
   3.302 +(* "[| (a,b) : r;  (b,c) : r^+ |]   ==>  (a,c) : r^+" *)
   3.303 +bind_thm ("trancl_into_trancl2", [trans_trancl, r_into_trancl] MRS transD);
   3.304 +
   3.305 +(* primitive recursion for trancl over finite relations: *)
   3.306 +Goal "(insert (y,x) r)^+ = r^+ Un {(a,b). (a,y):r^* & (x,b):r^*}";
   3.307 +by (rtac equalityI 1);
   3.308 + by (rtac subsetI 1);
   3.309 + by (split_all_tac 1);
   3.310 + by (etac trancl_induct 1);
   3.311 +  by (blast_tac (claset() addIs [r_into_trancl]) 1);
   3.312 + by (blast_tac (claset() addIs
   3.313 +     [rtrancl_into_trancl1,trancl_into_rtrancl,r_into_trancl,trancl_trans]) 1);
   3.314 +by (rtac subsetI 1);
   3.315 +by (blast_tac (claset() addIs
   3.316 +     [rtrancl_into_trancl2, rtrancl_trancl_trancl,
   3.317 +      impOfSubs rtrancl_mono, trancl_mono]) 1);
   3.318 +qed "trancl_insert";
   3.319 +
   3.320 +Goalw [trancl_def] "(r^-1)^+ = (r^+)^-1";
   3.321 +by (simp_tac (simpset() addsimps [rtrancl_converse,converse_comp]) 1);
   3.322 +by (simp_tac (simpset() addsimps [rtrancl_converse RS sym,
   3.323 +				  r_comp_rtrancl_eq]) 1);
   3.324 +qed "trancl_converse";
   3.325 +
   3.326 +Goal "(x,y) : (r^+)^-1 ==> (x,y) : (r^-1)^+";
   3.327 +by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1);
   3.328 +qed "trancl_converseI";
   3.329 +
   3.330 +Goal "(x,y) : (r^-1)^+ ==> (x,y) : (r^+)^-1";
   3.331 +by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1);
   3.332 +qed "trancl_converseD";
   3.333 +
   3.334 +val major::prems = Goal
   3.335 +    "[| (a,b) : r^+; !!y. (y,b) : r ==> P(y); \
   3.336 +\       !!y z.[| (y,z) : r;  (z,b) : r^+;  P(z) |] ==> P(y) |]  \
   3.337 +\     ==> P(a)";
   3.338 +by (rtac ((major RS converseI RS trancl_converseI) RS trancl_induct) 1);
   3.339 + by (resolve_tac prems 1);
   3.340 + by (etac converseD 1);
   3.341 +by (blast_tac (claset() addIs prems addSDs [trancl_converseD])1);
   3.342 +qed "converse_trancl_induct";
   3.343 +
   3.344 +Goal "(x,y):R^+ ==> ? z. (x,z):R & (z,y):R^*";
   3.345 +be converse_trancl_induct 1;
   3.346 +by Auto_tac;
   3.347 +by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   3.348 +qed "tranclD";
   3.349 +
   3.350 +(*Unused*)
   3.351 +Goal "r^-1 Int r^+ = {} ==> (x, x) ~: r^+";
   3.352 +by (subgoal_tac "!y. (x, y) : r^+ --> x~=y" 1);
   3.353 +by (Fast_tac 1);
   3.354 +by (strip_tac 1);
   3.355 +by (etac trancl_induct 1);
   3.356 +by (auto_tac (claset() addIs [r_into_trancl], simpset()));
   3.357 +qed "irrefl_tranclI";
   3.358 +
   3.359 +Goal "!!X. [| !x. (x, x) ~: r^+; (x,y) : r |] ==> x ~= y";
   3.360 +by (blast_tac (claset() addDs [r_into_trancl]) 1);
   3.361 +qed "irrefl_trancl_rD";
   3.362 +
   3.363 +Goal "[| (a,b) : r^*;  r <= A <*> A |] ==> a=b | a:A";
   3.364 +by (etac rtrancl_induct 1);
   3.365 +by Auto_tac;
   3.366 +val lemma = result();
   3.367 +
   3.368 +Goalw [trancl_def] "r <= A <*> A ==> r^+ <= A <*> A";
   3.369 +by (blast_tac (claset() addSDs [lemma]) 1);
   3.370 +qed "trancl_subset_Sigma";
   3.371 +
   3.372 +
   3.373 +Goal "(r^+)^= = r^*";
   3.374 +by Safe_tac;
   3.375 +by  (etac trancl_into_rtrancl 1);
   3.376 +by (blast_tac (claset() addEs [rtranclE] addDs [rtrancl_into_trancl1]) 1);
   3.377 +qed "reflcl_trancl";
   3.378 +Addsimps[reflcl_trancl];
   3.379 +
   3.380 +Goal "(r^=)^+ = r^*";
   3.381 +by Safe_tac;
   3.382 +by  (dtac trancl_into_rtrancl 1);
   3.383 +by  (Asm_full_simp_tac 1);
   3.384 +by (etac rtranclE 1);
   3.385 +by  Safe_tac;
   3.386 +by  (rtac r_into_trancl 1);
   3.387 +by  (Simp_tac 1);
   3.388 +by (rtac rtrancl_into_trancl1 1);
   3.389 +by (etac (rtrancl_reflcl RS equalityD2 RS subsetD) 1);
   3.390 +by (Fast_tac 1);
   3.391 +qed "trancl_reflcl";
   3.392 +Addsimps[trancl_reflcl];
   3.393 +
   3.394 +Goal "{}^+ = {}";
   3.395 +by (auto_tac (claset() addEs [trancl_induct], simpset()));
   3.396 +qed "trancl_empty";
   3.397 +Addsimps[trancl_empty];
   3.398 +
   3.399 +Goal "{}^* = Id";
   3.400 +by (rtac (reflcl_trancl RS subst) 1);
   3.401 +by (Simp_tac 1);
   3.402 +qed "rtrancl_empty";
   3.403 +Addsimps[rtrancl_empty];
   3.404 +
   3.405 +Goal "(a,b):R^* ==> a=b | a~=b & (a,b):R^+";
   3.406 +by(force_tac (claset(), simpset() addsimps [reflcl_trancl RS sym] 
   3.407 +				  delsimps [reflcl_trancl]) 1);
   3.408 +qed "rtranclD";
   3.409 +