# Theory Handshake

theory Handshake
imports UNITY_Main
```(*  Title:      HOL/UNITY/Comp/Handshake.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

Handshake Protocol

From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
*)

theory Handshake imports "../UNITY_Main" begin

record state =
BB :: bool
NF :: nat
NG :: nat

definition
(*F's program*)
cmdF :: "(state*state) set"
where "cmdF = {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"

definition
F :: "state program"
where "F = mk_total_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)"

definition
(*G's program*)
cmdG :: "(state*state) set"
where "cmdG = {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"

definition
G :: "state program"
where "G = mk_total_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)"

definition
(*the joint invariant*)
invFG :: "state set"
where "invFG = {s. NG s <= NF s & NF s <= Suc (NG s) & (BB s = (NF s = NG s))}"

declare F_def [THEN def_prg_Init, simp]
G_def [THEN def_prg_Init, simp]

cmdF_def [THEN def_act_simp, simp]
cmdG_def [THEN def_act_simp, simp]

invFG_def [THEN def_set_simp, simp]

lemma invFG: "(F ⊔ G) ∈ Always invFG"
apply (rule AlwaysI)
apply force
apply (rule constrains_imp_Constrains [THEN StableI])
apply auto
apply (unfold F_def, safety)
apply (unfold G_def, safety)
done

lemma lemma2_1: "(F ⊔ G) ∈ ({s. NF s = k} - {s. BB s}) LeadsTo
({s. NF s = k} Int {s. BB s})"
apply (unfold F_def, safety)
apply (unfold G_def, ensures_tac "cmdG")
done

lemma lemma2_2: "(F ⊔ G) ∈ ({s. NF s = k} Int {s. BB s}) LeadsTo
{s. k < NF s}"
apply (unfold F_def, ensures_tac "cmdF")
apply (unfold G_def, safety)
done

lemma progress: "(F ⊔ G) ∈ UNIV LeadsTo {s. m < NF s}"