Organization of constraints in isabelle for system simulation

Question

Suppose Isabelle / HOL has the following expression:

typedecl Person
typedecl Car

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

It is supposed to model the types Person and Car with two relationships between them, called disks and their own, as well as the age property of Person.

I would like to state that everyone who owns a car will definitely drive a car, and people who drive cars will be over 17, so the restrictions are:

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

What is the best way to define these constraints in Isabelle in the sense that I can prove some properties over a model if these constraints persist?

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)