2013-05-12から1日間の記事一覧
0とは限らない自然数からの帰納法は,Nat.thyのdec_inductという定理となっています. print_statement dec_inducttheorem dec_induct: fixes i :: "nat" and j :: "nat" and P :: "nat ⇒ bool" assumes "i ≤ j" and "P i" and "⋀n. i ≤ n ⟹ P n ⟹ P (Suc n)…
0とは限らない自然数からの帰納法は,Nat.thyのdec_inductという定理となっています. print_statement dec_inducttheorem dec_induct: fixes i :: "nat" and j :: "nat" and P :: "nat ⇒ bool" assumes "i ≤ j" and "P i" and "⋀n. i ≤ n ⟹ P n ⟹ P (Suc n)…