ロケールの解釈に必要な証明で、構造体のいくつかのプロパティを使用したいと考えています。
例として、述語 P を定義し、述語を満たす要素に対する操作についていくつかの補題 (addは閉二項操作であり、結合的であり、中立要素addが存在する) を証明したとします。zeroaddP
次に、要素のセットを、ロケールを満たす構造として解釈したいと思います。monoid
interpretation "{s . P s}" :: monoid "(add)" "(zero)"
unfolding
monoid_def
using
add_is_associative
zero_is_neutral
しかし、私の証明の目標では、すべての要素が実際に述語を満たしていることを得ることができず、セット内の要素について既に証明したPような一般的な目標が残されています。add zero a = a
すべての要素が predicate を満たすことを目標に強制するにはどうすればよいPですか?