Re: [isabelle] 2 questions

I think you mean that you are looking for a tactic that applies the rule repeatedly until every occurrence of xRy has been used. You'd have to write ML code to locate them and instantiate the rule appropriately, e.g. calling res_inst_tac, since unguided rule applications will always find the first occurrence of xRy.

Larry Paulson

On 31 Mar 2006, at 11:26, F. Miguel Dionisio wrote:

b) (Saturation) The BoxLeft rule looks like ([|x:[]A; xRy|]==>R)==> ([|x:[]A; xRy; y:A|]==>R) and is somehow similar to the left rule for the universal quantifier. There may be several unification possibilities, for example if xRy and xRy1 are present in the premises. I would like to have a rule that uses all possible unifications. For that particular case the rule ([|x:[]A; xRy; xRy1|]==>R)==>([|x:[]A; xRy; xRy1; y:A;y1:A|]==>R) would do. This is similar to having a left rule for the universal quantifier that would instanciate the predicate in all unifiable terms available.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.