src/HOL/UNITY/Handshake.ML

--- a/src/HOL/UNITY/Handshake.ML	Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Handshake.ML	Thu Oct 15 11:35:07 1998 +0200
@@ -11,8 +11,9 @@
 (*split_all_tac causes a big blow-up*)
 claset_ref() := claset() delSWrapper "split_all_tac";
 
-Addsimps [prgF_def RS def_prg_simps];
-Addsimps [prgG_def RS def_prg_simps];
+Addsimps [F_def RS def_prg_Init, G_def RS def_prg_Init];
+program_defs_ref := [F_def, G_def];
+
 Addsimps (map simp_of_act [cmdF_def, cmdG_def]);
 
 (*Simplification for records*)
@@ -20,7 +21,7 @@
 Addsimps [simp_of_set invFG_def];
 
 
-Goal "Invariant (prgF Join prgG) invFG";
+Goal "(F Join G) : Invariant invFG";
 by (rtac InvariantI 1);
 by (Force_tac 1);
 by (rtac (constrains_imp_Constrains RS StableI) 1);
@@ -30,26 +31,26 @@
 by (constrains_tac 1);
 qed "invFG";
 
-Goal "LeadsTo (prgF Join prgG) ({s. NF s = k} - {s. BB s}) \
+Goal "(F Join G) : LeadsTo ({s. NF s = k} - {s. BB s}) \
 \                              ({s. NF s = k} Int {s. BB s})";
 by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
 by (ensures_tac "cmdG" 2);
 by (constrains_tac 1);
 qed "lemma2_1";
 
-Goal "LeadsTo (prgF Join prgG) ({s. NF s = k} Int {s. BB s}) {s. k < NF s}";
+Goal "(F Join G) : LeadsTo ({s. NF s = k} Int {s. BB s}) {s. k < NF s}";
 by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
 by (constrains_tac 2);
 by (ensures_tac "cmdF" 1);
 qed "lemma2_2";
 
 
-Goal "LeadsTo (prgF Join prgG) UNIV {s. m < NF s}";
+Goal "(F Join G) : LeadsTo UNIV {s. m < NF s}";
 by (rtac LeadsTo_weaken_R 1);
 by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")] 
     GreaterThan_bounded_induct 1);
 by (auto_tac (claset(), simpset() addsimps [vimage_def]));
-(*The inductive step: LeadsTo (prgF Join prgG) {x. NF x = ma} {x. ma < NF x}*)
+(*The inductive step: (F Join G) : LeadsTo {x. NF x = ma} {x. ma < NF x}*)
 by (rtac LeadsTo_Diff 1);
 by (rtac lemma2_2 2);
 by (rtac LeadsTo_Trans 1);