Isabelle/Isar（その26)

　とはいえ，絶対を場合分けで処理するのはやはり面倒なので，２つ目のサブゴールの別の証明を考えましょう（ここは人間の仕事です）．

　．．．考えました．次の恒等式を用います．

lemma lem_max:
  "ALL (x::real) p q. abs (x - p) + abs (x - q)
 = max (abs(2 * x - (p + q))) (abs (p - q))" by auto

これなら?Qが直接導けます．この補題はグラフを考えれば判りますが，数学としては

lemma
  "ALL (p::real) q . abs p + abs q
 = max (abs (p + q)) (abs (p - q))" by auto

つまり，|p|+|q|=max{p+q,-(p+q),p-q,-(p-q)}=max{max{p+q,-(p+q)},max{p-q,-(p-q)}}ということです．

　ということで，後半は

  assume "?Q"
  hence "ALL x. max (abs(2 * x - (c + d))) (abs (c - d)) 
             <= max (abs(2 * x - (a + b))) (abs (a - b))"
    by auto
  thus "?P"
  using lem_max
    by simp

とすることもできます．