Theory Execution

section ‹Execution›

text ‹
  \file{Execution} introduces a locale for executions within asynchronous systems.
›

theory Execution
imports AsynchronousSystem ListUtilities
begin

subsection ‹Execution locale definition›

text ‹
  A (finite) execution within a system is a list of configurations \isb{exec}
  accompanied by a list of messages \isb{trace} such that the first configuration
  is initial and every next state can be reached processing the messages
  in \isb{trace}.
›
locale execution =
  asynchronousSystem trans sends start    
for
  trans :: "'p ⇒ 's ⇒ 'v messageValue ⇒ 's" and
  sends :: "'p ⇒ 's ⇒ 'v messageValue ⇒ ('p, 'v) message multiset" and
  start :: "'p ⇒ 's"
+
fixes
  exec :: "('p, 'v, 's ) configuration list" and
  trace :: "('p, 'v) message list"
assumes 
  notEmpty: "length exec ≥ 1" and 
  length: "length exec - 1 = length trace" and
  base: "initial (hd exec)" and
  step: "⟦ i < length exec - 1 ; cfg1 = exec ! i ; cfg2 = exec ! (i + 1) ⟧
      ⟹ ((cfg1 ⊢ trace ! i ↦ cfg2)) "
begin

abbreviation execMsg ::
  "nat ⇒ ('p,'v) message"
where
  "execMsg n ≡ (trace ! n)"

abbreviation execConf ::
  "nat ⇒ ('p, 'v, 's) configuration"
where
  "execConf n  ≡ (exec ! n)"

subsection ‹Enabledness and occurrence in the execution›

definition minimalEnabled ::
  "('p, 'v) message ⇒ bool"
where
  "minimalEnabled msg ≡ (∃ p . isReceiverOf p msg) 
    ∧ (enabled (last exec) msg)
    ∧ (∃ n . n < length exec ∧ enabled (execConf n) msg 
      ∧ (∀ n' ≥ n . n' < length trace ⟶ msg ≠ (execMsg n'))
    ∧ (∀ n' msg' . ((∃ p . isReceiverOf p msg') 
      ∧ (enabled (last exec) msg') 
      ∧ n' < length trace 
      ∧ enabled (execConf n') msg' 
      ∧ (∀ n'' ≥ n' . n'' < length trace ⟶ msg' ≠ 
                      (execMsg n''))) ⟶ n' ≥ n))"

definition firstOccurrence ::
  "('p, 'v) message ⇒ nat ⇒ bool"
where                    
  "firstOccurrence msg n ≡ (∃ p . isReceiverOf p msg) 
    ∧ (enabled (last exec) msg) ∧ n < (length exec)
    ∧ enabled (execConf n) msg 
    ∧ (∀ n' ≥ n . n' < length trace ⟶ msg ≠ (execMsg n'))
    ∧ ( n ≠ 0 ⟶ (¬ enabled (execConf (n - 1)) msg 
      ∨ msg = execMsg (n - 1)))"

lemma FirstOccurrenceExists:
assumes
  "enabled (last exec) msg"
  "∃p. isReceiverOf p msg"
shows
  "∃ n . firstOccurrence msg n"
proof-
  have "length exec - 1 < length exec 
    ∧ (∀ n' ≥ (length exec - 1) . n' < length trace ⟶ trace ! n' ≠ msg)"
    using length
    by (metis diff_diff_cancel leD notEmpty zero_less_diff 
      zero_less_one)
  hence NNotInTrace: "∃ n < length exec . 
    (∀ n'≥n . n' < length trace ⟶ trace ! n' ≠ msg)" by blast
  hence "∃ n0 < length exec . 
    (∀ n'≥n0 . n' < length trace ⟶ trace ! n' ≠ msg) ∧
    ((n0 = 0) 
      ∨ ¬ (∀ n' ≥ (n0 - 1) . n' < length trace ⟶ trace ! n' ≠ msg))" 
    using MinPredicate2[of "λx.(x < length exec 
      ∧ (∀n'≥x.(n'<length trace ⟶ trace ! n' ≠ msg)))"]
    by auto
  hence "∃ n0. n0 < length exec 
    ∧ (∀ n'≥n0 . n' < length trace ⟶ trace ! n' ≠ msg) 
    ∧ ((n0 = 0) 
      ∨ ¬ (∀ n' ≥ (n0 - 1) . n' < length trace ⟶ trace ! n' ≠ msg))" 
    by simp
  from this obtain n0 where N0a: "n0 < length exec 
    ∧ (∀ n'≥n0 . n' < length trace ⟶ trace ! n' ≠ msg) 
    ∧ ((n0 = 0) 
      ∨ ¬ (∀ n' ≥ (n0 - 1) . n' < length trace ⟶ trace ! n' ≠ msg))" 
    by metis
  hence N0: "n0 < length exec" 
    "(∀ n'≥n0 . n' < length trace ⟶ trace ! n' ≠ msg)"
    "((n0 = 0) 
      ∨ ¬ (∀ n' ≥ (n0 - 1) . n' < length trace ⟶ trace ! n' ≠ msg))" 
    using N0a by auto
  have N0': "n0 = 0 ∨ trace ! (n0 - 1) = msg"
  proof(cases "n0 = 0", auto)
    assume N0NotZero: "n0 > 0"
    hence "¬ (∀ n' ≥ (n0 - 1) . n' < length trace ⟶ trace ! n' ≠ msg)" 
      using N0(3) by blast
    moreover have "n0 - 1 < length trace"
      using N0(1) length N0NotZero 
      by (metis calculation le_less_trans)
    ultimately show "execMsg (n0 - Suc 0) = msg" using N0(2) 
      by (metis One_nat_def Suc_diff_Suc diff_Suc_eq_diff_pred 
         diff_diff_cancel diff_is_0_eq leI nat_le_linear)
  qed
  have "∃ n1 < length exec . 
    (∀ n'≥n1 . n' < length trace ⟶ trace ! n' ≠ msg) 
    ∧ enabled (exec ! n1) msg 
    ∧ (n1 = 0 ∨ ¬ enabled (exec ! (n1 - 1)) msg ∨ trace ! (n1 - 1) = msg)"
  proof(cases "enabled (exec ! n0) msg")
    assume "enabled (execConf n0) msg"
    hence "n0 < length exec" 
      "(∀ n'≥n0 . n' < length trace ⟶ trace ! n' ≠ msg)" 
      "enabled (exec ! n0) msg ∧
      (n0 = 0 ∨ ¬ enabled (exec ! (n0 - 1)) msg ∨ trace ! (n0 - 1) = msg)"
    using N0 N0' by auto
    thus "∃n1<length exec.
       (∀n'≥n1. n' < length trace ⟶ execMsg n' ≠ msg) 
       ∧ enabled (execConf n1) msg 
       ∧ (n1 = 0 ∨ ¬ enabled (execConf (n1 - 1)) msg 
         ∨ execMsg (n1 - 1) = msg)"
      by metis
  next
    assume NotEnabled: "¬ enabled (execConf n0) msg"
    have "last exec = exec ! (length exec - 1)" using last_conv_nth notEmpty 
      by (metis NNotInTrace length_0_conv less_nat_zero_code)
    hence EnabledInLast: "enabled (exec ! (length exec - 1)) msg" 
      using assms(1) by simp
    hence "n0 ≠ length exec - 1" using NotEnabled by auto
    hence N0Small: "n0 < length exec - 1" using N0(1) by simp
    hence "∃ k < length exec - 1 - n0  . ¬ enabled (execConf (n0 + k)) msg 
      ∧ enabled (execConf (n0 + k + 1)) msg"
      using NatPredicateTippingPoint[of "length exec - 1 - n0" 
        "λx.¬(enabled (exec ! (n0 + x)) msg)"]
        assms(1) NotEnabled EnabledInLast by simp
    then obtain k where K: " k < length exec - 1 - n0" 
      "¬ enabled (execConf (n0 + k)) msg" 
      "enabled (execConf (n0 + k + 1)) msg" by blast
    define n1 where "n1 = k + n0 + 1"
    hence N1: "n1 ≥ n0" "¬ enabled (execConf (n1 - 1)) msg" 
      "enabled (execConf n1) msg" "n1 < length exec"
      unfolding n1_def using K
      by (auto simp add: add.commute)
    have "∀n'≥n1. n' < length trace ⟶ execMsg n' ≠ msg" 
      using N1(1) N0(2) by (metis order_trans)
    thus "∃n1<length exec.
        (∀n'≥n1. n' < length trace ⟶ execMsg n' ≠ msg) 
        ∧ enabled (execConf n1) msg 
        ∧ (n1 = 0 ∨ ¬ enabled (execConf (n1 - 1)) msg 
          ∨ execMsg (n1 - 1) = msg)" 
    using N1 by auto
  qed
  then obtain n1 where N1: "n1 < length exec" 
    "∀ n'≥n1 . n' < length trace ⟶ trace ! n' ≠ msg"
    "enabled (exec ! n1) msg"
    "n1 = 0 ∨ ¬ enabled (exec ! (n1 - 1)) msg ∨ trace ! (n1 - 1) = msg" 
    by metis
  hence "firstOccurrence msg n1" using assms unfolding firstOccurrence_def 
    by auto
  thus "∃n. firstOccurrence msg n" by blast
qed

lemma ReachableInExecution:
assumes
  "i < length exec"
  "j ≤ i"
shows
  "reachable (execConf j) (execConf i)"
using assms proof(induct i, auto)
  show "reachable (execConf 0) (execConf 0)" 
    using reachable.simps by blast
next
  fix ia
  assume 
    IH: "(j ≤ ia ⟹ reachable (execConf j) (execConf ia))" 
    "Suc ia < length exec" 
    "j ≤ Suc ia"  
    "i < length exec" 
    "j ≤ i"
  show "reachable (execConf j) (execConf (Suc ia))" 
  proof(cases "j = Suc ia", auto)
    show "reachable (execConf (Suc ia)) (execConf (Suc ia))" 
      using reachable.simps by metis
  next
    assume "j ≠ Suc ia"
    hence "j ≤ ia" using IH(3) by simp
    hence "reachable (execConf j) (execConf ia)" using IH(1) by simp
    moreover have "reachable (execConf ia) (execConf (Suc ia))" 
      using reachable.simps
      by (metis IH(2) Suc_eq_plus1 less_diff_conv local.step)
    ultimately show "reachable (execConf j) (execConf (Suc ia))" 
      using ReachableTrans by blast
  qed
qed

lemma LastPoint:
fixes
  msg::"('p, 'v) message"
assumes
  "enabled (last exec) msg"
obtains n where
  "n < length exec"
  "enabled (execConf n) msg"
  "∀ n' ≥ n .
    n' < length trace ⟶ msg ≠ (execMsg n')"
  "∀ n0 . 
      n0 < length exec 
    ∧ enabled (execConf n0) msg 
    ∧ (∀ n' ≥ n0 .
        n' < length trace ⟶ msg ≠ (execMsg n'))
    ⟶ n0 ≥ n"
proof (cases ?thesis, simp)
  case False
  define len where "len = length exec - 1"
  have
    "len < length exec"
    "enabled (execConf len) msg" 
    "∀ n' ≥ len . n' < length trace ⟶ msg ≠ (execMsg n')"
    using assms notEmpty length unfolding len_def
    by (auto, metis One_nat_def last_conv_nth list.size(3) not_one_le_zero)
  hence "∃ n . n < length exec ∧ enabled (execConf n) msg 
    ∧ (∀ n' ≥ n . n' < length trace ⟶ msg ≠ (execMsg n'))"
    by blast
  from MinPredicate[OF this] 
    show ?thesis using that False by blast
qed

lemma ExistImpliesMinEnabled:
fixes 
  msg :: "('p, 'v) message" and
  p :: 'p
assumes 
  "isReceiverOf p msg" 
  "enabled (last exec) msg"
shows
  "∃ msg' . minimalEnabled msg'"
proof-
  have MsgHasMinTime:"∀ msg . (enabled (last exec) msg 
    ∧ (∃ p . isReceiverOf p msg))
    ⟶ (∃ n .  n < length exec ∧ enabled (execConf n) msg 
        ∧ (∀ n' ≥ n . n' < length trace ⟶ msg ≠ (execMsg n'))
        ∧ (∀ n0 .  n0 < length exec ∧ enabled (execConf n0) msg 
        ∧ (∀ n' ≥ n0 . n' < length trace ⟶ msg ≠ (execMsg n')) 
        ⟶ n0 ≥ n))" by (clarify, rule LastPoint, auto)
  let ?enabledTimes = "{n::nat . ∃ msg . (enabled (last exec) msg 
    ∧ (∃ p . isReceiverOf p msg))
    ∧  n < length exec ∧ (enabled (execConf n) msg 
    ∧ (∀ n' ≥ n . n' < length trace ⟶ msg ≠ (execMsg n')))}"
  have NotEmpty:"?enabledTimes ≠ {}" using assms MsgHasMinTime by blast
  hence "∃ n0 . n0 ∈ ?enabledTimes" by blast
  hence "∃ nMin ∈ ?enabledTimes . ∀ x ∈ ?enabledTimes . x ≥ nMin" 
    using MinPredicate[of "λn.(n ∈ ?enabledTimes)"] by simp
  then obtain nMin where NMin: "nMin ∈ ?enabledTimes" 
    "∀ x ∈ ?enabledTimes . x ≥ nMin" by blast
  hence "∃ msg . (enabled (last exec) msg ∧ (∃ p . isReceiverOf p msg))
    ∧  nMin < length exec ∧ (enabled (execConf nMin) msg 
    ∧ (∀ n' ≥ nMin . n' < length trace ⟶ msg ≠ (execMsg n'))
    ∧ (∀ n0 .  n0 < length exec ∧ enabled (execConf n0) msg 
      ∧ (∀ n' ≥ n0 . n' < length trace ⟶ msg ≠ (execMsg n')) 
      ⟶ n0 ≥ nMin))" by blast
  then obtain msg where "(enabled (last exec) msg 
    ∧ (∃ p . isReceiverOf p msg))
    ∧ nMin < length exec ∧(enabled (execConf nMin) msg 
    ∧ (∀ n' ≥ nMin . n' < length trace ⟶ msg ≠ (execMsg n'))
    ∧ (∀ n0 .  n0 < length exec ∧ enabled (execConf n0) msg 
      ∧ (∀ n' ≥ n0 . n' < length trace ⟶ msg ≠ (execMsg n')) 
      ⟶ n0 ≥ nMin))" by blast
  moreover have "(∀ n' msg' . ((∃ p . isReceiverOf p msg') 
    ∧ (enabled (last exec) msg') 
    ∧ n' < length trace ∧ enabled (execConf n') msg' 
    ∧ (∀ n'' ≥ n' . n'' < length trace ⟶ msg' ≠ (execMsg n''))) 
      ⟶ n' ≥ nMin)"
  proof(clarify)
    fix n' msg' p
    assume Assms:
      "isReceiverOf p msg'" 
      "enabled (last exec) msg'" 
      "n' < length trace" 
      "enabled (execConf n') msg'" 
      "∀n'' ≥ n'. (n'' < length trace) ⟶ (msg' ≠ execMsg n'')"
    from Assms(3) have "n' < length exec" using length by simp
    with Assms have "n' ∈ ?enabledTimes" by auto
    thus "nMin ≤ n'" using NMin(2) by simp
  qed
  ultimately have "minimalEnabled msg"
    using minimalEnabled_def by blast
  thus ?thesis by blast
qed

lemma StaysEnabledStep:
assumes
  En: "enabled cfg msg" and
  Cfg: "cfg = exec ! n" and
  N: "n < length exec" 
shows
  "enabled (exec ! (n + 1)) msg 
  ∨ n = (length exec - 1) 
  ∨ msg = trace ! n"
proof(cases "n = length exec - 1")
  case True
  thus ?thesis by simp
next
  case False
  with N have N: "n < length exec - 1" by simp
  with Cfg have Step:  "cfg ⊢ trace ! n ↦ (exec ! (n + 1))" 
    using step by simp
  thus ?thesis proof(cases "enabled (exec ! (n + 1)) msg")
    case True
    thus ?thesis by simp
  next
    case False
    hence "¬ enabled (exec ! (n + 1)) msg" by simp
    thus ?thesis using En enabled_def Step N OnlyOccurenceDisables by blast
  qed
qed                          

lemma StaysEnabledHelp:
assumes
  "enabled cfg msg" and
  "cfg = exec ! n" and
  "n < length exec"    
shows 
  "∀ i . i ≥ n ∧ i < (length exec - 1) ∧ enabled (exec ! i) msg 
  ⟶ msg = (trace ! i) ∨ (enabled (exec ! (i+1)) msg)"
proof(clarify)
  fix i
  assume "n ≤ i" "i < length exec - 1"
    "enabled (execConf i) msg" "¬ enabled (execConf (i + 1)) msg"
  thus "msg = (trace ! i)"
    using assms StaysEnabledStep
    by (metis add.right_neutral add_strict_mono le_add_diff_inverse2
        nat_neq_iff notEmpty  zero_less_one)
qed

lemma StaysEnabled:
assumes En: "enabled cfg msg" and
  "cfg = exec ! n" and
  "n < length exec"   
shows "enabled (last exec) msg ∨ (∃ i . i ≥ n ∧ i < (length exec - 1) 
  ∧ msg = trace ! i )"
proof(cases "enabled (last exec) msg")
  case True
  thus ?thesis by simp
next
  case False 
  hence NotEnabled: "¬ enabled (last exec) msg" by simp
  have "last exec = exec ! (length exec - 1)" 
    by (metis last_conv_nth list.size(3) notEmpty not_one_le_zero)
  hence "∃ l . l ≥ n ∧ last exec = exec ! l ∧ l = length exec - 1" 
    using assms(3) by auto
  then obtain l where L: "l ≥ n" "last exec = exec ! l" 
    "l = length exec - 1" by blast
  have "(∃ i . i ≥ n ∧ i < (length exec - 1) ∧ msg = trace ! i )"  
  proof (rule ccontr)
    assume Ass: " ¬ (∃i≥n. i < length exec - 1 ∧ msg = execMsg i)" 
    hence Not: "∀ i. i < n ∨ i ≥ length exec - 1 ∨ msg ≠ execMsg i" 
      by (metis leI)
    have "∀ i. i ≥ n ∧ i ≤ length exec - 1 ⟶ enabled (exec ! i) msg" 
    proof(clarify)
      fix i 
      assume I: "n ≤ i" "i ≤ length exec - 1"  
      thus "enabled (execConf i) msg"
        using StaysEnabledHelp[OF assms] assms(1,2) Ass 
        by (induct i, auto, metis Suc_le_lessD le_Suc_eq)
    qed
    with NotEnabled L show False by simp
  qed
  thus ?thesis by simp
qed

end ― ‹end of locale Execution›

subsection ‹Expanding executions to longer executions›

lemma (in asynchronousSystem) expandExecutionStep:
fixes 
  cfg :: "('p, 'v, 's ) configuration"
assumes
  CfgIsReachable: "(last exec') ⊢ msg ↦ cMsg" and
  ExecIsExecution: "execution trans sends start exec' trace'" 
shows
  "∃ exec'' trace''. (execution trans sends start exec'' trace'') 
  ∧ (prefixList exec' exec'') 
  ∧ (prefixList trace' trace'') 
  ∧ (last exec'') = cMsg 
  ∧ (last trace'' = msg)"
proof -
  define execMsg where "execMsg = exec' @ [cMsg]"
  define traceMsg where "traceMsg = trace' @ [msg]"
  have ExecMsgEq: "∀ i < ((length execMsg) - 1) . execMsg ! i = exec'!i " 
    using execMsg_def by (auto simp add: nth_append)
  have TraceMsgEq: "∀ i < ((length traceMsg) - 1) . traceMsg!i = trace'!i" 
    using traceMsg_def 
    by (auto simp add: nth_append)
  have ExecLen: "(length execMsg) ≥ 1" using execMsg_def by auto
  have lessLessExec: "∀ i . i < (length exec') ⟶ i < (length execMsg )" 
    unfolding execMsg_def by auto
  have ExecLenTraceLen: "length exec'- 1 = length trace'" 
    using ExecIsExecution execution.length by auto
  have lessLessTrace: "∀ i . i < (length exec' - 1) ⟶ i < (length trace')" 
    using ExecLenTraceLen by auto
  have Exec'Len: "length exec' ≥ 1" 
    using ExecIsExecution execution.notEmpty by blast
  hence "hd exec' = hd execMsg " using execMsg_def
    by (metis One_nat_def hd_append2 length_0_conv not_one_le_zero)
  moreover have "initial (hd exec')" 
    using ExecIsExecution execution.base by blast 
  ultimately have ExecInit: "initial (hd execMsg)" using execMsg_def by auto
  have ExecMsgLen: "length execMsg - 1 = length traceMsg" 
    using ExecLenTraceLen unfolding execMsg_def traceMsg_def
    by (auto,metis Exec'Len Suc_pred length_greater_0_conv list.size(3) 
       not_one_le_zero) 
  have ExecSteps:"∀ i < length exec' - 1 .
    ((exec' ! i)  ⊢ trace' ! i ↦ (exec' ! (i + 1)))" 
    using ExecIsExecution execution.step by blast
  have "∀ i < length execMsg - 1. 
    ((execMsg ! i) ⊢ traceMsg ! i ↦ (execMsg ! (i + 1)))" 
    unfolding execMsg_def traceMsg_def
  proof auto
    fix i
    assume IlessLen:"i < (length exec')"
    show "((exec' @ [cMsg]) ! i) ⊢ ((trace' @ [msg]) ! i) 
      ↦ ((exec' @ [cMsg]) ! (Suc i))" 
    proof (cases "(i < (length exec') - 1)")
    case True
      hence IlessLen1: "(i < (length exec') - 1)" by auto
      hence "((exec' ! i)  ⊢ trace' ! i ↦ (exec' ! (i + 1)))" 
        using ExecSteps by auto
      with IlessLen1 ExecMsgEq lessLessExec execMsg_def 
      have "((exec' @ [cMsg]) ! i) ⊢ ((trace') ! i) 
        ↦ ((exec' @ [cMsg]) ! (Suc i))" by auto
      thus "((exec' @ [cMsg]) ! i) ⊢ ((trace' @ [msg]) ! i) 
        ↦ ((exec' @ [cMsg]) ! (Suc i))" 
        using IlessLen1 TraceMsgEq lessLessTrace traceMsg_def by auto
    next
    case False
      with IlessLen have IEqLen1: "(i = (length exec') - 1)" by auto
      thus "((exec' @ [cMsg]) ! i) ⊢ ((trace' @ [msg]) ! i) 
        ↦ ((exec' @ [cMsg]) ! (Suc i))" 
        using  execMsg_def traceMsg_def  CfgIsReachable Exec'Len 
               ExecLenTraceLen ExecMsgEq ExecMsgLen IlessLen   
        by (metis One_nat_def Suc_eq_plus1 Suc_eq_plus1_left last_conv_nth 
           le_add_diff_inverse length_append less_nat_zero_code list.size(3) 
           list.size(4) nth_append_length)
    qed
  qed
  hence isExecution: "execution trans sends start execMsg traceMsg" 
    using ExecLen ExecMsgLen ExecInit  
    by (unfold_locales ,auto) 
  moreover have "prefixList exec' execMsg" unfolding execMsg_def 
    by (metis TailIsPrefixList not_Cons_self2)
  moreover have "prefixList trace' traceMsg" unfolding traceMsg_def 
    by (metis TailIsPrefixList not_Cons_self2)
  ultimately show ?thesis using execMsg_def traceMsg_def by (metis last_snoc)
qed

lemma (in asynchronousSystem) expandExecutionReachable:
fixes 
  cfg :: "('p, 'v, 's ) configuration" and
  cfgLast :: "('p, 'v, 's ) configuration"
assumes
  CfgIsReachable: "reachable (cfgLast) cfg" and
  ExecIsExecution: "execution trans sends start exec trace"  and
  ExecLast: "cfgLast = last exec" 
shows
  "∃ exec' trace'. (execution trans sends start exec' trace') 
  ∧ ((prefixList exec exec' 
    ∧ prefixList trace trace') 
    ∨ (exec = exec' ∧ trace = trace')) 
  ∧ (last exec') = cfg"
using CfgIsReachable  ExecIsExecution ExecLast 
proof (induct cfgLast cfg rule: reachable.induct, auto)
  fix msg cfg3 exec' trace'
  assume "(last exec') ⊢ msg ↦ cfg3"
         "execution trans sends start exec' trace'"
  hence "∃ exec'' trace''. (execution trans sends start exec'' trace'') 
    ∧ (prefixList exec' exec'') 
    ∧ (prefixList trace' trace'') ∧ (last exec'') = cfg3 
    ∧ (last trace'') = msg" by (simp add: expandExecutionStep)
  then obtain  exec'' trace'' where 
    NewExec: "execution trans sends start exec'' trace''" 
             "prefixList exec' exec''" "prefixList trace' trace''" 
             "last exec'' = cfg3" by blast
  assume prefixLists: "prefixList exec exec'" 
                      "prefixList trace trace'" 
  from prefixLists(1) NewExec(2) have "prefixList exec exec''" 
    using PrefixListTransitive by auto
  moreover from prefixLists(2) NewExec(3) have 
    "prefixList trace trace''"  using PrefixListTransitive by auto
  ultimately show "∃ exec'' trace'' .
          execution trans sends start exec'' trace'' ∧
          ((prefixList exec exec'' ∧ prefixList trace trace'') 
          ∨ (exec = exec'' ∧ trace = trace'')) ∧
          last exec'' = cfg3" using NewExec(1) NewExec(4) by blast
next
  fix msg cfg3
  assume "(last exec) ⊢ msg ↦ cfg3" "execution trans sends start exec trace"
  then show
    "∃exec' trace'. execution trans sends start exec' trace' ∧
       (prefixList exec exec' ∧ prefixList trace trace' 
        ∨ exec = exec' ∧ trace = trace') ∧ last exec' = cfg3" 
    using expandExecutionStep by blast
qed

lemma (in asynchronousSystem) expandExecution:
fixes 
  cfg :: "('p, 'v, 's ) configuration" and
  cfgLast :: "('p, 'v, 's ) configuration"
assumes
  CfgIsReachable: "stepReachable (last exec) msg cfg" and
  ExecIsExecution: "execution trans sends start exec trace"
shows
  "∃ exec' trace'. (execution trans sends start exec' trace') 
  ∧ (prefixList exec exec') 
  ∧ (prefixList trace trace') ∧ (last exec') = cfg 
  ∧ (msg ∈ set (drop (length trace) trace'))"  
proof -
  from CfgIsReachable obtain c' c'' where 
    Step: "reachable (last exec) c'" "c' ⊢ msg ↦ c''" "reachable c'' cfg" 
    by (auto simp add: stepReachable_def)
  from Step(1) ExecIsExecution have "∃ exec' trace' .
    execution trans sends start exec' trace' ∧
    ((prefixList exec exec' ∧ prefixList trace trace') 
    ∨ (exec = exec' ∧ trace = trace')) ∧
    last exec' = c'" by (auto simp add: expandExecutionReachable)
  then obtain  exec' trace' where Exec': 
    "execution trans sends start exec' trace'"
    "(prefixList exec exec' ∧ prefixList trace trace') 
      ∨ (exec = exec' ∧ trace = trace')"
    "last exec' = c'" by blast
  from Exec'(1) Exec'(3) Step(2) have "∃ exec'' trace'' . 
    execution trans sends start exec'' trace'' ∧
    prefixList exec' exec'' ∧ prefixList trace' trace'' 
    ∧ last exec'' = c'' ∧ last trace'' = msg" 
    by (auto simp add: expandExecutionStep)
  then obtain exec'' trace'' where Exec'': 
    "execution trans sends start exec'' trace''"
    "prefixList exec' exec''" "prefixList trace' trace''" 
    "last exec'' = c''" "last trace'' = msg" by blast
  have PrefixLists: "prefixList exec exec'' ∧ prefixList trace trace''"  
  proof(cases "exec = exec' ∧ trace = trace'")
  case True
    with Exec'' show "prefixList exec exec'' ∧ prefixList trace trace''" 
    by auto
  next
  case False
    with Exec'(2) have Prefix: "prefixList exec exec'" 
      "prefixList trace trace'" by auto
    from Prefix(1) Exec''(2) have "prefixList exec exec''" 
      using PrefixListTransitive by auto
    with Prefix(2) Exec''(3) show  "prefixList exec exec'' 
      ∧ prefixList trace trace''" 
      using PrefixListTransitive by auto
  qed
  with Exec''(5) have MsgInTrace'': "msg ∈ set (drop (length trace) trace'')" 
    by (metis PrefixListMonotonicity drop_eq_Nil last_drop 
      last_in_set not_le)
  from Step(3) Exec''(1) Exec''(4) have "∃ exec''' trace''' .
    execution trans sends start exec''' trace''' ∧
    ((prefixList exec'' exec''' ∧ prefixList trace'' trace''') 
    ∨ (exec'' = exec''' ∧ trace'' = trace''')) ∧
    last exec''' = cfg" 
    by (auto simp add: expandExecutionReachable)
  then obtain exec''' trace''' where Exec''': 
    "execution trans sends start exec''' trace'''"
    "(prefixList exec'' exec''' ∧ prefixList trace'' trace''') 
    ∨ (exec'' = exec''' ∧ trace'' = trace''')"
    "last exec''' = cfg" by blast
  have "prefixList exec exec''' ∧ prefixList trace trace''' 
    ∧ msg ∈ set (drop (length trace) trace''')"  
  proof(cases "exec'' = exec''' ∧ trace'' = trace'''")
  case True
    with PrefixLists MsgInTrace'' 
    show "prefixList exec exec''' ∧ prefixList trace trace''' 
    ∧ msg ∈ set (drop (length trace) trace''')" by auto
  next
  case False
    with Exec'''(2) have Prefix: "prefixList exec'' exec'''" 
      "prefixList trace'' trace'''" by auto
    from Prefix(1) PrefixLists have "prefixList exec exec'''" 
      using PrefixListTransitive by auto
    with Prefix(2) PrefixLists have "prefixList exec exec''' 
      ∧ prefixList trace trace'''"  
      using PrefixListTransitive by auto
    moreover have "msg ∈ set (drop (length trace) trace''')" 
      using Prefix(2) PrefixLists MsgInTrace'' 
      by (metis (opaque_lifting, no_types) PrefixListHasTail append_eq_conv_conj 
         drop_take rev_subsetD set_take_subset)
    ultimately show ?thesis by auto
  qed
  with Exec'''(1) Exec'''(3) show ?thesis by blast
qed

subsection ‹Infinite and fair executions›

text ‹
  Völzer does not give much attention to the definition of the
  infinite executions. We derive them from finite executions by considering
  infinite executions to be infinite sequence of finite executions increasing
  monotonically w.r.t. the list prefix relation.
›

definition (in asynchronousSystem) infiniteExecution ::
  "(nat ⇒ (('p, 'v, 's) configuration list)) 
  ⇒ (nat ⇒ (('p, 'v) message list)) ⇒ bool"
where
  "infiniteExecution fe ft ≡
    ∀ n . execution trans sends start (fe n) (ft n) ∧ 
      prefixList (fe n) (fe (n+1)) ∧
      prefixList (ft n) (ft (n+1))"

definition (in asynchronousSystem) correctInfinite ::
  "(nat ⇒ (('p, 'v, 's) configuration list)) 
  ⇒ (nat ⇒ (('p, 'v) message list)) ⇒ 'p ⇒ bool"
where 
  "correctInfinite fe ft p ≡ 
    infiniteExecution fe ft
    ∧ (∀ n . ∀ n0 < length (fe n). ∀ msg .(enabled ((fe n) ! n0) msg) 
    ∧ isReceiverOf p msg 
    ⟶ (∃ msg' . ∃ n' ≥ n . ∃ n0' ≥ n0 .isReceiverOf p msg' 
    ∧ n0' < length (fe n') ∧ (msg' = ((ft n') ! n0'))))"

definition (in asynchronousSystem) fairInfiniteExecution ::
  "(nat ⇒ (('p, 'v, 's) configuration list)) 
  ⇒ (nat ⇒ (('p, 'v) message list)) ⇒ bool"
where
  "fairInfiniteExecution fe ft ≡
    infiniteExecution fe ft
    ∧ (∀ n . ∀ n0 < length (fe n). ∀ p . ∀ msg . 
      ((enabled ((fe n) ! n0) msg) 
        ∧ isReceiverOf p msg ∧ correctInfinite fe ft p ) 
      ⟶ (∃ n' ≥ n . ∃ n0' ≥ n0 . n0' < length (ft n') 
        ∧ (msg = ((ft n') ! n0'))))"

end