Email Gateway (Aug 18 2022 at 13:09): Email Gateway (Aug 18 2022 at 13:09):From: Victor Porton <porton@narod.ru>
Hi,
I am a novice to Isabelle.
The below theory does not verify at the point of "by (unfold bij_converse_bij)". What it should be replaced to? Which document to read about this kind of questions I ask?
Before presenting my theory I want to explain what I am trying to achieve: Suppose (in ZF) we have two sets 'small' and 'big' (not necessarily disjoint) and an injection 'embed' from small to big. I want to replace 'big' with 'newbig' so that 'newbig' would bijectively correspond to 'big' but 'small' would become a subset of 'newbig'. Example: 'small' are integers, 'big' are reals, we want to embed the set of integers into the (another) set of reals. Another example: 'small' is the powerset of some set, 'big' is the set of filters on 'small', 'embed' maps every set to the corresponding principal filter; so filters are considered as a generalization of sets.
Well, below my theory:
theory embedding
imports ZF Perm
begin
locale embedding2 =
fixes big::i and small::i
fixes embed
assumes is_inj: "embded: inj(small, big)"
begin
(* <a,b> == {{a,a}, {a,b}} *)
definition "newbig == big" (to be replaced with the real definition)
definition "move == 0" (to be replaced with the real definition)
definition "ret == converse(move)"
theorem "small <= newbig"
sorry
theorem "move: bij(big, newbig)"
sorry
theorem "ret: bij(newbig, big)"
by (unfold bij_converse_bij)
end
end
Email Gateway (Aug 18 2022 at 13:09):From: Slawomir Kolodynski <skokodyn@yahoo.com>
Technically, you can do it by removing the image of small from big and putting small in place of it. Something like this
theory test2 imports Cardinal
begin
definition
"Emedding(embed, small, big) \<equiv> small \<union> (big - embed``(small))"
text{Embedding is bijective with big and small is contained in it.}
lemma emmbed_prop: assumes "embed \<in> inj(small, big)"
shows
"big \<approx> Emedding(embed, small, big)" and
"small \<subseteq> Emedding(embed, small, big)"
sorry
Slawekk
Email Gateway (Aug 18 2022 at 13:09):From: Victor Porton <porton@narod.ru>
-------- Пересылаемое сообщение --------
Email Gateway (Aug 18 2022 at 13:09):From: Victor Porton <porton@narod.ru>
-------- Пересылаемое сообщение --------
14.03.09, 22:18, "Victor Porton" <porton@narod.ru>:
14.03.09, 21:01, "Slawomir Kolodynski" <skokodyn@yahoo.com>:
Slawomir, your solution may fail if small and big aren't
disjoint.
True. A better definition would be
definition
"Emedding(embed, small, big) \<equiv>
(small - big) \<union> (big - embed``(small - big))"
What is "``"? I'm a novice with Isabelle and don't understand two backquotes.
definition "ret == converse(move)"
I don't understand this definition. The right hand side depends on a variable "move" and the left hand does not. Is "move" a constant? How it is defined?
"move" should be a constant. It will be defined in a somehow tricky way. For now we can use the stub definition:
definition "move == 0" (to be replaced with the real definition)
-------- Завершение пересылаемого сообщения --------
Last updated: May 03 2024 at 08:18 UTC