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
5 Handshake Protocol
7 From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
8 *)
10 theory Handshake imports "../UNITY_Main" begin
12 record state =
13   BB :: bool
14   NF :: nat
15   NG :: nat
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}"
22 definition
23   F :: "state program"
24   where "F = mk_total_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)"
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}"
31 definition
32   G :: "state program"
33   where "G = mk_total_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)"
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))}"
41 declare F_def [THEN def_prg_Init, simp]
42         G_def [THEN def_prg_Init, simp]
44         cmdF_def [THEN def_act_simp, simp]
45         cmdG_def [THEN def_act_simp, simp]
47         invFG_def [THEN def_set_simp, simp]
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
59 lemma lemma2_1: "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo
60                               ({s. NF s = k} Int {s. BB s})"
62  apply (unfold F_def, safety)
63 apply (unfold G_def, ensures_tac "cmdG")
64 done
66 lemma lemma2_2: "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo
67                               {s. k < NF s}"