如何在Isabelle的一组数字（nat）中找到最大元素。max函数无效，因为仅将其定义为最多包含两个元素。我对如何使用reduce like函数实现它有所了解，但是我不知道如何从集合中选择一个随机元素。
在Isabelle中,偶尔会出现一些重复的子目标.例如,假设以下证明脚本:
lemma "a ? a"
apply (rule conjI)
目标:
proof (prove): step 1
goal (2 subgoals):
1. a
2. a
有没有办法在原地消除重复的子目标,所以不需要重复证明？
我是伊莎贝尔的初学者,学习基础知识.令我惊讶的是,我刚才证明了
lemma "? ( ? x. P ) ? ( ? x. Q ) ? ? ? x. (P ? Q)"
apply ( auto )
done
在伊莎贝尔/ HOL.现在假设P和Q的范围超过任意谓词,这是错误的,只是将P实例化为x = 1,Q实例化为x = 2.
当然,错误必须在我身边,但我的误解在哪里？
我试图证明Isabelle/HOL的交换性是一种自定义的add功能.我设法证明了相关性,但我坚持这个.
定义add:
fun add :: "nat ? nat ? nat" where
"add 0 n = n" |
"add (Suc m) n = Suc(add m n)"
相关性证明:
lemma add_Associative: "add(add k m) z = add k (add m z)"
apply(induction k)
apply(auto)
done
交换的证明:
theorem add_commutativity: "add k m = add m k"
apply(induction k)
apply(induction m)
apply(auto)
我有以下目标:
goal (3 subgoals):
1. add 0 0 = add 0 0
2. ?m. add 0 m = add …证明一个简单的定理 我在证明中遇到了元级别的含义。可以拥有它们还是可以避免它们？如果我应该处理它们，这是正确的方法吗？
theory Sandbox
imports Main
begin
lemma "(x::nat) > 0 ? x = 0"
proof (cases x)
assume "x = 0"
show "0 < x ? x = 0" by (auto)
next
have "x = Suc n ? 0 < x" by (simp only: Nat.zero_less_Suc)
then have "x = Suc n ? 0 < x ? x = 0" by (auto)
then show "?nat. x = Suc nat ? 0 < x ? x = 0" by (auto)
qed …Suppose I have the following code in Isabelle:
lemma"[| xs@zs = ys@xs ;[]@xs = []@[] |] => ys=zs" (*never mind the lemma body*)
apply simp
done
In the above code, The simp method proves the lemma. I am interested to see and print out the detailed (rewriting /simplification) steps that the simplification method takes to prove this lemma ( and possibly be able to do the same for all the other proof methods). How this is possible?
I am using …
简而言之，我正在寻找一个定理证明器，它的底层逻辑支持多个子类型化/子类化机制。（我尝试使用 Isabelle，但它似乎没有为子类型化提供一流的支持。看到这个）
我想定义几种类型，其中一些是其他类型的子类/子类型。此外，每种类型可能是一种以上类型的子类型。例如：
Type A
Type B
Type C
Type E
Type F
C is subtype of A
C is also subtype of B
E and F are subtypes of B
PS：我正在再次编辑这个问题以更具体（因为有人抱怨是主题！）：我正在寻找定理证明者/证明帮助，我可以在其中以直接的方式定义上述结构（不是解决方法，因为这里有一些可敬的答案对它进行了亲切的描述）。如果我将类型作为类，那么似乎可以在 C++ 中轻松地制定子类型！所以我正在寻找一个正式的系统/工具，我可以在那里定义这样的子类型结构并且我可以推理？
非常感谢
我想在 Isabelle 中使用 nat 类型，但我想重载一些现有的定义，例如加法。我写了以下代码：
theory Prueba
imports Main HOL
begin
primrec suma::"nat ? nat ? nat" where
"suma 0 n = 0" |
"suma (Suc x) n = 0"
no_notation suma (infix "+" 65)
value "2 + (1 :: nat)"
我试图用一个总是输出 0 的新定义来重载加法。但是，当我评估2 + (1 :: nat)I get 时"Suc (Suc (Suc 0))" :: "nat"，这意味着 Isabelle 仍在使用来自 Nat 的加号定义。我怎样才能让它使用我对 + 的新定义？
谢谢
我想获得与该理论相关的 LaTeX 代码。以前的答案仅提供指向文档的链接。让我描述一下我做了什么。
我转到目录Hales.thy并执行isabelle mkroot，然后是isabelle build -D .，它生成了一个名为 document 的文件和一个*.pdf可疑（几乎）为空的文件。通过添加Hales.thy为参数来修改此命令未成功。
如果有人能简要描述所需的命令，我将不胜感激。