[isabelle] Term rewriting systems
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and