如何在引理证明后立即制作一个例子来测试 rev_app 。自定义引理的起始示例

Question

期望将子目标用于运行 let 定义的列表？ AA = [1,2] 和运行 rev_app 在此 aa 上并将值显示为 [2,1]

theory Scratch2
imports Datatype
begin
datatype 'a list  = Nil ("[]")
                  | Cons 'a "'a list" (infixr "#" 65)
(* This is the append function: *)
primrec app :: "'a list => 'a list => 'a list" (infixr "@" 65)
where
"[] @ ys = ys" |
"(x # xs) @ ys = x # (xs @ ys)"
primrec rev :: "'a list => 'a list" where
"rev [] = []" |
"rev (x # xs) = (rev xs) @ (x # [])"
primrec itrev :: "'a list => 'a list => 'a list" where
"itrev [] ys = ys" |
"itrev (x#xs) ys = itrev xs (x#ys)"
value "rev (True # False # [])"
lemma app_Nil2 [simp]: "xs @ [] = xs"
apply(induct_tac xs)
apply(auto)
done
lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
apply(induct_tac xs)
apply(auto)
done

(第 1 次试验)

lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
apply(induct_tac xs)
thus ?aa by rev_app
show "rev_app [1; 2]"

(二审)

value "rev_app [1,2]"

(第三次审判)

fun ff :: "'a list ⇒ 'a list" 
where "rev(xs @ ys) = (rev ys) @ (rev xs)"
value "ff [1,2]"
thus ?aa by rev_app
show "rev_app [1; 2]"

end

Answer 1

首先，你需要列表枚举的语法（我刚刚在 src/HOL/List.thy 文件中找到它）：

syntax
  -- {* list Enumeration *}
  "_list" :: "args => 'a list"    ("[(_)]")

translations
  "[x, xs]" == "x#[xs]"
  "[x]" == "x#[]"

那么，以下是您要搜索的内容之一吗？

命题 1：

lemma example1: "rev [a, b] = [b, a]"
  by simp

这个引理是通过应用方法simp使用的rev的定义规则来证明的，以重写左手项并证明等式的两侧相等。这是我更喜欢的解决方案，因为即使不使用 Isabelle 对其进行评估，您也可以看到该示例令人满意。

命题 2：

value "rev [a, b]" (* return "[b, a]" *)

这里和命题3中，我们只是使用命令value来计算rev。

命题 3：

value "rev [a, b] = [b, a]" (* returns "True" *)

前面的命题没有用到这个引理：

lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
  apply (induct_tac xs)
  by simp_all

备注：

作为一般原则，您不应单独导入 "Datatype" 包，而应导入 "Main"。
在您的第一次尝试中，您混合了 "apply"（应用...）和 "structured proof"（因此...）样式
"thus ?aa" 如果 "?aa" 是 "[1,2]" 是没有意义的，因为 "thus" 的参数应该是一个子目标，即。具有布尔值的命题。
为了评估，命令 "value" 使用 ML 执行，或者如果失败，则通过评估进行归一化。
在示例 1 中，您可以使用自定义证明和引理（例如：by (simp add:rev_app)

如何在引理证明后立即制作一个例子来测试 rev_app 。自定义引理的起始示例

how to make an example to test the rev_app immediately after lemma proved. an starting example for custom lemma

isabelle