src/HOL/UNITY/Common.ML
author paulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 4776 1f9362e769c1
child 5069 3ea049f7979d
permissions -rw-r--r--
New UNITY theory
     1 (*  Title:      HOL/UNITY/Common
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Common Meeting Time example from Misra (1994)
     7 
     8 The state is identified with the one variable in existence.
     9 
    10 From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
    11 *)
    12 
    13 
    14 open Common;
    15 
    16 (*Misra's property CMT4: t exceeds no common meeting time*)
    17 goal thy
    18   "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); n: common |] \
    19 \           ==> stable Acts (atMost n)";
    20 by (dres_inst_tac [("P", "%t. t<=n")] elimination_sing 1);
    21 by (asm_full_simp_tac
    22     (simpset() addsimps [atMost_def, stable_def, common_def, maxfg_def,
    23 			 constrains_def, le_max_iff_disj]) 1);
    24 by (Clarify_tac 1);
    25 by (dtac bspec 1);
    26 by (assume_tac 1);
    27 by (blast_tac (claset() addSEs [subsetCE]
    28 			addIs [order_eq_refl, fmono, gmono, le_trans]) 1);
    29 qed "common_stable";
    30 
    31 goal thy
    32   "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); n: common |] \
    33 \           ==> reachable {0} Acts <= atMost n";
    34 by (rtac strongest_invariant 1);
    35 by (asm_simp_tac (simpset() addsimps [common_stable]) 2);
    36 by (simp_tac (simpset() addsimps [atMost_def]) 1);
    37 qed "common_invariant";
    38 
    39 
    40 (*** Some programs that implement the safety property above ***)
    41 
    42 (*This one is just Skip*)
    43 goal thy "constrains {id} {m} (maxfg m)";
    44 by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj,
    45 				  fasc, gasc]) 1);
    46 result();
    47 
    48 (*This one is  t := ftime t || t := gtime t    really needs Skip too*)
    49 goal thy "constrains {range(%t.(t,ftime t)), range(%t.(t,gtime t))} \
    50 \                    {m} (maxfg m)";
    51 by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, 
    52 				  le_max_iff_disj]) 1);
    53 by (Blast_tac 1);
    54 result();
    55 
    56 (*This one is  t := max (ftime t) (gtime t)    really needs Skip too*)
    57 goal thy "constrains {range(%t.(t, max (ftime t) (gtime t)))} \
    58 \                    {m} (maxfg m)";
    59 by (simp_tac (simpset() addsimps [constrains_def, maxfg_def]) 1);
    60 by (Blast_tac 1);
    61 result();
    62 
    63 (*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
    64 goalw thy [constrains_def, maxfg_def] 
    65     "constrains { {(t, Suc t) | t. t < max (ftime t) (gtime t)} } \
    66 \               {m} (maxfg m)";
    67 by (blast_tac (claset() addIs [Suc_leI]) 1);
    68 result();
    69 
    70 
    71 (*It remans to prove that they satisfy CMT3': t does not decrease,
    72   and that CMT3' implies that t stops changing once common(t) holds.*)
    73 
    74 
    75 (*** Progress under weak fairness ***)
    76 
    77 Addsimps [atMost_Int_atLeast];
    78 
    79 goal thy
    80     "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); \
    81 \               ALL m: lessThan n. leadsTo Acts {m} (greaterThan m); \
    82 \               n: common;  id: Acts |]  \
    83 \            ==> leadsTo Acts (atMost n) common";
    84 by (rtac leadsTo_weaken_R 1);
    85 by (res_inst_tac [("f","%x. x"), ("l", "n")] greaterThan_bounded_induct 1);
    86 by (ALLGOALS Asm_simp_tac);
    87 by (rtac subset_refl 2);
    88 by (blast_tac (claset() addDs [PSP_stable2] 
    89                         addIs [common_stable, leadsTo_weaken_R]) 1);
    90 val lemma = result();
    91 
    92 (*The "ALL m: Compl common" form echoes CMT6.*)
    93 goal thy
    94     "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); \
    95 \               ALL m: Compl common. leadsTo Acts {m} (greaterThan m); \
    96 \               n: common;  id: Acts |]  \
    97 \            ==> leadsTo Acts (atMost (LEAST n. n: common)) common";
    98 by (rtac lemma 1);
    99 by (ALLGOALS Asm_simp_tac);
   100 by (etac LeastI 2);
   101 by (blast_tac (claset() addSDs [not_less_Least]) 1);
   102 qed "leadsTo_common";