*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Curried functions in binding operators*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Thu, 12 Feb 2015 10:54:08 +0100*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.4.0

Dear all, I have large subgoals with operators that bind variables like let, bind and integrals.

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

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

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"

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)

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

Thanks in advance for any pointers and ideas, Andreas

**Attachment:
Split.thy**

**Follow-Ups**:**Re: [isabelle] Curried functions in binding operators***From:*Michael Norrish

**Re: [isabelle] Curried functions in binding operators***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] libisabelle: Small Scala library to communicate with Isabelle
- Next by Date: [isabelle] Local_Theory.map_naming in locales
- Previous by Thread: Re: [isabelle] apply simp: Tactic failed
- 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