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

Isabelle Tutorial その26

9.2 Advanced Induction Techniques この節では、証明したい式が帰納法に適した形になっていない場合にどうすべきか、そして帰納法のための新たな定理をどのように導出し使うかということを見ていきます。 9.2.1 Massaging the Proposition 証明したい式が帰…