Theory ICAInstance

(*  Title:       Instances of Schneider's generalized protocol of clock synchronization
    Author:      Damián Barsotti <damian at hal.famaf.unc.edu.ar>, 2006
    Maintainer:  Damián Barsotti <damian at hal.famaf.unc.edu.ar>
*)

section ‹Interactive Convergence Algorithms (ICA)›

theory ICAInstance imports Complex_Main begin

text ‹This algorithm is presented in \<^cite>‹"lamport_cs"›.›

text ‹A proof of the three properties can be found in
\<^cite>‹"shankar92mechanical"›.›

subsection ‹Model of the system›

text ‹The main ideas for the formalization of the system were
obtained from \<^cite>‹"shankar92mechanical"›.›

subsubsection ‹Types in the formalization›

text ‹The election of the basics types was based on
\<^cite>‹"shankar92mechanical"›. There, the process are natural numbers and
the real time and the clock readings are reals.›

type_synonym process = nat
type_synonym time = real       ― ‹real time›
type_synonym Clocktime = real  ― ‹time of the clock readings (clock time)›

subsubsection ‹Some constants›

text‹Here we define some parameters of the algorithm that we use:
the number of process and the fix value that is used to discard the
processes whose clocks differ more than this amount from the own one
(see \<^cite>‹"shankar92mechanical"›). The defined constants must satisfy
this axiom (if $np = 0$ we have a division by cero in the definition
of the convergence function).›

axiomatization
  np :: nat      ― ‹Number of processes› and
  Δ :: Clocktime ― ‹Fix value to discard processes› where
  constants_ax: "0 <= Δ ∧ np > 0" 

text ‹We define also the set of process that the algorithm
manage. This definition exist only for readability matters.›

definition
PR :: "process set" where
[simp]: "PR = {..<np}"


subsubsection ‹Convergence function›

text ‹This functions is called ``Egocentric Average''
(\<^cite>‹"schneider87understanding"›)›

text ‹In this algorithm each process has an array where it store the
clocks readings from the others processes (including itself). We
formalise that as a function from processes to clock time as
\<^cite>‹"shankar92mechanical"›.›

text ‹First we define an auxiliary function. It takes a function of
clock readings and two processes, and return de reading of the second
process if the difference of the readings is grater than @{term Δ},
otherwise it returns the reading of the first one.›

definition
  fiX :: "[(process ⇒ Clocktime), process, process] ⇒ Clocktime" where
  "fiX f p l = (if ¦f p - f l¦ <= Δ then (f l) else (f p))"

text ‹And finally the convergence function. This is defined with the
builtin generalized summation over a set constructor of Isabelle.
Also we had to use the overloaded @{term real} function to typecast de
number @{term np}.›

definition
  (* The averaging function to calculate clock adjustment *)
  cfni :: "[process, (process ⇒ Clocktime)] ⇒ Clocktime" where
  "cfni p f = (∑ l∈{..<np}. fiX f p l) / (real np)"

subsection ‹Translation Invariance property.›

text ‹We first need to prove this auxiliary lemma.›

lemma trans_inv': 
"(∑ l∈{..<np'}. fiX (λ y. f y + x) p l) = 
        (∑ l∈{..<np'}. fiX f p l) + real np' * x"
apply (induct_tac np')
apply (auto simp add: cfni_def  fiX_def of_nat_Suc 
       distrib_right lessThan_Suc)
done

theorem trans_inv: 
"∀ p f x . cfni p (λ y. f y + x) = cfni p f + x"
apply (auto simp add: cfni_def trans_inv' distrib_right 
       divide_inverse  constants_ax)
done

subsection ‹Precision Enhancement property›

text ‹An informal proof of this theorem can be found in
\<^cite>‹"shankar92mechanical"››

subsubsection ‹Auxiliary lemmas›

lemma finitC:
  "C ⊆ PR ⟹ finite C"
proof-
  assume "C ⊆ PR"
  thus ?thesis using finite_subset by auto
qed

lemma finitnpC:
  "finite (PR - C)"
proof-
  show ?thesis  using finite_Diff by auto
qed
 

text ‹The next lemmas are about arithmetic properties of the
generalized summation over a set constructor.›

lemma sum_abs_triangle_ineq:
"finite S ⟹
  ¦∑l∈S. (f::'a ⇒ 'b::linordered_idom) l¦ <= (∑l∈S. ¦f l¦)"
  (is "... ⟹ ?P S")
  by (rule sum_abs)

lemma sum_le:
  "⟦finite S ; ∀ r∈S. f r <= b ⟧
  ⟹
  (∑l∈S. f l) <= real (card S) * b"
  (is "⟦ finite S ; ∀ r∈S. f r <= b ⟧ ⟹ ?P S")
proof(induct S rule: finite_induct)
  show "?P {}" by simp 
next
  fix F x 
  assume  finit: "finite F" and xnotinF: "x ∉ F" and
          HI1: "∀r∈F. f r ≤ b ⟹ sum f F ≤ real (card F) * b"
          and HI2: "∀r∈insert x F. f r ≤ b"
  from HI1 HI2 and finit and xnotinF
  have "sum f (insert x F) <= b + real (card F) * b"
    by auto
  also 
  have "... = real (Suc (card  F)) * b"
    by (simp add: distrib_right  of_nat_Suc)
  also 
  from   finit xnotinF have "...= real (card (insert x F)) * b"
    by simp
  finally
  show "?P (insert x F)" .
qed

lemma sum_np_eq:
assumes 
  hC: "C ⊆ PR"
shows 
  "(∑l∈{..<np}. f l) = (∑l∈C. f l) + (∑l∈({..<np}-C). f l)"
proof-
  note finitC[where C=C]
  moreover
  note finitnpC[where C=C]
  moreover
  have "C ∩ ({..<np}-C) = {}" by auto
  moreover
  from hC have "C ∪ ({..<np}-C) = {..<np}" by auto
  ultimately
  show ?thesis
    using sum.union_disjoint[where A=C and B="{..<np} - C"]
    by auto
qed
 
lemma abs_sum_np_ineq:
assumes 
  hC: "C ⊆ PR"
shows 
  "¦(∑l∈{..<np}. (f::nat ⇒ real) l)¦ <=  
     (∑l∈C. ¦f l¦) + (∑l∈({..<np}-C). ¦f l¦)"
    (is "?abs_sum <= ?sumC + ?sumnpC")
proof-
  from hC and sum_np_eq[where f=f] 
  have "?abs_sum = ¦(∑l∈C. f l) + (∑l∈({..<np}-C). f l)¦" 
    (is "?abs_sum = ¦?sumC' + ?sumnpC'¦")
    by simp
  also
  from abs_triangle_ineq
  have "...<= ¦?sumC'¦ + ¦?sumnpC'¦" .
  also
  have "... <=  ?sumC + ?sumnpC "
  proof-
    from hC finitC sum_abs_triangle_ineq 
    have "¦?sumC'¦ <= ?sumC" by blast
    moreover
    from finitnpC and
           sum_abs_triangle_ineq[where f=f and S="PR-C"]  
    have "¦?sumnpC'¦ <= ?sumnpC" 
      by force
    ultimately
    show ?thesis by arith
  qed
  finally
  show ?thesis .
qed

text ‹The next lemmas are about the existence of bounds that are
necesary in order to prove the Precicion Enhancement theorem.›
  
lemma fiX_ubound:
  "fiX f p l <= f p + Δ"
proof(cases "¦f p - f l¦ ≤ Δ")
  assume asm: "¦f p - f l¦ ≤ Δ" 
  hence "fiX f p l = f l" by (simp add: fiX_def) 
  also
  from asm have "f l <= f p + Δ" by arith
  finally
  show ?thesis by arith
next
  assume asm: "¬¦f p - f l¦ ≤ Δ" 
  hence "fiX f p l = f p" by (simp add: fiX_def) 
  also
  from asm and  constants_ax have "f p <= f p + Δ" by arith
  finally
  show ?thesis by arith
qed

lemma fiX_lbound:
  "f p - Δ <= fiX f p l"
proof(cases "¦f p - f l¦ ≤ Δ")
  assume asm: "¦f p - f l¦ ≤ Δ" 
  hence "fiX f p l = f l" by (simp add: fiX_def) 
  also
  from asm have "f p - Δ <= f l" by arith
  finally
  show ?thesis by arith
next
  assume asm: "¬¦f p - f l¦ ≤ Δ" 
  with  constants_ax have "f p - Δ <= f p" by arith
  also
  from asm have "f p = fiX f p l" by (simp add: fiX_def) 
  finally
  show ?thesis by arith
qed

lemma abs_fiX_bound: "¦fiX f p l - f p ¦ <= Δ"
proof-
(*
from constants_ax and fiX_lbound and fiX_ubound show ?thesis by arith
*)
have "f p - Δ <= fiX f p l ∧ fiX f p l <= f p + Δ ⟶ ?thesis"
by arith
with fiX_lbound  fiX_ubound show ?thesis by blast
qed

lemma abs_dif_fiX_bound:
assumes
  hbx: "∀ l∈C. ¦f l - g l¦ <= x" and
  hby: "∀ l∈C. ∀ m∈C. ¦f l - f m¦ <= y" and
  hpC: "p∈C" and
  hqC: "q∈C" 
shows
  "¦fiX f p r - fiX g q r¦ <= 2 * Δ + x + y"
proof-
  have "¦fiX f p r - fiX g q r¦ = 
    ¦fiX f p r - f p + f p - fiX g q r¦ "
    by auto
  also
  have "... <= ¦fiX f p r - f p ¦ + ¦f p - fiX g q r¦ "
    by arith
  also 
  from abs_fiX_bound 
  have "... <= Δ + ¦f p - fiX g q r¦"
    by simp
  also
  have "... = Δ + ¦f p - g q + (g q - fiX g q r)¦"
    by simp
  also
  from abs_triangle_ineq[where a = "f p - g q" and 
                               b = "g q - fiX g q r"] 
  have "... <= Δ + ¦f p - g q ¦ + ¦ g q - fiX g q r¦"
    by simp
  also 
  have "... = Δ + ¦f p - g q ¦ + ¦ fiX g q r - g q¦"
    by arith
  also 
  from abs_fiX_bound
  have "... <= 2 * Δ + ¦f p - g q ¦ " 
    by simp
  also
  have "... = 2 * Δ + ¦f p - f q + (f q - g q) ¦ " 
    by simp
  also
  from abs_triangle_ineq[where a = "f p - f q" and 
                               b = "f q - g q"] 
  have "... <= 2 * Δ + ¦f p - f q ¦ + ¦ f q - g q ¦ " 
    by simp
  finally
  show ?thesis using hbx hby hpC hqC
    by force
qed
        

lemma abs_dif_fiX_bound_C_aux1:
assumes 
  hbx: "∀ l∈C. ¦f l - g l¦ <= x" and
  hby1: "∀ l∈C. ∀ m∈C. ¦f l - f m¦ <= y" and
  hby2: "∀ l∈C. ∀ m∈C. ¦g l - g m¦ <= y" and
  hpC: "p∈C" and
  hqC: "q∈C" and
  hrC: "r∈C" 
shows
  "¦fiX f p r - fiX g q r¦ <= x + y"
proof(cases "¦f p - f r¦ ≤ Δ")
  case True 
  note outer_IH = True 
  show ?thesis
  proof(cases "¦g q - g r¦ ≤ Δ")
    case True
    show ?thesis
    proof -
      from hpC and hby1 have "0<=y" by force
      with hrC and hbx have "¦ f r - g r ¦ <= x + y" by auto
      with outer_IH and True show ?thesis 
        by (auto simp add: fiX_def)
    qed
  next
    case False 
    show ?thesis
    proof -
      from outer_IH and False 
      have "¦fiX f p r - fiX g q r¦ = ¦f r - g q¦" 
        by  (auto simp add: fiX_def)
      also
      have "... = ¦ f r - f q + f q - g q ¦" by simp
      also
      have "... <= ¦ f r - f q ¦ + ¦ f q - g q ¦" 
        by arith
      also
      from hbx hby1 hpC hqC hrC have "... <= x + y" by force
      finally
      show ?thesis .
    qed
  qed
next
  case False 
  note outer_IH = False
  show ?thesis
  proof(cases "¦g q - g r¦ ≤ Δ")
    case True
    show ?thesis
    proof -
      from outer_IH and True 
      have "¦fiX f p r - fiX g q r¦ = ¦f p - g r¦" 
        by  (auto simp add: fiX_def)
      also
      have "... = ¦ f p - f r + f r - g r ¦" by simp
      also
      from abs_triangle_ineq[where a = "f p - f r" and 
                                   b = "f r - g r"]
      have "... <= ¦ f p - f r ¦ + ¦ f r - g r ¦" 
        by auto
      also
      from hbx hby1 hpC hrC have "... <= x + y" by force
      finally
      show ?thesis .
    qed
  next
    case False 
    show ?thesis
    proof -
      from outer_IH and False 
      have "¦fiX f p r - fiX g q r¦ = ¦f p - g q¦" 
        by  (auto simp add: fiX_def)
      also
      have "... = ¦ f p - f q + f q - g q ¦" by simp
      also
      from abs_triangle_ineq[where a = "f p - f q" and 
                                   b = "f q - g q"]
      have "... <= ¦ f p - f q ¦ + ¦ f q - g q ¦" 
        by auto
      also
      from hbx hby1 hpC hqC have "... <= x + y" by force
      finally
      show ?thesis .
    qed
  qed
qed

lemma abs_dif_fiX_bound_C_aux2:
assumes 
  hbx: "∀ l∈C. ¦f l - g l¦ <= x" and
  hby1: "∀ l∈C. ∀ m∈C. ¦f l - f m¦ <= y" and
  hby2: "∀ l∈C. ∀ m∈C. ¦g l - g m¦ <= y" and
  hpC: "p∈C" and
  hqC: "q∈C" and
  hrC: "r∈C" 
shows
  "y <= Δ ⟶ ¦fiX f p r - fiX g q r¦ <= x"
proof
  assume hyd: "y<=Δ"
  show "¦fiX f p r - fiX g q r¦ <= x" 
  proof-
    from hpC and hrC and hby1 and hyd have "¦f p - f r¦ ≤ Δ" 
      by force
    moreover
    from hqC and hrC and hby2 and hyd have "¦g q - g r¦ ≤ Δ"
      by force
    moreover
    from hrC and hbx have "¦ f r - g r ¦ <= x " by auto
    ultimately
    show ?thesis 
      by (auto simp add: fiX_def)
  qed
qed

lemma abs_dif_fiX_bound_C:
assumes 
  hbx: "∀ l∈C. ¦f l - g l¦ <= x" and
  hby1: "∀ l∈C. ∀ m∈C. ¦f l - f m¦ <= y" and
  hby2: "∀ l∈C. ∀ m∈C. ¦g l - g m¦ <= y" and
  hpC: "p∈C" and
  hqC: "q∈C" and
  hrC: "r∈C" 
shows
  "¦fiX f p r - fiX g q r¦ <= 
                     x + (if (y <= Δ) then 0 else y)"
proof (cases "y <= Δ")
  case True 
  with abs_dif_fiX_bound_C_aux2 and
    hbx and hby1 and hby2 and hpC and hqC and hrC 
  have "¦fiX f p r - fiX g q r¦ <= x " by blast
  with True show "?thesis" by simp
next
  case False
  with abs_dif_fiX_bound_C_aux1 and
    hbx and hby1 and hby2 and hpC and hqC and hrC 
  have "¦fiX f p r - fiX g q r¦ <= x + y" by blast
  with False show "?thesis" by simp
qed

subsubsection ‹Main theorem›

theorem prec_enh:
assumes 
  hC: "C ⊆ PR" and
  hbx: "∀ l∈C. ¦f l - g l¦ <= x" and
  hby1: "∀ l∈C. ∀ m∈C. ¦f l - f m¦ <= y" and
  hby2: "∀ l∈C. ∀ m∈C. ¦g l - g m¦ <= y" and
  hpC: "p∈C" and
  hqC: "q∈C" 
shows "¦ cfni p f - cfni q g ¦ <= 
  (real (card C) * (x + (if (y <= Δ) then 0 else y)) +
    real (card ({..<np} - C)) * (2 * Δ + x + y)) / real np"
       (is "¦ ?dif_div_np ¦ <= ?B")  
proof-
  have "¦(∑l∈{..<np}. fiX f p l ) - 
                    (∑l∈{..<np}. fiX g q l)¦ = 
    ¦(∑l∈{..<np}. fiX f p l -fiX g q l)¦"
    (is "¦?dif¦ = ¦?dif'¦" )
    by (simp add: sum_subtractf)
  also
  from abs_sum_np_ineq hC
  have " ... <=
      (∑l∈C. ¦fiX f p l - fiX g q l¦) + 
      (∑l∈({..<np}-C). ¦fiX f p l - fiX g q l¦)"
    (is " ¦?dif'¦ <= ?boundC' + ?boundnpC'" )
    by simp
  also
  have "... <= 
    real (card C) * (x + (if (y <= Δ) then 0 else y))+
    real (card ({..<np}-C)) * (2 * Δ + x + y)"
    (is " ... <= ?boundC + ?boundnpC" )
  proof-
    have " ?boundC' <= ?boundC"
    proof -
      from abs_dif_fiX_bound_C and 
        hbx and hby1 and hby2 and  hpC and hqC  
      have "∀r∈C. 
        ¦fiX f p r - fiX g q r¦ <= x + 
                         (if (y <= Δ) then 0 else y)"
        by blast     
      thus ?thesis using sum_le[where S=C] and finitC[OF hC] 
        by force
    qed
    moreover
    have "?boundnpC' <= ?boundnpC"
    proof -
      from abs_dif_fiX_bound and 
        hbx and hby1 and  hpC and hqC  
      have "∀r∈({..<np}-C). ¦fiX f p r - fiX g q r¦ <= 2 * Δ + x + y"
        by blast
      with finitnpC
      show ?thesis
        by (auto intro: sum_le)
    qed
    ultimately
    show ?thesis by arith
  qed
  finally 
  have bound: "¦?dif¦ <= ?boundC + ?boundnpC" .
  thus ?thesis
  proof-
    have "?dif_div_np = ?dif / real np"
      by (simp add: cfni_def divide_inverse algebra_simps)
    hence "¦ cfni p f - cfni q g ¦ = ¦?dif¦ / real np"
      by force
    with bound show "?thesis" 
      by (auto simp add: cfni_def divide_inverse constants_ax)
  qed
qed

subsection ‹Accuracy Preservation property›

text ‹First, a simple lemma about an arithmetic propertie of the
generalized summation over a set constructor.›

lemma sum_div_card:
"(∑l∈{..<n::nat}. f l) + q * real n= 
  (∑l∈{..<n}. f l + q )"
  (is "?Sl n = ?Sr n")
proof (induct n)
case 0 thus ?case by simp
next
case (Suc n)
thus ?case
  by (auto simp: of_nat_Suc distrib_left lessThan_Suc) 
qed

text ‹Next, some lemmas about bounds that are used in the proof of Accuracy Preservation›

lemma bound_aux_C:
assumes
  hby: "∀ l∈C. ∀ m∈C. ¦f l - f m¦ <= x" and
  hpC: "p∈C" and
  hqC: "q∈C" and
  hrC: "r∈C" 
shows
  "¦fiX f p r - f q¦ <= x"
proof (cases "¦ f p - f r ¦ <= Δ")
  case True
  then have "¦fiX f p r - f q¦ = ¦ f r - f q ¦" 
    by (simp add: fiX_def)
  also
  from hby hqC hrC have "... <= x" by blast
  finally 
  show ?thesis .
next
  case False
  then have "¦fiX f p r - f q¦ = ¦ f p - f q ¦" 
    by (simp add: fiX_def)
  also
  from hby hpC hqC have "... <= x" by blast
  finally 
  show ?thesis .
qed

lemma bound_aux:
assumes
  hby: "∀ l∈C. ∀ m∈C. ¦f l - f m¦ <= x" and
  hpC: "p∈C" and
  hqC: "q∈C" 
shows
  "¦fiX f p r - f q¦ <= x + Δ"
proof (cases "¦ f p - f r ¦ <= Δ")
  case True
  then have "¦fiX f p r - f q¦ = ¦ f r - f q ¦" 
    by (simp add: fiX_def)
  also
  have "... = ¦ (f r - f p) + (f p - f q) ¦" 
    by arith
  also
  have "... <= ¦ f p - f r ¦ + ¦ f p - f q ¦" 
    by arith
  also
  from True have "... <= Δ + ¦ f p - f q ¦" by arith
  also
  from hby hpC hqC have "... <= Δ + x" by simp
  finally 
  show ?thesis by simp
next
  case False
  then have "¦fiX f p r - f q¦ = ¦ f p - f q ¦" 
    by (simp add: fiX_def)
  also
  from hby hpC hqC have "... <= x" by blast
  finally 
  show ?thesis using constants_ax by arith
qed

subsubsection ‹Main theorem›

lemma accur_pres:
assumes 
  hC: "C ⊆ PR" and
  hby: "∀ l∈C. ∀ m∈C. ¦f l - f m¦ <= x" and
  hpC: "p∈C" and
  hqC: "q∈C" 
shows "¦ cfni p f - f q ¦ <= 
  (real (card C) * x + real (card ({..<np} - C)) * (x + Δ))/
                  real np"
  (is "?abs1 <= (?bC + ?bnpC)/real np")
proof-
from abs_sum_np_ineq and hC have 
  "¦∑l∈{..<np}. fiX f p l  - f q ¦ <= 
    (∑l∈C. ¦ fiX f p l  - f q ¦) + 
            (∑l∈({..<np}-C). ¦ fiX f p l  - f q ¦)" 
  by simp
also 
have 
  "... <= real (card C) * x + 
            real (card ({..<np} - C)) * (x + Δ)"
  proof-
    have "(∑l∈C. ¦ fiX f p l  - f q ¦) <= 
                    real (card C) * x"
    proof-
      from bound_aux_C and 
        hby and  hpC and hqC  
      have "∀r∈C. 
        ¦fiX f p r - f q¦ <= x"
        by blast     
      thus ?thesis using sum_le[where S=C] and finitC[OF hC] 
        by force
    qed
    moreover
    have " (∑l∈({..<np}-C). ¦ fiX f p l  - f q ¦) <= 
                real (card ({..<np} - C)) * (x + Δ)"
    proof -
      from bound_aux and 
        hby and  hpC and hqC  
      have "∀r∈({..<np}-C). 
        ¦fiX f p r - f q¦ <= x + Δ"
        by blast
      thus ?thesis using sum_le[where S="{..<np}-C"] 
        and finitnpC 
        by force
    qed
    ultimately
    show ?thesis by arith
  qed
  finally 
  have bound: "¦∑l∈{..<np}. fiX f p l - f q¦
  ≤ real (card C) * x + real (card ({..<np} - C)) * (x + Δ)"
    .
  thus 
    ?thesis
  proof-
    from constants_ax have
      res: "inverse (real np) * real np = 1" 
      by auto
    have
      "(cfni p f - f q) * real np = 
      (∑l∈{..<np}. fiX f p l) * real np / real np - f q * real np"
      by (simp add: cfni_def algebra_simps)
    also 
    have "... = 
      (∑l∈{..<np}. fiX f p l) - f q * real np"
      by simp
    also
    from sum_div_card[where f="fiX f p" and n=np and q="- f q"]
    have "... = (∑l∈{..<np}. fiX f p l - f q)"
      by simp
    finally
    have 
      "(cfni p f - f q) * real np = (∑l∈{..<np}. fiX f p l - f q)"
      .
― ‹cambia›
    hence
      "(cfni p f - f q) * real np / real np = 
      (∑l∈{..<np}. fiX f p l - f q)/ real np"
      by auto
    with constants_ax have  
      "(cfni p f - f q) = 
      (∑l∈{..<np}. fiX f p l - f q) / real np"
    by simp
    hence "¦ cfni p f - f q ¦ = 
      ¦(∑l∈{..<np}. fiX f p l - f q) / real np ¦"
      by simp
    also have
      "... = ¦(∑l∈{..<np}. fiX f p l - f q)¦ / real np "
      by auto
    finally have "¦ cfni p f - f q ¦ = 
      ¦(∑l∈{..<np}. fiX f p l - f q)¦ / real np "
      .
    with bound show "?thesis" 
      by (auto simp add: cfni_def divide_inverse constants_ax)
  qed
qed

end