The Problem(s)
For the long time I felt that having a separate named_theorems per interpretation of the Arch locale was somewhat silly. Not only are we running around with the names Ipc_R, Ipc_R_2, KHeap_R, Ipc_AI, and so forth, each one of these introduces an attribute for adding and deleting from a set. Try a print_attributes towards the end of Refine and you'll see what I mean.
The reason I didn't say anything is because I had no way of improving the situation, and dumping every single interface lemma into a single named_theorems didn't strike me as very clever either.
Named theorems also have the issue that if you try look at a named theorem declared in the Arch locale from outside the Arch locale, you get no theorems back. This means if you want to use those theorems in order to satisfy some Arch interface, you need to get them out somehow. The current technology uses interpret Arch . inside of the interpretation, which is slow. Interpreting Arch should be avoided unless critically needed.
To make it even worse, as far as I can tell the environment after a global interpretation is unclear until the interpretation is done. If you shove a slow interpret Arch . inside that, you'll get a multi-second (4s+) stall even with skip_proofs on.
In terms of what we want to do is:
- declare named_theorems Something_assms
- add architecture-specific lemmas to Something_assms
- use Something_assms to satisfy an interface locale
- get rid of Something_assms and never think about it again
Isabelle's principle of monotonicity means that you can't delete attributes. Removing named_theorems sets also appears impossible. Trying to hide named_theorems doesn't really work, and there seems to be no way to hide attributes. So that means step 4 is out, and we have the attribute confetti outlined above. Step 3 fails because you can't get the named_theorems out directly.
Partial solution to interpreting Arch during interpretation
Then I had an idea. We can export a named_theorems into a lemmas inside the Arch locale and forcibly dig into those from the outside, e.g. :
context Arch begin arch_global_naming
lemmas Something_assms_final = Something_assms
end (* Arch *)
interpretation Something?: Something
proof goal_cases
(* no need to interpret Arch anymore, but the naming is still Arch-specific so can't be shoved into a
generic theory by mistake *)
case 1 show ?case by (intro_locales; (unfold_locales; fact ARM.Something_assms_final)?)
qed
Well, that works in principle and seemed like a decent enough solution and speed-up, but now we have even more lemma bindings on top of the existing named_theorems confetti.
Sweeping away named_theorems confetti
Despite efforts to nuke named_theorems and its attributes, there is no way to do that. However, there is a way to clear existing named_theorems for the context we are in. That means we can re-use an existing named_theorems without having to create a new one any time we want to accumulate something. If we can make that into a command, then the flow will look something like this:
- Somewhere very high up, maybe as high as Machine_AI or something, create a
named_theorems Arch_assms inside an Arch context.
- To start a new accumulation, clear
Arch_assms (alternatively we can do it at the end of the accumulation)
- Accumulate lemmas as usual by using
[Arch_assms] attribute to add them to the set
lemmas Something_assms = Arch_assms gives a static name to the accumulated theorem set- If we didn't clear
Arch_assms above, clear it now.
- Do the interpretation, using
ARM.Something_assms (or whatever arch we're on)
- Repeat from 1
If we adopt this way of doing things, there's an open question: do we want to clear Arch_assms to init, or do we want to clear it when we're done with it?
Proof of concept
If anyone can explain why Local_Theory.declaration works for lifting a Context.generic transformer to a local_theory (i.e. Proof_Context) transformer, but with an even more obvious type signature Context.proof_map does not (everything appears to work, but the named_theorems set doesn't change), I will be most grateful, because the thoughts I have about this and how well it's documented are not ones I can write here. Thanks @lsf37 for getting me to try Local_Theory.declaration after replicating the confusion.
Named_Theorems_Clear.thy:
theory Named_Theorems_Clear
imports Lib.Lib Lib.Requalify
keywords "clear_named_theorems" :: thy_decl
begin
ML ‹
local
(* We need to lift from a Context.generic transformer to a local_theory transformer.
Context.proof_map looks like it should do this, but using it with Named_Theorems.clear does not
have any effect. It is unclear why that's the case.
Going via Local_Theory.declaration does work, even if we have to give it a "morphism" that
doesn't actually contain a morphism. *)
fun alt_proof_map f =
Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>} (fn _ => f);
val _ =
Outer_Syntax.local_theory \<^command_keyword>‹clear_named_theorems›
"clear named collection of theorems"
((Parse.name_position) >> (fn (b,pos) => fn ctxt =>
alt_proof_map (Named_Theorems.clear (Named_Theorems.check ctxt (b, pos))) ctxt));
in end›
named_theorems glob_thms
declare TrueI[glob_thms]
thm glob_thms (* True *)
clear_named_theorems glob_thms
thm glob_thms (* nothing, SUCCESS *)
locale Arch
context Arch begin arch_global_naming
named_theorems Arch_assms
declare TrueI[Arch_assms]
thm Arch_assms (* True *)
clear_named_theorems Arch_assms
thm Arch_assms (* nothing, SUCCESS *)
declare TrueI[Arch_assms]
thm Arch_assms (* True *)
end (* Arch *)
context Arch begin
thm Arch_assms (* True *)
clear_named_theorems Arch_assms
thm Arch_assms (* nothing, SUCCESS *)
declare TrueI[Arch_assms]
thm Arch_assms (* True *)
end (* Arch *)
thm ARM.Arch_assms (* nothing, as expected *)
clear_named_theorems ARM.Arch_assms
context Arch begin arch_global_naming
thm Arch_assms (* True, i.e. the global removal does not change the contents in the locale *)
end (* Arch *)
declare TrueI[glob_thms]
thm glob_thms (* True *)
end
Next_Theory.thy:
theory Next_Theory imports Named_Theorems_Clear begin
(* now let's try clear and re-use named_theorems from a previous theory *)
thm glob_thms (* True *)
clear_named_theorems glob_thms
thm glob_thms (* nothing, SUCCESS *)
declare TrueI[glob_thms]
thm glob_thms (* True *)
(* and now in an Arch locale *)
context Arch begin
thm Arch_assms (* True *)
lemmas Some_R_assms = Arch_assms (* now also True *)
clear_named_theorems Arch_assms
thm Arch_assms (* nothing, SUCCESS *)
thm Some_R_assms (* static, so still True *)
end (* Arch *)
(* Now for an instantiation, we can use ARM.Some_R_assms or whatever directly outside of the locale;
for this example I won't use arch_global_naming because that depends on testing environment and
will use Arch instead. *)
thm Arch.Some_R_assms (* True, directly and without interpretation *)
end
The Problem(s)
For the long time I felt that having a separate named_theorems per interpretation of the Arch locale was somewhat silly. Not only are we running around with the names Ipc_R, Ipc_R_2, KHeap_R, Ipc_AI, and so forth, each one of these introduces an attribute for adding and deleting from a set. Try a
print_attributestowards the end of Refine and you'll see what I mean.The reason I didn't say anything is because I had no way of improving the situation, and dumping every single interface lemma into a single named_theorems didn't strike me as very clever either.
Named theorems also have the issue that if you try look at a named theorem declared in the Arch locale from outside the Arch locale, you get no theorems back. This means if you want to use those theorems in order to satisfy some Arch interface, you need to get them out somehow. The current technology uses
interpret Arch .inside of theinterpretation, which is slow. Interpreting Arch should be avoided unless critically needed.To make it even worse, as far as I can tell the environment after a global interpretation is unclear until the interpretation is done. If you shove a slow
interpret Arch .inside that, you'll get a multi-second (4s+) stall even with skip_proofs on.In terms of what we want to do is:
Isabelle's principle of monotonicity means that you can't delete attributes. Removing named_theorems sets also appears impossible. Trying to hide named_theorems doesn't really work, and there seems to be no way to hide attributes. So that means step 4 is out, and we have the attribute confetti outlined above. Step 3 fails because you can't get the named_theorems out directly.
Partial solution to interpreting Arch during interpretation
Then I had an idea. We can export a named_theorems into a lemmas inside the Arch locale and forcibly dig into those from the outside, e.g. :
Well, that works in principle and seemed like a decent enough solution and speed-up, but now we have even more lemma bindings on top of the existing named_theorems confetti.
Sweeping away named_theorems confetti
Despite efforts to nuke named_theorems and its attributes, there is no way to do that. However, there is a way to clear existing named_theorems for the context we are in. That means we can re-use an existing named_theorems without having to create a new one any time we want to accumulate something. If we can make that into a command, then the flow will look something like this:
named_theorems Arch_assmsinside an Arch context.Arch_assms(alternatively we can do it at the end of the accumulation)[Arch_assms]attribute to add them to the setlemmas Something_assms = Arch_assmsgives a static name to the accumulated theorem setArch_assmsabove, clear it now.ARM.Something_assms(or whatever arch we're on)If we adopt this way of doing things, there's an open question: do we want to clear
Arch_assmsto init, or do we want to clear it when we're done with it?Proof of concept
If anyone can explain why Local_Theory.declaration works for lifting a Context.generic transformer to a local_theory (i.e. Proof_Context) transformer, but with an even more obvious type signature
Context.proof_mapdoes not (everything appears to work, but the named_theorems set doesn't change), I will be most grateful, because the thoughts I have about this and how well it's documented are not ones I can write here. Thanks @lsf37 for getting me to try Local_Theory.declaration after replicating the confusion.Named_Theorems_Clear.thy:Next_Theory.thy: