问题[isabelle](coding)

原始帖子：

我试图展示以下内容：

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}"])

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

我遇到了一个问题，我不知道这是否是伊莎贝尔管理集合理解的方式，或者我遇到了一个非常缓慢的时刻。

这个引理继续得很好

lemma "{x | x. P x} ∩ {x | x y. (Q x y)} = {x | x y. (P x) ∧ (Q x y)}"
  by auto

而这个却没有

lemma "{x | x y. (P x y)} ∩ {x | x y z. (Q x y z)} = {x | x y z. (P x y) ∧ (Q x y z)}"

两者之间一定有区别，但我看不出来。显然，我需要第二个，我的(P x y)和(Q x y z)非常复杂，我很难简化它。

像往常一样，我们非常感谢任何帮助（或将我引导到一些更健康的方向）。