src/ZF/AC/DC.ML
author paulson
Thu, 13 Jan 2000 17:31:30 +0100
changeset 8123 a71686059be0
parent 7499 23e090051cb8
child 9402 480a1b40fdd6
permissions -rw-r--r--
a bit of tidying
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
     1
(*  Title:      ZF/AC/DC.ML
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
     2
    ID:  $Id$
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
     3
    Author:     Krzysztof Grabczewski
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
     4
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
     5
The proofs concerning the Axiom of Dependent Choice
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
     6
*)
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
     7
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
     8
(* ********************************************************************** *)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
     9
(* DC ==> DC(omega)                                                       *)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    10
(*                                                                        *)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    11
(* The scheme of the proof:                                               *)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    12
(*                                                                        *)
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    13
(* Assume DC. Let R and X satisfy the premise of DC(omega).               *)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    14
(*                                                                        *)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    15
(* Define XX and RR as follows:                                           *)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    16
(*                                                                        *)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    17
(*       XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R})              *)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    18
(*       f RR g iff domain(g)=succ(domain(f)) &                           *)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    19
(*              restrict(g, domain(f)) = f                                *)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    20
(*                                                                        *)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    21
(* Then RR satisfies the hypotheses of DC.                                *)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    22
(* So applying DC:                                                        *)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    23
(*                                                                        *)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    24
(*       EX f:nat->XX. ALL n:nat. f`n RR f`succ(n)                        *)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    25
(*                                                                        *)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    26
(* Thence                                                                 *)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    27
(*                                                                        *)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    28
(*       ff = {<n, f`succ(n)`n>. n:nat}                                   *)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    29
(*                                                                        *)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    30
(* is the desired function.                                               *)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    31
(*                                                                        *)
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
    32
(* ********************************************************************** *)
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
    33
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    34
Open_locale "DC0_imp";
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    35
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    36
val all_ex = thm "all_ex";
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    37
val XX_def = thm "XX_def";
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    38
val RR_def = thm "RR_def";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
    39
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    40
Goalw [RR_def] "RR <= XX*XX";
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    41
by (Fast_tac 1);
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    42
qed "lemma1_1";
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    43
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    44
Goalw [RR_def, XX_def] "RR ~= 0";
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    45
by (rtac (all_ex RS ballE) 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
    46
by (eresolve_tac [empty_subsetI RS PowI RSN (2, notE)] 2);
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
    47
by (eresolve_tac [nat_0I RS n_lesspoll_nat RSN (2, impE)] 1);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
    48
by (etac bexE 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
    49
by (res_inst_tac [("a","<0, {<0, x>}>")] not_emptyI 1);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
    50
by (rtac CollectI 1);
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
    51
by (rtac SigmaI 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
    52
by (fast_tac (claset() addSIs [nat_0I RS UN_I, empty_fun]) 1);
2493
bdeb5024353a Removal of sum_cs and eq_cs
paulson
parents: 2483
diff changeset
    53
by (rtac (nat_1I RS UN_I) 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    54
by (asm_full_simp_tac (simpset() addsimps [singleton_0]) 2);
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    55
by (force_tac (claset() addSIs [singleton_fun RS Pi_type],
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    56
	      simpset() addsimps [singleton_0 RS sym]) 1);
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    57
qed "lemma1_2";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
    58
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    59
Goalw [RR_def, XX_def] "range(RR) <= domain(RR)";
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
    60
by (rtac range_subset_domain 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    61
by (Blast_tac 2);
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    62
by (Clarify_tac 1);
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    63
by (forward_tac [fun_is_rel RS image_subset RS PowI RS (all_ex RS bspec)] 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
    64
by (eresolve_tac [[n_lesspoll_nat, nat_into_Ord RSN (2, image_Ord_lepoll)]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    65
        MRS lepoll_lesspoll_lesspoll RSN (2, impE)] 1
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    66
        THEN REPEAT (assume_tac 1));
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
    67
by (etac bexE 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
    68
by (res_inst_tac [("x","cons(<n,x>, g)")] exI 1);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
    69
by (rtac CollectI 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    70
by (force_tac (claset() addSEs [cons_fun_type2],
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    71
	       simpset() addsimps [cons_image_n, cons_val_n, 
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    72
				   cons_image_k, cons_val_k]) 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
    73
by (asm_full_simp_tac (simpset()
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    74
        addsimps [domain_of_fun, succ_def, restrict_cons_eq]) 1);
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    75
qed "lemma1_3";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
    76
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
    77
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    78
Goal "[| ALL n:nat. <f`n, f`succ(n)> : RR;  f: nat -> XX;  n:nat |]  \
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    79
\     ==> EX k:nat. f`succ(n) : k -> X & n:k  \
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    80
\                 & <f`succ(n)``n, f`succ(n)`n> : R";
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6021
diff changeset
    81
by (induct_tac "n" 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
    82
by (dresolve_tac [nat_1I RSN (2, apply_type)] 1);
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
    83
by (dresolve_tac [nat_0I RSN (2, bspec)] 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    84
by (asm_full_simp_tac (simpset() addsimps [XX_def]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2496
diff changeset
    85
by Safe_tac;
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
    86
by (rtac bexI 1 THEN (assume_tac 2));
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    87
by (force_tac (claset() addIs [ltD]
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    88
                        addSEs [nat_0_le RS leE]
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    89
			addEs [sym RS trans RS succ_neq_0, domain_of_fun], 
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    90
	       simpset() addsimps [RR_def]) 1);
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    91
(** LEVEL 7, other subgoal **)
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
    92
by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1));
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
    93
by (subgoal_tac "f ` succ(succ(x)) : succ(k)->X" 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
    94
by (dresolve_tac [nat_succI RS nat_succI RSN (2, apply_type)] 1
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    95
        THEN (assume_tac 1));
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
    96
by (full_simp_tac (simpset() addsimps [XX_def,RR_def]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2496
diff changeset
    97
by Safe_tac;
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
    98
by (forw_inst_tac [("a","succ(k)")] (domain_of_fun RS sym RS trans) 1 THEN
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
    99
    (assume_tac 1));
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   100
by (forw_inst_tac [("a","xa")] (domain_of_fun RS sym RS trans) 1 THEN
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   101
    (assume_tac 1));
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   102
by (fast_tac (claset() addSEs [nat_into_Ord RS succ_in_succ]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   103
        addSDs [nat_into_Ord RS succ_in_succ RSN (2, bspec)]) 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   104
by (dtac domain_of_fun 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   105
by (full_simp_tac (simpset() addsimps [XX_def,RR_def]) 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   106
by (deepen_tac (claset() addDs [domain_of_fun RS sym RS trans]) 0 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   107
qed "lemma2";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   108
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   109
Goal "[| ALL n:nat. <f`n, f`succ(n)> : RR;  f: nat -> XX;  m:nat |]  \
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   110
\     ==>  {f`succ(x)`x. x:m} = {f`succ(m)`x. x:m}";
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   111
by (subgoal_tac "ALL x:m. f`succ(m)`x = f`succ(x)`x" 1);
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   112
by (Asm_full_simp_tac 1);
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6021
diff changeset
   113
by (induct_tac "m" 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   114
by (Fast_tac 1);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   115
by (rtac ballI 1);
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   116
by (etac succE 1);
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   117
by (rtac restrict_eq_imp_val_eq 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   118
by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1));
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   119
by (asm_full_simp_tac (simpset() addsimps [RR_def]) 1);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   120
by (dtac lemma2 1 THEN REPEAT (assume_tac 1));
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   121
by (fast_tac (claset() addSDs [domain_of_fun]) 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   122
by (dres_inst_tac [("x","xa")] bspec 1 THEN (assume_tac 1));
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   123
by (eresolve_tac [sym RS trans RS sym] 1);
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   124
by (resolve_tac [restrict_eq_imp_val_eq RS sym] 1);
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   125
by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1));
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   126
by (asm_full_simp_tac (simpset() addsimps [RR_def]) 1);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   127
by (dtac lemma2 1 THEN REPEAT (assume_tac 1));
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   128
by (blast_tac (claset() addSDs [domain_of_fun]
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   129
                        addIs [nat_into_Ord RSN (2, OrdmemD) RS subsetD]) 1);
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   130
qed "lemma3_1";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   131
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   132
Goal "[| ALL n:nat. <f`n, f`succ(n)> : RR;  f: nat -> XX;  m:nat |] \
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   133
\     ==> (lam x:nat. f`succ(x)`x) `` m = f`succ(m)``m";
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   134
by (etac natE 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   135
by (Asm_simp_tac 1);
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   136
by (stac image_lam 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   137
by (fast_tac (claset() addSEs [[nat_succI, Ord_nat] MRS OrdmemD]) 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   138
by (stac lemma3_1 1 THEN REPEAT (assume_tac 1));
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   139
by (Fast_tac 1);
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   140
by (fast_tac (claset() addSDs [lemma2]
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   141
		       addSEs [nat_into_Ord RSN (2, OrdmemD) RSN 
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   142
                            (2, image_fun RS sym)]) 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   143
qed "lemma3";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   144
6021
4a3fc834288e new Close_locale synatx
paulson
parents: 5482
diff changeset
   145
Close_locale "DC0_imp";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   146
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   147
Goalw [DC_def, DC0_def] "DC0 ==> DC(nat)";
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   148
by (Clarify_tac 1);
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   149
by (REPEAT (etac allE 1));
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   150
by (etac impE 1);
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   151
   (*these three results comprise Lemma 1*)
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   152
by (blast_tac (claset() addSIs (map export [lemma1_1, lemma1_2, lemma1_3])) 1);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   153
by (etac bexE 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   154
by (res_inst_tac [("x","lam n:nat. f`succ(n)`n")] bexI 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   155
by (fast_tac (claset() addSIs [lam_type] addSDs [export lemma2]
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   156
                       addSEs [fun_weaken_type, apply_type]) 2);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   157
by (rtac oallI 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   158
by (forward_tac [ltD RSN (3, export lemma2)] 1
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   159
        THEN assume_tac 2);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   160
by (fast_tac (claset() addSEs [fun_weaken_type]) 1);
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   161
(** LEVEL 10: last subgoal **)
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   162
by (stac (ltD RSN (3, export lemma3)) 1);
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   163
by (Force_tac 4);
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   164
by (assume_tac 3);
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   165
by (assume_tac 1);
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   166
by (fast_tac (claset() addSEs [fun_weaken_type]) 1);
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   167
qed "DC0_imp_DC_nat";
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   168
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   169
3862
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   170
(* ************************************************************************
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   171
   DC(omega) ==> DC                                                       
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   172
                                                                          
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   173
   The scheme of the proof:                                               
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   174
                                                                          
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   175
   Assume DC(omega). Let R and x satisfy the premise of DC.               
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   176
                                                                          
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   177
   Define XX and RR as follows:                                           
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   178
                                                                          
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   179
    XX = (UN n:nat. {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R})
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   180
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   181
    RR = {<z1,z2>:Fin(XX)*XX. 
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   182
           (domain(z2)=succ(UN f:z1. domain(f)) &
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   183
	    (ALL f:z1. restrict(z2, domain(f)) = f)) |      
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   184
	   (~ (EX g:XX. domain(g)=succ(UN f:z1. domain(f)) &
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   185
	                (ALL f:z1. restrict(g, domain(f)) = f)) &           
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   186
	    z2={<0,x>})}                                          
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   187
                                                                          
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   188
   Then XX and RR satisfy the hypotheses of DC(omega).                    
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   189
   So applying DC:                                                        
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   190
                                                                          
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   191
         EX f:nat->XX. ALL n:nat. f``n RR f`n                             
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   192
                                                                          
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   193
   Thence                                                                 
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   194
                                                                          
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   195
         ff = {<n, f`n`n>. n:nat}                                         
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   196
                                                                          
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   197
   is the desired function.                                               
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   198
                                                                          
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   199
************************************************************************* *)
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   200
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4723
diff changeset
   201
Goalw [lesspoll_def, Finite_def]
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   202
        "A lesspoll nat ==> Finite(A)";
8123
a71686059be0 a bit of tidying
paulson
parents: 7499
diff changeset
   203
by (fast_tac (claset() addSDs [ltD, lepoll_imp_ex_le_eqpoll]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2496
diff changeset
   204
qed "lesspoll_nat_is_Finite";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   205
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5068
diff changeset
   206
Goal "n:nat ==> ALL A. (A eqpoll n & A <= X) --> A : Fin(X)";
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6021
diff changeset
   207
by (induct_tac "n" 1);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   208
by (rtac allI 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   209
by (fast_tac (claset() addSIs [Fin.emptyI]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   210
        addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]) 1);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   211
by (rtac allI 1);
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   212
by (rtac impI 1);
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   213
by (etac conjE 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   214
by (resolve_tac [eqpoll_succ_imp_not_empty RS not_emptyE] 1
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   215
        THEN (assume_tac 1));
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 6070
diff changeset
   216
by (ftac Diff_sing_eqpoll 1 THEN (assume_tac 1));
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   217
by (etac allE 1);
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   218
by (etac impE 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   219
by (Fast_tac 1);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   220
by (dtac subsetD 1 THEN (assume_tac 1));
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   221
by (dresolve_tac [Fin.consI] 1 THEN (assume_tac 1));
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   222
by (asm_full_simp_tac (simpset() addsimps [cons_Diff]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2496
diff changeset
   223
qed "Finite_Fin_lemma";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   224
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5068
diff changeset
   225
Goalw [Finite_def] "[| Finite(A); A <= X |] ==> A : Fin(X)";
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   226
by (etac bexE 1);
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   227
by (dtac Finite_Fin_lemma 1);
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   228
by (etac allE 1);
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   229
by (etac impE 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   230
by (assume_tac 2);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   231
by (Fast_tac 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2496
diff changeset
   232
qed "Finite_Fin";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   233
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   234
Goal
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   235
 "x:X ==> {<0,x>}: (UN n:nat. {f:succ(n)->X. ALL k:n. <f`k, f`succ(k)> : R})";
2493
bdeb5024353a Removal of sum_cs and eq_cs
paulson
parents: 2483
diff changeset
   236
by (rtac (nat_0I RS UN_I) 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   237
by (fast_tac (claset() addSIs [singleton_fun RS Pi_type]
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   238
        addss (simpset() addsimps [singleton_0 RS sym])) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2496
diff changeset
   239
qed "singleton_in_funs";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   240
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   241
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   242
Open_locale "imp_DC0";
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   243
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   244
val XX_def = thm "XX_def";
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   245
val RR_def = thm "RR_def";
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   246
val allRR_def = thm "allRR_def";
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   247
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   248
Goal "[| range(R) <= domain(R);  x:domain(R) |]  \
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   249
\     ==> RR <= Pow(XX)*XX &  \
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   250
\            (ALL Y:Pow(XX). Y lesspoll nat --> (EX x:XX. <Y,x>:RR))";
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   251
by (rtac conjI 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   252
by (force_tac (claset() addSDs [FinD RS PowI], 
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   253
	       simpset() addsimps [RR_def]) 1); 
2483
95c2f9c0930a Default rewrite rules for quantification over Collect(A,P)
paulson
parents: 2469
diff changeset
   254
by (rtac (impI RS ballI) 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   255
by (dresolve_tac [[lesspoll_nat_is_Finite, PowD] MRS Finite_Fin] 1
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   256
        THEN (assume_tac 1));
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   257
by (excluded_middle_tac "EX g:XX. domain(g)=succ(UN f:Y. domain(f))  \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   258
\       & (ALL f:Y. restrict(g, domain(f)) = f)" 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   259
by (fast_tac (claset() addss (simpset() addsimps [RR_def])) 2); 
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   260
by (safe_tac (claset() delrules [domainE]));
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   261
by (rewrite_goals_tac [XX_def,RR_def]);
2483
95c2f9c0930a Default rewrite rules for quantification over Collect(A,P)
paulson
parents: 2469
diff changeset
   262
by (swap_res_tac [bexI] 1 THEN etac singleton_in_funs 2);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   263
by (asm_full_simp_tac (simpset() addsimps [nat_0I  RSN (2, bexI), 
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   264
					   cons_fun_type2]) 1);
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   265
qed "lemma4";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   266
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5068
diff changeset
   267
Goal "[| f:nat->X; n:nat |] ==>  \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   268
\       (UN x:f``succ(n). P(x)) =  P(f`n) Un (UN x:f``n. P(x))";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   269
by (asm_full_simp_tac (simpset()
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   270
        addsimps [Ord_nat RSN (2, OrdmemD) RSN (2, image_fun),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   271
        [nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2496
diff changeset
   272
qed "UN_image_succ_eq";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   273
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5068
diff changeset
   274
Goal "[| (UN x:f``n. P(x)) = y; P(f`n) = succ(y);  \
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   275
\        f:nat -> X; n:nat |] ==> (UN x:f``succ(n). P(x)) = succ(y)";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   276
by (asm_full_simp_tac (simpset() addsimps [UN_image_succ_eq]) 1);
2496
40efb87985b5 Removal of needless "addIs [equality]", etc.
paulson
parents: 2493
diff changeset
   277
by (Fast_tac 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2496
diff changeset
   278
qed "UN_image_succ_eq_succ";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   279
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5068
diff changeset
   280
Goal "[| f:succ(n) -> D;  n:nat;  \
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   281
\        domain(f)=succ(x); x=y |] ==> f`y : D";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   282
by (fast_tac (claset() addEs [apply_type]
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   283
	      addSDs [[sym, domain_of_fun] MRS trans]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2496
diff changeset
   284
qed "apply_domain_type";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   285
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5068
diff changeset
   286
Goal "[| f : nat -> X; n:nat |] ==> f``succ(n) = cons(f`n, f``n)";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   287
by (asm_full_simp_tac (simpset()
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   288
        addsimps [nat_succI, Ord_nat RSN (2, OrdmemD), image_fun]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2496
diff changeset
   289
qed "image_fun_succ";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   290
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   291
Goalw [XX_def] "[| domain(f`n) = succ(u); f : nat -> XX;  u=k;  n:nat |]   \
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   292
\               ==> f`n : succ(k) -> domain(R)";
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   293
by (dtac apply_type 1 THEN (assume_tac 1));
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   294
by (fast_tac (claset() addEs [domain_eq_imp_fun_type]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2496
diff changeset
   295
qed "f_n_type";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   296
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   297
Goalw [XX_def]
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   298
     "[| f : nat -> XX;  domain(f`n) = succ(k);  n:nat |]  \
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   299
\     ==> ALL i:k. <f`n`i, f`n`succ(i)> : R";
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   300
by (dtac apply_type 1 THEN (assume_tac 1));
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   301
by (etac UN_E 1);
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   302
by (etac CollectE 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   303
by (dresolve_tac [domain_of_fun RS sym RS trans] 1 THEN (assume_tac 1));
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   304
by (Asm_full_simp_tac 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2496
diff changeset
   305
qed "f_n_pairs_in_R";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   306
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4723
diff changeset
   307
Goalw [restrict_def]
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   308
     "[| restrict(f, domain(x))=x;  f:n->X;  domain(x) <= n |]  \
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   309
\     ==> restrict(cons(<n, y>, f), domain(x)) = x";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   310
by (eresolve_tac [sym RS trans RS sym] 1);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   311
by (rtac fun_extension 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   312
by (fast_tac (claset() addSIs [lam_type]) 1);
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   313
by (fast_tac (claset() addSIs [lam_type]) 1);
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   314
by (asm_full_simp_tac (simpset() addsimps [subsetD RS cons_val_k]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2496
diff changeset
   315
qed "restrict_cons_eq_restrict";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   316
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5068
diff changeset
   317
Goal "[| ALL x:f``n. restrict(f`n, domain(x))=x;  \
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   318
\        f : nat -> XX;  \
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   319
\        n:nat;  domain(f`n) = succ(n);  \
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   320
\        (UN x:f``n. domain(x)) <= n |] \
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   321
\     ==> ALL x:f``succ(n). restrict(cons(<succ(n),y>, f`n), domain(x)) = x";
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   322
by (rtac ballI 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   323
by (asm_full_simp_tac (simpset() addsimps [image_fun_succ]) 1);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   324
by (dtac f_n_type 1 THEN REPEAT (ares_tac [refl] 1));
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   325
by (etac disjE 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   326
by (asm_full_simp_tac (simpset() addsimps [domain_of_fun,restrict_cons_eq]) 1);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   327
by (dtac bspec 1 THEN (assume_tac 1));
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   328
by (fast_tac (claset() addSEs [restrict_cons_eq_restrict]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2496
diff changeset
   329
qed "all_in_image_restrict_eq";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   330
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   331
Goalw [RR_def, allRR_def]
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   332
     "[| ALL b<nat. <f``b, f`b> : RR;  \
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   333
\        f: nat -> XX; range(R) <= domain(R); x:domain(R)|]   \
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   334
\     ==> allRR";
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   335
by (rtac oallI 1);
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   336
by (dtac ltD 1);
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   337
by (etac nat_induct 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   338
by (dresolve_tac [[nat_0I, Ord_nat] MRS ltI RSN (2, ospec)] 1);
1200
d4551b1a6da7 Many small changes to make proofs run faster
lcp
parents: 1196
diff changeset
   339
by (fast_tac (FOL_cs addss
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   340
              (simpset() addsimps [singleton_fun RS domain_of_fun,
2493
bdeb5024353a Removal of sum_cs and eq_cs
paulson
parents: 2483
diff changeset
   341
                                  singleton_0, singleton_in_funs])) 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   342
(*induction step*) (** LEVEL 5 **)
3862
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   343
by (full_simp_tac (*prevent simplification of ~EX to ALL~*)
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   344
		  (FOL_ss addsimps [separation, split]) 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   345
by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   346
        THEN (assume_tac 1));
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   347
by (REPEAT (eresolve_tac [conjE, disjE] 1));
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   348
by (force_tac (FOL_cs addSEs [trans, subst_context]
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   349
                     addSIs [UN_image_succ_eq_succ], simpset()) 1);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   350
by (etac conjE 1);
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   351
by (etac notE 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   352
by (asm_lr_simp_tac (simpset() addsimps [XX_def, UN_image_succ_eq_succ]) 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   353
(** LEVEL 12 **)
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   354
by (REPEAT (eresolve_tac [conjE, bexE] 1));
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   355
by (dtac apply_domain_type 1 THEN REPEAT (assume_tac 1));
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   356
by (etac domainE 1);
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   357
by (etac domainE 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   358
by (forward_tac [export f_n_type] 1 THEN REPEAT (assume_tac 1));
2493
bdeb5024353a Removal of sum_cs and eq_cs
paulson
parents: 2483
diff changeset
   359
by (rtac bexI 1);
2483
95c2f9c0930a Default rewrite rules for quantification over Collect(A,P)
paulson
parents: 2469
diff changeset
   360
by (etac nat_succI 2);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   361
by (res_inst_tac [("x","cons(<succ(xa), ya>, f`xa)")] bexI 1);
2493
bdeb5024353a Removal of sum_cs and eq_cs
paulson
parents: 2483
diff changeset
   362
by (rtac conjI 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   363
by (fast_tac (FOL_cs
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   364
        addEs [subst_context RSN (2, trans) RS domain_cons_eq_succ,
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   365
	       subst_context, export all_in_image_restrict_eq, 
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   366
	       trans, equalityD1]) 2);
2483
95c2f9c0930a Default rewrite rules for quantification over Collect(A,P)
paulson
parents: 2469
diff changeset
   367
by (eresolve_tac [rangeI RSN (2, subsetD) RSN (2, cons_fun_type2)] 2
95c2f9c0930a Default rewrite rules for quantification over Collect(A,P)
paulson
parents: 2469
diff changeset
   368
        THEN REPEAT (assume_tac 2));
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   369
by (rtac ballI 1);
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   370
by (etac succE 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   371
(** LEVEL 25 **)
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   372
by (dresolve_tac [domain_of_fun RSN (2, export f_n_pairs_in_R)] 2
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   373
        THEN REPEAT (assume_tac 2));
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   374
by (dtac bspec 2 THEN (assume_tac 2));
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   375
by (asm_full_simp_tac (simpset()
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   376
        addsimps [nat_into_Ord RS succ_in_succ, succI2, cons_val_k]) 2);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   377
by (asm_full_simp_tac (simpset() addsimps [cons_val_n, cons_val_k]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2496
diff changeset
   378
qed "simplify_recursion";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   379
2483
95c2f9c0930a Default rewrite rules for quantification over Collect(A,P)
paulson
parents: 2469
diff changeset
   380
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   381
Goalw [allRR_def]
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   382
     "[| allRR; f: nat -> XX; range(R) <= domain(R); x:domain(R); n:nat |]   \
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   383
\     ==> f`n : succ(n) -> domain(R) & (ALL i:n. <f`n`i, f`n`succ(i)>:R)";
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   384
by (dtac ospec 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   385
by (eresolve_tac [Ord_nat RSN (2, ltI)] 1);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   386
by (etac CollectE 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   387
by (Asm_full_simp_tac 1);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   388
by (rtac conjI 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   389
by (fast_tac (FOL_cs addSEs [conjE, f_n_pairs_in_R, trans, subst_context]) 2);
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   390
by (rewtac XX_def);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   391
by (fast_tac (claset()
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   392
        addSEs [trans RS domain_eq_imp_fun_type, subst_context]) 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   393
qed "lemma2";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   394
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   395
Goal "[| allRR;  f : nat -> XX;  n:nat;  range(R) <= domain(R);  x:domain(R)  \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   396
\       |] ==> f`n`n = f`succ(n)`n";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   397
by (forward_tac [lemma2 RS conjunct1 RS domain_of_fun] 1
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   398
        THEN REPEAT (assume_tac 1));
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   399
by (rewtac allRR_def);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   400
by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   401
        THEN (assume_tac 1));
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   402
by (Asm_full_simp_tac 1);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   403
by (REPEAT (etac conjE 1));
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   404
by (etac ballE 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   405
by (eresolve_tac [restrict_eq_imp_val_eq RS sym] 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   406
by (fast_tac (claset() addSEs [ssubst]) 1);
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   407
by (asm_full_simp_tac (simpset()
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   408
        addsimps [[nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   409
qed "lemma3";
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   410
6021
4a3fc834288e new Close_locale synatx
paulson
parents: 5482
diff changeset
   411
Close_locale "imp_DC0";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   412
3862
6f389875ab33 Patch to avoid simplification of ~EX to ALL~
paulson
parents: 3731
diff changeset
   413
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   414
Goalw [DC_def, DC0_def] "DC(nat) ==> DC0";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   415
by (REPEAT (resolve_tac [allI, impI] 1));
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   416
by (REPEAT (eresolve_tac [asm_rl, conjE, ex_in_domain RS exE, allE] 1));
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   417
by (eresolve_tac [export lemma4 RSN (2, impE)] 1
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   418
        THEN REPEAT (assume_tac 1));
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   419
by (etac bexE 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   420
by (dresolve_tac [export simplify_recursion] 1
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   421
        THEN REPEAT (assume_tac 1));
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   422
by (res_inst_tac [("x","lam n:nat. f`n`n")] bexI 1);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   423
by (rtac lam_type 2);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   424
by (eresolve_tac [[export lemma2 RS conjunct1, succI1] MRS apply_type] 2
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   425
        THEN REPEAT (assume_tac 2));
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   426
by (rtac ballI 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   427
by (forward_tac [export (nat_succI RSN (5,lemma2)) RS conjunct2] 1
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   428
        THEN REPEAT (assume_tac 1));
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   429
by (dresolve_tac [export lemma3] 1 THEN REPEAT (assume_tac 1));
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   430
by (asm_full_simp_tac (simpset() addsimps [nat_succI]) 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   431
qed "DC_nat_imp_DC0";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   432
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   433
(* ********************************************************************** *)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   434
(* ALL K. Card(K) --> DC(K) ==> WO3                                       *)
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   435
(* ********************************************************************** *)
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   436
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4723
diff changeset
   437
Goalw [lesspoll_def]
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   438
        "[| ~ A lesspoll B; C lesspoll B |] ==> A - C ~= 0";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   439
by (fast_tac (claset() addSDs [Diff_eq_0_iff RS iffD1 RS subset_imp_lepoll]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   440
        addSIs [eqpollI] addEs [notE] addSEs [eqpollE, lepoll_trans]) 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   441
qed "lesspoll_lemma";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   442
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   443
val [f_type, Ord_a, not_eq] = goalw thy [inj_def]
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   444
        "[| f:a->X; Ord(a); (!!b c. [| b<c; c:a |] ==> f`b~=f`c) |]   \
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   445
\        ==> f:inj(a, X)";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   446
by (resolve_tac [f_type RS CollectI] 1);
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   447
by (REPEAT (resolve_tac [ballI,impI] 1));
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   448
by (resolve_tac [Ord_a RS Ord_in_Ord RS Ord_linear_lt] 1
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   449
        THEN (assume_tac 1));
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   450
by (eres_inst_tac [("j","x")] (Ord_a RS Ord_in_Ord) 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   451
by (REPEAT (fast_tac (claset() addDs [not_eq, not_eq RS not_sym]) 1));
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2496
diff changeset
   452
qed "fun_Ord_inj";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   453
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5068
diff changeset
   454
Goal "[| f:X->Y; A<=X; a:A |] ==> f`a : f``A";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   455
by (fast_tac (claset() addSEs [image_fun RS ssubst]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2496
diff changeset
   456
qed "value_in_image";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   457
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   458
Goalw [DC_def, WO3_def] "ALL K. Card(K) --> DC(K) ==> WO3";
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   459
by (rtac allI 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   460
by (excluded_middle_tac "A lesspoll Hartog(A)" 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   461
by (fast_tac (claset() addSDs [lesspoll_imp_ex_lt_eqpoll]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   462
        addSIs [Ord_Hartog, leI RS le_imp_subset]) 2);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   463
by (REPEAT (eresolve_tac [allE, impE] 1));
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   464
by (rtac Card_Hartog 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   465
by (eres_inst_tac [("x","A")] allE 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   466
by (eres_inst_tac [("x","{<z1,z2>:Pow(A)*A . z1  \
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   467
\               lesspoll Hartog(A) & z2 ~: z1}")] allE 1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   468
by (Asm_full_simp_tac 1);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   469
by (etac impE 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   470
by (fast_tac (claset() addEs [lesspoll_lemma RS not_emptyE]) 1);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   471
by (etac bexE 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   472
by (resolve_tac [exI RS (lepoll_def RS (def_imp_iff RS iffD2))
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   473
        RS (HartogI RS notE)] 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   474
by (resolve_tac [Ord_Hartog RSN (2, fun_Ord_inj)] 1 THEN (assume_tac 1));
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   475
by (dresolve_tac [Ord_Hartog RSN (2, OrdmemD) RSN (2,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   476
        ltD RSN (3, value_in_image))] 1 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   477
        THEN REPEAT (assume_tac 1));
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   478
by (force_tac (claset() addSDs [Ord_Hartog RSN (2, ltI) RSN (2, ospec)], 
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   479
	       simpset()) 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   480
qed "DC_WO3";
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   481
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   482
(* ********************************************************************** *)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   483
(* WO1 ==> ALL K. Card(K) --> DC(K)                                       *)
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   484
(* ********************************************************************** *)
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   485
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5265
diff changeset
   486
Goal "[| Ord(a); b:a |] ==> (lam x:a. P(x))``b = (lam x:b. P(x))``b";
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   487
by (rtac images_eq 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   488
by (REPEAT (fast_tac (claset() addSEs [RepFunI, OrdmemD]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   489
        addSIs [lam_type]) 2));
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   490
by (rtac ballI 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   491
by (dresolve_tac [OrdmemD RS subsetD] 1
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   492
        THEN REPEAT (assume_tac 1));
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   493
by (Asm_full_simp_tac 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2496
diff changeset
   494
qed "lam_images_eq";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   495
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5068
diff changeset
   496
Goalw [lesspoll_def] "[| Card(K); b:K |] ==> b lesspoll K";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   497
by (asm_full_simp_tac (simpset() addsimps [Card_iff_initial]) 1);
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   498
by (fast_tac (claset() addSIs [le_imp_lepoll, ltI, leI]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2496
diff changeset
   499
qed "in_Card_imp_lesspoll";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   500
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4723
diff changeset
   501
Goal "(lam b:a. P(b)) : a -> {P(b). b:a}";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   502
by (fast_tac (claset() addSIs [lam_type, RepFunI]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2496
diff changeset
   503
qed "lam_type_RepFun";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   504
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   505
Goal "[| ALL Y:Pow(X). Y lesspoll K --> (EX x:X. <Y, x> : R);  \
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   506
\        b:K; Z:Pow(X); Z lesspoll K |]  \
5241
e5129172cb2b Renamed equals0D to equals0E; tidied
paulson
parents: 5147
diff changeset
   507
\     ==> {x:X. <Z,x> : R} ~= 0";
5265
9d1d4c43c76d Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents: 5241
diff changeset
   508
by (Blast_tac 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   509
qed "lemmaX";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   510
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5068
diff changeset
   511
Goal "[| Card(K); well_ord(X,Q);  \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   512
\       ALL Y:Pow(X). Y lesspoll K --> (EX x:X. <Y, x> : R); b:K |]  \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   513
\       ==> ff(b, X, Q, R) : {x:X. <(lam c:b. ff(c, X, Q, R))``b, x> : R}";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   514
by (res_inst_tac [("P","b:K")] impE 1 THEN TRYALL assume_tac);
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   515
by (res_inst_tac [("i","b")] (Card_is_Ord RS Ord_in_Ord RS trans_induct) 1
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   516
        THEN REPEAT (assume_tac 1));
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   517
by (rtac impI 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   518
by (resolve_tac [ff_def RS def_transrec RS ssubst] 1);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   519
by (etac the_first_in 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1932
diff changeset
   520
by (Fast_tac 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   521
by (asm_full_simp_tac (simpset()
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   522
        addsimps [[lam_type_RepFun, subset_refl] MRS image_fun]) 1);
5241
e5129172cb2b Renamed equals0D to equals0E; tidied
paulson
parents: 5147
diff changeset
   523
by (etac lemmaX 1 THEN assume_tac 1);
e5129172cb2b Renamed equals0D to equals0E; tidied
paulson
parents: 5147
diff changeset
   524
by (blast_tac (claset() addIs [Card_is_Ord RSN (2, OrdmemD) RS subsetD]) 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   525
by (fast_tac (claset() addSEs [[in_Card_imp_lesspoll, RepFun_lepoll]
5241
e5129172cb2b Renamed equals0D to equals0E; tidied
paulson
parents: 5147
diff changeset
   526
			       MRS lepoll_lesspoll_lesspoll]) 1);
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   527
qed "lemma";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   528
5482
73dc3b2a7102 tidied using locales
paulson
parents: 5268
diff changeset
   529
Goalw [DC_def, WO1_def] "WO1 ==> ALL K. Card(K) --> DC(K)";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   530
by (REPEAT (resolve_tac [allI,impI] 1));
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   531
by (REPEAT (eresolve_tac [allE,exE,conjE] 1));
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   532
by (res_inst_tac [("x","lam b:K. ff(b, X, Ra, R)")] bexI 1);
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   533
by (rtac lam_type 2);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents:
diff changeset
   534
by (resolve_tac [lemma RS CollectD1] 2 THEN REPEAT (assume_tac 2));
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   535
by (asm_full_simp_tac (simpset()
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   536
        addsimps [[Card_is_Ord, ltD] MRS lam_images_eq]) 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3862
diff changeset
   537
by (fast_tac (claset() addSEs [ltE, lemma RS CollectD2]) 1);
4723
9e2609b1bfb1 Adapted proofs because of new simplification tactics.
nipkow
parents: 4091
diff changeset
   538
qed "WO1_DC_Card";