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:
datatype
 AppSrcStmt =
   skip |
   ifStmt nat "AppSrcOp list" "AppSrcOp list" |
   while nat "AppSrcOp list"
and
 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) &
         (func asList)
    )
 "
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 fine.

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:
datatype
 AppSrcStmt =
   skip |
   ifStmt nat "AppSrcStmt list" "AppSrcStmt list" |
   while nat "AppSrcStmt list"

--
                            Greg Bronevetsky


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)
  apply simp_all
  done

By the way, why don't you use the standard "size" funtion already provided
by the datatype package?

Greetings,
Stefan







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