New approach, using a locale
authorpaulson
Tue Sep 01 15:07:11 1998 +0200 (1998-09-01)
changeset 5420b48ab3281944
parent 5419 3a744748dd21
child 5421 01fc8d6a40f2
New approach, using a locale
src/HOL/UNITY/Token.ML
src/HOL/UNITY/Token.thy
     1.1 --- a/src/HOL/UNITY/Token.ML	Tue Sep 01 15:05:59 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Token.ML	Tue Sep 01 15:07:11 1998 +0200
     1.3 @@ -10,8 +10,6 @@
     1.4  
     1.5  val Token_defs = [HasTok_def, H_def, E_def, T_def];
     1.6  
     1.7 -AddIffs [N_positive, skip];
     1.8 -
     1.9  Goalw [HasTok_def] "[| s: HasTok i; s: HasTok j |] ==> i=j";
    1.10  by Auto_tac;
    1.11  qed "HasToK_partition";
    1.12 @@ -22,7 +20,20 @@
    1.13  by Auto_tac;
    1.14  qed "not_E_eq";
    1.15  
    1.16 -(*This proof is in the "massaging" style and is much faster! *)
    1.17 +Open_locale "Token";
    1.18 +
    1.19 +(*Strip meta-quantifiers: perhaps the locale should do this?*)
    1.20 +val TR2   = forall_elim_vars 0 (thm "TR2");
    1.21 +val TR3   = forall_elim_vars 0 (thm "TR3");
    1.22 +val TR4   = forall_elim_vars 0 (thm "TR4");
    1.23 +val TR5   = forall_elim_vars 0 (thm "TR5");
    1.24 +val TR6   = forall_elim_vars 0 (thm "TR6");
    1.25 +val TR7   = forall_elim_vars 0 (thm "TR7");
    1.26 +val nodeOrder_def   = (thm "nodeOrder_def");
    1.27 +val next_def   = (thm "next_def");
    1.28 +
    1.29 +AddIffs [thm "N_positive", thm"skip"];
    1.30 +
    1.31  Goalw [stable_def] "stable acts (Compl(E i) Un (HasTok i))";
    1.32  by (rtac constrains_weaken 1);
    1.33  by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1);
    1.34 @@ -38,37 +49,19 @@
    1.35  by (Blast_tac 1);
    1.36  qed"wf_nodeOrder";
    1.37  
    1.38 -Goal "[| m<n; Suc m ~= n |] ==> Suc(m) < n";
    1.39 -    by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1);
    1.40 -    by (blast_tac (claset() addEs [less_asym, less_SucE]) 1);
    1.41 -    qed "Suc_lessI";
    1.42 -
    1.43  Goalw [nodeOrder_def, next_def, inv_image_def]
    1.44      "[| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)";
    1.45  by (auto_tac (claset(),
    1.46  	      simpset() addsimps [Suc_lessI, mod_Suc, mod_less, mod_geq]));
    1.47 -by (dtac sym 1);
    1.48 -(*The next two lines...**)
    1.49 -by (REPEAT (eres_inst_tac [("P", "?a<N")] rev_mp 1));
    1.50 -by (etac ssubst 1);
    1.51 -(*were with the previous version of asm_full_simp_tac...
    1.52 -  by (rotate_tac ~1 1);
    1.53 -*)
    1.54 -by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv, mod_Suc, mod_less]) 1);
    1.55  by (subgoal_tac "(j + N - i) = Suc (j + N - Suc i)" 1);
    1.56 -by (asm_simp_tac (simpset() addsimps [Suc_diff_Suc, less_imp_le, Suc_leI, 
    1.57 +by (asm_simp_tac (simpset() addsimps [Suc_diff_Suc, Suc_leI, 
    1.58                                        diff_add_assoc]) 2);
    1.59  by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1);
    1.60  by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc]) 1);
    1.61 -(*including less_asym here would slow things down*)
    1.62 -by (auto_tac (claset() delrules [notI], 
    1.63 -              simpset() addsimps [diff_add_assoc2, Suc_leI,
    1.64 -                                  less_imp_diff_less, 
    1.65 -                                  mod_less, mod_geq, nat_neq_iff]));
    1.66 -by (REPEAT (blast_tac (claset() addEs [less_asym]) 3));
    1.67 -by (asm_simp_tac (simpset() addsimps [less_imp_diff_less,
    1.68 -				      Suc_diff_n RS sym]) 1);
    1.69 -by (asm_simp_tac (simpset() addsimps [add_diff_less, mod_less]) 1);
    1.70 +by (auto_tac (claset(), 
    1.71 +              simpset() addsimps [diff_add_assoc2, nat_neq_iff, 
    1.72 +                                  Suc_le_eq, Suc_diff_Suc, less_imp_diff_less, 
    1.73 +                                  add_diff_less, mod_less, mod_geq]));
    1.74  by (etac subst 1);
    1.75  by (asm_simp_tac (simpset() addsimps [add_diff_less]) 1);
    1.76  qed "nodeOrder_eq";
     2.1 --- a/src/HOL/UNITY/Token.thy	Tue Sep 01 15:05:59 1998 +0200
     2.2 +++ b/src/HOL/UNITY/Token.thy	Tue Sep 01 15:07:11 1998 +0200
     2.3 @@ -18,17 +18,8 @@
     2.4    token :: nat
     2.5    proc  :: nat => pstate
     2.6  
     2.7 -consts
     2.8 -  N :: nat	(*number of nodes in the ring*)
     2.9  
    2.10  constdefs
    2.11 -  nodeOrder :: "nat => (nat*nat)set"
    2.12 -    "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N))  Int
    2.13 -                    (lessThan N Times lessThan N)"
    2.14 -
    2.15 -  next      :: nat => nat
    2.16 -    "next i == (Suc i) mod N"
    2.17 -
    2.18    HasTok :: nat => state set
    2.19      "HasTok i == {s. token s = i}"
    2.20  
    2.21 @@ -41,21 +32,37 @@
    2.22    T :: nat => state set
    2.23      "T i == {s. proc s i = Thinking}"
    2.24  
    2.25 -rules
    2.26 -  N_positive "0<N"
    2.27  
    2.28 -  skip "id: acts"
    2.29 +locale Token =
    2.30 +  fixes
    2.31 +    N         :: nat	 (*number of nodes in the ring*)
    2.32 +    acts      :: "(state*state)set set"
    2.33 +    nodeOrder :: "nat => (nat*nat)set"
    2.34 +    next      :: nat => nat
    2.35  
    2.36 -  TR2  "constrains acts (T i) (T i Un H i)"
    2.37 +  assumes
    2.38 +    N_positive "0<N"
    2.39 +
    2.40 +    skip "id: acts"
    2.41 +
    2.42 +    TR2  "!!i. constrains acts (T i) (T i Un H i)"
    2.43  
    2.44 -  TR3  "constrains acts (H i) (H i Un E i)"
    2.45 +    TR3  "!!i. constrains acts (H i) (H i Un E i)"
    2.46 +
    2.47 +    TR4  "!!i. constrains acts (H i - HasTok i) (H i)"
    2.48  
    2.49 -  TR4  "constrains acts (H i - HasTok i) (H i)"
    2.50 +    TR5  "!!i. constrains acts (HasTok i) (HasTok i Un Compl(E i))"
    2.51 +
    2.52 +    TR6  "!!i. leadsTo acts (H i Int HasTok i) (E i)"
    2.53  
    2.54 -  TR5  "constrains acts (HasTok i) (HasTok i Un Compl(E i))"
    2.55 +    TR7  "!!i. leadsTo acts (HasTok i) (HasTok (next i))"
    2.56  
    2.57 -  TR6  "leadsTo acts (H i Int HasTok i) (E i)"
    2.58 +  defines
    2.59 +    nodeOrder_def
    2.60 +      "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N))  Int
    2.61 +		      (lessThan N Times lessThan N)"
    2.62  
    2.63 -  TR7  "leadsTo acts (HasTok i) (HasTok (next i))"
    2.64 +    next_def
    2.65 +      "next i == (Suc i) mod N"
    2.66  
    2.67  end