--- 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);
--- 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"