Theory FLPTheorem
section ‹FLPTheorem›
text ‹
\file{FLPTheorem} combines the results of \file{FLPSystem} with the concept
of fair infinite executions and culminates in showing the impossibility
of a consensus algorithm in the proposed setting.
›
theory FLPTheorem
imports Execution FLPSystem
begin
locale flpPseudoConsensus =
flpSystem trans sends start
for
trans :: "'p ⇒ 's ⇒ 'v messageValue ⇒'s" and
sends :: "'p ⇒ 's ⇒ 'v messageValue ⇒ ('p, 'v) message multiset" and
start :: "'p ⇒ 's" +
assumes
Agreement: "⋀ i c . agreementInit i c" and
PseudoTermination: "⋀cc Q . terminationPseudo 1 cc Q"
begin
subsection ‹Obtaining non-uniform executions›
text ‹
Executions which end with a \isb{nonUniform} configuration can be expanded
to a strictly longer execution consuming a particular message.
This lemma connects the previous results to the world of executions,
thereby paving the way to the final contradiction. It covers a big part of
the original proof of the theorem, i.e.\ finding the expansion to a longer
execution where the decision for both values is still possible.
\voelzer{constructing executions using Lemma 2}
›
lemma NonUniformExecutionsConstructable:
fixes
exec :: "('p, 'v, 's ) configuration list " and
trace :: "('p, 'v) message list" and
msg :: "('p, 'v) message" and
p :: 'p
assumes
MsgEnabled: "enabled (last exec) msg" and
PisReceiverOf: "isReceiverOf p msg" and
ExecIsExecution: "execution trans sends start exec trace" and
NonUniformLexec: "nonUniform (last exec)" and
Agree: "⋀ cfg . reachable (last exec) cfg ⟶ agreement cfg"
shows
"∃ exec' trace' . (execution trans sends start exec' trace')
∧ nonUniform (last exec')
∧ prefixList exec exec' ∧ prefixList trace trace'
∧ (∀ cfg . reachable (last exec') cfg ⟶ agreement cfg)
∧ stepReachable (last exec) msg (last exec')
∧ (msg ∈ set (drop (length trace) trace'))"
proof -
from NonUniformCanReachSilentBivalence[OF NonUniformLexec PseudoTermination Agree]
obtain c' where C':
"reachable (last exec) c'"
"val[p,c'] = {True, False}"
by blast
show ?thesis
proof (cases "stepReachable (last exec) msg c'")
case True
hence IsStepReachable: "stepReachable (last exec) msg c'" by simp
hence "∃ exec' trace'. (execution trans sends start exec' trace')
∧ prefixList exec exec'
∧ prefixList trace trace' ∧ (last exec') = c'
∧ msg ∈ set (drop (length trace) trace')"
using ExecIsExecution expandExecution
by auto
then obtain exec' trace' where NewExec:
"(execution trans sends start exec' trace')"
"prefixList exec exec'" "(last exec') = c'" "prefixList trace trace'"
"msg ∈ set (drop (length trace) trace')" by blast
hence lastExecExec'Reachable: "reachable (last exec) (last exec')"
using C'(1) by simp
hence InitReachLastExec': "initReachable (last exec')"
using NonUniformLexec
by (metis ReachableTrans initReachable_def)
hence nonUniformC': "nonUniform (last exec')" using C'(2) NewExec(3)
by (auto simp add: vUniform_def)
hence isAgreementPreventing:
"(∀ cfg . reachable (last exec') cfg ⟶ agreement cfg)"
using lastExecExec'Reachable Agree by (metis ReachableTrans)
with NewExec nonUniformC' IsStepReachable show ?thesis by auto
next
case False
hence NotStepReachable: "¬ (stepReachable (last exec) msg c')" by simp
from C'(1) obtain exec' trace' where NewExec:
"execution trans sends start exec' trace'"
"(prefixList exec exec' ∧ prefixList trace trace')
∨ (exec = exec' ∧ trace = trace')"
"last exec' = c'"
using ExecIsExecution expandExecutionReachable by blast
have lastExecExec'Reachable: "reachable (last exec) (last exec')"
using C'(1) NewExec(3) by simp
with NonUniformLexec have InitReachLastExec':
"initReachable (last exec')"
by (metis ReachableTrans initReachable_def)
with C'(2) NewExec(3) have nonUniformC': "nonUniform (last exec')"
by (auto simp add: vUniform_def)
show "∃ exec1 trace1 . (execution trans sends start exec1 trace1)
∧ nonUniform (last exec1)
∧ prefixList exec exec1 ∧ prefixList trace trace1
∧ (∀ cfg . reachable (last exec1) cfg ⟶ agreement cfg)
∧ stepReachable (last exec) msg (last exec1)
∧ (msg ∈ set (drop (length trace) trace1))"
proof (cases "enabled (last exec') msg")
case True
hence EnabledMsg: "enabled (last exec') msg" by auto
hence "∃ cMsg . ((last exec') ⊢ msg ↦ cMsg )"
proof (cases msg)
case (InMsg p' b)
with PisReceiverOf have MsgIsInMsg: "(msg = <p, inM b>)" by auto
define cfgInM where "cfgInM = ⦇states = λproc. (
if proc = p then
trans p (states (last exec') p) (Bool b)
else states (last exec') proc),
msgs = (((sends p (states (last exec') p) (Bool b))
∪# (msgs (last exec')-# msg)))⦈ "
with UniqueReceiverOf MsgIsInMsg EnabledMsg have
"((last exec') ⊢ msg ↦ cfgInM)" by auto
thus "∃ cMsg . ((last exec') ⊢ msg ↦ cMsg )" by blast
next
case (OutMsg b)
thus "∃ cMsg . ((last exec') ⊢ msg ↦ cMsg )" using PisReceiverOf
by auto
next
case (Msg p' v')
with PisReceiverOf have MsgIsVMsg: "(msg = <p, v'>)" by auto
define cfgVMsg where "cfgVMsg =
⦇states = λproc. (
if proc = p then
trans p (states (last exec') p) (Value v')
else states (last exec') proc),
msgs = (((sends p (states (last exec') p) (Value v'))
∪# (msgs (last exec') -# msg )))⦈ "
with UniqueReceiverOf MsgIsVMsg EnabledMsg noInSends have
"((last exec') ⊢ msg ↦ cfgVMsg)" by auto
thus "∃ cMsg . ((last exec') ⊢ msg ↦ cMsg )" by blast
qed
then obtain cMsg where CMsg:"((last exec') ⊢ msg ↦ cMsg )" by auto
define execMsg where "execMsg = exec' @ [cMsg]"
define traceMsg where "traceMsg = trace' @ [msg]"
from NewExec(1) CMsg obtain execMsg traceMsg where isExecution:
"execution trans sends start execMsg traceMsg"
and ExecMsg: "prefixList exec' execMsg" "prefixList trace' traceMsg"
"last execMsg = cMsg" "last traceMsg = msg"
using expandExecutionStep by blast
have isPrefixListExec: "prefixList exec execMsg"
using PrefixListTransitive NewExec(2) ExecMsg(1) by auto
have isPrefixListTrace: "prefixList trace traceMsg"
using PrefixListTransitive NewExec(2) ExecMsg(2) by auto
have cMsgLastReachable: "reachable cMsg (last execMsg)"
by (auto simp add: ExecMsg reachable.init)
hence isStepReachable: "stepReachable (last exec) msg (last execMsg)"
using CMsg lastExecExec'Reachable
by (auto simp add: stepReachable_def)
have InitReachLastExecMsg: "initReachable (last execMsg)"
using CMsg InitReachLastExec' cMsgLastReachable
by (metis ReachableTrans initReachable_def step)
have "val[p, (last exec')] ⊆ val[p, cMsg]"
using CMsg PisReceiverOf InitReachLastExec'
ActiveProcessSilentDecisionValuesIncrease[of p p "last exec'" msg cMsg]
by auto
with ExecMsg C'(2) NewExec(3) have
"val[p, (last execMsg)] = {True, False}" by auto
with InitReachLastExecMsg have isNonUniform:
"nonUniform (last execMsg)" by (auto simp add: vUniform_def)
have "reachable (last exec) (last execMsg)"
using lastExecExec'Reachable cMsgLastReachable CMsg
by (metis ReachableTrans step)
hence isAgreementPreventing:
"(∀ cfg . reachable (last execMsg) cfg ⟶ agreement cfg)"
using Agree by (metis ReachableTrans)
have "msg ∈ set (drop (length trace) traceMsg)" using ExecMsg(4)
isPrefixListTrace
by (metis (full_types) PrefixListMonotonicity last_drop last_in_set
length_0_conv length_drop less_zeroE zero_less_diff)
thus ?thesis using isExecution isNonUniform isPrefixListExec
isPrefixListTrace isAgreementPreventing isStepReachable by blast
next
case False
hence notEnabled: "¬ (enabled (last exec') msg)" by auto
have isStepReachable: "stepReachable (last exec) msg (last exec')"
using MsgEnabled notEnabled lastExecExec'Reachable StepReachable
by auto
with NotStepReachable NewExec(3) show ?thesis by simp
qed
qed
qed
lemma NonUniformExecutionBase:
fixes
cfg
assumes
Cfg: "initial cfg" "nonUniform cfg"
shows
"execution trans sends start [cfg] []
∧ nonUniform (last [cfg])
∧ (∃ cfgList' msgList'. nonUniform (last cfgList')
∧ prefixList [cfg] cfgList'
∧ prefixList [] msgList'
∧ (execution trans sends start cfgList' msgList')
∧ (∃ msg'. execution.minimalEnabled [cfg] [] msg'
∧ msg' ∈ set msgList'))"
proof -
have NonUniListCfg: "nonUniform (last [cfg])" using Cfg(2) by auto
have AgreeCfg': "∀ cfg' .
reachable (last [cfg]) cfg' ⟶ agreement cfg'"
using Agreement Cfg(1)
by (auto simp add: agreementInit_def reachable.init agreement_def)
have StartExec: "execution trans sends start [cfg] []"
using Cfg(1) by (unfold_locales, auto)
hence "∃ msg . execution.minimalEnabled [cfg] [] msg"
using Cfg execution.ExistImpliesMinEnabled
by (metis enabled_def initial_def isReceiverOf.simps(1)
last.simps zero_less_one)
then obtain msg where MinEnabledMsg:
"execution.minimalEnabled [cfg] [] msg" by blast
hence "∃ pMin . isReceiverOf pMin msg" using StartExec
by (auto simp add: execution.minimalEnabled_def)
then obtain pMin where PMin: "isReceiverOf pMin msg" by blast
hence "enabled (last [cfg]) msg ∧ isReceiverOf pMin msg"
using MinEnabledMsg StartExec
by (auto simp add: execution.minimalEnabled_def)
hence Enabled: "enabled (last [cfg]) msg" "isReceiverOf pMin msg"
by auto
from Enabled StartExec NonUniListCfg PseudoTermination AgreeCfg'
have "∃ exec' trace' . (execution trans sends start exec' trace')
∧ nonUniform (last exec')
∧ prefixList [cfg] exec' ∧ prefixList [] trace'
∧ (∀ cfg' . reachable (last exec') cfg' ⟶ agreement cfg')
∧ stepReachable (last [cfg]) msg (last exec')
∧ (msg ∈ set (drop (length []) trace'))"
using NonUniformExecutionsConstructable[of "[cfg]" "msg" "pMin"
"[]::('p,'v) message list"]
by simp
with StartExec NonUniListCfg MinEnabledMsg show ?thesis by auto
qed
lemma NonUniformExecutionStep:
fixes
cfgList msgList
assumes
Init: "initial (hd cfgList)" and
NonUni: "nonUniform (last cfgList)" and
Execution: "execution trans sends start cfgList msgList"
shows
"(∃ cfgList' msgList' .
nonUniform (last cfgList')
∧ prefixList cfgList cfgList'
∧ prefixList msgList msgList'
∧ (execution trans sends start cfgList' msgList')
∧ (initial (hd cfgList'))
∧ (∃ msg'. execution.minimalEnabled cfgList msgList msg'
∧ msg' ∈ (set (drop (length msgList ) msgList')) ))"
proof -
have ReachImplAgree: "∀ cfg . reachable (last cfgList) cfg
⟶ agreement cfg"
using Agreement Init NonUni ReachableTrans
unfolding agreementInit_def agreement_def initReachable_def
by (metis (full_types))
have "∃ msg p. enabled (last cfgList) msg ∧ isReceiverOf p msg"
proof -
from PseudoTermination NonUni have
"∃c'. qReachable (last cfgList) Proc c' ∧ decided c'"
using terminationPseudo_def by auto
then obtain c' where C': "reachable (last cfgList) c'"
"decided c'"
using QReachImplReach by blast
have NoOut:
"0 = msgs (last cfgList) <⊥, outM False>"
"0 = msgs (last cfgList) <⊥, outM True>"
using NonUni ReachImplAgree PseudoTermination
by (metis NonUniformImpliesNotDecided neq0_conv)+
with C'(2) have "(last cfgList) ≠ c'"
by (metis (full_types) less_zeroE)
thus ?thesis using C'(1) ReachableStepFirst by blast
qed
then obtain msg p where Enabled:
"enabled (last cfgList) msg" "isReceiverOf p msg" by blast
hence "∃ msg . execution.minimalEnabled cfgList msgList msg"
using Init execution.ExistImpliesMinEnabled[OF Execution] by auto
then obtain msg' where MinEnabledMsg:
"execution.minimalEnabled cfgList msgList msg'" by blast
hence "∃ p' . isReceiverOf p' msg'"
using Execution
by (auto simp add: execution.minimalEnabled_def)
then obtain p' where
P': "isReceiverOf p' msg'" by blast
hence Enabled':
"enabled (last cfgList) msg'" "isReceiverOf p' msg'"
using MinEnabledMsg Execution
by (auto simp add: execution.minimalEnabled_def)
have "∃ exec' trace' . (execution trans sends start exec' trace')
∧ nonUniform (last exec')
∧ prefixList cfgList exec' ∧ prefixList msgList trace'
∧ (∀ cfg . reachable (last exec') cfg ⟶ agreement cfg)
∧ stepReachable (last cfgList) msg' (last exec')
∧ (msg' ∈ set (drop (length msgList) trace')) "
using NonUniformExecutionsConstructable[OF Enabled' Execution
NonUni] ReachImplAgree by auto
thus ?thesis
using MinEnabledMsg by (metis execution.base)
qed
subsection ‹Non-uniformity even when demanding fairness›
text ‹
Using \isb{NonUniformExecutionBase} and \isb{NonUniformExecutionStep} one can obtain
non-uniform executions which are fair.
Proving the fairness turned out quite cumbersome.
›
text ‹
These two functions construct infinite series of configurations lists
and message lists from two extension functions.
›
fun infiniteExecutionCfg ::
"('p, 'v, 's) configuration ⇒
(('p, 'v, 's) configuration list ⇒ ('p, 'v) message list
⇒ ('p, 'v, 's) configuration list) ⇒
(('p, 'v, 's) configuration list ⇒ ('p, 'v) message list
⇒('p, 'v) message list)
⇒ nat
⇒ (('p, 'v, 's) configuration list)"
and infiniteExecutionMsg ::
"('p, 'v, 's) configuration ⇒
(('p, 'v, 's) configuration list ⇒ ('p, 'v) message list
⇒ ('p, 'v, 's) configuration list) ⇒
(('p, 'v, 's) configuration list ⇒ ('p, 'v) message list
⇒('p, 'v) message list)
⇒ nat
⇒ ('p, 'v) message list"
where
"infiniteExecutionCfg cfg fStepCfg fStepMsg 0 = [cfg]"
| "infiniteExecutionCfg cfg fStepCfg fStepMsg (Suc n) =
fStepCfg (infiniteExecutionCfg cfg fStepCfg fStepMsg n)
(infiniteExecutionMsg cfg fStepCfg fStepMsg n)"
| "infiniteExecutionMsg cfg fStepCfg fStepMsg 0 = []"
| "infiniteExecutionMsg cfg fStepCfg fStepMsg (Suc n) =
fStepMsg (infiniteExecutionCfg cfg fStepCfg fStepMsg n)
(infiniteExecutionMsg cfg fStepCfg fStepMsg n)"
lemma FairNonUniformExecution:
fixes
cfg
assumes
Cfg: "initial cfg" "nonUniform cfg"
shows "∃ fe ft.
(fe 0) = [cfg]
∧ fairInfiniteExecution fe ft
∧ (∀ n . nonUniform (last (fe n))
∧ prefixList (fe n) (fe (n+1))
∧ prefixList (ft n) (ft (n+1))
∧ (execution trans sends start (fe n) (ft n)))"
proof -
have BC:
"execution trans sends start [cfg] []
∧ nonUniform (last [cfg])
∧ (∃ cfgList' msgList'. nonUniform (last cfgList')
∧ prefixList [cfg] cfgList'
∧ prefixList [] msgList'
∧ (execution trans sends start cfgList' msgList')
∧ (∃ msg'. execution.minimalEnabled [cfg] [] msg'
∧ msg' ∈ set msgList'))"
using NonUniformExecutionBase[OF assms] .
obtain fStepCfg fStepMsg where FStep: "∀ cfgList msgList . ∃cfgList' msgList' .
fStepCfg cfgList msgList = cfgList' ∧
fStepMsg cfgList msgList = msgList' ∧
(initial (hd cfgList) ∧
nonUniform (last cfgList) ∧
execution trans sends start cfgList msgList ⟶
(nonUniform (last (fStepCfg cfgList msgList))
∧ prefixList cfgList (fStepCfg cfgList msgList)
∧ prefixList msgList (fStepMsg cfgList msgList)
∧ execution trans sends start (fStepCfg cfgList msgList)
(fStepMsg cfgList msgList)
∧ (initial (hd (fStepCfg cfgList msgList)))
∧ (∃ msg'. execution.minimalEnabled cfgList msgList msg'
∧ msg' ∈ (set (drop (length msgList)
(fStepMsg cfgList msgList))))))"
using NonUniformExecutionStep
PredicatePairFunctions2[of
"λ cfgList msgList cfgList' msgList'.
(initial (hd cfgList)
∧ nonUniform (last cfgList)
∧ execution trans sends start cfgList msgList
⟶ (nonUniform (last cfgList')
∧ prefixList cfgList cfgList'
∧ prefixList msgList msgList'
∧ execution trans sends start cfgList' msgList'
∧ (initial (hd cfgList'))
∧ (∃ msg'. execution.minimalEnabled cfgList msgList msg'
∧ msg' ∈ (set (drop (length msgList ) msgList')))))" "False"] by auto
define fe ft
where "fe = infiniteExecutionCfg cfg fStepCfg fStepMsg"
and "ft = infiniteExecutionMsg cfg fStepCfg fStepMsg"
have BasicProperties: "(∀n. nonUniform (last (fe n))
∧ prefixList (fe n) (fe (n + 1)) ∧ prefixList (ft n) (ft (n + 1))
∧ execution trans sends start (fe n) (ft n)
∧ initial (hd (fe (n + 1))))"
proof (clarify)
fix n
show "nonUniform (last (fe n)) ∧
prefixList (fe n) (fe (n + (1::nat)))
∧ prefixList (ft n) (ft (n + (1::nat)))
∧ execution trans sends start (fe n) (ft n)
∧ initial (hd (fe (n + 1)))"
proof(induct n)
case 0
hence "fe 0 = [cfg]" "ft 0 = []" "fe 1 = fStepCfg (fe 0) (ft 0)"
"ft 1 = fStepMsg (fe 0) (ft 0)"
using fe_def ft_def
by simp_all
thus ?case
using BC FStep
by (simp, metis execution.base)
next
case (Suc n)
thus ?case
using fe_def ft_def
by (auto, (metis FStep execution.base)+)
qed
qed
have Fair: "fairInfiniteExecution fe ft"
using BasicProperties
unfolding fairInfiniteExecution_def infiniteExecution_def
execution_def flpSystem_def
proof(auto simp add: finiteProcs minimalProcs finiteSends noInSends)
fix n n0 p msg
assume AssumptionFair: "∀n. initReachable (last (fe n)) ∧
¬ vUniform False (last (fe n)) ∧
¬ vUniform True (last (fe n)) ∧
prefixList (fe n) (fe (Suc n)) ∧
prefixList (ft n) (ft (Suc n)) ∧
Suc 0 ≤ length (fe n) ∧
length (fe n) - Suc 0 = length (ft n) ∧
initial (hd (fe n)) ∧
(∀i<length (fe n) - Suc 0. ((fe n ! i) ⊢ (ft n ! i)
↦ (fe n ! Suc i))) ∧ initial (hd (fe (Suc n)))"
"n0 < length (fe n)"
"enabled (fe n ! n0) msg"
"isReceiverOf p msg"
"correctInfinite fe ft p"
have MessageStaysOrConsumed: "⋀ n n1 n2 msg.
(n1 ≤ n2 ∧ n2 < length (fe n) ∧ (enabled (fe n ! n1) msg))
⟶ (enabled (fe n ! n2) msg)
∨ (∃ n0' ≥ n1. n0' < length (ft n) ∧ ft n ! n0' = msg)"
proof(auto)
fix n n1 n2 msg
assume Ass: "n1 ≤ n2" "n2 < length (fe n)" "enabled (fe n ! n1) msg"
"∀index<length (ft n). n1 ≤ index ⟶ ft n ! index ≠ msg"
have "∀ k ≤ n2 - n1 .
msgs (fe n ! n1) msg ≤ msgs (fe n ! (n1 + k)) msg"
proof(auto)
fix k
show "k ≤ n2 - n1 ⟹
msgs (fe n ! n1) msg ≤ msgs (fe n ! (n1 + k)) msg"
proof(induct k, auto)
fix k
assume IV: "msgs (fe n ! n1) msg ≤ msgs (fe n ! (n1 + k)) msg"
"Suc k ≤ n2 - n1"
from BasicProperties have Exec:
"execution trans sends start (fe n) (ft n)" by blast
have "n2 ≤ length (ft n)"
using Exec Ass(2)
execution.length[of trans sends start "fe n" "ft n"]
by simp
hence RightIndex: "n1 + k ≥ n1 ∧ n1 + k < length (ft n)"
using IV(2) by simp
have Step: "(fe n ! (n1 + k)) ⊢ (ft n ! (n1 + k))
↦ (fe n ! Suc (n1 + k))"
using Exec execution.step[of trans sends start "fe n" "ft n"
"n1 + k" "fe n ! (n1 + k)" "fe n ! (n1 + k + 1)"] IV(2)
Ass(2)
by simp
hence "msg ≠ (ft n ! (n1 + k))"
using Ass(4) Ass(2) IV(2) RightIndex Exec
execution.length[of trans sends start "fe n" "ft n"]
by blast
thus "msgs (fe n ! n1) msg ≤ msgs (fe n ! Suc (n1 + k)) msg"
using Step OtherMessagesOnlyGrowing[of "(fe n ! (n1 + k))"
"(ft n ! (n1 + k))" "(fe n ! Suc (n1 + k))" "msg"] IV(1)
by simp
qed
qed
hence "msgs (fe n ! n1) msg ≤ msgs (fe n ! n2) msg"
by (metis Ass(1) le_add_diff_inverse order_refl)
thus "enabled (fe n ! n2) msg" using Ass(3) enabled_def
by (metis gr0I leD)
qed
have EnabledOrConsumed: "enabled (fe n ! (length (fe n) - 1)) msg
∨ (∃n0'≥n0. n0' < length (ft n) ∧ ft n ! n0' = msg)"
using AssumptionFair(3) AssumptionFair(2)
MessageStaysOrConsumed[of "n0" "length (fe n) - 1" "n" "msg"]
by auto
have EnabledOrConsumedAtLast: "enabled (last (fe n)) msg ∨
(∃ n0' . n0' ≥ n0 ∧ n0' < length (ft n) ∧ (ft n) ! n0' = msg )"
using EnabledOrConsumed last_conv_nth AssumptionFair(2)
by (metis length_0_conv less_nat_zero_code)
have Case2ImplThesis: "(∃ n0' . n0' ≥ n0 ∧ n0' < length (ft n)
∧ ft n ! n0' = msg)
⟹ (∃n'≥n. ∃n0'≥n0. n0' < length (ft n') ∧ msg = ft n' ! n0')"
by auto
have Case1ImplThesis': "enabled (last (fe n)) msg
⟶ (∃n'≥n. ∃n0'≥ (length (ft n)). n0' < length (ft n')
∧ msg = ft n' ! n0')"
proof(clarify)
assume AssumptionCase1ImplThesis': "enabled (last (fe n)) msg"
show "∃n'≥n. ∃n0'≥length (ft n). n0' < length (ft n')
∧ msg = ft n' ! n0'"
proof(rule ccontr,simp)
assume AssumptionFairContr: "∀n'≥n. ∀n0'<length (ft n').
length (ft n) ≤ n0' ⟶ msg ≠ ft n' ! n0'"
define firstOccSet where "firstOccSet n = { msg1 . ∃ nMsg .
∃ n1 ≤ nMsg .
execution.firstOccurrence (fe n) (ft n) msg1 n1
∧ execution.firstOccurrence (fe n) (ft n) msg nMsg }" for n
have NotEmpty: "fe n ≠ []" using AssumptionFair(2)
by (metis less_nat_zero_code list.size(3))
have FirstToLast':
"∀ n . reachable ((fe n) ! 0) ((fe n) ! (length (fe n) - 1))"
using execution.ReachableInExecution BasicProperties execution.notEmpty
by (metis diff_less less_or_eq_imp_le not_gr0 not_one_le_zero)
hence FirstToLast: "∀ n . reachable (hd (fe n)) (last (fe n))"
using NotEmpty hd_conv_nth last_conv_nth AssumptionFair(1)
by (metis (full_types) One_nat_def length_0_conv
not_one_le_zero)
hence InitToLast: "∀ n . initReachable (last (fe n))"
using BasicProperties by auto
have "⋀ msg n0 . ∀ n .
(execution.firstOccurrence (fe n) (ft n) msg n0)
⟶ 0 < msgs (last (fe n)) msg"
using BasicProperties execution.firstOccurrence_def
enabled_def
by metis
hence "∀ n . ∀ msg' ∈ (firstOccSet n) .
0 < msgs (last (fe n)) msg'" using firstOccSet_def by blast
hence "∀ n . firstOccSet n ⊆ {msg. 0 < msgs (last (fe n)) msg}"
by (metis (lifting, full_types) mem_Collect_eq subsetI)
hence FiniteMsgs: "∀ n . finite (firstOccSet n)"
using FiniteMessages[OF finiteProcs finiteSends] InitToLast
by (metis rev_finite_subset)
have FirstOccSetDecrOrConsumed: "∀ index .
(enabled (last (fe index)) msg)
⟶ (firstOccSet (Suc index) ⊂ firstOccSet index
∧ (enabled (last (fe (Suc index))) msg)
∨ msg ∈ (set (drop (length (ft index)) (ft (Suc index)))))"
proof(clarify)
fix index
assume AssumptionFirstOccSetDecrOrConsumed:
"enabled (last (fe index)) msg"
"msg ∉ set (drop (length (ft index)) (ft (Suc index)))"
have NotEmpty: "fe (Suc index) ≠ []" "fe index ≠ []"
using BasicProperties
by (metis AssumptionFair(1) One_nat_def list.size(3)
not_one_le_zero)+
have LengthStep: "length (ft (Suc index)) > length (ft index)"
using AssumptionFair(1)
by (metis PrefixListMonotonicity)
have IPrefixList:
"∀ i::nat . prefixList (ft i) (ft (Suc i))"
using AssumptionFair(1) by auto
have IPrefixListEx:
"∀ i::nat . prefixList (fe i) (fe (Suc i))"
using AssumptionFair(1) by auto
have LastOfIndex:
"(fe (Suc index) ! (length (fe index) - Suc 0))
= (last (fe index))"
using PrefixSameOnLow[of "fe index" "fe (Suc index)"]
IPrefixListEx[rule_format, of index]
NotEmpty LengthStep
by (auto simp add: last_conv_nth)
have NotConsumedIntermediate:
"∀ i::nat < length (ft (Suc index)) .
(i ≥ length (ft index)
⟶ ft (Suc index) ! i ≠ msg)"
using AssumptionFirstOccSetDecrOrConsumed(2) ListLenDrop
by auto
hence
"¬(∃i. i < length (ft (Suc index)) ∧ i ≥ length (ft index)
∧ msg = (ft (Suc index)) ! i)"
using execution.length BasicProperties
by auto
hence "¬(∃i. i < length (fe (Suc index)) - 1
∧ i ≥ length (fe index) - 1
∧ msg = (ft (Suc index)) ! i)"
using BasicProperties[rule_format, of "Suc index"]
BasicProperties[rule_format, of "index"]
execution.length[of trans sends start]
by auto
hence EnabledIntermediate:
"∀ i < length (fe (Suc index)) . (i ≥ length (fe index) - 1
⟶ enabled (fe (Suc index) ! i) msg)"
using BasicProperties[rule_format, of "Suc index"]
BasicProperties[rule_format, of "index"]
execution.StaysEnabled[of trans sends start
"fe (Suc index)" "ft (Suc index)" "last (fe index)" msg
"length (fe index) - 1 "]
AssumptionFirstOccSetDecrOrConsumed(1)
by (auto, metis AssumptionFair(1) LastOfIndex
MessageStaysOrConsumed)
have "length (fe (Suc index)) - 1 ≥ length (fe index) - 1"
using PrefixListMonotonicity NotEmpty BasicProperties
by (metis AssumptionFair(1) diff_le_mono less_imp_le)
hence "enabled (fe (Suc index)
! (length (fe (Suc index)) - 1)) msg"
using EnabledIntermediate NotEmpty(1)
by (metis diff_less length_greater_0_conv zero_less_one)
hence EnabledInSuc: "enabled (last (fe (Suc index))) msg"
using NotEmpty last_conv_nth[of "fe (Suc index)"] by simp
have IndexIsExec:
"execution trans sends start (fe index) (ft index)"
using BasicProperties by blast
have SucIndexIsExec:
"execution trans sends start (fe (Suc index))
(ft (Suc index))"
using BasicProperties by blast
have SameCfgOnLow: "∀ i < length (fe index) . (fe index) ! i
= (fe (Suc index)) ! i"
using BasicProperties PrefixSameOnLow by auto
have SameMsgOnLow: "∀ i < length (ft index) . (ft index) ! i
= (ft (Suc index)) ! i"
using BasicProperties PrefixSameOnLow by auto
have SmallIndex: "⋀ nMsg . execution.firstOccurrence
(fe (Suc index)) (ft (Suc index)) msg nMsg
⟹ nMsg < length (fe index)"
proof(-)
fix nMsg
assume "execution.firstOccurrence (fe (Suc index))
(ft (Suc index)) msg nMsg"
hence AssumptionSubset3:
"∃p. isReceiverOf p msg"
"enabled (last (fe (Suc index))) msg"
"nMsg < length (fe (Suc index))"
"enabled (fe (Suc index) ! nMsg) msg"
"∀n'≥nMsg. n' < length (ft (Suc index))
⟶ msg ≠ ft (Suc index) ! n'"
"nMsg ≠ 0 ⟶ ¬ enabled (fe (Suc index) ! (nMsg - 1))
msg ∨ msg = ft (Suc index) ! (nMsg - 1)"
using execution.firstOccurrence_def[of "trans" "sends"
"start" "fe (Suc index)" "ft (Suc index)" "msg" "nMsg"]
SucIndexIsExec by auto
show "nMsg < length (fe index)"
proof(rule ccontr)
assume AssumpSmallIndex: "¬ nMsg < length (fe index)"
have "fe index ≠ []" using BasicProperties
AssumptionFair(1)
by (metis One_nat_def list.size(3) not_one_le_zero)
hence "length (fe index) > 0"
by (metis length_greater_0_conv)
hence nMsgNotZero: "nMsg ≠ 0"
using AssumpSmallIndex by metis
hence SucCases: "¬ enabled ((fe (Suc index)) ! (nMsg - 1))
msg ∨ msg = (ft (Suc index)) ! (nMsg - 1)"
using AssumptionSubset3(6) by blast
have Cond1: "nMsg - 1 ≥ length (fe index) - 1"
using AssumpSmallIndex by (metis diff_le_mono leI)
hence Enabled: "enabled (fe (Suc index) ! (nMsg - 1)) msg"
using EnabledIntermediate AssumptionSubset3(3)
by (metis less_imp_diff_less)
have Cond2: "nMsg - 1 ≥ length (ft index) ∧ nMsg - 1
< length (ft (Suc index))"
using Cond1 execution.length[of "trans" "sends" "start"
"fe index" "ft index"]
IndexIsExec AssumptionSubset3(3)
by (simp, metis AssumptionFair(1) One_nat_def Suc_diff_1
Suc_eq_plus1 less_diff_conv nMsgNotZero neq0_conv)
hence NotConsumed: "ft (Suc index) ! (nMsg - 1) ≠ msg"
using NotConsumedIntermediate by simp
show False using SucCases Enabled NotConsumed
by blast
qed
qed
have Subset: "⋀ msgInSet . msgInSet ∈ firstOccSet (Suc index)
⟹ msgInSet ∈ firstOccSet index"
unfolding firstOccSet_def
proof(auto)
fix msgInSet nMsg n1
assume AssumptionSubset: "n1 ≤ nMsg"
"execution.firstOccurrence (fe (Suc index))
(ft (Suc index)) msgInSet n1"
"execution.firstOccurrence (fe (Suc index))
(ft (Suc index)) msg nMsg"
have AssumptionSubset2:
"∃p. isReceiverOf p msgInSet"
"enabled (last (fe (Suc index))) msgInSet"
"n1 < length (fe (Suc index))"
"enabled (fe (Suc index) ! n1) msgInSet"
"∀n'≥n1. n' < length (ft (Suc index))
⟶ msgInSet ≠ ft (Suc index) ! n'"
"n1 ≠ 0 ⟶ ¬ enabled (fe (Suc index) ! (n1 - 1))
msgInSet ∨ msgInSet = ft (Suc index) ! (n1 - 1)"
using execution.firstOccurrence_def[of "trans" "sends"
"start" "fe (Suc index)" "ft (Suc index)" "msgInSet"
"n1"] AssumptionSubset(2) SucIndexIsExec by auto
have AssumptionSubset3:
"∃p. isReceiverOf p msg"
"enabled (last (fe (Suc index))) msg"
"nMsg < length (fe (Suc index))"
"enabled (fe (Suc index) ! nMsg) msg"
"∀n'≥nMsg. n' < length (ft (Suc index))
⟶ msg ≠ ft (Suc index) ! n'"
"nMsg ≠ 0 ⟶ ¬ enabled (fe (Suc index) ! (nMsg - 1))
msg ∨ msg = ft (Suc index) ! (nMsg - 1)"
using execution.firstOccurrence_def[of "trans" "sends"
"start" "fe (Suc index)" "ft (Suc index)" "msg" "nMsg"]
AssumptionSubset(3) SucIndexIsExec by auto
have ShorterTrace: "length (ft index)
< length (ft (Suc index))"
using PrefixListMonotonicity BasicProperties by auto
have FirstOccurrenceMsg: "execution.firstOccurrence
(fe index) (ft index) msg nMsg"
proof-
have Occ1: "∃ p . isReceiverOf p msg"
using AssumptionSubset3(1) by blast
have Occ2: "enabled (last (fe index)) msg"
using AssumptionFirstOccSetDecrOrConsumed by blast
have "(fe index) ! nMsg = (fe (Suc index)) ! nMsg"
using SmallIndex AssumptionSubset(3)
PrefixSameOnLow[of "fe index" "fe (Suc index)"]
BasicProperties
by simp
hence Occ4: "enabled ((fe index) ! nMsg) msg"
using AssumptionSubset3(4) by simp
have OccSameMsg: "∀ n' ≥ nMsg . n' < length (ft index)
⟶ (ft index) ! n' = (ft (Suc index)) ! n'"
using PrefixSameOnLow BasicProperties by auto
hence Occ5: "∀ n' ≥ nMsg . n' < length (ft index)
⟶ msg ≠ ((ft index) ! n')"
using AssumptionSubset3(5) ShorterTrace by simp
have Occ6: "nMsg ≠ 0 ⟶ (¬ enabled ((fe index) !
(nMsg - 1)) msg ∨ msg = (ft index ) ! (nMsg - 1))"
proof(clarify)
assume AssumpOcc6: "0 < nMsg" "msg ≠ ft index !
(nMsg - 1)" "enabled (fe index ! (nMsg - 1)) msg"
have "nMsg - (Suc 0) < length (fe index) - (Suc 0)"
using SmallIndex AssumptionSubset(3) AssumpOcc6(1)
by (metis Suc_le_eq diff_less_mono)
hence SmallIndexTrace: "nMsg - 1 < length (ft index)"
using IndexIsExec execution.length
by (metis One_nat_def)
have "¬ enabled (fe (Suc index) ! (nMsg - 1)) msg
∨ msg = ft (Suc index) ! (nMsg - 1)"
using AssumptionSubset3(6) AssumpOcc6(1) by blast
moreover have "fe (Suc index) ! (nMsg - 1)
= fe index ! (nMsg - 1)"
using SameCfgOnLow SmallIndex AssumptionSubset(3)
by (metis less_imp_diff_less)
moreover have "ft (Suc index) ! (nMsg - 1)
= ft index ! (nMsg - 1)"
using SameMsgOnLow SmallIndexTrace by metis
ultimately have "¬ enabled (fe index ! (nMsg - 1)) msg
∨ msg = ft index ! (nMsg - 1)"
by simp
thus False using AssumpOcc6 by blast
qed
show ?thesis using IndexIsExec Occ1 Occ2 SmallIndex
AssumptionSubset(3) Occ4 Occ5 Occ6
execution.firstOccurrence_def[of "trans" "sends" "start"
"fe index" "ft index"]
by simp
qed
have "execution.firstOccurrence (fe index) (ft index)
msgInSet n1"
using AssumptionSubset2 AssumptionSubset(1)
proof-
have Occ1': "∃p. isReceiverOf p msgInSet"
using AssumptionSubset2(1) by blast
have Occ3': "n1 < length (fe index)"
using SmallIndex AssumptionSubset(3) AssumptionSubset(1)
by (metis le_less_trans)
have "(fe index) ! n1 = (fe (Suc index)) ! n1"
using Occ3' PrefixSameOnLow[of "fe index"
"fe (Suc index)"] BasicProperties by simp
hence Occ4': "enabled (fe index ! n1) msgInSet"
using AssumptionSubset2(4) by simp
have OccSameMsg': "∀ n' ≥ n1 . n' < length (ft index)
⟶ (ft index) ! n' = (ft (Suc index)) ! n'"
using PrefixSameOnLow BasicProperties by auto
hence Occ5': "∀n' ≥ n1. n' < length (ft index)
⟶ msgInSet ≠ ft index ! n'"
using AssumptionSubset2(5) ShorterTrace by simp
have "length (fe index) > 0" using NotEmpty(2)
by (metis length_greater_0_conv)
hence "length (fe index) - 1 < length (fe index)"
by (metis One_nat_def diff_Suc_less)
hence
"enabled (fe index ! (length (fe index) - 1)) msgInSet
∨ (∃n0'≥n1. n0' < length (ft index) ∧ ft index ! n0'
= msgInSet)"
using Occ4' Occ3' MessageStaysOrConsumed[of "n1"
"length (fe index) - 1" "index" "msgInSet"]
by (metis Suc_pred' ‹0 < length (fe index)›
not_le not_less_eq_eq)
hence "enabled ((fe index) ! (length (fe index) - 1))
msgInSet"
using Occ5' by auto
hence Occ2': "enabled (last (fe index)) msgInSet"
using last_conv_nth[of "fe index"] NotEmpty(2) by simp
have Occ6': "n1 ≠ 0 ⟶ ¬ enabled (fe index ! (n1 - 1))
msgInSet ∨ msgInSet = ft index ! (n1 - 1)"
proof(clarify)
assume AssumpOcc6': "0 < n1" "msgInSet ≠ ft index !
(n1 - 1)" "enabled (fe index ! (n1 - 1)) msgInSet"
have "n1 - (Suc 0) < length (fe index) - (Suc 0)"
using Occ3' AssumpOcc6'(1)
by (metis Suc_le_eq diff_less_mono)
hence SmallIndexTrace': "n1 - 1 < length (ft index)"
using IndexIsExec execution.length
by (metis One_nat_def)
have "¬ enabled (fe (Suc index) ! (n1 - 1)) msgInSet
∨ msgInSet = ft (Suc index) ! (n1 - 1)"
using AssumptionSubset2(6) AssumpOcc6'(1) by blast
moreover have "fe (Suc index) ! (n1 - 1)
= fe index ! (n1 - 1)"
using SameCfgOnLow Occ3' by (metis less_imp_diff_less)
moreover have "ft (Suc index) ! (n1 - 1)
= ft index ! (n1 - 1)"
using SameMsgOnLow SmallIndexTrace' by metis
ultimately have "¬ enabled (fe index !
(n1 - 1)) msgInSet ∨ msgInSet = ft index ! (n1 - 1)"
by simp
thus False using AssumpOcc6' by blast
qed
show ?thesis using IndexIsExec Occ1' Occ2' Occ3' Occ4'
Occ5' Occ6'
execution.firstOccurrence_def[of "trans" "sends"
"start" "fe index" "ft index"]
by simp
qed
thus "∃nMsg' n1'. n1' ≤ nMsg'
∧ execution.firstOccurrence (fe index) (ft index)
msgInSet n1'
∧ execution.firstOccurrence (fe index) (ft index)
msg nMsg'"
using FirstOccurrenceMsg AssumptionSubset(1) by blast
qed
have ProperSubset: "∃ msg' .msg' ∈ firstOccSet index
∧ msg' ∉ firstOccSet (Suc index)"
proof-
have "initial (hd (fe index))" using AssumptionFair(1)
by blast
hence "∃msg'. execution.minimalEnabled (fe index) (ft index)
msg' ∧ msg' ∈ set (drop (length (ft index))
(fStepMsg (fe index) (ft index)))"
using FStep fe_def ft_def
BasicProperties by simp
then obtain consumedMsg where ConsumedMsg:
"execution.minimalEnabled (fe index) (ft index)
consumedMsg"
"consumedMsg ∈ set (drop (length (ft index))
(fStepMsg (fe index) (ft index)))" by blast
hence ConsumedIsInDrop:
"consumedMsg ∈ set (drop (length (ft index)) (ft (Suc index)))"
using fe_def ft_def FStep
BasicProperties[rule_format, of index]
by auto
have MinImplAllBigger: "⋀ msg' . execution.minimalEnabled
(fe index) (ft index) msg'
⟶ (∃ OccM' . (execution.firstOccurrence (fe index)
(ft index) msg' OccM' )
∧ (∀ msg . ∀ OccM . execution.firstOccurrence (fe index)
(ft index) msg OccM
⟶ OccM' ≤ OccM))"
proof(auto)
fix msg'
assume AssumpMinImplAllBigger: "execution.minimalEnabled
(fe index) (ft index) msg'"
have IsExecIndex: "execution trans sends start
(fe index) (ft index)"
using BasicProperties[rule_format, of index] by simp
have "(∃ p . isReceiverOf p msg') ∧
(enabled (last (fe index)) msg')
∧ (∃ n . n < length (fe index)
∧ enabled ( (fe index) ! n) msg'
∧ (∀ n' ≥ n . n' < length (ft index)
⟶ msg' ≠ ((ft index)! n'))
∧ (∀ n' msg' . ((∃ p . isReceiverOf p msg')
∧ (enabled (last (fe index)) msg')
∧ n' < length (ft index)
∧ enabled ((fe index)! n') msg'
∧ (∀ n'' ≥ n' . n'' < length (ft index)
⟶ msg' ≠ ((ft index) ! n''))) ⟶ n' ≥ n))"
using execution.minimalEnabled_def[of trans sends start
"(fe index)" "(ft index)" msg']
AssumpMinImplAllBigger IsExecIndex by auto
then obtain OccM' where OccM':
"(∃ p . isReceiverOf p msg')"
"(enabled (last (fe index)) msg')"
"OccM' < length (fe index)"
"enabled ( (fe index) ! OccM') msg'"
"(∀ n' ≥ OccM' . n' < length (ft index)
⟶ msg' ≠ ((ft index)! n'))"
"(∀ n' msg' . ((∃ p . isReceiverOf p msg')
∧ (enabled (last (fe index)) msg')
∧ n' < length (ft index)
∧ enabled ((fe index)! n') msg'
∧ (∀ n'' ≥ n' . n'' < length (ft index)
⟶ msg' ≠ ((ft index) ! n''))) ⟶ n' ≥ OccM')"
by blast
have "0 < OccM' ⟹ enabled (fe index ! (OccM' - Suc 0)) msg'
⟹ msg' ≠ ft index ! (OccM' - Suc 0) ⟹ False"
proof(-)
fix p
assume AssumpContr:
"0 < OccM'"
"enabled (fe index ! (OccM' - Suc 0)) msg'"
"msg' ≠ ft index ! (OccM' - Suc 0)"
have LengthOccM': "(OccM' - 1) < length (ft index)"
using OccM'(3) IndexIsExec AssumpContr(1)
AssumptionFair(1)
by (metis One_nat_def Suc_diff_1 Suc_eq_plus1_left
Suc_less_eq le_add_diff_inverse)
have BiggerIndices: "(∀n''≥(OccM' - 1).
n'' < length (ft index) ⟶ msg' ≠ ft index ! n'')"
using OccM'(5) by (metis AssumpContr(3) One_nat_def
Suc_eq_plus1 diff_Suc_1 le_SucE le_diff_conv)
have "(∃p. isReceiverOf p msg') ∧ enabled (last
(fe index)) msg' ∧ (OccM' - 1) < length (ft index)
∧ enabled (fe index ! (OccM' - 1)) msg'
∧ (∀n''≥(OccM' - 1). n'' < length (ft index)
⟶ msg' ≠ ft index ! n'')"
using OccM' LengthOccM' AssumpContr BiggerIndices
by simp
hence "OccM' ≤ OccM' - 1" using OccM'(6) by blast
thus False using AssumpContr(1) diff_less leD zero_less_one by blast
qed
hence FirstOccMsg': "execution.firstOccurrence (fe index)
(ft index) msg' OccM'"
unfolding execution_def
execution.firstOccurrence_def[OF IsExecIndex, of msg' OccM']
by (auto simp add: OccM'(1,2,3,4,5))
have "∀msg OccM. execution.firstOccurrence (fe index)
(ft index) msg OccM ⟶ OccM' ≤ OccM"
proof clarify
fix msg OccM
assume "execution.firstOccurrence (fe index)
(ft index) msg OccM"
hence AssumpOccMFirstOccurrence:
"∃ p . isReceiverOf p msg"
"enabled (last (fe index)) msg"
"OccM < (length (fe index))"
"enabled ((fe index) ! OccM) msg"
"(∀ n' ≥ OccM . n' < length (ft index)
⟶ msg ≠ ((ft index) ! n'))"
"(OccM ≠ 0 ⟶ (¬ enabled ((fe index) ! (OccM - 1))
msg ∨ msg = (ft index)!(OccM - 1)))"
by (auto simp add: execution.firstOccurrence_def[of
trans sends start "(fe index)" "(ft index)"
msg OccM] IsExecIndex)
hence "(∃p. isReceiverOf p msg) ∧
enabled (last (fe index)) msg ∧
enabled (fe index ! OccM) msg ∧
(∀n''≥ OccM. n'' < length (ft index)
⟶ msg ≠ ft index ! n'')"
by simp
thus "OccM' ≤ OccM" using OccM'
proof(cases "OccM < length (ft index)",auto)
assume "¬ OccM < length (ft index)"
hence "OccM ≥ length (fe index) - 1"
using AssumptionFair(1) by (metis One_nat_def leI)
hence "OccM = length (fe index) - 1"
using AssumpOccMFirstOccurrence(3) by simp
thus "OccM' ≤ OccM" using OccM'(3) by simp
qed
qed
with FirstOccMsg' show "∃OccM'.
execution.firstOccurrence (fe index) (ft index)
msg' OccM'
∧ (∀msg OccM. execution.firstOccurrence (fe index)
(ft index) msg OccM ⟶ OccM' ≤ OccM)" by blast
qed
have MinImplFirstOcc: "⋀ msg' . execution.minimalEnabled
(fe index) (ft index) msg'
⟹ msg' ∈ firstOccSet index"
proof -
fix msg'
assume AssumpMinImplFirstOcc:
"execution.minimalEnabled (fe index) (ft index) msg'"
then obtain OccM' where OccM':
"execution.firstOccurrence (fe index) (ft index)
msg' OccM'"
"∀ msg . ∀ OccM . execution.firstOccurrence
(fe index) (ft index) msg OccM
⟶ OccM' ≤ OccM" using MinImplAllBigger by blast
thus "msg' ∈ firstOccSet index" using OccM'
proof (auto simp add: firstOccSet_def)
have "enabled (last (fe index)) msg"
using AssumptionFirstOccSetDecrOrConsumed(1) by blast
hence "∃nMsg . execution.firstOccurrence (fe index)
(ft index) msg nMsg"
using execution.FirstOccurrenceExists IndexIsExec
AssumptionFair(4) by blast
then obtain nMsg where NMsg: "execution.firstOccurrence
(fe index) (ft index) msg nMsg" by blast
hence "OccM' ≤ nMsg" using OccM' by simp
hence "∃nMsg . OccM' ≤ nMsg ∧
execution.firstOccurrence (fe index) (ft index) msg'
OccM' ∧
execution.firstOccurrence (fe index) (ft index) msg
nMsg"
using OccM'(1) NMsg by blast
thus "∃nMsg n1 . n1 ≤ nMsg ∧
execution.firstOccurrence (fe index) (ft index)
msg' n1 ∧
execution.firstOccurrence (fe index) (ft index)
msg nMsg" by blast
qed
qed
hence ConsumedInSet: "consumedMsg ∈ firstOccSet index"
using ConsumedMsg by simp
have GreaterOccurrence: "⋀ nMsg n1 .
execution.firstOccurrence (fe (Suc index))
(ft (Suc index)) consumedMsg n1 ∧
execution.firstOccurrence (fe (Suc index))
(ft (Suc index)) msg nMsg
⟹ nMsg < n1"
proof(rule ccontr,auto)
fix nMsg n1
assume AssumpGreaterOccurrence: "¬ nMsg < n1"
"execution.firstOccurrence (fe (Suc index))
(ft (Suc index)) consumedMsg n1"
"execution.firstOccurrence (fe (Suc index))
(ft (Suc index)) msg nMsg"
have "nMsg < length (fe index)"
using SmallIndex AssumpGreaterOccurrence(3) by simp
hence "n1 < length (fe index)"
using AssumpGreaterOccurrence(1)
by (metis less_trans nat_neq_iff)
hence N1Small: "n1 ≤ length (ft index)"
using IndexIsExec AssumptionFair(1)
by (metis One_nat_def Suc_eq_plus1 le_diff_conv2
not_le not_less_eq_eq)
have NotConsumed: "∀ i ≥ n1 . i < length (ft (Suc index))
⟶ consumedMsg ≠ (ft (Suc index)) ! i"
using execution.firstOccurrence_def[of "trans" "sends"
"start" "fe (Suc index)" "ft (Suc index)"
"consumedMsg" "n1"]
AssumpGreaterOccurrence(2) SucIndexIsExec by auto
have "∃ i ≥ length (ft index) .
i < length (ft (Suc index))
∧ consumedMsg = (ft (Suc index)) ! i"
using DropToIndex[of "consumedMsg" "length (ft index)"]
ConsumedIsInDrop by simp
then obtain i where IDef: "i ≥ length (ft index)"
"i < length (ft (Suc index))"
"consumedMsg = (ft (Suc index)) ! i" by blast
thus False using NotConsumed N1Small by simp
qed
have "consumedMsg ∉ firstOccSet (Suc index)"
proof(clarify)
assume AssumpConsumedInSucSet:
"consumedMsg ∈ firstOccSet (Suc index)"
hence "∃nMsg n1. n1 ≤ nMsg ∧
execution.firstOccurrence (fe (Suc index))
(ft (Suc index)) consumedMsg n1 ∧
execution.firstOccurrence (fe (Suc index))
(ft (Suc index)) msg nMsg"
using firstOccSet_def by blast
thus False using GreaterOccurrence
by (metis less_le_trans less_not_refl3)
qed
thus ?thesis using ConsumedInSet by blast
qed
hence "firstOccSet (Suc index) ⊂ firstOccSet index"
using Subset by blast
thus "firstOccSet (Suc index) ⊂ firstOccSet index
∧ enabled (last (fe (Suc index))) msg"
using EnabledInSuc by blast
qed
have NotConsumed: "∀ index ≥ n . ¬ msg ∈
(set (drop (length (ft index)) (ft (Suc index))))"
proof(clarify)
fix index
assume AssumpMsgNotConsumed: "n ≤ index"
"msg ∈ set (drop (length (ft index)) (ft (Suc index)))"
have "∃ n0' ≥ length (ft index) .
n0' < length (ft (Suc index))
∧ msg = (ft (Suc index)) ! n0'"
using AssumpMsgNotConsumed(2) DropToIndex[of "msg"
"length (ft index)" "ft (Suc index)"] by auto
then obtain n0' where MessageIndex: "n0' ≥ length (ft index)"
"n0' < length (ft (Suc index))"
"msg = (ft (Suc index)) ! n0'" by blast
have LengthIncreasing: "length (ft n) ≤ length (ft index)"
using AssumpMsgNotConsumed(1)
proof(induct index,auto)
fix indexa
assume AssumpLengthIncreasing:
"n ≤ indexa ⟹ length (ft n) ≤ length (ft indexa)"
"n ≤ Suc indexa" "n ≤ index"
show "length (ft n) ≤ length (ft (Suc indexa))"
proof(cases "n = Suc indexa",auto)
assume "n ≠ Suc indexa"
hence "n ≤ indexa" using AssumpLengthIncreasing(2)
by (metis le_SucE)
hence LengthNA: "length (ft n) ≤ length (ft indexa)"
using AssumpLengthIncreasing(1) by blast
have PrefixIndexA: "prefixList (ft indexa) (ft (Suc indexa))"
using BasicProperties by simp
show "length (ft n) ≤ length (ft (Suc indexa))"
using LengthNA PrefixListMonotonicity[OF PrefixIndexA]
by (metis (opaque_lifting, no_types) antisym le_cases
less_imp_le less_le_trans)
qed
qed
thus False using AssumptionFairContr MessageIndex
AssumpMsgNotConsumed(1)
by (metis ‹length (ft index) ≤ n0'› le_SucI le_trans)
qed
hence FirstOccSetDecrImpl:
"∀ index ≥ n . (enabled (last (fe index)) msg)
⟶ firstOccSet (Suc index) ⊂ firstOccSet index
∧ (enabled (last (fe (Suc index))) msg)"
using FirstOccSetDecrOrConsumed by blast
hence FirstOccSetDecrImpl: "∀ index ≥ n . firstOccSet
(Suc index) ⊂ firstOccSet index"
using KeepProperty[of "n" "λx.(enabled (last (fe x)) msg)"
"λx.(firstOccSet (Suc x) ⊂ firstOccSet x)"]
AssumptionCase1ImplThesis' by blast
hence FirstOccSetDecr': "∀ index ≥ n .
card (firstOccSet (Suc index)) < card (firstOccSet index)"
using FiniteMsgs psubset_card_mono by metis
hence "card (firstOccSet (n + (card (firstOccSet n) + 1)))
≤ card (firstOccSet n) - (card (firstOccSet n) + 1)"
using SmallerMultipleStepsWithLimit[of "n"
"λx. card (firstOccSet x)" "card (firstOccSet n) + 1"]
by blast
hence IsNegative:"card (firstOccSet (n + (card
(firstOccSet n) + 1))) < 0"
by (metis FirstOccSetDecr' diff_add_zero leD le_add1
less_nat_zero_code neq0_conv)
thus False by (metis less_nat_zero_code)
qed
qed
hence Case1ImplThesis: "enabled (last (fe n)) msg
⟹ (∃n'≥n. ∃n0'≥n0. n0' < length (ft n') ∧ msg = ft n' ! n0')"
using AssumptionFair(2) execution.length[of trans sends start
"fe n" "ft n"] BasicProperties
by (metis One_nat_def Suc_eq_plus1 Suc_lessI leI le_less_trans
less_asym less_diff_conv)
show "∃n'≥n. ∃n0'≥n0. n0' < length (ft n') ∧ msg = ft n' ! n0'"
using disjE[OF EnabledOrConsumedAtLast Case1ImplThesis Case2ImplThesis] .
qed
show ?thesis proof (rule exI[of _ fe], rule exI[of _ ft])
show "fe 0 = [cfg] ∧ fairInfiniteExecution fe ft
∧ (∀n. nonUniform (last (fe n)) ∧ prefixList (fe n) (fe (n + 1))
∧ prefixList (ft n) (ft (n + 1))
∧ execution trans sends start (fe n) (ft n))"
using Fair fe_def FStep BasicProperties by auto
qed
qed
subsection ‹Contradiction›
text ‹
An infinite execution is said to be a terminating FLP execution if each process
at some point sends a decision message or if it stops, which is expressed
by the process not processing any further messages.
›
definition (in flpSystem) terminationFLP::
"(nat ⇒ ('p, 'v, 's) configuration list)
⇒ (nat ⇒ ('p, 'v) message list) ⇒ bool"
where
"terminationFLP fe ft ≡ infiniteExecution fe ft ⟶
(∀ p . ∃ n .
(∃ i0 < length (ft n). ∃ b .
(<⊥, outM b> ∈# sends p (states ((fe n) ! i0) p) (unpackMessage ((ft n) ! i0)))
∧ isReceiverOf p ((ft n) ! i0))
∨ (∀ n1 > n . ∀ m ∈ set (drop (length (ft n)) (ft n1)) . ¬ isReceiverOf p m))"
theorem ConsensusFails:
assumes
Termination:
"⋀ fe ft . (fairInfiniteExecution fe ft ⟹ terminationFLP fe ft)" and
Validity: "∀ i c . validity i c" and
Agreement: "∀ i c . agreementInit i c"
shows
"False"
proof -
obtain cfg where Cfg: "initial cfg" "nonUniform cfg"
using InitialNonUniformCfg[OF PseudoTermination Validity Agreement]
by blast
obtain fe:: "nat ⇒ ('p, 'v, 's) configuration list" and
ft:: "nat ⇒ ('p, 'v) message list"
where FE: "(fe 0) = [cfg]" "fairInfiniteExecution fe ft"
"(∀(n::nat) . nonUniform (last (fe n))
∧ prefixList (fe n) (fe (n+1))
∧ prefixList (ft n) (ft (n+1))
∧ (execution trans sends start (fe n) (ft n)))"
using FairNonUniformExecution[OF Cfg]
by blast
have AllArePrefixesExec: "∀ m . ∀ n > m . prefixList (fe m) (fe n)"
proof(clarify)
fix m::nat and n::nat
assume MLessN: "m < n"
have "prefixList (fe m) (fe n)" using MLessN
proof(induct n, simp)
fix n
assume IA: "(m < n) ⟹ (prefixList (fe m) (fe n))" "m < (Suc n)"
have "m = n ∨ m < n" using IA(2) by (metis less_SucE)
thus "prefixList (fe m) (fe (Suc n))"
proof(cases "m = n", auto)
show "prefixList (fe n) (fe (Suc n))" using FE by simp
next
assume "m < n"
hence IA2: "prefixList (fe m) (fe n)" using IA(1) by simp
have "prefixList (fe n) (fe (n+1))" using FE by simp
thus "prefixList (fe m) (fe (Suc n))" using PrefixListTransitive
IA2 by simp
qed
qed
thus "prefixList (fe m) (fe n)" by simp
qed
have AllArePrefixesTrace: "∀ m . ∀ n > m . prefixList (ft m) (ft n)"
proof(clarify)
fix m::nat and n::nat
assume MLessN: "m < n"
have "prefixList (ft m) (ft n)" using MLessN
proof(induct n, simp)
fix n
assume IA: "(m < n) ⟹ (prefixList (ft m) (ft n))" "m < (Suc n)"
have "m = n ∨ m < n" using IA(2) by (metis less_SucE)
thus "prefixList (ft m) (ft (Suc n))"
proof(cases "m = n", auto)
show "prefixList (ft n) (ft (Suc n))" using FE by simp
next
assume "m < n"
hence IA2: "prefixList (ft m) (ft n)" using IA(1) by simp
have "prefixList (ft n) (ft (n+1))" using FE by simp
thus "prefixList (ft m) (ft (Suc n))" using PrefixListTransitive
IA2 by simp
qed
qed
thus "prefixList (ft m) (ft n)" by simp
qed
have Length: "∀ n . length (fe n) ≥ n + 1"
proof(clarify)
fix n
show "length (fe n) ≥ n + 1"
proof(induct n, simp add: FE(1))
fix n
assume IH: "(n + (1::nat)) ≤ (length (fe n))"
have "length (fe (n+1)) ≥ length (fe n) + 1" using FE(3)
PrefixListMonotonicity
by (metis Suc_eq_plus1 Suc_le_eq)
thus "(Suc n) + (1::nat) ≤ (length (fe (Suc n)))" using IH by auto
qed
qed
have AllExecsFromInit: "∀ n . ∀ n0 < length (fe n) .
reachable cfg ((fe n) ! n0)"
proof(clarify)
fix n::nat and n0::nat
assume "n0 < length (fe n)"
thus "reachable cfg ((fe n) ! n0)"
proof(cases "0 = n", auto)
assume N0Less: "n0 < length (fe 0)"
have NoStep: "reachable cfg cfg" using reachable.simps by blast
have "length (fe 0) = 1" using FE(1) by simp
hence N0Zero: "n0 = 0" using N0Less FE by simp
hence "(fe 0) ! n0 = cfg" using FE(1) by simp
thus "reachable cfg ((fe 0) ! n0)" using FE(1) NoStep N0Zero by simp
next
assume NNotZero: "0 < n" "n0 < (length (fe n))"
have ZeroCfg: "(fe 0) = [cfg]" using FE by simp
have "prefixList (fe 0) (fe n)" using AllArePrefixesExec NNotZero
by simp
hence PrList: "prefixList [cfg] (fe n)" using ZeroCfg by simp
have CfgFirst: "cfg = (fe n) ! 0"
using prefixList.cases[OF PrList]
by (metis (full_types) ZeroCfg list.distinct(1) nth_Cons_0)
have "reachable ((fe n) ! 0) ((fe n) ! n0)"
using execution.ReachableInExecution FE NNotZero(2) by (metis le0)
thus "(reachable cfg ((fe n) ! n0))" using assms CfgFirst by simp
qed
qed
have NoDecided: "(∀ n n0 v . (n0 < length (fe n))
⟶ ¬ vDecided v ((fe n) ! n0))"
proof(clarify)
fix n n0 v
assume AssmNoDecided: "n0 < length (fe n)"
"initReachable ((fe n) ! n0)"
"0 < (msgs ((fe n) ! n0) <⊥, outM v>)"
have LastNonUniform: "nonUniform (last (fe n))" using FE by simp
have LastIsLastIndex: "⋀ l . l ≠ [] ⟶ last l = l ! ((length l) - 1)"
by (metis last_conv_nth)
have Fou: "n0 ≤ length (fe n) - 1" using AssmNoDecided by simp
have FeNNotEmpty:"fe n ≠ []" using FE(1) AllArePrefixesExec
by (metis AssmNoDecided(1) less_nat_zero_code list.size(3))
hence Fou2: "length (fe n) - 1 < length (fe n)" by simp
have "last (fe n) = (fe n) ! (length (fe n) - 1)"
using LastIsLastIndex FeNNotEmpty by auto
have LastNonUniform: "nonUniform (last (fe n))" using FE by simp
have "reachable ((fe n) ! n0) ((fe n) ! (length (fe n) - 1))"
using FE execution.ReachableInExecution Fou Fou2 by metis
hence N0ToLast: "reachable ((fe n) ! n0) (last (fe n))"
using LastIsLastIndex[of "fe n"] FeNNotEmpty by simp
hence LastVDecided: "vDecided v (last (fe n))"
using NoOutMessageLoss[of "((fe n) ! n0)" "(last (fe n))"]
AssmNoDecided
by (simp,
metis LastNonUniform le_neq_implies_less less_nat_zero_code neq0_conv)
have AllAgree: "∀ cfg' . reachable (last (fe n)) cfg'
⟶ agreement cfg'"
proof(clarify)
fix cfg'
assume LastToNext: "reachable (last (fe n)) cfg'"
hence "reachable cfg ((fe n) ! (length (fe n) - 1))"
using AllExecsFromInit AssmNoDecided(1) by auto
hence "reachable cfg (last (fe n))" using LastIsLastIndex[of "fe n"]
FeNNotEmpty by simp
hence FirstToLast: "reachable cfg cfg'" using initReachable_def Cfg
LastToNext ReachableTrans by blast
hence "agreementInit cfg cfg'" using Agreement by simp
hence "∀v1. (<⊥, outM v1> ∈# msgs cfg') ⟶ (∀v2. (<⊥, outM v2> ∈#
msgs cfg') ⟷ v2 = v1)"
using Cfg FirstToLast
by (simp add: agreementInit_def)
thus "agreement cfg'" by (simp add: agreement_def)
qed
thus "False" using NonUniformImpliesNotDecided LastNonUniform
PseudoTermination LastVDecided by simp
qed
have Termination: "terminationFLP fe ft" using assms(1)[OF FE(2)] .
hence AllDecideOrCrash:
"∀p. ∃n .
(∃ i0 < length (ft n) . ∃b.
(<⊥, outM b> ∈#
sends p (states (fe n ! i0) p) (unpackMessage (ft n ! i0)))
∧ isReceiverOf p (ft n ! i0))
∨ (∀ n1 > n . ∀ m ∈ (set (drop (length (ft n)) (ft n1))) .
¬ isReceiverOf p m)"
using FE(2)
unfolding terminationFLP_def fairInfiniteExecution_def
by blast
have "∀ p . ∃ n . (∀ n1 > n . ∀ m ∈ (set (drop (length (ft n)) (ft n1))) .
¬ isReceiverOf p m)"
proof(clarify)
fix p
from AllDecideOrCrash have
"∃ n .
(∃ i0 < length (ft n) . ∃b.
(<⊥, outM b> ∈# sends p (states (fe n ! i0) p) (unpackMessage (ft n ! i0)))
∧ isReceiverOf p (ft n ! i0))
∨ (∀ n1 > n . ∀ m ∈ (set (drop (length (ft n)) (ft n1))).
¬ isReceiverOf p m)" by simp
hence "(∃ n . ∃ i0 < length (ft n) .
(∃b. (<⊥, outM b> ∈#
sends p (states (fe n ! i0) p) (unpackMessage (ft n ! i0)))
∧ isReceiverOf p (ft n ! i0)))
∨ (∃ n .∀ n1 > n . ∀ m ∈ (set (drop (length (ft n)) (ft n1))) .
¬ isReceiverOf p m)" by blast
thus "∃n. (∀n1>n. (∀ m ∈ (set (drop (length (ft n)) (ft n1))).
(¬ (isReceiverOf p m))))"
proof(elim disjE, auto)
fix n i0 b
assume DecidingPoint:
"i0 < length (ft n)"
"isReceiverOf p (ft n ! i0)"
"<⊥, outM b> ∈# sends p (states (fe n ! i0) p) (unpackMessage (ft n ! i0))"
have "i0 < length (fe n) - 1"
using DecidingPoint(1)
by (metis (no_types) FE(3) execution.length)
hence StepN0: "((fe n) ! i0) ⊢ ((ft n) ! i0) ↦ ((fe n) ! (i0 + 1))"
using FE by (metis execution.step)
hence "msgs ((fe n) ! (i0 + 1)) <⊥, outM b>
= (msgs ((fe n) ! i0) <⊥, outM b>) +
(sends p (states ((fe n) ! i0) p)
(unpackMessage ((ft n) ! i0)) <⊥, outM b>)"
using DecidingPoint(2) OutOnlyGrowing[of "(fe n) ! i0" "(ft n) ! i0"
"(fe n) ! (i0 + 1)" "p"]
by auto
hence "(sends p (states ((fe n) ! i0) p)
(unpackMessage ((ft n) ! i0)) <⊥, outM b>)
≤ msgs ((fe n) ! (i0 + 1)) <⊥, outM b>"
using asynchronousSystem.steps_def by auto
hence OutMsgEx: "0 < msgs ((fe n) ! (i0 + 1)) <⊥, outM b>"
using asynchronousSystem.steps_def DecidingPoint(3) by auto
have "(i0 + 1) < length (fe n)"
using DecidingPoint(1) ‹i0 < length (fe n) - 1› by auto
hence "initReachable ((fe n) ! (i0 + 1))"
using AllExecsFromInit Cfg(1)
by (metis asynchronousSystem.initReachable_def)
hence Decided: "vDecided b ((fe n) ! (i0 + 1))" using OutMsgEx
by auto
have "i0 + 1 < length (fe n)" using DecidingPoint(1)
by (metis ‹(((i0::nat) + (1::nat)) < (length (
(fe::(nat ⇒ ('p, 'v, 's) configuration list)) (n::nat))))›)
hence "¬ vDecided b ((fe n) ! (i0 + 1))" using NoDecided by auto
hence "False" using Decided by auto
thus "∃n. (∀n1>n. (∀ m ∈ (set (drop (length (ft n)) (ft n1))).
(¬ (isReceiverOf p m))))" by simp
qed
qed
hence "∃ (crashPoint::'p ⇒ nat) .
∀ p . ∃ n . crashPoint p = n ∧ (∀ n1 > n . ∀ m ∈ (set (drop
(length (ft n)) (ft n1))) . (¬ isReceiverOf p m))" by metis
then obtain crashPoint where CrashPoint:
"∀ p . (∀ n1 > (crashPoint p) . ∀ m ∈ (set (drop (length
(ft (crashPoint p))) (ft n1))) . (¬ isReceiverOf p m))"
by blast
define limitSet where "limitSet = {crashPoint p | p . p ∈ Proc}"
have "finite {p. p ∈ Proc}" using finiteProcs by simp
hence "finite limitSet" using limitSet_def finite_image_set[] by blast
hence "∃ limit . ∀ l ∈ limitSet . l < limit" using
finite_nat_set_iff_bounded by auto
hence "∃ limit . ∀ p . (crashPoint p) < limit" using limitSet_def by auto
then obtain limit where Limit: "∀ p . (crashPoint p) < limit" by blast
define lengthLimit where "lengthLimit = length (ft limit) - 1"
define lateMessage where "lateMessage = last (ft limit)"
hence "lateMessage = (ft limit) ! (length (ft limit) - 1)"
by (metis AllArePrefixesTrace Limit last_conv_nth less_nat_zero_code
list.size(3) PrefixListMonotonicity)
hence LateIsLast: "lateMessage = (ft limit) ! lengthLimit"
using lateMessage_def lengthLimit_def by auto
have "∃ p . isReceiverOf p lateMessage"
proof(rule ccontr)
assume "¬ (∃(p::'p). (isReceiverOf p lateMessage))"
hence IsOutMsg: "∃ v . lateMessage = <⊥, outM v>"
by (metis isReceiverOf.simps(1) isReceiverOf.simps(2) message.exhaust)
have "execution trans sends start (fe limit) (ft limit)" using FE
by auto
hence "length (fe limit) - 1 = length (ft limit)"
using execution.length by simp
hence "lengthLimit < length (fe limit) - 1"
using lengthLimit_def
by (metis (opaque_lifting, no_types) Length Limit One_nat_def Suc_eq_plus1
Suc_le_eq diff_less
diffs0_imp_equal gr_implies_not0 less_Suc0 neq0_conv)
hence "((fe limit) ! lengthLimit) ⊢ ((ft limit) ! lengthLimit)
↦ ((fe limit) ! (lengthLimit + 1))"
using FE by (metis execution.step)
hence "((fe limit) ! lengthLimit) ⊢ lateMessage ↦ ((fe limit) !
(lengthLimit + 1))"
using LateIsLast by auto
thus False using IsOutMsg steps_def by auto
qed
then obtain p where ReceiverOfLate: "isReceiverOf p lateMessage" by blast
have "∀ n1 > (crashPoint p) .
∀ m ∈ (set (drop (length (ft (crashPoint p))) (ft n1))) .
(¬ isReceiverOf p m)"
using CrashPoint
by simp
hence NoMsgAfterLimit: "∀ m ∈ (set (drop (length (ft (crashPoint p)))
(ft limit))) . (¬ isReceiverOf p m)"
using Limit
by auto
have "lateMessage ∈ set (drop (length(ft (crashPoint p))) (ft limit))"
proof-
have "crashPoint p < limit" using Limit by simp
hence "prefixList (ft (crashPoint p)) (ft limit)"
using AllArePrefixesTrace by auto
hence CrashShorterLimit: "length (ft (crashPoint p))
< length (ft limit)" using PrefixListMonotonicity by auto
hence "last (drop (length (ft (crashPoint p))) (ft limit))
= last (ft limit)" by (metis last_drop)
hence "lateMessage = last (drop (length (ft (crashPoint p)))
(ft limit))" using lateMessage_def by auto
thus "lateMessage ∈ set (drop (length(ft (crashPoint p))) (ft limit))"
by (metis CrashShorterLimit drop_eq_Nil last_in_set not_le)
qed
hence "¬ isReceiverOf p lateMessage" using NoMsgAfterLimit by auto
thus "False" using ReceiverOfLate by simp
qed
end
end