New UNITY theory
authorpaulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 47761f9362e769c1
parent 4775 66b1a7c42d94
child 4777 379f32b0ae40
New UNITY theory
src/HOL/UNITY/Channel.ML
src/HOL/UNITY/Channel.thy
src/HOL/UNITY/Common.ML
src/HOL/UNITY/Common.thy
src/HOL/UNITY/Deadlock.ML
src/HOL/UNITY/Deadlock.thy
src/HOL/UNITY/FP.ML
src/HOL/UNITY/FP.thy
src/HOL/UNITY/LessThan.ML
src/HOL/UNITY/LessThan.thy
src/HOL/UNITY/Mutex.ML
src/HOL/UNITY/Mutex.thy
src/HOL/UNITY/Network.ML
src/HOL/UNITY/Network.thy
src/HOL/UNITY/README.html
src/HOL/UNITY/ROOT.ML
src/HOL/UNITY/Reach.ML
src/HOL/UNITY/Reach.thy
src/HOL/UNITY/SubstAx.ML
src/HOL/UNITY/SubstAx.thy
src/HOL/UNITY/Token.ML
src/HOL/UNITY/Token.thy
src/HOL/UNITY/Traces.ML
src/HOL/UNITY/Traces.thy
src/HOL/UNITY/UNITY.ML
src/HOL/UNITY/UNITY.thy
src/HOL/UNITY/Update.ML
src/HOL/UNITY/Update.thy
src/HOL/UNITY/WFair.ML
src/HOL/UNITY/WFair.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/UNITY/Channel.ML	Fri Apr 03 12:34:33 1998 +0200
     1.3 @@ -0,0 +1,67 @@
     1.4 +(*  Title:      HOL/UNITY/Channel
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1998  University of Cambridge
     1.8 +
     1.9 +Unordered Channel
    1.10 +
    1.11 +From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
    1.12 +*)
    1.13 +
    1.14 +open Channel;
    1.15 +
    1.16 +AddIffs [skip];
    1.17 +
    1.18 +
    1.19 +(*None represents "infinity" while Some represents proper integers*)
    1.20 +goalw thy [minSet_def] "!!A. minSet A = Some x --> x : A";
    1.21 +by (Simp_tac 1);
    1.22 +by (fast_tac (claset() addIs [LeastI]) 1);
    1.23 +qed_spec_mp "minSet_eq_SomeD";
    1.24 +
    1.25 +goalw thy [minSet_def] " minSet{} = None";
    1.26 +by (Asm_simp_tac 1);
    1.27 +qed_spec_mp "minSet_empty";
    1.28 +Addsimps [minSet_empty];
    1.29 +
    1.30 +goalw thy [minSet_def] "!!A. x:A ==> minSet A = Some (LEAST x. x: A)";
    1.31 +by (ALLGOALS Asm_simp_tac);
    1.32 +by (Blast_tac 1);
    1.33 +qed_spec_mp "minSet_nonempty";
    1.34 +
    1.35 +goal thy
    1.36 +    "leadsTo Acts (minSet -`` {Some x}) (minSet -`` (Some``greaterThan x))";
    1.37 +by (rtac leadsTo_weaken 1);
    1.38 +by (rtac ([UC2, UC1] MRS PSP) 1);
    1.39 +by (ALLGOALS Asm_simp_tac);
    1.40 +by (Blast_tac 1);
    1.41 +by Safe_tac;
    1.42 +by (auto_tac (claset() addDs [minSet_eq_SomeD], 
    1.43 +	      simpset() addsimps [le_def, nat_neq_iff]));
    1.44 +qed "minSet_greaterThan";
    1.45 +
    1.46 +
    1.47 +(*The induction*)
    1.48 +goal thy "leadsTo Acts (UNIV-{{}}) (minSet -`` (Some``atLeast y))";
    1.49 +by (rtac leadsTo_weaken_R 1);
    1.50 +by (res_inst_tac  [("l", "y"), ("f", "the o minSet"), ("B", "{}")]
    1.51 +     greaterThan_bounded_induct 1);
    1.52 +by Safe_tac;
    1.53 +by (ALLGOALS Asm_simp_tac);
    1.54 +by (dtac minSet_nonempty 2);
    1.55 +by (Asm_full_simp_tac 2);
    1.56 +by (rtac (minSet_greaterThan RS leadsTo_weaken) 1);
    1.57 +by Safe_tac;
    1.58 +by (ALLGOALS Asm_full_simp_tac);
    1.59 +by (dtac minSet_nonempty 1);
    1.60 +by (Asm_full_simp_tac 1);
    1.61 +val lemma = result();
    1.62 +
    1.63 +
    1.64 +goal thy "!!y::nat. leadsTo Acts (UNIV-{{}}) {s. y ~: s}";
    1.65 +by (rtac (lemma RS leadsTo_weaken_R) 1);
    1.66 +by (Clarify_tac 1);
    1.67 +by (forward_tac [minSet_nonempty] 1);
    1.68 +by (asm_full_simp_tac (simpset() addsimps [Suc_le_eq]) 1);
    1.69 +by (blast_tac (claset() addDs [Suc_le_lessD, not_less_Least]) 1);
    1.70 +qed "Channel_progress";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/UNITY/Channel.thy	Fri Apr 03 12:34:33 1998 +0200
     2.3 @@ -0,0 +1,29 @@
     2.4 +(*  Title:      HOL/UNITY/Channel
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1998  University of Cambridge
     2.8 +
     2.9 +Unordered Channel
    2.10 +
    2.11 +From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
    2.12 +*)
    2.13 +
    2.14 +Channel = WFair + Option + 
    2.15 +
    2.16 +types state = nat set
    2.17 +
    2.18 +constdefs
    2.19 +  minSet :: nat set => nat option
    2.20 +    "minSet A == if A={} then None else Some (LEAST x. x:A)"
    2.21 +
    2.22 +rules
    2.23 +
    2.24 +  skip "id: Acts"
    2.25 +
    2.26 +  UC1  "constrains Acts (minSet -`` {Some x}) (minSet -`` (Some``atLeast x))"
    2.27 +
    2.28 +  (*  UC1  "constrains Acts {s. minSet s = x} {s. x <= minSet s}"  *)
    2.29 +
    2.30 +  UC2  "leadsTo Acts (minSet -`` {Some x}) {s. x ~: s}"
    2.31 +
    2.32 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/UNITY/Common.ML	Fri Apr 03 12:34:33 1998 +0200
     3.3 @@ -0,0 +1,102 @@
     3.4 +(*  Title:      HOL/UNITY/Common
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1998  University of Cambridge
     3.8 +
     3.9 +Common Meeting Time example from Misra (1994)
    3.10 +
    3.11 +The state is identified with the one variable in existence.
    3.12 +
    3.13 +From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
    3.14 +*)
    3.15 +
    3.16 +
    3.17 +open Common;
    3.18 +
    3.19 +(*Misra's property CMT4: t exceeds no common meeting time*)
    3.20 +goal thy
    3.21 +  "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); n: common |] \
    3.22 +\           ==> stable Acts (atMost n)";
    3.23 +by (dres_inst_tac [("P", "%t. t<=n")] elimination_sing 1);
    3.24 +by (asm_full_simp_tac
    3.25 +    (simpset() addsimps [atMost_def, stable_def, common_def, maxfg_def,
    3.26 +			 constrains_def, le_max_iff_disj]) 1);
    3.27 +by (Clarify_tac 1);
    3.28 +by (dtac bspec 1);
    3.29 +by (assume_tac 1);
    3.30 +by (blast_tac (claset() addSEs [subsetCE]
    3.31 +			addIs [order_eq_refl, fmono, gmono, le_trans]) 1);
    3.32 +qed "common_stable";
    3.33 +
    3.34 +goal thy
    3.35 +  "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); n: common |] \
    3.36 +\           ==> reachable {0} Acts <= atMost n";
    3.37 +by (rtac strongest_invariant 1);
    3.38 +by (asm_simp_tac (simpset() addsimps [common_stable]) 2);
    3.39 +by (simp_tac (simpset() addsimps [atMost_def]) 1);
    3.40 +qed "common_invariant";
    3.41 +
    3.42 +
    3.43 +(*** Some programs that implement the safety property above ***)
    3.44 +
    3.45 +(*This one is just Skip*)
    3.46 +goal thy "constrains {id} {m} (maxfg m)";
    3.47 +by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj,
    3.48 +				  fasc, gasc]) 1);
    3.49 +result();
    3.50 +
    3.51 +(*This one is  t := ftime t || t := gtime t    really needs Skip too*)
    3.52 +goal thy "constrains {range(%t.(t,ftime t)), range(%t.(t,gtime t))} \
    3.53 +\                    {m} (maxfg m)";
    3.54 +by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, 
    3.55 +				  le_max_iff_disj]) 1);
    3.56 +by (Blast_tac 1);
    3.57 +result();
    3.58 +
    3.59 +(*This one is  t := max (ftime t) (gtime t)    really needs Skip too*)
    3.60 +goal thy "constrains {range(%t.(t, max (ftime t) (gtime t)))} \
    3.61 +\                    {m} (maxfg m)";
    3.62 +by (simp_tac (simpset() addsimps [constrains_def, maxfg_def]) 1);
    3.63 +by (Blast_tac 1);
    3.64 +result();
    3.65 +
    3.66 +(*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
    3.67 +goalw thy [constrains_def, maxfg_def] 
    3.68 +    "constrains { {(t, Suc t) | t. t < max (ftime t) (gtime t)} } \
    3.69 +\               {m} (maxfg m)";
    3.70 +by (blast_tac (claset() addIs [Suc_leI]) 1);
    3.71 +result();
    3.72 +
    3.73 +
    3.74 +(*It remans to prove that they satisfy CMT3': t does not decrease,
    3.75 +  and that CMT3' implies that t stops changing once common(t) holds.*)
    3.76 +
    3.77 +
    3.78 +(*** Progress under weak fairness ***)
    3.79 +
    3.80 +Addsimps [atMost_Int_atLeast];
    3.81 +
    3.82 +goal thy
    3.83 +    "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); \
    3.84 +\               ALL m: lessThan n. leadsTo Acts {m} (greaterThan m); \
    3.85 +\               n: common;  id: Acts |]  \
    3.86 +\            ==> leadsTo Acts (atMost n) common";
    3.87 +by (rtac leadsTo_weaken_R 1);
    3.88 +by (res_inst_tac [("f","%x. x"), ("l", "n")] greaterThan_bounded_induct 1);
    3.89 +by (ALLGOALS Asm_simp_tac);
    3.90 +by (rtac subset_refl 2);
    3.91 +by (blast_tac (claset() addDs [PSP_stable2] 
    3.92 +                        addIs [common_stable, leadsTo_weaken_R]) 1);
    3.93 +val lemma = result();
    3.94 +
    3.95 +(*The "ALL m: Compl common" form echoes CMT6.*)
    3.96 +goal thy
    3.97 +    "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); \
    3.98 +\               ALL m: Compl common. leadsTo Acts {m} (greaterThan m); \
    3.99 +\               n: common;  id: Acts |]  \
   3.100 +\            ==> leadsTo Acts (atMost (LEAST n. n: common)) common";
   3.101 +by (rtac lemma 1);
   3.102 +by (ALLGOALS Asm_simp_tac);
   3.103 +by (etac LeastI 2);
   3.104 +by (blast_tac (claset() addSDs [not_less_Least]) 1);
   3.105 +qed "leadsTo_common";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/UNITY/Common.thy	Fri Apr 03 12:34:33 1998 +0200
     4.3 @@ -0,0 +1,32 @@
     4.4 +(*  Title:      HOL/UNITY/Common
     4.5 +    ID:         $Id$
     4.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 +    Copyright   1998  University of Cambridge
     4.8 +
     4.9 +Common Meeting Time example from Misra (1994)
    4.10 +
    4.11 +The state is identified with the one variable in existence.
    4.12 +
    4.13 +From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
    4.14 +*)
    4.15 +
    4.16 +Common = WFair +
    4.17 +
    4.18 +consts
    4.19 +  ftime,gtime :: nat=>nat
    4.20 +
    4.21 +rules
    4.22 +  fmono "m <= n ==> ftime m <= ftime n"
    4.23 +  gmono "m <= n ==> gtime m <= gtime n"
    4.24 +
    4.25 +  fasc  "m <= ftime n"
    4.26 +  gasc  "m <= gtime n"
    4.27 +
    4.28 +constdefs
    4.29 +  common :: nat set
    4.30 +    "common == {n. ftime n = n & gtime n = n}"
    4.31 +
    4.32 +  maxfg :: nat => nat set
    4.33 +    "maxfg m == {t. t <= max (ftime m) (gtime m)}"
    4.34 +
    4.35 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/UNITY/Deadlock.ML	Fri Apr 03 12:34:33 1998 +0200
     5.3 @@ -0,0 +1,90 @@
     5.4 +
     5.5 +
     5.6 +(*** Deadlock examples from section 5.6 ***)
     5.7 +
     5.8 +(*Trivial, two-process case*)
     5.9 +goalw thy [constrains_def, stable_def]
    5.10 +    "!!Acts. [| constrains Acts (A Int B) A;  constrains Acts (B Int A) B |] \
    5.11 +\           ==> stable Acts (A Int B)";
    5.12 +by (Blast_tac 1);
    5.13 +result();
    5.14 +
    5.15 +
    5.16 +goal thy "{i. i < Suc n} = insert n {i. i < n}";
    5.17 +by (blast_tac (claset() addSEs [less_SucE] addIs [less_SucI]) 1);
    5.18 +qed "Collect_less_Suc_insert";
    5.19 +
    5.20 +
    5.21 +goal thy "{i. i <= Suc n} = insert (Suc n) {i. i <= n}";
    5.22 +by (blast_tac (claset() addSEs [le_SucE] addIs [le_SucI]) 1);
    5.23 +qed "Collect_le_Suc_insert";
    5.24 +
    5.25 +
    5.26 +(*a simplification step*)
    5.27 +goal thy "(INT i:{i. i <= n}. A(Suc i) Int A i) = \
    5.28 +\         (INT i:{i. i <= Suc n}. A i)";
    5.29 +by (induct_tac "n" 1);
    5.30 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [Collect_le_Suc_insert])));
    5.31 +by (blast_tac (claset() addEs [le_SucE] addSEs [equalityE]) 1);
    5.32 +qed "Collect_le_Int_equals";
    5.33 +
    5.34 +
    5.35 +(*Dual of the required property.  Converse inclusion fails.*)
    5.36 +goal thy "(UN i:{i. i < n}. A i) Int Compl (A n) <=  \
    5.37 +\         (UN i:{i. i < n}. (A i) Int Compl (A(Suc i)))";
    5.38 +by (induct_tac "n" 1);
    5.39 +by (Asm_simp_tac 1);
    5.40 +by (simp_tac (simpset() addsimps [Collect_less_Suc_insert]) 1);
    5.41 +by (Blast_tac 1);
    5.42 +qed "UN_Int_Compl_subset";
    5.43 +
    5.44 +
    5.45 +(*Converse inclusion fails.*)
    5.46 +goal thy "(INT i:{i. i < n}. Compl(A i) Un A (Suc i))  <= \
    5.47 +\         (INT i:{i. i < n}. Compl(A i)) Un A n";
    5.48 +by (induct_tac "n" 1);
    5.49 +by (Asm_simp_tac 1);
    5.50 +by (asm_simp_tac (simpset() addsimps [Collect_less_Suc_insert]) 1);
    5.51 +by (Blast_tac 1);
    5.52 +qed "INT_Un_Compl_subset";
    5.53 +
    5.54 +
    5.55 +(*Specialized rewriting*)
    5.56 +goal thy "A 0 Int (Compl (A n) Int \
    5.57 +\                  (INT i:{i. i < n}. Compl(A i) Un A (Suc i))) = {}";
    5.58 +by (blast_tac (claset() addIs [gr0I]
    5.59 +		        addDs [impOfSubs INT_Un_Compl_subset]) 1);
    5.60 +val lemma = result();
    5.61 +
    5.62 +(*Reverse direction makes it harder to invoke the ind hyp*)
    5.63 +goal thy "(INT i:{i. i <= n}. A i) = \
    5.64 +\         A 0 Int (INT i:{i. i < n}. Compl(A i) Un A(Suc i))";
    5.65 +by (induct_tac "n" 1);
    5.66 +by (Asm_simp_tac 1);
    5.67 +by (asm_simp_tac
    5.68 +    (simpset() addsimps (Int_ac @
    5.69 +			 [Int_Un_distrib, Int_Un_distrib2, lemma,
    5.70 +			  Collect_less_Suc_insert, Collect_le_Suc_insert])) 1);
    5.71 +qed "INT_le_equals_Int";
    5.72 +
    5.73 +goal thy "(INT i:{i. i <= Suc n}. A i) = \
    5.74 +\         A 0 Int (INT i:{i. i <= n}. Compl(A i) Un A(Suc i))";
    5.75 +by (simp_tac (simpset() addsimps [le_eq_less_Suc RS sym, 
    5.76 +				  INT_le_equals_Int]) 1);
    5.77 +qed "INT_le_Suc_equals_Int";
    5.78 +
    5.79 +
    5.80 +(*The final deadlock example*)
    5.81 +val [zeroprem, allprem] = goalw thy [stable_def]
    5.82 +    "[| constrains Acts (A 0 Int A (Suc n)) (A 0);  \
    5.83 +\       ALL i:{i. i <= n}. constrains Acts (A(Suc i) Int A i) \
    5.84 +\                                         (Compl(A i) Un A(Suc i)) |] \
    5.85 +\    ==> stable Acts (INT i:{i. i <= Suc n}. A i)";
    5.86 +
    5.87 +by (rtac ([zeroprem, allprem RS ball_constrains_INT] MRS 
    5.88 +    constrains_Int RS constrains_weaken) 1);
    5.89 +by (simp_tac (simpset() addsimps [Collect_le_Int_equals, 
    5.90 +				  Int_assoc, INT_absorb]) 1);
    5.91 +by (simp_tac (simpset() addsimps ([INT_le_Suc_equals_Int])) 1);
    5.92 +result();
    5.93 +
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/UNITY/Deadlock.thy	Fri Apr 03 12:34:33 1998 +0200
     6.3 @@ -0,0 +1,1 @@
     6.4 +Deadlock = UNITY
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/UNITY/FP.ML	Fri Apr 03 12:34:33 1998 +0200
     7.3 @@ -0,0 +1,66 @@
     7.4 +(*  Title:      HOL/UNITY/FP
     7.5 +    ID:         $Id$
     7.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.7 +    Copyright   1998  University of Cambridge
     7.8 +
     7.9 +Fixed Point of a Program
    7.10 +
    7.11 +From Misra, "A Logic for Concurrent Programming", 1994
    7.12 +*)
    7.13 +
    7.14 +goal thy "Union(B) Int A = (UN C:B. C Int A)";
    7.15 +by (Blast_tac 1);
    7.16 +qed "Int_Union2";
    7.17 +
    7.18 +open FP;
    7.19 +
    7.20 +goalw thy [FP_Orig_def, stable_def] "stable Acts (FP_Orig Acts Int B)";
    7.21 +by (stac Int_Union2 1);
    7.22 +by (rtac ball_constrains_UN 1);
    7.23 +by (Simp_tac 1);
    7.24 +qed "stable_FP_Orig_Int";
    7.25 +
    7.26 +
    7.27 +val prems = goalw thy [FP_Orig_def, stable_def]
    7.28 +    "(!!B. stable Acts (A Int B)) ==> A <= FP_Orig Acts";
    7.29 +by (blast_tac (claset() addIs prems) 1);
    7.30 +qed "FP_Orig_weakest";
    7.31 +
    7.32 +
    7.33 +goal thy "stable Acts (FP Acts Int B)";
    7.34 +by (subgoal_tac "FP Acts Int B = (UN x:B. FP Acts Int {x})" 1);
    7.35 +by (Blast_tac 2);
    7.36 +by (asm_simp_tac (simpset() addsimps [Int_insert_right]) 1);
    7.37 +by (rewrite_goals_tac [FP_def, stable_def]);
    7.38 +by (rtac ball_constrains_UN 1);
    7.39 +by (Simp_tac 1);
    7.40 +qed "stable_FP_Int";
    7.41 +
    7.42 +goal thy "FP Acts <= FP_Orig Acts";
    7.43 +by (rtac (stable_FP_Int RS FP_Orig_weakest) 1);
    7.44 +val lemma1 = result();
    7.45 +
    7.46 +goalw thy [FP_Orig_def, FP_def] "FP_Orig Acts <= FP Acts";
    7.47 +by (Clarify_tac 1);
    7.48 +by (dres_inst_tac [("x", "{x}")] spec 1);
    7.49 +by (asm_full_simp_tac (simpset() addsimps [Int_insert_right]) 1);
    7.50 +val lemma2 = result();
    7.51 +
    7.52 +goal thy "FP Acts = FP_Orig Acts";
    7.53 +by (rtac ([lemma1,lemma2] MRS equalityI) 1);
    7.54 +qed "FP_equivalence";
    7.55 +
    7.56 +val [prem] = goal thy
    7.57 +    "(!!B. stable Acts (A Int B)) ==> A <= FP Acts";
    7.58 +by (simp_tac (simpset() addsimps [FP_equivalence, prem RS FP_Orig_weakest]) 1);
    7.59 +qed "FP_weakest";
    7.60 +
    7.61 +goalw thy [FP_def, stable_def, constrains_def]
    7.62 +    "Compl (FP Acts) = (UN act:Acts. Compl{s. act^^{s} <= {s}})";
    7.63 +by (Blast_tac 1);
    7.64 +qed "Compl_FP";
    7.65 +
    7.66 +goal thy "A - (FP Acts) = (UN act:Acts. A - {s. act^^{s} <= {s}})";
    7.67 +by (simp_tac (simpset() addsimps [Diff_eq, Compl_FP]) 1);
    7.68 +qed "Diff_FP";
    7.69 +
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/UNITY/FP.thy	Fri Apr 03 12:34:33 1998 +0200
     8.3 @@ -0,0 +1,21 @@
     8.4 +(*  Title:      HOL/UNITY/FP
     8.5 +    ID:         $Id$
     8.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.7 +    Copyright   1998  University of Cambridge
     8.8 +
     8.9 +Fixed Point of a Program
    8.10 +
    8.11 +From Misra, "A Logic for Concurrent Programming", 1994
    8.12 +*)
    8.13 +
    8.14 +FP = UNITY +
    8.15 +
    8.16 +constdefs
    8.17 +
    8.18 +  FP_Orig :: "('a * 'a)set set => 'a set"
    8.19 +    "FP_Orig Acts == Union{A. ALL B. stable Acts (A Int B)}"
    8.20 +
    8.21 +  FP :: "('a * 'a)set set => 'a set"
    8.22 +    "FP Acts == {s. stable Acts {s}}"
    8.23 +
    8.24 +end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/UNITY/LessThan.ML	Fri Apr 03 12:34:33 1998 +0200
     9.3 @@ -0,0 +1,146 @@
     9.4 +(*  Title:      HOL/LessThan/LessThan
     9.5 +    ID:         $Id$
     9.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7 +    Copyright   1998  University of Cambridge
     9.8 +
     9.9 +lessThan, greaterThan, atLeast, atMost
    9.10 +*)
    9.11 +
    9.12 +
    9.13 +open LessThan;
    9.14 +
    9.15 +
    9.16 +(*** lessThan ***)
    9.17 +
    9.18 +goalw thy [lessThan_def] "(i: lessThan k) = (i<k)";
    9.19 +by (Blast_tac 1);
    9.20 +qed "lessThan_iff";
    9.21 +AddIffs [lessThan_iff];
    9.22 +
    9.23 +goalw thy [lessThan_def] "lessThan 0 = {}";
    9.24 +by (Simp_tac 1);
    9.25 +qed "lessThan_0";
    9.26 +Addsimps [lessThan_0];
    9.27 +
    9.28 +goalw thy [lessThan_def] "lessThan (Suc k) = insert k (lessThan k)";
    9.29 +by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
    9.30 +by (Blast_tac 1);
    9.31 +qed "lessThan_Suc";
    9.32 +
    9.33 +goal thy "(UN m. lessThan m) = UNIV";
    9.34 +by (Blast_tac 1);
    9.35 +qed "UN_lessThan_UNIV";
    9.36 +
    9.37 +goalw thy [lessThan_def, atLeast_def, le_def]
    9.38 +    "Compl(lessThan k) = atLeast k";
    9.39 +by (Blast_tac 1);
    9.40 +qed "Compl_lessThan";
    9.41 +
    9.42 +
    9.43 +(*** greaterThan ***)
    9.44 +
    9.45 +goalw thy [greaterThan_def] "(i: greaterThan k) = (k<i)";
    9.46 +by (Blast_tac 1);
    9.47 +qed "greaterThan_iff";
    9.48 +AddIffs [greaterThan_iff];
    9.49 +
    9.50 +goalw thy [greaterThan_def] "greaterThan 0 = range Suc";
    9.51 +by (blast_tac (claset() addIs [Suc_pred RS sym]) 1);
    9.52 +qed "greaterThan_0";
    9.53 +Addsimps [greaterThan_0];
    9.54 +
    9.55 +goalw thy [greaterThan_def] "greaterThan (Suc k) = greaterThan k - {Suc k}";
    9.56 +by Safe_tac;
    9.57 +by (blast_tac (claset() addIs [less_trans]) 1);
    9.58 +by (asm_simp_tac (simpset() addsimps [le_Suc_eq, not_le_iff_less RS sym]) 1);
    9.59 +by (asm_simp_tac (simpset() addsimps [not_le_iff_less]) 1);
    9.60 +qed "greaterThan_Suc";
    9.61 +
    9.62 +goal thy "(INT m. greaterThan m) = {}";
    9.63 +by (Blast_tac 1);
    9.64 +qed "INT_greaterThan_UNIV";
    9.65 +
    9.66 +goalw thy [greaterThan_def, atMost_def, le_def]
    9.67 +    "Compl(greaterThan k) = atMost k";
    9.68 +by (Blast_tac 1);
    9.69 +qed "Compl_greaterThan";
    9.70 +
    9.71 +goalw thy [greaterThan_def, atMost_def, le_def]
    9.72 +    "Compl(atMost k) = greaterThan k";
    9.73 +by (Blast_tac 1);
    9.74 +qed "Compl_atMost";
    9.75 +
    9.76 +goal thy "less_than ^^ {k} = greaterThan k";
    9.77 +by (Blast_tac 1);
    9.78 +qed "Image_less_than";
    9.79 +
    9.80 +Addsimps [Compl_greaterThan, Compl_atMost, Image_less_than];
    9.81 +
    9.82 +(*** atLeast ***)
    9.83 +
    9.84 +goalw thy [atLeast_def] "(i: atLeast k) = (k<=i)";
    9.85 +by (Blast_tac 1);
    9.86 +qed "atLeast_iff";
    9.87 +AddIffs [atLeast_iff];
    9.88 +
    9.89 +goalw thy [atLeast_def, UNIV_def] "atLeast 0 = UNIV";
    9.90 +by (Simp_tac 1);
    9.91 +qed "atLeast_0";
    9.92 +Addsimps [atLeast_0];
    9.93 +
    9.94 +goalw thy [atLeast_def] "atLeast (Suc k) = atLeast k - {k}";
    9.95 +by (simp_tac (simpset() addsimps [Suc_le_eq]) 1);
    9.96 +by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
    9.97 +by (Blast_tac 1);
    9.98 +qed "atLeast_Suc";
    9.99 +
   9.100 +goal thy "(UN m. atLeast m) = UNIV";
   9.101 +by (Blast_tac 1);
   9.102 +qed "UN_atLeast_UNIV";
   9.103 +
   9.104 +goalw thy [lessThan_def, atLeast_def, le_def]
   9.105 +    "Compl(atLeast k) = lessThan k";
   9.106 +by (Blast_tac 1);
   9.107 +qed "Compl_atLeast";
   9.108 +
   9.109 +goal thy "less_than^-1 ^^ {k} = lessThan k";
   9.110 +by (Blast_tac 1);
   9.111 +qed "Image_inverse_less_than";
   9.112 +
   9.113 +Addsimps [Compl_lessThan, Compl_atLeast, Image_inverse_less_than];
   9.114 +
   9.115 +(*** atMost ***)
   9.116 +
   9.117 +goalw thy [atMost_def] "(i: atMost k) = (i<=k)";
   9.118 +by (Blast_tac 1);
   9.119 +qed "atMost_iff";
   9.120 +AddIffs [atMost_iff];
   9.121 +
   9.122 +goalw thy [atMost_def] "atMost 0 = {0}";
   9.123 +by (Simp_tac 1);
   9.124 +qed "atMost_0";
   9.125 +Addsimps [atMost_0];
   9.126 +
   9.127 +goalw thy [atMost_def] "atMost (Suc k) = insert (Suc k) (atMost k)";
   9.128 +by (simp_tac (simpset() addsimps [less_Suc_eq, le_eq_less_or_eq]) 1);
   9.129 +by (Blast_tac 1);
   9.130 +qed "atMost_Suc";
   9.131 +
   9.132 +goal thy "(UN m. atMost m) = UNIV";
   9.133 +by (Blast_tac 1);
   9.134 +qed "UN_atMost_UNIV";
   9.135 +
   9.136 +goalw thy [atMost_def, le_def]
   9.137 +    "Compl(atMost k) = greaterThan k";
   9.138 +by (Blast_tac 1);
   9.139 +qed "Compl_atMost";
   9.140 +Addsimps [Compl_atMost];
   9.141 +
   9.142 +
   9.143 +(*** Combined properties ***)
   9.144 +
   9.145 +goal thy "atMost n Int atLeast n = {n}";
   9.146 +by (blast_tac (claset() addIs [le_anti_sym]) 1);
   9.147 +qed "atMost_Int_atLeast";
   9.148 +
   9.149 +
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/UNITY/LessThan.thy	Fri Apr 03 12:34:33 1998 +0200
    10.3 @@ -0,0 +1,25 @@
    10.4 +(*  Title:      HOL/UNITY/LessThan
    10.5 +    ID:         $Id$
    10.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.7 +    Copyright   1998  University of Cambridge
    10.8 +
    10.9 +lessThan, greaterThan, atLeast, atMost
   10.10 +*)
   10.11 +
   10.12 +LessThan = List +
   10.13 +
   10.14 +constdefs
   10.15 +
   10.16 +  lessThan   :: "nat => nat set"
   10.17 +     "lessThan n == {i. i<n}"
   10.18 +
   10.19 +  atMost   :: "nat => nat set"
   10.20 +     "atMost n == {i. i<=n}"
   10.21 + 
   10.22 +  greaterThan   :: "nat => nat set"
   10.23 +     "greaterThan n == {i. n<i}"
   10.24 +
   10.25 +  atLeast   :: "nat => nat set"
   10.26 +     "atLeast n == {i. n<=i}"
   10.27 +
   10.28 +end
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/UNITY/Mutex.ML	Fri Apr 03 12:34:33 1998 +0200
    11.3 @@ -0,0 +1,254 @@
    11.4 +(*  Title:      HOL/UNITY/Mutex.thy
    11.5 +    ID:         $Id$
    11.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    11.7 +    Copyright   1998  University of Cambridge
    11.8 +
    11.9 +Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
   11.10 +*)
   11.11 +
   11.12 +open Mutex;
   11.13 +
   11.14 +val cmd_defs = [mutex_def, cmd0_def, cmd1u_def, cmd1v_def, 
   11.15 +		cmd2_def, cmd3_def, cmd4_def];
   11.16 +
   11.17 +goalw thy [mutex_def] "id : mutex";
   11.18 +by (Simp_tac 1);
   11.19 +qed "id_in_mutex";
   11.20 +AddIffs [id_in_mutex];
   11.21 +
   11.22 +
   11.23 +(** Constrains/Ensures tactics: NEED TO BE GENERALIZED OVER ALL PROGRAMS **)
   11.24 +
   11.25 +(*proves "constrains" properties when the program is specified*)
   11.26 +val constrains_tac = 
   11.27 +   SELECT_GOAL
   11.28 +      (EVERY [rtac constrainsI 1,
   11.29 +	      rewtac mutex_def,
   11.30 +	      REPEAT_FIRST (eresolve_tac [insertE, emptyE]),
   11.31 +	      rewrite_goals_tac cmd_defs,
   11.32 +	      ALLGOALS (SELECT_GOAL Auto_tac)]);
   11.33 +
   11.34 +
   11.35 +(*proves "ensures" properties when the program is specified*)
   11.36 +fun ensures_tac sact = 
   11.37 +    SELECT_GOAL
   11.38 +      (EVERY [REPEAT (resolve_tac [LeadsTo_Basis, leadsTo_Basis, ensuresI] 1),
   11.39 +	      res_inst_tac [("act", sact)] transient_mem 2,
   11.40 +	      Simp_tac 2,
   11.41 +	      constrains_tac 1,
   11.42 +	      rewrite_goals_tac cmd_defs,
   11.43 +	      Auto_tac]);
   11.44 +
   11.45 +
   11.46 +(*The booleans p, u, v are always either 0 or 1*)
   11.47 +goalw thy [stable_def, boolVars_def]
   11.48 +    "stable mutex boolVars";
   11.49 +by (constrains_tac 1);
   11.50 +by (auto_tac (claset() addSEs [less_SucE], simpset()));
   11.51 +qed "stable_boolVars";
   11.52 +
   11.53 +goal thy "reachable MInit mutex <= boolVars";
   11.54 +by (rtac strongest_invariant 1);
   11.55 +by (rtac stable_boolVars 2);
   11.56 +by (rewrite_goals_tac [MInit_def, boolVars_def]);
   11.57 +by Auto_tac;
   11.58 +qed "reachable_subset_boolVars";
   11.59 +
   11.60 +val reachable_subset_boolVars' = 
   11.61 +    rewrite_rule [boolVars_def] reachable_subset_boolVars;
   11.62 +
   11.63 +goalw thy [stable_def, invariant_def]
   11.64 +    "stable mutex (invariant 0 UU MM)";
   11.65 +by (constrains_tac 1);
   11.66 +qed "stable_invar_0um";
   11.67 +
   11.68 +goalw thy [stable_def, invariant_def]
   11.69 +    "stable mutex (invariant 1 VV NN)";
   11.70 +by (constrains_tac 1);
   11.71 +qed "stable_invar_1vn";
   11.72 +
   11.73 +goalw thy [MInit_def, invariant_def] "MInit <= invariant 0 UU MM";
   11.74 +by Auto_tac;
   11.75 +qed "MInit_invar_0um";
   11.76 +
   11.77 +goalw thy [MInit_def, invariant_def] "MInit <= invariant 1 VV NN";
   11.78 +by Auto_tac;
   11.79 +qed "MInit_invar_1vn";
   11.80 +
   11.81 +(*The intersection is an invariant of the system*)
   11.82 +goal thy "reachable MInit mutex <= invariant 0 UU MM Int invariant 1 VV NN";
   11.83 +by (simp_tac (simpset() addsimps
   11.84 +	      [strongest_invariant, Int_greatest, stable_Int, 
   11.85 +	       stable_invar_0um, stable_invar_1vn, 
   11.86 +	       MInit_invar_0um,MInit_invar_1vn]) 1); 
   11.87 +qed "reachable_subset_invariant";
   11.88 +
   11.89 +val reachable_subset_invariant' = 
   11.90 +    rewrite_rule [invariant_def] reachable_subset_invariant;
   11.91 +
   11.92 +
   11.93 +(*The safety property (mutual exclusion) follows from the claimed invar_s*)
   11.94 +goalw thy [invariant_def]
   11.95 +    "{s. s MM = 3 & s NN = 3} <= \
   11.96 +\    Compl (invariant 0 UU MM Int invariant 1 VV NN)";
   11.97 +by Auto_tac;
   11.98 +val lemma = result();
   11.99 +
  11.100 +goal thy "{s. s MM = 3 & s NN = 3} <= Compl (reachable MInit mutex)";
  11.101 +by (rtac ([lemma, reachable_subset_invariant RS Compl_anti_mono] MRS subset_trans) 1);
  11.102 +qed "mutual_exclusion";
  11.103 +
  11.104 +
  11.105 +(*The bad invariant FAILS in cmd1v*)
  11.106 +goalw thy [stable_def, bad_invariant_def]
  11.107 +    "stable mutex (bad_invariant 0 UU MM)";
  11.108 +by (constrains_tac 1);
  11.109 +by (trans_tac 1);
  11.110 +by (safe_tac (claset() addSEs [le_SucE]));
  11.111 +by (Asm_full_simp_tac 1);
  11.112 +(*Resulting state: n=1, p=false, m=4, u=false.  
  11.113 +  Execution of cmd1v (the command of process v guarded by n=1) sets p:=true,
  11.114 +  violating the invariant!*)
  11.115 +(*Check that subgoals remain: proof failed.*)
  11.116 +getgoal 1;  
  11.117 +
  11.118 +
  11.119 +(*** Progress for U ***)
  11.120 +
  11.121 +goalw thy [unless_def] "unless mutex {s. s MM=2} {s. s MM=3}";
  11.122 +by (constrains_tac 1);
  11.123 +qed "U_F0";
  11.124 +
  11.125 +goal thy "LeadsTo MInit mutex {s. s MM=1} {s. s PP = s VV & s MM = 2}";
  11.126 +by (rtac leadsTo_imp_LeadsTo 1);   (*makes the proof much faster*)
  11.127 +by (ensures_tac "cmd1u" 1);
  11.128 +qed "U_F1";
  11.129 +
  11.130 +goal thy "LeadsTo MInit mutex {s. s PP = 0 & s MM = 2} {s. s MM = 3}";
  11.131 +by (cut_facts_tac [reachable_subset_invariant'] 1);
  11.132 +by (ensures_tac "cmd2 0 MM" 1);
  11.133 +qed "U_F2";
  11.134 +
  11.135 +goalw thy [mutex_def] "LeadsTo MInit mutex {s. s MM = 3} {s. s PP = 1}";
  11.136 +by (rtac leadsTo_imp_LeadsTo 1); 
  11.137 +by (res_inst_tac [("B", "{s. s MM = 4}")] leadsTo_Trans 1);
  11.138 +by (ensures_tac "cmd4 1 MM" 2);
  11.139 +by (ensures_tac "cmd3 UU MM" 1);
  11.140 +qed "U_F3";
  11.141 +
  11.142 +goal thy "LeadsTo MInit mutex {s. s MM = 2} {s. s PP = 1}";
  11.143 +by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] 
  11.144 +	  MRS LeadsTo_Diff) 1);
  11.145 +by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
  11.146 +by (cut_facts_tac [reachable_subset_boolVars'] 1);
  11.147 +by (auto_tac (claset() addSEs [less_SucE], simpset()));
  11.148 +val lemma2 = result();
  11.149 +
  11.150 +goal thy "LeadsTo MInit mutex {s. s MM = 1} {s. s PP = 1}";
  11.151 +by (rtac ([U_F1 RS LeadsTo_weaken_R, lemma2] MRS LeadsTo_Trans) 1);
  11.152 +by (Blast_tac 1);
  11.153 +val lemma1 = result();
  11.154 +
  11.155 +
  11.156 +goal thy "LeadsTo MInit mutex {s. 1 <= s MM & s MM <= 3} {s. s PP = 1}";
  11.157 +by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL] 
  11.158 +	                addcongs [rev_conj_cong]) 1);
  11.159 +by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
  11.160 +				  lemma1, lemma2, U_F3] ) 1);
  11.161 +val lemma123 = result();
  11.162 +
  11.163 +
  11.164 +(*Misra's F4*)
  11.165 +goal thy "LeadsTo MInit mutex {s. s UU = 1} {s. s PP = 1}";
  11.166 +by (rtac LeadsTo_weaken_L 1);
  11.167 +by (rtac lemma123 1);
  11.168 +by (cut_facts_tac [reachable_subset_invariant'] 1);
  11.169 +by Auto_tac;
  11.170 +qed "u_leadsto_p";
  11.171 +
  11.172 +
  11.173 +(*** Progress for V ***)
  11.174 +
  11.175 +
  11.176 +goalw thy [unless_def] "unless mutex {s. s NN=2} {s. s NN=3}";
  11.177 +by (constrains_tac 1);
  11.178 +qed "V_F0";
  11.179 +
  11.180 +goal thy "LeadsTo MInit mutex {s. s NN=1} {s. s PP = 1 - s UU & s NN = 2}";
  11.181 +by (rtac leadsTo_imp_LeadsTo 1);   (*makes the proof much faster*)
  11.182 +by (ensures_tac "cmd1v" 1);
  11.183 +qed "V_F1";
  11.184 +
  11.185 +goal thy "LeadsTo MInit mutex {s. s PP = 1 & s NN = 2} {s. s NN = 3}";
  11.186 +by (cut_facts_tac [reachable_subset_invariant'] 1);
  11.187 +by (ensures_tac "cmd2 1 NN" 1);
  11.188 +qed "V_F2";
  11.189 +
  11.190 +goalw thy [mutex_def] "LeadsTo MInit mutex {s. s NN = 3} {s. s PP = 0}";
  11.191 +by (rtac leadsTo_imp_LeadsTo 1); 
  11.192 +by (res_inst_tac [("B", "{s. s NN = 4}")] leadsTo_Trans 1);
  11.193 +by (ensures_tac "cmd4 0 NN" 2);
  11.194 +by (ensures_tac "cmd3 VV NN" 1);
  11.195 +qed "V_F3";
  11.196 +
  11.197 +goal thy "LeadsTo MInit mutex {s. s NN = 2} {s. s PP = 0}";
  11.198 +by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] 
  11.199 +	  MRS LeadsTo_Diff) 1);
  11.200 +by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
  11.201 +by (cut_facts_tac [reachable_subset_boolVars'] 1);
  11.202 +by (auto_tac (claset() addSEs [less_SucE], simpset()));
  11.203 +val lemma2 = result();
  11.204 +
  11.205 +goal thy "LeadsTo MInit mutex {s. s NN = 1} {s. s PP = 0}";
  11.206 +by (rtac ([V_F1 RS LeadsTo_weaken_R, lemma2] MRS LeadsTo_Trans) 1);
  11.207 +by (Blast_tac 1);
  11.208 +val lemma1 = result();
  11.209 +
  11.210 +
  11.211 +goal thy "LeadsTo MInit mutex {s. 1 <= s NN & s NN <= 3} {s. s PP = 0}";
  11.212 +by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL] 
  11.213 +	                addcongs [rev_conj_cong]) 1);
  11.214 +by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
  11.215 +				  lemma1, lemma2, V_F3] ) 1);
  11.216 +val lemma123 = result();
  11.217 +
  11.218 +
  11.219 +(*Misra's F4*)
  11.220 +goal thy "LeadsTo MInit mutex {s. s VV = 1} {s. s PP = 0}";
  11.221 +by (rtac LeadsTo_weaken_L 1);
  11.222 +by (rtac lemma123 1);
  11.223 +by (cut_facts_tac [reachable_subset_invariant'] 1);
  11.224 +by Auto_tac;
  11.225 +qed "v_leadsto_not_p";
  11.226 +
  11.227 +
  11.228 +(** Absence of starvation **)
  11.229 +
  11.230 +(*Misra's F6*)
  11.231 +goal thy "LeadsTo MInit mutex {s. s MM = 1} {s. s MM = 3}";
  11.232 +by (rtac LeadsTo_Un_duplicate 1);
  11.233 +by (rtac LeadsTo_cancel2 1);
  11.234 +by (rtac U_F2 2);
  11.235 +by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
  11.236 +by (stac Un_commute 1);
  11.237 +by (rtac LeadsTo_Un_duplicate 1);
  11.238 +by (rtac ([v_leadsto_not_p, U_F0] MRS R_PSP_unless  RSN(2, LeadsTo_cancel2)) 1);
  11.239 +by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
  11.240 +by (cut_facts_tac [reachable_subset_boolVars'] 1);
  11.241 +by (auto_tac (claset() addSEs [less_SucE], simpset()));
  11.242 +qed "m1_leadsto_3";
  11.243 +
  11.244 +
  11.245 +(*The same for V*)
  11.246 +goal thy "LeadsTo MInit mutex {s. s NN = 1} {s. s NN = 3}";
  11.247 +by (rtac LeadsTo_Un_duplicate 1);
  11.248 +by (rtac LeadsTo_cancel2 1);
  11.249 +by (rtac V_F2 2);
  11.250 +by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
  11.251 +by (stac Un_commute 1);
  11.252 +by (rtac LeadsTo_Un_duplicate 1);
  11.253 +by (rtac ([u_leadsto_p, V_F0] MRS R_PSP_unless  RSN(2, LeadsTo_cancel2)) 1);
  11.254 +by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
  11.255 +by (cut_facts_tac [reachable_subset_boolVars'] 1);
  11.256 +by (auto_tac (claset() addSEs [less_SucE], simpset()));
  11.257 +qed "n1_leadsto_3";
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/UNITY/Mutex.thy	Fri Apr 03 12:34:33 1998 +0200
    12.3 @@ -0,0 +1,74 @@
    12.4 +(*  Title:      HOL/UNITY/Mutex.thy
    12.5 +    ID:         $Id$
    12.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    12.7 +    Copyright   1998  University of Cambridge
    12.8 +
    12.9 +Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
   12.10 +*)
   12.11 +
   12.12 +Mutex = Update + UNITY + Traces + SubstAx +
   12.13 +
   12.14 +(*WE NEED A GENERAL TREATMENT OF NUMBERS!!*)
   12.15 +syntax
   12.16 +  "3"       :: nat                ("3")
   12.17 +  "4"       :: nat                ("4")
   12.18 +
   12.19 +translations
   12.20 +   "3"  == "Suc 2"
   12.21 +   "4"  == "Suc 3"
   12.22 +
   12.23 +
   12.24 +(*program variables*)
   12.25 +datatype pvar = PP | MM | NN | UU | VV
   12.26 +
   12.27 +(*No booleans; instead True=1 and False=0*)
   12.28 +types state = pvar => nat
   12.29 +
   12.30 +constdefs
   12.31 +  cmd0 :: "[pvar,pvar] => (state*state) set"
   12.32 +    "cmd0 u m == {(s,s'). s' = s[u|->1][m|->1] & s m = 0}"
   12.33 +
   12.34 +  cmd1u :: "(state*state) set"
   12.35 +    "cmd1u == {(s,s'). s' = s[PP|-> s VV][MM|->2] & s MM = 1}"
   12.36 +
   12.37 +  cmd1v :: "(state*state) set"
   12.38 +    "cmd1v == {(s,s'). s' = s[PP|-> 1 - s UU][NN|->2] & s NN = 1}"
   12.39 +
   12.40 +  (*Put pv=0 for u's program and pv=1 for v's program*)
   12.41 +  cmd2 :: "[nat,pvar] => (state*state) set"
   12.42 +    "cmd2 pv m == {(s,s'). s' = s[m|->3] & s PP = pv & s m = 2}"
   12.43 +
   12.44 +  cmd3 :: "[pvar,pvar] => (state*state) set"
   12.45 +    "cmd3 u m == {(s,s'). s' = s[u|->0][m|->4] & s m = 3}"
   12.46 +
   12.47 +  (*Put pv=1 for u's program and pv=0 for v's program*)
   12.48 +  cmd4 :: "[nat,pvar] => (state*state) set"
   12.49 +    "cmd4 pv m == {(s,s'). s' = s[PP|->pv][m|->0] & s m = 4}"
   12.50 +
   12.51 +  mutex :: "(state*state) set set"
   12.52 +    "mutex == {id,
   12.53 +	       cmd0 UU MM, cmd0 VV NN,
   12.54 +	       cmd1u, cmd1v,
   12.55 +	       cmd2 0 MM, cmd2 1 NN,
   12.56 +	       cmd3 UU MM, cmd3 VV NN,
   12.57 +	       cmd4 1 MM, cmd4 0 NN}"
   12.58 +
   12.59 +  MInit :: "state set"
   12.60 +    "MInit == {s. s PP < 2 & s UU = 0 & s VV = 0 & s MM = 0 & s NN = 0}"
   12.61 +
   12.62 +  boolVars :: "state set"
   12.63 +    "boolVars == {s. s PP<2 & s UU < 2 & s VV < 2}"
   12.64 +
   12.65 +  (*Put pv=0 for u's program and pv=1 for v's program*)
   12.66 +  invariant :: "[nat,pvar,pvar] => state set"
   12.67 +    "invariant pv u m == {s. ((s u=1) = (1 <= s m & s m <= 3)) &
   12.68 +			     (s m = 3 --> s PP = pv)}"
   12.69 +
   12.70 +  bad_invariant :: "[nat,pvar,pvar] => state set"
   12.71 +    "bad_invariant pv u m == {s. ((s u=1) = (1 <= s m & s m <= 3)) &
   12.72 +			         (3 <= s m & s m <= 4 --> s PP = pv)}"
   12.73 +
   12.74 +
   12.75 +  
   12.76 +
   12.77 +end
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/UNITY/Network.ML	Fri Apr 03 12:34:33 1998 +0200
    13.3 @@ -0,0 +1,61 @@
    13.4 +(*  Title:      HOL/UNITY/Network
    13.5 +    ID:         $Id$
    13.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    13.7 +    Copyright   1998  University of Cambridge
    13.8 +
    13.9 +The Communication Network
   13.10 +
   13.11 +From Misra, "A Logic for Concurrent Programming" (1994), section 5.7
   13.12 +*)
   13.13 +
   13.14 +open Network;
   13.15 +
   13.16 +val [rsA, rsB, sent_nondec, rcvd_nondec, rcvd_idle, sent_idle] = 
   13.17 +goalw thy [stable_def]
   13.18 +   "[| !! m. stable Acts {s. s(Bproc,Rcvd) <= s(Aproc,Sent)};  \
   13.19 +\      !! m. stable Acts {s. s(Aproc,Rcvd) <= s(Bproc,Sent)};  \
   13.20 +\      !! m proc. stable Acts {s. m <= s(proc,Sent)};  \
   13.21 +\      !! n proc. stable Acts {s. n <= s(proc,Rcvd)};  \
   13.22 +\      !! m proc. constrains Acts {s. s(proc,Idle) = 1 & s(proc,Rcvd) = m} \
   13.23 +\                                 {s. s(proc,Rcvd) = m --> s(proc,Idle) = 1}; \
   13.24 +\      !! n proc. constrains Acts {s. s(proc,Idle) = 1 & s(proc,Sent) = n} \
   13.25 +\                                 {s. s(proc,Sent) = n} \
   13.26 +\   |] ==> stable Acts {s. s(Aproc,Idle) = 1 & s(Bproc,Idle) = 1 & \
   13.27 +\                         s(Aproc,Sent) = s(Bproc,Rcvd) & \
   13.28 +\                         s(Bproc,Sent) = s(Aproc,Rcvd) & \
   13.29 +\                         s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}";
   13.30 +
   13.31 +val sent_nondec_A = read_instantiate [("proc","Aproc")] sent_nondec;
   13.32 +val sent_nondec_B = read_instantiate [("proc","Bproc")] sent_nondec;
   13.33 +val rcvd_nondec_A = read_instantiate [("proc","Aproc")] rcvd_nondec;
   13.34 +val rcvd_nondec_B = read_instantiate [("proc","Bproc")] rcvd_nondec;
   13.35 +val rcvd_idle_A = read_instantiate [("proc","Aproc")] rcvd_idle;
   13.36 +val rcvd_idle_B = read_instantiate [("proc","Bproc")] rcvd_idle;
   13.37 +val sent_idle_A = read_instantiate [("proc","Aproc")] sent_idle;
   13.38 +val sent_idle_B = read_instantiate [("proc","Bproc")] sent_idle;
   13.39 +
   13.40 +val rs_AB = [rsA, rsB] MRS constrains_Int;
   13.41 +val sent_nondec_AB = [sent_nondec_A, sent_nondec_B] MRS constrains_Int;
   13.42 +val rcvd_nondec_AB = [rcvd_nondec_A, rcvd_nondec_B] MRS constrains_Int;
   13.43 +val rcvd_idle_AB = [rcvd_idle_A, rcvd_idle_B] MRS constrains_Int;
   13.44 +val sent_idle_AB = [sent_idle_A, sent_idle_B] MRS constrains_Int;
   13.45 +val nondec_AB = [sent_nondec_AB, rcvd_nondec_AB] MRS constrains_Int;
   13.46 +val idle_AB = [rcvd_idle_AB, sent_idle_AB] MRS constrains_Int;
   13.47 +val nondec_idle = [nondec_AB, idle_AB] MRS constrains_Int;
   13.48 +
   13.49 +by (rtac constrainsI 1);
   13.50 +by (dtac ([rs_AB, nondec_idle] MRS constrains_Int RS constrainsD) 1);
   13.51 +by (assume_tac 1);
   13.52 +by (ALLGOALS Asm_full_simp_tac);
   13.53 +by (Blast_tac 1);
   13.54 +by (Clarify_tac 1);
   13.55 +by (subgoals_tac ["s' (Aproc, Rcvd) = s (Aproc, Rcvd)",
   13.56 +		  "s' (Bproc, Rcvd) = s (Bproc, Rcvd)"] 1);
   13.57 +by (REPEAT (blast_tac (claset() addIs [le_anti_sym, le_trans, eq_imp_le]) 2));
   13.58 +
   13.59 +by (Asm_simp_tac 1);
   13.60 +result();
   13.61 +
   13.62 +
   13.63 +
   13.64 +
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/UNITY/Network.thy	Fri Apr 03 12:34:33 1998 +0200
    14.3 @@ -0,0 +1,9 @@
    14.4 +Network = UNITY +
    14.5 +
    14.6 +datatype pvar = Sent | Rcvd | Idle
    14.7 +
    14.8 +datatype pname = Aproc | Bproc
    14.9 +
   14.10 +types state = "pname * pvar => nat"
   14.11 +
   14.12 +end
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/UNITY/README.html	Fri Apr 03 12:34:33 1998 +0200
    15.3 @@ -0,0 +1,51 @@
    15.4 +<!-- $Id$ -->
    15.5 +<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
    15.6 +
    15.7 +<H2>UNITY--Chandy and Misra's UNITY formalism</H2>
    15.8 +
    15.9 +<P>The book <EM>Parallel Program Design: A Foundation</EM> by Chandy and Misra
   15.10 +(Addison-Wesley, 1988) presents UNITY, which consists of an abstract
   15.11 +programming language of guarded assignments and an associated calculus.
   15.12 +Misra's 1994 paper "A Logic for Concurrent Programming" presents "New UNITY",
   15.13 +giving more elegant foundations for a more general class of languages.
   15.14 +
   15.15 +<P> This directory is a preliminary formalization of New UNITY.  The Isabelle
   15.16 +examples may not represent the most natural treatment of UNITY style.  Hand
   15.17 +UNITY proofs tend to be written in the forwards direction, as in informal
   15.18 +mathematics, while Isabelle works best in a backwards (goal-directed) style.
   15.19 +
   15.20 +<P>
   15.21 +The syntax, also, is rather unnatural.   Programs are expressed as sets of 
   15.22 +commands, where each command is a relation on states.  Quantification over 
   15.23 +commands using [] is easily expressed.  At present, there are no examples of
   15.24 +quantification using ||.
   15.25 +
   15.26 +<P>
   15.27 +The directory presents a few small examples, mostly taken from Misra's 1994
   15.28 +paper:
   15.29 +<UL>
   15.30 +<LI>common meeting time
   15.31 +
   15.32 +<LI>the token ring
   15.33 +
   15.34 +<LI>the communication network
   15.35 +
   15.36 +<LI><EM>n</EM>-process deadlock
   15.37 +
   15.38 +<LI>unordered channel
   15.39 +
   15.40 +<LI>reachability in directed graphs (section 6.4 of the book)
   15.41 +</UL>
   15.42 +
   15.43 +<P> Safety proofs (invariants) are often proved automatically.  Progress
   15.44 +proofs involving ENSURES can sometimes be proved automatically.  The
   15.45 +level of automation appears to be about the same as in HOL-UNITY by Flemming
   15.46 +Andersen et al.
   15.47 +
   15.48 +<HR>
   15.49 +<P>Last modified on $Date$
   15.50 +
   15.51 +<ADDRESS>
   15.52 +<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
   15.53 +</ADDRESS>
   15.54 +</BODY></HTML>
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/HOL/UNITY/ROOT.ML	Fri Apr 03 12:34:33 1998 +0200
    16.3 @@ -0,0 +1,21 @@
    16.4 +(*  Title:      HOL/UNITY/ROOT
    16.5 +    ID:         $Id$
    16.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    16.7 +    Copyright   1998  University of Cambridge
    16.8 +
    16.9 +Root file for UNITY proofs.
   16.10 +*)
   16.11 +
   16.12 +HOL_build_completed;    (*Make examples fail if HOL did*)
   16.13 +
   16.14 +writeln"Root file for HOL/UNITY";
   16.15 +set proof_timing;
   16.16 +time_use_thy "Deadlock";
   16.17 +time_use_thy "WFair";
   16.18 +time_use_thy "Common";
   16.19 +time_use_thy "Network";
   16.20 +time_use_thy "Token";
   16.21 +time_use_thy "Channel";
   16.22 +time_use_thy "Mutex";
   16.23 +time_use_thy "FP";
   16.24 +time_use_thy "Reach";
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/HOL/UNITY/Reach.ML	Fri Apr 03 12:34:33 1998 +0200
    17.3 @@ -0,0 +1,188 @@
    17.4 +(*  Title:      HOL/UNITY/Reach.thy
    17.5 +    ID:         $Id$
    17.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    17.7 +    Copyright   1998  University of Cambridge
    17.8 +
    17.9 +Reachability in Directed Graphs.  From Chandy and Misra, section 6.4.
   17.10 +*)
   17.11 +
   17.12 +open Reach;
   17.13 +
   17.14 +(*TO SIMPDATA.ML??  FOR CLASET??  *)
   17.15 +val major::prems = goal thy 
   17.16 +    "[| if P then Q else R;    \
   17.17 +\       [| P;   Q |] ==> S;    \
   17.18 +\       [| ~ P; R |] ==> S |] ==> S";
   17.19 +by (cut_facts_tac [major] 1);
   17.20 +by (blast_tac (claset() addSDs [if_bool_eq_disj RS iffD1] addIs prems) 1);
   17.21 +qed "ifE";
   17.22 +
   17.23 +AddSEs [ifE];
   17.24 +
   17.25 +
   17.26 +val cmd_defs = [racts_def, asgt_def, update_def];
   17.27 +
   17.28 +goalw thy [racts_def] "id : racts";
   17.29 +by (Simp_tac 1);
   17.30 +qed "id_in_racts";
   17.31 +AddIffs [id_in_racts];
   17.32 +
   17.33 +(*All vertex sets are finite*)
   17.34 +AddIffs [[subset_UNIV, finite_graph] MRS finite_subset];
   17.35 +
   17.36 +
   17.37 +(** Constrains/Ensures tactics: NEED TO BE GENERALIZED OVER ALL PROGRAMS **)
   17.38 +
   17.39 +(*proves "constrains" properties when the program is specified*)
   17.40 +val constrains_tac = 
   17.41 +   SELECT_GOAL
   17.42 +      (EVERY [rtac constrainsI 1,
   17.43 +	      rewtac racts_def,
   17.44 +	      REPEAT_FIRST (eresolve_tac [insertE, emptyE]),
   17.45 +	      rewrite_goals_tac [racts_def, asgt_def],
   17.46 +	      ALLGOALS (SELECT_GOAL Auto_tac)]);
   17.47 +
   17.48 +
   17.49 +(*proves "ensures" properties when the program is specified*)
   17.50 +fun ensures_tac sact = 
   17.51 +    SELECT_GOAL
   17.52 +      (EVERY [REPEAT (resolve_tac [LeadsTo_Basis, leadsTo_Basis, ensuresI] 1),
   17.53 +	      res_inst_tac [("act", sact)] transient_mem 2,
   17.54 +	      Simp_tac 2,
   17.55 +	      constrains_tac 1,
   17.56 +	      rewrite_goals_tac [racts_def, asgt_def],
   17.57 +	      Auto_tac]);
   17.58 +
   17.59 +
   17.60 +goalw thy [stable_def, invariant_def]
   17.61 +    "stable racts invariant";
   17.62 +by (constrains_tac 1);
   17.63 +by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
   17.64 +qed "stable_invariant";
   17.65 +
   17.66 +goalw thy [rinit_def, invariant_def] "rinit <= invariant";
   17.67 +by Auto_tac;
   17.68 +qed "rinit_invariant";
   17.69 +
   17.70 +goal thy "reachable rinit racts <= invariant";
   17.71 +by (simp_tac (simpset() addsimps
   17.72 +	      [strongest_invariant, stable_invariant, rinit_invariant]) 1); 
   17.73 +qed "reachable_subset_invariant";
   17.74 +
   17.75 +val reachable_subset_invariant' = 
   17.76 +    rewrite_rule [invariant_def] reachable_subset_invariant;
   17.77 +
   17.78 +
   17.79 +(*** Fixedpoint ***)
   17.80 +
   17.81 +(*If it reaches a fixedpoint, it has found a solution*)
   17.82 +goalw thy [fixedpoint_def, invariant_def]
   17.83 +    "fixedpoint Int invariant = { %v. (init, v) : edges^* }";
   17.84 +by (rtac equalityI 1);
   17.85 +by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 2);
   17.86 +by (auto_tac (claset() addSIs [ext], simpset()));
   17.87 +by (etac rtrancl_induct 1);
   17.88 +by Auto_tac;
   17.89 +qed "fixedpoint_invariant_correct";
   17.90 +
   17.91 +goalw thy (cmd_defs @ [FP_def, fixedpoint_def, stable_def, constrains_def])
   17.92 +    "FP racts <= fixedpoint";
   17.93 +by Auto_tac;
   17.94 +by (dtac bspec 1); 
   17.95 +by (Blast_tac 1);
   17.96 +by (asm_full_simp_tac (simpset() addsimps [Image_singleton, image_iff]) 1);
   17.97 +by (dtac fun_cong 1);
   17.98 +by Auto_tac;
   17.99 +val lemma1 = result();
  17.100 +
  17.101 +goalw thy (cmd_defs @ [FP_def, fixedpoint_def, stable_def, constrains_def])
  17.102 +    "fixedpoint <= FP racts";
  17.103 +by (auto_tac (claset() addIs [ext], simpset()));
  17.104 +val lemma2 = result();
  17.105 +
  17.106 +goal thy "FP racts = fixedpoint";
  17.107 +by (rtac ([lemma1,lemma2] MRS equalityI) 1);
  17.108 +qed "FP_fixedpoint";
  17.109 +
  17.110 +
  17.111 +(*If we haven't reached a fixedpoint then there is some edge for which u but
  17.112 +  not v holds.  Progress will be proved via an ENSURES assertion that the
  17.113 +  metric will decrease for each suitable edge.  A union over all edges proves
  17.114 +  a LEADSTO assertion that the metric decreases if we are not at a fixedpoint.
  17.115 +  *)
  17.116 +
  17.117 +goal thy "Compl fixedpoint = (UN (u,v): edges. {s. s u & ~ s v})";
  17.118 +by (simp_tac (simpset() addsimps
  17.119 +	      ([Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym, 
  17.120 +		racts_def, asgt_def])) 1);
  17.121 +by Safe_tac;
  17.122 +by (rtac update_idem 1);
  17.123 +by (Blast_tac 1);
  17.124 +by (Full_simp_tac 1);
  17.125 +by (REPEAT (dtac bspec 1 THEN Simp_tac 1));
  17.126 +by (dtac subsetD 1);
  17.127 +by (Simp_tac 1);
  17.128 +by (asm_full_simp_tac (simpset() addsimps [update_idem_iff]) 1);
  17.129 +qed "Compl_fixedpoint";
  17.130 +
  17.131 +goal thy "A - fixedpoint = (UN (u,v): edges. A Int {s. s u & ~ s v})";
  17.132 +by (simp_tac (simpset() addsimps [Diff_eq, Compl_fixedpoint]) 1);
  17.133 +by (Blast_tac 1);
  17.134 +qed "Diff_fixedpoint";
  17.135 +
  17.136 +
  17.137 +(*** Progress ***)
  17.138 +
  17.139 +goalw thy [metric_def] "!!s. ~ s x ==> Suc (metric (s[x|->True])) = metric s";
  17.140 +by (subgoal_tac "{v. ~ (s[x|->True]) v} = {v. ~ s v} - {x}" 1);
  17.141 +by Auto_tac;
  17.142 +by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1);
  17.143 +qed "Suc_metric";
  17.144 +
  17.145 +goal thy "!!s. ~ s x ==> metric (s[x|->True]) < metric s";
  17.146 +by (etac (Suc_metric RS subst) 1);
  17.147 +by (Blast_tac 1);
  17.148 +qed "metric_less";
  17.149 +AddSIs [metric_less];
  17.150 +
  17.151 +goal thy "metric (s[y|->s x | s y]) <= metric s";
  17.152 +by (case_tac "s x --> s y" 1);
  17.153 +by (auto_tac (claset() addIs [less_imp_le],
  17.154 +	      simpset() addsimps [update_idem]));
  17.155 +qed "metric_le";
  17.156 +
  17.157 +goal thy "!!m. (u,v): edges ==> \
  17.158 +\              ensures racts ((metric-``{m}) Int {s. s u & ~ s v})  \
  17.159 +\                            (metric-``(lessThan m))";
  17.160 +by (ensures_tac "asgt u v" 1);
  17.161 +by (cut_facts_tac [metric_le] 1);
  17.162 +by (fast_tac (claset() addSDs [le_imp_less_or_eq]) 1);
  17.163 +qed "edges_ensures";
  17.164 +
  17.165 +goal thy "leadsTo racts ((metric-``{m}) - fixedpoint) (metric-``(lessThan m))";
  17.166 +by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1);
  17.167 +by (rtac leadsTo_UN 1);
  17.168 +by (split_all_tac 1);
  17.169 +by (asm_simp_tac (simpset() addsimps [edges_ensures RS leadsTo_Basis]) 1);
  17.170 +qed "leadsTo_Diff_fixedpoint";
  17.171 +
  17.172 +goal thy "leadsTo racts (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)";
  17.173 +by (rtac (leadsTo_Diff_fixedpoint RS leadsTo_weaken_R RS leadsTo_Diff) 1);
  17.174 +by (ALLGOALS (blast_tac (claset() addIs [subset_imp_leadsTo])));
  17.175 +qed "leadsTo_Un_fixedpoint";
  17.176 +
  17.177 +
  17.178 +(*Execution in any state leads to a fixedpoint (i.e. can terminate)*)
  17.179 +goal thy "leadsTo racts UNIV fixedpoint";
  17.180 +by (rtac lessThan_induct 1);
  17.181 +by Auto_tac;
  17.182 +by (rtac leadsTo_Un_fixedpoint 1);
  17.183 +qed "leadsTo_fixedpoint";
  17.184 +
  17.185 +goal thy "LeadsTo rinit racts UNIV { %v. (init, v) : edges^* }";
  17.186 +by (stac (fixedpoint_invariant_correct RS sym) 1);
  17.187 +by (rtac (leadsTo_fixedpoint RS leadsTo_imp_LeadsTo RS LeadsTo_weaken_R) 1); 
  17.188 +by (cut_facts_tac [reachable_subset_invariant] 1);
  17.189 +by (Blast_tac 1);
  17.190 +qed "LeadsTo_correct";
  17.191 +
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/src/HOL/UNITY/Reach.thy	Fri Apr 03 12:34:33 1998 +0200
    18.3 @@ -0,0 +1,46 @@
    18.4 +(*  Title:      HOL/UNITY/Reach.thy
    18.5 +    ID:         $Id$
    18.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    18.7 +    Copyright   1998  University of Cambridge
    18.8 +
    18.9 +Reachability in Directed Graphs.  From Chandy and Misra, section 6.4.
   18.10 +*)
   18.11 +
   18.12 +Reach = Update + FP + Traces + SubstAx +
   18.13 +
   18.14 +types   vertex
   18.15 +        state = "vertex=>bool"
   18.16 +
   18.17 +arities vertex :: term
   18.18 +
   18.19 +consts
   18.20 +  init ::  "vertex"
   18.21 +
   18.22 +  edges :: "(vertex*vertex) set"
   18.23 +
   18.24 +constdefs
   18.25 +
   18.26 +  asgt  :: "[vertex,vertex] => (state*state) set"
   18.27 +    "asgt u v == {(s,s'). s' = s[v|-> s u | s v]}"
   18.28 +
   18.29 +  racts :: "(state*state) set set"
   18.30 +    "racts == insert id (UN (u,v): edges. {asgt u v})"
   18.31 +
   18.32 +  rinit :: "state set"
   18.33 +    "rinit == {%v. v=init}"
   18.34 +
   18.35 +  invariant :: state set
   18.36 +    "invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}"
   18.37 +
   18.38 +  fixedpoint :: state set
   18.39 +    "fixedpoint == {s. ALL (u,v): edges. s u --> s v}"
   18.40 +
   18.41 +  metric :: state => nat
   18.42 +    "metric == (%s. card {v. ~ s v})"
   18.43 +
   18.44 +rules
   18.45 +
   18.46 +  (*We assume that the set of vertices is finite*)
   18.47 +  finite_graph "finite (UNIV :: vertex set)"
   18.48 +  
   18.49 +end
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/src/HOL/UNITY/SubstAx.ML	Fri Apr 03 12:34:33 1998 +0200
    19.3 @@ -0,0 +1,405 @@
    19.4 +(*  Title:      HOL/UNITY/SubstAx
    19.5 +    ID:         $Id$
    19.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    19.7 +    Copyright   1998  University of Cambridge
    19.8 +
    19.9 +Weak Fairness versions of transient, ensures, LeadsTo.
   19.10 +
   19.11 +From Misra, "A Logic for Concurrent Programming", 1994
   19.12 +*)
   19.13 +
   19.14 +open SubstAx;
   19.15 +
   19.16 +(*constrains Acts B B' ==> constrains Acts (reachable Init Acts Int B)
   19.17 +                                           (reachable Init Acts Int B') *)
   19.18 +bind_thm ("constrains_reachable",
   19.19 +	  rewrite_rule [stable_def] stable_reachable RS constrains_Int);
   19.20 +
   19.21 +
   19.22 +(*** Introduction rules: Basis, Trans, Union ***)
   19.23 +
   19.24 +goalw thy [LeadsTo_def]
   19.25 +    "!!Acts. leadsTo Acts A B ==> LeadsTo Init Acts A B";
   19.26 +by (blast_tac (claset() addIs [PSP_stable2, stable_reachable]) 1);
   19.27 +qed "leadsTo_imp_LeadsTo";
   19.28 +
   19.29 +goalw thy [LeadsTo_def]
   19.30 +    "!!Acts. [| constrains Acts (reachable Init Acts Int (A - A'))   \
   19.31 +\                               (A Un A'); \
   19.32 +\               transient  Acts (reachable Init Acts Int (A-A')) |]   \
   19.33 +\           ==> LeadsTo Init Acts A A'";
   19.34 +by (rtac (stable_reachable RS stable_ensures_Int RS leadsTo_Basis) 1);
   19.35 +by (assume_tac 2);
   19.36 +by (asm_simp_tac 
   19.37 +    (simpset() addsimps [Int_Un_distrib RS sym, Diff_Int_distrib RS sym,
   19.38 +			 stable_constrains_Int]) 1);
   19.39 +qed "LeadsTo_Basis";
   19.40 +
   19.41 +goalw thy [LeadsTo_def]
   19.42 +    "!!Acts. [| LeadsTo Init Acts A B;  LeadsTo Init Acts B C |] \
   19.43 +\            ==> LeadsTo Init Acts A C";
   19.44 +by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
   19.45 +qed "LeadsTo_Trans";
   19.46 +
   19.47 +val prems = goalw thy [LeadsTo_def]
   19.48 + "(!!A. A : S ==> LeadsTo Init Acts A B) ==> LeadsTo Init Acts (Union S) B";
   19.49 +by (stac Int_Union 1);
   19.50 +by (blast_tac (claset() addIs (leadsTo_UN::prems)) 1);
   19.51 +qed "LeadsTo_Union";
   19.52 +
   19.53 +
   19.54 +(*** Derived rules ***)
   19.55 +
   19.56 +goal thy "!!Acts. id: Acts ==> LeadsTo Init Acts A UNIV";
   19.57 +by (asm_simp_tac (simpset() addsimps [LeadsTo_def, 
   19.58 +				      Int_lower1 RS subset_imp_leadsTo]) 1);
   19.59 +qed "LeadsTo_UNIV";
   19.60 +Addsimps [LeadsTo_UNIV];
   19.61 +
   19.62 +(*Useful with cancellation, disjunction*)
   19.63 +goal thy "!!Acts. LeadsTo Init Acts A (A' Un A') ==> LeadsTo Init Acts A A'";
   19.64 +by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
   19.65 +qed "LeadsTo_Un_duplicate";
   19.66 +
   19.67 +goal thy "!!Acts. LeadsTo Init Acts A (A' Un C Un C) ==> LeadsTo Init Acts A (A' Un C)";
   19.68 +by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
   19.69 +qed "LeadsTo_Un_duplicate2";
   19.70 +
   19.71 +val prems = goal thy
   19.72 +   "(!!i. i : I ==> LeadsTo Init Acts (A i) B) \
   19.73 +\   ==> LeadsTo Init Acts (UN i:I. A i) B";
   19.74 +by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
   19.75 +by (blast_tac (claset() addIs (LeadsTo_Union::prems)) 1);
   19.76 +qed "LeadsTo_UN";
   19.77 +
   19.78 +(*Binary union introduction rule*)
   19.79 +goal thy
   19.80 +  "!!C. [| LeadsTo Init Acts A C; LeadsTo Init Acts B C |] ==> LeadsTo Init Acts (A Un B) C";
   19.81 +by (stac Un_eq_Union 1);
   19.82 +by (blast_tac (claset() addIs [LeadsTo_Union]) 1);
   19.83 +qed "LeadsTo_Un";
   19.84 +
   19.85 +
   19.86 +goalw thy [LeadsTo_def]
   19.87 +    "!!A B. [| reachable Init Acts Int A <= B;  id: Acts |] \
   19.88 +\           ==> LeadsTo Init Acts A B";
   19.89 +by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
   19.90 +qed "Int_subset_imp_LeadsTo";
   19.91 +
   19.92 +goalw thy [LeadsTo_def]
   19.93 +    "!!A B. [| A <= B;  id: Acts |] \
   19.94 +\           ==> LeadsTo Init Acts A B";
   19.95 +by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
   19.96 +qed "subset_imp_LeadsTo";
   19.97 +
   19.98 +bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo);
   19.99 +Addsimps [empty_LeadsTo];
  19.100 +
  19.101 +goal thy
  19.102 +    "!!A B. [| reachable Init Acts Int A = {};  id: Acts |] \
  19.103 +\           ==> LeadsTo Init Acts A B";
  19.104 +by (asm_simp_tac (simpset() addsimps [Int_subset_imp_LeadsTo]) 1);
  19.105 +qed "Int_empty_LeadsTo";
  19.106 +
  19.107 +
  19.108 +goalw thy [LeadsTo_def]
  19.109 +    "!!Acts. [| LeadsTo Init Acts A A';   \
  19.110 +\               reachable Init Acts Int A' <= B' |] \
  19.111 +\            ==> LeadsTo Init Acts A B'";
  19.112 +by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1);
  19.113 +qed_spec_mp "LeadsTo_weaken_R";
  19.114 +
  19.115 +
  19.116 +goalw thy [LeadsTo_def]
  19.117 +    "!!Acts. [| LeadsTo Init Acts A A'; \
  19.118 +     \               reachable Init Acts Int B <= A; id: Acts |]  \
  19.119 +\            ==> LeadsTo Init Acts B A'";
  19.120 +by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
  19.121 +qed_spec_mp "LeadsTo_weaken_L";
  19.122 +
  19.123 +
  19.124 +(*Distributes over binary unions*)
  19.125 +goal thy
  19.126 +  "!!C. id: Acts ==> \
  19.127 +\       LeadsTo Init Acts (A Un B) C  =  \
  19.128 +\       (LeadsTo Init Acts A C & LeadsTo Init Acts B C)";
  19.129 +by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
  19.130 +qed "LeadsTo_Un_distrib";
  19.131 +
  19.132 +goal thy
  19.133 +  "!!C. id: Acts ==> \
  19.134 +\       LeadsTo Init Acts (UN i:I. A i) B  =  \
  19.135 +\       (ALL i : I. LeadsTo Init Acts (A i) B)";
  19.136 +by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
  19.137 +qed "LeadsTo_UN_distrib";
  19.138 +
  19.139 +goal thy
  19.140 +  "!!C. id: Acts ==> \
  19.141 +\       LeadsTo Init Acts (Union S) B  =  \
  19.142 +\       (ALL A : S. LeadsTo Init Acts A B)";
  19.143 +by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1);
  19.144 +qed "LeadsTo_Union_distrib";
  19.145 +
  19.146 +
  19.147 +goal thy 
  19.148 +   "!!Acts. [| LeadsTo Init Acts A A'; id: Acts;   \
  19.149 +\               reachable Init Acts Int B  <= A;     \
  19.150 +\               reachable Init Acts Int A' <= B' |] \
  19.151 +\           ==> LeadsTo Init Acts B B'";
  19.152 +(*PROOF FAILED: why?*)
  19.153 +by (blast_tac (claset() addIs [LeadsTo_Trans, LeadsTo_weaken_R,
  19.154 +			       LeadsTo_weaken_L]) 1);
  19.155 +qed "LeadsTo_weaken";
  19.156 +
  19.157 +
  19.158 +(*Set difference: maybe combine with leadsTo_weaken_L??*)
  19.159 +goal thy
  19.160 +  "!!C. [| LeadsTo Init Acts (A-B) C; LeadsTo Init Acts B C; id: Acts |] \
  19.161 +\       ==> LeadsTo Init Acts A C";
  19.162 +by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
  19.163 +qed "LeadsTo_Diff";
  19.164 +
  19.165 +
  19.166 +(** Meta or object quantifier ???????????????????
  19.167 +    see ball_constrains_UN in UNITY.ML***)
  19.168 +
  19.169 +val prems = goal thy
  19.170 +   "(!! i. i:I ==> LeadsTo Init Acts (A i) (A' i)) \
  19.171 +\   ==> LeadsTo Init Acts (UN i:I. A i) (UN i:I. A' i)";
  19.172 +by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
  19.173 +by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_R] 
  19.174 +                        addIs prems) 1);
  19.175 +qed "LeadsTo_UN_UN";
  19.176 +
  19.177 +
  19.178 +(*Version with no index set*)
  19.179 +val prems = goal thy
  19.180 +   "(!! i. LeadsTo Init Acts (A i) (A' i)) \
  19.181 +\   ==> LeadsTo Init Acts (UN i. A i) (UN i. A' i)";
  19.182 +by (blast_tac (claset() addIs [LeadsTo_UN_UN] 
  19.183 +                        addIs prems) 1);
  19.184 +qed "LeadsTo_UN_UN_noindex";
  19.185 +
  19.186 +(*Version with no index set*)
  19.187 +goal thy
  19.188 +   "!!Acts. ALL i. LeadsTo Init Acts (A i) (A' i) \
  19.189 +\           ==> LeadsTo Init Acts (UN i. A i) (UN i. A' i)";
  19.190 +by (blast_tac (claset() addIs [LeadsTo_UN_UN]) 1);
  19.191 +qed "all_LeadsTo_UN_UN";
  19.192 +
  19.193 +
  19.194 +(*Binary union version*)
  19.195 +goal thy "!!Acts. [| LeadsTo Init Acts A A'; LeadsTo Init Acts B B' |] \
  19.196 +\                 ==> LeadsTo Init Acts (A Un B) (A' Un B')";
  19.197 +by (blast_tac (claset() addIs [LeadsTo_Un, 
  19.198 +			       LeadsTo_weaken_R]) 1);
  19.199 +qed "LeadsTo_Un_Un";
  19.200 +
  19.201 +
  19.202 +(** The cancellation law **)
  19.203 +
  19.204 +goal thy
  19.205 +   "!!Acts. [| LeadsTo Init Acts A (A' Un B); LeadsTo Init Acts B B'; \
  19.206 +\              id: Acts |]    \
  19.207 +\           ==> LeadsTo Init Acts A (A' Un B')";
  19.208 +by (blast_tac (claset() addIs [LeadsTo_Un_Un, 
  19.209 +			       subset_imp_LeadsTo, LeadsTo_Trans]) 1);
  19.210 +qed "LeadsTo_cancel2";
  19.211 +
  19.212 +goal thy
  19.213 +   "!!Acts. [| LeadsTo Init Acts A (A' Un B); LeadsTo Init Acts (B-A') B'; id: Acts |] \
  19.214 +\           ==> LeadsTo Init Acts A (A' Un B')";
  19.215 +by (rtac LeadsTo_cancel2 1);
  19.216 +by (assume_tac 2);
  19.217 +by (ALLGOALS Asm_simp_tac);
  19.218 +qed "LeadsTo_cancel_Diff2";
  19.219 +
  19.220 +goal thy
  19.221 +   "!!Acts. [| LeadsTo Init Acts A (B Un A'); LeadsTo Init Acts B B'; id: Acts |] \
  19.222 +\           ==> LeadsTo Init Acts A (B' Un A')";
  19.223 +by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
  19.224 +by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1);
  19.225 +qed "LeadsTo_cancel1";
  19.226 +
  19.227 +goal thy
  19.228 +   "!!Acts. [| LeadsTo Init Acts A (B Un A'); LeadsTo Init Acts (B-A') B'; id: Acts |] \
  19.229 +\           ==> LeadsTo Init Acts A (B' Un A')";
  19.230 +by (rtac LeadsTo_cancel1 1);
  19.231 +by (assume_tac 2);
  19.232 +by (ALLGOALS Asm_simp_tac);
  19.233 +qed "LeadsTo_cancel_Diff1";
  19.234 +
  19.235 +
  19.236 +
  19.237 +(** The impossibility law **)
  19.238 +
  19.239 +goalw thy [LeadsTo_def]
  19.240 +    "!!Acts. LeadsTo Init Acts A {} ==> reachable Init Acts Int A  = {}";
  19.241 +by (Full_simp_tac 1);
  19.242 +by (etac leadsTo_empty 1);
  19.243 +qed "LeadsTo_empty";
  19.244 +
  19.245 +
  19.246 +(** PSP: Progress-Safety-Progress **)
  19.247 +
  19.248 +(*Special case of PSP: Misra's "stable conjunction".  Doesn't need id:Acts. *)
  19.249 +goalw thy [LeadsTo_def]
  19.250 +   "!!Acts. [| LeadsTo Init Acts A A'; stable Acts B |] \
  19.251 +\           ==> LeadsTo Init Acts (A Int B) (A' Int B)";
  19.252 +by (asm_simp_tac (simpset() addsimps [Int_assoc RS sym, PSP_stable]) 1);
  19.253 +qed "R_PSP_stable";
  19.254 +
  19.255 +goal thy
  19.256 +   "!!Acts. [| LeadsTo Init Acts A A'; stable Acts B |] \
  19.257 +\           ==> LeadsTo Init Acts (B Int A) (B Int A')";
  19.258 +by (asm_simp_tac (simpset() addsimps (R_PSP_stable::Int_ac)) 1);
  19.259 +qed "R_PSP_stable2";
  19.260 +
  19.261 +
  19.262 +goalw thy [LeadsTo_def]
  19.263 +   "!!Acts. [| LeadsTo Init Acts A A'; constrains Acts B B'; id: Acts |] \
  19.264 +\           ==> LeadsTo Init Acts (A Int B) ((A' Int B) Un (B' - B))";
  19.265 +by (dtac PSP 1);
  19.266 +by (etac constrains_reachable 1);
  19.267 +by (etac leadsTo_weaken 2);
  19.268 +by (ALLGOALS Blast_tac);
  19.269 +qed "R_PSP";
  19.270 +
  19.271 +goal thy
  19.272 +   "!!Acts. [| LeadsTo Init Acts A A'; constrains Acts B B'; id: Acts |] \
  19.273 +\           ==> LeadsTo Init Acts (B Int A) ((B Int A') Un (B' - B))";
  19.274 +by (asm_simp_tac (simpset() addsimps (R_PSP::Int_ac)) 1);
  19.275 +qed "R_PSP2";
  19.276 +
  19.277 +goalw thy [unless_def]
  19.278 +   "!!Acts. [| LeadsTo Init Acts A A'; unless Acts B B'; id: Acts |] \
  19.279 +\           ==> LeadsTo Init Acts (A Int B) ((A' Int B) Un B')";
  19.280 +by (dtac R_PSP 1);
  19.281 +by (assume_tac 1);
  19.282 +by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2);
  19.283 +by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 2);
  19.284 +by (etac LeadsTo_Diff 2);
  19.285 +by (blast_tac (claset() addIs [subset_imp_LeadsTo]) 2);
  19.286 +by Auto_tac;
  19.287 +qed "R_PSP_unless";
  19.288 +
  19.289 +
  19.290 +(*** Induction rules ***)
  19.291 +
  19.292 +(** Meta or object quantifier ????? **)
  19.293 +goalw thy [LeadsTo_def]
  19.294 +   "!!Acts. [| wf r;     \
  19.295 +\              ALL m. LeadsTo Init Acts (A Int f-``{m})                     \
  19.296 +\                                       ((A Int f-``(r^-1 ^^ {m})) Un B);   \
  19.297 +\              id: Acts |] \
  19.298 +\           ==> LeadsTo Init Acts A B";
  19.299 +by (etac leadsTo_wf_induct 1);
  19.300 +by (assume_tac 2);
  19.301 +by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
  19.302 +qed "LeadsTo_wf_induct";
  19.303 +
  19.304 +
  19.305 +goal thy
  19.306 +   "!!Acts. [| wf r;     \
  19.307 +\              ALL m:I. LeadsTo Init Acts (A Int f-``{m})                   \
  19.308 +\                                  ((A Int f-``(r^-1 ^^ {m})) Un B);   \
  19.309 +\              id: Acts |] \
  19.310 +\           ==> LeadsTo Init Acts A ((A - (f-``I)) Un B)";
  19.311 +by (etac LeadsTo_wf_induct 1);
  19.312 +by Safe_tac;
  19.313 +by (case_tac "m:I" 1);
  19.314 +by (blast_tac (claset() addIs [LeadsTo_weaken]) 1);
  19.315 +by (blast_tac (claset() addIs [subset_imp_LeadsTo]) 1);
  19.316 +qed "R_bounded_induct";
  19.317 +
  19.318 +
  19.319 +goal thy
  19.320 +   "!!Acts. [| ALL m. LeadsTo Init Acts (A Int f-``{m})                     \
  19.321 +\                                  ((A Int f-``(lessThan m)) Un B);   \
  19.322 +\              id: Acts |] \
  19.323 +\           ==> LeadsTo Init Acts A B";
  19.324 +by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
  19.325 +by (assume_tac 2);
  19.326 +by (Asm_simp_tac 1);
  19.327 +qed "R_lessThan_induct";
  19.328 +
  19.329 +goal thy
  19.330 +   "!!Acts. [| ALL m:(greaterThan l). LeadsTo Init Acts (A Int f-``{m})   \
  19.331 +\                                        ((A Int f-``(lessThan m)) Un B);   \
  19.332 +\              id: Acts |] \
  19.333 +\           ==> LeadsTo Init Acts A ((A Int (f-``(atMost l))) Un B)";
  19.334 +by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);
  19.335 +by (rtac (wf_less_than RS R_bounded_induct) 1);
  19.336 +by (assume_tac 2);
  19.337 +by (Asm_simp_tac 1);
  19.338 +qed "R_lessThan_bounded_induct";
  19.339 +
  19.340 +goal thy
  19.341 +   "!!Acts. [| ALL m:(lessThan l). LeadsTo Init Acts (A Int f-``{m})   \
  19.342 +\                                    ((A Int f-``(greaterThan m)) Un B);   \
  19.343 +\              id: Acts |] \
  19.344 +\           ==> LeadsTo Init Acts A ((A Int (f-``(atLeast l))) Un B)";
  19.345 +by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
  19.346 +    (wf_less_than RS wf_inv_image RS LeadsTo_wf_induct) 1);
  19.347 +by (assume_tac 2);
  19.348 +by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
  19.349 +by (Clarify_tac 1);
  19.350 +by (case_tac "m<l" 1);
  19.351 +by (blast_tac (claset() addIs [not_leE, subset_imp_LeadsTo]) 2);
  19.352 +by (blast_tac (claset() addIs [LeadsTo_weaken_R, diff_less_mono2]) 1);
  19.353 +qed "R_greaterThan_bounded_induct";
  19.354 +
  19.355 +
  19.356 +
  19.357 +(*** Completion: Binary and General Finite versions ***)
  19.358 +
  19.359 +goalw thy [LeadsTo_def]
  19.360 +   "!!Acts. [| LeadsTo Init Acts A A';  stable Acts A';   \
  19.361 +\              LeadsTo Init Acts B B';  stable Acts B';  id: Acts |] \
  19.362 +\           ==> LeadsTo Init Acts (A Int B) (A' Int B')";
  19.363 +by (blast_tac (claset() addIs [stable_completion RS leadsTo_weaken] 
  19.364 +                        addSIs [stable_Int, stable_reachable]) 1);
  19.365 +qed "R_stable_completion";
  19.366 +
  19.367 +
  19.368 +goal thy
  19.369 +   "!!Acts. [| finite I;  id: Acts |]                     \
  19.370 +\           ==> (ALL i:I. LeadsTo Init Acts (A i) (A' i)) -->  \
  19.371 +\               (ALL i:I. stable Acts (A' i)) -->         \
  19.372 +\               LeadsTo Init Acts (INT i:I. A i) (INT i:I. A' i)";
  19.373 +by (etac finite_induct 1);
  19.374 +by (Asm_simp_tac 1);
  19.375 +by (asm_simp_tac 
  19.376 +    (simpset() addsimps [R_stable_completion, stable_def, 
  19.377 +			 ball_constrains_INT]) 1);
  19.378 +qed_spec_mp "R_finite_stable_completion";
  19.379 +
  19.380 +
  19.381 +goalw thy [LeadsTo_def]
  19.382 + "!!Acts. [| LeadsTo Init Acts A (A' Un C);  constrains Acts A' (A' Un C); \
  19.383 +\            LeadsTo Init Acts B (B' Un C);  constrains Acts B' (B' Un C); \
  19.384 +\            id: Acts |] \
  19.385 +\         ==> LeadsTo Init Acts (A Int B) ((A' Int B') Un C)";
  19.386 +
  19.387 +by (full_simp_tac (simpset() addsimps [Int_Un_distrib]) 1);
  19.388 +by (dtac completion 1);
  19.389 +by (assume_tac 2);
  19.390 +by (ALLGOALS 
  19.391 +    (asm_simp_tac 
  19.392 +     (simpset() addsimps [constrains_reachable, Int_Un_distrib RS sym])));
  19.393 +by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
  19.394 +qed "R_completion";
  19.395 +
  19.396 +
  19.397 +goal thy
  19.398 +   "!!Acts. [| finite I;  id: Acts |] \
  19.399 +\           ==> (ALL i:I. LeadsTo Init Acts (A i) (A' i Un C)) -->  \
  19.400 +\               (ALL i:I. constrains Acts (A' i) (A' i Un C)) --> \
  19.401 +\               LeadsTo Init Acts (INT i:I. A i) ((INT i:I. A' i) Un C)";
  19.402 +by (etac finite_induct 1);
  19.403 +by (ALLGOALS Asm_simp_tac);
  19.404 +by (Clarify_tac 1);
  19.405 +by (dtac ball_constrains_INT 1);
  19.406 +by (asm_full_simp_tac (simpset() addsimps [R_completion]) 1); 
  19.407 +qed "R_finite_completion";
  19.408 +
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/src/HOL/UNITY/SubstAx.thy	Fri Apr 03 12:34:33 1998 +0200
    20.3 @@ -0,0 +1,19 @@
    20.4 +(*  Title:      HOL/UNITY/SubstAx
    20.5 +    ID:         $Id$
    20.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    20.7 +    Copyright   1998  University of Cambridge
    20.8 +
    20.9 +My treatment of the Substitution Axiom -- not as an axiom!
   20.10 +*)
   20.11 +
   20.12 +SubstAx = WFair +
   20.13 +
   20.14 +constdefs
   20.15 +
   20.16 +   LeadsTo :: "['a set, ('a * 'a)set set, 'a set, 'a set] => bool"
   20.17 +    "LeadsTo Init Acts A B ==
   20.18 +     leadsTo Acts (reachable Init Acts Int A)
   20.19 +                  (reachable Init Acts Int B)"
   20.20 +
   20.21 +
   20.22 +end
    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/src/HOL/UNITY/Token.ML	Fri Apr 03 12:34:33 1998 +0200
    21.3 @@ -0,0 +1,150 @@
    21.4 +(*  Title:      HOL/UNITY/Token
    21.5 +    ID:         $Id$
    21.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    21.7 +    Copyright   1998  University of Cambridge
    21.8 +
    21.9 +The Token Ring.
   21.10 +
   21.11 +From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
   21.12 +*)
   21.13 +
   21.14 +
   21.15 +open Token;
   21.16 +
   21.17 +
   21.18 +val Token_defs = [WellTyped_def, Token_def, HasTok_def, H_def, E_def, T_def];
   21.19 +
   21.20 +AddIffs [N_positive, skip];
   21.21 +
   21.22 +goalw thy [HasTok_def] "!!i. [| s: HasTok i; s: HasTok j |] ==> i=j";
   21.23 +by Auto_tac;
   21.24 +qed "HasToK_partition";
   21.25 +
   21.26 +goalw thy Token_defs "!!s. s : WellTyped ==> (s ~: E i) = (s : H i | s : T i)";
   21.27 +by (Simp_tac 1);
   21.28 +by (exhaust_tac "s (Suc i)" 1);
   21.29 +by Auto_tac;
   21.30 +qed "not_E_eq";
   21.31 +
   21.32 +(** We should be able to prove WellTyped as a separate Invariant.  Then
   21.33 +    the Invariant rule should let us assume that the initial
   21.34 +    state is reachable, and therefore contained in any Invariant.  Then
   21.35 +    we'd not have to mention WellTyped in the statement of this theorem.
   21.36 +**)
   21.37 +
   21.38 +goalw thy [stable_def]
   21.39 +    "stable Acts (WellTyped Int {s. s : E i --> s : HasTok i})";
   21.40 +by (rtac (stable_WT RS stable_constrains_Int) 1);
   21.41 +by (cut_facts_tac [TR2,TR4,TR5] 1);
   21.42 +by (asm_full_simp_tac (simpset() addsimps [constrains_def]) 1);
   21.43 +by (REPEAT_FIRST (rtac ballI ORELSE' (dtac bspec THEN' assume_tac)));
   21.44 +by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
   21.45 +by (case_tac "xa : HasTok i" 1);
   21.46 +by (auto_tac (claset(), simpset() addsimps [H_def, E_def, T_def]));
   21.47 +qed "token_stable";
   21.48 +
   21.49 +(*This proof is in the "massaging" style and is much faster! *)
   21.50 +goalw thy [stable_def]
   21.51 +    "stable Acts (WellTyped Int (Compl(E i) Un (HasTok i)))";
   21.52 +by (rtac (stable_WT RS stable_constrains_Int) 1);
   21.53 +by (rtac constrains_weaken 1);
   21.54 +by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1);
   21.55 +by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
   21.56 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [H_def, E_def, T_def])));
   21.57 +qed "token_stable";
   21.58 +
   21.59 +
   21.60 +(*** Progress under weak fairness ***)
   21.61 +
   21.62 +goalw thy [nodeOrder_def] "wf(nodeOrder j)";
   21.63 +by (rtac (wf_less_than RS wf_inv_image RS wf_subset) 1);
   21.64 +by (Blast_tac 1);
   21.65 +qed"wf_nodeOrder";
   21.66 +
   21.67 +    goal thy "!!m. [| m<n; Suc m ~= n |] ==> Suc(m) < n";
   21.68 +    by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1);
   21.69 +    by (blast_tac (claset() addEs [less_asym, less_SucE]) 1);
   21.70 +    qed "Suc_lessI";
   21.71 +
   21.72 +goalw thy [nodeOrder_def, next_def, inv_image_def]
   21.73 +    "!!x. [| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)";
   21.74 +by (auto_tac (claset(),
   21.75 +	      simpset() addsimps [Suc_lessI, mod_Suc, mod_less, mod_geq]));
   21.76 +by (dtac sym 1);
   21.77 +(*The next two lines...**)
   21.78 +by (REPEAT (eres_inst_tac [("P", "?a<N")] rev_mp 1));
   21.79 +by (etac ssubst 1);
   21.80 +(*were with the previous version of asm_full_simp_tac...
   21.81 +  by (rotate_tac ~1 1);
   21.82 +*)
   21.83 +by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv, mod_Suc, mod_less]) 1);
   21.84 +by (subgoal_tac "(j + N - i) = Suc (j + N - Suc i)" 1);
   21.85 +by (asm_simp_tac (simpset() addsimps [Suc_diff_Suc, less_imp_le, Suc_leI, 
   21.86 +                                      diff_add_assoc]) 2);
   21.87 +by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1);
   21.88 +by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc]) 1);
   21.89 +(*including less_asym here would slow things down*)
   21.90 +by (auto_tac (claset() delrules [notI], 
   21.91 +              simpset() addsimps [diff_add_assoc2, Suc_leI,
   21.92 +                                  less_imp_diff_less, 
   21.93 +                                  mod_less, mod_geq, nat_neq_iff]));
   21.94 +by (REPEAT (blast_tac (claset() addEs [less_asym]) 3));
   21.95 +by (asm_simp_tac (simpset() addsimps [less_imp_diff_less,
   21.96 +				      Suc_diff_n RS sym]) 1);
   21.97 +by (asm_simp_tac (simpset() addsimps [add_diff_less, mod_less]) 1);
   21.98 +by (etac subst 1);
   21.99 +by (asm_simp_tac (simpset() addsimps [add_diff_less]) 1);
  21.100 +qed "nodeOrder_eq";
  21.101 +
  21.102 +
  21.103 +(*From "A Logic for Concurrent Programming", but not used in Chapter 4.
  21.104 +  Note the use of case_tac.  Reasoning about leadsTo takes practice!*)
  21.105 +goal thy
  21.106 + "!!i. [| i<N; j<N |] ==> \
  21.107 +\      leadsTo Acts (HasTok i) ({s. (Token s, i) : nodeOrder j} Un HasTok j)";
  21.108 +by (case_tac "i=j" 1);
  21.109 +by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
  21.110 +by (rtac (TR7 RS leadsTo_weaken_R) 1);
  21.111 +by (Clarify_tac 1);
  21.112 +by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
  21.113 +qed "TR7_nodeOrder";
  21.114 +
  21.115 +
  21.116 +(*Chapter 4 variant, the one actually used below.*)
  21.117 +goal thy
  21.118 + "!!i. [| i<N; j<N; i~=j |] ==> \
  21.119 +\      leadsTo Acts (HasTok i) {s. (Token s, i) : nodeOrder j}";
  21.120 +by (rtac (TR7 RS leadsTo_weaken_R) 1);
  21.121 +by (Clarify_tac 1);
  21.122 +by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
  21.123 +qed "TR7_aux";
  21.124 +
  21.125 +goal thy "({s. Token s < N} Int Token -`` {m}) = \
  21.126 +\         (if m<N then Token -`` {m} else {})";
  21.127 +by Auto_tac;
  21.128 +val Token_lemma = result();
  21.129 +
  21.130 +
  21.131 +(*Misra's TR9: the token reaches an arbitrary node*)
  21.132 +goal thy
  21.133 + "!!i. j<N ==> leadsTo Acts {s. Token s < N} (HasTok j)";
  21.134 +by (rtac leadsTo_weaken_R 1);
  21.135 +by (res_inst_tac [("I", "Compl{j}"), ("f", "Token"), ("B", "{}")]
  21.136 +     (wf_nodeOrder RS bounded_induct) 1);
  21.137 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [Token_lemma, vimage_Diff,
  21.138 +						HasTok_def])));
  21.139 +by (Blast_tac 2);
  21.140 +by (Clarify_tac 1);
  21.141 +by (rtac (TR7_aux RS leadsTo_weaken) 1);
  21.142 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [nodeOrder_def, HasTok_def])));
  21.143 +by (ALLGOALS Blast_tac);
  21.144 +qed "leadsTo_j";
  21.145 +
  21.146 +(*Misra's TR8: a hungry process eventually eats*)
  21.147 +goal thy "!!i. j<N ==> leadsTo Acts ({s. Token s < N} Int H j) (E j)";
  21.148 +by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1);
  21.149 +by (rtac TR6 2);
  21.150 +by (rtac leadsTo_weaken_R 1);
  21.151 +by (rtac ([leadsTo_j, TR3] MRS PSP) 1);
  21.152 +by (ALLGOALS Blast_tac);
  21.153 +qed "Token_progress";
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/src/HOL/UNITY/Token.thy	Fri Apr 03 12:34:33 1998 +0200
    22.3 @@ -0,0 +1,71 @@
    22.4 +(*  Title:      HOL/UNITY/Token
    22.5 +    ID:         $Id$
    22.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    22.7 +    Copyright   1998  University of Cambridge
    22.8 +
    22.9 +The Token Ring.
   22.10 +
   22.11 +From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
   22.12 +*)
   22.13 +
   22.14 +
   22.15 +Token = WFair +
   22.16 +
   22.17 +(*process states*)
   22.18 +datatype pstate = Hungry | Eating | Thinking | Pnum nat
   22.19 +
   22.20 +types state = nat => pstate
   22.21 +
   22.22 +consts
   22.23 +  N :: nat	(*number of nodes in the ring*)
   22.24 +
   22.25 +constdefs
   22.26 +  nodeOrder :: "nat => (nat*nat)set"
   22.27 +    "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N))  Int
   22.28 +                    (lessThan N Times lessThan N)"
   22.29 +
   22.30 +  next      :: nat => nat
   22.31 +    "next i == (Suc i) mod N"
   22.32 +
   22.33 +  WellTyped :: state set
   22.34 +    "WellTyped == {s. ALL i j. s (Suc i) ~= Pnum j}"
   22.35 +
   22.36 +  Token :: state => nat
   22.37 +    "Token s == case s 0 of 
   22.38 +                    Hungry => 0
   22.39 +                  | Eating => 0
   22.40 +                  | Thinking => 0
   22.41 +                  | Pnum i => i"
   22.42 +
   22.43 +  HasTok :: nat => state set
   22.44 +    "HasTok i == Token -`` {i}"
   22.45 +
   22.46 +  H :: nat => state set
   22.47 +    "H i == {s. s (Suc i) = Hungry}"
   22.48 +
   22.49 +  E :: nat => state set
   22.50 +    "E i == {s. s (Suc i) = Eating}"
   22.51 +
   22.52 +  T :: nat => state set
   22.53 +    "T i == {s. s (Suc i) = Thinking}"
   22.54 +
   22.55 +rules
   22.56 +  N_positive "0<N"
   22.57 +
   22.58 +  stable_WT  "stable Acts WellTyped"
   22.59 +
   22.60 +  skip "id: Acts"
   22.61 +
   22.62 +  TR2  "constrains Acts (T i) (T i Un H i)"
   22.63 +
   22.64 +  TR3  "constrains Acts (H i) (H i Un E i)"
   22.65 +
   22.66 +  TR4  "constrains Acts (H i - HasTok i) (H i)"
   22.67 +
   22.68 +  TR5  "constrains Acts (HasTok i) (HasTok i Un Compl(E i))"
   22.69 +
   22.70 +  TR6  "leadsTo Acts (H i Int HasTok i) (E i)"
   22.71 +
   22.72 +  TR7  "leadsTo Acts (HasTok i) (HasTok (next i))"
   22.73 +
   22.74 +end
    23.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.2 +++ b/src/HOL/UNITY/Traces.ML	Fri Apr 03 12:34:33 1998 +0200
    23.3 @@ -0,0 +1,39 @@
    23.4 +open Traces;
    23.5 +
    23.6 +goal thy "reachable Init Acts <= {s. EX evs. s#evs: traces Init Acts}";
    23.7 +by (rtac subsetI 1);
    23.8 +be reachable.induct 1;
    23.9 +by (REPEAT (blast_tac (claset() addIs traces.intrs) 1));
   23.10 +val lemma1 = result();
   23.11 +
   23.12 +goal thy "!!evs. evs : traces Init Acts \
   23.13 +\                ==> ALL s evs'. evs = s#evs' --> s: reachable Init Acts";
   23.14 +be traces.induct 1;
   23.15 +by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
   23.16 +val lemma2 = normalize_thm [RSmp, RSspec] (result());
   23.17 +
   23.18 +goal thy "{s. EX evs. s#evs: traces Init Acts} <= reachable Init Acts";
   23.19 +by (blast_tac (claset() addIs [lemma2]) 1);
   23.20 +val lemma3 = result();
   23.21 +
   23.22 +goal thy "reachable Init Acts = {s. EX evs. s#evs: traces Init Acts}";
   23.23 +by (rtac ([lemma1,lemma3] MRS equalityI) 1);
   23.24 +qed "reachable_eq_traces";
   23.25 +
   23.26 +
   23.27 +(*Could/should this be proved?*)
   23.28 +goal thy "reachable Init Acts = (UN evs: traces Init Acts. set evs)";
   23.29 +
   23.30 +
   23.31 +(*The strongest invariant is the set of all reachable states!*)
   23.32 +goalw thy [stable_def, constrains_def]
   23.33 +    "!!A. [| Init<=A;  stable Acts A |] ==> reachable Init Acts <= A";
   23.34 +by (rtac subsetI 1);
   23.35 +be reachable.induct 1;
   23.36 +by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
   23.37 +qed "strongest_invariant";
   23.38 +
   23.39 +goal thy "stable Acts (reachable Init Acts)";
   23.40 +by (REPEAT (blast_tac (claset() addIs [stableI, constrainsI]
   23.41 +				addIs reachable.intrs) 1));
   23.42 +qed "stable_reachable";
    24.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.2 +++ b/src/HOL/UNITY/Traces.thy	Fri Apr 03 12:34:33 1998 +0200
    24.3 @@ -0,0 +1,24 @@
    24.4 +Traces = UNITY +
    24.5 +
    24.6 +consts traces :: "['a set, ('a * 'a)set set] => 'a list set"
    24.7 +
    24.8 +inductive "traces Init Acts"
    24.9 +  intrs 
   24.10 +         (*Initial trace is empty*)
   24.11 +    Init  "s: Init ==> [s] : traces Init Acts"
   24.12 +
   24.13 +    Acts  "[| act: Acts;  s#evs : traces Init Acts;  (s,s'): act |]
   24.14 +	   ==> s'#s#evs : traces Init Acts"
   24.15 +
   24.16 +
   24.17 +consts reachable :: "['a set, ('a * 'a)set set] => 'a set"
   24.18 +
   24.19 +inductive "reachable Init Acts"
   24.20 +  intrs 
   24.21 +         (*Initial trace is empty*)
   24.22 +    Init  "s: Init ==> s : reachable Init Acts"
   24.23 +
   24.24 +    Acts  "[| act: Acts;  s : reachable Init Acts;  (s,s'): act |]
   24.25 +	   ==> s' : reachable Init Acts"
   24.26 +
   24.27 +end
    25.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.2 +++ b/src/HOL/UNITY/UNITY.ML	Fri Apr 03 12:34:33 1998 +0200
    25.3 @@ -0,0 +1,229 @@
    25.4 +(*  Title:      HOL/UNITY/UNITY
    25.5 +    ID:         $Id$
    25.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    25.7 +    Copyright   1998  University of Cambridge
    25.8 +
    25.9 +The basic UNITY theory (revised version, based upon the "co" operator)
   25.10 +
   25.11 +From Misra, "A Logic for Concurrent Programming", 1994
   25.12 +*)
   25.13 +
   25.14 +set proof_timing;
   25.15 +HOL_quantifiers := false;
   25.16 +
   25.17 +
   25.18 +(*CAN BOOLEAN SIMPLIFICATION BE AUTOMATED?*)
   25.19 +
   25.20 +(** Rewrites rules to eliminate A.  Conditions can be satisfied by letting B
   25.21 +    be any set including A Int C and contained in A Un C, such as B=A or B=C.
   25.22 +**)
   25.23 +
   25.24 +goal thy "!!x. [| A Int C <= B; B <= A Un C |] \
   25.25 +\              ==> (A Int B) Un (Compl A Int C) = B Un C";
   25.26 +by (Blast_tac 1);
   25.27 +
   25.28 +goal thy "!!x. [| A Int C <= B; B <= A Un C |] \
   25.29 +\              ==> (A Un B) Int (Compl A Un C) = B Int C";
   25.30 +by (Blast_tac 1);
   25.31 +
   25.32 +(*The base B=A*)
   25.33 +goal thy "A Un (Compl A Int C) = A Un C";
   25.34 +by (Blast_tac 1);
   25.35 +
   25.36 +goal thy "A Int (Compl A Un C) = A Int C";
   25.37 +by (Blast_tac 1);
   25.38 +
   25.39 +(*The base B=C*)
   25.40 +goal thy "(A Int C) Un (Compl A Int C) = C";
   25.41 +by (Blast_tac 1);
   25.42 +
   25.43 +goal thy "(A Un C) Int (Compl A Un C) = C";
   25.44 +by (Blast_tac 1);
   25.45 +
   25.46 +
   25.47 +(** More ad-hoc rules **)
   25.48 +
   25.49 +goal thy "A Un B - (A - B) = B";
   25.50 +by (Blast_tac 1);
   25.51 +qed "Un_Diff_Diff";
   25.52 +
   25.53 +goal thy "A Int (B - C) Un C = A Int B Un C";
   25.54 +by (Blast_tac 1);
   25.55 +qed "Int_Diff_Un";
   25.56 +
   25.57 +
   25.58 +open UNITY;
   25.59 +
   25.60 +
   25.61 +(*** constrains ***)
   25.62 +
   25.63 +val prems = goalw thy [constrains_def]
   25.64 +    "(!!act s s'. [| act: Acts;  (s,s') : act;  s: A |] ==> s': A') \
   25.65 +\    ==> constrains Acts A A'";
   25.66 +by (blast_tac (claset() addIs prems) 1);
   25.67 +qed "constrainsI";
   25.68 +
   25.69 +goalw thy [constrains_def]
   25.70 +    "!!Acts. [| constrains Acts A A'; act: Acts;  (s,s'): act;  s: A |] \
   25.71 +\            ==> s': A'";
   25.72 +by (Blast_tac 1);
   25.73 +qed "constrainsD";
   25.74 +
   25.75 +goalw thy [constrains_def] "constrains Acts {} B";
   25.76 +by (Blast_tac 1);
   25.77 +qed "constrains_empty";
   25.78 +
   25.79 +goalw thy [constrains_def] "constrains Acts A UNIV";
   25.80 +by (Blast_tac 1);
   25.81 +qed "constrains_UNIV";
   25.82 +AddIffs [constrains_empty, constrains_UNIV];
   25.83 +
   25.84 +goalw thy [constrains_def]
   25.85 +    "!!Acts. [| constrains Acts A A'; A'<=B' |] ==> constrains Acts A B'";
   25.86 +by (Blast_tac 1);
   25.87 +qed "constrains_weaken_R";
   25.88 +
   25.89 +goalw thy [constrains_def]
   25.90 +    "!!Acts. [| constrains Acts A A'; B<=A |] ==> constrains Acts B A'";
   25.91 +by (Blast_tac 1);
   25.92 +qed "constrains_weaken_L";
   25.93 +
   25.94 +goalw thy [constrains_def]
   25.95 +   "!!Acts. [| constrains Acts A A'; B<=A; A'<=B' |] ==> constrains Acts B B'";
   25.96 +by (Blast_tac 1);
   25.97 +qed "constrains_weaken";
   25.98 +
   25.99 +(*Set difference: UNUSED*)
  25.100 +goalw thy [constrains_def]
  25.101 +  "!!C. [| constrains Acts (A-B) C; constrains Acts B C |] \
  25.102 +\       ==> constrains Acts A C";
  25.103 +by (Blast_tac 1);
  25.104 +qed "constrains_Diff";
  25.105 +
  25.106 +(** Union **)
  25.107 +
  25.108 +goalw thy [constrains_def]
  25.109 +    "!!Acts. [| constrains Acts A A'; constrains Acts B B' |]   \
  25.110 +\           ==> constrains Acts (A Un B) (A' Un B')";
  25.111 +by (Blast_tac 1);
  25.112 +qed "constrains_Un";
  25.113 +
  25.114 +goalw thy [constrains_def]
  25.115 +    "!!Acts. ALL i:I. constrains Acts (A i) (A' i) \
  25.116 +\    ==> constrains Acts (UN i:I. A i) (UN i:I. A' i)";
  25.117 +by (Blast_tac 1);
  25.118 +qed "ball_constrains_UN";
  25.119 +
  25.120 +goalw thy [constrains_def]
  25.121 +    "!!Acts. [| ALL i. constrains Acts (A i) (A' i) |] \
  25.122 +\           ==> constrains Acts (UN i. A i) (UN i. A' i)";
  25.123 +by (Blast_tac 1);
  25.124 +qed "all_constrains_UN";
  25.125 +
  25.126 +(** Intersection **)
  25.127 +
  25.128 +goalw thy [constrains_def]
  25.129 +    "!!Acts. [| constrains Acts A A'; constrains Acts B B' |]   \
  25.130 +\           ==> constrains Acts (A Int B) (A' Int B')";
  25.131 +by (Blast_tac 1);
  25.132 +qed "constrains_Int";
  25.133 +
  25.134 +goalw thy [constrains_def]
  25.135 +    "!!Acts. ALL i:I. constrains Acts (A i) (A' i) \
  25.136 +\    ==> constrains Acts (INT i:I. A i) (INT i:I. A' i)";
  25.137 +by (Blast_tac 1);
  25.138 +qed "ball_constrains_INT";
  25.139 +
  25.140 +goalw thy [constrains_def]
  25.141 +    "!!Acts. [| ALL i. constrains Acts (A i) (A' i) |] \
  25.142 +\           ==> constrains Acts (INT i. A i) (INT i. A' i)";
  25.143 +by (Blast_tac 1);
  25.144 +qed "all_constrains_INT";
  25.145 +
  25.146 +goalw thy [stable_def, constrains_def]
  25.147 +    "!!Acts. [| stable Acts C; constrains Acts A (C Un A') |]   \
  25.148 +\           ==> constrains Acts (C Un A) (C Un A')";
  25.149 +by (Blast_tac 1);
  25.150 +qed "stable_constrains_Un";
  25.151 +
  25.152 +goalw thy [stable_def, constrains_def]
  25.153 +    "!!Acts. [| stable Acts C; constrains Acts (C Int A) A' |]   \
  25.154 +\           ==> constrains Acts (C Int A) (C Int A')";
  25.155 +by (Blast_tac 1);
  25.156 +qed "stable_constrains_Int";
  25.157 +
  25.158 +
  25.159 +(*** stable ***)
  25.160 +
  25.161 +goalw thy [stable_def]
  25.162 +    "!!Acts. constrains Acts A A ==> stable Acts A";
  25.163 +by (assume_tac 1);
  25.164 +qed "stableI";
  25.165 +
  25.166 +goalw thy [stable_def]
  25.167 +    "!!Acts. stable Acts A ==> constrains Acts A A";
  25.168 +by (assume_tac 1);
  25.169 +qed "stableD";
  25.170 +
  25.171 +goalw thy [stable_def]
  25.172 +    "!!Acts. [| stable Acts A; stable Acts A' |]   \
  25.173 +\           ==> stable Acts (A Un A')";
  25.174 +by (blast_tac (claset() addIs [constrains_Un]) 1);
  25.175 +qed "stable_Un";
  25.176 +
  25.177 +goalw thy [stable_def]
  25.178 +    "!!Acts. [| stable Acts A; stable Acts A' |]   \
  25.179 +\           ==> stable Acts (A Int A')";
  25.180 +by (blast_tac (claset() addIs [constrains_Int]) 1);
  25.181 +qed "stable_Int";
  25.182 +
  25.183 +goalw thy [constrains_def]
  25.184 +    "!!Acts. [| constrains Acts A A'; id: Acts |] ==> A<=A'";
  25.185 +by (Blast_tac 1);
  25.186 +qed "constrains_imp_subset";
  25.187 +
  25.188 +
  25.189 +goalw thy [constrains_def]
  25.190 +    "!!Acts. [| id: Acts; constrains Acts A B; constrains Acts B C |]   \
  25.191 +\           ==> constrains Acts A C";
  25.192 +by (Blast_tac 1);
  25.193 +qed "constrains_trans";
  25.194 +
  25.195 +
  25.196 +(*The Elimination Theorem.  The "free" m has become universally quantified!
  25.197 +  Should the premise be !!m instead of ALL m ?  Would make it harder to use
  25.198 +  in forward proof.*)
  25.199 +goalw thy [constrains_def]
  25.200 +    "!!Acts. [| ALL m. constrains Acts {s. s x = m} (B m) |] \
  25.201 +\           ==> constrains Acts {s. P(s x)} (UN m. {s. P(m)} Int B m)";
  25.202 +by (Blast_tac 1);
  25.203 +qed "elimination";
  25.204 +
  25.205 +(*As above, but for the trivial case of a one-variable state, in which the
  25.206 +  state is identified with its one variable.*)
  25.207 +goalw thy [constrains_def]
  25.208 +    "!!Acts. [| ALL m. constrains Acts {m} (B m) |] \
  25.209 +\           ==> constrains Acts {s. P s} (UN m. {s. P(m)} Int B m)";
  25.210 +by (Blast_tac 1);
  25.211 +qed "elimination_sing";
  25.212 +
  25.213 +
  25.214 +goalw thy [constrains_def]
  25.215 +   "!!Acts. [| constrains Acts A (A' Un B); constrains Acts B B'; id: Acts |] \
  25.216 +\           ==> constrains Acts A (A' Un B')";
  25.217 +by (Blast_tac 1);
  25.218 +qed "constrains_cancel";
  25.219 +
  25.220 +
  25.221 +
  25.222 +(*** Theoretical Results from Section 6 ***)
  25.223 +
  25.224 +goalw thy [constrains_def, strongest_rhs_def]
  25.225 +    "constrains Acts A (strongest_rhs Acts A )";
  25.226 +by (Blast_tac 1);
  25.227 +qed "constrains_strongest_rhs";
  25.228 +
  25.229 +goalw thy [constrains_def, strongest_rhs_def]
  25.230 +    "!!Acts. constrains Acts A B ==> strongest_rhs Acts A <= B";
  25.231 +by (Blast_tac 1);
  25.232 +qed "strongest_rhs_is_strongest";
    26.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.2 +++ b/src/HOL/UNITY/UNITY.thy	Fri Apr 03 12:34:33 1998 +0200
    26.3 @@ -0,0 +1,27 @@
    26.4 +(*  Title:      HOL/UNITY/UNITY
    26.5 +    ID:         $Id$
    26.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    26.7 +    Copyright   1998  University of Cambridge
    26.8 +
    26.9 +The basic UNITY theory (revised version, based upon the "co" operator)
   26.10 +
   26.11 +From Misra, "A Logic for Concurrent Programming", 1994
   26.12 +*)
   26.13 +
   26.14 +UNITY = LessThan +
   26.15 +
   26.16 +constdefs
   26.17 +
   26.18 +  constrains :: "[('a * 'a)set set, 'a set, 'a set] => bool"
   26.19 +    "constrains Acts A B == ALL act:Acts. act^^A <= B"
   26.20 +
   26.21 +  stable     :: "('a * 'a)set set => 'a set => bool"
   26.22 +    "stable Acts A == constrains Acts A A"
   26.23 +
   26.24 +  strongest_rhs :: "[('a * 'a)set set, 'a set] => 'a set"
   26.25 +    "strongest_rhs Acts A == Inter {B. constrains Acts A B}"
   26.26 +
   26.27 +  unless :: "[('a * 'a)set set, 'a set, 'a set] => bool"
   26.28 +    "unless mutex A B == constrains mutex (A-B) (A Un B)"
   26.29 +
   26.30 +end
    27.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.2 +++ b/src/HOL/UNITY/Update.ML	Fri Apr 03 12:34:33 1998 +0200
    27.3 @@ -0,0 +1,26 @@
    27.4 +(*  Title:      HOL/UNITY/Update.thy
    27.5 +    ID:         $Id$
    27.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    27.7 +    Copyright   1998  University of Cambridge
    27.8 +
    27.9 +Function updates: like the standard theory Map, but for ordinary functions
   27.10 +*)
   27.11 +
   27.12 +open Update;
   27.13 +
   27.14 +goalw thy [update_def] "(f[x|->y] = f) = (f x = y)";
   27.15 +by Safe_tac;
   27.16 +by (etac subst 1);
   27.17 +by (rtac ext 2);
   27.18 +by Auto_tac;
   27.19 +qed "update_idem_iff";
   27.20 +
   27.21 +(* f x = y ==> f[x|->y] = f *)
   27.22 +bind_thm("update_idem", update_idem_iff RS iffD2);
   27.23 +
   27.24 +AddIffs [refl RS update_idem];
   27.25 +
   27.26 +goal thy "(f[x|->y])z = (if x=z then y else f z)";
   27.27 +by (simp_tac (simpset() addsimps [update_def]) 1);
   27.28 +qed "update_apply";
   27.29 +Addsimps [update_apply];
    28.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    28.2 +++ b/src/HOL/UNITY/Update.thy	Fri Apr 03 12:34:33 1998 +0200
    28.3 @@ -0,0 +1,22 @@
    28.4 +(*  Title:      HOL/UNITY/Update.thy
    28.5 +    ID:         $Id$
    28.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    28.7 +    Copyright   1998  University of Cambridge
    28.8 +
    28.9 +Function updates: like the standard theory Map, but for ordinary functions
   28.10 +*)
   28.11 +
   28.12 +Update = Fun +
   28.13 +
   28.14 +consts
   28.15 +  update  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
   28.16 +           ("_/[_/|->/_]" [900,0,0] 900)
   28.17 +
   28.18 +syntax (symbols)
   28.19 +  update    :: "('a => 'b) => 'a => 'b => ('a => 'b)"
   28.20 +               ("_/[_/\\<mapsto>/_]" [900,0,0] 900)
   28.21 +
   28.22 +defs
   28.23 +  update_def "f[a|->b] == %x. if x=a then b else f x"
   28.24 +
   28.25 +end
    29.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    29.2 +++ b/src/HOL/UNITY/WFair.ML	Fri Apr 03 12:34:33 1998 +0200
    29.3 @@ -0,0 +1,576 @@
    29.4 +(*  Title:      HOL/UNITY/WFair
    29.5 +    ID:         $Id$
    29.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    29.7 +    Copyright   1998  University of Cambridge
    29.8 +
    29.9 +Weak Fairness versions of transient, ensures, leadsTo.
   29.10 +
   29.11 +From Misra, "A Logic for Concurrent Programming", 1994
   29.12 +*)
   29.13 +
   29.14 +open WFair;
   29.15 +
   29.16 +goal thy "Union(B) Int A = Union((%C. C Int A)``B)";
   29.17 +by (Blast_tac 1);
   29.18 +qed "Int_Union_Union";
   29.19 +
   29.20 +
   29.21 +(*** transient ***)
   29.22 +
   29.23 +goalw thy [stable_def, constrains_def, transient_def]
   29.24 +    "!!A. [| stable Acts A; transient Acts A |] ==> A = {}";
   29.25 +by (Blast_tac 1);
   29.26 +qed "stable_transient_empty";
   29.27 +
   29.28 +goalw thy [transient_def]
   29.29 +    "!!A. [| transient Acts A; B<=A |] ==> transient Acts B";
   29.30 +by (Clarify_tac 1);
   29.31 +by (rtac bexI 1 THEN assume_tac 2);
   29.32 +by (Blast_tac 1);
   29.33 +qed "transient_strengthen";
   29.34 +
   29.35 +goalw thy [transient_def]
   29.36 +    "!!A. [| act:Acts;  A <= Domain act;  act^^A <= Compl A |] \
   29.37 +\         ==> transient Acts A";
   29.38 +by (Blast_tac 1);
   29.39 +qed "transient_mem";
   29.40 +
   29.41 +
   29.42 +(*** ensures ***)
   29.43 +
   29.44 +goalw thy [ensures_def]
   29.45 +    "!!Acts. [| constrains Acts (A-B) (A Un B); transient Acts (A-B) |] \
   29.46 +\            ==> ensures Acts A B";
   29.47 +by (Blast_tac 1);
   29.48 +qed "ensuresI";
   29.49 +
   29.50 +goalw thy [ensures_def]
   29.51 +    "!!Acts. ensures Acts A B  \
   29.52 +\            ==> constrains Acts (A-B) (A Un B) & transient Acts (A-B)";
   29.53 +by (Blast_tac 1);
   29.54 +qed "ensuresD";
   29.55 +
   29.56 +(*The L-version (precondition strengthening) doesn't hold for ENSURES*)
   29.57 +goalw thy [ensures_def]
   29.58 +    "!!Acts. [| ensures Acts A A'; A'<=B' |] ==> ensures Acts A B'";
   29.59 +by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
   29.60 +qed "ensures_weaken_R";
   29.61 +
   29.62 +goalw thy [ensures_def, constrains_def, transient_def]
   29.63 +    "!!Acts. Acts ~= {} ==> ensures Acts A UNIV";
   29.64 +by (Asm_simp_tac 1);  (*omitting this causes PROOF FAILED, even with Safe_tac*)
   29.65 +by (Blast_tac 1);
   29.66 +qed "ensures_UNIV";
   29.67 +
   29.68 +goalw thy [ensures_def]
   29.69 +    "!!Acts. [| stable Acts C; \
   29.70 +\               constrains Acts (C Int (A - A')) (A Un A'); \
   29.71 +\               transient  Acts (C Int (A-A')) |]   \
   29.72 +\           ==> ensures Acts (C Int A) (C Int A')";
   29.73 +by (asm_simp_tac (simpset() addsimps [Int_Un_distrib RS sym,
   29.74 +				      Diff_Int_distrib RS sym,
   29.75 +				      stable_constrains_Int]) 1);
   29.76 +qed "stable_ensures_Int";
   29.77 +
   29.78 +
   29.79 +(*** leadsTo ***)
   29.80 +
   29.81 +(*Synonyms for the theorems produced by the inductive defn package*)
   29.82 +bind_thm ("leadsTo_Basis", leadsto.Basis);
   29.83 +bind_thm ("leadsTo_Trans", leadsto.Trans);
   29.84 +
   29.85 +goal thy "!!Acts. act: Acts ==> leadsTo Acts A UNIV";
   29.86 +by (blast_tac (claset() addIs [ensures_UNIV RS leadsTo_Basis]) 1);
   29.87 +qed "leadsTo_UNIV";
   29.88 +Addsimps [leadsTo_UNIV];
   29.89 +
   29.90 +(*Useful with cancellation, disjunction*)
   29.91 +goal thy "!!Acts. leadsTo Acts A (A' Un A') ==> leadsTo Acts A A'";
   29.92 +by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
   29.93 +qed "leadsTo_Un_duplicate";
   29.94 +
   29.95 +goal thy "!!Acts. leadsTo Acts A (A' Un C Un C) ==> leadsTo Acts A (A' Un C)";
   29.96 +by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
   29.97 +qed "leadsTo_Un_duplicate2";
   29.98 +
   29.99 +(*The Union introduction rule as we should have liked to state it*)
  29.100 +val prems = goal thy
  29.101 +    "(!!A. A : S ==> leadsTo Acts A B) ==> leadsTo Acts (Union S) B";
  29.102 +by (blast_tac (claset() addIs (leadsto.Union::prems)) 1);
  29.103 +qed "leadsTo_Union";
  29.104 +
  29.105 +val prems = goal thy
  29.106 +    "(!!i. i : I ==> leadsTo Acts (A i) B) ==> leadsTo Acts (UN i:I. A i) B";
  29.107 +by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
  29.108 +by (blast_tac (claset() addIs (leadsto.Union::prems)) 1);
  29.109 +qed "leadsTo_UN";
  29.110 +
  29.111 +(*Binary union introduction rule*)
  29.112 +goal thy
  29.113 +  "!!C. [| leadsTo Acts A C; leadsTo Acts B C |] ==> leadsTo Acts (A Un B) C";
  29.114 +by (stac Un_eq_Union 1);
  29.115 +by (blast_tac (claset() addIs [leadsTo_Union]) 1);
  29.116 +qed "leadsTo_Un";
  29.117 +
  29.118 +
  29.119 +(*The INDUCTION rule as we should have liked to state it*)
  29.120 +val major::prems = goal thy
  29.121 +  "[| leadsTo Acts za zb;  \
  29.122 +\     !!A B. ensures Acts A B ==> P A B; \
  29.123 +\     !!A B C. [| leadsTo Acts A B; P A B; leadsTo Acts B C; P B C |] \
  29.124 +\              ==> P A C; \
  29.125 +\     !!B S. ALL A:S. leadsTo Acts A B & P A B ==> P (Union S) B \
  29.126 +\  |] ==> P za zb";
  29.127 +br (major RS leadsto.induct) 1;
  29.128 +by (REPEAT (blast_tac (claset() addIs prems) 1));
  29.129 +qed "leadsTo_induct";
  29.130 +
  29.131 +
  29.132 +goal thy "!!A B. [| A<=B;  id: Acts |] ==> leadsTo Acts A B";
  29.133 +by (rtac leadsTo_Basis 1);
  29.134 +by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
  29.135 +by (Blast_tac 1);
  29.136 +qed "subset_imp_leadsTo";
  29.137 +
  29.138 +bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo);
  29.139 +Addsimps [empty_leadsTo];
  29.140 +
  29.141 +
  29.142 +(*There's a direct proof by leadsTo_Trans and subset_imp_leadsTo, but it
  29.143 +  needs the extra premise id:Acts*)
  29.144 +goal thy "!!Acts. leadsTo Acts A A' ==> A'<=B' --> leadsTo Acts A B'";
  29.145 +by (etac leadsTo_induct 1);
  29.146 +by (Clarify_tac 3);
  29.147 +by (blast_tac (claset() addIs [leadsTo_Union]) 3);
  29.148 +by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
  29.149 +by (blast_tac (claset() addIs [leadsTo_Basis, ensures_weaken_R]) 1);
  29.150 +qed_spec_mp "leadsTo_weaken_R";
  29.151 +
  29.152 +
  29.153 +goal thy "!!Acts. [| leadsTo Acts A A'; B<=A; id: Acts |] ==>  \
  29.154 +\                 leadsTo Acts B A'";
  29.155 +by (blast_tac (claset() addIs [leadsTo_Basis, leadsTo_Trans, 
  29.156 +			       subset_imp_leadsTo]) 1);
  29.157 +qed_spec_mp "leadsTo_weaken_L";
  29.158 +
  29.159 +(*Distributes over binary unions*)
  29.160 +goal thy
  29.161 +  "!!C. id: Acts ==> \
  29.162 +\       leadsTo Acts (A Un B) C  =  (leadsTo Acts A C & leadsTo Acts B C)";
  29.163 +by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1);
  29.164 +qed "leadsTo_Un_distrib";
  29.165 +
  29.166 +goal thy
  29.167 +  "!!C. id: Acts ==> \
  29.168 +\       leadsTo Acts (UN i:I. A i) B  =  (ALL i : I. leadsTo Acts (A i) B)";
  29.169 +by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1);
  29.170 +qed "leadsTo_UN_distrib";
  29.171 +
  29.172 +goal thy
  29.173 +  "!!C. id: Acts ==> \
  29.174 +\       leadsTo Acts (Union S) B  =  (ALL A : S. leadsTo Acts A B)";
  29.175 +by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1);
  29.176 +qed "leadsTo_Union_distrib";
  29.177 +
  29.178 +
  29.179 +goal thy
  29.180 +   "!!Acts. [| leadsTo Acts A A'; id: Acts; B<=A; A'<=B' |] \
  29.181 +\           ==> leadsTo Acts B B'";
  29.182 +(*PROOF FAILED: why?*)
  29.183 +by (blast_tac (claset() addIs [leadsTo_Trans, leadsTo_weaken_R,
  29.184 +			       leadsTo_weaken_L]) 1);
  29.185 +qed "leadsTo_weaken";
  29.186 +
  29.187 +
  29.188 +(*Set difference: maybe combine with leadsTo_weaken_L??*)
  29.189 +goal thy
  29.190 +  "!!C. [| leadsTo Acts (A-B) C; leadsTo Acts B C; id: Acts |] \
  29.191 +\       ==> leadsTo Acts A C";
  29.192 +by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1);
  29.193 +qed "leadsTo_Diff";
  29.194 +
  29.195 +
  29.196 +(** Meta or object quantifier ???
  29.197 +    see ball_constrains_UN in UNITY.ML***)
  29.198 +
  29.199 +val prems = goal thy
  29.200 +   "(!! i. i:I ==> leadsTo Acts (A i) (A' i)) \
  29.201 +\   ==> leadsTo Acts (UN i:I. A i) (UN i:I. A' i)";
  29.202 +by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
  29.203 +by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_R] 
  29.204 +                        addIs prems) 1);
  29.205 +qed "leadsTo_UN_UN";
  29.206 +
  29.207 +
  29.208 +(*Version with no index set*)
  29.209 +val prems = goal thy
  29.210 +   "(!! i. leadsTo Acts (A i) (A' i)) \
  29.211 +\   ==> leadsTo Acts (UN i. A i) (UN i. A' i)";
  29.212 +by (blast_tac (claset() addIs [leadsTo_UN_UN] 
  29.213 +                        addIs prems) 1);
  29.214 +qed "leadsTo_UN_UN_noindex";
  29.215 +
  29.216 +(*Version with no index set*)
  29.217 +goal thy
  29.218 +   "!!Acts. ALL i. leadsTo Acts (A i) (A' i) \
  29.219 +\           ==> leadsTo Acts (UN i. A i) (UN i. A' i)";
  29.220 +by (blast_tac (claset() addIs [leadsTo_UN_UN]) 1);
  29.221 +qed "all_leadsTo_UN_UN";
  29.222 +
  29.223 +
  29.224 +(*Binary union version*)
  29.225 +goal thy "!!Acts. [| leadsTo Acts A A'; leadsTo Acts B B' |] \
  29.226 +\                 ==> leadsTo Acts (A Un B) (A' Un B')";
  29.227 +by (blast_tac (claset() addIs [leadsTo_Un, 
  29.228 +			       leadsTo_weaken_R]) 1);
  29.229 +qed "leadsTo_Un_Un";
  29.230 +
  29.231 +
  29.232 +(** The cancellation law **)
  29.233 +
  29.234 +goal thy
  29.235 +   "!!Acts. [| leadsTo Acts A (A' Un B); leadsTo Acts B B'; id: Acts |] \
  29.236 +\           ==> leadsTo Acts A (A' Un B')";
  29.237 +by (blast_tac (claset() addIs [leadsTo_Un_Un, 
  29.238 +			       subset_imp_leadsTo, leadsTo_Trans]) 1);
  29.239 +qed "leadsTo_cancel2";
  29.240 +
  29.241 +goal thy
  29.242 +   "!!Acts. [| leadsTo Acts A (A' Un B); leadsTo Acts (B-A') B'; id: Acts |] \
  29.243 +\           ==> leadsTo Acts A (A' Un B')";
  29.244 +by (rtac leadsTo_cancel2 1);
  29.245 +by (assume_tac 2);
  29.246 +by (ALLGOALS Asm_simp_tac);
  29.247 +qed "leadsTo_cancel_Diff2";
  29.248 +
  29.249 +goal thy
  29.250 +   "!!Acts. [| leadsTo Acts A (B Un A'); leadsTo Acts B B'; id: Acts |] \
  29.251 +\           ==> leadsTo Acts A (B' Un A')";
  29.252 +by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
  29.253 +by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1);
  29.254 +qed "leadsTo_cancel1";
  29.255 +
  29.256 +goal thy
  29.257 +   "!!Acts. [| leadsTo Acts A (B Un A'); leadsTo Acts (B-A') B'; id: Acts |] \
  29.258 +\           ==> leadsTo Acts A (B' Un A')";
  29.259 +by (rtac leadsTo_cancel1 1);
  29.260 +by (assume_tac 2);
  29.261 +by (ALLGOALS Asm_simp_tac);
  29.262 +qed "leadsTo_cancel_Diff1";
  29.263 +
  29.264 +
  29.265 +
  29.266 +(** The impossibility law **)
  29.267 +
  29.268 +goal thy "!!Acts. leadsTo Acts A B ==> B={} --> A={}";
  29.269 +by (etac leadsTo_induct 1);
  29.270 +by (ALLGOALS Asm_simp_tac);
  29.271 +by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
  29.272 +by (Blast_tac 1);
  29.273 +val lemma = result() RS mp;
  29.274 +
  29.275 +goal thy "!!Acts. leadsTo Acts A {} ==> A={}";
  29.276 +by (blast_tac (claset() addSIs [lemma]) 1);
  29.277 +qed "leadsTo_empty";
  29.278 +
  29.279 +
  29.280 +(** PSP: Progress-Safety-Progress **)
  29.281 +
  29.282 +(*Special case of PSP: Misra's "stable conjunction".  Doesn't need id:Acts. *)
  29.283 +goalw thy [stable_def]
  29.284 +   "!!Acts. [| leadsTo Acts A A'; stable Acts B |] \
  29.285 +\           ==> leadsTo Acts (A Int B) (A' Int B)";
  29.286 +by (etac leadsTo_induct 1);
  29.287 +by (simp_tac (simpset() addsimps [Int_Union_Union]) 3);
  29.288 +by (blast_tac (claset() addIs [leadsTo_Union]) 3);
  29.289 +by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
  29.290 +by (rtac leadsTo_Basis 1);
  29.291 +by (asm_full_simp_tac
  29.292 +    (simpset() addsimps [ensures_def, 
  29.293 +			 Diff_Int_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1);
  29.294 +by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1);
  29.295 +qed "PSP_stable";
  29.296 +
  29.297 +goal thy
  29.298 +   "!!Acts. [| leadsTo Acts A A'; stable Acts B |] \
  29.299 +\           ==> leadsTo Acts (B Int A) (B Int A')";
  29.300 +by (asm_simp_tac (simpset() addsimps (PSP_stable::Int_ac)) 1);
  29.301 +qed "PSP_stable2";
  29.302 +
  29.303 +
  29.304 +goalw thy [ensures_def]
  29.305 +   "!!Acts. [| ensures Acts A A'; constrains Acts B B' |] \
  29.306 +\           ==> ensures Acts (A Int B) ((A' Int B) Un (B' - B))";
  29.307 +by Safe_tac;
  29.308 +by (blast_tac (claset() addIs [constrainsI] addDs [constrainsD]) 1);
  29.309 +by (etac transient_strengthen 1);
  29.310 +by (Blast_tac 1);
  29.311 +qed "PSP_ensures";
  29.312 +
  29.313 +
  29.314 +goal thy
  29.315 +   "!!Acts. [| leadsTo Acts A A'; constrains Acts B B'; id: Acts |] \
  29.316 +\           ==> leadsTo Acts (A Int B) ((A' Int B) Un (B' - B))";
  29.317 +by (etac leadsTo_induct 1);
  29.318 +by (simp_tac (simpset() addsimps [Int_Union_Union]) 3);
  29.319 +by (blast_tac (claset() addIs [leadsTo_Union]) 3);
  29.320 +(*Transitivity case has a delicate argument involving "cancellation"*)
  29.321 +by (rtac leadsTo_Un_duplicate2 2);
  29.322 +by (etac leadsTo_cancel_Diff1 2);
  29.323 +by (assume_tac 3);
  29.324 +by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2);
  29.325 +(*Basis case*)
  29.326 +by (blast_tac (claset() addIs [leadsTo_Basis, PSP_ensures]) 1);
  29.327 +qed "PSP";
  29.328 +
  29.329 +goal thy
  29.330 +   "!!Acts. [| leadsTo Acts A A'; constrains Acts B B'; id: Acts |] \
  29.331 +\           ==> leadsTo Acts (B Int A) ((B Int A') Un (B' - B))";
  29.332 +by (asm_simp_tac (simpset() addsimps (PSP::Int_ac)) 1);
  29.333 +qed "PSP2";
  29.334 +
  29.335 +
  29.336 +goalw thy [unless_def]
  29.337 +   "!!Acts. [| leadsTo Acts A A'; unless Acts B B'; id: Acts |] \
  29.338 +\           ==> leadsTo Acts (A Int B) ((A' Int B) Un B')";
  29.339 +by (dtac PSP 1);
  29.340 +by (assume_tac 1);
  29.341 +by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2);
  29.342 +by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 2);
  29.343 +by (etac leadsTo_Diff 2);
  29.344 +by (blast_tac (claset() addIs [subset_imp_leadsTo]) 2);
  29.345 +by Auto_tac;
  29.346 +qed "PSP_unless";
  29.347 +
  29.348 +
  29.349 +(*** Proving the induction rules ***)
  29.350 +
  29.351 +goal thy
  29.352 +   "!!Acts. [| wf r;     \
  29.353 +\              ALL m. leadsTo Acts (A Int f-``{m})                     \
  29.354 +\                                  ((A Int f-``(r^-1 ^^ {m})) Un B);   \
  29.355 +\              id: Acts |] \
  29.356 +\           ==> leadsTo Acts (A Int f-``{m}) B";
  29.357 +by (eres_inst_tac [("a","m")] wf_induct 1);
  29.358 +by (subgoal_tac "leadsTo Acts (A Int (f -`` (r^-1 ^^ {x}))) B" 1);
  29.359 +by (stac vimage_eq_UN 2);
  29.360 +by (asm_simp_tac (HOL_ss addsimps (UN_simps RL [sym])) 2);
  29.361 +by (blast_tac (claset() addIs [leadsTo_UN]) 2);
  29.362 +by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1);
  29.363 +val lemma = result();
  29.364 +
  29.365 +
  29.366 +(** Meta or object quantifier ????? **)
  29.367 +goal thy
  29.368 +   "!!Acts. [| wf r;     \
  29.369 +\              ALL m. leadsTo Acts (A Int f-``{m})                     \
  29.370 +\                                  ((A Int f-``(r^-1 ^^ {m})) Un B);   \
  29.371 +\              id: Acts |] \
  29.372 +\           ==> leadsTo Acts A B";
  29.373 +by (res_inst_tac [("t", "A")] subst 1);
  29.374 +by (rtac leadsTo_UN 2);
  29.375 +by (etac lemma 2);
  29.376 +by (REPEAT (assume_tac 2));
  29.377 +by (Fast_tac 1);    (*Blast_tac: Function unknown's argument not a parameter*)
  29.378 +qed "leadsTo_wf_induct";
  29.379 +
  29.380 +
  29.381 +goal thy
  29.382 +   "!!Acts. [| wf r;     \
  29.383 +\              ALL m:I. leadsTo Acts (A Int f-``{m})                   \
  29.384 +\                                  ((A Int f-``(r^-1 ^^ {m})) Un B);   \
  29.385 +\              id: Acts |] \
  29.386 +\           ==> leadsTo Acts A ((A - (f-``I)) Un B)";
  29.387 +by (etac leadsTo_wf_induct 1);
  29.388 +by Safe_tac;
  29.389 +by (case_tac "m:I" 1);
  29.390 +by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
  29.391 +by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
  29.392 +qed "bounded_induct";
  29.393 +
  29.394 +
  29.395 +(*Alternative proof is via the lemma leadsTo Acts (A Int f-``(lessThan m)) B*)
  29.396 +goal thy
  29.397 +   "!!Acts. [| ALL m. leadsTo Acts (A Int f-``{m})                     \
  29.398 +\                                  ((A Int f-``(lessThan m)) Un B);   \
  29.399 +\              id: Acts |] \
  29.400 +\           ==> leadsTo Acts A B";
  29.401 +by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
  29.402 +by (assume_tac 2);
  29.403 +by (Asm_simp_tac 1);
  29.404 +qed "lessThan_induct";
  29.405 +
  29.406 +goal thy
  29.407 +   "!!Acts. [| ALL m:(greaterThan l). leadsTo Acts (A Int f-``{m})   \
  29.408 +\                                        ((A Int f-``(lessThan m)) Un B);   \
  29.409 +\              id: Acts |] \
  29.410 +\           ==> leadsTo Acts A ((A Int (f-``(atMost l))) Un B)";
  29.411 +by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);
  29.412 +by (rtac (wf_less_than RS bounded_induct) 1);
  29.413 +by (assume_tac 2);
  29.414 +by (Asm_simp_tac 1);
  29.415 +qed "lessThan_bounded_induct";
  29.416 +
  29.417 +goal thy
  29.418 +   "!!Acts. [| ALL m:(lessThan l). leadsTo Acts (A Int f-``{m})   \
  29.419 +\                                    ((A Int f-``(greaterThan m)) Un B);   \
  29.420 +\              id: Acts |] \
  29.421 +\           ==> leadsTo Acts A ((A Int (f-``(atLeast l))) Un B)";
  29.422 +by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
  29.423 +    (wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1);
  29.424 +by (assume_tac 2);
  29.425 +by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
  29.426 +by (Clarify_tac 1);
  29.427 +by (case_tac "m<l" 1);
  29.428 +by (blast_tac (claset() addIs [not_leE, subset_imp_leadsTo]) 2);
  29.429 +by (blast_tac (claset() addIs [leadsTo_weaken_R, diff_less_mono2]) 1);
  29.430 +qed "greaterThan_bounded_induct";
  29.431 +
  29.432 +
  29.433 +
  29.434 +(*** wlt ****)
  29.435 +
  29.436 +(*Misra's property W3*)
  29.437 +goalw thy [wlt_def] "leadsTo Acts (wlt Acts B) B";
  29.438 +by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
  29.439 +qed "wlt_leadsTo";
  29.440 +
  29.441 +goalw thy [wlt_def] "!!Acts. leadsTo Acts A B ==> A <= wlt Acts B";
  29.442 +by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
  29.443 +qed "leadsTo_subset";
  29.444 +
  29.445 +(*Misra's property W2*)
  29.446 +goal thy "!!Acts. id: Acts ==> leadsTo Acts A B = (A <= wlt Acts B)";
  29.447 +by (blast_tac (claset() addSIs [leadsTo_subset, 
  29.448 +				wlt_leadsTo RS leadsTo_weaken_L]) 1);
  29.449 +qed "leadsTo_eq_subset_wlt";
  29.450 +
  29.451 +(*Misra's property W4*)
  29.452 +goal thy "!!Acts. id: Acts ==> B <= wlt Acts B";
  29.453 +by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS sym,
  29.454 +				      subset_imp_leadsTo]) 1);
  29.455 +qed "wlt_increasing";
  29.456 +
  29.457 +
  29.458 +(*Used in the Trans case below*)
  29.459 +goalw thy [constrains_def]
  29.460 +   "!!Acts. [| B <= A2;  \
  29.461 +\              constrains Acts (A1 - B) (A1 Un B); \
  29.462 +\              constrains Acts (A2 - C) (A2 Un C) |] \
  29.463 +\           ==> constrains Acts (A1 Un A2 - C) (A1 Un A2 Un C)";
  29.464 +by (Clarify_tac 1);
  29.465 +by (blast_tac (claset() addSDs [bspec]) 1);
  29.466 +val lemma1 = result();
  29.467 +
  29.468 +
  29.469 +(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
  29.470 +goal thy
  29.471 +   "!!Acts. [| leadsTo Acts A A';  id: Acts |] ==> \
  29.472 +\      EX B. A<=B & leadsTo Acts B A' & constrains Acts (B-A') (B Un A')";
  29.473 +by (etac leadsTo_induct 1);
  29.474 +(*Basis*)
  29.475 +by (blast_tac (claset() addIs [leadsTo_Basis]
  29.476 +                        addDs [ensuresD]) 1);
  29.477 +(*Trans*)
  29.478 +by (Clarify_tac 1);
  29.479 +by (res_inst_tac [("x", "Ba Un Bb")] exI 1);
  29.480 +by (blast_tac (claset() addIs [lemma1, leadsTo_Un_Un, leadsTo_cancel1,
  29.481 +			       leadsTo_Un_duplicate]) 1);
  29.482 +(*Union*)
  29.483 +by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1,
  29.484 +				  bchoice, ball_constrains_UN]) 1);;
  29.485 +by (res_inst_tac [("x", "UN A:S. f A")] exI 1);
  29.486 +by (blast_tac (claset() addIs [leadsTo_UN, constrains_weaken]) 1);
  29.487 +qed "leadsTo_123";
  29.488 +
  29.489 +
  29.490 +(*Misra's property W5*)
  29.491 +goal thy "!!Acts. id: Acts ==> constrains Acts (wlt Acts B - B) (wlt Acts B)";
  29.492 +by (forward_tac [wlt_leadsTo RS leadsTo_123] 1);
  29.493 +by (Clarify_tac 1);
  29.494 +by (subgoal_tac "Ba = wlt Acts B" 1);
  29.495 +by (blast_tac (claset() addDs [leadsTo_eq_subset_wlt]) 2);
  29.496 +by (Clarify_tac 1);
  29.497 +by (asm_full_simp_tac (simpset() addsimps [wlt_increasing, Un_absorb2]) 1);
  29.498 +qed "wlt_constrains_wlt";
  29.499 +
  29.500 +
  29.501 +(*** Completion: Binary and General Finite versions ***)
  29.502 +
  29.503 +goal thy
  29.504 +   "!!Acts. [| leadsTo Acts A A';  stable Acts A';   \
  29.505 +\              leadsTo Acts B B';  stable Acts B';  id: Acts |] \
  29.506 +\           ==> leadsTo Acts (A Int B) (A' Int B')";
  29.507 +by (subgoal_tac "stable Acts (wlt Acts B')" 1);
  29.508 +by (asm_full_simp_tac (simpset() addsimps [stable_def]) 2);
  29.509 +by (EVERY [etac (constrains_Un RS constrains_weaken) 2,
  29.510 +	   etac wlt_constrains_wlt 2,
  29.511 +	   fast_tac (claset() addEs [wlt_increasing RSN (2,rev_subsetD)]) 3,
  29.512 +	   Blast_tac 2]);
  29.513 +by (subgoal_tac "leadsTo Acts (A Int wlt Acts B') (A' Int wlt Acts B')" 1);
  29.514 +by (blast_tac (claset() addIs [PSP_stable]) 2);
  29.515 +by (subgoal_tac "leadsTo Acts (A' Int wlt Acts B') (A' Int B')" 1);
  29.516 +by (blast_tac (claset() addIs [wlt_leadsTo, PSP_stable2]) 2);
  29.517 +by (subgoal_tac "leadsTo Acts (A Int B) (A Int wlt Acts B')" 1);
  29.518 +by (blast_tac (claset() addIs [leadsTo_subset RS subsetD, 
  29.519 +			       subset_imp_leadsTo]) 2);
  29.520 +(*Blast_tac gives PROOF FAILED*)
  29.521 +by (best_tac (claset() addIs [leadsTo_Trans]) 1);
  29.522 +qed "stable_completion";
  29.523 +
  29.524 +
  29.525 +goal thy
  29.526 +   "!!Acts. [| finite I;  id: Acts |]                     \
  29.527 +\           ==> (ALL i:I. leadsTo Acts (A i) (A' i)) -->  \
  29.528 +\               (ALL i:I. stable Acts (A' i)) -->         \
  29.529 +\               leadsTo Acts (INT i:I. A i) (INT i:I. A' i)";
  29.530 +by (etac finite_induct 1);
  29.531 +by (Asm_simp_tac 1);
  29.532 +by (asm_simp_tac 
  29.533 +    (simpset() addsimps [stable_completion, stable_def, 
  29.534 +			 ball_constrains_INT]) 1);
  29.535 +qed_spec_mp "finite_stable_completion";
  29.536 +
  29.537 +
  29.538 +goal thy
  29.539 +   "!!Acts. [| W = wlt Acts (B' Un C);     \
  29.540 +\              leadsTo Acts A (A' Un C);  constrains Acts A' (A' Un C);   \
  29.541 +\              leadsTo Acts B (B' Un C);  constrains Acts B' (B' Un C);   \
  29.542 +\              id: Acts |] \
  29.543 +\           ==> leadsTo Acts (A Int B) ((A' Int B') Un C)";
  29.544 +by (subgoal_tac "constrains Acts (W-C) (W Un B' Un C)" 1);
  29.545 +by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt] 
  29.546 +			       MRS constrains_Un RS constrains_weaken]) 2);
  29.547 +by (subgoal_tac "constrains Acts (W-C) W" 1);
  29.548 +by (asm_full_simp_tac 
  29.549 +    (simpset() addsimps [wlt_increasing, Un_assoc, Un_absorb2]) 2);
  29.550 +by (subgoal_tac "leadsTo Acts (A Int W - C) (A' Int W Un C)" 1);
  29.551 +by (simp_tac (simpset() addsimps [Int_Diff]) 2);
  29.552 +by (blast_tac (claset() addIs [wlt_leadsTo, PSP RS leadsTo_weaken_R]) 2);
  29.553 +by (subgoal_tac "leadsTo Acts (A' Int W Un C) (A' Int B' Un C)" 1);
  29.554 +by (blast_tac (claset() addIs [wlt_leadsTo, leadsTo_Un_Un, 
  29.555 +                               PSP2 RS leadsTo_weaken_R, 
  29.556 +			       subset_refl RS subset_imp_leadsTo, 
  29.557 +			       leadsTo_Un_duplicate2]) 2);
  29.558 +by (dtac leadsTo_Diff 1);
  29.559 +by (assume_tac 2);
  29.560 +by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
  29.561 +by (subgoal_tac "A Int B <= A Int W" 1);
  29.562 +by (blast_tac (claset() addIs [leadsTo_subset, Int_mono] 
  29.563 +	                delrules [subsetI]) 2);
  29.564 +by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1);
  29.565 +bind_thm("completion", refl RS result());
  29.566 +
  29.567 +
  29.568 +goal thy
  29.569 +   "!!Acts. [| finite I;  id: Acts |] \
  29.570 +\           ==> (ALL i:I. leadsTo Acts (A i) (A' i Un C)) -->  \
  29.571 +\               (ALL i:I. constrains Acts (A' i) (A' i Un C)) --> \
  29.572 +\               leadsTo Acts (INT i:I. A i) ((INT i:I. A' i) Un C)";
  29.573 +by (etac finite_induct 1);
  29.574 +by (ALLGOALS Asm_simp_tac);
  29.575 +by (Clarify_tac 1);
  29.576 +by (dtac ball_constrains_INT 1);
  29.577 +by (asm_full_simp_tac (simpset() addsimps [completion]) 1); 
  29.578 +qed "finite_completion";
  29.579 +
    30.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    30.2 +++ b/src/HOL/UNITY/WFair.thy	Fri Apr 03 12:34:33 1998 +0200
    30.3 @@ -0,0 +1,43 @@
    30.4 +(*  Title:      HOL/UNITY/WFair
    30.5 +    ID:         $Id$
    30.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    30.7 +    Copyright   1998  University of Cambridge
    30.8 +
    30.9 +Weak Fairness versions of transient, ensures, leadsTo.
   30.10 +
   30.11 +From Misra, "A Logic for Concurrent Programming", 1994
   30.12 +*)
   30.13 +
   30.14 +WFair = Traces + Vimage +
   30.15 +
   30.16 +constdefs
   30.17 +
   30.18 +  transient :: "[('a * 'a)set set, 'a set] => bool"
   30.19 +    "transient Acts A == EX act:Acts. A <= Domain act & act^^A <= Compl A"
   30.20 +
   30.21 +  ensures :: "[('a * 'a)set set, 'a set, 'a set] => bool"
   30.22 +    "ensures Acts A B == constrains Acts (A-B) (A Un B) & transient Acts (A-B)"
   30.23 +
   30.24 +consts leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool"
   30.25 +       leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set"
   30.26 +  
   30.27 +translations
   30.28 +  "leadsTo Acts A B" == "(A,B) : leadsto Acts"
   30.29 +
   30.30 +inductive "leadsto Acts"
   30.31 +  intrs 
   30.32 +
   30.33 +    Basis  "ensures Acts A B ==> leadsTo Acts A B"
   30.34 +
   30.35 +    Trans  "[| leadsTo Acts A B;  leadsTo Acts B C |]
   30.36 +	   ==> leadsTo Acts A C"
   30.37 +
   30.38 +    Union  "(UN A:S. {(A,B)}) : Pow (leadsto Acts)
   30.39 +	   ==> leadsTo Acts (Union S) B"
   30.40 +
   30.41 +  monos "[Pow_mono]"
   30.42 +
   30.43 +constdefs wlt :: "[('a * 'a)set set, 'a set] => 'a set"
   30.44 +  "wlt Acts B == Union {A. leadsTo Acts A B}"
   30.45 +
   30.46 +end