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