Dear All,
Sorry for the extensive background if you prefer please go straight
to the PROBLEM that is a bit below in the mail.
------------> BACKGROUND <------------
I'm trying to use HOL to prove termination of recursive functions
with preconditions in VDM. What I plan to do is generate the
termination conditions myself by inspecting the VDM source file and
then trying to prove them in HOL. I know HOL doesn't support sub-
typing so what I'm doing at the moment is for example:
f(x) = if (x=3) then 3 else f(x-1)
precondition: x >= 3
What is inserted into HOL is a goal like this:
- g `?R. WF R /\ ( ~(x=3) /\ (x>=3) ==> R (x-1) x )`;
The thing if I try to prove this using the command:
e (WF_REL_TAC `measure (\x.x)`)
I am successful because '<' is well founded and the rest of the
equation is true. But the proof is unsound because inserting the
'(x>=3)' assumption makes this statement "~(x=3) /\ (x>=3) ==> R
(x-1) x" true. This could be solved if I use (\x.x-3) instead of
'(\x.x)'. But what I'm trying to do is for use of general use so I
don't want people to incur in the risk of making unsound proofs.
------------> PROBLEM <------------
So what I tried to follow other approach and define the 'measure'
relation myself, like this:
- g `?R. WF R /\ ( ~(x=3) /\ (x>=3) ==> R (x-1) x )`;
- val measure2 = Define `measure2 f x y = if (x>= 3 /\ y >= 3) then f
x < f y else F`;
- e (WF_REL_TAC `measure2 (\x.x)`)
- e (RW_TAC arith_ss [measure2])
And using this tactic all goes alright until I get stuck with:
> val it =
WF (measure2 (\x. x))
: goalstack
Although the relation is well founded because it's just a restriction
of the Naturals. I couldn't prove it until now. Is there a tactic to
prove this or at least to do some simplification. I couldn't do
nothing to continue this proof yet. Or maybe there is other ways to
do this. Thank you for your time and help.
Cheers,
Augusto Silva
-------------------------------------------------------------------------
This SF.net email is sponsored by the 2008 JavaOne(SM) Conference
Register now and save $200. Hurry, offer ends at 11:59 p.m.,
Monday, April 7! Use priority code J8TLD2.
http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
