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