Tidied
authorpaulson
Wed Aug 05 11:00:21 1998 +0200 (1998-08-05)
changeset 5255e29e77ad7b91
parent 5254 a275d0a3dc08
child 5256 e6983301ce5e
Tidied
src/HOL/Trancl.ML
     1.1 --- a/src/HOL/Trancl.ML	Wed Aug 05 10:59:51 1998 +0200
     1.2 +++ b/src/HOL/Trancl.ML	Wed Aug 05 11:00:21 1998 +0200
     1.3 @@ -225,19 +225,16 @@
     1.4  qed "r_into_trancl";
     1.5  
     1.6  (*intro rule by definition: from rtrancl and r*)
     1.7 -val prems = goalw Trancl.thy [trancl_def]
     1.8 -    "[| (a,b) : r^*;  (b,c) : r |]   ==>  (a,c) : r^+";
     1.9 -by (REPEAT (resolve_tac ([compI]@prems) 1));
    1.10 +Goalw [trancl_def] "[| (a,b) : r^*;  (b,c) : r |]   ==>  (a,c) : r^+";
    1.11 +by Auto_tac;
    1.12  qed "rtrancl_into_trancl1";
    1.13  
    1.14  (*intro rule from r and rtrancl*)
    1.15 -val prems = goal Trancl.thy
    1.16 -    "[| (a,b) : r;  (b,c) : r^* |]   ==>  (a,c) : r^+";
    1.17 -by (resolve_tac (prems RL [rtranclE]) 1);
    1.18 -by (etac subst 1);
    1.19 -by (resolve_tac (prems RL [r_into_trancl]) 1);
    1.20 +Goal "[| (a,b) : r;  (b,c) : r^* |]   ==>  (a,c) : r^+";
    1.21 +by (etac rtranclE 1);
    1.22 +by (blast_tac (claset() addIs [r_into_trancl]) 1);
    1.23  by (rtac (rtrancl_trans RS rtrancl_into_trancl1) 1);
    1.24 -by (REPEAT (ares_tac (prems@[r_into_rtrancl]) 1));
    1.25 +by (REPEAT (ares_tac [r_into_rtrancl] 1));
    1.26  qed "rtrancl_into_trancl2";
    1.27  
    1.28  (*Nice induction rule for trancl*)
    1.29 @@ -280,17 +277,12 @@
    1.30  
    1.31  bind_thm ("trancl_trans", trans_trancl RS transD);
    1.32  
    1.33 -Goalw [trancl_def]
    1.34 -  "[| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+";
    1.35 +Goalw [trancl_def] "[| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+";
    1.36  by (blast_tac (claset() addIs [rtrancl_trans,r_into_rtrancl]) 1);
    1.37  qed "rtrancl_trancl_trancl";
    1.38  
    1.39 -val prems = goal Trancl.thy
    1.40 -    "[| (a,b) : r;  (b,c) : r^+ |]   ==>  (a,c) : r^+";
    1.41 -by (rtac (r_into_trancl RS (trans_trancl RS transD)) 1);
    1.42 -by (resolve_tac prems 1);
    1.43 -by (resolve_tac prems 1);
    1.44 -qed "trancl_into_trancl2";
    1.45 +(* "[| (a,b) : r;  (b,c) : r^+ |]   ==>  (a,c) : r^+" *)
    1.46 +bind_thm ("trancl_into_trancl2", [trans_trancl, r_into_trancl] MRS transD);
    1.47  
    1.48  (* primitive recursion for trancl over finite relations: *)
    1.49  Goal "(insert (y,x) r)^+ = r^+ Un {(a,b). (a,y):r^* & (x,b):r^*}";
    1.50 @@ -319,14 +311,11 @@
    1.51  	 Fast_tac 1,
    1.52  	strip_tac 1,
    1.53  	etac trancl_induct 1,
    1.54 -	 auto_tac (claset() addEs [equals0D, r_into_trancl], simpset())]);
    1.55 +	 auto_tac (claset() addEs [equals0E, r_into_trancl], simpset())]);
    1.56  
    1.57 -val major::prems = goal Trancl.thy
    1.58 -    "[| (a,b) : r^*;  r <= A Times A |] ==> a=b | a:A";
    1.59 -by (cut_facts_tac prems 1);
    1.60 -by (rtac (major RS rtrancl_induct) 1);
    1.61 -by (rtac (refl RS disjI1) 1);
    1.62 -by (Blast_tac 1);
    1.63 +Goal "[| (a,b) : r^*;  r <= A Times A |] ==> a=b | a:A";
    1.64 +by (etac rtrancl_induct 1);
    1.65 +by Auto_tac;
    1.66  val lemma = result();
    1.67  
    1.68  Goalw [trancl_def] "r <= A Times A ==> r^+ <= A Times A";