caeruiro https://blog.hatena.ne.jp/caeruiro/ caeruiro https://caeruiro.hatenadiary.org/ Isabelle 5.15 Forward Proof: Transforming Theorems ここまでは後ろ向きの証明を扱ってきましたが、前向きに証明を行うこともできます。前向きの証明は、一般的な定理から固有の定理を導くのに便利です。例えば最大公約数の分配法則を考えます。 k * gcd(m, n) = gcd(k * m, k * n) m = 1とすると次の新しい定理が得られます。 k = gcd(k, k * n) この新しい定理は左右を入れ替えると、単純化ルールとして便利そうです。左右を入れ替え、さらにn = 1とするとまた新たな定理が得られます。 gcd(k, k) = k 変数への値の代入が… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fcaeruiro.hatenadiary.org%2Fentry%2F20100415%2F1271340648" title="Isabelle Tutorial その14 - caeruiro" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2010-04-15 23:10:48 rich https://caeruiro.hatenadiary.org/entry/20100415/1271340648 1.0 100%