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

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

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.

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

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

@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?

theorem skip_implies_SKIP:

assumes "skip c"

shows "c ∼ SKIP"

using assms

apply (simp)

results in

proof (prove)

goal (1 subgoal):

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

so it unfolds skip but not ∼

how can I do the latter?

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

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

otherwise, exactly what Lukas said.

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

.

Thanks indeed.

Last updated: Dec 07 2023 at 20:16 UTC