Robert Soeldner (Sep 05 2021 at 15:34): 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 .
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 facta > 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: Dec 21 2024 at 16:20 UTC