src/ZF/ZF.ML
author paulson
Fri, 03 Jan 1997 15:01:55 +0100
changeset 2469 b50b8c0eec01
parent 1902 e349b91cf197
child 2493 bdeb5024353a
permissions -rw-r--r--
Implicit simpsets and clasets for FOL and ZF
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1016
diff changeset
     1
(*  Title:      ZF/ZF.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1016
diff changeset
     3
    Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
     4
    Copyright   1994  University of Cambridge
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Basic introduction and elimination rules for Zermelo-Fraenkel Set Theory 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
open ZF;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
825
76d9575950f2 Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents: 775
diff changeset
    11
(*Useful examples:  singletonI RS subst_elem,  subst_elem RSN (2,IntI) *)
76d9575950f2 Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents: 775
diff changeset
    12
goal ZF.thy "!!a b A. [| b:A;  a=b |] ==> a:A";
76d9575950f2 Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents: 775
diff changeset
    13
by (etac ssubst 1);
76d9575950f2 Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents: 775
diff changeset
    14
by (assume_tac 1);
76d9575950f2 Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents: 775
diff changeset
    15
val subst_elem = result();
76d9575950f2 Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents: 775
diff changeset
    16
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
    17
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
(*** Bounded universal quantifier ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
    20
qed_goalw "ballI" ZF.thy [Ball_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
    "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
 (fn prems=> [ (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
    24
qed_goalw "bspec" ZF.thy [Ball_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
    "[| ALL x:A. P(x);  x: A |] ==> P(x)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
  [ (rtac (major RS spec RS mp) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
    (resolve_tac prems 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
    30
qed_goalw "ballE" ZF.thy [Ball_def]
37
cebe01deba80 added ~: for "not in"
lcp
parents: 6
diff changeset
    31
    "[| ALL x:A. P(x);  P(x) ==> Q;  x~:A ==> Q |] ==> Q"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
  [ (rtac (major RS allE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
    (REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
(*Used in the datatype package*)
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
    37
qed_goal "rev_bspec" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
    "!!x A P. [| x: A;  ALL x:A. P(x) |] ==> P(x)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
 (fn _ =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
  [ REPEAT (ares_tac [bspec] 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
(*Instantiates x first: better for automatic theorem proving?*)
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
    43
qed_goal "rev_ballE" ZF.thy
37
cebe01deba80 added ~: for "not in"
lcp
parents: 6
diff changeset
    44
    "[| ALL x:A. P(x);  x~:A ==> Q;  P(x) ==> Q |] ==> Q"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
  [ (rtac (major RS ballE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
    (REPEAT (eresolve_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
    49
AddSIs [ballI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
    50
AddEs  [rev_ballE];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
    51
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
(*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
val ball_tac = dtac bspec THEN' assume_tac;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
(*Trival rewrite rule;   (ALL x:A.P)<->P holds only if A is nonempty!*)
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
    56
qed_goal "ball_simp" ZF.thy "(ALL x:A. True) <-> True"
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
    57
 (fn _=> [ Fast_tac 1 ]);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
    58
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
    59
Addsimps [ball_simp];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
(*Congruence rule for rewriting*)
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
    62
qed_goalw "ball_cong" ZF.thy [Ball_def]
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    63
    "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> Ball(A,P) <-> Ball(A',P')"
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    64
 (fn prems=> [ (simp_tac (FOL_ss addsimps prems) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
(*** Bounded existential quantifier ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
    68
qed_goalw "bexI" ZF.thy [Bex_def]
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
    69
    "!!P. [| P(x);  x: A |] ==> EX x:A. P(x)"
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
    70
 (fn _=> [ Fast_tac 1 ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
(*Not of the general form for such rules; ~EX has become ALL~ *)
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
    73
qed_goal "bexCI" ZF.thy 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
   "[| ALL x:A. ~P(x) ==> P(a);  a: A |] ==> EX x:A.P(x)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
  [ (rtac classical 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
    (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
    79
qed_goalw "bexE" ZF.thy [Bex_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
    "[| EX x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
\    |] ==> Q"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
  [ (rtac (major RS exE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
    (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
    86
AddIs  [bexI];  
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
    87
AddSEs [bexE];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
    88
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
(*We do not even have (EX x:A. True) <-> True unless A is nonempty!!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
    91
qed_goalw "bex_cong" ZF.thy [Bex_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
    "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) \
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    93
\    |] ==> Bex(A,P) <-> Bex(A',P')"
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    94
 (fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
    96
Addcongs [ball_cong, bex_cong];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
    97
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
    98
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
(*** Rules for subsets ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   101
qed_goalw "subsetI" ZF.thy [subset_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
    "(!!x.x:A ==> x:B) ==> A <= B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
 (fn prems=> [ (REPEAT (ares_tac (prems @ [ballI]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
(*Rule in Modus Ponens style [was called subsetE] *)
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   106
qed_goalw "subsetD" ZF.thy [subset_def] "[| A <= B;  c:A |] ==> c:B"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
  [ (rtac (major RS bspec) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
    (resolve_tac prems 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
(*Classical elimination rule*)
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   112
qed_goalw "subsetCE" ZF.thy [subset_def]
37
cebe01deba80 added ~: for "not in"
lcp
parents: 6
diff changeset
   113
    "[| A <= B;  c~:A ==> P;  c:B ==> P |] ==> P"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
  [ (rtac (major RS ballE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
    (REPEAT (eresolve_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   118
AddSIs [subsetI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   119
AddEs  [subsetCE, subsetD];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   120
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   121
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
(*Takes assumptions A<=B; c:A and creates the assumption c:B *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
val set_mp_tac = dtac subsetD THEN' assume_tac;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
(*Sometimes useful with premises in this order*)
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   126
qed_goal "rev_subsetD" ZF.thy "!!A B c. [| c:A; A<=B |] ==> c:B"
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   127
 (fn _=> [ Fast_tac 1 ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
1889
661603db8ee2 Addition of contra_subsetD and rev_contra_subsetD
paulson
parents: 1461
diff changeset
   129
qed_goal "contra_subsetD" ZF.thy "!!c. [| A <= B; c ~: B |] ==> c ~: A"
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   130
 (fn _=> [ Fast_tac 1 ]);
1889
661603db8ee2 Addition of contra_subsetD and rev_contra_subsetD
paulson
parents: 1461
diff changeset
   131
661603db8ee2 Addition of contra_subsetD and rev_contra_subsetD
paulson
parents: 1461
diff changeset
   132
qed_goal "rev_contra_subsetD" ZF.thy "!!c. [| c ~: B;  A <= B |] ==> c ~: A"
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   133
 (fn _=> [ Fast_tac 1 ]);
1889
661603db8ee2 Addition of contra_subsetD and rev_contra_subsetD
paulson
parents: 1461
diff changeset
   134
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   135
qed_goal "subset_refl" ZF.thy "A <= A"
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   136
 (fn _=> [ Fast_tac 1 ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   138
Addsimps [subset_refl];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   139
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   140
qed_goal "subset_trans" ZF.thy "!!A B C. [| A<=B;  B<=C |] ==> A<=C"
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   141
 (fn _=> [ Fast_tac 1 ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   143
(*Useful for proving A<=B by rewriting in some cases*)
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   144
qed_goalw "subset_iff" ZF.thy [subset_def,Ball_def]
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   145
     "A<=B <-> (ALL x. x:A --> x:B)"
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   146
 (fn _=> [ (rtac iff_refl 1) ]);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   147
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
(*** Rules for equality ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
(*Anti-symmetry of the subset relation*)
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   152
qed_goal "equalityI" ZF.thy "[| A <= B;  B <= A |] ==> A = B"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
 (fn prems=> [ (REPEAT (resolve_tac (prems@[conjI, extension RS iffD2]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   155
qed_goal "equality_iffI" ZF.thy "(!!x. x:A <-> x:B) ==> A = B"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
 (fn [prem] =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
  [ (rtac equalityI 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
    (REPEAT (ares_tac [subsetI, prem RS iffD1, prem RS iffD2] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   160
bind_thm ("equalityD1", extension RS iffD1 RS conjunct1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   161
bind_thm ("equalityD2", extension RS iffD1 RS conjunct2);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   163
qed_goal "equalityE" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
    "[| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
  [ (DEPTH_SOLVE (resolve_tac (prems@[equalityD1,equalityD2]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   168
qed_goal "equalityCE" ZF.thy
37
cebe01deba80 added ~: for "not in"
lcp
parents: 6
diff changeset
   169
    "[| A = B;  [| c:A; c:B |] ==> P;  [| c~:A; c~:B |] ==> P |]  ==>  P"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
  [ (rtac (major RS equalityE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
    (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
(*Lemma for creating induction formulae -- for "pattern matching" on p
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
  To make the induction hypotheses usable, apply "spec" or "bspec" to
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
  put universal quantifiers over the free variables in p. 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
  Would it be better to do subgoal_tac "ALL z. p = f(z) --> R(z)" ??*)
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   178
qed_goal "setup_induction" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
    "[| p: A;  !!z. z: A ==> p=z --> R |] ==> R"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
  [ (rtac mp 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
    (REPEAT (resolve_tac (refl::prems) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
(*** Rules for Replace -- the derived form of replacement ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   187
qed_goalw "Replace_iff" ZF.thy [Replace_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
    "b : {y. x:A, P(x,y)}  <->  (EX x:A. P(x,b) & (ALL y. P(x,y) --> y=b))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
 (fn _=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
  [ (rtac (replacement RS iff_trans) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
    (REPEAT (ares_tac [refl,bex_cong,iffI,ballI,allI,conjI,impI,ex1I] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
        ORELSE eresolve_tac [conjE, spec RS mp, ex1_functional] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
(*Introduction; there must be a unique y such that P(x,y), namely y=b. *)
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   195
qed_goal "ReplaceI" ZF.thy
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   196
    "[| P(x,b);  x: A;  !!y. P(x,y) ==> y=b |] ==> \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
\    b : {y. x:A, P(x,y)}"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
  [ (rtac (Replace_iff RS iffD2) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
    (REPEAT (ares_tac (prems@[bexI,conjI,allI,impI]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *)
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   203
qed_goal "ReplaceE" ZF.thy 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
    "[| b : {y. x:A, P(x,y)};  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
\       !!x. [| x: A;  P(x,b);  ALL y. P(x,y)-->y=b |] ==> R \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
\    |] ==> R"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
  [ (rtac (Replace_iff RS iffD1 RS bexE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
    (etac conjE 2),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
    (REPEAT (ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   212
(*As above but without the (generally useless) 3rd assumption*)
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   213
qed_goal "ReplaceE2" ZF.thy 
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   214
    "[| b : {y. x:A, P(x,y)};  \
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   215
\       !!x. [| x: A;  P(x,b) |] ==> R \
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   216
\    |] ==> R"
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   217
 (fn major::prems=>
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   218
  [ (rtac (major RS ReplaceE) 1),
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   219
    (REPEAT (ares_tac prems 1)) ]);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   220
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   221
AddIs  [ReplaceI];  
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   222
AddSEs [ReplaceE2];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   223
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   224
qed_goal "Replace_cong" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
    "[| A=B;  !!x y. x:B ==> P(x,y) <-> Q(x,y) |] ==> \
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   226
\    Replace(A,P) = Replace(B,Q)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
   let val substprems = prems RL [subst, ssubst]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
       and iffprems = prems RL [iffD1,iffD2]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
   in [ (rtac equalityI 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1016
diff changeset
   231
        (REPEAT (eresolve_tac (substprems@[asm_rl, ReplaceE, spec RS mp]) 1
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1016
diff changeset
   232
         ORELSE resolve_tac [subsetI, ReplaceI] 1
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1016
diff changeset
   233
         ORELSE (resolve_tac iffprems 1 THEN assume_tac 2))) ]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
   end);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   236
Addcongs [Replace_cong];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   237
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
(*** Rules for RepFun ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   240
qed_goalw "RepFunI" ZF.thy [RepFun_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
    "!!a A. a : A ==> f(a) : {f(x). x:A}"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
 (fn _ => [ (REPEAT (ares_tac [ReplaceI,refl] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
120
09287f26bfb8 changed all co- and co_ to co
lcp
parents: 37
diff changeset
   244
(*Useful for coinduction proofs*)
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   245
qed_goal "RepFun_eqI" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
    "!!b a f. [| b=f(a);  a : A |] ==> b : {f(x). x:A}"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
 (fn _ => [ etac ssubst 1, etac RepFunI 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   249
qed_goalw "RepFunE" ZF.thy [RepFun_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
    "[| b : {f(x). x:A};  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
\       !!x.[| x:A;  b=f(x) |] ==> P |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
\    P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
  [ (rtac (major RS ReplaceE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
    (REPEAT (ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   257
AddIs  [RepFunI];  
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   258
AddSEs [RepFunE];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   259
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   260
qed_goalw "RepFun_cong" ZF.thy [RepFun_def]
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   261
    "[| A=B;  !!x. x:B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)"
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   262
 (fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   263
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   264
Addcongs [RepFun_cong];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   266
qed_goalw "RepFun_iff" ZF.thy [Bex_def]
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   267
    "b : {f(x). x:A} <-> (EX x:A. b=f(x))"
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   268
 (fn _ => [Fast_tac 1]);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   269
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   270
goal ZF.thy "{x.x:A} = A";
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   271
by (fast_tac (!claset addSIs [equalityI]) 1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   272
qed "triv_RepFun";
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   273
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   274
Addsimps [RepFun_iff, triv_RepFun];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
(*** Rules for Collect -- forming a subset by separation ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
(*Separation is derivable from Replacement*)
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   279
qed_goalw "separation" ZF.thy [Collect_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
    "a : {x:A. P(x)} <-> a:A & P(a)"
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   281
 (fn _=> [Fast_tac 1]);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   282
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   283
Addsimps [separation];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   285
qed_goal "CollectI" ZF.thy
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   286
    "!!P. [| a:A;  P(a) |] ==> a : {x:A. P(x)}"
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   287
 (fn _=> [ Asm_simp_tac 1 ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   289
qed_goal "CollectE" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
    "[| a : {x:A. P(x)};  [| a:A; P(a) |] ==> R |] ==> R"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
  [ (rtac (separation RS iffD1 RS conjE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
    (REPEAT (ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   295
qed_goal "CollectD1" ZF.thy "!!P. a : {x:A. P(x)} ==> a:A"
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   296
 (fn _=> [ (etac CollectE 1), (assume_tac 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   298
qed_goal "CollectD2" ZF.thy "!!P. a : {x:A. P(x)} ==> P(a)"
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   299
 (fn _=> [ (etac CollectE 1), (assume_tac 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   301
qed_goalw "Collect_cong" ZF.thy [Collect_def] 
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   302
    "[| A=B;  !!x. x:B ==> P(x) <-> Q(x) |] ==> Collect(A,P) = Collect(B,Q)"
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   303
 (fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   304
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   305
AddSIs [CollectI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   306
AddSEs [CollectE];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   307
Addcongs [Collect_cong];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   308
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   309
(*** Rules for Unions ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   310
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   311
Addsimps [Union_iff];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   312
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
(*The order of the premises presupposes that C is rigid; A may be flexible*)
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   314
qed_goal "UnionI" ZF.thy "!!C. [| B: C;  A: B |] ==> A: Union(C)"
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   315
 (fn _=> [ Simp_tac 1, Fast_tac 1 ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   317
qed_goal "UnionE" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318
    "[| A : Union(C);  !!B.[| A: B;  B: C |] ==> R |] ==> R"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   319
 (fn prems=>
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   320
  [ (resolve_tac [Union_iff RS iffD1 RS bexE] 1),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
    (REPEAT (ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   322
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
(*** Rules for Unions of families ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
(* UN x:A. B(x) abbreviates Union({B(x). x:A}) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   325
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   326
qed_goalw "UN_iff" ZF.thy [Bex_def]
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   327
    "b : (UN x:A. B(x)) <-> (EX x:A. b : B(x))"
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   328
 (fn _=> [ Simp_tac 1, Fast_tac 1 ]);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   329
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   330
Addsimps [UN_iff];
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   331
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
(*The order of the premises presupposes that A is rigid; b may be flexible*)
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   333
qed_goal "UN_I" ZF.thy "!!A B. [| a: A;  b: B(a) |] ==> b: (UN x:A. B(x))"
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   334
 (fn _=> [ Simp_tac 1, Fast_tac 1 ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   335
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   336
qed_goal "UN_E" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   337
    "[| b : (UN x:A. B(x));  !!x.[| x: A;  b: B(x) |] ==> R |] ==> R"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   338
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   339
  [ (rtac (major RS UnionE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   340
    (REPEAT (eresolve_tac (prems@[asm_rl, RepFunE, subst]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   341
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   342
qed_goal "UN_cong" ZF.thy
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   343
    "[| A=B;  !!x. x:B ==> C(x)=D(x) |] ==> (UN x:A.C(x)) = (UN x:B.D(x))"
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   344
 (fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   345
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   346
(*No "Addcongs [UN_cong]" because UN is a combination of constants*)
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   347
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   348
(* UN_E appears before UnionE so that it is tried first, to avoid expensive
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   349
  calls to hyp_subst_tac.  Cannot include UN_I as it is unsafe: would enlarge
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   350
  the search space.*)
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   351
AddIs  [UnionI];  
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   352
AddSEs [UN_E];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   353
AddSEs [UnionE];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   354
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   355
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   356
(*** Rules for Inter ***)
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   357
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   358
(*Not obviously useful towards proving InterI, InterD, InterE*)
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   359
qed_goalw "Inter_iff" ZF.thy [Inter_def,Ball_def]
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   360
    "A : Inter(C) <-> (ALL x:C. A: x) & (EX x. x:C)"
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   361
 (fn _=> [ Simp_tac 1, Fast_tac 1 ]);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   362
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   363
(* Intersection is well-behaved only if the family is non-empty! *)
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   364
qed_goalw "InterI" ZF.thy [Inter_def]
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   365
    "[| !!x. x: C ==> A: x;  c:C |] ==> A : Inter(C)"
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   366
 (fn prems=> [ fast_tac (!claset addIs prems) 1 ]);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   367
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   368
(*A "destruct" rule -- every B in C contains A as an element, but
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   369
  A:B can hold when B:C does not!  This rule is analogous to "spec". *)
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   370
qed_goalw "InterD" ZF.thy [Inter_def]
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   371
    "!!C. [| A : Inter(C);  B : C |] ==> A : B"
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   372
 (fn _=> [ Fast_tac 1 ]);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   373
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   374
(*"Classical" elimination rule -- does not require exhibiting B:C *)
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   375
qed_goalw "InterE" ZF.thy [Inter_def]
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   376
    "[| A : Inter(C);  A:B ==> R;  B~:C ==> R |] ==> R"
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   377
 (fn major::prems=>
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   378
  [ (rtac (major RS CollectD2 RS ballE) 1),
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   379
    (REPEAT (eresolve_tac prems 1)) ]);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   380
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   381
AddSIs [InterI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   382
AddEs  [InterD, make_elim InterD];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   383
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   384
(*** Rules for Intersections of families ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   385
(* INT x:A. B(x) abbreviates Inter({B(x). x:A}) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   386
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   387
qed_goalw "INT_iff" ZF.thy [Inter_def]
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   388
    "b : (INT x:A. B(x)) <-> (ALL x:A. b : B(x)) & (EX x. x:A)"
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   389
 (fn _=> [ Simp_tac 1, Best_tac 1 ]);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   390
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   391
qed_goal "INT_I" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   392
    "[| !!x. x: A ==> b: B(x);  a: A |] ==> b: (INT x:A. B(x))"
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   393
 (fn prems=> [ fast_tac (!claset addIs prems) 1 ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   394
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   395
qed_goal "INT_E" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   396
    "[| b : (INT x:A. B(x));  a: A |] ==> b : B(a)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   397
 (fn [major,minor]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   398
  [ (rtac (major RS InterD) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   399
    (rtac (minor RS RepFunI) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   400
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   401
qed_goal "INT_cong" ZF.thy
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   402
    "[| A=B;  !!x. x:B ==> C(x)=D(x) |] ==> (INT x:A.C(x)) = (INT x:B.D(x))"
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   403
 (fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   404
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   405
(*No "Addcongs [INT_cong]" because INT is a combination of constants*)
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   406
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   407
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   408
(*** Rules for Powersets ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   409
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   410
qed_goal "PowI" ZF.thy "A <= B ==> A : Pow(B)"
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   411
 (fn [prem]=> [ (rtac (prem RS (Pow_iff RS iffD2)) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   412
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   413
qed_goal "PowD" ZF.thy "A : Pow(B)  ==>  A<=B"
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   414
 (fn [major]=> [ (rtac (major RS (Pow_iff RS iffD1)) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   415
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   416
AddSIs [PowI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   417
AddSDs [PowD];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   418
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   419
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   420
(*** Rules for the empty set ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   421
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   422
(*The set {x:0.False} is empty; by foundation it equals 0 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   423
  See Suppes, page 21.*)
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   424
qed_goal "not_mem_empty" ZF.thy "a ~: 0"
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   425
 (fn _=>
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   426
  [ (cut_facts_tac [foundation] 1), 
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   427
    (best_tac (!claset addDs [equalityD2]) 1) ]);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   428
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   429
bind_thm ("emptyE", not_mem_empty RS notE);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   430
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   431
Addsimps [not_mem_empty];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   432
AddSEs [emptyE];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   433
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   434
qed_goal "empty_subsetI" ZF.thy "0 <= A"
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   435
 (fn _=> [ Fast_tac 1 ]);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   436
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   437
Addsimps [empty_subsetI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   438
AddSIs [empty_subsetI];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   439
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   440
qed_goal "equals0I" ZF.thy "[| !!y. y:A ==> False |] ==> A=0"
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   441
 (fn prems=> [ fast_tac (!claset addIs [equalityI] addDs prems) 1 ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   442
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   443
qed_goal "equals0D" ZF.thy "!!P. [| A=0;  a:A |] ==> P"
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   444
 (fn _=> [ Full_simp_tac 1, Fast_tac 1 ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   445
825
76d9575950f2 Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents: 775
diff changeset
   446
qed_goal "not_emptyI" ZF.thy "!!A a. a:A ==> A ~= 0"
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   447
 (fn _=> [ Fast_tac 1 ]);
825
76d9575950f2 Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents: 775
diff changeset
   448
868
452f1e6ae3bc Deleted semicolon at the end of the qed_goal line, which was preventing
lcp
parents: 854
diff changeset
   449
qed_goal "not_emptyE" ZF.thy "[| A ~= 0;  !!x. x:A ==> R |] ==> R"
825
76d9575950f2 Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents: 775
diff changeset
   450
 (fn [major,minor]=>
76d9575950f2 Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents: 775
diff changeset
   451
  [ rtac ([major, equals0I] MRS swap) 1,
76d9575950f2 Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents: 775
diff changeset
   452
    swap_res_tac [minor] 1,
76d9575950f2 Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents: 775
diff changeset
   453
    assume_tac 1 ]);
76d9575950f2 Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents: 775
diff changeset
   454
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   455
748
ba231bd734d2 moved Cantors theorem here from ZF/ex/misc
lcp
parents: 722
diff changeset
   456
(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***)
ba231bd734d2 moved Cantors theorem here from ZF/ex/misc
lcp
parents: 722
diff changeset
   457
ba231bd734d2 moved Cantors theorem here from ZF/ex/misc
lcp
parents: 722
diff changeset
   458
val cantor_cs = FOL_cs   (*precisely the rules needed for the proof*)
ba231bd734d2 moved Cantors theorem here from ZF/ex/misc
lcp
parents: 722
diff changeset
   459
  addSIs [ballI, CollectI, PowI, subsetI] addIs [bexI]
ba231bd734d2 moved Cantors theorem here from ZF/ex/misc
lcp
parents: 722
diff changeset
   460
  addSEs [CollectE, equalityCE];
ba231bd734d2 moved Cantors theorem here from ZF/ex/misc
lcp
parents: 722
diff changeset
   461
ba231bd734d2 moved Cantors theorem here from ZF/ex/misc
lcp
parents: 722
diff changeset
   462
(*The search is undirected; similar proof attempts may fail.
ba231bd734d2 moved Cantors theorem here from ZF/ex/misc
lcp
parents: 722
diff changeset
   463
  b represents ANY map, such as (lam x:A.b(x)): A->Pow(A). *)
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   464
qed_goal "cantor" ZF.thy "EX S: Pow(A). ALL x:A. b(x) ~= S"
748
ba231bd734d2 moved Cantors theorem here from ZF/ex/misc
lcp
parents: 722
diff changeset
   465
 (fn _ => [best_tac cantor_cs 1]);
ba231bd734d2 moved Cantors theorem here from ZF/ex/misc
lcp
parents: 722
diff changeset
   466
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
   467
(*Lemma for the inductive definition in Zorn.thy*)
775
7b60621e2bad removed ZF_Lemmas and added qed_goal
clasohm
parents: 748
diff changeset
   468
qed_goal "Union_in_Pow" ZF.thy
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
   469
    "!!Y. Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)"
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   470
 (fn _ => [Fast_tac 1]);
1902
e349b91cf197 Added function for storing default claset in theory.
berghofe
parents: 1889
diff changeset
   471