Re: [isabelle] Isabelle 2007 - Inductive sets + syntax



On Fri, 21 Dec 2007, George Karabotsos wrote:

> I am wondering how I can change the following inductive set definition 
> (along with its associated syntax) using Isabelle 2007.  I am able to 
> use the inductive_set syntax for its definition, however, I am unable to 
> use the -e-> syntax.
> 
> consts
>  eval :: "(B * bool)set"
> 
> syntax
>  "_eval" :: "B => bool => bool" (infixl "-e->" 50)
> 
> translations
>  "b -e-> b'" == "(b,b') : eval"
> 
> inductive eval
> intros
> TrueB: "TrueB -e-> True"
> FalseB: "FalseB -e-> False"

This works by using abbreviations simultaneously within the 
'inductive_set' definition, e.g. like this:

  inductive_set eval and eval_syn (infixl "-e->" 50)
  where
    "b -e-> b' == (b, b') : eval"
  | TrueB: "TrueB -e-> True"
  | FalseB: "FalseB -e-> False"

Also note that 'inductive' for inductive predicates is usually more 
convient than the historical detour via sets; it does not need separate 
syntax at all:

  inductive eval_rel (infixl "-e->" 50)
  where
    TrueB: "TrueB -e-> True"
  | FalseB: "FalseB -e-> False"


	Makarius





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