src/ZF/upair.ML

tuned;
prepare ext;

(*  Title:      ZF/upair
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge

UNORDERED pairs in Zermelo-Fraenkel Set Theory 

Observe the order of dependence:
    Upair is defined in terms of Replace
    Un is defined in terms of Upair and Union (similarly for Int)
    cons is defined in terms of Upair and Un
    Ordered pairs and descriptions are defined using cons ("set notation")
*)

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

val Pow_bottom = empty_subsetI RS PowI;         (* 0 : Pow(B) *)
val Pow_top = subset_refl RS PowI;              (* A : Pow(A) *)
val Pow_neq_0 = Pow_top RSN (2,equals0D);       (* Pow(a)=0 ==> P *) 


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

qed_goalw "Upair_iff" ZF.thy [Upair_def]
    "c : Upair(a,b) <-> (c=a | c=b)"
 (fn _ => [ (blast_tac (!claset addEs [Pow_neq_0, sym RS Pow_neq_0]) 1) ]);

Addsimps [Upair_iff];

qed_goal "UpairI1" ZF.thy "a : Upair(a,b)"
 (fn _ => [ Simp_tac 1 ]);

qed_goal "UpairI2" ZF.thy "b : Upair(a,b)"
 (fn _ => [ Simp_tac 1 ]);

qed_goal "UpairE" ZF.thy
    "[| a : Upair(b,c);  a=b ==> P;  a=c ==> P |] ==> P"
 (fn major::prems=>
  [ (rtac (major RS (Upair_iff RS iffD1 RS disjE)) 1),
    (REPEAT (eresolve_tac prems 1)) ]);

AddSIs [UpairI1,UpairI2];
AddSEs [UpairE];

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

qed_goalw "Un_iff" ZF.thy [Un_def] "c : A Un B <-> (c:A | c:B)"
 (fn _ => [ Blast_tac 1 ]);

Addsimps [Un_iff];

qed_goal "UnI1" ZF.thy "!!c. c : A ==> c : A Un B"
 (fn _ => [ Asm_simp_tac 1 ]);

qed_goal "UnI2" ZF.thy "!!c. c : B ==> c : A Un B"
 (fn _ => [ Asm_simp_tac 1 ]);

qed_goal "UnE" ZF.thy 
    "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P"
 (fn major::prems=>
  [ (rtac (major RS (Un_iff RS iffD1 RS disjE)) 1),
    (REPEAT (eresolve_tac prems 1)) ]);

(*Stronger version of the rule above*)
qed_goal "UnE'" ZF.thy
    "[| c : A Un B;  c:A ==> P;  [| c:B;  c~:A |] ==> P |] ==> P"
 (fn major::prems =>
  [(rtac (major RS UnE) 1),
   (eresolve_tac prems 1),
   (rtac classical 1),
   (eresolve_tac prems 1),
   (swap_res_tac prems 1),
   (etac notnotD 1)]);

(*Classical introduction rule: no commitment to A vs B*)
qed_goal "UnCI" ZF.thy "(c ~: B ==> c : A) ==> c : A Un B"
 (fn prems=>
  [ Simp_tac 1, blast_tac (!claset addSIs prems) 1 ]);

AddSIs [UnCI];
AddSEs [UnE];


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

qed_goalw "Int_iff" ZF.thy [Int_def] "c : A Int B <-> (c:A & c:B)"
 (fn _ => [ Blast_tac 1 ]);

Addsimps [Int_iff];

qed_goal "IntI" ZF.thy "!!c. [| c : A;  c : B |] ==> c : A Int B"
 (fn _ => [ Asm_simp_tac 1 ]);

qed_goal "IntD1" ZF.thy "!!c. c : A Int B ==> c : A"
 (fn _ => [ Asm_full_simp_tac 1 ]);

qed_goal "IntD2" ZF.thy "!!c. c : A Int B ==> c : B"
 (fn _ => [ Asm_full_simp_tac 1 ]);

qed_goal "IntE" ZF.thy
    "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P"
 (fn prems=>
  [ (resolve_tac prems 1),
    (REPEAT (resolve_tac (prems RL [IntD1,IntD2]) 1)) ]);

AddSIs [IntI];
AddSEs [IntE];

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

qed_goalw "Diff_iff" ZF.thy [Diff_def] "c : A-B <-> (c:A & c~:B)"
 (fn _ => [ Blast_tac 1 ]);

Addsimps [Diff_iff];

qed_goal "DiffI" ZF.thy "!!c. [| c : A;  c ~: B |] ==> c : A - B"
 (fn _ => [ Asm_simp_tac 1 ]);

qed_goal "DiffD1" ZF.thy "!!c. c : A - B ==> c : A"
 (fn _ => [ Asm_full_simp_tac 1 ]);

qed_goal "DiffD2" ZF.thy "!!c. c : A - B ==> c ~: B"
 (fn _ => [ Asm_full_simp_tac 1 ]);

qed_goal "DiffE" ZF.thy
    "[| c : A - B;  [| c:A; c~:B |] ==> P |] ==> P"
 (fn prems=>
  [ (resolve_tac prems 1),
    (REPEAT (ares_tac (prems RL [DiffD1, DiffD2]) 1)) ]);

AddSIs [DiffI];
AddSEs [DiffE];

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

qed_goalw "cons_iff" ZF.thy [cons_def] "a : cons(b,A) <-> (a=b | a:A)"
 (fn _ => [ Blast_tac 1 ]);

Addsimps [cons_iff];

qed_goal "consI1" ZF.thy "a : cons(a,B)"
 (fn _ => [ Simp_tac 1 ]);

Addsimps [consI1];

qed_goal "consI2" ZF.thy "!!B. a : B ==> a : cons(b,B)"
 (fn _ => [ Asm_simp_tac 1 ]);

qed_goal "consE" ZF.thy
    "[| a : cons(b,A);  a=b ==> P;  a:A ==> P |] ==> P"
 (fn major::prems=>
  [ (rtac (major RS (cons_iff RS iffD1 RS disjE)) 1),
    (REPEAT (eresolve_tac (prems @ [UpairE]) 1)) ]);

(*Stronger version of the rule above*)
qed_goal "consE'" ZF.thy
    "[| a : cons(b,A);  a=b ==> P;  [| a:A;  a~=b |] ==> P |] ==> P"
 (fn major::prems =>
  [(rtac (major RS consE) 1),
   (eresolve_tac prems 1),
   (rtac classical 1),
   (eresolve_tac prems 1),
   (swap_res_tac prems 1),
   (etac notnotD 1)]);

(*Classical introduction rule*)
qed_goal "consCI" ZF.thy "(a~:B ==> a=b) ==> a: cons(b,B)"
 (fn prems=>
  [ Simp_tac 1, blast_tac (!claset addSIs prems) 1 ]);

AddSIs [consCI];
AddSEs [consE];

qed_goal "cons_not_0" ZF.thy "cons(a,B) ~= 0"
 (fn _ => [ (blast_tac (!claset addEs [equalityE]) 1) ]);

bind_thm ("cons_neq_0", cons_not_0 RS notE);

Addsimps [cons_not_0, cons_not_0 RS not_sym];


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

qed_goal "singleton_iff" ZF.thy "a : {b} <-> a=b"
 (fn _ => [ Simp_tac 1 ]);

qed_goal "singletonI" ZF.thy "a : {a}"
 (fn _=> [ (rtac consI1 1) ]);

bind_thm ("singletonE", make_elim (singleton_iff RS iffD1));

AddSIs [singletonI];
AddSEs [singletonE];

(*** Rules for Descriptions ***)

qed_goalw "the_equality" ZF.thy [the_def]
    "[| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
 (fn [pa,eq] =>
  [ (fast_tac (!claset addSIs [pa] addEs [eq RS subst]) 1) ]);

(* Only use this if you already know EX!x. P(x) *)
qed_goal "the_equality2" ZF.thy
    "!!P. [| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
 (fn _ =>
  [ (deepen_tac (!claset addSIs [the_equality]) 1 1) ]);

qed_goal "theI" ZF.thy "EX! x. P(x) ==> P(THE x. P(x))"
 (fn [major]=>
  [ (rtac (major RS ex1E) 1),
    (resolve_tac [major RS the_equality2 RS ssubst] 1),
    (REPEAT (assume_tac 1)) ]);

(*Easier to apply than theI: conclusion has only one occurrence of P*)
qed_goal "theI2" ZF.thy
    "[| EX! x. P(x);  !!x. P(x) ==> Q(x) |] ==> Q(THE x. P(x))"
 (fn prems => [ resolve_tac prems 1, 
                rtac theI 1, 
                resolve_tac prems 1 ]);

(*the_cong is no longer necessary: if (ALL y.P(y)<->Q(y)) then 
  (THE x.P(x))  rewrites to  (THE x. Q(x))  *)

(*If it's "undefined", it's zero!*)
qed_goalw "the_0" ZF.thy [the_def]
    "!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0"
 (fn _ => [ (deepen_tac (!claset addSEs [ReplaceE]) 0 1) ]);


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

goalw ZF.thy [if_def] "if(True,a,b) = a";
by (blast_tac (!claset addSIs [the_equality]) 1);
qed "if_true";

goalw ZF.thy [if_def] "if(False,a,b) = b";
by (blast_tac (!claset addSIs [the_equality]) 1);
qed "if_false";

(*Never use with case splitting, or if P is known to be true or false*)
val prems = goalw ZF.thy [if_def]
    "[| P<->Q;  Q ==> a=c;  ~Q ==> b=d |] ==> if(P,a,b) = if(Q,c,d)";
by (simp_tac (!simpset addsimps prems addcongs [conj_cong]) 1);
qed "if_cong";

(*Not needed for rewriting, since P would rewrite to True anyway*)
goalw ZF.thy [if_def] "!!P. P ==> if(P,a,b) = a";
by (blast_tac (!claset addSIs [the_equality]) 1);
qed "if_P";

(*Not needed for rewriting, since P would rewrite to False anyway*)
goalw ZF.thy [if_def] "!!P. ~P ==> if(P,a,b) = b";
by (blast_tac (!claset addSIs [the_equality]) 1);
qed "if_not_P";

Addsimps [if_true, if_false];

qed_goal "expand_if" ZF.thy
    "P(if(Q,x,y)) <-> ((Q --> P(x)) & (~Q --> P(y)))"
 (fn _=> [ (excluded_middle_tac "Q" 1),
           (Asm_simp_tac 1),
           (Asm_simp_tac 1) ]);

qed_goal "if_iff" ZF.thy "a: if(P,x,y) <-> P & a:x | ~P & a:y"
 (fn _=> [ (simp_tac (!simpset setloop split_tac [expand_if]) 1) ]);

qed_goal "if_type" ZF.thy
    "[| P ==> a: A;  ~P ==> b: A |] ==> if(P,a,b): A"
 (fn prems=> [ (simp_tac 
                (!simpset addsimps prems setloop split_tac [expand_if]) 1) ]);


(*** Foundation lemmas ***)

(*was called mem_anti_sym*)
qed_goal "mem_asym" ZF.thy "[| a:b;  ~P ==> b:a |] ==> P"
 (fn prems=>
  [ (rtac classical 1),
    (res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1),
    REPEAT (blast_tac (!claset addIs prems addSEs [equalityE]) 1) ]);

(*was called mem_anti_refl*)
qed_goal "mem_irrefl" ZF.thy "a:a ==> P"
 (fn [major]=> [ (rtac ([major,major] MRS mem_asym) 1) ]);

(*mem_irrefl should NOT be added to default databases:
      it would be tried on most goals, making proofs slower!*)

qed_goal "mem_not_refl" ZF.thy "a ~: a"
 (K [ (rtac notI 1), (etac mem_irrefl 1) ]);

(*Good for proving inequalities by rewriting*)
qed_goal "mem_imp_not_eq" ZF.thy "!!a A. a:A ==> a ~= A"
 (fn _=> [ blast_tac (!claset addSEs [mem_irrefl]) 1 ]);

(*** Rules for succ ***)

qed_goalw "succ_iff" ZF.thy [succ_def] "i : succ(j) <-> i=j | i:j"
 (fn _ => [ Blast_tac 1 ]);

qed_goalw "succI1" ZF.thy [succ_def] "i : succ(i)"
 (fn _=> [ (rtac consI1 1) ]);

Addsimps [succI1];

qed_goalw "succI2" ZF.thy [succ_def]
    "i : j ==> i : succ(j)"
 (fn [prem]=> [ (rtac (prem RS consI2) 1) ]);

qed_goalw "succE" ZF.thy [succ_def]
    "[| i : succ(j);  i=j ==> P;  i:j ==> P |] ==> P"
 (fn major::prems=>
  [ (rtac (major RS consE) 1),
    (REPEAT (eresolve_tac prems 1)) ]);

(*Classical introduction rule*)
qed_goal "succCI" ZF.thy "(i~:j ==> i=j) ==> i: succ(j)"
 (fn [prem]=>
  [ (rtac (disjCI RS (succ_iff RS iffD2)) 1),
    (etac prem 1) ]);

AddSIs [succCI];
AddSEs [succE];

qed_goal "succ_not_0" ZF.thy "succ(n) ~= 0"
 (fn _=> [ (blast_tac (!claset addSEs [equalityE]) 1) ]);

bind_thm ("succ_neq_0", succ_not_0 RS notE);

Addsimps [succ_not_0, succ_not_0 RS not_sym];
AddSEs [succ_neq_0, sym RS succ_neq_0];


(* succ(c) <= B ==> c : B *)
val succ_subsetD = succI1 RSN (2,subsetD);

(* succ(b) ~= b *)
bind_thm ("succ_neq_self", succI1 RS mem_imp_not_eq RS not_sym);


qed_goal "succ_inject_iff" ZF.thy "succ(m) = succ(n) <-> m=n"
 (fn _=> [ (blast_tac (!claset addEs [mem_asym] addSEs [equalityE]) 1) ]);

bind_thm ("succ_inject", succ_inject_iff RS iffD1);

Addsimps [succ_inject_iff];
AddSDs [succ_inject];

(*Not needed now that cons is available.  Deletion reduces the search space.*)
Delrules [UpairI1,UpairI2,UpairE];

use"simpdata.ML";