[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.