Quellcode-Bibliothek isar.thy   Sprache: Isabelle

{* -----------------------------
  Output for Isabelle from binsearch.cob
  Date=3.5.2011 10:54:54:40
  ------------------------------- *}

def k::int
def u::int
def m::int
def @t::int
def n::int
def v::int
def ret::int

lemma "k+((-5*k)+(5*u)) = (-5*k)+((5*u)+k)"
proof -
  have         "u-k = (-1*k)+u"
  also have    "5*(-1*k) = -5*k"
  also have    "5*((-1*k)+u) = (-5*k)+(5*u)"
  also have    "((-1*k)+u)/2 = (-5*k)+(5*u)"
  finally      "k+((-5*k)+(5*u)) = (-5*k)+((5*u)+k)"
qed

lemma "¬1 = 0"
proof -
  have         "u-k = (-1*k)+u"
  also have    "5*(-1*k) = -5*k"
  also have    "5*((-1*k)+u) = (-5*k)+(5*u)"
  also have    "((-1*k)+u)/2 = (-5*k)+(5*u)"
  finally      "¬1 = 0"
qed

lemma "(-5*k)+(k+(5*u)) = (-5*k)+((5*u)+k)"
proof -
  have         "5*1 = 5"
  also have    "(5*u)+k = k+(5*u)"
  finally      "(-5*k)+(k+(5*u)) = (-5*k)+((5*u)+k)"
qed

lemma "(-5*k)+(k+(5*u)) = (-5*k)+((5*u)+k)"
proof -
  have         "5*1 = 5"
  also have    "(5*u)+k = k+(5*u)"
  finally      "(-5*k)+(k+(5*u)) = (-5*k)+((5*u)+k)"
qed

lemma "((-5*k)+((5*u)+k))-1 = (-4*k)+((5*u)+-1)"
proof -
  have         "5*1 = 5"
  also have    "(5*u)+k = k+(5*u)"
  also have    "(-5*k)+(k+(5*u)) = (-5*k)+((5*u)+k)"
  also have    "-5*1 = -5"
  also have    "-5+1 = -4"
  finally      "((-5*k)+((5*u)+k))-1 = (-4*k)+((5*u)+-1)"
qed

lemma "(-5*k)+(k+(5*u)) = (-5*k)+((5*u)+k)"
proof -
  have         "5*1 = 5"
  also have    "(5*u)+k = k+(5*u)"
  finally      "(-5*k)+(k+(5*u)) = (-5*k)+((5*u)+k)"
qed

lemma "(-5*k)+(k+(5*u)) = (-5*k)+((5*u)+k)"
proof -
  have         "5*1 = 5"
  also have    "(5*u)+k = k+(5*u)"
  finally      "(-5*k)+(k+(5*u)) = (-5*k)+((5*u)+k)"
qed

lemma "(-5*k)+((5*u)+k) = (-4*k)+(5*u)"
proof -
  have         "k+(5*u) = (5*u)+k"
  also have    "-5*1 = -5"
  also have    "-5+1 = -4"
  finally      "(-5*k)+((5*u)+k) = (-4*k)+(5*u)"
qed

lemma "¬1 = 0"
proof -
  have         "k+(5*u) = (5*u)+k"
  also have    "-5*1 = -5"
  also have    "-5+1 = -4"
  finally      "¬1 = 0"
qed

lemma "(-5*k)+(k+(5*u)) = (-5*k)+((5*u)+k)"
proof -
  have         "5*1 = 5"
  also have    "(5*u)+k = k+(5*u)"
  finally      "(-5*k)+(k+(5*u)) = (-5*k)+((5*u)+k)"
qed

lemma "(-5*k)+(k+(5*u)) = (-5*k)+((5*u)+k)"
proof -
  have         "5*1 = 5"
  also have    "(5*u)+k = k+(5*u)"
  finally      "(-5*k)+(k+(5*u)) = (-5*k)+((5*u)+k)"
qed

lemma "(-4**$42)*((5*u)+1) = (5*((-4**$42)*u))+(-4**$42)"
proof -
  have         "1*1 = 1"
  also have    "(-4**$42)*(5*u) = 5*((-4**$42)*u)"
  also have    "(-4**$42)*1 = -4**$42"
  finally      "(-4**$42)*((5*u)+1) = (5*((-4**$42)*u))+(-4**$42)"
qed

lemma "k+(((-4**$41)*k)+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42))) = ((-4**$41)*k)+(k+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42)))"
proof -
  have         "1*1 = 1"
  also have    "1-$41 = (-1*$41)+1"
  also have    "-1*1 = -1"
  also have    "1>$41 = ((-1*$41)+1)>0"
  finally      "k+(((-4**$41)*k)+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42))) = ((-4**$41)*k)+(k+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42)))"
qed

lemma "\$41: k = ((-4**$41)*k)+(k+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42)))"
proof -
  have         "k::int"
  also have    "$41::nat"
  finally      "\$41: k = ((-4**$41)*k)+(k+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42)))"
qed

lemma "((-4*((-4**$41)*k))+((-4*k)+(-4*Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42)))))+(5*u) = (-4*((-4**$41)*k))+((-4*k)+((5*u)+(-4*Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42)))))"
proof -
  have         "1*1 = 1"
  also have    "1-$41 = (-1*$41)+1"
  also have    "-1*1 = -1"
  also have    "1>$41 = ((-1*$41)+1)>0"
  also have    "1*1 = 1"
  also have    "1-$41 = (-1*$41)+1"
  also have    "-1*1 = -1"
  also have    "1>$41 = ((-1*$41)+1)>0"
  also have    "1*1 = 1"
  also have    "1*1 = 1"
  also have    "1-$41 = (-1*$41)+1"
  also have    "-1*1 = -1"
  also have    "1>$41 = ((-1*$41)+1)>0"
  also have    "-4*(((-4**$41)*k)+(k+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42)))) = (-4*((-4**$41)*k))+((-4*k)+(-4*Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42))))"
  finally      "((-4*((-4**$41)*k))+((-4*k)+(-4*Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42)))))+(5*u) = (-4*((-4**$41)*k))+((-4*k)+((5*u)+(-4*Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42)))))"
qed

lemma "(((((-4**$41)*k)+(k+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42))))-u)>0)|((@t[@t:1]-v)>=0) = ((((-4**$41)*k)+(k+((-1*u)+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42)))))>0)|((@t[@t:1]-v)>=0)"
proof -
  have         "1*1 = 1"
  also have    "1-$41 = (-1*$41)+1"
  also have    "-1*1 = -1"
  also have    "1>$41 = ((-1*$41)+1)>0"
  also have    "(((-4**$41)*k)+(k+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42))))-u = ((-4**$41)*k)+(k+((-1*u)+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42))))"
  also have    "1*1 = 1"
  also have    "1-$41 = (-1*$41)+1"
  also have    "-1*1 = -1"
  also have    "1>$41 = ((-1*$41)+1)>0"
  also have    "k+((-1*u)+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42))) = (-1*u)+(k+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42)))"
  also have    "((-4**$41)*k)+((-1*u)+(k+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42)))) = ((-4**$41)*k)+(k+((-1*u)+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42))))"
  finally      "(((((-4**$41)*k)+(k+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42))))-u)>0)|((@t[@t:1]-v)>=0) = ((((-4**$41)*k)+(k+((-1*u)+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42)))))>0)|((@t[@t:1]-v)>=0)"
qed

lemma "\ {"k::int","u::int","$42::nat","@t::int","m::int","v::int"}.\ "$41::nat".(((((-4**$41)*k)+(k+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42))))-u)>0)|((@t[@t:1]-v)>=0)"
proof -
     "\ $41.\ "
qed

lemma "(((((-4**$41)*k)+(k+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42))))-u)>0)|((@t[@t:1]-v)>=0) = ((((-4**$41)*k)+(k+((-1*u)+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42)))))>0)|((@t[@t:1]-v)>=0)"
proof -
  have         "1*1 = 1"
  also have    "1-$41 = (-1*$41)+1"
  also have    "-1*1 = -1"
  also have    "1>$41 = ((-1*$41)+1)>0"
  also have    "(((-4**$41)*k)+(k+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42))))-u = ((-4**$41)*k)+(k+((-1*u)+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42))))"
  also have    "1*1 = 1"
  also have    "1-$41 = (-1*$41)+1"
  also have    "-1*1 = -1"
  also have    "1>$41 = ((-1*$41)+1)>0"
  also have    "k+((-1*u)+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42))) = (-1*u)+(k+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42)))"
  also have    "((-4**$41)*k)+((-1*u)+(k+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42)))) = ((-4**$41)*k)+(k+((-1*u)+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42))))"
  finally      "(((((-4**$41)*k)+(k+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42))))-u)>0)|((@t[@t:1]-v)>=0) = ((((-4**$41)*k)+(k+((-1*u)+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42)))))>0)|((@t[@t:1]-v)>=0)"
qed

lemma "\ {"k::int","u::int","$42::nat","@t::int","m::int","v::int"}.\ "$41::nat".(((((-4**$41)*k)+(k+Sum($42,1,$41,(5*((-4**$42)*u))+(-4**$42))))-u)>0)|((@t[@t:1]-v)>=0)"
proof -
     "\ $41.\ "
qed

lemma "(5**$50)*((4*k)+1) = (4*((5**$50)*k))+(5**$50)"
proof -
  have         "1-(-4*k) = (4*k)+1"
  also have    "1*1 = 1"
  also have    "(5**$50)*(4*k) = 4*((5**$50)*k)"
  also have    "(5**$50)*1 = 5**$50"
  finally      "(5**$50)*((4*k)+1) = (4*((5**$50)*k))+(5**$50)"
qed

lemma "u-(((5**$49)*u)+Sum($50,1,$49,(4*((5**$50)*k))+(5**$50))) = (-1*((5**$49)*u))+(u-Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))"
proof -
  have         "1*1 = 1"
  also have    "1-$49 = (-1*$49)+1"
  also have    "-1*1 = -1"
  also have    "1>$49 = ((-1*$49)+1)>0"
  also have    "1*1 = 1"
  finally      "u-(((5**$49)*u)+Sum($50,1,$49,(4*((5**$50)*k))+(5**$50))) = (-1*((5**$49)*u))+(u-Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))"
qed

lemma "\$49: u = (-1*((5**$49)*u))+(u-Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))"
proof -
  have         "u::int"
  also have    "$49::nat"
  finally      "\$49: u = (-1*((5**$49)*u))+(u-Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))"
qed

lemma "(-5*k)+((-5*((5**$49)*u))+(k+((5*u)+(-5*Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))))) = (-5*((5**$49)*u))+((-4*k)+((5*u)+(-5*Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))))"
proof -
  have         "1*1 = 1"
  also have    "1*1 = 1"
  also have    "1-$49 = (-1*$49)+1"
  also have    "-1*1 = -1"
  also have    "1>$49 = ((-1*$49)+1)>0"
  also have    "1*1 = 1"
  also have    "1-$49 = (-1*$49)+1"
  also have    "-1*1 = -1"
  also have    "1>$49 = ((-1*$49)+1)>0"
  also have    "1*1 = 1"
  also have    "1*1 = 1"
  also have    "5*(-1*((5**$49)*u)) = -5*((5**$49)*u)"
  also have    "1*1 = 1"
  also have    "1-$49 = (-1*$49)+1"
  also have    "-1*1 = -1"
  also have    "1>$49 = ((-1*$49)+1)>0"
  also have    "5*((-1*((5**$49)*u))+(u-Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))) = (-5*((5**$49)*u))+((5*u)-(5*Sum($50,1,$49,(4*((5**$50)*k))+(5**$50))))"
  also have    "1*1 = 1"
  also have    "1-$49 = (-1*$49)+1"
  also have    "-1*1 = -1"
  also have    "1>$49 = ((-1*$49)+1)>0"
  also have    "((-5*((5**$49)*u))+((5*u)-(5*Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))))+k = (-5*((5**$49)*u))+(k+((5*u)+(-5*Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))))"
  also have    "-5*1 = -5"
  also have    "-5+1 = -4"
  finally      "(-5*k)+((-5*((5**$49)*u))+(k+((5*u)+(-5*Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))))) = (-5*((5**$49)*u))+((-4*k)+((5*u)+(-5*Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))))"
qed

lemma "((k-((-1*((5**$49)*u))+(u-Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))))>0)|(((@t[@t:1]-v)<0)|((@t[@t:1]-v)<=0)) = ((((5**$49)*u)+(k-(u-Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))))>0)|(((@t[@t:1]-v)<0)|((@t[@t:1]-v)<=0))"
proof -
  have         "1*1 = 1"
  also have    "1*1 = 1"
  also have    "1-$49 = (-1*$49)+1"
  also have    "-1*1 = -1"
  also have    "1>$49 = ((-1*$49)+1)>0"
  also have    "k-((-1*((5**$49)*u))+(u-Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))) = ((5**$49)*u)+(k-(u-Sum($50,1,$49,(4*((5**$50)*k))+(5**$50))))"
  also have    "1*1 = 1"
  also have    "1-$49 = (-1*$49)+1"
  also have    "-1*1 = -1"
  also have    "1>$49 = ((-1*$49)+1)>0"
  finally      "((k-((-1*((5**$49)*u))+(u-Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))))>0)|(((@t[@t:1]-v)<0)|((@t[@t:1]-v)<=0)) = ((((5**$49)*u)+(k-(u-Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))))>0)|(((@t[@t:1]-v)<0)|((@t[@t:1]-v)<=0))"
qed

lemma "\ {"u::int","k::int","$50::nat","@t::int","m::int","v::int"}.\ "$49::nat".((k-((-1*((5**$49)*u))+(u-Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))))>0)|(((@t[@t:1]-v)<0)|((@t[@t:1]-v)<=0))"
proof -
     "\ $49.\ "
qed

lemma "((k-((-1*((5**$49)*u))+(u-Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))))>0)|(((@t[@t:1]-v)<0)|((@t[@t:1]-v)<=0)) = ((((5**$49)*u)+(k-(u-Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))))>0)|(((@t[@t:1]-v)<0)|((@t[@t:1]-v)<=0))"
proof -
  have         "1*1 = 1"
  also have    "1*1 = 1"
  also have    "1-$49 = (-1*$49)+1"
  also have    "-1*1 = -1"
  also have    "1>$49 = ((-1*$49)+1)>0"
  also have    "k-((-1*((5**$49)*u))+(u-Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))) = ((5**$49)*u)+(k-(u-Sum($50,1,$49,(4*((5**$50)*k))+(5**$50))))"
  also have    "1*1 = 1"
  also have    "1-$49 = (-1*$49)+1"
  also have    "-1*1 = -1"
  also have    "1>$49 = ((-1*$49)+1)>0"
  finally      "((k-((-1*((5**$49)*u))+(u-Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))))>0)|(((@t[@t:1]-v)<0)|((@t[@t:1]-v)<=0)) = ((((5**$49)*u)+(k-(u-Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))))>0)|(((@t[@t:1]-v)<0)|((@t[@t:1]-v)<=0))"
qed

lemma "\ {"u::int","k::int","$50::nat","@t::int","m::int","v::int"}.\ "$49::nat".((k-((-1*((5**$49)*u))+(u-Sum($50,1,$49,(4*((5**$50)*k))+(5**$50)))))>0)|(((@t[@t:1]-v)<0)|((@t[@t:1]-v)<=0))"
proof -
     "\ $49.\ "
qed

{* ------------------------------------
  End of output from binsearch.cob
  Date=3.5.2011 10:54:54:40
  -------------------------------------- *}