src/HOL/Hilbert_Choice_lemmas.ML
author paulson
Thu Sep 26 10:51:29 2002 +0200 (2002-09-26)
changeset 13585 db4005b40cc6
parent 12459 6978ab7cac64
permissions -rw-r--r--
Converted Fun to Isar style.
Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy.
Renamed constant "Fun.op o" to "Fun.comp"
paulson@11453
     1
(*  Title:      HOL/Hilbert_Choice_lemmas
paulson@11454
     2
    ID: $Id$
paulson@11453
     3
    Author:     Lawrence C Paulson
paulson@11453
     4
    Copyright   2001  University of Cambridge
paulson@11453
     5
paulson@11453
     6
Lemmas for Hilbert's epsilon-operator and the Axiom of Choice
paulson@11453
     7
*)
paulson@11453
     8
paulson@11453
     9
paulson@11453
    10
(* ML bindings *)
paulson@11453
    11
val someI = thm "someI";
paulson@11453
    12
paulson@11453
    13
section "SOME: Hilbert's Epsilon-operator";
paulson@11453
    14
paulson@11453
    15
(*Easier to apply than someI if witness ?a comes from an EX-formula*)
paulson@11453
    16
Goal "EX x. P x ==> P (SOME x. P x)";
paulson@11453
    17
by (etac exE 1);
paulson@11453
    18
by (etac someI 1);
paulson@11453
    19
qed "someI_ex";
paulson@11453
    20
paulson@11453
    21
(*Easier to apply than someI: conclusion has only one occurrence of P*)
paulson@11453
    22
val prems = Goal "[| P a;  !!x. P x ==> Q x |] ==> Q (SOME x. P x)";
paulson@11453
    23
by (resolve_tac prems 1);
paulson@11453
    24
by (rtac someI 1);
paulson@11453
    25
by (resolve_tac prems 1) ;
paulson@11453
    26
qed "someI2";
paulson@11453
    27
paulson@11453
    28
(*Easier to apply than someI2 if witness ?a comes from an EX-formula*)
paulson@11453
    29
val [major,minor] = Goal "[| EX a. P a; !!x. P x ==> Q x |] ==> Q (SOME x. P x)";
paulson@11453
    30
by (rtac (major RS exE) 1);
paulson@11453
    31
by (etac someI2 1 THEN etac minor 1);
paulson@11453
    32
qed "someI2_ex";
paulson@11453
    33
paulson@11453
    34
val prems = Goal "[| P a;  !!x. P x ==> x=a |] ==> (SOME x. P x) = a";
paulson@11453
    35
by (rtac someI2 1);
paulson@11453
    36
by (REPEAT (ares_tac prems 1)) ;
paulson@11453
    37
qed "some_equality";
paulson@11453
    38
AddIs [some_equality];
paulson@11453
    39
paulson@11453
    40
Goal "[| EX!x. P x; P a |] ==> (SOME x. P x) = a";
paulson@11453
    41
by (rtac some_equality 1);
paulson@11453
    42
by  (atac 1);
paulson@11453
    43
by (etac ex1E 1);
paulson@11453
    44
by (etac all_dupE 1);
paulson@11453
    45
by (dtac mp 1);
paulson@11453
    46
by  (atac 1);
paulson@11453
    47
by (etac ssubst 1);
paulson@11453
    48
by (etac allE 1);
paulson@11453
    49
by (etac mp 1);
paulson@11453
    50
by (atac 1);
paulson@11453
    51
qed "some1_equality";
paulson@11453
    52
paulson@11453
    53
Goal "P (SOME x. P x) =  (EX x. P x)";
paulson@11453
    54
by (rtac iffI 1);
paulson@11453
    55
by (etac exI 1);
paulson@11453
    56
by (etac exE 1);
paulson@11453
    57
by (etac someI 1);
paulson@11453
    58
qed "some_eq_ex";
paulson@11453
    59
paulson@11453
    60
Goal "(SOME y. y=x) = x";
paulson@11453
    61
by (rtac some_equality 1);
paulson@11453
    62
by (rtac refl 1);
paulson@11453
    63
by (atac 1);
paulson@11453
    64
qed "some_eq_trivial";
paulson@11453
    65
paulson@11453
    66
Goal "(SOME y. x=y) = x";
paulson@11453
    67
by (rtac some_equality 1);
paulson@11453
    68
by (rtac refl 1);
paulson@11453
    69
by (etac sym 1);
paulson@11453
    70
qed "some_sym_eq_trivial";
paulson@11453
    71
Addsimps [some_eq_trivial, some_sym_eq_trivial];
paulson@11453
    72
paulson@11453
    73
paulson@11453
    74
(** "Axiom" of Choice, proved using the description operator **)
paulson@11453
    75
paulson@11460
    76
(*Used in Tools/meson.ML*)
paulson@11460
    77
Goal "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
paulson@11460
    78
by (fast_tac (claset() addEs [someI]) 1);
paulson@11460
    79
qed "choice";
paulson@11453
    80
paulson@11453
    81
Goal "ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
paulson@11453
    82
by (fast_tac (claset() addEs [someI]) 1);
paulson@11453
    83
qed "bchoice";
paulson@11453
    84
paulson@11453
    85
paulson@11460
    86
section "Function Inverse";
paulson@11453
    87
paulson@11453
    88
val inv_def = thm "inv_def";
paulson@11453
    89
val Inv_def = thm "Inv_def";
paulson@11453
    90
paulson@11453
    91
Goal "inv id = id";
paulson@11453
    92
by (simp_tac (simpset() addsimps [inv_def,id_def]) 1);
paulson@11453
    93
qed "inv_id";
paulson@11453
    94
Addsimps [inv_id];
paulson@11453
    95
paulson@11453
    96
(*A one-to-one function has an inverse.*)
paulson@11453
    97
Goalw [inv_def] "inj(f) ==> inv f (f x) = x";
paulson@11453
    98
by (asm_simp_tac (simpset() addsimps [inj_eq]) 1); 
paulson@11453
    99
qed "inv_f_f";
paulson@11453
   100
Addsimps [inv_f_f];
paulson@11453
   101
paulson@11453
   102
Goal "[| inj(f);  f x = y |] ==> inv f y = x";
paulson@11453
   103
by (etac subst 1);
paulson@11453
   104
by (etac inv_f_f 1);
paulson@11453
   105
qed "inv_f_eq";
paulson@11453
   106
paulson@11453
   107
Goal "[| inj f; ALL x. f(g x) = x |] ==> inv f = g";
paulson@11453
   108
by (blast_tac (claset() addIs [ext, inv_f_eq]) 1); 
paulson@11453
   109
qed "inj_imp_inv_eq";
paulson@11453
   110
paulson@11453
   111
(* Useful??? *)
paulson@11453
   112
val [oneone,minor] = Goal
paulson@11453
   113
    "[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)";
paulson@11453
   114
by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1);
paulson@11453
   115
by (rtac (rangeI RS minor) 1);
paulson@11453
   116
qed "inj_transfer";
paulson@11453
   117
paulson@11453
   118
Goal "(inj f) = (inv f o f = id)";
paulson@11453
   119
by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
paulson@11453
   120
by (blast_tac (claset() addIs [inj_inverseI, inv_f_f]) 1);
paulson@11453
   121
qed "inj_iff";
paulson@11453
   122
paulson@11453
   123
Goal "inj f ==> surj (inv f)";
paulson@11453
   124
by (blast_tac (claset() addIs [surjI, inv_f_f]) 1);
paulson@11453
   125
qed "inj_imp_surj_inv";
paulson@11453
   126
paulson@11453
   127
Goalw [inv_def] "y : range(f) ==> f(inv f y) = y";
paulson@11453
   128
by (fast_tac (claset() addIs [someI]) 1);
paulson@11453
   129
qed "f_inv_f";
paulson@11453
   130
paulson@11453
   131
Goal "surj f ==> f(inv f y) = y";
paulson@11453
   132
by (asm_simp_tac (simpset() addsimps [f_inv_f, surj_range]) 1);
paulson@11453
   133
qed "surj_f_inv_f";
paulson@11453
   134
paulson@11453
   135
Goal "[| inv f x = inv f y;  x: range(f);  y: range(f) |] ==> x=y";
paulson@11453
   136
by (rtac (arg_cong RS box_equals) 1);
paulson@11453
   137
by (REPEAT (ares_tac [f_inv_f] 1));
paulson@11453
   138
qed "inv_injective";
paulson@11453
   139
paulson@11453
   140
Goal "A <= range(f) ==> inj_on (inv f) A";
paulson@11453
   141
by (fast_tac (claset() addIs [inj_onI] 
paulson@11453
   142
                       addEs [inv_injective, injD]) 1);
paulson@11453
   143
qed "inj_on_inv";
paulson@11453
   144
paulson@11453
   145
Goal "surj f ==> inj (inv f)";
paulson@11453
   146
by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1);
paulson@11453
   147
qed "surj_imp_inj_inv";
paulson@11453
   148
paulson@11453
   149
Goal "(surj f) = (f o inv f = id)";
paulson@11453
   150
by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
paulson@11453
   151
by (blast_tac (claset() addIs [surjI, surj_f_inv_f]) 1);
paulson@11453
   152
qed "surj_iff";
paulson@11453
   153
paulson@11453
   154
Goal "[| surj f; ALL x. g(f x) = x |] ==> inv f = g";
paulson@11453
   155
by (rtac ext 1);
paulson@11453
   156
by (dres_inst_tac [("x","inv f x")] spec 1); 
paulson@11453
   157
by (asm_full_simp_tac (simpset() addsimps [surj_f_inv_f]) 1); 
paulson@11453
   158
qed "surj_imp_inv_eq";
paulson@11453
   159
paulson@11453
   160
Goalw [bij_def] "bij f ==> bij (inv f)";
paulson@11453
   161
by (asm_simp_tac (simpset() addsimps [inj_imp_surj_inv, surj_imp_inj_inv]) 1);
paulson@11453
   162
qed "bij_imp_bij_inv";
paulson@11453
   163
paulson@11453
   164
val prems = 
paulson@11453
   165
Goalw [inv_def] "[| !! x. g (f x) = x;  !! y. f (g y) = y |] ==> inv f = g";
paulson@11453
   166
by (rtac ext 1);
paulson@11453
   167
by (auto_tac (claset(), simpset() addsimps prems));
paulson@11453
   168
qed "inv_equality";
paulson@11453
   169
paulson@11453
   170
Goalw [bij_def] "bij f ==> inv (inv f) = f";
paulson@11453
   171
by (rtac inv_equality 1);
paulson@11453
   172
by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f]));
paulson@11453
   173
qed "inv_inv_eq";
paulson@11453
   174
paulson@11453
   175
(** bij(inv f) implies little about f.  Consider f::bool=>bool such that
paulson@11453
   176
    f(True)=f(False)=True.  Then it's consistent with axiom someI that
paulson@11453
   177
    inv(f) could be any function at all, including the identity function.
paulson@11453
   178
    If inv(f)=id then inv(f) is a bijection, but inj(f), surj(f) and
paulson@11453
   179
    inv(inv(f))=f all fail.
paulson@11453
   180
**)
paulson@11453
   181
paulson@11453
   182
Goalw [bij_def] "[| bij f; bij g |] ==> inv (f o g) = inv g o inv f";
paulson@11453
   183
by (rtac (inv_equality) 1);
paulson@11453
   184
by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f]));
paulson@11453
   185
qed "o_inv_distrib";
paulson@11453
   186
paulson@11453
   187
paulson@11453
   188
Goal "surj f ==> f ` (inv f ` A) = A";
paulson@11453
   189
by (asm_simp_tac (simpset() addsimps [image_eq_UN, surj_f_inv_f]) 1);
paulson@11453
   190
qed "image_surj_f_inv_f";
paulson@11453
   191
paulson@11453
   192
Goal "inj f ==> (inv f) ` (f ` A) = A";
paulson@11453
   193
by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 1);
paulson@11453
   194
qed "image_inv_f_f";
paulson@11453
   195
paulson@11453
   196
Goalw [image_def] "inj(f) ==> inv(f)`(f`X) = X";
paulson@11453
   197
by Auto_tac;
paulson@11453
   198
qed "inv_image_comp";
paulson@11453
   199
paulson@11453
   200
Goal "bij f ==> f ` Collect P = {y. P (inv f y)}";
paulson@11453
   201
by Auto_tac;
paulson@11453
   202
by (force_tac (claset(), simpset() addsimps [bij_is_inj]) 1);
paulson@11453
   203
by (blast_tac (claset() addIs [bij_is_surj RS surj_f_inv_f RS sym]) 1);
paulson@11453
   204
qed "bij_image_Collect_eq";
paulson@11453
   205
paulson@11453
   206
Goal "bij f ==> f -` A = inv f ` A";
paulson@11453
   207
by Safe_tac;
paulson@11453
   208
by (asm_simp_tac (simpset() addsimps [bij_is_surj RS surj_f_inv_f]) 2);
paulson@11453
   209
by (blast_tac (claset() addIs [bij_is_inj RS inv_f_f RS sym]) 1);
paulson@11453
   210
qed "bij_vimage_eq_inv_image";
paulson@11453
   211
paulson@11460
   212
paulson@11460
   213
section "Inverse of a PI-function (restricted domain)";
paulson@11453
   214
paulson@11453
   215
Goal "[| inj_on f A;  x : A |] ==> Inv A f (f x) = x";
paulson@11453
   216
by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
paulson@11453
   217
by (blast_tac (claset() addIs [someI2]) 1); 
paulson@11453
   218
qed "Inv_f_f";
paulson@11453
   219
paulson@11453
   220
Goal "y : f`A  ==> f (Inv A f y) = y";
paulson@11453
   221
by (asm_simp_tac (simpset() addsimps [Inv_def]) 1);
paulson@11453
   222
by (fast_tac (claset() addIs [someI2]) 1);
paulson@11453
   223
qed "f_Inv_f";
paulson@11453
   224
paulson@11453
   225
Goal "[| Inv A f x = Inv A f y;  x : f`A;  y : f`A |] ==> x=y";
paulson@11453
   226
by (rtac (arg_cong RS box_equals) 1);
paulson@11453
   227
by (REPEAT (ares_tac [f_Inv_f] 1));
paulson@11453
   228
qed "Inv_injective";
paulson@11453
   229
paulson@11453
   230
Goal "B <= f`A ==> inj_on (Inv A f) B";
paulson@11453
   231
by (rtac inj_onI 1);
paulson@11453
   232
by (blast_tac (claset() addIs [inj_onI] addDs [Inv_injective, injD]) 1);
paulson@11453
   233
qed "inj_on_Inv";
paulson@11453
   234
paulson@11453
   235
paulson@11460
   236
paulson@11460
   237
section "split and SOME";
paulson@11453
   238
paulson@11453
   239
(*Can't be added to simpset: loops!*)
paulson@11453
   240
Goal "(SOME x. P x) = (SOME (a,b). P(a,b))";
paulson@11453
   241
by (simp_tac (simpset() addsimps [split_Pair_apply]) 1);
paulson@11453
   242
qed "split_paired_Eps";
paulson@11453
   243
paulson@11453
   244
Goalw [split_def] "Eps (split P) = (SOME xy. P (fst xy) (snd xy))";
paulson@11453
   245
by (rtac refl 1);
paulson@11453
   246
qed "Eps_split";
paulson@11453
   247
paulson@11453
   248
Goal "(@(x',y'). x = x' & y = y') = (x,y)";
paulson@11453
   249
by (Blast_tac 1);
paulson@11453
   250
qed "Eps_split_eq";
paulson@11453
   251
Addsimps [Eps_split_eq];
paulson@11454
   252
paulson@11454
   253
paulson@11460
   254
section "A relation is wellfounded iff it has no infinite descending chain";
paulson@11454
   255
paulson@11454
   256
Goalw [wf_eq_minimal RS eq_reflection]
paulson@11454
   257
  "wf r = (~(EX f. ALL i. (f(Suc i),f i) : r))";
paulson@11454
   258
by (rtac iffI 1);
paulson@11454
   259
 by (rtac notI 1);
paulson@11454
   260
 by (etac exE 1);
paulson@11454
   261
 by (eres_inst_tac [("x","{w. EX i. w=f i}")] allE 1);
paulson@11454
   262
 by (Blast_tac 1);
paulson@11454
   263
by (etac contrapos_np 1);
paulson@11454
   264
by (Asm_full_simp_tac 1);
paulson@11454
   265
by (Clarify_tac 1);
paulson@11454
   266
by (subgoal_tac "ALL n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
paulson@11454
   267
 by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
paulson@11454
   268
 by (rtac allI 1);
paulson@11454
   269
 by (Simp_tac 1);
paulson@11454
   270
 by (rtac someI2_ex 1);
paulson@11454
   271
  by (Blast_tac 1);
paulson@11454
   272
 by (Blast_tac 1);
paulson@11454
   273
by (rtac allI 1);
paulson@11454
   274
by (induct_tac "n" 1);
paulson@11454
   275
 by (Asm_simp_tac 1);
paulson@11454
   276
by (Simp_tac 1);
paulson@11454
   277
by (rtac someI2_ex 1);
paulson@11454
   278
 by (Blast_tac 1);
paulson@11454
   279
by (Blast_tac 1);
paulson@11454
   280
qed "wf_iff_no_infinite_down_chain";
paulson@11454
   281