*To*: Lars Hupel <hupel at in.tum.de>*Subject*: Re: [isabelle] BNFs and sort constraints*From*: Dmitriy Traytel <traytel at inf.ethz.ch>*Date*: Wed, 23 May 2018 14:35:19 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Jasmin Blanchette <jasmin.blanchette at inria.fr>*In-reply-to*: <989C1719-FDE3-45A1-9936-3A03DF30ADFC@inria.fr>*References*: <101441f2-3dad-5ee9-1b13-e7e56bec7b9b@in.tum.de> <989C1719-FDE3-45A1-9936-3A03DF30ADFC@inria.fr>

Hi Lars, let me refine Jasmin's anwer. > On 22 May 2018, at 21:57, Jasmin Blanchette <jasmin.blanchette at inria.fr> wrote: > > Hi Lars, > >> Could somebody shed some light onto how this works? I looked at some of >> the papers but didn't find anything. > > I can answer Observation 4, which involves some of my code. > > BNF type variables may not have sort constraints. "map_id" is part of the BNF structure, so it accordingly doesn't have sort constraints. More high-level theorems and constants are declared with the sort constraints. To overgeneralize a bit, Dmitriy's low-level BNF code doesn't like sort constraints, whereas my higher-level "(co)datatype" code copes with them to the extent possible. In the code, you'll see this by grepping for "unsorted_As" in "bnf_fp_def_sugar.ML". > > I presume there's no deep reason for not supporting syntactic type class constraints in BNFs. It would complicate the composition operators for sure, and in a bunch of places we'd have to discharge 0 goals arising from syntactic type class instantiations. If you're up for putting in the effort, we won't stop you. *Live* BNF type variables may not have sort constraints. This is inherent: live variables indicate where we may recurse through. Imagine a BNF "'a :: foo F" with 'a live. Then we should be able to define: datatype X = N | C "X F" which in turn would require X to be an instance foo. Suddenly the datatype command would need to instantiate arbitrary type classes simultaneously with defining the type, which sounds quite ambitious even for syntactic type classes (e.g., one might get the "wrong" instance). In contrast, *dead* BNF type variables may carry sort constraints. Consider e.g., datatype (dead 'a::plus, 'b) X = N 'b | C 'a "('a, 'b) X" term map_X where the first type argument of X in map_X has the sort constraint. Sometimes one can even use the sort constraints on dead type variables to prove that some type is a BNF. My favorite example that uses this trick are arity-correct first-order terms: declare [[typedef_overloaded]] class arity = fixes arity :: "'a ⇒ nat" instantiation unit :: arity begin definition arity_unit :: "unit ⇒ nat" where "arity_unit x = 0" instance proof qed typedef (overloaded) ('c :: arity, 'ty) comb (infixr "$" 65) = "{(s :: 'c, Ts :: 'ty list). arity s = length Ts}" morphisms Rep_comb comb by (auto intro!: exI[of _ "replicate _ undefined"]) lift_bnf (no_warn_wits) (dead 'c :: arity, 'ty) comb by auto setup_lifting type_definition_comb lift_definition "fun" :: "'c :: arity $ 'ty ⇒ 'c" is fst . lift_definition "args" :: "'c :: arity $ 'ty ⇒ 'ty list" is snd . datatype ('x, 'c :: arity) "term" = Var 'x | App "'c $ ('x, 'c) term" Dmitriy PS: For sure, copy_bnf should emit a proper failure instead of the tactic failure in "observation 1". I will have a look eventually.

**References**:**[isabelle] BNFs and sort constraints***From:*Lars Hupel

**Re: [isabelle] BNFs and sort constraints***From:*Jasmin Blanchette

- Previous by Date: [isabelle] New AFP entry: Axiom Systems for Category Theory in Free Logic
- Next by Date: [isabelle] Simplifier not simplifying statement
- Previous by Thread: Re: [isabelle] BNFs and sort constraints
- Next by Thread: [isabelle] New in the AFP: Monadification, Memoization and Dynamic Programming
- Cl-isabelle-users May 2018 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