## Stream: Beginner Questions

### Topic: ✔ locale context & assumptions\goals

#### Robert Soeldner (Sep 05 2021 at 15:34):

I'm currently learning about locales. What is difficult for me to pick up, is the fact that the assumptions aren't included in the current proof goal. See the following toy example:

``````locale bla =
fixes a :: nat
assumes p: "a > 1"
begin

lemma "a > 1"
oops
end
``````

I would have guessed, Isabelle transforms the lemma to include the "locale assumptions" towards something like `a > 1 ==> a > 1`. Am I misunderstanding locales, ...?

#### Wolfgang Jeltsch (Sep 06 2021 at 00:08):

Between the `begin` and the `end`, you’re working in the locale context. In this context, Isabelle knows the locale assumptions as facts. For your example, this means that you don’t have to prove `a > 1 ⟹ a > 1` (after all, the lemma states just `a > 1`), but you have to prove `a > 1` and in doing so you can refer to the locale assumption by its name `p`. Thus you could write the following:

``````lemma "a > 1"
using p .
``````

#### Wolfgang Jeltsch (Sep 06 2021 at 10:13):

Let me add that Isabelle in fact does transform the lemma statement `a > 1` into the implication `a > 1 ⟹ a > 1`. However, it does so only after you have proved the lemma and only for the global context. Thus your goal is `a > 1`, which you can prove using the fact `p: a > 1`, and after you have proved this goal, Isabelle will give you the fact `a > 1` in the locale context and the fact`a > 1 ⟹ a > 1` in the global context.

#### Robert Soeldner (Sep 06 2021 at 19:28):

Thank you Wolfgang for the explanation.

#### Notification Bot (Sep 13 2021 at 15:18):

Robert Soeldner has marked this topic as resolved.

Last updated: Aug 13 2022 at 06:26 UTC