在isabelle中组织约束以对系统进行建模 [英] Organizing constraints in isabelle in order to model a system

问题描述

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

Suppose that I have the following expression in Isabelle/HOL:

typedecl Person
typedecl Car

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

这应该通过具有两种关系的个人和汽车类型来建模，分别是驱动器和拥有者，以及个人的年龄属性.

This is supposed to model Person and Car types with two relations between them, named drives and owns, and also the age property of Person.

我想指出的是，每个拥有汽车的人都一定会开车，而开车的人大于17岁，因此有以下限制条件:

I would like to state that everybody who owns a car, would definitely drive the car, and people who drive cars are greater than 17, So the constraints:

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

在这样的意义上，假设这些约束成立，我可以证明模型的某些特性，那么在Isabelle中定义此类约束的最佳方法是什么?

What is the best way to define these kind of constraints in Isabelle, in the sense that I can prove some properties over the model, assuming these constraints hold true?

推荐答案

搁置您可能需要解决的问题，例如(Person * Car)对不拥有或不驱动，您有两种类型，Person和Car没有为其定义的属性.

Setting aside things you might need to fix, such as that a (Person * Car) pair doesn't own or drive, you have two types, Person and Car which have no properties defined for them.

要为它们提供属性，您需要公理，但您不想使用类似axiomatization之类的方法来定义全局公理.

To give them properties, you need axioms, but you don't want to use something like axiomatization to define global axioms.

要采取一些公理措施，您要做的是使用类型类或语言环境.会有其他人想要填写更多的细节，但这是一个简单的模板:

What you do to get some axiom action going is use type classes or locales. Someone else will want to fill in more details, but here's one bare-bones template:

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)

这篇关于在isabelle中组织约束以对系统进行建模的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！