2010-04-15から1日間の記事一覧

Isabelle Tutorial その14

5.15 Forward Proof: Transforming Theorems ここまでは後ろ向きの証明を扱ってきましたが、前向きに証明を行うこともできます。前向きの証明は、一般的な定理から固有の定理を導くのに便利です。例えば最大公約数の分配法則を考えます。 k * gcd(m, n) = gc…