Email Gateway (Aug 18 2022 at 13:12): Email Gateway (Aug 18 2022 at 13:12):From: Victor Porton <porton@narod.ru>
I have written my first Isabelle theory. It does not verify and my Isar
proofs are a monkey-nonsense. Indeed (after being corrected) this will
be a very important theory for Isabelle/ZF project. The idea is
brilliant, the implementation is poor.
My theory defines (bijective) modification ("newbig") of a set ("big")
in such a way that an another set "small" becomes it subset. "small" is
embedded into big by an injection "embed".
Example: We may modify the set of integers ("big") into an another
exemplar ("newbig") (that is bijective image) of integers which will
contain the set of naturals ("small"); "embed" is the correspondence of
naturals to integers. (In the current Isabelle/ZF naturals are not a
subset of integers and this needs to be corrected.)
We can further extend it to rational, real, and complex numbers, so that
our exemplars of these would contain each previous set.
Another example: We may want to identify the set of principal filters
with the corresponding lattice elements. Then filters is "big", our
lattice is "small" and "embed" is the function which maps a lattice
element into the corresponding principla filter.
I ask you several things:
Edit my broken theory in such the way that it would become good
quality (first, it should verify). I even ask you to create a perfect
example of Isar proofs. I would learn from this example.
Put the theory into the Isabelle package.
Decide how we will deal and how we will name sets produces using my
theory. (The bijective copy of the set "int" could become "int_obj",
"int_gen", "int_over_nat", etc. We need to chose a naming convention.)
My theory follows:
theory Generalization
imports ZF Perm upair
begin
locale generalization =
fixes big::i and small::i
fixes embed::i
assumes is_inj: "embded: inj(small, big)"
begin
definition "small2 == range(embed)"
definition converse_embed: "spec == converse(embed)"
theorem spec_bij: "spec: bij(small2, small)"
by auto
definition "token == Pow(Union(Union(small)))"
lemma token_not_small: "<token,x>~: small"
proof
assume "<token,x>: small"
have "{{token,token}, {token,x}}: small"
then "{{token}, {token,x}}: small"
then "{token}: Union(small)"
then "token <= Union(Union(small))"
then "token: Pow(Union(Union(small)))"
then "token: token"
then show False by mem_not_refl
qed
definition move_fun::"i=>i" where "move_fun(x) == if x: small2 then
spec`x else <token,x>"
definition "move == (lam x:big. move_fun(x))"
definition "newbig == range(move)"
definition ret_def: "ret == converse(move)"
theorem "small <= newbig"
proof
assume "x: small"
have "embedx: small2"
then "move(embedx) = spec(embedx)"
then "move(embed`x) = x"
then "x: range(move)"
show "x: newbig"
qed
theorem move_inj: "move: inj(big, newbig)"
proof
assume "a: big" "b:big" and "movea = moveb"
proof cases
assume "a: small2" "b: small2"
have "movea = speca"
have "moveb = specb"
have "speca = specb"
using spec_bij show "a = b"
next
assume "a: small2" "b~: small2"
have "movea = speca"
have "moveb = <token,b>"
have "movea: small"
have "moveb~: small" by token_not_small
show "False"
next
assume "a~: small2" "b: small2"
have "movea = <token,a>"
have "moveb = specb"
have "movea~: small"
have "moveb: small" by token_not_small
show "False"
next
assume "a~: small2" "b~: small2"
have "movea = <token,a>"
have "moveb = <token,b>"
have "<token,a>=<token,b>"
show "a = b"
qed
show "a = b"
qed
theorem move_surj: "move: surj(big, newbig)"
by auto
theorem move_bij: "move: bij(big, newbig)"
by auto
theorem ret_bij: "ret: bij(newbig, big)"
unfolding ret_def
using move_bij bij_converse_bij by simp
theorem embed_move: "move O embded = id(small)"
proof
assume "x: small"
have "embedx: small2"
have "move(embedx) = spec(embedx)"
from converse_embed have "move(embed`x) = x"
show "move O embded = id(small)"
qed
end
end;
Last updated: May 03 2024 at 12:27 UTC