*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] "syntax" challange*From*: Brendan Mahony <Brendan.Mahony at dsto.defence.gov.au>*Date*: Mon, 19 Sep 2005 09:13:56 +0930*Cc*:*In-reply-to*: <61C7D080-4327-49B2-8DC3-B927BBEF8C48@acm.org>*References*: <61C7D080-4327-49B2-8DC3-B927BBEF8C48@acm.org>

You need a parse translation. This is an ML function that maps a term to a term. The following is a good start: syntax (xsymbols) "_toT" :: "logic => logic" ("\<tau> _" [1000] 1000) parse_translation {* let fun mkpr s = s^"'"; fun tr (f $ a) = tr f $ tr a | tr (Abs(n, T, b)) = Abs(mkpr n, T, tr b) | tr (Free(n, T)) = Free(mkpr n, T) | tr (Var((n,x), T)) = Var((mkpr n, x), T) | tr t = t; fun toT_tr [t] = Const("toT", dummyT) $ t $ tr t; in [("_toT", toT_tr)] end *}

variables may not be bound etc...

make Isabelle respect your variable convention, whatever it is. Easiest thing might be to mark the identifiers you want treated as specification variables with a dummy syntax. syntax (xsymbols) "_toT" :: "logic => logic" ("\<tau> _" [1000] 1000) "_v" :: "id => logic" ("\<v>_" [1000] 1000) parse_translation {* let fun mkpr s = s^"'"; fun st (Const("_v", _) $ Free(n, T)) = Free(n, T) | st (f $ a) = st f $ st a | st (Abs(n, T, b)) = Abs(mkpr n, T, st b) | st t = t; fun pr (Const("_v", _) $ Free(n, T)) = Free(mkpr n, T) | pr (f $ a) = pr f $ pr a | pr (Abs(n, T, b)) = Abs(mkpr n, T, pr b) | pr t = t; fun toT_tr [t] = Const("toT", dummyT) $ st t $ pr t; in [("_toT", toT_tr)] end *} term "\<tau> (\<v>a \<or> \<v>b)"

you still have to be careful. term "\<tau> (\<v> True \<or> False)" On 16/09/2005, at 6:09 AM, Reto Kramer wrote:

I'm an engineer trying to leverage Isabelle in practice. I appreciateyour patience if I did not get all the terminology right.The toT function below has the intuitive meaning that (toT a a') is true, iff a was false in the "old state" (unprimed),and changed to true in the "new state", a'(primed)constdefs toT :: "bool => bool => bool" (infix "\<Delta>" 60) "a \<Delta> a' == ~a /\ a'"To work out boolean operations involving toT (~, /\, \/, xor, liftingto forall and exist), it would be very nice if I could write theformulas a little more concisely. Specifically, I don't want to haveto repeat the a term, just to prime all it's variables.So I'd like to say \<tau> (a \/ b) = (~b /\ \<tau> a) \/ (~a /\ \<tau b>), where \<tau> a rewrites to ~a /\ a' (* 1 *) rather than (cumbersome \<Delta>)lemma "(a \/ b) \<Delta> (a' \/ b') = ((a \<Delta> a') /\ ~b) \/ ((b\<Delta> b') /\ ~a)"apply (simp only: toT_def) apply auto doneTo the "syntax" construct the views the a' as a new variable and thuscannot it won't allow the rewrite I'm looking for in (* 1 *).I suppose I need a meta operation such that \<tau> manufactures a newterm t' in which all of the original terms variables are primed.Is there an Isabelle/HOL feature that lets me manufacture new termsfrom old one (for generic bool terms, including new operations, like\<tau> itself)?Thanks, - Reto

Dr Brendan Mahony Information Networks Division ph +61 8 8259 6046 Defence Science and Technology Organisation fx +61 8 8259 5589 Salisbury, South Australia Brendan.Mahony at dsto.defence.gov.au Important: This document remains the property of the Australian Government Department of Defence and is subject to the jurisdiction

you are requested to contact the sender and delete the document.

**References**:**[isabelle] "syntax" challange***From:*Reto Kramer

- Previous by Date: Re: [isabelle] recdef problem
- Next by Date: Re: [isabelle] recdef problem
- Previous by Thread: [isabelle] "syntax" challange
- Next by Thread: [isabelle] who knows theorem-proving about cache protocols
- Cl-isabelle-users September 2005 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