7. Representation II Locales in Isabelle/HOL Flashcards
1
Q
Why are definitional extensions preferred over axiomatic extensions?
A
Axiomatization can introduce inconsistency
2
Q
Why locales?
A
Encapsulates axioms locally in a sound way.
Within the locale you can use the assumptions as if they are axioms
Outside the locale (when it is instanciated with concrete types) you must discarge these assumptions.
3
Q
How do you define parameters in a locale?
A
fixes …
4
Q
How do you define assumptions in a locale?
A
assumes … and … and …
5
Q
What is the format of a locale?
A
locale name =
fixes …
assumes …
and …
begin
lemma foo ….
theorem bar …
end
6
Q
How do you extend a locale?
A
locale name = other_locale +
…
