src/HOL/UNITY/Token.ML

 
 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";
+Goalw [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)";
+Goalw 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";
 

     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]
+Goalw [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 (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]
+Goalw [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]));

 qed "token_stable";
 
 
 (*** Progress under weak fairness ***)
 
-goalw thy [nodeOrder_def] "wf(nodeOrder j)";
+Goalw [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";
+Goal "!!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]
+Goalw [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...**)

 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
+Goal
  "!!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 (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
 qed "TR7_nodeOrder";
 
 
 (*Chapter 4 variant, the one actually used below.*)
-goal thy
+Goal
  "!!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}) = \
+Goal "({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
+Goal
  "!!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,

 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)";
+Goal "!!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);