为什么一个函数（类）的定义如下 definition nondecreasing_on :: "real set => (real => real) => bool"
where "nondecreasing_on S f <-> (ALL x:S. ALL y:S. x<=y --> f x <= f y)"
回报Inner syntax error⌂ Failed to parse pr
考虑以下Isabelle的最小工作示例，其中我定义了两个不同的函数func1和func2，它们应该模拟Eulers Totient函数。 奇怪的是，明显的定义是错误的，并通过引入∈ℕ导致正确的，但尚未确定的定义，只是略微改变了定义。 （我穿插代码的确切问题，因为这使得它可能更清楚我所指的）。 theory T
imports
Complex_Main
"~~/src/
在通过伊莎贝尔教程的练习中，我遇到了让我困惑的情况。为什么涉及预先列表的下列引理很容易被证明： lemma ‹count_list xs x = n ⟹ count_list (x # xs) x = Suc n›
by simp
虽然这个涉及追加的不是？ lemma ‹count_list xs x = n ⟹ count_list (xs @ [x]) x = Suc n›
在与Isabelle（版本2016-1）一起玩时，我遇到了以下奇怪的情况：我不能使用字母o作为变量或函数名称（大部分/全部？）上下文。下面的例子都失败，尽管大部分工作（全部？）英文字母表的其他字母： value o (* quoted version doesn't work either *)
definition invert :: ‹bool ⇒ bool› where
‹in
我是Isabelle的新手，我试图定义原始递归函数。我已经试过了，但我在乘法时遇到了麻烦。 datatype nati = Zero | Suc nati
primrec add :: "nati ⇒ nati ⇒ nati" where
"add Zero n = n" |
"add (Suc m) n = Suc(add m n)"
primrec mult :: "nati ⇒