src/HOL/UNITY/Common.ML

--- a/src/HOL/UNITY/Common.ML	Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Common.ML	Thu Oct 15 11:35:07 1998 +0200
@@ -11,8 +11,8 @@
 *)
 
 (*Misra's property CMT4: t exceeds no common meeting time*)
-Goal "[| ALL m. Constrains F {m} (maxfg m); n: common |] \
-\     ==> Stable F (atMost n)";
+Goal "[| ALL m. F : Constrains {m} (maxfg m); n: common |] \
+\     ==> F : Stable (atMost n)";
 by (dres_inst_tac [("M", "{t. t<=n}")] Elimination_sing 1);
 by (asm_full_simp_tac
     (simpset() addsimps [atMost_def, Stable_def, common_def, maxfg_def,
@@ -22,39 +22,40 @@
 qed "common_stable";
 
 Goal "[| Init F <= atMost n;  \
-\        ALL m. Constrains F {m} (maxfg m); n: common |] \
-\     ==> Invariant F (atMost n)";
+\        ALL m. F : Constrains {m} (maxfg m); n: common |] \
+\     ==> F : Invariant (atMost n)";
 by (asm_simp_tac (simpset() addsimps [InvariantI, common_stable]) 1);
 qed "common_Invariant";
 
 
 (*** Some programs that implement the safety property above ***)
 
-(*This one is just Skip*)
-Goal "constrains {Id} {m} (maxfg m)";
+Goal "SKIP : constrains {m} (maxfg m)";
 by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj,
-				  fasc, gasc]) 1);
+				  fasc]) 1);
 result();
 
-(*This one is  t := ftime t || t := gtime t    really needs Skip too*)
-Goal "constrains {range(%t.(t,ftime t)), range(%t.(t,gtime t))} \
-\                    {m} (maxfg m)";
+(*This one is  t := ftime t || t := gtime t*)
+Goal "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}) \
+\      : constrains {m} (maxfg m)";
 by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, 
-				  le_max_iff_disj]) 1);
+				  le_max_iff_disj, fasc]) 1);
 by (Blast_tac 1);
 result();
 
-(*This one is  t := max (ftime t) (gtime t)    really needs Skip too*)
-Goal "constrains {range(%t.(t, max (ftime t) (gtime t)))} \
-\                    {m} (maxfg m)";
-by (simp_tac (simpset() addsimps [constrains_def, maxfg_def]) 1);
+(*This one is  t := max (ftime t) (gtime t)*)
+Goal "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}) \
+\      : constrains {m} (maxfg m)";
+by (simp_tac 
+    (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
 by (Blast_tac 1);
 result();
 
 (*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
-Goalw [constrains_def, maxfg_def] 
-    "constrains { {(t, Suc t) | t. t < max (ftime t) (gtime t)} } \
-\               {m} (maxfg m)";
+Goal "mk_program (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }) \
+\      : constrains {m} (maxfg m)";
+by (simp_tac 
+    (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
 by (blast_tac (claset() addIs [Suc_leI]) 1);
 result();
 
@@ -67,10 +68,10 @@
 
 Addsimps [atMost_Int_atLeast];
 
-Goal "[| ALL m. Constrains F {m} (maxfg m); \
-\               ALL m: lessThan n. LeadsTo F {m} (greaterThan m); \
+Goal "[| ALL m. F : Constrains {m} (maxfg m); \
+\               ALL m: lessThan n. F : LeadsTo {m} (greaterThan m); \
 \               n: common |]  \
-\            ==> LeadsTo F (atMost n) common";
+\     ==> F : LeadsTo (atMost n) common";
 by (rtac LeadsTo_weaken_R 1);
 by (res_inst_tac [("f","%x. x"), ("l", "n")] GreaterThan_bounded_induct 1);
 by (ALLGOALS Asm_simp_tac);
@@ -80,10 +81,10 @@
 val lemma = result();
 
 (*The "ALL m: -common" form echoes CMT6.*)
-Goal "[| ALL m. Constrains F {m} (maxfg m); \
-\               ALL m: -common. LeadsTo F {m} (greaterThan m); \
+Goal "[| ALL m. F : Constrains {m} (maxfg m); \
+\               ALL m: -common. F : LeadsTo {m} (greaterThan m); \
 \               n: common |]  \
-\            ==> LeadsTo F (atMost (LEAST n. n: common)) common";
+\            ==> F : LeadsTo (atMost (LEAST n. n: common)) common";
 by (rtac lemma 1);
 by (ALLGOALS Asm_simp_tac);
 by (etac LeastI 2);