src/HOL/UNITY/Handshake.ML
author paulson
Thu Aug 13 18:06:40 1998 +0200 (1998-08-13)
changeset 5313 1861a564d7e2
parent 5277 e4297d03e5d2
child 5320 79b326bceafb
permissions -rw-r--r--
Constrains, Stable, Invariant...more of the substitution axiom, but Union
does not work well with them
     1 (*  Title:      HOL/UNITY/Handshake
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Handshake Protocol
     7 
     8 From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
     9 *)
    10 
    11 (*split_all_tac causes a big blow-up*)
    12 claset_ref() := claset() delSWrapper "split_all_tac";
    13 
    14 (*Simplification for records*)
    15 Addsimps (thms"state.update_defs");
    16 Addsimps [invFG_def];
    17 
    18 
    19 Goalw [prgF_def, Join_def] "id : Acts (Join prgF prgG) ";
    20 by (Simp_tac 1);
    21 qed "id_in_Acts";
    22 AddIffs [id_in_Acts];
    23 
    24 
    25 Goalw [prgF_def, prgG_def] "Invariant (Join prgF prgG) invFG";
    26 by (rtac InvariantI 1);
    27 by (Force_tac 1);
    28 by (rtac (constrains_imp_Constrains RS StableI) 1);
    29 by (auto_tac (claset(), simpset() addsimps [constrains_Join]));
    30 by (constrains_tac [prgG_def,cmdG_def] 2);
    31 by (auto_tac (claset() addIs [le_anti_sym] addSEs [le_SucE], simpset()));
    32 by (constrains_tac [prgF_def,cmdF_def] 1);
    33 qed "invFG";
    34 
    35 Goal "LeadsTo (Join prgF prgG) {s. NF s = k & ~ BB s} {s. NF s = k & BB s}";
    36 by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
    37 by (ensures_tac [prgG_def,cmdG_def] "cmdG" 2);
    38 by (constrains_tac [prgF_def,cmdF_def] 1);
    39 qed "lemma2_1";
    40 
    41 Goal "LeadsTo (Join prgF prgG) {s. NF s = k & BB s} {s. k < NF s}";
    42 by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
    43 by (constrains_tac [prgG_def,cmdG_def] 2);
    44 by (ensures_tac [prgF_def,cmdF_def] "cmdF" 1);
    45 qed "lemma2_2";
    46 
    47 
    48 Goal "LeadsTo (Join prgF prgG) UNIV {s. m < NF s}";
    49 by (rtac LeadsTo_weaken_R 1);
    50 by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")] 
    51     GreaterThan_bounded_induct 1);
    52 by (auto_tac (claset(), simpset() addsimps [vimage_def]));
    53 by (trans_tac 2);
    54 (*The inductive step: LeadsTo (Join prgF prgG) {x. NF x = ma} {x. ma < NF x}*)
    55 by (rtac LeadsTo_Diff 1);
    56 by (rtac lemma2_2 2);
    57 by (rtac LeadsTo_Trans 1);
    58 by (rtac lemma2_2 2);
    59 by (rtac (lemma2_1 RS LeadsTo_weaken_L) 1);
    60 by Auto_tac;
    61 qed "progress";