# HG changeset patch
# User paulson
# Date 936798611 -7200
# Node ID 3a716ebc2fc020a1de3550a0b6673a1f9e9f7a15
# Parent  d93b52bda2dd06081b30d2045d43d51c9296192b
more rational theorem names (?)

diff -r d93b52bda2dd -r 3a716ebc2fc0 src/HOL/UNITY/Handshake.ML
--- 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","{}")] 
diff -r d93b52bda2dd -r 3a716ebc2fc0 src/HOL/UNITY/PPROD.ML
--- 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";
 
diff -r d93b52bda2dd -r 3a716ebc2fc0 src/HOL/UNITY/Union.ML
--- 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);