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?

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

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

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)

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: Sep 25 2022 at 23:25 UTC