[isabelle] parameters of function definitions and scope of constants



Thnx for the answers to my previous questions. I have 2 more :)

1) When defining a function using the `fun' keyword, it is not possible to use the name of an existing constant as parameter. E.g.,

definition foo :: "bool" where "foo = True"

fun bar :: "nat => nat" where "bar foo = Suc(foo)"

doesn't work. It produces:

*** Type unification failed: Clash of types "bool" and "nat"
*** Type error in application: Incompatible operand type
***
*** Operator:  bar :: nat => nat
*** Operand:   foo :: bool
***
*** At command "fun".

Is that the intended behavior?

2) Is it possible to `hide' previously defined constants that have only be used in some lemmas and aren't needed later on, in order to be able to reuse the name? Or put differently, can I use `fun' and/or `definition' in a local scope (let's say, within a proof)?

cheers

christian





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