## Stream: Beginner Questions

### Topic: referring to a definition

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

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

I see, thanks.

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

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

#### 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’. ;)

#### Mathias Fleury (Nov 11 2020 at 09:47):

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

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

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

#### Gergely Buday (Nov 11 2020 at 10:09):

Thanks, experts.

Last updated: Sep 11 2024 at 16:22 UTC