2013-05-15から1日間の記事一覧
Isarの証明は対話的,つまりシステムが生成するサブゴールを次の目標とするのが基本ですが,過信は禁物です.例えば lemma fixes a b :: "real" assumes "a + b = 0" shows "a < 0 | b <= 0" proof に対するOutputは proof (state): step 1goal (1 subgoal):…
Isarの証明は対話的,つまりシステムが生成するサブゴールを次の目標とするのが基本ですが,過信は禁物です.例えば lemma fixes a b :: "real" assumes "a + b = 0" shows "a < 0 | b <= 0" proof に対するOutputは proof (state): step 1goal (1 subgoal):…