*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Problems with transfer_prover*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Fri, 17 Jul 2015 16:48:14 +0200*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.7.0

Dear experts of parametricity and the transfer package,

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

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

**Attachment:
Transfer_Prover_Problem.thy**

**Follow-Ups**:**Re: [isabelle] Problems with transfer_prover***From:*Peter Lammich

**Re: [isabelle] Problems with transfer_prover***From:*OndÅej KunÄar

**[isabelle] which library should be imported in order to prove these***From:*Mandy Martin

- Previous by Date: [isabelle] REMS postdoc researcher / research-engineer positions
- Next by Date: Re: [isabelle] Problems with transfer_prover
- Previous by Thread: [isabelle] REMS postdoc researcher / research-engineer positions
- 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