src/HOL/UNITY/WFair.ML

 From Misra, "A Logic for Concurrent Programming", 1994
 *)
 
 open WFair;
 
-goal thy "Union(B) Int A = Union((%C. C Int A)``B)";
+Goal "Union(B) Int A = Union((%C. C Int A)``B)";
 by (Blast_tac 1);
 qed "Int_Union_Union";
 
 
 (*** transient ***)
 
-goalw thy [stable_def, constrains_def, transient_def]
+Goalw [stable_def, constrains_def, transient_def]
     "!!A. [| stable Acts A; transient Acts A |] ==> A = {}";
 by (Blast_tac 1);
 qed "stable_transient_empty";
 
-goalw thy [transient_def]
+Goalw [transient_def]
     "!!A. [| transient Acts A; B<=A |] ==> transient Acts B";
 by (Clarify_tac 1);
 by (rtac bexI 1 THEN assume_tac 2);
 by (Blast_tac 1);
 qed "transient_strengthen";
 
-goalw thy [transient_def]
+Goalw [transient_def]
     "!!A. [| act:Acts;  A <= Domain act;  act^^A <= Compl A |] \
 \         ==> transient Acts A";
 by (Blast_tac 1);
 qed "transient_mem";
 
 
 (*** ensures ***)
 
-goalw thy [ensures_def]
+Goalw [ensures_def]
     "!!Acts. [| constrains Acts (A-B) (A Un B); transient Acts (A-B) |] \
 \            ==> ensures Acts A B";
 by (Blast_tac 1);
 qed "ensuresI";
 
-goalw thy [ensures_def]
+Goalw [ensures_def]
     "!!Acts. ensures Acts A B  \
 \            ==> constrains Acts (A-B) (A Un B) & transient Acts (A-B)";
 by (Blast_tac 1);
 qed "ensuresD";
 
 (*The L-version (precondition strengthening) doesn't hold for ENSURES*)
-goalw thy [ensures_def]
+Goalw [ensures_def]
     "!!Acts. [| ensures Acts A A'; A'<=B' |] ==> ensures Acts A B'";
 by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
 qed "ensures_weaken_R";
 
-goalw thy [ensures_def, constrains_def, transient_def]
+Goalw [ensures_def, constrains_def, transient_def]
     "!!Acts. Acts ~= {} ==> ensures Acts A UNIV";
 by (Asm_simp_tac 1);  (*omitting this causes PROOF FAILED, even with Safe_tac*)
 by (Blast_tac 1);
 qed "ensures_UNIV";
 
-goalw thy [ensures_def]
+Goalw [ensures_def]
     "!!Acts. [| 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')";
 by (asm_simp_tac (simpset() addsimps [Int_Un_distrib RS sym,

 
 (*Synonyms for the theorems produced by the inductive defn package*)
 bind_thm ("leadsTo_Basis", leadsto.Basis);
 bind_thm ("leadsTo_Trans", leadsto.Trans);
 
-goal thy "!!Acts. act: Acts ==> leadsTo Acts A UNIV";
+Goal "!!Acts. act: Acts ==> leadsTo Acts A UNIV";
 by (blast_tac (claset() addIs [ensures_UNIV RS leadsTo_Basis]) 1);
 qed "leadsTo_UNIV";
 Addsimps [leadsTo_UNIV];
 
 (*Useful with cancellation, disjunction*)
-goal thy "!!Acts. leadsTo Acts A (A' Un A') ==> leadsTo Acts A A'";
+Goal "!!Acts. leadsTo Acts A (A' Un A') ==> leadsTo Acts A A'";
 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
 qed "leadsTo_Un_duplicate";
 
-goal thy "!!Acts. leadsTo Acts A (A' Un C Un C) ==> leadsTo Acts A (A' Un C)";
+Goal "!!Acts. leadsTo Acts A (A' Un C Un C) ==> leadsTo Acts A (A' Un C)";
 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
 qed "leadsTo_Un_duplicate2";
 
 (*The Union introduction rule as we should have liked to state it*)
 val prems = goal thy

 by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
 by (blast_tac (claset() addIs (leadsto.Union::prems)) 1);
 qed "leadsTo_UN";
 
 (*Binary union introduction rule*)
-goal thy
+Goal
   "!!C. [| 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";
 

 br (major RS leadsto.induct) 1;
 by (REPEAT (blast_tac (claset() addIs prems) 1));
 qed "leadsTo_induct";
 
 
-goal thy "!!A B. [| A<=B;  id: Acts |] ==> leadsTo Acts A B";
+Goal "!!A B. [| A<=B;  id: Acts |] ==> leadsTo Acts A B";
 by (rtac leadsTo_Basis 1);
 by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
 by (Blast_tac 1);
 qed "subset_imp_leadsTo";
 

 Addsimps [empty_leadsTo];
 
 
 (*There's a direct proof by leadsTo_Trans and subset_imp_leadsTo, but it
   needs the extra premise id:Acts*)
-goal thy "!!Acts. leadsTo Acts A A' ==> A'<=B' --> leadsTo Acts A B'";
+Goal "!!Acts. leadsTo Acts A A' ==> A'<=B' --> leadsTo Acts A B'";
 by (etac leadsTo_induct 1);
 by (Clarify_tac 3);
 by (blast_tac (claset() addIs [leadsTo_Union]) 3);
 by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
 by (blast_tac (claset() addIs [leadsTo_Basis, ensures_weaken_R]) 1);
 qed_spec_mp "leadsTo_weaken_R";
 
 
-goal thy "!!Acts. [| leadsTo Acts A A'; B<=A; id: Acts |] ==>  \
+Goal "!!Acts. [| leadsTo Acts A A'; B<=A; id: Acts |] ==>  \
 \                 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 thy
+Goal
   "!!C. 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 thy
+Goal
   "!!C. 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 thy
+Goal
   "!!C. 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 thy
+Goal
    "!!Acts. [| 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);
 qed "leadsTo_weaken";
 
 
 (*Set difference: maybe combine with leadsTo_weaken_L??*)
-goal thy
+Goal
   "!!C. [| 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";
 

 by (blast_tac (claset() addIs [leadsTo_UN_UN] 
                         addIs prems) 1);
 qed "leadsTo_UN_UN_noindex";
 
 (*Version with no index set*)
-goal thy
+Goal
    "!!Acts. 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 thy "!!Acts. [| leadsTo Acts A A'; leadsTo Acts B B' |] \
+Goal "!!Acts. [| leadsTo Acts A A'; leadsTo Acts B B' |] \
 \                 ==> leadsTo Acts (A Un B) (A' Un B')";
 by (blast_tac (claset() addIs [leadsTo_Un, 
 			       leadsTo_weaken_R]) 1);
 qed "leadsTo_Un_Un";
 
 
 (** The cancellation law **)
 
-goal thy
+Goal
    "!!Acts. [| 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 thy
+Goal
    "!!Acts. [| 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 thy
+Goal
    "!!Acts. [| 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 thy
+Goal
    "!!Acts. [| 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);

 
 
 
 (** The impossibility law **)
 
-goal thy "!!Acts. leadsTo Acts A B ==> B={} --> A={}";
+Goal "!!Acts. leadsTo Acts A B ==> B={} --> A={}";
 by (etac leadsTo_induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
 by (Blast_tac 1);
 val lemma = result() RS mp;
 
-goal thy "!!Acts. leadsTo Acts A {} ==> A={}";
+Goal "!!Acts. leadsTo Acts A {} ==> A={}";
 by (blast_tac (claset() addSIs [lemma]) 1);
 qed "leadsTo_empty";
 
 
 (** PSP: Progress-Safety-Progress **)
 
 (*Special case of PSP: Misra's "stable conjunction".  Doesn't need id:Acts. *)
-goalw thy [stable_def]
+Goalw [stable_def]
    "!!Acts. [| leadsTo Acts A A'; stable Acts 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);

     (simpset() addsimps [ensures_def, 
 			 Diff_Int_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1);
 by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1);
 qed "PSP_stable";
 
-goal thy
+Goal
    "!!Acts. [| 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 thy [ensures_def]
+Goalw [ensures_def]
    "!!Acts. [| ensures Acts A A'; constrains Acts 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);
 by (Blast_tac 1);
 qed "PSP_ensures";
 
 
-goal thy
+Goal
    "!!Acts. [| 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);
 by (blast_tac (claset() addIs [leadsTo_Union]) 3);

 by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2);
 (*Basis case*)
 by (blast_tac (claset() addIs [leadsTo_Basis, PSP_ensures]) 1);
 qed "PSP";
 
-goal thy
+Goal
    "!!Acts. [| 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 thy [unless_def]
+Goalw [unless_def]
    "!!Acts. [| leadsTo Acts A A'; unless Acts B B'; id: Acts |] \
 \           ==> 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);

 qed "PSP_unless";
 
 
 (*** Proving the induction rules ***)
 
-goal thy
+Goal
    "!!Acts. [| 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 (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1);
 val lemma = result();
 
 
 (** Meta or object quantifier ????? **)
-goal thy
+Goal
    "!!Acts. [| 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 (REPEAT (assume_tac 2));
 by (Fast_tac 1);    (*Blast_tac: Function unknown's argument not a parameter*)
 qed "leadsTo_wf_induct";
 
 
-goal thy
+Goal
    "!!Acts. [| 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 (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
 qed "bounded_induct";
 
 
 (*Alternative proof is via the lemma leadsTo Acts (A Int f-``(lessThan m)) B*)
-goal thy
+Goal
    "!!Acts. [| 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 thy
+Goal
    "!!Acts. [| 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 thy
+Goal
    "!!Acts. [| 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")]

 
 
 (*** wlt ****)
 
 (*Misra's property W3*)
-goalw thy [wlt_def] "leadsTo Acts (wlt Acts B) B";
+Goalw [wlt_def] "leadsTo Acts (wlt Acts B) B";
 by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
 qed "wlt_leadsTo";
 
-goalw thy [wlt_def] "!!Acts. leadsTo Acts A B ==> A <= wlt Acts B";
+Goalw [wlt_def] "!!Acts. leadsTo Acts A B ==> A <= wlt Acts B";
 by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
 qed "leadsTo_subset";
 
 (*Misra's property W2*)
-goal thy "!!Acts. id: Acts ==> leadsTo Acts A B = (A <= wlt Acts B)";
+Goal "!!Acts. id: Acts ==> leadsTo Acts A B = (A <= wlt Acts B)";
 by (blast_tac (claset() addSIs [leadsTo_subset, 
 				wlt_leadsTo RS leadsTo_weaken_L]) 1);
 qed "leadsTo_eq_subset_wlt";
 
 (*Misra's property W4*)
-goal thy "!!Acts. id: Acts ==> B <= wlt Acts B";
+Goal "!!Acts. id: Acts ==> B <= wlt Acts B";
 by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS sym,
 				      subset_imp_leadsTo]) 1);
 qed "wlt_increasing";
 
 
 (*Used in the Trans case below*)
-goalw thy [constrains_def]
+Goalw [constrains_def]
    "!!Acts. [| 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)";
 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 thy
+Goal
    "!!Acts. [| 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*)
 by (blast_tac (claset() addIs [leadsTo_Basis]

 by (blast_tac (claset() addIs [leadsTo_UN, constrains_weaken]) 1);
 qed "leadsTo_123";
 
 
 (*Misra's property W5*)
-goal thy "!!Acts. id: Acts ==> constrains Acts (wlt Acts B - B) (wlt Acts B)";
+Goal "!!Acts. id: Acts ==> constrains Acts (wlt Acts B - B) (wlt Acts B)";
 by (forward_tac [wlt_leadsTo RS leadsTo_123] 1);
 by (Clarify_tac 1);
 by (subgoal_tac "Ba = wlt Acts B" 1);
 by (blast_tac (claset() addDs [leadsTo_eq_subset_wlt]) 2);
 by (Clarify_tac 1);

 qed "wlt_constrains_wlt";
 
 
 (*** Completion: Binary and General Finite versions ***)
 
-goal thy
+Goal
    "!!Acts. [| 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);

 (*Blast_tac gives PROOF FAILED*)
 by (best_tac (claset() addIs [leadsTo_Trans]) 1);
 qed "stable_completion";
 
 
-goal thy
+Goal
    "!!Acts. [| 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);

     (simpset() addsimps [stable_completion, stable_def, 
 			 ball_constrains_INT]) 1);
 qed_spec_mp "finite_stable_completion";
 
 
-goal thy
+Goal
    "!!Acts. [| 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)";

 	                delrules [subsetI]) 2);
 by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1);
 bind_thm("completion", refl RS result());
 
 
-goal thy
+Goal
    "!!Acts. [| 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);