时间戳

首页 > 解决方案 > 在 Isabelle/ML 中编写可变模式

isabelle - 在 Isabelle/ML 中编写可变模式

问题描述

我正在研究翻译方法：

apply(rewrite in "_ / ⌑" some_theorem)

进入ML，我想出了以下内容：

apply(tactic ‹
   let 
    val pat = [
      Rewrite.In,
      Rewrite.Term (@{const divide(real)} $ Var (("c", 0), \<^typ>‹real›) $ 
                      Rewrite.mk_hole 1 (\<^typ>‹real›), []),
      Rewrite.In      
    ]
    val to = NONE
   in
    CCONVERSION (Rewrite.rewrite_conv @{context} (pat, to) @{thms juanito_def}) 1 
   end
  ›)

在这里我是说“请与商中术语的任何子项进行模式匹配”。您可能会看到问题的先前编辑以查看有趣的模式。

使用图书馆的一些有趣的结论是

不明白

您能否解释一下以下策略的作用？

lemma
  assumes "Q (λb :: int. P (λa. a + b) (λa. a + b))"
  shows "Q (λb :: int. P (λa. a + b) (λa. b + a))"
  apply (tactic ‹
    let
      val (x, ctxt) = yield_singleton Variable.add_fixes "x" \<^context>
      val pat = [
        Rewrite.Concl,
        Rewrite.In,
        Rewrite.Term (Free ("Q", (\<^typ>‹int› --> TVar (("'b",0), [])) --> \<^typ>‹bool›)
          $ Abs ("x", \<^typ>‹int›, Rewrite.mk_hole 1 (\<^typ>‹int› --> TVar (("'b",0), [])) $ Bound 0), [(x, \<^typ>‹int›)]),
        Rewrite.In,
        Rewrite.Term (@{const plus(int)} $ Free (x, \<^typ>‹int›) $ Var (("c", 0), \<^typ>‹int›), [])
        ]
      val to = NONE
    in CCONVERSION (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) 1 end
  ›)
  apply (fact assms)
  done

第一个 Rewrite.Term 和变量的修复对我来说有点模糊。

标签： isabelleml

解决方案

推荐阅读