时间戳

首页 > 解决方案 > thy_goal_defn 关键字 qed 后更新理论数据

isabelle - 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

我的实现方法如下：

  1. 在理论开始时声明关键字
theory ProvedData
  imports Main
keywords
  "data" :: thy_goal_defn and
  "print_data" :: diag
begin
  1. 实现一个简单的结构来存储数据。这里的合并逻辑不完整，但我怀疑不是罪魁祸首，因为我能够使用 ML 代码模拟向结构添加多个元素。
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;
  1. 最后，我实现了一个简单的函数来启动证明状态并更新理论数据。
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

非常感谢您的参与！

标签： isabelle

解决方案

推荐阅读