src/HOL/Fun.ML
author paulson
Mon, 16 Nov 1998 10:36:30 +0100
changeset 5865 2303f5a3036d
parent 5852 4d7320490be4
child 6171 cd237a10cbf8
permissions -rw-r--r--
moved some facts about Pi from ex/PiSets to Fun.ML
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
4656
134d24ddaad3 Proved choice and bchoice; changed Fun.thy -> thy
paulson
parents: 4089
diff changeset
     9
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4830
diff changeset
    10
Goal "(f = g) = (!x. f(x)=g(x))";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    11
by (rtac iffI 1);
1264
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 923
diff changeset
    12
by (Asm_simp_tac 1);
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 923
diff changeset
    13
by (rtac ext 1 THEN Asm_simp_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    14
qed "expand_fun_eq";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    15
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
    16
val prems = Goal
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    17
    "[| 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
    18
by (rtac (arg_cong RS box_equals) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    19
by (REPEAT (resolve_tac (prems@[refl]) 1));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    20
qed "apply_inverse";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    21
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    22
4656
134d24ddaad3 Proved choice and bchoice; changed Fun.thy -> thy
paulson
parents: 4089
diff changeset
    23
(** "Axiom" of Choice, proved using the description operator **)
134d24ddaad3 Proved choice and bchoice; changed Fun.thy -> thy
paulson
parents: 4089
diff changeset
    24
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
    25
Goal "!!Q. ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
4656
134d24ddaad3 Proved choice and bchoice; changed Fun.thy -> thy
paulson
parents: 4089
diff changeset
    26
by (fast_tac (claset() addEs [selectI]) 1);
134d24ddaad3 Proved choice and bchoice; changed Fun.thy -> thy
paulson
parents: 4089
diff changeset
    27
qed "choice";
134d24ddaad3 Proved choice and bchoice; changed Fun.thy -> thy
paulson
parents: 4089
diff changeset
    28
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
    29
Goal "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
4656
134d24ddaad3 Proved choice and bchoice; changed Fun.thy -> thy
paulson
parents: 4089
diff changeset
    30
by (fast_tac (claset() addEs [selectI]) 1);
134d24ddaad3 Proved choice and bchoice; changed Fun.thy -> thy
paulson
parents: 4089
diff changeset
    31
qed "bchoice";
134d24ddaad3 Proved choice and bchoice; changed Fun.thy -> thy
paulson
parents: 4089
diff changeset
    32
134d24ddaad3 Proved choice and bchoice; changed Fun.thy -> thy
paulson
parents: 4089
diff changeset
    33
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5441
diff changeset
    34
section "id";
5441
45bd13b15d80 added Id_apply
oheimb
parents: 5318
diff changeset
    35
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5441
diff changeset
    36
qed_goalw "id_apply" thy [id_def] "id x = x" (K [rtac refl 1]);
a82a038a3e7a id <-> Id
nipkow
parents: 5441
diff changeset
    37
Addsimps [id_apply];
5441
45bd13b15d80 added Id_apply
oheimb
parents: 5318
diff changeset
    38
45bd13b15d80 added Id_apply
oheimb
parents: 5318
diff changeset
    39
5306
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    40
section "o";
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    41
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    42
qed_goalw "o_apply" thy [o_def] "(f o g) x = f (g x)"
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    43
 (K [rtac refl 1]);
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    44
Addsimps [o_apply];
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    45
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    46
qed_goalw "o_assoc" thy [o_def] "f o (g o h) = f o g o h"
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    47
  (K [rtac ext 1, rtac refl 1]);
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    48
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5441
diff changeset
    49
qed_goalw "id_o" thy [id_def] "id o g = g"
5306
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    50
 (K [rtac ext 1, Simp_tac 1]);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5441
diff changeset
    51
Addsimps [id_o];
5306
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    52
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5441
diff changeset
    53
qed_goalw "o_id" thy [id_def] "f o id = f"
5306
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    54
 (K [rtac ext 1, Simp_tac 1]);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5441
diff changeset
    55
Addsimps [o_id];
5306
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    56
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    57
Goalw [o_def] "(f o g)``r = f``(g``r)";
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    58
by (Blast_tac 1);
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    59
qed "image_compose";
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    60
5852
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
    61
Goalw [o_def] "UNION A (g o f) = UNION (f``A) g";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
    62
by (Blast_tac 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
    63
qed "UNION_o";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
    64
5306
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    65
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    66
section "inj";
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
    67
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    68
(*** inj(f): f is a one-to-one function ***)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    69
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
    70
val prems = Goalw [inj_def]
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    71
    "[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
    72
by (blast_tac (claset() addIs prems) 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    73
qed "injI";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    74
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
    75
val [major] = Goal "(!!x. g(f(x)) = x) ==> inj(f)";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    76
by (rtac injI 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    77
by (etac (arg_cong RS box_equals) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    78
by (rtac major 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    79
by (rtac major 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    80
qed "inj_inverseI";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    81
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
    82
Goalw [inj_def] "[| inj(f); f(x) = f(y) |] ==> x=y";
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
    83
by (Blast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    84
qed "injD";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    85
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    86
(*Useful with the simplifier*)
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
    87
Goal "inj(f) ==> (f(x) = f(y)) = (x=y)";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    88
by (rtac iffI 1);
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
    89
by (etac arg_cong 2);
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
    90
by (etac injD 1);
5318
72bf8039b53f expandshort
paulson
parents: 5316
diff changeset
    91
by (assume_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    92
qed "inj_eq";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    93
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
    94
Goal "inj(f) ==> (@x. f(x)=f(y)) = y";
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
    95
by (etac injD 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    96
by (rtac selectI 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    97
by (rtac refl 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    98
qed "inj_select";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    99
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   100
(*A one-to-one function has an inverse (given using select).*)
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   101
Goalw [inv_def] "inj(f) ==> inv f (f x) = x";
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   102
by (etac inj_select 1);
2912
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv.
nipkow
parents: 2890
diff changeset
   103
qed "inv_f_f";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   104
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   105
(* Useful??? *)
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   106
val [oneone,minor] = Goal
2912
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv.
nipkow
parents: 2890
diff changeset
   107
    "[| 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
   108
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
   109
by (rtac (rangeI RS minor) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   110
qed "inj_transfer";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   111
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   112
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   113
(*** 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
   114
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   115
val prems = Goalw [inj_on_def]
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   116
    "(!! 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
   117
by (blast_tac (claset() addIs prems) 1);
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   118
qed "inj_onI";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   119
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   120
val [major] = Goal 
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   121
    "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   122
by (rtac inj_onI 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   123
by (etac (apply_inverse RS trans) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   124
by (REPEAT (eresolve_tac [asm_rl,major] 1));
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   125
qed "inj_on_inverseI";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   126
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   127
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
   128
by (Blast_tac 1);
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   129
qed "inj_onD";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   130
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   131
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
   132
by (blast_tac (claset() addSDs [inj_onD]) 1);
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   133
qed "inj_on_iff";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   134
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   135
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
   136
by (Blast_tac 1);
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   137
qed "inj_on_contraD";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   138
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   139
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
   140
by (Blast_tac 1);
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   141
qed "subset_inj_on";
3341
89fe22bf9f54 New theorem subset_inj_onto
paulson
parents: 2935
diff changeset
   142
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   143
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   144
(*** Lemmas about inj ***)
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
Goalw [o_def] "[| inj(f);  inj_on g (range f) |] ==> inj(g o f)";
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   147
by (fast_tac (claset() addIs [injI] addEs [injD, inj_onD]) 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   148
qed "comp_inj";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   149
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   150
Goal "inj(f) ==> inj_on f A";
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   151
by (blast_tac (claset() addIs [injD, inj_onI]) 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   152
qed "inj_imp";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   153
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   154
Goalw [inv_def] "y : range(f) ==> f(inv f y) = y";
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   155
by (fast_tac (claset() addIs [selectI]) 1);
2912
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv.
nipkow
parents: 2890
diff changeset
   156
qed "f_inv_f";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   157
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   158
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
   159
by (rtac (arg_cong RS box_equals) 1);
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5306
diff changeset
   160
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
   161
qed "inv_injective";
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv.
nipkow
parents: 2890
diff changeset
   162
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   163
Goal "[| inj(f);  A<=range(f) |] ==> inj_on (inv f) A";
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   164
by (fast_tac (claset() addIs [inj_onI] 
2912
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv.
nipkow
parents: 2890
diff changeset
   165
                      addEs [inv_injective,injD]) 1);
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   166
qed "inj_on_inv";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   167
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4830
diff changeset
   168
Goalw [inj_on_def]
5148
74919e8f221c More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5143
diff changeset
   169
   "[| 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
   170
by (Blast_tac 1);
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   171
qed "inj_on_image_Int";
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 3842
diff changeset
   172
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4830
diff changeset
   173
Goalw [inj_on_def]
5148
74919e8f221c More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5143
diff changeset
   174
   "[| 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
   175
by (Blast_tac 1);
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4656
diff changeset
   176
qed "inj_on_image_set_diff";
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 3842
diff changeset
   177
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   178
Goalw [inj_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
   179
by (Blast_tac 1);
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 3842
diff changeset
   180
qed "image_Int";
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 3842
diff changeset
   181
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   182
Goalw [inj_def] "inj f ==> f``(A-B) = f``A - f``B";
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 3842
diff changeset
   183
by (Blast_tac 1);
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 3842
diff changeset
   184
qed "image_set_diff";
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 3842
diff changeset
   185
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   186
5847
17c869f24c5f proved surjI
paulson
parents: 5608
diff changeset
   187
17c869f24c5f proved surjI
paulson
parents: 5608
diff changeset
   188
val [major] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g";
17c869f24c5f proved surjI
paulson
parents: 5608
diff changeset
   189
by (blast_tac (claset() addIs [major RS sym]) 1);
17c869f24c5f proved surjI
paulson
parents: 5608
diff changeset
   190
qed "surjI";
17c869f24c5f proved surjI
paulson
parents: 5608
diff changeset
   191
17c869f24c5f proved surjI
paulson
parents: 5608
diff changeset
   192
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   193
val set_cs = claset() delrules [equalityI];
5305
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   194
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   195
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   196
section "fun_upd";
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   197
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   198
Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)";
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   199
by Safe_tac;
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   200
by (etac subst 1);
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   201
by (rtac ext 2);
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   202
by Auto_tac;
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   203
qed "fun_upd_idem_iff";
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   204
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   205
(* f x = y ==> f(x:=y) = f *)
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   206
bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2);
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   207
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   208
(* f(x := f x) = f *)
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   209
AddIffs [refl RS fun_upd_idem];
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   210
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   211
Goal "(f(x:=y))z = (if z=x then y else f z)";
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   212
by (simp_tac (simpset() addsimps [fun_upd_def]) 1);
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   213
qed "fun_upd_apply";
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   214
Addsimps [fun_upd_apply];
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   215
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   216
qed_goal "fun_upd_same" thy "(f(x:=y)) x = y" 
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   217
	(K [Simp_tac 1]);
5306
3d1368a3a2a2 added theorems Id_o, o_Id
oheimb
parents: 5305
diff changeset
   218
qed_goal "fun_upd_other" thy "!!X. z~=x ==> (f(x:=y)) z = f z"
5305
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   219
	(K [Asm_simp_tac 1]);
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   220
(*Addsimps [fun_upd_same, fun_upd_other];*)
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   221
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   222
Goal "a ~= c ==> m(a:=b)(c:=d) = m(c:=d)(a:=b)";
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   223
by (rtac ext 1);
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   224
by (Auto_tac);
513925de8962 cleanup for Fun.thy:
oheimb
parents: 5148
diff changeset
   225
qed "fun_upd_twist";
5852
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   226
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   227
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   228
(*** -> and Pi, by Florian Kammueller and LCP ***)
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   229
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   230
val prems = Goalw [Pi_def]
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   231
"[| !!x. x: A ==> f x: B x; !!x. x ~: A  ==> f(x) = (@ y. True)|] \
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   232
\    ==> f: Pi A B";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   233
by (auto_tac (claset(), simpset() addsimps prems));
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   234
qed "Pi_I";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   235
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   236
val prems = Goal 
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   237
"[| !!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
   238
by (blast_tac (claset() addIs Pi_I::prems) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   239
qed "funcsetI";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   240
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   241
Goalw [Pi_def] "[|f: Pi A B; x: A|] ==> f x: B x";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   242
by Auto_tac;
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   243
qed "Pi_mem";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   244
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   245
Goalw [Pi_def] "[|f: A funcset B; x: A|] ==> f x: B";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   246
by Auto_tac;
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   247
qed "funcset_mem";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   248
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   249
Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = (@ y. True)";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   250
by Auto_tac;
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   251
qed "apply_arb";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   252
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   253
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
   254
by (rtac ext 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   255
by Auto_tac;
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   256
val Pi_extensionality = ballI RSN (3, result());
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   257
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   258
(*** compose ***)
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   259
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   260
Goalw [Pi_def, compose_def, restrict_def]
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   261
     "[| 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
   262
by Auto_tac;
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   263
qed "funcset_compose";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   264
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   265
Goal "[| f: A funcset B; g: B funcset C; h: C funcset D |]\
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   266
\     ==> compose A h (compose A g f) = compose A (compose B h g) f";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   267
by (res_inst_tac [("A","A")] Pi_extensionality 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   268
by (blast_tac (claset() addIs [funcset_compose]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   269
by (blast_tac (claset() addIs [funcset_compose]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   270
by (rewrite_goals_tac [Pi_def, compose_def, restrict_def]);  
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   271
by Auto_tac;
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   272
qed "compose_assoc";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   273
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   274
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
   275
by (asm_full_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   276
qed "compose_eq";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   277
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   278
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
   279
\     ==> compose A g f `` A = C";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   280
by (auto_tac (claset(),
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   281
	      simpset() addsimps [image_def, compose_eq]));
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   282
qed "surj_compose";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   283
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   284
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   285
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
   286
\     ==> inj_on (compose A g f) A";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   287
by (auto_tac (claset(),
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   288
	      simpset() addsimps [inj_on_def, compose_eq]));
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   289
qed "inj_on_compose";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   290
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   291
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   292
(*** restrict / lam ***)
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   293
Goal "[| f `` A <= B |] ==> (lam x: A. f x) : A funcset B";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   294
by (auto_tac (claset(),
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   295
	      simpset() addsimps [restrict_def, Pi_def]));
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   296
qed "restrict_in_funcset";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   297
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   298
val prems = Goalw [restrict_def, Pi_def]
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   299
     "(!!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
   300
by (asm_simp_tac (simpset() addsimps prems) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   301
qed "restrictI";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   302
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   303
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   304
Goal "x: A ==> (lam y: A. f y) x = f x";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   305
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   306
qed "restrict_apply1";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   307
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   308
Goal "[| x: A; f : A funcset B |] ==> (lam y: A. f y) x : B";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   309
by (asm_full_simp_tac (simpset() addsimps [restrict_apply1,Pi_def]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   310
qed "restrict_apply1_mem";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   311
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   312
Goal "x ~: A ==> (lam y: A. f y) x =  (@ y. True)";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   313
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   314
qed "restrict_apply2";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   315
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   316
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   317
val prems = Goal
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   318
    "(!!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
   319
by (rtac ext 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   320
by (auto_tac (claset(),
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   321
	      simpset() addsimps prems@[restrict_def, Pi_def]));
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   322
qed "restrict_ext";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   323
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   324
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   325
(*** Inverse ***)
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   326
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   327
Goal "[|f `` A = B;  x: B |] ==> ? y: A. f y = x";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   328
by (Blast_tac 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   329
qed "surj_image";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   330
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   331
Goalw [Inv_def] "[| f `` A = B; f : A funcset B |] \
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   332
\                ==> (lam x: B. (Inv A f) x) : B funcset A";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   333
by (fast_tac (claset() addIs [restrict_in_funcset, selectI2]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   334
qed "Inv_funcset";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   335
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   336
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   337
Goal "[| f: A funcset B;  inj_on f A;  f `` A = B;  x: A |] \
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   338
\     ==> (lam y: B. (Inv A f) y) (f x) = x";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   339
by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   340
by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   341
by (rtac selectI2 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   342
by Auto_tac;
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   343
qed "Inv_f_f";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   344
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   345
Goal "[| f: A funcset B;  f `` A = B;  x: B |] \
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   346
\     ==> f ((lam y: B. (Inv A f y)) x) = x";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   347
by (asm_simp_tac (simpset() addsimps [Inv_def, restrict_apply1]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   348
by (fast_tac (claset() addIs [selectI2]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   349
qed "f_Inv_f";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   350
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   351
Goal "[| f: A funcset B;  inj_on f A;  f `` A = B |]\
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   352
\     ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   353
by (rtac Pi_extensionality 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   354
by (blast_tac (claset() addIs [funcset_compose, Inv_funcset]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   355
by (blast_tac (claset() addIs [restrict_in_funcset]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   356
by (asm_simp_tac
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   357
    (simpset() addsimps [restrict_apply1, compose_def, Inv_f_f]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   358
qed "compose_Inv_id";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   359
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   360
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   361
(*** Pi and Applyall ***)
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   362
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   363
Goalw [Pi_def] "[| B(x) = {};  x: A |] ==> (PI x: A. B x) = {}";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   364
by Auto_tac;
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   365
qed "Pi_eq_empty";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   366
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   367
Goal "[| (PI x: A. B x) ~= {};  x: A |] ==> B(x) ~= {}";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   368
by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   369
qed "Pi_total1";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   370
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   371
Goal "[| a : A; Pi A B ~= {} |] ==> Applyall (Pi A B) a = B a";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   372
by (auto_tac (claset(), simpset() addsimps [Applyall_def, Pi_def]));
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   373
by (rename_tac "g z" 1);
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   374
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
   375
by (auto_tac (claset(), simpset() addsimps [split_if_mem1, split_if_eq1]));
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   376
qed "Applyall_beta";
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   377
5865
2303f5a3036d moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents: 5852
diff changeset
   378
Goal "Pi {} B = { (%x. @ y. True) }";
2303f5a3036d moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents: 5852
diff changeset
   379
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
   380
qed "Pi_empty";
5852
4d7320490be4 the function space operator
paulson
parents: 5847
diff changeset
   381
5865
2303f5a3036d moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents: 5852
diff changeset
   382
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
   383
by (auto_tac (claset(),
2303f5a3036d moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents: 5852
diff changeset
   384
	      simpset() addsimps [impOfSubs major]));
2303f5a3036d moved some facts about Pi from ex/PiSets to Fun.ML
paulson
parents: 5852
diff changeset
   385
qed "Pi_mono";