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