Stream: Beginner Questions

Topic: cases of an inductive definition

Gergely Buday (Aug 25 2020 at 14:28):

inductive trc :: "(conf ⇒ conf ⇒ bool) ⇒ (conf ⇒ conf ⇒ bool)" for virtm :: "conf ⇒ conf ⇒ bool"
where
refl: "trc virtm c c" |
step: "virtm c d ⟹ (trc virtm) d e ⟹ (trc virtm) c e"

definition trcvm where "trcvm = rtranclp vm"

definition trcvm' where "trcvm' = trc vm"

notation trcvm' (infix "->>" 80)

lemma assumes "(c -> d)" shows "(c ->> d)"
proof -
have "d ->> d" using trc.refl trcvm'_def by simp
then show "?thesis" using assms trc.step trcvm'_def by simp
qed

lemma assumes "c ->> d"
assumes "d ->> e"
shows "c ->> e"
proof (induct rule: trc.induct)

I used my own transitive closure definition as I was better able to refer to its parts than of the more professional HOL rtanclp predicate definition.

I stuck at how to properly set up induction for the "c ->> e" goal. Do you have an advice?

Mathias Fleury (Aug 25 2020 at 15:46):

I can give you the answer:

lemmas trcvm'_induct =
  trc.induct[of vm, unfolded trcvm'_def[symmetric], consumes 1, case_names refl stop]

lemma assumes "c ->> d"
assumes "d ->> e"
shows "c ->> e"
  using assms
proof (induct rule: trcvm'_induct)

but it would be more interesting for you to follow the Isabelle part of the concrete semantics where you would learn that you have to unfold definition before doing induction or define your own induction principle (as I do here)

EDIT: I forgot to name the cases

Gergely Buday (Aug 26 2020 at 06:09):

Thanks. From your solution it seems that this is far from trivial and so I better asked this.

Mathias Fleury (Aug 26 2020 at 07:36):

The easier solution is

lemma assumes "c ->> d"
assumes "d ->> e"
shows "c ->> e"
  using assms unfolding trcvm'_def
proof (induct rule: trc.induct)

(or variants with unfolding only one of the ->> symbols)

Gergely Buday (Aug 26 2020 at 07:47):

This is more close to what I thought I should do: "unpack the definition of ->> and prove by induction". I see that I should unpack, i.e. unfold the definition of trcvm' instead and then I can use trc's induction rule directly, without the square bracket magic.

Last updated: Dec 21 2024 at 16:20 UTC