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):
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 2024 at 16:22 UTC