Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
Token.thy
Sprache: Unknown
|
(* Title: HOL/UNITY/Simple/Token.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
*)
section \<open>The Token Ring\<close>
theory Token
imports "../WFair"
begin
text\<open>From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.\<close>
subsection\<open>Definitions\<close>
datatype pstate = Hungry | Eating | Thinking
\<comment> \<open>process states\<close>
record state =
token :: "nat"
proc :: "nat => pstate"
definition HasTok :: "nat => state set" where
"HasTok i == {s. token s = i}"
definition H :: "nat => state set" where
"H i == {s. proc s i = Hungry}"
definition E :: "nat => state set" where
"E i == {s. proc s i = Eating}"
definition T :: "nat => state set" where
"T i == {s. proc s i = Thinking}"
locale Token =
fixes N and F and nodeOrder and "next"
defines nodeOrder_def:
"nodeOrder j == measure(%i. ((j+N)-i) mod N) \ {.. {..
and next_def:
"next i == (Suc i) mod N"
assumes N_positive [iff]: "0
and TR2: "F \ (T i) co (T i \ H i)"
and TR3: "F \ (H i) co (H i \ E i)"
and TR4: "F \ (H i - HasTok i) co (H i)"
and TR5: "F \ (HasTok i) co (HasTok i \ -(E i))"
and TR6: "F \ (H i \ HasTok i) leadsTo (E i)"
and TR7: "F \ (HasTok i) leadsTo (HasTok (next i))"
lemma HasToK_partition: "[| s \ HasTok i; s \ HasTok j |] ==> i=j"
by (unfold HasTok_def, auto)
lemma not_E_eq: "(s \ E i) = (s \ H i | s \ T i)"
apply (simp add: H_def E_def T_def)
apply (cases "proc s i", auto)
done
context Token
begin
lemma token_stable: "F \ stable (-(E i) \ (HasTok i))"
apply (unfold stable_def)
apply (rule constrains_weaken)
apply (rule constrains_Un [OF constrains_Un [OF TR2 TR4] TR5])
apply (auto simp add: not_E_eq)
apply (simp_all add: H_def E_def T_def)
done
subsection\<open>Progress under Weak Fairness\<close>
lemma wf_nodeOrder: "wf(nodeOrder j)"
apply (unfold nodeOrder_def)
apply (rule wf_measure [THEN wf_subset], blast)
done
lemma nodeOrder_eq:
"[| i ((next i, i) \ nodeOrder j) = (i \ j)"
apply (unfold nodeOrder_def next_def)
apply (auto simp add: mod_Suc mod_geq)
apply (auto split: nat_diff_split simp add: linorder_neq_iff mod_geq)
done
text\<open>From "A Logic for Concurrent Programming", but not used in Chapter 4.
Note the use of \<open>cases\<close>. Reasoning about leadsTo takes practice!\<close>
lemma TR7_nodeOrder:
"[| i
F \<in> (HasTok i) leadsTo ({s. (token s, i) \<in> nodeOrder j} \<union> HasTok j)"
apply (cases "i=j")
apply (blast intro: subset_imp_leadsTo)
apply (rule TR7 [THEN leadsTo_weaken_R])
apply (auto simp add: HasTok_def nodeOrder_eq)
done
text\<open>Chapter 4 variant, the one actually used below.\<close>
lemma TR7_aux: "[| ij |]
==> F \<in> (HasTok i) leadsTo {s. (token s, i) \<in> nodeOrder j}"
apply (rule TR7 [THEN leadsTo_weaken_R])
apply (auto simp add: HasTok_def nodeOrder_eq)
done
lemma token_lemma:
"({s. token s < N} \ token -` {m}) = (if m
by auto
text\<open>Misra's TR9: the token reaches an arbitrary node\<close>
lemma leadsTo_j: "j F \ {s. token s < N} leadsTo (HasTok j)"
apply (rule leadsTo_weaken_R)
apply (rule_tac I = "-{j}" and f = token and B = "{}"
in wf_nodeOrder [THEN bounded_induct])
apply (simp_all (no_asm_simp) add: token_lemma vimage_Diff HasTok_def)
prefer 2 apply blast
apply clarify
apply (rule TR7_aux [THEN leadsTo_weaken])
apply (auto simp add: HasTok_def nodeOrder_def)
done
text\<open>Misra's TR8: a hungry process eventually eats\<close>
lemma token_progress:
"j F \ ({s. token s < N} \ H j) leadsTo (E j)"
apply (rule leadsTo_cancel1 [THEN leadsTo_Un_duplicate])
apply (rule_tac [2] TR6)
apply (rule psp [OF leadsTo_j TR3, THEN leadsTo_weaken], blast+)
done
end
end
[ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
]
|
|
