Resolving the cross-dependencies of various locales and Arch required
extending locales with assumptions that overlap those of the CSpace1_R*
locales. This lets us treat these extended locales as if they were the
real thing while inside CSpace1_R* in the generic theory. Once
CSpace1_R* locales are instantiated, we can satisfy the extended
assumptions and export the facts back to the original locale (via
sublocale command).
For example, for locale mdb_swap we declare
locale mdb_swap_gen = mdb_swap + assumes isMDBParentOf_eq
where isMDBParentOf_eq requires Arch to prove.
Since isMDBParentOf_eq is also an assumption of CSpace1_R_2,
while inside, we can act as if mdb_swap_gen is mdb_swap:
lemma (in CSpace1_R_2) mdb_swap_gen_convert:
"mdb_swap_gen m m' = mdb_swap m m'"
Then in the arch-specific theory, once CSpace1_R_2 is instantiated with
an actual isMDBParentOf_eq, we can use it to satisfy the extra
mdb_swap_gen assumption and get lemmas that look like what we originally
wanted in mdb_swap (which can be done in a generic theory again):
context mdb_swap begin
sublocale mdb_swap_gen by (unfold_locales; fastforce elim: isMDBParentOf_eq)+
end
We are still stuck with the limitation that any fact proven this way
will be named mdb_swap_gen.fact and the name either needs to be re-bound
in mdb_swap, or proofs that point to it explicitly need to be adjusted
(e.g. by using mdb_swap_gen_convert).
As seen in this commit message, but for public consumption: