0

假设我在 Isabelle/HOL 中有以下表达式：

typedecl Person
typedecl Car

consts age :: "Person ⇒ int" 
consts drives ::"(Person × Car) set"
consts owns ::"(Person × Car) set"

这应该为 Person 和 Car 类型建模，它们之间有两个关系，命名为 drive 和 owns，还有 Person 的 age 属性。

我想说每个有车的人肯定会开车，而且开车的人都大于17岁，所以限制条件：

(∀a. a ∈ owns ⟶ a ∈ drives)
(∀d ∈ drives. age (fst d) > 17)

在 Isabelle 中定义此类约束的最佳方法是什么，从某种意义上说，假设这些约束成立，我可以证明模型的某些属性？

4

1 回答 1

2

抛开您可能需要修复的事情，例如一(Person * Car)对不拥有或驱动，您有两种类型，Person并且Car没有为它们定义属性。

要赋予它们属性，您需要公理，但您不想使用诸如axiomatization定义全局公理之类的东西。

要使某些公理动作进行，您所做的是使用类型类或语言环境。其他人会想要填写更多详细信息，但这里有一个简单的模板：

typedecl Person
typedecl Car

locale foo_model =
  fixes age :: "Person => int" 
  fixes drives :: "(Person * Car) set"
  fixes owns :: "(Person * Car) set"
  assumes owns_axiom: "a ∈ owns --> a ∈ drives"
  assumes age_axiom: "∀d ∈ drives.  age (fst d) > 17"
begin
lemma some_lemma_you_want: "True"
  by(simp)
end

lemma (in foo_model) some_other_lemma_you_want : "True"
  by(simp)
于 2014-11-06T21:04:19.993 回答