[isabelle] Definition


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

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 "
fix x
assume n:"xâu"
show "xâsignal T R "
from n have ?thesis by(simp add: signal_def)

so does the upper statement correct or I have to use something else?


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