Re: [isabelle] primrec on nested mutually-recursive datatype

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?

                            Greg Bronevetsky

Stefan Berghofer wrote:

The problem is that each occurrence of "AppSrcOp list" is unfolded.
Consequently, you have to give a separate size function for each of
these occurrences, even though they happen to behave in the same way.
The following definition should work:

 AppSrcStmtSize :: "AppSrcStmt => nat"
 AppSrcOpSize :: "AppSrcOp => nat"
 AppSrcOpListSize1 :: "(AppSrcOp list) => nat"
 AppSrcOpListSize2 :: "(AppSrcOp list) => nat"
 AppSrcOpListSize3 :: "(AppSrcOp list) => nat"
 AppSrcOpTripleSize :: "FuncMark * TypeMark * AppSrcStmt => nat"
 AppSrcOpPairSize :: "TypeMark * AppSrcStmt => nat"

"AppSrcOpSize (opTriple asOp) = AppSrcOpTripleSize asOp"

"AppSrcOpTripleSize (x, y) = AppSrcOpPairSize y"

"AppSrcOpPairSize (x, y) = AppSrcStmtSize y"

"AppSrcOpListSize1 [] = 0"
"AppSrcOpListSize1 (asOp # opList) = (AppSrcOpSize asOp) + (AppSrcOpListSize1 opList)"

"AppSrcOpListSize2 [] = 0"
"AppSrcOpListSize2 (asOp # opList) = (AppSrcOpSize asOp) + (AppSrcOpListSize2 opList)"

"AppSrcOpListSize3 [] = 0"
"AppSrcOpListSize3 (asOp # opList) = (AppSrcOpSize asOp) + (AppSrcOpListSize3 opList)"

"AppSrcStmtSize skip = 1"
"AppSrcStmtSize (ifStmt pv aTrue aFalse) = 1 + (AppSrcOpListSize1 aTrue) + (AppSrcOpListSize2 aFalse)"
"AppSrcStmtSize (while pv aW) = 1 + (AppSrcOpListSize3 aW)"

Again, a quick look at the theorems AppSrcStmt_AppSrcOp.size reveals
how the scheme works.


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