Join now an infix operator
authorpaulson
Mon Oct 05 10:22:49 1998 +0200 (1998-10-05)
changeset 56116957f124ca97
parent 5610 377acd99d74c
child 5612 e981ca6f7332
Join now an infix operator
src/HOL/UNITY/Handshake.ML
src/HOL/UNITY/Union.ML
src/HOL/UNITY/Union.thy
     1.1 --- a/src/HOL/UNITY/Handshake.ML	Mon Oct 05 10:19:21 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Handshake.ML	Mon Oct 05 10:22:49 1998 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  Addsimps [simp_of_set invFG_def];
     1.5  
     1.6  
     1.7 -Goal "Invariant (Join prgF prgG) invFG";
     1.8 +Goal "Invariant (prgF Join prgG) invFG";
     1.9  by (rtac InvariantI 1);
    1.10  by (Force_tac 1);
    1.11  by (rtac (constrains_imp_Constrains RS StableI) 1);
    1.12 @@ -30,26 +30,26 @@
    1.13  by (constrains_tac 1);
    1.14  qed "invFG";
    1.15  
    1.16 -Goal "LeadsTo (Join prgF prgG) ({s. NF s = k} - {s. BB s}) \
    1.17 +Goal "LeadsTo (prgF Join prgG) ({s. NF s = k} - {s. BB s}) \
    1.18  \                              ({s. NF s = k} Int {s. BB s})";
    1.19  by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
    1.20  by (ensures_tac "cmdG" 2);
    1.21  by (constrains_tac 1);
    1.22  qed "lemma2_1";
    1.23  
    1.24 -Goal "LeadsTo (Join prgF prgG) ({s. NF s = k} Int {s. BB s}) {s. k < NF s}";
    1.25 +Goal "LeadsTo (prgF Join prgG) ({s. NF s = k} Int {s. BB s}) {s. k < NF s}";
    1.26  by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
    1.27  by (constrains_tac 2);
    1.28  by (ensures_tac "cmdF" 1);
    1.29  qed "lemma2_2";
    1.30  
    1.31  
    1.32 -Goal "LeadsTo (Join prgF prgG) UNIV {s. m < NF s}";
    1.33 +Goal "LeadsTo (prgF Join prgG) UNIV {s. m < NF s}";
    1.34  by (rtac LeadsTo_weaken_R 1);
    1.35  by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")] 
    1.36      GreaterThan_bounded_induct 1);
    1.37  by (auto_tac (claset(), simpset() addsimps [vimage_def]));
    1.38 -(*The inductive step: LeadsTo (Join prgF prgG) {x. NF x = ma} {x. ma < NF x}*)
    1.39 +(*The inductive step: LeadsTo (prgF Join prgG) {x. NF x = ma} {x. ma < NF x}*)
    1.40  by (rtac LeadsTo_Diff 1);
    1.41  by (rtac lemma2_2 2);
    1.42  by (rtac LeadsTo_Trans 1);
     2.1 --- a/src/HOL/UNITY/Union.ML	Mon Oct 05 10:19:21 1998 +0200
     2.2 +++ b/src/HOL/UNITY/Union.ML	Mon Oct 05 10:22:49 1998 +0200
     2.3 @@ -9,51 +9,63 @@
     2.4  *)
     2.5  
     2.6  
     2.7 -Goal "Init (Join prgF prgG) = Init prgF Int Init prgG";
     2.8 +Goal "Init (F Join G) = Init F Int Init G";
     2.9 +by (simp_tac (simpset() addsimps [Join_def]) 1);
    2.10 +qed "Init_SKIP";
    2.11 +
    2.12 +Goal "Init (F Join G) = Init F Int Init G";
    2.13  by (simp_tac (simpset() addsimps [Join_def]) 1);
    2.14  qed "Init_Join";
    2.15  
    2.16 -Goal "Acts (Join prgF prgG) = Acts prgF Un Acts prgG";
    2.17 +Goal "Acts (F Join G) = Acts F Un Acts G";
    2.18  by (auto_tac (claset(), simpset() addsimps [Join_def]));
    2.19  qed "Acts_Join";
    2.20  
    2.21 -Goal "Init (JN i:I. prg i) = (INT i:I. Init (prg i))";
    2.22 +Goal "Init (JN i:I. F i) = (INT i:I. Init (F i))";
    2.23  by (simp_tac (simpset() addsimps [JOIN_def]) 1);
    2.24  qed "Init_JN";
    2.25  
    2.26 -Goal "Acts (JN i:I. prg i) = insert Id (UN i:I. Acts (prg i))";
    2.27 +Goal "Acts (JN i:I. F i) = insert Id (UN i:I. Acts (F i))";
    2.28  by (auto_tac (claset(), simpset() addsimps [JOIN_def]));
    2.29  qed "Acts_JN";
    2.30  
    2.31  Addsimps [Init_Join, Init_JN];
    2.32  
    2.33 -Goal "(JN x:insert a A. B x) = Join (B a) (JN x:A. B x)";
    2.34 -br program_equalityI 1;
    2.35 +Goal "(JN x:insert a A. B x) = (B a) Join (JN x:A. B x)";
    2.36 +by (rtac program_equalityI 1);
    2.37  by (ALLGOALS (simp_tac (simpset() addsimps [JOIN_def, Join_def])));
    2.38  qed "JN_insert";
    2.39  Addsimps[JN_insert];
    2.40  
    2.41  
    2.42 -(** Theoretical issues **)
    2.43 +(** Algebraic laws **)
    2.44  
    2.45 -Goal "Join prgF prgG = Join prgG prgF";
    2.46 +Goal "F Join G = G Join F";
    2.47  by (simp_tac (simpset() addsimps [Join_def, Un_commute, Int_commute]) 1);
    2.48  qed "Join_commute";
    2.49  
    2.50 -Goal "Join (Join prgF prgG) prgH = Join prgF (Join prgG prgH)";
    2.51 +Goal "(F Join G) Join H = F Join (G Join H)";
    2.52  by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc]) 1);
    2.53  qed "Join_assoc";
    2.54   
    2.55 -Goalw [Join_def, SKIP_def] "Join prgF SKIP = prgF";
    2.56 -br program_equalityI 1;
    2.57 +Goalw [Join_def, SKIP_def] "SKIP Join F = F";
    2.58 +by (rtac program_equalityI 1);
    2.59  by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb])));
    2.60 -qed "Join_SKIP";
    2.61 +qed "Join_SKIP_left";
    2.62  
    2.63 -Goalw [Join_def] "Join prgF prgF = prgF";
    2.64 -br program_equalityI 1;
    2.65 +Goalw [Join_def, SKIP_def] "F Join SKIP = F";
    2.66 +by (rtac program_equalityI 1);
    2.67 +by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb])));
    2.68 +qed "Join_SKIP_right";
    2.69 +
    2.70 +Addsimps [Join_SKIP_left, Join_SKIP_right];
    2.71 +
    2.72 +Goalw [Join_def] "F Join F = F";
    2.73 +by (rtac program_equalityI 1);
    2.74  by Auto_tac;
    2.75  qed "Join_absorb";
    2.76  
    2.77 +Addsimps [Join_absorb];
    2.78  
    2.79  Goal "(JN G:{}. G) = SKIP";
    2.80  by (simp_tac (simpset() addsimps [JOIN_def, SKIP_def]) 1);
    2.81 @@ -67,44 +79,44 @@
    2.82  
    2.83  Goalw [constrains_def, JOIN_def]
    2.84      "I ~= {} ==> \
    2.85 -\    constrains (Acts (JN i:I. prg i)) A B = \
    2.86 -\    (ALL i:I. constrains (Acts (prg i)) A B)";
    2.87 +\    constrains (Acts (JN i:I. F i)) A B = \
    2.88 +\    (ALL i:I. constrains (Acts (F i)) A B)";
    2.89  by (Simp_tac 1);
    2.90  by (Blast_tac 1);
    2.91  qed "constrains_JN";
    2.92  
    2.93  (**FAILS, I think; see 5.4.1, Substitution Axiom.
    2.94  Goalw [Constrains_def]
    2.95 -    "Constrains (JN i:I. prg i) A B = (ALL i:I. Constrains (prg i) A B)";
    2.96 +    "Constrains (JN i:I. F i) A B = (ALL i:I. Constrains (F i) A B)";
    2.97  by (simp_tac (simpset() addsimps [constrains_JN]) 1);
    2.98  by (Blast_tac 1);
    2.99  qed "Constrains_JN";
   2.100  **)
   2.101  
   2.102 -Goal "constrains (Acts (Join prgF prgG)) A B =  \
   2.103 -\     (constrains (Acts prgF) A B & constrains (Acts prgG) A B)";
   2.104 +Goal "constrains (Acts (F Join G)) A B =  \
   2.105 +\     (constrains (Acts F) A B & constrains (Acts G) A B)";
   2.106  by (auto_tac
   2.107      (claset(),
   2.108       simpset() addsimps [constrains_def, Join_def, ball_Un]));
   2.109  qed "constrains_Join";
   2.110  
   2.111 -Goal "[| constrains (Acts prgF) A A';  constrains (Acts prgG) B B' |] \
   2.112 -\     ==> constrains (Acts (Join prgF prgG)) (A Int B) (A' Un B')";
   2.113 +Goal "[| constrains (Acts F) A A';  constrains (Acts G) B B' |] \
   2.114 +\     ==> constrains (Acts (F Join G)) (A Int B) (A' Un B')";
   2.115  by (simp_tac (simpset() addsimps [constrains_Join]) 1);
   2.116  by (blast_tac (claset() addIs [constrains_weaken]) 1);
   2.117  qed "constrains_Join_weaken";
   2.118  
   2.119  Goal "I ~= {} ==> \
   2.120 -\     stable (Acts (JN i:I. prg i)) A = (ALL i:I. stable (Acts (prg i)) A)";
   2.121 +\     stable (Acts (JN i:I. F i)) A = (ALL i:I. stable (Acts (F i)) A)";
   2.122  by (asm_simp_tac (simpset() addsimps [stable_def, constrains_JN]) 1);
   2.123  qed "stable_JN";
   2.124  
   2.125 -Goal "stable (Acts (Join prgF prgG)) A = \
   2.126 -\     (stable (Acts prgF) A & stable (Acts prgG) A)";
   2.127 +Goal "stable (Acts (F Join G)) A = \
   2.128 +\     (stable (Acts F) A & stable (Acts G) A)";
   2.129  by (simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1);
   2.130  qed "stable_Join";
   2.131  
   2.132 -Goal "I ~= {} ==> FP (Acts (JN i:I. prg i)) = (INT i:I. FP (Acts (prg i)))";
   2.133 +Goal "I ~= {} ==> FP (Acts (JN i:I. F i)) = (INT i:I. FP (Acts (F i)))";
   2.134  by (asm_simp_tac (simpset() addsimps [FP_def, stable_JN, INTER_def]) 1);
   2.135  qed "FP_JN";
   2.136  
   2.137 @@ -112,54 +124,54 @@
   2.138  (*** Progress: transient, ensures ***)
   2.139  
   2.140  Goal "I ~= {} ==> \
   2.141 -\   transient (Acts (JN i:I. prg i)) A = (EX i:I. transient (Acts (prg i)) A)";
   2.142 +\   transient (Acts (JN i:I. F i)) A = (EX i:I. transient (Acts (F i)) A)";
   2.143  by (auto_tac (claset(),
   2.144  	      simpset() addsimps [transient_def, JOIN_def]));
   2.145  qed "transient_JN";
   2.146  
   2.147 -Goal "transient (Acts (Join prgF prgG)) A = \
   2.148 -\     (transient (Acts prgF) A | transient (Acts prgG) A)";
   2.149 +Goal "transient (Acts (F Join G)) A = \
   2.150 +\     (transient (Acts F) A | transient (Acts G) A)";
   2.151  by (auto_tac (claset(),
   2.152  	      simpset() addsimps [bex_Un, transient_def,
   2.153  				  Join_def]));
   2.154  qed "transient_Join";
   2.155  
   2.156  Goal "I ~= {} ==> \
   2.157 -\     ensures (Acts (JN i:I. prg i)) A B = \
   2.158 -\     ((ALL i:I. constrains (Acts (prg i)) (A-B) (A Un B)) & \
   2.159 -\      (EX i:I. ensures (Acts (prg i)) A B))";
   2.160 +\     ensures (Acts (JN i:I. F i)) A B = \
   2.161 +\     ((ALL i:I. constrains (Acts (F i)) (A-B) (A Un B)) & \
   2.162 +\      (EX i:I. ensures (Acts (F i)) A B))";
   2.163  by (auto_tac (claset(),
   2.164  	      simpset() addsimps [ensures_def, constrains_JN, transient_JN]));
   2.165  qed "ensures_JN";
   2.166  
   2.167  Goalw [ensures_def]
   2.168 -     "ensures (Acts (Join prgF prgG)) A B =     \
   2.169 -\     (constrains (Acts prgF) (A-B) (A Un B) & \
   2.170 -\      constrains (Acts prgG) (A-B) (A Un B) & \
   2.171 -\      (ensures (Acts prgF) A B | ensures (Acts prgG) A B))";
   2.172 +     "ensures (Acts (F Join G)) A B =     \
   2.173 +\     (constrains (Acts F) (A-B) (A Un B) & \
   2.174 +\      constrains (Acts G) (A-B) (A Un B) & \
   2.175 +\      (ensures (Acts F) A B | ensures (Acts G) A B))";
   2.176  by (auto_tac (claset(),
   2.177  	      simpset() addsimps [constrains_Join, transient_Join]));
   2.178  qed "ensures_Join";
   2.179  
   2.180  Goalw [stable_def, constrains_def, Join_def]
   2.181 -    "[| stable (Acts prgF) A;  constrains (Acts prgG) A A';  Id: Acts prgG |] \
   2.182 -\    ==> constrains (Acts (Join prgF prgG)) A A'";
   2.183 +    "[| stable (Acts F) A;  constrains (Acts G) A A';  Id: Acts G |] \
   2.184 +\    ==> constrains (Acts (F Join G)) A A'";
   2.185  by (asm_simp_tac (simpset() addsimps [ball_Un]) 1);
   2.186  by (Blast_tac 1);
   2.187  qed "stable_constrains_Join";
   2.188  
   2.189 -(*Premises cannot use Invariant because  Stable prgF A  is weaker than
   2.190 -  stable (Acts prgG) A *)
   2.191 -Goal "[| stable (Acts prgF) A;  Init prgG <= A;  stable (Acts prgG) A |] \
   2.192 -\      ==> Invariant (Join prgF prgG) A";
   2.193 +(*Premises cannot use Invariant because  Stable F A  is weaker than
   2.194 +  stable (Acts G) A *)
   2.195 +Goal "[| stable (Acts F) A;  Init G <= A;  stable (Acts G) A |] \
   2.196 +\      ==> Invariant (F Join G) A";
   2.197  by (simp_tac (simpset() addsimps [Invariant_def, Stable_eq_stable,
   2.198  				  stable_Join]) 1);
   2.199  by (force_tac(claset() addIs [stable_reachable, stable_Int],
   2.200  	      simpset() addsimps [Acts_Join]) 1);
   2.201  qed "stable_Join_Invariant";
   2.202  
   2.203 -Goal "[| stable (Acts prgF) A;  ensures (Acts prgG) A B |]     \
   2.204 -\     ==> ensures (Acts (Join prgF prgG)) A B";
   2.205 +Goal "[| stable (Acts F) A;  ensures (Acts G) A B |]     \
   2.206 +\     ==> ensures (Acts (F Join G)) A B";
   2.207  by (asm_simp_tac (simpset() addsimps [ensures_Join]) 1);
   2.208  by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
   2.209  by (etac constrains_weaken 1);
   2.210 @@ -167,8 +179,8 @@
   2.211  qed "ensures_stable_Join1";
   2.212  
   2.213  (*As above, but exchanging the roles of F and G*)
   2.214 -Goal "[| ensures (Acts prgF) A B;  stable (Acts prgG) A |]     \
   2.215 -\     ==> ensures (Acts (Join prgF prgG)) A B";
   2.216 +Goal "[| ensures (Acts F) A B;  stable (Acts G) A |]     \
   2.217 +\     ==> ensures (Acts (F Join G)) A B";
   2.218  by (stac Join_commute 1);
   2.219  by (blast_tac (claset() addIs [ensures_stable_Join1]) 1);
   2.220  qed "ensures_stable_Join2";
     3.1 --- a/src/HOL/UNITY/Union.thy	Mon Oct 05 10:19:21 1998 +0200
     3.2 +++ b/src/HOL/UNITY/Union.thy	Mon Oct 05 10:22:49 1998 +0200
     3.3 @@ -12,12 +12,10 @@
     3.4  
     3.5  constdefs
     3.6     JOIN  :: ['a set, 'a => 'b program] => 'b program
     3.7 -    "JOIN I prg == mk_program (INT i:I. Init (prg i),
     3.8 -			       UN  i:I. Acts (prg i))"
     3.9 +    "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i))"
    3.10  
    3.11 -   Join :: ['a program, 'a program] => 'a program
    3.12 -    "Join prgF prgG == mk_program (Init prgF Int Init prgG,
    3.13 -				   Acts prgF Un Acts prgG)"
    3.14 +   Join :: ['a program, 'a program] => 'a program      (infixl 65)
    3.15 +    "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G)"
    3.16  
    3.17     SKIP :: 'a program
    3.18      "SKIP == mk_program (UNIV, {})"