--- a/src/HOL/UNITY/Comp/Handshake.thy Fri Jan 24 14:06:49 2003 +0100
+++ b/src/HOL/UNITY/Comp/Handshake.thy Fri Jan 24 18:13:59 2003 +0100
@@ -8,7 +8,7 @@
From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
*)
-Handshake = Union +
+theory Handshake = UNITY_Main:
record state =
BB :: bool
@@ -34,4 +34,46 @@
invFG :: "state set"
"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 Join G) : Always invFG"
+apply (rule AlwaysI)
+apply force
+apply (rule constrains_imp_Constrains [THEN StableI])
+apply auto
+ apply (unfold F_def, constrains)
+apply (unfold G_def, constrains)
+done
+
+lemma lemma2_1: "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo
+ ({s. NF s = k} Int {s. BB s})"
+apply (rule stable_Join_ensures1[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
+ apply (unfold F_def, constrains)
+apply (unfold G_def, ensures_tac "cmdG")
+done
+
+lemma lemma2_2: "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo
+ {s. k < NF s}"
+apply (rule stable_Join_ensures2[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
+ apply (unfold F_def, ensures_tac "cmdF")
+apply (unfold G_def, constrains)
+done
+
+lemma progress: "(F Join G) : UNIV LeadsTo {s. m < NF s}"
+apply (rule LeadsTo_weaken_R)
+apply (rule_tac f = "NF" and l = "Suc m" and B = "{}"
+ in GreaterThan_bounded_induct)
+(*The inductive step is (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
+apply (auto intro!: lemma2_1 lemma2_2
+ intro: LeadsTo_Trans LeadsTo_Diff simp add: vimage_def)
+done
+
end