src/ZF/upair.ML
author wenzelm
Wed, 05 Dec 2001 03:07:44 +0100
changeset 12372 cd3a09c7dac9
parent 11589 9a6d4511bb3c
permissions -rw-r--r--
tuned declarations;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1017
diff changeset
     1
(*  Title:      ZF/upair
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1017
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
UNORDERED pairs in Zermelo-Fraenkel Set Theory 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
Observe the order of dependence:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
    Upair is defined in terms of Replace
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
    Un is defined in terms of Upair and Union (similarly for Int)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
    cons is defined in terms of Upair and Un
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
    Ordered pairs and descriptions are defined using cons ("set notation")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
(*** Lemmas about power sets  ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
9907
473a6604da94 tuned ML code (the_context, bind_thms(s));
wenzelm
parents: 9570
diff changeset
    17
bind_thm ("Pow_bottom", empty_subsetI RS PowI);         (* 0 : Pow(B) *)
473a6604da94 tuned ML code (the_context, bind_thms(s));
wenzelm
parents: 9570
diff changeset
    18
bind_thm ("Pow_top", subset_refl RS PowI);              (* A : Pow(A) *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
(*** Unordered pairs - Upair ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    23
Goalw [Upair_def] "c : Upair(a,b) <-> (c=a | c=b)";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    24
by (Blast_tac 1) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    25
qed "Upair_iff";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
    26
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
    27
Addsimps [Upair_iff];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    29
Goal "a : Upair(a,b)";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    30
by (Simp_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    31
qed "UpairI1";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    33
Goal "b : Upair(a,b)";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    34
by (Simp_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    35
qed "UpairI2";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    36
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    37
val major::prems= Goal
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    38
    "[| a : Upair(b,c);  a=b ==> P;  a=c ==> P |] ==> P";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    39
by (rtac (major RS (Upair_iff RS iffD1 RS disjE)) 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    40
by (REPEAT (eresolve_tac prems 1)) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    41
qed "UpairE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
    43
AddSIs [UpairI1,UpairI2];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
    44
AddSEs [UpairE];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
    45
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
(*** Rules for binary union -- Un -- defined via Upair ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    48
Goalw [Un_def]  "c : A Un B <-> (c:A | c:B)";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    49
by (Blast_tac 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    50
qed "Un_iff";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
    51
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
    52
Addsimps [Un_iff];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    54
Goal "c : A ==> c : A Un B";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    55
by (Asm_simp_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    56
qed "UnI1";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
    57
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    58
Goal "c : B ==> c : A Un B";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    59
by (Asm_simp_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    60
qed "UnI2";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    61
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    62
val major::prems= Goal 
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    63
    "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    64
by (rtac (major RS (Un_iff RS iffD1 RS disjE)) 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    65
by (REPEAT (eresolve_tac prems 1)) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    66
qed "UnE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
572
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
    68
(*Stronger version of the rule above*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    69
val major::prems = Goal
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    70
    "[| c : A Un B;  c:A ==> P;  [| c:B;  c~:A |] ==> P |] ==> P";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    71
by (rtac (major RS UnE) 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    72
by (eresolve_tac prems 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    73
by (rtac classical 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    74
by (eresolve_tac prems 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    75
by (swap_res_tac prems 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    76
by (etac notnotD 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    77
qed "UnE'";
572
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
    78
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
    79
(*Classical introduction rule: no commitment to A vs B*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    80
val prems = Goal "(c ~: B ==> c : A) ==> c : A Un B";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    81
by (Simp_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    82
by (blast_tac (claset() addSIs prems) 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    83
qed "UnCI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
    85
AddSIs [UnCI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
    86
AddSEs [UnE];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
(*** Rules for small intersection -- Int -- defined via Upair ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    91
Goalw [Int_def]  "c : A Int B <-> (c:A & c:B)";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    92
by (Blast_tac 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    93
qed "Int_iff";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
    94
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
    95
Addsimps [Int_iff];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
    96
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    97
Goal "[| c : A;  c : B |] ==> c : A Int B";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    98
by (Asm_simp_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    99
qed "IntI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   101
Goal "c : A Int B ==> c : A";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   102
by (Asm_full_simp_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   103
qed "IntD1";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   105
Goal "c : A Int B ==> c : B";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   106
by (Asm_full_simp_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   107
qed "IntD2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   109
val prems = Goal "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   110
by (resolve_tac prems 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   111
by (REPEAT (resolve_tac (prems RL [IntD1,IntD2]) 1)) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   112
qed "IntE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   114
AddSIs [IntI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   115
AddSEs [IntE];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
(*** Rules for set difference -- defined via Upair ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   119
Goalw [Diff_def]  "c : A-B <-> (c:A & c~:B)";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   120
by (Blast_tac 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   121
qed "Diff_iff";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   122
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   123
Addsimps [Diff_iff];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   124
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   125
Goal "[| c : A;  c ~: B |] ==> c : A - B";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   126
by (Asm_simp_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   127
qed "DiffI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   129
Goal "c : A - B ==> c : A";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   130
by (Asm_full_simp_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   131
qed "DiffD1";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   133
Goal "c : A - B ==> c ~: B";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   134
by (Asm_full_simp_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   135
qed "DiffD2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   137
val prems = Goal "[| c : A - B;  [| c:A; c~:B |] ==> P |] ==> P";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   138
by (resolve_tac prems 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   139
by (REPEAT (ares_tac (prems RL [DiffD1, DiffD2]) 1)) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   140
qed "DiffE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   142
AddSIs [DiffI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   143
AddSEs [DiffE];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
(*** Rules for cons -- defined via Un and Upair ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   147
Goalw [cons_def]  "a : cons(b,A) <-> (a=b | a:A)";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   148
by (Blast_tac 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   149
qed "cons_iff";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   150
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   151
Addsimps [cons_iff];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   153
Goal "a : cons(a,B)";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   154
by (Simp_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   155
qed "consI1";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   156
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   157
Addsimps [consI1];
6153
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6068
diff changeset
   158
AddTCs   [consI1];   (*risky as a typechecking rule, but solves otherwise
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6068
diff changeset
   159
		       unconstrained goals of the form  x : ?A*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   161
Goal "a : B ==> a : cons(b,B)";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   162
by (Asm_simp_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   163
qed "consI2";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   164
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   165
val major::prems= Goal
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   166
    "[| a : cons(b,A);  a=b ==> P;  a:A ==> P |] ==> P";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   167
by (rtac (major RS (cons_iff RS iffD1 RS disjE)) 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   168
by (REPEAT (eresolve_tac (prems @ [UpairE]) 1)) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   169
qed "consE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
572
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
   171
(*Stronger version of the rule above*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   172
val major::prems = Goal
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   173
    "[| a : cons(b,A);  a=b ==> P;  [| a:A;  a~=b |] ==> P |] ==> P";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   174
by (rtac (major RS consE) 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   175
by (eresolve_tac prems 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   176
by (rtac classical 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   177
by (eresolve_tac prems 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   178
by (swap_res_tac prems 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   179
by (etac notnotD 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   180
qed "consE'";
572
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
   181
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   182
(*Classical introduction rule*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   183
val prems = Goal "(a~:B ==> a=b) ==> a: cons(b,B)";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   184
by (Simp_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   185
by (blast_tac (claset() addSIs prems) 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   186
qed "consCI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   188
AddSIs [consCI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   189
AddSEs [consE];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   191
Goal "cons(a,B) ~= 0";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   192
by (blast_tac (claset() addEs [equalityE]) 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   193
qed "cons_not_0";
1609
5324067d993f New lemmas for Mutilated Checkerboard
paulson
parents: 1461
diff changeset
   194
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   195
bind_thm ("cons_neq_0", cons_not_0 RS notE);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   196
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   197
Addsimps [cons_not_0, cons_not_0 RS not_sym];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   198
1609
5324067d993f New lemmas for Mutilated Checkerboard
paulson
parents: 1461
diff changeset
   199
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
(*** Singletons - using cons ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   202
Goal "a : {b} <-> a=b";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   203
by (Simp_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   204
qed "singleton_iff";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   205
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   206
Goal "a : {a}";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   207
by (rtac consI1 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   208
qed "singletonI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   210
bind_thm ("singletonE", make_elim (singleton_iff RS iffD1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   212
AddSIs [singletonI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   213
AddSEs [singletonE];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
(*** Rules for Descriptions ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   217
val [pa,eq] = Goalw [the_def] 
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   218
    "[| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   219
by (fast_tac (claset() addSIs [pa] addEs [eq RS subst]) 1) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   220
qed "the_equality";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
5506
e07254044384 stronger version of theI2
paulson
parents: 5488
diff changeset
   222
AddIs [the_equality];
e07254044384 stronger version of theI2
paulson
parents: 5488
diff changeset
   223
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
(* Only use this if you already know EX!x. P(x) *)
8127
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   225
Goal "[| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a";
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   226
by (Blast_tac 1);
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   227
qed "the_equality2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
8127
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   229
Goal "EX! x. P(x) ==> P(THE x. P(x))";
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   230
by (etac ex1E 1);
8183
344888de76c4 expandshort
paulson
parents: 8127
diff changeset
   231
by (stac the_equality 1);
8127
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   232
by (REPEAT (Blast_tac 1));
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   233
qed "theI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   235
(*the_cong is no longer necessary: if (ALL y.P(y)<->Q(y)) then 
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   236
  (THE x.P(x))  rewrites to  (THE x. Q(x))  *)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   237
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   238
(*If it's "undefined", it's zero!*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   239
Goalw  [the_def] "~ (EX! x. P(x)) ==> (THE x. P(x))=0";
8127
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   240
by (blast_tac (claset() addSEs [ReplaceE]) 1);
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6163
diff changeset
   241
qed "the_0";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
5506
e07254044384 stronger version of theI2
paulson
parents: 5488
diff changeset
   243
(*Easier to apply than theI: conclusion has only one occurrence of P*)
e07254044384 stronger version of theI2
paulson
parents: 5488
diff changeset
   244
val prems = 
e07254044384 stronger version of theI2
paulson
parents: 5488
diff changeset
   245
Goal "[| ~ Q(0) ==> EX! x. P(x);  !!x. P(x) ==> Q(x) |] ==> Q(THE x. P(x))";
e07254044384 stronger version of theI2
paulson
parents: 5488
diff changeset
   246
by (rtac classical 1);
e07254044384 stronger version of theI2
paulson
parents: 5488
diff changeset
   247
by (resolve_tac prems 1);
e07254044384 stronger version of theI2
paulson
parents: 5488
diff changeset
   248
by (rtac theI 1);
e07254044384 stronger version of theI2
paulson
parents: 5488
diff changeset
   249
by (rtac classical 1);
e07254044384 stronger version of theI2
paulson
parents: 5488
diff changeset
   250
by (resolve_tac prems 1);
6163
be8234f37e48 expandshort
paulson
parents: 6153
diff changeset
   251
by (etac (the_0 RS subst) 1);
be8234f37e48 expandshort
paulson
parents: 6153
diff changeset
   252
by (assume_tac 1);
5506
e07254044384 stronger version of theI2
paulson
parents: 5488
diff changeset
   253
qed "theI2";
e07254044384 stronger version of theI2
paulson
parents: 5488
diff changeset
   254
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
(*** if -- a conditional expression for formulae ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
6068
2d8f3e1f1151 if-then-else syntax for ZF
paulson
parents: 5506
diff changeset
   257
Goalw [if_def] "(if True then a else b) = a";
5506
e07254044384 stronger version of theI2
paulson
parents: 5488
diff changeset
   258
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   259
qed "if_true";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
6068
2d8f3e1f1151 if-then-else syntax for ZF
paulson
parents: 5506
diff changeset
   261
Goalw [if_def] "(if False then a else b) = b";
5506
e07254044384 stronger version of theI2
paulson
parents: 5488
diff changeset
   262
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   263
qed "if_false";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   265
(*Never use with case splitting, or if P is known to be true or false*)
5325
f7a5e06adea1 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents: 5242
diff changeset
   266
val prems = Goalw [if_def]
6068
2d8f3e1f1151 if-then-else syntax for ZF
paulson
parents: 5506
diff changeset
   267
    "[| P<->Q;  Q ==> a=c;  ~Q ==> b=d |] \
2d8f3e1f1151 if-then-else syntax for ZF
paulson
parents: 5506
diff changeset
   268
\    ==> (if P then a else b) = (if Q then c else d)";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3914
diff changeset
   269
by (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   270
qed "if_cong";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
9570
e16e168984e1 installation of cancellation simprocs for the integers
paulson
parents: 9211
diff changeset
   272
(*Prevents simplification of x and y: faster and allows the execution
e16e168984e1 installation of cancellation simprocs for the integers
paulson
parents: 9211
diff changeset
   273
  of functional programs. NOW THE DEFAULT.*)
e16e168984e1 installation of cancellation simprocs for the integers
paulson
parents: 9211
diff changeset
   274
Goal "P<->Q ==> (if P then x else y) = (if Q then x else y)";
e16e168984e1 installation of cancellation simprocs for the integers
paulson
parents: 9211
diff changeset
   275
by (Asm_simp_tac 1);
e16e168984e1 installation of cancellation simprocs for the integers
paulson
parents: 9211
diff changeset
   276
qed "if_weak_cong";
e16e168984e1 installation of cancellation simprocs for the integers
paulson
parents: 9211
diff changeset
   277
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
(*Not needed for rewriting, since P would rewrite to True anyway*)
6068
2d8f3e1f1151 if-then-else syntax for ZF
paulson
parents: 5506
diff changeset
   279
Goalw [if_def] "P ==> (if P then a else b) = a";
5506
e07254044384 stronger version of theI2
paulson
parents: 5488
diff changeset
   280
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   281
qed "if_P";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
(*Not needed for rewriting, since P would rewrite to False anyway*)
6068
2d8f3e1f1151 if-then-else syntax for ZF
paulson
parents: 5506
diff changeset
   284
Goalw [if_def] "~P ==> (if P then a else b) = b";
5506
e07254044384 stronger version of theI2
paulson
parents: 5488
diff changeset
   285
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   286
qed "if_not_P";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   288
Addsimps [if_true, if_false];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   289
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   290
Goal "P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   291
by (case_tac "Q" 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   292
by (Asm_simp_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   293
by (Asm_simp_tac 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   294
qed "split_if";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
3914
9e393b363c71 New rewrite rules for simplifying conditionals
paulson
parents: 3840
diff changeset
   296
(** Rewrite rules for boolean case-splitting: faster than 
5116
8eb343ab5748 Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents: 4091
diff changeset
   297
	addsplits[split_if]
3914
9e393b363c71 New rewrite rules for simplifying conditionals
paulson
parents: 3840
diff changeset
   298
**)
9e393b363c71 New rewrite rules for simplifying conditionals
paulson
parents: 3840
diff changeset
   299
8551
5c22595bc599 tidied using new "inst" rule
paulson
parents: 8183
diff changeset
   300
bind_thm ("split_if_eq1", inst "P" "%x. x = ?b" split_if);
5c22595bc599 tidied using new "inst" rule
paulson
parents: 8183
diff changeset
   301
bind_thm ("split_if_eq2", inst "P" "%x. ?a = x" split_if);
3914
9e393b363c71 New rewrite rules for simplifying conditionals
paulson
parents: 3840
diff changeset
   302
8551
5c22595bc599 tidied using new "inst" rule
paulson
parents: 8183
diff changeset
   303
bind_thm ("split_if_mem1", inst "P" "%x. x : ?b" split_if);
5c22595bc599 tidied using new "inst" rule
paulson
parents: 8183
diff changeset
   304
bind_thm ("split_if_mem2", inst "P" "%x. ?a : x" split_if);
3914
9e393b363c71 New rewrite rules for simplifying conditionals
paulson
parents: 3840
diff changeset
   305
9907
473a6604da94 tuned ML code (the_context, bind_thms(s));
wenzelm
parents: 9570
diff changeset
   306
bind_thms ("split_ifs", [split_if_eq1, split_if_eq2, split_if_mem1, split_if_mem2]);
3914
9e393b363c71 New rewrite rules for simplifying conditionals
paulson
parents: 3840
diff changeset
   307
5116
8eb343ab5748 Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents: 4091
diff changeset
   308
(*Logically equivalent to split_if_mem2*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   309
Goal "a: (if P then x else y) <-> P & a:x | ~P & a:y";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   310
by (simp_tac (simpset() addsplits [split_if]) 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   311
qed "if_iff";
1017
6a402dc505cf Proved if_iff and used it to simplify proof of if_type.
lcp
parents: 985
diff changeset
   312
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   313
val prems = Goal
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   314
    "[| P ==> a: A;  ~P ==> b: A |] ==> (if P then a else b): A";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   315
by (simp_tac (simpset() addsimps prems addsplits [split_if]) 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   316
qed "if_type";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   317
6153
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 6068
diff changeset
   318
AddTCs [if_type];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   319
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   320
(*** Foundation lemmas ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   322
(*was called mem_anti_sym*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   323
val prems = Goal "[| a:b;  ~P ==> b:a |] ==> P";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   324
by (rtac classical 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   325
by (res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   326
by (REPEAT (blast_tac (claset() addIs prems addSEs [equalityE]) 1));
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   327
qed "mem_asym";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   329
(*was called mem_anti_refl*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   330
Goal "a:a ==> P";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   331
by (blast_tac (claset() addIs [mem_asym]) 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   332
qed "mem_irrefl";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   333
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   334
(*mem_irrefl should NOT be added to default databases:
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   335
      it would be tried on most goals, making proofs slower!*)
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   336
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   337
Goal "a ~: a";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   338
by (rtac notI 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   339
by (etac mem_irrefl 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   340
qed "mem_not_refl";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   341
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   342
(*Good for proving inequalities by rewriting*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   343
Goal "a:A ==> a ~= A";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   344
by (blast_tac (claset() addSEs [mem_irrefl]) 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   345
qed "mem_imp_not_eq";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   346
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   347
(*** Rules for succ ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   348
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   349
Goalw [succ_def]  "i : succ(j) <-> i=j | i:j";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   350
by (Blast_tac 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   351
qed "succ_iff";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   352
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   353
Goalw [succ_def]  "i : succ(i)";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   354
by (rtac consI1 1) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   355
qed "succI1";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   356
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   357
Addsimps [succI1];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   358
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   359
Goalw [succ_def] "i : j ==> i : succ(j)";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   360
by (etac consI2 1) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   361
qed "succI2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   362
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   363
val major::prems= Goalw [succ_def] 
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   364
    "[| i : succ(j);  i=j ==> P;  i:j ==> P |] ==> P";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   365
by (rtac (major RS consE) 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   366
by (REPEAT (eresolve_tac prems 1)) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   367
qed "succE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   368
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   369
(*Classical introduction rule*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   370
val [prem]= Goal "(i~:j ==> i=j) ==> i: succ(j)";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   371
by (rtac (disjCI RS (succ_iff RS iffD2)) 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   372
by (etac prem 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   373
qed "succCI";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   374
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   375
AddSIs [succCI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   376
AddSEs [succE];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   377
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   378
Goal "succ(n) ~= 0";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   379
by (blast_tac (claset() addSEs [equalityE]) 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   380
qed "succ_not_0";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   381
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   382
bind_thm ("succ_neq_0", succ_not_0 RS notE);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   383
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   384
Addsimps [succ_not_0, succ_not_0 RS not_sym];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   385
AddSEs [succ_neq_0, sym RS succ_neq_0];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   386
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   387
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   388
(* succ(c) <= B ==> c : B *)
9907
473a6604da94 tuned ML code (the_context, bind_thms(s));
wenzelm
parents: 9570
diff changeset
   389
bind_thm ("succ_subsetD", succI1 RSN (2,subsetD));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   390
1609
5324067d993f New lemmas for Mutilated Checkerboard
paulson
parents: 1461
diff changeset
   391
(* succ(b) ~= b *)
5324067d993f New lemmas for Mutilated Checkerboard
paulson
parents: 1461
diff changeset
   392
bind_thm ("succ_neq_self", succI1 RS mem_imp_not_eq RS not_sym);
5324067d993f New lemmas for Mutilated Checkerboard
paulson
parents: 1461
diff changeset
   393
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   394
Goal "succ(m) = succ(n) <-> m=n";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   395
by (blast_tac (claset() addEs [mem_asym] addSEs [equalityE]) 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   396
qed "succ_inject_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   397
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   398
bind_thm ("succ_inject", succ_inject_iff RS iffD1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   399
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   400
Addsimps [succ_inject_iff];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1609
diff changeset
   401
AddSDs [succ_inject];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   402
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2690
diff changeset
   403
(*Not needed now that cons is available.  Deletion reduces the search space.*)
6476784dba1c Converted to call blast_tac.
paulson
parents: 2690
diff changeset
   404
Delrules [UpairI1,UpairI2,UpairE];