*To*: Joshua Schneider <dev at jshs.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Lifting and datatypes with dead arguments*From*: Andrei Popescu <A.Popescu at mdx.ac.uk>*Date*: Mon, 27 Mar 2017 19:21:09 +0000*Accept-language*: en-GB, en-US*Authentication-results*: jshs.de; dkim=none (message not signed) header.d=none;jshs.de; dmarc=none action=none header.from=mdx.ac.uk;*In-reply-to*: <20170327154428.GA1224@josh-linux>*References*: <20170324090804.GA2107@jshs-laptop.fritz.box> <VI1PR0101MB214361006458F90C2C958EB2B7300@VI1PR0101MB2143.eurprd01.prod.exchangelabs.com>, <20170327154428.GA1224@josh-linux>*Spamdiagnosticmetadata*: NSPM*Spamdiagnosticoutput*: 1:99*Thread-index*: AQHSpy9J+1vBH1ZlJECuUSgKBuc6VA==*Thread-topic*: [isabelle] Lifting and datatypes with dead arguments

Hi Joshua, Thanks for the theory file. You are up to some very nice and useful results. :-) However, to approach the case of arbitrary (nested) datatypes, I don't think fixpoint induction for constructors is very helpful. Over the last few years, we have built powerful abstractions that you can use here: Given a BNF ('a,'b) F, there is a generic way to construct its datatype BNF, 'a D, and its codatatype BNF, 'a C, i.e., such that: (1) ('a, 'a D) F is isomorphic to 'a D, (2) ('a, 'a C) F is isomorphic to 'a C, (3) suitable (co)induction and (co)recursion principles hold for these. Our main motivation behind BNFs was to provide enough structure for being able to construct 'a D and 'a C abstractly (without caring about how the underlying F looks like). Note that this situation covers the nested case, since F can be any BNF. The familiar high-level case distinction, induction, recursion etc. made available to the users is essentially implemented as "syntactic sugar" on top of these abstract constructions (performed for n mutually (co)recursive fixpoint equations like the above). This is all described in our paper: http://andreipopescu.uk/pdf/LICS2012.pdf So, IMO, the best^[*] way to go is: --(1) Prove the quotient theorem under abstract assumptions, using BNFs and their fixpoints. You will see that the abstract induction theorem encodes your fixpoint "apply_T_ctors" induction as structural induction, so you will not need a generalized quotient predicate. --(2) Then either manually instantiate to particular (co)datatypes of interest (it is very easy!), or, more ambitiously, automate the instantiation in Isabelle/ML. If you are interested in going on this path (perhaps after having consulted the above paper), I can set up for you a theory file with the relevant structure for pursuing point (1). Best regards, Andrei PS. By "best," I mean "most interesting scientifically and most useful for Isabelle." ________________________________ From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Joshua Schneider <dev at jshs.de> Sent: 27 March 2017 16:44 To: cl-isabelle-users at lists.cam.ac.uk Subject: Re: [isabelle] Lifting and datatypes with dead arguments Hi Andrei, Thank you for working through the proof! It seems like the transfer of the equivalence relation is the trickiest part, which was the missing piece in my own attempt at proving this. I would also like to generalise the quotient mapping to arbitrary nested BNFs, but I don't see how that would work based on your solution. I recently talked to Andreas Lochbihler about the problem, and he suggested a fixed-point induction. I have now implemented that idea (see attached theory), using a version of the Quotient predicate which is restricted to some subset of the abstract type. I think that it is promising, because the core of the proof is compositional with respect to the functor structure. I have not tried to scale it to larger examples, though. Do you think that this is a worthwhile path towards automation, or do you have something different in mind? Cheers, Joshua

**References**:**[isabelle] Lifting and datatypes with dead arguments***From:*Joshua Schneider

**Re: [isabelle] Lifting and datatypes with dead arguments***From:*Andrei Popescu

**Re: [isabelle] Lifting and datatypes with dead arguments***From:*Joshua Schneider

- Previous by Date: Re: [isabelle] Lifting and datatypes with dead arguments
- Next by Date: Re: [isabelle] Isabell HOLCF tutorial
- Previous by Thread: Re: [isabelle] Lifting and datatypes with dead arguments
- Next by Thread: [isabelle] Fwd: CFP: Automated Reasoning Workshop, 3-4 April 2017, University of Bristol
- Cl-isabelle-users March 2017 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