Isabelle/HOL に次の式があるとします。
typedecl Person
typedecl Car
consts age :: "Person ⇒ int"
consts drives ::"(Person × Car) set"
consts owns ::"(Person × Car) set"
これは、Drivers と Owns という名前の 2 つの関係と、Person の age プロパティを使用して、Person と Car のタイプをモデル化することになっています。
車を所有する人は誰でも間違いなく車を運転し、車を運転する人は 17 歳以上であると述べたいと思います。したがって、制約は次のとおりです。
(∀a. a ∈ owns ⟶ a ∈ drives)
(∀d ∈ drives. age (fst d) > 17)
これらの制約が当てはまると仮定して、モデルに対していくつかのプロパティを証明できるという意味で、イザベルでこれらの種類の制約を定義する最良の方法は何ですか?