--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Handshake.ML Wed Aug 05 10:56:58 1998 +0200
@@ -0,0 +1,62 @@
+(* Title: HOL/UNITY/Handshake
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Handshake Protocol
+
+From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
+*)
+
+(*split_all_tac causes a big blow-up*)
+claset_ref() := claset() delSWrapper "split_all_tac";
+
+(*Simplification for records*)
+Addsimps (thms"state.update_defs");
+Addsimps [invFG_def];
+
+
+Goalw [prgF_def, Join_def] "id : Acts (Join prgF prgG) ";
+by (Simp_tac 1);
+qed "id_in_Acts";
+AddIffs [id_in_Acts];
+
+
+Goalw [prgF_def, prgG_def] "invariant (Join prgF prgG) invFG";
+by (rtac invariantI 1);
+by (force_tac (claset(),
+ simpset() addsimps [Join_def]) 1);
+by (auto_tac (claset(), simpset() addsimps [stable_Join]));
+by (constrains_tac [prgG_def,cmdG_def] 2);
+by (auto_tac (claset() addIs [le_anti_sym] addSEs [le_SucE], simpset()));
+by (constrains_tac [prgF_def,cmdF_def] 1);
+qed "invFG";
+
+Goal "LeadsTo (Join prgF prgG) {s. NF s = k & ~ BB s} {s. NF s = k & BB s}";
+br (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1;
+by (ensures_tac [prgG_def,cmdG_def] "cmdG" 2);
+by (constrains_tac [prgF_def,cmdF_def] 1);
+qed "lemma2_1";
+
+Goal "LeadsTo (Join prgF prgG) {s. NF s = k & BB s} {s. k < NF s}";
+br (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1;
+by (constrains_tac [prgG_def,cmdG_def] 2);
+by (ensures_tac [prgF_def,cmdF_def] "cmdF" 1);
+qed "lemma2_2";
+
+
+Goal "LeadsTo (Join prgF prgG) {s. NF s = k} {s. k < NF s}";
+br LeadsTo_Diff 1;
+br lemma2_2 2;
+br LeadsTo_Trans 1;
+br lemma2_2 2;
+br (lemma2_1 RS LeadsTo_weaken_L) 1;
+by Auto_tac;
+val lemma = result();
+
+
+Goal "LeadsTo (Join prgF prgG) UNIV {s. m < NF s}";
+by (res_inst_tac [("f", "NF")] R_lessThan_induct 1);
+auto();
+br (lemma RS LeadsTo_weaken) 1;
+auto();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Handshake.thy Wed Aug 05 10:56:58 1998 +0200
@@ -0,0 +1,39 @@
+(* Title: HOL/UNITY/Handshake.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Handshake Protocol
+
+From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
+*)
+
+Handshake = Union +
+
+record state =
+ BB :: bool
+ NF :: nat
+ NG :: nat
+
+constdefs
+ (*F's program*)
+ cmdF :: "(state*state) set"
+ "cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"
+
+ prgF :: "state program"
+ "prgF == (|Init = {s. NF s = 0 & BB s},
+ Acts = {id, cmdF}|)"
+
+ (*G's program*)
+ cmdG :: "(state*state) set"
+ "cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"
+
+ prgG :: "state program"
+ "prgG == (|Init = {s. NG s = 0 & BB s},
+ Acts = {id, cmdG}|)"
+
+ (*the joint invariant*)
+ invFG :: "state set"
+ "invFG == {s. NG s <= NF s & NF s <= Suc (NG s) & (BB s = (NF s = NG s))}"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Union.ML Wed Aug 05 10:56:58 1998 +0200
@@ -0,0 +1,117 @@
+(* Title: HOL/UNITY/Union.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Unions of programs
+
+From Misra's Chapter 5: Asynchronous Compositions of Programs
+
+NOT CLEAR WHETHER ALL THESE FORMS ARE NEEDED:
+ Maybe Join instead of Un, and JOIN for UNION
+*)
+
+(*** Safety: constrains, stable, FP ***)
+
+Goalw [constrains_def]
+ "constrains (UN i:I. acts i) A B = (ALL i:I. constrains (acts i) A B)";
+by (Blast_tac 1);
+qed "constrains_UN";
+
+Goalw [constrains_def]
+ "constrains (actsF Un actsG) A B = \
+\ (constrains actsF A B & constrains actsG A B)";
+by (simp_tac (simpset() addsimps [ball_Un]) 1);
+qed "constrains_Un";
+
+(*Provable by constrains_Un and constrains_weaken, but why bother?*)
+Goalw [constrains_def]
+ "[| constrains actsF A A'; constrains actsG B B' |] \
+\ ==> constrains (actsF Un actsG) (A Int B) (A' Un B')";
+by (Blast_tac 1);
+qed "constrains_Un_weaken";
+
+Goalw [stable_def] "stable (UN i:I. acts i) A = (ALL i:I. stable (acts i) A)";
+by (simp_tac (simpset() addsimps [constrains_UN]) 1);
+qed "stable_UN";
+
+Goalw [stable_def]
+ "stable (actsF Un actsG) A = (stable actsF A & stable actsG A)";
+by (simp_tac (simpset() addsimps [constrains_Un]) 1);
+qed "stable_Un";
+
+Goal "stable (Acts (Join prgF prgG)) A = \
+\ (stable (Acts prgF) A & stable (Acts prgG) A)";
+by (simp_tac (simpset() addsimps [Join_def, stable_Un]) 1);
+qed "stable_Join";
+
+Goalw [FP_def] "FP (UN i:I. acts i) = (INT i:I. FP (acts i))";
+by (simp_tac (simpset() addsimps [stable_UN, INTER_def]) 1);
+qed "FP_UN";
+
+
+(*** Progress: transient, ensures ***)
+
+Goalw [transient_def]
+ "transient (UN i:I. acts i) A = (EX i:I. transient (acts i) A)";
+by (Simp_tac 1);
+qed "transient_UN";
+
+Goalw [ensures_def,transient_def]
+ "ensures (UN i:I. acts i) A B = \
+\ ((ALL i:I. constrains (acts i) (A-B) (A Un B)) & \
+\ (EX i:I. ensures (acts i) A B))";
+by (simp_tac (simpset() addsimps [constrains_UN]) 1);
+by Auto_tac;
+qed "ensures_UN";
+
+(*Alternative proof: simplify using ensures_def,transient_def,constrains_Un*)
+Goal "ensures (actsF Un actsG) A B = \
+\ (constrains actsF (A-B) (A Un B) & \
+\ constrains actsG (A-B) (A Un B) & \
+\ (ensures actsF A B | ensures actsG A B))";
+by (simp_tac (simpset() addcongs [conj_cong]
+ addsimps [ensures_UN, Un_eq_UN,
+ all_bool_eq, ex_bool_eq]) 1);
+qed "ensures_Un";
+
+(*Or a longer proof via constrains_imp_subset*)
+Goalw [stable_def, constrains_def]
+ "[| stable actsF A; constrains actsG A A'; id: actsG |] \
+\ ==> constrains (actsF Un actsG) A A'";
+by (asm_simp_tac (simpset() addsimps [ball_Un]) 1);
+by (Blast_tac 1);
+qed "stable_constrains_Un";
+
+Goalw [Join_def]
+ "[| stable (Acts prgF) A; invariant prgG A |] \
+\ ==> invariant (Join prgF prgG) A";
+by (asm_full_simp_tac (simpset() addsimps [invariant_def, stable_Un]) 1);
+by (Blast_tac 1);
+qed "stable_Join_invariant";
+
+Goal "[| stable actsF A; ensures actsG A B |] \
+\ ==> ensures (actsF Un actsG) A B";
+by (asm_simp_tac (simpset() addsimps [ensures_Un]) 1);
+by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
+by (etac constrains_weaken 1);
+by Auto_tac;
+qed "ensures_stable_Un1";
+
+Goal "[| stable (Acts prgF) A; ensures (Acts prgG) A B |] \
+\ ==> ensures (Acts (Join prgF prgG)) A B";
+by (asm_simp_tac (simpset() addsimps [Join_def, ensures_stable_Un1]) 1);
+qed "ensures_stable_Join1";
+
+(*As above, but exchanging the roles of F and G*)
+Goal "[| ensures actsF A B; stable actsG A |] \
+\ ==> ensures (actsF Un actsG) A B";
+by (stac Un_commute 1);
+by (blast_tac (claset() addIs [ensures_stable_Un1]) 1);
+qed "ensures_stable_Un2";
+
+Goal "[| ensures (Acts prgF) A B; stable (Acts prgG) A |] \
+\ ==> ensures (Acts (Join prgF prgG)) A B";
+by (asm_simp_tac (simpset() addsimps [Join_def, ensures_stable_Un2]) 1);
+qed "ensures_stable_Join2";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Union.thy Wed Aug 05 10:56:58 1998 +0200
@@ -0,0 +1,19 @@
+(* Title: HOL/UNITY/Union.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Unions of programs
+
+From Misra's Chapter 5: Asynchronous Compositions of Programs
+*)
+
+Union = SubstAx + FP +
+
+constdefs
+
+ Join :: "['a program, 'a program] => 'a program"
+ "Join prgF prgG == (|Init = Init prgF Int Init prgG,
+ Acts = Acts prgF Un Acts prgG|)"
+
+end