src/HOL/UNITY/Comp/Handshake.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 37936 1e4c5015a72e
child 60773 d09c66a0ea10
permissions -rw-r--r--
specialized specification: avoid trivial instances
     1 (*  Title:      HOL/UNITY/Comp/Handshake.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1998  University of Cambridge
     4 
     5 Handshake Protocol
     6 
     7 From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
     8 *)
     9 
    10 theory Handshake imports "../UNITY_Main" begin
    11 
    12 record state =
    13   BB :: bool
    14   NF :: nat
    15   NG :: nat
    16 
    17 definition
    18   (*F's program*)
    19   cmdF :: "(state*state) set"
    20   where "cmdF = {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"
    21 
    22 definition
    23   F :: "state program"
    24   where "F = mk_total_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)"
    25 
    26 definition
    27   (*G's program*)
    28   cmdG :: "(state*state) set"
    29   where "cmdG = {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"
    30 
    31 definition
    32   G :: "state program"
    33   where "G = mk_total_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)"
    34 
    35 definition
    36   (*the joint invariant*)
    37   invFG :: "state set"
    38   where "invFG = {s. NG s <= NF s & NF s <= Suc (NG s) & (BB s = (NF s = NG s))}"
    39 
    40 
    41 declare F_def [THEN def_prg_Init, simp] 
    42         G_def [THEN def_prg_Init, simp]
    43 
    44         cmdF_def [THEN def_act_simp, simp]
    45         cmdG_def [THEN def_act_simp, simp]
    46 
    47         invFG_def [THEN def_set_simp, simp]
    48 
    49 
    50 lemma invFG: "(F Join G) : Always invFG"
    51 apply (rule AlwaysI)
    52 apply force
    53 apply (rule constrains_imp_Constrains [THEN StableI])
    54 apply auto
    55  apply (unfold F_def, safety) 
    56 apply (unfold G_def, safety) 
    57 done
    58 
    59 lemma lemma2_1: "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo  
    60                               ({s. NF s = k} Int {s. BB s})"
    61 apply (rule stable_Join_ensures1[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
    62  apply (unfold F_def, safety) 
    63 apply (unfold G_def, ensures_tac "cmdG") 
    64 done
    65 
    66 lemma lemma2_2: "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo 
    67                               {s. k < NF s}"
    68 apply (rule stable_Join_ensures2[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
    69  apply (unfold F_def, ensures_tac "cmdF") 
    70 apply (unfold G_def, safety) 
    71 done
    72 
    73 lemma progress: "(F Join G) : UNIV LeadsTo {s. m < NF s}"
    74 apply (rule LeadsTo_weaken_R)
    75 apply (rule_tac f = "NF" and l = "Suc m" and B = "{}" 
    76        in GreaterThan_bounded_induct)
    77 (*The inductive step is (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
    78 apply (auto intro!: lemma2_1 lemma2_2
    79             intro: LeadsTo_Trans LeadsTo_Diff simp add: vimage_def)
    80 done
    81 
    82 end