Stream: Beginner Questions

Topic: ✔ locale context & assumptions\goals


view this post on Zulip 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, ...?

view this post on Zulip 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 .

view this post on Zulip 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 facta > 1 ⟹ a > 1 in the global context.

view this post on Zulip Robert Soeldner (Sep 06 2021 at 19:28):

Thank you Wolfgang for the explanation.

view this post on Zulip Notification Bot (Sep 13 2021 at 15:18):

Robert Soeldner has marked this topic as resolved.


Last updated: Mar 29 2024 at 12:28 UTC