--- a/src/HOL/UNITY/Handshake.ML Wed Sep 08 15:45:36 1999 +0200
+++ b/src/HOL/UNITY/Handshake.ML Wed Sep 08 15:50:11 1999 +0200
@@ -19,7 +19,7 @@
by (rtac AlwaysI 1);
by (Force_tac 1);
by (rtac (constrains_imp_Constrains RS StableI) 1);
-by (auto_tac (claset(), simpset() addsimps [constrains_Join]));
+by (auto_tac (claset(), simpset() addsimps [Join_constrains]));
by (constrains_tac 2);
by (auto_tac (claset() addIs [order_antisym] addSEs [le_SucE], simpset()));
by (constrains_tac 1);
@@ -27,18 +27,17 @@
Goal "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo \
\ ({s. NF s = k} Int {s. BB s})";
-by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
+by (rtac (stable_Join_ensures1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
by (ensures_tac "cmdG" 2);
by (constrains_tac 1);
qed "lemma2_1";
Goal "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo {s. k < NF s}";
-by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
+by (rtac (stable_Join_ensures2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
by (constrains_tac 2);
by (ensures_tac "cmdF" 1);
qed "lemma2_2";
-
Goal "(F Join G) : UNIV LeadsTo {s. m < NF s}";
by (rtac LeadsTo_weaken_R 1);
by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")]
--- a/src/HOL/UNITY/PPROD.ML Wed Sep 08 15:45:36 1999 +0200
+++ b/src/HOL/UNITY/PPROD.ML Wed Sep 08 15:50:11 1999 +0200
@@ -10,9 +10,6 @@
*)
-val rinst = read_instantiate_sg (sign_of thy);
-
-
(*** Basic properties ***)
Goalw [PLam_def] "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))";
@@ -46,12 +43,12 @@
qed "component_PLam";
-(** Safety **)
+(** Safety & Progress **)
Goal "i : I ==> \
\ (PLam I F : (lift_set i A) co (lift_set i B)) = \
\ (F i : A co B)";
-by (asm_simp_tac (simpset() addsimps [PLam_def, constrains_JN]) 1);
+by (asm_simp_tac (simpset() addsimps [PLam_def, JN_constrains]) 1);
by (blast_tac (claset() addIs [lift_prog_constrains RS iffD1,
constrains_imp_lift_prog_constrains]) 1);
qed "PLam_constrains";
@@ -60,21 +57,25 @@
by (asm_simp_tac (simpset() addsimps [stable_def, PLam_constrains]) 1);
qed "PLam_stable";
-(*Possibly useful in Lift_set.ML?*)
-Goal "[| lift_prog i F : AA co BB |] \
-\ ==> F : (drop_set i AA) co (drop_set i BB)";
-by (auto_tac (claset(),
- simpset() addsimps [constrains_def, drop_set_def]));
-by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] image_eqI],
- simpset()) 1);
-qed "lift_prog_constrains_drop_set";
+Goal "i : I ==> \
+\ PLam I F : transient A = (EX i:I. lift_prog i (F i) : transient A)";
+by (asm_simp_tac (simpset() addsimps [JN_transient, PLam_def]) 1);
+qed "PLam_transient";
+
+Addsimps [PLam_constrains, PLam_stable, PLam_transient];
+
+Goal "[| i : I; F i : (A-B) co (A Un B); F i : transient (A-B) |] ==> \
+\ PLam I F : (lift_set i A) leadsTo lift_set i B";
+by (rtac (ensuresI RS leadsTo_Basis) 1);
+by (auto_tac (claset(), simpset() addsimps [lift_prog_transient_eq_disj]));
+qed "PLam_leadsTo_Basis";
Goal "[| PLam I F : AA co BB; i: I |] \
\ ==> F i : (drop_set i AA) co (drop_set i BB)";
by (rtac lift_prog_constrains_drop_set 1);
(*rotate this assumption to be last*)
by (dres_inst_tac [("psi", "PLam I F : ?C")] asm_rl 1);
-by (asm_full_simp_tac (simpset() addsimps [PLam_def, constrains_JN]) 1);
+by (asm_full_simp_tac (simpset() addsimps [PLam_def, JN_constrains]) 1);
qed "PLam_constrains_drop_set";
@@ -83,14 +84,14 @@
Goal "[| F i : invariant A; i : I |] \
\ ==> PLam I F : invariant (lift_set i A)";
by (auto_tac (claset(),
- simpset() addsimps [invariant_def, PLam_stable]));
+ simpset() addsimps [invariant_def]));
qed "invariant_imp_PLam_invariant";
(*The f0 premise ensures that the product is well-defined.*)
Goal "[| PLam I F : invariant (lift_set i A); i : I; \
\ f0: Init (PLam I F) |] ==> F i : invariant A";
by (auto_tac (claset(),
- simpset() addsimps [invariant_def, PLam_stable]));
+ simpset() addsimps [invariant_def]));
by (dres_inst_tac [("c", "f0(i:=x)")] subsetD 1);
by Auto_tac;
qed "PLam_invariant_imp_invariant";
@@ -106,7 +107,7 @@
Goal "i : I \
\ ==> ((plam x:I. F) : invariant (lift_set i A)) = (F : invariant A)";
by (auto_tac (claset(),
- simpset() addsimps [invariant_def, PLam_stable]));
+ simpset() addsimps [invariant_def]));
qed "const_PLam_invariant";
@@ -190,7 +191,7 @@
Goal "[| ALL j:I. f0 j : A j; i: I |] \
\ ==> drop_set i (INT j:I. lift_set j (A j)) = A i";
-by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] image_eqI],
+by (force_tac (claset() addSIs [image_eqI'],
simpset() addsimps [drop_set_def]) 1);
qed "drop_set_INT_lift_set";
@@ -205,7 +206,7 @@
by (dtac PLam_constrains_drop_set 1);
by (assume_tac 1);
by (asm_full_simp_tac
- (simpset() addsimps [drop_set_lift_set_Int2,
+ (simpset() addsimps [drop_set_Int_lift_set2,
drop_set_INT_lift_set, reachable_PLam_eq]) 1);
qed "PLam_Constrains_imp_Constrains";
@@ -234,7 +235,7 @@
by (assume_tac 1);
by (asm_full_simp_tac
(simpset() addsimps [drop_set_INT,
- drop_set_lift_set_Int2, Collect_conj_eq RS sym,
+ drop_set_Int_lift_set2, Collect_conj_eq RS sym,
reachable_PLam_eq]) 1);
qed "const_PLam_Constrains_imp_Constrains";
--- a/src/HOL/UNITY/Union.ML Wed Sep 08 15:45:36 1999 +0200
+++ b/src/HOL/UNITY/Union.ML Wed Sep 08 15:50:11 1999 +0200
@@ -171,13 +171,13 @@
"i : I ==> (JN i:I. F i) : A co B = (ALL i:I. F i : A co B)";
by (Simp_tac 1);
by (Blast_tac 1);
-qed "constrains_JN";
+qed "JN_constrains";
Goal "(F Join G : A co B) = (F : A co B & G : A co B)";
by (auto_tac
(claset(),
simpset() addsimps [constrains_def, Join_def]));
-qed "constrains_Join";
+qed "Join_constrains";
(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
reachable (F Join G) could be much bigger than reachable F, reachable G
@@ -186,40 +186,40 @@
Goal "[| F : A co A'; G : B co B' |] \
\ ==> F Join G : (A Int B) co (A' Un B')";
-by (simp_tac (simpset() addsimps [constrains_Join]) 1);
+by (simp_tac (simpset() addsimps [Join_constrains]) 1);
by (blast_tac (claset() addIs [constrains_weaken]) 1);
-qed "constrains_Join_weaken";
+qed "Join_constrains_weaken";
Goal "[| ALL i:I. F i : A i co A' i; i: I |] \
\ ==> (JN i:I. F i) : (INT i:I. A i) co (UN i:I. A' i)";
-by (asm_simp_tac (simpset() addsimps [constrains_JN]) 1);
+by (asm_simp_tac (simpset() addsimps [JN_constrains]) 1);
by (blast_tac (claset() addIs [constrains_weaken]) 1);
-qed "constrains_JN_weaken";
+qed "JN_constrains_weaken";
Goal "i : I ==> \
\ (JN i:I. F i) : stable A = (ALL i:I. F i : stable A)";
-by (asm_simp_tac (simpset() addsimps [stable_def, constrains_JN]) 1);
-qed "stable_JN";
+by (asm_simp_tac (simpset() addsimps [stable_def, JN_constrains]) 1);
+qed "JN_stable";
Goal "[| ALL i:I. F i : invariant A; i : I |] \
\ ==> (JN i:I. F i) : invariant A";
-by (asm_full_simp_tac (simpset() addsimps [invariant_def, stable_JN]) 1);
+by (asm_full_simp_tac (simpset() addsimps [invariant_def, JN_stable]) 1);
by (Blast_tac 1);
bind_thm ("invariant_JN_I", ballI RS result());
Goal "F Join G : stable A = \
\ (F : stable A & G : stable A)";
-by (simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1);
-qed "stable_Join";
+by (simp_tac (simpset() addsimps [stable_def, Join_constrains]) 1);
+qed "Join_stable";
Goal "[| F : invariant A; G : invariant A |] \
\ ==> F Join G : invariant A";
-by (full_simp_tac (simpset() addsimps [invariant_def, stable_Join]) 1);
+by (full_simp_tac (simpset() addsimps [invariant_def, Join_stable]) 1);
by (Blast_tac 1);
qed "invariant_JoinI";
Goal "i : I ==> FP (JN i:I. F i) = (INT i:I. FP (F i))";
-by (asm_simp_tac (simpset() addsimps [FP_def, stable_JN, INTER_def]) 1);
+by (asm_simp_tac (simpset() addsimps [FP_def, JN_stable, INTER_def]) 1);
qed "FP_JN";
@@ -229,22 +229,22 @@
\ (JN i:I. F i) : transient A = (EX i:I. F i : transient A)";
by (auto_tac (claset(),
simpset() addsimps [transient_def, JOIN_def]));
-qed "transient_JN";
+qed "JN_transient";
Goal "F Join G : transient A = \
\ (F : transient A | G : transient A)";
by (auto_tac (claset(),
simpset() addsimps [bex_Un, transient_def,
Join_def]));
-qed "transient_Join";
+qed "Join_transient";
Goal "i : I ==> \
\ (JN i:I. F i) : A ensures B = \
\ ((ALL i:I. F i : (A-B) co (A Un B)) & \
\ (EX i:I. F i : A ensures B))";
by (auto_tac (claset(),
- simpset() addsimps [ensures_def, constrains_JN, transient_JN]));
-qed "ensures_JN";
+ simpset() addsimps [ensures_def, JN_constrains, JN_transient]));
+qed "JN_ensures";
Goalw [ensures_def]
"F Join G : A ensures B = \
@@ -252,37 +252,37 @@
\ G : (A-B) co (A Un B) & \
\ (F : A ensures B | G : A ensures B))";
by (auto_tac (claset(),
- simpset() addsimps [constrains_Join, transient_Join]));
-qed "ensures_Join";
+ simpset() addsimps [Join_constrains, Join_transient]));
+qed "Join_ensures";
Goalw [stable_def, constrains_def, Join_def]
"[| F : stable A; G : A co A' |] \
\ ==> F Join G : A co A'";
by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1);
by (Blast_tac 1);
-qed "stable_constrains_Join";
+qed "stable_Join_constrains";
(*Premise for G cannot use Always because F: Stable A is weaker than
G : stable A *)
Goal "[| F : stable A; G : invariant A |] ==> F Join G : Always A";
by (full_simp_tac (simpset() addsimps [Always_def, invariant_def,
- Stable_eq_stable, stable_Join]) 1);
+ Stable_eq_stable, Join_stable]) 1);
by (force_tac(claset() addIs [stable_reachable, stable_Int],
simpset() addsimps [Acts_Join]) 1);
qed "stable_Join_Always";
Goal "[| F : stable A; G : A ensures B |] ==> F Join G : A ensures B";
-by (asm_simp_tac (simpset() addsimps [ensures_Join]) 1);
+by (asm_simp_tac (simpset() addsimps [Join_ensures]) 1);
by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
by (etac constrains_weaken 1);
by Auto_tac;
-qed "ensures_stable_Join1";
+qed "stable_Join_ensures1";
(*As above, but exchanging the roles of F and G*)
Goal "[| F : A ensures B; G : stable A |] ==> F Join G : A ensures B";
by (stac Join_commute 1);
-by (blast_tac (claset() addIs [ensures_stable_Join1]) 1);
-qed "ensures_stable_Join2";
+by (blast_tac (claset() addIs [stable_Join_ensures1]) 1);
+qed "stable_Join_ensures2";
(** Diff and localTo **)
@@ -358,7 +358,7 @@
by (rtac ballI 1);
by (subgoal_tac "F Join G : ({s. v s = k} Int {s. v s <= w s}) co \
\ ({s. v s = k} Un {s. v s <= w s})" 1);
-by (asm_simp_tac (simpset() addsimps [constrains_Join]) 2);
+by (asm_simp_tac (simpset() addsimps [Join_constrains]) 2);
by (blast_tac (claset() addIs [constrains_weaken]) 2);
by (dtac (constrains_imp_Constrains RS Constrains_Int) 1 THEN etac INT_D 1);
by (etac Constrains_weaken 2);