referring to a definition · Beginner Questions

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

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.

Gergely Buday (Nov 11 2020 at 09:34):

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

Mathias Fleury (Nov 11 2020 at 09:39):

Dmitriy Traytel (Nov 11 2020 at 09:43):

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

If the predicate is defined in a context where the flag inductive_internals is set, one gets access to the big_step_def theorem.

theory Scratch
imports "~~/src/HOL/IMP/Big_Step"
begin

no_notation big_step (infix "⇒" 55)
context notes [[inductive_internals]] begin
inductive
  big_step :: "com × state ⇒ state ⇒ bool" (infix "⇒" 55)
where
Skip: "(SKIP,s) ⇒ s" |
Assign: "(x ::= a,s) ⇒ s(x := aval a s)" |
Seq: "⟦ (c⇩1,s⇩1) ⇒ s⇩2;  (c⇩2,s⇩2) ⇒ s⇩3 ⟧ ⟹ (c⇩1;;c⇩2, s⇩1) ⇒ s⇩3" |
IfTrue: "⟦ bval b s;  (c⇩1,s) ⇒ t ⟧ ⟹ (IF b THEN c⇩1 ELSE c⇩2, s) ⇒ t" |
IfFalse: "⟦ ¬bval b s;  (c⇩2,s) ⇒ t ⟧ ⟹ (IF b THEN c⇩1 ELSE c⇩2, s) ⇒ t" |
WhileFalse: "¬bval b s ⟹ (WHILE b DO c,s) ⇒ s" |
WhileTrue:
"⟦ bval b s⇩1;  (c,s⇩1) ⇒ s⇩2;  (WHILE b DO c, s⇩2) ⇒ s⇩3 ⟧ 
⟹ (WHILE b DO c, s⇩1) ⇒ s⇩3"
end

thm big_step_def

end

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

Stream: Beginner Questions

Topic: referring to a definition

Gergely Buday (Nov 11 2020 at 09:29):