src/HOL/UNITY/Handshake.ML
changeset 7403 c318acb88251
parent 7221 13e43b7456a1
child 7523 3a716ebc2fc0
     1.1 --- a/src/HOL/UNITY/Handshake.ML	Wed Sep 01 11:15:35 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Handshake.ML	Wed Sep 01 11:16:02 1999 +0200
     1.3 @@ -30,14 +30,12 @@
     1.4  by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
     1.5  by (ensures_tac "cmdG" 2);
     1.6  by (constrains_tac 1);
     1.7 -by Auto_tac;
     1.8  qed "lemma2_1";
     1.9  
    1.10  Goal "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo {s. k < NF s}";
    1.11  by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
    1.12  by (constrains_tac 2);
    1.13  by (ensures_tac "cmdF" 1);
    1.14 -by Auto_tac;
    1.15  qed "lemma2_2";
    1.16  
    1.17  
    1.18 @@ -45,11 +43,8 @@
    1.19  by (rtac LeadsTo_weaken_R 1);
    1.20  by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")] 
    1.21      GreaterThan_bounded_induct 1);
    1.22 -by (auto_tac (claset(), simpset() addsimps [vimage_def]));
    1.23 -(*The inductive step: (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
    1.24 -by (rtac LeadsTo_Diff 1);
    1.25 -by (rtac lemma2_2 2);
    1.26 -by (rtac LeadsTo_Trans 1);
    1.27 -by (rtac lemma2_2 2);
    1.28 -by (rtac lemma2_1 1);
    1.29 +(*The inductive step is (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
    1.30 +by (auto_tac (claset() addSIs [lemma2_1, lemma2_2] 
    1.31 +	               addIs[LeadsTo_Trans, LeadsTo_Diff], 
    1.32 +	      simpset() addsimps [vimage_def]));
    1.33  qed "progress";