[isabelle] Curried functions in binding operators



Dear all,

I have large subgoals with operators that bind variables like let, bind and integrals.
These operators are just higher-order functions which use the standard function abstraction to implement the binding. Unfortunately, lemmas about these operators no longer apply when the bound variable is a tuple which is split up into its components using patterns (internally implemented via case_prod), because the case_prod destroys the pattern. Here is an example to illustrate the problem (also attached as a theory file). The bind operation on option commutes.

notation Option.bind (infixr "Â=" 54)

lemma bind_commute: "x Â= (Îx. y Â= (Îy. f x y)) = y Â= (Îy. x Â= (Îx. f x y))"
  by(cases "x = None â y = None") auto

Now, I would like to apply this lemma in a situation where the "x" is a tupled option and the "Îx" splits the tuple into its components say "Î((b, c), d)". For example,

have "f x Â= (Î((b, c), d). g x Â= h b d) = foo"
  apply(subst bind_commute)

Of course, the subst method fails here, because between the two binds there are the case_prod functions, i.e., the pattern does not match. I have not been able to find a satisfactory solution for this problem. I expect that others have the same problem and hope that they share their solutions with me.

Here are my attempts so far:

1. apply(unfold split_def)
This works but the resulting subgoal is

  "g x Â= (Îy. f x Â= (Îx. h (fst (fst x)) (snd x) y)) = foo

which is much harder to read than the desired

  "g x Â= (Îy. f x Â= (Î((b, c), d). h b d y)) = foo"

(Think of f, g, and h being huge terms with many occurrences of b and d.) Moreover, the variable names b and d get lost,

2. Derive a commutativity rule for each way of splitting:

lemma bind_commute_ss:
  "x Â= (Î((a, b), c). y Â= h a b c) = y Â= (Îy. x Â= (Î((a, b), c). h a b c y))"
  unfolding split_def by(rule bind_commute)

Now, I can use apply(subst bind_commute_ss), but the variable names are still lost. The new subgoal is
  "g x Â= (Îy. f x Â= (Î((a, b), c). h a c y)) = foo"
instead of
  "g x Â= (Îy. f x Â= (Î((b, c), d). h b d y)) = foo"
Moreover, I have to derive a new rule for each way in which the tuples are split up.

3. State the desired result as an intermediate step:

  have "f x Â= (Î((b, c), d). g x Â= h b d) = g x Â= (Îy. f x Â= (Î((b, c), d). h b d y))"
    by(unfold split_def)(rule bind_commute)
  also have "... = foo"

When f, g, and h are huge terms, this is very inconvenient, especially when I am in the middle of an apply script.

Thanks in advance for any pointers and ideas,
Andreas

Attachment: Split.thy
Description: application/extension-thy



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.