On 24/03/12 09:32, Rob Arthan wrote:
The scripts for the ProofPower mathematical case studies have a little tool called
"check_thms" which does a quality assurance check on the the theorems in a
theory. It checks against:
a) Theorems with free variables. Typically this means you forgot an outer
universal quantifier. Later on you will be puzzled when tools like the
rewriting tools think you don't want the free variables to be instantiated.
b) Theorems with variables bound by logical quantifiers (universal, existential
and unique existential) that are not used in the body of the abstraction. This
happens for various reasons (often hand in hand with (a)). It is misleading for
the reader and can be confusing when you try to use the theorem.
It outputs a little report on any problems it finds.
I am considering putting a bug-fixed and documented version of check_thms in
the next working release of ProofPower. Any comments or suggestions for other
things to check for would be welcome.
I am wondering about a stronger version of check b for individual
conjuncts of a theorem. In the past, I have found that e.g. rewriting
can be awkward when an equational conjunct of a theorem does not mention
a universally quantified variable (that is mentioned by other
conjuncts). I think the issue was when the unmentioned variable was
quantified over a non-maximal set, so this is probably most relevant to
Z. For example, given
│ _ ^ _ : ℤ × ℕ → ℤ
├──────
│ ∀ i : ℤ; j : ℕ ⦁ i ^ 0 = 1 ∧ i ^ (j + 1) = i * i ^ j
I think rewriting with the base case requires manual intervention to
provide a value for j, so the following would be preferable:
├──────
│ ∀ i : ℤ ⦁ i ^ 0 = 1 ∧ (∀ j : ℕ ⦁ i ^ (j + 1) = i * i ^ j)
I expect that this sort of check would be dependent on the current proof
context (perhaps making use of canonicalization support) so may not be
desirable as part of the same utility.
This is currently just for HOL, but I could do something similar for Z too.
Certainly this would be a useful facility for HOL users but I could only
make use of a Z version.
Regards,
Phil
P.S. The above formal text is UTF8 encoded! Hopefully that is not a
problem these days. It would be useful to know if any mail systems
aren't displaying it properly.
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
