Added Tanja's Detects and Reachability theories. Also
changed object-quantifiers to meta-quantifiers in ball_constrains_UN/INT...
--- a/src/HOL/UNITY/Constrains.ML Fri Mar 03 18:22:53 2000 +0100
+++ b/src/HOL/UNITY/Constrains.ML Fri Mar 03 18:26:19 2000 +0100
@@ -108,12 +108,13 @@
by (blast_tac (claset() addIs [constrains_Un RS constrains_weaken]) 1);
qed "Constrains_Un";
-Goal "ALL i:I. F : (A i) Co (A' i) \
+val [prem] = Goalw [Constrains_def]
+ "(!!i. i:I ==> F : (A i) Co (A' i)) \
\ ==> F : (UN i:I. A i) Co (UN i:I. A' i)";
-by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
-by (dtac ball_constrains_UN 1);
-by (blast_tac (claset() addIs [constrains_weaken]) 1);
-qed "ball_Constrains_UN";
+by (rtac CollectI 1);
+by (rtac (prem RS CollectD RS constrains_UN RS constrains_weaken) 1);
+by Auto_tac;
+qed "Constrains_UN";
(** Intersection **)
@@ -123,13 +124,13 @@
by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1);
qed "Constrains_Int";
-Goal "ALL i:I. F : (A i) Co (A' i) \
+val [prem] = Goalw [Constrains_def]
+ "(!!i. i:I ==> F : (A i) Co (A' i)) \
\ ==> F : (INT i:I. A i) Co (INT i:I. A' i)";
-by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
-by (dtac ball_constrains_INT 1);
-by (dtac constrains_reachable_Int 1);
-by (blast_tac (claset() addIs [constrains_weaken]) 1);
-qed "ball_Constrains_INT";
+by (rtac CollectI 1);
+by (rtac (prem RS CollectD RS constrains_INT RS constrains_weaken) 1);
+by Auto_tac;
+qed "Constrains_INT";
Goal "F : A Co A' ==> reachable F Int A <= A'";
by (asm_full_simp_tac (simpset() addsimps [constrains_imp_subset,
@@ -150,6 +151,11 @@
(*** Stable ***)
+(*Useful because there's no Stable_weaken. [Tanja Vos]*)
+Goal "[| F: Stable A; A = B |] ==> F : Stable B";
+by (Blast_tac 1);
+qed "Stable_eq";
+
Goal "(F : Stable A) = (F : stable (reachable F Int A))";
by (simp_tac (simpset() addsimps [Stable_def, Constrains_eq_constrains,
stable_def]) 1);
@@ -185,15 +191,17 @@
by (blast_tac (claset() addIs [Constrains_Int RS Constrains_weaken]) 1);
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";
+val [prem] = Goalw [Stable_def]
+ "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (UN i:I. A i)";
+by (rtac (prem RS Constrains_UN) 1);
+by (assume_tac 1);
+qed "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";
+val [prem] = Goalw [Stable_def]
+ "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (INT i:I. A i)";
+by (rtac (prem RS Constrains_INT) 1);
+by (assume_tac 1);
+qed "Stable_INT";
Goal "F : Stable (reachable F)";
by (simp_tac (simpset() addsimps [Stable_eq_stable]) 1);
@@ -257,6 +265,7 @@
qed "AlwaysD";
bind_thm ("AlwaysE", AlwaysD RS conjE);
+bind_thm ("Always_imp_Stable", AlwaysD RS conjunct2);
(*The set of all reachable states is Always*)
--- a/src/HOL/UNITY/Deadlock.ML Fri Mar 03 18:22:53 2000 +0100
+++ b/src/HOL/UNITY/Deadlock.ML Fri Mar 03 18:26:19 2000 +0100
@@ -65,13 +65,13 @@
(*The final deadlock example*)
-val [zeroprem, allprem] = goalw thy [stable_def]
+val [zeroprem, allprem] = Goalw [stable_def]
"[| F : (A 0 Int A (Suc n)) co (A 0); \
-\ ALL i: atMost n. F : (A(Suc i) Int A i) co \
-\ (-A i Un A(Suc i)) |] \
+\ !!i. i: atMost n ==> F : (A(Suc i) Int A i) co (-A i Un A(Suc i)) |] \
\ ==> F : stable (INT i: atMost (Suc n). A i)";
-by (rtac ([zeroprem, allprem RS ball_constrains_INT] MRS
+by (rtac ([zeroprem, constrains_INT] MRS
constrains_Int RS constrains_weaken) 1);
+by (etac allprem 1);
by (simp_tac (simpset() addsimps [Collect_le_Int_equals,
Int_assoc, INT_absorb]) 1);
by (simp_tac (simpset() addsimps [INT_le_Suc_equals_Int]) 1);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Detects.ML Fri Mar 03 18:26:19 2000 +0100
@@ -0,0 +1,69 @@
+(* Title: HOL/UNITY/Detects
+ ID: $Id$
+ Author: Tanja Vos, Cambridge University Computer Laboratory
+ Copyright 2000 University of Cambridge
+
+Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
+*)
+
+(* Corollary from Sectiom 3.6.4 *)
+
+Goal "F: A LeadsTo B ==> F : Always (-((FP F) Int A Int -B))";
+by (rtac LeadsTo_empty 1);
+by (subgoal_tac "F : (FP F Int A Int - B) LeadsTo (B Int (FP F Int -B))" 1);
+by (subgoal_tac "(FP F Int A Int - B) = (A Int (FP F Int -B))" 2);
+by (subgoal_tac "(B Int (FP F Int -B)) = {}" 1);
+by Auto_tac;
+by (blast_tac (claset() addIs [PSP_Stable, stable_imp_Stable,
+ stable_FP_Int]) 1);
+qed "Always_at_FP";
+
+
+Goalw [Detects_def, Int_def]
+ "[| F : A Detects B; F : B Detects C |] ==> F : A Detects C";
+by (Simp_tac 1);
+by Safe_tac;
+by (rtac LeadsTo_Trans 2);
+by Auto_tac;
+by (subgoal_tac "F : Always ((-A Un B) Int (-B Un C))" 1);
+by (simp_tac (simpset() addsimps [Always_Int_distrib]) 2);
+by Auto_tac;
+by (blast_tac (claset() addIs [Always_weaken]) 1);
+qed "Detects_Trans";
+
+
+Goalw [Detects_def] "F : A Detects A";
+by (simp_tac (simpset() addsimps [Un_commute, Compl_partition,
+ subset_imp_LeadsTo]) 1);
+qed "Detects_refl";
+
+Goalw [Equality_def] "(A<==>B) = (A Int B) Un (-A Int -B)";
+by (Blast_tac 1);
+qed "Detects_eq_Un";
+
+(*Not quite antisymmetry: sets A and B agree in all reachable states *)
+Goalw [Detects_def, Equality_def]
+ "[| F : A Detects B; F : B Detects A|] ==> F : Always (A <==> B)";
+by (asm_full_simp_tac (simpset() addsimps [Always_Int_I, Un_commute]) 1);
+qed "Detects_antisym";
+
+
+(* Theorem from Section 3.8 *)
+
+Goalw [Detects_def, Equality_def]
+ "F : A Detects B ==> F : Always ((-(FP F)) Un (A <==> B))";
+by (simp_tac (simpset() addsimps [Un_Int_distrib, Always_Int_distrib]) 1);
+by (blast_tac (claset() addDs [Always_at_FP]
+ addIs [Always_weaken]) 1);
+qed "Detects_Always";
+
+(* Theorem from exercise 11.1 Section 11.3.1 *)
+
+Goalw [Detects_def, Equality_def]
+ "F : A Detects B ==> F : UNIV LeadsTo (A <==> B)";
+by (res_inst_tac [("B", "B")] LeadsTo_Diff 1);
+by (blast_tac (claset() addIs [Always_LeadsTo_weaken]) 2);
+by (blast_tac (claset() addIs [Always_LeadsToI, subset_imp_LeadsTo]) 1);
+qed "Detects_Imp_LeadstoEQ";
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Detects.thy Fri Mar 03 18:26:19 2000 +0100
@@ -0,0 +1,21 @@
+(* Title: HOL/UNITY/Detects
+ ID: $Id$
+ Author: Tanja Vos, Cambridge University Computer Laboratory
+ Copyright 2000 University of Cambridge
+
+Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
+*)
+
+Detects = WFair + Reach +
+
+
+consts
+ op_Detects :: "['a set, 'a set] => 'a program set" (infixl "Detects" 60)
+ op_Equality :: "['a set, 'a set] => 'a set" (infixl "<==>" 60)
+
+defs
+ Detects_def "A Detects B == (Always (-A Un B)) Int (B LeadsTo A)"
+ Equality_def "A <==> B == (-A Un B) Int (A Un -B)"
+
+end
+
--- a/src/HOL/UNITY/ELT.ML Fri Mar 03 18:22:53 2000 +0100
+++ b/src/HOL/UNITY/ELT.ML Fri Mar 03 18:26:19 2000 +0100
@@ -77,21 +77,6 @@
by (deepen_tac (set_cs addSIs [equalityI]) 0 1);
qed "givenBy_DiffI";
-Goal "givenBy (v o f) = extend_set h `` (givenBy v)";
-by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
-by (Deepen_tac 0 1);
-qed "givenBy_o_eq_extend_set";
-
-Goal "givenBy f = range (extend_set h)";
-by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
-by (Deepen_tac 0 1);
-qed "givenBy_eq_extend_set";
-
-Goal "D : givenBy v ==> extend_set h D : givenBy (v o f)";
-by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
-by (Blast_tac 1);
-qed "extend_set_givenBy_I";
-
(** Standard leadsTo rules **)
@@ -232,17 +217,6 @@
qed "leadsETo_Diff";
-(** Meta or object quantifier ???
- see ball_constrains_UN in UNITY.ML***)
-
-val prems = goal thy
- "[| !! i. i:I ==> F : (A i) leadsTo[CC] (A' i) |] \
-\ ==> F : (UN i:I. A i) leadsTo[CC] (UN i:I. A' i)";
-by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1);
-by (blast_tac (claset() addIs [leadsETo_Union, leadsETo_weaken_R]
- addIs prems) 1);
-qed "leadsETo_UN_UN";
-
(*Binary union version*)
Goal "[| F : A leadsTo[CC] A'; F : B leadsTo[CC] B' |] \
\ ==> F : (A Un B) leadsTo[CC] (A' Un B')";
@@ -259,13 +233,6 @@
subset_imp_leadsETo, leadsETo_Trans]) 1);
qed "leadsETo_cancel2";
-Goal "[| F : A leadsTo[CC] (A' Un B); F : (B-A') leadsTo[CC] B' |] \
-\ ==> F : A leadsTo[CC] (A' Un B')";
-by (rtac leadsETo_cancel2 1);
-by (assume_tac 2);
-by (ALLGOALS Asm_simp_tac);
-qed "leadsETo_cancel_Diff2";
-
Goal "[| F : A leadsTo[CC] (B Un A'); F : B leadsTo[CC] B' |] \
\ ==> F : A leadsTo[CC] (B' Un A')";
by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
@@ -509,6 +476,23 @@
Open_locale "Extend";
+(*givenBy laws that need to be in the locale*)
+
+Goal "givenBy (v o f) = extend_set h `` (givenBy v)";
+by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
+by (Deepen_tac 0 1);
+qed "givenBy_o_eq_extend_set";
+
+Goal "givenBy f = range (extend_set h)";
+by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
+by (Deepen_tac 0 1);
+qed "givenBy_eq_extend_set";
+
+Goal "D : givenBy v ==> extend_set h D : givenBy (v o f)";
+by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
+by (Blast_tac 1);
+qed "extend_set_givenBy_I";
+
Goal "F : A leadsTo[CC] B \
\ ==> extend h F : (extend_set h A) leadsTo[extend_set h `` CC] \
\ (extend_set h B)";
@@ -545,6 +529,18 @@
by (auto_tac (claset(), simpset() addsimps [Int_Diff]));
qed "Join_project_ensures_strong";
+(*Generalizes preserves_project_transient_empty*)
+Goal "[| G : preserves (v o f); \
+\ project h C G : transient (C' Int D); \
+\ project h C G : stable C'; D : givenBy v |] \
+\ ==> C' Int D = {}";
+by (rtac stable_transient_empty 1);
+by (assume_tac 2);
+(*If addIs then PROOF FAILED at depth 3*)
+by (blast_tac (claset() addSIs [stable_Int, preserves_givenBy_imp_stable,
+ project_preserves_I]) 1);
+qed "preserves_o_project_transient_empty";
+
Goal "[| extend h F Join G : stable C; \
\ F Join project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)``givenBy v] B; \
\ G : preserves (v o f) |] \
--- a/src/HOL/UNITY/FP.ML Fri Mar 03 18:22:53 2000 +0100
+++ b/src/HOL/UNITY/FP.ML Fri Mar 03 18:26:19 2000 +0100
@@ -10,8 +10,7 @@
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);
+by (blast_tac (claset() addIs [constrains_UN]) 1);
qed "stable_FP_Orig_Int";
@@ -26,7 +25,7 @@
by (Blast_tac 2);
by (asm_simp_tac (simpset() addsimps [Int_insert_right]) 1);
by (rewrite_goals_tac [FP_def, stable_def]);
-by (rtac ball_constrains_UN 1);
+by (rtac constrains_UN 1);
by (Simp_tac 1);
qed "stable_FP_Int";
--- a/src/HOL/UNITY/ROOT.ML Fri Mar 03 18:22:53 2000 +0100
+++ b/src/HOL/UNITY/ROOT.ML Fri Mar 03 18:26:19 2000 +0100
@@ -25,10 +25,11 @@
time_use_thy "Comp";
(*Allocator example*)
time_use_thy "Client";
-time_use_thy "Extend";
+time_use_thy "ELT"; (*obsolete*)
time_use_thy "PPROD";
time_use_thy "TimerArray";
time_use_thy "Alloc";
+time_use_thy "Reachability";
add_path "../Auth"; (*to find Public.thy*)
use_thy"NSP_Bad";
--- a/src/HOL/UNITY/Reach.ML Fri Mar 03 18:22:53 2000 +0100
+++ b/src/HOL/UNITY/Reach.ML Fri Mar 03 18:26:19 2000 +0100
@@ -74,11 +74,12 @@
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, Rprg_def])) 1);
+ [Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym, Rprg_def]) 1);
by Auto_tac;
- by (ALLGOALS (dtac bspec THEN' atac));
- by (rtac fun_upd_idem 1);
- by (auto_tac (claset(),simpset() addsimps [fun_upd_idem_iff]));
+by (rtac fun_upd_idem 1);
+by Auto_tac;
+by (force_tac (claset() addSIs [rev_bexI],
+ simpset() addsimps [fun_upd_idem_iff]) 1);
qed "Compl_fixedpoint";
Goal "A - fixedpoint = (UN (u,v): edges. A Int {s. s u & ~ s v})";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Reachability.ML Fri Mar 03 18:26:19 2000 +0100
@@ -0,0 +1,308 @@
+(* Title: HOL/UNITY/Reachability
+ ID: $Id$
+ Author: Tanja Vos, Cambridge University Computer Laboratory
+ Copyright 2000 University of Cambridge
+
+Reachability in Graphs
+
+From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2 and 11.3
+*)
+
+bind_thm("E_imp_in_V_L", Graph2 RS conjunct1);
+bind_thm("E_imp_in_V_R", Graph2 RS conjunct2);
+
+Goal "(v,w) : E ==> F : reachable v LeadsTo nmsg_eq 0 (v,w) Int reachable v";
+by (rtac (MA7 RS PSP_Stable RS LeadsTo_weaken_L) 1);
+by (rtac MA6 3);
+by (auto_tac (claset(), simpset() addsimps [E_imp_in_V_L, E_imp_in_V_R]));
+qed "lemma2";
+
+Goal "(v,w) : E ==> F : reachable v LeadsTo reachable w";
+by (rtac (MA4 RS Always_LeadsTo_weaken) 1);
+by (rtac lemma2 2);
+by (auto_tac (claset(), simpset() addsimps [nmsg_eq_def, nmsg_gt_def]));
+qed "Induction_base";
+
+Goal "(v,w) : REACHABLE ==> F : reachable v LeadsTo reachable w";
+by (etac REACHABLE.induct 1);
+by (rtac subset_imp_LeadsTo 1);
+by (Blast_tac 1);
+by (blast_tac (claset() addIs [LeadsTo_Trans, Induction_base]) 1);
+qed "REACHABLE_LeadsTo_reachable";
+
+Goal "F : {s. (root,v) : REACHABLE} LeadsTo reachable v";
+by (rtac single_LeadsTo_I 1);
+by (full_simp_tac (simpset() addsplits [split_if_asm]) 1);
+by (rtac (MA1 RS Always_LeadsToI) 1);
+by (etac (REACHABLE_LeadsTo_reachable RS LeadsTo_weaken_L) 1);
+by Auto_tac;
+qed "Detects_part1";
+
+
+Goalw [Detects_def]
+ "v : V ==> F : (reachable v) Detects {s. (root,v) : REACHABLE}";
+by Auto_tac;
+by (blast_tac (claset() addIs [MA2 RS Always_weaken]) 2);
+by (rtac (Detects_part1 RS LeadsTo_weaken_L) 1);
+by (Blast_tac 1);
+qed "Reachability_Detected";
+
+
+Goal "v : V ==> F : UNIV LeadsTo (reachable v <==> {s. (root,v) : REACHABLE})";
+by (etac (Reachability_Detected RS Detects_Imp_LeadstoEQ) 1);
+qed "LeadsTo_Reachability";
+
+(* ------------------------------------ *)
+
+(* Some lemmas about <==> *)
+
+Goalw [Equality_def]
+ "(reachable v <==> {s. (root,v) : REACHABLE}) = \
+\ {s. ((s : reachable v) = ((root,v) : REACHABLE))}";
+by (Blast_tac 1);
+qed "Eq_lemma1";
+
+
+Goalw [Equality_def]
+ "(reachable v <==> (if (root,v) : REACHABLE then UNIV else {})) = \
+\ {s. ((s : reachable v) = ((root,v) : REACHABLE))}";
+by Auto_tac;
+qed "Eq_lemma2";
+
+(* ------------------------------------ *)
+
+
+(* Some lemmas about final (I don't need all of them!) *)
+
+Goalw [final_def, Equality_def]
+ "(INT v: V. INT w:V. {s. ((s : reachable v) = ((root,v) : REACHABLE)) & \
+\ s : nmsg_eq 0 (v,w)}) \
+\ <= final";
+by Auto_tac;
+by (ftac E_imp_in_V_R 1);
+by (ftac E_imp_in_V_L 1);
+by (Blast_tac 1);
+qed "final_lemma1";
+
+Goalw [final_def, Equality_def]
+ "E~={} \
+\ ==> (INT v: V. INT e: E. {s. ((s : reachable v) = ((root,v) : REACHABLE))} \
+\ Int nmsg_eq 0 e) <= final";
+by (auto_tac (claset(), simpset() addsplits [split_if_asm]));
+by (ftac E_imp_in_V_L 1);
+by (Blast_tac 1);
+qed "final_lemma2";
+
+Goal "E~={} \
+\ ==> (INT v: V. INT e: E. \
+\ (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e) \
+\ <= final";
+by (ftac final_lemma2 1);
+by (simp_tac (simpset() addsimps [Eq_lemma2]) 1);
+qed "final_lemma3";
+
+
+Goal "E~={} \
+\ ==> (INT v: V. INT e: E. \
+\ {s. ((s : reachable v) = ((root,v) : REACHABLE))} Int nmsg_eq 0 e) \
+\ = final";
+by (rtac subset_antisym 1);
+by (etac final_lemma2 1);
+by (rewrite_goals_tac [final_def,Equality_def]);
+by (Blast_tac 1);
+qed "final_lemma4";
+
+Goal "E~={} \
+\ ==> (INT v: V. INT e: E. \
+\ ((reachable v) <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e) \
+\ = final";
+by (ftac final_lemma4 1);
+by (simp_tac (simpset() addsimps [Eq_lemma2]) 1);
+qed "final_lemma5";
+
+
+Goal "(INT v: V. INT w: V. \
+\ (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 (v,w)) \
+\ <= final";
+by (simp_tac (simpset() addsimps [Eq_lemma2, Int_def]) 1);
+by (rtac final_lemma1 1);
+qed "final_lemma6";
+
+
+Goalw [final_def]
+ "final = \
+\ (INT v: V. INT w: V. \
+\ ((reachable v) <==> {s. (root,v) : REACHABLE}) Int \
+\ (-{s. (v,w) : E} Un (nmsg_eq 0 (v,w))))";
+by (rtac subset_antisym 1);
+by (Blast_tac 1);
+by (auto_tac (claset(), simpset() addsplits [split_if_asm]));
+by (ftac E_imp_in_V_R 1);
+by (ftac E_imp_in_V_L 1);
+by (Blast_tac 1);
+qed "final_lemma7";
+
+(* ------------------------------------ *)
+
+
+(* ------------------------------------ *)
+
+(* Stability theorems *)
+
+
+Goal "[| v : V; (root,v) ~: REACHABLE |] ==> F : Stable (- reachable v)";
+by (dtac (MA2 RS AlwaysD) 1);
+by Auto_tac;
+qed "not_REACHABLE_imp_Stable_not_reachable";
+
+Goal "v : V ==> F : Stable (reachable v <==> {s. (root,v) : REACHABLE})";
+by (simp_tac (simpset() addsimps [Equality_def, Eq_lemma2]) 1);
+by (blast_tac (claset() addIs [MA6,not_REACHABLE_imp_Stable_not_reachable]) 1);
+qed "Stable_reachable_EQ_R";
+
+
+Goalw [nmsg_gte_def, nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
+ "((nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w)) Int (- nmsg_gt 0 (v,w) Un A)) \
+\ <= A Un nmsg_eq 0 (v,w)";
+by Auto_tac;
+qed "lemma4";
+
+
+Goalw [nmsg_gte_def,nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
+ "reachable v Int nmsg_eq 0 (v,w) = \
+\ ((nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w)) Int \
+\ (reachable v Int nmsg_lte 0 (v,w)))";
+by Auto_tac;
+qed "lemma5";
+
+Goalw [nmsg_gte_def,nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
+ "- nmsg_gt 0 (v,w) Un reachable v <= nmsg_eq 0 (v,w) Un reachable v";
+by Auto_tac;
+qed "lemma6";
+
+Goal "[|v : V; w : V|] ==> F : Always (reachable v Un nmsg_eq 0 (v,w))";
+by (rtac ([MA5, MA3] MRS Always_Int_I RS Always_weaken) 1);
+by (rtac lemma4 5);
+by Auto_tac;
+qed "Always_reachable_OR_nmsg_0";
+
+Goal "[|v : V; w : V|] ==> F : Stable (reachable v Int nmsg_eq 0 (v,w))";
+by (stac lemma5 1);
+by (blast_tac (claset() addIs [MA5, Always_imp_Stable RS Stable_Int, MA6b]) 1);
+qed "Stable_reachable_AND_nmsg_0";
+
+Goal "[|v : V; w : V|] ==> F : Stable (nmsg_eq 0 (v,w) Un reachable v)";
+by (blast_tac (claset() addSIs [Always_weaken RS Always_imp_Stable,
+ lemma6, MA3]) 1);
+qed "Stable_nmsg_0_OR_reachable";
+
+Goal "[| v : V; w:V; (root,v) ~: REACHABLE |] \
+\ ==> F : Stable (- reachable v Int nmsg_eq 0 (v,w))";
+by (rtac ([MA2 RS Always_imp_Stable, Stable_nmsg_0_OR_reachable] MRS
+ Stable_Int RS Stable_eq) 1);
+by (Blast_tac 4);
+by Auto_tac;
+qed "not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0";
+
+Goal "[| v : V; w:V |] \
+\ ==> F : Stable ((reachable v <==> {s. (root,v) : REACHABLE}) Int \
+\ nmsg_eq 0 (v,w))";
+by (asm_simp_tac
+ (simpset() addsimps [Equality_def, Eq_lemma2,
+ not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0,
+ Stable_reachable_AND_nmsg_0]) 1);
+qed "Stable_reachable_EQ_R_AND_nmsg_0";
+
+
+(* ------------------------------------ *)
+
+
+(* LeadsTo final predicate (Exercise 11.2 page 274) *)
+
+Goal "UNIV <= (INT v: V. UNIV)";
+by (Blast_tac 1);
+val UNIV_lemma = result();
+
+val UNIV_LeadsTo_completion =
+ [Finite_stable_completion, UNIV_lemma] MRS LeadsTo_weaken_L;
+
+Goalw [final_def] "E={} ==> F : UNIV LeadsTo final";
+by (Asm_full_simp_tac 1);
+by (rtac UNIV_LeadsTo_completion 1);
+by Safe_tac;
+by (etac (simplify (simpset()) LeadsTo_Reachability) 1);
+by (dtac Stable_reachable_EQ_R 1);
+by (Asm_full_simp_tac 1);
+qed "LeadsTo_final_E_empty";
+
+
+Goal "[| v : V; w:V |] \
+\ ==> F : UNIV LeadsTo \
+\ ((reachable v <==> {s. (root,v): REACHABLE}) Int nmsg_eq 0 (v,w))";
+by (rtac (LeadsTo_Reachability RS LeadsTo_Trans) 1);
+by (Blast_tac 1);
+by (subgoal_tac "F : (reachable v <==> {s. (root,v) : REACHABLE}) Int UNIV LeadsTo (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 (v,w)" 1);
+by (Asm_full_simp_tac 1);
+by (rtac PSP_Stable2 1);
+by (rtac MA7 1);
+by (rtac Stable_reachable_EQ_R 3);
+by Auto_tac;
+qed "Leadsto_reachability_AND_nmsg_0";
+
+
+Goal "E~={} ==> F : UNIV LeadsTo final";
+by (rtac ([LeadsTo_weaken_R, UNIV_lemma] MRS LeadsTo_weaken_L) 1);
+by (rtac final_lemma6 2);
+by (rtac Finite_stable_completion 1);
+by (Blast_tac 1);
+by (rtac UNIV_LeadsTo_completion 1);
+by (REPEAT
+ (blast_tac (claset() addIs [Stable_INT,
+ Stable_reachable_EQ_R_AND_nmsg_0,
+ Leadsto_reachability_AND_nmsg_0]) 1));
+qed "LeadsTo_final_E_NOT_empty";
+
+
+Goal "F : UNIV LeadsTo final";
+by (case_tac "E={}" 1);
+by (rtac LeadsTo_final_E_NOT_empty 2);
+by (rtac LeadsTo_final_E_empty 1);
+by Auto_tac;
+qed "LeadsTo_final";
+
+(* ------------------------------------ *)
+
+(* Stability of final (Exercise 11.2 page 274) *)
+
+Goalw [final_def] "E={} ==> F : Stable final";
+by (Asm_full_simp_tac 1);
+by (rtac Stable_INT 1);
+by (dtac Stable_reachable_EQ_R 1);
+by (Asm_full_simp_tac 1);
+qed "Stable_final_E_empty";
+
+
+Goal "E~={} ==> F : Stable final";
+by (stac final_lemma7 1);
+by (rtac Stable_INT 1);
+by (rtac Stable_INT 1);
+by (simp_tac (simpset() addsimps [Eq_lemma2]) 1);
+by Safe_tac;
+by (rtac Stable_eq 1);
+by (subgoal_tac "({s. (s : reachable v) = ((root,v) : REACHABLE)} Int nmsg_eq 0 (v,w)) = \
+\ ({s. (s : reachable v) = ((root,v) : REACHABLE)} Int (- UNIV Un nmsg_eq 0 (v,w)))" 2);
+by (Blast_tac 2); by (Blast_tac 2);
+by (rtac (simplify (simpset() addsimps [Eq_lemma2]) Stable_reachable_EQ_R_AND_nmsg_0) 1);
+by (Blast_tac 1);by (Blast_tac 1);
+by (rtac Stable_eq 1);
+by (subgoal_tac "({s. (s : reachable v) = ((root,v) : REACHABLE)}) = ({s. (s : reachable v) = ((root,v) : REACHABLE)} Int (- {} Un nmsg_eq 0 (v,w)))" 2);
+by (Blast_tac 2); by (Blast_tac 2);
+by (rtac (simplify (simpset() addsimps [Eq_lemma2]) Stable_reachable_EQ_R) 1);
+by Auto_tac;
+qed "Stable_final_E_NOT_empty";
+
+Goal "F : Stable final";
+by (case_tac "E={}" 1);
+by (blast_tac (claset() addIs [Stable_final_E_NOT_empty]) 2);
+by (blast_tac (claset() addIs [Stable_final_E_empty]) 1);
+qed "Stable_final";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Reachability.thy Fri Mar 03 18:26:19 2000 +0100
@@ -0,0 +1,72 @@
+(* Title: HOL/UNITY/Reachability
+ ID: $Id$
+ Author: Tanja Vos, Cambridge University Computer Laboratory
+ Copyright 2000 University of Cambridge
+
+Reachability in Graphs
+
+From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2 and 11.3
+*)
+
+Reachability = Detects +
+
+types edge = "(vertex*vertex)"
+
+record state =
+ reach :: vertex => bool
+ nmsg :: edge => nat
+
+consts REACHABLE :: edge set
+ root :: vertex
+ E :: edge set
+ V :: vertex set
+
+inductive "REACHABLE"
+ intrs
+ base "v : V ==> ((v,v) : REACHABLE)"
+ step "((u,v) : REACHABLE) & (v,w) : E ==> ((u,w) : REACHABLE)"
+
+constdefs
+ reachable :: vertex => state set
+ "reachable p == {s. reach s p}"
+
+ nmsg_eq :: nat => edge => state set
+ "nmsg_eq k == %e. {s. nmsg s e = k}"
+
+ nmsg_gt :: nat => edge => state set
+ "nmsg_gt k == %e. {s. k < nmsg s e}"
+
+ nmsg_gte :: nat => edge => state set
+ "nmsg_gte k == %e. {s. k <= nmsg s e}"
+
+ nmsg_lte :: nat => edge => state set
+ "nmsg_lte k == %e. {s. nmsg s e <= k}"
+
+
+
+ final :: state set
+ "final == (INTER V (%v. reachable v <==> {s. (root, v) : REACHABLE})) Int (INTER E (nmsg_eq 0))"
+
+rules
+ Graph1 "root : V"
+
+ Graph2 "(v,w) : E ==> (v : V) & (w : V)"
+
+ MA1 "F : Always (reachable root)"
+
+ MA2 "[|v:V|] ==> F : Always (- reachable v Un {s. ((root,v) : REACHABLE)})"
+
+ MA3 "[|v:V;w:V|] ==> F : Always (-(nmsg_gt 0 (v,w)) Un (reachable v))"
+
+ MA4 "[|(v,w) : E|] ==> F : Always (-(reachable v) Un (nmsg_gt 0 (v,w)) Un (reachable w))"
+
+ MA5 "[|v:V;w:V|] ==> F : Always (nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w))"
+
+ MA6 "[|v:V|] ==> F : Stable (reachable v)"
+
+ MA6b "[|v:V;w:W|] ==> F : Stable (reachable v Int nmsg_lte k (v,w))"
+
+ MA7 "[|v:V;w:V|] ==> F : UNIV LeadsTo nmsg_eq 0 (v,w)"
+
+end
+
--- a/src/HOL/UNITY/SubstAx.ML Fri Mar 03 18:22:53 2000 +0100
+++ b/src/HOL/UNITY/SubstAx.ML Fri Mar 03 18:26:19 2000 +0100
@@ -376,25 +376,6 @@
(*** Completion: Binary and General Finite versions ***)
-Goal "[| F : A LeadsTo A'; F : Stable A'; \
-\ F : B LeadsTo B'; F : Stable B' |] \
-\ ==> F : (A Int B) LeadsTo (A' Int B')";
-by (full_simp_tac
- (simpset() addsimps [LeadsTo_eq_leadsTo, Stable_eq_stable]) 1);
-by (blast_tac (claset() addIs [stable_completion, leadsTo_weaken]) 1);
-qed "Stable_completion";
-
-
-Goal "finite I \
-\ ==> (ALL i:I. F : (A i) LeadsTo (A' i)) --> \
-\ (ALL i:I. F : Stable (A' i)) --> \
-\ F : (INT i:I. A i) LeadsTo (INT i:I. A' i)";
-by (etac finite_induct 1);
-by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [Stable_completion, ball_Stable_INT]) 1);
-qed_spec_mp "Finite_stable_completion";
-
-
Goal "[| F : A LeadsTo (A' Un C); F : A' Co (A' Un C); \
\ F : B LeadsTo (B' Un C); F : B' Co (B' Un C) |] \
\ ==> F : (A Int B) LeadsTo ((A' Int B') Un C)";
@@ -404,17 +385,43 @@
by (blast_tac (claset() addIs [completion, leadsTo_weaken]) 1);
qed "Completion";
-
Goal "finite I \
\ ==> (ALL i:I. F : (A i) LeadsTo (A' i Un C)) --> \
\ (ALL i:I. F : (A' i) Co (A' i Un C)) --> \
\ F : (INT i:I. A i) LeadsTo ((INT i:I. A' i) Un C)";
by (etac finite_induct 1);
+by Auto_tac;
+by (rtac Completion 1);
+by (simp_tac (HOL_ss addsimps (INT_simps RL [sym])) 4);
+by (rtac Constrains_INT 4);
+by Auto_tac;
+val lemma = result();
+
+val prems = Goal
+ "[| finite I; \
+\ !!i. i:I ==> F : (A i) LeadsTo (A' i Un C); \
+\ !!i. i:I ==> F : (A' i) Co (A' i Un C) |] \
+\ ==> F : (INT i:I. A i) LeadsTo ((INT i:I. A' i) Un C)";
+by (blast_tac (claset() addIs (lemma RS mp RS mp)::prems) 1);
+qed "Finite_completion";
+
+Goalw [Stable_def]
+ "[| F : A LeadsTo A'; F : Stable A'; \
+\ F : B LeadsTo B'; F : Stable B' |] \
+\ ==> F : (A Int B) LeadsTo (A' Int B')";
+by (res_inst_tac [("C1", "{}")] (Completion RS LeadsTo_weaken_R) 1);
+by (REPEAT (Force_tac 1));
+qed "Stable_completion";
+
+val prems = Goalw [Stable_def]
+ "[| finite I; \
+\ !!i. i:I ==> F : (A i) LeadsTo (A' i); \
+\ !!i. i:I ==> F : Stable (A' i) |] \
+\ ==> F : (INT i:I. A i) LeadsTo (INT i:I. A' i)";
+by (res_inst_tac [("C1", "{}")] (Finite_completion RS LeadsTo_weaken_R) 1);
by (ALLGOALS Asm_simp_tac);
-by (Clarify_tac 1);
-by (dtac ball_Constrains_INT 1);
-by (asm_full_simp_tac (simpset() addsimps [Completion]) 1);
-qed_spec_mp "Finite_completion";
+by (ALLGOALS (blast_tac (claset() addIs prems)));
+qed "Finite_stable_completion";
(*proves "ensures/leadsTo" properties when the program is specified*)
--- a/src/HOL/UNITY/UNITY.ML Fri Mar 03 18:22:53 2000 +0100
+++ b/src/HOL/UNITY/UNITY.ML Fri Mar 03 18:26:19 2000 +0100
@@ -186,7 +186,7 @@
Goalw [constrains_def]
"ALL i:I. F : (A i) co (A' i) ==> F : (UN i:I. A i) co (UN i:I. A' i)";
by (Blast_tac 1);
-qed "ball_constrains_UN";
+bind_thm ("constrains_UN", ballI RS result());
Goalw [constrains_def] "(A Un B) co C = (A co C) Int (B co C)";
by (Blast_tac 1);
@@ -214,7 +214,7 @@
Goalw [constrains_def]
"ALL i:I. F : (A i) co (A' i) ==> F : (INT i:I. A i) co (INT i:I. A' i)";
by (Blast_tac 1);
-qed "ball_constrains_INT";
+bind_thm ("constrains_INT", ballI RS result());
Goalw [constrains_def] "F : A co A' ==> A <= A'";
by Auto_tac;
@@ -269,8 +269,8 @@
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";
+by (blast_tac (claset() addIs [constrains_UN]) 1);
+bind_thm ("stable_UN", ballI RS result());
(** Intersection **)
@@ -281,8 +281,8 @@
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";
+by (blast_tac (claset() addIs [constrains_INT]) 1);
+bind_thm ("stable_INT", ballI RS result());
Goalw [stable_def, constrains_def]
"[| F : stable C; F : A co (C Un A') |] ==> F : (C Un A) co (C Un A')";
--- a/src/HOL/UNITY/WFair.ML Fri Mar 03 18:22:53 2000 +0100
+++ b/src/HOL/UNITY/WFair.ML Fri Mar 03 18:26:19 2000 +0100
@@ -240,10 +240,6 @@
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1);
qed "leadsTo_Diff";
-
-(** Meta or object quantifier ???
- see ball_constrains_UN in UNITY.ML***)
-
val prems = goal thy
"(!! i. i:I ==> F : (A i) leadsTo (A' i)) \
\ ==> F : (UN i:I. A i) leadsTo (UN i:I. A' i)";
@@ -467,22 +463,22 @@
(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
-Goal "F : A leadsTo A' ==> \
-\ EX B. A<=B & F : B leadsTo A' & F : (B-A') co (B Un A')";
+Goal "F : A leadsTo A' \
+\ ==> EX B. A<=B & F : B leadsTo A' & F : (B-A') co (B Un A')";
by (etac leadsTo_induct 1);
(*Basis*)
-by (blast_tac (claset() addIs [leadsTo_Basis]
- addDs [ensuresD]) 1);
+by (blast_tac (claset() addIs [leadsTo_Basis] addDs [ensuresD]) 1);
(*Trans*)
by (Clarify_tac 1);
by (res_inst_tac [("x", "Ba Un Bb")] exI 1);
by (blast_tac (claset() addIs [lemma1, leadsTo_Un_Un, leadsTo_cancel1,
leadsTo_Un_duplicate]) 1);
(*Union*)
-by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1,
- bchoice, ball_constrains_UN]) 1);;
+by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1, bchoice]) 1);;
by (res_inst_tac [("x", "UN A:S. f A")] exI 1);
-by (blast_tac (claset() addIs [leadsTo_UN, constrains_weaken]) 1);
+by (auto_tac (claset() addIs [leadsTo_UN], simpset()));
+(*Blast_tac says PROOF FAILED*)
+by (deepen_tac (claset() addIs [constrains_UN RS constrains_weaken]) 0 1);
qed "leadsTo_123";
@@ -531,10 +527,19 @@
\ F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)";
by (etac finite_induct 1);
by Auto_tac;
-by (dtac ball_constrains_INT 1);
-by (asm_full_simp_tac (simpset() addsimps [completion]) 1);
-qed_spec_mp "finite_completion";
+by (rtac completion 1);
+by (simp_tac (HOL_ss addsimps (INT_simps RL [sym])) 4);
+by (rtac constrains_INT 4);
+by Auto_tac;
+val lemma = result();
+val prems = Goal
+ "[| finite I; \
+\ !!i. i:I ==> F : (A i) leadsTo (A' i Un C); \
+\ !!i. i:I ==> F : (A' i) co (A' i Un C) |] \
+\ ==> F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)";
+by (blast_tac (claset() addIs (lemma RS mp RS mp)::prems) 1);
+qed "finite_completion";
Goalw [stable_def]
"[| F : A leadsTo A'; F : stable A'; \
@@ -544,13 +549,14 @@
by (REPEAT (Force_tac 1));
qed "stable_completion";
-Goalw [stable_def]
+val prems = Goalw [stable_def]
"[| finite I; \
-\ ALL i:I. F : (A i) leadsTo (A' i); \
-\ ALL i:I. F : stable (A' i) |] \
+\ !!i. i:I ==> F : (A i) leadsTo (A' i); \
+\ !!i. i:I ==> F : stable (A' i) |] \
\ ==> F : (INT i:I. A i) leadsTo (INT i:I. A' i)";
by (res_inst_tac [("C1", "{}")] (finite_completion RS leadsTo_weaken_R) 1);
-by (REPEAT (Force_tac 1));
-qed_spec_mp "finite_stable_completion";
+by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (blast_tac (claset() addIs prems)));
+qed "finite_stable_completion";