Email Gateway (Aug 18 2022 at 10:13): Email Gateway (Aug 18 2022 at 10:13):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
In Isabelle/HOL - A Proof Assistant for Higher-Order Logic' ([1] in the following) recdef' is used to define functions for the datatype
datatype ('v,'f)"term" =
Var 'v
| Fun 'f "('v,'f)term list"
For me it gets interesting as soon as higher-order functions can be used to define functions with `recdef'. In [1] there is following example:
consts trev :: "('v,'f)term => ('v,'f)term"
recdef trev "measure size"
"trev (Var x) = Var x"
"trev (Fun f ts) = Fun f (rev (map trev ts))"
which could be proved terminating after the hint
t : set ts --> size t < Suc (term_list_size ts)
I wanted to define following function (which gives the set of positions of a term---where a position is a possibly empty list of natural numbers):
consts pos :: "('v,'f)term => nat list set"
recdef pos "measure (% t. size t)"
"pos (Var v) = {[]}"
"pos (Fun f ts) =
{[]} Un {(i#p) | i p. i : {0..<length ts} & p : pos (ts!i)}"
which is not possible automatically because of the unsolved goal:
\<forall> :001 ts. size (ts ! :001) < Suc (term_list_size ts)
now my questions:
1) what does :001 mean (I just assumed its the index variable i from my definition).
2) why is the information i : {0..<length ts} lost, which would make the unsolved goal equivalent to:
t : set ts --> size t < Suc (term_list_size ts)
3) is it possible to do a termination proof for a recdef definition fully by hand in order to make sure, that i : {0..<length ts} is used?
Thanks in advance.
cheers
christian sternagel
Email Gateway (Aug 18 2022 at 10:14):From: Alexander Krauss <krauss@in.tum.de>
Christian,
I wanted to define following function (which gives the set of
positions of a term---where a position is a possibly empty list of
natural numbers):consts pos :: "('v,'f)term => nat list set"
recdef pos "measure (% t. size t)"
"pos (Var v) = {[]}"
"pos (Fun f ts) =
{[]} Un {(i#p) | i p. i : {0..<length ts} & p : pos (ts!i)}"which is not possible automatically because of the unsolved goal:
\<forall> :001 ts. size (ts ! :001) < Suc (term_list_size ts)
now my questions:
1) what does :001 mean (I just assumed its the index variable i from
my definition).
It's an internal variable produced by the simplifier. I am not sure why
you get to see this strange name, but reading it as "i" is probably just
right.
2) why is the information i : {0..<length ts} lost, which would make
the unsolved goal equivalent to:
You are missing a congruence rule here. Congruence rules are needed for recdef
to know at which values the recursive call actually occurs. In your
example, the
following congruence rule for conjunction helps:
lemma conj_cong[recdef_cong]:
"[| A = A'; A' ==> B = B' |] ==> A & B = A' & B' "
by blast
In the second premise, you see the hypothesis A'. This gives you the
extra hypothesis for the termination proof.
You can see congruence rules as if they express something about evaluation
order, which is not otherwise defined, since we're just doing logic. By giving
this congruence rule to recdef you state (and have proved) that the
second part of the conjunction only relevant if the first part is
satisfied. In the tutorial
(end of 9.2.2) this is only mentioned briefly, but the example given
there works
out-of-the-box, because the map_cong rule is there already (and
conj_cong should
probably also be). In general you need a suitable congruence rule for every
higher-order combinator you use in the definition.
You can see the preconfigured congruence rules by issuing
ML "RecdefPackage.print_recdefs (the_context ())"
By looking at some of them you will quickly learn how to make your own ones if
you need them.
3) is it possible to do a termination proof for a recdef definition
fully by hand in order to make sure, that i : {0..<length ts} is used?
Yes you can, by a largely unkown feature:
Issue your recdef definition using the "permissive" keyword:
recdef (permissive) pos ....
Then the defintion goes through, but the unproven termination
conditions end up as premises of the pos.simps rules:
thm pos.simps
Then you can set up a manual proof by
recdef_tc abc: pos
and when you have finished the proof, the lemmas will be stored as "abc". You
will still have to remove the premises manually from pos.simps though.
The above information is for Isabelle 2005. In the developer snapshot
you would
instead use the new "function" package. There, handling termination proofs is
easier and can be done manually, but the issue with congruence rules remains.
Hope this helps...
Alex
Last updated: May 03 2024 at 08:18 UTC