目标转换 "rule"

Question

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

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

伊莎贝尔将其转化为三个子目标，我认为这应该是 dec_induct 的前提与我的目标统一。 dec_induct 是

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

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

?i ≤ a
?P ?i
⋀n. ⟦?i≤n； n < 一个； ?P n⟧ ⟹ ?P (Suc n)

但 Isabelle 实际上将其转换为的子目标是

?i ≤ ?j
P a
⋀n. ⟦?i≤n； n < j; P a⟧ ⟹ P a

Isabelle 是如何得到它的，我怎样才能让它按照我的预期执行感应？我意识到我应该使用 induct 方法，但我只是想了解规则的工作原理。

Answer 1

高阶统一会产生非常不直观的结果，尤其是当您有像 ?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 "↦", 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.[=18这样的模式时=]

目标转换 "rule"

Transformation of goals by "rule"

isabelle