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, ...?
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: Aug 13 2022 at 06:26 UTC