*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Problems with transfer_prover*From*: Peter Lammich <lammich at in.tum.de>*Date*: Fri, 17 Jul 2015 17:07:23 +0200*In-reply-to*: <55A915AE.9080609@inf.ethz.ch>*References*: <55A915AE.9080609@inf.ethz.ch>

The first problem looks familiar to me. The type of option.bind is "'a option => ('a => 'b option) => 'b option" and its transfer rule is accordingly. However, in the first term, you specify just "op =" as relator, but bind wants something of the form "rel_option A". One workaround is to expand the "op =" - relators, based on their type, as much as possible, e.g., by simplification rules. Another workaround would be a custom "relator unification" procedure built into transfer, which is able to handle those cases ... I tried something similar for Autoref, but quickly gave up on it. -- Peter On Fr, 2015-07-17 at 16:48 +0200, Andreas Lochbihler wrote: > Dear experts of parametricity and the transfer package, > > I am struggling to prove parametricity of a big function defined by primitive recursion > over a largish tree datatype. I thought I'd use the transfer prover from the transfer > package. Unfortunately, it is driving me almost crazy as it appears as completely > non-deterministic to me when it is able to prove the parametricity statement and when not > (even if parametricity rules for all constants have been declared as [transfer_rule]). > > Here are two minimised examples which I do not understand. They are also in the attached > theory (tested with Isabelle2015 and Isabelle/c1b7793c23a3). Why does transfer_prover fail > to prove the rules? And what can I do to make transfer_prover work? > > 1. The problem seems to be related to how "op =" is treated as a relation. > > interpretation lifting_syntax . > consts f :: "nat â nat" > > lemma > "(op = ===> B ===> rel_option (rel_prod op = B)) > (Îx y. Option.bind x (Îx. Some (f x, y))) > (Îx y. Option.bind x (Îx. Some (f x, y)))" > by transfer_prover (* fails *) > > lemma (* same lemma, but the first "op =" is expanded to "rel_option op =" *) > "(rel_option op = ===> B ===> rel_option (rel_prod op = B)) > (Îx y. Option.bind x (Îx. Some (f x, y))) > (Îx y. Option.bind x (Îx. Some (f x, y)))" > by transfer_prover (* succeeds *) > > > > 2. Transfer prover is not able to prove the parametricity rule at all, even though all > rules are available (as the manual proof shows). > > datatype nonce = PNonce nat | ANonce "bool list" > datatype ('a, 'b, dead 'c) gpv = Done 'a > > lemma case_nonce_transfer [transfer_rule]: > "((op = ===> A) ===> (op = ===> A) ===> op = ===> A) case_nonce case_nonce" > by(auto simp add: rel_fun_def split: nonce.split) > > consts pnonce :: "nat â 's â nat â (bool list Ã 's, 'call, 'ret) gpv" > consts Î :: nat > lemma pnonce_transfer [transfer_rule]: "(op = ===> S ===> op = ===> rel_gpv (rel_prod op = > S) C) pnonce pnonce" sorry > > lemma "(op = ===> S ===> rel_gpv (rel_prod op = S) C) > (Înonce s. case nonce of PNonce x â pnonce Î s x | ANonce bs â Done (bs, s)) > (Înonce s. case nonce of PNonce x â pnonce Î s x | ANonce bs â Done (bs, s))" > apply transfer_prover > > apply(rule rel_funI)+ > apply(rule case_nonce_transfer[THEN rel_funD, THEN rel_funD, THEN rel_funD]) > apply(rule pnonce_transfer[THEN rel_funD, THEN rel_funD]) > apply(rule refl) > apply assumption > apply(rule rel_funI) > apply(rule gpv.ctr_transfer[THEN rel_funD]) > apply(erule (1) Pair_transfer[THEN rel_funD, THEN rel_funD]) > apply assumption > done > > Best, > Andreas

**References**:**[isabelle] Problems with transfer_prover***From:*Andreas Lochbihler

- Previous by Date: [isabelle] Problems with transfer_prover
- Next by Date: Re: [isabelle] Problems with transfer_prover
- Previous by Thread: [isabelle] Problems with transfer_prover
- Next by Thread: Re: [isabelle] Problems with transfer_prover
- Cl-isabelle-users July 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