# [isabelle] Brilliant but broken theory

```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.

1. 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.

2. Put the theory into the Isabelle package.

3. 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 "embed`x: small2"
then "move`(embed`x) = spec`(embed`x)"
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 "move`a = move`b"
proof cases
assume "a: small2" "b: small2"
have "move`a = spec`a"
have "move`b = spec`b"
have "spec`a = spec`b"
using spec_bij show "a = b"
next
assume "a: small2" "b~: small2"
have "move`a = spec`a"
have "move`b = <token,b>"
have "move`a: small"
have "move`b~: small" by token_not_small
show "False"
next
assume "a~: small2" "b: small2"
have "move`a = <token,a>"
have "move`b = spec`b"
have "move`a~: small"
have "move`b: small" by token_not_small
show "False"
next
assume "a~: small2" "b~: small2"
have "move`a = <token,a>"
have "move`b = <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 "embed`x: small2"
have "move`(embed`x) = spec`(embed`x)"
from converse_embed have "move`(embed`x) = x"
show "move O embded = id(small)"
qed

end

end;

```

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