src/HOL/UNITY/Common.ML
author paulson
Thu Aug 13 18:06:40 1998 +0200 (1998-08-13)
changeset 5313 1861a564d7e2
parent 5277 e4297d03e5d2
child 5490 85855f65d0c6
permissions -rw-r--r--
Constrains, Stable, Invariant...more of the substitution axiom, but Union
does not work well with them
     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 (*Misra's property CMT4: t exceeds no common meeting time*)
    14 Goal "[| ALL m. Constrains prg {m} (maxfg m); n: common |] \
    15 \     ==> Stable prg (atMost n)";
    16 by (dres_inst_tac [("M", "{t. t<=n}")] Elimination_sing 1);
    17 by (asm_full_simp_tac
    18     (simpset() addsimps [atMost_def, Stable_def, common_def, maxfg_def,
    19 			 le_max_iff_disj]) 1);
    20 by (etac Constrains_weaken_R 1);
    21 by (blast_tac (claset() addIs [order_eq_refl, fmono, gmono, le_trans]) 1);
    22 qed "common_stable";
    23 
    24 Goal "[| Init prg <= atMost n;  \
    25 \        ALL m. Constrains prg {m} (maxfg m); n: common |] \
    26 \     ==> Invariant prg (atMost n)";
    27 by (asm_simp_tac (simpset() addsimps [InvariantI, common_stable]) 1);
    28 qed "common_Invariant";
    29 
    30 
    31 (*** Some programs that implement the safety property above ***)
    32 
    33 (*This one is just Skip*)
    34 Goal "constrains {id} {m} (maxfg m)";
    35 by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj,
    36 				  fasc, gasc]) 1);
    37 result();
    38 
    39 (*This one is  t := ftime t || t := gtime t    really needs Skip too*)
    40 Goal "constrains {range(%t.(t,ftime t)), range(%t.(t,gtime t))} \
    41 \                    {m} (maxfg m)";
    42 by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, 
    43 				  le_max_iff_disj]) 1);
    44 by (Blast_tac 1);
    45 result();
    46 
    47 (*This one is  t := max (ftime t) (gtime t)    really needs Skip too*)
    48 Goal "constrains {range(%t.(t, max (ftime t) (gtime t)))} \
    49 \                    {m} (maxfg m)";
    50 by (simp_tac (simpset() addsimps [constrains_def, maxfg_def]) 1);
    51 by (Blast_tac 1);
    52 result();
    53 
    54 (*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
    55 Goalw [constrains_def, maxfg_def] 
    56     "constrains { {(t, Suc t) | t. t < max (ftime t) (gtime t)} } \
    57 \               {m} (maxfg m)";
    58 by (blast_tac (claset() addIs [Suc_leI]) 1);
    59 result();
    60 
    61 
    62 (*It remans to prove that they satisfy CMT3': t does not decrease,
    63   and that CMT3' implies that t stops changing once common(t) holds.*)
    64 
    65 
    66 (*** Progress under weak fairness ***)
    67 
    68 Addsimps [atMost_Int_atLeast];
    69 
    70 Goal "[| ALL m. Constrains prg {m} (maxfg m); \
    71 \               ALL m: lessThan n. LeadsTo prg {m} (greaterThan m); \
    72 \               n: common;  id: Acts prg |]  \
    73 \            ==> LeadsTo prg (atMost n) common";
    74 by (rtac LeadsTo_weaken_R 1);
    75 by (res_inst_tac [("f","%x. x"), ("l", "n")] GreaterThan_bounded_induct 1);
    76 by (ALLGOALS Asm_simp_tac);
    77 by (rtac subset_refl 2);
    78 by (blast_tac (claset() addDs [PSP_stable2] 
    79                         addIs [common_stable, LeadsTo_weaken_R]) 1);
    80 val lemma = result();
    81 
    82 (*The "ALL m: Compl common" form echoes CMT6.*)
    83 Goal "[| ALL m. Constrains prg {m} (maxfg m); \
    84 \               ALL m: Compl common. LeadsTo prg {m} (greaterThan m); \
    85 \               n: common;  id: Acts prg |]  \
    86 \            ==> LeadsTo prg (atMost (LEAST n. n: common)) common";
    87 by (rtac lemma 1);
    88 by (ALLGOALS Asm_simp_tac);
    89 by (etac LeastI 2);
    90 by (blast_tac (claset() addSDs [not_less_Least]) 1);
    91 qed "leadsTo_common";