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.
big_step
is an inductive predicate. Inductive predicates don't have a definition. You can use induction big_step.induct
.
I see, thanks.
The closest thing to a definition is big_step.simps
(which is recursive and is therefore not safe to use as a simp rule!)
Section 3.5 of http://isabelle.in.tum.de/dist/Isabelle2020/doc/prog-prove.pdf
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
I pondered whether to say this, but decided against it since this thread is called ‘beginner questions’. ;)
I have never used inductive_internals
and completely forgot that it exists :surprise:
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.
(To clarify: this is not important for actually proving things, but important for having trust in the system.)
Thanks, experts.
Last updated: Dec 07 2024 at 16:22 UTC