Theory GenClock

(*  Title:       Formalization of Schneider's generalized clock synchronization protocol.
    Author:      Alwen Tiu, LORIA, June 11, 2005
    Maintainer:  Alwen Tiu <Alwen.Tiu at loria.fr>
*)

theory GenClock imports Complex_Main begin

subsection‹Types and constants definitions›

text‹Process is represented by natural numbers. The type 'event' corresponds
to synchronization rounds.›

type_synonym process = nat
type_synonym event = nat      (* synchronization rounds *)
type_synonym time = real
type_synonym Clocktime = real

axiomatization
  δ :: real and
  μ :: real and
  ρ :: real and
  rmin :: real and
  rmax :: real and
  β :: real and
  Λ :: real and
  (* Number of processes *)
  np :: process and
  maxfaults :: process and
  (* Physical clocks *)
  PC :: "[process, time] ⇒ Clocktime" and
  (* Virtual / Logical clocks *)
  VC :: "[process, time] ⇒ Clocktime" and
  (* Starting (real) time of synchronization rounds *)
  te :: "[process, event] ⇒ time" and
  (* Clock readings at each round *)
  θ :: "[process, event] ⇒ (process ⇒ Clocktime)" and
  (* Logical clock in-effect at a time interval *)
  IC :: "[process, event, time] ⇒ Clocktime" and
  (* Correct clocks *)
  correct :: "[process, time] ⇒ bool" and
  (* The averaging function to calculate clock adjustment *)
  cfn :: "[process, (process ⇒ Clocktime)] ⇒ Clocktime" and

  π :: "[Clocktime, Clocktime] ⇒ Clocktime" and

  α :: "Clocktime ⇒ Clocktime"

definition
  count :: "[process ⇒ bool, process] ⇒ nat" where
  "count f n = card {p. p < n ∧ f p}"

definition
  (* Adjustment to a clock *)
  Adj :: "[process, event] ⇒ Clocktime" where
  "Adj = (λ p i. if 0 < i then cfn p (θ p i) - PC p (te p i)
                 else 0)"

definition
  (* Auxilary predicates used in the definition of precision enhancement *)
  okRead1 :: "[process ⇒ Clocktime, Clocktime, process ⇒ bool] ⇒ bool" where
  "okRead1 f x ppred ⟷ (∀ l m. ppred l ∧ ppred m ⟶ ¦f l - f m¦ ≤ x)"

definition
  okRead2 :: "[process ⇒ Clocktime, process ⇒ Clocktime, Clocktime,
               process ⇒ bool] ⇒ bool" where
  "okRead2 f g x ppred ⟷ (∀ p. ppred p ⟶ ¦f p - g p¦ ≤ x)"

definition
  rho_bound1 :: "[[process, time] ⇒ Clocktime] ⇒ bool" where
  "rho_bound1 C ⟷ (∀ p s t. correct p t ∧ s ≤ t ⟶ C p t - C p s ≤ (t - s)*(1 + ρ))"
definition
  rho_bound2 :: "[[process, time] ⇒ Clocktime] ⇒ bool" where
  "rho_bound2 C ⟷ (∀ p s t. correct p t ∧ s ≤ t ⟶ (t - s)*(1 - ρ) ≤ C p t - C p s)"

subsection‹Clock conditions›

text‹Some general assumptions›
axiomatization where
  constants_ax: "0 < β ∧ 0 < μ ∧ 0 < rmin
  ∧ rmin ≤ rmax ∧ 0 < ρ ∧ 0 < np ∧ maxfaults ≤ np"

axiomatization where
  PC_monotone: "∀ p s t. correct p t ∧ s ≤ t ⟶ PC p s ≤ PC p t"

axiomatization where
  VClock: "∀ p t i. correct p t ∧ te p i ≤ t ∧ t < te p (i + 1) ⟶ VC p t = IC p i t"

axiomatization where
  IClock: "∀ p t i. correct p t ⟶ IC p i t = PC p t + Adj p i"

text‹Condition 1: initial skew›
axiomatization where
  init: "∀ p. correct p 0 ⟶ 0 ≤ PC p 0 ∧ PC p 0 ≤ μ"

text‹Condition 2: bounded drift›
axiomatization where
  rate_1: "∀ p s t. correct p t ∧ s ≤ t ⟶ PC p t - PC p s ≤ (t - s)*(1 + ρ)" and
  rate_2: "∀ p s t. correct p t ∧ s ≤ t ⟶ (t - s)*(1 - ρ) ≤ PC p t - PC p s"

text‹Condition 3: bounded interval›
axiomatization where
  rts0: "∀ p t i. correct p t ∧ t ≤ te p (i+1) ⟶ t - te p i ≤ rmax" and
  rts1: "∀ p t i. correct p t ∧ te p (i+1) ≤ t ⟶ rmin ≤ t - te p i"

text‹Condition 4 : bounded delay›
axiomatization where
  rts2a: "∀ p q t i. correct p t ∧ correct q t ∧ te q i + β ≤ t ⟶ te p i ≤ t"  and
  rts2b: "∀ p q i. correct p (te p i) ∧ correct q (te q i) ⟶ abs(te p i - te q i) ≤ β"

text‹Condition 5: initial synchronization›
axiomatization where
  synch0: "∀ p. te p 0 = 0"

text‹Condition 6: nonoverlap›
axiomatization where
  nonoverlap: "β ≤ rmin"

text‹Condition 7: reading errors›
axiomatization where
  readerror: "∀ p q i. correct p (te p (i+1)) ∧ correct q (te p (i+1)) ⟶
              abs(θ p (i+1) q - IC q i (te p (i+1))) ≤ Λ"

text‹Condition 8: bounded faults›
axiomatization where
  correct_closed: "∀ p s t. s ≤ t ∧ correct p t ⟶ correct p s" and
  correct_count:  "∀ t. np - maxfaults ≤ count (λ p. correct p t) np"

text‹Condition 9: Translation invariance›
axiomatization where
  trans_inv: "∀ p f x. 0 ≤ x ⟶ cfn p (λ y. f y + x) = cfn p f + x"

text‹Condition 10: precision enhancement›
axiomatization where
  prec_enh:
  "∀ ppred p q f g x y.
          np - maxfaults ≤ count ppred np ∧
          okRead1 f y ppred ∧ okRead1 g y ppred ∧
          okRead2 f g x ppred ∧ ppred p ∧ ppred q
      ⟶ abs(cfn p f - cfn q g) ≤ π x y"

text‹Condition 11: accuracy preservation›
axiomatization where
  acc_prsv:
  "∀ ppred p q f x. okRead1 f x ppred ∧ np - maxfaults ≤ count ppred np
          ∧ ppred p ∧ ppred q ⟶ abs(cfn p f - f q) ≤ α x"


subsubsection‹Some derived properties of clocks›

lemma rts0d:
assumes cp: "correct p (te p (i+1))"
shows "te p (i+1) - te p i ≤ rmax"
using cp rts0 by simp

lemma rts1d:
assumes cp: "correct p (te p (i+1))"
shows "rmin ≤ te p (i+1) - te p i"
using cp rts1 by simp

lemma rte:
assumes cp: "correct p (te p (i+1))"
shows "te p i ≤ te p (i+1)"
proof-
  from cp rts1d have "rmin ≤ te p (i+1) - te p i"
    by simp
  from this constants_ax show ?thesis by arith
qed

lemma beta_bound1:
assumes corr_p: "correct p (te p (i+1))"
and corr_q: "correct q (te p (i+1))"
shows "0 ≤ te p (i+1) - te q i"
proof-
  from corr_p rte have "te p i ≤ te p (i+1)"
    by simp
  from this corr_p correct_closed have corr_pi: "correct p (te p i)"
    by blast
  from corr_p rts1d nonoverlap have "rmin ≤ te p (i+1) - te p i"
    by simp
  from this nonoverlap have "β ≤ te p (i+1) - te p i" by simp
  hence "te p i + β ≤ te p (i+1)" by simp

  from this corr_p corr_q rts2a
  have "te q i ≤ te p (i+1)"
    by blast
  thus ?thesis by simp
qed

lemma beta_bound2:
assumes corr_p: "correct p (te p (i+1))"
and corr_q: "correct q (te q i)"
shows "te p (i+1) - te q i ≤ rmax + β"
proof-
  from corr_p rte have "te p i ≤ te p (i+1)"
    by simp
  from this corr_p correct_closed have corr_pi: "correct p (te p i)"
    by blast

  have split: "te p (i+1) - te q i =
    (te p (i+1) - te p i) + (te p i - te q i)"
    by (simp)

  from corr_q corr_pi rts2b have Eq1: "abs(te p i - te q i) ≤ β"
    by simp
  have Eq2: "te p i - te q i ≤ β"
  proof cases
    assume "te q i ≤ te p i"
    from this Eq1 show ?thesis
      by (simp add: abs_if)
  next
    assume "¬ (te q i ≤ te p i)"
    from this Eq1 show ?thesis
      by (simp add: abs_if)
  qed

  from corr_p rts0d have "te p (i+1) - te p i ≤ rmax"
    by simp
  from this split Eq2 show ?thesis by simp
qed

subsubsection‹Bounded-drift for logical clocks (IC)›

lemma bd:
  assumes ie: "s ≤ t"
  and rb1: "rho_bound1 C"
  and rb2: "rho_bound2 D"
  and PC_ie: "D q t - D q s ≤ C p t - C p s"
  and corr_p: "correct p t"
  and corr_q: "correct q t"
  shows "¦ C p t - D q t ¦  ≤ ¦ C p s - D q s ¦ + 2*ρ*(t - s)"
proof-
  let ?Dt = "C p t - D q t"
  let ?Ds = "C p s - D q s"
  let ?Bp = "C p t - C p s"
  let ?Bq = "D q t - D q s"
  let ?I = "t - s"

  have "¦ ?Bp - ?Bq ¦ ≤ 2*ρ*(t - s)"
  proof-
    from PC_ie have Eq1: "¦ ?Bp - ?Bq ¦ = ?Bp - ?Bq" by (simp add: abs_if)
    from corr_p ie rb1 have Eq2: "?Bp - ?Bq ≤ ?I*(1+ρ) - ?Bq" (is "?E1 ≤ ?E2")
      by(simp add: rho_bound1_def)
    from corr_q ie rb2 have "?I*(1 - ρ) ≤ ?Bq"
      by(simp add: rho_bound2_def)
    from this have Eq3: "?E2 ≤ ?I*(1+ρ) - ?I*(1 - ρ)"
      by(simp)
    have Eq4: "?I*(1+ρ) - ?I*(1 - ρ) = 2*ρ*?I"
      by(simp add: algebra_simps)
    from Eq1 Eq2 Eq3 Eq4 show ?thesis by simp
  qed
  moreover
  have "¦?Dt¦  ≤ ¦?Bp - ?Bq¦  + ¦?Ds¦"
    by(simp add: abs_if)
  ultimately show ?thesis by simp
qed

lemma bounded_drift:
  assumes ie: "s ≤ t"
  and rb1: "rho_bound1 C"
  and rb2: "rho_bound2 C"
  and rb3: "rho_bound1 D"
  and rb4: "rho_bound2 D"
  and corr_p: "correct p t"
  and corr_q: "correct q t"
  shows "¦C p t - D q t¦ ≤ ¦C p s - D q s¦  + 2*ρ*(t - s)"
proof-
  let ?Bp = "C p t - C p s"
  let ?Bq = "D q t - D q s"

  show ?thesis
  proof cases
    assume "?Bq ≤ ?Bp"
    from this ie rb1 rb4 corr_p corr_q bd show ?thesis by simp
  next
    assume "¬ (?Bq ≤ ?Bp)"
    hence "?Bp ≤ ?Bq" by simp
    from this ie rb2 rb3 corr_p corr_q bd
    have "¦D q t - C p t¦  ≤ ¦D q s - C p s¦ + 2*ρ*(t - s)"
      by simp
    from this show ?thesis by (simp add: abs_minus_commute)
  qed
qed

text‹Drift rate of logical clocks›

lemma IC_rate1:
"rho_bound1 (λ p t. IC p i t)"
proof-
  {
    fix p::process
    fix s::time
    fix t::time
    assume cp: "correct p t"
    assume ie: "s ≤ t"
    from cp ie correct_closed have cps: "correct p s"
      by blast
    have "IC p i t - IC p i s ≤ (t - s)*(1+ρ)"
    proof-
      from cp IClock have "IC p i t = PC p t + Adj p i"
        by simp
      moreover
      from cps IClock have "IC p i s = PC p s + Adj p i"
        by simp
      moreover
      from cp ie rate_1 have "PC p t - PC p s ≤ (t - s)*(1+ρ)"
        by simp
      ultimately show ?thesis by simp
    qed
  }
  thus ?thesis by (simp add: rho_bound1_def)
qed

lemma IC_rate2:
"rho_bound2 (λ p t. IC p i t)"
proof-
  {
    fix p::process
    fix s::time
    fix t::time
    assume cp: "correct p t"
    assume ie: "s ≤ t"
    from cp ie correct_closed have cps: "correct p s"
      by blast
    have "(t - s)*(1 - ρ) ≤ IC p i t - IC p i s"
    proof-
      from cp IClock have "IC p i t = PC p t + Adj p i"
        by simp
      moreover
      from cps IClock have "IC p i s = PC p s + Adj p i"
        by simp
      moreover
      from cp ie rate_2 have "(t - s)*(1-ρ) ≤ PC p t - PC p s"
        by simp
      ultimately show ?thesis by simp
    qed
  }
  thus ?thesis by (simp add: rho_bound2_def)
qed

text‹Auxilary function ‹ICf›: we introduce this to avoid some
unification problem in some tactic of isabelle.›

definition
  ICf :: "nat ⇒ (process ⇒ time ⇒ Clocktime)" where
  "ICf i = (λ p t. IC p i t)"

lemma IC_bd:
  assumes ie: "s ≤ t"
  and corr_p: "correct p t"
  and corr_q: "correct q t"
  shows "¦IC p i t - IC q j t¦ ≤ ¦IC p i s - IC q j s¦ + 2*ρ*(t - s)"
proof-
  let ?C = "ICf i"
  let ?D = "ICf j"
  let ?G = "¦?C p t - ?D q t¦ ≤ ¦?C p s - ?D q s¦ + 2*ρ*(t - s)"

  from IC_rate1 have rb1: "rho_bound1 (ICf i) ∧ rho_bound1 (ICf j)"
    by (simp add: ICf_def)

  from IC_rate2 have rb2: "rho_bound2 (ICf i) ∧ rho_bound2 (ICf j)"
    by (simp add: ICf_def)

  from ie rb1 rb2 corr_p corr_q bounded_drift
  have ?G by simp

  from this show ?thesis by (simp add: ICf_def)
qed

lemma event_bound:
assumes ie1: "0 ≤ (t::real)"
and corr_p: "correct p t"
and corr_q: "correct q t"
shows "∃ i. t < max (te p i) (te q i)"
proof (rule ccontr)
  assume A: "¬ (∃ i. t < max (te p i) (te q i))"
  show False
  proof-
    have F1: "∀ i. te p i ≤ t"
    proof
      fix i :: nat
      from A have "¬ (t < max (te p i) (te q i))"
        by simp
      hence Eq1: "max (te p i) (te q i) ≤ t" by arith
      have Eq2: "te p i ≤ max (te p i) (te q i)"
        by (simp add: max_def)
      from Eq1 Eq2 show "te p i ≤ t" by simp
    qed

    have F2: "∀ (i :: nat). correct p (te p i)"
    proof
      fix i :: nat
      from F1 have "te p i ≤ t" by simp
      from this corr_p correct_closed
      show "correct p (te p i)" by blast
    qed

    have F3: "∀ (i :: nat). real i * rmin ≤ te p i"
    proof
      fix i :: nat
      show "real i * rmin ≤ te p i"
      proof (induct i)
        from synch0 show "real (0::nat) * rmin ≤ te p 0" by simp
      next
        fix i :: nat assume ind_hyp: "real i * rmin ≤ te p i"

        show "real (Suc i) * rmin ≤ te p (Suc i)"
        proof-

          have Eq1: "real i * rmin + rmin = (real i + 1)*rmin"
            by (simp add: distrib_right)
          have Eq2: "real i + 1 = real (i+1)" by simp
          from Eq1 Eq2
          have Eq3: "real i * rmin + rmin = real (i+1) * rmin"
            by presburger

          from F2 have cp1: "correct p (te p (i+1))"
            by simp
          from F2 have cp2: "correct p (te p i)"
            by simp
          from cp1 rts1d have "rmin ≤ te p (i+1) - te p i"
            by simp
          hence Eq4: "te p i + rmin ≤ te p (i+1)" by simp
          from ind_hyp have "real i * rmin + rmin ≤ te p i + rmin"
            by (simp)
          from this Eq4 have "real i * rmin + rmin ≤ te p (i+1)"
            by simp
          from this Eq3 show ?thesis by simp
        qed
      qed
    qed

    have F4: "∀ (i::nat). real i * rmin ≤ t"
    proof
      fix i::nat
      from F1 have "te p i ≤ t" by simp
      moreover
      from F3 have "real i * rmin ≤ te p i" by simp
      ultimately show "real i * rmin ≤ t" by simp
    qed

    from constants_ax have "0 < rmin" by simp

    from this reals_Archimedean3
    have Archi: "∃ (k::nat). t < real k * rmin"
      by blast

    from Archi obtain k::nat where C: "t < real k * rmin" ..

    from F4 have "real k * rmin ≤ t" by simp
    hence notC: "¬ (t < real k * rmin)" by simp

    from C notC show False by simp
  qed
qed

subsection‹Agreement property›

definition "γ1 x = π (2*ρ*β + 2*Λ) (2*Λ + x + 2*ρ*(rmax + β))"
definition "γ2 x = x + 2*ρ*rmax"
definition "γ3 x = α (2*Λ + x + 2*ρ*(rmax + β)) + Λ + 2*ρ*β"

definition
  okmaxsync :: "[nat, Clocktime] ⇒ bool" where
  "okmaxsync i x ⟷ (∀ p q. correct p (max (te p i) (te q i))
     ∧ correct q (max (te p i) (te q i)) ⟶
       ¦IC p i (max (te p i) (te q i)) - IC q i (max (te p i) (te q i))¦ ≤ x)"

definition
  okClocks :: "[process, process, nat] ⇒ bool" where
  "okClocks p q i ⟷ (∀ t. 0 ≤ t ∧ t < max (te p i) (te q i)
        ∧ correct p t ∧ correct q t
     ⟶ ¦VC p t - VC q t¦ ≤ δ)"

lemma okClocks_sym:
assumes ok_pq: "okClocks p q i"
shows "okClocks q p i"
proof-
  {
    fix t :: time
    assume ie1: "0 ≤ t"
    assume ie2: "t < max (te q i) (te p i)"
    assume corr_q: "correct q t"
    assume corr_p: "correct p t"

    have "max (te q i) (te p i) = max (te p i) (te q i)"
      by (simp add: max_def)
    from this ok_pq ie1 ie2 corr_p corr_q
    have "¦VC q t - VC p t¦ ≤ δ"
      by(simp add: abs_minus_commute okClocks_def)
  }
  thus ?thesis by (simp add: okClocks_def)
qed

lemma ICp_Suc:
assumes corr_p: "correct p (te p (i+1))"
shows "IC p (i+1) (te p (i+1)) = cfn p (θ p (i+1)) "
using corr_p IClock by(simp add: Adj_def)

lemma IC_trans_inv:
assumes ie1: "te q (i+1) ≤ te p (i+1)"
and corr_p: "correct p (te p (i+1))"
and corr_q: "correct q (te p (i+1))"
shows
"IC q (i+1) (te p (i+1)) =
  cfn q (λ n. θ q (i+1) n + (PC q (te p (i+1)) - PC q (te q (i+1))))"
(is "?T1 = ?T2")
proof-
  let ?X = "PC q (te p (i+1)) - PC q (te q (i+1))"


  from corr_q ie1 PC_monotone have posX: "0 ≤ ?X"
    by (simp add: le_diff_eq)
  from IClock corr_q have "?T1 = cfn q (θ q (i+1)) + ?X"
    by(simp add: Adj_def)

  from this posX trans_inv show ?thesis by simp
qed

lemma beta_rho:
assumes ie: "te q (i+1) ≤ te p (i+1)"
and corr_p: "correct p (te p (i+1))"
and corr_q: "correct q (te p (i+1))"
and corr_l: "correct l (te p (i+1))"
shows "¦(PC l (te p (i+1)) - PC l (te q (i+1))) - (te p (i+1) - te q (i+1))¦ ≤ β*ρ"
proof-
  let ?X = "(PC l (te p (i+1)) - PC l (te q (i+1)))"
  let ?D = "te p (i+1) - te q (i+1)"

  from ie have posD: "0 ≤ ?D" by simp

  from ie PC_monotone corr_l have posX: "0 ≤ ?X"
    by (simp add: le_diff_eq)
  from ie corr_l rate_1 have bound1: "?X ≤ ?D * (1 + ρ)" by simp
  from ie corr_l correct_closed have corr_l_tq: "correct l (te q (i+1))"
    by(blast)
  from ie corr_q correct_closed have corr_q_tq: "correct q (te q (i+1))"
    by blast
  from corr_q_tq corr_p rts2b have "¦?D¦ ≤ β"
    by(simp)
  from this constants_ax posD have D_beta: "?D*ρ ≤ β*ρ"
    by(simp add: abs_if)

  show ?thesis
  proof cases
    assume A: "?D ≤ ?X"
    from posX posD A have absEq: "¦?X - ?D¦ = ?X - ?D"
      by(simp add: abs_if)
    from bound1 have bound2: "?X - ?D ≤ ?D*ρ"
      by(simp add: mult.commute distrib_right)
    from D_beta absEq bound2 show ?thesis by simp
  next
    assume notA: "¬ (?D ≤ ?X)"
    from this have absEq2: "¦?X - ?D¦ = ?D - ?X"
      by(simp add: abs_if)
    from ie corr_l rate_2 have bound3: "?D*(1 - ρ) ≤ ?X" by simp
    from this have "?D - ?X ≤ ?D*ρ" by (simp add: algebra_simps)
    from this absEq2 D_beta show ?thesis by simp
  qed
qed

text‹This lemma (and the next one pe-cond2) proves an assumption used
in the precision enhancement.›

lemma pe_cond1:
assumes ie: "te q (i+1) ≤ te p (i+1)"
and corr_p: "correct p (te p (i+1))"
and corr_q: "correct q (te p (i + 1))"
and corr_l: "correct l (te p (i+1))"
shows "¦θ q (i+1) l + (PC q (te p (i+1)) - PC q (te q (i+1))) -
           θ p (i+1) l¦ ≤ 2* ρ * β + 2*Λ"
(is "?M ≤ ?N")
proof-
  let ?Xl = "(PC l (te p (i+1)) - PC l (te q (i+1)))"
  let ?Xq = "(PC q (te p (i+1)) - PC q (te q (i+1)))"
  let ?D = "te p (i+1) - te q (i+1)"
  let ?T = "θ p (i+1) l - θ q (i+1) l"
  let ?RE1 = "θ p (i+1) l - IC l i (te p (i+1))"
  let ?RE2 = "θ q (i+1) l - IC l i (te q (i+1))"
  let ?ICT = "IC l i (te p (i+1)) - IC l i (te q (i+1))"

  have "?M = ¦(?Xq - ?D) - (?T - ?D)¦"
  by(simp add: abs_if)

  hence Split: "?M ≤ ¦?Xq - ?D¦ + ¦?T - ?D¦"
    by(simp add: abs_if)

  from ie corr_q correct_closed have corr_q_tq: "correct q (te q (i+1))"
    by(blast)
  from ie corr_l correct_closed have corr_l_tq: "correct l (te q (i+1))"
    by blast

  from corr_p corr_q corr_l ie beta_rho
  have XlD: "¦?Xl - ?D¦ ≤ β*ρ"
    by simp

  from corr_p corr_q ie beta_rho
  have XqD: "¦?Xq - ?D¦ ≤ β*ρ" by simp

  have TD: "¦?T - ?D¦ ≤ 2*Λ + β*ρ"
  proof-
    have Eq1: "¦?T - ?D¦ = ¦(?T - ?ICT) + (?ICT - ?D)¦" (is "?E1 = ?E2")
      by (simp add: abs_if)

    have Eq2: "?E2 ≤ ¦?T - ?ICT¦ + ¦?ICT - ?D¦"
      by(simp add: abs_if)

    have Eq3: "¦?T - ?ICT¦ ≤  ¦?RE1¦ + ¦?RE2¦"
      by(simp add: abs_if)

    from readerror corr_p corr_l
    have Eq4: "¦?RE1¦ ≤ Λ" by simp


    from corr_l_tq corr_q_tq this readerror
    have Eq5: "¦?RE2¦ ≤ Λ" by simp

    from Eq3 Eq4 Eq5 have Eq6: "¦?T - ?ICT¦ ≤ 2*Λ"
      by simp

    have Eq7: "?ICT - ?D = ?Xl - ?D"
    proof-
      from corr_p rte have "te p i ≤ te p (i+1)"
        by(simp)
      from this corr_l correct_closed have corr_l_tpi: "correct l (te p i)"
        by blast
      from corr_q_tq rte have "te q i ≤ te q (i+1)"
        by simp
      from this corr_l_tq correct_closed have corr_l_tqi: "correct l (te q i)"
        by blast

      from IClock corr_l
      have F1: "IC l i (te p (i+1)) = PC l (te p (i+1)) + Adj l i"
        by(simp)
      from IClock corr_l_tq
      have F2: "IC l i (te q (i+1)) = PC l (te q (i+1)) + Adj l i"
        by simp
      from F1 F2 show ?thesis by(simp)
    qed

    from this XlD have Eq8: "¦?ICT - ?D¦ ≤ β*ρ"
      by arith
    from Eq1 Eq2 Eq6 Eq8 show ?thesis
      by(simp)
  qed

  from Split XqD TD have F1: "?M ≤ 2* β * ρ + 2*Λ"
    by(simp)
  have F2: "2 * ρ * β + 2*Λ = 2* β * ρ + 2*Λ"
    by simp
  from F1 show ?thesis by (simp only: F2)

qed

lemma pe_cond2:
assumes ie: "te m i ≤ te l i"
and corr_k: "correct k (te k (i+1))"
and corr_l_tk: "correct l (te k (i+1))"
and corr_m_tk: "correct m (te k (i+1))"
and ind_hyp: "¦IC l i (te l i) - IC m i (te l i)¦ ≤ δS"
shows "¦θ k (i+1) l - θ k (i+1) m¦ ≤ 2*Λ + δS + 2*ρ*(rmax + β)"
proof-
  let ?X = "θ k (i+1) l - θ k (i+1) m"
  let ?N = "2*Λ + δS + 2*ρ*(rmax + β)"
  let ?D1 = "θ k (i+1) l - IC l i (te k (i+1))"
  let ?D2 = "θ k (i+1) m - IC m i (te k (i+1))"
  let ?ICS = "IC l i (te k (i+1)) - IC m i (te k (i+1))"
  let ?tlm = "te l i"
  let ?IC = "IC l i ?tlm - IC m i ?tlm"

  have Eq1: "¦?X¦ = ¦(?D1 - ?D2) + ?ICS¦" (is "?E1 = ?E2")
    by (simp add: abs_if)

  have Eq2: "?E2 ≤ ¦?D1 - ?D2¦ + ¦?ICS¦" by (simp add: abs_if)

  from corr_l_tk corr_k beta_bound1 have ie_lk: "te l i ≤ te k (i+1)"
    by (simp add: le_diff_eq)

  from this corr_l_tk correct_closed have corr_l: "correct l (te l i)"
    by blast

  from ie_lk corr_l_tk corr_m_tk IC_bd
  have Eq3: "¦?ICS¦ ≤ ¦?IC¦ + 2*ρ*(te k (i+1) - ?tlm)"
    by simp
  from this ind_hyp have Eq4: "¦?ICS¦ ≤ δS + 2*ρ*(te k (i+1) - ?tlm)"
    by simp

  from corr_l corr_k beta_bound2 have "te k (i+1) - ?tlm ≤ rmax + β"
    by simp
  from this constants_ax have "2*ρ*(te k (i+1) - ?tlm) ≤ 2*ρ*(rmax + β)"
    by simp
  from this Eq4 have Eq4a: "¦?ICS¦ ≤ δS + 2*ρ*(rmax + β)"
    by simp

  from corr_k corr_l_tk readerror
  have Eq5: "¦?D1¦ ≤ Λ" by simp
  from corr_k corr_m_tk readerror
  have Eq6: "¦?D2¦ ≤ Λ" by simp
  have "¦?D1 - ?D2¦ ≤ ¦?D1¦ + ¦?D2¦" by (simp add: abs_if)
  from this Eq5 Eq6 have Eq7: "¦?D1 - ?D2¦ ≤ 2*Λ"
    by (simp)

  from Eq1 Eq2 Eq4a Eq7 split show ?thesis by (simp)
qed

lemma theta_bound:
assumes corr_l: "correct l (te p (i+1))"
and corr_m: "correct m (te p (i+1))"
and corr_p: "correct p (te p (i+1))"
and IC_bound:
    "¦IC l i (max (te l i) (te m i)) - IC m i (max (te l i) (te m i))¦
      ≤ δS"
shows "¦θ p (i+1) l - θ p (i+1) m¦
       ≤  2*Λ + δS + 2*ρ*(rmax + β)"
proof-
  from corr_p corr_l beta_bound1 have tli_le_tp: "te l i ≤ te p (i+1)"
    by (simp add: le_diff_eq)
  from corr_p corr_m beta_bound1 have tmi_le_tp: "te m i ≤ te p (i+1)"
    by (simp add: le_diff_eq)

  let ?tml = "max (te l i) (te m i)"
  from tli_le_tp tmi_le_tp have tml_le_tp: "?tml ≤ te p (i+1)"
    by simp

  from tml_le_tp corr_l correct_closed have corr_l_tml: "correct l ?tml"
    by blast
  from tml_le_tp corr_m correct_closed have corr_m_tml: "correct m ?tml"
    by blast

  let ?Y = "2*Λ + δS + 2*ρ*(rmax + β)"
  show "¦θ p (i+1) l - θ p (i+1) m¦ ≤ ?Y"
  proof cases
    assume A: "te m i < te l i"

    from this IC_bound
    have "¦IC l i (te l i) - IC m i (te l i)¦ ≤ δS"
      by(simp add: max_def)
    from this A corr_p corr_l corr_m pe_cond2
    show ?thesis by(simp)
  next
    assume "¬ (te m i < te l i)"
    hence Eq1: "te l i ≤ te m i" by simp
    from this IC_bound
    have Eq2: "¦IC l i (te m i) - IC m i (te m i)¦ ≤ δS"
      by(simp add: max_def)

    hence "¦IC m i (te m i) - IC l i (te m i)¦ ≤ δS"
      by (simp add: abs_minus_commute)
    from this Eq1 corr_p corr_l corr_m pe_cond2
    have "¦θ p (i+1) m - θ p (i+1) l¦ ≤ ?Y"
      by(simp)
    thus ?thesis by (simp add: abs_minus_commute)
  qed
qed

lemma four_one_ind_half:
  assumes ie1: "β ≤ rmin"
  and ie2: "μ ≤ δS"
  and ie3: "γ1 δS ≤ δS"
  and ind_hyp: "okmaxsync i δS"
  and ie4: "te q (i+1) ≤ te p (i+1)"
  and corr_p: "correct p (te p (i+1))"
  and corr_q: "correct q (te p (i+1))"
shows "¦IC p (i+1) (te p (i+1)) - IC q (i+1) (te p (i+1))¦ ≤ δS"
proof-
  let ?tpq = "te p (i+1)"

  let ?f = "λ n. θ q (i+1) n + (PC q (te p (i+1)) - PC q (te q (i+1)))"
  let ?g = "θ p (i+1)"

  from ie4 corr_q correct_closed have corr_q_tq: "correct q (te q (i+1))"
    by blast

  have Eq_IC_cfn: "¦IC p (i+1) ?tpq - IC q (i+1) ?tpq¦ =
    ¦cfn q ?f - cfn p ?g¦"
  proof-
    from corr_p ICp_Suc have Eq1: "IC p (i+1) ?tpq = cfn p ?g" by simp

    from ie4 corr_p corr_q IC_trans_inv
    have Eq2: "IC q (i+1) ?tpq = cfn q ?f" by simp

    from Eq1 Eq2 show ?thesis by(simp add: abs_if)
  qed

  let ?ppred = "λ l. correct l (te p (i+1))"

  let ?X = "2*ρ*β + 2*Λ"
  have "∀ l. ?ppred l ⟶ ¦?f l - ?g l¦ ≤ ?X"
  proof -
    {
      fix l
      assume "?ppred l"
      from ie4 corr_p corr_q this pe_cond1
      have "¦?f l - ?g l¦ ≤ (2*ρ*β + 2*Λ)"
        by(auto)
    }
    thus ?thesis by blast
  qed
  hence cond1: "okRead2 ?f ?g ?X ?ppred"
    by(simp add: okRead2_def)

  let ?Y = "2*Λ + δS + 2*ρ*(rmax + β)"

  have "∀ l m. ?ppred l ∧ ?ppred m ⟶ ¦?f l - ?f m¦ ≤ ?Y"
  proof-
    {
      fix l m
      assume corr_l: "?ppred l"
      assume corr_m: "?ppred m"

      from corr_p corr_l beta_bound1 have tli_le_tp: "te l i ≤ te p (i+1)"
        by (simp add: le_diff_eq)
      from corr_p corr_m beta_bound1 have tmi_le_tp: "te m i ≤ te p (i+1)"
        by (simp add: le_diff_eq)

      let ?tlm = "max (te l i) (te m i)"

      from tli_le_tp tmi_le_tp have tlm_le_tp: "?tlm ≤ te p (i+1)"
        by simp

      from ie4 corr_l correct_closed have corr_l_tq: "correct l (te q (i+1))"
        by blast
      from ie4 corr_m correct_closed have corr_m_tq: "correct m (te q (i+1))"
        by blast
      from tlm_le_tp corr_l correct_closed have corr_l_tlm: "correct l ?tlm"
        by blast
      from tlm_le_tp corr_m correct_closed have corr_m_tlm: "correct m ?tlm"
        by blast

      from ind_hyp corr_l_tlm corr_m_tlm
      have EqAbs1: "¦IC l i ?tlm - IC m i ?tlm¦ ≤ δS"
        by(auto simp add: okmaxsync_def)

      have EqAbs3: "¦?f l - ?f m¦ = ¦θ q (i+1) l - θ q (i+1) m¦"
        by (simp add: abs_if)

      from EqAbs1 corr_q_tq corr_l_tq corr_m_tq theta_bound
      have "¦θ q (i+1) l - θ q (i+1) m¦ ≤ ?Y"
        by simp
      from this EqAbs3  have "¦?f l - ?f m¦ ≤ ?Y"
        by simp
    }
    thus ?thesis by simp
  qed
  hence cond2a: "okRead1 ?f ?Y ?ppred" by (simp add: okRead1_def)

  have "∀ l m. ?ppred l ∧ ?ppred m ⟶ ¦?g l - ?g m¦ ≤ ?Y"
  proof-
    {
      fix l m
      assume corr_l: "?ppred l"
      assume corr_m: "?ppred m"

      from corr_p corr_l beta_bound1 have tli_le_tp: "te l i ≤ te p (i+1)"
        by (simp add: le_diff_eq)
      from corr_p corr_m beta_bound1 have tmi_le_tp: "te m i ≤ te p (i+1)"
        by (simp add: le_diff_eq)

      let ?tlm = "max (te l i) (te m i)"
      from tli_le_tp tmi_le_tp have tlm_le_tp: "?tlm ≤ te p (i+1)"
        by simp

      from tlm_le_tp corr_l correct_closed have corr_l_tlm: "correct l ?tlm"
        by blast
      from tlm_le_tp corr_m correct_closed have corr_m_tlm: "correct m ?tlm"
        by blast

      from ind_hyp corr_l_tlm corr_m_tlm
      have EqAbs1: "¦IC l i ?tlm - IC m i ?tlm¦ ≤ δS"
        by(auto simp add: okmaxsync_def)

      from EqAbs1 corr_p corr_l corr_m theta_bound
      have "¦?g l - ?g m¦ ≤ ?Y" by simp
    }
    thus ?thesis by simp
  qed
  hence cond2b: "okRead1 ?g ?Y ?ppred" by (simp add: okRead1_def)

  from correct_count have "np - maxfaults ≤ count ?ppred np"
    by simp
  from this corr_p corr_q cond1 cond2a cond2b prec_enh
  have "¦cfn q ?f - cfn p ?g¦ ≤ π ?X ?Y"
    by blast

  from ie3 this have "¦cfn q ?f - cfn p ?g¦ ≤ δS"
    by (simp add: γ1_def)

  from this Eq_IC_cfn show ?thesis by (simp)
qed

text‹Theorem 4.1 in Shankar's paper.›

theorem four_one:
  assumes ie1: "β ≤ rmin"
  and ie2: "μ ≤ δS"
  and ie3: "γ1 δS ≤ δS"
shows "okmaxsync i δS"
proof(induct i)
  show "okmaxsync 0 δS"
  proof-
    {
      fix p q
      assume corr_p: "correct p (max (te p 0) (te q 0))"
      assume corr_q: "correct q (max (te p 0) (te q 0))"

      from corr_p synch0 have cp0: "correct p 0" by simp
      from corr_q synch0 have cq0: "correct q 0" by simp

      from synch0 cp0 cq0 IClock
      have IC_eq_PC:
        "¦IC p 0 (max (te p 0) (te q 0)) - IC q 0 (max (te p 0) (te q 0))¦
         = ¦PC p 0 - PC q 0¦" (is "?T1 = ?T2")
        by(simp add: Adj_def)

      from ie2 init synch0 cp0 have range1: "0 ≤ PC p 0 ∧ PC p 0 ≤ δS"
        by auto
      from ie2 init synch0 cq0 have range2: "0 ≤ PC q 0 ∧ PC q 0 ≤ δS"
        by auto
      have "?T2 ≤ δS"
      proof cases
        assume A:"PC p 0 < PC q 0"
        from A range1 range2 show ?thesis
          by(auto simp add: abs_if)
      next
        assume notA: "¬ (PC p 0 < PC q 0)"
        from notA range1 range2 show ?thesis
          by(auto simp add: abs_if)
      qed
      from this IC_eq_PC have "?T1 ≤ δS" by simp
    }
    thus ?thesis by (simp add: okmaxsync_def)
  qed
next
  fix i assume ind_hyp: "okmaxsync i δS"
  show "okmaxsync (Suc i) δS"
  proof-
    {
      fix p q
      assume corr_p: "correct p (max (te p (i + 1)) (te q (i + 1)))"
      assume corr_q: "correct q (max (te p (i + 1)) (te q (i + 1)))"
      let ?tp = "te p (i + 1)"
      let ?tq = "te q (i + 1)"
      let ?tpq = "max ?tp ?tq"

      have "¦IC p (i+1) ?tpq - IC q (i+1) ?tpq¦ ≤ δS" (is "?E1 ≤ δS")
      proof cases
        assume A: "?tq < ?tp"
        from A corr_p have cp1: "correct p (te p (i+1))"
          by (simp add: max_def)
        from A corr_q have cq1: "correct q (te p (i+1))"
          by (simp add: max_def)
        from A
        have Eq1: "?E1 = ¦IC p (i+1) (te p (i+1)) - IC q (i+1) (te p (i+1))¦"
                  (is "?E1 = ?E2")
          by (simp add: max_def)
        from A cp1 cq1 corr_p corr_q ind_hyp ie1 ie2 ie3
          four_one_ind_half
        have "?E2 ≤ δS" by (simp)
        from this Eq1 show ?thesis by simp
      next
        assume notA: "¬ (?tq < ?tp)"
        from this corr_p have cp2: "correct p (te q (i+1))"
          by (simp add: max_def)
        from notA corr_q have cq2: "correct q (te q (i+1))"
          by (simp add: max_def)
        from notA
        have Eq2: "?E1 = ¦IC q (i+1) (te q (i+1)) - IC p (i+1) (te q (i+1))¦"
                  (is "?E1  = ?E3")
          by (simp add: max_def abs_minus_commute)
        from notA have "?tp ≤ ?tq" by simp
        from this cp2 cq2 ind_hyp ie1 ie2 ie3 four_one_ind_half
        have "?E3 ≤ δS"
          by simp
        from this Eq2 show ?thesis by (simp)
      qed
    }
    thus ?thesis by (simp add: okmaxsync_def)
  qed
qed

lemma VC_cfn:
  assumes corr_p: "correct p (te p (i+1))"
  and ie: "te p (i+1) < te p (i+2)"
shows "VC p (te p (i+1)) = cfn p (θ p (i+1))"
proof-
  from ie corr_p VClock have "VC p (te p (i+1)) = IC p (i+1) (te p (i+1))"
    by simp
  moreover
  from corr_p IClock
  have "IC p (i+1) (te p (i+1)) = PC p (te p (i+1)) + Adj p (i+1)"
    by blast
  moreover
  have "PC p (te p (i+1)) + Adj p (i+1) = cfn p (θ p (i+1))"
    by(simp add: Adj_def)
  ultimately show ?thesis by simp
qed

text‹Lemma for the inductive case in Theorem 4.2›

lemma four_two_ind:
  assumes ie1: "β ≤ rmin"
  and ie2: "μ ≤ δS"
  and ie3: "γ1 δS ≤ δS"
  and ie4: "γ2 δS ≤ δ"
  and ie5: "γ3 δS ≤ δ"
  and ie6: "te q (i+1) ≤ te p (i+1)"
  and ind_hyp: "okClocks p q i"
  and t_bound1: "0 ≤ t"
  and t_bound2: "t < max (te p (i+1)) (te q (i+1))"
  and t_bound3: "max (te p i) (te q i) ≤ t"
  and tpq_bound: "max (te p i) (te q i) < max (te p (i+1)) (te q (i+1))"
  and corr_p: "correct p t"
  and corr_q: "correct q t"
shows "¦VC p t - VC q t¦ ≤ δ"
proof cases
  assume A: "t < te q (i+1)"

  let ?tpq = "max (te p i) (te q i)"

  have Eq1: "te p i ≤ t ∧ te q i ≤ t"
  proof cases
    assume "te p i ≤ te q i"
    from this  t_bound3 show ?thesis by (simp add: max_def)
  next
    assume "¬ (te p i ≤ te q i)"
    from this t_bound3 show ?thesis by (simp add: max_def)
  qed

  from ie6 have tp_max: "max (te p (i+1)) (te q (i+1)) = te p (i+1)"
    by(simp add: max_def)
  from this t_bound2 have Eq2: "t < te p (i+1)" by simp

  from VClock Eq1 Eq2 corr_p have Eq3: "VC p t = IC p i t" by simp

  from VClock Eq1 A corr_q have Eq4: "VC q t = IC q i t" by simp
  from Eq3 Eq4 have Eq5: "¦VC p t - VC q t¦ = ¦IC p i t - IC q i t¦"
    by simp

  from t_bound3 corr_p corr_q correct_closed
  have corr_tpq: "correct p ?tpq ∧ correct q ?tpq"
    by(blast)

  from t_bound3 IC_bd corr_p corr_q
  have Eq6: "¦IC p i t - IC q i t¦  ≤ ¦IC p i ?tpq - IC q i ?tpq¦
    + 2*ρ*(t - ?tpq)" (is "?E1 ≤ ?E2")
    by(blast)

  from ie1 ie2 ie3 four_one have "okmaxsync i δS" by simp

  from this corr_tpq have "¦IC p i ?tpq - IC q i ?tpq¦ ≤ δS"
    by(simp add: okmaxsync_def)

  from Eq6 this  have Eq7: "?E1 ≤ δS + 2*ρ*(t - ?tpq)" by simp

  from corr_p Eq2 rts0 have "t - te p i ≤ rmax" by simp
  from this have "t - ?tpq ≤ rmax" by (simp add: max_def)
  from this constants_ax have "2*ρ*(t - ?tpq) ≤ 2*ρ*rmax"
    by simp
  hence "δS + 2*ρ*(t - ?tpq) ≤ δS + 2*ρ*rmax"
    by simp
  from this Eq7 have "?E1 ≤ δS + 2*ρ*rmax" by simp
  from this Eq5 ie4 show ?thesis by(simp add: γ2_def)
next
  assume "¬ (t < te q (i+1))"
  hence  B: "te q (i+1) ≤ t" by simp

  from ie6 t_bound2
  have tp_max: "max (te p (i+1)) (te q (i+1)) = te p (i+1)"
    by(simp add: max_def)

  have "te p i ≤ max (te p i) (te q i)"
    by(simp add: max_def)

  from this t_bound3 have tp_bound1: "te p i ≤ t" by simp

  from tp_max t_bound2 have tp_bound2: "t < te p (i+1)" by simp

  have tq_bound1: "t < te q (i+2)"
  proof (rule ccontr)
    assume "¬ (t < te q (i+2))"
    hence C: "te q (i+2) ≤ t" by simp

    from C corr_q correct_closed
    have corr_q_t2: "correct q (te q (i+2))" by blast

    have "te q (i+1) + β ≤ t"
    proof-
      from corr_q_t2 rts1d have "rmin ≤ te q (i+2) - te q (i+1)"
        by simp
      from this ie1 have "β ≤ te q (i+2) - te q (i+1)"
        by simp
      hence "te q (i+1) + β ≤ te q (i+2)" by simp
      from this C show ?thesis by simp
    qed
    from this corr_p corr_q rts2a have "te p (i+1) ≤ t"
      by blast
    hence "¬ (t < te p (i+1))" by simp
    from this tp_bound2 show False by simp
  qed

  from tq_bound1 B have tq_bound2: "te q (i+1) < te q (i+2)" by simp
  from B tp_bound2 have tq_bound3: "te q (i+1) < te p (i+1)"
    by simp
  from B corr_p correct_closed
  have corr_p_tq1: "correct p (te q (i+1))" by blast

  from B correct_closed corr_q
  have corr_q_tq1: "correct q (te q (i+1))" by blast

  from corr_p_tq1 corr_q_tq1 beta_bound1
  have tq_bound4: "te p i ≤ te q (i+1)"
    by(simp add: le_diff_eq)

  from tq_bound1 VClock B corr_q
  have Eq1: "VC q t = IC q (i+1) t" by simp

  from VClock tp_bound1 tp_bound2 corr_p
  have Eq2: "VC p t = IC p i t" by simp

  from Eq1 Eq2 have Eq3: "¦VC p t - VC q t¦ = ¦IC p i t - IC q (i+1) t¦"
    by simp

  from B corr_p corr_q IC_bd
  have "¦IC p i t - IC q (i+1) t¦ ≤
     ¦IC p i (te q (i+1)) - IC q (i+1) (te q (i+1))¦ + 2*ρ*(t - te q (i+1))"
    by simp

  from this Eq3
  have VC_split: "¦VC p t - VC q t¦ ≤
    ¦IC p i (te q (i+1)) - IC q (i+1) (te q (i+1))¦ + 2*ρ*(t - te q (i+1))"
    by simp

  from tq_bound2 VClock corr_q_tq1
  have Eq4: "VC q (te q (i+1)) = IC q (i+1) (te q (i+1))" by simp

  from this tq_bound2 VC_cfn corr_q_tq1
  have Eq5: "IC q (i+1) (te q (i+1)) = cfn q (θ q (i+1))" by simp

  hence IC_eq_cfn: "IC p i (te q (i+1)) - IC q (i+1) (te q (i+1)) =
    IC p i (te q (i+1)) - cfn q (θ q (i+1))"
    (is "?E1 = ?E2")
    by simp

  let ?f = "θ q (i+1)"
  let ?ppred = "λ l. correct l (te q (i+1))"
  let ?X = "2*Λ + δS + 2*ρ*(rmax + β)"

  have "∀ l m. ?ppred l ∧ ?ppred m ⟶ ¦θ q (i+1) l - θ q (i+1) m¦ ≤ ?X"
  proof-
    {
      fix l :: process
      fix m :: process
      assume corr_l: "?ppred l"
      assume corr_m: "?ppred m"

      let ?tlm = "max (te l i) (te m i)"
      have tlm_bound: "?tlm ≤ te q (i+1)"
      proof-
        from corr_l corr_q_tq1 beta_bound1 have "te l i ≤ te q (i+1)"
          by (simp add: le_diff_eq)
        moreover
        from corr_m corr_q_tq1 beta_bound1 have "te m i ≤ te q (i+1)"
          by (simp add: le_diff_eq)
        ultimately show ?thesis by simp
      qed

      from tlm_bound corr_l corr_m correct_closed
      have corr_tlm: "correct l ?tlm ∧ correct m ?tlm"
        by blast

      have "¦IC l i ?tlm - IC m i ?tlm¦ ≤ δS"
      proof-
        from ie1 ie2 ie3 four_one  have "okmaxsync i δS"
          by simp
        from this corr_tlm show ?thesis by(simp add: okmaxsync_def)
      qed

      from this corr_l corr_m corr_q_tq1 theta_bound
      have "¦θ q (i+1) l - θ q (i+1) m¦ ≤ ?X" by simp
    }
    thus ?thesis by blast
  qed
  hence readOK: "okRead1 (θ q (i+1)) ?X ?ppred"
    by(simp add: okRead1_def)

  let ?E3 = "cfn q (θ q (i+1)) - θ q (i+1) p"
  let ?E4 = "θ q (i+1) p - IC p i (te q (i+1))"

  have "¦?E2¦ = ¦?E3 + ?E4¦" by (simp add: abs_if)
  hence Eq8: "¦?E2¦ ≤ ¦?E3¦ + ¦?E4¦" by (simp add: abs_if)

  from correct_count have ppredOK: "np - maxfaults ≤ count ?ppred np"
    by simp
  from readOK ppredOK corr_p_tq1 corr_q_tq1 acc_prsv
  have "¦?E3¦ ≤ α ?X"
    by blast
  from this Eq8 have Eq9: "¦?E2¦ ≤ α ?X + ¦?E4¦" by simp

  from corr_p_tq1 corr_q_tq1 readerror
  have "¦?E4¦ ≤ Λ" by simp

  from this Eq9 have Eq10: "¦?E2¦ ≤ α ?X + Λ" by simp

  from this VC_split IC_eq_cfn
  have almost_right:
    "¦VC p t - VC q t¦ ≤
     α ?X + Λ + 2*ρ*(t - te q (i+1))"
    by simp

  have "t - te q (i+1) ≤ β"
  proof (rule ccontr)
    assume "¬ (t - te q (i+1) ≤ β)"
    hence "te q (i+1) + β ≤ t" by simp
    from this corr_p corr_q rts2a have "te p (i+1) ≤ t"
      by auto
    hence "¬ (t < te p (i+1))" by simp
    from this tp_bound2 show False
      by simp
  qed

  from this constants_ax
  have "α ?X + Λ + 2*ρ*(t - te q (i+1))
        ≤ α ?X + Λ + 2*ρ*β"
    by (simp)

  from this almost_right
  have "¦VC p t - VC q t¦ ≤ α ?X + Λ + 2*ρ*β"
    by arith

  from this ie5 show ?thesis by (simp add: γ3_def)
qed

text‹Theorem 4.2 in Shankar's paper.›

theorem four_two:
  assumes ie1: "β ≤ rmin"
  and ie2: "μ ≤ δS"
  and ie3: "γ1 δS ≤ δS"
  and ie4: "γ2 δS ≤ δ"
  and ie5: "γ3 δS ≤ δ"
shows "okClocks p q i"
proof (induct i)
  show "okClocks p q 0"
  proof-
    {
      fix t :: time
      assume t_bound1: "0 ≤ t"
      assume t_bound2: "t < max (te p 0) (te q 0)"
      assume corr_p: "correct p t"
      assume corr_q: "correct q t"
      from t_bound2 synch0 have "t < 0"
        by(simp add: max_def)
      from this t_bound1 have False by simp
      hence "¦VC p t - VC q t¦ ≤ δ" by simp
    }
    thus ?thesis by (simp add: okClocks_def)
  qed
next
  fix i::nat assume ind_hyp: "okClocks p q i"
  show "okClocks p q (Suc i)"
  proof -
    {
      fix t :: time
      assume t_bound1: "0 ≤ t"
      assume t_bound2: "t < max (te p (i+1)) (te q (i+1))"
      assume corr_p: "correct p t"
      assume corr_q: "correct q t"

      let ?tpq1 = "max (te p i) (te q i)"
      let ?tpq2 = "max (te p (i+1)) (te q (i+1))"

      have "¦VC p t - VC q t¦ ≤ δ"
      proof cases
        assume tpq_bound: "?tpq1 < ?tpq2"
        show ?thesis
        proof cases
          assume "t < ?tpq1"
          from t_bound1 this  corr_p corr_q ind_hyp
          show ?thesis by(simp add: okClocks_def)
        next
          assume "¬ (t < ?tpq1)"
          hence tpq_le_t: "?tpq1 ≤ t" by arith

          show ?thesis
          proof cases
            assume A: "te q (i+1) ≤ te p (i+1)"

            from this tpq_le_t tpq_bound ie1 ie2 ie3 ie4 ie5
              ind_hyp t_bound1 t_bound2
              corr_p corr_q tpq_bound four_two_ind
            show ?thesis by(simp)
          next
            assume "¬ (te q (i+1) ≤ te p (i+1))"
            hence B: "te p (i+1) ≤ te q (i+1)" by simp

            from ind_hyp okClocks_sym have ind_hyp1: "okClocks q p i"
              by blast

            have maxsym1: "max (te p (i+1)) (te q (i+1)) = max (te q (i+1)) (te p (i+1))"
              by (simp add: max_def)
            have maxsym2: "max (te p i) (te q i) = max (te q i) (te p i)"
              by (simp add: max_def)

            from maxsym1 t_bound2
            have t_bound21: "t < max (te q (i+1)) (te p (i+1))"
              by simp

            from maxsym1 maxsym2 tpq_bound
            have tpq_bound1: "max (te q i) (te p i) < max (te q (i+1)) (te p (i+1))"
              by simp
            from maxsym2 tpq_le_t
            have tpq_le_t1: "max (te q i) (te p i) ≤ t" by simp

            from B tpq_le_t1 tpq_bound1 ie1 ie2 ie3 ie4 ie5
              ind_hyp1 t_bound1 t_bound21
              corr_p corr_q tpq_bound four_two_ind
            have "¦VC q t - VC p t¦ ≤ δ" by(simp)
            thus ?thesis by (simp add: abs_minus_commute)
          qed

        qed
      next
        assume "¬ (?tpq1 < ?tpq2)"
        hence "?tpq2 ≤ ?tpq1" by arith
        from t_bound2 this have "t < ?tpq1" by arith
        from t_bound1 this corr_p corr_q ind_hyp
        show ?thesis by(simp add: okClocks_def)
      qed
    }
    thus ?thesis by (simp add: okClocks_def)
  qed
qed

text‹The main theorem: all correct clocks are synchronized within the
bound delta.›

theorem agreement:
  assumes ie1: "β ≤ rmin"
  and ie2: "μ ≤ δS"
  and ie3: "γ1 δS ≤ δS"
  and ie4: "γ2 δS ≤ δ"
  and ie5: "γ3 δS ≤ δ"
  and ie6: "0 ≤ t"
  and cpq: "correct p t ∧ correct q t"
shows "¦VC p t - VC q t¦ ≤ δ"
proof-
  from ie6 cpq event_bound have "∃ i :: nat. t < max (te p i) (te q i)"
    by simp
  from this obtain i  :: nat where t_bound: "t < max (te p i) (te q i)" ..

  from t_bound ie1 ie2 ie3 ie4 ie5 four_two have "okClocks p q i"
    by simp

  from ie6 this t_bound cpq show ?thesis
    by (simp add: okClocks_def)
qed

end