次は逆です． next とすれば proof (state): step 26goal (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のブロッ…

この?Q1を今から導く?Q2と併せて?Qとするので moreover により calculation: (a∷real) + (b∷real) = (c∷real) + (d∷real) のように蓄積し，また，thisとして0と併せて直ちに利用します． with 0 have "?L ((c + d) / 2) <= ?R ((a + b) / 2)" by metis このw…

まず (is "?P <-> ?Q" is "(ALL x. ?LR x) <-> ?Q" is "(ALL x. ?L x <= ?R x) <-> ?Q1 & ?Q2") によりマッチングを設定し，入力の反復を避けています（可読性は落ちます）．今回は，isを並べて３通り設定しました． 次のproofコマンドにより，イニシャルプ…

では，次の例として 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}…