Theory Perm

(*  Title:      ZF/Perm.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge

The theory underlying permutation groups
  -- Composition of relations, the identity relation
  -- Injections, surjections, bijections
  -- Lemmas for the Schroeder-Bernstein Theorem

section‹Injections, Surjections, Bijections, Composition›

theory Perm imports func begin

  (*composition of relations and functions; NOT Suppes's relative product*)
  comp     :: "[i,i]i"      (infixr O 60)  where
    "r O s  {xz  domain(s)*range(r) .
               x y z. xz=x,z  x,y:s  y,z:r}"

  (*the identity function for A*)
  id    :: "ii"  where
    "id(A)  (λxA. x)"

  (*one-to-one functions from A to B*)
  inj   :: "[i,i]i"  where
    "inj(A,B)  { f  A->B. wA. xA. f`w=f`x  w=x}"

  (*onto functions from A to B*)
  surj  :: "[i,i]i"  where
    "surj(A,B)  { f  A->B . yB. xA. f`x=y}"

  (*one-to-one and onto functions*)
  bij   :: "[i,i]i"  where
    "bij(A,B)  inj(A,B)  surj(A,B)"

subsection‹Surjective Function Space›

lemma surj_is_fun: "f  surj(A,B)  f  A->B"
  unfolding surj_def
apply (erule CollectD1)

lemma fun_is_surj: "f  Pi(A,B)  f  surj(A,range(f))"
  unfolding surj_def
apply (blast intro: apply_equality range_of_fun domain_type)

lemma surj_range: "f  surj(A,B)  range(f)=B"
  unfolding surj_def
apply (best intro: apply_Pair elim: range_type)

text‹A function with a right inverse is a surjection›

lemma f_imp_surjective:
    "f  A->B;  y. y  B  d(y): A;  y. y  B  f`d(y) = y
      f  surj(A,B)"
  by (simp add: surj_def, blast)

lemma lam_surjective:
    "x. x  A  c(x): B;
        y. y  B  d(y): A;
        y. y  B  c(d(y)) = y
  (λxA. c(x))  surj(A,B)"
apply (rule_tac d = d in f_imp_surjective)
apply (simp_all add: lam_type)

text‹Cantor's theorem revisited›
lemma cantor_surj: "f  surj(A,Pow(A))"
apply (unfold surj_def, safe)
apply (cut_tac cantor)
apply (best del: subsetI)

subsection‹Injective Function Space›

lemma inj_is_fun: "f  inj(A,B)  f  A->B"
  unfolding inj_def
apply (erule CollectD1)

text‹Good for dealing with sets of pairs, but a bit ugly in use [used in AC]›
lemma inj_equality:
    "a,b:f;  c,b:f;  f  inj(A,B)  a=c"
  unfolding inj_def
apply (blast dest: Pair_mem_PiD)

lemma inj_apply_equality: "f  inj(A,B);  f`a=f`b;  a  A;  b  A  a=b"
by (unfold inj_def, blast)

text‹A function with a left inverse is an injection›

lemma f_imp_injective: "f  A->B;  xA. d(f`x)=x  f  inj(A,B)"
apply (simp (no_asm_simp) add: inj_def)
apply (blast intro: subst_context [THEN box_equals])

lemma lam_injective:
    "x. x  A  c(x): B;
        x. x  A  d(c(x)) = x
      (λxA. c(x))  inj(A,B)"
apply (rule_tac d = d in f_imp_injective)
apply (simp_all add: lam_type)


lemma bij_is_inj: "f  bij(A,B)  f  inj(A,B)"
  unfolding bij_def
apply (erule IntD1)

lemma bij_is_surj: "f  bij(A,B)  f  surj(A,B)"
  unfolding bij_def
apply (erule IntD2)

lemma bij_is_fun: "f  bij(A,B)  f  A->B"
  by (rule bij_is_inj [THEN inj_is_fun])

lemma lam_bijective:
    "x. x  A  c(x): B;
        y. y  B  d(y): A;
        x. x  A  d(c(x)) = x;
        y. y  B  c(d(y)) = y
  (λxA. c(x))  bij(A,B)"
  unfolding bij_def
apply (blast intro!: lam_injective lam_surjective)

lemma RepFun_bijective: "(yx. ∃!y'. f(y') = f(y))
       (λz{f(y). y  x}. THE y. f(y) = z)  bij({f(y). y  x}, x)"
apply (rule_tac d = f in lam_bijective)
apply (auto simp add: the_equality2)

subsection‹Identity Function›

lemma idI [intro!]: "a  A  a,a  id(A)"
  unfolding id_def
apply (erule lamI)

lemma idE [elim!]: "p  id(A);  x.x  A; p=x,x  P   P"
by (simp add: id_def lam_def, blast)

lemma id_type: "id(A)  A->A"
  unfolding id_def
apply (rule lam_type, assumption)

lemma id_conv [simp]: "x  A  id(A)`x = x"
  unfolding id_def
apply (simp (no_asm_simp))

lemma id_mono: "A<=B  id(A)  id(B)"
  unfolding id_def
apply (erule lam_mono)

lemma id_subset_inj: "A<=B  id(A): inj(A,B)"
apply (simp add: inj_def id_def)
apply (blast intro: lam_type)

lemmas id_inj = subset_refl [THEN id_subset_inj]

lemma id_surj: "id(A): surj(A,A)"
  unfolding id_def surj_def
apply (simp (no_asm_simp))

lemma id_bij: "id(A): bij(A,A)"
  unfolding bij_def
apply (blast intro: id_inj id_surj)

lemma subset_iff_id: "A  B  id(A)  A->B"
  unfolding id_def
apply (force intro!: lam_type dest: apply_type)

texttermid as the identity relation›
lemma id_iff [simp]: "x,y  id(A)  x=y  y  A"
by auto

subsection‹Converse of a Function›

lemma inj_converse_fun: "f  inj(A,B)  converse(f)  range(f)->A"
  unfolding inj_def
apply (simp (no_asm_simp) add: Pi_iff function_def)
apply (erule CollectE)
apply (simp (no_asm_simp) add: apply_iff)
apply (blast dest: fun_is_rel)

text‹Equations for converse(f)›

text‹The premises are equivalent to saying that f is injective...›
lemma left_inverse_lemma:
     "f  A->B;  converse(f): C->A;  a  A  converse(f)`(f`a) = a"
by (blast intro: apply_Pair apply_equality converseI)

lemma left_inverse [simp]: "f  inj(A,B);  a  A  converse(f)`(f`a) = a"
by (blast intro: left_inverse_lemma inj_converse_fun inj_is_fun)

lemma left_inverse_eq:
     "f  inj(A,B); f ` x = y; x  A  converse(f) ` y = x"
by auto

lemmas left_inverse_bij = bij_is_inj [THEN left_inverse]

lemma right_inverse_lemma:
     "f  A->B;  converse(f): C->A;  b  C  f`(converse(f)`b) = b"
by (rule apply_Pair [THEN converseD [THEN apply_equality]], auto)

(*Should the premises be f ∈ surj(A,B), b ∈ B for symmetry with left_inverse?
  No: they would not imply that converse(f) was a function! *)
lemma right_inverse [simp]:
     "f  inj(A,B);  b  range(f)  f`(converse(f)`b) = b"
by (blast intro: right_inverse_lemma inj_converse_fun inj_is_fun)

lemma right_inverse_bij: "f  bij(A,B);  b  B  f`(converse(f)`b) = b"
by (force simp add: bij_def surj_range)

subsection‹Converses of Injections, Surjections, Bijections›

lemma inj_converse_inj: "f  inj(A,B)  converse(f): inj(range(f), A)"
apply (rule f_imp_injective)
apply (erule inj_converse_fun, clarify)
apply (rule right_inverse)
 apply assumption
apply blast

lemma inj_converse_surj: "f  inj(A,B)  converse(f): surj(range(f), A)"
by (blast intro: f_imp_surjective inj_converse_fun left_inverse inj_is_fun
                 range_of_fun [THEN apply_type])

text‹Adding this as an intro! rule seems to cause looping›
lemma bij_converse_bij [TC]: "f  bij(A,B)  converse(f): bij(B,A)"
  unfolding bij_def
apply (fast elim: surj_range [THEN subst] inj_converse_inj inj_converse_surj)

subsection‹Composition of Two Relations›

text‹The inductive definition package could derive these theorems for termr O s

lemma compI [intro]: "a,b:s; b,c:r  a,c  r O s"
by (unfold comp_def, blast)

lemma compE [elim!]:
    "xz  r O s;
        x y z. xz=x,z;  x,y:s;  y,z:r  P
by (unfold comp_def, blast)

lemma compEpair:
    "a,c  r O s;
        y. a,y:s;  y,c:r  P
by (erule compE, simp)

lemma converse_comp: "converse(R O S) = converse(S) O converse(R)"
by blast

subsection‹Domain and Range -- see Suppes, Section 3.1›

text‹Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327›
lemma range_comp: "range(r O s)  range(r)"
by blast

lemma range_comp_eq: "domain(r)  range(s)  range(r O s) = range(r)"
by (rule range_comp [THEN equalityI], blast)

lemma domain_comp: "domain(r O s)  domain(s)"
by blast

lemma domain_comp_eq: "range(s)  domain(r)  domain(r O s) = domain(s)"
by (rule domain_comp [THEN equalityI], blast)

lemma image_comp: "(r O s)``A = r``(s``A)"
by blast

lemma inj_inj_range: "f  inj(A,B)  f  inj(A,range(f))"
  by (auto simp add: inj_def Pi_iff function_def)

lemma inj_bij_range: "f  inj(A,B)  f  bij(A,range(f))"
  by (auto simp add: bij_def intro: inj_inj_range inj_is_fun fun_is_surj)

subsection‹Other Results›

lemma comp_mono: "r'<=r; s'<=s  (r' O s')  (r O s)"
by blast

text‹composition preserves relations›
lemma comp_rel: "s<=A*B;  r<=B*C  (r O s)  A*C"
by blast

text‹associative law for composition›
lemma comp_assoc: "(r O s) O t = r O (s O t)"
by blast

(*left identity of composition; provable inclusions are
        id(A) O r ⊆ r
  and   ⟦r<=A*B; B<=C⟧ ⟹ r ⊆ id(C) O r *)
lemma left_comp_id: "r<=A*B  id(B) O r = r"
by blast

(*right identity of composition; provable inclusions are
        r O id(A) ⊆ r
  and   ⟦r<=A*B; A<=C⟧ ⟹ r ⊆ r O id(C) *)
lemma right_comp_id: "r<=A*B  r O id(A) = r"
by blast

subsection‹Composition Preserves Functions, Injections, and Surjections›

lemma comp_function: "function(g);  function(f)  function(f O g)"
by (unfold function_def, blast)

text‹Don't think the premises can be weakened much›
lemma comp_fun: "g  A->B;  f  B->C  (f O g)  A->C"
apply (auto simp add: Pi_def comp_function Pow_iff comp_rel)
apply (subst range_rel_subset [THEN domain_comp_eq], auto)

(*Thanks to the new definition of "apply", the premise f ∈ B->C is gone!*)
lemma comp_fun_apply [simp]:
     "g  A->B;  a  A  (f O g)`a = f`(g`a)"
apply (frule apply_Pair, assumption)
apply (simp add: apply_def image_comp)
apply (blast dest: apply_equality)

text‹Simplifies compositions of lambda-abstractions›
lemma comp_lam:
    "x. x  A  b(x): B
      (λyB. c(y)) O (λxA. b(x)) = (λxA. c(b(x)))"
apply (subgoal_tac "(λxA. b(x))  A -> B")
 apply (rule fun_extension)
   apply (blast intro: comp_fun lam_funtype)
  apply (rule lam_funtype)
 apply simp
apply (simp add: lam_type)

lemma comp_inj:
     "g  inj(A,B);  f  inj(B,C)  (f O g)  inj(A,C)"
apply (frule inj_is_fun [of g])
apply (frule inj_is_fun [of f])
apply (rule_tac d = "λy. converse (g) ` (converse (f) ` y)" in f_imp_injective)
 apply (blast intro: comp_fun, simp)

lemma comp_surj:
    "g  surj(A,B);  f  surj(B,C)  (f O g)  surj(A,C)"
  unfolding surj_def
apply (blast intro!: comp_fun comp_fun_apply)

lemma comp_bij:
    "g  bij(A,B);  f  bij(B,C)  (f O g)  bij(A,C)"
  unfolding bij_def
apply (blast intro: comp_inj comp_surj)

subsection‹Dual Properties of terminj and termsurj

text‹Useful for proofs from
    D Pastre.  Automatic theorem proving in set theory.
    Artificial Intelligence, 10:1--27, 1978.›

lemma comp_mem_injD1:
    "(f O g): inj(A,C);  g  A->B;  f  B->C  g  inj(A,B)"
by (unfold inj_def, force)

lemma comp_mem_injD2:
    "(f O g): inj(A,C);  g  surj(A,B);  f  B->C  f  inj(B,C)"
apply (unfold inj_def surj_def, safe)
apply (rule_tac x1 = x in bspec [THEN bexE])
apply (erule_tac [3] x1 = w in bspec [THEN bexE], assumption+, safe)
apply (rule_tac t = "(`) (g) " in subst_context)
apply (erule asm_rl bspec [THEN bspec, THEN mp])+
apply (simp (no_asm_simp))

lemma comp_mem_surjD1:
    "(f O g): surj(A,C);  g  A->B;  f  B->C  f  surj(B,C)"
  unfolding surj_def
apply (blast intro!: comp_fun_apply [symmetric] apply_funtype)

lemma comp_mem_surjD2:
    "(f O g): surj(A,C);  g  A->B;  f  inj(B,C)  g  surj(A,B)"
apply (unfold inj_def surj_def, safe)
apply (drule_tac x = "f`y" in bspec, auto)
apply (blast intro: apply_funtype)

subsubsection‹Inverses of Composition›

text‹left inverse of composition; one inclusion is
        termf  A->B  id(A)  converse(f) O f
lemma left_comp_inverse: "f  inj(A,B)  converse(f) O f = id(A)"
apply (unfold inj_def, clarify)
apply (rule equalityI)
 apply (auto simp add: apply_iff, blast)

text‹right inverse of composition; one inclusion is
                termf  A->B  f O converse(f)  id(B)
lemma right_comp_inverse:
    "f  surj(A,B)  f O converse(f) = id(B)"
apply (simp add: surj_def, clarify)
apply (rule equalityI)
apply (best elim: domain_type range_type dest: apply_equality2)
apply (blast intro: apply_Pair)

subsubsection‹Proving that a Function is a Bijection›

lemma comp_eq_id_iff:
    "f  A->B;  g  B->A  f O g = id(B)  (yB. f`(g`y)=y)"
apply (unfold id_def, safe)
 apply (drule_tac t = "λh. h`y " in subst_context)
 apply simp
apply (rule fun_extension)
  apply (blast intro: comp_fun lam_type)
 apply auto

lemma fg_imp_bijective:
    "f  A->B;  g  B->A;  f O g = id(B);  g O f = id(A)  f  bij(A,B)"
  unfolding bij_def
apply (simp add: comp_eq_id_iff)
apply (blast intro: f_imp_injective f_imp_surjective apply_funtype)

lemma nilpotent_imp_bijective: "f  A->A;  f O f = id(A)  f  bij(A,A)"
by (blast intro: fg_imp_bijective)

lemma invertible_imp_bijective:
     "converse(f): B->A;  f  A->B  f  bij(A,B)"
by (simp add: fg_imp_bijective comp_eq_id_iff
              left_inverse_lemma right_inverse_lemma)

subsubsection‹Unions of Functions›

text‹See similar theorems in func.thy›

text‹Theorem by KG, proof by LCP›
lemma inj_disjoint_Un:
     "f  inj(A,B);  g  inj(C,D);  B  D = 0
       (λaA  C. if a  A then f`a else g`a)  inj(A  C, B  D)"
apply (rule_tac d = "λz. if z  B then converse (f) `z else converse (g) `z"
       in lam_injective)
apply (auto simp add: inj_is_fun [THEN apply_type])

lemma surj_disjoint_Un:
    "f  surj(A,B);  g  surj(C,D);  A  C = 0
      (f  g)  surj(A  C, B  D)"
apply (simp add: surj_def fun_disjoint_Un)
apply (blast dest!: domain_of_fun
             intro!: fun_disjoint_apply1 fun_disjoint_apply2)

text‹A simple, high-level proof; the version for injections follows from it,
  using  termf  inj(A,B)  f  bij(A,range(f))
lemma bij_disjoint_Un:
     "f  bij(A,B);  g  bij(C,D);  A  C = 0;  B  D = 0
       (f  g)  bij(A  C, B  D)"
apply (rule invertible_imp_bijective)
apply (subst converse_Un)
apply (auto intro: fun_disjoint_Un bij_is_fun bij_converse_bij)

subsubsection‹Restrictions as Surjections and Bijections›

lemma surj_image:
    "f  Pi(A,B)  f  surj(A, f``A)"
apply (simp add: surj_def)
apply (blast intro: apply_equality apply_Pair Pi_type)

lemma surj_image_eq: "f  surj(A, B)  f``A = B"
  by (auto simp add: surj_def image_fun) (blast dest: apply_type) 

lemma restrict_image [simp]: "restrict(f,A) `` B = f `` (A  B)"
by (auto simp add: restrict_def)

lemma restrict_inj:
    "f  inj(A,B);  C<=A  restrict(f,C): inj(C,B)"
  unfolding inj_def
apply (safe elim!: restrict_type2, auto)

lemma restrict_surj: "f  Pi(A,B);  C<=A  restrict(f,C): surj(C, f``C)"
apply (insert restrict_type2 [THEN surj_image])
apply (simp add: restrict_image)

lemma restrict_bij:
    "f  inj(A,B);  C<=A  restrict(f,C): bij(C, f``C)"
apply (simp add: inj_def bij_def)
apply (blast intro: restrict_surj surj_is_fun)

subsubsection‹Lemmas for Ramsey's Theorem›

lemma inj_weaken_type: "f  inj(A,B);  B<=D  f  inj(A,D)"
  unfolding inj_def
apply (blast intro: fun_weaken_type)

lemma inj_succ_restrict:
     "f  inj(succ(m), A)  restrict(f,m)  inj(m, A-{f`m})"
apply (rule restrict_bij [THEN bij_is_inj, THEN inj_weaken_type], assumption, blast)
  unfolding inj_def
apply (fast elim: range_type mem_irrefl dest: apply_equality)

lemma inj_extend:
    "f  inj(A,B);  aA;  bB
      cons(a,b,f)  inj(cons(a,A), cons(b,B))"
  unfolding inj_def
apply (force intro: apply_type  simp add: fun_extend)