{"description":"2.6 Some Basic Types 2.6.1 Natural Numbers \u81ea\u7136\u6570\u3092\u8868\u3059\u578bnat\u306f\u69cb\u6210\u5b500\u3068Suc\u3067\u5b9a\u7fa9\u3055\u308c\u3066\u3044\u307e\u3059\u3002case\u5f0f\u3092\u4f7f\u3063\u305f\u4f8b\u3092\u793a\u3057\u307e\u3059\u3002 case n of 0 => 0 | Suc m => m \u539f\u59cb\u518d\u5e30\u95a2\u6570\u306e\u5b9a\u7fa9\u3068\u3001\u5e30\u7d0d\u6cd5\u306b\u3088\u308b\u8a3c\u660e\u306e\u4f8b\u3082\u793a\u3057\u307e\u3059\u3002 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 +,\u2026","height":"190","width":"100%","categories":["Isabelle"],"author_name":"caeruiro","provider_url":"https://hatena.blog","provider_name":"Hatena Blog","title":"Isabelle Tutorial \u305d\u306e5","author_url":"https://blog.hatena.ne.jp/caeruiro/","blog_url":"https://caeruiro.hatenadiary.org/","url":"https://caeruiro.hatenadiary.org/entry/20100323/1269346495","image_url":null,"blog_title":"caeruiro","type":"rich","version":"1.0","published":"2010-03-23 21:14:55","html":"<iframe src=\"https://hatenablog-parts.com/embed?url=https%3A%2F%2Fcaeruiro.hatenadiary.org%2Fentry%2F20100323%2F1269346495\" title=\"Isabelle Tutorial \u305d\u306e5 - caeruiro\" class=\"embed-card embed-blogcard\" scrolling=\"no\" frameborder=\"0\" style=\"display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;\"></iframe>"}