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