# [isabelle] "syntax" challange

`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

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