[isabelle] 2 questions

Dear Isabelle users,

I am trying to develop a tactic for a sequente calculus for labelled modal logics (from Luca Viganò "Labelled non-Classical Logics", Kluwer, 2000) and I am facing 2 problems that might have been already solved in other context by some of you:

a) In some of those logics an upper bound on the number of applications of non-safe rules (i.e. BoxLeft) can be found depending on the complexity of the formula to be established (or not establised). To represente this an ML-function has to be written that calculates the complexity of the formula (easy). However it is not clear to me how I can write a tactic looking like
REPEAT_DETERM_N (complexity ??formula??)

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.

Many thanks,
ps: just direct me to some code if you have already solved somethig similar

Francisco Miguel Dionísio

Departamento de Matemática  
Instituto Superior Técnico

 tel: 218417143
fmd at math.ist.utl.pt

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