9. Advanced Simplification and Induction 9.1 Simplification この節では、単純化に関してこれまで述べてこなかった部分を補足します。 9.1.1 Advanced Features Congruence Rules.P ==> QのQを単純化するのに前提Pを利用できます。==>ならば当然のように…

8.5 Introducing New Types 多くの場合は定義済みの型boolや=>とそれらの組み合わせで事が足りますが、稀にこれらでは表わせない高度な型が必要になる場合があります。そのような場合に必要となる型の導入方法を紹介します。 8.5.1 Declaring New Types type…

8.3 Type Classes 型クラスの概念はHaskellによって広まりました。型クラスは型とインタフェースの集合を定義し、そのクラスに属する型はインタフェースを実装しなければなりません。Isabelleが提供する型クラスも同様ですが、さらにプロパティ(型公理)を定…

8. More about Typesこの章ではより高度な型の扱い方を紹介します。 8.1 Pairs and Tuples ペアやタプルは既に登場しましたが、ここではパターンマッチついて見てみます。 8.1.1 Pattern Matching with Tuples 変数を束縛するためのパターンとしてペアやタプ…

7.4 Case Study: A Context Free Grammer ここでは、HopcroftとUllmanによる文脈自由文法の例*1を取り上げます。生成規則は次のようになっており、これはaとbの数が同じ文字列を生成します。 まず、アルファベットを定義します。 datatype alpha = a | b 便…

7.2 The Reflexive Transitive Closure 帰納的定義はパラメータを取り、集合を作るための関数とすることができます。また関係はペアの集合であることから、これも帰納的に定義できます。例として関係から反射推移閉包への写像関数を考えます。 inductive_set…