src/HOL/Fun.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10076 2683ff181047
child 10826 f3b7201dda27
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1264
diff changeset
     1
(*  Title:      HOL/Fun
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1264
diff changeset
     3
    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     6
Lemmas about functions.
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     8
7089
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
     9
Goal "(f = g) = (! x. f(x)=g(x))";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    10
by (rtac iffI 1);
1264
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 923
diff changeset
    11
by (Asm_simp_tac 1);
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 923
diff changeset
    12
by (rtac ext 1 THEN Asm_simp_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    13
qed "expand_fun_eq";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    14
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
    15
val prems = Goal
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    16
    "[| f(x)=u;  !!x. P(x) ==> g(f(x)) = x;  P(x) |] ==> x=g(u)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    17
by (rtac (arg_cong RS box_equals) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    18
by (REPEAT (resolve_tac (prems@[refl]) 1));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    19
qed "apply_inverse";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    20
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    21
4656
134d24ddaad3 Proved choice and bchoice; changed Fun.thy -> thy
paulson
parents: 4089
diff changeset
    22
(** "Axiom" of Choice, proved using the description operator **)
134d24ddaad3 Proved choice and bchoice; changed Fun.thy -> thy
paulson
parents: 4089
diff changeset
    23
9838
dc84dda48a5a moved proof of "choice" to Tools/meson.ML
paulson
parents: 9422
diff changeset
    24
(*"choice" is now proved in Tools/meson.ML*)
4656
134d24ddaad3 Proved choice and bchoice; changed Fun.thy -> thy
paulson
parents: 4089
diff changeset
    25
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
    26
Goal "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
9970
dfe4747c8318 the final renaming: selectI -> someI
paulson
parents: 9969
diff changeset
    27
by (fast_tac (claset() addEs [someI]) 1);
4656
134d24ddaad3 Proved choice and bchoice; changed Fun.thy -> thy
paulson
parents: 4089
diff changeset
    28
qed "bchoice";
134d24ddaad3 Proved choice and bchoice; changed Fun.thy -> thy
paulson
parents: 4089
diff changeset
    29
134d24ddaad3 Proved choice and bchoice; changed Fun.thy -> thy
paulson
parents: 4089
diff changeset
    30
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5441
diff changeset
    31
section "id";
5441
45bd13b15d80 added Id_apply
oheimb
parents: 5318
diff changeset
    32
7089
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    33
Goalw [id_def] "id x = x";
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    34
by (rtac refl 1);
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    35
qed "id_apply";
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5441
diff changeset
    36
Addsimps [id_apply];
5441
45bd13b15d80 added Id_apply
oheimb
parents: 5318
diff changeset
    37
8226
07284f7ad262 new thm and simprule inv_id
paulson
parents: 8173
diff changeset
    38
Goal "inv id = id";
07284f7ad262 new thm and simprule inv_id
paulson
parents: 8173
diff changeset
    39
by (simp_tac (simpset() addsimps [inv_def,id_def]) 1);
07284f7ad262 new thm and simprule inv_id
paulson
parents: 8173
diff changeset
    40
qed "inv_id";
07284f7ad262 new thm and simprule inv_id
paulson
parents: 8173
diff changeset
    41
Addsimps [inv_id];
07284f7ad262 new thm and simprule inv_id
paulson
parents: 8173
diff changeset
    42
5441
45bd13b15d80 added Id_apply
oheimb
parents: 5318
diff changeset
    43
5306
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    44
section "o";
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    45
7089
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    46
Goalw [o_def] "(f o g) x = f (g x)";
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    47
by (rtac refl 1);
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    48
qed "o_apply";
5306
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    49
Addsimps [o_apply];
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    50
7089
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    51
Goalw [o_def] "f o (g o h) = f o g o h";
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    52
by (rtac ext 1);
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    53
by (rtac refl 1);
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    54
qed "o_assoc";
5306
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    55
7089
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    56
Goalw [id_def] "id o g = g";
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    57
by (rtac ext 1);
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    58
by (Simp_tac 1);
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    59
qed "id_o";
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5441
diff changeset
    60
Addsimps [id_o];
5306
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    61
7089
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    62
Goalw [id_def] "f o id = f";
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    63
by (rtac ext 1);
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    64
by (Simp_tac 1);
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    65
qed "o_id";
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5441
diff changeset
    66
Addsimps [o_id];
5306
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    67
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    68
Goalw [o_def] "(f o g)``r = f``(g``r)";
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    69
by (Blast_tac 1);
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    70
qed "image_compose";
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    71
7916
3cb310f40a3a replaced image_image_eq_UN by image_eq_UN
paulson
parents: 7876
diff changeset
    72
Goal "f``A = (UN x:A. {f x})";
7536
5c094aec523d new theorem image_image_eq_UN
paulson
parents: 7514
diff changeset
    73
by (Blast_tac 1);
7916
3cb310f40a3a replaced image_image_eq_UN by image_eq_UN
paulson
parents: 7876
diff changeset
    74
qed "image_eq_UN";
7536
5c094aec523d new theorem image_image_eq_UN
paulson
parents: 7514
diff changeset
    75
5852
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
    76
Goalw [o_def] "UNION A (g o f) = UNION (f``A) g";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
    77
by (Blast_tac 1);
6829
50459a995aa3 renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents: 6301
diff changeset
    78
qed "UN_o";
5852
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
    79
7014
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 6829
diff changeset
    80
(** lemma for proving injectivity of representation functions for **)
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 6829
diff changeset
    81
(** datatypes involving function types                            **)
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 6829
diff changeset
    82
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 6829
diff changeset
    83
Goalw [o_def]
7089
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    84
  "[| ! x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa";
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    85
by (rtac ext 1);
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    86
by (etac allE 1);
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    87
by (etac allE 1);
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    88
by (etac mp 1);
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
    89
by (etac fun_cong 1);
7014
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 6829
diff changeset
    90
qed "inj_fun_lemma";
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 6829
diff changeset
    91
5306
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    92
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    93
section "inj";
6171
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5865
diff changeset
    94
(**NB: inj now just translates to inj_on**)
5306
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    95
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    96
(*** inj(f): f is a one-to-one function ***)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    97
6171
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5865
diff changeset
    98
(*for Tools/datatype_rep_proofs*)
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5865
diff changeset
    99
val [prem] = Goalw [inj_on_def]
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5865
diff changeset
   100
    "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)";
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5865
diff changeset
   101
by (blast_tac (claset() addIs [prem RS spec RS mp]) 1);
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5865
diff changeset
   102
qed "datatype_injI";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   103
6171
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5865
diff changeset
   104
Goalw [inj_on_def] "[| inj(f); f(x) = f(y) |] ==> x=y";
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   105
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   106
qed "injD";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   107
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   108
(*Useful with the simplifier*)
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   109
Goal "inj(f) ==> (f(x) = f(y)) = (x=y)";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   110
by (rtac iffI 1);
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   111
by (etac arg_cong 2);
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   112
by (etac injD 1);
5318
72bf8039b53f expandshort
paulson
parents: 5316
diff changeset
   113
by (assume_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   114
qed "inj_eq";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   115
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   116
(*A one-to-one function has an inverse (given using select).*)
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   117
Goalw [inv_def] "inj(f) ==> inv f (f x) = x";
10076
2683ff181047 removed the obsolete (and badly named) inj_select
paulson
parents: 10066
diff changeset
   118
by (asm_simp_tac (simpset() addsimps [inj_eq]) 1); 
2912
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv.
nipkow
parents: 2890
diff changeset
   119
qed "inv_f_f";
7338
b275ae194e5a new theorem inv_f_eq
paulson
parents: 7089
diff changeset
   120
Addsimps [inv_f_f];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   121
7338
b275ae194e5a new theorem inv_f_eq
paulson
parents: 7089
diff changeset
   122
Goal "[| inj(f);  f x = y |] ==> inv f y = x";
b275ae194e5a new theorem inv_f_eq
paulson
parents: 7089
diff changeset
   123
by (etac subst 1);
b275ae194e5a new theorem inv_f_eq
paulson
parents: 7089
diff changeset
   124
by (etac inv_f_f 1);
b275ae194e5a new theorem inv_f_eq
paulson
parents: 7089
diff changeset
   125
qed "inv_f_eq";
6235
c8a69ecafb99 new surj rules
paulson
parents: 6171
diff changeset
   126
10066
2f5686cf8c9a new theorems and comment
paulson
parents: 9970
diff changeset
   127
Goal "[| inj f; ALL x. f(g x) = x |] ==> inv f = g";
2f5686cf8c9a new theorems and comment
paulson
parents: 9970
diff changeset
   128
by (blast_tac (claset() addIs [ext, inv_f_eq]) 1); 
2f5686cf8c9a new theorems and comment
paulson
parents: 9970
diff changeset
   129
qed "inj_imp_inv_eq";
2f5686cf8c9a new theorems and comment
paulson
parents: 9970
diff changeset
   130
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   131
(* Useful??? *)
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   132
val [oneone,minor] = Goal
2912
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv.
nipkow
parents: 2890
diff changeset
   133
    "[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)";
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv.
nipkow
parents: 2890
diff changeset
   134
by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   135
by (rtac (rangeI RS minor) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   136
qed "inj_transfer";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   137
7014
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 6829
diff changeset
   138
Goalw [o_def] "[| inj f; f o g = f o h |] ==> g = h";
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 6829
diff changeset
   139
by (rtac ext 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 6829
diff changeset
   140
by (etac injD 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 6829
diff changeset
   141
by (etac fun_cong 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 6829
diff changeset
   142
qed "inj_o";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   143
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   144
(*** inj_on f A: f is one-to-one over A ***)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   145
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   146
val prems = Goalw [inj_on_def]
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   147
    "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_on f A";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   148
by (blast_tac (claset() addIs prems) 1);
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   149
qed "inj_onI";
9108
9fff97d29837 bind_thm(s);
wenzelm
parents: 8767
diff changeset
   150
bind_thm ("injI", inj_onI);                  (*for compatibility*)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   151
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   152
val [major] = Goal 
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   153
    "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   154
by (rtac inj_onI 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   155
by (etac (apply_inverse RS trans) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   156
by (REPEAT (eresolve_tac [asm_rl,major] 1));
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   157
qed "inj_on_inverseI";
9108
9fff97d29837 bind_thm(s);
wenzelm
parents: 8767
diff changeset
   158
bind_thm ("inj_inverseI", inj_on_inverseI);   (*for compatibility*)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   159
8285
16216dbe4f20 new theorems inj_iff, surj_iff
paulson
parents: 8258
diff changeset
   160
Goal "(inj f) = (inv f o f = id)";
16216dbe4f20 new theorems inj_iff, surj_iff
paulson
parents: 8258
diff changeset
   161
by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
16216dbe4f20 new theorems inj_iff, surj_iff
paulson
parents: 8258
diff changeset
   162
by (blast_tac (claset() addIs [inj_inverseI, inv_f_f]) 1);
16216dbe4f20 new theorems inj_iff, surj_iff
paulson
parents: 8258
diff changeset
   163
qed "inj_iff";
16216dbe4f20 new theorems inj_iff, surj_iff
paulson
parents: 8258
diff changeset
   164
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   165
Goalw [inj_on_def] "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   166
by (Blast_tac 1);
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   167
qed "inj_onD";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   168
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   169
Goal "[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   170
by (blast_tac (claset() addSDs [inj_onD]) 1);
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   171
qed "inj_on_iff";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   172
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   173
Goalw [inj_on_def] "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   174
by (Blast_tac 1);
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   175
qed "inj_on_contraD";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   176
8156
33d23d0a300e added inj_singleton
oheimb
parents: 8138
diff changeset
   177
Goal "inj (%s. {s})";
8253
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   178
by (rtac injI 1);
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   179
by (etac singleton_inject 1);
8156
33d23d0a300e added inj_singleton
oheimb
parents: 8138
diff changeset
   180
qed "inj_singleton";
33d23d0a300e added inj_singleton
oheimb
parents: 8138
diff changeset
   181
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   182
Goalw [inj_on_def] "[| A<=B; inj_on f B |] ==> inj_on f A";
3341
89fe22bf9f54 New theorem subset_inj_onto
paulson
parents: 2935
diff changeset
   183
by (Blast_tac 1);
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   184
qed "subset_inj_on";
3341
89fe22bf9f54 New theorem subset_inj_onto
paulson
parents: 2935
diff changeset
   185
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   186
6235
c8a69ecafb99 new surj rules
paulson
parents: 6171
diff changeset
   187
(** surj **)
c8a69ecafb99 new surj rules
paulson
parents: 6171
diff changeset
   188
6267
a3098667b9b6 new lemma surjD
paulson
parents: 6235
diff changeset
   189
val [prem] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g";
a3098667b9b6 new lemma surjD
paulson
parents: 6235
diff changeset
   190
by (blast_tac (claset() addIs [prem RS sym]) 1);
6235
c8a69ecafb99 new surj rules
paulson
parents: 6171
diff changeset
   191
qed "surjI";
c8a69ecafb99 new surj rules
paulson
parents: 6171
diff changeset
   192
c8a69ecafb99 new surj rules
paulson
parents: 6171
diff changeset
   193
Goalw [surj_def] "surj f ==> range f = UNIV";
c8a69ecafb99 new surj rules
paulson
parents: 6171
diff changeset
   194
by Auto_tac;
c8a69ecafb99 new surj rules
paulson
parents: 6171
diff changeset
   195
qed "surj_range";
c8a69ecafb99 new surj rules
paulson
parents: 6171
diff changeset
   196
6267
a3098667b9b6 new lemma surjD
paulson
parents: 6235
diff changeset
   197
Goalw [surj_def] "surj f ==> EX x. y = f x";
a3098667b9b6 new lemma surjD
paulson
parents: 6235
diff changeset
   198
by (Blast_tac 1);
a3098667b9b6 new lemma surjD
paulson
parents: 6235
diff changeset
   199
qed "surjD";
a3098667b9b6 new lemma surjD
paulson
parents: 6235
diff changeset
   200
8253
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   201
Goal "inj f ==> surj (inv f)";
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   202
by (blast_tac (claset() addIs [surjI, inv_f_f]) 1);
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   203
qed "inj_imp_surj_inv";
7374
dec7b838f5cb the bij predicate (at last)
paulson
parents: 7338
diff changeset
   204
dec7b838f5cb the bij predicate (at last)
paulson
parents: 7338
diff changeset
   205
6171
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5865
diff changeset
   206
(*** Lemmas about injective functions and inv ***)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   207
7051
9b6bdced3dc6 Mod by Norber Voelcker
nipkow
parents: 7014
diff changeset
   208
Goalw [o_def] "[| inj_on f A;  inj_on g (f``A) |] ==> inj_on (g o f) A";
6171
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5865
diff changeset
   209
by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1);
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5865
diff changeset
   210
qed "comp_inj_on";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   211
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   212
Goalw [inv_def] "y : range(f) ==> f(inv f y) = y";
9970
dfe4747c8318 the final renaming: selectI -> someI
paulson
parents: 9969
diff changeset
   213
by (fast_tac (claset() addIs [someI]) 1);
2912
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv.
nipkow
parents: 2890
diff changeset
   214
qed "f_inv_f";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   215
6235
c8a69ecafb99 new surj rules
paulson
parents: 6171
diff changeset
   216
Goal "surj f ==> f(inv f y) = y";
c8a69ecafb99 new surj rules
paulson
parents: 6171
diff changeset
   217
by (asm_simp_tac (simpset() addsimps [f_inv_f, surj_range]) 1);
c8a69ecafb99 new surj rules
paulson
parents: 6171
diff changeset
   218
qed "surj_f_inv_f";
c8a69ecafb99 new surj rules
paulson
parents: 6171
diff changeset
   219
6171
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5865
diff changeset
   220
Goal "[| inv f x = inv f y;  x: range(f);  y: range(f) |] ==> x=y";
2912
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv.
nipkow
parents: 2890
diff changeset
   221
by (rtac (arg_cong RS box_equals) 1);
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   222
by (REPEAT (ares_tac [f_inv_f] 1));
2912
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv.
nipkow
parents: 2890
diff changeset
   223
qed "inv_injective";
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv.
nipkow
parents: 2890
diff changeset
   224
6235
c8a69ecafb99 new surj rules
paulson
parents: 6171
diff changeset
   225
Goal "A <= range(f) ==> inj_on (inv f) A";
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   226
by (fast_tac (claset() addIs [inj_onI] 
6235
c8a69ecafb99 new surj rules
paulson
parents: 6171
diff changeset
   227
                       addEs [inv_injective, injD]) 1);
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   228
qed "inj_on_inv";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   229
6235
c8a69ecafb99 new surj rules
paulson
parents: 6171
diff changeset
   230
Goal "surj f ==> inj (inv f)";
c8a69ecafb99 new surj rules
paulson
parents: 6171
diff changeset
   231
by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1);
c8a69ecafb99 new surj rules
paulson
parents: 6171
diff changeset
   232
qed "surj_imp_inj_inv";
c8a69ecafb99 new surj rules
paulson
parents: 6171
diff changeset
   233
8285
16216dbe4f20 new theorems inj_iff, surj_iff
paulson
parents: 8258
diff changeset
   234
Goal "(surj f) = (f o inv f = id)";
16216dbe4f20 new theorems inj_iff, surj_iff
paulson
parents: 8258
diff changeset
   235
by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
16216dbe4f20 new theorems inj_iff, surj_iff
paulson
parents: 8258
diff changeset
   236
by (blast_tac (claset() addIs [surjI, surj_f_inv_f]) 1);
16216dbe4f20 new theorems inj_iff, surj_iff
paulson
parents: 8258
diff changeset
   237
qed "surj_iff";
16216dbe4f20 new theorems inj_iff, surj_iff
paulson
parents: 8258
diff changeset
   238
10066
2f5686cf8c9a new theorems and comment
paulson
parents: 9970
diff changeset
   239
Goal "[| surj f; ALL x. g(f x) = x |] ==> inv f = g";
2f5686cf8c9a new theorems and comment
paulson
parents: 9970
diff changeset
   240
by (rtac ext 1);
2f5686cf8c9a new theorems and comment
paulson
parents: 9970
diff changeset
   241
by (dres_inst_tac [("x","inv f x")] spec 1); 
2f5686cf8c9a new theorems and comment
paulson
parents: 9970
diff changeset
   242
by (asm_full_simp_tac (simpset() addsimps [surj_f_inv_f]) 1); 
2f5686cf8c9a new theorems and comment
paulson
parents: 9970
diff changeset
   243
qed "surj_imp_inv_eq";
2f5686cf8c9a new theorems and comment
paulson
parents: 9970
diff changeset
   244
8253
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   245
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   246
(** Bijections **)
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   247
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   248
Goalw [bij_def] "[| inj f; surj f |] ==> bij f";
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   249
by (Blast_tac 1);
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   250
qed "bijI";
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   251
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   252
Goalw [bij_def] "bij f ==> inj f";
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   253
by (Blast_tac 1);
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   254
qed "bij_is_inj";
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   255
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   256
Goalw [bij_def] "bij f ==> surj f";
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   257
by (Blast_tac 1);
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   258
qed "bij_is_surj";
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   259
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   260
Goalw [bij_def] "bij f ==> bij (inv f)";
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   261
by (asm_simp_tac (simpset() addsimps [inj_imp_surj_inv, surj_imp_inj_inv]) 1);
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   262
qed "bij_imp_bij_inv";
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   263
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   264
val prems = 
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   265
Goalw [inv_def] "[| !! x. g (f x) = x;  !! y. f (g y) = y |] ==> inv f = g";
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   266
by (rtac ext 1);
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   267
by (auto_tac (claset(), simpset() addsimps prems));
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   268
qed "inv_equality";
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   269
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   270
Goalw [bij_def] "bij f ==> inv (inv f) = f";
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   271
by (rtac inv_equality 1);
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   272
by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f]));
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   273
qed "inv_inv_eq";
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   274
10066
2f5686cf8c9a new theorems and comment
paulson
parents: 9970
diff changeset
   275
(** bij(inv f) implies little about f.  Consider f::bool=>bool such that
2f5686cf8c9a new theorems and comment
paulson
parents: 9970
diff changeset
   276
    f(True)=f(False)=True.  Then it's consistent with axiom someI that
2f5686cf8c9a new theorems and comment
paulson
parents: 9970
diff changeset
   277
    inv(f) could be any function at all, including the identity function.
2f5686cf8c9a new theorems and comment
paulson
parents: 9970
diff changeset
   278
    If inv(f)=id then inv(f) is a bijection, but inj(f), surj(f) and
2f5686cf8c9a new theorems and comment
paulson
parents: 9970
diff changeset
   279
    inv(inv(f))=f all fail.
2f5686cf8c9a new theorems and comment
paulson
parents: 9970
diff changeset
   280
**)
2f5686cf8c9a new theorems and comment
paulson
parents: 9970
diff changeset
   281
8253
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   282
Goalw [bij_def] "[| bij f; bij g |] ==> inv (f o g) = inv g o inv f";
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   283
by (rtac (inv_equality) 1);
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   284
by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f]));
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   285
qed "o_inv_distrib";
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   286
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   287
7514
3235863a069a images and preimages of the identity function
paulson
parents: 7445
diff changeset
   288
(** We seem to need both the id-forms and the (%x. x) forms; the latter can
3235863a069a images and preimages of the identity function
paulson
parents: 7445
diff changeset
   289
    arise by rewriting, while id may be used explicitly. **)
3235863a069a images and preimages of the identity function
paulson
parents: 7445
diff changeset
   290
3235863a069a images and preimages of the identity function
paulson
parents: 7445
diff changeset
   291
Goal "(%x. x) `` Y = Y";
3235863a069a images and preimages of the identity function
paulson
parents: 7445
diff changeset
   292
by (Blast_tac 1);
3235863a069a images and preimages of the identity function
paulson
parents: 7445
diff changeset
   293
qed "image_ident";
3235863a069a images and preimages of the identity function
paulson
parents: 7445
diff changeset
   294
3235863a069a images and preimages of the identity function
paulson
parents: 7445
diff changeset
   295
Goalw [id_def] "id `` Y = Y";
3235863a069a images and preimages of the identity function
paulson
parents: 7445
diff changeset
   296
by (Blast_tac 1);
3235863a069a images and preimages of the identity function
paulson
parents: 7445
diff changeset
   297
qed "image_id";
3235863a069a images and preimages of the identity function
paulson
parents: 7445
diff changeset
   298
Addsimps [image_ident, image_id];
3235863a069a images and preimages of the identity function
paulson
parents: 7445
diff changeset
   299
3235863a069a images and preimages of the identity function
paulson
parents: 7445
diff changeset
   300
Goal "(%x. x) -`` Y = Y";
3235863a069a images and preimages of the identity function
paulson
parents: 7445
diff changeset
   301
by (Blast_tac 1);
3235863a069a images and preimages of the identity function
paulson
parents: 7445
diff changeset
   302
qed "vimage_ident";
3235863a069a images and preimages of the identity function
paulson
parents: 7445
diff changeset
   303
3235863a069a images and preimages of the identity function
paulson
parents: 7445
diff changeset
   304
Goalw [id_def] "id -`` A = A";
3235863a069a images and preimages of the identity function
paulson
parents: 7445
diff changeset
   305
by Auto_tac;
3235863a069a images and preimages of the identity function
paulson
parents: 7445
diff changeset
   306
qed "vimage_id";
3235863a069a images and preimages of the identity function
paulson
parents: 7445
diff changeset
   307
Addsimps [vimage_ident, vimage_id];
3235863a069a images and preimages of the identity function
paulson
parents: 7445
diff changeset
   308
7876
1b3b683c092e new thm vimage_image_eq
paulson
parents: 7536
diff changeset
   309
Goal "f -`` (f `` A) = {y. EX x:A. f x = f y}";
1b3b683c092e new thm vimage_image_eq
paulson
parents: 7536
diff changeset
   310
by (blast_tac (claset() addIs [sym]) 1);
1b3b683c092e new thm vimage_image_eq
paulson
parents: 7536
diff changeset
   311
qed "vimage_image_eq";
1b3b683c092e new thm vimage_image_eq
paulson
parents: 7536
diff changeset
   312
8173
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   313
Goal "f `` (f -`` A) <= A";
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   314
by (Blast_tac 1);
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   315
qed "image_vimage_subset";
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   316
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   317
Goal "f `` (f -`` A) = A Int range f";
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   318
by (Blast_tac 1);
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   319
qed "image_vimage_eq";
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   320
Addsimps [image_vimage_eq];
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   321
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   322
Goal "surj f ==> f `` (f -`` A) = A";
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   323
by (asm_simp_tac (simpset() addsimps [surj_range]) 1);
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   324
qed "surj_image_vimage_eq";
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   325
8253
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   326
Goal "surj f ==> f `` (inv f `` A) = A";
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   327
by (asm_simp_tac (simpset() addsimps [image_eq_UN, surj_f_inv_f]) 1);
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   328
qed "image_surj_f_inv_f";
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   329
8173
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   330
Goalw [inj_on_def] "inj f ==> f -`` (f `` A) = A";
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   331
by (Blast_tac 1);
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   332
qed "inj_vimage_image_eq";
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   333
8253
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   334
Goal "inj f ==> (inv f) `` (f `` A) = A";
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   335
by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 1);
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   336
qed "image_inv_f_f";
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   337
8173
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   338
Goalw [surj_def] "surj f ==> f -`` B <= A ==> B <= f `` A";
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   339
by (blast_tac (claset() addIs [sym]) 1);
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   340
qed "vimage_subsetD";
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   341
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   342
Goalw [inj_on_def] "inj f ==> B <= f `` A ==> f -`` B <= A";
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   343
by (Blast_tac 1);
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   344
qed "vimage_subsetI";
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   345
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   346
Goalw [bij_def] "bij f ==> (f -`` B <= A) = (B <= f `` A)";
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   347
by (blast_tac (claset() delrules [subsetI]
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   348
			addIs [vimage_subsetI, vimage_subsetD]) 1);
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   349
qed "vimage_subset_eq";
a9966d5ab84d various theorems about image and inverse image
paulson
parents: 8156
diff changeset
   350
6290
31483ca40e91 new image laws
paulson
parents: 6267
diff changeset
   351
Goal "f``(A Int B) <= f``A Int f``B";
31483ca40e91 new image laws
paulson
parents: 6267
diff changeset
   352
by (Blast_tac 1);
31483ca40e91 new image laws
paulson
parents: 6267
diff changeset
   353
qed "image_Int_subset";
31483ca40e91 new image laws
paulson
parents: 6267
diff changeset
   354
31483ca40e91 new image laws
paulson
parents: 6267
diff changeset
   355
Goal "f``A - f``B <= f``(A - B)";
31483ca40e91 new image laws
paulson
parents: 6267
diff changeset
   356
by (Blast_tac 1);
31483ca40e91 new image laws
paulson
parents: 6267
diff changeset
   357
qed "image_diff_subset";
31483ca40e91 new image laws
paulson
parents: 6267
diff changeset
   358
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4830
diff changeset
   359
Goalw [inj_on_def]
5148
74919e8f221c More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5143
diff changeset
   360
   "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 3842
diff changeset
   361
by (Blast_tac 1);
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   362
qed "inj_on_image_Int";
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 3842
diff changeset
   363
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4830
diff changeset
   364
Goalw [inj_on_def]
5148
74919e8f221c More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5143
diff changeset
   365
   "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 3842
diff changeset
   366
by (Blast_tac 1);
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   367
qed "inj_on_image_set_diff";
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 3842
diff changeset
   368
6171
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5865
diff changeset
   369
Goalw [inj_on_def] "inj f ==> f``(A Int B) = f``A Int f``B";
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 3842
diff changeset
   370
by (Blast_tac 1);
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 3842
diff changeset
   371
qed "image_Int";
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 3842
diff changeset
   372
6171
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5865
diff changeset
   373
Goalw [inj_on_def] "inj f ==> f``(A-B) = f``A - f``B";
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 3842
diff changeset
   374
by (Blast_tac 1);
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 3842
diff changeset
   375
qed "image_set_diff";
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 3842
diff changeset
   376
6235
c8a69ecafb99 new surj rules
paulson
parents: 6171
diff changeset
   377
Goalw [image_def] "inj(f) ==> inv(f)``(f``X) = X";
c8a69ecafb99 new surj rules
paulson
parents: 6171
diff changeset
   378
by Auto_tac;
c8a69ecafb99 new surj rules
paulson
parents: 6171
diff changeset
   379
qed "inv_image_comp";
5847
17c869f24c5f proved surjI
paulson
parents: 5608
diff changeset
   380
6301
08245f5a436d expandshort
paulson
parents: 6290
diff changeset
   381
Goal "inj f ==> (f a : f``A) = (a : A)";
08245f5a436d expandshort
paulson
parents: 6290
diff changeset
   382
by (blast_tac (claset() addDs [injD]) 1);
08245f5a436d expandshort
paulson
parents: 6290
diff changeset
   383
qed "inj_image_mem_iff";
08245f5a436d expandshort
paulson
parents: 6290
diff changeset
   384
8253
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   385
Goalw [inj_on_def] "inj f ==> (f``A <= f``B) = (A<=B)";
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   386
by (Blast_tac 1);
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   387
qed "inj_image_subset_iff";
975eb12aa040 many new theorems about inj, surj etc.
paulson
parents: 8226
diff changeset
   388
6301
08245f5a436d expandshort
paulson
parents: 6290
diff changeset
   389
Goal "inj f ==> (f``A = f``B) = (A = B)";
08245f5a436d expandshort
paulson
parents: 6290
diff changeset
   390
by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1);
08245f5a436d expandshort
paulson
parents: 6290
diff changeset
   391
qed "inj_image_eq_iff";
08245f5a436d expandshort
paulson
parents: 6290
diff changeset
   392
6829
50459a995aa3 renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents: 6301
diff changeset
   393
Goal  "(f `` (UNION A B)) = (UN x:A.(f `` (B x)))";
50459a995aa3 renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents: 6301
diff changeset
   394
by (Blast_tac 1);
50459a995aa3 renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents: 6301
diff changeset
   395
qed "image_UN";
50459a995aa3 renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents: 6301
diff changeset
   396
50459a995aa3 renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents: 6301
diff changeset
   397
(*injectivity's required.  Left-to-right inclusion holds even if A is empty*)
50459a995aa3 renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents: 6301
diff changeset
   398
Goalw [inj_on_def]
50459a995aa3 renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents: 6301
diff changeset
   399
   "[| inj_on f C;  ALL x:A. B x <= C;  j:A |] \
50459a995aa3 renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents: 6301
diff changeset
   400
\   ==> f `` (INTER A B) = (INT x:A. f `` B x)";
50459a995aa3 renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents: 6301
diff changeset
   401
by (Blast_tac 1);
50459a995aa3 renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents: 6301
diff changeset
   402
qed "image_INT";
50459a995aa3 renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
paulson
parents: 6301
diff changeset
   403
8309
a054d5c98b21 more bijection theorems
paulson
parents: 8285
diff changeset
   404
(*Compare with image_INT: no use of inj_on, and if f is surjective then
a054d5c98b21 more bijection theorems
paulson
parents: 8285
diff changeset
   405
  it doesn't matter whether A is empty*)
a054d5c98b21 more bijection theorems
paulson
parents: 8285
diff changeset
   406
Goalw [bij_def] "bij f ==> f `` (INTER A B) = (INT x:A. f `` B x)";
a054d5c98b21 more bijection theorems
paulson
parents: 8285
diff changeset
   407
by (force_tac (claset() addSIs [surj_f_inv_f RS sym RS image_eqI], 
a054d5c98b21 more bijection theorems
paulson
parents: 8285
diff changeset
   408
	       simpset()) 1);
a054d5c98b21 more bijection theorems
paulson
parents: 8285
diff changeset
   409
qed "bij_image_INT";
a054d5c98b21 more bijection theorems
paulson
parents: 8285
diff changeset
   410
a054d5c98b21 more bijection theorems
paulson
parents: 8285
diff changeset
   411
Goal "bij f ==> f `` Collect P = {y. P (inv f y)}";
a054d5c98b21 more bijection theorems
paulson
parents: 8285
diff changeset
   412
by Auto_tac;
a054d5c98b21 more bijection theorems
paulson
parents: 8285
diff changeset
   413
by (force_tac (claset(), simpset() addsimps [bij_is_inj]) 1);
a054d5c98b21 more bijection theorems
paulson
parents: 8285
diff changeset
   414
by (blast_tac (claset() addIs [bij_is_surj RS surj_f_inv_f RS sym]) 1);
a054d5c98b21 more bijection theorems
paulson
parents: 8285
diff changeset
   415
qed "bij_image_Collect_eq";
a054d5c98b21 more bijection theorems
paulson
parents: 8285
diff changeset
   416
a054d5c98b21 more bijection theorems
paulson
parents: 8285
diff changeset
   417
Goal "bij f ==> f -`` A = inv f `` A";
8767
eae30939b592 this change saves 15 seconds
paulson
parents: 8309
diff changeset
   418
by Safe_tac;
8309
a054d5c98b21 more bijection theorems
paulson
parents: 8285
diff changeset
   419
by (asm_simp_tac (simpset() addsimps [bij_is_surj RS surj_f_inv_f]) 2);
a054d5c98b21 more bijection theorems
paulson
parents: 8285
diff changeset
   420
by (blast_tac (claset() addIs [bij_is_inj RS inv_f_f RS sym]) 1);
a054d5c98b21 more bijection theorems
paulson
parents: 8285
diff changeset
   421
qed "bij_vimage_eq_inv_image";
a054d5c98b21 more bijection theorems
paulson
parents: 8285
diff changeset
   422
10076
2683ff181047 removed the obsolete (and badly named) inj_select
paulson
parents: 10066
diff changeset
   423
Goal "surj f ==> -(f``A) <= f``(-A)";
2683ff181047 removed the obsolete (and badly named) inj_select
paulson
parents: 10066
diff changeset
   424
by (auto_tac (claset(), simpset() addsimps [surj_def]));  
2683ff181047 removed the obsolete (and badly named) inj_select
paulson
parents: 10066
diff changeset
   425
qed "surj_Compl_image_subset";
2683ff181047 removed the obsolete (and badly named) inj_select
paulson
parents: 10066
diff changeset
   426
2683ff181047 removed the obsolete (and badly named) inj_select
paulson
parents: 10066
diff changeset
   427
Goal "inj f ==> f``(-A) <= -(f``A)";
2683ff181047 removed the obsolete (and badly named) inj_select
paulson
parents: 10066
diff changeset
   428
by (auto_tac (claset(), simpset() addsimps [inj_on_def]));  
2683ff181047 removed the obsolete (and badly named) inj_select
paulson
parents: 10066
diff changeset
   429
qed "inj_image_Compl_subset";
2683ff181047 removed the obsolete (and badly named) inj_select
paulson
parents: 10066
diff changeset
   430
2683ff181047 removed the obsolete (and badly named) inj_select
paulson
parents: 10066
diff changeset
   431
Goalw [bij_def] "bij f ==> f``(-A) = -(f``A)";
2683ff181047 removed the obsolete (and badly named) inj_select
paulson
parents: 10066
diff changeset
   432
by (rtac equalityI 1); 
2683ff181047 removed the obsolete (and badly named) inj_select
paulson
parents: 10066
diff changeset
   433
by (ALLGOALS (asm_simp_tac (simpset() addsimps [inj_image_Compl_subset, 
2683ff181047 removed the obsolete (and badly named) inj_select
paulson
parents: 10066
diff changeset
   434
                                                surj_Compl_image_subset]))); 
2683ff181047 removed the obsolete (and badly named) inj_select
paulson
parents: 10066
diff changeset
   435
qed "bij_image_Compl_eq";
2683ff181047 removed the obsolete (and badly named) inj_select
paulson
parents: 10066
diff changeset
   436
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   437
val set_cs = claset() delrules [equalityI];
5305
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   438
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   439
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   440
section "fun_upd";
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   441
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   442
Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)";
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   443
by Safe_tac;
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   444
by (etac subst 1);
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   445
by (rtac ext 2);
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   446
by Auto_tac;
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   447
qed "fun_upd_idem_iff";
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   448
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   449
(* f x = y ==> f(x:=y) = f *)
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   450
bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2);
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   451
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   452
(* f(x := f x) = f *)
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   453
AddIffs [refl RS fun_upd_idem];
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   454
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   455
Goal "(f(x:=y))z = (if z=x then y else f z)";
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   456
by (simp_tac (simpset() addsimps [fun_upd_def]) 1);
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   457
qed "fun_upd_apply";
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   458
Addsimps [fun_upd_apply];
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   459
9339
0d8b0eb2932d added fun_upd2_simproc
oheimb
parents: 9108
diff changeset
   460
(* fun_upd_apply supersedes these two,   but they are useful 
0d8b0eb2932d added fun_upd2_simproc
oheimb
parents: 9108
diff changeset
   461
   if fun_upd_apply is intentionally removed from the simpset *)
7089
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
   462
Goal "(f(x:=y)) x = y";
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
   463
by (Simp_tac 1);
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
   464
qed "fun_upd_same";
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
   465
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
   466
Goal "z~=x ==> (f(x:=y)) z = f z";
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
   467
by (Asm_simp_tac 1);
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
   468
qed "fun_upd_other";
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
   469
7445
6dd6110968c9 new theorem fun_upd_upd
paulson
parents: 7374
diff changeset
   470
Goal "f(x:=y,x:=z) = f(x:=z)";
6dd6110968c9 new theorem fun_upd_upd
paulson
parents: 7374
diff changeset
   471
by (rtac ext 1);
6dd6110968c9 new theorem fun_upd_upd
paulson
parents: 7374
diff changeset
   472
by (Simp_tac 1);
6dd6110968c9 new theorem fun_upd_upd
paulson
parents: 7374
diff changeset
   473
qed "fun_upd_upd";
6dd6110968c9 new theorem fun_upd_upd
paulson
parents: 7374
diff changeset
   474
Addsimps [fun_upd_upd];
5305
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   475
9339
0d8b0eb2932d added fun_upd2_simproc
oheimb
parents: 9108
diff changeset
   476
(* simplifies terms of the form f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *)
0d8b0eb2932d added fun_upd2_simproc
oheimb
parents: 9108
diff changeset
   477
local 
0d8b0eb2932d added fun_upd2_simproc
oheimb
parents: 9108
diff changeset
   478
  fun gen_fun_upd  None    T _ _ = None
0d8b0eb2932d added fun_upd2_simproc
oheimb
parents: 9108
diff changeset
   479
  |   gen_fun_upd (Some f) T x y = Some (Const ("Fun.fun_upd",T) $ f $ x $ y)
0d8b0eb2932d added fun_upd2_simproc
oheimb
parents: 9108
diff changeset
   480
  fun dest_fun_T1 (Type (_,T::Ts)) = T
0d8b0eb2932d added fun_upd2_simproc
oheimb
parents: 9108
diff changeset
   481
  fun find_double (t as Const ("Fun.fun_upd",T) $ f $ x $ y) = let
0d8b0eb2932d added fun_upd2_simproc
oheimb
parents: 9108
diff changeset
   482
      fun find         (Const ("Fun.fun_upd",T) $ g $ v $ w) = 
0d8b0eb2932d added fun_upd2_simproc
oheimb
parents: 9108
diff changeset
   483
          if v aconv x then Some g else gen_fun_upd (find g) T v w
0d8b0eb2932d added fun_upd2_simproc
oheimb
parents: 9108
diff changeset
   484
      |   find t = None
0d8b0eb2932d added fun_upd2_simproc
oheimb
parents: 9108
diff changeset
   485
      in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end
9422
4b6bc2b347e5 avoid referencing thy value;
wenzelm
parents: 9339
diff changeset
   486
  val ss = simpset ();
9339
0d8b0eb2932d added fun_upd2_simproc
oheimb
parents: 9108
diff changeset
   487
  val fun_upd_prover = K [rtac eq_reflection 1, rtac ext 1, 
9422
4b6bc2b347e5 avoid referencing thy value;
wenzelm
parents: 9339
diff changeset
   488
                          simp_tac ss 1]
9339
0d8b0eb2932d added fun_upd2_simproc
oheimb
parents: 9108
diff changeset
   489
  fun mk_eq_cterm sg T l r = Thm.cterm_of sg (equals T $ l $ r)
0d8b0eb2932d added fun_upd2_simproc
oheimb
parents: 9108
diff changeset
   490
in 
0d8b0eb2932d added fun_upd2_simproc
oheimb
parents: 9108
diff changeset
   491
  val fun_upd2_simproc = Simplifier.mk_simproc "fun_upd2"
9422
4b6bc2b347e5 avoid referencing thy value;
wenzelm
parents: 9339
diff changeset
   492
   [Thm.read_cterm (sign_of (the_context ())) ("f(v:=w,x:=y)", HOLogic.termT)]
9339
0d8b0eb2932d added fun_upd2_simproc
oheimb
parents: 9108
diff changeset
   493
   (fn sg => (K (fn t => case find_double t of (T,None)=> None | (T,Some rhs)=> 
0d8b0eb2932d added fun_upd2_simproc
oheimb
parents: 9108
diff changeset
   494
       Some (prove_goalw_cterm [] (mk_eq_cterm sg T t rhs) fun_upd_prover))))
0d8b0eb2932d added fun_upd2_simproc
oheimb
parents: 9108
diff changeset
   495
end;
0d8b0eb2932d added fun_upd2_simproc
oheimb
parents: 9108
diff changeset
   496
Addsimprocs[fun_upd2_simproc];
0d8b0eb2932d added fun_upd2_simproc
oheimb
parents: 9108
diff changeset
   497
8258
666d3a4f3b9d changed precedence of function update
oheimb
parents: 8253
diff changeset
   498
Goal "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)";
5305
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   499
by (rtac ext 1);
7089
9bfb8e218b99 expandshort and tidying
paulson
parents: 7051
diff changeset
   500
by Auto_tac;
5305
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   501
qed "fun_upd_twist";
5852
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   502
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   503
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   504
(*** -> and Pi, by Florian Kammueller and LCP ***)
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   505
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   506
val prems = Goalw [Pi_def]
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   507
"[| !!x. x: A ==> f x: B x; !!x. x ~: A  ==> f(x) = (@ y. True)|] \
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   508
\    ==> f: Pi A B";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   509
by (auto_tac (claset(), simpset() addsimps prems));
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   510
qed "Pi_I";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   511
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   512
val prems = Goal 
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   513
"[| !!x. x: A ==> f x: B; !!x. x ~: A  ==> f(x) = (@ y. True)|] ==> f: A funcset B";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   514
by (blast_tac (claset() addIs Pi_I::prems) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   515
qed "funcsetI";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   516
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   517
Goalw [Pi_def] "[|f: Pi A B; x: A|] ==> f x: B x";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   518
by Auto_tac;
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   519
qed "Pi_mem";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   520
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   521
Goalw [Pi_def] "[|f: A funcset B; x: A|] ==> f x: B";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   522
by Auto_tac;
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   523
qed "funcset_mem";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   524
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   525
Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = (@ y. True)";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   526
by Auto_tac;
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   527
qed "apply_arb";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   528
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   529
Goalw [Pi_def] "[| f: Pi A B; g: Pi A B; ! x: A. f x = g x |] ==> f = g";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   530
by (rtac ext 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   531
by Auto_tac;
9108
9fff97d29837 bind_thm(s);
wenzelm
parents: 8767
diff changeset
   532
bind_thm ("Pi_extensionality", ballI RSN (3, result()));
5852
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   533
8138
1e4cb069b19d new theorem inj_on_restrict_eq
paulson
parents: 8081
diff changeset
   534
5852
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   535
(*** compose ***)
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   536
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   537
Goalw [Pi_def, compose_def, restrict_def]
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   538
     "[| f: A funcset B; g: B funcset C |]==> compose A g f: A funcset C";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   539
by Auto_tac;
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   540
qed "funcset_compose";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   541
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   542
Goal "[| f: A funcset B; g: B funcset C; h: C funcset D |]\
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   543
\     ==> compose A h (compose A g f) = compose A (compose B h g) f";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   544
by (res_inst_tac [("A","A")] Pi_extensionality 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   545
by (blast_tac (claset() addIs [funcset_compose]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   546
by (blast_tac (claset() addIs [funcset_compose]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   547
by (rewrite_goals_tac [Pi_def, compose_def, restrict_def]);  
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   548
by Auto_tac;
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   549
qed "compose_assoc";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   550
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   551
Goal "[| f: A funcset B; g: B funcset C; x: A |]==> compose A g f x = g(f(x))";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   552
by (asm_full_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   553
qed "compose_eq";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   554
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   555
Goal "[| f : A funcset B; f `` A = B; g: B funcset C; g `` B = C |]\
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   556
\     ==> compose A g f `` A = C";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   557
by (auto_tac (claset(),
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   558
	      simpset() addsimps [image_def, compose_eq]));
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   559
qed "surj_compose";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   560
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   561
Goal "[| f : A funcset B; g: B funcset C; f `` A = B; inj_on f A; inj_on g B |]\
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   562
\     ==> inj_on (compose A g f) A";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   563
by (auto_tac (claset(),
8081
1c8de414b45d removed inj_eq from the default simpset again
oheimb
parents: 7958
diff changeset
   564
	      simpset() addsimps [inj_on_def, compose_eq]));
5852
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   565
qed "inj_on_compose";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   566
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   567
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   568
(*** restrict / lam ***)
8138
1e4cb069b19d new theorem inj_on_restrict_eq
paulson
parents: 8081
diff changeset
   569
1e4cb069b19d new theorem inj_on_restrict_eq
paulson
parents: 8081
diff changeset
   570
Goal "f``A <= B ==> (lam x: A. f x) : A funcset B";
5852
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   571
by (auto_tac (claset(),
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   572
	      simpset() addsimps [restrict_def, Pi_def]));
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   573
qed "restrict_in_funcset";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   574
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   575
val prems = Goalw [restrict_def, Pi_def]
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   576
     "(!!x. x: A ==> f x: B x) ==> (lam x: A. f x) : Pi A B";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   577
by (asm_simp_tac (simpset() addsimps prems) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   578
qed "restrictI";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   579
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   580
Goal "x: A ==> (lam y: A. f y) x = f x";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   581
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   582
qed "restrict_apply1";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   583
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   584
Goal "[| x: A; f : A funcset B |] ==> (lam y: A. f y) x : B";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   585
by (asm_full_simp_tac (simpset() addsimps [restrict_apply1,Pi_def]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   586
qed "restrict_apply1_mem";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   587
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   588
Goal "x ~: A ==> (lam y: A. f y) x =  (@ y. True)";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   589
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   590
qed "restrict_apply2";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   591
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   592
val prems = Goal
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   593
    "(!!x. x: A ==> f x = g x) ==> (lam x: A. f x) = (lam x: A. g x)";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   594
by (rtac ext 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   595
by (auto_tac (claset(),
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   596
	      simpset() addsimps prems@[restrict_def, Pi_def]));
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   597
qed "restrict_ext";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   598
8138
1e4cb069b19d new theorem inj_on_restrict_eq
paulson
parents: 8081
diff changeset
   599
Goalw [inj_on_def, restrict_def] "inj_on (restrict f A) A = inj_on f A";
1e4cb069b19d new theorem inj_on_restrict_eq
paulson
parents: 8081
diff changeset
   600
by Auto_tac;
1e4cb069b19d new theorem inj_on_restrict_eq
paulson
parents: 8081
diff changeset
   601
qed "inj_on_restrict_eq";
1e4cb069b19d new theorem inj_on_restrict_eq
paulson
parents: 8081
diff changeset
   602
5852
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   603
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   604
(*** Inverse ***)
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   605
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   606
Goal "[|f `` A = B;  x: B |] ==> ? y: A. f y = x";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   607
by (Blast_tac 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   608
qed "surj_image";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   609
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   610
Goalw [Inv_def] "[| f `` A = B; f : A funcset B |] \
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   611
\                ==> (lam x: B. (Inv A f) x) : B funcset A";
9969
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 9838
diff changeset
   612
by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1);
5852
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   613
qed "Inv_funcset";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   614
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   615
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   616
Goal "[| f: A funcset B;  inj_on f A;  f `` A = B;  x: A |] \
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   617
\     ==> (lam y: B. (Inv A f) y) (f x) = x";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   618
by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1);
8081
1c8de414b45d removed inj_eq from the default simpset again
oheimb
parents: 7958
diff changeset
   619
by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
9969
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 9838
diff changeset
   620
by (rtac someI2 1);
5852
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   621
by Auto_tac;
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   622
qed "Inv_f_f";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   623
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   624
Goal "[| f: A funcset B;  f `` A = B;  x: B |] \
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   625
\     ==> f ((lam y: B. (Inv A f y)) x) = x";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   626
by (asm_simp_tac (simpset() addsimps [Inv_def, restrict_apply1]) 1);
9969
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 9838
diff changeset
   627
by (fast_tac (claset() addIs [someI2]) 1);
5852
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   628
qed "f_Inv_f";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   629
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   630
Goal "[| f: A funcset B;  inj_on f A;  f `` A = B |]\
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   631
\     ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   632
by (rtac Pi_extensionality 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   633
by (blast_tac (claset() addIs [funcset_compose, Inv_funcset]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   634
by (blast_tac (claset() addIs [restrict_in_funcset]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   635
by (asm_simp_tac
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   636
    (simpset() addsimps [restrict_apply1, compose_def, Inv_f_f]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   637
qed "compose_Inv_id";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   638
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   639
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   640
(*** Pi and Applyall ***)
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   641
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   642
Goalw [Pi_def] "[| B(x) = {};  x: A |] ==> (PI x: A. B x) = {}";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   643
by Auto_tac;
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   644
qed "Pi_eq_empty";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   645
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   646
Goal "[| (PI x: A. B x) ~= {};  x: A |] ==> B(x) ~= {}";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   647
by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   648
qed "Pi_total1";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   649
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   650
Goal "[| a : A; Pi A B ~= {} |] ==> Applyall (Pi A B) a = B a";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   651
by (auto_tac (claset(), simpset() addsimps [Applyall_def, Pi_def]));
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   652
by (rename_tac "g z" 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   653
by (res_inst_tac [("x","%y. if  (y = a) then z else g y")] exI 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   654
by (auto_tac (claset(), simpset() addsimps [split_if_mem1, split_if_eq1]));
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   655
qed "Applyall_beta";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   656
5865
2303f5a3036d moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents: 5852
diff changeset
   657
Goal "Pi {} B = { (%x. @ y. True) }";
2303f5a3036d moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents: 5852
diff changeset
   658
by (auto_tac (claset() addIs [ext], simpset() addsimps [Pi_def]));
2303f5a3036d moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents: 5852
diff changeset
   659
qed "Pi_empty";
5852
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   660
5865
2303f5a3036d moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents: 5852
diff changeset
   661
val [major] = Goalw [Pi_def] "(!!x. x: A ==> B x <= C x) ==> Pi A B <= Pi A C";
2303f5a3036d moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents: 5852
diff changeset
   662
by (auto_tac (claset(),
2303f5a3036d moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents: 5852
diff changeset
   663
	      simpset() addsimps [impOfSubs major]));
2303f5a3036d moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents: 5852
diff changeset
   664
qed "Pi_mono";