[isabelle] Syntax translations for the new inductive package



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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.