尝试定义自定义 'declare' & 'using' 命令
Trying to define custom 'declare' & 'using' commands
我想出了如何修改一些Isar和ML，但在这里我不知道如何得到我想要的。
我使用 declare 和 using 打开和关闭信息，就像这些（和其他更长的组合）一样：
declare[[simp_trace_new mode=full]]
declare[[show_sorts=false]]
using[[simp_trace_new mode=full]]
using[[show_sorts=false]]
我创建了 jEdit 宏来临时插入 big long declare 和 using 命令，但一个问题是我可能会忘记删除它们。
我想要做的是定义不带参数的 declare 和 using 命令。此外，这些命令将使用 Output.warning 以便我知道删除它们。
比如我会定义如下关键字，对应上面的4条命令：
keywords
"simpD" "~sortsD" :: thy_decl
and
"simpU" "~sortsU" :: prf_decl % "proof"
从 src/Pure/Isar/isar_syn.ML#l229 and src/Pure/Isar/isar_syn.ML#l588，我找到 declare 和 using 命令：
val _ = Outer_Syntax.local_theory' @{command_spec "declare"} "declare theorems"
(Parse.and_list1 Parse_Spec.xthms1 -- Parse.for_fixes
>> (fn (facts, fixes) =>
#2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
val _ = Outer_Syntax.command @{command_spec "using"} "augment goal facts"
(facts >> (Toplevel.proof o Proof.using_cmd));
下面，我包含一个简短的理论来展示如何使用这些命令。我使用虚拟命令为 simpD 和 simpU 定义了外部语法，这部分显示了我想要的内容。虚拟命令带有一个参数，但我不希望那样。我想要一个像 help 这样不带参数的命令。
谢谢。
theory i150312a__custom_declare_and_using_syntax
imports Complex_Main
keywords
"simpD" "~sortsD" :: thy_decl
and
"simpU" "~sortsU" :: prf_decl % "proof"
begin
(*Want outer syntax for fixed 'declare' (and 'using') commands like these.*)
declare[[simp_trace_new mode=full]]
declare[[show_sorts=false]]
(*EXE: declare[[simp_trace_new mode=full]] with a warning. Please modify as needed.*)
ML{*Outer_Syntax.improper_command @{command_spec "simpD"} ""
(Parse.text >> (fn _ => Toplevel.keep (fn _ =>
let
val _ = Output.warning "DECLARE: declare[[simp_trace_new mode=full]]"
in () end)))*}
simpD"" (* But here, I don't want to have to use the double quotes.*)
(*EXE: using[[simp_trace_new mode=full]] with a warning. Please modify as needed.*)
ML{*Outer_Syntax.improper_command @{command_spec "simpU"} ""
(Parse.text >> (fn _ => Toplevel.keep (fn _ =>
let
val _ = Output.warning "USING: using[[simp_trace_new mode=full]]"
in () end)))*}
lemma "True"
simpU"" (* But here, I don't want to have to use the double quotes.*)
by(simp)
(* FROM src/Pure/Isar/isar_syn.ML
val _ = Outer_Syntax.local_theory' @{command_spec "declare"} "declare theorems"
(Parse.and_list1 Parse_Spec.xthms1 -- Parse.for_fixes
>> (fn (facts, fixes) =>
#2 oo Specification.theorems_cmd
"" [(Attrib.empty_binding, flat facts)] fixes));
val _ = Outer_Syntax.command @{command_spec "using"} "augment goal facts"
(facts >> (Toplevel.proof o Proof.using_cmd));
*)
end
告诫自己最重要。这是我的 WARN 和跟踪命令的样子，插入了 jEdit 宏和键序列：
lemma "True"
WARN"trace"using[[simp_trace_new mode=full]]
WARN"trace"using[[linarith_trace,rule_trace,blast_trace,blast_stats]]
by(blast)
我实际上使用 \<open> 和 \<close> 代替双引号，但漩涡花饰并不总能在浏览器中正确显示。
设置默认值，忘记更改时会感到困惑
我的 THY 基本上没有警告，所以我应该注意到右侧排水沟中的琥珀色警告颜色。
我在导入 i0.thy 中设置了我的工作首选项，如下所示，其中一些更改了默认值，并且都明确告诉我应该看到或不应该看到的内容：
declare[[show_sorts=true]]
declare[[show_types=false]]
declare[[show_brackets=false]]
declare[[names_unique=true]]
declare[[show_question_marks=true]]
declare[[show_consts=true]]
...(and more)
大多数我从不改变，但是show_sorts、show_types和show_brackets我需要不断改变，有时是为了展示细节，有时是为了摆脱混乱。
我一直打开输出面板，show_consts 对查看类型的推断方式有很大帮助，因为这在尝试实例化类型时非常重要 类，总的来说很重要。
为了避免处理不必要的来源，我必须在我工作的地方插入 declare。
好吧，问题是当我插入一个 show 命令，然后忘记它，我最终变得困惑。我查看了我在 i0.thy 中设置的内容，然后无法弄清楚为什么我没有看到某些细节，或者看到了某些细节。
关于 THY 的一些解释
下面，我包含一个理论，其中包含 WARN 命令。我还包含了 jEdit 宏，它位于我的 .isabelle/Isabelle2014/jEdit/macros 文件夹中。在 jEdit 全局选项/快捷方式 中，我为宏分配了一个键序列。
一些细节：
keywords 中的 diag 允许在证明中使用 WARN 关键字。- 这里只有
blast_trace和blast_stats是必要的，因为我展示了我每次使用simp_trace_new时打开的痕迹。
blast_trace 和 blast_stats 的来源来自 M. Wenzel on the isabelle-users mailing list。WARN 的来源是由 L. Noschinski in another SO question 提供的来源调整。- 我打开其他跟踪的一个原因是因为
auto 有时会调用其他方法，例如 blast，甚至 simp 可能会调用一些东西。
- 有时我想确切地知道正在使用什么
simp 规则，并使用像 apply(simp only: thm1, thm2, ...) 或 apply(auto simp only: thm1, thm2, ...) 这样的命令。我过去看到的是可以自动调用 blast 或线性算术方法。
- 如果您想在证明之外使用
declare，而不是在证明中使用 using，请为 declare 创建一个 jEdit 宏。
宏
短的部分是jEdit宏：
//isar__ust....using_simp_trace.bsh
textArea.setSelectedText("WARN\<open>trace\<close>using[[simp_trace_new mode=full]]");
textArea.insertEnterAndIndent();
textArea.setSelectedText("WARN\<open>trace\<close>using[[linarith_trace,rule_trace,blast_trace,blast_stats]]");
我记不住我的键序列，所以我把它们放在了文件名中。我使用 4 个字母的序列，ALT-i u s t.
我使用 Q-Dir 查看包含我的 jEdit 宏文件的 4 个不同文件夹。
你的
这是你的：
theory i150312b__my_WARN
imports Main
keywords "WARN" :: diag
begin
ML{*Outer_Syntax.improper_command @{command_spec "WARN"}
"Print a warning message"
(Parse.text >> (fn s => Toplevel.keep (fn _ =>
let val _ = Output.warning ("WARNING: " ^ s) in () end)))*}
attribute_setup blast_trace = {*
Scan.lift
(Parse.$$$ "=" -- Args.$$$ "true" >> K true ||
Parse.$$$ "=" -- Args.$$$ "false" >> K false ||
Scan.succeed true) >>
(fn b => Thm.declaration_attribute (K (Config.put_generic Blast.trace b)))
*}
attribute_setup blast_stats = {*
Scan.lift
(Parse.$$$ "=" -- Args.$$$ "true" >> K true ||
Parse.$$$ "=" -- Args.$$$ "false" >> K false ||
Scan.succeed true) >>
(fn b => Thm.declaration_attribute (K (Config.put_generic Blast.stats b)))
*}
lemma "True"
WARN"trace"using[[simp_trace_new mode=full]]
WARN"trace"using[[linarith_trace,rule_trace,blast_trace,blast_stats]]
by(blast)
end
The Isabelle Cookbook，作者 Christian Urban，有贡献
我需要抽出时间阅读 Isabelle Cookbook，以便能够调整和创建 Isar 外部语法命令。人们不想免费工作，否则我会破坏桥梁。页面是 www.inf.kcl.ac.uk/staff/urbanc/Cookbook.
PDF 也在 TUM repository page, which contains the source. Click on the gz link 上的 tar.gz 文件中。
我想出了如何修改一些Isar和ML，但在这里我不知道如何得到我想要的。
我使用 declare 和 using 打开和关闭信息，就像这些（和其他更长的组合）一样：
declare[[simp_trace_new mode=full]]
declare[[show_sorts=false]]
using[[simp_trace_new mode=full]]
using[[show_sorts=false]]
我创建了 jEdit 宏来临时插入 big long declare 和 using 命令，但一个问题是我可能会忘记删除它们。
我想要做的是定义不带参数的 declare 和 using 命令。此外，这些命令将使用 Output.warning 以便我知道删除它们。
比如我会定义如下关键字，对应上面的4条命令：
keywords
"simpD" "~sortsD" :: thy_decl
and
"simpU" "~sortsU" :: prf_decl % "proof"
从 src/Pure/Isar/isar_syn.ML#l229 and src/Pure/Isar/isar_syn.ML#l588，我找到 declare 和 using 命令：
val _ = Outer_Syntax.local_theory' @{command_spec "declare"} "declare theorems"
(Parse.and_list1 Parse_Spec.xthms1 -- Parse.for_fixes
>> (fn (facts, fixes) =>
#2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
val _ = Outer_Syntax.command @{command_spec "using"} "augment goal facts"
(facts >> (Toplevel.proof o Proof.using_cmd));
下面，我包含一个简短的理论来展示如何使用这些命令。我使用虚拟命令为 simpD 和 simpU 定义了外部语法，这部分显示了我想要的内容。虚拟命令带有一个参数，但我不希望那样。我想要一个像 help 这样不带参数的命令。
谢谢。
theory i150312a__custom_declare_and_using_syntax
imports Complex_Main
keywords
"simpD" "~sortsD" :: thy_decl
and
"simpU" "~sortsU" :: prf_decl % "proof"
begin
(*Want outer syntax for fixed 'declare' (and 'using') commands like these.*)
declare[[simp_trace_new mode=full]]
declare[[show_sorts=false]]
(*EXE: declare[[simp_trace_new mode=full]] with a warning. Please modify as needed.*)
ML{*Outer_Syntax.improper_command @{command_spec "simpD"} ""
(Parse.text >> (fn _ => Toplevel.keep (fn _ =>
let
val _ = Output.warning "DECLARE: declare[[simp_trace_new mode=full]]"
in () end)))*}
simpD"" (* But here, I don't want to have to use the double quotes.*)
(*EXE: using[[simp_trace_new mode=full]] with a warning. Please modify as needed.*)
ML{*Outer_Syntax.improper_command @{command_spec "simpU"} ""
(Parse.text >> (fn _ => Toplevel.keep (fn _ =>
let
val _ = Output.warning "USING: using[[simp_trace_new mode=full]]"
in () end)))*}
lemma "True"
simpU"" (* But here, I don't want to have to use the double quotes.*)
by(simp)
(* FROM src/Pure/Isar/isar_syn.ML
val _ = Outer_Syntax.local_theory' @{command_spec "declare"} "declare theorems"
(Parse.and_list1 Parse_Spec.xthms1 -- Parse.for_fixes
>> (fn (facts, fixes) =>
#2 oo Specification.theorems_cmd
"" [(Attrib.empty_binding, flat facts)] fixes));
val _ = Outer_Syntax.command @{command_spec "using"} "augment goal facts"
(facts >> (Toplevel.proof o Proof.using_cmd));
*)
end
告诫自己最重要。这是我的 WARN 和跟踪命令的样子，插入了 jEdit 宏和键序列：
lemma "True"
WARN"trace"using[[simp_trace_new mode=full]]
WARN"trace"using[[linarith_trace,rule_trace,blast_trace,blast_stats]]
by(blast)
我实际上使用 \<open> 和 \<close> 代替双引号，但漩涡花饰并不总能在浏览器中正确显示。
设置默认值，忘记更改时会感到困惑
我的 THY 基本上没有警告，所以我应该注意到右侧排水沟中的琥珀色警告颜色。
我在导入 i0.thy 中设置了我的工作首选项，如下所示，其中一些更改了默认值，并且都明确告诉我应该看到或不应该看到的内容：
declare[[show_sorts=true]]
declare[[show_types=false]]
declare[[show_brackets=false]]
declare[[names_unique=true]]
declare[[show_question_marks=true]]
declare[[show_consts=true]]
...(and more)
大多数我从不改变，但是show_sorts、show_types和show_brackets我需要不断改变，有时是为了展示细节，有时是为了摆脱混乱。
我一直打开输出面板，show_consts 对查看类型的推断方式有很大帮助，因为这在尝试实例化类型时非常重要 类，总的来说很重要。
为了避免处理不必要的来源，我必须在我工作的地方插入 declare。
好吧，问题是当我插入一个 show 命令，然后忘记它，我最终变得困惑。我查看了我在 i0.thy 中设置的内容，然后无法弄清楚为什么我没有看到某些细节，或者看到了某些细节。
关于 THY 的一些解释
下面，我包含一个理论，其中包含 WARN 命令。我还包含了 jEdit 宏，它位于我的 .isabelle/Isabelle2014/jEdit/macros 文件夹中。在 jEdit 全局选项/快捷方式 中，我为宏分配了一个键序列。
一些细节：
keywords中的diag允许在证明中使用WARN关键字。- 这里只有
blast_trace和blast_stats是必要的，因为我展示了我每次使用simp_trace_new时打开的痕迹。 blast_trace和blast_stats的来源来自 M. Wenzel on the isabelle-users mailing list。WARN的来源是由 L. Noschinski in another SO question 提供的来源调整。- 我打开其他跟踪的一个原因是因为
auto有时会调用其他方法，例如blast，甚至simp可能会调用一些东西。 - 有时我想确切地知道正在使用什么
simp规则，并使用像apply(simp only: thm1, thm2, ...)或apply(auto simp only: thm1, thm2, ...)这样的命令。我过去看到的是可以自动调用blast或线性算术方法。 - 如果您想在证明之外使用
declare，而不是在证明中使用using，请为declare创建一个 jEdit 宏。
宏
短的部分是jEdit宏：
//isar__ust....using_simp_trace.bsh
textArea.setSelectedText("WARN\<open>trace\<close>using[[simp_trace_new mode=full]]");
textArea.insertEnterAndIndent();
textArea.setSelectedText("WARN\<open>trace\<close>using[[linarith_trace,rule_trace,blast_trace,blast_stats]]");
我记不住我的键序列，所以我把它们放在了文件名中。我使用 4 个字母的序列，ALT-i u s t.
我使用 Q-Dir 查看包含我的 jEdit 宏文件的 4 个不同文件夹。
你的
这是你的：
theory i150312b__my_WARN
imports Main
keywords "WARN" :: diag
begin
ML{*Outer_Syntax.improper_command @{command_spec "WARN"}
"Print a warning message"
(Parse.text >> (fn s => Toplevel.keep (fn _ =>
let val _ = Output.warning ("WARNING: " ^ s) in () end)))*}
attribute_setup blast_trace = {*
Scan.lift
(Parse.$$$ "=" -- Args.$$$ "true" >> K true ||
Parse.$$$ "=" -- Args.$$$ "false" >> K false ||
Scan.succeed true) >>
(fn b => Thm.declaration_attribute (K (Config.put_generic Blast.trace b)))
*}
attribute_setup blast_stats = {*
Scan.lift
(Parse.$$$ "=" -- Args.$$$ "true" >> K true ||
Parse.$$$ "=" -- Args.$$$ "false" >> K false ||
Scan.succeed true) >>
(fn b => Thm.declaration_attribute (K (Config.put_generic Blast.stats b)))
*}
lemma "True"
WARN"trace"using[[simp_trace_new mode=full]]
WARN"trace"using[[linarith_trace,rule_trace,blast_trace,blast_stats]]
by(blast)
end
The Isabelle Cookbook，作者 Christian Urban，有贡献
我需要抽出时间阅读 Isabelle Cookbook，以便能够调整和创建 Isar 外部语法命令。人们不想免费工作，否则我会破坏桥梁。页面是 www.inf.kcl.ac.uk/staff/urbanc/Cookbook.
PDF 也在 TUM repository page, which contains the source. Click on the gz link 上的 tar.gz 文件中。