--- 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);
--- 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";
--- 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, {})"