问题标签 [isar]

我有理论文件 Test_Func.thy，我在 Isabelle src/HOL 中复制了它，它定义了函数 add_123：

然后我有 Test_1.thy 文件，其中包含导入和引理：

奇怪的是，apply(simp)还是apply(auto)失败了Failed to apply proof method。没有关于未定义函数或不可见函数的错误消息，但是当函数定义和关于它的引理被分成两个文件时，这种简单的证明不起作用。

所以 - 这个问题可能有不同的问题和不同的解决方案 - 也许是因为我没有导入理论文件的经验，或者我对战术选择和应用感到困惑。

我在 Isabelle 2021 的 jEdit 中观察到这一点，但在不同的设置中，我可以看到 Isabelle 2020 也发生了同样的事情。

当我有很多假设时，有时我会得到很多使证明混乱的临时名称。

我在谈论这样的事情：

你能想象它是如何演变的吗？许多语句的名称，在事物的宏大计划中，不值得命名，但仍然被命名，因为我们需要稍后引用它们。

另一方面，如果我们使用所有当前假设，多余的名称不会使证明混乱：

当然，using assumptions伊莎贝尔不是一个有效的说法。我知道 about assms，它引用了该assumes子句，但我不知道是否存在这样的事情 for assume。

有没有办法引用由创建的所有当前假设assume？

有时在证明中我发现自己需要累积结果，但也需要使用最后的结果，所以我最终使用 " also then" 来达到这个目的：

我觉得有更多我不知道的惯用方法。另一方面，这可能是标准的做法，并受到社区的鼓励。

因此，鉴于此，我有两个问题：

1. 不鼓励使用“ also then”？
2. 如果是这样，我可以在使用它们时使用哪些替代方法来累积结果？

为了学习目的，我试图重新创建自然数的简化版本（因为它涉及归纳定义、递归函数等......）。然而，在那个过程中，我陷入了一些我认为非常微不足道的事情。

基本上，我有一个自然数的natt定义 ' ' 和一个 ' <' 关系的定义：

从这些，我试图证明<关系的 3 个基本属性：

1. 非反身性：~ (a < a)
2. 非对称：a < b ⟹ ~ (b < a)
3. 传递性：a < b ⟹ b < c ⟹ a < c

我能够证明第一个，但不能证明其他。更让我吃惊的是，有一些子引理可以帮助解决这些问题，例如Succ a < b ⟹ a < b或a < b ⟹ a < Succ b，这似乎更加微不足道，但即使经过多次尝试a < b ∨ a = b ∨ b < a，我也无法证明。似乎只有其中一个（包括and ）足以证明其余部分，但我无法证明其中任何一个。2.3.

我主要是尝试使用归纳法。加上我自己做出定义的事实，有两种可能性 - 我的定义是错误的，并且没有所需的属性，或者我缺少一些方法/参数。所以，我有两个问题：

1. 我的定义是否错误（即它不能准确表示<并且缺少所需的属性）？如果是这样，我该如何解决？
2. 如果不是，我如何证明这些看似微不足道的性质？

就上下文而言，我目前的尝试是通过归纳，我可以证明基本情况，但总是陷入归纳情况，不知道在哪里进行假设，例如在这个例子中：

假设我有一个前提，例如A ∨ B ∨ C，并且想证明P。证明它的自然方法是证明A ⟹ P和。但是，它适用于 2 种情况，因此我必须应用两次：B ⟹ PC ⟹ PdisjE

当然，现在我可以证明我自己的lemma disjE_3 [rulify]: assumes "P ∨ Q ∨ R" "P ⟹ A" "Q ⟹ A" "R ⟹ A" shows "A"并改用它，这将产生一个更具可读性的证明：

另一方面，如果我有 4 例、5 例或 10 例怎么办？为您可能需要的每个案例创建规则似乎非常不方便。尽管您可以一次应用多个规则，proof (rule disjE disjE)但在这种情况下似乎并没有削减它。

那么，有没有办法通过尽可能多地应用规则来将子目标减少到“最小形式”？

我有带有非归纳定义的 Isabelle 理论（我想对避免归纳的算法进行建模，就像工业开发人员通常所做的那样）和为此定义说明的引理：

当前的证明状态已经生成了 3 个目标，所有这些目标都与归纳有关（直接应用 simp 失败并显示Failed to apply proof method）：

我的问题是 - 是否有可以避免归纳的证明方法和策略，并且可以应用于这个简单的案例？也许与simp战术家族有关？

我正在玩 Isabelle/HOL 教程中的一个示例，以更好地理解 Isar 和 Tactics 证明之间的对应关系。

这是一个有效的版本：

我想实例化converse_rtrancl_into_rtrancl哪些证明(?a, ?b) ∈ ?r ⟹ (?b, ?c) ∈ ?r^* ⟹ (?a, ?c) ∈ ?r^*。
但是如果没有看似荒谬的apply (subgoal_tac "1=(1::nat)")线，这个错误

如果我完全实例化规则，apply (rule converse_rtrancl_into_rtrancl[of z y r x])这将变为Clash: z__ =/= ya__.

这给我留下了三个问题：为什么这个特定案例会破裂？我该如何解决？由于我无法真正理解 unify_trace_failure 消息想要告诉我什么，我如何才能弄清楚在这些情况下出了什么问题。

我正在尝试编写一个函数balanced，以便balanced n w当且仅当S (an @ w)列表包含n相同字母列表的数量时才是正确的。对于函数的第三个方程，"(balanced n w = S (a # m @ w)) ⟹ (balanced (Suc n) w = S (a # a # m @ w))"我得到错误“变量“m”仅出现在右侧：”即使m左侧有。我能想到的唯一解决方案是以另一种方式编写函数，但目前无法想到如何。

该函数balanced被定义为balanced n w = S (replicate n a @ w) wherereplicate n a返回[a,a,...,a]长度为 n 的列表。我必须证明balanced n w ⟹ S (replicate n a @ w)，S (replicate n a @ w) ⟹ balanced n w并且在这两方面都遇到了麻烦。

因为balanced n w ⟹ S (replicate n a @ w)我试图证明如下。

对于第三种情况，我得到了子目标 (balanced n w ⟹ S (replicate n a @ w)) ⟹ balanced (Suc n) (b # w) ⟹ S (replicate (Suc n) a @ b # w)，即使使用 . 也未能证明它try。假设 S (x @ y) ⟹ S (x @ [a,b] @ y)会解决问题，但我也找不到证明它的方法。有没有其他方法可以证明或可以证明 S (x @ y) ⟹ S (x @ [a,b] @ y)？

因为S (replicate n a @ w) ⟹ balanced n w 我试图证明如下。

我无法证明案例 3、4_1 和 4_2 的原因显然是因为所有 3 个子目标的假设总是错误的。例如，我为案例 4_2 得到的子目标是 S (replicate 0 a @ b # va) ⟹ balanced 0 (b # va). 因为balanced 0 (b # va)总是假的。我需要证明这S (replicate 0 a @ b # va)也总是错误的。有没有办法在不改变定义的情况下做到这一点S ？

是否可以选择在 Isar 中使用相同类型的对象创建多个集合？

伊萨尔文档：https ://isar.dev/

我如何创建单个集合：

我想要第二个 ProgramModel 集合，但我不能将另一个 @Collection() 添加到同一个模型。