Theory Generalization_ZF

(* 
    This file is a part of IsarMathLib - 
    a library of formalized mathematics written for Isabelle/Isar.

    Copyright (C) 2011 Victor Porton

    This program is free software; Redistribution and use in source and binary forms, 
    with or without modification, are permitted provided that the following conditions are met:

   1. Redistributions of source code must retain the above copyright notice, 
   this list of conditions and the following disclaimer.
   2. Redistributions in binary form must reproduce the above copyright notice, 
   this list of conditions and the following disclaimer in the documentation and/or 
   other materials provided with the distribution.
   3. The name of the author may not be used to endorse or promote products 
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED 
WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF 
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. 
IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, 
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; 
OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, 
WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR 
OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, 
EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *)

header{*\isaheader{Generalization\_ZF.thy}*}

theory Generalization_ZF imports func1

begin

text{*
  This theory formalizes the intuitive notion of \emph{generalization}.

  See http://www.mathematics21.org/generalization.html for more details.

  Contributed by Victor Porton.
  *}


section{* Generalization situation *}

text{*In mathematics it is often encountered that a small set $S$ 
  naturally bijectively corresponds to a
  subset $R$ of a larger set $B$. (In other words, there is specified an injection 
  $E$ from $S$ to $B$.) It is a widespread practice to equate $S$ with $R$.
  But strictly speaking this equating may contradict to the axioms of ZF/ZFC 
  because we are not insured against $S\cap B\neq \emptyset$ incidents.
  To work around of this (and formulate things exactly what could benefit 
  computer proof assistants) we will replace the set B with a new set B 
  having a bijection $M : B \rightarrow B$ such that $M \circ E = id_S$. 
  (I call this bijection $M$ from the first letter of the word "move" 
  which signifies the move from the old set $B$ to a new set $B$.
  This section contains some basic lemmas holding in this setup. 
  *}

text{*The next locale defines our assumptions.*}

locale generalization =
  fixes small and big
  fixes embed
  assumes embed_inj: "embed ∈ inj(small, big)"

text{*We define the @{text "small2"} set as the range of @{text "embed"}.*}

definition (in generalization) "small2 ≡ range(embed)"

text{*We define @{text "spec"} as the converse of @{text "embed"}.*}

definition (in generalization) "spec ≡ converse(embed)"

text{*Spec is an injection from range of @{text "embed"} to @{text "small"}.*}

lemma (in generalization) spec_inj: shows "spec ∈ inj(small2, small)"
  using embed_inj inj_converse_inj small2_def spec_def by simp

text{*Spec maps range of @{text "embed"} to @{text "small"}.*}

lemma (in generalization) spec_fun: shows "spec: small2→small"
  using embed_inj inj_converse_fun small2_def spec_def by simp

text{*Embed maps @{text "small"}small to @{text "big"}.*}

lemma (in generalization) embed_fun: shows "embed: small→big"
  using  embed_inj inj_is_fun by simp

text{*Embed is a surjection from @{text "small"} to @{text "small2"}.*}

lemma (in generalization) embed_surj: shows "embed ∈ surj(small, small2)"
  using fun_is_surj embed_fun small2_def by simp

text{*Embed is a bijection between @{text "small"} and @{text "small2"}.*}

theorem (in generalization) embed_bij: shows "embed ∈ bij(small, small2)"
  using embed_inj inj_bij_range small2_def by simp

text{* @{text "small2"} (i.e. range of @{text "embed"}) is a 
  subset of @{text "big"}.*}

theorem (in generalization) small2_sub_big: shows "small2 ⊆ big"
  using embed_fun func1_1_L5B small2_def by simp

text{*@{text "spec"} is a bijection beween @{text "small2"} and @{text "small"}.*}

theorem (in generalization) spec_bij: shows "spec ∈ bij(small2, small)"
  using bij_converse_bij embed_bij spec_def by simp

section{*Arbitrary generalizations *}

text{*This section considers a more general situation.*}

text{*The next locale extends @{text "generalization"} 
  adding another big set and the @{text "move"} operation. *}

locale generalization1 = generalization +
  fixes newbig
  fixes move
  assumes move_bij: "move ∈ bij(big, newbig)"
  assumes move_embed: "move O embed = id(small)"

text{*in @{text "generalization1"} context we define @{text "ret"} 
  as the converse of @{text "move"}.*}

definition (in generalization1) "ret ≡ converse(move)"

text{* @{text "move"} is a map from @{text "big"} to @{text "newbig"}.*}

lemma (in generalization1) move_fun: shows "move: big→newbig" 
  using move_bij bij_is_fun by simp

text{*@{text "move"} is an injection from @{text "big"} to @{text "newbig"}. *}

lemma (in generalization1) move_inj: shows "move∈inj(big, newbig)" 
  using move_bij bij_is_inj by simp

text{*Move is a surjection @{text "big"} to @{text "newbig"}.*}

lemma (in generalization1) move_surj: shows "move∈surj(big, newbig)" 
  using move_bij bij_is_surj by simp

text{* @{text "big"} is the domain of @{text "move"}.*}

lemma (in generalization1) move_domain: shows "domain(move) = big" 
  using domain_of_fun move_fun by simp

text{*Composing @{text "move"} with @{text "embed"} takes elements of 
  @{text "small"} to themselves. *}

theorem (in generalization1) move_embed_plain: assumes "x∈small" 
  shows "move`(embed`(x)) = x"
proof -
  from assms have "move`(embed`(x)) = (move O embed)`(x)"
    using embed_fun comp_fun_apply by simp
  with assms show ?thesis using move_embed by simp
qed

text{* @{text "ret"} is a bijection from @{text "newbig"}newbig to @{text "big"}.*}

lemma (in generalization1) ret_bij: shows "ret∈bij(newbig, big)" 
  using move_bij ret_def by simp

text{* @{text "ret"} is a injection from @{text "newbig"} onto @{text "big"}.*}

lemma (in generalization1) ret_inj: shows "ret ∈ inj(newbig,big)" 
  using ret_bij bij_is_inj by simp

text{* @{text "ret"} is a surjection from @{text "newbig"} onto @{text "big"}.*}

lemma (in generalization1) ret_surj: shows "ret ∈ surj(newbig,big)" 
  using ret_bij bij_is_surj by simp

text{* @{text "embed"} is a restriciton of @{text "ret"} to @{text "small"}.*}

lemma (in generalization1) ret_restrict: shows "embed = restrict(ret, small)"
proof -
  have "embed⊆small×big" 
    using fun_is_rel embed_fun by auto
  moreover
  have "(converse(move) O move) O embed = converse(move) O id(small)" 
    using  move_embed comp_assoc by auto
  then have a: "id(big) O embed = converse(move) O id(small)"
    using left_comp_inverse move_inj by simp
  ultimately show ?thesis using left_comp_id right_comp_id_any ret_def
    by auto
qed

section{*ZF generalization*}

text{*We continue material from the previous section.*}


text{* We will need this lemma to assert that ZF generalization 
  is an arbitrary generalization: *}

lemma mem_not_refl_2: shows "{t} ∉ t"
  using foundation by auto

text{*Definition of token.*}

definition (in generalization) "token ≡ Pow(⋃(⋃(small)))"

text{*Definition of function moving the @{text "small"} set into @{text "big"}.*}

definition (in generalization) 
  "zf_move_fun(x) ≡ if x∈small2 then spec`(x) else ⟨token,x⟩"

text{*Definition of @{text "zf_move"} - the ZF version of @{text "zf_move_fun"}.*}

definition (in generalization)
  "zf_move ≡ {⟨x,zf_move_fun(x)⟩. x∈big}"

text{*Definition of @{text "zf_newbig"} as the range of @{text "zf_move"}.*}

definition (in generalization) "zf_newbig ≡ range(zf_move)"

text{* @{text "zf_move"} is a function that maps @{text "big"} to @{text "newbig"}.*}

lemma (in generalization) zf_move_fun: shows "zf_move: big→zf_newbig"
  using lam_is_fun_range zf_move_def zf_newbig_def by simp

text{* @{text "token"} is not in @{text "small"}.*}

lemma (in generalization) token_not_small: shows "⟨token,x⟩∉small"
proof
  assume "⟨token,x⟩∈small"
  then have "{token}∈token" using token_def Pair_def by auto
  then show False using mem_not_refl_2 by blast
qed

text{*Domain of @{text "zf_move"} is @{text "big"}.*}

lemma (in generalization) zf_move_domain: shows "domain(zf_move) = big"
  using  zf_move_fun func1_1_L1 by simp

text{* @{text "small"} is a subset of @{text "big"}.*}

theorem (in generalization) small_less_zf_newbig: 
  shows "small ⊆ zf_newbig"
proof
  fix x
  assume s: "x ∈ small"
  then have s1: "embed`(x) ∈ small2" 
    using embed_fun apply_rangeI small2_def
    by simp
  then have s2: "embed`(x)∈big" using small2_sub_big by auto
  with s1 s have x_val: "zf_move`(embed`(x)) = x" 
    using ZF_fun_from_tot_val zf_move_fun embed_inj 
      left_inverse spec_def zf_move_def zf_move_fun_def 
    by simp
  from s2 have "zf_move`(embed`(x))∈range(zf_move)" 
    using zf_move_fun apply_rangeI by simp
  with x_val show "x ∈ zf_newbig" using zf_newbig_def by auto
qed
  
text{* @{text "zf_move"} is an injection from @{text "big"}
  to @{text "zf_newbig"}. *}

theorem (in generalization) zf_move_inj: shows "zf_move∈inj(big, zf_newbig)"
proof -
  have "∀a∈big. ∀b∈big. 
    zf_move`(a) = zf_move`(b) ⟶ a=b"
  proof -
    {
      fix a b
      assume "a∈big" and "b∈big"
      then have spec1_a: "a∈small2  ⟶  zf_move`(a) = spec`(a)" and
        spec2_a: "a∉small2 ⟶ zf_move`a = ⟨token,a⟩" and
        spec1_b: "b∈small2  ⟶ zf_move`(b) = spec`(b)" and
        spec2_b: "b∉small2 ⟶ zf_move`(b) = ⟨token,b⟩"
        using ZF_fun_from_tot_val1 zf_move_fun_def zf_move_def 
        by auto
      assume move_eq: "zf_move`(a) = zf_move`(b)"
      have "a=b"
      proof -
        { assume "a∈small2" and "b∈small2"
          with `a∈small2` spec1_a `b∈small2` spec1_b move_eq
          have I: "spec`(a) = spec`(b)" by simp
          have "spec ∈ inj(small2,small)"
            using spec_inj by simp
          then have "spec ∈ 
            {f:small2 → small. ∀w∈small2. ∀x∈small2. f`(w)=f`(x) ⟶ w=x}"
            unfolding inj_def by auto
          hence "∀w∈small2. ∀x∈small2. spec`(w)=spec`(x) ⟶ w=x" by auto
          with `a∈small2` `b∈small2` I have "a=b" by auto
        }
        moreover
        { assume "a∈small2" "b∉small2"
          with spec1_a spec_fun have ma_s: "zf_move`a∈small"
            using apply_funtype by auto
          from `b∉small2` spec2_b have "zf_move`b∉small"
            using token_not_small by auto
           with move_eq ma_s have False by auto
        }
        moreover
        { assume "a∉small2" and "b∈small2"
          with spec1_b spec_fun have mb_s: "zf_move`(b)∈small" 
            using apply_funtype by auto
          from `a∉small2` spec2_a  have "zf_move`(a)∉small"
            using token_not_small by auto
          with move_eq mb_s have False by auto
        }
        moreover
        { assume "a∉small2" and "b∉small2"
          with spec2_a spec2_b have 
            "zf_move`(a) = ⟨token,a⟩" and
            "zf_move`(b) = ⟨token,b⟩"
            by auto
          with move_eq have "a=b" by auto 
        }
        ultimately show "a=b" by auto
      qed
    }
    thus ?thesis by auto
  qed
  with zf_move_fun show ?thesis using inj_def by simp
qed

text{* @{text "zf_move"} is a surjection of @{text "big"} onto  @{text "zf_newbig"}.*}

theorem (in generalization) zf_move_surj: 
  shows "zf_move ∈ surj(big,zf_newbig)"
  using zf_move_fun fun_is_surj zf_newbig_def by simp

text{* @{text "zf_move"} is a bijection from @{text "big"} to  @{text "zf_newbig"}.*}

theorem (in generalization) zf_move_bij: shows "zf_move ∈ bij(big, zf_newbig)"
  using zf_move_inj inj_bij_range zf_newbig_def by simp

text{*The essential condition to prove that composition of @{text "zf_move"} 
  and @{text "embed"} is identity.*}

theorem (in generalization) zf_move_embed: 
  assumes "x ∈ small" shows "zf_move`(embed`(x)) = x"
  using assms embed_fun apply_rangeI small2_sub_big ZF_fun_from_tot_val1
    embed_inj small2_def spec_def zf_move_def zf_move_fun_def by auto

text{*Composition of @{text "zf_move"}  and @{text "embed"} is identity.*}

theorem (in generalization) zf_embed_move: shows "zf_move O embed = id(small)"
proof -
  have "∀y∈small. zf_move`(embed`y) = y" and 
     "embed: small→big" and "zf_move: big→zf_newbig"
    using zf_move_embed embed_fun zf_move_fun by auto
  then show ?thesis using comp_eq_id_iff1 by blast
qed


end