Email Gateway (Aug 19 2022 at 17:31): Email Gateway (Aug 19 2022 at 17:31):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Given a thm, a name, and an lthy, I’d like to “note” this thm such that it is declared as safe introduction rule. Roughly like
declare name[intro!]
What I currently have is
ML {*
fun f .. lthy =
let ..
val intro = Attrib.internal (K (Context_Rules.intro_bang NONE));
val lthy' = Local_Theory.notes [((Binding.name nm, [intro]), [([thm], [intro])])] lthy
in lthy’ end
*}
local_setup {*
f ..
*}
thm name
now shows the theorem, but it’s not declared as safe intro.
What am I doing wrong?
I’m not sure what the “int option” parameter is on intro_bang, and I’m also not sure why notes wants 2 lists of attributes, but that doesn’t seem to be the problem.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 10:10):From: Makarius <makarius@sketis.net>
On Thu, 26 Mar 2015, Gerwin Klein wrote:
Given a thm, a name, and an lthy, I’d like to “note” this thm such that
it is declared as safe introduction rule. Roughly likedeclare name[intro!]
Here is an example for Isabelle2015:
experiment
fixes A B C
assumes a: A
and b: B
and c: C
begin
local_setup ‹
let
val b = @{binding test};
val ths = @{thms a b c};
in snd o Local_Theory.note ((b, @{attributes [intro!]}), ths) end
›
thm test
lemma A B C by blast+
end
What I currently have is
ML {*
fun f .. lthy =
let ..
val intro = Attrib.internal (K (Context_Rules.intro_bang NONE));
val lthy' = Local_Theory.notes [((Binding.name nm, [intro]), [([thm], [intro])])] lthy
in lthy’ end
*}local_setup {*
f ..
*}thm name
now shows the theorem, but it’s not declared as safe intro.
What am I doing wrong?
Hovering in PIDE over the formal text "[intro!]" shows that the standard
attribute is from the Classical module in HOL, not Context_Rules in Pure.
More notes:
* Local_Theory.note is a convenient shortcut for many situations.
Tools should refrain from introducing further shortcuts without any
good reason. It obscures applications uncessarily when everybody has
his proviate set of system operations.
* Attrib.internal is a rather old form. The @{attributes} antiquotation
seen above supersedes that for all situations of constant attribute
expressions, without ML arguments. Most declaration attributes are of
that form.
* "nm" is a slightly of ML name for a "name"; normally letters "a" or
"b" are used for that, or something more specific according to the
meaning of the thing.
I need to point this out explicitly, because I've spent significant
time to sanitize the Eisbach sources in that respect.
I’m not sure what the “int option” parameter is on intro_bang
It is a priority for the Pure version of these attributes. This is only
relevant to the intuitionistic prover, and normally not relevant for
Isabelle/HOL applications.
Makarius
Last updated: Apr 26 2024 at 04:17 UTC