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