Email Gateway (Aug 18 2022 at 10:12): Email Gateway (Aug 18 2022 at 10:12):From: "Kobayashi, Hidetsune" <hd_coba@yahoo.co.jp>
Hello!
Let A be a naive set, then is it true that
arbitrary \<in> A ?
The question arose when I tryed to prove the following:
constdefs
domain_test::"['a set, nat, nat => 'a] => bool"
"domain_test A n f == f \<in> extensional {j. j \<le> n} \<and>
(\<forall>j \<le> n. f j \<in> A)"
lemma test:"[| domain_test A n f; domain_test A m f |] ==> n = m"
Is this lemma true? If this is true, is there any proof?
Hidetsune Kobayashi
Email Gateway (Aug 18 2022 at 10:12):From: Tjark Weber <tjark.weber@gmx.de>
On Thursday 15 February 2007 23:18, Kobayashi, Hidetsune wrote:
Let A be a naive set, then is it true that
arbitrary \<in> A ?
Not necessarily. You can think of "arbitrary" as a completely unspecified
constant, so unless A = UNIV, you won't be able to prove arbitrary \<in> A.
(Note that you won't be able to prove arbitrary \<notin> A either, unless A =
\<emptyset>.)
The question arose when I tryed to prove the following:
constdefs
domain_test::"['a set, nat, nat => 'a] => bool"
"domain_test A n f == f \<in> extensional {j. j \<le> n} \<and>
(\<forall>j \<le> n. f j \<in> A)"lemma test:"[| domain_test A n f; domain_test A m f |] ==> n = m"
Is this lemma true? If this is true, is there any proof?
Assuming that extensional is defined as
"extensional A = {f. \<forall>x. x~:A --> f x = arbitrary}",
the lemma is not true. The problem is once again that "arbitrary" is just a
name for some specific value; it is not a value on its own that's somehow
magically different from all other values. So "f j = arbitrary" and "f j
\<in> A" may both be true.
If you want to model partial functions, then another possibility is to use the
"'a option" datatype, with constructors "None" and "Some 'a". The following
lemma is indeed true, because "None" is provably different from "Some a":
constdefs
domain_test' :: "['a set, nat, nat => 'a] => bool"
"domain_test' A n f == (\<forall>j. n < j --> f j = None) \<and>
(\<forall>j\<le>n. \<exists>a\<in>A. f j = Some a)"
lemma: "[| domain_test' A n f; domain_test' A m f |] ==> n = m"
See theory HOL/Map (http://isabelle.in.tum.de/dist/library/HOL/Map.html) for
existing related syntax and lemmas. I'm not sure however how well this
approach would go together with the Algebra theories.
Best,
Tjark
Email Gateway (Aug 18 2022 at 10:12):From: "Kobayashi, Hidetsune" <hd_coba@yahoo.co.jp>
Thanks, Tjark. The lemma should be true, (if not,
~~~~
there is a function which is equal to a strict
^^^^^^^
restriction of itself).
Hidetsune
--- Tjark Weber <tjark.weber@gmx.de> wrote:
Start Yahoo! Auction now! Check out the cool campaign
http://pr.mail.yahoo.co.jp/auction/
Email Gateway (Aug 18 2022 at 10:12):From: Clemens Ballarin <ballarin@in.tum.de>
Dear Hidetsune,
unfortunately, modelling partial functions with arbitrary is rather
counter-intuitive and weak. Since arbitrary is an (unspecified)
element from the underlying type, it is not possible to determine the
domain of such a function. The function could be undefined at point x,
or it could map x to a value that coincides with the (unspecified)
value of arbitrary.
If you want to deal with partial functions seriously, you will have to
make the domain explicit. I can think of two ways of dealing with
this. You can either make the function a pair (f, A) where A is the
domain of f. Or you let f be of type 'a => 'b option, and x is in the
domain of f iff f x = None. Both are precise but not convenient to
deal with, I'm afraid.
Clemens
Email Gateway (Aug 18 2022 at 10:12):From: "Dr. Brendan Patrick Mahony" <brendan.mahony@dsto.defence.gov.au>
There is of course a third (Z) option: modelling partial functions as
deterministic relations,
ie ('a * 'b) set. This is similar to the 'a => 'b option model in
most respects, but is
slightly more natural when defining finite functions and has the
advantage of inheriting a lot of
machinery from the relational super-type.
You can reduce this model (and those mentioned by Clemens) to the
arbitrary-off-domain model by defining an application operator, in
this case
f.x = (THE y. (x, y) : f),
but you now have the advantage of an explicit record of the domain.
Dr Brendan Mahony
Information Networks Division ph +61 8 8259 6046
Defence Science and Technology Organisation fx +61 8 8259 5589
Edinburgh, South Australia Brendan.Mahony@dsto.defence.gov.au
Important: This document remains the property of the Australian
Government Department of Defence and is subject to the jurisdiction
of the Crimes Act section 70. If you have received this document in
error, you are requested to contact the sender and delete the document.
Last updated: May 03 2024 at 08:18 UTC