Isabelle/Isar（その25）

　次は逆です．

next

とすれば

proof (state): step 26

goal (1 subgoal):
1. a + b = c + d ∧ ¦c - d¦ ≤ ¦a - b¦ ⟹
∀x∷real. ¦x - c¦ + ¦x - d¦ ≤ ¦x - a¦ + ¦x - b¦
variables:
a, b, c, d :: real

なので

  assume 0: "?Q"

とします．nextによりproofのブロックが移り，前半の名前はリセットされています．また，場合分けの境界に名前を与えておきます．

  let ?A = "min a b" and ?C = "min c d" and ?D = "max c d" and ?B = "max a b"

今回は場合分けなので直接

  show "?P"
  proof

とします．proofによりメタの全称量化に書き換わりましたので，入力も

    fix x

とし，任意の実数xを固定します．

　すると，そのxは先述の５つの区間の何れかに属することは，autoでも解り

    have "x <= ?A | ?A < x & x <= ?C | ?C < x & x <= ?D | ?D < x & x <= ?B | ?B < x"
      by auto

このことをmoreoverにより

calculation:
x ≤ min a b ∨
min a b < x ∧ x ≤ min c d ∨
min c d < x ∧ x ≤ max c d ∨ max c d < x ∧ x ≤ max a b ∨ max a b < x

として蓄積，各場合について ?LR x となることを

    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

のように 0 を参照して証明させて，ultimatelyにより

calculation:
x ≤ min a b ∨
min a b < x ∧ x ≤ min c d ∨
min c d < x ∧ x ≤ max c d ∨ max c d < x ∧ x ≤ max a b ∨ max a b < x
x ≤ min a b ⟶ ¦x - c¦ + ¦x - d¦ ≤ ¦x - a¦ + ¦x - b¦
min a b < x ∧ x ≤ min c d ⟶ ¦x - c¦ + ¦x - d¦ ≤ ¦x - a¦ + ¦x - b¦
min c d < x ∧ x ≤ max c d ⟶ ¦x - c¦ + ¦x - d¦ ≤ ¦x - a¦ + ¦x - b¦
max c d < x ∧ x ≤ max a b ⟶ ¦x - c¦ + ¦x - d¦ ≤ ¦x - a¦ + ¦x - b¦
max a b < x ⟶ ¦x - c¦ + ¦x - d¦ ≤ ¦x - a¦ + ¦x - b¦

とまとめれば，後はロジックなので

    show "?LR x"
      by metis
  qed

で

Successful attempt to solve goal by exported rule:
(a + b = c + d ∧ ¦c - d¦ ≤ ¦a - b¦) ⟹ ∀x. ¦x - c¦ + ¦x - d¦ ≤ ¦x - a¦ + ¦x - b¦

となり，２つ目のサブゴールも消えて，qedで証明完成です．

　５つの場合の絶対値記号を外す処理は多少もたつきますが，autoは頑張っていると思います．