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