# [isabelle] Term rewriting systems

Hi all,

`I wonder whether there is any tool support (best Isabelle compatible
``tool support) to reason about term rewriting systems of the following form:
`
I have a term rewriting system defined over terms of the form:
datatype 'm action = ENTER "'m" | LEAVE "'m" | USE "'m set"
datatype 'm tree = NIL | NODE "'m action" "'m tree list" "'m tree"
the rules are like this:

`1) NODE (ENTER m) c1 (NODE (LEAVE m) c2
``t) -> NODE (USE m) (c1 at c2) t
``2) NODE (ENTER m) c1 (NODE (USE m') c2 (NODE (LEAVE m) c3 t))
``-> NODE (USE (m\<union>m')) (c1 at c2@c3) t
``3) NODE (USE u1) c1 (NODE (USE u2) c2 t)
`` -> NODE (USE (u1\<union>u2)) (c1 at c2) t
``4) NODE (USE u) (c1 at NIL#c2) t
`` -> NODE (USE u) (c1 at c2) t
``5) NODE (USE u) (c1@(NODE (USE u1) cs1 ts1)@c2@(NODE (USE u2) cs2
``ts2)@c3) t -> NODE (USE u) (c1@(NODE (USE (u1\<union>u2)) cs1
``ts1)#c2 at cs2@ts2#c3) t
``6) NODE (USE u1) (c1@(NODE (USE u2) cs ts)#c2) NIL ->
``NODE (USE (u1\<union>u2)) (c1 at cs@ts#c2)
`

`My rewriting strategy is rewriting of an arbitrary subterm. Currently I
``define an inductive predicate step ("->") by the rules 1-6 and
``additionally the inductive rules:
`7) t -> t' ==> NODE a c t -> NODE a c t'
8) t -> t' ==> NODE a (c1 at t#c2) x -> NODE a (c1 at t'#c2) x

`I want to show termination and confluence of this system. Termination is
``easy, as the size of the tree decreases in any step, hence I easily get
` lemma "wfP (step^--)"

`By Newman's lemma (A version is in HOL/Lambda/Commutation.thy), it
``suffices to show local confluence, I even think my system above has the
``diamond property.
`

`Is there any standard approach to term rewriting systems in Isabelle or
``are there some other tools out there, to show confluence (and
``termination) as automatic as possible?
``Are there any suggestions on how to show local confluence of such a
``system in Isabelle (as automatic as possible)?
`

`The main problem seems to be the non-constructor patterns (like c1 at t#c2)
``I use in my rewriting rules (4,5,6,8)
`
Thanks for any suggestions/comments in advance, best
Peter

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