src/HOL/UNITY/Token.ML
author wenzelm
Tue, 17 Nov 1998 14:07:25 +0100
changeset 5906 1f58694fc3e2
parent 5782 7559f116cb10
child 6055 fdf4638bf726
permissions -rw-r--r--
Drule.rev_triv_goal;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/Token
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     2
    ID:         $Id$
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     5
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     6
The Token Ring.
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     7
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     8
From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     9
*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    10
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    11
val Token_defs = [HasTok_def, H_def, E_def, T_def];
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    12
5111
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 5069
diff changeset
    13
Goalw [HasTok_def] "[| s: HasTok i; s: HasTok j |] ==> i=j";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    14
by Auto_tac;
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    15
qed "HasToK_partition";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    16
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    17
Goalw Token_defs "(s ~: E i) = (s : H i | s : T i)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    18
by (Simp_tac 1);
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    19
by (exhaust_tac "proc s i" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    20
by Auto_tac;
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    21
qed "not_E_eq";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    22
5420
b48ab3281944 New approach, using a locale
paulson
parents: 5277
diff changeset
    23
Open_locale "Token";
b48ab3281944 New approach, using a locale
paulson
parents: 5277
diff changeset
    24
5782
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5648
diff changeset
    25
val TR2 = thm "TR2";
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5648
diff changeset
    26
val TR3 = thm "TR3";
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5648
diff changeset
    27
val TR4 = thm "TR4";
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5648
diff changeset
    28
val TR5 = thm "TR5";
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5648
diff changeset
    29
val TR6 = thm "TR6";
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5648
diff changeset
    30
val TR7 = thm "TR7";
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5648
diff changeset
    31
val nodeOrder_def = thm "nodeOrder_def";
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5648
diff changeset
    32
val next_def = thm "next_def";
5420
b48ab3281944 New approach, using a locale
paulson
parents: 5277
diff changeset
    33
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5625
diff changeset
    34
AddIffs [thm "N_positive"];
5420
b48ab3281944 New approach, using a locale
paulson
parents: 5277
diff changeset
    35
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5625
diff changeset
    36
Goalw [stable_def] "F : stable (-(E i) Un (HasTok i))";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    37
by (rtac constrains_weaken 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    38
by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    39
by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    40
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [H_def, E_def, T_def])));
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    41
qed "token_stable";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    42
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    43
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    44
(*** Progress under weak fairness ***)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    45
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
    46
Goalw [nodeOrder_def] "wf(nodeOrder j)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    47
by (rtac (wf_less_than RS wf_inv_image RS wf_subset) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    48
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    49
qed"wf_nodeOrder";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    50
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
    51
Goalw [nodeOrder_def, next_def, inv_image_def]
5111
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 5069
diff changeset
    52
    "[| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    53
by (auto_tac (claset(),
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    54
	      simpset() addsimps [Suc_lessI, mod_Suc, mod_less, mod_geq]));
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    55
by (subgoal_tac "(j + N - i) = Suc (j + N - Suc i)" 1);
5596
b29d18d8c4d2 abstype of programs
paulson
parents: 5490
diff changeset
    56
by (asm_simp_tac (simpset() addsimps [Suc_diff_Suc, Suc_leI, less_imp_le,
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    57
                                      diff_add_assoc]) 2);
5625
77e9ab9cd7b1 polymorphic versions of nat_neq_iff and nat_neqE
paulson
parents: 5596
diff changeset
    58
by (full_simp_tac (simpset() addsimps [linorder_neq_iff]) 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    59
by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc]) 1);
5420
b48ab3281944 New approach, using a locale
paulson
parents: 5277
diff changeset
    60
by (auto_tac (claset(), 
5625
77e9ab9cd7b1 polymorphic versions of nat_neq_iff and nat_neqE
paulson
parents: 5596
diff changeset
    61
              simpset() addsimps [diff_add_assoc2, linorder_neq_iff, 
5420
b48ab3281944 New approach, using a locale
paulson
parents: 5277
diff changeset
    62
                                  Suc_le_eq, Suc_diff_Suc, less_imp_diff_less, 
b48ab3281944 New approach, using a locale
paulson
parents: 5277
diff changeset
    63
                                  add_diff_less, mod_less, mod_geq]));
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    64
by (etac subst 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    65
by (asm_simp_tac (simpset() addsimps [add_diff_less]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    66
qed "nodeOrder_eq";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    67
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    68
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    69
(*From "A Logic for Concurrent Programming", but not used in Chapter 4.
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    70
  Note the use of case_tac.  Reasoning about leadsTo takes practice!*)
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    71
Goal "[| i<N; j<N |] ==>   \
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5625
diff changeset
    72
\     F : leadsTo (HasTok i) ({s. (token s, i) : nodeOrder j} Un HasTok j)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    73
by (case_tac "i=j" 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    74
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    75
by (rtac (TR7 RS leadsTo_weaken_R) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    76
by (Clarify_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    77
by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    78
qed "TR7_nodeOrder";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    79
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    80
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    81
(*Chapter 4 variant, the one actually used below.*)
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    82
Goal "[| i<N; j<N; i~=j |]    \
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5625
diff changeset
    83
\     ==> F : leadsTo (HasTok i) {s. (token s, i) : nodeOrder j}";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    84
by (rtac (TR7 RS leadsTo_weaken_R) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    85
by (Clarify_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    86
by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    87
qed "TR7_aux";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    88
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    89
Goal "({s. token s < N} Int token -`` {m}) = \
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    90
\     (if m<N then token -`` {m} else {})";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    91
by Auto_tac;
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
    92
val token_lemma = result();
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    93
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    94
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    95
(*Misra's TR9: the token reaches an arbitrary node*)
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5625
diff changeset
    96
Goal "j<N ==> F : leadsTo {s. token s < N} (HasTok j)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    97
by (rtac leadsTo_weaken_R 1);
5490
85855f65d0c6 From Compl(A) to -A
paulson
parents: 5420
diff changeset
    98
by (res_inst_tac [("I", "-{j}"), ("f", "token"), ("B", "{}")]
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    99
     (wf_nodeOrder RS bounded_induct) 1);
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
   100
by (ALLGOALS (asm_simp_tac (simpset() addsimps [token_lemma, vimage_Diff,
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   101
						HasTok_def])));
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   102
by (Blast_tac 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   103
by (Clarify_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   104
by (rtac (TR7_aux RS leadsTo_weaken) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   105
by (ALLGOALS (asm_simp_tac (simpset() addsimps [nodeOrder_def, HasTok_def])));
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   106
by (ALLGOALS Blast_tac);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   107
qed "leadsTo_j";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   108
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   109
(*Misra's TR8: a hungry process eventually eats*)
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5625
diff changeset
   110
Goal "j<N ==> F : leadsTo ({s. token s < N} Int H j) (E j)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   111
by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   112
by (rtac TR6 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   113
by (rtac leadsTo_weaken_R 1);
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents: 5253
diff changeset
   114
by (rtac ([leadsTo_j, TR3] MRS psp) 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   115
by (ALLGOALS Blast_tac);
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
   116
qed "token_progress";