Email Gateway (Aug 22 2022 at 12:53): Email Gateway (Aug 22 2022 at 12:53):From: Omar Jasim <oajasim1@sheffield.ac.uk>
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
Email Gateway (Aug 22 2022 at 12:53):From: Lawrence Paulson <lp15@cam.ac.uk>
On 30 Mar 2016, at 16:20, Omar Jasim <oajasim1@sheffield.ac.uk> wrote:
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!
There are some big misunderstandings here. Because u is a variable, proving subset_u would mean that signal T R was the universal set.
definition sos :: "_"
where "sos T R = {u | u. u ∈ signal T R }”
This definition makes sos identical to signal, so probably you had something else in mind.
Larry Paulson
Last updated: Nov 21 2024 at 12:39 UTC