主页 / coding / 问题 / 79551444
Accepted
Squirtle
Asked: 2025-04-03 03:45:38 +0800 CST

使用 Continuous_on_diff 与 subst (Isabelle)

  • 772

原始帖子：

我试图展示以下内容：

have "continuous_on {x. 0 < x} (λx. 12 * x⇧2 - 1)"

我想使用以下引理：

thm continuous_on_diff
----------------------------------------------------------------------------------------------------------
Output:
⟦continuous_on ?s ?f; continuous_on ?s ?g⟧ ⟹ continuous_on ?s (λx. ?f x - ?g x)

但也许这不是正确的形式所以我尝试这个：

 have "continuous_on {x. 0 < x} (λx. (λw . 12 * w⇧2) x  - (λw . 1)x)"
                      apply(subst continuous_on_diff)

但这不起作用所以我使它更加明确：

have "continuous_on {x. 0 < x} (λx. (λw . 12 * w⇧2) x  - (λw . 1)x)"
      apply(subst continuous_on_diff[where f = "(λw . 12 * w⇧2)" and g= "(λw . 1)" and s = "{x. 0 < x}"])

然而，这仍然不起作用，然而，当我检查定理时：

thm continuous_on_diff[where f = "(λw . 12 * w⇧2)" and g = "(λw . 1)" and s = "{x. 0 < x}"]
-------------------------------------------------------------------------------------------
Output:
⟦continuous_on {x. 0 < x} (λw. 12 * w⇧2); continuous_on {x. 0 < x} (λw. 1)⟧ ⟹ continuous_on {x. 0 < x} (λx. 12 * x⇧2 - 1)

这似乎正是我想要的。我唯一能想到的是“subst”不适合处理非等式风格的参数，而且我也无法让“rule”工作。

任何帮助都将不胜感激！

类似地，我也在努力证明：

"have continuous_on {x. 0 < x} ((*) 6)"

编辑：当我使输入信息更加明确时，例如：

have "continuous_on {x :: real. 0 < x} (λx. (λw . 12 * w⇧2) x  - (λw . 1)x)"
                      apply(rule continuous_on_diff[where f = "(λw . 12 * w⇧2)" and g = "(λw . 1)" and s = "{x. 0 < x}"])

这使得它可证明。但是有什么区别呢？

isabelle

1 个回答

  1. Best Answer

    我不明白你为什么要使用subst。该subst方法用于代换；只有当你给出一个方程时它才有效。你的意思是使用rule？那会更有意义。

    无论如何，证明连续性的常用方法就是做一些类似的事情apply (auto intro!: continuous_intros)。定理列表continuous_intros是专门为消除明显的连续性证明义务而设计的。当然，只有当您的目标中的所有函数在中都有相应的规则时，它才会起作用continuous_intros，并且您可能会得到出现的附带条件。但它通常非常有效。

    对于解析性、全纯性以及最重要的导数（analytic_intros，， ） holomorphic_intros，也有类似的规则集derivative_eq_intros。

    还要注意，您可能必须注释类型。如果您只是写，continuous_on {x. 0 < x} ((*) 6)那么 Isabelle 将为该函数派生出一个非常通用的类型，您可能无法证明这一点。在其中添加类型注释（real，complex，无论您想要什么），例如采用以下方式之一：

    continuous_on {x::real. 0 < x} ((*) 6)
continuous_on {x. 0 < x} ((*) (6::real))
continuous_on {x. 0 < x} ((*) 6 :: real ⇒ real)

    以下作品：

    lemma "continuous_on {x. 0 < x} ((*) 6 :: real ⇒ real)"
  by (auto intro!: continuous_intros)
    • 1

相关问题