Theory ICAInstance

Up to index of Isabelle/HOL/ClockSynchInst

theory ICAInstance
imports Complex_Main
`(*  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>*)header {* Interactive Convergence Algorithms (ICA) *}theory ICAInstance imports Complex_Main begintext {* 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 wereobtained 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 andthe real time and the clock readings are reals. *}type_synonym process = nattype_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 theprocesses whose clocks differ more than this amount from the own one(see \cite{shankar92mechanical}). The defined constants must satisfythis axiom (if \$np = 0\$ we have a division by cero in the definitionof 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 algorithmmanage. This definition exist only for readability matters. *}definitionPR :: "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 theclocks readings from the others processes (including itself). Weformalise that as a function from processes to clock time as\cite{shankar92mechanical}. *}text {* First we define an auxiliary function. It takes a function ofclock readings and two processes, and return de reading of the secondprocess 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 thebuiltin generalized summation over a set constructor of Isabelle.Also we had to use the overloaded @{term real} function to typecast denumber @{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 real_of_nat_Suc        distrib_right diff_minus lessThan_Suc)donetheorem 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)donesubsection {* 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 autoqedlemma finitnpC:  "finite (PR - C)"proof-  show ?thesis  using finite_Diff by autoqed text {* The next lemmas are about arithmetic properties of thegeneralized 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 setsum_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 ==> setsum f F ≤ real (card F) * b"          and HI2: "∀r∈insert x F. f r ≤ b"  from HI1 HI2 and finit and xnotinF  have "setsum f (insert x F) <= b + real (card F) * b"    by auto  also   have "... = real (Suc (card  F)) * b"    by (simp add: distrib_right  real_of_nat_Suc)  also   from   finit xnotinF have "...= real (card (insert x F)) * b"    by simp  finally  show "?P (insert x F)" .qedlemma 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 setsum_Un_disjoint[where A=C and B="{..<np} - C"]    by autoqed 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 .qedtext {* The next lemmas are about the existence of bounds that arenecesary 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 arithnext  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 arithqedlemma 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 arithnext  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 arithqedlemma 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 arithwith fiX_lbound  fiX_ubound show ?thesis by blastqedlemma 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 add: diff_minus)  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 add: diff_minus)  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 forceqed        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  qednext  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 simp add: diff_minus)      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 simp add: diff_minus)      also      from hbx hby1 hpC hqC have "... <= x + y" by force      finally      show ?thesis .    qed  qedqedlemma 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)  qedqedlemma 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 simpnext  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 simpqedsubsubsection {* 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: diff_minus setsum_addf setsum_negf)  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 (auto simp add:  cfni_def distrib_right         divide_inverse diff_minus)    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)  qedqedsubsection {* Accuracy Preservation property *}text {* First, a simple lemma about an arithmetic propertie of thegeneralized 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 simpnextcase (Suc n)thus ?case  by (auto simp: real_of_nat_Suc distrib_left lessThan_Suc) qedtext {* 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 .qedlemma 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 simpnext  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 arithqedsubsubsection {* 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 simpalso 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 (auto simp add:  cfni_def  diff_minus distrib_right)    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 (auto simp add:  diff_minus)    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)  qedqedend`