--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Channel.ML Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,67 @@
+(* Title: HOL/UNITY/Channel
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Unordered Channel
+
+From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
+*)
+
+open Channel;
+
+AddIffs [skip];
+
+
+(*None represents "infinity" while Some represents proper integers*)
+goalw thy [minSet_def] "!!A. minSet A = Some x --> x : A";
+by (Simp_tac 1);
+by (fast_tac (claset() addIs [LeastI]) 1);
+qed_spec_mp "minSet_eq_SomeD";
+
+goalw thy [minSet_def] " minSet{} = None";
+by (Asm_simp_tac 1);
+qed_spec_mp "minSet_empty";
+Addsimps [minSet_empty];
+
+goalw thy [minSet_def] "!!A. x:A ==> minSet A = Some (LEAST x. x: A)";
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1);
+qed_spec_mp "minSet_nonempty";
+
+goal thy
+ "leadsTo Acts (minSet -`` {Some x}) (minSet -`` (Some``greaterThan x))";
+by (rtac leadsTo_weaken 1);
+by (rtac ([UC2, UC1] MRS PSP) 1);
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1);
+by Safe_tac;
+by (auto_tac (claset() addDs [minSet_eq_SomeD],
+ simpset() addsimps [le_def, nat_neq_iff]));
+qed "minSet_greaterThan";
+
+
+(*The induction*)
+goal thy "leadsTo Acts (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);
+by Safe_tac;
+by (ALLGOALS Asm_simp_tac);
+by (dtac minSet_nonempty 2);
+by (Asm_full_simp_tac 2);
+by (rtac (minSet_greaterThan RS leadsTo_weaken) 1);
+by Safe_tac;
+by (ALLGOALS Asm_full_simp_tac);
+by (dtac minSet_nonempty 1);
+by (Asm_full_simp_tac 1);
+val lemma = result();
+
+
+goal thy "!!y::nat. leadsTo Acts (UNIV-{{}}) {s. y ~: s}";
+by (rtac (lemma RS leadsTo_weaken_R) 1);
+by (Clarify_tac 1);
+by (forward_tac [minSet_nonempty] 1);
+by (asm_full_simp_tac (simpset() addsimps [Suc_le_eq]) 1);
+by (blast_tac (claset() addDs [Suc_le_lessD, not_less_Least]) 1);
+qed "Channel_progress";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Channel.thy Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,29 @@
+(* Title: HOL/UNITY/Channel
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Unordered Channel
+
+From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
+*)
+
+Channel = WFair + Option +
+
+types state = nat set
+
+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 "constrains Acts {s. minSet s = x} {s. x <= minSet s}" *)
+
+ UC2 "leadsTo Acts (minSet -`` {Some x}) {s. x ~: s}"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Common.ML Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,102 @@
+(* Title: HOL/UNITY/Common
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Common Meeting Time example from Misra (1994)
+
+The state is identified with the one variable in existence.
+
+From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
+*)
+
+
+open Common;
+
+(*Misra's property CMT4: t exceeds no common meeting time*)
+goal thy
+ "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); n: common |] \
+\ ==> stable Acts (atMost n)";
+by (dres_inst_tac [("P", "%t. t<=n")] elimination_sing 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [atMost_def, stable_def, common_def, maxfg_def,
+ constrains_def, le_max_iff_disj]) 1);
+by (Clarify_tac 1);
+by (dtac bspec 1);
+by (assume_tac 1);
+by (blast_tac (claset() addSEs [subsetCE]
+ addIs [order_eq_refl, fmono, gmono, le_trans]) 1);
+qed "common_stable";
+
+goal thy
+ "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); n: common |] \
+\ ==> reachable {0} Acts <= atMost n";
+by (rtac strongest_invariant 1);
+by (asm_simp_tac (simpset() addsimps [common_stable]) 2);
+by (simp_tac (simpset() addsimps [atMost_def]) 1);
+qed "common_invariant";
+
+
+(*** Some programs that implement the safety property above ***)
+
+(*This one is just Skip*)
+goal thy "constrains {id} {m} (maxfg m)";
+by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj,
+ fasc, gasc]) 1);
+result();
+
+(*This one is t := ftime t || t := gtime t really needs Skip too*)
+goal thy "constrains {range(%t.(t,ftime t)), range(%t.(t,gtime t))} \
+\ {m} (maxfg m)";
+by (simp_tac (simpset() addsimps [constrains_def, maxfg_def,
+ le_max_iff_disj]) 1);
+by (Blast_tac 1);
+result();
+
+(*This one is t := max (ftime t) (gtime t) really needs Skip too*)
+goal thy "constrains {range(%t.(t, max (ftime t) (gtime t)))} \
+\ {m} (maxfg m)";
+by (simp_tac (simpset() addsimps [constrains_def, maxfg_def]) 1);
+by (Blast_tac 1);
+result();
+
+(*This one is t := t+1 if t <max (ftime t) (gtime t) *)
+goalw thy [constrains_def, maxfg_def]
+ "constrains { {(t, Suc t) | t. t < max (ftime t) (gtime t)} } \
+\ {m} (maxfg m)";
+by (blast_tac (claset() addIs [Suc_leI]) 1);
+result();
+
+
+(*It remans to prove that they satisfy CMT3': t does not decrease,
+ and that CMT3' implies that t stops changing once common(t) holds.*)
+
+
+(*** Progress under weak fairness ***)
+
+Addsimps [atMost_Int_atLeast];
+
+goal thy
+ "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); \
+\ ALL m: lessThan n. leadsTo Acts {m} (greaterThan m); \
+\ n: common; id: Acts |] \
+\ ==> leadsTo Acts (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);
+by (rtac subset_refl 2);
+by (blast_tac (claset() addDs [PSP_stable2]
+ addIs [common_stable, leadsTo_weaken_R]) 1);
+val lemma = result();
+
+(*The "ALL m: Compl common" form echoes CMT6.*)
+goal thy
+ "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); \
+\ ALL m: Compl common. leadsTo Acts {m} (greaterThan m); \
+\ n: common; id: Acts |] \
+\ ==> leadsTo Acts (atMost (LEAST n. n: common)) common";
+by (rtac lemma 1);
+by (ALLGOALS Asm_simp_tac);
+by (etac LeastI 2);
+by (blast_tac (claset() addSDs [not_less_Least]) 1);
+qed "leadsTo_common";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Common.thy Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,32 @@
+(* Title: HOL/UNITY/Common
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Common Meeting Time example from Misra (1994)
+
+The state is identified with the one variable in existence.
+
+From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
+*)
+
+Common = WFair +
+
+consts
+ ftime,gtime :: nat=>nat
+
+rules
+ fmono "m <= n ==> ftime m <= ftime n"
+ gmono "m <= n ==> gtime m <= gtime n"
+
+ fasc "m <= ftime n"
+ gasc "m <= gtime n"
+
+constdefs
+ common :: nat set
+ "common == {n. ftime n = n & gtime n = n}"
+
+ maxfg :: nat => nat set
+ "maxfg m == {t. t <= max (ftime m) (gtime m)}"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Deadlock.ML Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,90 @@
+
+
+(*** Deadlock examples from section 5.6 ***)
+
+(*Trivial, two-process case*)
+goalw thy [constrains_def, stable_def]
+ "!!Acts. [| constrains Acts (A Int B) A; constrains Acts (B Int A) B |] \
+\ ==> stable Acts (A Int B)";
+by (Blast_tac 1);
+result();
+
+
+goal thy "{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 thy "{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 thy "(INT i:{i. i <= n}. A(Suc i) Int A i) = \
+\ (INT i:{i. i <= Suc n}. A i)";
+by (induct_tac "n" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [Collect_le_Suc_insert])));
+by (blast_tac (claset() addEs [le_SucE] addSEs [equalityE]) 1);
+qed "Collect_le_Int_equals";
+
+
+(*Dual of the required property. Converse inclusion fails.*)
+goal thy "(UN i:{i. i < n}. A i) Int Compl (A n) <= \
+\ (UN i:{i. i < n}. (A i) Int Compl (A(Suc i)))";
+by (induct_tac "n" 1);
+by (Asm_simp_tac 1);
+by (simp_tac (simpset() addsimps [Collect_less_Suc_insert]) 1);
+by (Blast_tac 1);
+qed "UN_Int_Compl_subset";
+
+
+(*Converse inclusion fails.*)
+goal thy "(INT i:{i. i < n}. Compl(A i) Un A (Suc i)) <= \
+\ (INT i:{i. i < n}. Compl(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 (Blast_tac 1);
+qed "INT_Un_Compl_subset";
+
+
+(*Specialized rewriting*)
+goal thy "A 0 Int (Compl (A n) Int \
+\ (INT i:{i. i < n}. Compl(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 thy "(INT i:{i. i <= n}. A i) = \
+\ A 0 Int (INT i:{i. i < n}. Compl(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);
+qed "INT_le_equals_Int";
+
+goal thy "(INT i:{i. i <= Suc n}. A i) = \
+\ A 0 Int (INT i:{i. i <= n}. Compl(A i) Un A(Suc i))";
+by (simp_tac (simpset() addsimps [le_eq_less_Suc RS sym,
+ 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) \
+\ (Compl(A i) Un A(Suc i)) |] \
+\ ==> stable Acts (INT i:{i. i <= Suc n}. A i)";
+
+by (rtac ([zeroprem, allprem RS ball_constrains_INT] MRS
+ constrains_Int RS constrains_weaken) 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);
+result();
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Deadlock.thy Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,1 @@
+Deadlock = UNITY
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/FP.ML Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,66 @@
+(* Title: HOL/UNITY/FP
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Fixed Point of a Program
+
+From Misra, "A Logic for Concurrent Programming", 1994
+*)
+
+goal thy "Union(B) Int A = (UN C:B. C Int A)";
+by (Blast_tac 1);
+qed "Int_Union2";
+
+open FP;
+
+goalw thy [FP_Orig_def, stable_def] "stable Acts (FP_Orig Acts Int B)";
+by (stac Int_Union2 1);
+by (rtac ball_constrains_UN 1);
+by (Simp_tac 1);
+qed "stable_FP_Orig_Int";
+
+
+val prems = goalw thy [FP_Orig_def, stable_def]
+ "(!!B. stable Acts (A Int B)) ==> A <= FP_Orig Acts";
+by (blast_tac (claset() addIs prems) 1);
+qed "FP_Orig_weakest";
+
+
+goal thy "stable Acts (FP Acts Int B)";
+by (subgoal_tac "FP Acts Int B = (UN x:B. FP Acts 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]);
+by (rtac ball_constrains_UN 1);
+by (Simp_tac 1);
+qed "stable_FP_Int";
+
+goal thy "FP Acts <= FP_Orig Acts";
+by (rtac (stable_FP_Int RS FP_Orig_weakest) 1);
+val lemma1 = result();
+
+goalw thy [FP_Orig_def, FP_def] "FP_Orig Acts <= FP Acts";
+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 thy "FP Acts = FP_Orig Acts";
+by (rtac ([lemma1,lemma2] MRS equalityI) 1);
+qed "FP_equivalence";
+
+val [prem] = goal thy
+ "(!!B. stable Acts (A Int B)) ==> A <= FP Acts";
+by (simp_tac (simpset() addsimps [FP_equivalence, prem RS FP_Orig_weakest]) 1);
+qed "FP_weakest";
+
+goalw thy [FP_def, stable_def, constrains_def]
+ "Compl (FP Acts) = (UN act:Acts. Compl{s. act^^{s} <= {s}})";
+by (Blast_tac 1);
+qed "Compl_FP";
+
+goal thy "A - (FP Acts) = (UN act:Acts. A - {s. act^^{s} <= {s}})";
+by (simp_tac (simpset() addsimps [Diff_eq, Compl_FP]) 1);
+qed "Diff_FP";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/FP.thy Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,21 @@
+(* Title: HOL/UNITY/FP
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Fixed Point of a Program
+
+From Misra, "A Logic for Concurrent Programming", 1994
+*)
+
+FP = UNITY +
+
+constdefs
+
+ FP_Orig :: "('a * 'a)set set => 'a set"
+ "FP_Orig Acts == Union{A. ALL B. stable Acts (A Int B)}"
+
+ FP :: "('a * 'a)set set => 'a set"
+ "FP Acts == {s. stable Acts {s}}"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/LessThan.ML Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,146 @@
+(* Title: HOL/LessThan/LessThan
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+lessThan, greaterThan, atLeast, atMost
+*)
+
+
+open LessThan;
+
+
+(*** lessThan ***)
+
+goalw thy [lessThan_def] "(i: lessThan k) = (i<k)";
+by (Blast_tac 1);
+qed "lessThan_iff";
+AddIffs [lessThan_iff];
+
+goalw thy [lessThan_def] "lessThan 0 = {}";
+by (Simp_tac 1);
+qed "lessThan_0";
+Addsimps [lessThan_0];
+
+goalw thy [lessThan_def] "lessThan (Suc k) = insert k (lessThan k)";
+by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
+by (Blast_tac 1);
+qed "lessThan_Suc";
+
+goal thy "(UN m. lessThan m) = UNIV";
+by (Blast_tac 1);
+qed "UN_lessThan_UNIV";
+
+goalw thy [lessThan_def, atLeast_def, le_def]
+ "Compl(lessThan k) = atLeast k";
+by (Blast_tac 1);
+qed "Compl_lessThan";
+
+
+(*** greaterThan ***)
+
+goalw thy [greaterThan_def] "(i: greaterThan k) = (k<i)";
+by (Blast_tac 1);
+qed "greaterThan_iff";
+AddIffs [greaterThan_iff];
+
+goalw thy [greaterThan_def] "greaterThan 0 = range Suc";
+by (blast_tac (claset() addIs [Suc_pred RS sym]) 1);
+qed "greaterThan_0";
+Addsimps [greaterThan_0];
+
+goalw thy [greaterThan_def] "greaterThan (Suc k) = greaterThan k - {Suc k}";
+by Safe_tac;
+by (blast_tac (claset() addIs [less_trans]) 1);
+by (asm_simp_tac (simpset() addsimps [le_Suc_eq, not_le_iff_less RS sym]) 1);
+by (asm_simp_tac (simpset() addsimps [not_le_iff_less]) 1);
+qed "greaterThan_Suc";
+
+goal thy "(INT m. greaterThan m) = {}";
+by (Blast_tac 1);
+qed "INT_greaterThan_UNIV";
+
+goalw thy [greaterThan_def, atMost_def, le_def]
+ "Compl(greaterThan k) = atMost k";
+by (Blast_tac 1);
+qed "Compl_greaterThan";
+
+goalw thy [greaterThan_def, atMost_def, le_def]
+ "Compl(atMost k) = greaterThan k";
+by (Blast_tac 1);
+qed "Compl_atMost";
+
+goal thy "less_than ^^ {k} = greaterThan k";
+by (Blast_tac 1);
+qed "Image_less_than";
+
+Addsimps [Compl_greaterThan, Compl_atMost, Image_less_than];
+
+(*** atLeast ***)
+
+goalw thy [atLeast_def] "(i: atLeast k) = (k<=i)";
+by (Blast_tac 1);
+qed "atLeast_iff";
+AddIffs [atLeast_iff];
+
+goalw thy [atLeast_def, UNIV_def] "atLeast 0 = UNIV";
+by (Simp_tac 1);
+qed "atLeast_0";
+Addsimps [atLeast_0];
+
+goalw thy [atLeast_def] "atLeast (Suc k) = atLeast k - {k}";
+by (simp_tac (simpset() addsimps [Suc_le_eq]) 1);
+by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
+by (Blast_tac 1);
+qed "atLeast_Suc";
+
+goal thy "(UN m. atLeast m) = UNIV";
+by (Blast_tac 1);
+qed "UN_atLeast_UNIV";
+
+goalw thy [lessThan_def, atLeast_def, le_def]
+ "Compl(atLeast k) = lessThan k";
+by (Blast_tac 1);
+qed "Compl_atLeast";
+
+goal thy "less_than^-1 ^^ {k} = lessThan k";
+by (Blast_tac 1);
+qed "Image_inverse_less_than";
+
+Addsimps [Compl_lessThan, Compl_atLeast, Image_inverse_less_than];
+
+(*** atMost ***)
+
+goalw thy [atMost_def] "(i: atMost k) = (i<=k)";
+by (Blast_tac 1);
+qed "atMost_iff";
+AddIffs [atMost_iff];
+
+goalw thy [atMost_def] "atMost 0 = {0}";
+by (Simp_tac 1);
+qed "atMost_0";
+Addsimps [atMost_0];
+
+goalw thy [atMost_def] "atMost (Suc k) = insert (Suc k) (atMost k)";
+by (simp_tac (simpset() addsimps [less_Suc_eq, le_eq_less_or_eq]) 1);
+by (Blast_tac 1);
+qed "atMost_Suc";
+
+goal thy "(UN m. atMost m) = UNIV";
+by (Blast_tac 1);
+qed "UN_atMost_UNIV";
+
+goalw thy [atMost_def, le_def]
+ "Compl(atMost k) = greaterThan k";
+by (Blast_tac 1);
+qed "Compl_atMost";
+Addsimps [Compl_atMost];
+
+
+(*** Combined properties ***)
+
+goal thy "atMost n Int atLeast n = {n}";
+by (blast_tac (claset() addIs [le_anti_sym]) 1);
+qed "atMost_Int_atLeast";
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/LessThan.thy Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,25 @@
+(* Title: HOL/UNITY/LessThan
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+lessThan, greaterThan, atLeast, atMost
+*)
+
+LessThan = List +
+
+constdefs
+
+ lessThan :: "nat => nat set"
+ "lessThan n == {i. i<n}"
+
+ atMost :: "nat => nat set"
+ "atMost n == {i. i<=n}"
+
+ greaterThan :: "nat => nat set"
+ "greaterThan n == {i. n<i}"
+
+ atLeast :: "nat => nat set"
+ "atLeast n == {i. n<=i}"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Mutex.ML Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,254 @@
+(* Title: HOL/UNITY/Mutex.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
+*)
+
+open Mutex;
+
+val cmd_defs = [mutex_def, cmd0_def, cmd1u_def, cmd1v_def,
+ cmd2_def, cmd3_def, cmd4_def];
+
+goalw thy [mutex_def] "id : mutex";
+by (Simp_tac 1);
+qed "id_in_mutex";
+AddIffs [id_in_mutex];
+
+
+(** Constrains/Ensures tactics: NEED TO BE GENERALIZED OVER ALL PROGRAMS **)
+
+(*proves "constrains" properties when the program is specified*)
+val constrains_tac =
+ SELECT_GOAL
+ (EVERY [rtac constrainsI 1,
+ rewtac mutex_def,
+ REPEAT_FIRST (eresolve_tac [insertE, emptyE]),
+ rewrite_goals_tac cmd_defs,
+ ALLGOALS (SELECT_GOAL Auto_tac)]);
+
+
+(*proves "ensures" properties when the program is specified*)
+fun ensures_tac sact =
+ SELECT_GOAL
+ (EVERY [REPEAT (resolve_tac [LeadsTo_Basis, leadsTo_Basis, ensuresI] 1),
+ res_inst_tac [("act", sact)] transient_mem 2,
+ Simp_tac 2,
+ constrains_tac 1,
+ rewrite_goals_tac cmd_defs,
+ Auto_tac]);
+
+
+(*The booleans p, u, v are always either 0 or 1*)
+goalw thy [stable_def, boolVars_def]
+ "stable mutex boolVars";
+by (constrains_tac 1);
+by (auto_tac (claset() addSEs [less_SucE], simpset()));
+qed "stable_boolVars";
+
+goal thy "reachable MInit mutex <= boolVars";
+by (rtac strongest_invariant 1);
+by (rtac stable_boolVars 2);
+by (rewrite_goals_tac [MInit_def, boolVars_def]);
+by Auto_tac;
+qed "reachable_subset_boolVars";
+
+val reachable_subset_boolVars' =
+ rewrite_rule [boolVars_def] reachable_subset_boolVars;
+
+goalw thy [stable_def, invariant_def]
+ "stable mutex (invariant 0 UU MM)";
+by (constrains_tac 1);
+qed "stable_invar_0um";
+
+goalw thy [stable_def, invariant_def]
+ "stable mutex (invariant 1 VV NN)";
+by (constrains_tac 1);
+qed "stable_invar_1vn";
+
+goalw thy [MInit_def, invariant_def] "MInit <= invariant 0 UU MM";
+by Auto_tac;
+qed "MInit_invar_0um";
+
+goalw thy [MInit_def, invariant_def] "MInit <= invariant 1 VV NN";
+by Auto_tac;
+qed "MInit_invar_1vn";
+
+(*The intersection is an invariant of the system*)
+goal thy "reachable MInit mutex <= invariant 0 UU MM Int invariant 1 VV NN";
+by (simp_tac (simpset() addsimps
+ [strongest_invariant, Int_greatest, stable_Int,
+ stable_invar_0um, stable_invar_1vn,
+ MInit_invar_0um,MInit_invar_1vn]) 1);
+qed "reachable_subset_invariant";
+
+val reachable_subset_invariant' =
+ rewrite_rule [invariant_def] reachable_subset_invariant;
+
+
+(*The safety property (mutual exclusion) follows from the claimed invar_s*)
+goalw thy [invariant_def]
+ "{s. s MM = 3 & s NN = 3} <= \
+\ Compl (invariant 0 UU MM Int invariant 1 VV NN)";
+by Auto_tac;
+val lemma = result();
+
+goal thy "{s. s MM = 3 & s NN = 3} <= Compl (reachable MInit mutex)";
+by (rtac ([lemma, reachable_subset_invariant RS Compl_anti_mono] MRS subset_trans) 1);
+qed "mutual_exclusion";
+
+
+(*The bad invariant FAILS in cmd1v*)
+goalw thy [stable_def, bad_invariant_def]
+ "stable mutex (bad_invariant 0 UU MM)";
+by (constrains_tac 1);
+by (trans_tac 1);
+by (safe_tac (claset() addSEs [le_SucE]));
+by (Asm_full_simp_tac 1);
+(*Resulting state: n=1, p=false, m=4, u=false.
+ Execution of cmd1v (the command of process v guarded by n=1) sets p:=true,
+ violating the invariant!*)
+(*Check that subgoals remain: proof failed.*)
+getgoal 1;
+
+
+(*** Progress for U ***)
+
+goalw thy [unless_def] "unless mutex {s. s MM=2} {s. s MM=3}";
+by (constrains_tac 1);
+qed "U_F0";
+
+goal thy "LeadsTo MInit mutex {s. s MM=1} {s. s PP = s VV & s MM = 2}";
+by (rtac leadsTo_imp_LeadsTo 1); (*makes the proof much faster*)
+by (ensures_tac "cmd1u" 1);
+qed "U_F1";
+
+goal thy "LeadsTo MInit mutex {s. s PP = 0 & s MM = 2} {s. s MM = 3}";
+by (cut_facts_tac [reachable_subset_invariant'] 1);
+by (ensures_tac "cmd2 0 MM" 1);
+qed "U_F2";
+
+goalw thy [mutex_def] "LeadsTo MInit mutex {s. s MM = 3} {s. s PP = 1}";
+by (rtac leadsTo_imp_LeadsTo 1);
+by (res_inst_tac [("B", "{s. s MM = 4}")] leadsTo_Trans 1);
+by (ensures_tac "cmd4 1 MM" 2);
+by (ensures_tac "cmd3 UU MM" 1);
+qed "U_F3";
+
+goal thy "LeadsTo MInit mutex {s. s MM = 2} {s. s PP = 1}";
+by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo]
+ MRS LeadsTo_Diff) 1);
+by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
+by (cut_facts_tac [reachable_subset_boolVars'] 1);
+by (auto_tac (claset() addSEs [less_SucE], simpset()));
+val lemma2 = result();
+
+goal thy "LeadsTo MInit mutex {s. s MM = 1} {s. s PP = 1}";
+by (rtac ([U_F1 RS LeadsTo_weaken_R, lemma2] MRS LeadsTo_Trans) 1);
+by (Blast_tac 1);
+val lemma1 = result();
+
+
+goal thy "LeadsTo MInit mutex {s. 1 <= s MM & s MM <= 3} {s. s PP = 1}";
+by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL]
+ addcongs [rev_conj_cong]) 1);
+by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
+ lemma1, lemma2, U_F3] ) 1);
+val lemma123 = result();
+
+
+(*Misra's F4*)
+goal thy "LeadsTo MInit mutex {s. s UU = 1} {s. s PP = 1}";
+by (rtac LeadsTo_weaken_L 1);
+by (rtac lemma123 1);
+by (cut_facts_tac [reachable_subset_invariant'] 1);
+by Auto_tac;
+qed "u_leadsto_p";
+
+
+(*** Progress for V ***)
+
+
+goalw thy [unless_def] "unless mutex {s. s NN=2} {s. s NN=3}";
+by (constrains_tac 1);
+qed "V_F0";
+
+goal thy "LeadsTo MInit mutex {s. s NN=1} {s. s PP = 1 - s UU & s NN = 2}";
+by (rtac leadsTo_imp_LeadsTo 1); (*makes the proof much faster*)
+by (ensures_tac "cmd1v" 1);
+qed "V_F1";
+
+goal thy "LeadsTo MInit mutex {s. s PP = 1 & s NN = 2} {s. s NN = 3}";
+by (cut_facts_tac [reachable_subset_invariant'] 1);
+by (ensures_tac "cmd2 1 NN" 1);
+qed "V_F2";
+
+goalw thy [mutex_def] "LeadsTo MInit mutex {s. s NN = 3} {s. s PP = 0}";
+by (rtac leadsTo_imp_LeadsTo 1);
+by (res_inst_tac [("B", "{s. s NN = 4}")] leadsTo_Trans 1);
+by (ensures_tac "cmd4 0 NN" 2);
+by (ensures_tac "cmd3 VV NN" 1);
+qed "V_F3";
+
+goal thy "LeadsTo MInit mutex {s. s NN = 2} {s. s PP = 0}";
+by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo]
+ MRS LeadsTo_Diff) 1);
+by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
+by (cut_facts_tac [reachable_subset_boolVars'] 1);
+by (auto_tac (claset() addSEs [less_SucE], simpset()));
+val lemma2 = result();
+
+goal thy "LeadsTo MInit mutex {s. s NN = 1} {s. s PP = 0}";
+by (rtac ([V_F1 RS LeadsTo_weaken_R, lemma2] MRS LeadsTo_Trans) 1);
+by (Blast_tac 1);
+val lemma1 = result();
+
+
+goal thy "LeadsTo MInit mutex {s. 1 <= s NN & s NN <= 3} {s. s PP = 0}";
+by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL]
+ addcongs [rev_conj_cong]) 1);
+by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
+ lemma1, lemma2, V_F3] ) 1);
+val lemma123 = result();
+
+
+(*Misra's F4*)
+goal thy "LeadsTo MInit mutex {s. s VV = 1} {s. s PP = 0}";
+by (rtac LeadsTo_weaken_L 1);
+by (rtac lemma123 1);
+by (cut_facts_tac [reachable_subset_invariant'] 1);
+by Auto_tac;
+qed "v_leadsto_not_p";
+
+
+(** Absence of starvation **)
+
+(*Misra's F6*)
+goal thy "LeadsTo MInit mutex {s. s MM = 1} {s. s MM = 3}";
+by (rtac LeadsTo_Un_duplicate 1);
+by (rtac LeadsTo_cancel2 1);
+by (rtac U_F2 2);
+by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
+by (stac Un_commute 1);
+by (rtac LeadsTo_Un_duplicate 1);
+by (rtac ([v_leadsto_not_p, U_F0] MRS R_PSP_unless RSN(2, LeadsTo_cancel2)) 1);
+by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
+by (cut_facts_tac [reachable_subset_boolVars'] 1);
+by (auto_tac (claset() addSEs [less_SucE], simpset()));
+qed "m1_leadsto_3";
+
+
+(*The same for V*)
+goal thy "LeadsTo MInit mutex {s. s NN = 1} {s. s NN = 3}";
+by (rtac LeadsTo_Un_duplicate 1);
+by (rtac LeadsTo_cancel2 1);
+by (rtac V_F2 2);
+by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
+by (stac Un_commute 1);
+by (rtac LeadsTo_Un_duplicate 1);
+by (rtac ([u_leadsto_p, V_F0] MRS R_PSP_unless RSN(2, LeadsTo_cancel2)) 1);
+by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
+by (cut_facts_tac [reachable_subset_boolVars'] 1);
+by (auto_tac (claset() addSEs [less_SucE], simpset()));
+qed "n1_leadsto_3";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Mutex.thy Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,74 @@
+(* Title: HOL/UNITY/Mutex.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
+*)
+
+Mutex = Update + UNITY + Traces + SubstAx +
+
+(*WE NEED A GENERAL TREATMENT OF NUMBERS!!*)
+syntax
+ "3" :: nat ("3")
+ "4" :: nat ("4")
+
+translations
+ "3" == "Suc 2"
+ "4" == "Suc 3"
+
+
+(*program variables*)
+datatype pvar = PP | MM | NN | UU | VV
+
+(*No booleans; instead True=1 and False=0*)
+types state = pvar => nat
+
+constdefs
+ cmd0 :: "[pvar,pvar] => (state*state) set"
+ "cmd0 u m == {(s,s'). s' = s[u|->1][m|->1] & s m = 0}"
+
+ cmd1u :: "(state*state) set"
+ "cmd1u == {(s,s'). s' = s[PP|-> s VV][MM|->2] & s MM = 1}"
+
+ cmd1v :: "(state*state) set"
+ "cmd1v == {(s,s'). s' = s[PP|-> 1 - s UU][NN|->2] & s NN = 1}"
+
+ (*Put pv=0 for u's program and pv=1 for v's program*)
+ cmd2 :: "[nat,pvar] => (state*state) set"
+ "cmd2 pv m == {(s,s'). s' = s[m|->3] & s PP = pv & s m = 2}"
+
+ cmd3 :: "[pvar,pvar] => (state*state) set"
+ "cmd3 u m == {(s,s'). s' = s[u|->0][m|->4] & s m = 3}"
+
+ (*Put pv=1 for u's program and pv=0 for v's program*)
+ cmd4 :: "[nat,pvar] => (state*state) set"
+ "cmd4 pv m == {(s,s'). s' = s[PP|->pv][m|->0] & s m = 4}"
+
+ mutex :: "(state*state) set set"
+ "mutex == {id,
+ cmd0 UU MM, cmd0 VV NN,
+ cmd1u, cmd1v,
+ cmd2 0 MM, cmd2 1 NN,
+ cmd3 UU MM, cmd3 VV NN,
+ cmd4 1 MM, cmd4 0 NN}"
+
+ MInit :: "state set"
+ "MInit == {s. s PP < 2 & s UU = 0 & s VV = 0 & s MM = 0 & s NN = 0}"
+
+ boolVars :: "state set"
+ "boolVars == {s. s PP<2 & s UU < 2 & s VV < 2}"
+
+ (*Put pv=0 for u's program and pv=1 for v's program*)
+ invariant :: "[nat,pvar,pvar] => state set"
+ "invariant pv u m == {s. ((s u=1) = (1 <= s m & s m <= 3)) &
+ (s m = 3 --> s PP = pv)}"
+
+ bad_invariant :: "[nat,pvar,pvar] => state set"
+ "bad_invariant pv u m == {s. ((s u=1) = (1 <= s m & s m <= 3)) &
+ (3 <= s m & s m <= 4 --> s PP = pv)}"
+
+
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Network.ML Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,61 @@
+(* Title: HOL/UNITY/Network
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+The Communication Network
+
+From Misra, "A Logic for Concurrent Programming" (1994), section 5.7
+*)
+
+open Network;
+
+val [rsA, rsB, sent_nondec, rcvd_nondec, rcvd_idle, sent_idle] =
+goalw thy [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} \
+\ {s. s(proc,Rcvd) = m --> s(proc,Idle) = 1}; \
+\ !! n proc. constrains Acts {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 & \
+\ s(Aproc,Sent) = s(Bproc,Rcvd) & \
+\ s(Bproc,Sent) = s(Aproc,Rcvd) & \
+\ s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}";
+
+val sent_nondec_A = read_instantiate [("proc","Aproc")] sent_nondec;
+val sent_nondec_B = read_instantiate [("proc","Bproc")] sent_nondec;
+val rcvd_nondec_A = read_instantiate [("proc","Aproc")] rcvd_nondec;
+val rcvd_nondec_B = read_instantiate [("proc","Bproc")] rcvd_nondec;
+val rcvd_idle_A = read_instantiate [("proc","Aproc")] rcvd_idle;
+val rcvd_idle_B = read_instantiate [("proc","Bproc")] rcvd_idle;
+val sent_idle_A = read_instantiate [("proc","Aproc")] sent_idle;
+val sent_idle_B = read_instantiate [("proc","Bproc")] sent_idle;
+
+val rs_AB = [rsA, rsB] MRS constrains_Int;
+val sent_nondec_AB = [sent_nondec_A, sent_nondec_B] MRS constrains_Int;
+val rcvd_nondec_AB = [rcvd_nondec_A, rcvd_nondec_B] MRS constrains_Int;
+val rcvd_idle_AB = [rcvd_idle_A, rcvd_idle_B] MRS constrains_Int;
+val sent_idle_AB = [sent_idle_A, sent_idle_B] MRS constrains_Int;
+val nondec_AB = [sent_nondec_AB, rcvd_nondec_AB] MRS constrains_Int;
+val idle_AB = [rcvd_idle_AB, sent_idle_AB] MRS constrains_Int;
+val nondec_idle = [nondec_AB, idle_AB] MRS constrains_Int;
+
+by (rtac constrainsI 1);
+by (dtac ([rs_AB, nondec_idle] MRS constrains_Int RS constrainsD) 1);
+by (assume_tac 1);
+by (ALLGOALS Asm_full_simp_tac);
+by (Blast_tac 1);
+by (Clarify_tac 1);
+by (subgoals_tac ["s' (Aproc, Rcvd) = s (Aproc, Rcvd)",
+ "s' (Bproc, Rcvd) = s (Bproc, Rcvd)"] 1);
+by (REPEAT (blast_tac (claset() addIs [le_anti_sym, le_trans, eq_imp_le]) 2));
+
+by (Asm_simp_tac 1);
+result();
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Network.thy Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,9 @@
+Network = UNITY +
+
+datatype pvar = Sent | Rcvd | Idle
+
+datatype pname = Aproc | Bproc
+
+types state = "pname * pvar => nat"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/README.html Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,51 @@
+<!-- $Id$ -->
+<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
+
+<H2>UNITY--Chandy and Misra's UNITY formalism</H2>
+
+<P>The book <EM>Parallel Program Design: A Foundation</EM> by Chandy and Misra
+(Addison-Wesley, 1988) presents UNITY, which consists of an abstract
+programming language of guarded assignments and an associated calculus.
+Misra's 1994 paper "A Logic for Concurrent Programming" presents "New UNITY",
+giving more elegant foundations for a more general class of languages.
+
+<P> This directory is a preliminary formalization of New UNITY. The Isabelle
+examples may not represent the most natural treatment of UNITY style. Hand
+UNITY proofs tend to be written in the forwards direction, as in informal
+mathematics, while Isabelle works best in a backwards (goal-directed) style.
+
+<P>
+The syntax, also, is rather unnatural. Programs are expressed as sets of
+commands, where each command is a relation on states. Quantification over
+commands using [] is easily expressed. At present, there are no examples of
+quantification using ||.
+
+<P>
+The directory presents a few small examples, mostly taken from Misra's 1994
+paper:
+<UL>
+<LI>common meeting time
+
+<LI>the token ring
+
+<LI>the communication network
+
+<LI><EM>n</EM>-process deadlock
+
+<LI>unordered channel
+
+<LI>reachability in directed graphs (section 6.4 of the book)
+</UL>
+
+<P> Safety proofs (invariants) are often proved automatically. Progress
+proofs involving ENSURES can sometimes be proved automatically. The
+level of automation appears to be about the same as in HOL-UNITY by Flemming
+Andersen et al.
+
+<HR>
+<P>Last modified on $Date$
+
+<ADDRESS>
+<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
+</ADDRESS>
+</BODY></HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/ROOT.ML Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,21 @@
+(* Title: HOL/UNITY/ROOT
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Root file for UNITY proofs.
+*)
+
+HOL_build_completed; (*Make examples fail if HOL did*)
+
+writeln"Root file for HOL/UNITY";
+set proof_timing;
+time_use_thy "Deadlock";
+time_use_thy "WFair";
+time_use_thy "Common";
+time_use_thy "Network";
+time_use_thy "Token";
+time_use_thy "Channel";
+time_use_thy "Mutex";
+time_use_thy "FP";
+time_use_thy "Reach";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Reach.ML Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,188 @@
+(* Title: HOL/UNITY/Reach.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Reachability in Directed Graphs. From Chandy and Misra, section 6.4.
+*)
+
+open Reach;
+
+(*TO SIMPDATA.ML?? FOR CLASET?? *)
+val major::prems = goal thy
+ "[| if P then Q else R; \
+\ [| P; Q |] ==> S; \
+\ [| ~ P; R |] ==> S |] ==> S";
+by (cut_facts_tac [major] 1);
+by (blast_tac (claset() addSDs [if_bool_eq_disj RS iffD1] addIs prems) 1);
+qed "ifE";
+
+AddSEs [ifE];
+
+
+val cmd_defs = [racts_def, asgt_def, update_def];
+
+goalw thy [racts_def] "id : racts";
+by (Simp_tac 1);
+qed "id_in_racts";
+AddIffs [id_in_racts];
+
+(*All vertex sets are finite*)
+AddIffs [[subset_UNIV, finite_graph] MRS finite_subset];
+
+
+(** Constrains/Ensures tactics: NEED TO BE GENERALIZED OVER ALL PROGRAMS **)
+
+(*proves "constrains" properties when the program is specified*)
+val constrains_tac =
+ SELECT_GOAL
+ (EVERY [rtac constrainsI 1,
+ rewtac racts_def,
+ REPEAT_FIRST (eresolve_tac [insertE, emptyE]),
+ rewrite_goals_tac [racts_def, asgt_def],
+ ALLGOALS (SELECT_GOAL Auto_tac)]);
+
+
+(*proves "ensures" properties when the program is specified*)
+fun ensures_tac sact =
+ SELECT_GOAL
+ (EVERY [REPEAT (resolve_tac [LeadsTo_Basis, leadsTo_Basis, ensuresI] 1),
+ res_inst_tac [("act", sact)] transient_mem 2,
+ Simp_tac 2,
+ constrains_tac 1,
+ rewrite_goals_tac [racts_def, asgt_def],
+ Auto_tac]);
+
+
+goalw thy [stable_def, invariant_def]
+ "stable racts invariant";
+by (constrains_tac 1);
+by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
+qed "stable_invariant";
+
+goalw thy [rinit_def, invariant_def] "rinit <= invariant";
+by Auto_tac;
+qed "rinit_invariant";
+
+goal thy "reachable rinit racts <= invariant";
+by (simp_tac (simpset() addsimps
+ [strongest_invariant, stable_invariant, rinit_invariant]) 1);
+qed "reachable_subset_invariant";
+
+val reachable_subset_invariant' =
+ rewrite_rule [invariant_def] reachable_subset_invariant;
+
+
+(*** Fixedpoint ***)
+
+(*If it reaches a fixedpoint, it has found a solution*)
+goalw thy [fixedpoint_def, invariant_def]
+ "fixedpoint Int invariant = { %v. (init, v) : edges^* }";
+by (rtac equalityI 1);
+by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 2);
+by (auto_tac (claset() addSIs [ext], simpset()));
+by (etac rtrancl_induct 1);
+by Auto_tac;
+qed "fixedpoint_invariant_correct";
+
+goalw thy (cmd_defs @ [FP_def, fixedpoint_def, stable_def, constrains_def])
+ "FP racts <= fixedpoint";
+by Auto_tac;
+by (dtac bspec 1);
+by (Blast_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [Image_singleton, image_iff]) 1);
+by (dtac fun_cong 1);
+by Auto_tac;
+val lemma1 = result();
+
+goalw thy (cmd_defs @ [FP_def, fixedpoint_def, stable_def, constrains_def])
+ "fixedpoint <= FP racts";
+by (auto_tac (claset() addIs [ext], simpset()));
+val lemma2 = result();
+
+goal thy "FP racts = fixedpoint";
+by (rtac ([lemma1,lemma2] MRS equalityI) 1);
+qed "FP_fixedpoint";
+
+
+(*If we haven't reached a fixedpoint then there is some edge for which u but
+ not v holds. Progress will be proved via an ENSURES assertion that the
+ metric will decrease for each suitable edge. A union over all edges proves
+ a LEADSTO assertion that the metric decreases if we are not at a fixedpoint.
+ *)
+
+goal thy "Compl fixedpoint = (UN (u,v): edges. {s. s u & ~ s v})";
+by (simp_tac (simpset() addsimps
+ ([Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym,
+ racts_def, asgt_def])) 1);
+by Safe_tac;
+by (rtac update_idem 1);
+by (Blast_tac 1);
+by (Full_simp_tac 1);
+by (REPEAT (dtac bspec 1 THEN Simp_tac 1));
+by (dtac subsetD 1);
+by (Simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [update_idem_iff]) 1);
+qed "Compl_fixedpoint";
+
+goal thy "A - fixedpoint = (UN (u,v): edges. A Int {s. s u & ~ s v})";
+by (simp_tac (simpset() addsimps [Diff_eq, Compl_fixedpoint]) 1);
+by (Blast_tac 1);
+qed "Diff_fixedpoint";
+
+
+(*** Progress ***)
+
+goalw thy [metric_def] "!!s. ~ s x ==> Suc (metric (s[x|->True])) = metric s";
+by (subgoal_tac "{v. ~ (s[x|->True]) v} = {v. ~ s v} - {x}" 1);
+by Auto_tac;
+by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1);
+qed "Suc_metric";
+
+goal thy "!!s. ~ s x ==> metric (s[x|->True]) < metric s";
+by (etac (Suc_metric RS subst) 1);
+by (Blast_tac 1);
+qed "metric_less";
+AddSIs [metric_less];
+
+goal thy "metric (s[y|->s x | s y]) <= metric s";
+by (case_tac "s x --> s y" 1);
+by (auto_tac (claset() addIs [less_imp_le],
+ simpset() addsimps [update_idem]));
+qed "metric_le";
+
+goal thy "!!m. (u,v): edges ==> \
+\ ensures racts ((metric-``{m}) Int {s. s u & ~ s v}) \
+\ (metric-``(lessThan m))";
+by (ensures_tac "asgt u v" 1);
+by (cut_facts_tac [metric_le] 1);
+by (fast_tac (claset() addSDs [le_imp_less_or_eq]) 1);
+qed "edges_ensures";
+
+goal thy "leadsTo racts ((metric-``{m}) - fixedpoint) (metric-``(lessThan m))";
+by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1);
+by (rtac leadsTo_UN 1);
+by (split_all_tac 1);
+by (asm_simp_tac (simpset() addsimps [edges_ensures RS leadsTo_Basis]) 1);
+qed "leadsTo_Diff_fixedpoint";
+
+goal thy "leadsTo racts (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)";
+by (rtac (leadsTo_Diff_fixedpoint RS leadsTo_weaken_R RS leadsTo_Diff) 1);
+by (ALLGOALS (blast_tac (claset() addIs [subset_imp_leadsTo])));
+qed "leadsTo_Un_fixedpoint";
+
+
+(*Execution in any state leads to a fixedpoint (i.e. can terminate)*)
+goal thy "leadsTo racts UNIV fixedpoint";
+by (rtac lessThan_induct 1);
+by Auto_tac;
+by (rtac leadsTo_Un_fixedpoint 1);
+qed "leadsTo_fixedpoint";
+
+goal thy "LeadsTo rinit racts UNIV { %v. (init, v) : edges^* }";
+by (stac (fixedpoint_invariant_correct RS sym) 1);
+by (rtac (leadsTo_fixedpoint RS leadsTo_imp_LeadsTo RS LeadsTo_weaken_R) 1);
+by (cut_facts_tac [reachable_subset_invariant] 1);
+by (Blast_tac 1);
+qed "LeadsTo_correct";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Reach.thy Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,46 @@
+(* Title: HOL/UNITY/Reach.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Reachability in Directed Graphs. From Chandy and Misra, section 6.4.
+*)
+
+Reach = Update + FP + Traces + SubstAx +
+
+types vertex
+ state = "vertex=>bool"
+
+arities vertex :: term
+
+consts
+ init :: "vertex"
+
+ edges :: "(vertex*vertex) set"
+
+constdefs
+
+ asgt :: "[vertex,vertex] => (state*state) set"
+ "asgt u v == {(s,s'). s' = s[v|-> s u | s v]}"
+
+ racts :: "(state*state) set set"
+ "racts == insert id (UN (u,v): edges. {asgt u v})"
+
+ rinit :: "state set"
+ "rinit == {%v. v=init}"
+
+ invariant :: state set
+ "invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}"
+
+ fixedpoint :: state set
+ "fixedpoint == {s. ALL (u,v): edges. s u --> s v}"
+
+ metric :: state => nat
+ "metric == (%s. card {v. ~ s v})"
+
+rules
+
+ (*We assume that the set of vertices is finite*)
+ finite_graph "finite (UNIV :: vertex set)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/SubstAx.ML Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,405 @@
+(* Title: HOL/UNITY/SubstAx
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Weak Fairness versions of transient, ensures, LeadsTo.
+
+From Misra, "A Logic for Concurrent Programming", 1994
+*)
+
+open SubstAx;
+
+(*constrains Acts B B' ==> constrains Acts (reachable Init Acts Int B)
+ (reachable Init Acts Int B') *)
+bind_thm ("constrains_reachable",
+ rewrite_rule [stable_def] stable_reachable RS constrains_Int);
+
+
+(*** Introduction rules: Basis, Trans, Union ***)
+
+goalw thy [LeadsTo_def]
+ "!!Acts. leadsTo Acts A B ==> LeadsTo Init Acts A B";
+by (blast_tac (claset() addIs [PSP_stable2, stable_reachable]) 1);
+qed "leadsTo_imp_LeadsTo";
+
+goalw thy [LeadsTo_def]
+ "!!Acts. [| constrains Acts (reachable Init Acts Int (A - A')) \
+\ (A Un A'); \
+\ transient Acts (reachable Init Acts Int (A-A')) |] \
+\ ==> LeadsTo Init Acts A A'";
+by (rtac (stable_reachable RS stable_ensures_Int RS leadsTo_Basis) 1);
+by (assume_tac 2);
+by (asm_simp_tac
+ (simpset() addsimps [Int_Un_distrib RS sym, Diff_Int_distrib RS sym,
+ stable_constrains_Int]) 1);
+qed "LeadsTo_Basis";
+
+goalw thy [LeadsTo_def]
+ "!!Acts. [| LeadsTo Init Acts A B; LeadsTo Init Acts B C |] \
+\ ==> LeadsTo Init Acts A C";
+by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
+qed "LeadsTo_Trans";
+
+val prems = goalw thy [LeadsTo_def]
+ "(!!A. A : S ==> LeadsTo Init Acts A B) ==> LeadsTo Init Acts (Union S) B";
+by (stac Int_Union 1);
+by (blast_tac (claset() addIs (leadsTo_UN::prems)) 1);
+qed "LeadsTo_Union";
+
+
+(*** Derived rules ***)
+
+goal thy "!!Acts. id: Acts ==> LeadsTo Init Acts 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 thy "!!Acts. LeadsTo Init Acts A (A' Un A') ==> LeadsTo Init Acts A A'";
+by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
+qed "LeadsTo_Un_duplicate";
+
+goal thy "!!Acts. LeadsTo Init Acts A (A' Un C Un C) ==> LeadsTo Init Acts A (A' Un C)";
+by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
+qed "LeadsTo_Un_duplicate2";
+
+val prems = goal thy
+ "(!!i. i : I ==> LeadsTo Init Acts (A i) B) \
+\ ==> LeadsTo Init Acts (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 thy
+ "!!C. [| LeadsTo Init Acts A C; LeadsTo Init Acts B C |] ==> LeadsTo Init Acts (A Un B) C";
+by (stac Un_eq_Union 1);
+by (blast_tac (claset() addIs [LeadsTo_Union]) 1);
+qed "LeadsTo_Un";
+
+
+goalw thy [LeadsTo_def]
+ "!!A B. [| reachable Init Acts Int A <= B; id: Acts |] \
+\ ==> LeadsTo Init Acts A B";
+by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
+qed "Int_subset_imp_LeadsTo";
+
+goalw thy [LeadsTo_def]
+ "!!A B. [| A <= B; id: Acts |] \
+\ ==> LeadsTo Init Acts A B";
+by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
+qed "subset_imp_LeadsTo";
+
+bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo);
+Addsimps [empty_LeadsTo];
+
+goal thy
+ "!!A B. [| reachable Init Acts Int A = {}; id: Acts |] \
+\ ==> LeadsTo Init Acts A B";
+by (asm_simp_tac (simpset() addsimps [Int_subset_imp_LeadsTo]) 1);
+qed "Int_empty_LeadsTo";
+
+
+goalw thy [LeadsTo_def]
+ "!!Acts. [| LeadsTo Init Acts A A'; \
+\ reachable Init Acts Int A' <= B' |] \
+\ ==> LeadsTo Init Acts A B'";
+by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1);
+qed_spec_mp "LeadsTo_weaken_R";
+
+
+goalw thy [LeadsTo_def]
+ "!!Acts. [| LeadsTo Init Acts A A'; \
+ \ reachable Init Acts Int B <= A; id: Acts |] \
+\ ==> LeadsTo Init Acts B A'";
+by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
+qed_spec_mp "LeadsTo_weaken_L";
+
+
+(*Distributes over binary unions*)
+goal thy
+ "!!C. id: Acts ==> \
+\ LeadsTo Init Acts (A Un B) C = \
+\ (LeadsTo Init Acts A C & LeadsTo Init Acts B C)";
+by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
+qed "LeadsTo_Un_distrib";
+
+goal thy
+ "!!C. id: Acts ==> \
+\ LeadsTo Init Acts (UN i:I. A i) B = \
+\ (ALL i : I. LeadsTo Init Acts (A i) B)";
+by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
+qed "LeadsTo_UN_distrib";
+
+goal thy
+ "!!C. id: Acts ==> \
+\ LeadsTo Init Acts (Union S) B = \
+\ (ALL A : S. LeadsTo Init Acts A B)";
+by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1);
+qed "LeadsTo_Union_distrib";
+
+
+goal thy
+ "!!Acts. [| LeadsTo Init Acts A A'; id: Acts; \
+\ reachable Init Acts Int B <= A; \
+\ reachable Init Acts Int A' <= B' |] \
+\ ==> LeadsTo Init Acts B B'";
+(*PROOF FAILED: why?*)
+by (blast_tac (claset() addIs [LeadsTo_Trans, LeadsTo_weaken_R,
+ LeadsTo_weaken_L]) 1);
+qed "LeadsTo_weaken";
+
+
+(*Set difference: maybe combine with leadsTo_weaken_L??*)
+goal thy
+ "!!C. [| LeadsTo Init Acts (A-B) C; LeadsTo Init Acts B C; id: Acts |] \
+\ ==> LeadsTo Init Acts A C";
+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 ==> LeadsTo Init Acts (A i) (A' i)) \
+\ ==> LeadsTo Init Acts (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);
+qed "LeadsTo_UN_UN";
+
+
+(*Version with no index set*)
+val prems = goal thy
+ "(!! i. LeadsTo Init Acts (A i) (A' i)) \
+\ ==> LeadsTo Init Acts (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 thy
+ "!!Acts. ALL i. LeadsTo Init Acts (A i) (A' i) \
+\ ==> LeadsTo Init Acts (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 thy "!!Acts. [| LeadsTo Init Acts A A'; LeadsTo Init Acts B B' |] \
+\ ==> LeadsTo Init Acts (A Un B) (A' Un B')";
+by (blast_tac (claset() addIs [LeadsTo_Un,
+ LeadsTo_weaken_R]) 1);
+qed "LeadsTo_Un_Un";
+
+
+(** The cancellation law **)
+
+goal thy
+ "!!Acts. [| LeadsTo Init Acts A (A' Un B); LeadsTo Init Acts B B'; \
+\ id: Acts |] \
+\ ==> LeadsTo Init Acts A (A' Un B')";
+by (blast_tac (claset() addIs [LeadsTo_Un_Un,
+ subset_imp_LeadsTo, LeadsTo_Trans]) 1);
+qed "LeadsTo_cancel2";
+
+goal thy
+ "!!Acts. [| LeadsTo Init Acts A (A' Un B); LeadsTo Init Acts (B-A') B'; id: Acts |] \
+\ ==> LeadsTo Init Acts A (A' Un B')";
+by (rtac LeadsTo_cancel2 1);
+by (assume_tac 2);
+by (ALLGOALS Asm_simp_tac);
+qed "LeadsTo_cancel_Diff2";
+
+goal thy
+ "!!Acts. [| LeadsTo Init Acts A (B Un A'); LeadsTo Init Acts B B'; id: Acts |] \
+\ ==> LeadsTo Init Acts 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 thy
+ "!!Acts. [| LeadsTo Init Acts A (B Un A'); LeadsTo Init Acts (B-A') B'; id: Acts |] \
+\ ==> LeadsTo Init Acts 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 **)
+
+goalw thy [LeadsTo_def]
+ "!!Acts. LeadsTo Init Acts A {} ==> reachable Init Acts Int A = {}";
+by (Full_simp_tac 1);
+by (etac leadsTo_empty 1);
+qed "LeadsTo_empty";
+
+
+(** PSP: Progress-Safety-Progress **)
+
+(*Special case of PSP: Misra's "stable conjunction". Doesn't need id:Acts. *)
+goalw thy [LeadsTo_def]
+ "!!Acts. [| LeadsTo Init Acts A A'; stable Acts B |] \
+\ ==> LeadsTo Init Acts (A Int B) (A' Int B)";
+by (asm_simp_tac (simpset() addsimps [Int_assoc RS sym, PSP_stable]) 1);
+qed "R_PSP_stable";
+
+goal thy
+ "!!Acts. [| LeadsTo Init Acts A A'; stable Acts B |] \
+\ ==> LeadsTo Init Acts (B Int A) (B Int A')";
+by (asm_simp_tac (simpset() addsimps (R_PSP_stable::Int_ac)) 1);
+qed "R_PSP_stable2";
+
+
+goalw thy [LeadsTo_def]
+ "!!Acts. [| LeadsTo Init Acts A A'; constrains Acts B B'; id: Acts |] \
+\ ==> LeadsTo Init Acts (A Int B) ((A' Int B) Un (B' - B))";
+by (dtac PSP 1);
+by (etac constrains_reachable 1);
+by (etac leadsTo_weaken 2);
+by (ALLGOALS Blast_tac);
+qed "R_PSP";
+
+goal thy
+ "!!Acts. [| LeadsTo Init Acts A A'; constrains Acts B B'; id: Acts |] \
+\ ==> LeadsTo Init Acts (B Int A) ((B Int A') Un (B' - B))";
+by (asm_simp_tac (simpset() addsimps (R_PSP::Int_ac)) 1);
+qed "R_PSP2";
+
+goalw thy [unless_def]
+ "!!Acts. [| LeadsTo Init Acts A A'; unless Acts B B'; id: Acts |] \
+\ ==> LeadsTo Init Acts (A Int B) ((A' Int B) Un B')";
+by (dtac R_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;
+qed "R_PSP_unless";
+
+
+(*** Induction rules ***)
+
+(** Meta or object quantifier ????? **)
+goalw thy [LeadsTo_def]
+ "!!Acts. [| wf r; \
+\ ALL m. LeadsTo Init Acts (A Int f-``{m}) \
+\ ((A Int f-``(r^-1 ^^ {m})) Un B); \
+\ id: Acts |] \
+\ ==> LeadsTo Init Acts A B";
+by (etac leadsTo_wf_induct 1);
+by (assume_tac 2);
+by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
+qed "LeadsTo_wf_induct";
+
+
+goal thy
+ "!!Acts. [| wf r; \
+\ ALL m:I. LeadsTo Init Acts (A Int f-``{m}) \
+\ ((A Int f-``(r^-1 ^^ {m})) Un B); \
+\ id: Acts |] \
+\ ==> LeadsTo Init Acts A ((A - (f-``I)) Un B)";
+by (etac LeadsTo_wf_induct 1);
+by Safe_tac;
+by (case_tac "m:I" 1);
+by (blast_tac (claset() addIs [LeadsTo_weaken]) 1);
+by (blast_tac (claset() addIs [subset_imp_LeadsTo]) 1);
+qed "R_bounded_induct";
+
+
+goal thy
+ "!!Acts. [| ALL m. LeadsTo Init Acts (A Int f-``{m}) \
+\ ((A Int f-``(lessThan m)) Un B); \
+\ id: Acts |] \
+\ ==> LeadsTo Init Acts A B";
+by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
+by (assume_tac 2);
+by (Asm_simp_tac 1);
+qed "R_lessThan_induct";
+
+goal thy
+ "!!Acts. [| ALL m:(greaterThan l). LeadsTo Init Acts (A Int f-``{m}) \
+\ ((A Int f-``(lessThan m)) Un B); \
+\ id: Acts |] \
+\ ==> LeadsTo Init 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);
+by (rtac (wf_less_than RS R_bounded_induct) 1);
+by (assume_tac 2);
+by (Asm_simp_tac 1);
+qed "R_lessThan_bounded_induct";
+
+goal thy
+ "!!Acts. [| ALL m:(lessThan l). LeadsTo Init Acts (A Int f-``{m}) \
+\ ((A Int f-``(greaterThan m)) Un B); \
+\ id: Acts |] \
+\ ==> LeadsTo Init Acts 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);
+by (blast_tac (claset() addIs [not_leE, subset_imp_LeadsTo]) 2);
+by (blast_tac (claset() addIs [LeadsTo_weaken_R, diff_less_mono2]) 1);
+qed "R_greaterThan_bounded_induct";
+
+
+
+(*** Completion: Binary and General Finite versions ***)
+
+goalw thy [LeadsTo_def]
+ "!!Acts. [| LeadsTo Init Acts A A'; stable Acts A'; \
+\ LeadsTo Init Acts B B'; stable Acts B'; id: Acts |] \
+\ ==> LeadsTo Init Acts (A Int B) (A' Int B')";
+by (blast_tac (claset() addIs [stable_completion RS leadsTo_weaken]
+ addSIs [stable_Int, stable_reachable]) 1);
+qed "R_stable_completion";
+
+
+goal thy
+ "!!Acts. [| finite I; id: Acts |] \
+\ ==> (ALL i:I. LeadsTo Init Acts (A i) (A' i)) --> \
+\ (ALL i:I. stable Acts (A' i)) --> \
+\ LeadsTo Init Acts (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 [R_stable_completion, stable_def,
+ ball_constrains_INT]) 1);
+qed_spec_mp "R_finite_stable_completion";
+
+
+goalw thy [LeadsTo_def]
+ "!!Acts. [| LeadsTo Init Acts A (A' Un C); constrains Acts A' (A' Un C); \
+\ LeadsTo Init Acts B (B' Un C); constrains Acts B' (B' Un C); \
+\ id: Acts |] \
+\ ==> LeadsTo Init Acts (A Int B) ((A' Int B') Un C)";
+
+by (full_simp_tac (simpset() addsimps [Int_Un_distrib]) 1);
+by (dtac completion 1);
+by (assume_tac 2);
+by (ALLGOALS
+ (asm_simp_tac
+ (simpset() addsimps [constrains_reachable, Int_Un_distrib RS sym])));
+by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
+qed "R_completion";
+
+
+goal thy
+ "!!Acts. [| finite I; id: Acts |] \
+\ ==> (ALL i:I. LeadsTo Init Acts (A i) (A' i Un C)) --> \
+\ (ALL i:I. constrains Acts (A' i) (A' i Un C)) --> \
+\ LeadsTo Init Acts (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);
+by (dtac ball_constrains_INT 1);
+by (asm_full_simp_tac (simpset() addsimps [R_completion]) 1);
+qed "R_finite_completion";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/SubstAx.thy Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,19 @@
+(* Title: HOL/UNITY/SubstAx
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+My treatment of the Substitution Axiom -- not as an axiom!
+*)
+
+SubstAx = WFair +
+
+constdefs
+
+ LeadsTo :: "['a set, ('a * 'a)set set, 'a set, 'a set] => bool"
+ "LeadsTo Init Acts A B ==
+ leadsTo Acts (reachable Init Acts Int A)
+ (reachable Init Acts Int B)"
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Token.ML Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,150 @@
+(* Title: HOL/UNITY/Token
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+The Token Ring.
+
+From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
+*)
+
+
+open Token;
+
+
+val Token_defs = [WellTyped_def, Token_def, HasTok_def, H_def, E_def, T_def];
+
+AddIffs [N_positive, skip];
+
+goalw thy [HasTok_def] "!!i. [| s: HasTok i; s: HasTok j |] ==> i=j";
+by Auto_tac;
+qed "HasToK_partition";
+
+goalw thy Token_defs "!!s. s : WellTyped ==> (s ~: E i) = (s : H i | s : T i)";
+by (Simp_tac 1);
+by (exhaust_tac "s (Suc i)" 1);
+by Auto_tac;
+qed "not_E_eq";
+
+(** We should be able to prove WellTyped as a separate Invariant. Then
+ the Invariant rule should let us assume that the initial
+ state is reachable, and therefore contained in any Invariant. Then
+ we'd not have to mention WellTyped in the statement of this theorem.
+**)
+
+goalw thy [stable_def]
+ "stable Acts (WellTyped Int {s. s : E i --> s : HasTok i})";
+by (rtac (stable_WT RS stable_constrains_Int) 1);
+by (cut_facts_tac [TR2,TR4,TR5] 1);
+by (asm_full_simp_tac (simpset() addsimps [constrains_def]) 1);
+by (REPEAT_FIRST (rtac ballI ORELSE' (dtac bspec THEN' assume_tac)));
+by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
+by (case_tac "xa : HasTok i" 1);
+by (auto_tac (claset(), simpset() addsimps [H_def, E_def, T_def]));
+qed "token_stable";
+
+(*This proof is in the "massaging" style and is much faster! *)
+goalw thy [stable_def]
+ "stable Acts (WellTyped Int (Compl(E i) Un (HasTok i)))";
+by (rtac (stable_WT RS stable_constrains_Int) 1);
+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]));
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [H_def, E_def, T_def])));
+qed "token_stable";
+
+
+(*** Progress under weak fairness ***)
+
+goalw thy [nodeOrder_def] "wf(nodeOrder j)";
+by (rtac (wf_less_than RS wf_inv_image RS wf_subset) 1);
+by (Blast_tac 1);
+qed"wf_nodeOrder";
+
+ goal thy "!!m. [| m<n; Suc m ~= n |] ==> Suc(m) < n";
+ by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1);
+ by (blast_tac (claset() addEs [less_asym, less_SucE]) 1);
+ qed "Suc_lessI";
+
+goalw thy [nodeOrder_def, next_def, inv_image_def]
+ "!!x. [| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)";
+by (auto_tac (claset(),
+ simpset() addsimps [Suc_lessI, mod_Suc, mod_less, mod_geq]));
+by (dtac sym 1);
+(*The next two lines...**)
+by (REPEAT (eres_inst_tac [("P", "?a<N")] rev_mp 1));
+by (etac ssubst 1);
+(*were with the previous version of asm_full_simp_tac...
+ by (rotate_tac ~1 1);
+*)
+by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv, mod_Suc, mod_less]) 1);
+by (subgoal_tac "(j + N - i) = Suc (j + N - Suc i)" 1);
+by (asm_simp_tac (simpset() addsimps [Suc_diff_Suc, less_imp_le, Suc_leI,
+ diff_add_assoc]) 2);
+by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1);
+by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc]) 1);
+(*including less_asym here would slow things down*)
+by (auto_tac (claset() delrules [notI],
+ simpset() addsimps [diff_add_assoc2, Suc_leI,
+ less_imp_diff_less,
+ mod_less, mod_geq, nat_neq_iff]));
+by (REPEAT (blast_tac (claset() addEs [less_asym]) 3));
+by (asm_simp_tac (simpset() addsimps [less_imp_diff_less,
+ Suc_diff_n RS sym]) 1);
+by (asm_simp_tac (simpset() addsimps [add_diff_less, mod_less]) 1);
+by (etac subst 1);
+by (asm_simp_tac (simpset() addsimps [add_diff_less]) 1);
+qed "nodeOrder_eq";
+
+
+(*From "A Logic for Concurrent Programming", but not used in Chapter 4.
+ Note the use of case_tac. Reasoning about leadsTo takes practice!*)
+goal thy
+ "!!i. [| i<N; j<N |] ==> \
+\ leadsTo Acts (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);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
+qed "TR7_nodeOrder";
+
+
+(*Chapter 4 variant, the one actually used below.*)
+goal thy
+ "!!i. [| i<N; j<N; i~=j |] ==> \
+\ leadsTo Acts (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);
+qed "TR7_aux";
+
+goal thy "({s. Token s < N} Int Token -`` {m}) = \
+\ (if m<N then Token -`` {m} else {})";
+by Auto_tac;
+val Token_lemma = result();
+
+
+(*Misra's TR9: the token reaches an arbitrary node*)
+goal thy
+ "!!i. j<N ==> leadsTo Acts {s. Token s < N} (HasTok j)";
+by (rtac leadsTo_weaken_R 1);
+by (res_inst_tac [("I", "Compl{j}"), ("f", "Token"), ("B", "{}")]
+ (wf_nodeOrder RS bounded_induct) 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [Token_lemma, vimage_Diff,
+ HasTok_def])));
+by (Blast_tac 2);
+by (Clarify_tac 1);
+by (rtac (TR7_aux RS leadsTo_weaken) 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [nodeOrder_def, HasTok_def])));
+by (ALLGOALS Blast_tac);
+qed "leadsTo_j";
+
+(*Misra's TR8: a hungry process eventually eats*)
+goal thy "!!i. j<N ==> leadsTo Acts ({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);
+by (rtac ([leadsTo_j, TR3] MRS PSP) 1);
+by (ALLGOALS Blast_tac);
+qed "Token_progress";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Token.thy Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,71 @@
+(* Title: HOL/UNITY/Token
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+The Token Ring.
+
+From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
+*)
+
+
+Token = WFair +
+
+(*process states*)
+datatype pstate = Hungry | Eating | Thinking | Pnum nat
+
+types state = nat => pstate
+
+consts
+ N :: nat (*number of nodes in the ring*)
+
+constdefs
+ nodeOrder :: "nat => (nat*nat)set"
+ "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N)) Int
+ (lessThan N Times lessThan N)"
+
+ next :: nat => nat
+ "next i == (Suc i) mod N"
+
+ WellTyped :: state set
+ "WellTyped == {s. ALL i j. s (Suc i) ~= Pnum j}"
+
+ Token :: state => nat
+ "Token s == case s 0 of
+ Hungry => 0
+ | Eating => 0
+ | Thinking => 0
+ | Pnum i => i"
+
+ HasTok :: nat => state set
+ "HasTok i == Token -`` {i}"
+
+ H :: nat => state set
+ "H i == {s. s (Suc i) = Hungry}"
+
+ E :: nat => state set
+ "E i == {s. s (Suc i) = Eating}"
+
+ T :: nat => state set
+ "T i == {s. s (Suc i) = Thinking}"
+
+rules
+ N_positive "0<N"
+
+ stable_WT "stable Acts WellTyped"
+
+ skip "id: Acts"
+
+ TR2 "constrains Acts (T i) (T i Un H i)"
+
+ TR3 "constrains Acts (H i) (H i Un E i)"
+
+ TR4 "constrains Acts (H i - HasTok i) (H i)"
+
+ TR5 "constrains Acts (HasTok i) (HasTok i Un Compl(E i))"
+
+ TR6 "leadsTo Acts (H i Int HasTok i) (E i)"
+
+ TR7 "leadsTo Acts (HasTok i) (HasTok (next i))"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Traces.ML Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,39 @@
+open Traces;
+
+goal thy "reachable Init Acts <= {s. EX evs. s#evs: traces Init Acts}";
+by (rtac subsetI 1);
+be reachable.induct 1;
+by (REPEAT (blast_tac (claset() addIs traces.intrs) 1));
+val lemma1 = result();
+
+goal thy "!!evs. evs : traces Init Acts \
+\ ==> ALL s evs'. evs = s#evs' --> s: reachable Init Acts";
+be traces.induct 1;
+by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
+val lemma2 = normalize_thm [RSmp, RSspec] (result());
+
+goal thy "{s. EX evs. s#evs: traces Init Acts} <= reachable Init Acts";
+by (blast_tac (claset() addIs [lemma2]) 1);
+val lemma3 = result();
+
+goal thy "reachable Init Acts = {s. EX evs. s#evs: traces Init Acts}";
+by (rtac ([lemma1,lemma3] MRS equalityI) 1);
+qed "reachable_eq_traces";
+
+
+(*Could/should this be proved?*)
+goal thy "reachable Init Acts = (UN evs: traces Init Acts. set evs)";
+
+
+(*The strongest invariant is the set of all reachable states!*)
+goalw thy [stable_def, constrains_def]
+ "!!A. [| Init<=A; stable Acts A |] ==> reachable Init Acts <= A";
+by (rtac subsetI 1);
+be reachable.induct 1;
+by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
+qed "strongest_invariant";
+
+goal thy "stable Acts (reachable Init Acts)";
+by (REPEAT (blast_tac (claset() addIs [stableI, constrainsI]
+ addIs reachable.intrs) 1));
+qed "stable_reachable";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Traces.thy Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,24 @@
+Traces = UNITY +
+
+consts traces :: "['a set, ('a * 'a)set set] => 'a list set"
+
+inductive "traces Init Acts"
+ intrs
+ (*Initial trace is empty*)
+ Init "s: Init ==> [s] : traces Init Acts"
+
+ Acts "[| act: Acts; s#evs : traces Init Acts; (s,s'): act |]
+ ==> s'#s#evs : traces Init Acts"
+
+
+consts reachable :: "['a set, ('a * 'a)set set] => 'a set"
+
+inductive "reachable Init Acts"
+ intrs
+ (*Initial trace is empty*)
+ Init "s: Init ==> s : reachable Init Acts"
+
+ Acts "[| act: Acts; s : reachable Init Acts; (s,s'): act |]
+ ==> s' : reachable Init Acts"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/UNITY.ML Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,229 @@
+(* Title: HOL/UNITY/UNITY
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+The basic UNITY theory (revised version, based upon the "co" operator)
+
+From Misra, "A Logic for Concurrent Programming", 1994
+*)
+
+set proof_timing;
+HOL_quantifiers := false;
+
+
+(*CAN BOOLEAN SIMPLIFICATION BE AUTOMATED?*)
+
+(** Rewrites rules to eliminate A. Conditions can be satisfied by letting B
+ be any set including A Int C and contained in A Un C, such as B=A or B=C.
+**)
+
+goal thy "!!x. [| A Int C <= B; B <= A Un C |] \
+\ ==> (A Int B) Un (Compl A Int C) = B Un C";
+by (Blast_tac 1);
+
+goal thy "!!x. [| A Int C <= B; B <= A Un C |] \
+\ ==> (A Un B) Int (Compl A Un C) = B Int C";
+by (Blast_tac 1);
+
+(*The base B=A*)
+goal thy "A Un (Compl A Int C) = A Un C";
+by (Blast_tac 1);
+
+goal thy "A Int (Compl A Un C) = A Int C";
+by (Blast_tac 1);
+
+(*The base B=C*)
+goal thy "(A Int C) Un (Compl A Int C) = C";
+by (Blast_tac 1);
+
+goal thy "(A Un C) Int (Compl A Un C) = C";
+by (Blast_tac 1);
+
+
+(** More ad-hoc rules **)
+
+goal thy "A Un B - (A - B) = B";
+by (Blast_tac 1);
+qed "Un_Diff_Diff";
+
+goal thy "A Int (B - C) Un C = A Int B Un C";
+by (Blast_tac 1);
+qed "Int_Diff_Un";
+
+
+open UNITY;
+
+
+(*** constrains ***)
+
+val prems = goalw thy [constrains_def]
+ "(!!act s s'. [| act: Acts; (s,s') : act; s: A |] ==> s': A') \
+\ ==> constrains Acts A A'";
+by (blast_tac (claset() addIs prems) 1);
+qed "constrainsI";
+
+goalw thy [constrains_def]
+ "!!Acts. [| constrains Acts A A'; act: Acts; (s,s'): act; s: A |] \
+\ ==> s': A'";
+by (Blast_tac 1);
+qed "constrainsD";
+
+goalw thy [constrains_def] "constrains Acts {} B";
+by (Blast_tac 1);
+qed "constrains_empty";
+
+goalw thy [constrains_def] "constrains Acts A UNIV";
+by (Blast_tac 1);
+qed "constrains_UNIV";
+AddIffs [constrains_empty, constrains_UNIV];
+
+goalw thy [constrains_def]
+ "!!Acts. [| constrains Acts A A'; A'<=B' |] ==> constrains Acts A B'";
+by (Blast_tac 1);
+qed "constrains_weaken_R";
+
+goalw thy [constrains_def]
+ "!!Acts. [| constrains Acts A A'; B<=A |] ==> constrains Acts B A'";
+by (Blast_tac 1);
+qed "constrains_weaken_L";
+
+goalw thy [constrains_def]
+ "!!Acts. [| constrains Acts A A'; B<=A; A'<=B' |] ==> constrains Acts B B'";
+by (Blast_tac 1);
+qed "constrains_weaken";
+
+(*Set difference: UNUSED*)
+goalw thy [constrains_def]
+ "!!C. [| constrains Acts (A-B) C; constrains Acts B C |] \
+\ ==> constrains Acts A C";
+by (Blast_tac 1);
+qed "constrains_Diff";
+
+(** Union **)
+
+goalw thy [constrains_def]
+ "!!Acts. [| constrains Acts A A'; constrains Acts B B' |] \
+\ ==> constrains Acts (A Un B) (A' Un B')";
+by (Blast_tac 1);
+qed "constrains_Un";
+
+goalw thy [constrains_def]
+ "!!Acts. ALL i:I. constrains Acts (A i) (A' i) \
+\ ==> constrains Acts (UN i:I. A i) (UN i:I. A' i)";
+by (Blast_tac 1);
+qed "ball_constrains_UN";
+
+goalw thy [constrains_def]
+ "!!Acts. [| ALL i. constrains Acts (A i) (A' i) |] \
+\ ==> constrains Acts (UN i. A i) (UN i. A' i)";
+by (Blast_tac 1);
+qed "all_constrains_UN";
+
+(** Intersection **)
+
+goalw thy [constrains_def]
+ "!!Acts. [| constrains Acts A A'; constrains Acts B B' |] \
+\ ==> constrains Acts (A Int B) (A' Int B')";
+by (Blast_tac 1);
+qed "constrains_Int";
+
+goalw thy [constrains_def]
+ "!!Acts. ALL i:I. constrains Acts (A i) (A' i) \
+\ ==> constrains Acts (INT i:I. A i) (INT i:I. A' i)";
+by (Blast_tac 1);
+qed "ball_constrains_INT";
+
+goalw thy [constrains_def]
+ "!!Acts. [| ALL i. constrains Acts (A i) (A' i) |] \
+\ ==> constrains Acts (INT i. A i) (INT i. A' i)";
+by (Blast_tac 1);
+qed "all_constrains_INT";
+
+goalw thy [stable_def, constrains_def]
+ "!!Acts. [| stable Acts C; constrains Acts A (C Un A') |] \
+\ ==> constrains Acts (C Un A) (C Un A')";
+by (Blast_tac 1);
+qed "stable_constrains_Un";
+
+goalw thy [stable_def, constrains_def]
+ "!!Acts. [| stable Acts C; constrains Acts (C Int A) A' |] \
+\ ==> constrains Acts (C Int A) (C Int A')";
+by (Blast_tac 1);
+qed "stable_constrains_Int";
+
+
+(*** stable ***)
+
+goalw thy [stable_def]
+ "!!Acts. constrains Acts A A ==> stable Acts A";
+by (assume_tac 1);
+qed "stableI";
+
+goalw thy [stable_def]
+ "!!Acts. stable Acts A ==> constrains Acts A A";
+by (assume_tac 1);
+qed "stableD";
+
+goalw thy [stable_def]
+ "!!Acts. [| stable Acts A; stable Acts A' |] \
+\ ==> stable Acts (A Un A')";
+by (blast_tac (claset() addIs [constrains_Un]) 1);
+qed "stable_Un";
+
+goalw thy [stable_def]
+ "!!Acts. [| stable Acts A; stable Acts A' |] \
+\ ==> stable Acts (A Int A')";
+by (blast_tac (claset() addIs [constrains_Int]) 1);
+qed "stable_Int";
+
+goalw thy [constrains_def]
+ "!!Acts. [| constrains Acts A A'; id: Acts |] ==> A<=A'";
+by (Blast_tac 1);
+qed "constrains_imp_subset";
+
+
+goalw thy [constrains_def]
+ "!!Acts. [| id: Acts; constrains Acts A B; constrains Acts B C |] \
+\ ==> constrains Acts A C";
+by (Blast_tac 1);
+qed "constrains_trans";
+
+
+(*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 thy [constrains_def]
+ "!!Acts. [| ALL m. constrains Acts {s. s x = m} (B m) |] \
+\ ==> constrains Acts {s. P(s x)} (UN m. {s. P(m)} Int 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 thy [constrains_def]
+ "!!Acts. [| ALL m. constrains Acts {m} (B m) |] \
+\ ==> constrains Acts {s. P s} (UN m. {s. P(m)} Int B m)";
+by (Blast_tac 1);
+qed "elimination_sing";
+
+
+goalw thy [constrains_def]
+ "!!Acts. [| constrains Acts A (A' Un B); constrains Acts B B'; id: Acts |] \
+\ ==> constrains Acts A (A' Un B')";
+by (Blast_tac 1);
+qed "constrains_cancel";
+
+
+
+(*** Theoretical Results from Section 6 ***)
+
+goalw thy [constrains_def, strongest_rhs_def]
+ "constrains Acts A (strongest_rhs Acts A )";
+by (Blast_tac 1);
+qed "constrains_strongest_rhs";
+
+goalw thy [constrains_def, strongest_rhs_def]
+ "!!Acts. constrains Acts A B ==> strongest_rhs Acts A <= B";
+by (Blast_tac 1);
+qed "strongest_rhs_is_strongest";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/UNITY.thy Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,27 @@
+(* Title: HOL/UNITY/UNITY
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+The basic UNITY theory (revised version, based upon the "co" operator)
+
+From Misra, "A Logic for Concurrent Programming", 1994
+*)
+
+UNITY = LessThan +
+
+constdefs
+
+ constrains :: "[('a * 'a)set set, 'a set, 'a set] => bool"
+ "constrains Acts A B == ALL act:Acts. act^^A <= B"
+
+ stable :: "('a * 'a)set set => 'a set => bool"
+ "stable Acts A == constrains Acts A A"
+
+ strongest_rhs :: "[('a * 'a)set set, 'a set] => 'a set"
+ "strongest_rhs Acts A == Inter {B. constrains Acts A B}"
+
+ unless :: "[('a * 'a)set set, 'a set, 'a set] => bool"
+ "unless mutex A B == constrains mutex (A-B) (A Un B)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Update.ML Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,26 @@
+(* Title: HOL/UNITY/Update.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Function updates: like the standard theory Map, but for ordinary functions
+*)
+
+open Update;
+
+goalw thy [update_def] "(f[x|->y] = f) = (f x = y)";
+by Safe_tac;
+by (etac subst 1);
+by (rtac ext 2);
+by Auto_tac;
+qed "update_idem_iff";
+
+(* f x = y ==> f[x|->y] = f *)
+bind_thm("update_idem", update_idem_iff RS iffD2);
+
+AddIffs [refl RS update_idem];
+
+goal thy "(f[x|->y])z = (if x=z then y else f z)";
+by (simp_tac (simpset() addsimps [update_def]) 1);
+qed "update_apply";
+Addsimps [update_apply];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Update.thy Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,22 @@
+(* Title: HOL/UNITY/Update.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Function updates: like the standard theory Map, but for ordinary functions
+*)
+
+Update = Fun +
+
+consts
+ update :: "('a => 'b) => 'a => 'b => ('a => 'b)"
+ ("_/[_/|->/_]" [900,0,0] 900)
+
+syntax (symbols)
+ update :: "('a => 'b) => 'a => 'b => ('a => 'b)"
+ ("_/[_/\\<mapsto>/_]" [900,0,0] 900)
+
+defs
+ update_def "f[a|->b] == %x. if x=a then b else f x"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/WFair.ML Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,576 @@
+(* Title: HOL/UNITY/WFair
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Weak Fairness versions of transient, ensures, leadsTo.
+
+From Misra, "A Logic for Concurrent Programming", 1994
+*)
+
+open WFair;
+
+goal thy "Union(B) Int A = Union((%C. C Int A)``B)";
+by (Blast_tac 1);
+qed "Int_Union_Union";
+
+
+(*** transient ***)
+
+goalw thy [stable_def, constrains_def, transient_def]
+ "!!A. [| stable Acts A; transient Acts A |] ==> A = {}";
+by (Blast_tac 1);
+qed "stable_transient_empty";
+
+goalw thy [transient_def]
+ "!!A. [| transient Acts A; B<=A |] ==> transient Acts B";
+by (Clarify_tac 1);
+by (rtac bexI 1 THEN assume_tac 2);
+by (Blast_tac 1);
+qed "transient_strengthen";
+
+goalw thy [transient_def]
+ "!!A. [| act:Acts; A <= Domain act; act^^A <= Compl A |] \
+\ ==> transient Acts A";
+by (Blast_tac 1);
+qed "transient_mem";
+
+
+(*** ensures ***)
+
+goalw thy [ensures_def]
+ "!!Acts. [| constrains Acts (A-B) (A Un B); transient Acts (A-B) |] \
+\ ==> ensures Acts A B";
+by (Blast_tac 1);
+qed "ensuresI";
+
+goalw thy [ensures_def]
+ "!!Acts. ensures Acts A B \
+\ ==> constrains Acts (A-B) (A Un B) & transient Acts (A-B)";
+by (Blast_tac 1);
+qed "ensuresD";
+
+(*The L-version (precondition strengthening) doesn't hold for ENSURES*)
+goalw thy [ensures_def]
+ "!!Acts. [| ensures Acts A A'; A'<=B' |] ==> ensures Acts A B'";
+by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
+qed "ensures_weaken_R";
+
+goalw thy [ensures_def, constrains_def, transient_def]
+ "!!Acts. Acts ~= {} ==> ensures Acts A UNIV";
+by (Asm_simp_tac 1); (*omitting this causes PROOF FAILED, even with Safe_tac*)
+by (Blast_tac 1);
+qed "ensures_UNIV";
+
+goalw thy [ensures_def]
+ "!!Acts. [| 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')";
+by (asm_simp_tac (simpset() addsimps [Int_Un_distrib RS sym,
+ Diff_Int_distrib RS sym,
+ stable_constrains_Int]) 1);
+qed "stable_ensures_Int";
+
+
+(*** leadsTo ***)
+
+(*Synonyms for the theorems produced by the inductive defn package*)
+bind_thm ("leadsTo_Basis", leadsto.Basis);
+bind_thm ("leadsTo_Trans", leadsto.Trans);
+
+goal thy "!!Acts. act: Acts ==> leadsTo Acts A UNIV";
+by (blast_tac (claset() addIs [ensures_UNIV RS leadsTo_Basis]) 1);
+qed "leadsTo_UNIV";
+Addsimps [leadsTo_UNIV];
+
+(*Useful with cancellation, disjunction*)
+goal thy "!!Acts. leadsTo Acts A (A' Un A') ==> leadsTo Acts A A'";
+by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
+qed "leadsTo_Un_duplicate";
+
+goal thy "!!Acts. leadsTo Acts A (A' Un C Un C) ==> leadsTo Acts 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);
+qed "leadsTo_Union";
+
+val prems = goal thy
+ "(!!i. i : I ==> leadsTo Acts (A i) B) ==> leadsTo Acts (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 thy
+ "!!C. [| leadsTo Acts A C; leadsTo Acts B C |] ==> leadsTo Acts (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 |] \
+\ ==> P A C; \
+\ !!B S. ALL A:S. leadsTo Acts A B & P A B ==> P (Union S) B \
+\ |] ==> P za zb";
+br (major RS leadsto.induct) 1;
+by (REPEAT (blast_tac (claset() addIs prems) 1));
+qed "leadsTo_induct";
+
+
+goal thy "!!A B. [| A<=B; id: Acts |] ==> leadsTo Acts A B";
+by (rtac leadsTo_Basis 1);
+by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
+by (Blast_tac 1);
+qed "subset_imp_leadsTo";
+
+bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo);
+Addsimps [empty_leadsTo];
+
+
+(*There's a direct proof by leadsTo_Trans and subset_imp_leadsTo, but it
+ needs the extra premise id:Acts*)
+goal thy "!!Acts. 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 thy "!!Acts. [| leadsTo Acts A A'; B<=A; id: Acts |] ==> \
+\ leadsTo Acts 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 thy
+ "!!C. id: Acts ==> \
+\ leadsTo Acts (A Un B) C = (leadsTo Acts A C & leadsTo Acts B C)";
+by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1);
+qed "leadsTo_Un_distrib";
+
+goal thy
+ "!!C. id: Acts ==> \
+\ leadsTo Acts (UN i:I. A i) B = (ALL i : I. leadsTo Acts (A i) B)";
+by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1);
+qed "leadsTo_UN_distrib";
+
+goal thy
+ "!!C. id: Acts ==> \
+\ leadsTo Acts (Union S) B = (ALL A : S. leadsTo Acts A B)";
+by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1);
+qed "leadsTo_Union_distrib";
+
+
+goal thy
+ "!!Acts. [| leadsTo Acts A A'; id: Acts; B<=A; A'<=B' |] \
+\ ==> leadsTo Acts B B'";
+(*PROOF FAILED: why?*)
+by (blast_tac (claset() addIs [leadsTo_Trans, leadsTo_weaken_R,
+ leadsTo_weaken_L]) 1);
+qed "leadsTo_weaken";
+
+
+(*Set difference: maybe combine with leadsTo_weaken_L??*)
+goal thy
+ "!!C. [| leadsTo Acts (A-B) C; leadsTo Acts B C; id: Acts |] \
+\ ==> leadsTo Acts A C";
+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 ==> leadsTo Acts (A i) (A' i)) \
+\ ==> leadsTo Acts (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);
+qed "leadsTo_UN_UN";
+
+
+(*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)";
+by (blast_tac (claset() addIs [leadsTo_UN_UN]
+ addIs prems) 1);
+qed "leadsTo_UN_UN_noindex";
+
+(*Version with no index set*)
+goal thy
+ "!!Acts. ALL i. leadsTo Acts (A i) (A' i) \
+\ ==> leadsTo Acts (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 thy "!!Acts. [| leadsTo Acts A A'; leadsTo Acts B B' |] \
+\ ==> leadsTo Acts (A Un B) (A' Un B')";
+by (blast_tac (claset() addIs [leadsTo_Un,
+ leadsTo_weaken_R]) 1);
+qed "leadsTo_Un_Un";
+
+
+(** The cancellation law **)
+
+goal thy
+ "!!Acts. [| leadsTo Acts A (A' Un B); leadsTo Acts B B'; id: Acts |] \
+\ ==> leadsTo Acts A (A' Un B')";
+by (blast_tac (claset() addIs [leadsTo_Un_Un,
+ subset_imp_leadsTo, leadsTo_Trans]) 1);
+qed "leadsTo_cancel2";
+
+goal thy
+ "!!Acts. [| leadsTo Acts A (A' Un B); leadsTo Acts (B-A') B'; id: Acts |] \
+\ ==> leadsTo Acts A (A' Un B')";
+by (rtac leadsTo_cancel2 1);
+by (assume_tac 2);
+by (ALLGOALS Asm_simp_tac);
+qed "leadsTo_cancel_Diff2";
+
+goal thy
+ "!!Acts. [| leadsTo Acts A (B Un A'); leadsTo Acts B B'; id: Acts |] \
+\ ==> leadsTo Acts 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 thy
+ "!!Acts. [| leadsTo Acts A (B Un A'); leadsTo Acts (B-A') B'; id: Acts |] \
+\ ==> leadsTo Acts 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 **)
+
+goal thy "!!Acts. leadsTo Acts 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 thy "!!Acts. leadsTo Acts A {} ==> A={}";
+by (blast_tac (claset() addSIs [lemma]) 1);
+qed "leadsTo_empty";
+
+
+(** PSP: Progress-Safety-Progress **)
+
+(*Special case of PSP: Misra's "stable conjunction". Doesn't need id:Acts. *)
+goalw thy [stable_def]
+ "!!Acts. [| leadsTo Acts A A'; stable Acts B |] \
+\ ==> leadsTo Acts (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);
+by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
+by (rtac leadsTo_Basis 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [ensures_def,
+ Diff_Int_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1);
+by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1);
+qed "PSP_stable";
+
+goal thy
+ "!!Acts. [| leadsTo Acts A A'; stable Acts B |] \
+\ ==> leadsTo Acts (B Int A) (B Int A')";
+by (asm_simp_tac (simpset() addsimps (PSP_stable::Int_ac)) 1);
+qed "PSP_stable2";
+
+
+goalw thy [ensures_def]
+ "!!Acts. [| ensures Acts A A'; constrains Acts B B' |] \
+\ ==> ensures Acts (A Int B) ((A' Int B) Un (B' - B))";
+by Safe_tac;
+by (blast_tac (claset() addIs [constrainsI] addDs [constrainsD]) 1);
+by (etac transient_strengthen 1);
+by (Blast_tac 1);
+qed "PSP_ensures";
+
+
+goal thy
+ "!!Acts. [| leadsTo Acts A A'; constrains Acts B B'; id: Acts |] \
+\ ==> leadsTo Acts (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 thy
+ "!!Acts. [| leadsTo Acts A A'; constrains Acts B B'; id: Acts |] \
+\ ==> leadsTo Acts (B Int A) ((B Int A') Un (B' - B))";
+by (asm_simp_tac (simpset() addsimps (PSP::Int_ac)) 1);
+qed "PSP2";
+
+
+goalw thy [unless_def]
+ "!!Acts. [| leadsTo Acts A A'; unless Acts B B'; id: Acts |] \
+\ ==> leadsTo Acts (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;
+qed "PSP_unless";
+
+
+(*** Proving the induction rules ***)
+
+goal thy
+ "!!Acts. [| 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";
+by (eres_inst_tac [("a","m")] wf_induct 1);
+by (subgoal_tac "leadsTo Acts (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);
+by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1);
+val lemma = result();
+
+
+(** Meta or object quantifier ????? **)
+goal thy
+ "!!Acts. [| wf r; \
+\ ALL m. leadsTo Acts (A Int f-``{m}) \
+\ ((A Int f-``(r^-1 ^^ {m})) Un B); \
+\ id: Acts |] \
+\ ==> leadsTo Acts A B";
+by (res_inst_tac [("t", "A")] subst 1);
+by (rtac leadsTo_UN 2);
+by (etac lemma 2);
+by (REPEAT (assume_tac 2));
+by (Fast_tac 1); (*Blast_tac: Function unknown's argument not a parameter*)
+qed "leadsTo_wf_induct";
+
+
+goal thy
+ "!!Acts. [| 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)";
+by (etac leadsTo_wf_induct 1);
+by Safe_tac;
+by (case_tac "m:I" 1);
+by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
+by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
+qed "bounded_induct";
+
+
+(*Alternative proof is via the lemma leadsTo Acts (A Int f-``(lessThan m)) B*)
+goal thy
+ "!!Acts. [| ALL m. leadsTo Acts (A Int f-``{m}) \
+\ ((A Int f-``(lessThan m)) Un B); \
+\ id: Acts |] \
+\ ==> leadsTo Acts 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 thy
+ "!!Acts. [| 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);
+by (rtac (wf_less_than RS bounded_induct) 1);
+by (assume_tac 2);
+by (Asm_simp_tac 1);
+qed "lessThan_bounded_induct";
+
+goal thy
+ "!!Acts. [| 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)";
+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);
+by (blast_tac (claset() addIs [not_leE, subset_imp_leadsTo]) 2);
+by (blast_tac (claset() addIs [leadsTo_weaken_R, diff_less_mono2]) 1);
+qed "greaterThan_bounded_induct";
+
+
+
+(*** wlt ****)
+
+(*Misra's property W3*)
+goalw thy [wlt_def] "leadsTo Acts (wlt Acts B) B";
+by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
+qed "wlt_leadsTo";
+
+goalw thy [wlt_def] "!!Acts. leadsTo Acts A B ==> A <= wlt Acts B";
+by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
+qed "leadsTo_subset";
+
+(*Misra's property W2*)
+goal thy "!!Acts. id: Acts ==> leadsTo Acts A B = (A <= wlt Acts 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 thy "!!Acts. id: Acts ==> B <= wlt Acts B";
+by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS sym,
+ subset_imp_leadsTo]) 1);
+qed "wlt_increasing";
+
+
+(*Used in the Trans case below*)
+goalw thy [constrains_def]
+ "!!Acts. [| 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)";
+by (Clarify_tac 1);
+by (blast_tac (claset() addSDs [bspec]) 1);
+val lemma1 = result();
+
+
+(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
+goal thy
+ "!!Acts. [| leadsTo Acts A A'; id: Acts |] ==> \
+\ EX B. A<=B & leadsTo Acts B A' & constrains Acts (B-A') (B Un A')";
+by (etac leadsTo_induct 1);
+(*Basis*)
+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 (res_inst_tac [("x", "UN A:S. f A")] exI 1);
+by (blast_tac (claset() addIs [leadsTo_UN, constrains_weaken]) 1);
+qed "leadsTo_123";
+
+
+(*Misra's property W5*)
+goal thy "!!Acts. id: Acts ==> constrains Acts (wlt Acts B - B) (wlt Acts B)";
+by (forward_tac [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 (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [wlt_increasing, Un_absorb2]) 1);
+qed "wlt_constrains_wlt";
+
+
+(*** Completion: Binary and General Finite versions ***)
+
+goal thy
+ "!!Acts. [| 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);
+by (asm_full_simp_tac (simpset() addsimps [stable_def]) 2);
+by (EVERY [etac (constrains_Un RS constrains_weaken) 2,
+ etac 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 (blast_tac (claset() addIs [PSP_stable]) 2);
+by (subgoal_tac "leadsTo Acts (A' Int wlt Acts 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 (blast_tac (claset() addIs [leadsTo_subset RS subsetD,
+ subset_imp_leadsTo]) 2);
+(*Blast_tac gives PROOF FAILED*)
+by (best_tac (claset() addIs [leadsTo_Trans]) 1);
+qed "stable_completion";
+
+
+goal thy
+ "!!Acts. [| 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)";
+by (etac finite_induct 1);
+by (Asm_simp_tac 1);
+by (asm_simp_tac
+ (simpset() addsimps [stable_completion, stable_def,
+ ball_constrains_INT]) 1);
+qed_spec_mp "finite_stable_completion";
+
+
+goal thy
+ "!!Acts. [| 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);
+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 (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 (simp_tac (simpset() addsimps [Int_Diff]) 2);
+by (blast_tac (claset() addIs [wlt_leadsTo, PSP RS leadsTo_weaken_R]) 2);
+by (subgoal_tac "leadsTo Acts (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() addIs [leadsTo_subset, Int_mono]
+ delrules [subsetI]) 2);
+by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1);
+bind_thm("completion", refl RS result());
+
+
+goal thy
+ "!!Acts. [| 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)";
+by (etac finite_induct 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 "finite_completion";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/WFair.thy Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,43 @@
+(* Title: HOL/UNITY/WFair
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Weak Fairness versions of transient, ensures, leadsTo.
+
+From Misra, "A Logic for Concurrent Programming", 1994
+*)
+
+WFair = Traces + Vimage +
+
+constdefs
+
+ 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)"
+
+consts leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool"
+ leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set"
+
+translations
+ "leadsTo Acts A B" == "(A,B) : leadsto Acts"
+
+inductive "leadsto Acts"
+ intrs
+
+ Basis "ensures Acts A B ==> leadsTo Acts A B"
+
+ Trans "[| leadsTo Acts A B; leadsTo Acts B C |]
+ ==> leadsTo Acts A C"
+
+ Union "(UN A:S. {(A,B)}) : Pow (leadsto Acts)
+ ==> leadsTo Acts (Union S) B"
+
+ monos "[Pow_mono]"
+
+constdefs wlt :: "[('a * 'a)set set, 'a set] => 'a set"
+ "wlt Acts B == Union {A. leadsTo Acts A B}"
+
+end