<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><br><div><div>On 29 Mar 2012, at 15:02, Phil Clayton wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div>On 27/03/12 08:36, Rob Arthan wrote:<br><blockquote type="cite"><br></blockquote><blockquote type="cite">On 25 Mar 2012, at 12:31, Phil Clayton wrote:<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite"><blockquote type="cite">On 24/03/12 09:32, Rob Arthan wrote:<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">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:<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">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.<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">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.<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">It outputs a little report on any problems it finds.<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">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.<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">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<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">│ _ ^ _ : ℤ × ℕ → ℤ<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">├──────<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">│ ∀ i : ℤ; j : ℕ ⦁ i ^ 0 = 1 ∧ i ^ (j + 1) = i * i ^ j<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">I think rewriting with the base case requires manual intervention to provide a value for j,<br></blockquote></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">Indeed. ∀ i : ℤ; j : X ⦁ i ^ 0 = 1 amounts to a convoluted way of saying "either X is empty or ∀ i : ℤ ^ 0 = 1".<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite"><blockquote type="cite">so the following would be preferable:<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">├──────<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">│ ∀ i : ℤ ⦁ i ^ 0 = 1 ∧ (∀ j : ℕ ⦁ i ^ (j + 1) = i * i ^ j)<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite"><blockquote type="cite">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.<br></blockquote></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">I think a simple heuristic would work. I think is reasonable to say that in a predicate of the form:<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite"><span class="Apple-tab-span" style="white-space:pre"> </span>∀ ... x : X | P ⦁ Q1 ∧ Q2 ∧ ...<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">If there is an i such that x doesn't appear free in P or Qi, then report a possible problem. There are many cases (e.g., law of transivity) where a theorem has an implication with an antecedent that contains variables that are not in the succedent, but it is a reasonable style rule in Z not to disguise such an implication by burying the antecedent in an implication.<br></blockquote><br>That sounds reasonable to me.<br><br>There is also the possibility of a schema declaration in the quantification which presents various options. For e.g. a schema reference:<br><br> ∀ S; ... | P ⦁ Q1 ∧ Q2 ∧ ...<br><br>would it make sense for the heuristic warn if there is an i such that frees(P) ∪ frees (Qi) does not mention any variable bound by S?<br></div></blockquote><div><br></div>Yes that makes sense. <br><blockquote type="cite"><div><br>Also, for a horizontal schema declaration, there is the question of whether to destruct it, i.e. expand out its contents, or treat it like any other schema.<br></div></blockquote></div><br><div>Do you mean a declaration in a quantifier of the form [Declaration | Predicate]? Do you use that idiom much? I can't see the point, so I don't have any views on how to handle it.</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div></body></html>