# HG changeset patch
# User paulson
# Date 925818448 -7200
# Node ID 70d758762c501644d9a9d0f54ff698761c057d1e
# Parent  a91b4cfd3104d8a9e989303c90b16797f0c27a87
new definitions of Co and LeadsTo

diff -r a91b4cfd3104 -r 70d758762c50 src/HOL/UNITY/Constrains.ML
--- a/src/HOL/UNITY/Constrains.ML	Tue May 04 13:32:53 1999 +0200
+++ b/src/HOL/UNITY/Constrains.ML	Tue May 04 13:47:28 1999 +0200
@@ -51,8 +51,15 @@
 	  rewrite_rule [stable_def] stable_reachable RS 
 	  constrains_Int);
 
+(*Resembles the previous definition of Constrains*)
+Goalw [Constrains_def]
+     "A Co B = {F. F : (reachable F  Int  A) co (reachable F  Int  B)}";
+by (blast_tac (claset() addDs [constrains_reachable_Int]
+			addIs [constrains_weaken]) 1);
+qed "Constrains_eq_constrains";
+
 Goalw [Constrains_def] "F : A co A' ==> F : A Co A'";
-by (blast_tac (claset() addIs [constrains_reachable_Int]) 1);
+by (blast_tac (claset() addIs [constrains_weaken_L]) 1);
 qed "constrains_imp_Constrains";
 
 Goalw [stable_def, Stable_def] "F : stable A ==> F : Stable A";
@@ -75,7 +82,6 @@
 qed "Constrains_UNIV";
 AddIffs [Constrains_empty, Constrains_UNIV];
 
-
 Goalw [Constrains_def]
     "[| F : A Co A'; A'<=B' |] ==> F : A Co B'";
 by (blast_tac (claset() addIs [constrains_weaken_R]) 1);
@@ -123,22 +129,18 @@
 qed "ball_Constrains_INT";
 
 Goal "F : A Co A' ==> reachable F Int A <= A'";
-by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
-by (dtac constrains_imp_subset 1);
-by (ALLGOALS
-    (full_simp_tac (simpset() addsimps [Int_subset_iff, Int_lower1])));
+by (asm_full_simp_tac (simpset() addsimps [constrains_imp_subset, 
+					   Constrains_def]) 1);
 qed "Constrains_imp_subset";
 
-Goalw [Constrains_def]
-    "[| F : A Co B; F : B Co C |]   \
-\    ==> F : A Co C";
+Goal "[| F : A Co B; F : B Co C |] ==> F : A Co C";
+by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1);
 by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
 qed "Constrains_trans";
 
-Goalw [Constrains_def, constrains_def]
-   "[| F : A Co (A' Un B); F : B Co B' |] \
-\   ==> F : A Co (A' Un B')";
-by (Clarify_tac 1);
+Goal "[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')";
+by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains, 
+				       constrains_def]) 1);
 by (Blast_tac 1);
 qed "Constrains_cancel";
 
@@ -146,7 +148,8 @@
 (*** Stable ***)
 
 Goal "(F : Stable A) = (F : stable (reachable F Int A))";
-by (simp_tac (simpset() addsimps [Stable_def, Constrains_def, stable_def]) 1);
+by (simp_tac (simpset() addsimps [Stable_def, Constrains_eq_constrains, 
+				  stable_def]) 1);
 qed "Stable_eq_stable";
 
 Goalw [Stable_def] "F : A Co A ==> F : Stable A";
@@ -259,13 +262,14 @@
 by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
 qed "Always_includes_reachable";
 
-Goalw [Always_def, invariant_def, Stable_def, Constrains_def, stable_def]
+Goalw [Always_def, invariant_def, Stable_def, stable_def]
      "F : invariant A ==> F : Always A";
-by (blast_tac (claset() addIs [constrains_reachable_Int]) 1);
+by (blast_tac (claset() addIs [constrains_imp_Constrains]) 1);
 qed "invariant_imp_Always";
 
-Goalw [Always_def, invariant_def, Stable_def, Constrains_def, stable_def]
-     "Always A = {F. F : invariant (reachable F Int A)}";
+Goal "Always A = {F. F : invariant (reachable F Int A)}";
+by (simp_tac (simpset() addsimps [Always_def, invariant_def, Stable_def, 
+				  Constrains_eq_constrains, stable_def]) 1);
 by (blast_tac (claset() addIs reachable.intrs) 1);
 qed "Always_eq_invariant_reachable";
 
@@ -291,8 +295,7 @@
 
 (*** "Co" rules involving Always ***)
 
-Goal "[| F : Always INV;  F : (INV Int A) Co A' |]   \
-\     ==> F : A Co A'";
+Goal "[| F : Always INV;  F : (INV Int A) Co A' |] ==> F : A Co A'";
 by (asm_full_simp_tac
     (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
 			 Constrains_def, Int_assoc RS sym]) 1);
@@ -306,7 +309,7 @@
 \     ==> F : A Co (INV Int A')";
 by (asm_full_simp_tac
     (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
-			 Constrains_def, Int_assoc RS sym]) 1);
+			 Constrains_eq_constrains, Int_assoc RS sym]) 1);
 qed "Always_ConstrainsD";
 
 bind_thm ("Always_StableD", StableD RSN (2,Always_ConstrainsD));
diff -r a91b4cfd3104 -r 70d758762c50 src/HOL/UNITY/Constrains.thy
--- a/src/HOL/UNITY/Constrains.thy	Tue May 04 13:32:53 1999 +0200
+++ b/src/HOL/UNITY/Constrains.thy	Tue May 04 13:47:28 1999 +0200
@@ -36,7 +36,7 @@
 
 defs
   Constrains_def
-    "A Co B == {F. F : (reachable F  Int  A) co (reachable F  Int  B)}"
+    "A Co B == {F. F : (reachable F Int A)  co  B}"
 
   Unless_def
     "A Unless B == (A-B) Co (A Un B)"
diff -r a91b4cfd3104 -r 70d758762c50 src/HOL/UNITY/PPROD.ML
--- a/src/HOL/UNITY/PPROD.ML	Tue May 04 13:32:53 1999 +0200
+++ b/src/HOL/UNITY/PPROD.ML	Tue May 04 13:47:28 1999 +0200
@@ -245,12 +245,12 @@
 	       simpset() addsimps [Applyall_def, lift_set_def]) 1);
 qed "Applyall_Int_depend";
 
-(*Again, we need the f0 premise because otherwise holds Co trivially
-  for PPROD I F.*)
+(*Again, we need the f0 premise so that PPROD I F has an initial state;
+  otherwise its Co-property is vacuous.*)
 Goal "[| PPROD I F : (lift_set i A) Co (lift_set i B);  \
 \        i: I;  finite I;  f0: Init (PPROD I F) |]  \
 \     ==> F i : A Co B";
-by (full_simp_tac (simpset() addsimps [Constrains_def]) 1);
+by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1);
 by (subgoal_tac "ALL i:I. f0 i : reachable (F i)" 1);
 by (blast_tac (claset() addIs [reachable.Init]) 2);
 by (dtac PPROD_constrains_projection 1);
@@ -284,7 +284,7 @@
 Goal "[| (PPI x:I. F) : (lift_set i A) Co (lift_set i B);  \
 \        i: I;  finite I |]  \
 \     ==> F : A Co B";
-by (full_simp_tac (simpset() addsimps [Constrains_def]) 1);
+by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1);
 by (dtac PPROD_constrains_projection 1);
 by (assume_tac 1);
 by (asm_full_simp_tac
diff -r a91b4cfd3104 -r 70d758762c50 src/HOL/UNITY/SubstAx.ML
--- a/src/HOL/UNITY/SubstAx.ML	Tue May 04 13:32:53 1999 +0200
+++ b/src/HOL/UNITY/SubstAx.ML	Tue May 04 13:47:28 1999 +0200
@@ -9,6 +9,14 @@
 overload_1st_set "SubstAx.op LeadsTo";
 
 
+(*Resembles the previous definition of LeadsTo*)
+Goalw [LeadsTo_def]
+     "A LeadsTo B = {F. F : (reachable F Int A) leadsTo (reachable F Int B)}";
+by (blast_tac (claset() addDs [psp_stable2] 
+                        addIs [leadsTo_weaken, stable_reachable]) 1);
+qed "LeadsTo_eq_leadsTo";
+
+
 (*** Specialized laws for handling invariants ***)
 
 (** Conjoining an Always property **)
@@ -23,7 +31,7 @@
 Goal "[| F : Always C;  F : A LeadsTo A' |]   \
 \     ==> F : A LeadsTo (C Int A')";
 by (asm_full_simp_tac
-    (simpset() addsimps [LeadsTo_def, Always_eq_includes_reachable, 
+    (simpset() addsimps [LeadsTo_eq_leadsTo, Always_eq_includes_reachable, 
 			 Int_absorb2, Int_assoc RS sym]) 1);
 qed "Always_LeadsToD";
 
@@ -32,11 +40,11 @@
 
 Goal "F : A leadsTo B ==> F : A LeadsTo B";
 by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
-by (blast_tac (claset() addIs [psp_stable2, stable_reachable]) 1);
+by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
 qed "leadsTo_imp_LeadsTo";
 
 Goal "[| F : A LeadsTo B;  F : B LeadsTo C |] ==> F : A LeadsTo C";
-by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
+by (full_simp_tac (simpset() addsimps [LeadsTo_eq_leadsTo]) 1);
 by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
 qed "LeadsTo_Trans";
 
@@ -51,8 +59,7 @@
 (*** Derived rules ***)
 
 Goal "F : A LeadsTo UNIV";
-by (asm_simp_tac 
-    (simpset() addsimps [LeadsTo_def, Int_lower1 RS subset_imp_leadsTo]) 1);
+by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 qed "LeadsTo_UNIV";
 Addsimps [LeadsTo_UNIV];
 
@@ -142,7 +149,8 @@
 
 Goal "[| F : (A-A') Co (A Un A');  F : transient (A-A') |]   \
 \     ==> F : A LeadsTo A'";
-by (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_def]) 1);
+by (asm_full_simp_tac
+    (simpset() addsimps [LeadsTo_def, Constrains_eq_constrains]) 1);
 by (rtac (ensuresI RS leadsTo_Basis) 1);
 by (blast_tac (claset() addIs [transient_strengthen]) 2);
 by (blast_tac (claset() addIs [constrains_weaken]) 1);
@@ -244,7 +252,8 @@
 (*Special case of PSP: Misra's "stable conjunction"*)
 Goal "[| F : A LeadsTo A';  F : Stable B |] \
 \     ==> F : (A Int B) LeadsTo (A' Int B)";
-by (full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1);
+by (full_simp_tac
+    (simpset() addsimps [LeadsTo_eq_leadsTo, Stable_eq_stable]) 1);
 by (dtac psp_stable 1);
 by (assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps Int_ac) 1);
@@ -255,9 +264,10 @@
 by (asm_simp_tac (simpset() addsimps PSP_stable::Int_ac) 1);
 qed "PSP_stable2";
 
-Goalw [LeadsTo_def, Constrains_def]
-     "[| F : A LeadsTo A'; F : B Co B' |] \
+Goal "[| F : A LeadsTo A'; F : B Co B' |] \
 \     ==> F : (A Int B) LeadsTo ((A' Int B) Un (B' - B))";
+by (full_simp_tac
+    (simpset() addsimps [LeadsTo_def, Constrains_eq_constrains]) 1);
 by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1);
 qed "PSP";
 
@@ -292,7 +302,7 @@
 \        ALL m. F : (A Int f-``{m}) LeadsTo                     \
 \                           ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
 \     ==> F : A LeadsTo B";
-by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
+by (full_simp_tac (simpset() addsimps [LeadsTo_eq_leadsTo]) 1);
 by (etac leadsTo_wf_induct 1);
 by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
 qed "LeadsTo_wf_induct";
@@ -355,7 +365,8 @@
 Goal "[| F : A LeadsTo A';  F : Stable A';   \
 \        F : B LeadsTo B';  F : Stable B' |] \
 \     ==> F : (A Int B) LeadsTo (A' Int B')";
-by (full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1);
+by (full_simp_tac
+    (simpset() addsimps [LeadsTo_eq_leadsTo, Stable_eq_stable]) 1);
 by (blast_tac (claset() addIs [stable_completion, leadsTo_weaken]) 1);
 qed "Stable_completion";
 
@@ -373,7 +384,8 @@
 Goal "[| F : A LeadsTo (A' Un C);  F : A' Co (A' Un C); \
 \        F : B LeadsTo (B' Un C);  F : B' Co (B' Un C) |] \
 \     ==> F : (A Int B) LeadsTo ((A' Int B') Un C)";
-by (full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_def,
+by (full_simp_tac
+    (simpset() addsimps [LeadsTo_eq_leadsTo, Constrains_eq_constrains,
 				       Int_Un_distrib]) 1);
 by (blast_tac (claset() addIs [completion, leadsTo_weaken]) 1);
 qed "Completion";
diff -r a91b4cfd3104 -r 70d758762c50 src/HOL/UNITY/SubstAx.thy
--- a/src/HOL/UNITY/SubstAx.thy	Tue May 04 13:32:53 1999 +0200
+++ b/src/HOL/UNITY/SubstAx.thy	Tue May 04 13:47:28 1999 +0200
@@ -13,6 +13,5 @@
 
 defs
    LeadsTo_def
-    "A LeadsTo B == {F. F : (reachable F  Int  A) leadsTo
-	   	            (reachable F  Int  B)}"
+    "A LeadsTo B == {F. F : (reachable F Int A) leadsTo  B}"
 end