# HG changeset patch
# User paulson
# Date 902307418 -7200
# Node ID 1b0f14d111429d02b7a481fb90c0dd7aafd34185
# Parent  fee54d5c511cb119e9fefffd91179d98ee7787e5
Union primitives and examples

diff -r fee54d5c511c -r 1b0f14d11142 src/HOL/UNITY/Handshake.ML
--- /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();
diff -r fee54d5c511c -r 1b0f14d11142 src/HOL/UNITY/Handshake.thy
--- /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
diff -r fee54d5c511c -r 1b0f14d11142 src/HOL/UNITY/Union.ML
--- /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";
+
diff -r fee54d5c511c -r 1b0f14d11142 src/HOL/UNITY/Union.thy
--- /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