caeruiro https://blog.hatena.ne.jp/caeruiro/ caeruiro https://caeruiro.hatenadiary.org/ Isabelle 2.6 Some Basic Types 2.6.1 Natural Numbers 自然数を表す型natは構成子0とSucで定義されています。case式を使った例を示します。 case n of 0 => 0 | Suc m => m 原始再帰関数の定義と、帰納法による証明の例も示します。 primrec sum :: "nat => nat" where "sum 0 = 0" | "sum (Suc n) = Suc n + sum n" lemma "sum n + sum n = n * (Suc n)" apply(induct_tac n) apply(auto) done +,… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fcaeruiro.hatenadiary.org%2Fentry%2F20100323%2F1269346495" title="Isabelle Tutorial その5 - 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-03-23 21:14:55 rich https://caeruiro.hatenadiary.org/entry/20100323/1269346495 1.0 100%