Hi Rob, Many thanks for the reply and clarification.

All below makes sense. I can see how effectively excluding terms such as |- n = 1 /\ n = {1}

`would in any case impose a big overhead on run-time, requiring some`

`dynamic type-checking when rules are applied, etc. To exclude such cases`

`nonetheless I suppose it will be cheapest to do manual checks in one's`

`own code where this duplicity can arise, and maybe raise custom error`

`messages or carry out renaming if feasible.`

> ... finding a good name for it seems the hardest problem just now :-) Maybe something like "match_inst_rule" ? > Yes. I have been meaning to get round to this for a long time. It > isn't quite as simple as you might think because the Z tactics are > designed to keep in Z, but the back-chaining tactics often need to > produce an existentially quantified goal and that would need to be > converted from HOL back into Z.

`Okay, I see. This happens I suppose when the theorem "asms | ant => suc"`

`used for backward-chaining contains free variables in the antecedent`

`which do not occur anywhere else, i.e. the assumptions or conclusion of`

`the implication used for backward-chaining. As far as I can see the`

`internal bc_rule wraps such free variables into an existential`

`quantification after the theorem used for backward-chaining has been`

`matched and suitably instantiated. So, basically, one needs to`

`reimplement bc_rule as well to ensure that the subgoal generated`

`(existential quantifiers) remains in the Z language. I might have a`

`crack at it next week and send a personal email if any success ;-).`

`Cheers, Rob, for taking the suggestions below into considerations with`

`the next release of ProofPower, and thanks for the feedback in general,`

Frank Rob Arthan wrote:

Frank, On 7 Apr 2009, at 14:39, Frank Zeyda wrote:Dear Roger, Many thanks for the reply. ....The additional feature of better error handling is easily supportedwith another line of code handling possible exceptions.The idea behind the caller parameter in many of these internal functionswas to make the reporting of the function that was the real detector ofthe error more precise. In this case, apply_matches_rule isn't doinganything very subtle so you are right that the calling function could doit with a simple handler.Maybe apply_matches_rule could be a nice function to have in thegeneral interface, what about exposing it?In many instances in the original development of ProofPower, there wereinstances of general purpose functions like this that were nearlygeneral enough and useful enough to "productise" but not quite (e.g.,because of the effort involved in getting the error handling completelygeneral or in documenting exactly what the function does, or even justthinking up the right name for the function). I will certainly considerexposing apply_matches_rule - finding a good name for it seems thehardest problem just now :-)>> A second case is when y occurs free in both thm and term,>> is not substituted but nonetheless introduced through thesubstitution.>> I presume this is okay >> as long as the types of y are identical in thm and term. > > Its still OK if the types are not the same, they will be > logically distinct variables and its a confusing situation > you shold seek to avoid.This sounds a little bit curious, is there a document that explainsmore about this situation?There are at least two accounts of the semantics of HOL and they agreeon this point as do the classical references on type theory and onmany-sorted first-order logic. For HOL, I have in mind the account byAndy Pitts in the Cambridge HOL documentation and my account in HOL inspc00{1,2,3,4}.doc supplied with ProofPower. It isn't really curious ifyou think about it the other way round: how could the semantics possiblyconsider two variables with different types to be the same? In Church'ssimple type theory and its polymorphic variant HOL, the types are disjoint.So although the variables have the same name they are actually treatedas logical distinct by the fact that they have different types? Soinstantiation would have be sensitive to variable types (not justnames) and might result in one variables n to be substitution, whileanother n is left unaffected e.g. if it has a different type?For example, assume we have a theorem thm n = 1 |- n = {1} Then (asm_inst_term_rule [(2, n)] thm) would yield 2 = 1 |- n = {1} ?Absolutely! Instantiation works just like that (it even has to renamebound variables if the instantiation would cause a capture problem). Butthis is a tiny price to pay: the alternative approaches are veryunattractive: e.g., the abstract data type of terms could ban terms thatused the same variable name with different types but that would impose abig runtime overhead on the constructors for applications andlambda-abstraction.Thanks for pointing this out, it clarified one or two behaviours ofProofPower for me which I could not explain before.> I think the main problem you will have is in matching against terms > containing bound variables.I haven't given considerations to this, but as far as I can see such asituation may not arise in the particular application. Thanks forpointing this out!Cheers once more, FrankPS: What about a function that supports backward-chaining with Ztheorems, something like z_bc_tac and z_bc_thm_tac? I suppose thiscould be quite useful too. Is there anything more that needs to bedone other than rewriting the Z universal quantifier into a HOL one,and using the HOL backward-chaining tactics?Yes. I have been meaning to get round to this for a long time. It isn'tquite as simple as you might think because the Z tactics are designed tokeep in Z, but the back-chaining tactics often need to produce anexistentially quantified goal and that would need to be converted fromHOL back into Z.PPS: A final comment. To implement some custom error handling Inoticed that there was no functions that could be used to infer the idof an error message (of type MESSAGE). Since the MESSAGE datatype isnot exposed, we cannot take the message apart; the only solution seemsto be to dissect the string of the error message. If I'm overlookingsomething please let me know, otherwise it would be beneficial to havesome function get_id in the general interface of BasicError to extractthe id of an error message ;-).You aren't overlooking anything. I have thought that a function like youget_id would be useful in some circumstances. I think I will add afunction that will just let you take the MESSAGE type apart, but with awarning that it should be used with caution since ti makes your codevery sensitive to changes in the code you are calling.By the way, it is very good to see that you are boxing very clever withProofPower just now!Regards, Rob.

_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com