Email Gateway (Aug 22 2022 at 15:30): Email Gateway (Aug 22 2022 at 15:30):From: Simon Cooksey <sjc205@kent.ac.uk>
Hello,
I have a locale which provides me with a few data structures and has the
proof burden of invariants on them. I'd like to use an instantiation of
a locale with concrete sets and relations and prove properties about it.
Is there some documentation I can follow to do this? I've not found the
locales and interpretations tutorial very helpful for the 2nd part.
If I'm misunderstanding how locales are used corrections are also welcome!
Thanks,
Simon
signature.asc
Email Gateway (Aug 22 2022 at 15:30):From: Simon Cooksey <sjc205@kent.ac.uk>
Some details:
locale partial_order =
fixes preceeds :: "'a ⇒ 'a ⇒ bool" (infixl "≼" 50)
and events :: "'a set" ("𝔈" 1000)
assumes refl [intro, simp]: "x ≼ x"
and anti_sym [intro]: "⟦ x ≼ y; y ≼ x ⟧ ⟹ x = y"
and trans [trans]: "⟦ x ≼ y; y ≼ z ⟧ ⟹ x ≼ z"
locale primeES = partial_order +
fixes conflict :: "'a ⇒ 'a ⇒ bool" (infixl "#" 50)
assumes sym [intro]: "⟦ conflict x y ⟧ ⟹ conflict y x"
and confOverPO [intro]: "⟦ conflict c d; d ≼ e ⟧ ⟹ conflict c e"
datatype mem_action = W | R | I
datatype label = Label mem_action string int
type_synonym 'a config = "'a set"
locale labelledES = primeES +
fixes config_domain :: "'a config set" ("ℭ" 1000)
and label :: "'a ⇒ label"
assumes conflict_free: "⟦C ∈ config_domain; x ∈ C; y ∈ C ⟧ ⟹
¬(conflict x y)"
and down_closed: "⟦C ∈ config_domain; y ∈ C; x ≼ y ⟧ ⟹ x ∈ C"
and config_subset: "C ∈ ℭ ⟹ C ⊆ 𝔈"
and the instantiation looks like this:
interpretation emptyES: labelledES
"λx y . (x, y) ∈ {(1,1)}⇧*" -- Order
"{1}" -- Events
"λx y . (x, y) ∈ {}" -- Conflict
"{{1}}"
"λx . Label I '''' 0" -- Labelling
apply(unfold_locales)
apply(auto)
apply (metis Domain_empty Domain_insert Not_Domain_rtrancl singleton_iff)
apply (meson converse_rtranclE prod.inject singletonD)
done
Which goes through cleanly.
There's some definitions in the context of labelledES, such as
well_justified and I'd like to prove something like "well_justified
emptyES" where emptyES is the instantiation of a labelledES as given above.
Cheers again,
Simon
signature.asc
Email Gateway (Aug 22 2022 at 15:30):From: Matthew.Brecknell@data61.csiro.au
You could write a locale expression to specialise labelledES to your
particular scenario:
locale emptyES = labelledES
"λx y . (x, y) ∈ {(1,1)}⇧*" -- Order
"{1}" -- Events
"λx y . (x, y) ∈ {}" -- Conflict
"{{1}}"
"λx . Label I '''' 0" -- Labelling
You can then prove lemmas in the context of emptyES:
lemma (in emptyES) well_justified: "well_justified"
sorry
I think you should still be able to prove that this has a valid
interpretation, without restating all the parameters. This will give
you emptyES.well_justified in the interpretation context:
interpretation emptyES: emptyES
sorry (* as before *)
If that produces conflicts, you might need to choose different names
for the locale and interpretation.
This seems a little fishy, though. I guess this is exploration, and you
are ultimately looking for some more general set of assumptions from
which well_justified always follows?
BTW, if you really mean to permanently interpret something in the
global context, you should prefer global_interpretation instead of
interpretation. A global_interpretation will insist on being in the
global context, whereas interpretation will silently adopt a
different behaviour if you later unintentionally wrap it in any kind of
context block.
Last updated: Apr 26 2024 at 20:16 UTC