Isabelle/Isar（その23）

　まず

    (is "?P <-> ?Q" is "(ALL x. ?LR x) <-> ?Q" is "(ALL x. ?L x <= ?R x) <-> ?Q1 & ?Q2")

によりマッチングを設定し，入力の反復を避けています（可読性は落ちます）．今回は，isを並べて３通り設定しました．

　次のproofコマンドにより，イニシャルプルーフとして(rule iffI)が適用されて

proof (state): step 1

goal (2 subgoals):
1. ∀x∷real. ¦x - c¦ + ¦x - d¦ ≤ ¦x - a¦ + ¦x - b¦ ⟹
a + b = c + d ∧ ¦c - d¦ ≤ ¦a - b¦
2. 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します．

  assume 0: "?P"

すると，thisが

this:
∀x∷real. ¦x - (c∷real)¦ + ¦x - (d∷real)¦ ≤ ¦x - (a∷real)¦ + ¦x - (b∷real)¦

となるので，これをfrom thisとして参照し，次の目標をhaveにより設定する為するため，from this have の短縮形 hence を用いて

  hence "?LR (max a (max b (max c d)))"

としています．この全称量化からのinstantiationはsimpやautoには無理なので，証明は述語論理のプルーバーmetisにより

    by metis

あるいは

    by (rule spec)

とし，得られた

¦max (a∷real) (max (b∷real) (max (c∷real) (d∷real))) - c¦ +
¦max a (max b (max c d)) - d¦
≤ ¦max a (max b (max c d)) - a¦ + ¦max a (max b (max c d)) - b¦

の絶対値記号はsimpでも外せますので

  hence "a + b <= c + d"
    by simp

とします．同様に，0を参照して逆向きの大小関係を導くのですが

  moreover

により，今の結果を

calculation: (a∷real) + (b∷real) ≤ (c∷real) + (d∷real)

のように蓄積します．moreoverは推移律を適用していくalsoと違い，事実をそのまま蓄積していくので，幾つかの事実をまとめて参照するのに便利です．そして

  from 0
  have "?LR (min a (min b (min c d)))"
    by metis
  hence "c + d <= a + b"
    by simp

の結果と併せるのが

  ultimately

であり

calculation:
(a∷real) + (b∷real) ≤ (c∷real) + (d∷real)
(c∷real) + (d∷real) ≤ (a∷real) + (b∷real)

となるので

  have "?Q1"
    by simp

として?Q1を得ます．