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