src/HOL/UNITY/Mutex.ML
changeset 7543 abefbd41bd3e
parent 7403 c318acb88251
child 8355 04d0f732e24e
equal deleted inserted replaced
7542:b6599e292011 7543:abefbd41bd3e
    25 qed "IV";
    25 qed "IV";
    26 
    26 
    27 (*The safety property: mutual exclusion*)
    27 (*The safety property: mutual exclusion*)
    28 Goal "Mutex : Always {s. ~ (m s = #3 & n s = #3)}";
    28 Goal "Mutex : Always {s. ~ (m s = #3 & n s = #3)}";
    29 by (rtac Always_weaken 1);
    29 by (rtac Always_weaken 1);
    30 by (rtac ([IU, IV] MRS Always_Int) 1);
    30 by (rtac ([IU, IV] MRS Always_Int_I) 1);
    31 by Auto_tac;
    31 by Auto_tac;
    32 qed "mutual_exclusion";
    32 qed "mutual_exclusion";
    33 
    33 
    34 
    34 
    35 (*The bad invariant FAILS in V1*)
    35 (*The bad invariant FAILS in V1*)