Re: [isabelle] Curried functions in binding operators



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


Attachment: signature.asc
Description: OpenPGP digital signature



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