1(*  Title:      HOL/UNITY/Comp/Handshake.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1998  University of Cambridge
4
5Handshake Protocol
6
7From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
8*)
9
10theory Handshake imports "../UNITY_Main" begin
11
12record state =
13  BB :: bool
14  NF :: nat
15  NG :: nat
16
17definition
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
22definition
23  F :: "state program"
24  where "F = mk_total_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)"
25
26definition
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
31definition
32  G :: "state program"
33  where "G = mk_total_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)"
34
35definition
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
41declare 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
50lemma invFG: "(F \<squnion> G) \<in> Always invFG"
51apply (rule AlwaysI)
52apply force
53apply (rule constrains_imp_Constrains [THEN StableI])
54apply auto
55 apply (unfold F_def, safety) 
56apply (unfold G_def, safety) 
57done
58
59lemma lemma2_1: "(F \<squnion> G) \<in> ({s. NF s = k} - {s. BB s}) LeadsTo  
60                              ({s. NF s = k} Int {s. BB s})"
61apply (rule stable_Join_ensures1[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
62 apply (unfold F_def, safety) 
63apply (unfold G_def, ensures_tac "cmdG") 
64done
65
66lemma lemma2_2: "(F \<squnion> G) \<in> ({s. NF s = k} Int {s. BB s}) LeadsTo 
67                              {s. k < NF s}"
68apply (rule stable_Join_ensures2[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
69 apply (unfold F_def, ensures_tac "cmdF") 
70apply (unfold G_def, safety) 
71done
72
73lemma progress: "(F \<squnion> G) \<in> UNIV LeadsTo {s. m < NF s}"
74apply (rule LeadsTo_weaken_R)
75apply (rule_tac f = "NF" and l = "Suc m" and B = "{}" 
76       in GreaterThan_bounded_induct)
77(*The inductive step is (F \<squnion> G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
78apply (auto intro!: lemma2_1 lemma2_2
79            intro: LeadsTo_Trans LeadsTo_Diff simp add: vimage_def)
80done
81
82end
83