ORIGINAL POST:

I'm trying to show the following:

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

And I would like to use the following lemma:

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

But maybe this isn't quite the right form so I try this:

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

But this didn't work so I made it even more explicit with:

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

Yet even this did not work, however when I check the theorem:

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)

This appears to be exactly what I want. The only thing I can think is that "subst" isn't suited to handle non-equational style arguments, and I can't get "rule" to work either.

Any help is much appreciated!

In a similar fashion, I'm also struggling to prove:

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

EDIT: When I made the typing information more explicit, as in:

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

This made it provable. But what's the difference?

ORIGINAL POST:

I'm trying to show the following:

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

And I would like to use the following lemma:

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

But maybe this isn't quite the right form so I try this:

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

But this didn't work so I made it even more explicit with:

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

Yet even this did not work, however when I check the theorem:

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)

This appears to be exactly what I want. The only thing I can think is that "subst" isn't suited to handle non-equational style arguments, and I can't get "rule" to work either.

Any help is much appreciated!

In a similar fashion, I'm also struggling to prove:

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

EDIT: When I made the typing information more explicit, as in:

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

This made it provable. But what's the difference?

• isabelle

1 Answer 1

I don't understand why you are trying to use subst. The subst method is for substitution; it only works when you give it an equation. Did you mean to use rule? That would make more sense.

In any case, the usual approach to proving continuity is to just do something like apply (auto intro!: continuous_intros). The theorem list continuous_intros is designed specifically to make obvious continuity proof obligations just go away. Of course it only works if all the functions you have in your goal have a corresponding rule in continuous_intros, and you might get side conditions that arise. But it usually works extremely well.

There are also similar sets of rules for things like analyticity, holomorphicity, and most importantly derivatives (analytic_intros, holomorphic_intros, derivative_eq_intros).

Also note that you're probably going to have to annotate types. If you just write continuous_on {x. 0 < x} ((*) 6) then Isabelle will derive a very generic type for that function, and you will probably not be able to prove it. Put a type annotation in there (real, complex, whatever you intended), e.g. in one of the following fashions:

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

The following works:

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