时间戳

首页 > 解决方案 > 用“规则”转化目标

isabelle - 用“规则”转化目标

问题描述

我正在尝试使用规则 dec_induct 对不为 0 的基本情况进行归纳证明，但我不明白 Isabelle 如何应用该规则。如果我陈述以下引理：

lemma test:
shows "P a"
proof (rule dec_induct)

Isabelle 将其转换为三个子目标，我认为这应该是与我的目标统一的 dec_induct 的前提。dec_induct 是

⟦?i ≤ ?j; ?P ?i; ⋀n. ⟦?i ≤ n; n < ?j; ?P n⟧ ⟹ ?P (Suc n)⟧ ⟹ ?P ?j

，所以我认为其结论中的 ?j 将与我的目标的“a”统一。也就是说，我期望以下三个子目标：

  1. ?i ≤ 一个
  2. ?P?i
  3. ⋀n. ⟦?i ≤ n; n <一个; ?P n⟧ ⟹ ?P (Suc n)

但伊莎贝尔实际上将其转换为的子目标是

  1. ?i ≤ ?j
  2. 帕
  3. ⋀n. ⟦?i ≤ n; n < ?j; 帕⟧⟹帕

Isabelle 是如何做到这一点的，我怎样才能让它按照我的预期进行归纳？我意识到我应该使用 induct 方法，但我只是想了解规则是如何工作的。

标签： isabelle

解决方案

高阶统一会产生非常不直观的结果，尤其是当您将模式?f ?x（即函数类型的示意图变量）应用于另一个示意图变量时。我对高阶统一了解不多，但似乎如果你?f ?x用类似的东西统一f x，你往往会得到统一器[?f ↦ λy. f x]而不是[?f ↦ f, ?x ↦ x]，这可能是你想要的。

您可以像这样进行试验，以准确了解可能的推断统一符是什么：

context
  fixes P :: "int ⇒ bool" and j :: int
begin

ML ‹
  local
    val ctxt = Context.Proof @{context}
    val env = Envir.init
    val ctxt' = @{context} |> Proof_Context.set_mode Proof_Context.mode_schematic
    val s1 = "?P ?j"
    val s2 = "P j"
    val (t1, t2) = apply2 (Syntax.read_term ctxt') (s1, s2)
    val prt = Syntax.pretty_term @{context}
    fun pretty_schem s = prt (Var ((s, 0), \<^typ>‹unit›))
    fun pretty_unifier (Envir.Envir {tenv, ...}, _) =
      tenv
      |> Vartab.dest
      |> map (fn ((s,_),(_,t)) => Pretty.block
             (Pretty.breaks [pretty_schem s, Pretty.str "↦&quot;, prt t]))
      |> (fn x => Pretty.block (Pretty.str "[" :: Pretty.commas x @ [Pretty.str "]"]))
  in
    val _ =
      Pretty.breaks [Pretty.str "Unifiers for", prt t1, Pretty.str "and", prt t2, Pretty.str ":"]
      |> Pretty.block
      |> Pretty.writeln
    val _ = 
      Unify.unifiers (ctxt, env, [(t1, t2)])
      |> Seq.list_of
      |> map pretty_unifier
      |> map (fn x => Pretty.block [Pretty.str "∙ ", x])
      |> map (Pretty.indent 2)
      |> Pretty.fbreaks
      |> Pretty.block
      |> Pretty.writeln
  end
›

输出：

Unifiers for ?P ?j and P j : 
  ∙ [?P ↦ λa. P j]

（免责声明：这只是说明发生了什么的实验代码，这不是干净的 Isabelle/ML 编码风格。）

总结一下：不要依赖高阶统一来计算函数变量的实例化，尤其是当你有像?f ?x.

推荐阅读