Stream: Beginner Questions

Topic: fun _def or .simps?


view this post on Zulip Gergely Buday (Jan 11 2021 at 11:03):

This might occurred previously. Isabelle seems not to know about myfunc_def anymore, only myfunc.simps .

Is that the standard way of using its definition with keyword unfolding?

theorem skip_implies_SKIP:
assumes "skip c"
shows "c ∼ SKIP"
using assms
unfolding skip.simps

view this post on Zulip Gergely Buday (Jan 11 2021 at 11:25):

Only definition-s have _def? What about abbreviations? How can I refer to them in unfolding?

view this post on Zulip Mathias Fleury (Jan 11 2021 at 11:31):

Indeed only definitions have a _def. Primrec and fun don't have one. [1]

Abbreviations only exists at pretty-printing. So unfolding the content of the abbreviation works.

[1] the definition exists internally, but you should never use it.

view this post on Zulip Mathias Fleury (Jan 11 2021 at 11:35):

An example:

definition f :: ‹nat ⇒ nat ⇒ nat› where
  ‹f x  y = x + 3 + y›

abbreviation add4 :: ‹nat ⇒ nat› where
  ‹add4 ≡ f 1›

lemma ‹add4 x = x + 4›
  unfolding f_def by auto

view this post on Zulip Manuel Eberl (Jan 11 2021 at 11:36):

primrec does produce an accessible _def theorem in terms of the primitive recursor and can very occasionally be useful (e.g. when you want to show measurability, parametricity, etc.)

view this post on Zulip Gergely Buday (Jan 11 2021 at 15:00):

@Mathias Fleury in your example you unfold f's definition explicitly, but not abbreviation add4. Does that happen because of the simp ingredient of auto?

view this post on Zulip Gergely Buday (Jan 11 2021 at 15:03):

theorem skip_implies_SKIP:
assumes "skip c"
shows "c ∼ SKIP"
using assms
apply (simp)

results in

proof (prove)
goal (1 subgoal):

  1. ∀s. (c, s) ⇒ s ⟹ c ∼ SKIP

so it unfolds skip but not ∼

how can I do the latter?

view this post on Zulip Lukas Stevens (Jan 11 2021 at 15:04):

Isabelle never sees the abbreviations internally. They are unfolded while parsing (basically).

view this post on Zulip Mathias Fleury (Jan 11 2021 at 15:45):

Gergely Buday said:

Mathias Fleury in your example you unfold f's definition explicitly, but not abbreviation add4. Does that happen because of the simp ingredient of auto?

The abbrevation don't exist for Isabelle:

lemma ‹add4 x = x + 4›
(*goal is ‹add4 x = x + 4› *)
  unfolding f_def
(*goal is ‹1 + 3 + x = x + 4› *)
by auto
(*no goal*)

view this post on Zulip Mathias Fleury (Jan 11 2021 at 15:45):

otherwise, exactly what Lukas said.

view this post on Zulip Mathias Fleury (Jan 11 2021 at 15:55):

For ~: if it is the one from Big_Step. It is an abbreviation for ∀s t. (c,s) ⇒ t = (c',s) ⇒ t, aka your lemma is equivalent to:

theorem skip_implies_SKIP:
assumes "skip c"
shows "∀s t. (c,s) ⇒ t  =  (SKIP,s) ⇒ t"

You could something like:

theorem skip_implies_SKIP:
assumes "skip c"
shows "c ∼ SKIP"
  apply (intro allI)

or even apply (intro allI impI).

view this post on Zulip Gergely Buday (Jan 20 2021 at 08:52):

Thanks indeed.


Last updated: Sep 25 2021 at 09:17 UTC