Re: [isabelle] [Q]Question about Isabelle/hol
On 07/28/2012 12:30 PM, 後藤 裕貴 wrote:
> It is the question about applying "map" to "Datatype" definition this time.
> 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
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and