# HG changeset patch
# User paulson
# Date 902220604 -7200
# Node ID 2fd94efb9d6462e997a6d07b08490c6ed6881723
# Parent  c449f23728dfc75b64a50ba5798559931e0f8e77
Tidying

diff -r c449f23728df -r 2fd94efb9d64 src/HOL/UNITY/WFair.ML
--- a/src/HOL/UNITY/WFair.ML	Tue Aug 04 10:48:21 1998 +0200
+++ b/src/HOL/UNITY/WFair.ML	Tue Aug 04 10:50:04 1998 +0200
@@ -34,13 +34,13 @@
 
 Goalw [ensures_def]
     "[| constrains Acts (A-B) (A Un B); transient Acts (A-B) |] \
-\            ==> ensures Acts A B";
+\    ==> ensures Acts A B";
 by (Blast_tac 1);
 qed "ensuresI";
 
 Goalw [ensures_def]
     "ensures Acts A B  \
-\            ==> constrains Acts (A-B) (A Un B) & transient Acts (A-B)";
+\    ==> constrains Acts (A-B) (A Un B) & transient Acts (A-B)";
 by (Blast_tac 1);
 qed "ensuresD";
 
@@ -58,9 +58,9 @@
 
 Goalw [ensures_def]
     "[| stable Acts C; \
-\               constrains Acts (C Int (A - A')) (A Un A'); \
-\               transient  Acts (C Int (A-A')) |]   \
-\           ==> ensures Acts (C Int A) (C Int A')";
+\       constrains Acts (C Int (A - A')) (A Un A'); \
+\       transient  Acts (C Int (A-A')) |]   \
+\   ==> ensures Acts (C Int A) (C Int A')";
 by (asm_simp_tac (simpset() addsimps [Int_Un_distrib RS sym,
 				      Diff_Int_distrib RS sym,
 				      stable_constrains_Int]) 1);
@@ -100,8 +100,7 @@
 qed "leadsTo_UN";
 
 (*Binary union introduction rule*)
-Goal
-  "[| leadsTo Acts A C; leadsTo Acts B C |] ==> leadsTo Acts (A Un B) C";
+Goal "[| leadsTo Acts A C; leadsTo Acts B C |] ==> leadsTo Acts (A Un B) C";
 by (stac Un_eq_Union 1);
 by (blast_tac (claset() addIs [leadsTo_Union]) 1);
 qed "leadsTo_Un";
@@ -142,34 +141,30 @@
 
 
 Goal "[| leadsTo Acts A A'; B<=A; id: Acts |] ==>  \
-\                 leadsTo Acts B A'";
+\         leadsTo Acts B A'";
 by (blast_tac (claset() addIs [leadsTo_Basis, leadsTo_Trans, 
 			       subset_imp_leadsTo]) 1);
 qed_spec_mp "leadsTo_weaken_L";
 
 (*Distributes over binary unions*)
-Goal
-  "id: Acts ==> \
+Goal "id: Acts ==> \
 \       leadsTo Acts (A Un B) C  =  (leadsTo Acts A C & leadsTo Acts B C)";
 by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1);
 qed "leadsTo_Un_distrib";
 
-Goal
-  "id: Acts ==> \
+Goal "id: Acts ==> \
 \       leadsTo Acts (UN i:I. A i) B  =  (ALL i : I. leadsTo Acts (A i) B)";
 by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1);
 qed "leadsTo_UN_distrib";
 
-Goal
-  "id: Acts ==> \
+Goal "id: Acts ==> \
 \       leadsTo Acts (Union S) B  =  (ALL A : S. leadsTo Acts A B)";
 by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1);
 qed "leadsTo_Union_distrib";
 
 
-Goal
-   "[| leadsTo Acts A A'; id: Acts; B<=A; A'<=B' |] \
-\           ==> leadsTo Acts B B'";
+Goal "[| leadsTo Acts A A'; id: Acts; B<=A; A'<=B' |] \
+\   ==> leadsTo Acts B B'";
 (*PROOF FAILED: why?*)
 by (blast_tac (claset() addIs [leadsTo_Trans, leadsTo_weaken_R,
 			       leadsTo_weaken_L]) 1);
@@ -177,8 +172,7 @@
 
 
 (*Set difference: maybe combine with leadsTo_weaken_L??*)
-Goal
-  "[| leadsTo Acts (A-B) C; leadsTo Acts B C; id: Acts |] \
+Goal "[| leadsTo Acts (A-B) C; leadsTo Acts B C; id: Acts |] \
 \       ==> leadsTo Acts A C";
 by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1);
 qed "leadsTo_Diff";
@@ -205,16 +199,15 @@
 qed "leadsTo_UN_UN_noindex";
 
 (*Version with no index set*)
-Goal
-   "ALL i. leadsTo Acts (A i) (A' i) \
-\           ==> leadsTo Acts (UN i. A i) (UN i. A' i)";
+Goal "ALL i. leadsTo Acts (A i) (A' i) \
+\   ==> leadsTo Acts (UN i. A i) (UN i. A' i)";
 by (blast_tac (claset() addIs [leadsTo_UN_UN]) 1);
 qed "all_leadsTo_UN_UN";
 
 
 (*Binary union version*)
 Goal "[| leadsTo Acts A A'; leadsTo Acts B B' |] \
-\                 ==> leadsTo Acts (A Un B) (A' Un B')";
+\         ==> leadsTo Acts (A Un B) (A' Un B')";
 by (blast_tac (claset() addIs [leadsTo_Un, 
 			       leadsTo_weaken_R]) 1);
 qed "leadsTo_Un_Un";
@@ -222,31 +215,27 @@
 
 (** The cancellation law **)
 
-Goal
-   "[| leadsTo Acts A (A' Un B); leadsTo Acts B B'; id: Acts |] \
-\           ==> leadsTo Acts A (A' Un B')";
+Goal "[| leadsTo Acts A (A' Un B); leadsTo Acts B B'; id: Acts |] \
+\   ==> leadsTo Acts A (A' Un B')";
 by (blast_tac (claset() addIs [leadsTo_Un_Un, 
 			       subset_imp_leadsTo, leadsTo_Trans]) 1);
 qed "leadsTo_cancel2";
 
-Goal
-   "[| leadsTo Acts A (A' Un B); leadsTo Acts (B-A') B'; id: Acts |] \
-\           ==> leadsTo Acts A (A' Un B')";
+Goal "[| leadsTo Acts A (A' Un B); leadsTo Acts (B-A') B'; id: Acts |] \
+\   ==> leadsTo Acts A (A' Un B')";
 by (rtac leadsTo_cancel2 1);
 by (assume_tac 2);
 by (ALLGOALS Asm_simp_tac);
 qed "leadsTo_cancel_Diff2";
 
-Goal
-   "[| leadsTo Acts A (B Un A'); leadsTo Acts B B'; id: Acts |] \
-\           ==> leadsTo Acts A (B' Un A')";
+Goal "[| leadsTo Acts A (B Un A'); leadsTo Acts B B'; id: Acts |] \
+\   ==> leadsTo Acts A (B' Un A')";
 by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
 by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1);
 qed "leadsTo_cancel1";
 
-Goal
-   "[| leadsTo Acts A (B Un A'); leadsTo Acts (B-A') B'; id: Acts |] \
-\           ==> leadsTo Acts A (B' Un A')";
+Goal "[| leadsTo Acts A (B Un A'); leadsTo Acts (B-A') B'; id: Acts |] \
+\   ==> leadsTo Acts A (B' Un A')";
 by (rtac leadsTo_cancel1 1);
 by (assume_tac 2);
 by (ALLGOALS Asm_simp_tac);
@@ -273,7 +262,7 @@
 (*Special case of PSP: Misra's "stable conjunction".  Doesn't need id:Acts. *)
 Goalw [stable_def]
    "[| leadsTo Acts A A'; stable Acts B |] \
-\           ==> leadsTo Acts (A Int B) (A' Int B)";
+\   ==> leadsTo Acts (A Int B) (A' Int B)";
 by (etac leadsTo_induct 1);
 by (simp_tac (simpset() addsimps [Int_Union_Union]) 3);
 by (blast_tac (claset() addIs [leadsTo_Union]) 3);
@@ -285,16 +274,15 @@
 by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1);
 qed "PSP_stable";
 
-Goal
-   "[| leadsTo Acts A A'; stable Acts B |] \
-\           ==> leadsTo Acts (B Int A) (B Int A')";
+Goal "[| leadsTo Acts A A'; stable Acts B |] \
+\   ==> leadsTo Acts (B Int A) (B Int A')";
 by (asm_simp_tac (simpset() addsimps (PSP_stable::Int_ac)) 1);
 qed "PSP_stable2";
 
 
 Goalw [ensures_def]
    "[| ensures Acts A A'; constrains Acts B B' |] \
-\           ==> ensures Acts (A Int B) ((A' Int B) Un (B' - B))";
+\   ==> ensures Acts (A Int B) ((A' Int B) Un (B' - B))";
 by Safe_tac;
 by (blast_tac (claset() addIs [constrainsI] addDs [constrainsD]) 1);
 by (etac transient_strengthen 1);
@@ -302,8 +290,7 @@
 qed "PSP_ensures";
 
 
-Goal
-   "[| leadsTo Acts A A'; constrains Acts B B'; id: Acts |] \
+Goal "[| leadsTo Acts A A'; constrains Acts B B'; id: Acts |] \
 \           ==> leadsTo Acts (A Int B) ((A' Int B) Un (B' - B))";
 by (etac leadsTo_induct 1);
 by (simp_tac (simpset() addsimps [Int_Union_Union]) 3);
@@ -317,16 +304,15 @@
 by (blast_tac (claset() addIs [leadsTo_Basis, PSP_ensures]) 1);
 qed "PSP";
 
-Goal
-   "[| leadsTo Acts A A'; constrains Acts B B'; id: Acts |] \
-\           ==> leadsTo Acts (B Int A) ((B Int A') Un (B' - B))";
+Goal "[| leadsTo Acts A A'; constrains Acts B B'; id: Acts |] \
+\   ==> leadsTo Acts (B Int A) ((B Int A') Un (B' - B))";
 by (asm_simp_tac (simpset() addsimps (PSP::Int_ac)) 1);
 qed "PSP2";
 
 
 Goalw [unless_def]
    "[| leadsTo Acts A A'; unless Acts B B'; id: Acts |] \
-\           ==> leadsTo Acts (A Int B) ((A' Int B) Un B')";
+\   ==> leadsTo Acts (A Int B) ((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]) 2);
@@ -339,12 +325,11 @@
 
 (*** Proving the induction rules ***)
 
-Goal
-   "[| wf r;     \
-\              ALL m. leadsTo Acts (A Int f-``{m})                     \
-\                                  ((A Int f-``(r^-1 ^^ {m})) Un B);   \
-\              id: Acts |] \
-\           ==> leadsTo Acts (A Int f-``{m}) B";
+Goal "[| wf r;     \
+\        ALL m. leadsTo Acts (A Int f-``{m})                     \
+\                            ((A Int f-``(r^-1 ^^ {m})) Un B);   \
+\        id: Acts |] \
+\     ==> leadsTo Acts (A Int f-``{m}) B";
 by (eres_inst_tac [("a","m")] wf_induct 1);
 by (subgoal_tac "leadsTo Acts (A Int (f -`` (r^-1 ^^ {x}))) B" 1);
 by (stac vimage_eq_UN 2);
@@ -355,12 +340,11 @@
 
 
 (** Meta or object quantifier ????? **)
-Goal
-   "[| wf r;     \
-\              ALL m. leadsTo Acts (A Int f-``{m})                     \
-\                                  ((A Int f-``(r^-1 ^^ {m})) Un B);   \
-\              id: Acts |] \
-\           ==> leadsTo Acts A B";
+Goal "[| wf r;     \
+\        ALL m. leadsTo Acts (A Int f-``{m})                     \
+\                            ((A Int f-``(r^-1 ^^ {m})) Un B);   \
+\        id: Acts |] \
+\     ==> leadsTo Acts A B";
 by (res_inst_tac [("t", "A")] subst 1);
 by (rtac leadsTo_UN 2);
 by (etac lemma 2);
@@ -369,12 +353,11 @@
 qed "leadsTo_wf_induct";
 
 
-Goal
-   "[| wf r;     \
-\              ALL m:I. leadsTo Acts (A Int f-``{m})                   \
-\                                  ((A Int f-``(r^-1 ^^ {m})) Un B);   \
-\              id: Acts |] \
-\           ==> leadsTo Acts A ((A - (f-``I)) Un B)";
+Goal "[| wf r;     \
+\        ALL m:I. leadsTo Acts (A Int f-``{m})                   \
+\                            ((A Int f-``(r^-1 ^^ {m})) Un B);   \
+\        id: Acts |] \
+\     ==> leadsTo Acts A ((A - (f-``I)) Un B)";
 by (etac leadsTo_wf_induct 1);
 by Safe_tac;
 by (case_tac "m:I" 1);
@@ -384,32 +367,29 @@
 
 
 (*Alternative proof is via the lemma leadsTo Acts (A Int f-``(lessThan m)) B*)
-Goal
-   "[| ALL m. leadsTo Acts (A Int f-``{m})                     \
-\                                  ((A Int f-``(lessThan m)) Un B);   \
-\              id: Acts |] \
-\           ==> leadsTo Acts A B";
+Goal "[| ALL m. leadsTo Acts (A Int f-``{m})                     \
+\                            ((A Int f-``(lessThan m)) Un B);   \
+\        id: Acts |] \
+\     ==> leadsTo Acts A B";
 by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
 by (assume_tac 2);
 by (Asm_simp_tac 1);
 qed "lessThan_induct";
 
-Goal
-   "[| ALL m:(greaterThan l). leadsTo Acts (A Int f-``{m})   \
-\                                        ((A Int f-``(lessThan m)) Un B);   \
-\              id: Acts |] \
-\           ==> leadsTo Acts A ((A Int (f-``(atMost l))) Un B)";
+Goal "[| ALL m:(greaterThan l). leadsTo Acts (A Int f-``{m})   \
+\                                  ((A Int f-``(lessThan m)) Un B);   \
+\        id: Acts |] \
+\     ==> leadsTo Acts A ((A Int (f-``(atMost l))) Un B)";
 by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);
 by (rtac (wf_less_than RS bounded_induct) 1);
 by (assume_tac 2);
 by (Asm_simp_tac 1);
 qed "lessThan_bounded_induct";
 
-Goal
-   "[| ALL m:(lessThan l). leadsTo Acts (A Int f-``{m})   \
-\                                    ((A Int f-``(greaterThan m)) Un B);   \
-\              id: Acts |] \
-\           ==> leadsTo Acts A ((A Int (f-``(atLeast l))) Un B)";
+Goal "[| ALL m:(lessThan l). leadsTo Acts (A Int f-``{m})   \
+\                              ((A Int f-``(greaterThan m)) Un B);   \
+\        id: Acts |] \
+\     ==> leadsTo Acts A ((A Int (f-``(atLeast l))) Un B)";
 by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
     (wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1);
 by (assume_tac 2);
@@ -449,17 +429,16 @@
 (*Used in the Trans case below*)
 Goalw [constrains_def]
    "[| B <= A2;  \
-\              constrains Acts (A1 - B) (A1 Un B); \
-\              constrains Acts (A2 - C) (A2 Un C) |] \
-\           ==> constrains Acts (A1 Un A2 - C) (A1 Un A2 Un C)";
+\      constrains Acts (A1 - B) (A1 Un B); \
+\      constrains Acts (A2 - C) (A2 Un C) |] \
+\   ==> constrains Acts (A1 Un A2 - C) (A1 Un A2 Un C)";
 by (Clarify_tac 1);
 by (blast_tac (claset() addSDs [bspec]) 1);
 val lemma1 = result();
 
 
 (*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
-Goal
-   "[| leadsTo Acts A A';  id: Acts |] ==> \
+Goal "[| leadsTo Acts A A';  id: Acts |] ==> \
 \      EX B. A<=B & leadsTo Acts B A' & constrains Acts (B-A') (B Un A')";
 by (etac leadsTo_induct 1);
 (*Basis*)
@@ -491,10 +470,9 @@
 
 (*** Completion: Binary and General Finite versions ***)
 
-Goal
-   "[| leadsTo Acts A A';  stable Acts A';   \
-\              leadsTo Acts B B';  stable Acts B';  id: Acts |] \
-\           ==> leadsTo Acts (A Int B) (A' Int B')";
+Goal "[| leadsTo Acts A A';  stable Acts A';   \
+\      leadsTo Acts B B';  stable Acts B';  id: Acts |] \
+\   ==> leadsTo Acts (A Int B) (A' Int B')";
 by (subgoal_tac "stable Acts (wlt Acts B')" 1);
 by (asm_full_simp_tac (simpset() addsimps [stable_def]) 2);
 by (EVERY [etac (constrains_Un RS constrains_weaken) 2,
@@ -513,11 +491,10 @@
 qed "stable_completion";
 
 
-Goal
-   "[| finite I;  id: Acts |]                     \
-\           ==> (ALL i:I. leadsTo Acts (A i) (A' i)) -->  \
-\               (ALL i:I. stable Acts (A' i)) -->         \
-\               leadsTo Acts (INT i:I. A i) (INT i:I. A' i)";
+Goal "[| finite I;  id: Acts |]                     \
+\   ==> (ALL i:I. leadsTo Acts (A i) (A' i)) -->  \
+\       (ALL i:I. stable Acts (A' i)) -->         \
+\       leadsTo Acts (INT i:I. A i) (INT i:I. A' i)";
 by (etac finite_induct 1);
 by (Asm_simp_tac 1);
 by (asm_simp_tac 
@@ -526,12 +503,11 @@
 qed_spec_mp "finite_stable_completion";
 
 
-Goal
-   "[| W = wlt Acts (B' Un C);     \
-\              leadsTo Acts A (A' Un C);  constrains Acts A' (A' Un C);   \
-\              leadsTo Acts B (B' Un C);  constrains Acts B' (B' Un C);   \
-\              id: Acts |] \
-\           ==> leadsTo Acts (A Int B) ((A' Int B') Un C)";
+Goal "[| W = wlt Acts (B' Un C);     \
+\      leadsTo Acts A (A' Un C);  constrains Acts A' (A' Un C);   \
+\      leadsTo Acts B (B' Un C);  constrains Acts B' (B' Un C);   \
+\      id: Acts |] \
+\   ==> leadsTo Acts (A Int B) ((A' Int B') Un C)";
 by (subgoal_tac "constrains Acts (W-C) (W Un B' Un C)" 1);
 by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt] 
 			       MRS constrains_Un RS constrains_weaken]) 2);
@@ -556,11 +532,10 @@
 bind_thm("completion", refl RS result());
 
 
-Goal
-   "[| finite I;  id: Acts |] \
-\           ==> (ALL i:I. leadsTo Acts (A i) (A' i Un C)) -->  \
-\               (ALL i:I. constrains Acts (A' i) (A' i Un C)) --> \
-\               leadsTo Acts (INT i:I. A i) ((INT i:I. A' i) Un C)";
+Goal "[| finite I;  id: Acts |] \
+\   ==> (ALL i:I. leadsTo Acts (A i) (A' i Un C)) -->  \
+\       (ALL i:I. constrains Acts (A' i) (A' i Un C)) --> \
+\       leadsTo Acts (INT i:I. A i) ((INT i:I. A' i) Un C)";
 by (etac finite_induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (Clarify_tac 1);
diff -r c449f23728df -r 2fd94efb9d64 src/HOL/UNITY/WFair.thy
--- a/src/HOL/UNITY/WFair.thy	Tue Aug 04 10:48:21 1998 +0200
+++ b/src/HOL/UNITY/WFair.thy	Tue Aug 04 10:50:04 1998 +0200
@@ -19,6 +19,7 @@
 
   ensures :: "[('a * 'a)set set, 'a set, 'a set] => bool"
     "ensures Acts A B == constrains Acts (A-B) (A Un B) & transient Acts (A-B)"
+			(*(unless Acts A B) would be equivalent*)
 
 consts leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool"
        leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set"