wneuper/isa: src/ZF/upair.ML@8ce8c4d13d4d

     1 (*  Title: 	ZF/upair

     2     ID:         $Id$

     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory

     4     Copyright   1991  University of Cambridge

     6 UNORDERED pairs in Zermelo-Fraenkel Set Theory

     8 Observe the order of dependence:

     9     Upair is defined in terms of Replace

    10     Un is defined in terms of Upair and Union (similarly for Int)

    11     cons is defined in terms of Upair and Un

    12     Ordered pairs and descriptions are defined using cons ("set notation")

    13 *)

    15 (*** Lemmas about power sets  ***)

    17 val Pow_bottom = empty_subsetI RS PowI;		(* 0 : Pow(B) *)

    18 val Pow_top = subset_refl RS PowI;		(* A : Pow(A) *)

    19 val Pow_neq_0 = Pow_top RSN (2,equals0D);	(* Pow(a)=0 ==> P *)

    22 (*** Unordered pairs - Upair ***)

    24 val pairing = prove_goalw ZF.thy [Upair_def]

    25     "c : Upair(a,b) <-> (c=a | c=b)"

    26  (fn _ => [ (fast_tac (lemmas_cs addEs [Pow_neq_0, sym RS Pow_neq_0]) 1) ]);

    28 val UpairI1 = prove_goal ZF.thy "a : Upair(a,b)"

    29  (fn _ => [ (rtac (refl RS disjI1 RS (pairing RS iffD2)) 1) ]);

    31 val UpairI2 = prove_goal ZF.thy "b : Upair(a,b)"

    32  (fn _ => [ (rtac (refl RS disjI2 RS (pairing RS iffD2)) 1) ]);

    34 val UpairE = prove_goal ZF.thy

    35     "[| a : Upair(b,c);  a=b ==> P;  a=c ==> P |] ==> P"

    36  (fn major::prems=>

    37   [ (rtac (major RS (pairing RS iffD1 RS disjE)) 1),

    38     (REPEAT (eresolve_tac prems 1)) ]);

    40 (*** Rules for binary union -- Un -- defined via Upair ***)

    42 val UnI1 = prove_goalw ZF.thy [Un_def] "c : A ==> c : A Un B"

    43  (fn [prem]=> [ (rtac (prem RS (UpairI1 RS UnionI)) 1) ]);

    45 val UnI2 = prove_goalw ZF.thy [Un_def] "c : B ==> c : A Un B"

    46  (fn [prem]=> [ (rtac (prem RS (UpairI2 RS UnionI)) 1) ]);

    48 val UnE = prove_goalw ZF.thy [Un_def]

    49     "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P"

    50  (fn major::prems=>

    51   [ (rtac (major RS UnionE) 1),

    52     (etac UpairE 1),

    53     (REPEAT (EVERY1 [resolve_tac prems, etac subst, assume_tac])) ]);

    55 val Un_iff = prove_goal ZF.thy "c : A Un B <-> (c:A | c:B)"

    56  (fn _ => [ (fast_tac (lemmas_cs addIs [UnI1,UnI2] addSEs [UnE]) 1) ]);

    58 (*Classical introduction rule: no commitment to A vs B*)

    59 val UnCI = prove_goal ZF.thy "(~c : B ==> c : A) ==> c : A Un B"

    60  (fn [prem]=>

    61   [ (rtac (disjCI RS (Un_iff RS iffD2)) 1),

    62     (etac prem 1) ]);

    65 (*** Rules for small intersection -- Int -- defined via Upair ***)

    67 val IntI = prove_goalw ZF.thy [Int_def]

    68     "[| c : A;  c : B |] ==> c : A Int B"

    69  (fn prems=>

    70   [ (REPEAT (resolve_tac (prems @ [UpairI1,InterI]) 1

    71      ORELSE eresolve_tac [UpairE, ssubst] 1)) ]);

    73 val IntD1 = prove_goalw ZF.thy [Int_def] "c : A Int B ==> c : A"

    74  (fn [major]=>

    75   [ (rtac (UpairI1 RS (major RS InterD)) 1) ]);

    77 val IntD2 = prove_goalw ZF.thy [Int_def] "c : A Int B ==> c : B"

    78  (fn [major]=>

    79   [ (rtac (UpairI2 RS (major RS InterD)) 1) ]);

    81 val IntE = prove_goal ZF.thy

    82     "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P"

    83  (fn prems=>

    84   [ (resolve_tac prems 1),

    85     (REPEAT (resolve_tac (prems RL [IntD1,IntD2]) 1)) ]);

    87 val Int_iff = prove_goal ZF.thy "c : A Int B <-> (c:A & c:B)"

    88  (fn _ => [ (fast_tac (lemmas_cs addSIs [IntI] addSEs [IntE]) 1) ]);

    91 (*** Rules for set difference -- defined via Upair ***)

    93 val DiffI = prove_goalw ZF.thy [Diff_def]

    94     "[| c : A;  ~ c : B |] ==> c : A - B"

    95  (fn prems=> [ (REPEAT (resolve_tac (prems @ [CollectI]) 1)) ]);

    97 val DiffD1 = prove_goalw ZF.thy [Diff_def]

    98     "c : A - B ==> c : A"

    99  (fn [major]=> [ (rtac (major RS CollectD1) 1) ]);

   101 val DiffD2 = prove_goalw ZF.thy [Diff_def]

   102     "[| c : A - B;  c : B |] ==> P"

   103  (fn [major,minor]=> [ (rtac (minor RS (major RS CollectD2 RS notE)) 1) ]);

   105 val DiffE = prove_goal ZF.thy

   106     "[| c : A - B;  [| c:A; ~ c:B |] ==> P |] ==> P"

   107  (fn prems=>

   108   [ (resolve_tac prems 1),

   109     (REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ]);

   111 val Diff_iff = prove_goal ZF.thy "c : A-B <-> (c:A & ~ c:B)"

   112  (fn _ => [ (fast_tac (lemmas_cs addSIs [DiffI] addSEs [DiffE]) 1) ]);

   114 (*** Rules for cons -- defined via Un and Upair ***)

   116 val consI1 = prove_goalw ZF.thy [cons_def] "a : cons(a,B)"

   117  (fn _ => [ (rtac (UpairI1 RS UnI1) 1) ]);

   119 val consI2 = prove_goalw ZF.thy [cons_def] "a : B ==> a : cons(b,B)"

   120  (fn [prem]=> [ (rtac (prem RS UnI2) 1) ]);

   122 val consE = prove_goalw ZF.thy [cons_def]

   123     "[| a : cons(b,A);  a=b ==> P;  a:A ==> P |] ==> P"

   124  (fn major::prems=>

   125   [ (rtac (major RS UnE) 1),

   126     (REPEAT (eresolve_tac (prems @ [UpairE]) 1)) ]);

   128 val cons_iff = prove_goal ZF.thy "a : cons(b,A) <-> (a=b | a:A)"

   129  (fn _ => [ (fast_tac (lemmas_cs addIs [consI1,consI2] addSEs [consE]) 1) ]);

   131 (*Classical introduction rule*)

   132 val consCI = prove_goal ZF.thy "(~ a:B ==> a=b) ==> a: cons(b,B)"

   133  (fn [prem]=>

   134   [ (rtac (disjCI RS (cons_iff RS iffD2)) 1),

   135     (etac prem 1) ]);

   137 (*** Singletons - using cons ***)

   139 val singletonI = prove_goal ZF.thy "a : {a}"

   140  (fn _=> [ (rtac consI1 1) ]);

   142 val singletonE = prove_goal ZF.thy "[| a: {b};  a=b ==> P |] ==> P"

   143  (fn major::prems=>

   144   [ (rtac (major RS consE) 1),

   145     (REPEAT (eresolve_tac (prems @ [emptyE]) 1)) ]);

   148 (*** Rules for Descriptions ***)

   150 val the_equality = prove_goalw ZF.thy [the_def]

   151     "[| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"

   152  (fn prems=>

   153   [ (fast_tac (lemmas_cs addIs ([equalityI,singletonI]@prems)

   154 	                 addEs (prems RL [subst])) 1) ]);

   156 (* Only use this if you already know EX!x. P(x) *)

   157 val the_equality2 = prove_goal ZF.thy

   158     "[| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a"

   159  (fn major::prems=>

   160   [ (rtac the_equality 1),

   161     (rtac (major RS ex1_equalsE) 2),

   162     (REPEAT (ares_tac prems 1)) ]);

   164 val theI = prove_goal ZF.thy "EX! x. P(x) ==> P(THE x. P(x))"

   165  (fn [major]=>

   166   [ (rtac (major RS ex1E) 1),

   167     (resolve_tac [major RS the_equality2 RS ssubst] 1),

   168     (REPEAT (assume_tac 1)) ]);

   171 (*** if -- a conditional expression for formulae ***)

   173 goalw ZF.thy [if_def] "if(True,a,b) = a";

   174 by (fast_tac (lemmas_cs addIs [the_equality]) 1);

   175 val if_true = result();

   177 goalw ZF.thy [if_def] "if(False,a,b) = b";

   178 by (fast_tac (lemmas_cs addIs [the_equality]) 1);

   179 val if_false = result();

   181 (*Never use with case splitting, or if P is known to be true or false*)

   182 val prems = goalw ZF.thy [if_def]

   183     "[| P<->Q;  Q ==> a=c;  ~Q ==> b=d |] ==> if(P,a,b) = if(Q,c,d)";

   184 by (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1);

   185 val if_cong = result();

   187 (*Not needed for rewriting, since P would rewrite to True anyway*)

   188 goalw ZF.thy [if_def] "!!P. P ==> if(P,a,b) = a";

   189 by (fast_tac (lemmas_cs addSIs [the_equality]) 1);

   190 val if_P = result();

   192 (*Not needed for rewriting, since P would rewrite to False anyway*)

   193 goalw ZF.thy [if_def] "!!P. ~P ==> if(P,a,b) = b";

   194 by (fast_tac (lemmas_cs addSIs [the_equality]) 1);

   195 val if_not_P = result();

   197 val if_ss = FOL_ss addsimps  [if_true,if_false];

   199 val expand_if = prove_goal ZF.thy

   200     "P(if(Q,x,y)) <-> ((Q --> P(x)) & (~Q --> P(y)))"

   201  (fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1),

   202 	   (asm_simp_tac if_ss 1),

   203 	   (asm_simp_tac if_ss 1) ]);

   205 val prems = goal ZF.thy

   206     "[| P ==> a: A;  ~P ==> b: A |] ==> if(P,a,b): A";

   207 by (res_inst_tac [("Q","P")] (excluded_middle RS disjE) 1);

   208 by (ALLGOALS (asm_simp_tac (if_ss addsimps prems)));

   209 val if_type = result();

   212 (*** Foundation lemmas ***)

   214 val mem_anti_sym = prove_goal ZF.thy "[| a:b;  b:a |] ==> P"

   215  (fn prems=>

   216   [ (rtac disjE 1),

   217     (res_inst_tac [("A","{a,b}")] foundation 1),

   218     (etac equals0D 1),

   219     (rtac consI1 1),

   220     (fast_tac (lemmas_cs addIs (prems@[consI1,consI2])

   221 		         addSEs [consE,equalityE]) 1) ]);

   223 val mem_anti_refl = prove_goal ZF.thy "a:a ==> P"

   224  (fn [major]=> [ (rtac (major RS (major RS mem_anti_sym)) 1) ]);

   226 val mem_not_refl = prove_goal ZF.thy "~ a:a"

   227  (K [ (rtac notI 1), (etac mem_anti_refl 1) ]);

   229 (*** Rules for succ ***)

   231 val succI1 = prove_goalw ZF.thy [succ_def] "i : succ(i)"

   232  (fn _=> [ (rtac consI1 1) ]);

   234 val succI2 = prove_goalw ZF.thy [succ_def]

   235     "i : j ==> i : succ(j)"

   236  (fn [prem]=> [ (rtac (prem RS consI2) 1) ]);

   238 (*Classical introduction rule*)

   239 val succCI = prove_goalw ZF.thy [succ_def]

   240    "(~ i:j ==> i=j) ==> i: succ(j)"

   241  (fn prems=> [ (rtac consCI 1), (eresolve_tac prems 1) ]);

   243 val succE = prove_goalw ZF.thy [succ_def]

   244     "[| i : succ(j);  i=j ==> P;  i:j ==> P |] ==> P"

   245  (fn major::prems=>

   246   [ (rtac (major RS consE) 1),

   247     (REPEAT (eresolve_tac prems 1)) ]);

   249 val succ_neq_0 = prove_goal ZF.thy "succ(n)=0 ==> P"

   250  (fn [major]=>

   251   [ (rtac (major RS equalityD1 RS subsetD RS emptyE) 1),

   252     (rtac succI1 1) ]);

   254 (*Useful for rewriting*)

   255 val succ_not_0 = prove_goal ZF.thy "~ succ(n)=0"

   256  (fn _=> [ (rtac notI 1), (etac succ_neq_0 1) ]);

   258 (* succ(c) <= B ==> c : B *)

   259 val succ_subsetD = succI1 RSN (2,subsetD);

   261 val succ_inject = prove_goal ZF.thy "succ(m) = succ(n) ==> m=n"

   262  (fn [major]=>

   263   [ (rtac (major RS equalityE) 1),

   264     (REPEAT (eresolve_tac [asm_rl, sym, succE, make_elim succ_subsetD,

   265 			   mem_anti_sym] 1)) ]);

   267 val succ_inject_iff = prove_goal ZF.thy "succ(m) = succ(n) <-> m=n"

   268  (fn _=> [ (fast_tac (FOL_cs addSEs [succ_inject]) 1) ]);

   270 (*UpairI1/2 should become UpairCI;  mem_anti_refl as a hazE? *)

   271 val upair_cs = lemmas_cs

   272   addSIs [singletonI, DiffI, IntI, UnCI, consCI, succCI, UpairI1,UpairI2]

   273   addSEs [singletonE, DiffE, IntE, UnE, consE, succE, UpairE];

author	lcp
	Fri, 17 Sep 1993 16:16:38 +0200
changeset 6	8ce8c4d13d4d
parent 0	a5a9c433f639
child 14	1c0926788772
permissions	-rw-r--r--