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

I ask you several things:

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

locale generalization =
  fixes big::i and small::i
  fixes embed::i
  assumes is_inj: "embded: inj(small, big)"

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"
  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

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"
  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"

theorem move_inj: "move: inj(big, newbig)"
  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"
    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"
    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"
    assume "a~: small2" "b~: small2"
    have "move`a = <token,a>"
    have "move`b = <token,b>"
    have "<token,a>=<token,b>"
    show "a = b"
  show "a = b"

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)"
  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)"



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