src/ZF/AC/AC_Equiv.ML
author paulson
Thu, 10 Sep 1998 17:42:44 +0200
changeset 5470 855654b691db
parent 5325 f7a5e06adea1
child 5505 b0856ff6fc69
permissions -rw-r--r--
eliminated equals0E
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
     1
(*  Title:      ZF/AC/AC_Equiv.ML
991
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
     3
    Author:     Krzysztof Grabczewski
991
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
     4
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
     5
*)
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
     6
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
     7
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
     8
open AC_Equiv;
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
     9
1071
96dfc9977bf5 Simple updates for compatibility with KG
lcp
parents: 1057
diff changeset
    10
val WO_defs = [WO1_def, WO2_def, WO3_def, WO4_def, WO5_def, WO6_def, WO8_def];
96dfc9977bf5 Simple updates for compatibility with KG
lcp
parents: 1057
diff changeset
    11
 
96dfc9977bf5 Simple updates for compatibility with KG
lcp
parents: 1057
diff changeset
    12
val AC_defs = [AC0_def, AC1_def, AC2_def, AC3_def, AC4_def, AC5_def, 
96dfc9977bf5 Simple updates for compatibility with KG
lcp
parents: 1057
diff changeset
    13
               AC6_def, AC7_def, AC8_def, AC9_def, AC10_def, AC11_def, 
96dfc9977bf5 Simple updates for compatibility with KG
lcp
parents: 1057
diff changeset
    14
               AC12_def, AC13_def, AC14_def, AC15_def, AC16_def, 
96dfc9977bf5 Simple updates for compatibility with KG
lcp
parents: 1057
diff changeset
    15
               AC17_def, AC18_def, AC19_def];
96dfc9977bf5 Simple updates for compatibility with KG
lcp
parents: 1057
diff changeset
    16
 
991
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    17
val AC_aux_defs = [pairwise_disjoint_def, sets_of_size_between_def];
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents: 1071
diff changeset
    18
 
991
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    19
(* ******************************************** *)
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    20
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    21
(* Theorems analogous to ones presented in "ZF/Ordinal.ML" *)
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    22
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    23
(* lemma for nat_le_imp_lepoll *)
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    24
val [prem] = goalw Cardinal.thy [lepoll_def]
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    25
             "m:nat ==> ALL n: nat. m le n --> m lepoll n";
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    26
by (nat_ind_tac "m" [prem] 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3731
diff changeset
    27
by (fast_tac (claset() addSIs [le_imp_subset RS id_subset_inj]) 1);
991
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    28
by (rtac ballI 1);
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    29
by (eres_inst_tac [("n","n")] natE 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3731
diff changeset
    30
by (asm_simp_tac (simpset() addsimps [inj_def, succI1 RS Pi_empty2]) 1);
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3731
diff changeset
    31
by (fast_tac (claset() addSIs [le_imp_subset RS id_subset_inj]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2873
diff changeset
    32
qed "nat_le_imp_lepoll_lemma";
991
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    33
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    34
(* used in : AC10-AC15.ML WO1-WO6.ML WO6WO1.ML*)
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    35
val nat_le_imp_lepoll = nat_le_imp_lepoll_lemma RS bspec RS mp |> standard;
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    36
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    37
(* ********************************************************************** *)
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    38
(*             lemmas concerning FOL and pure ZF theory                   *)
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    39
(* ********************************************************************** *)
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    40
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5068
diff changeset
    41
Goal "(A->X)=0 ==> X=0";
5470
855654b691db eliminated equals0E
paulson
parents: 5325
diff changeset
    42
by (fast_tac (claset() addSIs [equals0I] addIs [lam_type]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2873
diff changeset
    43
qed "fun_space_emptyD";
991
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    44
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    45
(* used only in WO1_DC.ML *)
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    46
(*Note simpler proof*)
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5265
diff changeset
    47
Goal "[| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg; A<=Df; A<=Dg |] ==> f``A=g``A";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3731
diff changeset
    48
by (asm_simp_tac (simpset() addsimps [image_fun]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2873
diff changeset
    49
qed "images_eq";
991
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    50
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    51
(* used in : AC10-AC15.ML AC16WO4.ML WO6WO1.ML *)
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    52
(*I don't know where to put this one.*)
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    53
goal Cardinal.thy
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    54
     "!!m A B. [| A lepoll succ(m); B<=A; B~=0 |] ==> A-B lepoll m";
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
    55
by (rtac not_emptyE 1 THEN (assume_tac 1));
991
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    56
by (forward_tac [singleton_subsetI] 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
    57
by (forward_tac [subsetD] 1 THEN (assume_tac 1));
991
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    58
by (res_inst_tac [("A2","A")] 
1057
5097aa914449 Renamed diff_sing_lepoll to Diff_sing_lepoll.
lcp
parents: 1037
diff changeset
    59
     (Diff_sing_lepoll RSN (2, subset_imp_lepoll RS lepoll_trans)) 1 
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
    60
    THEN (REPEAT (assume_tac 2)));
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1615
diff changeset
    61
by (Fast_tac 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2873
diff changeset
    62
qed "Diff_lepoll";
991
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    63
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    64
(* ********************************************************************** *)
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    65
(*              lemmas concerning lepoll and eqpoll relations             *)
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    66
(* ********************************************************************** *)
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    67
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    68
(* ********************************************************************** *)
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    69
(*                    Theorems concerning ordinals                        *)
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    70
(* ********************************************************************** *)
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    71
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    72
(* lemma for ordertype_Int *)
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    73
goalw Cardinal.thy [rvimage_def] "rvimage(A,id(A),r) = r Int A*A";
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
    74
by (rtac equalityI 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2873
diff changeset
    75
by Safe_tac;
991
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    76
by (dres_inst_tac [("P","%a. <id(A)`xb,a>:r")] (id_conv RS subst) 1
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
    77
    THEN (assume_tac 1));
991
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    78
by (dres_inst_tac [("P","%a. <a,ya>:r")] (id_conv RS subst) 1
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
    79
    THEN (REPEAT (assume_tac 1)));
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3731
diff changeset
    80
by (fast_tac (claset() addIs [id_conv RS ssubst]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2873
diff changeset
    81
qed "rvimage_id";
991
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    82
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    83
(* used only in Hartog.ML *)
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    84
goal Cardinal.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    85
        "!!A r. well_ord(A,r) ==> ordertype(A, r Int A*A) = ordertype(A,r)";
991
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    86
by (res_inst_tac [("P","%a. ordertype(A,a)=ordertype(A,r)")] 
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    87
    (rvimage_id RS subst) 1);
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    88
by (eresolve_tac [id_bij RS bij_ordertype_vimage] 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2873
diff changeset
    89
qed "ordertype_Int";
991
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    90
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    91
(* used only in AC16_lemmas.ML *)
547931cbbf08 New example of AC Equivalences by Krzysztof Grabczewski
lcp
parents:
diff changeset
    92
goalw CardinalArith.thy [InfCard_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    93
        "!!i. [| ~Finite(i); Card(i) |] ==> InfCard(i)";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3731
diff changeset
    94
by (asm_simp_tac (simpset() addsimps [Card_is_Ord RS nat_le_infinite_Ord]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2873
diff changeset
    95
qed "Inf_Card_is_InfCard";
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents: 1071
diff changeset
    96
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
    97
Goal "(THE z. {x}={z}) = x";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3731
diff changeset
    98
by (fast_tac (claset() addSIs [the_equality]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
    99
                addSEs [singleton_eq_iff RS iffD1 RS sym]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2873
diff changeset
   100
qed "the_element";
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents: 1071
diff changeset
   101
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
   102
Goal "(lam x:A. {x}) : bij(A, {{x}. x:A})";
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents: 1071
diff changeset
   103
by (res_inst_tac [("d","%z. THE x. z={x}")] lam_bijective 1);
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents: 1071
diff changeset
   104
by (TRYALL (eresolve_tac [RepFunI, RepFunE]));
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3731
diff changeset
   105
by (REPEAT (asm_full_simp_tac (simpset() addsimps [the_element]) 1));
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2873
diff changeset
   106
qed "lam_sing_bij";
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents: 1071
diff changeset
   107
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents: 1071
diff changeset
   108
val [major,minor] = goal thy 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   109
        "[| f : Pi(A,B); (!!x. x:A ==> B(x)<=C(x)) |] ==> f : Pi(A,C)";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3731
diff changeset
   110
by (fast_tac (claset() addSIs [major RS Pi_type, minor RS subsetD,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   111
                major RS apply_type]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2873
diff changeset
   112
qed "Pi_weaken_type";
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents: 1071
diff changeset
   113
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents: 1071
diff changeset
   114
val [major, minor] = goalw thy [inj_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   115
        "[| f:inj(A, B); (!!a. a:A ==> f`a : C) |] ==> f:inj(A,C)";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3731
diff changeset
   116
by (fast_tac (claset() addSEs [minor]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   117
        addSIs [major RS CollectD1 RS Pi_type, major RS CollectD2]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2873
diff changeset
   118
qed "inj_strengthen_type";
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents: 1071
diff changeset
   119
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5068
diff changeset
   120
Goalw [Finite_def] "n:nat ==> Finite(n)";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3731
diff changeset
   121
by (fast_tac (claset() addSIs [eqpoll_refl]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2873
diff changeset
   122
qed "nat_into_Finite";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   123
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
   124
Goalw [Finite_def] "~Finite(nat)";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3731
diff changeset
   125
by (fast_tac (claset() addSDs [eqpoll_imp_lepoll]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   126
                addIs [Ord_nat RSN (2, ltI) RS lt_not_lepoll RS notE]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2873
diff changeset
   127
qed "nat_not_Finite";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   128
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   129
val le_imp_lepoll = le_imp_subset RS subset_imp_lepoll;
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   130
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   131
(* ********************************************************************** *)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   132
(* Another elimination rule for EX!                                       *)
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   133
(* ********************************************************************** *)
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   134
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5068
diff changeset
   135
Goal "[| EX! x. P(x); P(x); P(y) |] ==> x=y";
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   136
by (etac ex1E 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   137
by (res_inst_tac [("b","xa")] (sym RSN (2, trans)) 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1615
diff changeset
   138
by (Fast_tac 1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1615
diff changeset
   139
by (Fast_tac 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2873
diff changeset
   140
qed "ex1_two_eq";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   141
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   142
(* ********************************************************************** *)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1207
diff changeset
   143
(* image of a surjection                                                  *)
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   144
(* ********************************************************************** *)
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   145
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5068
diff changeset
   146
Goalw [surj_def] "f : surj(A, B) ==> f``A = B";
1207
3f460842e919 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1200
diff changeset
   147
by (etac CollectE 1);
2496
40efb87985b5 Removal of needless "addIs [equality]", etc.
paulson
parents: 2469
diff changeset
   148
by (resolve_tac [subset_refl RSN (2, image_fun) RS ssubst] 1 
40efb87985b5 Removal of needless "addIs [equality]", etc.
paulson
parents: 2469
diff changeset
   149
    THEN (assume_tac 1));
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3731
diff changeset
   150
by (fast_tac (claset() addSEs [apply_type] addIs [equalityI]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2873
diff changeset
   151
qed "surj_image_eq";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   152
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   153
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5068
diff changeset
   154
Goal "succ(x) lepoll y ==> y ~= 0";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3731
diff changeset
   155
by (fast_tac (claset() addSDs [lepoll_0_is_0]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2873
diff changeset
   156
qed "succ_lepoll_imp_not_empty";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   157
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5068
diff changeset
   158
Goal "x eqpoll succ(n) ==> x ~= 0";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3731
diff changeset
   159
by (fast_tac (claset() addSEs [eqpoll_sym RS eqpoll_0_is_0 RS succ_neq_0]) 1);
3731
71366483323b result() -> qed; Step_tac -> Safe_tac
paulson
parents: 2873
diff changeset
   160
qed "eqpoll_succ_imp_not_empty";
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
   161