Email Gateway (Aug 18 2022 at 12:55): Email Gateway (Aug 18 2022 at 12:55):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
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
Email Gateway (Aug 18 2022 at 12:55):From: Alexander Krauss <krauss@in.tum.de>
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/ordefinition' in a local scope (let's say, within a proof)?
Not really... Locales are local scopes in a way, but thats probably
overkill.
Alex
Last updated: Nov 21 2024 at 12:39 UTC