src/HOL/UNITY/Handshake.ML
changeset 5313 1861a564d7e2
parent 5277 e4297d03e5d2
child 5320 79b326bceafb
     1.1 --- a/src/HOL/UNITY/Handshake.ML	Thu Aug 13 17:44:50 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Handshake.ML	Thu Aug 13 18:06:40 1998 +0200
     1.3 @@ -22,40 +22,40 @@
     1.4  AddIffs [id_in_Acts];
     1.5  
     1.6  
     1.7 -Goalw [prgF_def, prgG_def] "invariant (Join prgF prgG) invFG";
     1.8 -by (rtac invariantI 1);
     1.9 -by (force_tac (claset(), 
    1.10 -	       simpset() addsimps [Join_def]) 1);
    1.11 -by (auto_tac (claset(), simpset() addsimps [stable_Join]));
    1.12 +Goalw [prgF_def, prgG_def] "Invariant (Join prgF prgG) invFG";
    1.13 +by (rtac InvariantI 1);
    1.14 +by (Force_tac 1);
    1.15 +by (rtac (constrains_imp_Constrains RS StableI) 1);
    1.16 +by (auto_tac (claset(), simpset() addsimps [constrains_Join]));
    1.17  by (constrains_tac [prgG_def,cmdG_def] 2);
    1.18  by (auto_tac (claset() addIs [le_anti_sym] addSEs [le_SucE], simpset()));
    1.19  by (constrains_tac [prgF_def,cmdF_def] 1);
    1.20  qed "invFG";
    1.21  
    1.22  Goal "LeadsTo (Join prgF prgG) {s. NF s = k & ~ BB s} {s. NF s = k & BB s}";
    1.23 -br (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1;
    1.24 +by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
    1.25  by (ensures_tac [prgG_def,cmdG_def] "cmdG" 2);
    1.26  by (constrains_tac [prgF_def,cmdF_def] 1);
    1.27  qed "lemma2_1";
    1.28  
    1.29  Goal "LeadsTo (Join prgF prgG) {s. NF s = k & BB s} {s. k < NF s}";
    1.30 -br (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1;
    1.31 +by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
    1.32  by (constrains_tac [prgG_def,cmdG_def] 2);
    1.33  by (ensures_tac [prgF_def,cmdF_def] "cmdF" 1);
    1.34  qed "lemma2_2";
    1.35  
    1.36  
    1.37  Goal "LeadsTo (Join prgF prgG) UNIV {s. m < NF s}";
    1.38 -br LeadsTo_weaken_R 1;
    1.39 +by (rtac LeadsTo_weaken_R 1);
    1.40  by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")] 
    1.41      GreaterThan_bounded_induct 1);
    1.42  by (auto_tac (claset(), simpset() addsimps [vimage_def]));
    1.43  by (trans_tac 2);
    1.44  (*The inductive step: LeadsTo (Join prgF prgG) {x. NF x = ma} {x. ma < NF x}*)
    1.45 -br LeadsTo_Diff 1;
    1.46 -br lemma2_2 2;
    1.47 -br LeadsTo_Trans 1;
    1.48 -br lemma2_2 2;
    1.49 -br (lemma2_1 RS LeadsTo_weaken_L) 1;
    1.50 +by (rtac LeadsTo_Diff 1);
    1.51 +by (rtac lemma2_2 2);
    1.52 +by (rtac LeadsTo_Trans 1);
    1.53 +by (rtac lemma2_2 2);
    1.54 +by (rtac (lemma2_1 RS LeadsTo_weaken_L) 1);
    1.55  by Auto_tac;
    1.56  qed "progress";