조직 제약

Question

내가 이자벨/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에서 이런 종류의 제약이 있습니다. 이러한 제약 조건이 적용된다고 가정 할 때 모델에 대해 몇 가지 특성을 증명할 수 있다는 의미에서입니까? 이러한 (Person * Car) 쌍을 소유하거나 구동하지 않는 등 당신이 해결해야 할 수도 있습니다 일을 제쳐두고 설정

Answer 1

, 당신은 두 가지 유형, Person 그들에 대해 정의 된 속성이 없습니다 Car 있습니다.

속성을 제공하려면 공리가 필요하지만 axiomatization과 같이 전역 공리를 정의하지 않으려합니다.

일부 공리 동작을 수행하기 위해 수행하는 작업은 사용 유형 클래스 또는 로케일입니다. 다른 사람이 자세한 내용을 작성하려고하지만 여기에 하나의 베어 본 템플릿이 있습니다.