Re: [isabelle] "syntax" challange



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

*}

It works for you examples, but will give strange results at times, because when the parse translation happens, some constants have not yet been recognised, bound
variables may not be bound etc...

I think you'll have trouble making it really fly, because you have no real way to
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)"

Now you have good control over what gets the priming treatment. Of course,
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 appreciate your 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, lifting to forall and exist), it would be very nice if I could write the formulas a little more concisely. Specifically, I don't want to have to 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
  done

To the "syntax" construct the views the a' as a new variable and thus cannot it won't allow the rewrite I'm looking for in (* 1 *).

I suppose I need a meta operation such that \<tau> manufactures a new term t' in which all of the original terms variables are primed.

Is there an Isabelle/HOL feature that lets me manufacture new terms from 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
of the Crimes Act section 70. If you have received this document in error,
you are requested to contact the sender and delete the document.






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