Revising the Client proof as suggested by Michel Charpentier. New lemmas
about composition (in Union.ML), etc. Also changed "length" to "size"
because it is displayed as "size" in any event.
--- a/src/HOL/UNITY/Client.ML Thu Nov 05 15:33:27 1998 +0100
+++ b/src/HOL/UNITY/Client.ML Fri Nov 06 13:20:29 1998 +0100
@@ -7,19 +7,7 @@
*)
-(*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);
-by (ALLGOALS (blast_tac (claset() addIs [subset_imp_LeadsTo])));
-qed "Stable_transient_reachable_LeadsTo";
-
-
-
-(*split_all_tac causes a big blow-up*)
-claset_ref() := claset() delSWrapper record_split_name;
+claset_ref() := claset();
Addsimps [Cli_prg_def RS def_prg_Init];
program_defs_ref := [Cli_prg_def];
@@ -29,17 +17,6 @@
(*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 [Cli_prg_def, Acts_Join]) 1);
-(*don't unfold definitions of actions*)
-by (blast_tac HOL_cs 1);
-qed "Acts_Cli_Join_eq";
-
fun invariant_tac i =
rtac invariantI i THEN
@@ -73,92 +50,92 @@
*)
Goal "Cli_prg: \
\ invariant ({s. tok s <= Max} Int \
-\ {s. ALL n: lessThan (length (ask s)). ask s!n <= Max})";
+\ {s. ALL n: lessThan (size (ask s)). ask s!n <= Max})";
by (invariant_tac 1);
by (auto_tac (claset() addSEs [less_SucE], simpset()));
qed "ask_bounded";
+(** Several facts used to prove Lemma 1 **)
+
+Goal "Cli_prg: stable {s. rel s <= giv s}";
+by (constrains_tac 1);
+by Auto_tac;
+qed "stable_rel_le_giv";
+
+Goal "Cli_prg: stable {s. size (rel s) <= size (giv s)}";
+by (constrains_tac 1);
+by Auto_tac;
+qed "stable_size_rel_le_giv";
+
+Goal "Cli_prg: stable {s. size (ask s) <= Suc (size (rel s))}";
+by (constrains_tac 1);
+by Auto_tac;
+qed "stable_size_ask_le_rel";
+
(*We no longer need constrains_tac to expand the program definition, and
- expanding it is extremely expensive! Instead, Acts_Cli_Join_eq expands
- the program.*)
+ 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}";
+Goal "Cli_prg : (Increasing giv Int (rel localTo Cli_prg)) \
+\ guarantees Invariant {s. rel s <= giv s}";
by (rtac guaranteesI 1);
-by (invariant_tac 1);
+by (rtac InvariantI 1);
by (Force_tac 1);
-by (subgoal_tac "rel s <= giv s'" 1);
-by (force_tac (claset(),
- simpset() 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()));
+by (blast_tac (claset() addIs [Increasing_localTo_Stable,
+ stable_rel_le_giv]) 1);
qed "ok_guar_rel_prefix_giv";
(*** Towards proving the liveness property ***)
Goal "Cli_prg Join G \
-\ : transient {s. length (giv s) = Suc k & \
-\ length (rel s) = k & ask s ! k <= giv s ! k}";
+\ : transient {s. size (giv s) = Suc k & \
+\ size (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, Cli_prg_def]));
qed "transient_lemma";
+
+
+val rewrite_o = rewrite_rule [o_def];
+
Goal "Cli_prg : \
-\ (increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
-\ Int invariant giv_meets_ask) \
-\ guarantees invariant {s. length (ask s) <= Suc (length (rel s)) & \
-\ length (rel s) <= length (giv s)}";
+\ (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg)) \
+\ guarantees Invariant ({s. size (ask s) <= Suc (size (rel s))} Int \
+\ {s. size (rel s) <= size (giv s)})";
by (rtac guaranteesI 1);
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;
- by (TRYALL (dtac localTo_imp_equals THEN' atac));
- by (auto_tac (claset() addD2 ("x",localTo_imp_equals), simpset()));
-by (force_tac (claset() addD2 ("x",localTo_imp_equals),
- simpset() addsimps [increasing_def, Acts_Join, stable_def,
- constrains_def]) 1);
+by (dtac (impOfSubs (rewrite_o Increasing_size)) 1);
+by (rtac InvariantI 1);
+by (Force_tac 1);
+by (rtac Stable_Int 1);
+by (fast_tac (claset() addEs [impOfSubs (rewrite_o localTo_imp_o_localTo)]
+ addIs [Increasing_localTo_Stable,
+ stable_size_rel_le_giv]) 2);
+by (fast_tac (claset() addEs [impOfSubs (rewrite_o localTo_imp_o_localTo)]
+ addIs [stable_localTo_stable2 RS stable_imp_Stable,
+ stable_size_ask_le_rel]) 1);
val lemma1 = result();
Goal "Cli_prg : \
-\ (increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
-\ Int invariant giv_meets_ask) \
-\ guarantees (LeadsTo {s. k < length (giv s)} \
-\ {s. k < length (rel s)})";
+\ (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
+\ Int Invariant giv_meets_ask) \
+\ guarantees (LeadsTo {s. k < size (giv s)} \
+\ {s. k < size (rel s)})";
by (rtac guaranteesI 1);
by (Clarify_tac 1);
by (rtac Stable_transient_reachable_LeadsTo 1);
- by (res_inst_tac [("k", "k")] transient_lemma 2);
- by (rtac stable_imp_Stable 1);
- by (dtac (impOfSubs increasing_length) 1);
- by (force_tac (claset(),
- simpset() addsimps [increasing_def,
- stable_def, constrains_def]) 1);
-(** LEVEL 7 **)
-(*
- 1. !!G. [| Cli_prg Join G : invariant giv_meets_ask;
- Cli_prg Join G : ask localTo Cli_prg;
- Cli_prg Join G : increasing giv;
- Cli_prg Join G : rel localTo Cli_prg |]
- ==> reachable (Cli_prg Join G)
- <= - {s. k < length (giv s)} Un {s. k < length (rel s)} Un
- {s. length (giv s) = Suc k &
- length (rel s) = k & ask s ! k <= giv s ! k}
-x
-*)
+by (res_inst_tac [("k", "k")] transient_lemma 2);
+by (force_tac (claset() addDs [impOfSubs Increasing_size,
+ impOfSubs Increasing_Stable_less],
+ simpset()) 1);
by (rtac (make_elim (lemma1 RS guaranteesD)) 1);
by (Blast_tac 1);
-by (auto_tac (claset() addSDs [invariant_includes_reachable],
- simpset() addsimps [giv_meets_ask_def]));
+by (auto_tac (claset(),
+ simpset() addsimps [Invariant_eq_always, giv_meets_ask_def]));
by (ALLGOALS Force_tac);
qed "client_correct";
--- a/src/HOL/UNITY/Client.thy Thu Nov 05 15:33:27 1998 +0100
+++ b/src/HOL/UNITY/Client.thy Fri Nov 06 13:20:29 1998 +0100
@@ -29,9 +29,9 @@
rel_act :: "(state*state) set"
"rel_act == {(s,s').
- EX nrel. nrel = length (rel s) &
+ EX nrel. nrel = size (rel s) &
s' = s (| rel := rel s @ [giv s!nrel] |) &
- nrel < length (giv s) &
+ nrel < size (giv s) &
ask s!nrel <= giv s!nrel}"
(** Choose a new token requirement **)
@@ -45,7 +45,7 @@
ask_act :: "(state*state) set"
"ask_act == {(s,s'). s'=s |
(s' = s (|ask := ask s @ [tok s]|) &
- length (ask s) = length (rel s))}"
+ size (ask s) = size (rel s))}"
Cli_prg :: state program
"Cli_prg == mk_program ({s. tok s : atMost Max &
@@ -56,7 +56,7 @@
giv_meets_ask :: state set
"giv_meets_ask ==
- {s. length (giv s) <= length (ask s) &
- (ALL n: lessThan (length (giv s)). ask s!n <= giv s!n)}"
+ {s. size (giv s) <= size (ask s) &
+ (ALL n: lessThan (size (giv s)). ask s!n <= giv s!n)}"
end
--- a/src/HOL/UNITY/Comp.ML Thu Nov 05 15:33:27 1998 +0100
+++ b/src/HOL/UNITY/Comp.ML Fri Nov 06 13:20:29 1998 +0100
@@ -43,6 +43,10 @@
component_Acts, component_Init]) 1);
qed "component_anti_sym";
+Goalw [component_def]
+ "component F H = (EX G. F Join G = H & Disjoint F G)";
+by (blast_tac (claset() addSIs [Diff_Disjoint, Join_Diff2]) 1);
+qed "component_eq";
(*** existential properties ***)
@@ -101,8 +105,9 @@
(*** guarantees ***)
(*This equation is more intuitive than the official definition*)
-Goalw [guarantees_def, component_def]
- "(F : A guarantees B) = (ALL G. F Join G : A --> F Join G : B)";
+Goal "(F : A guarantees B) = \
+\ (ALL G. F Join G : A & Disjoint F G --> F Join G : B)";
+by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
by (Blast_tac 1);
qed "guarantees_eq";
@@ -154,13 +159,16 @@
by (Blast_tac 1);
qed "ex_guarantees";
-val prems = Goalw [guarantees_def, component_def]
- "(!!G. F Join G : A ==> F Join G : B) ==> F : A guarantees B";
+val prems = Goal
+ "(!!G. [| F Join G : A; Disjoint F G |] ==> F Join G : B) \
+\ ==> F : A guarantees B";
+by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
by (blast_tac (claset() addIs prems) 1);
qed "guaranteesI";
-Goal "[| F : A guarantees B; F Join G : A |] ==> F Join G : B";
-by (asm_full_simp_tac (simpset() addsimps [guarantees_eq]) 1);
+Goalw [guarantees_def, component_def]
+ "[| F : A guarantees B; F Join G : A |] ==> F Join G : B";
+by (Blast_tac 1);
qed "guaranteesD";
--- a/src/HOL/UNITY/Constrains.ML Thu Nov 05 15:33:27 1998 +0100
+++ b/src/HOL/UNITY/Constrains.ML Fri Nov 06 13:20:29 1998 +0100
@@ -81,7 +81,7 @@
by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1);
qed "Constrains_Int";
-Goal "[| ALL i:I. F : Constrains (A 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);
@@ -140,6 +140,11 @@
qed "Stable_Constrains_Int";
Goalw [Stable_def]
+ "(ALL i:I. F : Stable (A i)) ==> F : Stable (UN i:I. A i)";
+by (etac ball_Constrains_UN 1);
+qed "ball_Stable_UN";
+
+Goalw [Stable_def]
"(ALL i:I. F : Stable (A i)) ==> F : Stable (INT i:I. A i)";
by (etac ball_Constrains_INT 1);
qed "ball_Stable_INT";
@@ -156,13 +161,13 @@
"Increasing f <= Increasing (length o f)";
by Auto_tac;
by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1);
-qed "Increasing_length";
+qed "Increasing_size";
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";
+qed "Increasing_Stable_less";
Goalw [increasing_def, Increasing_def]
"F : increasing f ==> F : Increasing f";
@@ -211,13 +216,7 @@
bind_thm ("InvariantE", InvariantD RS conjE);
-(*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!*)
+(*The set of all reachable states is the strongest Invariant*)
Goal "F : Invariant A ==> reachable F <= A";
by (full_simp_tac
(simpset() addsimps [Stable_def, Constrains_def, constrains_def,
@@ -233,22 +232,33 @@
qed "invariant_imp_Invariant";
Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def]
- "(F : Invariant A) = (F : invariant (reachable F Int A))";
+ "Invariant A = {F. F : invariant (reachable F Int A)}";
by (blast_tac (claset() addIs reachable.intrs) 1);
qed "Invariant_eq_invariant_reachable";
+(*Invariant is the "always" notion*)
+Goal "Invariant A = {F. reachable F <= A}";
+by (auto_tac (claset() addDs [invariant_includes_reachable],
+ simpset() addsimps [Int_absorb2, invariant_reachable,
+ Invariant_eq_invariant_reachable]));
+qed "Invariant_eq_always";
-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 A = (UN I: Pow A. invariant I)";
+by (simp_tac (simpset() addsimps [Invariant_eq_always]) 1);
+by (blast_tac (claset() addIs [invariantI, impOfSubs Init_subset_reachable,
+ stable_reachable,
+ impOfSubs invariant_includes_reachable]) 1);
+qed "Invariant_eq_UN_invariant";
+
+
+(*** "Constrains" rules involving Invariant ***)
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);
+ (simpset() addsimps [Invariant_includes_reachable RS Int_absorb2,
+ Constrains_def, Int_assoc RS sym]) 1);
qed "Invariant_ConstrainsI";
(* [| F : Invariant INV; F : Constrains (INV Int A) A |]
@@ -258,8 +268,8 @@
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);
+ (simpset() addsimps [Invariant_includes_reachable RS Int_absorb2,
+ Constrains_def, Int_assoc RS sym]) 1);
qed "Invariant_ConstrainsD";
bind_thm ("Invariant_StableD", StableD RSN (2,Invariant_ConstrainsD));
@@ -269,8 +279,7 @@
(** Conjoining Invariants **)
Goal "[| F : Invariant A; F : Invariant B |] ==> F : Invariant (A Int B)";
-by (auto_tac (claset(),
- simpset() addsimps [Invariant_def, Stable_Int]));
+by (auto_tac (claset(), simpset() addsimps [Invariant_eq_always]));
qed "Invariant_Int";
(*Delete the nearest invariance assumption (which will be the second one
--- a/src/HOL/UNITY/SubstAx.ML Thu Nov 05 15:33:27 1998 +0100
+++ b/src/HOL/UNITY/SubstAx.ML Fri Nov 06 13:20:29 1998 +0100
@@ -294,6 +294,15 @@
qed "PSP_Unless";
+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);
+by (ALLGOALS (blast_tac (claset() addIs [subset_imp_LeadsTo])));
+qed "Stable_transient_reachable_LeadsTo";
+
+
(*** Induction rules ***)
(** Meta or object quantifier ????? **)
--- a/src/HOL/UNITY/UNITY.ML Thu Nov 05 15:33:27 1998 +0100
+++ b/src/HOL/UNITY/UNITY.ML Fri Nov 06 13:20:29 1998 +0100
@@ -69,12 +69,6 @@
by (Blast_tac 1);
qed "ball_constrains_UN";
-Goalw [constrains_def]
- "[| 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]
@@ -89,12 +83,6 @@
by (Blast_tac 1);
qed "ball_constrains_INT";
-Goalw [constrains_def]
- "[| 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] "[| F : constrains A A' |] ==> A<=A'";
by (Blast_tac 1);
qed "constrains_imp_subset";
@@ -116,16 +104,30 @@
by (assume_tac 1);
qed "stableD";
+(** Union **)
+
Goalw [stable_def]
"[| 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]
+ "ALL i:I. F : stable (A i) ==> F : stable (UN i:I. A i)";
+by (blast_tac (claset() addIs [ball_constrains_UN]) 1);
+qed "ball_stable_UN";
+
+(** Intersection **)
+
+Goalw [stable_def]
"[| 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]
+ "ALL i:I. F : stable (A i) ==> F : stable (INT i:I. A i)";
+by (blast_tac (claset() addIs [ball_constrains_INT]) 1);
+qed "ball_stable_INT";
+
Goalw [stable_def, constrains_def]
"[| F : stable C; F : constrains A (C Un A') |] \
\ ==> F : constrains (C Un A) (C Un A')";
@@ -150,7 +152,7 @@
bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
-(*** invariant & always ***)
+(*** invariant ***)
Goal "[| Init F<=A; F: stable A |] ==> F : invariant A";
by (asm_simp_tac (simpset() addsimps [invariant_def]) 1);
@@ -176,17 +178,6 @@
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 ***)
@@ -194,13 +185,13 @@
"increasing f <= increasing (length o f)";
by Auto_tac;
by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1);
-qed "increasing_length";
+qed "increasing_size";
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";
+qed "increasing_stable_less";
(** The Elimination Theorem. The "free" m has become universally quantified!
--- a/src/HOL/UNITY/UNITY.thy Thu Nov 05 15:33:27 1998 +0100
+++ b/src/HOL/UNITY/UNITY.thy Fri Nov 06 13:20:29 1998 +0100
@@ -24,15 +24,9 @@
unless :: "['a set, 'a set] => 'a program set"
"unless A B == constrains (A-B) (A Un 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"
- (*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}"
--- a/src/HOL/UNITY/Union.ML Thu Nov 05 15:33:27 1998 +0100
+++ b/src/HOL/UNITY/Union.ML Fri Nov 06 13:20:29 1998 +0100
@@ -97,44 +97,6 @@
simpset() addsimps [constrains_def, Join_def]));
qed "constrains_Join";
-
-(**
-Michel says...
-
- p inductive-next q' in F
- p inductive-next q'' in G
- p noninductive-next q in FoG
- -------------------------------------------
- p noninductive-next q /\ (q' \/ q'') in FoG
-
- From which you deduce:
-
- inductive-stable A /\ B in F
- inductive-stable A in G
- noninductive-stable B in FoG
- ---------------------------------
- noninductive-stable A /\ B in FoG
-**)
-
-Goal "[| F : constrains A B'; G : constrains A B''; \
-\ F Join G : Constrains A B |] \
-\ ==> F Join G : Constrains A (B Int (B' Un B''))";
-by (auto_tac
- (claset() addIs [constrains_Int RS constrains_weaken],
- simpset() addsimps [Constrains_def, constrains_Join]));
-qed "constrains_imp_Join_Constrains";
-
-Goalw [Stable_def, stable_def]
- "[| F : stable (A Int B); G : stable A; \
-\ F Join G : Stable B |] \
-\ ==> F Join G : Stable (A Int B)";
-by (auto_tac
- (claset() addIs [constrains_Int RS constrains_weaken],
- simpset() addsimps [Constrains_def, constrains_Join]));
-qed "stable_imp_Join_Stable";
-
-
-
(**FAILS, I think; see 5.4.1, Substitution Axiom.
The problem is to relate reachable (F Join G) with
reachable F and reachable G
@@ -235,12 +197,82 @@
qed "ensures_stable_Join2";
-(** localTo **)
+(** Diff and localTo **)
+
+Goalw [Join_def, Diff_def] "F Join (Diff G (Acts F)) = F Join G";
+by (rtac program_equalityI 1);
+by Auto_tac;
+qed "Join_Diff2";
+
+Goalw [Diff_def, Disjoint_def] "Disjoint F (Diff G (Acts F))";
+by Auto_tac;
+qed "Diff_Disjoint";
-Goal "[| F Join G : f localTo F; (s,s') : act; \
-\ act : Acts G; act ~: Acts F |] ==> f s' = f s";
+Goal "[| F Join G : v localTo F; Disjoint F G |] \
+\ ==> G : (INT z. stable {s. v s = z})";
by (asm_full_simp_tac
- (simpset() addsimps [localTo_def, Diff_def, Acts_Join, stable_def,
- constrains_def]) 1);
+ (simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
+ Acts_Join, stable_def, constrains_def]) 1);
+by (Blast_tac 1);
+qed "localTo_imp_stable";
+
+Goal "[| F Join G : v localTo F; (s,s') : act; \
+\ act : Acts G; Disjoint F G |] ==> v s' = v s";
+by (asm_full_simp_tac
+ (simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
+ Acts_Join, stable_def, constrains_def]) 1);
by (Blast_tac 1);
qed "localTo_imp_equals";
+
+Goalw [localTo_def, stable_def, constrains_def]
+ "v localTo F <= (f o v) localTo F";
+by (Clarify_tac 1);
+by (auto_tac (claset() addSEs [allE, ballE], simpset()));
+qed "localTo_imp_o_localTo";
+
+
+(*** Higher-level rules involving localTo and Join ***)
+
+Goal "[| F : constrains {s. P (v s) (w s)} {s. P' (v s) (w s)}; \
+\ F Join G : v localTo F; \
+\ F Join G : w localTo F; \
+\ Disjoint F G |] \
+\ ==> F Join G : constrains {s. P (v s) (w s)} {s. P' (v s) (w s)}";
+by (auto_tac (claset(), simpset() addsimps [constrains_def, Acts_Join]));
+by (REPEAT_FIRST (dtac localTo_imp_equals THEN' REPEAT1 o atac));
+by Auto_tac;
+qed "constrains_localTo_constrains2";
+
+Goalw [stable_def]
+ "[| F : stable {s. P (v s) (w s)}; \
+\ F Join G : v localTo F; \
+\ F Join G : w localTo F; \
+\ Disjoint F G |] \
+\ ==> F Join G : stable {s. P (v s) (w s)}";
+by (blast_tac (claset() addIs [constrains_localTo_constrains2]) 1);
+qed "stable_localTo_stable2";
+
+
+Goal "(UN k. {s. f s = k}) = UNIV";
+by (Blast_tac 1);
+qed "UN_eq_UNIV";
+
+Goal "[| F : stable {s. v s <= w s}; \
+\ F Join G : v localTo F; \
+\ F Join G : Increasing w; \
+\ Disjoint F G |] \
+\ ==> F Join G : Stable {s. v s <= w s}";
+by (safe_tac (claset() addSDs [localTo_imp_stable]));
+by (rewrite_goals_tac [stable_def, Stable_def, Increasing_def]);
+by (subgoal_tac "ALL k: UNIV. ?H : Constrains ({s. v s = k} Int ?AA) ?AA" 1);
+by (dtac ball_Constrains_UN 1);
+by (full_simp_tac (simpset() addsimps [UN_eq_UNIV]) 1);
+by (rtac ballI 1);
+by (subgoal_tac "F Join G : constrains ({s. v s = k} Int {s. v s <= w s}) \
+\ ({s. v s = k} Un {s. v s <= w s})" 1);
+by (asm_simp_tac (simpset() addsimps [constrains_Join]) 2);
+by (blast_tac (claset() addIs [constrains_weaken]) 2);
+by (dtac (constrains_imp_Constrains RS Constrains_Int) 1 THEN etac INT_D 1);
+by (etac Constrains_weaken 2);
+by Auto_tac;
+qed "Increasing_localTo_Stable";
--- a/src/HOL/UNITY/Union.thy Thu Nov 05 15:33:27 1998 +0100
+++ b/src/HOL/UNITY/Union.thy Fri Nov 06 13:20:29 1998 +0100
@@ -5,7 +5,7 @@
Unions of programs
-From Misra's Chapter 5: Asynchronous Compositions of Programs
+Partly from Misra's Chapter 5: Asynchronous Compositions of Programs
*)
Union = SubstAx + FP +
@@ -23,9 +23,13 @@
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*)
+ (*The set of systems that regard "v" 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}}"
+ "v localTo F == {G. ALL z. Diff G (Acts F) : stable {s. v s = z}}"
+
+ (*Two programs with disjoint actions, except for Id (idling)*)
+ Disjoint :: ['a program, 'a program] => bool
+ "Disjoint F G == Acts F Int Acts G <= {Id}"
syntax
"@JOIN" :: [pttrn, 'a set, 'b set] => 'b set ("(3JN _:_./ _)" 10)