How to explicitly bind variables in an induction proof?

Question

I have a datatype and an inductive predicate over it (which is actually a small-step semantics of some transition system):

datatype dtype = E | A | B dtype

inductive dsem :: "dtype ⇒ dtype ⇒ bool" where  
  "dsem A E"
| "dsem (B E) E"
| "dsem d d' ⟹ dsem (B d) (B d')"

and also a function which is computed by case distinction:

fun f :: "dtype ⇒ nat" where
  "f E = 0"  
| "f A = 1"
| "f (B _) = 2"

I'm trying to prove some property about the inductive predicate, and assumptions also involve computing the value of f which doesn't participate in induction.

lemma
  assumes d: "dsem s s'"
    and h: "h s v"
    and v: "v = f s"
  shows "P v"
using d h
proof (induct rule: dsem.induct)

For the 3rd semantics rule Isabelle computes the subgoal

⋀d d'. dsem d d' ⟹ (h d v ⟹ P v) ⟹ h (B d) v ⟹ P v

where the value of s is lost so it is impossible to compute the value v. I can neither include v into the induction assumptions because then Isabelle generates the subgoal

⋀d d'. dsem d d' ⟹ (h d v ⟹ v = f d ⟹ P v) ⟹ h (B d) v ⟹ v = f (B d) ⟹ P v

where the induction hypothesis says v = f d which is incorrect since v = f (B d) in this case. Nor can I put v into arbitrary: ... because the value of v must be fixed throughout the proof.

It would be nice to have an explicit binding s = B d in the generated subgoal; unfortunately, the rule dsem.induct doesn't provide it.

Does anybody know a workaround for computing the value v in this case?

Does it help to rephrase your lemma as lemma "dsem s s' ⟹ (⋀v. ⟦ h s v ; v = f s ⟧ ⟹ P v)"? — John Wickerson
Since the fact v (i.e., v = f s) contains the variable s and you are doing induction on dsem s s' (which also contains s) there is no way around also including v into the induction assumptions. If the statement is not provable after doing so, you will have to reformulate it appropriately (whatever that means). — chris
You might try the proof with assumption v unfolded, i.e. lemma "dsem s s' ⟹ h s (f s) ⟹ P (f s)". This version is logically equivalent to the one stated in the question (and to the one suggested by John Wickerson above). — Brian Huffman

Mathieu Mathieu · Accepted Answer · 2014-01-31T18:40:33

It seems strange to me that v should be at the same time fixed and computed from s and that is what chris is saying in the comments.

If the solution Brian gives in the comments is what you want, it could duplicate the expression f s which could be big (and use s several times) and perhaps the point of the assumption v = f s was to avoid this.

A first workaround (that was possibly what Brian implicitly proposed) is to make Isabelle do the unfolding:

lemma
  assumes d: "dsem s s'"
    and h: "h s v"
    and v: "v = big_f s s"
  shows "P v"
using d h
unfolding v -- {* <<<< *}
proof (induct rule: dsem.induct)

A second workaround could be to abbreviate big_f instead of big_f s s:

lemma
  assumes d: "dsem s s'"
    and h: "h s (f s)"
    and v: "f = (λs. big_f s s)" -- {* <<<< *}
  shows "P (f s)"
using d h
proof (induct rule: dsem.induct)

How to explicitly bind variables in an induction proof?

1 Answers