diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/Token.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Token.ML	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,150 @@
+(*  Title:      HOL/UNITY/Token
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+The Token Ring.
+
+From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
+*)
+
+
+open Token;
+
+
+val Token_defs = [WellTyped_def, Token_def, HasTok_def, H_def, E_def, T_def];
+
+AddIffs [N_positive, skip];
+
+goalw thy [HasTok_def] "!!i. [| s: HasTok i; s: HasTok j |] ==> i=j";
+by Auto_tac;
+qed "HasToK_partition";
+
+goalw thy Token_defs "!!s. s : WellTyped ==> (s ~: E i) = (s : H i | s : T i)";
+by (Simp_tac 1);
+by (exhaust_tac "s (Suc i)" 1);
+by Auto_tac;
+qed "not_E_eq";
+
+(** We should be able to prove WellTyped as a separate Invariant.  Then
+    the Invariant rule should let us assume that the initial
+    state is reachable, and therefore contained in any Invariant.  Then
+    we'd not have to mention WellTyped in the statement of this theorem.
+**)
+
+goalw thy [stable_def]
+    "stable Acts (WellTyped Int {s. s : E i --> s : HasTok i})";
+by (rtac (stable_WT RS stable_constrains_Int) 1);
+by (cut_facts_tac [TR2,TR4,TR5] 1);
+by (asm_full_simp_tac (simpset() addsimps [constrains_def]) 1);
+by (REPEAT_FIRST (rtac ballI ORELSE' (dtac bspec THEN' assume_tac)));
+by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
+by (case_tac "xa : HasTok i" 1);
+by (auto_tac (claset(), simpset() addsimps [H_def, E_def, T_def]));
+qed "token_stable";
+
+(*This proof is in the "massaging" style and is much faster! *)
+goalw thy [stable_def]
+    "stable Acts (WellTyped Int (Compl(E i) Un (HasTok i)))";
+by (rtac (stable_WT RS stable_constrains_Int) 1);
+by (rtac constrains_weaken 1);
+by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1);
+by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [H_def, E_def, T_def])));
+qed "token_stable";
+
+
+(*** Progress under weak fairness ***)
+
+goalw thy [nodeOrder_def] "wf(nodeOrder j)";
+by (rtac (wf_less_than RS wf_inv_image RS wf_subset) 1);
+by (Blast_tac 1);
+qed"wf_nodeOrder";
+
+    goal thy "!!m. [| m<n; Suc m ~= n |] ==> Suc(m) < n";
+    by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1);
+    by (blast_tac (claset() addEs [less_asym, less_SucE]) 1);
+    qed "Suc_lessI";
+
+goalw thy [nodeOrder_def, next_def, inv_image_def]
+    "!!x. [| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)";
+by (auto_tac (claset(),
+	      simpset() addsimps [Suc_lessI, mod_Suc, mod_less, mod_geq]));
+by (dtac sym 1);
+(*The next two lines...**)
+by (REPEAT (eres_inst_tac [("P", "?a<N")] rev_mp 1));
+by (etac ssubst 1);
+(*were with the previous version of asm_full_simp_tac...
+  by (rotate_tac ~1 1);
+*)
+by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv, mod_Suc, mod_less]) 1);
+by (subgoal_tac "(j + N - i) = Suc (j + N - Suc i)" 1);
+by (asm_simp_tac (simpset() addsimps [Suc_diff_Suc, less_imp_le, Suc_leI, 
+                                      diff_add_assoc]) 2);
+by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1);
+by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc]) 1);
+(*including less_asym here would slow things down*)
+by (auto_tac (claset() delrules [notI], 
+              simpset() addsimps [diff_add_assoc2, Suc_leI,
+                                  less_imp_diff_less, 
+                                  mod_less, mod_geq, nat_neq_iff]));
+by (REPEAT (blast_tac (claset() addEs [less_asym]) 3));
+by (asm_simp_tac (simpset() addsimps [less_imp_diff_less,
+				      Suc_diff_n RS sym]) 1);
+by (asm_simp_tac (simpset() addsimps [add_diff_less, mod_less]) 1);
+by (etac subst 1);
+by (asm_simp_tac (simpset() addsimps [add_diff_less]) 1);
+qed "nodeOrder_eq";
+
+
+(*From "A Logic for Concurrent Programming", but not used in Chapter 4.
+  Note the use of case_tac.  Reasoning about leadsTo takes practice!*)
+goal thy
+ "!!i. [| i<N; j<N |] ==> \
+\      leadsTo Acts (HasTok i) ({s. (Token s, i) : nodeOrder j} Un HasTok j)";
+by (case_tac "i=j" 1);
+by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
+by (rtac (TR7 RS leadsTo_weaken_R) 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
+qed "TR7_nodeOrder";
+
+
+(*Chapter 4 variant, the one actually used below.*)
+goal thy
+ "!!i. [| i<N; j<N; i~=j |] ==> \
+\      leadsTo Acts (HasTok i) {s. (Token s, i) : nodeOrder j}";
+by (rtac (TR7 RS leadsTo_weaken_R) 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
+qed "TR7_aux";
+
+goal thy "({s. Token s < N} Int Token -`` {m}) = \
+\         (if m<N then Token -`` {m} else {})";
+by Auto_tac;
+val Token_lemma = result();
+
+
+(*Misra's TR9: the token reaches an arbitrary node*)
+goal thy
+ "!!i. j<N ==> leadsTo Acts {s. Token s < N} (HasTok j)";
+by (rtac leadsTo_weaken_R 1);
+by (res_inst_tac [("I", "Compl{j}"), ("f", "Token"), ("B", "{}")]
+     (wf_nodeOrder RS bounded_induct) 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [Token_lemma, vimage_Diff,
+						HasTok_def])));
+by (Blast_tac 2);
+by (Clarify_tac 1);
+by (rtac (TR7_aux RS leadsTo_weaken) 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [nodeOrder_def, HasTok_def])));
+by (ALLGOALS Blast_tac);
+qed "leadsTo_j";
+
+(*Misra's TR8: a hungry process eventually eats*)
+goal thy "!!i. j<N ==> leadsTo Acts ({s. Token s < N} Int H j) (E j)";
+by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1);
+by (rtac TR6 2);
+by (rtac leadsTo_weaken_R 1);
+by (rtac ([leadsTo_j, TR3] MRS PSP) 1);
+by (ALLGOALS Blast_tac);
+qed "Token_progress";