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

[Brian Huffman]

Hi Alex,

Thanks for the info about the function package. I'll give a bit more
explanation of the proofs that fixrec does, using an example:

domain 'a LList = LNil | LCons 'a (lazy "'a LList")

fixrec mapL :: "('a -> 'b) -> 'a LList -> 'b LList" where
  "mapL$f$LNil = LNil"
| "x ~= UU ==> mapL$f$(LCons$x$xs) = LCons$(f$x)$(mapL$f$xs)"

(Definedness side-conditions like "x ~= UU" are needed with strict
constructors.)

First fixrec defines the constant "mapL" as a least fixed-point.

(1) "mapL == fix$(LAM mapL f z. ... big case expression ... mapL ...)"

Next fixrec proves that the functional from the definition is
continuous. This part uses user-supplied continuity rules (attribute
cont2cont).

(2) "cont (%mapL. LAM f z. ... big case expression ... mapL ...)"

The continuity lemma is used to prove the unfolding rule:

(3) "mapL = (LAM f z. ... big case expression ... mapL ...)"

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.

On Fri, May 7, 2010 at 7:24 AM, Alexander Krauss <krauss at in.tum.de> wrote:
> - The termination prover uses the global simpset (clasimpset actually),
> since I explicitly want it to pick up lemmas from the user. In practice, I
> have never seen a termination proof break because of a bad simp rule
> declared by the user. However, there is alse the possibility to declare
> rules [termination_simp] that should be used *only* in termination proofs.
> So the termination prover uses a superset.

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.

> - I think one should be particularly careful when the actual result of some
> package (like the format of some rules) and not just success or failure is
> influenced by declarations. [fundef_cong] is such a case. In this case, it
> should really be a separate declaration, because otherwise the dependencies
> get really strange.

This is not the case with fixrec. User-supplied rules do not affect
the formulation of the generated theorems, although they may determine
success or failure.

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. I think that definitions are much more likely to fail
due to users declaring an important rule [simp] but not declaring
[fixrec_simp].

- Brian