src/HOL/UNITY/Common.ML
changeset 5313 1861a564d7e2
parent 5277 e4297d03e5d2
child 5490 85855f65d0c6
     1.1 --- a/src/HOL/UNITY/Common.ML	Thu Aug 13 17:44:50 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Common.ML	Thu Aug 13 18:06:40 1998 +0200
     1.3 @@ -11,25 +11,21 @@
     1.4  *)
     1.5  
     1.6  (*Misra's property CMT4: t exceeds no common meeting time*)
     1.7 -Goal "[| ALL m. constrains acts {m} (maxfg m); n: common |] \
     1.8 -\     ==> stable acts (atMost n)";
     1.9 -by (dres_inst_tac [("P", "%t. t<=n")] elimination_sing 1);
    1.10 +Goal "[| ALL m. Constrains prg {m} (maxfg m); n: common |] \
    1.11 +\     ==> Stable prg (atMost n)";
    1.12 +by (dres_inst_tac [("M", "{t. t<=n}")] Elimination_sing 1);
    1.13  by (asm_full_simp_tac
    1.14 -    (simpset() addsimps [atMost_def, stable_def, common_def, maxfg_def,
    1.15 -			 constrains_def, le_max_iff_disj]) 1);
    1.16 -by (Clarify_tac 1);
    1.17 -by (dtac bspec 1);
    1.18 -by (assume_tac 1);
    1.19 -by (blast_tac (claset() addSEs [subsetCE]
    1.20 -			addIs [order_eq_refl, fmono, gmono, le_trans]) 1);
    1.21 +    (simpset() addsimps [atMost_def, Stable_def, common_def, maxfg_def,
    1.22 +			 le_max_iff_disj]) 1);
    1.23 +by (etac Constrains_weaken_R 1);
    1.24 +by (blast_tac (claset() addIs [order_eq_refl, fmono, gmono, le_trans]) 1);
    1.25  qed "common_stable";
    1.26  
    1.27 -Goal "[| ALL m. constrains acts {m} (maxfg m); n: common |] \
    1.28 -\     ==> invariant (|Init={0}, Acts=acts|) (atMost n)";
    1.29 -by (rtac invariantI 1);
    1.30 -by (asm_simp_tac (simpset() addsimps [common_stable]) 2);
    1.31 -by (simp_tac (simpset() addsimps [atMost_def]) 1);
    1.32 -qed "common_invariant";
    1.33 +Goal "[| Init prg <= atMost n;  \
    1.34 +\        ALL m. Constrains prg {m} (maxfg m); n: common |] \
    1.35 +\     ==> Invariant prg (atMost n)";
    1.36 +by (asm_simp_tac (simpset() addsimps [InvariantI, common_stable]) 1);
    1.37 +qed "common_Invariant";
    1.38  
    1.39  
    1.40  (*** Some programs that implement the safety property above ***)
    1.41 @@ -71,23 +67,23 @@
    1.42  
    1.43  Addsimps [atMost_Int_atLeast];
    1.44  
    1.45 -Goal "[| ALL m. constrains acts {m} (maxfg m); \
    1.46 -\               ALL m: lessThan n. leadsTo acts {m} (greaterThan m); \
    1.47 -\               n: common;  id: acts |]  \
    1.48 -\            ==> leadsTo acts (atMost n) common";
    1.49 -by (rtac leadsTo_weaken_R 1);
    1.50 -by (res_inst_tac [("f","%x. x"), ("l", "n")] greaterThan_bounded_induct 1);
    1.51 +Goal "[| ALL m. Constrains prg {m} (maxfg m); \
    1.52 +\               ALL m: lessThan n. LeadsTo prg {m} (greaterThan m); \
    1.53 +\               n: common;  id: Acts prg |]  \
    1.54 +\            ==> LeadsTo prg (atMost n) common";
    1.55 +by (rtac LeadsTo_weaken_R 1);
    1.56 +by (res_inst_tac [("f","%x. x"), ("l", "n")] GreaterThan_bounded_induct 1);
    1.57  by (ALLGOALS Asm_simp_tac);
    1.58  by (rtac subset_refl 2);
    1.59 -by (blast_tac (claset() addDs [psp_stable2] 
    1.60 -                        addIs [common_stable, leadsTo_weaken_R]) 1);
    1.61 +by (blast_tac (claset() addDs [PSP_stable2] 
    1.62 +                        addIs [common_stable, LeadsTo_weaken_R]) 1);
    1.63  val lemma = result();
    1.64  
    1.65  (*The "ALL m: Compl common" form echoes CMT6.*)
    1.66 -Goal "[| ALL m. constrains acts {m} (maxfg m); \
    1.67 -\               ALL m: Compl common. leadsTo acts {m} (greaterThan m); \
    1.68 -\               n: common;  id: acts |]  \
    1.69 -\            ==> leadsTo acts (atMost (LEAST n. n: common)) common";
    1.70 +Goal "[| ALL m. Constrains prg {m} (maxfg m); \
    1.71 +\               ALL m: Compl common. LeadsTo prg {m} (greaterThan m); \
    1.72 +\               n: common;  id: Acts prg |]  \
    1.73 +\            ==> LeadsTo prg (atMost (LEAST n. n: common)) common";
    1.74  by (rtac lemma 1);
    1.75  by (ALLGOALS Asm_simp_tac);
    1.76  by (etac LeastI 2);