--- a/src/HOL/UNITY/Channel.ML Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/Channel.ML Thu Apr 29 10:51:58 1999 +0200
@@ -24,7 +24,7 @@
by (Blast_tac 1);
qed_spec_mp "minSet_nonempty";
-Goal "F : leadsTo (minSet -`` {Some x}) (minSet -`` (Some``greaterThan x))";
+Goal "F : (minSet -`` {Some x}) leadsTo (minSet -`` (Some``greaterThan x))";
by (rtac leadsTo_weaken 1);
by (rtac ([UC2, UC1] MRS psp) 1);
by (ALLGOALS Asm_simp_tac);
@@ -36,7 +36,7 @@
(*The induction*)
-Goal "F : leadsTo (UNIV-{{}}) (minSet -`` (Some``atLeast y))";
+Goal "F : (UNIV-{{}}) leadsTo (minSet -`` (Some``atLeast y))";
by (rtac leadsTo_weaken_R 1);
by (res_inst_tac [("l", "y"), ("f", "the o minSet"), ("B", "{}")]
greaterThan_bounded_induct 1);
@@ -52,7 +52,7 @@
val lemma = result();
-Goal "!!y::nat. F : leadsTo (UNIV-{{}}) {s. y ~: s}";
+Goal "!!y::nat. F : (UNIV-{{}}) leadsTo {s. y ~: s}";
by (rtac (lemma RS leadsTo_weaken_R) 1);
by (Clarify_tac 1);
by (forward_tac [minSet_nonempty] 1);
--- a/src/HOL/UNITY/Channel.thy Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/Channel.thy Thu Apr 29 10:51:58 1999 +0200
@@ -21,10 +21,10 @@
rules
- UC1 "F : constrains (minSet -`` {Some x}) (minSet -`` (Some``atLeast x))"
+ UC1 "F : (minSet -`` {Some x}) co (minSet -`` (Some``atLeast x))"
- (* UC1 "F : constrains {s. minSet s = x} {s. x <= minSet s}" *)
+ (* UC1 "F : {s. minSet s = x} co {s. x <= minSet s}" *)
- UC2 "F : leadsTo (minSet -`` {Some x}) {s. x ~: s}"
+ UC2 "F : (minSet -`` {Some x}) leadsTo {s. x ~: s}"
end
--- a/src/HOL/UNITY/Client.ML Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/Client.ML Thu Apr 29 10:51:58 1999 +0200
@@ -124,8 +124,7 @@
Goal "Cli_prg : \
\ (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
\ Int Invariant giv_meets_ask) \
-\ guarantees (LeadsTo {s. k < size (giv s)} \
-\ {s. k < size (rel s)})";
+\ guarantees ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})";
by (rtac guaranteesI 1);
by (Clarify_tac 1);
by (rtac Stable_transient_reachable_LeadsTo 1);
--- a/src/HOL/UNITY/Common.ML Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/Common.ML Thu Apr 29 10:51:58 1999 +0200
@@ -11,7 +11,7 @@
*)
(*Misra's property CMT4: t exceeds no common meeting time*)
-Goal "[| ALL m. F : Constrains {m} (maxfg m); n: common |] \
+Goal "[| ALL m. F : {m} Co (maxfg m); n: common |] \
\ ==> F : Stable (atMost n)";
by (dres_inst_tac [("M", "{t. t<=n}")] Elimination_sing 1);
by (asm_full_simp_tac
@@ -22,7 +22,7 @@
qed "common_stable";
Goal "[| Init F <= atMost n; \
-\ ALL m. F : Constrains {m} (maxfg m); n: common |] \
+\ ALL m. F : {m} Co (maxfg m); n: common |] \
\ ==> F : Invariant (atMost n)";
by (asm_simp_tac (simpset() addsimps [InvariantI, common_stable]) 1);
qed "common_Invariant";
@@ -30,14 +30,14 @@
(*** Some programs that implement the safety property above ***)
-Goal "SKIP : constrains {m} (maxfg m)";
+Goal "SKIP : {m} co (maxfg m)";
by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj,
fasc]) 1);
result();
(*This one is t := ftime t || t := gtime t*)
Goal "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}) \
-\ : constrains {m} (maxfg m)";
+\ : {m} co (maxfg m)";
by (simp_tac (simpset() addsimps [constrains_def, maxfg_def,
le_max_iff_disj, fasc]) 1);
by (Blast_tac 1);
@@ -45,7 +45,7 @@
(*This one is t := max (ftime t) (gtime t)*)
Goal "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}) \
-\ : constrains {m} (maxfg m)";
+\ : {m} co (maxfg m)";
by (simp_tac
(simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
by (Blast_tac 1);
@@ -53,7 +53,7 @@
(*This one is t := t+1 if t <max (ftime t) (gtime t) *)
Goal "mk_program (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }) \
-\ : constrains {m} (maxfg m)";
+\ : {m} co (maxfg m)";
by (simp_tac
(simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
by (blast_tac (claset() addIs [Suc_leI]) 1);
@@ -68,10 +68,10 @@
Addsimps [atMost_Int_atLeast];
-Goal "[| ALL m. F : Constrains {m} (maxfg m); \
-\ ALL m: lessThan n. F : LeadsTo {m} (greaterThan m); \
+Goal "[| ALL m. F : {m} Co (maxfg m); \
+\ ALL m: lessThan n. F : {m} LeadsTo (greaterThan m); \
\ n: common |] \
-\ ==> F : LeadsTo (atMost n) common";
+\ ==> F : (atMost n) LeadsTo common";
by (rtac LeadsTo_weaken_R 1);
by (res_inst_tac [("f","%x. x"), ("l", "n")] GreaterThan_bounded_induct 1);
by (ALLGOALS Asm_simp_tac);
@@ -81,10 +81,10 @@
val lemma = result();
(*The "ALL m: -common" form echoes CMT6.*)
-Goal "[| ALL m. F : Constrains {m} (maxfg m); \
-\ ALL m: -common. F : LeadsTo {m} (greaterThan m); \
+Goal "[| ALL m. F : {m} Co (maxfg m); \
+\ ALL m: -common. F : {m} LeadsTo (greaterThan m); \
\ n: common |] \
-\ ==> F : LeadsTo (atMost (LEAST n. n: common)) common";
+\ ==> F : (atMost (LEAST n. n: common)) LeadsTo common";
by (rtac lemma 1);
by (ALLGOALS Asm_simp_tac);
by (etac LeastI 2);
--- a/src/HOL/UNITY/Constrains.ML Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/Constrains.ML Thu Apr 29 10:51:58 1999 +0200
@@ -41,18 +41,17 @@
qed "invariant_includes_reachable";
-(*** Constrains ***)
+(*** Co ***)
-overload_1st_set "Constrains.Constrains";
+overload_1st_set "Constrains.op Co";
-(*F : constrains B B'
- ==> F : constrains (reachable F Int B) (reachable F Int B')*)
+(*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*)
bind_thm ("constrains_reachable_Int",
subset_refl RS
rewrite_rule [stable_def] stable_reachable RS
constrains_Int);
-Goalw [Constrains_def] "F : constrains A A' ==> F : Constrains A A'";
+Goalw [Constrains_def] "F : A co A' ==> F : A Co A'";
by (blast_tac (claset() addIs [constrains_reachable_Int]) 1);
qed "constrains_imp_Constrains";
@@ -62,46 +61,46 @@
val prems = Goal
"(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A') \
-\ ==> F : Constrains A A'";
+\ ==> F : A Co A'";
by (rtac constrains_imp_Constrains 1);
by (blast_tac (claset() addIs (constrainsI::prems)) 1);
qed "ConstrainsI";
-Goalw [Constrains_def, constrains_def] "F : Constrains {} B";
+Goalw [Constrains_def, constrains_def] "F : {} Co B";
by (Blast_tac 1);
qed "Constrains_empty";
-Goal "F : Constrains A UNIV";
+Goal "F : A Co UNIV";
by (blast_tac (claset() addIs [ConstrainsI]) 1);
qed "Constrains_UNIV";
AddIffs [Constrains_empty, Constrains_UNIV];
Goalw [Constrains_def]
- "[| F : Constrains A A'; A'<=B' |] ==> F : Constrains A B'";
+ "[| F : A Co A'; A'<=B' |] ==> F : A Co B'";
by (blast_tac (claset() addIs [constrains_weaken_R]) 1);
qed "Constrains_weaken_R";
Goalw [Constrains_def]
- "[| F : Constrains A A'; B<=A |] ==> F : Constrains B A'";
+ "[| F : A Co A'; B<=A |] ==> F : B Co A'";
by (blast_tac (claset() addIs [constrains_weaken_L]) 1);
qed "Constrains_weaken_L";
Goalw [Constrains_def]
- "[| F : Constrains A A'; B<=A; A'<=B' |] ==> F : Constrains B B'";
+ "[| F : A Co A'; B<=A; A'<=B' |] ==> F : B Co B'";
by (blast_tac (claset() addIs [constrains_weaken]) 1);
qed "Constrains_weaken";
(** Union **)
Goalw [Constrains_def]
- "[| F : Constrains A A'; F : Constrains B B' |] \
-\ ==> F : Constrains (A Un B) (A' Un B')";
+ "[| F : A Co A'; F : B Co B' |] \
+\ ==> F : (A Un B) Co (A' Un B')";
by (blast_tac (claset() addIs [constrains_Un RS constrains_weaken]) 1);
qed "Constrains_Un";
-Goal "ALL i:I. F : Constrains (A i) (A' i) \
-\ ==> F : Constrains (UN i:I. A i) (UN i:I. A' i)";
+Goal "ALL i:I. F : (A i) Co (A' i) \
+\ ==> F : (UN i:I. A i) Co (UN i:I. A' i)";
by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
by (dtac ball_constrains_UN 1);
by (blast_tac (claset() addIs [constrains_weaken]) 1);
@@ -110,20 +109,20 @@
(** Intersection **)
Goalw [Constrains_def]
- "[| F : Constrains A A'; F : Constrains B B' |] \
-\ ==> F : Constrains (A Int B) (A' Int B')";
+ "[| F : A Co A'; F : B Co B' |] \
+\ ==> F : (A Int B) Co (A' Int B')";
by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1);
qed "Constrains_Int";
-Goal "ALL i:I. F : Constrains (A i) (A' i) \
-\ ==> F : Constrains (INT i:I. A i) (INT i:I. A' i)";
+Goal "ALL i:I. F : (A i) Co (A' i) \
+\ ==> F : (INT i:I. A i) Co (INT i:I. A' i)";
by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
by (dtac ball_constrains_INT 1);
by (dtac constrains_reachable_Int 1);
by (blast_tac (claset() addIs [constrains_weaken]) 1);
qed "ball_Constrains_INT";
-Goal "F : Constrains A A' ==> reachable F Int A <= A'";
+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
@@ -131,14 +130,14 @@
qed "Constrains_imp_subset";
Goalw [Constrains_def]
- "[| F : Constrains A B; F : Constrains B C |] \
-\ ==> F : Constrains A C";
+ "[| F : A Co B; F : B Co C |] \
+\ ==> F : A Co C";
by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
qed "Constrains_trans";
Goalw [Constrains_def, constrains_def]
- "[| F : Constrains A (A' Un B); F : Constrains B B' |] \
-\ ==> F : Constrains A (A' Un B')";
+ "[| F : A Co (A' Un B); F : B Co B' |] \
+\ ==> F : A Co (A' Un B')";
by (Clarify_tac 1);
by (Blast_tac 1);
qed "Constrains_cancel";
@@ -150,11 +149,11 @@
by (simp_tac (simpset() addsimps [Stable_def, Constrains_def, stable_def]) 1);
qed "Stable_eq_stable";
-Goalw [Stable_def] "F : Constrains A A ==> F : Stable A";
+Goalw [Stable_def] "F : A Co A ==> F : Stable A";
by (assume_tac 1);
qed "StableI";
-Goalw [Stable_def] "F : Stable A ==> F : Constrains A A";
+Goalw [Stable_def] "F : Stable A ==> F : A Co A";
by (assume_tac 1);
qed "StableD";
@@ -169,14 +168,14 @@
qed "Stable_Int";
Goalw [Stable_def]
- "[| F : Stable C; F : Constrains A (C Un A') |] \
-\ ==> F : Constrains (C Un A) (C Un A')";
+ "[| F : Stable C; F : A Co (C Un A') |] \
+\ ==> F : (C Un A) Co (C Un A')";
by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken]) 1);
qed "Stable_Constrains_Un";
Goalw [Stable_def]
- "[| F : Stable C; F : Constrains (C Int A) A' |] \
-\ ==> F : Constrains (C Int A) (C Int A')";
+ "[| F : Stable C; F : (C Int A) Co A' |] \
+\ ==> F : (C Int A) Co (C Int A')";
by (blast_tac (claset() addIs [Constrains_Int RS Constrains_weaken]) 1);
qed "Stable_Constrains_Int";
@@ -222,15 +221,15 @@
in forward proof. ***)
Goalw [Constrains_def, constrains_def]
- "[| ALL m. F : Constrains {s. s x = m} (B m) |] \
-\ ==> F : Constrains {s. s x : M} (UN m:M. B m)";
+ "[| ALL m. F : {s. s x = m} Co (B m) |] \
+\ ==> F : {s. s x : M} Co (UN m:M. B m)";
by (Blast_tac 1);
qed "Elimination";
(*As above, but for the trivial case of a one-variable state, in which the
state is identified with its one variable.*)
Goalw [Constrains_def, constrains_def]
- "(ALL m. F : Constrains {m} (B m)) ==> F : Constrains M (UN m:M. B m)";
+ "(ALL m. F : {m} Co (B m)) ==> F : M Co (UN m:M. B m)";
by (Blast_tac 1);
qed "Elimination_sing";
@@ -286,21 +285,21 @@
qed "Invariant_eq_UN_invariant";
-(*** "Constrains" rules involving Invariant ***)
+(*** "Co" rules involving Invariant ***)
-Goal "[| F : Invariant INV; F : Constrains (INV Int A) A' |] \
-\ ==> F : Constrains A A'";
+Goal "[| F : Invariant INV; F : (INV Int A) Co A' |] \
+\ ==> F : A Co A'";
by (asm_full_simp_tac
(simpset() addsimps [Invariant_includes_reachable RS Int_absorb2,
Constrains_def, Int_assoc RS sym]) 1);
qed "Invariant_ConstrainsI";
-(* [| F : Invariant INV; F : Constrains (INV Int A) A |]
+(* [| F : Invariant INV; F : (INV Int A) Co A |]
==> F : Stable A *)
bind_thm ("Invariant_StableI", Invariant_ConstrainsI RS StableI);
-Goal "[| F : Invariant INV; F : Constrains A A' |] \
-\ ==> F : Constrains A (INV Int A')";
+Goal "[| F : Invariant INV; F : A Co A' |] \
+\ ==> F : A Co (INV Int A')";
by (asm_full_simp_tac
(simpset() addsimps [Invariant_includes_reachable RS Int_absorb2,
Constrains_def, Int_assoc RS sym]) 1);
@@ -334,7 +333,7 @@
(*To allow expansion of the program's definition when appropriate*)
val program_defs_ref = ref ([] : thm list);
-(*proves "constrains" properties when the program is specified*)
+(*proves "co" properties when the program is specified*)
fun constrains_tac i =
SELECT_GOAL
(EVERY [simp_tac (simpset() addsimps !program_defs_ref) 1,
--- a/src/HOL/UNITY/Constrains.thy Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/Constrains.thy Thu Apr 29 10:51:58 1999 +0200
@@ -31,17 +31,20 @@
Acts "[| act: Acts F; s : reachable F; (s,s'): act |]
==> s' : reachable F"
+consts
+ Co, Unless :: "['a set, 'a set] => 'a program set" (infixl 60)
+
+defs
+ Constrains_def
+ "A Co B == {F. F : (reachable F Int A) co (reachable F Int B)}"
+
+ Unless_def
+ "A Unless B == (A-B) Co (A Un B)"
+
constdefs
- Constrains :: "['a set, 'a set] => 'a program set"
- "Constrains A B == {F. F : constrains (reachable F Int A)
- (reachable F Int B)}"
-
Stable :: "'a set => 'a program set"
- "Stable A == Constrains A A"
-
- Unless :: "['a set, 'a set] => 'a program set"
- "Unless A B == Constrains (A-B) (A Un B)"
+ "Stable A == A Co A"
Invariant :: "'a set => 'a program set"
"Invariant A == {F. Init F <= A} Int Stable A"
--- a/src/HOL/UNITY/Deadlock.ML Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/Deadlock.ML Thu Apr 29 10:51:58 1999 +0200
@@ -9,7 +9,7 @@
(*Trivial, two-process case*)
Goalw [constrains_def, stable_def]
- "[| F : constrains (A Int B) A; F : constrains (B Int A) B |] \
+ "[| F : (A Int B) co A; F : (B Int A) co B |] \
\ ==> F : stable (A Int B)";
by (Blast_tac 1);
result();
@@ -69,9 +69,9 @@
(*The final deadlock example*)
val [zeroprem, allprem] = goalw thy [stable_def]
- "[| F : constrains (A 0 Int A (Suc n)) (A 0); \
-\ ALL i: atMost n. F : constrains (A(Suc i) Int A i) \
-\ (-A i Un A(Suc i)) |] \
+ "[| F : (A 0 Int A (Suc n)) co (A 0); \
+\ ALL i: atMost n. F : (A(Suc i) Int A i) co \
+\ (-A i Un A(Suc i)) |] \
\ ==> F : stable (INT i: atMost (Suc n). A i)";
by (rtac ([zeroprem, allprem RS ball_constrains_INT] MRS
--- a/src/HOL/UNITY/Extend.ML Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/Extend.ML Thu Apr 29 10:51:58 1999 +0200
@@ -172,10 +172,10 @@
Addsimps [extend_Join];
-(*** Safety: constrains, stable ***)
+(*** Safety: co, stable ***)
-Goal "(extend h F : constrains (extend_set h A) (extend_set h B)) = \
-\ (F : constrains A B)";
+Goal "(extend h F : (extend_set h A) co (extend_set h B)) = \
+\ (F : A co B)";
by (simp_tac (simpset() addsimps [constrains_def]) 1);
qed "extend_constrains";
@@ -187,7 +187,7 @@
by (asm_simp_tac (simpset() addsimps [invariant_def, extend_stable]) 1);
qed "extend_invariant";
-(** Substitution Axiom versions: Constrains, Stable **)
+(** Substitution Axiom versions: Co, Stable **)
Goal "p : reachable (extend h F) ==> f p : reachable F";
by (etac reachable.induct 1);
@@ -212,8 +212,8 @@
simpset())));
qed "reachable_extend_eq";
-Goal "(extend h F : Constrains (extend_set h A) (extend_set h B)) = \
-\ (F : Constrains A B)";
+Goal "(extend h F : (extend_set h A) Co (extend_set h B)) = \
+\ (F : A Co B)";
by (simp_tac
(simpset() addsimps [Constrains_def, reachable_extend_eq,
extend_constrains, extend_set_Int_distrib RS sym]) 1);
@@ -232,16 +232,16 @@
Domain_extend_act]));
qed "extend_transient";
-Goal "(extend h F : ensures (extend_set h A) (extend_set h B)) = \
-\ (F : ensures A B)";
+Goal "(extend h F : (extend_set h A) ensures (extend_set h B)) = \
+\ (F : A ensures B)";
by (simp_tac
(simpset() addsimps [ensures_def, extend_constrains, extend_transient,
extend_set_Un_distrib RS sym,
extend_set_Diff_distrib RS sym]) 1);
qed "extend_ensures";
-Goal "F : leadsTo A B \
-\ ==> extend h F : leadsTo (extend_set h A) (extend_set h B)";
+Goal "F : A leadsTo B \
+\ ==> extend h F : (extend_set h A) leadsTo (extend_set h B)";
by (etac leadsTo_induct 1);
by (asm_simp_tac (simpset() addsimps [leadsTo_UN, extend_set_Union]) 3);
by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
@@ -272,7 +272,7 @@
by (force_tac (claset(), simpset() addsimps [extend_act_def]) 1);
qed "extend_transient_slice";
-Goal "extend h F : ensures A B ==> F : ensures (slice A y) (f `` B)";
+Goal "extend h F : A ensures B ==> F : (slice A y) ensures (f `` B)";
by (full_simp_tac
(simpset() addsimps [ensures_def, extend_constrains, extend_transient,
image_Un RS sym,
@@ -292,14 +292,14 @@
simpset() addsimps [slice_def]) 1);
qed "extend_ensures_slice";
-Goal "ALL y. F : leadsTo (slice B y) CU ==> F : leadsTo (f `` B) CU";
+Goal "ALL y. F : (slice B y) leadsTo CU ==> F : (f `` B) leadsTo CU";
by (simp_tac (simpset() addsimps [image_is_UN_slice]) 1);
by (blast_tac (claset() addIs [leadsTo_UN]) 1);
qed "leadsTo_slice_image";
-Goal "extend h F : leadsTo AU BU \
-\ ==> ALL y. F : leadsTo (slice AU y) (f `` BU)";
+Goal "extend h F : AU leadsTo BU \
+\ ==> ALL y. F : (slice AU y) leadsTo (f `` BU)";
by (etac leadsTo_induct 1);
by (full_simp_tac (simpset() addsimps [slice_Union]) 3);
by (blast_tac (claset() addIs [leadsTo_UN]) 3);
@@ -307,16 +307,16 @@
by (blast_tac (claset() addIs [extend_ensures_slice, leadsTo_Basis]) 1);
qed_spec_mp "extend_leadsTo_slice";
-Goal "(extend h F : leadsTo (extend_set h A) (extend_set h B)) = \
-\ (F : leadsTo A B)";
+Goal "(extend h F : (extend_set h A) leadsTo (extend_set h B)) = \
+\ (F : A leadsTo B)";
by Safe_tac;
by (etac leadsTo_imp_extend_leadsTo 2);
by (dtac extend_leadsTo_slice 1);
by (full_simp_tac (simpset() addsimps [slice_extend_set]) 1);
qed "extend_leadsto_eq";
-Goal "(extend h F : LeadsTo (extend_set h A) (extend_set h B)) = \
-\ (F : LeadsTo A B)";
+Goal "(extend h F : (extend_set h A) LeadsTo (extend_set h B)) = \
+\ (F : A LeadsTo B)";
by (simp_tac
(simpset() addsimps [LeadsTo_def, reachable_extend_eq,
extend_leadsto_eq, extend_set_Int_distrib RS sym]) 1);
--- a/src/HOL/UNITY/Handshake.ML Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/Handshake.ML Thu Apr 29 10:51:58 1999 +0200
@@ -31,7 +31,7 @@
by (constrains_tac 1);
qed "invFG";
-Goal "(F Join G) : LeadsTo ({s. NF s = k} - {s. BB s}) \
+Goal "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo \
\ ({s. NF s = k} Int {s. BB s})";
by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
by (ensures_tac "cmdG" 2);
@@ -39,7 +39,7 @@
by Auto_tac;
qed "lemma2_1";
-Goal "(F Join G) : LeadsTo ({s. NF s = k} Int {s. BB s}) {s. k < NF s}";
+Goal "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo {s. k < NF s}";
by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
by (constrains_tac 2);
by (ensures_tac "cmdF" 1);
@@ -47,12 +47,12 @@
qed "lemma2_2";
-Goal "(F Join G) : LeadsTo UNIV {s. m < NF s}";
+Goal "(F Join G) : UNIV LeadsTo {s. m < NF s}";
by (rtac LeadsTo_weaken_R 1);
by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")]
GreaterThan_bounded_induct 1);
by (auto_tac (claset(), simpset() addsimps [vimage_def]));
-(*The inductive step: (F Join G) : LeadsTo {x. NF x = ma} {x. ma < NF x}*)
+(*The inductive step: (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
by (rtac LeadsTo_Diff 1);
by (rtac lemma2_2 2);
by (rtac LeadsTo_Trans 1);
--- a/src/HOL/UNITY/Lift.ML Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/Lift.ML Thu Apr 29 10:51:58 1999 +0200
@@ -55,7 +55,7 @@
val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un;
-(* [| Lprg : LeadsTo B C; Lprg : LeadsTo A B |] ==> Lprg : LeadsTo (A Un B) C *)
+(* [| Lprg : B LeadsTo C; Lprg : A LeadsTo B |] ==> Lprg : (A Un B) LeadsTo C *)
(*Simplification for records*)
@@ -126,24 +126,24 @@
(** Lift_1 **)
-Goal "Lprg : LeadsTo (stopped Int atFloor n) (opened Int atFloor n)";
+Goal "Lprg : (stopped Int atFloor n) LeadsTo (opened Int atFloor n)";
by (cut_facts_tac [stop_floor] 1);
by (ensures_tac "open_act" 1);
qed "E_thm01"; (*lem_lift_1_5*)
-Goal "Lprg : LeadsTo (Req n Int stopped - atFloor n) \
+Goal "Lprg : (Req n Int stopped - atFloor n) LeadsTo \
\ (Req n Int opened - atFloor n)";
by (cut_facts_tac [stop_floor] 1);
by (ensures_tac "open_act" 1);
qed "E_thm02"; (*lem_lift_1_1*)
-Goal "Lprg : LeadsTo (Req n Int opened - atFloor n) \
+Goal "Lprg : (Req n Int opened - atFloor n) LeadsTo \
\ (Req n Int closed - (atFloor n - queueing))";
by (ensures_tac "close_act" 1);
qed "E_thm03"; (*lem_lift_1_2*)
-Goal "Lprg : LeadsTo (Req n Int closed Int (atFloor n - queueing)) \
-\ (opened Int atFloor n)";
+Goal "Lprg : (Req n Int closed Int (atFloor n - queueing)) \
+\ LeadsTo (opened Int atFloor n)";
by (ensures_tac "open_act" 1);
qed "E_thm04"; (*lem_lift_1_7*)
@@ -166,16 +166,16 @@
(*lem_lift_2_0
NOT an ensures property, but a mere inclusion;
don't know why script lift_2.uni says ENSURES*)
-Goal "Lprg : LeadsTo (Req n Int closed - (atFloor n - queueing)) \
-\ ((closed Int goingup Int Req n) Un \
+Goal "Lprg : (Req n Int closed - (atFloor n - queueing)) \
+\ LeadsTo ((closed Int goingup Int Req n) Un \
\ (closed Int goingdown Int Req n))";
by (rtac subset_imp_LeadsTo 1);
by (auto_tac (claset() addSEs [int_neqE], simpset()));
qed "E_thm05c";
(*lift_2*)
-Goal "Lprg : LeadsTo (Req n Int closed - (atFloor n - queueing)) \
-\ (moving Int Req n)";
+Goal "Lprg : (Req n Int closed - (atFloor n - queueing)) \
+\ LeadsTo (moving Int Req n)";
by (rtac ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1);
by (ensures_tac "req_down" 2);
by (ensures_tac "req_up" 1);
@@ -188,9 +188,9 @@
(*lem_lift_4_1 *)
Goal "#0 < N ==> \
-\ Lprg : LeadsTo \
-\ (moving Int Req n Int {s. metric n s = N} Int \
-\ {s. floor s ~: req s} Int {s. up s}) \
+\ Lprg : (moving Int Req n Int {s. metric n s = N} Int \
+\ {s. floor s ~: req s} Int {s. up s}) \
+\ LeadsTo \
\ (moving Int Req n Int {s. metric n s < N})";
by (cut_facts_tac [moving_up] 1);
by (ensures_tac "move_up" 1);
@@ -208,10 +208,9 @@
(*lem_lift_4_3 *)
Goal "#0 < N ==> \
-\ Lprg : LeadsTo \
-\ (moving Int Req n Int {s. metric n s = N} Int \
-\ {s. floor s ~: req s} - {s. up s}) \
-\ (moving Int Req n Int {s. metric n s < N})";
+\ Lprg : (moving Int Req n Int {s. metric n s = N} Int \
+\ {s. floor s ~: req s} - {s. up s}) \
+\ LeadsTo (moving Int Req n Int {s. metric n s < N})";
by (cut_facts_tac [moving_down] 1);
by (ensures_tac "move_down" 1);
by Safe_tac;
@@ -224,8 +223,8 @@
qed "E_thm12b";
(*lift_4*)
-Goal "#0<N ==> Lprg : LeadsTo (moving Int Req n Int {s. metric n s = N} Int \
-\ {s. floor s ~: req s}) \
+Goal "#0<N ==> Lprg : (moving Int Req n Int {s. metric n s = N} Int \
+\ {s. floor s ~: req s}) LeadsTo \
\ (moving Int Req n Int {s. metric n s < N})";
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
by (etac E_thm12b 3);
@@ -238,7 +237,7 @@
(*lem_lift_5_3*)
Goal "#0<N \
-\ ==> Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N} Int goingup) \
+\ ==> Lprg : (closed Int Req n Int {s. metric n s = N} Int goingup) LeadsTo \
\ (moving Int Req n Int {s. metric n s < N})";
by (cut_facts_tac [bounded] 1);
by (ensures_tac "req_up" 1);
@@ -250,7 +249,7 @@
(*lem_lift_5_1 has ~goingup instead of goingdown*)
Goal "#0<N ==> \
-\ Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N} Int goingdown) \
+\ Lprg : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo \
\ (moving Int Req n Int {s. metric n s < N})";
by (cut_facts_tac [bounded] 1);
by (ensures_tac "req_down" 1);
@@ -272,7 +271,7 @@
(*lift_5*)
-Goal "#0<N ==> Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N}) \
+Goal "#0<N ==> Lprg : (closed Int Req n Int {s. metric n s = N}) LeadsTo \
\ (moving Int Req n Int {s. metric n s < N})";
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
by (etac E_thm16b 3);
@@ -295,7 +294,7 @@
(*lem_lift_3_1*)
-Goal "Lprg : LeadsTo (moving Int Req n Int {s. metric n s = #0}) \
+Goal "Lprg : (moving Int Req n Int {s. metric n s = #0}) LeadsTo \
\ (stopped Int atFloor n)";
by (cut_facts_tac [bounded] 1);
by (ensures_tac "request_act" 1);
@@ -303,27 +302,26 @@
qed "E_thm11";
(*lem_lift_3_5*)
-Goal "Lprg : LeadsTo \
-\ (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
-\ (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})";
+Goal
+ "Lprg : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
+\ LeadsTo (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})";
by (ensures_tac "request_act" 1);
by (auto_tac (claset(), simpset() addsimps metric_simps));
qed "E_thm13";
(*lem_lift_3_6*)
Goal "#0 < N ==> \
-\ Lprg : LeadsTo \
+\ Lprg : \
\ (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
-\ (opened Int Req n Int {s. metric n s = N})";
+\ LeadsTo (opened Int Req n Int {s. metric n s = N})";
by (ensures_tac "open_act" 1);
by (REPEAT_FIRST (eresolve_tac mov_metrics));
by (auto_tac (claset(), simpset() addsimps metric_simps));
qed "E_thm14";
(*lem_lift_3_7*)
-Goal "Lprg : LeadsTo \
-\ (opened Int Req n Int {s. metric n s = N}) \
-\ (closed Int Req n Int {s. metric n s = N})";
+Goal "Lprg : (opened Int Req n Int {s. metric n s = N}) \
+\ LeadsTo (closed Int Req n Int {s. metric n s = N})";
by (ensures_tac "close_act" 1);
by (auto_tac (claset(), simpset() addsimps metric_simps));
qed "E_thm15";
@@ -332,9 +330,9 @@
(** the final steps **)
Goal "#0 < N ==> \
-\ Lprg : LeadsTo \
+\ Lprg : \
\ (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
-\ (moving Int Req n Int {s. metric n s < N})";
+\ LeadsTo (moving Int Req n Int {s. metric n s < N})";
by (blast_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5]
addIs [LeadsTo_Trans]) 1);
qed "lift_3_Req";
@@ -353,7 +351,7 @@
val R_thm11 = [reach_nonneg, E_thm11] MRS reachable_LeadsTo_weaken;
-Goal "Lprg : LeadsTo (moving Int Req n) (stopped Int atFloor n)";
+Goal "Lprg : (moving Int Req n) LeadsTo (stopped Int atFloor n)";
by (rtac (reach_nonneg RS integ_0_le_induct) 1);
by (case_tac "#0 < z" 1);
(*If z <= #0 then actually z = #0*)
@@ -367,7 +365,7 @@
qed "lift_3";
-Goal "Lprg : LeadsTo (Req n) (opened Int atFloor n)";
+Goal "Lprg : (Req n) LeadsTo (opened Int atFloor n)";
by (rtac LeadsTo_Trans 1);
by (rtac (E_thm04 RS LeadsTo_Un) 2);
by (rtac LeadsTo_Un_post 2);
--- a/src/HOL/UNITY/Mutex.ML Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/Mutex.ML Thu Apr 29 10:51:58 1999 +0200
@@ -74,44 +74,44 @@
(*** Progress for U ***)
-Goalw [Unless_def] "Mprg : Unless {s. MM s=#2} {s. MM s=#3}";
+Goalw [Unless_def] "Mprg : {s. MM s=#2} Unless {s. MM s=#3}";
by (constrains_tac 1);
qed "U_F0";
-Goal "Mprg : LeadsTo {s. MM s=#1} {s. PP s = VV s & MM s = #2}";
+Goal "Mprg : {s. MM s=#1} LeadsTo {s. PP s = VV s & MM s = #2}";
by (ensures_tac "cmd1U" 1);
qed "U_F1";
-Goal "Mprg : LeadsTo {s. ~ PP s & MM s = #2} {s. MM s = #3}";
+Goal "Mprg : {s. ~ PP s & MM s = #2} LeadsTo {s. MM s = #3}";
by (cut_facts_tac [invariantU] 1);
by (ensures_tac "cmd2U" 1);
qed "U_F2";
-Goal "Mprg : LeadsTo {s. MM s = #3} {s. PP s}";
+Goal "Mprg : {s. MM s = #3} LeadsTo {s. PP s}";
by (res_inst_tac [("B", "{s. MM s = #4}")] LeadsTo_Trans 1);
by (ensures_tac "cmd4U" 2);
by (ensures_tac "cmd3U" 1);
qed "U_F3";
-Goal "Mprg : LeadsTo {s. MM s = #2} {s. PP s}";
+Goal "Mprg : {s. MM s = #2} LeadsTo {s. PP s}";
by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo]
MRS LeadsTo_Diff) 1);
by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
by (auto_tac (claset() addSEs [less_SucE], simpset()));
val U_lemma2 = result();
-Goal "Mprg : LeadsTo {s. MM s = #1} {s. PP s}";
+Goal "Mprg : {s. MM s = #1} LeadsTo {s. PP s}";
by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1);
by (Blast_tac 1);
val U_lemma1 = result();
-Goal "Mprg : LeadsTo {s. #1 <= MM s & MM s <= #3} {s. PP s}";
+Goal "Mprg : {s. #1 <= MM s & MM s <= #3} LeadsTo {s. PP s}";
by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
U_lemma1, U_lemma2, U_F3] ) 1);
val U_lemma123 = result();
(*Misra's F4*)
-Goal "Mprg : LeadsTo {s. UU s} {s. PP s}";
+Goal "Mprg : {s. UU s} LeadsTo {s. PP s}";
by (rtac ([invariantU, U_lemma123] MRS Invariant_LeadsTo_weaken) 1);
by Auto_tac;
qed "u_Leadsto_p";
@@ -120,45 +120,45 @@
(*** Progress for V ***)
-Goalw [Unless_def] "Mprg : Unless {s. NN s=#2} {s. NN s=#3}";
+Goalw [Unless_def] "Mprg : {s. NN s=#2} Unless {s. NN s=#3}";
by (constrains_tac 1);
qed "V_F0";
-Goal "Mprg : LeadsTo {s. NN s=#1} {s. PP s = (~ UU s) & NN s = #2}";
+Goal "Mprg : {s. NN s=#1} LeadsTo {s. PP s = (~ UU s) & NN s = #2}";
by (ensures_tac "cmd1V" 1);
qed "V_F1";
-Goal "Mprg : LeadsTo {s. PP s & NN s = #2} {s. NN s = #3}";
+Goal "Mprg : {s. PP s & NN s = #2} LeadsTo {s. NN s = #3}";
by (cut_facts_tac [invariantV] 1);
by (ensures_tac "cmd2V" 1);
qed "V_F2";
-Goal "Mprg : LeadsTo {s. NN s = #3} {s. ~ PP s}";
+Goal "Mprg : {s. NN s = #3} LeadsTo {s. ~ PP s}";
by (res_inst_tac [("B", "{s. NN s = #4}")] LeadsTo_Trans 1);
by (ensures_tac "cmd4V" 2);
by (ensures_tac "cmd3V" 1);
qed "V_F3";
-Goal "Mprg : LeadsTo {s. NN s = #2} {s. ~ PP s}";
+Goal "Mprg : {s. NN s = #2} LeadsTo {s. ~ PP s}";
by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo]
MRS LeadsTo_Diff) 1);
by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
by (auto_tac (claset() addSEs [less_SucE], simpset()));
val V_lemma2 = result();
-Goal "Mprg : LeadsTo {s. NN s = #1} {s. ~ PP s}";
+Goal "Mprg : {s. NN s = #1} LeadsTo {s. ~ PP s}";
by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1);
by (Blast_tac 1);
val V_lemma1 = result();
-Goal "Mprg : LeadsTo {s. #1 <= NN s & NN s <= #3} {s. ~ PP s}";
+Goal "Mprg : {s. #1 <= NN s & NN s <= #3} LeadsTo {s. ~ PP s}";
by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
V_lemma1, V_lemma2, V_F3] ) 1);
val V_lemma123 = result();
(*Misra's F4*)
-Goal "Mprg : LeadsTo {s. VV s} {s. ~ PP s}";
+Goal "Mprg : {s. VV s} LeadsTo {s. ~ PP s}";
by (rtac ([invariantV, V_lemma123] MRS Invariant_LeadsTo_weaken) 1);
by Auto_tac;
qed "v_Leadsto_not_p";
@@ -167,7 +167,7 @@
(** Absence of starvation **)
(*Misra's F6*)
-Goal "Mprg : LeadsTo {s. MM s = #1} {s. MM s = #3}";
+Goal "Mprg : {s. MM s = #1} LeadsTo {s. MM s = #3}";
by (rtac LeadsTo_Un_duplicate 1);
by (rtac LeadsTo_cancel2 1);
by (rtac U_F2 2);
@@ -181,7 +181,7 @@
(*The same for V*)
-Goal "Mprg : LeadsTo {s. NN s = #1} {s. NN s = #3}";
+Goal "Mprg : {s. NN s = #1} LeadsTo {s. NN s = #3}";
by (rtac LeadsTo_Un_duplicate 1);
by (rtac LeadsTo_cancel2 1);
by (rtac V_F2 2);
--- a/src/HOL/UNITY/Network.ML Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/Network.ML Thu Apr 29 10:51:58 1999 +0200
@@ -14,9 +14,9 @@
\ !! m. F : stable {s. s(Aproc,Rcvd) <= s(Bproc,Sent)}; \
\ !! m proc. F : stable {s. m <= s(proc,Sent)}; \
\ !! n proc. F : stable {s. n <= s(proc,Rcvd)}; \
-\ !! m proc. F : constrains {s. s(proc,Idle) = 1 & s(proc,Rcvd) = m} \
+\ !! m proc. F : {s. s(proc,Idle) = 1 & s(proc,Rcvd) = m} co \
\ {s. s(proc,Rcvd) = m --> s(proc,Idle) = 1}; \
-\ !! n proc. F : constrains {s. s(proc,Idle) = 1 & s(proc,Sent) = n} \
+\ !! n proc. F : {s. s(proc,Idle) = 1 & s(proc,Sent) = n} co \
\ {s. s(proc,Sent) = n} \
\ |] ==> F : stable {s. s(Aproc,Idle) = 1 & s(Bproc,Idle) = 1 & \
\ s(Aproc,Sent) = s(Bproc,Rcvd) & \
--- a/src/HOL/UNITY/PPROD.ML Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/PPROD.ML Thu Apr 29 10:51:58 1999 +0200
@@ -68,12 +68,12 @@
qed "component_PPROD";
-(*** Safety: constrains, stable, invariant ***)
+(*** Safety: co, stable, invariant ***)
(** 1st formulation of lifting **)
-Goal "(lift_prog i F : constrains (lift_set i A) (lift_set i B)) = \
-\ (F : constrains A B)";
+Goal "(lift_prog i F : (lift_set i A) co (lift_set i B)) = \
+\ (F : A co B)";
by (auto_tac (claset(),
simpset() addsimps [constrains_def, Acts_lift_prog]));
by (Blast_tac 2);
@@ -85,16 +85,16 @@
qed "lift_prog_stable_eq";
(*This one looks strange! Proof probably is by case analysis on i=j.*)
-Goal "F i : constrains A B \
-\ ==> lift_prog j (F j) : constrains (lift_set i A) (lift_set i B)";
+Goal "F i : A co B \
+\ ==> lift_prog j (F j) : (lift_set i A) co (lift_set i B)";
by (auto_tac (claset(),
simpset() addsimps [constrains_def, Acts_lift_prog]));
by (REPEAT (Blast_tac 1));
qed "constrains_imp_lift_prog_constrains";
Goal "i : I ==> \
-\ (PPROD I F : constrains (lift_set i A) (lift_set i B)) = \
-\ (F i : constrains A B)";
+\ (PPROD I F : (lift_set i A) co (lift_set i B)) = \
+\ (F i : A co B)";
by (asm_simp_tac (simpset() addsimps [PPROD_def, constrains_JN]) 1);
by (blast_tac (claset() addIs [lift_prog_constrains_eq RS iffD1,
constrains_imp_lift_prog_constrains]) 1);
@@ -107,8 +107,8 @@
(** 2nd formulation of lifting **)
-Goal "[| lift_prog i F : constrains AA BB |] \
-\ ==> F : constrains (Applyall AA i) (Applyall BB i)";
+Goal "[| lift_prog i F : AA co BB |] \
+\ ==> F : (Applyall AA i) co (Applyall BB i)";
by (auto_tac (claset(),
simpset() addsimps [Applyall_def, constrains_def,
Acts_lift_prog]));
@@ -116,8 +116,8 @@
simpset()) 1);
qed "lift_prog_constrains_projection";
-Goal "[| PPROD I F : constrains AA BB; i: I |] \
-\ ==> F i : constrains (Applyall AA i) (Applyall BB i)";
+Goal "[| PPROD I F : AA co BB; i: I |] \
+\ ==> F i : (Applyall AA i) co (Applyall BB i)";
by (rtac lift_prog_constrains_projection 1);
(*rotate this assumption to be last*)
by (dres_inst_tac [("psi", "PPROD I F : ?C")] asm_rl 1);
@@ -163,7 +163,7 @@
qed "PFUN_invariant";
-(*** Substitution Axiom versions: Constrains, Stable ***)
+(*** Substitution Axiom versions: Co, Stable ***)
(** Reachability **)
@@ -225,10 +225,10 @@
qed "reachable_PPROD_eq";
-(** Constrains **)
+(** Co **)
-Goal "[| F i : Constrains A B; i: I; finite I |] \
-\ ==> PPROD I F : Constrains (lift_set i A) (lift_set i B)";
+Goal "[| F i : A Co B; i: I; finite I |] \
+\ ==> PPROD I F : (lift_set i A) Co (lift_set i B)";
by (auto_tac
(claset(),
simpset() addsimps [Constrains_def, Collect_conj_eq RS sym,
@@ -245,11 +245,11 @@
simpset() addsimps [Applyall_def, lift_set_def]) 1);
qed "Applyall_Int_depend";
-(*Again, we need the f0 premise because otherwise Constrains holds trivially
+(*Again, we need the f0 premise because otherwise holds Co trivially
for PPROD I F.*)
-Goal "[| PPROD I F : Constrains (lift_set i A) (lift_set i B); \
+Goal "[| PPROD I F : (lift_set i A) Co (lift_set i B); \
\ i: I; finite I; f0: Init (PPROD I F) |] \
-\ ==> F i : Constrains A B";
+\ ==> F i : A Co B";
by (full_simp_tac (simpset() addsimps [Constrains_def]) 1);
by (subgoal_tac "ALL i:I. f0 i : reachable (F i)" 1);
by (blast_tac (claset() addIs [reachable.Init]) 2);
@@ -261,8 +261,8 @@
Goal "[| i: I; finite I; f0: Init (PPROD I F) |] \
-\ ==> (PPROD I F : Constrains (lift_set i A) (lift_set i B)) = \
-\ (F i : Constrains A B)";
+\ ==> (PPROD I F : (lift_set i A) Co (lift_set i B)) = \
+\ (F i : A Co B)";
by (blast_tac (claset() addIs [Constrains_imp_PPROD_Constrains,
PPROD_Constrains_imp_Constrains]) 1);
qed "PPROD_Constrains";
@@ -281,9 +281,9 @@
by (force_tac (claset(), simpset() addsimps [Applyall_def]) 1);
qed "Applyall_Int";
-Goal "[| (PPI x:I. F) : Constrains (lift_set i A) (lift_set i B); \
+Goal "[| (PPI x:I. F) : (lift_set i A) Co (lift_set i B); \
\ i: I; finite I |] \
-\ ==> F : Constrains A B";
+\ ==> F : A Co B";
by (full_simp_tac (simpset() addsimps [Constrains_def]) 1);
by (dtac PPROD_constrains_projection 1);
by (assume_tac 1);
@@ -293,8 +293,8 @@
qed "PFUN_Constrains_imp_Constrains";
Goal "[| i: I; finite I |] \
-\ ==> ((PPI x:I. F) : Constrains (lift_set i A) (lift_set i B)) = \
-\ (F : Constrains A B)";
+\ ==> ((PPI x:I. F) : (lift_set i A) Co (lift_set i B)) = \
+\ (F : A Co B)";
by (blast_tac (claset() addIs [Constrains_imp_PPROD_Constrains,
PFUN_Constrains_imp_Constrains]) 1);
qed "PFUN_Constrains";
--- a/src/HOL/UNITY/ROOT.ML Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/ROOT.ML Thu Apr 29 10:51:58 1999 +0200
@@ -13,7 +13,6 @@
add_path "../Lex"; (*to find Prefix.thy*)
time_use_thy"UNITY";
-
time_use_thy "Deadlock";
time_use_thy "WFair";
time_use_thy "Common";
--- a/src/HOL/UNITY/Reach.ML Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/Reach.ML Thu Apr 29 10:51:58 1999 +0200
@@ -109,7 +109,7 @@
simpset() addsimps [fun_upd_idem]));
qed "metric_le";
-Goal "Rprg : LeadsTo ((metric-``{m}) - fixedpoint) (metric-``(lessThan m))";
+Goal "Rprg : ((metric-``{m}) - fixedpoint) LeadsTo (metric-``(lessThan m))";
by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1);
by (rtac LeadsTo_UN 1);
by Auto_tac;
@@ -121,7 +121,7 @@
simpset()));
qed "LeadsTo_Diff_fixedpoint";
-Goal "Rprg : LeadsTo (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)";
+Goal "Rprg : (metric-``{m}) LeadsTo (metric-``(lessThan m) Un fixedpoint)";
by (rtac ([LeadsTo_Diff_fixedpoint RS LeadsTo_weaken_R,
subset_imp_LeadsTo] MRS LeadsTo_Diff) 1);
by Auto_tac;
@@ -129,13 +129,13 @@
(*Execution in any state leads to a fixedpoint (i.e. can terminate)*)
-Goal "Rprg : LeadsTo UNIV fixedpoint";
+Goal "Rprg : UNIV LeadsTo fixedpoint";
by (rtac LessThan_induct 1);
by Auto_tac;
by (rtac LeadsTo_Un_fixedpoint 1);
qed "LeadsTo_fixedpoint";
-Goal "Rprg : LeadsTo UNIV { %v. (init, v) : edges^* }";
+Goal "Rprg : UNIV LeadsTo { %v. (init, v) : edges^* }";
by (stac (fixedpoint_invariant_correct RS sym) 1);
by (rtac ([reach_invariant, LeadsTo_fixedpoint]
MRS Invariant_LeadsTo_weaken) 1);
--- a/src/HOL/UNITY/SubstAx.ML Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/SubstAx.ML Thu Apr 29 10:51:58 1999 +0200
@@ -6,21 +6,21 @@
LeadsTo relation, restricted to the set of reachable states.
*)
-overload_1st_set "SubstAx.LeadsTo";
+overload_1st_set "SubstAx.op LeadsTo";
(*** Specialized laws for handling invariants ***)
(** Conjoining a safety property **)
-Goal "[| reachable F <= C; F : LeadsTo (C Int A) A' |] \
-\ ==> F : LeadsTo A A'";
+Goal "[| reachable F <= C; F : (C Int A) LeadsTo A' |] \
+\ ==> F : A LeadsTo A'";
by (asm_full_simp_tac
(simpset() addsimps [LeadsTo_def, Int_absorb2, Int_assoc RS sym]) 1);
qed "reachable_LeadsToI";
-Goal "[| reachable F <= C; F : LeadsTo A A' |] \
-\ ==> F : LeadsTo A (C Int A')";
+Goal "[| reachable F <= C; F : A LeadsTo A' |] \
+\ ==> F : A LeadsTo (C Int A')";
by (asm_full_simp_tac
(simpset() addsimps [LeadsTo_def, Int_absorb2,
Int_assoc RS sym]) 1);
@@ -29,11 +29,11 @@
(** Conjoining an invariant **)
-(* [| Invariant F C; F : LeadsTo (C Int A) A' |] ==> F : LeadsTo A A' *)
+(* [| Invariant F C; F : (C Int A) LeadsTo A' |] ==> F : A LeadsTo A' *)
bind_thm ("Invariant_LeadsToI",
Invariant_includes_reachable RS reachable_LeadsToI);
-(* [| Invariant F C; F : LeadsTo A A' |] ==> F : LeadsTo A (C Int A') *)
+(* [| Invariant F C; F : A LeadsTo A' |] ==> F : A LeadsTo (C Int A') *)
bind_thm ("Invariant_LeadsToD",
Invariant_includes_reachable RS reachable_LeadsToD);
@@ -42,18 +42,18 @@
(*** Introduction rules: Basis, Trans, Union ***)
-Goal "F : leadsTo A B ==> F : LeadsTo A B";
+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);
qed "leadsTo_imp_LeadsTo";
-Goal "[| F : LeadsTo A B; F : LeadsTo B C |] ==> F : LeadsTo A C";
+Goal "[| F : A LeadsTo B; F : B LeadsTo C |] ==> F : A LeadsTo C";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
qed "LeadsTo_Trans";
val prems = Goalw [LeadsTo_def]
- "(!!A. A : S ==> F : LeadsTo A B) ==> F : LeadsTo (Union S) B";
+ "(!!A. A : S ==> F : A LeadsTo B) ==> F : (Union S) LeadsTo B";
by (Simp_tac 1);
by (stac Int_Union 1);
by (blast_tac (claset() addIs [leadsTo_UN] addDs prems) 1);
@@ -62,34 +62,34 @@
(*** Derived rules ***)
-Goal "F : LeadsTo A UNIV";
+Goal "F : A LeadsTo UNIV";
by (asm_simp_tac
(simpset() addsimps [LeadsTo_def, Int_lower1 RS subset_imp_leadsTo]) 1);
qed "LeadsTo_UNIV";
Addsimps [LeadsTo_UNIV];
(*Useful with cancellation, disjunction*)
-Goal "F : LeadsTo A (A' Un A') ==> F : LeadsTo A A'";
+Goal "F : A LeadsTo (A' Un A') ==> F : A LeadsTo A'";
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
qed "LeadsTo_Un_duplicate";
-Goal "F : LeadsTo A (A' Un C Un C) ==> F : LeadsTo A (A' Un C)";
+Goal "F : A LeadsTo (A' Un C Un C) ==> F : A LeadsTo (A' Un C)";
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
qed "LeadsTo_Un_duplicate2";
val prems =
-Goal "(!!i. i : I ==> F : LeadsTo (A i) B) ==> F : LeadsTo (UN i:I. A i) B";
+Goal "(!!i. i : I ==> F : (A i) LeadsTo B) ==> F : (UN i:I. A i) LeadsTo B";
by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1);
by (blast_tac (claset() addIs (LeadsTo_Union::prems)) 1);
qed "LeadsTo_UN";
(*Binary union introduction rule*)
-Goal "[| F : LeadsTo A C; F : LeadsTo B C |] ==> F : LeadsTo (A Un B) C";
+Goal "[| F : A LeadsTo C; F : B LeadsTo C |] ==> F : (A Un B) LeadsTo C";
by (stac Un_eq_Union 1);
by (blast_tac (claset() addIs [LeadsTo_Union]) 1);
qed "LeadsTo_Un";
-Goal "A <= B ==> F : LeadsTo A B";
+Goal "A <= B ==> F : A LeadsTo B";
by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
qed "subset_imp_LeadsTo";
@@ -97,39 +97,39 @@
bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo);
Addsimps [empty_LeadsTo];
-Goal "[| F : LeadsTo A A'; A' <= B' |] ==> F : LeadsTo A B'";
+Goal "[| F : A LeadsTo A'; A' <= B' |] ==> F : A LeadsTo B'";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1);
qed_spec_mp "LeadsTo_weaken_R";
-Goal "[| F : LeadsTo A A'; B <= A |] \
-\ ==> F : LeadsTo B A'";
+Goal "[| F : A LeadsTo A'; B <= A |] \
+\ ==> F : B LeadsTo A'";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
qed_spec_mp "LeadsTo_weaken_L";
-Goal "[| F : LeadsTo A A'; \
+Goal "[| F : A LeadsTo A'; \
\ B <= A; A' <= B' |] \
-\ ==> F : LeadsTo B B'";
+\ ==> F : B LeadsTo B'";
by (blast_tac (claset() addIs [LeadsTo_weaken_R, LeadsTo_weaken_L,
LeadsTo_Trans]) 1);
qed "LeadsTo_weaken";
-Goal "[| reachable F <= C; F : LeadsTo A A'; \
+Goal "[| reachable F <= C; F : A LeadsTo A'; \
\ C Int B <= A; C Int A' <= B' |] \
-\ ==> F : LeadsTo B B'";
+\ ==> F : B LeadsTo B'";
by (blast_tac (claset() addDs [reachable_LeadsToI] addIs[LeadsTo_weaken]
addIs [reachable_LeadsToD]) 1);
qed "reachable_LeadsTo_weaken";
(** Two theorems for "proof lattices" **)
-Goal "[| F : LeadsTo A B |] ==> F : LeadsTo (A Un B) B";
+Goal "[| F : A LeadsTo B |] ==> F : (A Un B) LeadsTo B";
by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo]) 1);
qed "LeadsTo_Un_post";
-Goal "[| F : LeadsTo A B; F : LeadsTo B C |] \
-\ ==> F : LeadsTo (A Un B) C";
+Goal "[| F : A LeadsTo B; F : B LeadsTo C |] \
+\ ==> F : (A Un B) LeadsTo C";
by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo,
LeadsTo_weaken_L, LeadsTo_Trans]) 1);
qed "LeadsTo_Trans_Un";
@@ -137,23 +137,23 @@
(** Distributive laws **)
-Goal "(F : LeadsTo (A Un B) C) = (F : LeadsTo A C & F : LeadsTo B C)";
+Goal "(F : (A Un B) LeadsTo C) = (F : A LeadsTo C & F : B LeadsTo C)";
by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
qed "LeadsTo_Un_distrib";
-Goal "(F : LeadsTo (UN i:I. A i) B) = (ALL i : I. F : LeadsTo (A i) B)";
+Goal "(F : (UN i:I. A i) LeadsTo B) = (ALL i : I. F : (A i) LeadsTo B)";
by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
qed "LeadsTo_UN_distrib";
-Goal "(F : LeadsTo (Union S) B) = (ALL A : S. F : LeadsTo A B)";
+Goal "(F : (Union S) LeadsTo B) = (ALL A : S. F : A LeadsTo B)";
by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1);
qed "LeadsTo_Union_distrib";
(** More rules using the premise "Invariant F" **)
-Goal "[| F : Constrains (A-A') (A Un A'); F : transient (A-A') |] \
-\ ==> F : LeadsTo A A'";
+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 (rtac (ensuresI RS leadsTo_Basis) 1);
by (blast_tac (claset() addIs [transient_strengthen]) 2);
@@ -161,9 +161,9 @@
qed "LeadsTo_Basis";
Goal "[| F : Invariant INV; \
-\ F : Constrains (INV Int (A-A')) (A Un A'); \
+\ F : (INV Int (A-A')) Co (A Un A'); \
\ F : transient (INV Int (A-A')) |] \
-\ ==> F : LeadsTo A A'";
+\ ==> F : A LeadsTo A'";
by (rtac Invariant_LeadsToI 1);
by (assume_tac 1);
by (rtac LeadsTo_Basis 1);
@@ -172,8 +172,8 @@
qed "Invariant_LeadsTo_Basis";
Goal "[| F : Invariant INV; \
-\ F : LeadsTo A A'; INV Int B <= A; INV Int A' <= B' |] \
-\ ==> F : LeadsTo B B'";
+\ F : A LeadsTo A'; INV Int B <= A; INV Int A' <= B' |] \
+\ ==> F : B LeadsTo B'";
by (REPEAT (ares_tac [Invariant_includes_reachable,
reachable_LeadsTo_weaken] 1));
qed "Invariant_LeadsTo_weaken";
@@ -181,15 +181,15 @@
(*Set difference: maybe combine with leadsTo_weaken_L??
This is the most useful form of the "disjunction" rule*)
-Goal "[| F : LeadsTo (A-B) C; F : LeadsTo (A Int B) C |] \
-\ ==> F : LeadsTo A C";
+Goal "[| F : (A-B) LeadsTo C; F : (A Int B) LeadsTo C |] \
+\ ==> F : A LeadsTo C";
by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
qed "LeadsTo_Diff";
val prems =
-Goal "(!! i. i:I ==> F : LeadsTo (A i) (A' i)) \
-\ ==> F : LeadsTo (UN i:I. A i) (UN i:I. A' i)";
+Goal "(!! i. i:I ==> F : (A i) LeadsTo (A' i)) \
+\ ==> F : (UN i:I. A i) LeadsTo (UN i:I. A' i)";
by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1);
by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_R]
addIs prems) 1);
@@ -198,22 +198,22 @@
(*Version with no index set*)
val prems =
-Goal "(!! i. F : LeadsTo (A i) (A' i)) \
-\ ==> F : LeadsTo (UN i. A i) (UN i. A' i)";
+Goal "(!! i. F : (A i) LeadsTo (A' i)) \
+\ ==> F : (UN i. A i) LeadsTo (UN i. A' i)";
by (blast_tac (claset() addIs [LeadsTo_UN_UN]
addIs prems) 1);
qed "LeadsTo_UN_UN_noindex";
(*Version with no index set*)
-Goal "ALL i. F : LeadsTo (A i) (A' i) \
-\ ==> F : LeadsTo (UN i. A i) (UN i. A' i)";
+Goal "ALL i. F : (A i) LeadsTo (A' i) \
+\ ==> F : (UN i. A i) LeadsTo (UN i. A' i)";
by (blast_tac (claset() addIs [LeadsTo_UN_UN]) 1);
qed "all_LeadsTo_UN_UN";
(*Binary union version*)
-Goal "[| F : LeadsTo A A'; F : LeadsTo B B' |] \
-\ ==> F : LeadsTo (A Un B) (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";
@@ -221,27 +221,27 @@
(** The cancellation law **)
-Goal "[| F : LeadsTo A (A' Un B); F : LeadsTo B B' |] \
-\ ==> F : LeadsTo A (A' Un B')";
+Goal "[| F : A LeadsTo (A' Un B); F : B LeadsTo 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 : LeadsTo A (A' Un B); F : LeadsTo (B-A') B' |] \
-\ ==> F : LeadsTo A (A' Un B')";
+Goal "[| F : A LeadsTo (A' Un B); F : (B-A') LeadsTo B' |] \
+\ ==> F : A LeadsTo (A' Un B')";
by (rtac LeadsTo_cancel2 1);
by (assume_tac 2);
by (ALLGOALS Asm_simp_tac);
qed "LeadsTo_cancel_Diff2";
-Goal "[| F : LeadsTo A (B Un A'); F : LeadsTo B B' |] \
-\ ==> F : LeadsTo A (B' Un A')";
+Goal "[| F : A LeadsTo (B Un A'); F : B LeadsTo B' |] \
+\ ==> F : A LeadsTo (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 "[| F : LeadsTo A (B Un A'); F : LeadsTo (B-A') B' |] \
-\ ==> F : LeadsTo A (B' Un A')";
+Goal "[| F : A LeadsTo (B Un A'); F : (B-A') LeadsTo B' |] \
+\ ==> F : A LeadsTo (B' Un A')";
by (rtac LeadsTo_cancel1 1);
by (assume_tac 2);
by (ALLGOALS Asm_simp_tac);
@@ -251,7 +251,7 @@
(** The impossibility law **)
(*The set "A" may be non-empty, but it contains no reachable states*)
-Goal "F : LeadsTo A {} ==> reachable F Int A = {}";
+Goal "F : A LeadsTo {} ==> reachable F Int A = {}";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (etac leadsTo_empty 1);
qed "LeadsTo_empty";
@@ -260,33 +260,33 @@
(** PSP: Progress-Safety-Progress **)
(*Special case of PSP: Misra's "stable conjunction"*)
-Goal "[| F : LeadsTo A A'; F : Stable B |] \
-\ ==> F : LeadsTo (A Int B) (A' Int B)";
+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 (dtac psp_stable 1);
by (assume_tac 1);
by (asm_full_simp_tac (simpset() addsimps Int_ac) 1);
qed "PSP_stable";
-Goal "[| F : LeadsTo A A'; F : Stable B |] \
-\ ==> F : LeadsTo (B Int A) (B Int A')";
+Goal "[| F : A LeadsTo A'; F : Stable B |] \
+\ ==> F : (B Int A) LeadsTo (B Int A')";
by (asm_simp_tac (simpset() addsimps PSP_stable::Int_ac) 1);
qed "PSP_stable2";
Goalw [LeadsTo_def, Constrains_def]
- "[| F : LeadsTo A A'; F : Constrains B B' |] \
-\ ==> F : LeadsTo (A Int B) ((A' Int B) Un (B' - B))";
+ "[| F : A LeadsTo A'; F : B Co B' |] \
+\ ==> F : (A Int B) LeadsTo ((A' Int B) Un (B' - B))";
by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1);
qed "PSP";
-Goal "[| F : LeadsTo A A'; F : Constrains B B' |] \
-\ ==> F : LeadsTo (B Int A) ((B Int A') Un (B' - B))";
+Goal "[| F : A LeadsTo A'; F : B Co B' |] \
+\ ==> F : (B Int A) LeadsTo ((B Int A') Un (B' - B))";
by (asm_simp_tac (simpset() addsimps PSP::Int_ac) 1);
qed "PSP2";
Goalw [Unless_def]
- "[| F : LeadsTo A A'; F : Unless B B' |] \
-\ ==> F : LeadsTo (A Int B) ((A' Int B) Un B')";
+ "[| F : A LeadsTo A'; F : B Unless B' |] \
+\ ==> F : (A Int B) LeadsTo ((A' Int B) Un B')";
by (dtac PSP 1);
by (assume_tac 1);
by (blast_tac (claset() addIs [LeadsTo_Diff, LeadsTo_weaken,
@@ -295,7 +295,7 @@
Goal "[| F : Stable A; F : transient C; \
-\ reachable F <= (-A Un B Un C) |] ==> F : LeadsTo A B";
+\ reachable F <= (-A Un B Un C) |] ==> F : A LeadsTo B";
by (etac reachable_LeadsTo_weaken 1);
by (rtac LeadsTo_Diff 1);
by (etac (transient_imp_leadsTo RS leadsTo_imp_LeadsTo RS PSP_stable2) 2);
@@ -307,9 +307,9 @@
(** Meta or object quantifier ????? **)
Goal "[| wf r; \
-\ ALL m. F : LeadsTo (A Int f-``{m}) \
+\ ALL m. F : (A Int f-``{m}) LeadsTo \
\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
-\ ==> F : LeadsTo A B";
+\ ==> F : A LeadsTo B";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (etac leadsTo_wf_induct 1);
by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
@@ -317,9 +317,9 @@
Goal "[| wf r; \
-\ ALL m:I. F : LeadsTo (A Int f-``{m}) \
+\ ALL m:I. F : (A Int f-``{m}) LeadsTo \
\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
-\ ==> F : LeadsTo A ((A - (f-``I)) Un B)";
+\ ==> F : A LeadsTo ((A - (f-``I)) Un B)";
by (etac LeadsTo_wf_induct 1);
by Safe_tac;
by (case_tac "m:I" 1);
@@ -328,9 +328,9 @@
qed "Bounded_induct";
-Goal "[| ALL m. F : LeadsTo (A Int f-``{m}) \
+Goal "[| ALL m. F : (A Int f-``{m}) LeadsTo \
\ ((A Int f-``(lessThan m)) Un B) |] \
-\ ==> F : LeadsTo A B";
+\ ==> F : A LeadsTo B";
by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
by (Asm_simp_tac 1);
qed "LessThan_induct";
@@ -338,26 +338,26 @@
(*Integer version. Could generalize from #0 to any lower bound*)
val [reach, prem] =
Goal "[| reachable F <= {s. #0 <= f s}; \
-\ !! z. F : LeadsTo (A Int {s. f s = z}) \
+\ !! z. F : (A Int {s. f s = z}) LeadsTo \
\ ((A Int {s. f s < z}) Un B) |] \
-\ ==> F : LeadsTo A B";
+\ ==> F : A LeadsTo B";
by (res_inst_tac [("f", "nat o f")] (allI RS LessThan_induct) 1);
by (simp_tac (simpset() addsimps [vimage_def]) 1);
by (rtac ([reach, prem] MRS reachable_LeadsTo_weaken) 1);
by (auto_tac (claset(), simpset() addsimps [nat_eq_iff, nat_less_iff]));
qed "integ_0_le_induct";
-Goal "[| ALL m:(greaterThan l). F : LeadsTo (A Int f-``{m}) \
+Goal "[| ALL m:(greaterThan l). F : (A Int f-``{m}) LeadsTo \
\ ((A Int f-``(lessThan m)) Un B) |] \
-\ ==> F : LeadsTo A ((A Int (f-``(atMost l))) Un B)";
+\ ==> F : A LeadsTo ((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 (Asm_simp_tac 1);
qed "LessThan_bounded_induct";
-Goal "[| ALL m:(lessThan l). F : LeadsTo (A Int f-``{m}) \
+Goal "[| ALL m:(lessThan l). F : (A Int f-``{m}) LeadsTo \
\ ((A Int f-``(greaterThan m)) Un B) |] \
-\ ==> F : LeadsTo A ((A Int (f-``(atLeast l))) Un B)";
+\ ==> F : A LeadsTo ((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 (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
@@ -370,27 +370,27 @@
(*** Completion: Binary and General Finite versions ***)
-Goal "[| F : LeadsTo A A'; F : Stable A'; \
-\ F : LeadsTo B B'; F : Stable B' |] \
-\ ==> F : LeadsTo (A Int B) (A' Int B')";
+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 (blast_tac (claset() addIs [stable_completion, leadsTo_weaken]) 1);
qed "Stable_completion";
Goal "finite I \
-\ ==> (ALL i:I. F : LeadsTo (A i) (A' i)) --> \
+\ ==> (ALL i:I. F : (A i) LeadsTo (A' i)) --> \
\ (ALL i:I. F : Stable (A' i)) --> \
-\ F : LeadsTo (INT i:I. A i) (INT i:I. A' i)";
+\ F : (INT i:I. A i) LeadsTo (INT i:I. A' i)";
by (etac finite_induct 1);
by (Asm_simp_tac 1);
by (asm_simp_tac (simpset() addsimps [Stable_completion, ball_Stable_INT]) 1);
qed_spec_mp "Finite_stable_completion";
-Goal "[| F : LeadsTo A (A' Un C); F : Constrains A' (A' Un C); \
-\ F : LeadsTo B (B' Un C); F : Constrains B' (B' Un C) |] \
-\ ==> F : LeadsTo (A Int B) ((A' Int B') Un C)";
+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,
Int_Un_distrib]) 1);
by (blast_tac (claset() addIs [completion, leadsTo_weaken]) 1);
@@ -398,9 +398,9 @@
Goal "[| finite I |] \
-\ ==> (ALL i:I. F : LeadsTo (A i) (A' i Un C)) --> \
-\ (ALL i:I. F : Constrains (A' i) (A' i Un C)) --> \
-\ F : LeadsTo (INT i:I. A i) ((INT i:I. A' i) Un C)";
+\ ==> (ALL i:I. F : (A i) LeadsTo (A' i Un C)) --> \
+\ (ALL i:I. F : (A' i) Co (A' i Un C)) --> \
+\ F : (INT i:I. A i) LeadsTo ((INT i:I. A' i) Un C)";
by (etac finite_induct 1);
by (ALLGOALS Asm_simp_tac);
by (Clarify_tac 1);
@@ -416,7 +416,7 @@
etac Invariant_LeadsTo_Basis 1
ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
REPEAT (ares_tac [LeadsTo_Basis, ensuresI] 1),
- (*now there are two subgoals: constrains & transient*)
+ (*now there are two subgoals: co & transient*)
simp_tac (simpset() addsimps !program_defs_ref) 2,
res_inst_tac [("act", sact)] transient_mem 2,
(*simplify the command's domain*)
--- a/src/HOL/UNITY/SubstAx.thy Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/SubstAx.thy Thu Apr 29 10:51:58 1999 +0200
@@ -3,14 +3,16 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-LeadsTo relation: restricted to the set of reachable states.
+Weak LeadsTo relation (restricted to the set of reachable states)
*)
SubstAx = WFair + Constrains +
-constdefs
+consts
+ LeadsTo :: "['a set, 'a set] => 'a program set" (infixl 60)
- LeadsTo :: "['a set, 'a set] => 'a program set"
- "LeadsTo A B == {F. F : leadsTo (reachable F Int A)
- (reachable F Int B)}"
+defs
+ LeadsTo_def
+ "A LeadsTo B == {F. F : (reachable F Int A) leadsTo
+ (reachable F Int B)}"
end
--- a/src/HOL/UNITY/Token.ML Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/Token.ML Thu Apr 29 10:51:58 1999 +0200
@@ -67,7 +67,7 @@
(*From "A Logic for Concurrent Programming", but not used in Chapter 4.
Note the use of case_tac. Reasoning about leadsTo takes practice!*)
Goal "[| i<N; j<N |] ==> \
-\ F : leadsTo (HasTok i) ({s. (token s, i) : nodeOrder j} Un HasTok j)";
+\ F : (HasTok i) leadsTo ({s. (token s, i) : nodeOrder j} Un HasTok j)";
by (case_tac "i=j" 1);
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
by (rtac (TR7 RS leadsTo_weaken_R) 1);
@@ -78,7 +78,7 @@
(*Chapter 4 variant, the one actually used below.*)
Goal "[| i<N; j<N; i~=j |] \
-\ ==> F : leadsTo (HasTok i) {s. (token s, i) : nodeOrder j}";
+\ ==> F : (HasTok i) leadsTo {s. (token s, i) : nodeOrder j}";
by (rtac (TR7 RS leadsTo_weaken_R) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
@@ -91,7 +91,7 @@
(*Misra's TR9: the token reaches an arbitrary node*)
-Goal "j<N ==> F : leadsTo {s. token s < N} (HasTok j)";
+Goal "j<N ==> F : {s. token s < N} leadsTo (HasTok j)";
by (rtac leadsTo_weaken_R 1);
by (res_inst_tac [("I", "-{j}"), ("f", "token"), ("B", "{}")]
(wf_nodeOrder RS bounded_induct) 1);
@@ -105,7 +105,7 @@
qed "leadsTo_j";
(*Misra's TR8: a hungry process eventually eats*)
-Goal "j<N ==> F : leadsTo ({s. token s < N} Int H j) (E j)";
+Goal "j<N ==> F : ({s. token s < N} Int H j) leadsTo (E j)";
by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1);
by (rtac TR6 2);
by (rtac leadsTo_weaken_R 1);
--- a/src/HOL/UNITY/Token.thy Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/Token.thy Thu Apr 29 10:51:58 1999 +0200
@@ -43,17 +43,17 @@
assumes
N_positive "0<N"
- TR2 "F : constrains (T i) (T i Un H i)"
+ TR2 "F : (T i) co (T i Un H i)"
- TR3 "F : constrains (H i) (H i Un E i)"
+ TR3 "F : (H i) co (H i Un E i)"
- TR4 "F : constrains (H i - HasTok i) (H i)"
+ TR4 "F : (H i - HasTok i) co (H i)"
- TR5 "F : constrains (HasTok i) (HasTok i Un -(E i))"
+ TR5 "F : (HasTok i) co (HasTok i Un -(E i))"
- TR6 "F : leadsTo (H i Int HasTok i) (E i)"
+ TR6 "F : (H i Int HasTok i) leadsTo (E i)"
- TR7 "F : leadsTo (HasTok i) (HasTok (next i))"
+ TR7 "F : (HasTok i) leadsTo (HasTok (next i))"
defines
nodeOrder_def
--- a/src/HOL/UNITY/UNITY.ML Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/UNITY.ML Thu Apr 29 10:51:58 1999 +0200
@@ -111,92 +111,91 @@
fun simp_of_set def = def RS def_set_simp;
-(*** constrains ***)
+(*** co ***)
-overload_1st_set "UNITY.constrains";
+overload_1st_set "UNITY.op co";
overload_1st_set "UNITY.stable";
overload_1st_set "UNITY.unless";
val prems = Goalw [constrains_def]
"(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A') \
-\ ==> F : constrains A A'";
+\ ==> F : A co A'";
by (blast_tac (claset() addIs prems) 1);
qed "constrainsI";
Goalw [constrains_def]
- "[| F : constrains A A'; act: Acts F; (s,s'): act; s: A |] ==> s': A'";
+ "[| F : A co A'; act: Acts F; (s,s'): act; s: A |] ==> s': A'";
by (Blast_tac 1);
qed "constrainsD";
-Goalw [constrains_def] "F : constrains {} B";
+Goalw [constrains_def] "F : {} co B";
by (Blast_tac 1);
qed "constrains_empty";
-Goalw [constrains_def] "F : constrains A UNIV";
+Goalw [constrains_def] "F : A co UNIV";
by (Blast_tac 1);
qed "constrains_UNIV";
AddIffs [constrains_empty, constrains_UNIV];
(*monotonic in 2nd argument*)
Goalw [constrains_def]
- "[| F : constrains A A'; A'<=B' |] ==> F : constrains A B'";
+ "[| F : A co A'; A'<=B' |] ==> F : A co B'";
by (Blast_tac 1);
qed "constrains_weaken_R";
(*anti-monotonic in 1st argument*)
Goalw [constrains_def]
- "[| F : constrains A A'; B<=A |] ==> F : constrains B A'";
+ "[| F : A co A'; B<=A |] ==> F : B co A'";
by (Blast_tac 1);
qed "constrains_weaken_L";
Goalw [constrains_def]
- "[| F : constrains A A'; B<=A; A'<=B' |] ==> F : constrains B B'";
+ "[| F : A co A'; B<=A; A'<=B' |] ==> F : B co B'";
by (Blast_tac 1);
qed "constrains_weaken";
(** Union **)
Goalw [constrains_def]
- "[| F : constrains A A'; F : constrains B B' |] \
-\ ==> F : constrains (A Un B) (A' Un B')";
+ "[| F : A co A'; F : B co B' |] \
+\ ==> F : (A Un B) co (A' Un B')";
by (Blast_tac 1);
qed "constrains_Un";
Goalw [constrains_def]
- "ALL i:I. F : constrains (A i) (A' i) \
-\ ==> F : constrains (UN i:I. A i) (UN i:I. A' i)";
+ "ALL i:I. F : (A i) co (A' i) \
+\ ==> F : (UN i:I. A i) co (UN i:I. A' i)";
by (Blast_tac 1);
qed "ball_constrains_UN";
(** Intersection **)
Goalw [constrains_def]
- "[| F : constrains A A'; F : constrains B B' |] \
-\ ==> F : constrains (A Int B) (A' Int B')";
+ "[| F : A co A'; F : B co B' |] \
+\ ==> F : (A Int B) co (A' Int B')";
by (Blast_tac 1);
qed "constrains_Int";
Goalw [constrains_def]
- "ALL i:I. F : constrains (A i) (A' i) \
-\ ==> F : constrains (INT i:I. A i) (INT i:I. A' i)";
+ "ALL i:I. F : (A i) co (A' i) \
+\ ==> F : (INT i:I. A i) co (INT i:I. A' i)";
by (Blast_tac 1);
qed "ball_constrains_INT";
-Goalw [constrains_def] "F : constrains A A' ==> A <= A'";
+Goalw [constrains_def] "F : A co A' ==> A <= A'";
by Auto_tac;
qed "constrains_imp_subset";
-(*The reasoning is by subsets since "constrains" refers to single actions
+(*The reasoning is by subsets since "co" refers to single actions
only. So this rule isn't that useful.*)
Goalw [constrains_def]
- "[| F : constrains A B; F : constrains B C |] \
-\ ==> F : constrains A C";
+ "[| F : A co B; F : B co C |] ==> F : A co C";
by (Blast_tac 1);
qed "constrains_trans";
Goalw [constrains_def]
- "[| F : constrains A (A' Un B); F : constrains B B' |] \
-\ ==> F : constrains A (A' Un B')";
+ "[| F : A co (A' Un B); F : B co B' |] \
+\ ==> F : A co (A' Un B')";
by (Clarify_tac 1);
by (Blast_tac 1);
qed "constrains_cancel";
@@ -204,11 +203,11 @@
(*** stable ***)
-Goalw [stable_def] "F : constrains A A ==> F : stable A";
+Goalw [stable_def] "F : A co A ==> F : stable A";
by (assume_tac 1);
qed "stableI";
-Goalw [stable_def] "F : stable A ==> F : constrains A A";
+Goalw [stable_def] "F : stable A ==> F : A co A";
by (assume_tac 1);
qed "stableD";
@@ -237,18 +236,18 @@
qed "ball_stable_INT";
Goalw [stable_def, constrains_def]
- "[| F : stable C; F : constrains A (C Un A') |] \
-\ ==> F : constrains (C Un A) (C Un A')";
+ "[| F : stable C; F : A co (C Un A') |] \
+\ ==> F : (C Un A) co (C Un A')";
by (Blast_tac 1);
qed "stable_constrains_Un";
Goalw [stable_def, constrains_def]
- "[| F : stable C; F : constrains (C Int A) A' |] \
-\ ==> F : constrains (C Int A) (C Int A')";
+ "[| F : stable C; F : (C Int A) co A' |] \
+\ ==> F : (C Int A) co (C Int A')";
by (Blast_tac 1);
qed "stable_constrains_Int";
-(*[| F : stable C; F : constrains (C Int A) A |] ==> F : stable (C Int A)*)
+(*[| F : stable C; F : co (C Int A) A |] ==> F : stable (C Int A)*)
bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
@@ -284,15 +283,15 @@
in forward proof. **)
Goalw [constrains_def]
- "[| ALL m. F : constrains {s. s x = m} (B m) |] \
-\ ==> F : constrains {s. s x : M} (UN m:M. B m)";
+ "[| ALL m:M. F : {s. s x = m} co (B m) |] \
+\ ==> F : {s. s x : M} co (UN m:M. B m)";
by (Blast_tac 1);
qed "elimination";
(*As above, but for the trivial case of a one-variable state, in which the
state is identified with its one variable.*)
Goalw [constrains_def]
- "(ALL m. F : constrains {m} (B m)) ==> F : constrains M (UN m:M. B m)";
+ "(ALL m:M. F : {m} co (B m)) ==> F : M co (UN m:M. B m)";
by (Blast_tac 1);
qed "elimination_sing";
@@ -301,11 +300,11 @@
(*** Theoretical Results from Section 6 ***)
Goalw [constrains_def, strongest_rhs_def]
- "F : constrains A (strongest_rhs F A )";
+ "F : A co (strongest_rhs F A )";
by (Blast_tac 1);
qed "constrains_strongest_rhs";
Goalw [constrains_def, strongest_rhs_def]
- "F : constrains A B ==> strongest_rhs F A <= B";
+ "F : A co B ==> strongest_rhs F A <= B";
by (Blast_tac 1);
qed "strongest_rhs_is_strongest";
--- a/src/HOL/UNITY/UNITY.thy Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/UNITY.thy Thu Apr 29 10:51:58 1999 +0200
@@ -14,6 +14,9 @@
typedef (Program)
'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
+consts
+ co, unless :: "['a set, 'a set] => 'a program set" (infixl 60)
+
constdefs
mk_program :: "('a set * ('a * 'a)set set) => 'a program"
"mk_program == %(init, acts). Abs_Program (init, insert Id acts)"
@@ -24,17 +27,11 @@
Acts :: "'a program => ('a * 'a)set set"
"Acts F == (%(init, acts). acts) (Rep_Program F)"
- constrains :: "['a set, 'a set] => 'a program set"
- "constrains A B == {F. ALL act: Acts F. act^^A <= B}"
-
stable :: "'a set => 'a program set"
- "stable A == constrains A A"
+ "stable A == A co A"
strongest_rhs :: "['a program, 'a set] => 'a set"
- "strongest_rhs F A == Inter {B. F : constrains A B}"
-
- unless :: "['a set, 'a set] => 'a program set"
- "unless A B == constrains (A-B) (A Un B)"
+ "strongest_rhs F A == Inter {B. F : A co B}"
invariant :: "'a set => 'a program set"
"invariant A == {F. Init F <= A} Int stable A"
@@ -43,4 +40,10 @@
increasing :: "['a => 'b::{ord}] => 'a program set"
"increasing f == INT z. stable {s. z <= f s}"
+
+defs
+ constrains_def "A co B == {F. ALL act: Acts F. act^^A <= B}"
+
+ unless_def "A unless B == (A-B) co (A Un B)"
+
end
--- a/src/HOL/UNITY/Union.ML Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/Union.ML Thu Apr 29 10:51:58 1999 +0200
@@ -137,24 +137,24 @@
qed "JN_Join_distrib";
-(*** Safety: constrains, stable, FP ***)
+(*** Safety: co, stable, FP ***)
Goalw [constrains_def, JOIN_def]
"i : I ==> \
-\ (JN i:I. F i) : constrains A B = (ALL i:I. F i : constrains A B)";
+\ (JN i:I. F i) : A co B = (ALL i:I. F i : A co B)";
by (Simp_tac 1);
by (Blast_tac 1);
qed "constrains_JN";
-Goal "F Join G : constrains A B = \
-\ (F : constrains A B & G : constrains A B)";
+Goal "F Join G : A co B = \
+\ (F : A co B & G : A co B)";
by (auto_tac
(claset(),
simpset() addsimps [constrains_def, Join_def]));
qed "constrains_Join";
-Goal "[| i : I; ALL i:I. F i : constrains A B |] \
-\ ==> (JN i:I. F i) : constrains A B";
+Goal "[| i : I; ALL i:I. F i : A co B |] \
+\ ==> (JN i:I. F i) : A co B";
by (full_simp_tac (simpset() addsimps [constrains_def, Acts_JN]) 1);
by (Blast_tac 1);
qed "constrains_imp_JN_constrains";
@@ -164,12 +164,12 @@
reachable F and reachable G
Goalw [Constrains_def]
- "(JN i:I. F i) : Constrains A B = (ALL i:I. F i : Constrains A B)";
+ "(JN i:I. F i) : A Co B = (ALL i:I. F i : A Co B)";
by (simp_tac (simpset() addsimps [constrains_JN]) 1);
by (Blast_tac 1);
qed "Constrains_JN";
- Goal "F Join G : Constrains A B = (Constrains F A B & Constrains G A B)";
+ Goal "F Join G : A Co B = (F Co A B & G Co A B)";
by (auto_tac
(claset(),
simpset() addsimps [Constrains_def, constrains_Join]));
@@ -177,8 +177,8 @@
**)
-Goal "[| F : constrains A A'; G : constrains B B' |] \
-\ ==> F Join G : constrains (A Int B) (A' Un B')";
+Goal "[| F : A co A'; G : B co B' |] \
+\ ==> F Join G : (A Int B) co (A' Un B')";
by (simp_tac (simpset() addsimps [constrains_Join]) 1);
by (blast_tac (claset() addIs [constrains_weaken]) 1);
qed "constrains_Join_weaken";
@@ -226,25 +226,25 @@
qed "transient_Join";
Goal "i : I ==> \
-\ (JN i:I. F i) : ensures A B = \
-\ ((ALL i:I. F i : constrains (A-B) (A Un B)) & \
-\ (EX i:I. F i : ensures A B))";
+\ (JN i:I. F i) : A ensures B = \
+\ ((ALL i:I. F i : (A-B) co (A Un B)) & \
+\ (EX i:I. F i : A ensures B))";
by (auto_tac (claset(),
simpset() addsimps [ensures_def, constrains_JN, transient_JN]));
qed "ensures_JN";
Goalw [ensures_def]
- "F Join G : ensures A B = \
-\ (F : constrains (A-B) (A Un B) & \
-\ G : constrains (A-B) (A Un B) & \
-\ (F : ensures A B | G : ensures A B))";
+ "F Join G : A ensures B = \
+\ (F : (A-B) co (A Un B) & \
+\ G : (A-B) co (A Un B) & \
+\ (F : A ensures B | G : A ensures B))";
by (auto_tac (claset(),
simpset() addsimps [constrains_Join, transient_Join]));
qed "ensures_Join";
Goalw [stable_def, constrains_def, Join_def]
- "[| F : stable A; G : constrains A A' |] \
-\ ==> F Join G : constrains A A'";
+ "[| F : stable A; G : A co A' |] \
+\ ==> F Join G : A co A'";
by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1);
by (Blast_tac 1);
qed "stable_constrains_Join";
@@ -258,7 +258,7 @@
simpset() addsimps [Acts_Join]) 1);
qed "stable_Join_Invariant";
-Goal "[| F : stable A; G : ensures A B |] ==> F Join G : ensures A B";
+Goal "[| F : stable A; G : A ensures B |] ==> F Join G : A ensures B";
by (asm_simp_tac (simpset() addsimps [ensures_Join]) 1);
by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
by (etac constrains_weaken 1);
@@ -266,7 +266,7 @@
qed "ensures_stable_Join1";
(*As above, but exchanging the roles of F and G*)
-Goal "[| F : ensures A B; G : stable A |] ==> F Join G : ensures A B";
+Goal "[| F : A ensures B; G : stable A |] ==> F Join G : A ensures B";
by (stac Join_commute 1);
by (blast_tac (claset() addIs [ensures_stable_Join1]) 1);
qed "ensures_stable_Join2";
@@ -308,11 +308,11 @@
(*** Higher-level rules involving localTo and Join ***)
-Goal "[| F : constrains {s. P (v s) (w s)} {s. P' (v s) (w s)}; \
+Goal "[| F : {s. P (v s) (w s)} co {s. P' (v s) (w s)}; \
\ F Join G : v localTo F; \
\ F Join G : w localTo F; \
\ Disjoint F G |] \
-\ ==> F Join G : constrains {s. P (v s) (w s)} {s. P' (v s) (w s)}";
+\ ==> F Join G : {s. P (v s) (w s)} co {s. P' (v s) (w s)}";
by (auto_tac (claset(), simpset() addsimps [constrains_def, Acts_Join]));
by (REPEAT_FIRST (dtac localTo_imp_equals THEN' REPEAT1 o atac));
by Auto_tac;
@@ -339,11 +339,11 @@
\ ==> F Join G : Stable {s. v s <= w s}";
by (safe_tac (claset() addSDs [localTo_imp_stable]));
by (rewrite_goals_tac [stable_def, Stable_def, Increasing_def]);
-by (subgoal_tac "ALL k: UNIV. ?H : Constrains ({s. v s = k} Int ?AA) ?AA" 1);
+by (subgoal_tac "ALL k: UNIV. ?H : ({s. v s = k} Int ?AA) Co ?AA" 1);
by (dtac ball_Constrains_UN 1);
by (full_simp_tac (simpset() addsimps [UN_eq_UNIV]) 1);
by (rtac ballI 1);
-by (subgoal_tac "F Join G : constrains ({s. v s = k} Int {s. v s <= w s}) \
+by (subgoal_tac "F Join G : ({s. v s = k} Int {s. v s <= w s}) co \
\ ({s. v s = k} Un {s. v s <= w s})" 1);
by (asm_simp_tac (simpset() addsimps [constrains_Join]) 2);
by (blast_tac (claset() addIs [constrains_weaken]) 2);
--- a/src/HOL/UNITY/WFair.ML Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/WFair.ML Thu Apr 29 10:51:58 1999 +0200
@@ -11,7 +11,7 @@
overload_1st_set "WFair.transient";
overload_1st_set "WFair.ensures";
-overload_1st_set "WFair.leadsTo";
+overload_1st_set "WFair.op leadsTo";
(*** transient ***)
@@ -35,38 +35,38 @@
(*** ensures ***)
Goalw [ensures_def]
- "[| F : constrains (A-B) (A Un B); F : transient (A-B) |] \
-\ ==> F : ensures A B";
+ "[| F : (A-B) co (A Un B); F : transient (A-B) |] \
+\ ==> F : A ensures B";
by (Blast_tac 1);
qed "ensuresI";
Goalw [ensures_def]
- "F : ensures A B ==> F : constrains (A-B) (A Un B) & F : transient (A-B)";
+ "F : A ensures B ==> F : (A-B) co (A Un B) & F : transient (A-B)";
by (Blast_tac 1);
qed "ensuresD";
(*The L-version (precondition strengthening) doesn't hold for ENSURES*)
Goalw [ensures_def]
- "[| F : ensures A A'; A'<=B' |] ==> F : ensures A B'";
+ "[| F : A ensures A'; A'<=B' |] ==> F : A ensures B'";
by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
qed "ensures_weaken_R";
Goalw [ensures_def, constrains_def, transient_def]
- "F : ensures A UNIV";
+ "F : A ensures UNIV";
by Auto_tac;
qed "ensures_UNIV";
Goalw [ensures_def]
"[| F : stable C; \
-\ F : constrains (C Int (A - A')) (A Un A'); \
+\ F : (C Int (A - A')) co (A Un A'); \
\ F : transient (C Int (A-A')) |] \
-\ ==> F : ensures (C Int A) (C Int A')";
+\ ==> F : (C Int A) ensures (C Int A')";
by (asm_simp_tac (simpset() addsimps [Int_Un_distrib RS sym,
Diff_Int_distrib RS sym,
stable_constrains_Int]) 1);
qed "stable_ensures_Int";
-Goal "[| F : stable A; F : transient C; A <= B Un C |] ==> F : ensures A B";
+Goal "[| F : stable A; F : transient C; A <= B Un C |] ==> F : A ensures B";
by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1);
by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
qed "stable_transient_ensures";
@@ -74,55 +74,55 @@
(*** leadsTo ***)
-Goalw [leadsTo_def] "F : ensures A B ==> F : leadsTo A B";
+Goalw [leadsTo_def] "F : A ensures B ==> F : A leadsTo B";
by (blast_tac (claset() addIs [leadsto.Basis]) 1);
qed "leadsTo_Basis";
Goalw [leadsTo_def]
- "[| F : leadsTo A B; F : leadsTo B C |] ==> F : leadsTo A C";
+ "[| F : A leadsTo B; F : B leadsTo C |] ==> F : A leadsTo C";
by (blast_tac (claset() addIs [leadsto.Trans]) 1);
qed "leadsTo_Trans";
-Goal "F : transient A ==> F : leadsTo A (-A)";
+Goal "F : transient A ==> F : A leadsTo (-A)";
by (asm_simp_tac
(simpset() addsimps [leadsTo_Basis, ensuresI, Compl_partition]) 1);
qed "transient_imp_leadsTo";
-Goal "F : leadsTo A UNIV";
+Goal "F : A leadsTo UNIV";
by (blast_tac (claset() addIs [ensures_UNIV RS leadsTo_Basis]) 1);
qed "leadsTo_UNIV";
Addsimps [leadsTo_UNIV];
(*Useful with cancellation, disjunction*)
-Goal "F : leadsTo A (A' Un A') ==> F : leadsTo A A'";
+Goal "F : A leadsTo (A' Un A') ==> F : A leadsTo A'";
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
qed "leadsTo_Un_duplicate";
-Goal "F : leadsTo A (A' Un C Un C) ==> F : leadsTo A (A' Un C)";
+Goal "F : A leadsTo (A' Un C Un C) ==> F : A leadsTo (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 = Goalw [leadsTo_def]
- "(!!A. A : S ==> F : leadsTo A B) ==> F : leadsTo (Union S) B";
+ "(!!A. A : S ==> F : A leadsTo B) ==> F : (Union S) leadsTo B";
by (blast_tac (claset() addIs [leadsto.Union] addDs prems) 1);
qed "leadsTo_Union";
val prems = Goalw [leadsTo_def]
- "(!!A. A : S ==> F : leadsTo (A Int C) B) \
-\ ==> F : leadsTo (Union S Int C) B";
+ "(!!A. A : S ==> F : (A Int C) leadsTo B) \
+\ ==> F : (Union S Int C) leadsTo B";
by (simp_tac (HOL_ss addsimps [Int_Union_Union]) 1);
by (blast_tac (claset() addIs [leadsto.Union] addDs prems) 1);
qed "leadsTo_Union_Int";
val prems = Goal
- "(!!i. i : I ==> F : leadsTo (A i) B) ==> F : leadsTo (UN i:I. A i) B";
+ "(!!i. i : I ==> F : (A i) leadsTo B) ==> F : (UN i:I. A i) leadsTo B";
by (stac (Union_image_eq RS sym) 1);
by (blast_tac (claset() addIs leadsTo_Union::prems) 1);
qed "leadsTo_UN";
(*Binary union introduction rule*)
-Goal "[| F : leadsTo A C; F : leadsTo B C |] ==> F : leadsTo (A Un B) C";
+Goal "[| F : A leadsTo C; F : B leadsTo C |] ==> F : (A Un B) leadsTo C";
by (stac Un_eq_Union 1);
by (blast_tac (claset() addIs [leadsTo_Union]) 1);
qed "leadsTo_Un";
@@ -130,18 +130,18 @@
(*The INDUCTION rule as we should have liked to state it*)
val major::prems = Goalw [leadsTo_def]
- "[| F : leadsTo za zb; \
-\ !!A B. F : ensures A B ==> P A B; \
-\ !!A B C. [| F : leadsTo A B; P A B; F : leadsTo B C; P B C |] \
+ "[| F : za leadsTo zb; \
+\ !!A B. F : A ensures B ==> P A B; \
+\ !!A B C. [| F : A leadsTo B; P A B; F : B leadsTo C; P B C |] \
\ ==> P A C; \
-\ !!B S. ALL A:S. F : leadsTo A B & P A B ==> P (Union S) B \
+\ !!B S. ALL A:S. F : A leadsTo B & P A B ==> P (Union S) B \
\ |] ==> P za zb";
by (rtac (major RS CollectD RS leadsto.induct) 1);
by (REPEAT (blast_tac (claset() addIs prems) 1));
qed "leadsTo_induct";
-Goal "A<=B ==> F : leadsTo A B";
+Goal "A<=B ==> F : A leadsTo B";
by (rtac leadsTo_Basis 1);
by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
by (Blast_tac 1);
@@ -151,36 +151,36 @@
Addsimps [empty_leadsTo];
-Goal "[| F : leadsTo A A'; A'<=B' |] ==> F : leadsTo A B'";
+Goal "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'";
by (blast_tac (claset() addIs [subset_imp_leadsTo, leadsTo_Trans]) 1);
qed "leadsTo_weaken_R";
-Goal "[| F : leadsTo A A'; B<=A |] ==> F : leadsTo B A'";
+Goal "[| F : A leadsTo A'; B<=A |] ==> F : B leadsTo A'";
by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1);
qed_spec_mp "leadsTo_weaken_L";
(*Distributes over binary unions*)
-Goal "F : leadsTo (A Un B) C = (F : leadsTo A C & F : leadsTo B C)";
+Goal "F : (A Un B) leadsTo C = (F : A leadsTo C & F : B leadsTo C)";
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1);
qed "leadsTo_Un_distrib";
-Goal "F : leadsTo (UN i:I. A i) B = (ALL i : I. F : leadsTo (A i) B)";
+Goal "F : (UN i:I. A i) leadsTo B = (ALL i : I. F : (A i) leadsTo B)";
by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1);
qed "leadsTo_UN_distrib";
-Goal "F : leadsTo (Union S) B = (ALL A : S. F : leadsTo A B)";
+Goal "F : (Union S) leadsTo B = (ALL A : S. F : A leadsTo B)";
by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1);
qed "leadsTo_Union_distrib";
-Goal "[| F : leadsTo A A'; B<=A; A'<=B' |] ==> F : leadsTo B B'";
+Goal "[| F : A leadsTo A'; B<=A; A'<=B' |] ==> F : B leadsTo B'";
by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L,
leadsTo_Trans]) 1);
qed "leadsTo_weaken";
(*Set difference: maybe combine with leadsTo_weaken_L??*)
-Goal "[| F : leadsTo (A-B) C; F : leadsTo B C |] ==> F : leadsTo A C";
+Goal "[| F : (A-B) leadsTo C; F : B leadsTo C |] ==> F : A leadsTo C";
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1);
qed "leadsTo_Diff";
@@ -189,8 +189,8 @@
see ball_constrains_UN in UNITY.ML***)
val prems = goal thy
- "(!! i. i:I ==> F : leadsTo (A i) (A' i)) \
-\ ==> F : leadsTo (UN i:I. A i) (UN i:I. A' i)";
+ "(!! i. i:I ==> F : (A i) leadsTo (A' i)) \
+\ ==> F : (UN i:I. A i) leadsTo (UN i:I. A' i)";
by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1);
by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_R]
addIs prems) 1);
@@ -199,21 +199,21 @@
(*Version with no index set*)
val prems = goal thy
- "(!! i. F : leadsTo (A i) (A' i)) \
-\ ==> F : leadsTo (UN i. A i) (UN i. A' i)";
+ "(!! i. F : (A i) leadsTo (A' i)) \
+\ ==> F : (UN i. A i) leadsTo (UN i. A' i)";
by (blast_tac (claset() addIs [leadsTo_UN_UN]
addIs prems) 1);
qed "leadsTo_UN_UN_noindex";
(*Version with no index set*)
-Goal "ALL i. F : leadsTo (A i) (A' i) \
-\ ==> F : leadsTo (UN i. A i) (UN i. A' i)";
+Goal "ALL i. F : (A i) leadsTo (A' i) \
+\ ==> F : (UN i. A i) leadsTo (UN i. A' i)";
by (blast_tac (claset() addIs [leadsTo_UN_UN]) 1);
qed "all_leadsTo_UN_UN";
(*Binary union version*)
-Goal "[| F : leadsTo A A'; F : leadsTo B B' |] ==> F : leadsTo (A Un B) (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";
@@ -221,27 +221,27 @@
(** The cancellation law **)
-Goal "[| F : leadsTo A (A' Un B); F : leadsTo B B' |] \
-\ ==> F : leadsTo A (A' Un B')";
+Goal "[| F : A leadsTo (A' Un B); F : B leadsTo 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 : leadsTo A (A' Un B); F : leadsTo (B-A') B' |] \
-\ ==> F : leadsTo A (A' Un B')";
+Goal "[| F : A leadsTo (A' Un B); F : (B-A') leadsTo B' |] \
+\ ==> F : A leadsTo (A' Un B')";
by (rtac leadsTo_cancel2 1);
by (assume_tac 2);
by (ALLGOALS Asm_simp_tac);
qed "leadsTo_cancel_Diff2";
-Goal "[| F : leadsTo A (B Un A'); F : leadsTo B B' |] \
-\ ==> F : leadsTo A (B' Un A')";
+Goal "[| F : A leadsTo (B Un A'); F : B leadsTo B' |] \
+\ ==> F : A leadsTo (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 "[| F : leadsTo A (B Un A'); F : leadsTo (B-A') B' |] \
-\ ==> F : leadsTo A (B' Un A')";
+Goal "[| F : A leadsTo (B Un A'); F : (B-A') leadsTo B' |] \
+\ ==> F : A leadsTo (B' Un A')";
by (rtac leadsTo_cancel1 1);
by (assume_tac 2);
by (ALLGOALS Asm_simp_tac);
@@ -251,14 +251,14 @@
(** The impossibility law **)
-Goal "F : leadsTo A B ==> B={} --> A={}";
+Goal "F : A leadsTo 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 "F : leadsTo A {} ==> A={}";
+Goal "F : A leadsTo {} ==> A={}";
by (blast_tac (claset() addSIs [lemma]) 1);
qed "leadsTo_empty";
@@ -267,8 +267,8 @@
(*Special case of PSP: Misra's "stable conjunction"*)
Goalw [stable_def]
- "[| F : leadsTo A A'; F : stable B |] \
-\ ==> F : leadsTo (A Int B) (A' Int B)";
+ "[| F : A leadsTo A'; F : stable B |] \
+\ ==> F : (A Int B) leadsTo (A' Int B)";
by (etac leadsTo_induct 1);
by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3);
by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
@@ -279,19 +279,19 @@
by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1);
qed "psp_stable";
-Goal "[| F : leadsTo A A'; F : stable B |] \
-\ ==> F : leadsTo (B Int A) (B Int A')";
+Goal "[| F : A leadsTo A'; F : stable B |] \
+\ ==> F : (B Int A) leadsTo (B Int A')";
by (asm_simp_tac (simpset() addsimps psp_stable::Int_ac) 1);
qed "psp_stable2";
Goalw [ensures_def, constrains_def]
- "[| F : ensures A A'; F : constrains B B' |] \
-\ ==> F : ensures (A Int B) ((A' Int B) Un (B' - B))";
+ "[| F : A ensures A'; F : B co B' |] \
+\ ==> F : (A Int B) ensures ((A' Int B) Un (B' - B))";
by (blast_tac (claset() addIs [transient_strengthen]) 1);
qed "psp_ensures";
-Goal "[| F : leadsTo A A'; F : constrains B B' |] \
-\ ==> F : leadsTo (A Int B) ((A' Int B) Un (B' - B))";
+Goal "[| F : A leadsTo A'; F : B co 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"*)
@@ -302,15 +302,15 @@
by (blast_tac (claset() addIs [leadsTo_Basis, psp_ensures]) 1);
qed "psp";
-Goal "[| F : leadsTo A A'; F : constrains B B' |] \
-\ ==> F : leadsTo (B Int A) ((B Int A') Un (B' - B))";
+Goal "[| F : A leadsTo A'; F : B co B' |] \
+\ ==> F : (B Int A) leadsTo ((B Int A') Un (B' - B))";
by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1);
qed "psp2";
Goalw [unless_def]
- "[| F : leadsTo A A'; F : unless B B' |] \
-\ ==> F : leadsTo (A Int B) ((A' Int B) Un B')";
+ "[| F : A leadsTo A'; F : B unless B' |] \
+\ ==> 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);
@@ -325,11 +325,11 @@
(** The most general rule: r is any wf relation; f is any variant function **)
Goal "[| wf r; \
-\ ALL m. F : leadsTo (A Int f-``{m}) \
+\ ALL m. F : (A Int f-``{m}) leadsTo \
\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
-\ ==> F : leadsTo (A Int f-``{m}) B";
+\ ==> F : (A Int f-``{m}) leadsTo B";
by (eres_inst_tac [("a","m")] wf_induct 1);
-by (subgoal_tac "F : leadsTo (A Int (f -`` (r^-1 ^^ {x}))) B" 1);
+by (subgoal_tac "F : (A Int (f -`` (r^-1 ^^ {x}))) leadsTo B" 1);
by (stac vimage_eq_UN 2);
by (asm_simp_tac (HOL_ss addsimps (UN_simps RL [sym])) 2);
by (blast_tac (claset() addIs [leadsTo_UN]) 2);
@@ -339,9 +339,9 @@
(** Meta or object quantifier ????? **)
Goal "[| wf r; \
-\ ALL m. F : leadsTo (A Int f-``{m}) \
+\ ALL m. F : (A Int f-``{m}) leadsTo \
\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
-\ ==> F : leadsTo A B";
+\ ==> F : A leadsTo B";
by (res_inst_tac [("t", "A")] subst 1);
by (rtac leadsTo_UN 2);
by (etac lemma 2);
@@ -351,9 +351,9 @@
Goal "[| wf r; \
-\ ALL m:I. F : leadsTo (A Int f-``{m}) \
+\ ALL m:I. F : (A Int f-``{m}) leadsTo \
\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
-\ ==> F : leadsTo A ((A - (f-``I)) Un B)";
+\ ==> F : A leadsTo ((A - (f-``I)) Un B)";
by (etac leadsTo_wf_induct 1);
by Safe_tac;
by (case_tac "m:I" 1);
@@ -362,26 +362,26 @@
qed "bounded_induct";
-(*Alternative proof is via the lemma F : leadsTo (A Int f-``(lessThan m)) B*)
-Goal "[| ALL m. F : leadsTo (A Int f-``{m}) \
+(*Alternative proof is via the lemma F : (A Int f-``(lessThan m)) leadsTo B*)
+Goal "[| ALL m. F : (A Int f-``{m}) leadsTo \
\ ((A Int f-``(lessThan m)) Un B) |] \
-\ ==> F : leadsTo A B";
+\ ==> F : A leadsTo B";
by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
by (Asm_simp_tac 1);
qed "lessThan_induct";
-Goal "[| ALL m:(greaterThan l). F : leadsTo (A Int f-``{m}) \
+Goal "[| ALL m:(greaterThan l). F : (A Int f-``{m}) leadsTo \
\ ((A Int f-``(lessThan m)) Un B) |] \
-\ ==> F : leadsTo A ((A Int (f-``(atMost l))) Un B)";
+\ ==> F : A leadsTo ((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 (Asm_simp_tac 1);
qed "lessThan_bounded_induct";
-Goal "[| ALL m:(lessThan l). F : leadsTo (A Int f-``{m}) \
+Goal "[| ALL m:(lessThan l). F : (A Int f-``{m}) leadsTo \
\ ((A Int f-``(greaterThan m)) Un B) |] \
-\ ==> F : leadsTo A ((A Int (f-``(atLeast l))) Un B)";
+\ ==> F : A leadsTo ((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 (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
@@ -396,16 +396,16 @@
(*** wlt ****)
(*Misra's property W3*)
-Goalw [wlt_def] "F : leadsTo (wlt F B) B";
+Goalw [wlt_def] "F : (wlt F B) leadsTo B";
by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
qed "wlt_leadsTo";
-Goalw [wlt_def] "F : leadsTo A B ==> A <= wlt F B";
+Goalw [wlt_def] "F : A leadsTo B ==> A <= wlt F B";
by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
qed "leadsTo_subset";
(*Misra's property W2*)
-Goal "F : leadsTo A B = (A <= wlt F B)";
+Goal "F : A leadsTo B = (A <= wlt F B)";
by (blast_tac (claset() addSIs [leadsTo_subset,
wlt_leadsTo RS leadsTo_weaken_L]) 1);
qed "leadsTo_eq_subset_wlt";
@@ -420,17 +420,17 @@
(*Used in the Trans case below*)
Goalw [constrains_def]
"[| B <= A2; \
-\ F : constrains (A1 - B) (A1 Un B); \
-\ F : constrains (A2 - C) (A2 Un C) |] \
-\ ==> F : constrains (A1 Un A2 - C) (A1 Un A2 Un C)";
+\ F : (A1 - B) co (A1 Un B); \
+\ F : (A2 - C) co (A2 Un C) |] \
+\ ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)";
by (Clarify_tac 1);
by (Blast_tac 1);
val lemma1 = result();
(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
-Goal "F : leadsTo A A' ==> \
-\ EX B. A<=B & F : leadsTo B A' & F : constrains (B-A') (B Un A')";
+Goal "F : A leadsTo A' ==> \
+\ EX B. A<=B & F : B leadsTo A' & F : (B-A') co (B Un A')";
by (etac leadsTo_induct 1);
(*Basis*)
by (blast_tac (claset() addIs [leadsTo_Basis]
@@ -449,7 +449,7 @@
(*Misra's property W5*)
-Goal "F : constrains (wlt F B - B) (wlt F B)";
+Goal "F : (wlt F B - B) co (wlt F B)";
by (cut_inst_tac [("F","F")] (wlt_leadsTo RS leadsTo_123) 1);
by (Clarify_tac 1);
by (subgoal_tac "Ba = wlt F B" 1);
@@ -461,29 +461,29 @@
(*** Completion: Binary and General Finite versions ***)
-Goal "[| F : leadsTo A A'; F : stable A'; \
-\ F : leadsTo B B'; F : stable B' |] \
-\ ==> F : leadsTo (A Int B) (A' Int B')";
+Goal "[| F : A leadsTo A'; F : stable A'; \
+\ F : B leadsTo B'; F : stable B' |] \
+\ ==> F : (A Int B) leadsTo (A' Int B')";
by (subgoal_tac "F : stable (wlt F B')" 1);
by (asm_full_simp_tac (simpset() addsimps [stable_def]) 2);
by (EVERY [etac (constrains_Un RS constrains_weaken) 2,
rtac wlt_constrains_wlt 2,
fast_tac (claset() addEs [wlt_increasing RSN (2,rev_subsetD)]) 3,
Blast_tac 2]);
-by (subgoal_tac "F : leadsTo (A Int wlt F B') (A' Int wlt F B')" 1);
+by (subgoal_tac "F : (A Int wlt F B') leadsTo (A' Int wlt F B')" 1);
by (blast_tac (claset() addIs [psp_stable]) 2);
-by (subgoal_tac "F : leadsTo (A' Int wlt F B') (A' Int B')" 1);
+by (subgoal_tac "F : (A' Int wlt F B') leadsTo (A' Int B')" 1);
by (blast_tac (claset() addIs [wlt_leadsTo, psp_stable2]) 2);
-by (subgoal_tac "F : leadsTo (A Int B) (A Int wlt F B')" 1);
+by (subgoal_tac "F : (A Int B) leadsTo (A Int wlt F B')" 1);
by (blast_tac (claset() addIs [leadsTo_subset RS subsetD,
subset_imp_leadsTo]) 2);
by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
qed "stable_completion";
-Goal "finite I ==> (ALL i:I. F : leadsTo (A i) (A' i)) --> \
+Goal "finite I ==> (ALL i:I. F : (A i) leadsTo (A' i)) --> \
\ (ALL i:I. F : stable (A' i)) --> \
-\ F : leadsTo (INT i:I. A i) (INT i:I. A' i)";
+\ F : (INT i:I. A i) leadsTo (INT i:I. A' i)";
by (etac finite_induct 1);
by (Asm_simp_tac 1);
by (asm_simp_tac
@@ -493,20 +493,20 @@
Goal "[| W = wlt F (B' Un C); \
-\ F : leadsTo A (A' Un C); F : constrains A' (A' Un C); \
-\ F : leadsTo B (B' Un C); F : constrains B' (B' Un C) |] \
-\ ==> F : leadsTo (A Int B) ((A' Int B') Un C)";
-by (subgoal_tac "F : constrains (W-C) (W Un B' Un C)" 1);
+\ 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 (subgoal_tac "F : (W-C) co (W Un B' Un C)" 1);
by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt]
MRS constrains_Un RS constrains_weaken]) 2);
-by (subgoal_tac "F : constrains (W-C) W" 1);
+by (subgoal_tac "F : (W-C) co W" 1);
by (asm_full_simp_tac
(simpset() addsimps [wlt_increasing, Un_assoc, Un_absorb2]) 2);
-by (subgoal_tac "F : leadsTo (A Int W - C) (A' Int W Un C)" 1);
+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);
(** LEVEL 7 **)
-by (subgoal_tac "F : leadsTo (A' Int W Un C) (A' Int B' Un C)" 1);
+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,
@@ -520,9 +520,9 @@
bind_thm("completion", refl RS result());
-Goal "finite I ==> (ALL i:I. F : leadsTo (A i) (A' i Un C)) --> \
-\ (ALL i:I. F : constrains (A' i) (A' i Un C)) --> \
-\ F : leadsTo (INT i:I. A i) ((INT i:I. A' i) Un C)";
+Goal "finite I ==> (ALL i:I. F : (A i) leadsTo (A' i Un C)) --> \
+\ (ALL i:I. F : (A' i) co (A' i Un C)) --> \
+\ F : (INT i:I. A i) leadsTo ((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 Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/WFair.thy Thu Apr 29 10:51:58 1999 +0200
@@ -17,16 +17,22 @@
transient :: "'a set => 'a program set"
"transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= -A}"
- ensures :: "['a set, 'a set] => 'a program set"
- "ensures A B == constrains (A-B) (A Un B) Int transient (A-B)"
+
+consts
+
+ ensures :: "['a set, 'a set] => 'a program set" (infixl 60)
+ (*LEADS-TO constant for the inductive definition*)
+ leadsto :: "'a program => ('a set * 'a set) set"
-consts leadsto :: "'a program => ('a set * 'a set) set"
+ (*visible version of the LEADS-TO relation*)
+ leadsTo :: "['a set, 'a set] => 'a program set" (infixl 60)
+
inductive "leadsto F"
intrs
- Basis "F : ensures A B ==> (A,B) : leadsto F"
+ Basis "F : A ensures B ==> (A,B) : leadsto F"
Trans "[| (A,B) : leadsto F; (B,C) : leadsto F |]
==> (A,C) : leadsto F"
@@ -40,12 +46,15 @@
-constdefs (*visible version of the relation*)
- leadsTo :: "['a set, 'a set] => 'a program set"
- "leadsTo A B == {F. (A,B) : leadsto F}"
+defs
+ ensures_def "A ensures B == (A-B co A Un B) Int transient (A-B)"
+
+ leadsTo_def "A leadsTo B == {F. (A,B) : leadsto F}"
+
+constdefs
(*wlt F B is the largest set that leads to B*)
wlt :: "['a program, 'a set] => 'a set"
- "wlt F B == Union {A. F: leadsTo A B}"
+ "wlt F B == Union {A. F: A leadsTo B}"
end