*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Syntax translations for the new inductive package*From*: Andreas Lochbihler <lochbihl at infosun.fim.uni-passau.de>*Date*: Fri, 26 Oct 2007 08:31:24 +0200*Reply-to*: lochbihl at fim.uni-passau.de*User-agent*: Mozilla Thunderbird 1.0.8-1.1.fc4 (X11/20060501)

Hello all, I'm currently converting my old theories to the new syntax of the latest Isabelle development snapshot. In doing so, I stumbled over the new inductive package which subsumes the set definition and the syntax translation in one step. However, in some cases, I have problems converting constants which formerly were function to sets. For example, if the old syntax read like this. In the syntax translation, the order of the parameters is changed: (* consts p :: "'a => 'b => nat => bool" consts w :: "'a => 'b => (nat * nat) set" syntax w_syntax :: "'a => nat => 'b => nat => bool" -- define here some nice syntax translations "w_syntax a c b d" == "(c, d) : w a b" inductive "w a b" intros "p a b c ==> w_syntax a c b 0" "w_syntax a (Suc c) b n ==> w_syntax a c b (Suc n)" *) I then tried to convert this to the new syntax, but then Isabelle responds with an error message consts p :: "'a => 'b => nat => bool" inductive w :: "'a => nat => 'b => nat => bool" for a :: 'a and b :: 'b where "p a b c => w a c b 0" | "w a (Suc c) b n => w a c b (Suc n)" *** Ill-formed introduction rule "" *** p a b c ==> w a c b 0 *** Inductive predicate must be applied to parameter(s) a, b *** At command "inductive". My workaround was to define the set w with type 'a => 'b => nat => nat => bool (thereby rewriting every introduction rule to get rid of the syntax translation which is no longer available) and then to provide an abbreviation which gives the original syntax back. Is there any way I can use the order of parameters as given by the old syntax translation in the introduction rules for w? Regards, Andreas Lochbihler

**Follow-Ups**:**Re: [isabelle] Syntax translations for the new inductive package***From:*Makarius

**Re: [isabelle] Syntax translations for the new inductive package***From:*Stefan Berghofer

- Previous by Date: Re: [isabelle] backward compatibility of development snapshot.
- Next by Date: Re: [isabelle] Syntax translations for the new inductive package
- Previous by Thread: Re: [isabelle] backward compatibility of development snapshot.
- Next by Thread: Re: [isabelle] Syntax translations for the new inductive package
- Cl-isabelle-users October 2007 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