Re: [isabelle] [Q]Question about Isabelle/hol



Dear Goto-san,

On 07/28/2012 12:30 PM, 後藤 裕貴 wrote:
> It is the question about applying "map" to "Datatype" definition this time.
> 
> datatype
>    char = A | B | C | D | E | F
> 
> type_synonym str = "char list"
> 
> type_synonym FileName = str
> datatype Gvar = GV Type str
Here Type is not defined. so I use

datatype Gvar = GV str

instead.
> type_synonym GvarList = "Gvar list"
> 
> type_synonym Prog = "(FileName * GvarList * Funcs * Main)"
Here I just removed Funcs and Main, i.e.,

  type_synonym Prog = "(FileName * GvarList)"

Now your function-definition still results in a syntax error.
> fun gvar_changename :: "Prog =>GvarList => GvarList" where
> "gvar_changebname pr1 xs = map (%(GV x y). (GV x (fst pr1)@y)) xs"
The point is that pattern matching does not work in general as part of
lambda abstractions (only for special cases, like pairs). So you have to
use a case-expression, e.g., as follows:

  fun gvar_changename :: "Prog => GvarList => GvarList" where
    "gvar_changename pr1 xs =
      map (%x. case x of GV y => GV (fst pr1 @ y)) xs"

(Also note that the paranthesization in your original definition is not
right, it should be "GV x (fst pr1 @ y)"; and you have to use the same
name for your function at every occurrence, cf. "gvar_changename" vs.
"gvar_changebname".)

cheers

chris





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