Theory GenClock

Up to index of Isabelle/HOL/GenClock

theory GenClock
imports Complex_Main
`(*  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 beginsubsection{* Types and constants definitions *}text{* Process is represented by natural numbers. The type 'event' correspondsto synchronization rounds. *}type_synonym process = nattype_synonym event = nat      (* synchronization rounds *)type_synonym time = realtype_synonym Clocktime = realaxiomatization  δ :: 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 simplemma rts1d:assumes cp: "correct p (te p (i+1))"shows "rmin ≤ te p (i+1) - te p i"using cp rts1 by simplemma 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 arithqedlemma 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 simpqedlemma 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 simpqedsubsubsection{* 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: diff_minus[symmetric] 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 simpqedlemma 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)  qedqedtext{* 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)qedlemma 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)qedtext{* Auxilary function @{text ICf}: we introduce this to avoid someunification 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)qedlemma 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(simp)          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  qedqedsubsection{* 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)qedlemma 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 simpqedlemma 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  qedqedtext{* 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)qedlemma 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 add: real_mult_le_cancel_iff2)  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)qedlemma 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)  qedqedlemma 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)qedtext{* 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)  qednext  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)  qedqedlemma 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 simpqedtext{* 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 add: real_mult_le_cancel_iff1)   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)qedtext{* 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)  qednext  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)  qedqed    text{* The main theorem: all correct clocks are synchronized within thebound 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)qedend`