src/HOL/UNITY/Comp/Handshake.thy
author wenzelm
Sat Jun 14 23:19:51 2008 +0200 (2008-06-14)
changeset 27208 5fe899199f85
parent 18556 dc39832e9280
child 36866 426d5781bb25
permissions -rw-r--r--
proper context for tactics derived from res_inst_tac;
     1 (*  Title:      HOL/UNITY/Handshake.thy
     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 theory Handshake imports "../UNITY_Main" begin
    12 
    13 record state =
    14   BB :: bool
    15   NF :: nat
    16   NG :: nat
    17 
    18 constdefs
    19   (*F's program*)
    20   cmdF :: "(state*state) set"
    21     "cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"
    22 
    23   F :: "state program"
    24     "F == mk_total_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)"
    25 
    26   (*G's program*)
    27   cmdG :: "(state*state) set"
    28     "cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"
    29 
    30   G :: "state program"
    31     "G == mk_total_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)"
    32 
    33   (*the joint invariant*)
    34   invFG :: "state set"
    35     "invFG == {s. NG s <= NF s & NF s <= Suc (NG s) & (BB s = (NF s = NG s))}"
    36 
    37 
    38 declare F_def [THEN def_prg_Init, simp] 
    39         G_def [THEN def_prg_Init, simp]
    40 
    41         cmdF_def [THEN def_act_simp, simp]
    42         cmdG_def [THEN def_act_simp, simp]
    43 
    44         invFG_def [THEN def_set_simp, simp]
    45 
    46 
    47 lemma invFG: "(F Join G) : Always invFG"
    48 apply (rule AlwaysI)
    49 apply force
    50 apply (rule constrains_imp_Constrains [THEN StableI])
    51 apply auto
    52  apply (unfold F_def, safety) 
    53 apply (unfold G_def, safety) 
    54 done
    55 
    56 lemma lemma2_1: "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo  
    57                               ({s. NF s = k} Int {s. BB s})"
    58 apply (rule stable_Join_ensures1[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
    59  apply (unfold F_def, safety) 
    60 apply (unfold G_def, ensures_tac "cmdG") 
    61 done
    62 
    63 lemma lemma2_2: "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo 
    64                               {s. k < NF s}"
    65 apply (rule stable_Join_ensures2[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
    66  apply (unfold F_def, ensures_tac "cmdF") 
    67 apply (unfold G_def, safety) 
    68 done
    69 
    70 lemma progress: "(F Join G) : UNIV LeadsTo {s. m < NF s}"
    71 apply (rule LeadsTo_weaken_R)
    72 apply (rule_tac f = "NF" and l = "Suc m" and B = "{}" 
    73        in GreaterThan_bounded_induct)
    74 (*The inductive step is (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
    75 apply (auto intro!: lemma2_1 lemma2_2
    76             intro: LeadsTo_Trans LeadsTo_Diff simp add: vimage_def)
    77 done
    78 
    79 end