Stream: Beginner Questions

Topic: referring to a definition


view this post on Zulip Gergely Buday (Nov 11 2020 at 09:29):

I am to use a definition in a proof:

theory Exercise7_1

imports "~~/src/HOL/IMP/Big_Step"

begin

fun assigned :: "com ⇒ vname set" where
"assigned SKIP = {}"
| "assigned (Assign var _) = { var }"
| "assigned (Seq command1 command2) = (assigned command1) ∪ (assigned command2)"
| "assigned (If condition then_branch else_branch) = (assigned then_branch) ∪ (assigned else_branch)"
| "assigned (While condition body) = assigned body"

theorem var_not_mod:
assumes "(c,s) ⇒ t"
assumes "x ∉ assigned c"
shows "s x = t x"
using assms
unfolding big_step_def
proof -

Interestingly, if you CTRL-click on =>, there is a definition called big_step, so I tried

 unfolding big_step_def

but Isabelle says

 Undefined fact: "big_step_def"

How should I do this? In another proof such a way of thinking worked, adding _def to the name of an inductive definition.

view this post on Zulip Mathias Fleury (Nov 11 2020 at 09:34):

big_step is an inductive predicate. Inductive predicates don't have a definition. You can use induction big_step.induct.

view this post on Zulip Gergely Buday (Nov 11 2020 at 09:34):

I see, thanks.

view this post on Zulip Mathias Fleury (Nov 11 2020 at 09:35):

The closest thing to a definition is big_step.simps (which is recursive and is therefore not safe to use as a simp rule!)

view this post on Zulip Mathias Fleury (Nov 11 2020 at 09:39):

Section 3.5 of http://isabelle.in.tum.de/dist/Isabelle2020/doc/prog-prove.pdf

view this post on Zulip Dmitriy Traytel (Nov 11 2020 at 09:43):

Inductive predicates don't have a definition.

Well, they do. It is simply hidden from users by default (for good reasons; the induction principle and the intro and elim rules should suffice in most cases).

Expert spoiler

view this post on Zulip Manuel Eberl (Nov 11 2020 at 09:44):

I pondered whether to say this, but decided against it since this thread is called ‘beginner questions’. ;)

view this post on Zulip Mathias Fleury (Nov 11 2020 at 09:47):

I have never used inductive_internals and completely forgot that it exists :surprise:

view this post on Zulip Dmitriy Traytel (Nov 11 2020 at 09:49):

It is important for beginners to understand that in Isabelle/HOL everything (except for definition and typedef) has a definition in terms of these lower-level primitives. Often these internal definitions are hidden, but they do exist.

view this post on Zulip Dmitriy Traytel (Nov 11 2020 at 09:50):

(To clarify: this is not important for actually proving things, but important for having trust in the system.)

view this post on Zulip Gergely Buday (Nov 11 2020 at 10:09):

Thanks, experts.


Last updated: Aug 13 2022 at 06:26 UTC