Организация ограничений в Изабеллу, с тем чтобы моделировать систему

Question

Предположим, что у меня есть следующее выражение в Isabelle/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) 

Что такое лучший способ определить эти ограничения в Изабель, в том смысле, что я могу доказать некоторые свойства над моделью, если эти ограничения сохраняются?

Answer 1

Откладывая вещи, которые вы, возможно, необходимо исправить, например, что (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)