[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",
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)
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and