src/HOL/UNITY/Deadlock.ML
changeset 4776 1f9362e769c1
child 5069 3ea049f7979d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/UNITY/Deadlock.ML	Fri Apr 03 12:34:33 1998 +0200
     1.3 @@ -0,0 +1,90 @@
     1.4 +
     1.5 +
     1.6 +(*** Deadlock examples from section 5.6 ***)
     1.7 +
     1.8 +(*Trivial, two-process case*)
     1.9 +goalw thy [constrains_def, stable_def]
    1.10 +    "!!Acts. [| constrains Acts (A Int B) A;  constrains Acts (B Int A) B |] \
    1.11 +\           ==> stable Acts (A Int B)";
    1.12 +by (Blast_tac 1);
    1.13 +result();
    1.14 +
    1.15 +
    1.16 +goal thy "{i. i < Suc n} = insert n {i. i < n}";
    1.17 +by (blast_tac (claset() addSEs [less_SucE] addIs [less_SucI]) 1);
    1.18 +qed "Collect_less_Suc_insert";
    1.19 +
    1.20 +
    1.21 +goal thy "{i. i <= Suc n} = insert (Suc n) {i. i <= n}";
    1.22 +by (blast_tac (claset() addSEs [le_SucE] addIs [le_SucI]) 1);
    1.23 +qed "Collect_le_Suc_insert";
    1.24 +
    1.25 +
    1.26 +(*a simplification step*)
    1.27 +goal thy "(INT i:{i. i <= n}. A(Suc i) Int A i) = \
    1.28 +\         (INT i:{i. i <= Suc n}. A i)";
    1.29 +by (induct_tac "n" 1);
    1.30 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [Collect_le_Suc_insert])));
    1.31 +by (blast_tac (claset() addEs [le_SucE] addSEs [equalityE]) 1);
    1.32 +qed "Collect_le_Int_equals";
    1.33 +
    1.34 +
    1.35 +(*Dual of the required property.  Converse inclusion fails.*)
    1.36 +goal thy "(UN i:{i. i < n}. A i) Int Compl (A n) <=  \
    1.37 +\         (UN i:{i. i < n}. (A i) Int Compl (A(Suc i)))";
    1.38 +by (induct_tac "n" 1);
    1.39 +by (Asm_simp_tac 1);
    1.40 +by (simp_tac (simpset() addsimps [Collect_less_Suc_insert]) 1);
    1.41 +by (Blast_tac 1);
    1.42 +qed "UN_Int_Compl_subset";
    1.43 +
    1.44 +
    1.45 +(*Converse inclusion fails.*)
    1.46 +goal thy "(INT i:{i. i < n}. Compl(A i) Un A (Suc i))  <= \
    1.47 +\         (INT i:{i. i < n}. Compl(A i)) Un A n";
    1.48 +by (induct_tac "n" 1);
    1.49 +by (Asm_simp_tac 1);
    1.50 +by (asm_simp_tac (simpset() addsimps [Collect_less_Suc_insert]) 1);
    1.51 +by (Blast_tac 1);
    1.52 +qed "INT_Un_Compl_subset";
    1.53 +
    1.54 +
    1.55 +(*Specialized rewriting*)
    1.56 +goal thy "A 0 Int (Compl (A n) Int \
    1.57 +\                  (INT i:{i. i < n}. Compl(A i) Un A (Suc i))) = {}";
    1.58 +by (blast_tac (claset() addIs [gr0I]
    1.59 +		        addDs [impOfSubs INT_Un_Compl_subset]) 1);
    1.60 +val lemma = result();
    1.61 +
    1.62 +(*Reverse direction makes it harder to invoke the ind hyp*)
    1.63 +goal thy "(INT i:{i. i <= n}. A i) = \
    1.64 +\         A 0 Int (INT i:{i. i < n}. Compl(A i) Un A(Suc i))";
    1.65 +by (induct_tac "n" 1);
    1.66 +by (Asm_simp_tac 1);
    1.67 +by (asm_simp_tac
    1.68 +    (simpset() addsimps (Int_ac @
    1.69 +			 [Int_Un_distrib, Int_Un_distrib2, lemma,
    1.70 +			  Collect_less_Suc_insert, Collect_le_Suc_insert])) 1);
    1.71 +qed "INT_le_equals_Int";
    1.72 +
    1.73 +goal thy "(INT i:{i. i <= Suc n}. A i) = \
    1.74 +\         A 0 Int (INT i:{i. i <= n}. Compl(A i) Un A(Suc i))";
    1.75 +by (simp_tac (simpset() addsimps [le_eq_less_Suc RS sym, 
    1.76 +				  INT_le_equals_Int]) 1);
    1.77 +qed "INT_le_Suc_equals_Int";
    1.78 +
    1.79 +
    1.80 +(*The final deadlock example*)
    1.81 +val [zeroprem, allprem] = goalw thy [stable_def]
    1.82 +    "[| constrains Acts (A 0 Int A (Suc n)) (A 0);  \
    1.83 +\       ALL i:{i. i <= n}. constrains Acts (A(Suc i) Int A i) \
    1.84 +\                                         (Compl(A i) Un A(Suc i)) |] \
    1.85 +\    ==> stable Acts (INT i:{i. i <= Suc n}. A i)";
    1.86 +
    1.87 +by (rtac ([zeroprem, allprem RS ball_constrains_INT] MRS 
    1.88 +    constrains_Int RS constrains_weaken) 1);
    1.89 +by (simp_tac (simpset() addsimps [Collect_le_Int_equals, 
    1.90 +				  Int_assoc, INT_absorb]) 1);
    1.91 +by (simp_tac (simpset() addsimps ([INT_le_Suc_equals_Int])) 1);
    1.92 +result();
    1.93 +