src/HOL/UNITY/Common.ML
changeset 4776 1f9362e769c1
child 5069 3ea049f7979d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/UNITY/Common.ML	Fri Apr 03 12:34:33 1998 +0200
     1.3 @@ -0,0 +1,102 @@
     1.4 +(*  Title:      HOL/UNITY/Common
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1998  University of Cambridge
     1.8 +
     1.9 +Common Meeting Time example from Misra (1994)
    1.10 +
    1.11 +The state is identified with the one variable in existence.
    1.12 +
    1.13 +From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
    1.14 +*)
    1.15 +
    1.16 +
    1.17 +open Common;
    1.18 +
    1.19 +(*Misra's property CMT4: t exceeds no common meeting time*)
    1.20 +goal thy
    1.21 +  "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); n: common |] \
    1.22 +\           ==> stable Acts (atMost n)";
    1.23 +by (dres_inst_tac [("P", "%t. t<=n")] elimination_sing 1);
    1.24 +by (asm_full_simp_tac
    1.25 +    (simpset() addsimps [atMost_def, stable_def, common_def, maxfg_def,
    1.26 +			 constrains_def, le_max_iff_disj]) 1);
    1.27 +by (Clarify_tac 1);
    1.28 +by (dtac bspec 1);
    1.29 +by (assume_tac 1);
    1.30 +by (blast_tac (claset() addSEs [subsetCE]
    1.31 +			addIs [order_eq_refl, fmono, gmono, le_trans]) 1);
    1.32 +qed "common_stable";
    1.33 +
    1.34 +goal thy
    1.35 +  "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); n: common |] \
    1.36 +\           ==> reachable {0} Acts <= atMost n";
    1.37 +by (rtac strongest_invariant 1);
    1.38 +by (asm_simp_tac (simpset() addsimps [common_stable]) 2);
    1.39 +by (simp_tac (simpset() addsimps [atMost_def]) 1);
    1.40 +qed "common_invariant";
    1.41 +
    1.42 +
    1.43 +(*** Some programs that implement the safety property above ***)
    1.44 +
    1.45 +(*This one is just Skip*)
    1.46 +goal thy "constrains {id} {m} (maxfg m)";
    1.47 +by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj,
    1.48 +				  fasc, gasc]) 1);
    1.49 +result();
    1.50 +
    1.51 +(*This one is  t := ftime t || t := gtime t    really needs Skip too*)
    1.52 +goal thy "constrains {range(%t.(t,ftime t)), range(%t.(t,gtime t))} \
    1.53 +\                    {m} (maxfg m)";
    1.54 +by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, 
    1.55 +				  le_max_iff_disj]) 1);
    1.56 +by (Blast_tac 1);
    1.57 +result();
    1.58 +
    1.59 +(*This one is  t := max (ftime t) (gtime t)    really needs Skip too*)
    1.60 +goal thy "constrains {range(%t.(t, max (ftime t) (gtime t)))} \
    1.61 +\                    {m} (maxfg m)";
    1.62 +by (simp_tac (simpset() addsimps [constrains_def, maxfg_def]) 1);
    1.63 +by (Blast_tac 1);
    1.64 +result();
    1.65 +
    1.66 +(*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
    1.67 +goalw thy [constrains_def, maxfg_def] 
    1.68 +    "constrains { {(t, Suc t) | t. t < max (ftime t) (gtime t)} } \
    1.69 +\               {m} (maxfg m)";
    1.70 +by (blast_tac (claset() addIs [Suc_leI]) 1);
    1.71 +result();
    1.72 +
    1.73 +
    1.74 +(*It remans to prove that they satisfy CMT3': t does not decrease,
    1.75 +  and that CMT3' implies that t stops changing once common(t) holds.*)
    1.76 +
    1.77 +
    1.78 +(*** Progress under weak fairness ***)
    1.79 +
    1.80 +Addsimps [atMost_Int_atLeast];
    1.81 +
    1.82 +goal thy
    1.83 +    "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); \
    1.84 +\               ALL m: lessThan n. leadsTo Acts {m} (greaterThan m); \
    1.85 +\               n: common;  id: Acts |]  \
    1.86 +\            ==> leadsTo Acts (atMost n) common";
    1.87 +by (rtac leadsTo_weaken_R 1);
    1.88 +by (res_inst_tac [("f","%x. x"), ("l", "n")] greaterThan_bounded_induct 1);
    1.89 +by (ALLGOALS Asm_simp_tac);
    1.90 +by (rtac subset_refl 2);
    1.91 +by (blast_tac (claset() addDs [PSP_stable2] 
    1.92 +                        addIs [common_stable, leadsTo_weaken_R]) 1);
    1.93 +val lemma = result();
    1.94 +
    1.95 +(*The "ALL m: Compl common" form echoes CMT6.*)
    1.96 +goal thy
    1.97 +    "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); \
    1.98 +\               ALL m: Compl common. leadsTo Acts {m} (greaterThan m); \
    1.99 +\               n: common;  id: Acts |]  \
   1.100 +\            ==> leadsTo Acts (atMost (LEAST n. n: common)) common";
   1.101 +by (rtac lemma 1);
   1.102 +by (ALLGOALS Asm_simp_tac);
   1.103 +by (etac LeastI 2);
   1.104 +by (blast_tac (claset() addSDs [not_less_Least]) 1);
   1.105 +qed "leadsTo_common";