src/HOL/UNITY/Simple/Token.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 15618 05bad476e0f0
child 19769 c40ce2de2020
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
paulson@11195
     1
(*  Title:      HOL/UNITY/Token
paulson@11195
     2
    ID:         $Id$
paulson@11195
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@11195
     4
    Copyright   1998  University of Cambridge
paulson@11195
     5
*)
paulson@11195
     6
paulson@11195
     7
paulson@15618
     8
header {*The Token Ring*}
paulson@15618
     9
paulson@15618
    10
theory Token
paulson@15618
    11
imports "../WFair"
paulson@15618
    12
paulson@15618
    13
begin
paulson@11195
    14
paulson@15618
    15
text{*From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.*}
paulson@15618
    16
paulson@15618
    17
subsection{*Definitions*}
paulson@15618
    18
paulson@11195
    19
datatype pstate = Hungry | Eating | Thinking
paulson@15618
    20
    --{*process states*}
paulson@11195
    21
paulson@11195
    22
record state =
paulson@13785
    23
  token :: "nat"
paulson@13785
    24
  proc  :: "nat => pstate"
paulson@11195
    25
paulson@11195
    26
paulson@11195
    27
constdefs
paulson@13785
    28
  HasTok :: "nat => state set"
paulson@11195
    29
    "HasTok i == {s. token s = i}"
paulson@11195
    30
paulson@13785
    31
  H :: "nat => state set"
paulson@11195
    32
    "H i == {s. proc s i = Hungry}"
paulson@11195
    33
paulson@13785
    34
  E :: "nat => state set"
paulson@11195
    35
    "E i == {s. proc s i = Eating}"
paulson@11195
    36
paulson@13785
    37
  T :: "nat => state set"
paulson@11195
    38
    "T i == {s. proc s i = Thinking}"
paulson@11195
    39
paulson@11195
    40
paulson@11195
    41
locale Token =
paulson@13785
    42
  fixes N and F and nodeOrder and "next"   
paulson@13785
    43
  defines nodeOrder_def:
paulson@15618
    44
       "nodeOrder j == measure(%i. ((j+N)-i) mod N) \<inter> {..<N} \<times> {..<N}"
paulson@13785
    45
      and next_def:
paulson@13785
    46
       "next i == (Suc i) mod N"
paulson@13785
    47
  assumes N_positive [iff]: "0<N"
paulson@13806
    48
      and TR2:  "F \<in> (T i) co (T i \<union> H i)"
paulson@13806
    49
      and TR3:  "F \<in> (H i) co (H i \<union> E i)"
paulson@13806
    50
      and TR4:  "F \<in> (H i - HasTok i) co (H i)"
paulson@13806
    51
      and TR5:  "F \<in> (HasTok i) co (HasTok i \<union> -(E i))"
paulson@13806
    52
      and TR6:  "F \<in> (H i \<inter> HasTok i) leadsTo (E i)"
paulson@13806
    53
      and TR7:  "F \<in> (HasTok i) leadsTo (HasTok (next i))"
paulson@13785
    54
paulson@13785
    55
paulson@13806
    56
lemma HasToK_partition: "[| s \<in> HasTok i; s \<in> HasTok j |] ==> i=j"
paulson@13785
    57
by (unfold HasTok_def, auto)
paulson@11195
    58
paulson@13806
    59
lemma not_E_eq: "(s \<notin> E i) = (s \<in> H i | s \<in> T i)"
paulson@13785
    60
apply (simp add: H_def E_def T_def)
paulson@13785
    61
apply (case_tac "proc s i", auto)
paulson@13785
    62
done
paulson@11195
    63
paulson@13806
    64
lemma (in Token) token_stable: "F \<in> stable (-(E i) \<union> (HasTok i))"
paulson@13785
    65
apply (unfold stable_def)
paulson@13785
    66
apply (rule constrains_weaken)
paulson@13785
    67
apply (rule constrains_Un [OF constrains_Un [OF TR2 TR4] TR5])
paulson@13785
    68
apply (auto simp add: not_E_eq)
paulson@13785
    69
apply (simp_all add: H_def E_def T_def)
paulson@13785
    70
done
paulson@11195
    71
paulson@13785
    72
paulson@15618
    73
subsection{*Progress under Weak Fairness*}
paulson@13785
    74
paulson@13785
    75
lemma (in Token) wf_nodeOrder: "wf(nodeOrder j)"
paulson@13785
    76
apply (unfold nodeOrder_def)
paulson@15618
    77
apply (rule wf_measure [THEN wf_subset], blast)
paulson@13785
    78
done
paulson@11195
    79
paulson@13785
    80
lemma (in Token) nodeOrder_eq: 
paulson@13806
    81
     "[| i<N; j<N |] ==> ((next i, i) \<in> nodeOrder j) = (i \<noteq> j)"
paulson@15618
    82
apply (unfold nodeOrder_def next_def measure_def inv_image_def)
paulson@13785
    83
apply (auto simp add: mod_Suc mod_geq)
paulson@13785
    84
apply (auto split add: nat_diff_split simp add: linorder_neq_iff mod_geq)
paulson@13785
    85
done
paulson@11195
    86
paulson@15618
    87
text{*From "A Logic for Concurrent Programming", but not used in Chapter 4.
paulson@15618
    88
  Note the use of @{text case_tac}.  Reasoning about leadsTo takes practice!*}
paulson@13785
    89
lemma (in Token) TR7_nodeOrder:
paulson@13785
    90
     "[| i<N; j<N |] ==>    
paulson@13806
    91
      F \<in> (HasTok i) leadsTo ({s. (token s, i) \<in> nodeOrder j} \<union> HasTok j)"
paulson@13785
    92
apply (case_tac "i=j")
paulson@13785
    93
apply (blast intro: subset_imp_leadsTo)
paulson@13785
    94
apply (rule TR7 [THEN leadsTo_weaken_R])
paulson@13785
    95
apply (auto simp add: HasTok_def nodeOrder_eq)
paulson@13785
    96
done
paulson@11195
    97
paulson@13785
    98
paulson@15618
    99
text{*Chapter 4 variant, the one actually used below.*}
paulson@13806
   100
lemma (in Token) TR7_aux: "[| i<N; j<N; i\<noteq>j |]     
paulson@13806
   101
      ==> F \<in> (HasTok i) leadsTo {s. (token s, i) \<in> nodeOrder j}"
paulson@13785
   102
apply (rule TR7 [THEN leadsTo_weaken_R])
paulson@13785
   103
apply (auto simp add: HasTok_def nodeOrder_eq)
paulson@13785
   104
done
paulson@11195
   105
paulson@13785
   106
lemma (in Token) token_lemma:
paulson@13806
   107
     "({s. token s < N} \<inter> token -` {m}) = (if m<N then token -` {m} else {})"
paulson@13785
   108
by auto
paulson@13785
   109
paulson@11195
   110
paulson@15618
   111
text{*Misra's TR9: the token reaches an arbitrary node*}
paulson@13806
   112
lemma  (in Token) leadsTo_j: "j<N ==> F \<in> {s. token s < N} leadsTo (HasTok j)"
paulson@13785
   113
apply (rule leadsTo_weaken_R)
paulson@13785
   114
apply (rule_tac I = "-{j}" and f = token and B = "{}" 
paulson@13785
   115
       in wf_nodeOrder [THEN bounded_induct])
paulson@13785
   116
apply (simp_all (no_asm_simp) add: token_lemma vimage_Diff HasTok_def)
paulson@13785
   117
 prefer 2 apply blast
paulson@13785
   118
apply clarify
paulson@13785
   119
apply (rule TR7_aux [THEN leadsTo_weaken])
paulson@13785
   120
apply (auto simp add: HasTok_def nodeOrder_def)
paulson@13785
   121
done
paulson@13785
   122
paulson@15618
   123
text{*Misra's TR8: a hungry process eventually eats*}
paulson@13785
   124
lemma (in Token) token_progress:
paulson@13806
   125
     "j<N ==> F \<in> ({s. token s < N} \<inter> H j) leadsTo (E j)"
paulson@13785
   126
apply (rule leadsTo_cancel1 [THEN leadsTo_Un_duplicate])
paulson@13785
   127
apply (rule_tac [2] TR6)
paulson@13785
   128
apply (rule psp [OF leadsTo_j TR3, THEN leadsTo_weaken], blast+)
paulson@13785
   129
done
paulson@13785
   130
paulson@11195
   131
paulson@11195
   132
end