Re: [isabelle] parameters of function definitions and scope of constants
Christian Sternagel wrote:
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)"
You can out an explicit quantifier:
fun bar :: ... where "!!foo. bar foo = Suc foo"
the specification parser normally puts quantifiers around free variables
in the spec, but you can also put them explicitly. With this trick you
can also influence the order in which variables are quantified in the
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?
hide const my_const
Or put differently, can I use `fun' and/or
`definition' in a local scope (let's say, within a proof)?
Not really... Locales are local scopes in a way, but thats probably
This archive was generated by a fusion of
Pipermail (Mailman edition) and