Isabelle中使用continuous_on_diff与subst的连续性证明问题

核心证明目标 #

需要证明以下命题：

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

计划使用的引理 #

希望借助continuous_on_diff引理完成证明，该引理内容如下：

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

遇到的问题 #

• 针对核心目标，改写后使用subst方法未成功，即使显式指定参数仍然失败。观察引理实例，其形式完全匹配需求，但推测subst不适合处理这类非等式参数，改用rule方法也无法成功应用。
• 此外，难以证明以下命题：

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

补充说明 #

添加显式类型注解后，使用rule方法可完成证明，想了解这其中的差异是什么？

内容的提问来源于stack exchange，提问作者Squirtle