# [isabelle] Definition

Hi
Just to clarify my previous email, I tried to define a signal with point
(t,x) where t is the time and x is the amplitude <x(t)> and both t and x
are belong to u. Then u is included in signal set. The next step I have to
define a set of signals. So I have problem with proving that x â u and also
uâ set_of_signals. I tried many lemmas as below:
definition signal :: "_"
where signal_def : "signal T R = {u| u. âtâT. â!xâR. (t,x)â u }"
definition sos :: "_"
where "sos T R = {u | u. u â signal T R }"
lemma subset_u: "u â signal T R " unfolding signal_def by blast
Its proved but I think there is problem with using blast as it highlight in
purple!
also I tried this, but it doesn't work:
lemma bb:
assumes a: "signal T R = {u| u. âtâT. â!xâR. (t,x)â u }"
and "T={tââ . (ât. 0ât â t<â )}"
shows "u â signal T R "
proof
fix x
assume n:"xâu"
show "xâsignal T R "
proof
from n have ?thesis by(simp add: signal_def)
so does the upper statement correct or I have to use something else?
regards
Omar

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