## 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

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: Dec 07 2023 at 20:16 UTC