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)"

doesn't work.

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 induction rule.

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 overkill.


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