Isabelle/Isar（その24）

　この?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

このwith 0はfrom 0 and thisの略です．辺々に代入するものが等しいことは0からの帰結で，やはりmetisを用います．得られた

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

の個々の変形はsimpでも賄えるので，先に

lemma lem_abs:
  "abs ((x + y) / 2 - (x::real)) = abs (x - y) / 2"
    by simp  

を用意し，それも参照して?Q2となります．

  with lem_abs
  have "?Q2"
    by simp

これと先の?Q1とを

  ultimately

により併せて?Qを得る訳ですが，本来?Qはそれらの連言なので　.　つまりby thisでは無理で　..　つまりby (rule conjI)あるいはby ruleが入用のところを，この程度のロジック（というかマッチング）はsimpにも解るのでby simpとしています．

  show "?Q"
    by simp

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