# HG changeset patch
# User paulson
# Date 907575769 -7200
# Node ID 6957f124ca97b5fae745cef4bec61d248c8d7e44
# Parent  377acd99d74cb6676bba49704395e6e4e6f1d9fa
Join now an infix operator

diff -r 377acd99d74c -r 6957f124ca97 src/HOL/UNITY/Handshake.ML
--- a/src/HOL/UNITY/Handshake.ML	Mon Oct 05 10:19:21 1998 +0200
+++ b/src/HOL/UNITY/Handshake.ML	Mon Oct 05 10:22:49 1998 +0200
@@ -20,7 +20,7 @@
 Addsimps [simp_of_set invFG_def];
 
 
-Goal "Invariant (Join prgF prgG) invFG";
+Goal "Invariant (prgF Join prgG) invFG";
 by (rtac InvariantI 1);
 by (Force_tac 1);
 by (rtac (constrains_imp_Constrains RS StableI) 1);
@@ -30,26 +30,26 @@
 by (constrains_tac 1);
 qed "invFG";
 
-Goal "LeadsTo (Join prgF prgG) ({s. NF s = k} - {s. BB s}) \
+Goal "LeadsTo (prgF Join prgG) ({s. NF s = k} - {s. BB s}) \
 \                              ({s. NF s = k} Int {s. BB s})";
 by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
 by (ensures_tac "cmdG" 2);
 by (constrains_tac 1);
 qed "lemma2_1";
 
-Goal "LeadsTo (Join prgF prgG) ({s. NF s = k} Int {s. BB s}) {s. k < NF s}";
+Goal "LeadsTo (prgF Join prgG) ({s. NF s = k} Int {s. BB s}) {s. k < NF s}";
 by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
 by (constrains_tac 2);
 by (ensures_tac "cmdF" 1);
 qed "lemma2_2";
 
 
-Goal "LeadsTo (Join prgF prgG) UNIV {s. m < NF s}";
+Goal "LeadsTo (prgF Join prgG) UNIV {s. m < NF s}";
 by (rtac LeadsTo_weaken_R 1);
 by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")] 
     GreaterThan_bounded_induct 1);
 by (auto_tac (claset(), simpset() addsimps [vimage_def]));
-(*The inductive step: LeadsTo (Join prgF prgG) {x. NF x = ma} {x. ma < NF x}*)
+(*The inductive step: LeadsTo (prgF Join prgG) {x. NF x = ma} {x. ma < NF x}*)
 by (rtac LeadsTo_Diff 1);
 by (rtac lemma2_2 2);
 by (rtac LeadsTo_Trans 1);
diff -r 377acd99d74c -r 6957f124ca97 src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Mon Oct 05 10:19:21 1998 +0200
+++ b/src/HOL/UNITY/Union.ML	Mon Oct 05 10:22:49 1998 +0200
@@ -9,51 +9,63 @@
 *)
 
 
-Goal "Init (Join prgF prgG) = Init prgF Int Init prgG";
+Goal "Init (F Join G) = Init F Int Init G";
+by (simp_tac (simpset() addsimps [Join_def]) 1);
+qed "Init_SKIP";
+
+Goal "Init (F Join G) = Init F Int Init G";
 by (simp_tac (simpset() addsimps [Join_def]) 1);
 qed "Init_Join";
 
-Goal "Acts (Join prgF prgG) = Acts prgF Un Acts prgG";
+Goal "Acts (F Join G) = Acts F Un Acts G";
 by (auto_tac (claset(), simpset() addsimps [Join_def]));
 qed "Acts_Join";
 
-Goal "Init (JN i:I. prg i) = (INT i:I. Init (prg i))";
+Goal "Init (JN i:I. F i) = (INT i:I. Init (F i))";
 by (simp_tac (simpset() addsimps [JOIN_def]) 1);
 qed "Init_JN";
 
-Goal "Acts (JN i:I. prg i) = insert Id (UN i:I. Acts (prg i))";
+Goal "Acts (JN i:I. F i) = insert Id (UN i:I. Acts (F i))";
 by (auto_tac (claset(), simpset() addsimps [JOIN_def]));
 qed "Acts_JN";
 
 Addsimps [Init_Join, Init_JN];
 
-Goal "(JN x:insert a A. B x) = Join (B a) (JN x:A. B x)";
-br program_equalityI 1;
+Goal "(JN x:insert a A. B x) = (B a) Join (JN x:A. B x)";
+by (rtac program_equalityI 1);
 by (ALLGOALS (simp_tac (simpset() addsimps [JOIN_def, Join_def])));
 qed "JN_insert";
 Addsimps[JN_insert];
 
 
-(** Theoretical issues **)
+(** Algebraic laws **)
 
-Goal "Join prgF prgG = Join prgG prgF";
+Goal "F Join G = G Join F";
 by (simp_tac (simpset() addsimps [Join_def, Un_commute, Int_commute]) 1);
 qed "Join_commute";
 
-Goal "Join (Join prgF prgG) prgH = Join prgF (Join prgG prgH)";
+Goal "(F Join G) Join H = F Join (G Join H)";
 by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc]) 1);
 qed "Join_assoc";
  
-Goalw [Join_def, SKIP_def] "Join prgF SKIP = prgF";
-br program_equalityI 1;
+Goalw [Join_def, SKIP_def] "SKIP Join F = F";
+by (rtac program_equalityI 1);
 by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb])));
-qed "Join_SKIP";
+qed "Join_SKIP_left";
 
-Goalw [Join_def] "Join prgF prgF = prgF";
-br program_equalityI 1;
+Goalw [Join_def, SKIP_def] "F Join SKIP = F";
+by (rtac program_equalityI 1);
+by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb])));
+qed "Join_SKIP_right";
+
+Addsimps [Join_SKIP_left, Join_SKIP_right];
+
+Goalw [Join_def] "F Join F = F";
+by (rtac program_equalityI 1);
 by Auto_tac;
 qed "Join_absorb";
 
+Addsimps [Join_absorb];
 
 Goal "(JN G:{}. G) = SKIP";
 by (simp_tac (simpset() addsimps [JOIN_def, SKIP_def]) 1);
@@ -67,44 +79,44 @@
 
 Goalw [constrains_def, JOIN_def]
     "I ~= {} ==> \
-\    constrains (Acts (JN i:I. prg i)) A B = \
-\    (ALL i:I. constrains (Acts (prg i)) A B)";
+\    constrains (Acts (JN i:I. F i)) A B = \
+\    (ALL i:I. constrains (Acts (F i)) A B)";
 by (Simp_tac 1);
 by (Blast_tac 1);
 qed "constrains_JN";
 
 (**FAILS, I think; see 5.4.1, Substitution Axiom.
 Goalw [Constrains_def]
-    "Constrains (JN i:I. prg i) A B = (ALL i:I. Constrains (prg i) A B)";
+    "Constrains (JN i:I. F i) A B = (ALL i:I. Constrains (F i) A B)";
 by (simp_tac (simpset() addsimps [constrains_JN]) 1);
 by (Blast_tac 1);
 qed "Constrains_JN";
 **)
 
-Goal "constrains (Acts (Join prgF prgG)) A B =  \
-\     (constrains (Acts prgF) A B & constrains (Acts prgG) A B)";
+Goal "constrains (Acts (F Join G)) A B =  \
+\     (constrains (Acts F) A B & constrains (Acts G) A B)";
 by (auto_tac
     (claset(),
      simpset() addsimps [constrains_def, Join_def, ball_Un]));
 qed "constrains_Join";
 
-Goal "[| constrains (Acts prgF) A A';  constrains (Acts prgG) B B' |] \
-\     ==> constrains (Acts (Join prgF prgG)) (A Int B) (A' Un B')";
+Goal "[| constrains (Acts F) A A';  constrains (Acts G) B B' |] \
+\     ==> constrains (Acts (F Join G)) (A Int B) (A' Un B')";
 by (simp_tac (simpset() addsimps [constrains_Join]) 1);
 by (blast_tac (claset() addIs [constrains_weaken]) 1);
 qed "constrains_Join_weaken";
 
 Goal "I ~= {} ==> \
-\     stable (Acts (JN i:I. prg i)) A = (ALL i:I. stable (Acts (prg i)) A)";
+\     stable (Acts (JN i:I. F i)) A = (ALL i:I. stable (Acts (F i)) A)";
 by (asm_simp_tac (simpset() addsimps [stable_def, constrains_JN]) 1);
 qed "stable_JN";
 
-Goal "stable (Acts (Join prgF prgG)) A = \
-\     (stable (Acts prgF) A & stable (Acts prgG) A)";
+Goal "stable (Acts (F Join G)) A = \
+\     (stable (Acts F) A & stable (Acts G) A)";
 by (simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1);
 qed "stable_Join";
 
-Goal "I ~= {} ==> FP (Acts (JN i:I. prg i)) = (INT i:I. FP (Acts (prg i)))";
+Goal "I ~= {} ==> FP (Acts (JN i:I. F i)) = (INT i:I. FP (Acts (F i)))";
 by (asm_simp_tac (simpset() addsimps [FP_def, stable_JN, INTER_def]) 1);
 qed "FP_JN";
 
@@ -112,54 +124,54 @@
 (*** Progress: transient, ensures ***)
 
 Goal "I ~= {} ==> \
-\   transient (Acts (JN i:I. prg i)) A = (EX i:I. transient (Acts (prg i)) A)";
+\   transient (Acts (JN i:I. F i)) A = (EX i:I. transient (Acts (F i)) A)";
 by (auto_tac (claset(),
 	      simpset() addsimps [transient_def, JOIN_def]));
 qed "transient_JN";
 
-Goal "transient (Acts (Join prgF prgG)) A = \
-\     (transient (Acts prgF) A | transient (Acts prgG) A)";
+Goal "transient (Acts (F Join G)) A = \
+\     (transient (Acts F) A | transient (Acts G) A)";
 by (auto_tac (claset(),
 	      simpset() addsimps [bex_Un, transient_def,
 				  Join_def]));
 qed "transient_Join";
 
 Goal "I ~= {} ==> \
-\     ensures (Acts (JN i:I. prg i)) A B = \
-\     ((ALL i:I. constrains (Acts (prg i)) (A-B) (A Un B)) & \
-\      (EX i:I. ensures (Acts (prg i)) A B))";
+\     ensures (Acts (JN i:I. F i)) A B = \
+\     ((ALL i:I. constrains (Acts (F i)) (A-B) (A Un B)) & \
+\      (EX i:I. ensures (Acts (F i)) A B))";
 by (auto_tac (claset(),
 	      simpset() addsimps [ensures_def, constrains_JN, transient_JN]));
 qed "ensures_JN";
 
 Goalw [ensures_def]
-     "ensures (Acts (Join prgF prgG)) A B =     \
-\     (constrains (Acts prgF) (A-B) (A Un B) & \
-\      constrains (Acts prgG) (A-B) (A Un B) & \
-\      (ensures (Acts prgF) A B | ensures (Acts prgG) A B))";
+     "ensures (Acts (F Join G)) A B =     \
+\     (constrains (Acts F) (A-B) (A Un B) & \
+\      constrains (Acts G) (A-B) (A Un B) & \
+\      (ensures (Acts F) A B | ensures (Acts G) A B))";
 by (auto_tac (claset(),
 	      simpset() addsimps [constrains_Join, transient_Join]));
 qed "ensures_Join";
 
 Goalw [stable_def, constrains_def, Join_def]
-    "[| stable (Acts prgF) A;  constrains (Acts prgG) A A';  Id: Acts prgG |] \
-\    ==> constrains (Acts (Join prgF prgG)) A A'";
+    "[| stable (Acts F) A;  constrains (Acts G) A A';  Id: Acts G |] \
+\    ==> constrains (Acts (F Join G)) A A'";
 by (asm_simp_tac (simpset() addsimps [ball_Un]) 1);
 by (Blast_tac 1);
 qed "stable_constrains_Join";
 
-(*Premises cannot use Invariant because  Stable prgF A  is weaker than
-  stable (Acts prgG) A *)
-Goal "[| stable (Acts prgF) A;  Init prgG <= A;  stable (Acts prgG) A |] \
-\      ==> Invariant (Join prgF prgG) A";
+(*Premises cannot use Invariant because  Stable F A  is weaker than
+  stable (Acts G) A *)
+Goal "[| stable (Acts F) A;  Init G <= A;  stable (Acts G) A |] \
+\      ==> Invariant (F Join G) A";
 by (simp_tac (simpset() addsimps [Invariant_def, Stable_eq_stable,
 				  stable_Join]) 1);
 by (force_tac(claset() addIs [stable_reachable, stable_Int],
 	      simpset() addsimps [Acts_Join]) 1);
 qed "stable_Join_Invariant";
 
-Goal "[| stable (Acts prgF) A;  ensures (Acts prgG) A B |]     \
-\     ==> ensures (Acts (Join prgF prgG)) A B";
+Goal "[| stable (Acts F) A;  ensures (Acts G) A B |]     \
+\     ==> ensures (Acts (F Join G)) A B";
 by (asm_simp_tac (simpset() addsimps [ensures_Join]) 1);
 by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
 by (etac constrains_weaken 1);
@@ -167,8 +179,8 @@
 qed "ensures_stable_Join1";
 
 (*As above, but exchanging the roles of F and G*)
-Goal "[| ensures (Acts prgF) A B;  stable (Acts prgG) A |]     \
-\     ==> ensures (Acts (Join prgF prgG)) A B";
+Goal "[| ensures (Acts F) A B;  stable (Acts G) A |]     \
+\     ==> ensures (Acts (F Join G)) A B";
 by (stac Join_commute 1);
 by (blast_tac (claset() addIs [ensures_stable_Join1]) 1);
 qed "ensures_stable_Join2";
diff -r 377acd99d74c -r 6957f124ca97 src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Mon Oct 05 10:19:21 1998 +0200
+++ b/src/HOL/UNITY/Union.thy	Mon Oct 05 10:22:49 1998 +0200
@@ -12,12 +12,10 @@
 
 constdefs
    JOIN  :: ['a set, 'a => 'b program] => 'b program
-    "JOIN I prg == mk_program (INT i:I. Init (prg i),
-			       UN  i:I. Acts (prg i))"
+    "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i))"
 
-   Join :: ['a program, 'a program] => 'a program
-    "Join prgF prgG == mk_program (Init prgF Int Init prgG,
-				   Acts prgF Un Acts prgG)"
+   Join :: ['a program, 'a program] => 'a program      (infixl 65)
+    "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G)"
 
    SKIP :: 'a program
     "SKIP == mk_program (UNIV, {})"