*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] Term rewriting systems*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Fri, 12 Sep 2008 08:57:42 +1000*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <48C92814.3030704@uni-muenster.de>*References*: <48C92814.3030704@uni-muenster.de>*User-agent*: Thunderbird 1.5.0.12 (X11/20070604)

Peter Lammich wrote:

Hi all,I wonder whether there is any tool support (best Isabelle compatibletool support) to reason about term rewriting systems of the followingform: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) c2t) -> NODE (USE m)(c1 at c2) t2) NODE (ENTER m) c1 (NODE (USE m') c2 (NODE (LEAVE m) c3 t))-> NODE (USE (m\<union>m')) (c1 at c2@c3) t3) NODE (USE u1) c1 (NODE (USE u2) c2 t)-> NODE (USE (u1\<union>u2)) (c1 at c2) t4) NODE (USE u) (c1 at NIL#c2)t-> NODE (USE u) (c1 at c2) t5) NODE (USE u) (c1@(NODE (USE u1) cs1 ts1)@c2@(NODE (USE u2) cs2ts2)@c3) t -> NODE (USE u) (c1@(NODE (USE (u1\<union>u2)) cs1ts1)#c2 at cs2@ts2#c3) t6) 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. CurrentlyI define an inductive predicate step ("->") by the rules 1-6 andadditionally 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) xI want to show termination and confluence of this system. Terminationis easy, as the size of the tree decreases in any step, hence I easilygetlemma "wfP (step^--)"By Newman's lemma (A version is in HOL/Lambda/Commutation.thy), itsuffices to show local confluence, I even think my system above hasthe diamond property.Is there any standard approach to term rewriting systems in Isabelleor are there some other tools out there, to show confluence (andtermination) as automatic as possible?Are there any suggestions on how to show local confluence of such asystem in Isabelle (as automatic as possible)?The main problem seems to be the non-constructor patterns (likec1 at t#c2) I use in my rewriting rules (4,5,6,8)Thanks for any suggestions/comments in advance, best Peter

Peter,

so rewriting a subterm naturally is rewriting f (c1 at t#c2) to f (c1 at t'#c2).

It's at http://users.rsise.anu.edu.au/~jeremy/isabelle/2005/snabs/ (also uses http://users.rsise.anu.edu.au/~jeremy/isabelle/2005/gen/) Jeremy

**References**:**[isabelle] Term rewriting systems***From:*Peter Lammich

- Previous by Date: [isabelle] interpretation of a locale in a locale
- Next by Date: Re: [isabelle] interpretation of a locale in a locale
- Previous by Thread: Re: [isabelle] Term rewriting systems
- Next by Thread: [isabelle] Final Call for Participation: VSTTE'08
- Cl-isabelle-users September 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list