src/ZF/UNITY/Mutex.ML
author paulson
Fri, 10 Oct 2003 17:39:33 +0200
changeset 14228 a1956417c6c1
parent 14092 68da54626309
permissions -rw-r--r--
trivial
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     1
(*  Title:      ZF/UNITY/Mutex.ML
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
     2
    ID:         $Id \\<in> Mutex.ML,v 1.4 2003/05/27 09:39:05 paulson Exp $
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     3
    Author:     Sidi O Ehmety, Computer Laboratory
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     4
    Copyright   2001  University of Cambridge
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     5
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     6
Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
     7
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
     8
Variables' types are introduced globally so that type verification
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
     9
reduces to the usual ZF typechecking \\<in> an ill-tyed expression will
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    10
reduce to the empty set.
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    11
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    12
*)
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    13
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    14
(** Variables' types **)
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    15
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    16
Addsimps  [p_type, u_type, v_type, m_type, n_type];
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    17
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
    18
Goalw [state_def] "s \\<in> state ==>s`u \\<in> bool";
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    19
by (dres_inst_tac [("a", "u")] apply_type 1);
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    20
by Auto_tac;
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    21
qed "u_value_type";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    22
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
    23
Goalw [state_def] "s \\<in> state ==> s`v \\<in> bool";
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    24
by (dres_inst_tac [("a", "v")] apply_type 1);
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    25
by Auto_tac;
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    26
qed "v_value_type";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    27
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
    28
Goalw [state_def] "s \\<in> state ==> s`p \\<in> bool";
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    29
by (dres_inst_tac [("a", "p")] apply_type 1);
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    30
by Auto_tac;
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    31
qed "p_value_type";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    32
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
    33
Goalw [state_def] "s \\<in> state ==> s`m \\<in> int";
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    34
by (dres_inst_tac [("a", "m")] apply_type 1);
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    35
by Auto_tac;
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    36
qed "m_value_type";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    37
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
    38
Goalw [state_def] "s \\<in> state ==>s`n \\<in> int";
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    39
by (dres_inst_tac [("a", "n")] apply_type 1);
12195
ed2893765a08 *** empty log message ***
ehmety
parents: 11479
diff changeset
    40
by Auto_tac;
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    41
qed "n_value_type";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    42
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    43
Addsimps [p_value_type, u_value_type, v_value_type,
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    44
          m_value_type, n_value_type];
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    45
AddTCs [p_value_type, u_value_type, v_value_type,
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    46
          m_value_type, n_value_type];
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    47
(** Mutex is a program **)
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    48
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
    49
Goalw [Mutex_def] "Mutex \\<in> program";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    50
by Auto_tac;
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    51
qed "Mutex_in_program";
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    52
Addsimps [Mutex_in_program];
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    53
AddTCs [Mutex_in_program];
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    54
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    55
Addsimps [Mutex_def RS def_prg_Init];
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    56
program_defs_ref := [Mutex_def];
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    57
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    58
Addsimps (map simp_of_act
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    59
          [U0_def, U1_def, U2_def, U3_def, U4_def, 
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    60
           V0_def, V1_def, V2_def, V3_def, V4_def]);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    61
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    62
Addsimps (map simp_of_set [U0_def, U1_def, U2_def, U3_def, U4_def, 
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    63
           V0_def, V1_def, V2_def, V3_def, V4_def]);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    64
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    65
Addsimps (map simp_of_set [IU_def, IV_def, bad_IU_def]);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    66
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
    67
Goal "Mutex \\<in> Always(IU)";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    68
by (always_tac 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    69
by Auto_tac;
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    70
qed "IU";
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    71
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
    72
Goal "Mutex \\<in> Always(IV)";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    73
by (always_tac 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    74
qed "IV";
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    75
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
    76
(*The safety property \\<in> mutual exclusion*)
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
    77
Goal "Mutex \\<in> Always({s \\<in> state. ~(s`m = #3 & s`n = #3)})";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    78
by (rtac ([IU, IV] MRS Always_Int_I RS Always_weaken) 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    79
by Auto_tac;
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    80
qed "mutual_exclusion";
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    81
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    82
(*The bad invariant FAILS in V1*)
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    83
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    84
Goal "[| x$<#1; #3 $<= x |] ==> P";
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    85
by (dres_inst_tac [("j", "#1"), ("k", "#3")]  zless_zle_trans 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    86
by (dres_inst_tac [("j", "x")]  zle_zless_trans 2);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    87
by Auto_tac;
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    88
qed "less_lemma";
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    89
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
    90
Goal "Mutex \\<in> Always(bad_IU)";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    91
by (always_tac 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    92
by (auto_tac (claset(), simpset() addsimps [not_zle_iff_zless]));
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
    93
by (auto_tac (claset(), simpset() addsimps [bool_def]));
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    94
by (subgoal_tac "#1 $<= #3" 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    95
by (dres_inst_tac [("x", "#1"), ("y", "#3")] zle_trans 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    96
by Auto_tac;
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    97
by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
    98
by Auto_tac;
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
    99
(*Resulting state \\<in> n=1, p=false, m=4, u=false.  
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   100
  Execution of V1 (the command of process v guarded by n=1) sets p:=true,
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   101
  violating the invariant!*)
14228
a1956417c6c1 trivial
paulson
parents: 14092
diff changeset
   102
(*Check that subgoals remain: proof failed.*)
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   103
getgoal 1;
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   104
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   105
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   106
(*** Progress for U ***)
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   107
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   108
Goalw [Unless_def] 
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
   109
"Mutex \\<in> {s \\<in> state. s`m=#2} Unless {s \\<in> state. s`m=#3}";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   110
by (constrains_tac 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   111
qed "U_F0";
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   112
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
   113
Goal "Mutex \\<in> {s \\<in> state. s`m=#1} LeadsTo {s \\<in> state. s`p = s`v & s`m = #2}";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   114
by (ensures_tac "U1" 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   115
qed "U_F1";
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   116
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
   117
Goal "Mutex \\<in> {s \\<in> state. s`p =0 & s`m = #2} LeadsTo {s \\<in> state. s`m = #3}";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   118
by (cut_facts_tac [IU] 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   119
by (ensures_tac "U2" 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   120
qed "U_F2";
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   121
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
   122
Goal "Mutex \\<in> {s \\<in> state. s`m = #3} LeadsTo {s \\<in> state. s`p=1}";
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
   123
by (res_inst_tac [("B", "{s \\<in> state. s`m = #4}")] LeadsTo_Trans 1);
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   124
by (ensures_tac "U4" 2);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   125
by (ensures_tac "U3" 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   126
qed "U_F3";
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   127
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   128
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
   129
Goal "Mutex \\<in> {s \\<in> state. s`m = #2} LeadsTo {s \\<in> state. s`p=1}";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   130
by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] 
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   131
          MRS LeadsTo_Diff) 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   132
by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   133
by Auto_tac;
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
   134
by (auto_tac (claset() addSDs [p_value_type], simpset() addsimps [bool_def]));
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   135
val U_lemma2 = result();
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   136
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
   137
Goal "Mutex \\<in> {s \\<in> state. s`m = #1} LeadsTo {s \\<in> state. s`p =1}";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   138
by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   139
by Auto_tac;
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   140
val U_lemma1 = result();
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   141
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
   142
Goal "i \\<in> int ==> (#1 $<= i & i $<= #3) <-> (i=#1 | i=#2 | i=#3)";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   143
by Auto_tac;
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   144
by (auto_tac (claset(), simpset() addsimps [neq_iff_zless]));
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   145
by (dres_inst_tac [("j", "#3"), ("i", "i")] zle_zless_trans 4);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   146
by (dres_inst_tac [("j", "i"), ("i", "#1")] zle_zless_trans 2);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   147
by (dres_inst_tac [("j", "i"), ("i", "#1")] zle_zless_trans 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   148
by Auto_tac;
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   149
by (rtac zle_anti_sym 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   150
by (ALLGOALS(asm_simp_tac (simpset()
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   151
      addsimps [zless_add1_iff_zle RS iff_sym])));
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   152
qed "eq_123";
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   153
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   154
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
   155
Goal "Mutex \\<in> {s \\<in> state. #1 $<= s`m & s`m $<= #3} LeadsTo {s \\<in> state. s`p=1}";
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
   156
by (simp_tac (simpset() addsimps [m_value_type RS eq_123, Collect_disj_eq,
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   157
                                  LeadsTo_Un_distrib,
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   158
                                  U_lemma1, U_lemma2, U_F3] ) 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   159
val U_lemma123 = result();
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   160
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   161
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   162
(*Misra's F4*)
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
   163
Goal "Mutex \\<in> {s \\<in> state. s`u = 1} LeadsTo {s \\<in> state. s`p=1}";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   164
by (rtac ([IU, U_lemma123] MRS Always_LeadsTo_weaken) 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   165
by Auto_tac;
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   166
qed "u_Leadsto_p";
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   167
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   168
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   169
(*** Progress for V ***)
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   170
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   171
Goalw [Unless_def] 
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
   172
"Mutex \\<in> {s \\<in> state. s`n=#2} Unless {s \\<in> state. s`n=#3}";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   173
by (constrains_tac 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   174
qed "V_F0";
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   175
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
   176
Goal "Mutex \\<in> {s \\<in> state. s`n=#1} LeadsTo {s \\<in> state. s`p = not(s`u) & s`n = #2}";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   177
by (ensures_tac "V1" 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   178
qed "V_F1";
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   179
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
   180
Goal "Mutex \\<in> {s \\<in> state. s`p=1 & s`n = #2} LeadsTo {s \\<in> state. s`n = #3}";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   181
by (cut_facts_tac [IV] 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   182
by (ensures_tac "V2" 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   183
qed "V_F2";
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   184
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
   185
Goal "Mutex \\<in> {s \\<in> state. s`n = #3} LeadsTo {s \\<in> state. s`p=0}";
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
   186
by (res_inst_tac [("B", "{s \\<in> state. s`n = #4}")] LeadsTo_Trans 1);
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   187
by (ensures_tac "V4" 2);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   188
by (ensures_tac "V3" 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   189
qed "V_F3";
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   190
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
   191
Goal "Mutex \\<in> {s \\<in> state. s`n = #2} LeadsTo {s \\<in> state. s`p=0}";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   192
by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] 
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   193
          MRS LeadsTo_Diff) 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   194
by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   195
by Auto_tac;
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
   196
by (auto_tac (claset() addSDs [p_value_type], simpset() addsimps [bool_def]));
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   197
val V_lemma2 = result();
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   198
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
   199
Goal "Mutex \\<in> {s \\<in> state. s`n = #1} LeadsTo {s \\<in> state. s`p = 0}";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   200
by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   201
by Auto_tac;
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   202
val V_lemma1 = result();
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   203
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
   204
Goal "Mutex \\<in> {s \\<in> state. #1 $<= s`n & s`n $<= #3} LeadsTo {s \\<in> state. s`p = 0}";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   205
by (simp_tac (simpset() addsimps 
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
   206
     [n_value_type RS eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   207
                  V_lemma1, V_lemma2, V_F3] ) 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   208
val V_lemma123 = result();
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   209
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   210
(*Misra's F4*)
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
   211
Goal "Mutex \\<in> {s \\<in> state. s`v = 1} LeadsTo {s \\<in> state. s`p = 0}";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   212
by (rtac ([IV, V_lemma123] MRS Always_LeadsTo_weaken) 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   213
by Auto_tac;
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   214
qed "v_Leadsto_not_p";
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   215
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   216
(** Absence of starvation **)
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   217
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   218
(*Misra's F6*)
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
   219
Goal "Mutex \\<in> {s \\<in> state. s`m = #1} LeadsTo {s \\<in> state. s`m = #3}";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   220
by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   221
by (rtac U_F2 2);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   222
by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   223
by (stac Un_commute 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   224
by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   225
by (rtac ([v_Leadsto_not_p, U_F0] MRS PSP_Unless) 2);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   226
by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   227
by Auto_tac;
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
   228
by (auto_tac (claset() addSDs [v_value_type], simpset() addsimps [bool_def]));
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   229
qed "m1_Leadsto_3";
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   230
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   231
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   232
(*The same for V*)
14092
68da54626309 Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents: 14046
diff changeset
   233
Goal "Mutex \\<in> {s \\<in> state. s`n = #1} LeadsTo {s \\<in> state. s`n = #3}";
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   234
by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   235
by (rtac V_F2 2);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   236
by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   237
by (stac Un_commute 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   238
by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   239
by (rtac ([u_Leadsto_p, V_F0] MRS PSP_Unless) 2);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   240
by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   241
by Auto_tac;
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 12195
diff changeset
   242
by (auto_tac (claset() addSDs [u_value_type], simpset() addsimps [bool_def]));
11479
697dcaaf478f new ZF/UNITY theory
paulson
parents:
diff changeset
   243
qed "n1_Leadsto_3";