[isabelle-dev] Use of global simpset by definition packages

[Alexander Krauss]

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