Re: [isabelle] primrec on nested mutually-recursive datatype
I'm not using size because it seems to be too generic. In particular,
when I use size as the measure function on a definition that traverses
my datatype, Isabelle tries to use the length function on the lists
inside my if or while statements, whereas it should be using
AppSrcOp_list_size1, AppSrcOp_list_size2 or AppSrcOp_list_size3 (more
detail in the example below).
Your proof suggestion works but doesn't seem to be enough for Isabelle.
Maybe if I gave you a fuller example, my needs would become clearer.
My datatype is as follows:
ifStmt nat "AppSrcOp list" "AppSrcOp list" |
while nat "AppSrcOp list"
AppSrcOp = opTriple "FuncMark * TypeMark * AppSrcStmt"
The size function created for this datatype is:
size skip = 0
size (ifStmt ?nat ?list1.0 ?list2.0) =
AppSrcOp_list_size1 ?list1.0 + AppSrcOp_list_size2 ?list2.0 + Suc 0
size (while ?nat ?list) = AppSrcOp_list_size3 ?list + Suc 0
size (opTriple ?x) = nat_nat_AppSrcStmt_x_x_size ?x + Suc 0
AppSrcOp_list_size1  = 0
AppSrcOp_list_size1 (?AppSrcOp # ?list) = size ?AppSrcOp +
AppSrcOp_list_size1 ?list + Suc 0
AppSrcOp_list_size2  = 0
AppSrcOp_list_size2 (?AppSrcOp # ?list) = size ?AppSrcOp +
AppSrcOp_list_size2 ?list + Suc 0
AppSrcOp_list_size3  = 0
AppSrcOp_list_size3 (?AppSrcOp # ?list) = size ?AppSrcOp +
AppSrcOp_list_size3 ?list + Suc 0
nat_nat_AppSrcStmt_x_x_size (?nat, ?x) = nat_AppSrcStmt_x_size ?x + Suc 0
nat_AppSrcStmt_x_size (?nat, ?AppSrcStmt) = size ?AppSrcStmt + Suc 0
The core of function definition is as follows:
consts func :: "(AppSrcOp list) => bool"
recdef func "measure size"
"func  = True"
"func (asOp # asList) =
(case asOp of
opTriple triple =>
(case (snd(snd triple)) of
(ifStmt pv aTrue aFalse) =>
((func aTrue) &
(func aFals)) |
(while pv aW) =>
(func aW) |
_ => True) &
This produces the following error from Isabelle:
"*** recursion equations must use the = relation
*** At command "recdef"."
When I comment out the case statement, the definition goes through just
When I comment out the ifStmt case and (func asList), Isabelle says:
"*** Bad final proof state:
*** ALL asList asOp nat pv.
*** (EX a aa. asOp = opTriple (a, aa, while nat pv)) --> length pv <
Suc (length asList)
*** 1. ALL asList asOp nat pv.
*** (EX a aa. asOp = opTriple (a, aa, while nat pv)) --> length
pv < Suc (length asList)
*** 1 unsolved goals!
*** Proof failed!
*** At command "recdef".
Thus, Isabelle is treating both the list of operations that was the
argument to func and the list of operations inside the while statement
as regular lists rather than lists of operations. Thus, its using the
length function on them rather than the more appropriate
AppSrcOp_list_size3. This is even true when I replace "(while pv aW)"
with "(while pv (aW::(AppSrcOp list)))" in the above definition.
I had hoped that creating my own size function would make things better
but since the argument to the function is a list and Isabelle forces me
to use three different functions for defining the size of a list of
operations, choosing any one of the operation list size functions
doesn't work. On the other hand, using the generic size function winds
up being too generic.
Note that the fact that the datatype is mutually recursive is
irrelevant. I tried the above example with the following simply
recursive datatype and got exactly the same results:
ifStmt nat "AppSrcStmt list" "AppSrcStmt list" |
while nat "AppSrcStmt list"
Stefan Berghofer wrote:
Greg Bronevetsky wrote:
I've finally gotten the the point where I need to use the measure
function to recdef a type. However, Isabelle wants me to prove that
(ALL asOp. 0 < AppSrcOpSize asOp). Unfortunately, I don't know how to
prove it. The most obvious proof is by structural induction but I'm
too new to Isabelle to know how to specify that. Doing something as
simple as "proof (induct asOp)" does not work since Isabelle says
"*** Unable to figure out induct rule". What else can I do?
You can only do induction on *free* variables. In your example, induction
is actually overkill, since you can prove the above goal by a sequence
of case distinctions followed by simplification:
lemma "0 < AppSrcOpSize asOp"
apply (case_tac asOp)
apply (case_tac x)
apply (case_tac b)
apply (case_tac ba)
By the way, why don't you use the standard "size" funtion already
by the datatype package?
This archive was generated by a fusion of
Pipermail (Mailman edition) and