Stream: Beginner Questions

Topic: fun _def or .simps?

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

Gergely Buday (Jan 11 2021 at 11:25):

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

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.

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

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

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?

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?

Lukas Stevens (Jan 11 2021 at 15:04):

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

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*)

Mathias Fleury (Jan 11 2021 at 15:45):

otherwise, exactly what Lukas said.

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

Gergely Buday (Jan 20 2021 at 08:52):

Thanks indeed.

Last updated: Apr 19 2024 at 20:15 UTC