*To*: <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Curried functions in binding operators*From*: Michael Norrish <michael.norrish at nicta.com.au>*Date*: Fri, 13 Feb 2015 09:47:20 +1100*In-reply-to*: <54DC7840.3050100@inf.ethz.ch>*References*: <54DC7840.3050100@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.4.0

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**

**Follow-Ups**:**Re: [isabelle] Curried functions in binding operators***From:*Andreas Lochbihler

**References**:**[isabelle] Curried functions in binding operators***From:*Andreas Lochbihler

- Previous by Date: [isabelle] CICM 2015 Doctoral Programme [Call for Applications]
- Next by Date: Re: [isabelle] Curried functions in binding operators
- Previous by Thread: [isabelle] Curried functions in binding operators
- Next by Thread: Re: [isabelle] Curried functions in binding operators
- Cl-isabelle-users February 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list