src/HOL/UNITY/Token.ML
author paulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 4776 1f9362e769c1
child 5069 3ea049f7979d
permissions -rw-r--r--
New UNITY theory
paulson@4776
     1
(*  Title:      HOL/UNITY/Token
paulson@4776
     2
    ID:         $Id$
paulson@4776
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4776
     4
    Copyright   1998  University of Cambridge
paulson@4776
     5
paulson@4776
     6
The Token Ring.
paulson@4776
     7
paulson@4776
     8
From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
paulson@4776
     9
*)
paulson@4776
    10
paulson@4776
    11
paulson@4776
    12
open Token;
paulson@4776
    13
paulson@4776
    14
paulson@4776
    15
val Token_defs = [WellTyped_def, Token_def, HasTok_def, H_def, E_def, T_def];
paulson@4776
    16
paulson@4776
    17
AddIffs [N_positive, skip];
paulson@4776
    18
paulson@4776
    19
goalw thy [HasTok_def] "!!i. [| s: HasTok i; s: HasTok j |] ==> i=j";
paulson@4776
    20
by Auto_tac;
paulson@4776
    21
qed "HasToK_partition";
paulson@4776
    22
paulson@4776
    23
goalw thy Token_defs "!!s. s : WellTyped ==> (s ~: E i) = (s : H i | s : T i)";
paulson@4776
    24
by (Simp_tac 1);
paulson@4776
    25
by (exhaust_tac "s (Suc i)" 1);
paulson@4776
    26
by Auto_tac;
paulson@4776
    27
qed "not_E_eq";
paulson@4776
    28
paulson@4776
    29
(** We should be able to prove WellTyped as a separate Invariant.  Then
paulson@4776
    30
    the Invariant rule should let us assume that the initial
paulson@4776
    31
    state is reachable, and therefore contained in any Invariant.  Then
paulson@4776
    32
    we'd not have to mention WellTyped in the statement of this theorem.
paulson@4776
    33
**)
paulson@4776
    34
paulson@4776
    35
goalw thy [stable_def]
paulson@4776
    36
    "stable Acts (WellTyped Int {s. s : E i --> s : HasTok i})";
paulson@4776
    37
by (rtac (stable_WT RS stable_constrains_Int) 1);
paulson@4776
    38
by (cut_facts_tac [TR2,TR4,TR5] 1);
paulson@4776
    39
by (asm_full_simp_tac (simpset() addsimps [constrains_def]) 1);
paulson@4776
    40
by (REPEAT_FIRST (rtac ballI ORELSE' (dtac bspec THEN' assume_tac)));
paulson@4776
    41
by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
paulson@4776
    42
by (case_tac "xa : HasTok i" 1);
paulson@4776
    43
by (auto_tac (claset(), simpset() addsimps [H_def, E_def, T_def]));
paulson@4776
    44
qed "token_stable";
paulson@4776
    45
paulson@4776
    46
(*This proof is in the "massaging" style and is much faster! *)
paulson@4776
    47
goalw thy [stable_def]
paulson@4776
    48
    "stable Acts (WellTyped Int (Compl(E i) Un (HasTok i)))";
paulson@4776
    49
by (rtac (stable_WT RS stable_constrains_Int) 1);
paulson@4776
    50
by (rtac constrains_weaken 1);
paulson@4776
    51
by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1);
paulson@4776
    52
by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
paulson@4776
    53
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [H_def, E_def, T_def])));
paulson@4776
    54
qed "token_stable";
paulson@4776
    55
paulson@4776
    56
paulson@4776
    57
(*** Progress under weak fairness ***)
paulson@4776
    58
paulson@4776
    59
goalw thy [nodeOrder_def] "wf(nodeOrder j)";
paulson@4776
    60
by (rtac (wf_less_than RS wf_inv_image RS wf_subset) 1);
paulson@4776
    61
by (Blast_tac 1);
paulson@4776
    62
qed"wf_nodeOrder";
paulson@4776
    63
paulson@4776
    64
    goal thy "!!m. [| m<n; Suc m ~= n |] ==> Suc(m) < n";
paulson@4776
    65
    by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1);
paulson@4776
    66
    by (blast_tac (claset() addEs [less_asym, less_SucE]) 1);
paulson@4776
    67
    qed "Suc_lessI";
paulson@4776
    68
paulson@4776
    69
goalw thy [nodeOrder_def, next_def, inv_image_def]
paulson@4776
    70
    "!!x. [| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)";
paulson@4776
    71
by (auto_tac (claset(),
paulson@4776
    72
	      simpset() addsimps [Suc_lessI, mod_Suc, mod_less, mod_geq]));
paulson@4776
    73
by (dtac sym 1);
paulson@4776
    74
(*The next two lines...**)
paulson@4776
    75
by (REPEAT (eres_inst_tac [("P", "?a<N")] rev_mp 1));
paulson@4776
    76
by (etac ssubst 1);
paulson@4776
    77
(*were with the previous version of asm_full_simp_tac...
paulson@4776
    78
  by (rotate_tac ~1 1);
paulson@4776
    79
*)
paulson@4776
    80
by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv, mod_Suc, mod_less]) 1);
paulson@4776
    81
by (subgoal_tac "(j + N - i) = Suc (j + N - Suc i)" 1);
paulson@4776
    82
by (asm_simp_tac (simpset() addsimps [Suc_diff_Suc, less_imp_le, Suc_leI, 
paulson@4776
    83
                                      diff_add_assoc]) 2);
paulson@4776
    84
by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1);
paulson@4776
    85
by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc]) 1);
paulson@4776
    86
(*including less_asym here would slow things down*)
paulson@4776
    87
by (auto_tac (claset() delrules [notI], 
paulson@4776
    88
              simpset() addsimps [diff_add_assoc2, Suc_leI,
paulson@4776
    89
                                  less_imp_diff_less, 
paulson@4776
    90
                                  mod_less, mod_geq, nat_neq_iff]));
paulson@4776
    91
by (REPEAT (blast_tac (claset() addEs [less_asym]) 3));
paulson@4776
    92
by (asm_simp_tac (simpset() addsimps [less_imp_diff_less,
paulson@4776
    93
				      Suc_diff_n RS sym]) 1);
paulson@4776
    94
by (asm_simp_tac (simpset() addsimps [add_diff_less, mod_less]) 1);
paulson@4776
    95
by (etac subst 1);
paulson@4776
    96
by (asm_simp_tac (simpset() addsimps [add_diff_less]) 1);
paulson@4776
    97
qed "nodeOrder_eq";
paulson@4776
    98
paulson@4776
    99
paulson@4776
   100
(*From "A Logic for Concurrent Programming", but not used in Chapter 4.
paulson@4776
   101
  Note the use of case_tac.  Reasoning about leadsTo takes practice!*)
paulson@4776
   102
goal thy
paulson@4776
   103
 "!!i. [| i<N; j<N |] ==> \
paulson@4776
   104
\      leadsTo Acts (HasTok i) ({s. (Token s, i) : nodeOrder j} Un HasTok j)";
paulson@4776
   105
by (case_tac "i=j" 1);
paulson@4776
   106
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
paulson@4776
   107
by (rtac (TR7 RS leadsTo_weaken_R) 1);
paulson@4776
   108
by (Clarify_tac 1);
paulson@4776
   109
by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
paulson@4776
   110
qed "TR7_nodeOrder";
paulson@4776
   111
paulson@4776
   112
paulson@4776
   113
(*Chapter 4 variant, the one actually used below.*)
paulson@4776
   114
goal thy
paulson@4776
   115
 "!!i. [| i<N; j<N; i~=j |] ==> \
paulson@4776
   116
\      leadsTo Acts (HasTok i) {s. (Token s, i) : nodeOrder j}";
paulson@4776
   117
by (rtac (TR7 RS leadsTo_weaken_R) 1);
paulson@4776
   118
by (Clarify_tac 1);
paulson@4776
   119
by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
paulson@4776
   120
qed "TR7_aux";
paulson@4776
   121
paulson@4776
   122
goal thy "({s. Token s < N} Int Token -`` {m}) = \
paulson@4776
   123
\         (if m<N then Token -`` {m} else {})";
paulson@4776
   124
by Auto_tac;
paulson@4776
   125
val Token_lemma = result();
paulson@4776
   126
paulson@4776
   127
paulson@4776
   128
(*Misra's TR9: the token reaches an arbitrary node*)
paulson@4776
   129
goal thy
paulson@4776
   130
 "!!i. j<N ==> leadsTo Acts {s. Token s < N} (HasTok j)";
paulson@4776
   131
by (rtac leadsTo_weaken_R 1);
paulson@4776
   132
by (res_inst_tac [("I", "Compl{j}"), ("f", "Token"), ("B", "{}")]
paulson@4776
   133
     (wf_nodeOrder RS bounded_induct) 1);
paulson@4776
   134
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Token_lemma, vimage_Diff,
paulson@4776
   135
						HasTok_def])));
paulson@4776
   136
by (Blast_tac 2);
paulson@4776
   137
by (Clarify_tac 1);
paulson@4776
   138
by (rtac (TR7_aux RS leadsTo_weaken) 1);
paulson@4776
   139
by (ALLGOALS (asm_simp_tac (simpset() addsimps [nodeOrder_def, HasTok_def])));
paulson@4776
   140
by (ALLGOALS Blast_tac);
paulson@4776
   141
qed "leadsTo_j";
paulson@4776
   142
paulson@4776
   143
(*Misra's TR8: a hungry process eventually eats*)
paulson@4776
   144
goal thy "!!i. j<N ==> leadsTo Acts ({s. Token s < N} Int H j) (E j)";
paulson@4776
   145
by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1);
paulson@4776
   146
by (rtac TR6 2);
paulson@4776
   147
by (rtac leadsTo_weaken_R 1);
paulson@4776
   148
by (rtac ([leadsTo_j, TR3] MRS PSP) 1);
paulson@4776
   149
by (ALLGOALS Blast_tac);
paulson@4776
   150
qed "Token_progress";