--- a/src/HOL/UNITY/Common.ML Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/Common.ML Wed Oct 07 10:32:00 1998 +0200
@@ -11,8 +11,8 @@
*)
(*Misra's property CMT4: t exceeds no common meeting time*)
-Goal "[| ALL m. Constrains prg {m} (maxfg m); n: common |] \
-\ ==> Stable prg (atMost n)";
+Goal "[| ALL m. Constrains F {m} (maxfg m); n: common |] \
+\ ==> Stable F (atMost n)";
by (dres_inst_tac [("M", "{t. t<=n}")] Elimination_sing 1);
by (asm_full_simp_tac
(simpset() addsimps [atMost_def, Stable_def, common_def, maxfg_def,
@@ -21,9 +21,9 @@
by (blast_tac (claset() addIs [order_eq_refl, fmono, gmono, le_trans]) 1);
qed "common_stable";
-Goal "[| Init prg <= atMost n; \
-\ ALL m. Constrains prg {m} (maxfg m); n: common |] \
-\ ==> Invariant prg (atMost n)";
+Goal "[| Init F <= atMost n; \
+\ ALL m. Constrains F {m} (maxfg m); n: common |] \
+\ ==> Invariant F (atMost n)";
by (asm_simp_tac (simpset() addsimps [InvariantI, common_stable]) 1);
qed "common_Invariant";
@@ -67,10 +67,10 @@
Addsimps [atMost_Int_atLeast];
-Goal "[| ALL m. Constrains prg {m} (maxfg m); \
-\ ALL m: lessThan n. LeadsTo prg {m} (greaterThan m); \
+Goal "[| ALL m. Constrains F {m} (maxfg m); \
+\ ALL m: lessThan n. LeadsTo F {m} (greaterThan m); \
\ n: common |] \
-\ ==> LeadsTo prg (atMost n) common";
+\ ==> LeadsTo F (atMost n) 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);
@@ -80,10 +80,10 @@
val lemma = result();
(*The "ALL m: -common" form echoes CMT6.*)
-Goal "[| ALL m. Constrains prg {m} (maxfg m); \
-\ ALL m: -common. LeadsTo prg {m} (greaterThan m); \
+Goal "[| ALL m. Constrains F {m} (maxfg m); \
+\ ALL m: -common. LeadsTo F {m} (greaterThan m); \
\ n: common |] \
-\ ==> LeadsTo prg (atMost (LEAST n. n: common)) common";
+\ ==> LeadsTo F (atMost (LEAST n. n: common)) common";
by (rtac lemma 1);
by (ALLGOALS Asm_simp_tac);
by (etac LeastI 2);
--- a/src/HOL/UNITY/Comp.ML Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/Comp.ML Wed Oct 07 10:32:00 1998 +0200
@@ -32,15 +32,15 @@
Goalw [component_def,Join_def] "component F G ==> Acts F <= Acts G";
by Auto_tac;
-qed "componet_Acts";
+qed "component_Acts";
Goalw [component_def,Join_def] "component F G ==> Init G <= Init F";
by Auto_tac;
-qed "componet_Init";
+qed "component_Init";
Goal "[| component F G; component G F |] ==> F=G";
by (asm_simp_tac (simpset() addsimps [program_equalityI, equalityI,
- componet_Acts, componet_Init]) 1);
+ component_Acts, component_Init]) 1);
qed "component_anti_sym";
--- a/src/HOL/UNITY/Constrains.ML Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/Constrains.ML Wed Oct 07 10:32:00 1998 +0200
@@ -13,61 +13,61 @@
Blast.overloaded ("Constrains.Constrains",
HOLogic.dest_setT o domain_type o range_type);
-(*constrains (Acts prg) B B'
- ==> constrains (Acts prg) (reachable prg Int B) (reachable prg Int B')*)
+(*constrains (Acts F) B B'
+ ==> constrains (Acts F) (reachable F Int B) (reachable F Int B')*)
bind_thm ("constrains_reachable_Int",
subset_refl RS
rewrite_rule [stable_def] stable_reachable RS
constrains_Int);
Goalw [Constrains_def]
- "constrains (Acts prg) A A' ==> Constrains prg A A'";
+ "constrains (Acts F) A A' ==> Constrains F A A'";
by (etac constrains_reachable_Int 1);
qed "constrains_imp_Constrains";
val prems = Goal
- "(!!act s s'. [| act: Acts prg; (s,s') : act; s: A |] ==> s': A') \
-\ ==> Constrains prg A A'";
+ "(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A') \
+\ ==> Constrains F A A'";
by (rtac constrains_imp_Constrains 1);
by (blast_tac (claset() addIs (constrainsI::prems)) 1);
qed "ConstrainsI";
-Goalw [Constrains_def, constrains_def] "Constrains prg {} B";
+Goalw [Constrains_def, constrains_def] "Constrains F {} B";
by (Blast_tac 1);
qed "Constrains_empty";
-Goal "Constrains prg A UNIV";
+Goal "Constrains F A UNIV";
by (blast_tac (claset() addIs [ConstrainsI]) 1);
qed "Constrains_UNIV";
AddIffs [Constrains_empty, Constrains_UNIV];
Goalw [Constrains_def]
- "[| Constrains prg A A'; A'<=B' |] ==> Constrains prg A B'";
+ "[| Constrains F A A'; A'<=B' |] ==> Constrains F A B'";
by (blast_tac (claset() addIs [constrains_weaken_R]) 1);
qed "Constrains_weaken_R";
Goalw [Constrains_def]
- "[| Constrains prg A A'; B<=A |] ==> Constrains prg B A'";
+ "[| Constrains F A A'; B<=A |] ==> Constrains F B A'";
by (blast_tac (claset() addIs [constrains_weaken_L]) 1);
qed "Constrains_weaken_L";
Goalw [Constrains_def]
- "[| Constrains prg A A'; B<=A; A'<=B' |] ==> Constrains prg B B'";
+ "[| Constrains F A A'; B<=A; A'<=B' |] ==> Constrains F B B'";
by (blast_tac (claset() addIs [constrains_weaken]) 1);
qed "Constrains_weaken";
(** Union **)
Goalw [Constrains_def]
- "[| Constrains prg A A'; Constrains prg B B' |] \
-\ ==> Constrains prg (A Un B) (A' Un B')";
+ "[| Constrains F A A'; Constrains F B B' |] \
+\ ==> Constrains F (A Un B) (A' Un B')";
by (blast_tac (claset() addIs [constrains_Un RS constrains_weaken]) 1);
qed "Constrains_Un";
Goalw [Constrains_def]
- "ALL i:I. Constrains prg (A i) (A' i) \
-\ ==> Constrains prg (UN i:I. A i) (UN i:I. A' i)";
+ "ALL i:I. Constrains F (A i) (A' i) \
+\ ==> Constrains F (UN i:I. A i) (UN i:I. A' i)";
by (dtac ball_constrains_UN 1);
by (blast_tac (claset() addIs [constrains_weaken]) 1);
qed "ball_Constrains_UN";
@@ -75,75 +75,75 @@
(** Intersection **)
Goalw [Constrains_def]
- "[| Constrains prg A A'; Constrains prg B B' |] \
-\ ==> Constrains prg (A Int B) (A' Int B')";
+ "[| Constrains F A A'; Constrains F B B' |] \
+\ ==> Constrains F (A Int B) (A' Int B')";
by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1);
qed "Constrains_Int";
Goalw [Constrains_def]
- "[| ALL i:I. Constrains prg (A i) (A' i) |] \
-\ ==> Constrains prg (INT i:I. A i) (INT i:I. A' i)";
+ "[| ALL i:I. Constrains F (A i) (A' i) |] \
+\ ==> Constrains F (INT i:I. A i) (INT i:I. A' i)";
by (dtac ball_constrains_INT 1);
by (dtac constrains_reachable_Int 1);
by (blast_tac (claset() addIs [constrains_weaken]) 1);
qed "ball_Constrains_INT";
Goalw [Constrains_def]
- "Constrains prg A A' ==> reachable prg Int A <= A'";
+ "Constrains F A A' ==> reachable F Int A <= A'";
by (dtac constrains_imp_subset 1);
by (ALLGOALS
(full_simp_tac (simpset() addsimps [Int_subset_iff, Int_lower1])));
qed "Constrains_imp_subset";
Goalw [Constrains_def]
- "[| Constrains prg A B; Constrains prg B C |] \
-\ ==> Constrains prg A C";
+ "[| Constrains F A B; Constrains F B C |] \
+\ ==> Constrains F A C";
by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
qed "Constrains_trans";
(*** Stable ***)
-Goal "Stable prg A = stable (Acts prg) (reachable prg Int A)";
+Goal "Stable F A = stable (Acts F) (reachable F Int A)";
by (simp_tac (simpset() addsimps [Stable_def, Constrains_def, stable_def]) 1);
qed "Stable_eq_stable";
-Goalw [Stable_def] "Constrains prg A A ==> Stable prg A";
+Goalw [Stable_def] "Constrains F A A ==> Stable F A";
by (assume_tac 1);
qed "StableI";
-Goalw [Stable_def] "Stable prg A ==> Constrains prg A A";
+Goalw [Stable_def] "Stable F A ==> Constrains F A A";
by (assume_tac 1);
qed "StableD";
Goalw [Stable_def]
- "[| Stable prg A; Stable prg A' |] ==> Stable prg (A Un A')";
+ "[| Stable F A; Stable F A' |] ==> Stable F (A Un A')";
by (blast_tac (claset() addIs [Constrains_Un]) 1);
qed "Stable_Un";
Goalw [Stable_def]
- "[| Stable prg A; Stable prg A' |] ==> Stable prg (A Int A')";
+ "[| Stable F A; Stable F A' |] ==> Stable F (A Int A')";
by (blast_tac (claset() addIs [Constrains_Int]) 1);
qed "Stable_Int";
Goalw [Stable_def]
- "[| Stable prg C; Constrains prg A (C Un A') |] \
-\ ==> Constrains prg (C Un A) (C Un A')";
+ "[| Stable F C; Constrains F A (C Un A') |] \
+\ ==> Constrains F (C Un A) (C Un A')";
by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken]) 1);
qed "Stable_Constrains_Un";
Goalw [Stable_def]
- "[| Stable prg C; Constrains prg (C Int A) A' |] \
-\ ==> Constrains prg (C Int A) (C Int A')";
+ "[| Stable F C; Constrains F (C Int A) A' |] \
+\ ==> Constrains F (C Int A) (C Int A')";
by (blast_tac (claset() addIs [Constrains_Int RS Constrains_weaken]) 1);
qed "Stable_Constrains_Int";
Goalw [Stable_def]
- "(ALL i:I. Stable prg (A i)) ==> Stable prg (INT i:I. A i)";
+ "(ALL i:I. Stable F (A i)) ==> Stable F (INT i:I. A i)";
by (etac ball_Constrains_INT 1);
qed "ball_Stable_INT";
-Goal "Stable prg (reachable prg)";
+Goal "Stable F (reachable F)";
by (simp_tac (simpset() addsimps [Stable_eq_stable, stable_reachable]) 1);
qed "Stable_reachable";
@@ -154,34 +154,34 @@
in forward proof. ***)
Goalw [Constrains_def, constrains_def]
- "[| ALL m. Constrains prg {s. s x = m} (B m) |] \
-\ ==> Constrains prg {s. s x : M} (UN m:M. B m)";
+ "[| ALL m. Constrains F {s. s x = m} (B m) |] \
+\ ==> Constrains F {s. s x : M} (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. Constrains prg {m} (B m)) ==> Constrains prg M (UN m:M. B m)";
+ "(ALL m. Constrains F {m} (B m)) ==> Constrains F M (UN m:M. B m)";
by (Blast_tac 1);
qed "Elimination_sing";
Goalw [Constrains_def, constrains_def]
- "[| Constrains prg A (A' Un B); Constrains prg B B' |] \
-\ ==> Constrains prg A (A' Un B')";
+ "[| Constrains F A (A' Un B); Constrains F B B' |] \
+\ ==> Constrains F A (A' Un B')";
by (Blast_tac 1);
qed "Constrains_cancel";
(*** Specialized laws for handling Invariants ***)
-(** Natural deduction rules for "Invariant prg A" **)
+(** Natural deduction rules for "Invariant F A" **)
-Goal "[| Init prg<=A; Stable prg A |] ==> Invariant prg A";
+Goal "[| Init F<=A; Stable F A |] ==> Invariant F A";
by (asm_simp_tac (simpset() addsimps [Invariant_def]) 1);
qed "InvariantI";
-Goal "Invariant prg A ==> Init prg<=A & Stable prg A";
+Goal "Invariant F A ==> Init F<=A & Stable F A";
by (asm_full_simp_tac (simpset() addsimps [Invariant_def]) 1);
qed "InvariantD";
@@ -189,13 +189,13 @@
(*The set of all reachable states is an Invariant...*)
-Goal "Invariant prg (reachable prg)";
+Goal "Invariant F (reachable F)";
by (simp_tac (simpset() addsimps [Invariant_def]) 1);
by (blast_tac (claset() addIs (Stable_reachable::reachable.intrs)) 1);
qed "Invariant_reachable";
(*...in fact the strongest Invariant!*)
-Goal "Invariant prg A ==> reachable prg <= A";
+Goal "Invariant F A ==> reachable F <= A";
by (full_simp_tac
(simpset() addsimps [Stable_def, Constrains_def, constrains_def,
Invariant_def]) 1);
@@ -205,24 +205,24 @@
qed "Invariant_includes_reachable";
-Goal "Invariant prg INV ==> reachable prg Int INV = reachable prg";
+Goal "Invariant F INV ==> reachable F Int INV = reachable F";
by (dtac Invariant_includes_reachable 1);
by (Blast_tac 1);
qed "reachable_Int_INV";
-Goal "[| Invariant prg INV; Constrains prg (INV Int A) A' |] \
-\ ==> Constrains prg A A'";
+Goal "[| Invariant F INV; Constrains F (INV Int A) A' |] \
+\ ==> Constrains F A A'";
by (asm_full_simp_tac
(simpset() addsimps [Constrains_def, reachable_Int_INV,
Int_assoc RS sym]) 1);
qed "Invariant_ConstrainsI";
-(* [| Invariant prg INV; Constrains prg (INV Int A) A |]
- ==> Stable prg A *)
+(* [| Invariant F INV; Constrains F (INV Int A) A |]
+ ==> Stable F A *)
bind_thm ("Invariant_StableI", Invariant_ConstrainsI RS StableI);
-Goal "[| Invariant prg INV; Constrains prg A A' |] \
-\ ==> Constrains prg A (INV Int A')";
+Goal "[| Invariant F INV; Constrains F A A' |] \
+\ ==> Constrains F A (INV Int A')";
by (asm_full_simp_tac
(simpset() addsimps [Constrains_def, reachable_Int_INV,
Int_assoc RS sym]) 1);
@@ -234,7 +234,7 @@
(** Conjoining Invariants **)
-Goal "[| Invariant prg A; Invariant prg B |] ==> Invariant prg (A Int B)";
+Goal "[| Invariant F A; Invariant F B |] ==> Invariant F (A Int B)";
by (auto_tac (claset(),
simpset() addsimps [Invariant_def, Stable_Int]));
qed "Invariant_Int";
@@ -261,7 +261,7 @@
constrains_imp_Constrains] 1),
rtac constrainsI 1,
Full_simp_tac 1,
- REPEAT_FIRST (etac disjE),
+ REPEAT (FIRSTGOAL (etac disjE)),
ALLGOALS Clarify_tac,
ALLGOALS Asm_full_simp_tac]);
--- a/src/HOL/UNITY/Constrains.thy Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/Constrains.thy Wed Oct 07 10:32:00 1998 +0200
@@ -11,18 +11,18 @@
constdefs
Constrains :: "['a program, 'a set, 'a set] => bool"
- "Constrains prg A B ==
- constrains (Acts prg)
- (reachable prg Int A)
- (reachable prg Int B)"
+ "Constrains F A B ==
+ constrains (Acts F)
+ (reachable F Int A)
+ (reachable F Int B)"
Stable :: "'a program => 'a set => bool"
- "Stable prg A == Constrains prg A A"
+ "Stable F A == Constrains F A A"
Unless :: "['a program, 'a set, 'a set] => bool"
- "Unless prg A B == Constrains prg (A-B) (A Un B)"
+ "Unless F A B == Constrains F (A-B) (A Un B)"
Invariant :: "['a program, 'a set] => bool"
- "Invariant prg A == (Init prg) <= A & Stable prg A"
+ "Invariant F A == (Init F) <= A & Stable F A"
end
--- a/src/HOL/UNITY/Mutex.ML Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/Mutex.ML Wed Oct 07 10:32:00 1998 +0200
@@ -71,7 +71,7 @@
by (exhaust_tac "na" 1);
by (exhaust_tac "nat" 2);
by (exhaust_tac "n" 3);
-auto();
+by Auto_tac;
qed "eq_123";
--- a/src/HOL/UNITY/ROOT.ML Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/ROOT.ML Wed Oct 07 10:32:00 1998 +0200
@@ -21,6 +21,12 @@
time_use_thy "Reach";
time_use_thy "Handshake";
time_use_thy "Lift";
+time_use_thy "Comp";
-loadpath := "../Auth" :: !loadpath; (*necessary to find the Auth theories*)
+loadpath := "../Auth" :: !loadpath; (*to find Public.thy*)
use_thy"NSP_Bad";
+
+(*
+loadpath := "../Lex" :: !loadpath; (*to find Prefix.thy*)
+use_thy"Client";
+*)
--- a/src/HOL/UNITY/SubstAx.ML Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML Wed Oct 07 10:32:00 1998 +0200
@@ -15,14 +15,14 @@
(** Conjoining a safety property **)
-Goal "[| reachable prg <= C; LeadsTo prg (C Int A) A' |] \
-\ ==> LeadsTo prg A A'";
+Goal "[| reachable F <= C; LeadsTo F (C Int A) A' |] \
+\ ==> LeadsTo F A A'";
by (asm_full_simp_tac
(simpset() addsimps [LeadsTo_def, Int_absorb2, Int_assoc RS sym]) 1);
qed "reachable_LeadsToI";
-Goal "[| reachable prg <= C; LeadsTo prg A A' |] \
-\ ==> LeadsTo prg A (C Int A')";
+Goal "[| reachable F <= C; LeadsTo F A A' |] \
+\ ==> LeadsTo F A (C Int A')";
by (asm_full_simp_tac
(simpset() addsimps [LeadsTo_def, Int_absorb2,
Int_assoc RS sym]) 1);
@@ -31,11 +31,11 @@
(** Conjoining an invariant **)
-(* [| Invariant prg C; LeadsTo prg (C Int A) A' |] ==> LeadsTo prg A A' *)
+(* [| Invariant F C; LeadsTo F (C Int A) A' |] ==> LeadsTo F A A' *)
bind_thm ("Invariant_LeadsToI",
Invariant_includes_reachable RS reachable_LeadsToI);
-(* [| Invariant prg C; LeadsTo prg A A' |] ==> LeadsTo prg A (C Int A') *)
+(* [| Invariant F C; LeadsTo F A A' |] ==> LeadsTo F A (C Int A') *)
bind_thm ("Invariant_LeadsToD",
Invariant_includes_reachable RS reachable_LeadsToD);
@@ -44,18 +44,18 @@
(*** Introduction rules: Basis, Trans, Union ***)
-Goal "leadsTo (Acts prg) A B ==> LeadsTo prg A B";
+Goal "leadsTo (Acts F) A B ==> LeadsTo F A B";
by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [psp_stable2, stable_reachable]) 1);
qed "leadsTo_imp_LeadsTo";
-Goal "[| LeadsTo prg A B; LeadsTo prg B C |] ==> LeadsTo prg A C";
+Goal "[| LeadsTo F A B; LeadsTo F B C |] ==> LeadsTo F A C";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
qed "LeadsTo_Trans";
val [prem] = Goalw [LeadsTo_def]
- "(!!A. A : S ==> LeadsTo prg A B) ==> LeadsTo prg (Union S) B";
+ "(!!A. A : S ==> LeadsTo F A B) ==> LeadsTo F (Union S) B";
by (Simp_tac 1);
by (stac Int_Union 1);
by (blast_tac (claset() addIs [leadsTo_UN,
@@ -65,34 +65,34 @@
(*** Derived rules ***)
-Goal "LeadsTo prg A UNIV";
+Goal "LeadsTo F A 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 "LeadsTo prg A (A' Un A') ==> LeadsTo prg A A'";
+Goal "LeadsTo F A (A' Un A') ==> LeadsTo F A A'";
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
qed "LeadsTo_Un_duplicate";
-Goal "LeadsTo prg A (A' Un C Un C) ==> LeadsTo prg A (A' Un C)";
+Goal "LeadsTo F A (A' Un C Un C) ==> LeadsTo F A (A' Un C)";
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
qed "LeadsTo_Un_duplicate2";
val prems =
-Goal "(!!i. i : I ==> LeadsTo prg (A i) B) ==> LeadsTo prg (UN i:I. A i) B";
+Goal "(!!i. i : I ==> LeadsTo F (A i) B) ==> LeadsTo F (UN i:I. A i) B";
by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
by (blast_tac (claset() addIs (LeadsTo_Union::prems)) 1);
qed "LeadsTo_UN";
(*Binary union introduction rule*)
-Goal "[| LeadsTo prg A C; LeadsTo prg B C |] ==> LeadsTo prg (A Un B) C";
+Goal "[| LeadsTo F A C; LeadsTo F B C |] ==> LeadsTo F (A Un B) C";
by (stac Un_eq_Union 1);
by (blast_tac (claset() addIs [LeadsTo_Union]) 1);
qed "LeadsTo_Un";
-Goal "[| A <= B |] ==> LeadsTo prg A B";
+Goal "[| A <= B |] ==> LeadsTo F A B";
by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
qed "subset_imp_LeadsTo";
@@ -100,39 +100,39 @@
bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo);
Addsimps [empty_LeadsTo];
-Goal "[| LeadsTo prg A A'; A' <= B' |] ==> LeadsTo prg A B'";
+Goal "[| LeadsTo F A A'; A' <= B' |] ==> LeadsTo F A 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 "[| LeadsTo prg A A'; B <= A |] \
-\ ==> LeadsTo prg B A'";
+Goal "[| LeadsTo F A A'; B <= A |] \
+\ ==> LeadsTo F B 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 "[| LeadsTo prg A A'; \
+Goal "[| LeadsTo F A A'; \
\ B <= A; A' <= B' |] \
-\ ==> LeadsTo prg B B'";
+\ ==> LeadsTo F B B'";
by (blast_tac (claset() addIs [LeadsTo_weaken_R, LeadsTo_weaken_L,
LeadsTo_Trans]) 1);
qed "LeadsTo_weaken";
-Goal "[| reachable prg <= C; LeadsTo prg A A'; \
+Goal "[| reachable F <= C; LeadsTo F A A'; \
\ C Int B <= A; C Int A' <= B' |] \
-\ ==> LeadsTo prg B B'";
+\ ==> LeadsTo F B 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 "[| LeadsTo prg A B |] ==> LeadsTo prg (A Un B) B";
+Goal "[| LeadsTo F A B |] ==> LeadsTo F (A Un B) B";
by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo]) 1);
qed "LeadsTo_Un_post";
-Goal "[| LeadsTo prg A B; LeadsTo prg B C |] \
-\ ==> LeadsTo prg (A Un B) C";
+Goal "[| LeadsTo F A B; LeadsTo F B C |] \
+\ ==> LeadsTo F (A Un B) C";
by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo,
LeadsTo_weaken_L, LeadsTo_Trans]) 1);
qed "LeadsTo_Trans_Un";
@@ -140,33 +140,33 @@
(** Distributive laws **)
-Goal "LeadsTo prg (A Un B) C = (LeadsTo prg A C & LeadsTo prg B C)";
+Goal "LeadsTo F (A Un B) C = (LeadsTo F A C & LeadsTo F B C)";
by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
qed "LeadsTo_Un_distrib";
-Goal "LeadsTo prg (UN i:I. A i) B = (ALL i : I. LeadsTo prg (A i) B)";
+Goal "LeadsTo F (UN i:I. A i) B = (ALL i : I. LeadsTo F (A i) B)";
by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
qed "LeadsTo_UN_distrib";
-Goal "LeadsTo prg (Union S) B = (ALL A : S. LeadsTo prg A B)";
+Goal "LeadsTo F (Union S) B = (ALL A : S. LeadsTo F A B)";
by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1);
qed "LeadsTo_Union_distrib";
-(** More rules using the premise "Invariant prg" **)
+(** More rules using the premise "Invariant F" **)
Goalw [LeadsTo_def, Constrains_def]
- "[| Constrains prg (A-A') (A Un A'); transient (Acts prg) (A-A') |] \
-\ ==> LeadsTo prg A A'";
+ "[| Constrains F (A-A') (A Un A'); transient (Acts F) (A-A') |] \
+\ ==> LeadsTo F A A'";
by (rtac (ensuresI RS leadsTo_Basis) 1);
by (blast_tac (claset() addIs [transient_strengthen]) 2);
by (blast_tac (claset() addIs [constrains_weaken]) 1);
qed "LeadsTo_Basis";
-Goal "[| Invariant prg INV; \
-\ Constrains prg (INV Int (A-A')) (A Un A'); \
-\ transient (Acts prg) (INV Int (A-A')) |] \
-\ ==> LeadsTo prg A A'";
+Goal "[| Invariant F INV; \
+\ Constrains F (INV Int (A-A')) (A Un A'); \
+\ transient (Acts F) (INV Int (A-A')) |] \
+\ ==> LeadsTo F A A'";
by (rtac Invariant_LeadsToI 1);
by (assume_tac 1);
by (rtac LeadsTo_Basis 1);
@@ -174,10 +174,10 @@
by (blast_tac (claset() addIs [Invariant_ConstrainsD RS Constrains_weaken]) 1);
qed "Invariant_LeadsTo_Basis";
-Goal "[| Invariant prg INV; \
-\ LeadsTo prg A A'; \
+Goal "[| Invariant F INV; \
+\ LeadsTo F A A'; \
\ INV Int B <= A; INV Int A' <= B' |] \
-\ ==> LeadsTo prg B B'";
+\ ==> LeadsTo F B B'";
by (rtac Invariant_LeadsToI 1);
by (assume_tac 1);
by (dtac Invariant_LeadsToD 1);
@@ -188,8 +188,8 @@
(*Set difference: maybe combine with leadsTo_weaken_L??
This is the most useful form of the "disjunction" rule*)
-Goal "[| LeadsTo prg (A-B) C; LeadsTo prg (A Int B) C |] \
-\ ==> LeadsTo prg A C";
+Goal "[| LeadsTo F (A-B) C; LeadsTo F (A Int B) C |] \
+\ ==> LeadsTo F A C";
by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
qed "LeadsTo_Diff";
@@ -197,8 +197,8 @@
val prems =
-Goal "(!! i. i:I ==> LeadsTo prg (A i) (A' i)) \
-\ ==> LeadsTo prg (UN i:I. A i) (UN i:I. A' i)";
+Goal "(!! i. i:I ==> LeadsTo F (A i) (A' i)) \
+\ ==> LeadsTo F (UN i:I. A i) (UN i:I. A' i)";
by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_R]
addIs prems) 1);
@@ -207,22 +207,22 @@
(*Version with no index set*)
val prems =
-Goal "(!! i. LeadsTo prg (A i) (A' i)) \
-\ ==> LeadsTo prg (UN i. A i) (UN i. A' i)";
+Goal "(!! i. LeadsTo F (A i) (A' i)) \
+\ ==> LeadsTo F (UN i. A i) (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. LeadsTo prg (A i) (A' i) \
-\ ==> LeadsTo prg (UN i. A i) (UN i. A' i)";
+Goal "ALL i. LeadsTo F (A i) (A' i) \
+\ ==> LeadsTo F (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 prg A A'; LeadsTo prg B B' |] \
-\ ==> LeadsTo prg (A Un B) (A' Un B')";
+Goal "[| LeadsTo F A A'; LeadsTo F B B' |] \
+\ ==> LeadsTo F (A Un B) (A' Un B')";
by (blast_tac (claset() addIs [LeadsTo_Un,
LeadsTo_weaken_R]) 1);
qed "LeadsTo_Un_Un";
@@ -230,27 +230,27 @@
(** The cancellation law **)
-Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg B B' |] \
-\ ==> LeadsTo prg A (A' Un B')";
+Goal "[| LeadsTo F A (A' Un B); LeadsTo F B B' |] \
+\ ==> LeadsTo F A (A' Un B')";
by (blast_tac (claset() addIs [LeadsTo_Un_Un,
subset_imp_LeadsTo, LeadsTo_Trans]) 1);
qed "LeadsTo_cancel2";
-Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg (B-A') B' |] \
-\ ==> LeadsTo prg A (A' Un B')";
+Goal "[| LeadsTo F A (A' Un B); LeadsTo F (B-A') B' |] \
+\ ==> LeadsTo F A (A' Un B')";
by (rtac LeadsTo_cancel2 1);
by (assume_tac 2);
by (ALLGOALS Asm_simp_tac);
qed "LeadsTo_cancel_Diff2";
-Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg B B' |] \
-\ ==> LeadsTo prg A (B' Un A')";
+Goal "[| LeadsTo F A (B Un A'); LeadsTo F B B' |] \
+\ ==> LeadsTo F 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 prg A (B Un A'); LeadsTo prg (B-A') B' |] \
-\ ==> LeadsTo prg A (B' Un A')";
+Goal "[| LeadsTo F A (B Un A'); LeadsTo F (B-A') B' |] \
+\ ==> LeadsTo F A (B' Un A')";
by (rtac LeadsTo_cancel1 1);
by (assume_tac 2);
by (ALLGOALS Asm_simp_tac);
@@ -261,7 +261,7 @@
(** The impossibility law **)
(*The set "A" may be non-empty, but it contains no reachable states*)
-Goal "LeadsTo prg A {} ==> reachable prg Int A = {}";
+Goal "LeadsTo F A {} ==> reachable F Int A = {}";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (etac leadsTo_empty 1);
qed "LeadsTo_empty";
@@ -271,32 +271,32 @@
(*Special case of PSP: Misra's "stable conjunction". Doesn't need id:Acts. *)
Goal
- "[| LeadsTo prg A A'; Stable prg B |] ==> LeadsTo prg (A Int B) (A' Int B)";
+ "[| LeadsTo F A A'; Stable F B |] ==> LeadsTo F (A Int B) (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 "[| LeadsTo prg A A'; Stable prg B |] \
-\ ==> LeadsTo prg (B Int A) (B Int A')";
+Goal "[| LeadsTo F A A'; Stable F B |] \
+\ ==> LeadsTo F (B Int A) (B Int A')";
by (asm_simp_tac (simpset() addsimps PSP_stable::Int_ac) 1);
qed "PSP_stable2";
Goalw [LeadsTo_def, Constrains_def]
- "[| LeadsTo prg A A'; Constrains prg B B' |] \
-\ ==> LeadsTo prg (A Int B) ((A' Int B) Un (B' - B))";
+ "[| LeadsTo F A A'; Constrains F B B' |] \
+\ ==> LeadsTo F (A Int B) ((A' Int B) Un (B' - B))";
by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1);
qed "PSP";
-Goal "[| LeadsTo prg A A'; Constrains prg B B' |] \
-\ ==> LeadsTo prg (B Int A) ((B Int A') Un (B' - B))";
+Goal "[| LeadsTo F A A'; Constrains F B B' |] \
+\ ==> LeadsTo F (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 prg A A'; Unless prg B B' |] \
-\ ==> LeadsTo prg (A Int B) ((A' Int B) Un B')";
+ "[| LeadsTo F A A'; Unless F B B' |] \
+\ ==> LeadsTo F (A Int B) ((A' Int B) Un B')";
by (dtac PSP 1);
by (assume_tac 1);
by (blast_tac (claset() addIs [LeadsTo_Diff, LeadsTo_weaken,
@@ -308,9 +308,9 @@
(** Meta or object quantifier ????? **)
Goal "[| wf r; \
-\ ALL m. LeadsTo prg (A Int f-``{m}) \
+\ ALL m. LeadsTo F (A Int f-``{m}) \
\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
-\ ==> LeadsTo prg A B";
+\ ==> LeadsTo F A B";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (etac leadsTo_wf_induct 1);
by (Simp_tac 2);
@@ -319,9 +319,9 @@
Goal "[| wf r; \
-\ ALL m:I. LeadsTo prg (A Int f-``{m}) \
+\ ALL m:I. LeadsTo F (A Int f-``{m}) \
\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
-\ ==> LeadsTo prg A ((A - (f-``I)) Un B)";
+\ ==> LeadsTo F A ((A - (f-``I)) Un B)";
by (etac LeadsTo_wf_induct 1);
by Safe_tac;
by (case_tac "m:I" 1);
@@ -330,36 +330,36 @@
qed "Bounded_induct";
-Goal "[| ALL m. LeadsTo prg (A Int f-``{m}) \
+Goal "[| ALL m. LeadsTo F (A Int f-``{m}) \
\ ((A Int f-``(lessThan m)) Un B) |] \
-\ ==> LeadsTo prg A B";
+\ ==> LeadsTo F A B";
by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
by (Asm_simp_tac 1);
qed "LessThan_induct";
(*Integer version. Could generalize from #0 to any lower bound*)
val [reach, prem] =
-Goal "[| reachable prg <= {s. #0 <= f s}; \
-\ !! z. LeadsTo prg (A Int {s. f s = z}) \
+Goal "[| reachable F <= {s. #0 <= f s}; \
+\ !! z. LeadsTo F (A Int {s. f s = z}) \
\ ((A Int {s. f s < z}) Un B) |] \
-\ ==> LeadsTo prg A B";
+\ ==> LeadsTo F A B";
by (res_inst_tac [("f", "nat o f")] (allI RS LessThan_induct) 1);
by (simp_tac (simpset() addsimps [vimage_def]) 1);
-br ([reach, prem] MRS reachable_LeadsTo_weaken) 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). LeadsTo prg (A Int f-``{m}) \
+Goal "[| ALL m:(greaterThan l). LeadsTo F (A Int f-``{m}) \
\ ((A Int f-``(lessThan m)) Un B) |] \
-\ ==> LeadsTo prg A ((A Int (f-``(atMost l))) Un B)";
+\ ==> LeadsTo F 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 (Asm_simp_tac 1);
qed "LessThan_bounded_induct";
-Goal "[| ALL m:(lessThan l). LeadsTo prg (A Int f-``{m}) \
+Goal "[| ALL m:(lessThan l). LeadsTo F (A Int f-``{m}) \
\ ((A Int f-``(greaterThan m)) Un B) |] \
-\ ==> LeadsTo prg A ((A Int (f-``(atLeast l))) Un B)";
+\ ==> LeadsTo F 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 (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
@@ -372,27 +372,27 @@
(*** Completion: Binary and General Finite versions ***)
-Goal "[| LeadsTo prg A A'; Stable prg A'; \
-\ LeadsTo prg B B'; Stable prg B' |] \
-\ ==> LeadsTo prg (A Int B) (A' Int B')";
+Goal "[| LeadsTo F A A'; Stable F A'; \
+\ LeadsTo F B B'; Stable F B' |] \
+\ ==> LeadsTo F (A Int B) (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. LeadsTo prg (A i) (A' i)) --> \
-\ (ALL i:I. Stable prg (A' i)) --> \
-\ LeadsTo prg (INT i:I. A i) (INT i:I. A' i)";
+\ ==> (ALL i:I. LeadsTo F (A i) (A' i)) --> \
+\ (ALL i:I. Stable F (A' i)) --> \
+\ LeadsTo F (INT i:I. A i) (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 "[| LeadsTo prg A (A' Un C); Constrains prg A' (A' Un C); \
-\ LeadsTo prg B (B' Un C); Constrains prg B' (B' Un C) |] \
-\ ==> LeadsTo prg (A Int B) ((A' Int B') Un C)";
+Goal "[| LeadsTo F A (A' Un C); Constrains F A' (A' Un C); \
+\ LeadsTo F B (B' Un C); Constrains F B' (B' Un C) |] \
+\ ==> LeadsTo F (A Int B) ((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);
@@ -400,9 +400,9 @@
Goal "[| finite I |] \
-\ ==> (ALL i:I. LeadsTo prg (A i) (A' i Un C)) --> \
-\ (ALL i:I. Constrains prg (A' i) (A' i Un C)) --> \
-\ LeadsTo prg (INT i:I. A i) ((INT i:I. A' i) Un C)";
+\ ==> (ALL i:I. LeadsTo F (A i) (A' i Un C)) --> \
+\ (ALL i:I. Constrains F (A' i) (A' i Un C)) --> \
+\ LeadsTo F (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/SubstAx.thy Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.thy Wed Oct 07 10:32:00 1998 +0200
@@ -11,8 +11,8 @@
constdefs
LeadsTo :: "['a program, 'a set, 'a set] => bool"
- "LeadsTo prg A B ==
- leadsTo (Acts prg)
- (reachable prg Int A)
- (reachable prg Int B)"
+ "LeadsTo F A B ==
+ leadsTo (Acts F)
+ (reachable F Int A)
+ (reachable F Int B)"
end
--- a/src/HOL/UNITY/Traces.ML Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/Traces.ML Wed Oct 07 10:32:00 1998 +0200
@@ -17,8 +17,8 @@
Rep_Program_inverse, Abs_Program_inverse];
-Goal "Id: Acts prg";
-by (cut_inst_tac [("x", "prg")] Rep_Program 1);
+Goal "Id: Acts F";
+by (cut_inst_tac [("x", "F")] Rep_Program 1);
by (auto_tac (claset(), rep_ss));
qed "Id_in_Acts";
AddIffs [Id_in_Acts];
@@ -35,8 +35,8 @@
Addsimps [Acts_eq, Init_eq];
-Goal "[| Init prg = Init prg'; Acts prg = Acts prg' |] ==> prg = prg'";
-by (cut_inst_tac [("p", "Rep_Program prg")] surjective_pairing 1);
+Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G";
+by (cut_inst_tac [("p", "Rep_Program F")] surjective_pairing 1);
by (auto_tac (claset(), rep_ss));
by (dres_inst_tac [("f", "Abs_Program")] arg_cong 1);
by (full_simp_tac (rep_ss addsimps [surjective_pairing RS sym]) 1);
@@ -46,8 +46,8 @@
(*** These three rules allow "lazy" definition expansion ***)
val [rew] = goal thy
- "[| prg == mk_program (init,acts) |] \
-\ ==> Init prg = init & Acts prg = insert Id acts";
+ "[| F == mk_program (init,acts) |] \
+\ ==> Init F = init & Acts F = insert Id acts";
by (rewtac rew);
by Auto_tac;
qed "def_prg_simps";
@@ -71,13 +71,17 @@
(*** traces and reachable ***)
-Goal "reachable prg = {s. EX evs. (s,evs): traces (Init prg) (Acts prg)}";
+Goal "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}";
by Safe_tac;
by (etac traces.induct 2);
by (etac reachable.induct 1);
-by (ALLGOALS (blast_tac (claset() addIs (reachable.intrs @ traces.intrs))));
+by (ALLGOALS (blast_tac (claset() addIs reachable.intrs @ traces.intrs)));
qed "reachable_equiv_traces";
-Goal "acts <= Acts prg ==> stable acts (reachable prg)";
-by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1);
+Goal "Init F <= reachable F";
+by (blast_tac (claset() addIs reachable.intrs) 1);
+qed "Init_subset_reachable";
+
+Goal "acts <= Acts F ==> stable acts (reachable F)";
+by (blast_tac (claset() addIs [stableI, constrainsI] @ reachable.intrs) 1);
qed "stable_reachable";
--- a/src/HOL/UNITY/Traces.thy Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/Traces.thy Wed Oct 07 10:32:00 1998 +0200
@@ -32,19 +32,19 @@
"mk_program == %(init, acts). Abs_Program (init, insert Id acts)"
Init :: "'a program => 'a set"
- "Init prg == fst (Rep_Program prg)"
+ "Init F == fst (Rep_Program F)"
Acts :: "'a program => ('a * 'a)set set"
- "Acts prg == snd (Rep_Program prg)"
+ "Acts F == snd (Rep_Program F)"
consts reachable :: "'a program => 'a set"
-inductive "reachable prg"
+inductive "reachable F"
intrs
- Init "s: Init prg ==> s : reachable prg"
+ Init "s: Init F ==> s : reachable F"
- Acts "[| act: Acts prg; s : reachable prg; (s,s'): act |]
- ==> s' : reachable prg"
+ Acts "[| act: Acts F; s : reachable F; (s,s'): act |]
+ ==> s' : reachable F"
end
--- a/src/HOL/UNITY/Union.ML Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/Union.ML Wed Oct 07 10:32:00 1998 +0200
@@ -85,20 +85,29 @@
by (Blast_tac 1);
qed "constrains_JN";
+Goal "constrains (Acts (F Join G)) A B = \
+\ (constrains (Acts F) A B & constrains (Acts G) A B)";
+by (auto_tac
+ (claset(),
+ simpset() addsimps [constrains_def, Join_def]));
+qed "constrains_Join";
+
(**FAILS, I think; see 5.4.1, Substitution Axiom.
+ The problem is to relate reachable (F Join G) with
+ reachable F and reachable G
+
Goalw [Constrains_def]
"Constrains (JN i:I. F i) A B = (ALL i:I. Constrains (F i) A B)";
by (simp_tac (simpset() addsimps [constrains_JN]) 1);
by (Blast_tac 1);
qed "Constrains_JN";
-**)
-Goal "constrains (Acts (F Join G)) A B = \
-\ (constrains (Acts F) A B & constrains (Acts G) A B)";
+Goal "Constrains (F Join G) A B = (Constrains F A B & Constrains G A B)";
by (auto_tac
(claset(),
- simpset() addsimps [constrains_def, Join_def, ball_Un]));
-qed "constrains_Join";
+ simpset() addsimps [Constrains_def, constrains_Join]));
+qed "Constrains_Join";
+**)
Goal "[| constrains (Acts F) A A'; constrains (Acts G) B B' |] \
\ ==> constrains (Acts (F Join G)) (A Int B) (A' Un B')";
--- a/src/HOL/UNITY/WFair.ML Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/WFair.ML Wed Oct 07 10:32:00 1998 +0200
@@ -434,7 +434,7 @@
\ 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(Blast_tac 1);
+by (Blast_tac 1);
val lemma1 = result();