src/ZF/Perm.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 47101 ded5cc757bc9
child 58871 c399ae4b836f
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
     1
(*  Title:      ZF/Perm.thy
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
The theory underlying permutation groups
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
  -- Composition of relations, the identity relation
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
  -- Injections, surjections, bijections
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
  -- Lemmas for the Schroeder-Bernstein Theorem
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
    11
header{*Injections, Surjections, Bijections, Composition*}
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
    12
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14883
diff changeset
    13
theory Perm imports func begin
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    15
definition
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    16
  (*composition of relations and functions; NOT Suppes's relative product*)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    17
  comp     :: "[i,i]=>i"      (infixr "O" 60)  where
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
    18
    "r O s == {xz \<in> domain(s)*range(r) .
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    19
               \<exists>x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    20
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    21
definition
1806
12708740f58d Converted to use constdefs instead of defs
paulson
parents: 1478
diff changeset
    22
  (*the identity function for A*)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    23
  id    :: "i=>i"  where
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    24
    "id(A) == (\<lambda>x\<in>A. x)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    26
definition
1806
12708740f58d Converted to use constdefs instead of defs
paulson
parents: 1478
diff changeset
    27
  (*one-to-one functions from A to B*)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    28
  inj   :: "[i,i]=>i"  where
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
    29
    "inj(A,B) == { f \<in> A->B. \<forall>w\<in>A. \<forall>x\<in>A. f`w=f`x \<longrightarrow> w=x}"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    31
definition
1806
12708740f58d Converted to use constdefs instead of defs
paulson
parents: 1478
diff changeset
    32
  (*onto functions from A to B*)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    33
  surj  :: "[i,i]=>i"  where
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
    34
    "surj(A,B) == { f \<in> A->B . \<forall>y\<in>B. \<exists>x\<in>A. f`x=y}"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    36
definition
1806
12708740f58d Converted to use constdefs instead of defs
paulson
parents: 1478
diff changeset
    37
  (*one-to-one and onto functions*)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    38
  bij   :: "[i,i]=>i"  where
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    39
    "bij(A,B) == inj(A,B) \<inter> surj(A,B)"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    40
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    41
41160
be34449f6cba Added two theorems about the concept of range. Tidied up the comments.
paulson
parents: 32960
diff changeset
    42
subsection{*Surjective Function Space*}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    43
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
    44
lemma surj_is_fun: "f \<in> surj(A,B) ==> f \<in> A->B"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    45
apply (unfold surj_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    46
apply (erule CollectD1)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    47
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    48
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
    49
lemma fun_is_surj: "f \<in> Pi(A,B) ==> f \<in> surj(A,range(f))"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    50
apply (unfold surj_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    51
apply (blast intro: apply_equality range_of_fun domain_type)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    52
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    53
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
    54
lemma surj_range: "f \<in> surj(A,B) ==> range(f)=B"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    55
apply (unfold surj_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    56
apply (best intro: apply_Pair elim: range_type)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    57
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    58
41160
be34449f6cba Added two theorems about the concept of range. Tidied up the comments.
paulson
parents: 32960
diff changeset
    59
text{* A function with a right inverse is a surjection *}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    60
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
    61
lemma f_imp_surjective:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
    62
    "[| f \<in> A->B;  !!y. y \<in> B ==> d(y): A;  !!y. y \<in> B ==> f`d(y) = y |]
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
    63
     ==> f \<in> surj(A,B)"
41160
be34449f6cba Added two theorems about the concept of range. Tidied up the comments.
paulson
parents: 32960
diff changeset
    64
  by (simp add: surj_def, blast)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    65
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
    66
lemma lam_surjective:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
    67
    "[| !!x. x \<in> A ==> c(x): B;
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
    68
        !!y. y \<in> B ==> d(y): A;
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
    69
        !!y. y \<in> B ==> c(d(y)) = y
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    70
     |] ==> (\<lambda>x\<in>A. c(x)) \<in> surj(A,B)"
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
    71
apply (rule_tac d = d in f_imp_surjective)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    72
apply (simp_all add: lam_type)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    73
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    74
41160
be34449f6cba Added two theorems about the concept of range. Tidied up the comments.
paulson
parents: 32960
diff changeset
    75
text{*Cantor's theorem revisited*}
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    76
lemma cantor_surj: "f \<notin> surj(A,Pow(A))"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
    77
apply (unfold surj_def, safe)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    78
apply (cut_tac cantor)
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
    79
apply (best del: subsetI)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    80
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    81
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    82
41160
be34449f6cba Added two theorems about the concept of range. Tidied up the comments.
paulson
parents: 32960
diff changeset
    83
subsection{*Injective Function Space*}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    84
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
    85
lemma inj_is_fun: "f \<in> inj(A,B) ==> f \<in> A->B"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    86
apply (unfold inj_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    87
apply (erule CollectD1)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    88
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    89
41160
be34449f6cba Added two theorems about the concept of range. Tidied up the comments.
paulson
parents: 32960
diff changeset
    90
text{*Good for dealing with sets of pairs, but a bit ugly in use [used in AC]*}
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
    91
lemma inj_equality:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
    92
    "[| <a,b>:f;  <c,b>:f;  f \<in> inj(A,B) |] ==> a=c"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    93
apply (unfold inj_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    94
apply (blast dest: Pair_mem_PiD)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    95
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    96
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
    97
lemma inj_apply_equality: "[| f \<in> inj(A,B);  f`a=f`b;  a \<in> A;  b \<in> A |] ==> a=b"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
    98
by (unfold inj_def, blast)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
    99
41160
be34449f6cba Added two theorems about the concept of range. Tidied up the comments.
paulson
parents: 32960
diff changeset
   100
text{* A function with a left inverse is an injection *}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   101
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   102
lemma f_imp_injective: "[| f \<in> A->B;  \<forall>x\<in>A. d(f`x)=x |] ==> f \<in> inj(A,B)"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   103
apply (simp (no_asm_simp) add: inj_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   104
apply (blast intro: subst_context [THEN box_equals])
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   105
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   106
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   107
lemma lam_injective:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   108
    "[| !!x. x \<in> A ==> c(x): B;
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   109
        !!x. x \<in> A ==> d(c(x)) = x |]
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   110
     ==> (\<lambda>x\<in>A. c(x)) \<in> inj(A,B)"
13784
b9f6154427a4 tidying (by script)
paulson
parents: 13611
diff changeset
   111
apply (rule_tac d = d in f_imp_injective)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   112
apply (simp_all add: lam_type)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   113
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   114
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   115
subsection{*Bijections*}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   116
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   117
lemma bij_is_inj: "f \<in> bij(A,B) ==> f \<in> inj(A,B)"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   118
apply (unfold bij_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   119
apply (erule IntD1)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   120
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   121
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   122
lemma bij_is_surj: "f \<in> bij(A,B) ==> f \<in> surj(A,B)"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   123
apply (unfold bij_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   124
apply (erule IntD2)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   125
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   126
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   127
lemma bij_is_fun: "f \<in> bij(A,B) ==> f \<in> A->B"
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   128
  by (rule bij_is_inj [THEN inj_is_fun])
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   129
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   130
lemma lam_bijective:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   131
    "[| !!x. x \<in> A ==> c(x): B;
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   132
        !!y. y \<in> B ==> d(y): A;
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   133
        !!x. x \<in> A ==> d(c(x)) = x;
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   134
        !!y. y \<in> B ==> c(d(y)) = y
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   135
     |] ==> (\<lambda>x\<in>A. c(x)) \<in> bij(A,B)"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   136
apply (unfold bij_def)
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   137
apply (blast intro!: lam_injective lam_surjective)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   138
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   139
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   140
lemma RepFun_bijective: "(\<forall>y\<in>x. EX! y'. f(y') = f(y))
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   141
      ==> (\<lambda>z\<in>{f(y). y \<in> x}. THE y. f(y) = z) \<in> bij({f(y). y \<in> x}, x)"
13784
b9f6154427a4 tidying (by script)
paulson
parents: 13611
diff changeset
   142
apply (rule_tac d = f in lam_bijective)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   143
apply (auto simp add: the_equality2)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   144
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   145
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   146
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   147
subsection{*Identity Function*}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   148
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   149
lemma idI [intro!]: "a \<in> A ==> <a,a> \<in> id(A)"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   150
apply (unfold id_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   151
apply (erule lamI)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   152
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   153
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   154
lemma idE [elim!]: "[| p \<in> id(A);  !!x.[| x \<in> A; p=<x,x> |] ==> P |] ==>  P"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   155
by (simp add: id_def lam_def, blast)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   156
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   157
lemma id_type: "id(A) \<in> A->A"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   158
apply (unfold id_def)
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   159
apply (rule lam_type, assumption)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   160
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   161
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   162
lemma id_conv [simp]: "x \<in> A ==> id(A)`x = x"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   163
apply (unfold id_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   164
apply (simp (no_asm_simp))
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   165
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   166
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   167
lemma id_mono: "A<=B ==> id(A) \<subseteq> id(B)"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   168
apply (unfold id_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   169
apply (erule lam_mono)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   170
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   171
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   172
lemma id_subset_inj: "A<=B ==> id(A): inj(A,B)"
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   173
apply (simp add: inj_def id_def)
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   174
apply (blast intro: lam_type)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   175
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   176
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 41160
diff changeset
   177
lemmas id_inj = subset_refl [THEN id_subset_inj]
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   178
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   179
lemma id_surj: "id(A): surj(A,A)"
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   180
apply (unfold id_def surj_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   181
apply (simp (no_asm_simp))
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   182
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   183
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   184
lemma id_bij: "id(A): bij(A,A)"
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   185
apply (unfold bij_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   186
apply (blast intro: id_inj id_surj)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   187
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   188
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   189
lemma subset_iff_id: "A \<subseteq> B \<longleftrightarrow> id(A) \<in> A->B"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   190
apply (unfold id_def)
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   191
apply (force intro!: lam_type dest: apply_type)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   192
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   193
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents: 13784
diff changeset
   194
text{*@{term id} as the identity relation*}
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   195
lemma id_iff [simp]: "<x,y> \<in> id(A) \<longleftrightarrow> x=y & y \<in> A"
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents: 13784
diff changeset
   196
by auto
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   197
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents: 13784
diff changeset
   198
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents: 13784
diff changeset
   199
subsection{*Converse of a Function*}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   200
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   201
lemma inj_converse_fun: "f \<in> inj(A,B) ==> converse(f) \<in> range(f)->A"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   202
apply (unfold inj_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   203
apply (simp (no_asm_simp) add: Pi_iff function_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   204
apply (erule CollectE)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   205
apply (simp (no_asm_simp) add: apply_iff)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   206
apply (blast dest: fun_is_rel)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   207
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   208
41160
be34449f6cba Added two theorems about the concept of range. Tidied up the comments.
paulson
parents: 32960
diff changeset
   209
text{* Equations for converse(f) *}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   210
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents: 13784
diff changeset
   211
text{*The premises are equivalent to saying that f is injective...*}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   212
lemma left_inverse_lemma:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   213
     "[| f \<in> A->B;  converse(f): C->A;  a \<in> A |] ==> converse(f)`(f`a) = a"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   214
by (blast intro: apply_Pair apply_equality converseI)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   215
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   216
lemma left_inverse [simp]: "[| f \<in> inj(A,B);  a \<in> A |] ==> converse(f)`(f`a) = a"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   217
by (blast intro: left_inverse_lemma inj_converse_fun inj_is_fun)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   218
14883
ca000a495448 Groups, Rings and supporting lemmas
paulson
parents: 14060
diff changeset
   219
lemma left_inverse_eq:
ca000a495448 Groups, Rings and supporting lemmas
paulson
parents: 14060
diff changeset
   220
     "[|f \<in> inj(A,B); f ` x = y; x \<in> A|] ==> converse(f) ` y = x"
ca000a495448 Groups, Rings and supporting lemmas
paulson
parents: 14060
diff changeset
   221
by auto
ca000a495448 Groups, Rings and supporting lemmas
paulson
parents: 14060
diff changeset
   222
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 41160
diff changeset
   223
lemmas left_inverse_bij = bij_is_inj [THEN left_inverse]
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   224
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   225
lemma right_inverse_lemma:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   226
     "[| f \<in> A->B;  converse(f): C->A;  b \<in> C |] ==> f`(converse(f)`b) = b"
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   227
by (rule apply_Pair [THEN converseD [THEN apply_equality]], auto)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   228
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   229
(*Should the premises be f \<in> surj(A,B), b \<in> B for symmetry with left_inverse?
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   230
  No: they would not imply that converse(f) was a function! *)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   231
lemma right_inverse [simp]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   232
     "[| f \<in> inj(A,B);  b \<in> range(f) |] ==> f`(converse(f)`b) = b"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   233
by (blast intro: right_inverse_lemma inj_converse_fun inj_is_fun)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   234
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   235
lemma right_inverse_bij: "[| f \<in> bij(A,B);  b \<in> B |] ==> f`(converse(f)`b) = b"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   236
by (force simp add: bij_def surj_range)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   237
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   238
subsection{*Converses of Injections, Surjections, Bijections*}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   239
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   240
lemma inj_converse_inj: "f \<in> inj(A,B) ==> converse(f): inj(range(f), A)"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   241
apply (rule f_imp_injective)
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   242
apply (erule inj_converse_fun, clarify)
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   243
apply (rule right_inverse)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   244
 apply assumption
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   245
apply blast
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   246
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   247
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   248
lemma inj_converse_surj: "f \<in> inj(A,B) ==> converse(f): surj(range(f), A)"
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   249
by (blast intro: f_imp_surjective inj_converse_fun left_inverse inj_is_fun
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   250
                 range_of_fun [THEN apply_type])
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   251
41160
be34449f6cba Added two theorems about the concept of range. Tidied up the comments.
paulson
parents: 32960
diff changeset
   252
text{*Adding this as an intro! rule seems to cause looping*}
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   253
lemma bij_converse_bij [TC]: "f \<in> bij(A,B) ==> converse(f): bij(B,A)"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   254
apply (unfold bij_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   255
apply (fast elim: surj_range [THEN subst] inj_converse_inj inj_converse_surj)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   256
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   257
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   258
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   259
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   260
subsection{*Composition of Two Relations*}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   261
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   262
text{*The inductive definition package could derive these theorems for @{term"r O s"}*}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   263
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   264
lemma compI [intro]: "[| <a,b>:s; <b,c>:r |] ==> <a,c> \<in> r O s"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   265
by (unfold comp_def, blast)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   266
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   267
lemma compE [elim!]:
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   268
    "[| xz \<in> r O s;
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   269
        !!x y z. [| xz=<x,z>;  <x,y>:s;  <y,z>:r |] ==> P |]
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   270
     ==> P"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   271
by (unfold comp_def, blast)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   272
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   273
lemma compEpair:
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   274
    "[| <a,c> \<in> r O s;
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   275
        !!y. [| <a,y>:s;  <y,c>:r |] ==> P |]
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   276
     ==> P"
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   277
by (erule compE, simp)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   278
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   279
lemma converse_comp: "converse(R O S) = converse(S) O converse(R)"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   280
by blast
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   281
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   282
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   283
subsection{*Domain and Range -- see Suppes, Section 3.1*}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   284
41160
be34449f6cba Added two theorems about the concept of range. Tidied up the comments.
paulson
parents: 32960
diff changeset
   285
text{*Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327*}
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   286
lemma range_comp: "range(r O s) \<subseteq> range(r)"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   287
by blast
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   288
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   289
lemma range_comp_eq: "domain(r) \<subseteq> range(s) ==> range(r O s) = range(r)"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   290
by (rule range_comp [THEN equalityI], blast)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   291
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   292
lemma domain_comp: "domain(r O s) \<subseteq> domain(s)"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   293
by blast
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   294
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   295
lemma domain_comp_eq: "range(s) \<subseteq> domain(r) ==> domain(r O s) = domain(s)"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   296
by (rule domain_comp [THEN equalityI], blast)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   297
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   298
lemma image_comp: "(r O s)``A = r``(s``A)"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   299
by blast
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   300
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   301
lemma inj_inj_range: "f \<in> inj(A,B) ==> f \<in> inj(A,range(f))"
41160
be34449f6cba Added two theorems about the concept of range. Tidied up the comments.
paulson
parents: 32960
diff changeset
   302
  by (auto simp add: inj_def Pi_iff function_def)
be34449f6cba Added two theorems about the concept of range. Tidied up the comments.
paulson
parents: 32960
diff changeset
   303
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   304
lemma inj_bij_range: "f \<in> inj(A,B) ==> f \<in> bij(A,range(f))"
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   305
  by (auto simp add: bij_def intro: inj_inj_range inj_is_fun fun_is_surj)
41160
be34449f6cba Added two theorems about the concept of range. Tidied up the comments.
paulson
parents: 32960
diff changeset
   306
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   307
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   308
subsection{*Other Results*}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   309
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   310
lemma comp_mono: "[| r'<=r; s'<=s |] ==> (r' O s') \<subseteq> (r O s)"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   311
by blast
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   312
41160
be34449f6cba Added two theorems about the concept of range. Tidied up the comments.
paulson
parents: 32960
diff changeset
   313
text{*composition preserves relations*}
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   314
lemma comp_rel: "[| s<=A*B;  r<=B*C |] ==> (r O s) \<subseteq> A*C"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   315
by blast
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   316
41160
be34449f6cba Added two theorems about the concept of range. Tidied up the comments.
paulson
parents: 32960
diff changeset
   317
text{*associative law for composition*}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   318
lemma comp_assoc: "(r O s) O t = r O (s O t)"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   319
by blast
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   320
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   321
(*left identity of composition; provable inclusions are
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   322
        id(A) O r \<subseteq> r
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   323
  and   [| r<=A*B; B<=C |] ==> r \<subseteq> id(C) O r *)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   324
lemma left_comp_id: "r<=A*B ==> id(B) O r = r"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   325
by blast
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   326
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   327
(*right identity of composition; provable inclusions are
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   328
        r O id(A) \<subseteq> r
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   329
  and   [| r<=A*B; A<=C |] ==> r \<subseteq> r O id(C) *)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   330
lemma right_comp_id: "r<=A*B ==> r O id(A) = r"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   331
by blast
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   332
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   333
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   334
subsection{*Composition Preserves Functions, Injections, and Surjections*}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   335
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   336
lemma comp_function: "[| function(g);  function(f) |] ==> function(f O g)"
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   337
by (unfold function_def, blast)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   338
41160
be34449f6cba Added two theorems about the concept of range. Tidied up the comments.
paulson
parents: 32960
diff changeset
   339
text{*Don't think the premises can be weakened much*}
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   340
lemma comp_fun: "[| g \<in> A->B;  f \<in> B->C |] ==> (f O g) \<in> A->C"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   341
apply (auto simp add: Pi_def comp_function Pow_iff comp_rel)
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   342
apply (subst range_rel_subset [THEN domain_comp_eq], auto)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   343
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   344
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   345
(*Thanks to the new definition of "apply", the premise f \<in> B->C is gone!*)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   346
lemma comp_fun_apply [simp]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   347
     "[| g \<in> A->B;  a \<in> A |] ==> (f O g)`a = f`(g`a)"
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   348
apply (frule apply_Pair, assumption)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   349
apply (simp add: apply_def image_comp)
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   350
apply (blast dest: apply_equality)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   351
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   352
41160
be34449f6cba Added two theorems about the concept of range. Tidied up the comments.
paulson
parents: 32960
diff changeset
   353
text{*Simplifies compositions of lambda-abstractions*}
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   354
lemma comp_lam:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   355
    "[| !!x. x \<in> A ==> b(x): B |]
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   356
     ==> (\<lambda>y\<in>B. c(y)) O (\<lambda>x\<in>A. b(x)) = (\<lambda>x\<in>A. c(b(x)))"
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   357
apply (subgoal_tac "(\<lambda>x\<in>A. b(x)) \<in> A -> B")
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   358
 apply (rule fun_extension)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   359
   apply (blast intro: comp_fun lam_funtype)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   360
  apply (rule lam_funtype)
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   361
 apply simp
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   362
apply (simp add: lam_type)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   363
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   364
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   365
lemma comp_inj:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   366
     "[| g \<in> inj(A,B);  f \<in> inj(B,C) |] ==> (f O g) \<in> inj(A,C)"
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   367
apply (frule inj_is_fun [of g])
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   368
apply (frule inj_is_fun [of f])
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   369
apply (rule_tac d = "%y. converse (g) ` (converse (f) ` y)" in f_imp_injective)
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   370
 apply (blast intro: comp_fun, simp)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   371
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   372
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   373
lemma comp_surj:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   374
    "[| g \<in> surj(A,B);  f \<in> surj(B,C) |] ==> (f O g) \<in> surj(A,C)"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   375
apply (unfold surj_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   376
apply (blast intro!: comp_fun comp_fun_apply)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   377
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   378
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   379
lemma comp_bij:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   380
    "[| g \<in> bij(A,B);  f \<in> bij(B,C) |] ==> (f O g) \<in> bij(A,C)"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   381
apply (unfold bij_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   382
apply (blast intro: comp_inj comp_surj)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   383
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   384
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   385
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   386
subsection{*Dual Properties of @{term inj} and @{term surj}*}
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   387
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   388
text{*Useful for proofs from
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   389
    D Pastre.  Automatic theorem proving in set theory.
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   390
    Artificial Intelligence, 10:1--27, 1978.*}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   391
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   392
lemma comp_mem_injD1:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   393
    "[| (f O g): inj(A,C);  g \<in> A->B;  f \<in> B->C |] ==> g \<in> inj(A,B)"
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   394
by (unfold inj_def, force)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   395
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   396
lemma comp_mem_injD2:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   397
    "[| (f O g): inj(A,C);  g \<in> surj(A,B);  f \<in> B->C |] ==> f \<in> inj(B,C)"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   398
apply (unfold inj_def surj_def, safe)
13784
b9f6154427a4 tidying (by script)
paulson
parents: 13611
diff changeset
   399
apply (rule_tac x1 = x in bspec [THEN bexE])
b9f6154427a4 tidying (by script)
paulson
parents: 13611
diff changeset
   400
apply (erule_tac [3] x1 = w in bspec [THEN bexE], assumption+, safe)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   401
apply (rule_tac t = "op ` (g) " in subst_context)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   402
apply (erule asm_rl bspec [THEN bspec, THEN mp])+
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   403
apply (simp (no_asm_simp))
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   404
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   405
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   406
lemma comp_mem_surjD1:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   407
    "[| (f O g): surj(A,C);  g \<in> A->B;  f \<in> B->C |] ==> f \<in> surj(B,C)"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   408
apply (unfold surj_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   409
apply (blast intro!: comp_fun_apply [symmetric] apply_funtype)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   410
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   411
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   412
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   413
lemma comp_mem_surjD2:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   414
    "[| (f O g): surj(A,C);  g \<in> A->B;  f \<in> inj(B,C) |] ==> g \<in> surj(A,B)"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   415
apply (unfold inj_def surj_def, safe)
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   416
apply (drule_tac x = "f`y" in bspec, auto)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   417
apply (blast intro: apply_funtype)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   418
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   419
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   420
subsubsection{*Inverses of Composition*}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   421
41160
be34449f6cba Added two theorems about the concept of range. Tidied up the comments.
paulson
parents: 32960
diff changeset
   422
text{*left inverse of composition; one inclusion is
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   423
        @{term "f \<in> A->B ==> id(A) \<subseteq> converse(f) O f"} *}
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   424
lemma left_comp_inverse: "f \<in> inj(A,B) ==> converse(f) O f = id(A)"
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   425
apply (unfold inj_def, clarify)
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   426
apply (rule equalityI)
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   427
 apply (auto simp add: apply_iff, blast)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   428
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   429
41160
be34449f6cba Added two theorems about the concept of range. Tidied up the comments.
paulson
parents: 32960
diff changeset
   430
text{*right inverse of composition; one inclusion is
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   431
                @{term "f \<in> A->B ==> f O converse(f) \<subseteq> id(B)"} *}
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   432
lemma right_comp_inverse:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   433
    "f \<in> surj(A,B) ==> f O converse(f) = id(B)"
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   434
apply (simp add: surj_def, clarify)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   435
apply (rule equalityI)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   436
apply (best elim: domain_type range_type dest: apply_equality2)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   437
apply (blast intro: apply_Pair)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   438
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   439
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   440
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   441
subsubsection{*Proving that a Function is a Bijection*}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   442
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   443
lemma comp_eq_id_iff:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   444
    "[| f \<in> A->B;  g \<in> B->A |] ==> f O g = id(B) \<longleftrightarrow> (\<forall>y\<in>B. f`(g`y)=y)"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   445
apply (unfold id_def, safe)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   446
 apply (drule_tac t = "%h. h`y " in subst_context)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   447
 apply simp
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   448
apply (rule fun_extension)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   449
  apply (blast intro: comp_fun lam_type)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   450
 apply auto
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   451
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   452
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   453
lemma fg_imp_bijective:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   454
    "[| f \<in> A->B;  g \<in> B->A;  f O g = id(B);  g O f = id(A) |] ==> f \<in> bij(A,B)"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   455
apply (unfold bij_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   456
apply (simp add: comp_eq_id_iff)
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   457
apply (blast intro: f_imp_injective f_imp_surjective apply_funtype)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   458
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   459
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   460
lemma nilpotent_imp_bijective: "[| f \<in> A->A;  f O f = id(A) |] ==> f \<in> bij(A,A)"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   461
by (blast intro: fg_imp_bijective)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   462
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   463
lemma invertible_imp_bijective:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   464
     "[| converse(f): B->A;  f \<in> A->B |] ==> f \<in> bij(A,B)"
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   465
by (simp add: fg_imp_bijective comp_eq_id_iff
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   466
              left_inverse_lemma right_inverse_lemma)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   467
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   468
subsubsection{*Unions of Functions*}
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   469
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   470
text{*See similar theorems in func.thy*}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   471
41160
be34449f6cba Added two theorems about the concept of range. Tidied up the comments.
paulson
parents: 32960
diff changeset
   472
text{*Theorem by KG, proof by LCP*}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   473
lemma inj_disjoint_Un:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   474
     "[| f \<in> inj(A,B);  g \<in> inj(C,D);  B \<inter> D = 0 |]
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   475
      ==> (\<lambda>a\<in>A \<union> C. if a \<in> A then f`a else g`a) \<in> inj(A \<union> C, B \<union> D)"
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   476
apply (rule_tac d = "%z. if z \<in> B then converse (f) `z else converse (g) `z"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   477
       in lam_injective)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   478
apply (auto simp add: inj_is_fun [THEN apply_type])
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   479
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   480
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   481
lemma surj_disjoint_Un:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   482
    "[| f \<in> surj(A,B);  g \<in> surj(C,D);  A \<inter> C = 0 |]
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   483
     ==> (f \<union> g) \<in> surj(A \<union> C, B \<union> D)"
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   484
apply (simp add: surj_def fun_disjoint_Un)
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   485
apply (blast dest!: domain_of_fun
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
   486
             intro!: fun_disjoint_apply1 fun_disjoint_apply2)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   487
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   488
41160
be34449f6cba Added two theorems about the concept of range. Tidied up the comments.
paulson
parents: 32960
diff changeset
   489
text{*A simple, high-level proof; the version for injections follows from it,
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   490
  using  @{term "f \<in> inj(A,B) \<longleftrightarrow> f \<in> bij(A,range(f))"}  *}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   491
lemma bij_disjoint_Un:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   492
     "[| f \<in> bij(A,B);  g \<in> bij(C,D);  A \<inter> C = 0;  B \<inter> D = 0 |]
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   493
      ==> (f \<union> g) \<in> bij(A \<union> C, B \<union> D)"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   494
apply (rule invertible_imp_bijective)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   495
apply (subst converse_Un)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   496
apply (auto intro: fun_disjoint_Un bij_is_fun bij_converse_bij)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   497
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   498
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   499
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   500
subsubsection{*Restrictions as Surjections and Bijections*}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   501
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   502
lemma surj_image:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   503
    "f \<in> Pi(A,B) ==> f \<in> surj(A, f``A)"
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   504
apply (simp add: surj_def)
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   505
apply (blast intro: apply_equality apply_Pair Pi_type)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   506
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   507
47101
ded5cc757bc9 proof tidying
paulson
parents: 46953
diff changeset
   508
lemma surj_image_eq: "f \<in> surj(A, B) ==> f``A = B"
ded5cc757bc9 proof tidying
paulson
parents: 46953
diff changeset
   509
  by (auto simp add: surj_def image_fun) (blast dest: apply_type) 
ded5cc757bc9 proof tidying
paulson
parents: 46953
diff changeset
   510
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   511
lemma restrict_image [simp]: "restrict(f,A) `` B = f `` (A \<inter> B)"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   512
by (auto simp add: restrict_def)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   513
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   514
lemma restrict_inj:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   515
    "[| f \<in> inj(A,B);  C<=A |] ==> restrict(f,C): inj(C,B)"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   516
apply (unfold inj_def)
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   517
apply (safe elim!: restrict_type2, auto)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   518
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   519
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   520
lemma restrict_surj: "[| f \<in> Pi(A,B);  C<=A |] ==> restrict(f,C): surj(C, f``C)"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   521
apply (insert restrict_type2 [THEN surj_image])
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   522
apply (simp add: restrict_image)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   523
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   524
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   525
lemma restrict_bij:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   526
    "[| f \<in> inj(A,B);  C<=A |] ==> restrict(f,C): bij(C, f``C)"
13180
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   527
apply (simp add: inj_def bij_def)
a82610e49b2d tidied; stronger lemmas about functions
paulson
parents: 13176
diff changeset
   528
apply (blast intro: restrict_surj surj_is_fun)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   529
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   530
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   531
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   532
subsubsection{*Lemmas for Ramsey's Theorem*}
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   533
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   534
lemma inj_weaken_type: "[| f \<in> inj(A,B);  B<=D |] ==> f \<in> inj(A,D)"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   535
apply (unfold inj_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   536
apply (blast intro: fun_weaken_type)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   537
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   538
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   539
lemma inj_succ_restrict:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   540
     "[| f \<in> inj(succ(m), A) |] ==> restrict(f,m) \<in> inj(m, A-{f`m})"
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13185
diff changeset
   541
apply (rule restrict_bij [THEN bij_is_inj, THEN inj_weaken_type], assumption, blast)
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   542
apply (unfold inj_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   543
apply (fast elim: range_type mem_irrefl dest: apply_equality)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   544
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   545
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   546
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   547
lemma inj_extend:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   548
    "[| f \<in> inj(A,B);  a\<notin>A;  b\<notin>B |]
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   549
     ==> cons(<a,b>,f) \<in> inj(cons(a,A), cons(b,B))"
13176
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   550
apply (unfold inj_def)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   551
apply (force intro: apply_type  simp add: fun_extend)
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   552
done
312bd350579b conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents: 9570
diff changeset
   553
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   554
end