组织的约束，以系统模型

假设我在伊莎贝尔/ HOL下面的表达式：组织的约束，以系统模型

typedecl Person 
typedecl Car 

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

这应该是人与车的类型与它们之间的两个关系，一个名为驱动器和建模拥有，也是人的年龄属性。

我想指出，大家谁拥有一辆汽车，肯定会开车，谁开车的人都大于17，因此限制：

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

什么是确定的最佳途径在Isabelle中存在这种约束，从某种意义上说，假设这些约束成立，我可以证明模型的某些性质？

来源

2014-11-06 qartal

撇开你可能需要修复的东西，例如(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-06 21:04:19

组织的约束，以系统模型

回答

相关问题