Isabelle/Isar（その22）

　では，次の例として

lemma
  fixes a b c d :: "real"
  shows "(ALL x. abs (x - c) + abs (x - d) <= abs (x - a) + abs(x - b))
     <-> (a + b = c + d & abs (c - d) <= abs (a - b))"

を取り上げます．

　普通の証明は，２つの含意に分けて，xとしてmax{a,b,c,d}を用いて-c-d≦-a-bつまりa+b≦c+d，xとしてmin{a,b,c,d}を用いてc+d≦a+b，従って，a+b=c+d．このとき(c+d)/2=(a+b)/2なので，それぞれを左辺，右辺のxとして用いて|c-d|≦|a-b|．逆はa+b=c+dならばmin{c,d},max{c,d},はmin{a,b},max{a,b}に挟まれるので，それらを境界として実数全体の集合を５つに分け，xが何れに属すかに応じて絶対値記号を外す．といったものでしょう．

　Isarで，この通りに書いてみます．

lemma
  fixes a b c d :: "real"
  shows "(ALL x. abs (x - c) + abs (x - d) <= abs (x - a) + abs(x - b))
         <-> (a + b = c + d & abs (c - d) <= abs (a - b))"
    (is "?P <-> ?Q" is "(ALL x. ?LR x) <-> ?Q" is "(ALL x. ?L x <= ?R x) <-> ?Q1 & ?Q2")
proof
  assume 0: "?P"
  hence "?LR (max a (max b (max c d)))"
    by metis
  hence "a + b <= c + d"
    by simp
  moreover
  from 0
  have "?LR (min a (min b (min c d)))"
    by metis
  hence "c + d <= a + b"
    by simp
  ultimately
  have "?Q1"
    by simp
  moreover
  with 0
  have "?L ((c + d) / 2) <= ?R ((a + b) / 2)"
    by metis
  with lem_abs have "?Q2"
    by simp
  ultimately
  show "?Q"
    by simp
next
  assume 0: "?Q"
  let ?A = "min a b" and ?C = "min c d" and ?D = "max c d" and ?B = "max a b"
  show "?P"
  proof
    fix x
    have "x <= ?A | ?A < x & x <= ?C | ?C < x & x <= ?D | ?D < x & x <= ?B | ?B < x"
      by auto
    moreover
    from 0
    have "x <= ?A --> ?LR x" and
         "?A < x & x <= ?C --> ?LR x" and
         "?C < x & x <= ?D --> ?LR x" and
         "?D < x & x <= ?B --> ?LR x" and
         "?B < x --> ?LR x"
      by auto
    ultimately
    show "?LR x"
      by metis
  qed
qed

　ご覧通りですが，かなり新しい項目がありますので，説明していきましょう．