# HG changeset patch
# User paulson
# Date 927553893 -7200
# Node ID 6b2b4ec581780b36075479dc56225872d9ac51c2
# Parent  614a76ce9bc610af5da724d8a9d805d858a19014
new rule single_leadsTo_I;  stronger PSP rule

diff -r 614a76ce9bc6 -r 6b2b4ec58178 src/HOL/UNITY/WFair.ML
--- a/src/HOL/UNITY/WFair.ML	Mon May 24 15:50:53 1999 +0200
+++ b/src/HOL/UNITY/WFair.ML	Mon May 24 15:51:33 1999 +0200
@@ -127,6 +127,12 @@
 by (blast_tac (claset() addIs [leadsTo_Union]) 1);
 qed "leadsTo_Un";
 
+val prems = 
+Goal "(!!x. x : A ==> F : {x} leadsTo B) ==> F : A leadsTo B";
+by (stac (UN_singleton RS sym) 1 THEN rtac leadsTo_UN 1);
+by (blast_tac (claset() addIs prems) 1);
+qed "single_leadsTo_I";
+
 
 (*The INDUCTION rule as we should have liked to state it*)
 val major::prems = Goalw [leadsTo_def]
@@ -213,7 +219,8 @@
 
 
 (*Binary union version*)
-Goal "[| F : A leadsTo A'; F : B leadsTo B' |]     ==> F : (A Un B) leadsTo (A' Un B')";
+Goal "[| F : A leadsTo A'; F : B leadsTo B' |] \
+\     ==> F : (A Un B) leadsTo (A' Un B')";
 by (blast_tac (claset() addIs [leadsTo_Un, 
 			       leadsTo_weaken_R]) 1);
 qed "leadsTo_Un_Un";
@@ -222,13 +229,13 @@
 (** The cancellation law **)
 
 Goal "[| F : A leadsTo (A' Un B); F : B leadsTo B' |] \
-\   ==> F : A leadsTo (A' Un B')";
+\     ==> F : A leadsTo (A' Un B')";
 by (blast_tac (claset() addIs [leadsTo_Un_Un, 
 			       subset_imp_leadsTo, leadsTo_Trans]) 1);
 qed "leadsTo_cancel2";
 
 Goal "[| F : A leadsTo (A' Un B); F : (B-A') leadsTo B' |] \
-\   ==> F : A leadsTo (A' Un B')";
+\     ==> F : A leadsTo (A' Un B')";
 by (rtac leadsTo_cancel2 1);
 by (assume_tac 2);
 by (ALLGOALS Asm_simp_tac);
@@ -286,24 +293,27 @@
 
 Goalw [ensures_def, constrains_def]
    "[| F : A ensures A'; F : B co B' |] \
-\   ==> F : (A Int B) ensures ((A' Int B) Un (B' - B))";
+\   ==> F : (A Int B') ensures ((A' Int B) Un (B' - B))";
+by (Clarify_tac 1);  (*speeds up the proof*)
 by (blast_tac (claset() addIs [transient_strengthen]) 1);
 qed "psp_ensures";
 
 Goal "[| F : A leadsTo A'; F : B co B' |] \
-\     ==> F : (A Int B) leadsTo ((A' Int B) Un (B' - B))";
+\     ==> F : (A Int B') leadsTo ((A' Int B) Un (B' - B))";
 by (etac leadsTo_induct 1);
 by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3);
 (*Transitivity case has a delicate argument involving "cancellation"*)
 by (rtac leadsTo_Un_duplicate2 2);
 by (etac leadsTo_cancel_Diff1 2);
 by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2);
+by (blast_tac (claset() addIs [leadsTo_weaken_L] 
+                        addDs [constrains_imp_subset]) 2);
 (*Basis case*)
 by (blast_tac (claset() addIs [leadsTo_Basis, psp_ensures]) 1);
 qed "psp";
 
 Goal "[| F : A leadsTo A'; F : B co B' |] \
-\   ==> F : (B Int A) leadsTo ((B Int A') Un (B' - B))";
+\   ==> F : (B' Int A) leadsTo ((B Int A') Un (B' - B))";
 by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1);
 qed "psp2";
 
@@ -313,10 +323,7 @@
 \   ==> F : (A Int B) leadsTo ((A' Int B) Un B')";
 by (dtac psp 1);
 by (assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 1);
-by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 1);
-by (etac leadsTo_Diff 1);
-by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
+by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
 qed "psp_unless";
 
 
@@ -504,13 +511,13 @@
     (simpset() addsimps [wlt_increasing, Un_assoc, Un_absorb2]) 2);
 by (subgoal_tac "F : (A Int W - C) leadsTo (A' Int W Un C)" 1);
 by (simp_tac (simpset() addsimps [Int_Diff]) 2);
-by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken_R]) 2);
+by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken]) 2);
 (** LEVEL 7 **)
 by (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C)" 1);
-by (blast_tac (claset() addIs [wlt_leadsTo, leadsTo_Un_Un, 
-                               psp2 RS leadsTo_weaken_R, 
-			       subset_refl RS subset_imp_leadsTo, 
-			       leadsTo_Un_duplicate2]) 2);
+by (rtac leadsTo_Un_duplicate2 2);
+by (blast_tac (claset() addIs [leadsTo_Un_Un, 
+                               wlt_leadsTo RS psp2 RS leadsTo_weaken, 
+                               subset_refl RS subset_imp_leadsTo]) 2);
 by (dtac leadsTo_Diff 1);
 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
 by (subgoal_tac "A Int B <= A Int W" 1);