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, ...?

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 .
```

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.

Thank you Wolfgang for the explanation.

Robert Soeldner has marked this topic as resolved.

Last updated: Sep 25 2022 at 23:25 UTC