src/ZF/UNITY/Mutex.ML

--- a/src/ZF/UNITY/Mutex.ML	Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/Mutex.ML	Tue May 27 11:39:03 2003 +0200
@@ -13,41 +13,44 @@
 
 (** Variables' types **)
 
-AddIffs  [p_type, u_type, v_type, m_type, n_type];
+Addsimps  [p_type, u_type, v_type, m_type, n_type];
 
-Goal "!!s. s:state ==> s`u:bool";
-by (dres_inst_tac [("a", "u"), ("A", "var")] apply_type 1);
+Goalw [state_def] "s:state ==>s`u:bool";
+by (dres_inst_tac [("a", "u")] apply_type 1);
 by Auto_tac;
-qed "u_apply_type";
+qed "u_value_type";
 
-Goal "!!s. s:state ==> s`v:bool";
-by (dres_inst_tac [("a", "v"), ("A", "var")] apply_type 1);
+Goalw [state_def] "s:state ==> s`v:bool";
+by (dres_inst_tac [("a", "v")] apply_type 1);
 by Auto_tac;
-qed "v_apply_type";
+qed "v_value_type";
 
-Goal "!!s. s:state ==> s`p:bool";
-by (dres_inst_tac [("a", "p"), ("A", "var")] apply_type 1);
+Goalw [state_def] "s:state ==> s`p:bool";
+by (dres_inst_tac [("a", "p")] apply_type 1);
 by Auto_tac;
-qed "p_apply_type";
+qed "p_value_type";
 
-Goal "!!s. s:state ==> s`m:int";
-by (dres_inst_tac [("a", "m"), ("A", "var")] apply_type 1);
+Goalw [state_def] "s:state ==> s`m:int";
+by (dres_inst_tac [("a", "m")] apply_type 1);
 by Auto_tac;
-qed "m_apply_type";
+qed "m_value_type";
 
-Goal "!!s. s:state ==> s`n:int";
-by (dres_inst_tac [("a", "n"), ("A", "var")] apply_type 1);
+Goalw [state_def] "s:state ==>s`n:int";
+by (dres_inst_tac [("a", "n")] apply_type 1);
 by Auto_tac;
-qed "n_apply_type";
-Addsimps [p_apply_type, u_apply_type, v_apply_type,
-          m_apply_type, n_apply_type];
+qed "n_value_type";
 
+Addsimps [p_value_type, u_value_type, v_value_type,
+          m_value_type, n_value_type];
+AddTCs [p_value_type, u_value_type, v_value_type,
+          m_value_type, n_value_type];
 (** Mutex is a program **)
 
 Goalw [Mutex_def] "Mutex:program";
 by Auto_tac;
 qed "Mutex_in_program";
-AddIffs [Mutex_in_program];
+Addsimps [Mutex_in_program];
+AddTCs [Mutex_in_program];
 
 Addsimps [Mutex_def RS def_prg_Init];
 program_defs_ref := [Mutex_def];
@@ -61,11 +64,6 @@
 
 Addsimps (map simp_of_set [IU_def, IV_def, bad_IU_def]);
 
-(** In case one wants to be sure that the initial state is not empty **)
-Goal "some(u:=0,v:=0, m:= #0,n:= #0):Init(Mutex)";
-by (auto_tac (claset() addSIs [update_type2], simpset()));
-qed "Mutex_Init_not_empty";
-
 Goal "Mutex : Always(IU)";
 by (always_tac 1);
 by Auto_tac;
@@ -75,7 +73,6 @@
 by (always_tac 1);
 qed "IV";
 
-
 (*The safety property: mutual exclusion*)
 Goal "Mutex : Always({s:state. ~(s`m = #3 & s`n = #3)})";
 by (rtac ([IU, IV] MRS Always_Int_I RS Always_weaken) 1);
@@ -93,7 +90,7 @@
 Goal "Mutex : Always(bad_IU)";
 by (always_tac 1);
 by (auto_tac (claset(), simpset() addsimps [not_zle_iff_zless]));
-by (auto_tac (claset() addSDs [u_apply_type], simpset() addsimps [bool_def]));
+by (auto_tac (claset(), simpset() addsimps [bool_def]));
 by (subgoal_tac "#1 $<= #3" 1);
 by (dres_inst_tac [("x", "#1"), ("y", "#3")] zle_trans 1);
 by Auto_tac;
@@ -134,7 +131,7 @@
           MRS LeadsTo_Diff) 1);
 by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
 by Auto_tac;
-by (auto_tac (claset() addSDs [p_apply_type], simpset() addsimps [bool_def]));
+by (auto_tac (claset() addSDs [p_value_type], simpset() addsimps [bool_def]));
 val U_lemma2 = result();
 
 Goal "Mutex : {s:state. s`m = #1} LeadsTo {s:state. s`p =1}";
@@ -156,7 +153,7 @@
 
 
 Goal "Mutex : {s:state. #1 $<= s`m & s`m $<= #3} LeadsTo {s:state. s`p=1}";
-by (simp_tac (simpset() addsimps [m_apply_type RS eq_123, Collect_disj_eq,
+by (simp_tac (simpset() addsimps [m_value_type RS eq_123, Collect_disj_eq,
                                   LeadsTo_Un_distrib,
                                   U_lemma1, U_lemma2, U_F3] ) 1);
 val U_lemma123 = result();
@@ -178,7 +175,6 @@
 
 Goal "Mutex : {s:state. s`n=#1} LeadsTo {s:state. s`p = not(s`u) & s`n = #2}";
 by (ensures_tac "V1" 1);
-by (auto_tac (claset() addIs [not_type], simpset()));
 qed "V_F1";
 
 Goal "Mutex : {s:state. s`p=1 & s`n = #2} LeadsTo {s:state. s`n = #3}";
@@ -192,13 +188,12 @@
 by (ensures_tac "V3" 1);
 qed "V_F3";
 
-
 Goal "Mutex : {s:state. s`n = #2} LeadsTo {s:state. s`p=0}";
 by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] 
           MRS LeadsTo_Diff) 1);
 by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
 by Auto_tac;
-by (auto_tac (claset() addSDs [p_apply_type], simpset() addsimps [bool_def]));
+by (auto_tac (claset() addSDs [p_value_type], simpset() addsimps [bool_def]));
 val V_lemma2 = result();
 
 Goal "Mutex : {s:state. s`n = #1} LeadsTo {s:state. s`p = 0}";
@@ -208,11 +203,10 @@
 
 Goal "Mutex : {s:state. #1 $<= s`n & s`n $<= #3} LeadsTo {s:state. s`p = 0}";
 by (simp_tac (simpset() addsimps 
-     [n_apply_type RS eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
+     [n_value_type RS eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
                   V_lemma1, V_lemma2, V_F3] ) 1);
 val V_lemma123 = result();
 
-
 (*Misra's F4*)
 Goal "Mutex : {s:state. s`v = 1} LeadsTo {s:state. s`p = 0}";
 by (rtac ([IV, V_lemma123] MRS Always_LeadsTo_weaken) 1);
@@ -231,7 +225,7 @@
 by (rtac ([v_Leadsto_not_p, U_F0] MRS PSP_Unless) 2);
 by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
 by Auto_tac;
-by (auto_tac (claset() addSDs [v_apply_type], simpset() addsimps [bool_def]));
+by (auto_tac (claset() addSDs [v_value_type], simpset() addsimps [bool_def]));
 qed "m1_Leadsto_3";
 
 
@@ -245,5 +239,5 @@
 by (rtac ([u_Leadsto_p, V_F0] MRS PSP_Unless) 2);
 by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
 by Auto_tac;
-by (auto_tac (claset() addSDs [u_apply_type], simpset() addsimps [bool_def]));
+by (auto_tac (claset() addSDs [u_value_type], simpset() addsimps [bool_def]));
 qed "n1_Leadsto_3";