Re: [isabelle] Curried functions in binding operators



Dear Michael,

I am aware of your approach with combinators and have been using it in Isabelle for a while. Unfortunately, the simplifier does not preserve variable names as required, but I was able to solve that by writing a simproc that takes care of that. Unfortunately, the reasoning infrastructure sometimes spontaneously eta-expands (e.g., due to congruence rules) or eta-contracts (in particular method subst) terms. Then, new variable names are introduced or some of the combinators remain in the goal. So this does not work as smoothly as in HOL.

Maybe I could make your system work to preserve the variable names in my approach no. 2, but I don't see how I could avoid devising combinator rules for all combinations of splitting.

Cheers,
Andreas

On 12/02/15 23:47, Michael Norrish wrote:
My experience with this sort of situation is that sometimes you are just doomed.
  However, Konrad Slind and I did have a proof pearl in TPHOLs 2005

http://nicta.com.au/people/norrishm/attachments/bibliographies_and_papers/2005/tphols2005-pearl.pdf

where we presented a solution to a pretty similar problem.

I don't know if the Isabelle simplifier will preserve variable names when it
applies the relevant rules, but at least the approach doesn't require anything
more than standard h.o pattern rewriting.

Michael

On 12/02/15 20:54, Andreas Lochbihler wrote:
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






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