Hi Brian,
Finally, the unfolding rule is used to prove the original equations.
This part uses the user-supplied fixrec_simp rules. The unfolding rule
is substituted on the LHS, and then the resulting goal is solved using
the simplifier.
(4) "mapL$f$LNil = LNil"
(5) "x ~= UU ==> mapL$f$(LCons$x$xs) = LCons$(f$x)$(mapL$f$xs)"
The fixrec_simp rules include rules related to the constants that make
up the "big case expression". The rules for case combinators of strict
constructors have definedness side-conditions, so definedness rules
for constructors are also declared [fixrec_simp]. Finally, proving the
equations also involves continuous beta-reduction, so the [cont2cont]
rules are included too.
When would the user actually have to declare his own [fixrec_simp] rule
then? From your description it seems that these rules would typically
come out of the domain package (and be declared [fixrec_simp] there
internally) or from the base library.
But I am not sure about [cont2cont]... Where does the beta reduction
come in?
In practice, fixrec_simp always seems to be a *subset* of the global
simpset. Fixrec needs simp rules for continuity, case combinators, and
definedness; such rules are always useful as global simp rules too.
So the only situation that comes to my mind is when some simp rule
loops. Then the fixrec invocation would loop too, which is at least a
bit strange.
Now that I think about it, I actually did see a looping termination
proof once. Of course the looping simp rule should not have been there
in the first place, but diagnosing that is not really nice...
In conclusion, I think maybe I should get rid of [fixrec_simp] and
just use the global simpset to solve the continuity goals and reduce
case expressions. Based on your experience with the function package,
I expect that bad simp rules would be very unlikely to break the
internal proofs.
The difference is that termination proofs are supposed to do clever
things that may or may not work (they rely on arithmetic built into the
simplifier, and they are supposed to exploit properties of user-defined
functions etc.). In your situation it seems that you "only" have to
simplify the case expression away, possibly solving definedness
conditions using a somewhat fixes scheme...
Could you use something like
[case and definedness rules by domain package] + [cont2cont] ?
Alex
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
