[isabelle-dev] Use of global simpset by definition packages
Alexander Krauss
krauss at in.tum.de
Fri May 7 22:55:10 CEST 2010
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
More information about the isabelle-dev
mailing list