# Theory LynchInstance

Up to index of Isabelle/HOL/ClockSynchInst

theory LynchInstance
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 {* Fault-tolerant Midpoint algorithm *}theory LynchInstance imports Complex_Main begintext {* This algorithm is presented in \cite{lynch_cs}. *}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 = 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 number of lowest and highest readedvalues that the algorithm discards. The defined constants must satisfythis axiom. If not, the algorithm cannot obtain the maximum andminimum value, because it will have discarded all the values. *}axiomatization  np  :: nat  -- "Number of processes" and  khl :: nat  -- "Number of lowest and highest values" where  constants_ax: "2 * khl < np"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 Fault-tolerant Midpoint''(\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 two functions. They take a function of clockreadings and a set of processes and they return a set of @{term khl}processes which has the greater (smaller) clock readings. They weredefined with the Hilbert's $\varepsilon$-operator (the indefinitedescription operator @{text SOME} in Isabelle) because in this way theformalization is not fixed to a particular eleccion of the processes'sreadings to discards and then the modelization is more general. *}definitionkmax :: "(process => Clocktime) => process set => process set" where"kmax f P = (SOME S. S ⊆ P ∧ card S = khl ∧                 (∀ i∈S. ∀ j∈(P-S). f j <= f i))"definitionkmin :: "(process => Clocktime) => process set => process set" where"kmin f P = (SOME S. S ⊆ P ∧ card S = khl ∧                 (∀ i∈S. ∀ j∈(P-S). f i <= f j))"text {* With the previus functions we define a new one @{termreduce}\footnote{The name of this function was taken from\cite{lynch_cs}.}. This take a function of clock readings and a set ofprocesses and return de set of readings of the not dicardedprocesses. In order to define this function we use the image operator(@{term "op "}) of Isabelle.*}definitionreduce :: "(process => Clocktime) => process set => Clocktime set" where"reduce f P = f  (P - (kmax f P ∪ kmin f P))"text {* And finally the convergence function. This is defined with thebuiltin @{term Max} and @{term Min} functions of Isabelle.*}definitioncfnl :: "process  => (process => Clocktime) => Clocktime" where"cfnl p f = (Max (reduce f PR) + Min (reduce f PR)) / 2"subsection {* Translation Invariance property.*}subsubsection {* Auxiliary lemmas *}text {* These lemmas proves the existence of the maximum and minimumof the image of a set, if the set is finite and not empty. *}(* The proofs are almost the same one that those of the lemmas @{thm *)(* [source] ex_Max} and @{thm [source] ex_Min} in the Isabelle's standard *)(* theories. *)lemma ex_Maxf:fixes S and f :: "'a => ('b::linorder)"  assumes fin: "finite S"   shows "S ≠ {} ==> ∃m∈S. ∀s ∈ S. f s ≤ f m"using finproof (induct)  case empty thus ?case by simpnext  case (insert x S)  show ?case  proof (cases)    assume "S = {}" thus ?thesis by simp  next    assume nonempty: "S ≠ {}"    then obtain m where m: "m∈S" "∀s∈S. f s ≤ f m"       using insert by blast    show ?thesis    proof (cases)      assume "f x ≤ f m" thus ?thesis using m by blast    next      assume "~ f x ≤ f m" thus ?thesis using m        by(simp add:linorder_not_le order_less_le)          (blast intro: order_trans)    qed  qedqedlemma ex_Minf:fixes S and f :: "'a => ('b::linorder)"  assumes fin: "finite S"   shows "S ≠ {} ==> ∃m∈S. ∀s ∈ S. f m ≤ f s"using finproof (induct)  case empty thus ?case by simpnext  case (insert x S)  show ?case  proof (cases)    assume "S = {}" thus ?thesis by simp  next    assume nonempty: "S ≠ {}"    then obtain m where m: "m∈S" "∀s∈S. f m ≤ f s"       using insert by blast    show ?thesis    proof (cases)      assume "f m ≤ f x" thus ?thesis using m by blast    next      assume "~ f m ≤ f x" thus ?thesis using m        by(simp add:linorder_not_le order_less_le)          (blast intro: order_trans)    qed  qedqedtext {* This trivial lemma is needed by the next two. *}lemma khl_bound: "khl < np"  using constants_ax by arithtext {* The next two lemmas prove that de functions kmin and kmaxreturn some values that satisfy their definition. This is not trivialbecause we need to prove the existence of these values, according tothe rule of the Hilbert's operator. We will need this lemma manytimes because is the only thing that we know about these functions. *}lemma kmax_prop:fixes f :: "nat => Clocktime"  shows"(kmax f PR) ⊆ PR ∧ card (kmax f PR) = khl ∧                 (∀i∈(kmax f PR). ∀j∈PR - (kmax f PR). f j ≤ f i)"proof-  have "khl <= np -->     (∃ S. S ⊆ PR ∧ card S = khl ∧ (∀i∈S. ∀j∈PR - S. f j ≤ f i))"    ( is "khl <= np --> ?P khl" )  proof(induct (khl))    have "?P 0" by force    thus "0 <= np --> ?P 0" ..  next    fix n     assume asm: "n <= np --> ?P n"     show "Suc n <= np --> ?P (Suc n)"    proof      assume asm2: "Suc n <= np"      with asm have "?P n" by simp      then obtain S where        SinPR : "S⊆PR" and         cardS: "card S = n" and         HI: "(∀i∈S. ∀j∈PR - S. f j ≤ f i)"         by blast      let ?e = "SOME i. i∈PR-S ∧         (∀j∈PR-S. f j ≤ f i)"      let ?S = "insert  ?e S"      have "∃i. i∈PR-S ∧ (∀j∈PR-S. f j ≤ f i)"      proof-        from SinPR and finite_subset         have "finite (PR-S)"           by auto        moreover        from cardS and asm2 SinPR        have "S⊂PR" by auto        hence "PR-S ≠ {}" by auto        ultimately        show ?thesis using ex_Maxf by blast      qed      hence         ePRS: "?e ∈ PR-S" and maxH: "(∀j ∈ PR-S. f j ≤ f ?e)"        by (auto dest!: someI_ex)      from maxH and HI      have "(∀i∈?S. ∀j∈PR - ?S. f j ≤ f i)"        by blast      moreover      from SinPR and finite_subset       cardS and ePRS       have "card ?S = Suc n"          by (auto dest: card_insert_disjoint)      moreover      have "?S ⊆ PR" using SinPR and ePRS by auto      ultimately      show "?P (Suc n)" by blast    qed  qed  hence "?P khl" using khl_bound by auto  then obtain S where     "S≤PR ∧ card S = khl ∧ (∀i∈S. ∀j∈PR - S. f j ≤ f i)" ..    thus ?thesis by (unfold kmax_def)      (rule someI [where P="λS. S ⊆ PR ∧ card S = khl ∧ (∀i∈S. ∀j∈PR - S. f j ≤ f i)"])qedlemma kmin_prop:fixes f :: "nat => Clocktime"  shows"(kmin f PR) ⊆ PR ∧ card (kmin f PR) = khl ∧                 (∀i∈(kmin f PR). ∀j∈PR - (kmin f PR). f i ≤ f j)"proof-  have "khl <= np -->     (∃ S. S ⊆ PR ∧ card S = khl ∧ (∀i∈S. ∀j∈PR - S. f i ≤ f j))"    ( is "khl <= np --> ?P khl" )  proof(induct (khl))    have "?P 0" by force    thus "0 <= np --> ?P 0" ..  next    fix n     assume asm: "n <= np --> ?P n"     show "Suc n <= np --> ?P (Suc n)"    proof      assume asm2: "Suc n <= np"      with asm have "?P n" by simp      then obtain S where        SinPR : "S⊆PR" and         cardS: "card S = n" and         HI: "(∀i∈S. ∀j∈PR - S. f i ≤ f j)"         by blast      let ?e = "SOME i. i∈PR-S ∧         (∀j∈PR-S. f i ≤ f j)"      let ?S = "insert  ?e S"      have "∃i. i∈PR-S ∧ (∀j∈PR-S. f i ≤ f j)"      proof-        from SinPR and finite_subset         have "finite (PR-S)"           by auto        moreover        from cardS and asm2 SinPR        have "S⊂PR" by auto        hence "PR-S ≠ {}" by auto        ultimately        show ?thesis using ex_Minf by blast      qed      hence         ePRS: "?e ∈ PR-S" and minH: "(∀j ∈ PR-S. f ?e ≤ f j)"        by (auto dest!: someI_ex)      from minH and  HI       have "(∀i∈?S. ∀j∈PR - ?S. f i ≤ f j)"        by blast      moreover      from SinPR and finite_subset and        cardS and ePRS      have "card ?S = Suc n"         by (auto dest: card_insert_disjoint)      moreover      have "?S ⊆ PR" using SinPR and ePRS by auto      ultimately      show "?P (Suc n)" by blast    qed  qed  hence "?P khl" using khl_bound by auto  then obtain S where     "S≤PR ∧ card S = khl ∧ (∀i∈S. ∀j∈PR - S. f i ≤ f j)" ..    thus ?thesis by (unfold kmin_def)      (rule someI [where P="λS. S ⊆ PR ∧ card S = khl ∧ (∀i∈S. ∀j∈PR - S. f i ≤ f j)"])qedtext {* The next two lemmas are trivial from the previous ones *}lemma finite_kmax:"finite (kmax f PR)"proof-  have "finite PR" by auto  with  kmax_prop and finite_subset show ?thesis    by blastqedlemma finite_kmin:"finite (kmin f PR)"proof-  have "finite PR" by auto  with  kmin_prop and finite_subset show ?thesis    by blastqedtext {* This lemma is necesary because the definition of theconvergence function use the builtin Max and Min. *}lemma reduce_not_empty:"reduce f PR ≠ {}"proof-  from constants_ax have     "0 < (np - 2 * khl)" by arith  also  {    from kmax_prop kmin_prop     have "card (kmax f PR) = khl ∧ card (kmin f PR) = khl"       by blast    moreover    from finite_kmax and finite_kmin card_Un_Int[THEN sym]    have "card (kmax f PR ∪ kmin f PR) +       card (kmax f PR ∩ kmin f PR) =       card (kmax f PR) +  card (kmin f PR)"      by auto    ultimately    have "card (kmax f PR ∪ kmin f PR) <= 2 * khl"      by auto  }  hence     "... <= card PR - card (kmax f PR ∪ kmin f PR)"    by simp  also  {    from kmax_prop and kmin_prop have    "(kmax f PR ∪ kmin f PR) ⊆ PR" by blast  }  hence    "... = card (PR-(kmax f PR ∪ kmin f PR))"    apply (intro card_Diff_subset[THEN sym])    apply (rule finite_subset)    by auto    (* by (intro card_Diff_subset,auto) *)  finally  have "0 < card (PR-(kmax f PR ∪ kmin f PR))" .  hence "(PR-(kmax f PR ∪ kmin f PR)) ≠ {}"    by (intro notI, simp only: card_0_eq, simp)  thus ?thesis    by (auto simp add: reduce_def)qedtext {* The next three are the main lemmas necessary for prove theTranslation Invariance property.*}lemma reduce_shift:fixes f :: "nat => Clocktime"  shows  "f  (PR - (kmax f PR ∪ kmin f PR)) =             f  (PR - (kmax (λ p. f p + c) PR ∪ kmin (λ p. f p + c) PR))"apply (unfold kmin_def kmax_def)by simplemma max_shift:fixes f :: "nat => Clocktime" and Sassumes notEmpFin: "S ≠ {}" "finite S"shows"Max (fS) + x = Max ( (λ p. f p + x)  S) "proof-    from notEmpFin have "fS ≠ {}" and "(λ p. f p + x)  S ≠ {}"    by auto  with notEmpFin have    "Max (fS) ∈ f  S " "Max ((λ p. f p + x)S) ∈ (λ p. f p + x)  S "    "(∀fs ∈ (fS). fs ≤ Max (fS))"     "(∀fs ∈ ((λ p. f p + x)S). fs ≤ Max ((λ p. f p + x)S))"    by auto  thus ?thesis by forceqed  lemma min_shift:fixes f :: "nat => Clocktime" and Sassumes notEmpFin: "S ≠ {}" "finite S"shows"Min (fS) + x = Min ( (λ p. f p + x)  S) "proof-  from notEmpFin have "fS ≠ {}" and "(λ p. f p + x)  S ≠ {}"    by auto  with notEmpFin have    "Min (fS) ∈ f  S " "Min ((λ p. f p + x)S) ∈ (λ p. f p + x)  S "    "(∀fs ∈ (fS). Min (fS) <= fs)"     "(∀fs ∈ ((λ p. f p + x)S). Min ((λ p. f p + x)S) <= fs)"    by auto  thus ?thesis by forceqedsubsubsection {* Main theorem *}  theorem trans_inv: fixes f :: "nat => Clocktime"  shows"cfnl p f + x = cfnl p (λ p. f p + x)"proof-  have "cfnl p (λ p. f p + x) =       (Max (reduce (λ p. f p + x) PR) + Min (reduce (λ p. f p + x) PR)) / 2"     by (unfold cfnl_def, simp)  also  have "... =     (Max ((λ p. f p + x)               (PR - (kmax (λ p. f p + x) PR ∪ kmin (λ p. f p + x) PR))) +      Min ((λ p. f p + x)               (PR - (kmax (λ p. f p + x) PR ∪ kmin (λ p. f p + x) PR)))) / 2"    by (unfold reduce_def, simp)  also  have    "... =     (Max (f               (PR - (kmax (λ p. f p + x) PR ∪ kmin (λ p. f p + x) PR))) + x +      Min (f               (PR - (kmax (λ p. f p + x) PR ∪ kmin (λ p. f p + x) PR))) + x ) / 2"  proof-    have "finite (PR - (kmax (λ p. f p + x) PR ∪ kmin (λ p. f p + x) PR))"      by auto    moreover    from reduce_not_empty have       "PR - (kmax (λ p. f p + x) PR ∪ kmin (λ p. f p + x) PR) ≠ {}"      by (auto simp add: reduce_def)    ultimately    have       "Max ((λ p. f p + x)         (PR - (kmax (λ p. f p + x) PR ∪ kmin (λ p. f p + x) PR)))      =        Max (f               (PR - (kmax (λ p. f p + x) PR ∪ kmin (λ p. f p + x) PR))) + x"       and       "Min ((λ p. f p + x)         (PR - (kmax (λ p. f p + x) PR ∪ kmin (λ p. f p + x) PR)))      =        Min (f               (PR - (kmax (λ p. f p + x) PR ∪ kmin (λ p. f p + x) PR))) + x"      using max_shift and min_shift      by auto    thus ?thesis by auto  qed  also  from reduce_shift  have    "... =     (Max (f               (PR - (kmax f  PR ∪ kmin f PR))) + x +      Min (f               (PR - (kmax f PR ∪ kmin f PR))) + x ) / 2"    by auto  also  have "... = ((Max (reduce f PR)+ x) + (Min (reduce f PR) + x)) / 2"    by (auto simp add: reduce_def)  also  have "... = (Max (reduce f PR) + Min (reduce f PR)) / 2 + x"     by auto  finally  show ?thesis by (auto simp add: cfnl_def) qedsubsection {* Precision Enhancement property *}text {* An informal proof of this theorem can be found in \cite{miner93} *}subsubsection {* Auxiliary lemmas *}text {* This first lemma is most important for prove theproperty. This is a consecuence of the @{thm [source] card_Un_Int}lemma *}lemma pigeonhole:assumes  finitA: "finite A" and   Bss: "B ⊆ A" and Css: "C ⊆ A" and   cardH: "card A + k <= card B + card C"shows "k <= card (B ∩ C)"proof-  from Bss Css have "B ∪ C ⊆ A" by blast  with finitA have "card (B ∪ C) <= card A"    by (simp add: card_mono)  with cardH have      h: "k <= card B + card C - card (B ∪ C)"     by arith  from finitA Bss Css and finite_subset   have "finite B ∧ finite C" by auto  thus ?thesis    using card_Un_Int and h by forceqedtext {*This lemma is a trivial consecuence of the previous one. Withonly this lemma we can prove the Precision Enhancement property withthe bound $\pi(x,y) = x + y$. But this bound not satisfy the property$\pi(2\Lambda + 2 \beta\rho, \delta_S + 2\rho(r_{max}+\beta) +2\Lambda) \leq \delta_S$ that is used in \cite{shankar92mechanical} for prove theSchneider's schema. *}lemma subsets_int:assumes  finitA: "finite A" and   Bss: "B ⊆ A" and Css: "C ⊆ A" and   cardH: "card A < card B + card C"shows  "B ∩ C ≠ {}"proof-  from finitA Bss Css cardH  have "1 <= card (B ∩ C)"    by (auto intro!:  pigeonhole)  thus ?thesis by autoqedtext {* This lemma is true because @{term "reduce f PR"} is the imageof @{term "PR-(kmax f PR ∪ kmin f PR)"} by the function @{term f}. *}lemma exist_reduce:"∀ c ∈ reduce f PR. ∃ i∈ PR-(kmax f PR ∪ kmin f PR). f i = c"prooffix c assume asm: "c ∈ reduce f PR"thus "∃ i∈ PR-(kmax f PR ∪ kmin f PR). f i = c"  by (auto simp add: reduce_def kmax_def kmin_def)qedtext {* The next three lemmas are consequence of the definition of@{term reduce}, @{term kmax} and @{term kmin} *} lemma finite_reduce:"finite (reduce f PR)"proof(unfold reduce_def)  show "finite (f  (PR - (kmax f PR ∪ kmin f PR)))"    by autoqedlemma kmax_ge:  "∀ i∈ (kmax f PR). ∀ r ∈ (reduce f PR). r <= f i "proof  fix i assume asm: "i ∈ kmax f PR"  show "∀r∈reduce f PR. r ≤ f i"  proof    fix r assume asm2: "r ∈ reduce f PR"    show "r ≤ f i"    proof-      from asm2 and exist_reduce have        "∃ j ∈ PR-(kmax f PR ∪ kmin f PR). f j = r" by blast      then obtain j       where fjr:"j ∈ PR-(kmax f PR ∪ kmin f PR) ∧ f j = r"         by blast      hence "j ∈ (PR - kmax f PR)"        by blast      from this fjr asm        show ?thesis using kmax_prop        by auto    qed  qedqedlemma kmin_le:  "∀ i∈ (kmin f PR). ∀ r ∈ (reduce f PR). f i <= r "proof  fix i assume asm: "i ∈ kmin f PR"  show "∀r∈reduce f PR. f i ≤ r"  proof    fix r assume asm2: "r ∈ reduce f PR"    show "f i <= r"    proof-      from asm2 and exist_reduce have        "∃ j∈ PR-(kmax f PR ∪ kmin f PR). f j = r" by blast      then obtain j       where fjr:"j ∈ PR-(kmax f PR ∪ kmin f PR) ∧ f j = r"         by blast      hence "j ∈ (PR - kmin f PR)"        by blast      from this fjr asm        show ?thesis using kmin_prop        by auto    qed  qedqedtext {* The next lemma is used for prove the Precision Enhancementproperty. This has been proved in ICS. The proof is in the appendix\ref{sec:abs_distrib_mult}.  This cannot be prove by a simple @{textarith} or @{text auto} tactic. *}text{* This lemma is true also with @{text "0 <= c"} !! *}lemma abs_distrib_div:  "0 < (c::real)  ==> ¦a / c - b / c¦ = ¦a - b¦ / c"proof-  assume ch: "0<c"  {    fix d :: real    assume dh: "0<=d"    have "a * d - b * d = (a - b) * d "      by (auto simp add: distrib_right diff_minus)    hence "¦a * d - b * d¦ = ¦(a - b) * d¦"      by simp    also with dh have      "... = ¦a - b¦ * d"      by (simp add: abs_mult)    finally      have "¦a * d - b * d¦ = ¦a - b¦ * d"        .    (* This sublemma is solved by ICS, file: abs_distrib_mult.ics *)    (* It is not solved nor        by (auto simp add: distrib_right diff_minus)(arith)         in Isabelle  *)  }  with ch and divide_inverse show ?thesis    by (auto simp add: divide_inverse)qedtext {* The next three lemmas are about the existence of bounds of thevalues @{term "Max (reduce f PR)"} and @{term "Min (reduce f PR)"}. Theseare used in the proof of the main property. *}lemma uboundmax:assumes   hC: "C ⊆ PR" and  hCk: "np <= card C + khl"shows  "∃ i∈C. Max (reduce f PR) <= f i"proof-  from reduce_not_empty and finite_reduce   have maxrinr: "Max (reduce f PR) ∈ reduce f PR"     by simp  with exist_reduce  have "∃ i∈ PR-(kmax f PR ∪ kmin f PR). f i = Max (reduce f PR)"    by simp  then obtain pmax where     pmax_in_reduc: "pmax ∈ PR-(kmax f PR ∪ kmin f PR)" and     fpmax_ismax: "f pmax = Max (reduce f PR)" ..  hence "C ∩ insert pmax (kmax f PR)  ≠ {}"  proof-    from kmax_prop and pmax_in_reduc       and finite_kmax and hCk  have       "card PR < card C + card (insert pmax (kmax f PR))"      by simp    moreover    from pmax_in_reduc and kmax_prop    have "insert pmax (kmax f PR) ⊆ PR" by blast    moreover    note hC    ultimately    show ?thesis       using subsets_int[of PR C "insert pmax (kmax f PR)"]      by simp  qed  hence res: "∃ i∈C. i=pmax ∨ i ∈ kmax f PR" by blast  then obtain i where    iinC: "i∈C" and altern: "i=pmax ∨ i ∈ kmax f PR" ..  thus ?thesis  proof(cases "i=pmax")    case True    with iinC fpmax_ismax show ?thesis by force  next    case False    with altern maxrinr fpmax_ismax kmax_ge    have "f pmax <= f i" by simp    with iinC fpmax_ismax show ?thesis by auto   qedqed  lemma lboundmin:assumes   hC: "C ⊆ PR" and  hCk: "np <= card C + khl"shows  "∃ i∈C. f i <= Min (reduce f PR)"proof-  from reduce_not_empty and finite_reduce   have minrinr: "Min (reduce f PR) ∈ reduce f PR"     by simp  with exist_reduce  have "∃ i∈ PR-(kmax f PR ∪ kmin f PR). f i = Min (reduce f PR)"    by simp  then obtain pmin where     pmin_in_reduc: "pmin ∈ PR-(kmax f PR ∪ kmin f PR)" and     fpmin_ismin: "f pmin = Min (reduce f PR)" ..  hence "C ∩ insert pmin (kmin f PR)  ≠ {}"  proof-    from kmin_prop and pmin_in_reduc       and finite_kmin and hCk  have       "card PR < card C + card (insert pmin (kmin f PR))"      by simp    moreover    from pmin_in_reduc and kmin_prop    have "insert pmin (kmin f PR) ⊆ PR" by blast    moreover    note hC    ultimately    show ?thesis       using subsets_int[of PR C "insert pmin (kmin f PR)"]      by simp  qed  hence res: "∃ i∈C. i=pmin ∨ i ∈ kmin f PR" by blast  then obtain i where    iinC: "i∈C" and altern: "i=pmin ∨ i ∈ kmin f PR" ..  thus ?thesis  proof(cases "i=pmin")    case True    with iinC fpmin_ismin show ?thesis by force  next    case False    with altern minrinr fpmin_ismin kmin_le    have "f i <= f pmin" by simp    with iinC fpmin_ismin show ?thesis by auto   qedqed  lemma same_bound:assumes   hC: "C ⊆ PR" and  hCk: "np <= card C + khl" and  hnk: "3 * khl < np" shows  "∃ i∈C. Min (reduce f PR) <= f i ∧ g i <= Max (reduce g PR) "proof-  have b1: "khl + 1 <= card (C ∩ (PR - kmin f PR))"  proof(rule pigeonhole)    show "finite PR" by simp  next    show "C ⊆ PR" by fact  next    show "PR - kmin f PR ⊆ PR" by blast  next    show "card PR + (khl + 1) ≤ card C + card (PR - kmin f PR)"     proof-      from hnk and hCk have         "np + khl < np + card C - khl" by arith       also      from kmin_prop      have "... = np + card C - card (kmin f PR)"        by auto      also      have "... = card C + (card PR - card (kmin f PR))"      proof-        from kmin_prop have          "card (kmin f PR) <= card PR"          by (intro card_mono, auto)        thus ?thesis by (simp)      qed      also      from kmin_prop       have "... = card C +  card (PR - kmin f PR)"       proof-        from kmin_prop and finite_kmin have           "card PR - card (kmin f PR) =  card (PR - kmin f PR)"          by (intro card_Diff_subset[THEN sym])(auto)        thus ?thesis by auto      qed      finally      show ?thesis         by (simp)    qed  qed          have "C ∩ (PR - kmin f PR) ∩ (PR - kmax g PR) ≠ {}"  proof(intro subsets_int)    show "finite PR" by simp  next    show "C ∩ (PR - kmin f PR) ⊆ PR"      by blast  next    show "PR - kmax g PR ⊆ PR"       by blast  next    show "card PR <       card (C ∩ (PR - kmin f PR)) + card (PR - kmax g PR)"    proof-      from kmax_prop and finite_kmax      have "card (PR - kmax g PR)= card PR - card (kmax g PR) "         by  (intro card_Diff_subset, auto)      with kmax_prop have         "card (PR - kmax g PR) = card PR - khl" by simp      with b1      show ?thesis by arith    qed  qed  hence     "∃ i. i ∈ C ∧ i ∈ (PR - kmin f PR) ∧ i ∈ (PR - kmax g PR)"    by blast  then obtain i where     in_C: "i ∈ C" and     not_in_kmin: "i ∈ (PR - kmin f PR)" and     not_in_kmax: "i ∈ (PR - kmax g PR)" by blast  have "Min (reduce f PR) <= f i"   proof(cases "i ∈ kmax f PR")    case True    from reduce_not_empty and finite_reduce have      " Min (reduce f PR) ∈ reduce f PR" by auto    with True show ?thesis      using kmax_ge by blast  next    case False    with not_in_kmin      have "i ∈ PR - (kmax f PR ∪ kmin f PR)"       by blast    with reduce_def have "f i ∈ reduce f PR"      by auto    with reduce_not_empty and finite_reduce    show ?thesis by auto  qed  moreover  have "g i <= Max (reduce g PR)"   proof(cases "i ∈ kmin g PR")    case True    from reduce_not_empty and finite_reduce have      " Max (reduce g PR) ∈ reduce g PR" by auto    with True show ?thesis      using kmin_le by blast  next    case False    with not_in_kmax      have "i ∈ PR - (kmax g PR ∪ kmin g PR)"       by blast    with reduce_def have "g i ∈ reduce g PR"      by auto    with reduce_not_empty and finite_reduce    show ?thesis by auto  qed  moreover  note in_C  ultimately  show ?thesis by blastqedsubsubsection {* Main theorem *}text {* The most part of this theorem can be proved with CVC-liteusing the three previous lemmas (appendix \ref{sec:bound_prec_enh}).*}theorem prec_enh:assumes   hC: "C ⊆ PR" and  hCF: "np - nF <= card C" and  hFn: "3 * nF < np" and  hFk: "nF = khl" 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 "¦ cfnl p f - cfnl q g ¦ <= y / 2 + x"proof-  from hCF and hFk   have hCk: "np <= card C + khl" by arith  from hFn and hFk   have hnk: "3 * khl < np"  by arith  let    ?maxf = "Max (reduce f PR)"     and  ?minf = "Min (reduce f PR)"    and  ?maxg = "Max (reduce g PR)"     and  ?ming = "Min (reduce g PR)"  from abs_distrib_div  have "¦cfnl p f - cfnl q g¦ =     ¦?maxf + ?minf  +  - ?maxg + - ?ming¦ / 2"    by (unfold cfnl_def, auto simp add: diff_minus)  moreover  have "¦?maxf + ?minf  +  - ?maxg + - ?ming¦ <= y + 2 * x"    -- {* The rest of the property can be proved by CVC-lite           (see appendix \ref{sec:bound_prec_enh}) *}  proof ( cases "0 <= ?maxf + ?minf  +  - ?maxg + - ?ming")    case True    hence    "¦?maxf + ?minf  +  - ?maxg + - ?ming¦ =       ?maxf + ?minf  +  - ?maxg + - ?ming" by arith    moreover    from uboundmax hC hCk     obtain mxf      where mxfinC: "mxf∈C" and             maxf: "?maxf <= f mxf" by blast    moreover    from lboundmin hC hCk     obtain mng       where mnginC: "mng∈C" and             ming: "g mng <= ?ming" by blast        moreover    from same_bound hC hCk hnk      obtain mxn       where mxninC: "mxn∈C" and             mxnf: "?minf  ≤ f mxn" and            mxng: "g mxn ≤ ?maxg" by blast    ultimately    have       "¦ ?maxf + ?minf  +  - ?maxg + - ?ming¦ <=       (f mxf + - g mng) + (f mxn  +  - g mxn)" by arith    also     from  mxninC hbx abs_le_D1    have      "... <= (f mxf + - g mng) + x"      by (auto simp add: diff_minus)    also    have       "... = (f mxf + - f mng ) + ( f mng + - g mng) + x"      by arith    also    have "... <= y + ( f mng + - g mng) + x"    proof-      from  mxfinC mnginC hby1 abs_le_D1      have "f mxf + - f mng <= y"         by (auto simp add: diff_minus)      thus ?thesis        by (auto simp add: diff_minus)    qed    also    from  mnginC hbx abs_le_D1    have "... <= y + 2 * x"      by (auto simp add: diff_minus)    finally     show ?thesis .  next    case False    hence    "¦?maxf + ?minf  +  - ?maxg + - ?ming¦ =       ?maxg + ?ming  +  - ?maxf + - ?minf" by arith    moreover    from uboundmax hC hCk     obtain mxg       where mxginC: "mxg∈C" and             maxg: "?maxg <= g mxg" by blast    moreover    from lboundmin hC hCk     obtain mnf       where mnfinC: "mnf∈C" and             minf: "f mnf <= ?minf" by blast        moreover    from same_bound hC hCk hnk      obtain mxn       where mxninC: "mxn∈C" and             mxnf: "?ming  ≤ g mxn" and            mxng: "f mxn ≤ ?maxf" by blast    ultimately    have       "¦ ?maxf + ?minf  +  - ?maxg + - ?ming¦ <=       (g mxg + - f mnf) + (g mxn  +  - f mxn)" by arith    also    from  mxninC hbx     have "... <= (g mxg + - f mnf) + x"        by (auto dest!: abs_le_D2)    also    have       "... = (g mxg + - g mnf ) + ( g mnf + - f mnf) + x"      by arith    also    have "... <= y + ( g mnf + - f mnf) + x"    proof-      from  mxginC mnfinC hby2 abs_le_D1      have "g mxg + - g mnf <= y"         by (auto simp add: diff_minus)      thus ?thesis        by (auto simp add: diff_minus)    qed    also    from  mnfinC hbx    have "... <= y + 2 * x"      by (auto dest!: abs_le_D2)    finally     show ?thesis .  qed  ultimately  show ?thesis    by simpqedsubsection {* Accuracy Preservation property *}text {* No new lemmas are needed for prove this property. The boundhas been found using the lemmas @{thm [source] uboundmax} and @{thm[source] lboundmin} *}text {* This theorem can be proved with ICS and CVC-lite assumingthose lemmas (see appendix \ref{sec:accur_pres}).  *}theorem accur_pres:assumes  hC: "C ⊆ PR" and  hCF: "np - nF <= card C" and  hFk: "nF = khl" and  hby: "∀ l∈C. ∀ m∈C. ¦f l - f m¦ <= y" and  hqC: "q∈C" shows "¦ cfnl p f - f q ¦ <= y"proof-  from hCF and hFk   have npleCk: "np <= card C + khl" by arith  show ?thesis  proof(cases "f q <= cfnl p f")    case True    from npleCk hC and  uboundmax     have "∃ i∈C. Max (reduce f PR) <= f i"      by auto    then obtain pi where       hpiC: "pi ∈ C" and       fpiGeMax: "Max (reduce f PR) <= f pi" by blast    from reduce_not_empty     have "Min (reduce f PR) <= Max (reduce f PR)"      by (auto simp add: reduce_def)    with fpiGeMax have      cfnlLefpi: "cfnl p f <= f pi"      by (auto simp add: cfnl_def)    with True have       "¦ cfnl p f - f q ¦ <= ¦ f pi - f q ¦"      by arith    with hpiC and hqC and hby show ?thesis       by force  next    case False    from npleCk hC and lboundmin     have "∃ i∈C. f i <= Min (reduce f PR)"      by auto    then obtain qi where       hqiC: "qi ∈ C" and       fqiLeMax: "f qi <= Min (reduce f PR)" by blast    from reduce_not_empty     have "Min (reduce f PR) <= Max (reduce f PR)"      by (auto simp add: reduce_def)    with fqiLeMax     have "f qi <= cfnl p f"      by (auto simp add: cfnl_def)    with False have       "¦ cfnl p f - f q ¦ <= ¦ f qi - f q ¦"      by arith    with hqiC and hqC and hby show ?thesis       by force  qedqedend`