Isabelle 中是否有像“∃x.a^x = b”这样的引理？

【问题标题】：Is there a lemma like "∃x. a^x = b" proved in Isabelle?Isabelle 中是否有像“∃x.a^x = b”这样的引理？
【发布时间】：2017-01-02 01:44:47
【问题描述】：

有谁知道类似的引理在哪里

∃(x::real). a^x = (b::real)

可能会被发现？我在“查询”中找不到类似的东西，但它看起来很方便。

【问题讨论】：

【解决方案1】：

您需要对a 和b 进行更多假设，并且您需要使用powr 运算符而不是^，因为^ 仅适用于n-th 幂，其中@987654327 @ 是一个自然数。另一方面，powr 用于任何非负实数的任何其他实数的幂。（或类似的复数）

lemma 
  fixes a b :: real
  assumes "a > 0" "a ≠ 1" "b > 0"
  shows   "∃x. a powr x = b"
proof
  from assms show "a powr (log a b) = b" by simp
qed

【讨论】：