src/HOL/UNITY/Token.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/Token.ML	Fri Apr 03 12:34:33 1998 +0200
1.3 @@ -0,0 +1,150 @@
1.4 +(*  Title:      HOL/UNITY/Token
1.5 +    ID:         \$Id\$
1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.7 +    Copyright   1998  University of Cambridge
1.8 +
1.9 +The Token Ring.
1.10 +
1.11 +From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
1.12 +*)
1.13 +
1.14 +
1.15 +open Token;
1.16 +
1.17 +
1.18 +val Token_defs = [WellTyped_def, Token_def, HasTok_def, H_def, E_def, T_def];
1.19 +
1.21 +
1.22 +goalw thy [HasTok_def] "!!i. [| s: HasTok i; s: HasTok j |] ==> i=j";
1.23 +by Auto_tac;
1.24 +qed "HasToK_partition";
1.25 +
1.26 +goalw thy Token_defs "!!s. s : WellTyped ==> (s ~: E i) = (s : H i | s : T i)";
1.27 +by (Simp_tac 1);
1.28 +by (exhaust_tac "s (Suc i)" 1);
1.29 +by Auto_tac;
1.30 +qed "not_E_eq";
1.31 +
1.32 +(** We should be able to prove WellTyped as a separate Invariant.  Then
1.33 +    the Invariant rule should let us assume that the initial
1.34 +    state is reachable, and therefore contained in any Invariant.  Then
1.35 +    we'd not have to mention WellTyped in the statement of this theorem.
1.36 +**)
1.37 +
1.38 +goalw thy [stable_def]
1.39 +    "stable Acts (WellTyped Int {s. s : E i --> s : HasTok i})";
1.40 +by (rtac (stable_WT RS stable_constrains_Int) 1);
1.41 +by (cut_facts_tac [TR2,TR4,TR5] 1);
1.42 +by (asm_full_simp_tac (simpset() addsimps [constrains_def]) 1);
1.43 +by (REPEAT_FIRST (rtac ballI ORELSE' (dtac bspec THEN' assume_tac)));
1.44 +by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
1.45 +by (case_tac "xa : HasTok i" 1);
1.46 +by (auto_tac (claset(), simpset() addsimps [H_def, E_def, T_def]));
1.47 +qed "token_stable";
1.48 +
1.49 +(*This proof is in the "massaging" style and is much faster! *)
1.50 +goalw thy [stable_def]
1.51 +    "stable Acts (WellTyped Int (Compl(E i) Un (HasTok i)))";
1.52 +by (rtac (stable_WT RS stable_constrains_Int) 1);
1.53 +by (rtac constrains_weaken 1);
1.54 +by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1);
1.55 +by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
1.56 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [H_def, E_def, T_def])));
1.57 +qed "token_stable";
1.58 +
1.59 +
1.60 +(*** Progress under weak fairness ***)
1.61 +
1.62 +goalw thy [nodeOrder_def] "wf(nodeOrder j)";
1.63 +by (rtac (wf_less_than RS wf_inv_image RS wf_subset) 1);
1.64 +by (Blast_tac 1);
1.65 +qed"wf_nodeOrder";
1.66 +
1.67 +    goal thy "!!m. [| m<n; Suc m ~= n |] ==> Suc(m) < n";
1.68 +    by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1);
1.69 +    by (blast_tac (claset() addEs [less_asym, less_SucE]) 1);
1.70 +    qed "Suc_lessI";
1.71 +
1.72 +goalw thy [nodeOrder_def, next_def, inv_image_def]
1.73 +    "!!x. [| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)";
1.74 +by (auto_tac (claset(),
1.75 +	      simpset() addsimps [Suc_lessI, mod_Suc, mod_less, mod_geq]));
1.76 +by (dtac sym 1);
1.77 +(*The next two lines...**)
1.78 +by (REPEAT (eres_inst_tac [("P", "?a<N")] rev_mp 1));
1.79 +by (etac ssubst 1);
1.80 +(*were with the previous version of asm_full_simp_tac...
1.81 +  by (rotate_tac ~1 1);
1.82 +*)
1.83 +by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv, mod_Suc, mod_less]) 1);
1.84 +by (subgoal_tac "(j + N - i) = Suc (j + N - Suc i)" 1);
1.85 +by (asm_simp_tac (simpset() addsimps [Suc_diff_Suc, less_imp_le, Suc_leI,
1.87 +by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1);
1.88 +by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc]) 1);
1.89 +(*including less_asym here would slow things down*)
1.90 +by (auto_tac (claset() delrules [notI],
1.92 +                                  less_imp_diff_less,
1.93 +                                  mod_less, mod_geq, nat_neq_iff]));
1.94 +by (REPEAT (blast_tac (claset() addEs [less_asym]) 3));
1.95 +by (asm_simp_tac (simpset() addsimps [less_imp_diff_less,
1.96 +				      Suc_diff_n RS sym]) 1);
1.98 +by (etac subst 1);
1.100 +qed "nodeOrder_eq";
1.101 +
1.102 +
1.103 +(*From "A Logic for Concurrent Programming", but not used in Chapter 4.
1.104 +  Note the use of case_tac.  Reasoning about leadsTo takes practice!*)
1.105 +goal thy
1.106 + "!!i. [| i<N; j<N |] ==> \
1.107 +\      leadsTo Acts (HasTok i) ({s. (Token s, i) : nodeOrder j} Un HasTok j)";
1.108 +by (case_tac "i=j" 1);
1.110 +by (rtac (TR7 RS leadsTo_weaken_R) 1);
1.111 +by (Clarify_tac 1);
1.112 +by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
1.113 +qed "TR7_nodeOrder";
1.114 +
1.115 +
1.116 +(*Chapter 4 variant, the one actually used below.*)
1.117 +goal thy
1.118 + "!!i. [| i<N; j<N; i~=j |] ==> \
1.119 +\      leadsTo Acts (HasTok i) {s. (Token s, i) : nodeOrder j}";
1.120 +by (rtac (TR7 RS leadsTo_weaken_R) 1);
1.121 +by (Clarify_tac 1);
1.122 +by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
1.123 +qed "TR7_aux";
1.124 +
1.125 +goal thy "({s. Token s < N} Int Token -`` {m}) = \
1.126 +\         (if m<N then Token -`` {m} else {})";
1.127 +by Auto_tac;
1.128 +val Token_lemma = result();
1.129 +
1.130 +
1.131 +(*Misra's TR9: the token reaches an arbitrary node*)
1.132 +goal thy
1.133 + "!!i. j<N ==> leadsTo Acts {s. Token s < N} (HasTok j)";
1.135 +by (res_inst_tac [("I", "Compl{j}"), ("f", "Token"), ("B", "{}")]
1.136 +     (wf_nodeOrder RS bounded_induct) 1);
1.137 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [Token_lemma, vimage_Diff,
1.138 +						HasTok_def])));
1.139 +by (Blast_tac 2);
1.140 +by (Clarify_tac 1);
1.141 +by (rtac (TR7_aux RS leadsTo_weaken) 1);
1.142 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [nodeOrder_def, HasTok_def])));
1.143 +by (ALLGOALS Blast_tac);