--- a/src/HOL/UNITY/Channel.ML Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Channel.ML Thu Oct 15 11:35:07 1998 +0200
@@ -8,8 +8,6 @@
From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
*)
-AddIffs [skip];
-
(*None represents "infinity" while Some represents proper integers*)
Goalw [minSet_def] "minSet A = Some x --> x : A";
by (Simp_tac 1);
@@ -26,7 +24,7 @@
by (Blast_tac 1);
qed_spec_mp "minSet_nonempty";
-Goal "leadsTo acts (minSet -`` {Some x}) (minSet -`` (Some``greaterThan x))";
+Goal "F : leadsTo (minSet -`` {Some x}) (minSet -`` (Some``greaterThan x))";
by (rtac leadsTo_weaken 1);
by (rtac ([UC2, UC1] MRS psp) 1);
by (ALLGOALS Asm_simp_tac);
@@ -38,7 +36,7 @@
(*The induction*)
-Goal "leadsTo acts (UNIV-{{}}) (minSet -`` (Some``atLeast y))";
+Goal "F : leadsTo (UNIV-{{}}) (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);
@@ -54,7 +52,7 @@
val lemma = result();
-Goal "!!y::nat. leadsTo acts (UNIV-{{}}) {s. y ~: s}";
+Goal "!!y::nat. F : leadsTo (UNIV-{{}}) {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 Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Channel.thy Thu Oct 15 11:35:07 1998 +0200
@@ -12,18 +12,19 @@
types state = nat set
+consts
+ F :: state program
+
constdefs
minSet :: nat set => nat option
"minSet A == if A={} then None else Some (LEAST x. x:A)"
rules
- skip "Id: acts"
-
- UC1 "constrains acts (minSet -`` {Some x}) (minSet -`` (Some``atLeast x))"
+ UC1 "F : constrains (minSet -`` {Some x}) (minSet -`` (Some``atLeast x))"
- (* UC1 "constrains acts {s. minSet s = x} {s. x <= minSet s}" *)
+ (* UC1 "F : constrains {s. minSet s = x} {s. x <= minSet s}" *)
- UC2 "leadsTo acts (minSet -`` {Some x}) {s. x ~: s}"
+ UC2 "F : leadsTo (minSet -`` {Some x}) {s. x ~: s}"
end
--- a/src/HOL/UNITY/Client.ML Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Client.ML Thu Oct 15 11:35:07 1998 +0200
@@ -7,74 +7,9 @@
*)
- (*MOVE higher-up: UNITY.thy or Traces.thy ???*)
-
-(*[| stable acts C; constrains acts (C Int A) A |] ==> stable acts (C Int A)*)
-bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
-
-
-(*"raw" notion of invariant. Yields a SET of programs*)
-Goal "[| Init F<=A; stable (Acts F) A |] ==> F : invariant A";
-by (asm_simp_tac (simpset() addsimps [invariant_def]) 1);
-qed "invariantI";
-
-Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def]
- "F : invariant A ==> Invariant F A";
-by (blast_tac (claset() addIs [constrains_reachable_Int]) 1);
-qed "invariant_imp_Invariant";
-
-
-(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*)
-Goal "[| F : invariant A; F : invariant B |] ==> F : invariant (A Int B)";
-by (auto_tac (claset(), simpset() addsimps [invariant_def, stable_Int]));
-qed "invariant_Int";
-
-Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def]
- "Invariant F A = (F : invariant (reachable F Int A))";
-by (blast_tac (claset() addIs reachable.intrs) 1);
-qed "Invariant_eq_invariant_reachable";
-
-
-bind_thm ("invariant_includes_reachable",
- invariant_imp_Invariant RS Invariant_includes_reachable);
-
-Goalw [always_def] "always A = (UN I: Pow A. invariant I)";
-by (blast_tac (claset() addIs [invariantI, impOfSubs Init_subset_reachable,
- stable_reachable,
- impOfSubs invariant_includes_reachable]) 1);
-qed "always_eq_UN_invariant";
-
-Goal "F : always A = (EX I. F: invariant I & I <= A)";
-by (simp_tac (simpset() addsimps [always_eq_UN_invariant]) 1);
-by (Blast_tac 1);
-qed "always_iff_ex_invariant";
-
-
-Goalw [increasing_def, stable_def, constrains_def]
- "increasing f <= increasing (length o f)";
-by Auto_tac;
-by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1);
-qed "increasing_length";
-
-
-Goalw [increasing_def]
- "increasing f <= {F. ALL z::nat. stable (Acts F) {s. z < f s}}";
-by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
-by (Blast_tac 1);
-qed "increasing_less";
-
-
-Goal "[| F Join G : f localTo F; (s,s') : act; \
-\ act : Acts G; act ~: Acts F |] ==> f s' = f s";
-by (asm_full_simp_tac
- (simpset() addsimps [localTo_def, Acts_Join, stable_def,
- constrains_def]) 1);
-by (Blast_tac 1);
-qed "localTo_imp_equals";
-
-
-Goal "[| Stable F A; transient (Acts F) C; \
-\ reachable F <= (-A Un B Un C) |] ==> LeadsTo F A B";
+(*Perhaps move to SubstAx.ML*)
+Goal "[| F : Stable A; F : transient C; \
+\ reachable F <= (-A Un B Un C) |] ==> F : LeadsTo A 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);
@@ -82,28 +17,25 @@
qed "Stable_transient_reachable_LeadsTo";
-(**** things that definitely belong in Client.ML ****)
(*split_all_tac causes a big blow-up*)
claset_ref() := claset() delSWrapper "split_all_tac";
-val Client_simp = Cli_prg_def RS def_prg_simps;
+Addsimps [Cli_prg_def RS def_prg_Init];
+program_defs_ref := [Cli_prg_def];
Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
-DelIffs [length_Suc_conv];
-
(*Simplification for records*)
Addsimps (thms"state.update_defs");
-
(*CAN THIS be generalized?
Importantly, the second case considers actions that are in G
and NOT in Cli_prg (needed to use localTo_imp_equals) *)
Goal "(act : Acts (Cli_prg Join G)) = \
\ (act : {Id, rel_act, tok_act, ask_act} | \
\ act : Acts G & act ~: Acts Cli_prg)";
-by (asm_full_simp_tac (simpset() addsimps [Client_simp, Acts_Join]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cli_prg_def, Acts_Join]) 1);
(*don't unfold definitions of actions*)
by (blast_tac HOL_cs 1);
qed "Acts_Cli_Join_eq";
@@ -111,19 +43,18 @@
fun invariant_tac i =
rtac invariantI i THEN
- auto_tac (claset(), simpset() addsimps [Client_simp]) THEN
- constrains_tac i;
+ constrains_tac (i+1);
(*Safety property 1(a): ask is nondecreasing*)
Goalw [increasing_def] "Cli_prg: increasing ask";
-by (auto_tac (claset(), simpset() addsimps [Client_simp]));
+by (Clarify_tac 1);
by (constrains_tac 1);
by Auto_tac;
qed "increasing_ask";
(*Safety property 1(b): rel is nondecreasing*)
Goalw [increasing_def] "Cli_prg: increasing rel";
-by (auto_tac (claset(), simpset() addsimps [Client_simp]));
+by (Clarify_tac 1);
by (constrains_tac 1);
by Auto_tac;
qed "increasing_rel";
@@ -148,16 +79,21 @@
qed "ask_bounded";
+(*Curiously, we no longer need to expand the program definition, and
+ expanding it is extremely expensive!*)
+program_defs_ref := [];
+
(*Safety property 2: clients return the right number of tokens*)
Goalw [increasing_def]
"Cli_prg : (increasing giv Int (rel localTo Cli_prg)) \
\ guarantees invariant {s. rel s <= giv s}";
by (rtac guaranteesI 1);
-by (Clarify_tac 1);
by (invariant_tac 1);
+by (Force_tac 1);
by (subgoal_tac "rel s <= giv s'" 1);
by (force_tac (claset(),
- simpset() addsimps [stable_def, constrains_def]) 2);
+ simpset() delsimps [Acts_eq]
+ addsimps [stable_def, constrains_def]) 2);
by (dtac (Acts_Cli_Join_eq RS iffD1) 1);
(*we note that "rel" is local to Client*)
by (auto_tac (claset() addD2 ("x",localTo_imp_equals), simpset()));
@@ -166,12 +102,12 @@
(*** Towards proving the liveness property ***)
-Goal "transient (Acts (Cli_prg Join G)) \
-\ {s. length (giv s) = Suc k & \
-\ length (rel s) = k & ask s ! k <= giv s ! k}";
+Goal "Cli_prg Join G \
+\ : transient {s. length (giv s) = Suc k & \
+\ length (rel s) = k & ask s ! k <= giv s ! k}";
by (res_inst_tac [("act", "rel_act")] transient_mem 1);
by (auto_tac (claset(),
- simpset() addsimps [Domain_def, Acts_Join, Client_simp]));
+ simpset() addsimps [Domain_def, Acts_Join, Cli_prg_def]));
qed "transient_lemma";
Goal "Cli_prg : \
@@ -183,6 +119,7 @@
by (Clarify_tac 1);
by (dtac (impOfSubs increasing_length) 1);
by (invariant_tac 1);
+by (Force_tac 1);
by (dtac (Acts_Cli_Join_eq RS iffD1) 1);
by (auto_tac (claset() addD2 ("x",localTo_imp_equals), simpset()));
by (force_tac (claset(),
@@ -194,8 +131,8 @@
Goal "Cli_prg : \
\ (increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
\ Int invariant giv_meets_ask) \
-\ guarantees {F. LeadsTo F {s. k < length (giv s)} \
-\ {s. k < length (rel s)}}";
+\ guarantees (LeadsTo {s. k < length (giv s)} \
+\ {s. k < length (rel s)})";
by (rtac guaranteesI 1);
by (Clarify_tac 1);
by (rtac Stable_transient_reachable_LeadsTo 1);
--- a/src/HOL/UNITY/Client.thy Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Client.thy Thu Oct 15 11:35:07 1998 +0200
@@ -8,24 +8,6 @@
Client = Comp + Prefix +
-constdefs (*MOVE higher-up: UNITY.thy or Traces.thy ???*)
- always :: "'a set => 'a program set"
- "always A == {F. reachable F <= A}"
-
- (*The traditional word for inductive properties. Anyway, INDUCTIVE is
- reserved!*)
- invariant :: "'a set => 'a program set"
- "invariant A == {F. Init F <= A & stable (Acts F) A}"
-
- (*Polymorphic in both states and the meaning of <= *)
- increasing :: "['a => 'b::{ord}] => 'a program set"
- "increasing f == {F. ALL z. stable (Acts F) {s. z <= f s}}"
-
- (*The set of systems that regard "f" as local to F*)
- localTo :: ['a => 'b, 'a program] => 'a program set (infixl 80)
- "f localTo F == {G. ALL z. stable (Acts G - Acts F) {s. f s = z}}"
-
-
consts
Max :: nat (*Maximum number of tokens*)
--- a/src/HOL/UNITY/Common.ML Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Common.ML Thu Oct 15 11:35:07 1998 +0200
@@ -11,8 +11,8 @@
*)
(*Misra's property CMT4: t exceeds no common meeting time*)
-Goal "[| ALL m. Constrains F {m} (maxfg m); n: common |] \
-\ ==> Stable F (atMost n)";
+Goal "[| ALL m. F : Constrains {m} (maxfg m); n: common |] \
+\ ==> F : Stable (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,
@@ -22,39 +22,40 @@
qed "common_stable";
Goal "[| Init F <= atMost n; \
-\ ALL m. Constrains F {m} (maxfg m); n: common |] \
-\ ==> Invariant F (atMost n)";
+\ ALL m. F : Constrains {m} (maxfg m); n: common |] \
+\ ==> F : Invariant (atMost n)";
by (asm_simp_tac (simpset() addsimps [InvariantI, common_stable]) 1);
qed "common_Invariant";
(*** Some programs that implement the safety property above ***)
-(*This one is just Skip*)
-Goal "constrains {Id} {m} (maxfg m)";
+Goal "SKIP : constrains {m} (maxfg m)";
by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj,
- fasc, gasc]) 1);
+ fasc]) 1);
result();
-(*This one is t := ftime t || t := gtime t really needs Skip too*)
-Goal "constrains {range(%t.(t,ftime t)), range(%t.(t,gtime t))} \
-\ {m} (maxfg m)";
+(*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)";
by (simp_tac (simpset() addsimps [constrains_def, maxfg_def,
- le_max_iff_disj]) 1);
+ le_max_iff_disj, fasc]) 1);
by (Blast_tac 1);
result();
-(*This one is t := max (ftime t) (gtime t) really needs Skip too*)
-Goal "constrains {range(%t.(t, max (ftime t) (gtime t)))} \
-\ {m} (maxfg m)";
-by (simp_tac (simpset() addsimps [constrains_def, maxfg_def]) 1);
+(*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)";
+by (simp_tac
+ (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
by (Blast_tac 1);
result();
(*This one is t := t+1 if t <max (ftime t) (gtime t) *)
-Goalw [constrains_def, maxfg_def]
- "constrains { {(t, Suc t) | t. t < max (ftime t) (gtime t)} } \
-\ {m} (maxfg m)";
+Goal "mk_program (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }) \
+\ : constrains {m} (maxfg m)";
+by (simp_tac
+ (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
by (blast_tac (claset() addIs [Suc_leI]) 1);
result();
@@ -67,10 +68,10 @@
Addsimps [atMost_Int_atLeast];
-Goal "[| ALL m. Constrains F {m} (maxfg m); \
-\ ALL m: lessThan n. LeadsTo F {m} (greaterThan m); \
+Goal "[| ALL m. F : Constrains {m} (maxfg m); \
+\ ALL m: lessThan n. F : LeadsTo {m} (greaterThan m); \
\ n: common |] \
-\ ==> LeadsTo F (atMost n) common";
+\ ==> F : LeadsTo (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 +81,10 @@
val lemma = result();
(*The "ALL m: -common" form echoes CMT6.*)
-Goal "[| ALL m. Constrains F {m} (maxfg m); \
-\ ALL m: -common. LeadsTo F {m} (greaterThan m); \
+Goal "[| ALL m. F : Constrains {m} (maxfg m); \
+\ ALL m: -common. F : LeadsTo {m} (greaterThan m); \
\ n: common |] \
-\ ==> LeadsTo F (atMost (LEAST n. n: common)) common";
+\ ==> F : LeadsTo (atMost (LEAST n. n: common)) common";
by (rtac lemma 1);
by (ALLGOALS Asm_simp_tac);
by (etac LeastI 2);
--- a/src/HOL/UNITY/Common.thy Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Common.thy Thu Oct 15 11:35:07 1998 +0200
@@ -10,7 +10,7 @@
From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
*)
-Common = SubstAx +
+Common = SubstAx + Union +
consts
ftime,gtime :: nat=>nat
--- a/src/HOL/UNITY/Constrains.ML Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Constrains.ML Thu Oct 15 11:35:07 1998 +0200
@@ -9,68 +9,66 @@
(*** Constrains ***)
-(*Map its type, ('a * 'a)set set, 'a set, 'a set] => bool, to just 'a*)
-Blast.overloaded ("Constrains.Constrains",
- HOLogic.dest_setT o domain_type o range_type);
+overload_1st_set "Constrains.Constrains";
-(*constrains (Acts F) B B'
- ==> constrains (Acts F) (reachable F Int B) (reachable F Int B')*)
+(*F : constrains B B'
+ ==> F : constrains (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 F) A A' ==> Constrains F A A'";
-by (etac constrains_reachable_Int 1);
+Goalw [Constrains_def] "F : constrains A A' ==> F : Constrains A A'";
+by (blast_tac (claset() addIs [constrains_reachable_Int]) 1);
qed "constrains_imp_Constrains";
-Goalw [stable_def, Stable_def] "stable (Acts F) A ==> Stable F A";
+Goalw [stable_def, Stable_def] "F : stable A ==> F : Stable A";
by (etac constrains_imp_Constrains 1);
qed "stable_imp_Stable";
val prems = Goal
"(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A') \
-\ ==> Constrains F A A'";
+\ ==> F : Constrains A A'";
by (rtac constrains_imp_Constrains 1);
by (blast_tac (claset() addIs (constrainsI::prems)) 1);
qed "ConstrainsI";
-Goalw [Constrains_def, constrains_def] "Constrains F {} B";
+Goalw [Constrains_def, constrains_def] "F : Constrains {} B";
by (Blast_tac 1);
qed "Constrains_empty";
-Goal "Constrains F A UNIV";
+Goal "F : Constrains A UNIV";
by (blast_tac (claset() addIs [ConstrainsI]) 1);
qed "Constrains_UNIV";
AddIffs [Constrains_empty, Constrains_UNIV];
Goalw [Constrains_def]
- "[| Constrains F A A'; A'<=B' |] ==> Constrains F A B'";
+ "[| F : Constrains A A'; A'<=B' |] ==> F : Constrains A B'";
by (blast_tac (claset() addIs [constrains_weaken_R]) 1);
qed "Constrains_weaken_R";
Goalw [Constrains_def]
- "[| Constrains F A A'; B<=A |] ==> Constrains F B A'";
+ "[| F : Constrains A A'; B<=A |] ==> F : Constrains B A'";
by (blast_tac (claset() addIs [constrains_weaken_L]) 1);
qed "Constrains_weaken_L";
Goalw [Constrains_def]
- "[| Constrains F A A'; B<=A; A'<=B' |] ==> Constrains F B B'";
+ "[| F : Constrains A A'; B<=A; A'<=B' |] ==> F : Constrains B B'";
by (blast_tac (claset() addIs [constrains_weaken]) 1);
qed "Constrains_weaken";
(** Union **)
Goalw [Constrains_def]
- "[| Constrains F A A'; Constrains F B B' |] \
-\ ==> Constrains F (A Un B) (A' Un B')";
+ "[| F : Constrains A A'; F : Constrains B B' |] \
+\ ==> F : Constrains (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 F (A i) (A' i) \
-\ ==> Constrains F (UN i:I. A i) (UN i:I. A' i)";
+Goal "ALL i:I. F : Constrains (A i) (A' i) \
+\ ==> F : Constrains (UN i:I. A i) (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);
qed "ball_Constrains_UN";
@@ -78,75 +76,75 @@
(** Intersection **)
Goalw [Constrains_def]
- "[| Constrains F A A'; Constrains F B B' |] \
-\ ==> Constrains F (A Int B) (A' Int B')";
+ "[| F : Constrains A A'; F : Constrains B B' |] \
+\ ==> F : Constrains (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 F (A i) (A' i) |] \
-\ ==> Constrains F (INT i:I. A i) (INT i:I. A' i)";
+Goal "[| ALL i:I. F : Constrains (A i) (A' i) |] \
+\ ==> F : Constrains (INT i:I. A i) (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";
-Goalw [Constrains_def]
- "Constrains F A A' ==> reachable F Int A <= A'";
+Goal "F : Constrains A A' ==> reachable F Int A <= A'";
+by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
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 F A B; Constrains F B C |] \
-\ ==> Constrains F A C";
+ "[| F : Constrains A B; F : Constrains B C |] \
+\ ==> F : Constrains A C";
by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
qed "Constrains_trans";
(*** Stable ***)
-Goal "Stable F A = stable (Acts F) (reachable F Int A)";
+Goal "(F : Stable A) = (F : stable (reachable F Int A))";
by (simp_tac (simpset() addsimps [Stable_def, Constrains_def, stable_def]) 1);
qed "Stable_eq_stable";
-Goalw [Stable_def] "Constrains F A A ==> Stable F A";
+Goalw [Stable_def] "F : Constrains A A ==> F : Stable A";
by (assume_tac 1);
qed "StableI";
-Goalw [Stable_def] "Stable F A ==> Constrains F A A";
+Goalw [Stable_def] "F : Stable A ==> F : Constrains A A";
by (assume_tac 1);
qed "StableD";
Goalw [Stable_def]
- "[| Stable F A; Stable F A' |] ==> Stable F (A Un A')";
+ "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Un A')";
by (blast_tac (claset() addIs [Constrains_Un]) 1);
qed "Stable_Un";
Goalw [Stable_def]
- "[| Stable F A; Stable F A' |] ==> Stable F (A Int A')";
+ "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Int A')";
by (blast_tac (claset() addIs [Constrains_Int]) 1);
qed "Stable_Int";
Goalw [Stable_def]
- "[| Stable F C; Constrains F A (C Un A') |] \
-\ ==> Constrains F (C Un A) (C Un A')";
+ "[| F : Stable C; F : Constrains A (C Un A') |] \
+\ ==> F : Constrains (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 F C; Constrains F (C Int A) A' |] \
-\ ==> Constrains F (C Int A) (C Int A')";
+ "[| F : Stable C; F : Constrains (C Int A) A' |] \
+\ ==> F : Constrains (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 F (A i)) ==> Stable F (INT i:I. A i)";
+ "(ALL i:I. F : Stable (A i)) ==> F : Stable (INT i:I. A i)";
by (etac ball_Constrains_INT 1);
qed "ball_Stable_INT";
-Goal "Stable F (reachable F)";
+Goal "F : Stable (reachable F)";
by (simp_tac (simpset() addsimps [Stable_eq_stable, stable_reachable]) 1);
qed "Stable_reachable";
@@ -157,21 +155,21 @@
in forward proof. ***)
Goalw [Constrains_def, constrains_def]
- "[| ALL m. Constrains F {s. s x = m} (B m) |] \
-\ ==> Constrains F {s. s x : M} (UN m:M. B m)";
+ "[| ALL m. F : Constrains {s. s x = m} (B m) |] \
+\ ==> F : Constrains {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 F {m} (B m)) ==> Constrains F M (UN m:M. B m)";
+ "(ALL m. F : Constrains {m} (B m)) ==> F : Constrains M (UN m:M. B m)";
by (Blast_tac 1);
qed "Elimination_sing";
Goalw [Constrains_def, constrains_def]
- "[| Constrains F A (A' Un B); Constrains F B B' |] \
-\ ==> Constrains F A (A' Un B')";
+ "[| F : Constrains A (A' Un B); F : Constrains B B' |] \
+\ ==> F : Constrains A (A' Un B')";
by (Blast_tac 1);
qed "Constrains_cancel";
@@ -180,11 +178,11 @@
(** Natural deduction rules for "Invariant F A" **)
-Goal "[| Init F<=A; Stable F A |] ==> Invariant F A";
+Goal "[| Init F<=A; F : Stable A |] ==> F : Invariant A";
by (asm_simp_tac (simpset() addsimps [Invariant_def]) 1);
qed "InvariantI";
-Goal "Invariant F A ==> Init F<=A & Stable F A";
+Goal "F : Invariant A ==> Init F<=A & F : Stable A";
by (asm_full_simp_tac (simpset() addsimps [Invariant_def]) 1);
qed "InvariantD";
@@ -192,13 +190,13 @@
(*The set of all reachable states is an Invariant...*)
-Goal "Invariant F (reachable F)";
+Goal "F : Invariant (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 F A ==> reachable F <= A";
+Goal "F : Invariant A ==> reachable F <= A";
by (full_simp_tac
(simpset() addsimps [Stable_def, Constrains_def, constrains_def,
Invariant_def]) 1);
@@ -207,25 +205,36 @@
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
qed "Invariant_includes_reachable";
+Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def]
+ "F : invariant A ==> F : Invariant A";
+by (blast_tac (claset() addIs [constrains_reachable_Int]) 1);
+qed "invariant_imp_Invariant";
-Goal "Invariant F INV ==> reachable F Int INV = reachable F";
+Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def]
+ "(F : Invariant A) = (F : invariant (reachable F Int A))";
+by (blast_tac (claset() addIs reachable.intrs) 1);
+qed "Invariant_eq_invariant_reachable";
+
+
+
+Goal "F : Invariant INV ==> reachable F Int INV = reachable F";
by (dtac Invariant_includes_reachable 1);
by (Blast_tac 1);
qed "reachable_Int_INV";
-Goal "[| Invariant F INV; Constrains F (INV Int A) A' |] \
-\ ==> Constrains F A A'";
+Goal "[| F : Invariant INV; F : Constrains (INV Int A) A' |] \
+\ ==> F : Constrains A A'";
by (asm_full_simp_tac
(simpset() addsimps [Constrains_def, reachable_Int_INV,
Int_assoc RS sym]) 1);
qed "Invariant_ConstrainsI";
-(* [| Invariant F INV; Constrains F (INV Int A) A |]
- ==> Stable F A *)
+(* [| F : Invariant INV; F : Constrains (INV Int A) A |]
+ ==> F : Stable A *)
bind_thm ("Invariant_StableI", Invariant_ConstrainsI RS StableI);
-Goal "[| Invariant F INV; Constrains F A A' |] \
-\ ==> Constrains F A (INV Int A')";
+Goal "[| F : Invariant INV; F : Constrains A A' |] \
+\ ==> F : Constrains A (INV Int A')";
by (asm_full_simp_tac
(simpset() addsimps [Constrains_def, reachable_Int_INV,
Int_assoc RS sym]) 1);
@@ -237,7 +246,7 @@
(** Conjoining Invariants **)
-Goal "[| Invariant F A; Invariant F B |] ==> Invariant F (A Int B)";
+Goal "[| F : Invariant A; F : Invariant B |] ==> F : Invariant (A Int B)";
by (auto_tac (claset(),
simpset() addsimps [Invariant_def, Stable_Int]));
qed "Invariant_Int";
@@ -246,7 +255,7 @@
used by Invariant_Int) *)
val Invariant_thin =
read_instantiate_sg (sign_of thy)
- [("V", "Invariant ?Prg ?A")] thin_rl;
+ [("V", "?F : Invariant ?A")] thin_rl;
(*Combines two invariance ASSUMPTIONS into one. USEFUL??*)
val Invariant_Int_tac = dtac Invariant_Int THEN'
@@ -257,15 +266,19 @@
val Invariant_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Invariant_Int);
+(*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*)
-val constrains_tac =
+fun constrains_tac i =
SELECT_GOAL
- (EVERY [REPEAT (resolve_tac [StableI, stableI,
+ (EVERY [simp_tac (simpset() addsimps !program_defs_ref) 1,
+ REPEAT (resolve_tac [StableI, stableI,
constrains_imp_Constrains] 1),
rtac constrainsI 1,
Full_simp_tac 1,
REPEAT (FIRSTGOAL (etac disjE)),
ALLGOALS Clarify_tac,
- ALLGOALS Asm_full_simp_tac]);
+ ALLGOALS Asm_full_simp_tac]) i;
--- a/src/HOL/UNITY/Constrains.thy Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Constrains.thy Thu Oct 15 11:35:07 1998 +0200
@@ -10,19 +10,17 @@
constdefs
- Constrains :: "['a program, 'a set, 'a set] => bool"
- "Constrains F A B ==
- constrains (Acts F)
- (reachable F Int A)
- (reachable F Int B)"
+ Constrains :: "['a set, 'a set] => 'a program set"
+ "Constrains A B == {F. F : constrains (reachable F Int A)
+ (reachable F Int B)}"
- Stable :: "'a program => 'a set => bool"
- "Stable F A == Constrains F A A"
+ Stable :: "'a set => 'a program set"
+ "Stable A == Constrains A A"
- Unless :: "['a program, 'a set, 'a set] => bool"
- "Unless F A B == Constrains F (A-B) (A Un B)"
+ Unless :: "['a set, 'a set] => 'a program set"
+ "Unless A B == Constrains (A-B) (A Un B)"
- Invariant :: "['a program, 'a set] => bool"
- "Invariant F A == (Init F) <= A & Stable F A"
+ Invariant :: "'a set => 'a program set"
+ "Invariant A == {F. Init F <= A} Int Stable A"
end
--- a/src/HOL/UNITY/Deadlock.ML Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Deadlock.ML Thu Oct 15 11:35:07 1998 +0200
@@ -9,80 +9,70 @@
(*Trivial, two-process case*)
Goalw [constrains_def, stable_def]
- "[| constrains Acts (A Int B) A; constrains Acts (B Int A) B |] \
-\ ==> stable Acts (A Int B)";
+ "[| F : constrains (A Int B) A; F : constrains (B Int A) B |] \
+\ ==> F : stable (A Int B)";
by (Blast_tac 1);
result();
-Goal "{i. i < Suc n} = insert n {i. i < n}";
-by (blast_tac (claset() addSEs [less_SucE] addIs [less_SucI]) 1);
-qed "Collect_less_Suc_insert";
-
-
-Goal "{i. i <= Suc n} = insert (Suc n) {i. i <= n}";
-by (blast_tac (claset() addSEs [le_SucE] addIs [le_SucI]) 1);
-qed "Collect_le_Suc_insert";
-
-
(*a simplification step*)
-Goal "(INT i:{i. i <= n}. A(Suc i) Int A i) = \
-\ (INT i:{i. i <= Suc n}. A i)";
+Goal "(INT i: atMost n. A(Suc i) Int A i) = \
+\ (INT i: atMost (Suc n). A i)";
by (induct_tac "n" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Collect_le_Suc_insert])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [atMost_Suc])));
by (blast_tac (claset() addEs [le_SucE] addSEs [equalityE]) 1);
qed "Collect_le_Int_equals";
(*Dual of the required property. Converse inclusion fails.*)
-Goal "(UN i:{i. i < n}. A i) Int -(A n) <= \
-\ (UN i:{i. i < n}. (A i) Int -(A(Suc i)))";
+Goal "(UN i: lessThan n. A i) Int -(A n) <= \
+\ (UN i: lessThan n. (A i) Int -(A(Suc i)))";
by (induct_tac "n" 1);
by (Asm_simp_tac 1);
-by (simp_tac (simpset() addsimps [Collect_less_Suc_insert]) 1);
+by (simp_tac (simpset() addsimps [lessThan_Suc]) 1);
by (Blast_tac 1);
qed "UN_Int_Compl_subset";
(*Converse inclusion fails.*)
-Goal "(INT i:{i. i < n}. -A i Un A (Suc i)) <= \
-\ (INT i:{i. i < n}. -A i) Un A n";
+Goal "(INT i: lessThan n. -A i Un A (Suc i)) <= \
+\ (INT i: lessThan n. -A i) Un A n";
by (induct_tac "n" 1);
by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [Collect_less_Suc_insert]) 1);
+by (asm_simp_tac (simpset() addsimps [lessThan_Suc]) 1);
by (Blast_tac 1);
qed "INT_Un_Compl_subset";
(*Specialized rewriting*)
-Goal "A 0 Int (-(A n) Int (INT i:{i. i < n}. -A i Un A (Suc i))) = {}";
+Goal "A 0 Int (-(A n) Int (INT i: lessThan n. -A i Un A (Suc i))) = {}";
by (blast_tac (claset() addIs [gr0I]
addDs [impOfSubs INT_Un_Compl_subset]) 1);
val lemma = result();
(*Reverse direction makes it harder to invoke the ind hyp*)
-Goal "(INT i:{i. i <= n}. A i) = \
-\ A 0 Int (INT i:{i. i < n}. -A i Un A(Suc i))";
+Goal "(INT i: atMost n. A i) = \
+\ A 0 Int (INT i: lessThan n. -A i Un A(Suc i))";
by (induct_tac "n" 1);
by (Asm_simp_tac 1);
by (asm_simp_tac
(simpset() addsimps Int_ac @
[Int_Un_distrib, Int_Un_distrib2, lemma,
- Collect_less_Suc_insert, Collect_le_Suc_insert]) 1);
+ lessThan_Suc, atMost_Suc]) 1);
qed "INT_le_equals_Int";
-Goal "(INT i:{i. i <= Suc n}. A i) = \
-\ A 0 Int (INT i:{i. i <= n}. -A i Un A(Suc i))";
-by (simp_tac (simpset() addsimps [less_Suc_eq_le, INT_le_equals_Int]) 1);
+Goal "(INT i: atMost (Suc n). A i) = \
+\ A 0 Int (INT i: atMost n. -A i Un A(Suc i))";
+by (simp_tac (simpset() addsimps [lessThan_Suc_atMost, INT_le_equals_Int]) 1);
qed "INT_le_Suc_equals_Int";
(*The final deadlock example*)
val [zeroprem, allprem] = goalw thy [stable_def]
- "[| constrains Acts (A 0 Int A (Suc n)) (A 0); \
-\ ALL i:{i. i <= n}. constrains Acts (A(Suc i) Int A i) \
+ "[| 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)) |] \
-\ ==> stable Acts (INT i:{i. i <= Suc n}. A i)";
+\ ==> F : stable (INT i: atMost (Suc n). A i)";
by (rtac ([zeroprem, allprem RS ball_constrains_INT] MRS
constrains_Int RS constrains_weaken) 1);
--- a/src/HOL/UNITY/FP.ML Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/FP.ML Thu Oct 15 11:35:07 1998 +0200
@@ -8,7 +8,7 @@
From Misra, "A Logic for Concurrent Programming", 1994
*)
-Goalw [FP_Orig_def, stable_def] "stable Acts (FP_Orig Acts Int B)";
+Goalw [FP_Orig_def, stable_def] "F : stable (FP_Orig F Int B)";
by (stac Int_Union2 1);
by (rtac ball_constrains_UN 1);
by (Simp_tac 1);
@@ -16,13 +16,13 @@
val prems = goalw thy [FP_Orig_def, stable_def]
- "(!!B. stable Acts (A Int B)) ==> A <= FP_Orig Acts";
+ "(!!B. F : stable (A Int B)) ==> A <= FP_Orig F";
by (blast_tac (claset() addIs prems) 1);
qed "FP_Orig_weakest";
-Goal "stable Acts (FP Acts Int B)";
-by (subgoal_tac "FP Acts Int B = (UN x:B. FP Acts Int {x})" 1);
+Goal "F : stable (FP F Int B)";
+by (subgoal_tac "FP F Int B = (UN x:B. FP F Int {x})" 1);
by (Blast_tac 2);
by (asm_simp_tac (simpset() addsimps [Int_insert_right]) 1);
by (rewrite_goals_tac [FP_def, stable_def]);
@@ -30,31 +30,31 @@
by (Simp_tac 1);
qed "stable_FP_Int";
-Goal "FP Acts <= FP_Orig Acts";
+Goal "FP F <= FP_Orig F";
by (rtac (stable_FP_Int RS FP_Orig_weakest) 1);
val lemma1 = result();
-Goalw [FP_Orig_def, FP_def] "FP_Orig Acts <= FP Acts";
+Goalw [FP_Orig_def, FP_def] "FP_Orig F <= FP F";
by (Clarify_tac 1);
by (dres_inst_tac [("x", "{x}")] spec 1);
by (asm_full_simp_tac (simpset() addsimps [Int_insert_right]) 1);
val lemma2 = result();
-Goal "FP Acts = FP_Orig Acts";
+Goal "FP F = FP_Orig F";
by (rtac ([lemma1,lemma2] MRS equalityI) 1);
qed "FP_equivalence";
val [prem] = goal thy
- "(!!B. stable Acts (A Int B)) ==> A <= FP Acts";
+ "(!!B. F : stable (A Int B)) ==> A <= FP F";
by (simp_tac (simpset() addsimps [FP_equivalence, prem RS FP_Orig_weakest]) 1);
qed "FP_weakest";
Goalw [FP_def, stable_def, constrains_def]
- "-(FP Acts) = (UN act:Acts. -{s. act^^{s} <= {s}})";
+ "-(FP F) = (UN act: Acts F. -{s. act^^{s} <= {s}})";
by (Blast_tac 1);
qed "Compl_FP";
-Goal "A - (FP Acts) = (UN act:Acts. A - {s. act^^{s} <= {s}})";
+Goal "A - (FP F) = (UN act: Acts F. A - {s. act^^{s} <= {s}})";
by (simp_tac (simpset() addsimps [Diff_eq, Compl_FP]) 1);
qed "Diff_FP";
--- a/src/HOL/UNITY/FP.thy Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/FP.thy Thu Oct 15 11:35:07 1998 +0200
@@ -12,10 +12,10 @@
constdefs
- FP_Orig :: "('a * 'a)set set => 'a set"
- "FP_Orig Acts == Union{A. ALL B. stable Acts (A Int B)}"
+ FP_Orig :: "'a program => 'a set"
+ "FP_Orig F == Union{A. ALL B. F : stable (A Int B)}"
- FP :: "('a * 'a)set set => 'a set"
- "FP Acts == {s. stable Acts {s}}"
+ FP :: "'a program => 'a set"
+ "FP F == {s. F : stable {s}}"
end
--- a/src/HOL/UNITY/Handshake.ML Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Handshake.ML Thu Oct 15 11:35:07 1998 +0200
@@ -11,8 +11,9 @@
(*split_all_tac causes a big blow-up*)
claset_ref() := claset() delSWrapper "split_all_tac";
-Addsimps [prgF_def RS def_prg_simps];
-Addsimps [prgG_def RS def_prg_simps];
+Addsimps [F_def RS def_prg_Init, G_def RS def_prg_Init];
+program_defs_ref := [F_def, G_def];
+
Addsimps (map simp_of_act [cmdF_def, cmdG_def]);
(*Simplification for records*)
@@ -20,7 +21,7 @@
Addsimps [simp_of_set invFG_def];
-Goal "Invariant (prgF Join prgG) invFG";
+Goal "(F Join G) : Invariant invFG";
by (rtac InvariantI 1);
by (Force_tac 1);
by (rtac (constrains_imp_Constrains RS StableI) 1);
@@ -30,26 +31,26 @@
by (constrains_tac 1);
qed "invFG";
-Goal "LeadsTo (prgF Join prgG) ({s. NF s = k} - {s. BB s}) \
+Goal "(F Join G) : LeadsTo ({s. NF s = k} - {s. BB s}) \
\ ({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);
by (constrains_tac 1);
qed "lemma2_1";
-Goal "LeadsTo (prgF Join prgG) ({s. NF s = k} Int {s. BB s}) {s. k < NF s}";
+Goal "(F Join G) : LeadsTo ({s. NF s = k} Int {s. BB s}) {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);
qed "lemma2_2";
-Goal "LeadsTo (prgF Join prgG) UNIV {s. m < NF s}";
+Goal "(F Join G) : LeadsTo UNIV {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: LeadsTo (prgF Join prgG) {x. NF x = ma} {x. ma < NF x}*)
+(*The inductive step: (F Join G) : LeadsTo {x. NF x = ma} {x. ma < NF x}*)
by (rtac LeadsTo_Diff 1);
by (rtac lemma2_2 2);
by (rtac LeadsTo_Trans 1);
--- a/src/HOL/UNITY/Handshake.thy Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Handshake.thy Thu Oct 15 11:35:07 1998 +0200
@@ -20,15 +20,15 @@
cmdF :: "(state*state) set"
"cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"
- prgF :: "state program"
- "prgF == mk_program ({s. NF s = 0 & BB s}, {cmdF})"
+ F :: "state program"
+ "F == mk_program ({s. NF s = 0 & BB s}, {cmdF})"
(*G's program*)
cmdG :: "(state*state) set"
"cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"
- prgG :: "state program"
- "prgG == mk_program ({s. NG s = 0 & BB s}, {cmdG})"
+ G :: "state program"
+ "G == mk_program ({s. NG s = 0 & BB s}, {cmdG})"
(*the joint invariant*)
invFG :: "state set"
--- a/src/HOL/UNITY/LessThan.ML Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/LessThan.ML Thu Oct 15 11:35:07 1998 +0200
@@ -7,6 +7,7 @@
*)
+(*Make Auto_tac and Force_tac try trans_tac!*)
claset_ref() := claset() addaltern ("trans_tac",trans_tac);
@@ -27,6 +28,10 @@
by (Blast_tac 1);
qed "lessThan_Suc";
+Goalw [lessThan_def, atMost_def] "lessThan (Suc k) = atMost k";
+by (simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
+qed "lessThan_Suc_atMost";
+
Goal "(UN m. lessThan m) = UNIV";
by (Blast_tac 1);
qed "UN_lessThan_UNIV";
--- a/src/HOL/UNITY/Lift.ML Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Lift.ML Thu Oct 15 11:35:07 1998 +0200
@@ -55,7 +55,8 @@
zless_not_refl2, zless_not_refl3];
-Addsimps [Lprg_def RS def_prg_simps];
+Addsimps [Lprg_def RS def_prg_Init];
+program_defs_ref := [Lprg_def];
Addsimps (map simp_of_act
[request_act_def, open_act_def, close_act_def,
@@ -69,7 +70,7 @@
val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un;
-(* [| LeadsTo Lprg B C; LeadsTo Lprg A B |] ==> LeadsTo Lprg (A Un B) C *)
+(* [| Lprg : LeadsTo B C; Lprg : LeadsTo A B |] ==> Lprg : LeadsTo (A Un B) C *)
(*Simplification for records*)
@@ -87,41 +88,41 @@
val nat_exhaust_pred_le =
read_instantiate_sg (sign_of thy) [("P", "?y-1 <= ?m")] nat.exhaust;
-Goal "Invariant Lprg open_stop";
+Goal "Lprg : Invariant open_stop";
by (rtac InvariantI 1);
by (Force_tac 1);
by (constrains_tac 1);
qed "open_stop";
-Goal "Invariant Lprg stop_floor";
+Goal "Lprg : Invariant stop_floor";
by (rtac InvariantI 1);
by (Force_tac 1);
by (constrains_tac 1);
qed "stop_floor";
(*This one needs open_stop, which was proved above*)
-Goal "Invariant Lprg open_move";
+Goal "Lprg : Invariant open_move";
by (rtac InvariantI 1);
by (rtac (open_stop RS Invariant_ConstrainsI RS StableI) 2);
by (Force_tac 1);
by (constrains_tac 1);
qed "open_move";
-Goal "Invariant Lprg moving_up";
+Goal "Lprg : Invariant moving_up";
by (rtac InvariantI 1);
by (Force_tac 1);
by (constrains_tac 1);
by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
qed "moving_up";
-Goal "Invariant Lprg moving_down";
+Goal "Lprg : Invariant moving_down";
by (rtac InvariantI 1);
by (Force_tac 1);
by (constrains_tac 1);
by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
qed "moving_down";
-Goal "Invariant Lprg bounded";
+Goal "Lprg : Invariant bounded";
by (rtac InvariantI 1);
by (rtac (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2);
by (Force_tac 1);
@@ -150,23 +151,23 @@
(** Lift_1 **)
-Goal "LeadsTo Lprg (stopped Int atFloor n) (opened Int atFloor n)";
+Goal "Lprg : LeadsTo (stopped Int atFloor n) (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 "LeadsTo Lprg (Req n Int stopped - atFloor n) \
+Goal "Lprg : LeadsTo (Req n Int stopped - atFloor n) \
\ (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 "LeadsTo Lprg (Req n Int opened - atFloor n) \
+Goal "Lprg : LeadsTo (Req n Int opened - atFloor n) \
\ (Req n Int closed - (atFloor n - queueing))";
by (ensures_tac "close_act" 1);
qed "E_thm03"; (*lem_lift_1_2*)
-Goal "LeadsTo Lprg (Req n Int closed Int (atFloor n - queueing)) \
+Goal "Lprg : LeadsTo (Req n Int closed Int (atFloor n - queueing)) \
\ (opened Int atFloor n)";
by (ensures_tac "open_act" 1);
qed "E_thm04"; (*lem_lift_1_7*)
@@ -190,7 +191,7 @@
(*lem_lift_2_0
NOT an ensures property, but a mere inclusion;
don't know why script lift_2.uni says ENSURES*)
-Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing)) \
+Goal "Lprg : LeadsTo (Req n Int closed - (atFloor n - queueing)) \
\ ((closed Int goingup Int Req n) Un \
\ (closed Int goingdown Int Req n))";
by (rtac subset_imp_LeadsTo 1);
@@ -198,7 +199,7 @@
qed "E_thm05c";
(*lift_2*)
-Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing)) \
+Goal "Lprg : LeadsTo (Req n Int closed - (atFloor n - queueing)) \
\ (moving Int Req n)";
by (rtac ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1);
by (ensures_tac "req_down" 2);
@@ -212,7 +213,7 @@
(*lem_lift_4_1 *)
Goal "#0 < N ==> \
-\ LeadsTo Lprg \
+\ Lprg : LeadsTo \
\ (moving Int Req n Int {s. metric n s = N} Int \
\ {s. floor s ~: req s} Int {s. up s}) \
\ (moving Int Req n Int {s. metric n s < N})";
@@ -232,7 +233,7 @@
(*lem_lift_4_3 *)
Goal "#0 < N ==> \
-\ LeadsTo Lprg \
+\ 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})";
@@ -250,7 +251,7 @@
qed "E_thm12b";
(*lift_4*)
-Goal "#0<N ==> LeadsTo Lprg (moving Int Req n Int {s. metric n s = N} Int \
+Goal "#0<N ==> Lprg : LeadsTo (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})";
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
@@ -264,7 +265,7 @@
(*lem_lift_5_3*)
Goal "#0<N \
-\ ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingup) \
+\ ==> Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N} Int goingup) \
\ (moving Int Req n Int {s. metric n s < N})";
by (cut_facts_tac [bounded] 1);
by (ensures_tac "req_up" 1);
@@ -280,7 +281,7 @@
(*lem_lift_5_1 has ~goingup instead of goingdown*)
Goal "#0<N ==> \
-\ LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingdown) \
+\ Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N} Int goingdown) \
\ (moving Int Req n Int {s. metric n s < N})";
by (cut_facts_tac [bounded] 1);
by (ensures_tac "req_down" 1);
@@ -309,7 +310,7 @@
(*lift_5*)
-Goal "#0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N}) \
+Goal "#0<N ==> Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N}) \
\ (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);
@@ -341,7 +342,7 @@
(*lem_lift_3_1*)
-Goal "LeadsTo Lprg (moving Int Req n Int {s. metric n s = #0}) \
+Goal "Lprg : LeadsTo (moving Int Req n Int {s. metric n s = #0}) \
\ (stopped Int atFloor n)";
by (cut_facts_tac [bounded] 1);
by (ensures_tac "request_act" 1);
@@ -349,7 +350,7 @@
qed "E_thm11";
(*lem_lift_3_5*)
-Goal "LeadsTo Lprg \
+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})";
by (ensures_tac "request_act" 1);
@@ -358,7 +359,7 @@
(*lem_lift_3_6*)
Goal "#0 < N ==> \
-\ LeadsTo Lprg \
+\ Lprg : LeadsTo \
\ (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})";
by (ensures_tac "open_act" 1);
@@ -367,7 +368,7 @@
qed "E_thm14";
(*lem_lift_3_7*)
-Goal "LeadsTo Lprg \
+Goal "Lprg : LeadsTo \
\ (opened Int Req n Int {s. metric n s = N}) \
\ (closed Int Req n Int {s. metric n s = N})";
by (ensures_tac "close_act" 1);
@@ -378,7 +379,7 @@
(** the final steps **)
Goal "#0 < N ==> \
-\ LeadsTo Lprg \
+\ Lprg : LeadsTo \
\ (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})";
by (blast_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5]
@@ -399,7 +400,7 @@
val R_thm11 = [reach_nonneg, E_thm11] MRS reachable_LeadsTo_weaken;
-Goal "LeadsTo Lprg (moving Int Req n) (stopped Int atFloor n)";
+Goal "Lprg : LeadsTo (moving Int Req n) (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*)
@@ -413,7 +414,7 @@
qed "lift_3";
-Goal "LeadsTo Lprg (Req n) (opened Int atFloor n)";
+Goal "Lprg : LeadsTo (Req n) (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 Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Mutex.ML Thu Oct 15 11:35:07 1998 +0200
@@ -9,7 +9,8 @@
(*split_all_tac causes a big blow-up*)
claset_ref() := claset() delSWrapper "split_all_tac";
-Addsimps [Mprg_def RS def_prg_simps];
+Addsimps [Mprg_def RS def_prg_Init];
+program_defs_ref := [Mprg_def];
Addsimps (map simp_of_act
[cmd0U_def, cmd1U_def, cmd2U_def, cmd3U_def, cmd4U_def,
@@ -21,13 +22,13 @@
(*Simplification for records*)
Addsimps (thms"state.update_defs");
-Goal "Invariant Mprg invariantU";
+Goal "Mprg : Invariant invariantU";
by (rtac InvariantI 1);
by (constrains_tac 2);
by Auto_tac;
qed "invariantU";
-Goal "Invariant Mprg invariantV";
+Goal "Mprg : Invariant invariantV";
by (rtac InvariantI 1);
by (constrains_tac 2);
by Auto_tac;
@@ -44,7 +45,7 @@
(*The bad invariant FAILS in cmd1V*)
-Goal "Invariant Mprg bad_invariantU";
+Goal "Mprg : Invariant bad_invariantU";
by (rtac InvariantI 1);
by (constrains_tac 2);
by (Force_tac 1);
@@ -77,44 +78,44 @@
(*** Progress for U ***)
-Goalw [Unless_def] "Unless Mprg {s. MM s=#2} {s. MM s=#3}";
+Goalw [Unless_def] "Mprg : Unless {s. MM s=#2} {s. MM s=#3}";
by (constrains_tac 1);
qed "U_F0";
-Goal "LeadsTo Mprg {s. MM s=#1} {s. PP s = VV s & MM s = #2}";
+Goal "Mprg : LeadsTo {s. MM s=#1} {s. PP s = VV s & MM s = #2}";
by (ensures_tac "cmd1U" 1);
qed "U_F1";
-Goal "LeadsTo Mprg {s. ~ PP s & MM s = #2} {s. MM s = #3}";
+Goal "Mprg : LeadsTo {s. ~ PP s & MM s = #2} {s. MM s = #3}";
by (cut_facts_tac [invariantU] 1);
by (ensures_tac "cmd2U" 1);
qed "U_F2";
-Goal "LeadsTo Mprg {s. MM s = #3} {s. PP s}";
+Goal "Mprg : LeadsTo {s. MM s = #3} {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 "LeadsTo Mprg {s. MM s = #2} {s. PP s}";
+Goal "Mprg : LeadsTo {s. MM s = #2} {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 "LeadsTo Mprg {s. MM s = #1} {s. PP s}";
+Goal "Mprg : LeadsTo {s. MM s = #1} {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 "LeadsTo Mprg {s. #1 <= MM s & MM s <= #3} {s. PP s}";
+Goal "Mprg : LeadsTo {s. #1 <= MM s & MM s <= #3} {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 "LeadsTo Mprg {s. UU s} {s. PP s}";
+Goal "Mprg : LeadsTo {s. UU s} {s. PP s}";
by (rtac ([invariantU, U_lemma123] MRS Invariant_LeadsTo_weaken) 1);
by Auto_tac;
qed "u_Leadsto_p";
@@ -123,45 +124,45 @@
(*** Progress for V ***)
-Goalw [Unless_def] "Unless Mprg {s. NN s=#2} {s. NN s=#3}";
+Goalw [Unless_def] "Mprg : Unless {s. NN s=#2} {s. NN s=#3}";
by (constrains_tac 1);
qed "V_F0";
-Goal "LeadsTo Mprg {s. NN s=#1} {s. PP s = (~ UU s) & NN s = #2}";
+Goal "Mprg : LeadsTo {s. NN s=#1} {s. PP s = (~ UU s) & NN s = #2}";
by (ensures_tac "cmd1V" 1);
qed "V_F1";
-Goal "LeadsTo Mprg {s. PP s & NN s = #2} {s. NN s = #3}";
+Goal "Mprg : LeadsTo {s. PP s & NN s = #2} {s. NN s = #3}";
by (cut_facts_tac [invariantV] 1);
by (ensures_tac "cmd2V" 1);
qed "V_F2";
-Goal "LeadsTo Mprg {s. NN s = #3} {s. ~ PP s}";
+Goal "Mprg : LeadsTo {s. NN s = #3} {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 "LeadsTo Mprg {s. NN s = #2} {s. ~ PP s}";
+Goal "Mprg : LeadsTo {s. NN s = #2} {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 "LeadsTo Mprg {s. NN s = #1} {s. ~ PP s}";
+Goal "Mprg : LeadsTo {s. NN s = #1} {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 "LeadsTo Mprg {s. #1 <= NN s & NN s <= #3} {s. ~ PP s}";
+Goal "Mprg : LeadsTo {s. #1 <= NN s & NN s <= #3} {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 "LeadsTo Mprg {s. VV s} {s. ~ PP s}";
+Goal "Mprg : LeadsTo {s. VV s} {s. ~ PP s}";
by (rtac ([invariantV, V_lemma123] MRS Invariant_LeadsTo_weaken) 1);
by Auto_tac;
qed "v_Leadsto_not_p";
@@ -170,7 +171,7 @@
(** Absence of starvation **)
(*Misra's F6*)
-Goal "LeadsTo Mprg {s. MM s = #1} {s. MM s = #3}";
+Goal "Mprg : LeadsTo {s. MM s = #1} {s. MM s = #3}";
by (rtac LeadsTo_Un_duplicate 1);
by (rtac LeadsTo_cancel2 1);
by (rtac U_F2 2);
@@ -184,7 +185,7 @@
(*The same for V*)
-Goal "LeadsTo Mprg {s. NN s = #1} {s. NN s = #3}";
+Goal "Mprg : LeadsTo {s. NN s = #1} {s. NN s = #3}";
by (rtac LeadsTo_Un_duplicate 1);
by (rtac LeadsTo_cancel2 1);
by (rtac V_F2 2);
--- a/src/HOL/UNITY/NSP_Bad.ML Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/NSP_Bad.ML Thu Oct 15 11:35:07 1998 +0200
@@ -24,6 +24,7 @@
Addsimps [Nprg_def RS def_prg_simps];
+
(*A "possibility property": there are traces that reach the end*)
Goal "A ~= B ==> EX NB. EX s: reachable Nprg. \
\ Says A B (Crypt (pubK B) (Nonce NB)) : set s";
@@ -32,7 +33,7 @@
by (res_inst_tac [("act", "NS2")] reachable.Acts 3);
by (res_inst_tac [("act", "NS1")] reachable.Acts 4);
by (rtac reachable.Init 5);
-by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [Nprg_def])));
by (REPEAT_FIRST (rtac exI ));
by possibility_tac;
result();
@@ -66,7 +67,7 @@
(*Spy never sees another agent's private key! (unless it's bad at start)*)
(*
- Goal "Invariant Nprg {s. (Key (priK A) : parts (spies s)) = (A : bad)}";
+ Goal "Nprg : Invariant {s. (Key (priK A) : parts (spies s)) = (A : bad)}";
by (rtac InvariantI 1);
by (Force_tac 1);
by (constrains_tac 1);
--- a/src/HOL/UNITY/Network.ML Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Network.ML Thu Oct 15 11:35:07 1998 +0200
@@ -10,15 +10,15 @@
val [rsA, rsB, sent_nondec, rcvd_nondec, rcvd_idle, sent_idle] =
Goalw [stable_def]
- "[| !! m. stable Acts {s. s(Bproc,Rcvd) <= s(Aproc,Sent)}; \
-\ !! m. stable Acts {s. s(Aproc,Rcvd) <= s(Bproc,Sent)}; \
-\ !! m proc. stable Acts {s. m <= s(proc,Sent)}; \
-\ !! n proc. stable Acts {s. n <= s(proc,Rcvd)}; \
-\ !! m proc. constrains Acts {s. s(proc,Idle) = 1 & s(proc,Rcvd) = m} \
+ "[| !! m. F : stable {s. s(Bproc,Rcvd) <= s(Aproc,Sent)}; \
+\ !! 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} \
\ {s. s(proc,Rcvd) = m --> s(proc,Idle) = 1}; \
-\ !! n proc. constrains Acts {s. s(proc,Idle) = 1 & s(proc,Sent) = n} \
+\ !! n proc. F : constrains {s. s(proc,Idle) = 1 & s(proc,Sent) = n} \
\ {s. s(proc,Sent) = n} \
-\ |] ==> stable Acts {s. s(Aproc,Idle) = 1 & s(Bproc,Idle) = 1 & \
+\ |] ==> F : stable {s. s(Aproc,Idle) = 1 & s(Bproc,Idle) = 1 & \
\ s(Aproc,Sent) = s(Bproc,Rcvd) & \
\ s(Bproc,Sent) = s(Aproc,Rcvd) & \
\ s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}";
--- a/src/HOL/UNITY/ROOT.ML Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/ROOT.ML Thu Oct 15 11:35:07 1998 +0200
@@ -10,6 +10,10 @@
writeln"Root file for HOL/UNITY";
set proof_timing;
+
+loadpath := "../Lex" :: !loadpath; (*to find Prefix.thy*)
+time_use_thy"UNITY";
+
time_use_thy "Deadlock";
time_use_thy "WFair";
time_use_thy "Common";
@@ -22,9 +26,7 @@
time_use_thy "Handshake";
time_use_thy "Lift";
time_use_thy "Comp";
+time_use_thy "Client";
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/Reach.ML Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Reach.ML Thu Oct 15 11:35:07 1998 +0200
@@ -19,7 +19,8 @@
AddSEs [ifE];
-Addsimps [Rprg_def RS def_prg_simps];
+Addsimps [Rprg_def RS def_prg_Init];
+program_defs_ref := [Rprg_def];
Addsimps [simp_of_act asgt_def];
@@ -28,7 +29,7 @@
Addsimps [simp_of_set reach_invariant_def];
-Goal "Invariant Rprg reach_invariant";
+Goal "Rprg : Invariant reach_invariant";
by (rtac InvariantI 1);
by Auto_tac; (*for the initial state; proof of stability remains*)
by (constrains_tac 1);
@@ -48,20 +49,20 @@
by Auto_tac;
qed "fixedpoint_invariant_correct";
-Goalw [FP_def, fixedpoint_def, stable_def, constrains_def]
- "FP (Acts Rprg) <= fixedpoint";
+Goalw [FP_def, fixedpoint_def, stable_def, constrains_def, Rprg_def]
+ "FP Rprg <= fixedpoint";
by Auto_tac;
by (asm_full_simp_tac (simpset() addsimps [Image_singleton, image_iff]) 1);
by (dtac fun_cong 1);
by Auto_tac;
val lemma1 = result();
-Goalw [FP_def, fixedpoint_def, stable_def, constrains_def]
- "fixedpoint <= FP (Acts Rprg)";
+Goalw [FP_def, fixedpoint_def, stable_def, constrains_def, Rprg_def]
+ "fixedpoint <= FP Rprg";
by (auto_tac (claset() addSIs [ext], simpset()));
val lemma2 = result();
-Goal "FP (Acts Rprg) = fixedpoint";
+Goal "FP Rprg = fixedpoint";
by (rtac ([lemma1,lemma2] MRS equalityI) 1);
qed "FP_fixedpoint";
@@ -74,7 +75,7 @@
Goal "- fixedpoint = (UN (u,v): edges. {s. s u & ~ s v})";
by (simp_tac (simpset() addsimps
- ([Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym])) 1);
+ ([Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym, Rprg_def])) 1);
by Auto_tac;
by (rtac fun_upd_idem 1);
by (auto_tac (claset(),simpset() addsimps [fun_upd_idem_iff]));
@@ -106,7 +107,7 @@
simpset() addsimps [fun_upd_idem]));
qed "metric_le";
-Goal "LeadsTo Rprg ((metric-``{m}) - fixedpoint) (metric-``(lessThan m))";
+Goal "Rprg : LeadsTo ((metric-``{m}) - fixedpoint) (metric-``(lessThan m))";
by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1);
by (rtac LeadsTo_UN 1);
by Auto_tac;
@@ -118,7 +119,7 @@
simpset()));
qed "LeadsTo_Diff_fixedpoint";
-Goal "LeadsTo Rprg (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)";
+Goal "Rprg : LeadsTo (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)";
by (rtac ([LeadsTo_Diff_fixedpoint RS LeadsTo_weaken_R,
subset_imp_LeadsTo] MRS LeadsTo_Diff) 1);
by Auto_tac;
@@ -126,13 +127,13 @@
(*Execution in any state leads to a fixedpoint (i.e. can terminate)*)
-Goal "LeadsTo Rprg UNIV fixedpoint";
+Goal "Rprg : LeadsTo UNIV fixedpoint";
by (rtac LessThan_induct 1);
by Auto_tac;
by (rtac LeadsTo_Un_fixedpoint 1);
qed "LeadsTo_fixedpoint";
-Goal "LeadsTo Rprg UNIV { %v. (init, v) : edges^* }";
+Goal "Rprg : LeadsTo UNIV { %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 Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML Thu Oct 15 11:35:07 1998 +0200
@@ -6,23 +6,21 @@
LeadsTo relation, restricted to the set of reachable states.
*)
-(*Map its type, ['a program, 'a set, 'a set] => bool, to just 'a*)
-Blast.overloaded ("SubstAx.LeadsTo",
- HOLogic.dest_setT o domain_type o range_type);
+overload_1st_set "SubstAx.LeadsTo";
(*** Specialized laws for handling invariants ***)
(** Conjoining a safety property **)
-Goal "[| reachable F <= C; LeadsTo F (C Int A) A' |] \
-\ ==> LeadsTo F A A'";
+Goal "[| reachable F <= C; F : LeadsTo (C Int A) A' |] \
+\ ==> F : LeadsTo A A'";
by (asm_full_simp_tac
(simpset() addsimps [LeadsTo_def, Int_absorb2, Int_assoc RS sym]) 1);
qed "reachable_LeadsToI";
-Goal "[| reachable F <= C; LeadsTo F A A' |] \
-\ ==> LeadsTo F A (C Int A')";
+Goal "[| reachable F <= C; F : LeadsTo A A' |] \
+\ ==> F : LeadsTo A (C Int A')";
by (asm_full_simp_tac
(simpset() addsimps [LeadsTo_def, Int_absorb2,
Int_assoc RS sym]) 1);
@@ -31,11 +29,11 @@
(** Conjoining an invariant **)
-(* [| Invariant F C; LeadsTo F (C Int A) A' |] ==> LeadsTo F A A' *)
+(* [| Invariant F C; F : LeadsTo (C Int A) A' |] ==> F : LeadsTo A A' *)
bind_thm ("Invariant_LeadsToI",
Invariant_includes_reachable RS reachable_LeadsToI);
-(* [| Invariant F C; LeadsTo F A A' |] ==> LeadsTo F A (C Int A') *)
+(* [| Invariant F C; F : LeadsTo A A' |] ==> F : LeadsTo A (C Int A') *)
bind_thm ("Invariant_LeadsToD",
Invariant_includes_reachable RS reachable_LeadsToD);
@@ -44,55 +42,54 @@
(*** Introduction rules: Basis, Trans, Union ***)
-Goal "leadsTo (Acts F) A B ==> LeadsTo F A B";
+Goal "F : leadsTo A B ==> F : LeadsTo 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 F A B; LeadsTo F B C |] ==> LeadsTo F A C";
+Goal "[| F : LeadsTo A B; F : LeadsTo B C |] ==> F : LeadsTo 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 F A B) ==> LeadsTo F (Union S) B";
+val prems = Goalw [LeadsTo_def]
+ "(!!A. A : S ==> F : LeadsTo A B) ==> F : LeadsTo (Union S) B";
by (Simp_tac 1);
by (stac Int_Union 1);
-by (blast_tac (claset() addIs [leadsTo_UN,
- simplify (simpset()) prem]) 1);
+by (blast_tac (claset() addIs [leadsTo_UN] addDs prems) 1);
qed "LeadsTo_Union";
(*** Derived rules ***)
-Goal "LeadsTo F A UNIV";
-by (asm_simp_tac (simpset() addsimps [LeadsTo_def,
- Int_lower1 RS subset_imp_leadsTo]) 1);
+Goal "F : LeadsTo 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 F A (A' Un A') ==> LeadsTo F A A'";
+Goal "F : LeadsTo A (A' Un A') ==> F : LeadsTo A A'";
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
qed "LeadsTo_Un_duplicate";
-Goal "LeadsTo F A (A' Un C Un C) ==> LeadsTo F A (A' Un C)";
+Goal "F : LeadsTo A (A' Un C Un C) ==> F : LeadsTo 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 F (A i) B) ==> LeadsTo F (UN i:I. A i) B";
+Goal "(!!i. i : I ==> F : LeadsTo (A i) B) ==> F : LeadsTo (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 F A C; LeadsTo F B C |] ==> LeadsTo F (A Un B) C";
+Goal "[| F : LeadsTo A C; F : LeadsTo B C |] ==> F : LeadsTo (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 F A B";
+Goal "A <= B ==> F : LeadsTo 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 +97,39 @@
bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo);
Addsimps [empty_LeadsTo];
-Goal "[| LeadsTo F A A'; A' <= B' |] ==> LeadsTo F A B'";
+Goal "[| F : LeadsTo A A'; A' <= B' |] ==> F : LeadsTo 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 F A A'; B <= A |] \
-\ ==> LeadsTo F B A'";
+Goal "[| F : LeadsTo A A'; B <= A |] \
+\ ==> F : LeadsTo 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 F A A'; \
+Goal "[| F : LeadsTo A A'; \
\ B <= A; A' <= B' |] \
-\ ==> LeadsTo F B B'";
+\ ==> F : LeadsTo B B'";
by (blast_tac (claset() addIs [LeadsTo_weaken_R, LeadsTo_weaken_L,
LeadsTo_Trans]) 1);
qed "LeadsTo_weaken";
-Goal "[| reachable F <= C; LeadsTo F A A'; \
+Goal "[| reachable F <= C; F : LeadsTo A A'; \
\ C Int B <= A; C Int A' <= B' |] \
-\ ==> LeadsTo F B B'";
+\ ==> F : LeadsTo 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 F A B |] ==> LeadsTo F (A Un B) B";
+Goal "[| F : LeadsTo A B |] ==> F : LeadsTo (A Un B) B";
by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo]) 1);
qed "LeadsTo_Un_post";
-Goal "[| LeadsTo F A B; LeadsTo F B C |] \
-\ ==> LeadsTo F (A Un B) C";
+Goal "[| F : LeadsTo A B; F : LeadsTo B C |] \
+\ ==> F : LeadsTo (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 +137,33 @@
(** Distributive laws **)
-Goal "LeadsTo F (A Un B) C = (LeadsTo F A C & LeadsTo F B C)";
+Goal "(F : LeadsTo (A Un B) C) = (F : LeadsTo A C & F : LeadsTo B C)";
by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
qed "LeadsTo_Un_distrib";
-Goal "LeadsTo F (UN i:I. A i) B = (ALL i : I. LeadsTo F (A i) B)";
+Goal "(F : LeadsTo (UN i:I. A i) B) = (ALL i : I. F : LeadsTo (A i) B)";
by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
qed "LeadsTo_UN_distrib";
-Goal "LeadsTo F (Union S) B = (ALL A : S. LeadsTo F A B)";
+Goal "(F : LeadsTo (Union S) B) = (ALL A : S. F : LeadsTo A B)";
by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1);
qed "LeadsTo_Union_distrib";
(** More rules using the premise "Invariant F" **)
-Goalw [LeadsTo_def, Constrains_def]
- "[| Constrains F (A-A') (A Un A'); transient (Acts F) (A-A') |] \
-\ ==> LeadsTo F A A'";
+Goal "[| F : Constrains (A-A') (A Un A'); F : transient (A-A') |] \
+\ ==> F : LeadsTo A 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);
by (blast_tac (claset() addIs [constrains_weaken]) 1);
qed "LeadsTo_Basis";
-Goal "[| Invariant F INV; \
-\ Constrains F (INV Int (A-A')) (A Un A'); \
-\ transient (Acts F) (INV Int (A-A')) |] \
-\ ==> LeadsTo F A A'";
+Goal "[| F : Invariant INV; \
+\ F : Constrains (INV Int (A-A')) (A Un A'); \
+\ F : transient (INV Int (A-A')) |] \
+\ ==> F : LeadsTo A A'";
by (rtac Invariant_LeadsToI 1);
by (assume_tac 1);
by (rtac LeadsTo_Basis 1);
@@ -174,10 +171,9 @@
by (blast_tac (claset() addIs [Invariant_ConstrainsD RS Constrains_weaken]) 1);
qed "Invariant_LeadsTo_Basis";
-Goal "[| Invariant F INV; \
-\ LeadsTo F A A'; \
-\ INV Int B <= A; INV Int A' <= B' |] \
-\ ==> LeadsTo F B B'";
+Goal "[| F : Invariant INV; \
+\ F : LeadsTo A A'; INV Int B <= A; INV Int A' <= B' |] \
+\ ==> F : LeadsTo B B'";
by (REPEAT (ares_tac [Invariant_includes_reachable,
reachable_LeadsTo_weaken] 1));
qed "Invariant_LeadsTo_weaken";
@@ -185,17 +181,15 @@
(*Set difference: maybe combine with leadsTo_weaken_L??
This is the most useful form of the "disjunction" rule*)
-Goal "[| LeadsTo F (A-B) C; LeadsTo F (A Int B) C |] \
-\ ==> LeadsTo F A C";
+Goal "[| F : LeadsTo (A-B) C; F : LeadsTo (A Int B) C |] \
+\ ==> F : LeadsTo A C";
by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
qed "LeadsTo_Diff";
-
-
val prems =
-Goal "(!! i. i:I ==> LeadsTo F (A i) (A' i)) \
-\ ==> LeadsTo F (UN i:I. A i) (UN i:I. A' i)";
+Goal "(!! i. i:I ==> F : LeadsTo (A i) (A' i)) \
+\ ==> F : LeadsTo (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);
@@ -204,22 +198,22 @@
(*Version with no index set*)
val prems =
-Goal "(!! i. LeadsTo F (A i) (A' i)) \
-\ ==> LeadsTo F (UN i. A i) (UN i. A' i)";
+Goal "(!! i. F : LeadsTo (A i) (A' i)) \
+\ ==> F : LeadsTo (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 F (A i) (A' i) \
-\ ==> LeadsTo F (UN i. A i) (UN i. A' i)";
+Goal "ALL i. F : LeadsTo (A i) (A' i) \
+\ ==> F : LeadsTo (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 F A A'; LeadsTo F B B' |] \
-\ ==> LeadsTo F (A Un B) (A' Un B')";
+Goal "[| F : LeadsTo A A'; F : LeadsTo B B' |] \
+\ ==> F : LeadsTo (A Un B) (A' Un B')";
by (blast_tac (claset() addIs [LeadsTo_Un,
LeadsTo_weaken_R]) 1);
qed "LeadsTo_Un_Un";
@@ -227,38 +221,37 @@
(** The cancellation law **)
-Goal "[| LeadsTo F A (A' Un B); LeadsTo F B B' |] \
-\ ==> LeadsTo F A (A' Un B')";
+Goal "[| F : LeadsTo A (A' Un B); F : LeadsTo B B' |] \
+\ ==> F : LeadsTo A (A' Un B')";
by (blast_tac (claset() addIs [LeadsTo_Un_Un,
subset_imp_LeadsTo, LeadsTo_Trans]) 1);
qed "LeadsTo_cancel2";
-Goal "[| LeadsTo F A (A' Un B); LeadsTo F (B-A') B' |] \
-\ ==> LeadsTo F A (A' Un B')";
+Goal "[| F : LeadsTo A (A' Un B); F : LeadsTo (B-A') B' |] \
+\ ==> F : LeadsTo A (A' Un B')";
by (rtac LeadsTo_cancel2 1);
by (assume_tac 2);
by (ALLGOALS Asm_simp_tac);
qed "LeadsTo_cancel_Diff2";
-Goal "[| LeadsTo F A (B Un A'); LeadsTo F B B' |] \
-\ ==> LeadsTo F A (B' Un A')";
+Goal "[| F : LeadsTo A (B Un A'); F : LeadsTo B B' |] \
+\ ==> F : LeadsTo 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 F A (B Un A'); LeadsTo F (B-A') B' |] \
-\ ==> LeadsTo F A (B' Un A')";
+Goal "[| F : LeadsTo A (B Un A'); F : LeadsTo (B-A') B' |] \
+\ ==> F : LeadsTo A (B' Un A')";
by (rtac LeadsTo_cancel1 1);
by (assume_tac 2);
by (ALLGOALS Asm_simp_tac);
qed "LeadsTo_cancel_Diff1";
-
(** The impossibility law **)
(*The set "A" may be non-empty, but it contains no reachable states*)
-Goal "LeadsTo F A {} ==> reachable F Int A = {}";
+Goal "F : LeadsTo A {} ==> reachable F Int A = {}";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (etac leadsTo_empty 1);
qed "LeadsTo_empty";
@@ -267,32 +260,33 @@
(** PSP: Progress-Safety-Progress **)
(*Special case of PSP: Misra's "stable conjunction"*)
-Goal "[| LeadsTo F A A'; Stable F B |] ==> LeadsTo F (A Int B) (A' Int B)";
+Goal "[| F : LeadsTo A A'; F : Stable B |] \
+\ ==> F : LeadsTo (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 F A A'; Stable F B |] \
-\ ==> LeadsTo F (B Int A) (B Int A')";
+Goal "[| F : LeadsTo A A'; F : Stable B |] \
+\ ==> F : LeadsTo (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 F A A'; Constrains F B B' |] \
-\ ==> LeadsTo F (A Int B) ((A' Int B) Un (B' - B))";
+ "[| F : LeadsTo A A'; F : Constrains B B' |] \
+\ ==> F : LeadsTo (A Int B) ((A' Int B) Un (B' - B))";
by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1);
qed "PSP";
-Goal "[| LeadsTo F A A'; Constrains F B B' |] \
-\ ==> LeadsTo F (B Int A) ((B Int A') Un (B' - B))";
+Goal "[| F : LeadsTo A A'; F : Constrains B B' |] \
+\ ==> F : LeadsTo (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 F A A'; Unless F B B' |] \
-\ ==> LeadsTo F (A Int B) ((A' Int B) Un B')";
+ "[| F : LeadsTo A A'; F : Unless B B' |] \
+\ ==> F : LeadsTo (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,
@@ -304,20 +298,19 @@
(** Meta or object quantifier ????? **)
Goal "[| wf r; \
-\ ALL m. LeadsTo F (A Int f-``{m}) \
+\ ALL m. F : LeadsTo (A Int f-``{m}) \
\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
-\ ==> LeadsTo F A B";
+\ ==> F : LeadsTo A B";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (etac leadsTo_wf_induct 1);
-by (Simp_tac 2);
by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
qed "LeadsTo_wf_induct";
Goal "[| wf r; \
-\ ALL m:I. LeadsTo F (A Int f-``{m}) \
+\ ALL m:I. F : LeadsTo (A Int f-``{m}) \
\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
-\ ==> LeadsTo F A ((A - (f-``I)) Un B)";
+\ ==> F : LeadsTo A ((A - (f-``I)) Un B)";
by (etac LeadsTo_wf_induct 1);
by Safe_tac;
by (case_tac "m:I" 1);
@@ -326,9 +319,9 @@
qed "Bounded_induct";
-Goal "[| ALL m. LeadsTo F (A Int f-``{m}) \
+Goal "[| ALL m. F : LeadsTo (A Int f-``{m}) \
\ ((A Int f-``(lessThan m)) Un B) |] \
-\ ==> LeadsTo F A B";
+\ ==> F : LeadsTo A B";
by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
by (Asm_simp_tac 1);
qed "LessThan_induct";
@@ -336,26 +329,26 @@
(*Integer version. Could generalize from #0 to any lower bound*)
val [reach, prem] =
Goal "[| reachable F <= {s. #0 <= f s}; \
-\ !! z. LeadsTo F (A Int {s. f s = z}) \
+\ !! z. F : LeadsTo (A Int {s. f s = z}) \
\ ((A Int {s. f s < z}) Un B) |] \
-\ ==> LeadsTo F A B";
+\ ==> F : LeadsTo A 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). LeadsTo F (A Int f-``{m}) \
+Goal "[| ALL m:(greaterThan l). F : LeadsTo (A Int f-``{m}) \
\ ((A Int f-``(lessThan m)) Un B) |] \
-\ ==> LeadsTo F A ((A Int (f-``(atMost l))) Un B)";
+\ ==> F : LeadsTo 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 F (A Int f-``{m}) \
+Goal "[| ALL m:(lessThan l). F : LeadsTo (A Int f-``{m}) \
\ ((A Int f-``(greaterThan m)) Un B) |] \
-\ ==> LeadsTo F A ((A Int (f-``(atLeast l))) Un B)";
+\ ==> F : LeadsTo 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);
@@ -368,27 +361,27 @@
(*** Completion: Binary and General Finite versions ***)
-Goal "[| LeadsTo F A A'; Stable F A'; \
-\ LeadsTo F B B'; Stable F B' |] \
-\ ==> LeadsTo F (A Int B) (A' Int B')";
+Goal "[| F : LeadsTo A A'; F : Stable A'; \
+\ F : LeadsTo B B'; F : Stable B' |] \
+\ ==> F : LeadsTo (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 F (A i) (A' i)) --> \
-\ (ALL i:I. Stable F (A' i)) --> \
-\ LeadsTo F (INT i:I. A i) (INT i:I. A' i)";
+\ ==> (ALL i:I. F : LeadsTo (A i) (A' i)) --> \
+\ (ALL i:I. F : Stable (A' i)) --> \
+\ F : LeadsTo (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 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)";
+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)";
by (full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_def,
Int_Un_distrib]) 1);
by (blast_tac (claset() addIs [completion, leadsTo_weaken]) 1);
@@ -396,9 +389,9 @@
Goal "[| finite I |] \
-\ ==> (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)";
+\ ==> (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)";
by (etac finite_induct 1);
by (ALLGOALS Asm_simp_tac);
by (Clarify_tac 1);
@@ -414,6 +407,8 @@
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*)
+ simp_tac (simpset() addsimps !program_defs_ref) 2,
res_inst_tac [("act", sact)] transient_mem 2,
(*simplify the command's domain*)
simp_tac (simpset() addsimps [Domain_def]) 3,
--- a/src/HOL/UNITY/SubstAx.thy Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.thy Thu Oct 15 11:35:07 1998 +0200
@@ -10,9 +10,7 @@
constdefs
- LeadsTo :: "['a program, 'a set, 'a set] => bool"
- "LeadsTo F A B ==
- leadsTo (Acts F)
- (reachable F Int A)
- (reachable F Int B)"
+ LeadsTo :: "['a set, 'a set] => 'a program set"
+ "LeadsTo A B == {F. F : leadsTo (reachable F Int A)
+ (reachable F Int B)}"
end
--- a/src/HOL/UNITY/Token.ML Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Token.ML Thu Oct 15 11:35:07 1998 +0200
@@ -32,9 +32,9 @@
val nodeOrder_def = (thm "nodeOrder_def");
val next_def = (thm "next_def");
-AddIffs [thm "N_positive", thm"skip"];
+AddIffs [thm "N_positive"];
-Goalw [stable_def] "stable acts (-(E i) Un (HasTok i))";
+Goalw [stable_def] "F : stable (-(E i) Un (HasTok i))";
by (rtac constrains_weaken 1);
by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1);
by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
@@ -70,7 +70,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 |] ==> \
-\ leadsTo acts (HasTok i) ({s. (token s, i) : nodeOrder j} Un HasTok j)";
+\ F : leadsTo (HasTok i) ({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);
@@ -81,7 +81,7 @@
(*Chapter 4 variant, the one actually used below.*)
Goal "[| i<N; j<N; i~=j |] \
-\ ==> leadsTo acts (HasTok i) {s. (token s, i) : nodeOrder j}";
+\ ==> F : leadsTo (HasTok i) {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);
@@ -94,7 +94,7 @@
(*Misra's TR9: the token reaches an arbitrary node*)
-Goal "j<N ==> leadsTo acts {s. token s < N} (HasTok j)";
+Goal "j<N ==> F : leadsTo {s. token s < N} (HasTok j)";
by (rtac leadsTo_weaken_R 1);
by (res_inst_tac [("I", "-{j}"), ("f", "token"), ("B", "{}")]
(wf_nodeOrder RS bounded_induct) 1);
@@ -108,7 +108,7 @@
qed "leadsTo_j";
(*Misra's TR8: a hungry process eventually eats*)
-Goal "j<N ==> leadsTo acts ({s. token s < N} Int H j) (E j)";
+Goal "j<N ==> F : leadsTo ({s. token s < N} Int H j) (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 Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Token.thy Thu Oct 15 11:35:07 1998 +0200
@@ -36,26 +36,24 @@
locale Token =
fixes
N :: nat (*number of nodes in the ring*)
- acts :: "(state*state)set set"
+ F :: state program
nodeOrder :: "nat => (nat*nat)set"
next :: nat => nat
assumes
N_positive "0<N"
- skip "Id: acts"
+ TR2 "!!i. F : constrains (T i) (T i Un H i)"
- TR2 "!!i. constrains acts (T i) (T i Un H i)"
+ TR3 "!!i. F : constrains (H i) (H i Un E i)"
- TR3 "!!i. constrains acts (H i) (H i Un E i)"
+ TR4 "!!i. F : constrains (H i - HasTok i) (H i)"
- TR4 "!!i. constrains acts (H i - HasTok i) (H i)"
-
- TR5 "!!i. constrains acts (HasTok i) (HasTok i Un Compl(E i))"
+ TR5 "!!i. F : constrains (HasTok i) (HasTok i Un Compl(E i))"
- TR6 "!!i. leadsTo acts (H i Int HasTok i) (E i)"
+ TR6 "!!i. F : leadsTo (H i Int HasTok i) (E i)"
- TR7 "!!i. leadsTo acts (HasTok i) (HasTok (next i))"
+ TR7 "!!i. F : leadsTo (HasTok i) (HasTok (next i))"
defines
nodeOrder_def
--- a/src/HOL/UNITY/Traces.ML Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Traces.ML Thu Oct 15 11:35:07 1998 +0200
@@ -43,8 +43,17 @@
qed "program_equalityI";
-(*** These three rules allow "lazy" definition expansion ***)
+(*** These rules allow "lazy" definition expansion ***)
+(*The program is not expanded, but its Init is*)
+val [rew] = goal thy
+ "[| F == mk_program (init,acts) |] \
+\ ==> Init F = init";
+by (rewtac rew);
+by Auto_tac;
+qed "def_prg_Init";
+
+(*The program is not expanded, but its Init and Acts are*)
val [rew] = goal thy
"[| F == mk_program (init,acts) |] \
\ ==> Init F = init & Acts F = insert Id acts";
@@ -52,6 +61,7 @@
by Auto_tac;
qed "def_prg_simps";
+(*An action is expanded only if a pair of states is being tested against it*)
val [rew] = goal thy
"[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'";
by (rewtac rew);
@@ -60,8 +70,9 @@
fun simp_of_act def = def RS def_act_simp;
+(*A set is expanded only if an element is being tested against it*)
val [rew] = goal thy
- "[| A == B |] ==> (x : A) = (x : B)";
+ "A == B ==> (x : A) = (x : B)";
by (rewtac rew);
by Auto_tac;
qed "def_set_simp";
@@ -77,11 +88,3 @@
by (etac reachable.induct 1);
by (ALLGOALS (blast_tac (claset() addIs reachable.intrs @ traces.intrs)));
qed "reachable_equiv_traces";
-
-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 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Traces.thy Thu Oct 15 11:35:07 1998 +0200
@@ -8,7 +8,7 @@
* reachable: the set of reachable states
*)
-Traces = UNITY +
+Traces = LessThan +
consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
--- a/src/HOL/UNITY/UNITY.ML Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/UNITY.ML Thu Oct 15 11:35:07 1998 +0200
@@ -14,154 +14,216 @@
(*** constrains ***)
-(*Map the type (anything => ('a set => anything) to just 'a*)
-fun overload_2nd_set s =
- Blast.overloaded (s, HOLogic.dest_setT o domain_type o range_type);
-
-overload_2nd_set "UNITY.constrains";
-overload_2nd_set "UNITY.stable";
-overload_2nd_set "UNITY.unless";
+overload_1st_set "UNITY.constrains";
+overload_1st_set "UNITY.stable";
+overload_1st_set "UNITY.unless";
val prems = Goalw [constrains_def]
- "(!!act s s'. [| act: acts; (s,s') : act; s: A |] ==> s': A') \
-\ ==> constrains acts A A'";
+ "(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A') \
+\ ==> F : constrains A A'";
by (blast_tac (claset() addIs prems) 1);
qed "constrainsI";
Goalw [constrains_def]
- "[| constrains acts A A'; act: acts; (s,s'): act; s: A |] ==> s': A'";
+ "[| F : constrains A A'; act: Acts F; (s,s'): act; s: A |] ==> s': A'";
by (Blast_tac 1);
qed "constrainsD";
-Goalw [constrains_def] "constrains acts {} B";
+Goalw [constrains_def] "F : constrains {} B";
by (Blast_tac 1);
qed "constrains_empty";
-Goalw [constrains_def] "constrains acts A UNIV";
+Goalw [constrains_def] "F : constrains A UNIV";
by (Blast_tac 1);
qed "constrains_UNIV";
AddIffs [constrains_empty, constrains_UNIV];
+(*monotonic in 2nd argument*)
Goalw [constrains_def]
- "[| constrains acts A A'; A'<=B' |] ==> constrains acts A B'";
+ "[| F : constrains A A'; A'<=B' |] ==> F : constrains A B'";
by (Blast_tac 1);
qed "constrains_weaken_R";
+(*anti-monotonic in 1st argument*)
Goalw [constrains_def]
- "[| constrains acts A A'; B<=A |] ==> constrains acts B A'";
+ "[| F : constrains A A'; B<=A |] ==> F : constrains B A'";
by (Blast_tac 1);
qed "constrains_weaken_L";
Goalw [constrains_def]
- "[| constrains acts A A'; B<=A; A'<=B' |] ==> constrains acts B B'";
+ "[| F : constrains A A'; B<=A; A'<=B' |] ==> F : constrains B B'";
by (Blast_tac 1);
qed "constrains_weaken";
(** Union **)
Goalw [constrains_def]
- "[| constrains acts A A'; constrains acts B B' |] \
-\ ==> constrains acts (A Un B) (A' Un B')";
+ "[| F : constrains A A'; F : constrains B B' |] \
+\ ==> F : constrains (A Un B) (A' Un B')";
by (Blast_tac 1);
qed "constrains_Un";
Goalw [constrains_def]
- "ALL i:I. constrains acts (A i) (A' i) \
-\ ==> constrains acts (UN i:I. A i) (UN i:I. A' i)";
+ "ALL i:I. F : constrains (A i) (A' i) \
+\ ==> F : constrains (UN i:I. A i) (UN i:I. A' i)";
by (Blast_tac 1);
qed "ball_constrains_UN";
Goalw [constrains_def]
- "[| ALL i. constrains acts (A i) (A' i) |] \
-\ ==> constrains acts (UN i. A i) (UN i. A' i)";
+ "[| ALL i. F : constrains (A i) (A' i) |] \
+\ ==> F : constrains (UN i. A i) (UN i. A' i)";
by (Blast_tac 1);
qed "all_constrains_UN";
(** Intersection **)
Goalw [constrains_def]
- "[| constrains acts A A'; constrains acts B B' |] \
-\ ==> constrains acts (A Int B) (A' Int B')";
+ "[| F : constrains A A'; F : constrains B B' |] \
+\ ==> F : constrains (A Int B) (A' Int B')";
by (Blast_tac 1);
qed "constrains_Int";
Goalw [constrains_def]
- "ALL i:I. constrains acts (A i) (A' i) \
-\ ==> constrains acts (INT i:I. A i) (INT i:I. A' i)";
+ "ALL i:I. F : constrains (A i) (A' i) \
+\ ==> F : constrains (INT i:I. A i) (INT i:I. A' i)";
by (Blast_tac 1);
qed "ball_constrains_INT";
Goalw [constrains_def]
- "[| ALL i. constrains acts (A i) (A' i) |] \
-\ ==> constrains acts (INT i. A i) (INT i. A' i)";
+ "[| ALL i. F : constrains (A i) (A' i) |] \
+\ ==> F : constrains (INT i. A i) (INT i. A' i)";
by (Blast_tac 1);
qed "all_constrains_INT";
-Goalw [constrains_def] "[| constrains acts A A'; Id: acts |] ==> A<=A'";
+Goalw [constrains_def] "[| F : constrains A A' |] ==> A<=A'";
by (Blast_tac 1);
qed "constrains_imp_subset";
Goalw [constrains_def]
- "[| Id: acts; constrains acts A B; constrains acts B C |] \
-\ ==> constrains acts A C";
+ "[| F : constrains A B; F : constrains B C |] \
+\ ==> F : constrains A C";
by (Blast_tac 1);
qed "constrains_trans";
(*** stable ***)
-Goalw [stable_def] "constrains acts A A ==> stable acts A";
+Goalw [stable_def] "F : constrains A A ==> F : stable A";
by (assume_tac 1);
qed "stableI";
-Goalw [stable_def] "stable acts A ==> constrains acts A A";
+Goalw [stable_def] "F : stable A ==> F : constrains A A";
by (assume_tac 1);
qed "stableD";
Goalw [stable_def]
- "[| stable acts A; stable acts A' |] ==> stable acts (A Un A')";
+ "[| F : stable A; F : stable A' |] ==> F : stable (A Un A')";
by (blast_tac (claset() addIs [constrains_Un]) 1);
qed "stable_Un";
Goalw [stable_def]
- "[| stable acts A; stable acts A' |] ==> stable acts (A Int A')";
+ "[| F : stable A; F : stable A' |] ==> F : stable (A Int A')";
by (blast_tac (claset() addIs [constrains_Int]) 1);
qed "stable_Int";
Goalw [stable_def, constrains_def]
- "[| stable acts C; constrains acts A (C Un A') |] \
-\ ==> constrains acts (C Un A) (C Un A')";
+ "[| F : stable C; F : constrains A (C Un A') |] \
+\ ==> F : constrains (C Un A) (C Un A')";
by (Blast_tac 1);
qed "stable_constrains_Un";
Goalw [stable_def, constrains_def]
- "[| stable acts C; constrains acts (C Int A) A' |] \
-\ ==> constrains acts (C Int A) (C Int A')";
+ "[| F : stable C; F : constrains (C Int A) A' |] \
+\ ==> F : constrains (C Int A) (C Int A')";
by (Blast_tac 1);
qed "stable_constrains_Int";
+Goal "Init F <= reachable F";
+by (blast_tac (claset() addIs reachable.intrs) 1);
+qed "Init_subset_reachable";
-(*The Elimination Theorem. The "free" m has become universally quantified!
- Should the premise be !!m instead of ALL m ? Would make it harder to use
- in forward proof.*)
+Goal "Acts G <= Acts F ==> G : stable (reachable F)";
+by (blast_tac (claset() addIs [stableI, constrainsI] @ reachable.intrs) 1);
+qed "stable_reachable";
+
+(*[| F : stable C; F : constrains (C Int A) A |] ==> F : stable (C Int A)*)
+bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
+
+
+(*** invariant & always ***)
+
+Goal "[| Init F<=A; F: stable A |] ==> F : invariant A";
+by (asm_simp_tac (simpset() addsimps [invariant_def]) 1);
+qed "invariantI";
+
+(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*)
+Goal "[| F : invariant A; F : invariant B |] ==> F : invariant (A Int B)";
+by (auto_tac (claset(), simpset() addsimps [invariant_def, stable_Int]));
+qed "invariant_Int";
+
+(*The set of all reachable states is an invariant...*)
+Goal "F : invariant (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 "F : invariant A ==> reachable F <= A";
+by (full_simp_tac
+ (simpset() addsimps [stable_def, constrains_def, invariant_def]) 1);
+by (rtac subsetI 1);
+by (etac reachable.induct 1);
+by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
+qed "invariant_includes_reachable";
+
+Goalw [always_def] "always A = (UN I: Pow A. invariant I)";
+by (blast_tac (claset() addIs [invariantI, impOfSubs Init_subset_reachable,
+ stable_reachable,
+ impOfSubs invariant_includes_reachable]) 1);
+qed "always_eq_UN_invariant";
+
+Goal "F : always A = (EX I. F: invariant I & I <= A)";
+by (simp_tac (simpset() addsimps [always_eq_UN_invariant]) 1);
+by (Blast_tac 1);
+qed "always_iff_ex_invariant";
+
+
+(*** increasing ***)
+
+Goalw [increasing_def, stable_def, constrains_def]
+ "increasing f <= increasing (length o f)";
+by Auto_tac;
+by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1);
+qed "increasing_length";
+
+Goalw [increasing_def]
+ "increasing f <= {F. ALL z::nat. F: stable {s. z < f s}}";
+by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
+by (Blast_tac 1);
+qed "increasing_less";
+
+
+(** The Elimination Theorem. The "free" m has become universally quantified!
+ Should the premise be !!m instead of ALL m ? Would make it harder to use
+ in forward proof. **)
+
Goalw [constrains_def]
- "[| ALL m. constrains acts {s. s x = m} (B m) |] \
-\ ==> constrains acts {s. s x : M} (UN m:M. B m)";
+ "[| ALL m. F : constrains {s. s x = m} (B m) |] \
+\ ==> F : constrains {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]
- "(ALL m. constrains acts {m} (B m)) ==> constrains acts M (UN m:M. B m)";
+ "(ALL m. F : constrains {m} (B m)) ==> F : constrains M (UN m:M. B m)";
by (Blast_tac 1);
qed "elimination_sing";
Goalw [constrains_def]
- "[| constrains acts A (A' Un B); constrains acts B B'; Id: acts |] \
-\ ==> constrains acts A (A' Un B')";
+ "[| F : constrains A (A' Un B); F : constrains B B' |] \
+\ ==> F : constrains A (A' Un B')";
by (Blast_tac 1);
qed "constrains_cancel";
@@ -170,11 +232,11 @@
(*** Theoretical Results from Section 6 ***)
Goalw [constrains_def, strongest_rhs_def]
- "constrains acts A (strongest_rhs acts A )";
+ "F : constrains A (strongest_rhs F A )";
by (Blast_tac 1);
qed "constrains_strongest_rhs";
Goalw [constrains_def, strongest_rhs_def]
- "constrains acts A B ==> strongest_rhs acts A <= B";
+ "F : constrains A B ==> strongest_rhs F A <= B";
by (Blast_tac 1);
qed "strongest_rhs_is_strongest";
--- a/src/HOL/UNITY/UNITY.thy Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/UNITY.thy Thu Oct 15 11:35:07 1998 +0200
@@ -8,20 +8,33 @@
From Misra, "A Logic for Concurrent Programming", 1994
*)
-UNITY = LessThan +
+UNITY = Traces + Prefix +
constdefs
- constrains :: "[('a * 'a)set set, 'a set, 'a set] => bool"
- "constrains acts A B == ALL act:acts. act^^A <= B"
+ 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)set set => 'a set => bool"
- "stable acts A == constrains acts A 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 :: "[('a * 'a)set set, 'a set] => 'a set"
- "strongest_rhs acts A == Inter {B. constrains acts A B}"
+ (*The traditional word for inductive properties. Anyway, INDUCTIVE is
+ reserved!*)
+ invariant :: "'a set => 'a program set"
+ "invariant A == {F. Init F <= A} Int stable A"
- unless :: "[('a * 'a)set set, 'a set, 'a set] => bool"
- "unless acts A B == constrains acts (A-B) (A Un B)"
+ (*Safety properties*)
+ always :: "'a set => 'a program set"
+ "always A == {F. reachable F <= A}"
+
+ (*Polymorphic in both states and the meaning of <= *)
+ increasing :: "['a => 'b::{ord}] => 'a program set"
+ "increasing f == INT z. stable {s. z <= f s}"
end
--- a/src/HOL/UNITY/Union.ML Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Union.ML Thu Oct 15 11:35:07 1998 +0200
@@ -9,10 +9,16 @@
*)
-Goal "Init (F Join G) = Init F Int Init G";
-by (simp_tac (simpset() addsimps [Join_def]) 1);
+Goal "Init SKIP = UNIV";
+by (simp_tac (simpset() addsimps [SKIP_def]) 1);
qed "Init_SKIP";
+Goal "Acts SKIP = {Id}";
+by (simp_tac (simpset() addsimps [SKIP_def]) 1);
+qed "Acts_SKIP";
+
+Addsimps [Init_SKIP, Acts_SKIP];
+
Goal "Init (F Join G) = Init F Int Init G";
by (simp_tac (simpset() addsimps [Join_def]) 1);
qed "Init_Join";
@@ -79,14 +85,13 @@
Goalw [constrains_def, JOIN_def]
"I ~= {} ==> \
-\ constrains (Acts (JN i:I. F i)) A B = \
-\ (ALL i:I. constrains (Acts (F i)) A B)";
+\ (JN i:I. F i) : constrains A B = (ALL i:I. F i : constrains A B)";
by (Simp_tac 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 "F Join G : constrains A B = \
+\ (F : constrains A B & G : constrains A B)";
by (auto_tac
(claset(),
simpset() addsimps [constrains_def, Join_def]));
@@ -97,35 +102,35 @@
reachable F and reachable G
Goalw [Constrains_def]
- "Constrains (JN i:I. F i) A B = (ALL i:I. Constrains (F i) A B)";
+ "(JN i:I. F i) : Constrains A B = (ALL i:I. F i : Constrains A B)";
by (simp_tac (simpset() addsimps [constrains_JN]) 1);
by (Blast_tac 1);
qed "Constrains_JN";
-Goal "Constrains (F Join G) A B = (Constrains F A B & Constrains G A B)";
+Goal "F Join G : Constrains A B = (Constrains F A B & Constrains G A B)";
by (auto_tac
(claset(),
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')";
+Goal "[| F : constrains A A'; G : constrains B B' |] \
+\ ==> F Join G : constrains (A Int B) (A' Un B')";
by (simp_tac (simpset() addsimps [constrains_Join]) 1);
by (blast_tac (claset() addIs [constrains_weaken]) 1);
qed "constrains_Join_weaken";
Goal "I ~= {} ==> \
-\ stable (Acts (JN i:I. F i)) A = (ALL i:I. stable (Acts (F i)) A)";
+\ (JN i:I. F i) : stable A = (ALL i:I. F i : stable A)";
by (asm_simp_tac (simpset() addsimps [stable_def, constrains_JN]) 1);
qed "stable_JN";
-Goal "stable (Acts (F Join G)) A = \
-\ (stable (Acts F) A & stable (Acts G) A)";
+Goal "F Join G : stable A = \
+\ (F : stable A & G : stable A)";
by (simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1);
qed "stable_Join";
-Goal "I ~= {} ==> FP (Acts (JN i:I. F i)) = (INT i:I. FP (Acts (F i)))";
+Goal "I ~= {} ==> FP (JN i:I. F i) = (INT i:I. FP (F i))";
by (asm_simp_tac (simpset() addsimps [FP_def, stable_JN, INTER_def]) 1);
qed "FP_JN";
@@ -133,54 +138,52 @@
(*** Progress: transient, ensures ***)
Goal "I ~= {} ==> \
-\ transient (Acts (JN i:I. F i)) A = (EX i:I. transient (Acts (F i)) A)";
+\ (JN i:I. F i) : transient A = (EX i:I. F i : transient A)";
by (auto_tac (claset(),
simpset() addsimps [transient_def, JOIN_def]));
qed "transient_JN";
-Goal "transient (Acts (F Join G)) A = \
-\ (transient (Acts F) A | transient (Acts G) A)";
+Goal "F Join G : transient A = \
+\ (F : transient A | G : transient A)";
by (auto_tac (claset(),
simpset() addsimps [bex_Un, transient_def,
Join_def]));
qed "transient_Join";
Goal "I ~= {} ==> \
-\ ensures (Acts (JN i:I. F i)) A B = \
-\ ((ALL i:I. constrains (Acts (F i)) (A-B) (A Un B)) & \
-\ (EX i:I. ensures (Acts (F i)) A B))";
+\ (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))";
by (auto_tac (claset(),
simpset() addsimps [ensures_def, constrains_JN, transient_JN]));
qed "ensures_JN";
Goalw [ensures_def]
- "ensures (Acts (F Join G)) A B = \
-\ (constrains (Acts F) (A-B) (A Un B) & \
-\ constrains (Acts G) (A-B) (A Un B) & \
-\ (ensures (Acts F) A B | ensures (Acts G) A B))";
+ "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))";
by (auto_tac (claset(),
simpset() addsimps [constrains_Join, transient_Join]));
qed "ensures_Join";
Goalw [stable_def, constrains_def, Join_def]
- "[| stable (Acts F) A; constrains (Acts G) A A' |] \
-\ ==> constrains (Acts (F Join G)) A A'";
-by (asm_simp_tac (simpset() addsimps [ball_Un]) 1);
+ "[| F : stable A; G : constrains A A' |] \
+\ ==> F Join G : constrains A A'";
+by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1);
by (Blast_tac 1);
qed "stable_constrains_Join";
-(*Premises cannot use Invariant because Stable F A is weaker than
- stable (Acts G) A *)
-Goal "[| stable (Acts F) A; Init G <= A; stable (Acts G) A |] \
-\ ==> Invariant (F Join G) A";
-by (simp_tac (simpset() addsimps [Invariant_def, Stable_eq_stable,
- stable_Join]) 1);
+(*Premise for G cannot use Invariant because Stable F A is weaker than
+ G : stable A *)
+Goal "[| F : stable A; G : invariant A |] ==> F Join G : Invariant A";
+by (full_simp_tac (simpset() addsimps [Invariant_def, invariant_def,
+ Stable_eq_stable, stable_Join]) 1);
by (force_tac(claset() addIs [stable_reachable, stable_Int],
simpset() addsimps [Acts_Join]) 1);
qed "stable_Join_Invariant";
-Goal "[| stable (Acts F) A; ensures (Acts G) A B |] \
-\ ==> ensures (Acts (F Join G)) A B";
+Goal "[| F : stable A; G : ensures A B |] ==> F Join G : ensures A 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);
@@ -188,9 +191,18 @@
qed "ensures_stable_Join1";
(*As above, but exchanging the roles of F and G*)
-Goal "[| ensures (Acts F) A B; stable (Acts G) A |] \
-\ ==> ensures (Acts (F Join G)) A B";
+Goal "[| F : ensures A B; G : stable A |] ==> F Join G : ensures A B";
by (stac Join_commute 1);
by (blast_tac (claset() addIs [ensures_stable_Join1]) 1);
qed "ensures_stable_Join2";
+
+(** localTo **)
+
+Goal "[| F Join G : f localTo F; (s,s') : act; \
+\ act : Acts G; act ~: Acts F |] ==> f s' = f s";
+by (asm_full_simp_tac
+ (simpset() addsimps [localTo_def, Diff_def, Acts_Join, stable_def,
+ constrains_def]) 1);
+by (Blast_tac 1);
+qed "localTo_imp_equals";
--- a/src/HOL/UNITY/Union.thy Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Union.thy Thu Oct 15 11:35:07 1998 +0200
@@ -11,15 +11,22 @@
Union = SubstAx + FP +
constdefs
- JOIN :: ['a set, 'a => 'b program] => 'b program
+ JOIN :: ['a set, 'a => 'b program] => 'b program
"JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i))"
- Join :: ['a program, 'a program] => 'a program (infixl 65)
+ Join :: ['a program, 'a program] => 'a program (infixl 65)
"F Join G == mk_program (Init F Int Init G, Acts F Un Acts G)"
- SKIP :: 'a program
+ SKIP :: 'a program
"SKIP == mk_program (UNIV, {})"
+ Diff :: "['a program, ('a * 'a)set set] => 'a program"
+ "Diff F acts == mk_program (Init F, Acts F - acts)"
+
+ (*The set of systems that regard "f" as local to F*)
+ localTo :: ['a => 'b, 'a program] => 'a program set (infixl 80)
+ "f localTo F == {G. ALL z. Diff G (Acts F) : stable {s. f s = z}}"
+
syntax
"@JOIN" :: [pttrn, 'a set, 'b set] => 'b set ("(3JN _:_./ _)" 10)
--- a/src/HOL/UNITY/WFair.ML Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/WFair.ML Thu Oct 15 11:35:07 1998 +0200
@@ -9,30 +9,26 @@
*)
-(*Map its type, [('a * 'a)set set] => ('a set * 'a set) set, to just 'a*)
-Blast.overloaded ("WFair.leadsto",
- #1 o HOLogic.dest_prodT o
- HOLogic.dest_setT o HOLogic.dest_setT o domain_type);
-
-overload_2nd_set "WFair.transient";
-overload_2nd_set "WFair.ensures";
+overload_1st_set "WFair.transient";
+overload_1st_set "WFair.ensures";
+overload_1st_set "WFair.leadsTo";
(*** transient ***)
Goalw [stable_def, constrains_def, transient_def]
- "[| stable acts A; transient acts A |] ==> A = {}";
+ "[| F : stable A; F : transient A |] ==> A = {}";
by (Blast_tac 1);
qed "stable_transient_empty";
Goalw [transient_def]
- "[| transient acts A; B<=A |] ==> transient acts B";
+ "[| F : transient A; B<=A |] ==> F : transient B";
by (Clarify_tac 1);
by (rtac bexI 1 THEN assume_tac 2);
by (Blast_tac 1);
qed "transient_strengthen";
Goalw [transient_def]
- "[| act:acts; A <= Domain act; act^^A <= -A |] ==> transient acts A";
+ "[| act: Acts F; A <= Domain act; act^^A <= -A |] ==> F : transient A";
by (Blast_tac 1);
qed "transient_mem";
@@ -40,40 +36,38 @@
(*** ensures ***)
Goalw [ensures_def]
- "[| constrains acts (A-B) (A Un B); transient acts (A-B) |] \
-\ ==> ensures acts A B";
+ "[| F : constrains (A-B) (A Un B); F : transient (A-B) |] \
+\ ==> F : ensures A B";
by (Blast_tac 1);
qed "ensuresI";
Goalw [ensures_def]
- "ensures acts A B \
-\ ==> constrains acts (A-B) (A Un B) & transient acts (A-B)";
+ "F : ensures A B ==> F : constrains (A-B) (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]
- "[| ensures acts A A'; A'<=B' |] ==> ensures acts A B'";
+ "[| F : ensures A A'; A'<=B' |] ==> F : ensures A B'";
by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
qed "ensures_weaken_R";
Goalw [ensures_def, constrains_def, transient_def]
- "acts ~= {} ==> ensures acts A UNIV";
+ "Acts F ~= {} ==> F : ensures A UNIV";
by Auto_tac;
qed "ensures_UNIV";
Goalw [ensures_def]
- "[| stable acts C; \
-\ constrains acts (C Int (A - A')) (A Un A'); \
-\ transient acts (C Int (A-A')) |] \
-\ ==> ensures acts (C Int A) (C Int A')";
+ "[| F : stable C; \
+\ F : constrains (C Int (A - A')) (A Un A'); \
+\ F : transient (C Int (A-A')) |] \
+\ ==> F : ensures (C Int A) (C Int A')";
by (asm_simp_tac (simpset() addsimps [Int_Un_distrib RS sym,
Diff_Int_distrib RS sym,
stable_constrains_Int]) 1);
qed "stable_ensures_Int";
-Goal "[| stable acts A; transient acts C; A <= B Un C |] \
-\ ==> ensures acts A B";
+Goal "[| F : stable A; F : transient C; A <= B Un C |] ==> F : ensures A 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";
@@ -81,62 +75,67 @@
(*** leadsTo ***)
-(*Synonyms for the theorems produced by the inductive defn package*)
-bind_thm ("leadsTo_Basis", leadsto.Basis);
-bind_thm ("leadsTo_Trans", leadsto.Trans);
+Goalw [leadsTo_def] "F : ensures A B ==> F : leadsTo A B";
+by (blast_tac (claset() addIs [leadsto.Basis]) 1);
+qed "leadsTo_Basis";
-Goal "transient acts A ==> leadsTo acts A (-A)";
+Goalw [leadsTo_def]
+ "[| F : leadsTo A B; F : leadsTo B C |] ==> F : leadsTo A C";
+by (blast_tac (claset() addIs [leadsto.Trans]) 1);
+qed "leadsTo_Trans";
+
+Goal "F : transient A ==> F : leadsTo A (-A)";
by (asm_simp_tac
(simpset() addsimps [leadsTo_Basis, ensuresI, Compl_partition]) 1);
qed "transient_imp_leadsTo";
-Goal "act: acts ==> leadsTo acts A UNIV";
+Goal "F : leadsTo A UNIV";
by (blast_tac (claset() addIs [ensures_UNIV RS leadsTo_Basis]) 1);
qed "leadsTo_UNIV";
Addsimps [leadsTo_UNIV];
(*Useful with cancellation, disjunction*)
-Goal "leadsTo acts A (A' Un A') ==> leadsTo acts A A'";
+Goal "F : leadsTo A (A' Un A') ==> F : leadsTo A A'";
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
qed "leadsTo_Un_duplicate";
-Goal "leadsTo acts A (A' Un C Un C) ==> leadsTo acts A (A' Un C)";
+Goal "F : leadsTo A (A' Un C Un C) ==> F : leadsTo A (A' Un C)";
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
qed "leadsTo_Un_duplicate2";
(*The Union introduction rule as we should have liked to state it*)
-val prems = goal thy
- "(!!A. A : S ==> leadsTo acts A B) ==> leadsTo acts (Union S) B";
-by (blast_tac (claset() addIs (leadsto.Union::prems)) 1);
+val prems = Goalw [leadsTo_def]
+ "(!!A. A : S ==> F : leadsTo A B) ==> F : leadsTo (Union S) B";
+by (blast_tac (claset() addIs [leadsto.Union] addDs prems) 1);
qed "leadsTo_Union";
-val prems = goal thy
- "(!!i. i : I ==> leadsTo acts (A i) B) ==> leadsTo acts (UN i:I. A i) B";
+val prems = Goal
+ "(!!i. i : I ==> F : leadsTo (A i) B) ==> F : leadsTo (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);
+by (blast_tac (claset() addIs leadsTo_Union::prems) 1);
qed "leadsTo_UN";
(*Binary union introduction rule*)
-Goal "[| leadsTo acts A C; leadsTo acts B C |] ==> leadsTo acts (A Un B) C";
+Goal "[| F : leadsTo A C; F : leadsTo B C |] ==> F : leadsTo (A Un B) C";
by (stac Un_eq_Union 1);
by (blast_tac (claset() addIs [leadsTo_Union]) 1);
qed "leadsTo_Un";
(*The INDUCTION rule as we should have liked to state it*)
-val major::prems = goal thy
- "[| leadsTo acts za zb; \
-\ !!A B. ensures acts A B ==> P A B; \
-\ !!A B C. [| leadsTo acts A B; P A B; leadsTo acts B C; P B C |] \
+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 |] \
\ ==> P A C; \
-\ !!B S. ALL A:S. leadsTo acts A B & P A B ==> P (Union S) B \
+\ !!B S. ALL A:S. F : leadsTo A B & P A B ==> P (Union S) B \
\ |] ==> P za zb";
-by (rtac (major RS leadsto.induct) 1);
+by (rtac (major RS CollectD RS leadsto.induct) 1);
by (REPEAT (blast_tac (claset() addIs prems) 1));
qed "leadsTo_induct";
-Goal "[| A<=B; Id: acts |] ==> leadsTo acts A B";
+Goal "A<=B ==> F : leadsTo A B";
by (rtac leadsTo_Basis 1);
by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
by (Blast_tac 1);
@@ -146,50 +145,38 @@
Addsimps [empty_leadsTo];
-(*There's a direct proof by leadsTo_Trans and subset_imp_leadsTo, but it
- needs the extra premise Id:acts*)
-Goal "leadsTo acts A A' ==> A'<=B' --> leadsTo acts A B'";
-by (etac leadsTo_induct 1);
-by (Clarify_tac 3);
-by (blast_tac (claset() addIs [leadsTo_Union]) 3);
-by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
-by (blast_tac (claset() addIs [leadsTo_Basis, ensures_weaken_R]) 1);
-qed_spec_mp "leadsTo_weaken_R";
+Goal "[| F : leadsTo A A'; A'<=B' |] ==> F : leadsTo A B'";
+by (blast_tac (claset() addIs [subset_imp_leadsTo, leadsTo_Trans]) 1);
+qed "leadsTo_weaken_R";
-Goal "[| leadsTo acts A A'; B<=A; Id: acts |] ==> \
-\ leadsTo acts B A'";
+Goal "[| F : leadsTo A A'; B<=A |] ==> F : leadsTo B A'";
by (blast_tac (claset() addIs [leadsTo_Basis, leadsTo_Trans,
subset_imp_leadsTo]) 1);
qed_spec_mp "leadsTo_weaken_L";
(*Distributes over binary unions*)
-Goal "Id: acts ==> \
-\ leadsTo acts (A Un B) C = (leadsTo acts A C & leadsTo acts B C)";
+Goal "F : leadsTo (A Un B) C = (F : leadsTo A C & F : leadsTo B C)";
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1);
qed "leadsTo_Un_distrib";
-Goal "Id: acts ==> \
-\ leadsTo acts (UN i:I. A i) B = (ALL i : I. leadsTo acts (A i) B)";
+Goal "F : leadsTo (UN i:I. A i) B = (ALL i : I. F : leadsTo (A i) B)";
by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1);
qed "leadsTo_UN_distrib";
-Goal "Id: acts ==> \
-\ leadsTo acts (Union S) B = (ALL A : S. leadsTo acts A B)";
+Goal "F : leadsTo (Union S) B = (ALL A : S. F : leadsTo A B)";
by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1);
qed "leadsTo_Union_distrib";
-Goal "[| leadsTo acts A A'; Id: acts; B<=A; A'<=B' |] \
-\ ==> leadsTo acts B B'";
+Goal "[| F : leadsTo A A'; B<=A; A'<=B' |] ==> F : leadsTo B 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 "[| leadsTo acts (A-B) C; leadsTo acts B C; Id: acts |] \
-\ ==> leadsTo acts A C";
+Goal "[| F : leadsTo (A-B) C; F : leadsTo B C |] ==> F : leadsTo A C";
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1);
qed "leadsTo_Diff";
@@ -198,8 +185,8 @@
see ball_constrains_UN in UNITY.ML***)
val prems = goal thy
- "(!! i. i:I ==> leadsTo acts (A i) (A' i)) \
-\ ==> leadsTo acts (UN i:I. A i) (UN i:I. A' i)";
+ "(!! i. i:I ==> F : leadsTo (A i) (A' i)) \
+\ ==> F : leadsTo (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);
@@ -208,22 +195,21 @@
(*Version with no index set*)
val prems = goal thy
- "(!! i. leadsTo acts (A i) (A' i)) \
-\ ==> leadsTo acts (UN i. A i) (UN i. A' i)";
+ "(!! i. F : leadsTo (A i) (A' i)) \
+\ ==> F : leadsTo (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 acts (A i) (A' i) \
-\ ==> leadsTo acts (UN i. A i) (UN i. A' i)";
+Goal "ALL i. F : leadsTo (A i) (A' i) \
+\ ==> F : leadsTo (UN i. A i) (UN i. A' i)";
by (blast_tac (claset() addIs [leadsTo_UN_UN]) 1);
qed "all_leadsTo_UN_UN";
(*Binary union version*)
-Goal "[| leadsTo acts A A'; leadsTo acts B B' |] \
-\ ==> leadsTo acts (A Un B) (A' Un B')";
+Goal "[| F : leadsTo A A'; F : leadsTo B B' |] ==> F : leadsTo (A Un B) (A' Un B')";
by (blast_tac (claset() addIs [leadsTo_Un,
leadsTo_weaken_R]) 1);
qed "leadsTo_Un_Un";
@@ -231,27 +217,27 @@
(** The cancellation law **)
-Goal "[| leadsTo acts A (A' Un B); leadsTo acts B B'; Id: acts |] \
-\ ==> leadsTo acts A (A' Un B')";
+Goal "[| F : leadsTo A (A' Un B); F : leadsTo B B' |] \
+\ ==> F : leadsTo A (A' Un B')";
by (blast_tac (claset() addIs [leadsTo_Un_Un,
subset_imp_leadsTo, leadsTo_Trans]) 1);
qed "leadsTo_cancel2";
-Goal "[| leadsTo acts A (A' Un B); leadsTo acts (B-A') B'; Id: acts |] \
-\ ==> leadsTo acts A (A' Un B')";
+Goal "[| F : leadsTo A (A' Un B); F : leadsTo (B-A') B' |] \
+\ ==> F : leadsTo A (A' Un B')";
by (rtac leadsTo_cancel2 1);
by (assume_tac 2);
by (ALLGOALS Asm_simp_tac);
qed "leadsTo_cancel_Diff2";
-Goal "[| leadsTo acts A (B Un A'); leadsTo acts B B'; Id: acts |] \
-\ ==> leadsTo acts A (B' Un A')";
+Goal "[| F : leadsTo A (B Un A'); F : leadsTo B B' |] \
+\ ==> F : leadsTo A (B' Un A')";
by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1);
qed "leadsTo_cancel1";
-Goal "[| leadsTo acts A (B Un A'); leadsTo acts (B-A') B'; Id: acts |] \
-\ ==> leadsTo acts A (B' Un A')";
+Goal "[| F : leadsTo A (B Un A'); F : leadsTo (B-A') B' |] \
+\ ==> F : leadsTo A (B' Un A')";
by (rtac leadsTo_cancel1 1);
by (assume_tac 2);
by (ALLGOALS Asm_simp_tac);
@@ -261,14 +247,14 @@
(** The impossibility law **)
-Goal "leadsTo acts A B ==> B={} --> A={}";
+Goal "F : leadsTo A B ==> B={} --> A={}";
by (etac leadsTo_induct 1);
by (ALLGOALS Asm_simp_tac);
by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
by (Blast_tac 1);
val lemma = result() RS mp;
-Goal "leadsTo acts A {} ==> A={}";
+Goal "F : leadsTo A {} ==> A={}";
by (blast_tac (claset() addSIs [lemma]) 1);
qed "leadsTo_empty";
@@ -277,8 +263,8 @@
(*Special case of PSP: Misra's "stable conjunction"*)
Goalw [stable_def]
- "[| leadsTo acts A A'; stable acts B |] \
-\ ==> leadsTo acts (A Int B) (A' Int B)";
+ "[| F : leadsTo A A'; F : stable B |] \
+\ ==> F : leadsTo (A Int B) (A' Int B)";
by (etac leadsTo_induct 1);
by (simp_tac (simpset() addsimps [Int_Union_Union]) 3);
by (blast_tac (claset() addIs [leadsTo_Union]) 3);
@@ -290,47 +276,45 @@
by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1);
qed "psp_stable";
-Goal "[| leadsTo acts A A'; stable acts B |] \
-\ ==> leadsTo acts (B Int A) (B Int A')";
+Goal "[| F : leadsTo A A'; F : stable B |] \
+\ ==> F : leadsTo (B Int A) (B Int A')";
by (asm_simp_tac (simpset() addsimps psp_stable::Int_ac) 1);
qed "psp_stable2";
Goalw [ensures_def, constrains_def]
- "[| ensures acts A A'; constrains acts B B' |] \
-\ ==> ensures acts (A Int B) ((A' Int B) Un (B' - B))";
+ "[| F : ensures A A'; F : constrains B B' |] \
+\ ==> F : ensures (A Int B) ((A' Int B) Un (B' - B))";
by (blast_tac (claset() addIs [transient_strengthen]) 1);
qed "psp_ensures";
-Goal "[| leadsTo acts A A'; constrains acts B B'; Id: acts |] \
-\ ==> leadsTo acts (A Int B) ((A' Int B) Un (B' - B))";
+Goal "[| F : leadsTo A A'; F : constrains B B' |] \
+\ ==> F : leadsTo (A Int B) ((A' Int B) Un (B' - B))";
by (etac leadsTo_induct 1);
by (simp_tac (simpset() addsimps [Int_Union_Union]) 3);
by (blast_tac (claset() addIs [leadsTo_Union]) 3);
(*Transitivity case has a delicate argument involving "cancellation"*)
by (rtac leadsTo_Un_duplicate2 2);
by (etac leadsTo_cancel_Diff1 2);
-by (assume_tac 3);
by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2);
(*Basis case*)
by (blast_tac (claset() addIs [leadsTo_Basis, psp_ensures]) 1);
qed "psp";
-Goal "[| leadsTo acts A A'; constrains acts B B'; Id: acts |] \
-\ ==> leadsTo acts (B Int A) ((B Int A') Un (B' - B))";
+Goal "[| F : leadsTo A A'; F : constrains B B' |] \
+\ ==> F : leadsTo (B Int A) ((B Int A') Un (B' - B))";
by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1);
qed "psp2";
Goalw [unless_def]
- "[| leadsTo acts A A'; unless acts B B'; Id: acts |] \
-\ ==> leadsTo acts (A Int B) ((A' Int B) Un B')";
+ "[| F : leadsTo A A'; F : unless B B' |] \
+\ ==> F : leadsTo (A Int B) ((A' Int B) Un B')";
by (dtac psp 1);
by (assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2);
-by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 2);
-by (etac leadsTo_Diff 2);
-by (blast_tac (claset() addIs [subset_imp_leadsTo]) 2);
-by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 1);
+by (etac leadsTo_Diff 1);
+by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
qed "psp_unless";
@@ -339,12 +323,11 @@
(** The most general rule: r is any wf relation; f is any variant function **)
Goal "[| wf r; \
-\ ALL m. leadsTo acts (A Int f-``{m}) \
-\ ((A Int f-``(r^-1 ^^ {m})) Un B); \
-\ Id: acts |] \
-\ ==> leadsTo acts (A Int f-``{m}) B";
+\ ALL m. F : leadsTo (A Int f-``{m}) \
+\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
+\ ==> F : leadsTo (A Int f-``{m}) B";
by (eres_inst_tac [("a","m")] wf_induct 1);
-by (subgoal_tac "leadsTo acts (A Int (f -`` (r^-1 ^^ {x}))) B" 1);
+by (subgoal_tac "F : leadsTo (A Int (f -`` (r^-1 ^^ {x}))) 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);
@@ -354,10 +337,9 @@
(** Meta or object quantifier ????? **)
Goal "[| wf r; \
-\ ALL m. leadsTo acts (A Int f-``{m}) \
-\ ((A Int f-``(r^-1 ^^ {m})) Un B); \
-\ Id: acts |] \
-\ ==> leadsTo acts A B";
+\ ALL m. F : leadsTo (A Int f-``{m}) \
+\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
+\ ==> F : leadsTo A B";
by (res_inst_tac [("t", "A")] subst 1);
by (rtac leadsTo_UN 2);
by (etac lemma 2);
@@ -367,10 +349,9 @@
Goal "[| wf r; \
-\ ALL m:I. leadsTo acts (A Int f-``{m}) \
-\ ((A Int f-``(r^-1 ^^ {m})) Un B); \
-\ Id: acts |] \
-\ ==> leadsTo acts A ((A - (f-``I)) Un B)";
+\ ALL m:I. F : leadsTo (A Int f-``{m}) \
+\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
+\ ==> F : leadsTo A ((A - (f-``I)) Un B)";
by (etac leadsTo_wf_induct 1);
by Safe_tac;
by (case_tac "m:I" 1);
@@ -379,33 +360,28 @@
qed "bounded_induct";
-(*Alternative proof is via the lemma leadsTo acts (A Int f-``(lessThan m)) B*)
-Goal "[| ALL m. leadsTo acts (A Int f-``{m}) \
-\ ((A Int f-``(lessThan m)) Un B); \
-\ Id: acts |] \
-\ ==> leadsTo acts A B";
+(*Alternative proof is via the lemma F : leadsTo (A Int f-``(lessThan m)) B*)
+Goal "[| ALL m. F : leadsTo (A Int f-``{m}) \
+\ ((A Int f-``(lessThan m)) Un B) |] \
+\ ==> F : leadsTo A B";
by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
-by (assume_tac 2);
by (Asm_simp_tac 1);
qed "lessThan_induct";
-Goal "[| ALL m:(greaterThan l). leadsTo acts (A Int f-``{m}) \
-\ ((A Int f-``(lessThan m)) Un B); \
-\ Id: acts |] \
-\ ==> leadsTo acts A ((A Int (f-``(atMost l))) Un B)";
-by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);
+Goal "[| ALL m:(greaterThan l). F : leadsTo (A Int f-``{m}) \
+\ ((A Int f-``(lessThan m)) Un B) |] \
+\ ==> F : leadsTo A ((A Int (f-``(atMost l))) Un B)";
+by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl,
+ Compl_greaterThan RS sym]) 1);
by (rtac (wf_less_than RS bounded_induct) 1);
-by (assume_tac 2);
by (Asm_simp_tac 1);
qed "lessThan_bounded_induct";
-Goal "[| ALL m:(lessThan l). leadsTo acts (A Int f-``{m}) \
-\ ((A Int f-``(greaterThan m)) Un B); \
-\ Id: acts |] \
-\ ==> leadsTo acts A ((A Int (f-``(atLeast l))) Un B)";
+Goal "[| ALL m:(lessThan l). F : leadsTo (A Int f-``{m}) \
+\ ((A Int f-``(greaterThan m)) Un B) |] \
+\ ==> F : leadsTo A ((A Int (f-``(atLeast l))) Un B)";
by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
(wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1);
-by (assume_tac 2);
by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
by (Clarify_tac 1);
by (case_tac "m<l" 1);
@@ -418,22 +394,22 @@
(*** wlt ****)
(*Misra's property W3*)
-Goalw [wlt_def] "leadsTo acts (wlt acts B) B";
+Goalw [wlt_def] "F : leadsTo (wlt F B) B";
by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
qed "wlt_leadsTo";
-Goalw [wlt_def] "leadsTo acts A B ==> A <= wlt acts B";
+Goalw [wlt_def] "F : leadsTo A B ==> A <= wlt F B";
by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
qed "leadsTo_subset";
(*Misra's property W2*)
-Goal "Id: acts ==> leadsTo acts A B = (A <= wlt acts B)";
+Goal "F : leadsTo A B = (A <= wlt F B)";
by (blast_tac (claset() addSIs [leadsTo_subset,
wlt_leadsTo RS leadsTo_weaken_L]) 1);
qed "leadsTo_eq_subset_wlt";
(*Misra's property W4*)
-Goal "Id: acts ==> B <= wlt acts B";
+Goal "B <= wlt F B";
by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS sym,
subset_imp_leadsTo]) 1);
qed "wlt_increasing";
@@ -442,16 +418,16 @@
(*Used in the Trans case below*)
Goalw [constrains_def]
"[| B <= A2; \
-\ constrains acts (A1 - B) (A1 Un B); \
-\ constrains acts (A2 - C) (A2 Un C) |] \
-\ ==> constrains acts (A1 Un A2 - C) (A1 Un A2 Un C)";
+\ 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)";
by (Blast_tac 1);
val lemma1 = result();
(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
-Goal "[| leadsTo acts A A'; Id: acts |] ==> \
-\ EX B. A<=B & leadsTo acts B A' & constrains acts (B-A') (B Un A')";
+Goal "F : leadsTo A A' ==> \
+\ EX B. A<=B & F : leadsTo B A' & F : constrains (B-A') (B Un A')";
by (etac leadsTo_induct 1);
(*Basis*)
by (blast_tac (claset() addIs [leadsTo_Basis]
@@ -470,11 +446,11 @@
(*Misra's property W5*)
-Goal "Id: acts ==> constrains acts (wlt acts B - B) (wlt acts B)";
-by (forward_tac [wlt_leadsTo RS leadsTo_123] 1);
+Goal "F : constrains (wlt F B - B) (wlt F B)";
+by (cut_inst_tac [("F","F")] (wlt_leadsTo RS leadsTo_123) 1);
by (Clarify_tac 1);
-by (subgoal_tac "Ba = wlt acts B" 1);
-by (blast_tac (claset() addDs [leadsTo_eq_subset_wlt]) 2);
+by (subgoal_tac "Ba = wlt F B" 1);
+by (blast_tac (claset() addDs [leadsTo_eq_subset_wlt RS iffD1]) 2);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [wlt_increasing, Un_absorb2]) 1);
qed "wlt_constrains_wlt";
@@ -482,30 +458,29 @@
(*** Completion: Binary and General Finite versions ***)
-Goal "[| leadsTo acts A A'; stable acts A'; \
-\ leadsTo acts B B'; stable acts B'; Id: acts |] \
-\ ==> leadsTo acts (A Int B) (A' Int B')";
-by (subgoal_tac "stable acts (wlt acts B')" 1);
+Goal "[| F : leadsTo A A'; F : stable A'; \
+\ F : leadsTo B B'; F : stable B' |] \
+\ ==> F : leadsTo (A Int B) (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,
- etac wlt_constrains_wlt 2,
+ rtac wlt_constrains_wlt 2,
fast_tac (claset() addEs [wlt_increasing RSN (2,rev_subsetD)]) 3,
Blast_tac 2]);
-by (subgoal_tac "leadsTo acts (A Int wlt acts B') (A' Int wlt acts B')" 1);
+by (subgoal_tac "F : leadsTo (A Int wlt F B') (A' Int wlt F B')" 1);
by (blast_tac (claset() addIs [psp_stable]) 2);
-by (subgoal_tac "leadsTo acts (A' Int wlt acts B') (A' Int B')" 1);
+by (subgoal_tac "F : leadsTo (A' Int wlt F B') (A' Int B')" 1);
by (blast_tac (claset() addIs [wlt_leadsTo, psp_stable2]) 2);
-by (subgoal_tac "leadsTo acts (A Int B) (A Int wlt acts B')" 1);
+by (subgoal_tac "F : leadsTo (A Int B) (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; Id: acts |] \
-\ ==> (ALL i:I. leadsTo acts (A i) (A' i)) --> \
-\ (ALL i:I. stable acts (A' i)) --> \
-\ leadsTo acts (INT i:I. A i) (INT i:I. A' i)";
+Goal "finite I ==> (ALL i:I. F : leadsTo (A i) (A' i)) --> \
+\ (ALL i:I. F : stable (A' i)) --> \
+\ F : leadsTo (INT i:I. A i) (INT i:I. A' i)";
by (etac finite_induct 1);
by (Asm_simp_tac 1);
by (asm_simp_tac
@@ -514,28 +489,26 @@
qed_spec_mp "finite_stable_completion";
-Goal "[| W = wlt acts (B' Un C); \
-\ leadsTo acts A (A' Un C); constrains acts A' (A' Un C); \
-\ leadsTo acts B (B' Un C); constrains acts B' (B' Un C); \
-\ Id: acts |] \
-\ ==> leadsTo acts (A Int B) ((A' Int B') Un C)";
-by (subgoal_tac "constrains acts (W-C) (W Un B' Un C)" 1);
+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);
by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt]
MRS constrains_Un RS constrains_weaken]) 2);
-by (subgoal_tac "constrains acts (W-C) W" 1);
+by (subgoal_tac "F : constrains (W-C) W" 1);
by (asm_full_simp_tac
(simpset() addsimps [wlt_increasing, Un_assoc, Un_absorb2]) 2);
-by (subgoal_tac "leadsTo acts (A Int W - C) (A' Int W Un C)" 1);
+by (subgoal_tac "F : leadsTo (A Int W - C) (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 "leadsTo acts (A' Int W Un C) (A' Int B' Un C)" 1);
+by (subgoal_tac "F : leadsTo (A' Int W Un C) (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,
leadsTo_Un_duplicate2]) 2);
by (dtac leadsTo_Diff 1);
-by (assume_tac 2);
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
by (subgoal_tac "A Int B <= A Int W" 1);
by (blast_tac (claset() addSDs [leadsTo_subset]
@@ -544,10 +517,9 @@
bind_thm("completion", refl RS result());
-Goal "[| finite I; Id: acts |] \
-\ ==> (ALL i:I. leadsTo acts (A i) (A' i Un C)) --> \
-\ (ALL i:I. constrains acts (A' i) (A' i Un C)) --> \
-\ leadsTo acts (INT i:I. A i) ((INT i:I. A' i) Un C)";
+Goal "finite I ==> (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)";
by (etac finite_induct 1);
by (ALLGOALS Asm_simp_tac);
by (Clarify_tac 1);
--- a/src/HOL/UNITY/WFair.thy Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/WFair.thy Thu Oct 15 11:35:07 1998 +0200
@@ -14,39 +14,38 @@
(*This definition specifies weak fairness. The rest of the theory
is generic to all forms of fairness.*)
- transient :: "[('a * 'a)set set, 'a set] => bool"
- "transient acts A == EX act:acts. A <= Domain act & act^^A <= Compl A"
-
- ensures :: "[('a * 'a)set set, 'a set, 'a set] => bool"
- "ensures acts A B == constrains acts (A-B) (A Un B) & transient acts (A-B)"
- (*(unless acts A B) would be equivalent*)
+ transient :: "'a set => 'a program set"
+ "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= Compl A}"
-syntax leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool"
-consts leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set"
+ ensures :: "['a set, 'a set] => 'a program set"
+ "ensures A B == constrains (A-B) (A Un B) Int transient (A-B)"
+
+
+consts leadsto :: "'a program => ('a set * 'a set) set"
-translations
- "leadsTo acts A B" == "(A,B) : leadsto acts"
- "~ leadsTo acts A B" <= "(A,B) ~: leadsto acts"
-
-inductive "leadsto acts"
+inductive "leadsto F"
intrs
- Basis "ensures acts A B ==> leadsTo acts A B"
+ Basis "F : ensures A B ==> (A,B) : leadsto F"
- Trans "[| leadsTo acts A B; leadsTo acts B C |]
- ==> leadsTo acts A C"
+ Trans "[| (A,B) : leadsto F; (B,C) : leadsto F |]
+ ==> (A,C) : leadsto F"
(*Encoding using powerset of the desired axiom
- (!!A. A : S ==> leadsTo acts A B) ==> leadsTo acts (Union S) B
+ (!!A. A : S ==> (A,B) : leadsto F) ==> (Union S, B) : leadsto F
*)
- Union "(UN A:S. {(A,B)}) : Pow (leadsto acts)
- ==> leadsTo acts (Union S) B"
+ Union "(UN A:S. {(A,B)}) : Pow (leadsto F) ==> (Union S, B) : leadsto F"
monos "[Pow_mono]"
-(*wlt acts B is the largest set that leads to B*)
-constdefs wlt :: "[('a * 'a)set set, 'a set] => 'a set"
- "wlt acts B == Union {A. leadsTo acts A B}"
+
+constdefs (*visible version of the relation*)
+ leadsTo :: "['a set, 'a set] => 'a program set"
+ "leadsTo A B == {F. (A,B) : leadsto F}"
+
+ (*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}"
end