如何解决在 thy_goal_defn 关键字 qed 后更新理论数据
在 thy_goal_defn 关键字引入的义务得到满足后,我正在尝试更新一些自定义理论数据。
举个例子,如果我有一个 data
关键字,它会为给定的术语打开一个简单的证明。我有一个 print_data
关键字,它只是打印出理论数据的状态。
data example:
"(x::int) < y ⟹ x ≤ y"
by simp
data example2:
"(x::int) > 0 ⟹ x ≥ 0"
by simp
print_data
然后在上面,print_data
关键字将只显示
example: x < y ⟹ x ≤ y
example2: 0 < x ⟹ 0 ≤ x
我一直试图了解如何实现这一点,但到目前为止,我只能在证明义务时更新理论数据,即以下内容将按预期打印 example: x < y ⟹ x ≤ y
。
data example:
"(x::int) < y ⟹ x ≤ y"
print_data
by simp
我的实现方法如下:
- 在理论开始时声明关键词
theory ProvedData
imports Main
keywords
"data" :: thy_goal_defn and
"print_data" :: diag
begin
type data =
{name: string,expression: term}
signature DATA_LIST =
sig
val get: theory -> data list
val add: data -> theory -> theory
val reset: theory -> theory
end;
structure DataList: DATA_LIST =
struct
structure DataStore = Theory_Data
(
type T = data list;
val empty = [];
val extend = I;
val merge = Library.merge (fn (_) => true);
);
val get = DataStore.get;
fun add t thy = DataStore.map (cons t) thy
val reset = DataStore.put [];
end;
fun open_data_goal
((bind: binding,_),exp: string) ctxt =
let
val prop = Syntax.read_prop ctxt exp;
val term = Syntax.read_term ctxt exp;
val register = DataList.add {name=Binding.print bind,expression=term}
fun after_qed _ ctxt =
(Proof_Context.background_theory register ctxt)
in
Proof.theorem NONE after_qed [[(prop,[])]]
(Proof_Context.background_theory register ctxt)
end
val _ =
Outer_Syntax.local_theory_to_proof \<^command_keyword>‹data›
"define an data and open proof obligation"
(Parse_Spec.thm_name ":"
-- Parse.term
>> open_data_goal);
这里我对两者使用了相同的数据更新逻辑,启动证明状态和 after_qed 回调。启动期间的逻辑允许在校样中途打印数据。
我相信我特别困惑的是如何在 after_qed 函数中更新顶级理论。实现这一目标的推荐方法是什么?
问题的最小工作示例:https://gist.github.com/BraeWebb/ac6b73354e61736e11836e655c69b507
非常感谢您的时间!
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。