# Theory upair

Up to index of Isabelle/ZF

theory upair
imports ZF
uses Tools/typechk.ML
begin

    (*  Title:      ZF/upair.thy
        ID:         $Id: upair.thy,v 1.17 2005/06/17 14:15:10 haftmann Exp $
        Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
        Copyright   1993  University of Cambridge

    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")
    *)

    header{*Unordered Pairs*}

    theory upair imports ZF
    uses "Tools/typechk.ML" begin

    setup TypeCheck.setup

    lemma atomize_ball [symmetric, rulify]:
         "(!!x. x:A ==> P(x)) == Trueprop (ALL x:A. P(x))"
    by (simp add: Ball_def atomize_all atomize_imp)

    subsection{*Unordered Pairs: constant @{term Upair}*}

    lemma Upair_iff [simp]: "c : Upair(a,b) <-> (c=a | c=b)"
    by (unfold Upair_def, blast)

    lemma UpairI1: "a : Upair(a,b)"
    by simp

    lemma UpairI2: "b : Upair(a,b)"
    by simp

    lemma UpairE: "[| a : Upair(b,c);  a=b ==> P;  a=c ==> P |] ==> P"
    by (simp, blast)

    subsection{*Rules for Binary Union, Defined via @{term Upair}*}

    lemma Un_iff [simp]: "c : A Un B <-> (c:A | c:B)"
    apply (simp add: Un_def)
    apply (blast intro: UpairI1 UpairI2 elim: UpairE)
    done

    lemma UnI1: "c : A ==> c : A Un B"
    by simp

    lemma UnI2: "c : B ==> c : A Un B"
    by simp

    declare UnI1 [elim?]  UnI2 [elim?]

    lemma UnE [elim!]: "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P"
    by (simp, blast)

    (*Stronger version of the rule above*)
    lemma UnE': "[| c : A Un B;  c:A ==> P;  [| c:B;  c~:A |] ==> P |] ==> P"
    by (simp, blast)

    (*Classical introduction rule: no commitment to A vs B*)
    lemma UnCI [intro!]: "(c ~: B ==> c : A) ==> c : A Un B"
    by (simp, blast)

    subsection{*Rules for Binary Intersection, Defined via @{term Upair}*}

    lemma Int_iff [simp]: "c : A Int B <-> (c:A & c:B)"
    apply (unfold Int_def)
    apply (blast intro: UpairI1 UpairI2 elim: UpairE)
    done

    lemma IntI [intro!]: "[| c : A;  c : B |] ==> c : A Int B"
    by simp

    lemma IntD1: "c : A Int B ==> c : A"
    by simp

    lemma IntD2: "c : A Int B ==> c : B"
    by simp

    lemma IntE [elim!]: "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P"
    by simp

    subsection{*Rules for Set Difference, Defined via @{term Upair}*}

    lemma Diff_iff [simp]: "c : A-B <-> (c:A & c~:B)"
    by (unfold Diff_def, blast)

    lemma DiffI [intro!]: "[| c : A;  c ~: B |] ==> c : A - B"
    by simp

    lemma DiffD1: "c : A - B ==> c : A"
    by simp

    lemma DiffD2: "c : A - B ==> c ~: B"
    by simp

    lemma DiffE [elim!]: "[| c : A - B;  [| c:A; c~:B |] ==> P |] ==> P"
    by simp

    subsection{*Rules for @{term cons}*}

    lemma cons_iff [simp]: "a : cons(b,A) <-> (a=b | a:A)"
    apply (unfold cons_def)
    apply (blast intro: UpairI1 UpairI2 elim: UpairE)
    done

    (*risky as a typechecking rule, but solves otherwise unconstrained goals of
    the form x : ?A*)
    lemma consI1 [simp,TC]: "a : cons(a,B)"
    by simp

    lemma consI2: "a : B ==> a : cons(b,B)"
    by simp

    lemma consE [elim!]: "[| a : cons(b,A);  a=b ==> P;  a:A ==> P |] ==> P"
    by (simp, blast)

    (*Stronger version of the rule above*)
    lemma consE':
        "[| a : cons(b,A);  a=b ==> P;  [| a:A;  a~=b |] ==> P |] ==> P"
    by (simp, blast)

    (*Classical introduction rule*)
    lemma consCI [intro!]: "(a~:B ==> a=b) ==> a: cons(b,B)"
    by (simp, blast)

    lemma cons_not_0 [simp]: "cons(a,B) ~= 0"
    by (blast elim: equalityE)

    lemmas cons_neq_0 = cons_not_0 [THEN notE, standard]

    declare cons_not_0 [THEN not_sym, simp]

    subsection{*Singletons*}

    lemma singleton_iff: "a : {b} <-> a=b"
    by simp

    lemma singletonI [intro!]: "a : {a}"
    by (rule consI1)

    lemmas singletonE = singleton_iff [THEN iffD1, elim_format, standard, elim!]

    subsection{*Descriptions*}

    lemma the_equality [intro]:
        "[| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
    apply (unfold the_def)
    apply (fast dest: subst)
    done

    (* Only use this if you already know EX!x. P(x) *)
    lemma the_equality2: "[| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
    by blast

    lemma theI: "EX! x. P(x) ==> P(THE x. P(x))"
    apply (erule ex1E)
    apply (subst the_equality)
    apply (blast+)
    done

    (*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!*)
    lemma the_0: "~ (EX! x. P(x)) ==> (THE x. P(x))=0"
    apply (unfold the_def)
    apply (blast elim!: ReplaceE)
    done

    (*Easier to apply than theI: conclusion has only one occurrence of P*)
    lemma theI2:
        assumes p1: "~ Q(0) ==> EX! x. P(x)"
            and p2: "!!x. P(x) ==> Q(x)"
        shows "Q(THE x. P(x))"
    apply (rule classical)
    apply (rule p2)
    apply (rule theI)
    apply (rule classical)
    apply (rule p1)
    apply (erule the_0 [THEN subst], assumption)
    done

    lemma the_eq_trivial [simp]: "(THE x. x = a) = a"
    by blast

    lemma the_eq_trivial2 [simp]: "(THE x. a = x) = a"
    by blast

    subsection{*Conditional Terms: @{text "if-then-else"}*}

    lemma if_true [simp]: "(if True then a else b) = a"
    by (unfold if_def, blast)

    lemma if_false [simp]: "(if False then a else b) = b"
    by (unfold if_def, blast)

    (*Never use with case splitting, or if P is known to be true or false*)
    lemma if_cong:
        "[| P<->Q;  Q ==> a=c;  ~Q ==> b=d |]
         ==> (if P then a else b) = (if Q then c else d)"
    by (simp add: if_def cong add: conj_cong)

    (*Prevents simplification of x and y: faster and allows the execution
      of functional programs. NOW THE DEFAULT.*)
    lemma if_weak_cong: "P<->Q ==> (if P then x else y) = (if Q then x else y)"
    by simp

    (*Not needed for rewriting, since P would rewrite to True anyway*)
    lemma if_P: "P ==> (if P then a else b) = a"
    by (unfold if_def, blast)

    (*Not needed for rewriting, since P would rewrite to False anyway*)
    lemma if_not_P: "~P ==> (if P then a else b) = b"
    by (unfold if_def, blast)

    lemma split_if [split]:
         "P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
    by (case_tac Q, simp_all)

    (** Rewrite rules for boolean case-splitting: faster than
            addsplits[split_if]
    **)

    lemmas split_if_eq1 = split_if [of "%x. x = b", standard]
    lemmas split_if_eq2 = split_if [of "%x. a = x", standard]

    lemmas split_if_mem1 = split_if [of "%x. x : b", standard]
    lemmas split_if_mem2 = split_if [of "%x. a : x", standard]

    lemmas split_ifs = split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2

    (*Logically equivalent to split_if_mem2*)
    lemma if_iff: "a: (if P then x else y) <-> P & a:x | ~P & a:y"
    by simp

    lemma if_type [TC]:
        "[| P ==> a: A;  ~P ==> b: A |] ==> (if P then a else b): A"
    by simp

    (** Splitting IFs in the assumptions **)

    lemma split_if_asm: "P(if Q then x else y) <-> (~((Q & ~P(x)) | (~Q & ~P(y))))"
    by simp

    lemmas if_splits = split_if split_if_asm

    subsection{*Consequences of Foundation*}

    (*was called mem_anti_sym*)
    lemma mem_asym: "[| a:b;  ~P ==> b:a |] ==> P"
    apply (rule classical)
    apply (rule_tac A1 = "{a,b}" in foundation [THEN disjE])
    apply (blast elim!: equalityE)+
    done

    (*was called mem_anti_refl*)
    lemma mem_irrefl: "a:a ==> P"
    by (blast intro: mem_asym)

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

    lemma mem_not_refl: "a ~: a"
    apply (rule notI)
    apply (erule mem_irrefl)
    done

    (*Good for proving inequalities by rewriting*)
    lemma mem_imp_not_eq: "a:A ==> a ~= A"
    by (blast elim!: mem_irrefl)

    lemma eq_imp_not_mem: "a=A ==> a ~: A"
    by (blast intro: elim: mem_irrefl)

    subsection{*Rules for Successor*}

    lemma succ_iff: "i : succ(j) <-> i=j | i:j"
    by (unfold succ_def, blast)

    lemma succI1 [simp]: "i : succ(i)"
    by (simp add: succ_iff)

    lemma succI2: "i : j ==> i : succ(j)"
    by (simp add: succ_iff)

    lemma succE [elim!]:
        "[| i : succ(j);  i=j ==> P;  i:j ==> P |] ==> P"
    apply (simp add: succ_iff, blast)
    done

    (*Classical introduction rule*)
    lemma succCI [intro!]: "(i~:j ==> i=j) ==> i: succ(j)"
    by (simp add: succ_iff, blast)

    lemma succ_not_0 [simp]: "succ(n) ~= 0"
    by (blast elim!: equalityE)

    lemmas succ_neq_0 = succ_not_0 [THEN notE, standard, elim!]

    declare succ_not_0 [THEN not_sym, simp]
    declare sym [THEN succ_neq_0, elim!]

    (* succ(c) <= B ==> c : B *)
    lemmas succ_subsetD = succI1 [THEN [2] subsetD]

    (* succ(b) ~= b *)
    lemmas succ_neq_self = succI1 [THEN mem_imp_not_eq, THEN not_sym, standard]

    lemma succ_inject_iff [simp]: "succ(m) = succ(n) <-> m=n"
    by (blast elim: mem_asym elim!: equalityE)

    lemmas succ_inject = succ_inject_iff [THEN iffD1, standard, dest!]

    subsection{*Miniscoping of the Bounded Universal Quantifier*}

    lemma ball_simps1:
         "(ALL x:A. P(x) & Q)   <-> (ALL x:A. P(x)) & (A=0 | Q)"
         "(ALL x:A. P(x) | Q)   <-> ((ALL x:A. P(x)) | Q)"
         "(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)"
         "(~(ALL x:A. P(x))) <-> (EX x:A. ~P(x))"
         "(ALL x:0.P(x)) <-> True"
         "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i. P(x))"
         "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B. P(x))"
         "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))"
         "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))"
    by blast+

    lemma ball_simps2:
         "(ALL x:A. P & Q(x))   <-> (A=0 | P) & (ALL x:A. Q(x))"
         "(ALL x:A. P | Q(x))   <-> (P | (ALL x:A. Q(x)))"
         "(ALL x:A. P --> Q(x)) <-> (P --> (ALL x:A. Q(x)))"
    by blast+

    lemma ball_simps3:
         "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))"
    by blast+

    lemmas ball_simps [simp] = ball_simps1 ball_simps2 ball_simps3

    lemma ball_conj_distrib:
        "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))"
    by blast

    subsection{*Miniscoping of the Bounded Existential Quantifier*}

    lemma bex_simps1:
         "(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)"
         "(EX x:A. P(x) | Q) <-> (EX x:A. P(x)) | (A~=0 & Q)"
         "(EX x:A. P(x) --> Q) <-> ((ALL x:A. P(x)) --> (A~=0 & Q))"
         "(EX x:0.P(x)) <-> False"
         "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))"
         "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))"
         "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))"
         "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y.  P(x))"
         "(~(EX x:A. P(x))) <-> (ALL x:A. ~P(x))"
    by blast+

    lemma bex_simps2:
         "(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))"
         "(EX x:A. P | Q(x)) <-> (A~=0 & P) | (EX x:A. Q(x))"
         "(EX x:A. P --> Q(x)) <-> ((A=0 | P) --> (EX x:A. Q(x)))"
    by blast+

    lemma bex_simps3:
         "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))"
    by blast

    lemmas bex_simps [simp] = bex_simps1 bex_simps2 bex_simps3

    lemma bex_disj_distrib:
        "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))"
    by blast

    (** One-point rule for bounded quantifiers: see HOL/Set.ML **)

    lemma bex_triv_one_point1 [simp]: "(EX x:A. x=a) <-> (a:A)"
    by blast

    lemma bex_triv_one_point2 [simp]: "(EX x:A. a=x) <-> (a:A)"
    by blast

    lemma bex_one_point1 [simp]: "(EX x:A. x=a & P(x)) <-> (a:A & P(a))"
    by blast

    lemma bex_one_point2 [simp]: "(EX x:A. a=x & P(x)) <-> (a:A & P(a))"
    by blast

    lemma ball_one_point1 [simp]: "(ALL x:A. x=a --> P(x)) <-> (a:A --> P(a))"
    by blast

    lemma ball_one_point2 [simp]: "(ALL x:A. a=x --> P(x)) <-> (a:A --> P(a))"
    by blast

    subsection{*Miniscoping of the Replacement Operator*}

    text{*These cover both @{term Replace} and @{term Collect}*}
    lemma Rep_simps [simp]:
         "{x. y:0, R(x,y)} = 0"
         "{x:0. P(x)} = 0"
         "{x:A. Q} = (if Q then A else 0)"
         "RepFun(0,f) = 0"
         "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))"
         "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"
    by (simp_all, blast+)

    subsection{*Miniscoping of Unions*}

    lemma UN_simps1:
         "(UN x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, UN x:C. B(x)))"
         "(UN x:C. A(x) Un B')   = (if C=0 then 0 else (UN x:C. A(x)) Un B')"
         "(UN x:C. A' Un B(x))   = (if C=0 then 0 else A' Un (UN x:C. B(x)))"
         "(UN x:C. A(x) Int B')  = ((UN x:C. A(x)) Int B')"
         "(UN x:C. A' Int B(x))  = (A' Int (UN x:C. B(x)))"
         "(UN x:C. A(x) - B')    = ((UN x:C. A(x)) - B')"
         "(UN x:C. A' - B(x))    = (if C=0 then 0 else A' - (INT x:C. B(x)))"
    apply (simp_all add: Inter_def)
    apply (blast intro!: equalityI )+
    done

    lemma UN_simps2:
          "(UN x: Union(A). B(x)) = (UN y:A. UN x:y. B(x))"
          "(UN z: (UN x:A. B(x)). C(z)) = (UN  x:A. UN z: B(x). C(z))"
          "(UN x: RepFun(A,f). B(x))     = (UN a:A. B(f(a)))"
    by blast+

    lemmas UN_simps [simp] = UN_simps1 UN_simps2

    text{*Opposite of miniscoping: pull the operator out*}

    lemma UN_extend_simps1:
         "(UN x:C. A(x)) Un B   = (if C=0 then B else (UN x:C. A(x) Un B))"
         "((UN x:C. A(x)) Int B) = (UN x:C. A(x) Int B)"
         "((UN x:C. A(x)) - B) = (UN x:C. A(x) - B)"
    apply simp_all
    apply blast+
    done

    lemma UN_extend_simps2:
         "cons(a, UN x:C. B(x)) = (if C=0 then {a} else (UN x:C. cons(a, B(x))))"
         "A Un (UN x:C. B(x))   = (if C=0 then A else (UN x:C. A Un B(x)))"
         "(A Int (UN x:C. B(x))) = (UN x:C. A Int B(x))"
         "A - (INT x:C. B(x))    = (if C=0 then A else (UN x:C. A - B(x)))"
         "(UN y:A. UN x:y. B(x)) = (UN x: Union(A). B(x))"
         "(UN a:A. B(f(a))) = (UN x: RepFun(A,f). B(x))"
    apply (simp_all add: Inter_def)
    apply (blast intro!: equalityI)+
    done

    lemma UN_UN_extend:
         "(UN  x:A. UN z: B(x). C(z)) = (UN z: (UN x:A. B(x)). C(z))"
    by blast

    lemmas UN_extend_simps = UN_extend_simps1 UN_extend_simps2 UN_UN_extend

    subsection{*Miniscoping of Intersections*}

    lemma INT_simps1:
         "(INT x:C. A(x) Int B) = (INT x:C. A(x)) Int B"
         "(INT x:C. A(x) - B)   = (INT x:C. A(x)) - B"
         "(INT x:C. A(x) Un B)  = (if C=0 then 0 else (INT x:C. A(x)) Un B)"
    by (simp_all add: Inter_def, blast+)

    lemma INT_simps2:
         "(INT x:C. A Int B(x)) = A Int (INT x:C. B(x))"
         "(INT x:C. A - B(x))   = (if C=0 then 0 else A - (UN x:C. B(x)))"
         "(INT x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, INT x:C. B(x)))"
         "(INT x:C. A Un B(x))  = (if C=0 then 0 else A Un (INT x:C. B(x)))"
    apply (simp_all add: Inter_def)
    apply (blast intro!: equalityI)+
    done

    lemmas INT_simps [simp] = INT_simps1 INT_simps2

    text{*Opposite of miniscoping: pull the operator out*}

    lemma INT_extend_simps1:
         "(INT x:C. A(x)) Int B = (INT x:C. A(x) Int B)"
         "(INT x:C. A(x)) - B = (INT x:C. A(x) - B)"
         "(INT x:C. A(x)) Un B  = (if C=0 then B else (INT x:C. A(x) Un B))"
    apply (simp_all add: Inter_def, blast+)
    done

    lemma INT_extend_simps2:
         "A Int (INT x:C. B(x)) = (INT x:C. A Int B(x))"
         "A - (UN x:C. B(x))   = (if C=0 then A else (INT x:C. A - B(x)))"
         "cons(a, INT x:C. B(x)) = (if C=0 then {a} else (INT x:C. cons(a, B(x))))"
         "A Un (INT x:C. B(x))  = (if C=0 then A else (INT x:C. A Un B(x)))"
    apply (simp_all add: Inter_def)
    apply (blast intro!: equalityI)+
    done

    lemmas INT_extend_simps = INT_extend_simps1 INT_extend_simps2

    subsection{*Other simprules*}

    (*** Miniscoping: pushing in big Unions, Intersections, quantifiers, etc. ***)

    lemma misc_simps [simp]:
         "0 Un A = A"
         "A Un 0 = A"
         "0 Int A = 0"
         "A Int 0 = 0"
         "0 - A = 0"
         "A - 0 = A"
         "Union(0) = 0"
         "Union(cons(b,A)) = b Un Union(A)"
         "Inter({b}) = b"
    by blast+

    ML
    {*
    val Upair_iff = thm "Upair_iff";
    val UpairI1 = thm "UpairI1";
    val UpairI2 = thm "UpairI2";
    val UpairE = thm "UpairE";
    val Un_iff = thm "Un_iff";
    val UnI1 = thm "UnI1";
    val UnI2 = thm "UnI2";
    val UnE = thm "UnE";
    val UnE' = thm "UnE'";
    val UnCI = thm "UnCI";
    val Int_iff = thm "Int_iff";
    val IntI = thm "IntI";
    val IntD1 = thm "IntD1";
    val IntD2 = thm "IntD2";
    val IntE = thm "IntE";
    val Diff_iff = thm "Diff_iff";
    val DiffI = thm "DiffI";
    val DiffD1 = thm "DiffD1";
    val DiffD2 = thm "DiffD2";
    val DiffE = thm "DiffE";
    val cons_iff = thm "cons_iff";
    val consI1 = thm "consI1";
    val consI2 = thm "consI2";
    val consE = thm "consE";
    val consE' = thm "consE'";
    val consCI = thm "consCI";
    val cons_not_0 = thm "cons_not_0";
    val cons_neq_0 = thm "cons_neq_0";
    val singleton_iff = thm "singleton_iff";
    val singletonI = thm "singletonI";
    val singletonE = thm "singletonE";
    val the_equality = thm "the_equality";
    val the_equality2 = thm "the_equality2";
    val theI = thm "theI";
    val the_0 = thm "the_0";
    val theI2 = thm "theI2";
    val if_true = thm "if_true";
    val if_false = thm "if_false";
    val if_cong = thm "if_cong";
    val if_weak_cong = thm "if_weak_cong";
    val if_P = thm "if_P";
    val if_not_P = thm "if_not_P";
    val split_if = thm "split_if";
    val split_if_eq1 = thm "split_if_eq1";
    val split_if_eq2 = thm "split_if_eq2";
    val split_if_mem1 = thm "split_if_mem1";
    val split_if_mem2 = thm "split_if_mem2";
    val if_iff = thm "if_iff";
    val if_type = thm "if_type";
    val mem_asym = thm "mem_asym";
    val mem_irrefl = thm "mem_irrefl";
    val mem_not_refl = thm "mem_not_refl";
    val mem_imp_not_eq = thm "mem_imp_not_eq";
    val succ_iff = thm "succ_iff";
    val succI1 = thm "succI1";
    val succI2 = thm "succI2";
    val succE = thm "succE";
    val succCI = thm "succCI";
    val succ_not_0 = thm "succ_not_0";
    val succ_neq_0 = thm "succ_neq_0";
    val succ_subsetD = thm "succ_subsetD";
    val succ_neq_self = thm "succ_neq_self";
    val succ_inject_iff = thm "succ_inject_iff";
    val succ_inject = thm "succ_inject";

    val split_ifs = thms "split_ifs";
    val ball_simps = thms "ball_simps";
    val bex_simps = thms "bex_simps";

    val ball_conj_distrib = thm "ball_conj_distrib";
    val bex_disj_distrib = thm "bex_disj_distrib";
    val bex_triv_one_point1 = thm "bex_triv_one_point1";
    val bex_triv_one_point2 = thm "bex_triv_one_point2";
    val bex_one_point1 = thm "bex_one_point1";
    val bex_one_point2 = thm "bex_one_point2";
    val ball_one_point1 = thm "ball_one_point1";
    val ball_one_point2 = thm "ball_one_point2";

    val Rep_simps = thms "Rep_simps";
    val misc_simps = thms "misc_simps";

    val UN_simps = thms "UN_simps";
    val INT_simps = thms "INT_simps";

    val UN_extend_simps = thms "UN_extend_simps";
    val INT_extend_simps = thms "INT_extend_simps";
    *}

    end

lemma atomize_ball:

      ∀x∈A1. P1(x) == (!!x. x ∈ A1 ==> P1(x))

### Unordered Pairs: constant @{term Upair}

lemma Upair_iff:

      c ∈ Upair(a, b) <-> c = a ∨ c = b

lemma UpairI1:

      a ∈ Upair(a, b)

lemma UpairI2:

      b ∈ Upair(a, b)

lemma UpairE:

      [| a ∈ Upair(b, c); a = b ==> P; a = c ==> P |] ==> P

### Rules for Binary Union, Defined via @{term Upair}

lemma Un_iff:

      c ∈ A ∪ B <-> c ∈ A ∨ c ∈ B

lemma UnI1:

      c ∈ A ==> c ∈ A ∪ B

lemma UnI2:

      c ∈ B ==> c ∈ A ∪ B

lemma UnE:

      [| c ∈ A ∪ B; c ∈ A ==> P; c ∈ B ==> P |] ==> P

lemma UnE':

      [| c ∈ A ∪ B; c ∈ A ==> P; [| c ∈ B; c ∉ A |] ==> P |] ==> P

lemma UnCI:

      (c ∉ B ==> c ∈ A) ==> c ∈ A ∪ B

### Rules for Binary Intersection, Defined via @{term Upair}

lemma Int_iff:

      c ∈ A ∩ B <-> c ∈ A ∧ c ∈ B

lemma IntI:

      [| c ∈ A; c ∈ B |] ==> c ∈ A ∩ B

lemma IntD1:

      c ∈ A ∩ B ==> c ∈ A

lemma IntD2:

      c ∈ A ∩ B ==> c ∈ B

lemma IntE:

      [| c ∈ A ∩ B; [| c ∈ A; c ∈ B |] ==> P |] ==> P

### Rules for Set Difference, Defined via @{term Upair}

lemma Diff_iff:

      c ∈ A - B <-> c ∈ A ∧ c ∉ B

lemma DiffI:

      [| c ∈ A; c ∉ B |] ==> c ∈ A - B

lemma DiffD1:

      c ∈ A - B ==> c ∈ A

lemma DiffD2:

      c ∈ A - B ==> c ∉ B

lemma DiffE:

      [| c ∈ A - B; [| c ∈ A; c ∉ B |] ==> P |] ==> P

### Rules for @{term cons}

lemma cons_iff:

      a ∈ cons(b, A) <-> a = b ∨ a ∈ A

lemma consI1:

      a ∈ cons(a, B)

lemma consI2:

      a ∈ B ==> a ∈ cons(b, B)

lemma consE:

      [| a ∈ cons(b, A); a = b ==> P; a ∈ A ==> P |] ==> P

lemma consE':

      [| a ∈ cons(b, A); a = b ==> P; [| a ∈ A; a ≠ b |] ==> P |] ==> P

lemma consCI:

      (a ∉ B ==> a = b) ==> a ∈ cons(b, B)

lemma cons_not_0:

      cons(a, B) ≠ 0

lemmas cons_neq_0:

      cons(a, B) = 0 ==> R

lemmas cons_neq_0:

      cons(a, B) = 0 ==> R

### Singletons

lemma singleton_iff:

      a ∈ {b} <-> a = b

lemma singletonI:

      a ∈ {a}

lemmas singletonE:

      [| a ∈ {b}; a = b ==> PROP W |] ==> PROP W

lemmas singletonE:

      [| a ∈ {b}; a = b ==> PROP W |] ==> PROP W

### Descriptions

lemma the_equality:

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

lemma the_equality2:

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

lemma theI:

      ∃!x. P(x) ==> P(THE x. P(x))

lemma the_0:

      ¬ (∃!x. P(x)) ==> (THE x. P(x)) = 0

lemma theI2:

      [| ¬ Q(0) ==> ∃!x. P(x); !!x. P(x) ==> Q(x) |] ==> Q(THE x. P(x))

lemma the_eq_trivial:

      (THE x. x = a) = a

lemma the_eq_trivial2:

      (THE x. a = x) = a

### Conditional Terms: @{text "if-then-else"}

lemma if_true:

      (if True then a else b) = a

lemma if_false:

      (if False then a else b) = b

lemma if_cong:

      [| P <-> Q; Q ==> a = c; ¬ Q ==> b = d |]
      ==> (if P then a else b) = (if Q then c else d)

lemma if_weak_cong:

      P <-> Q ==> (if P then x else y) = (if Q then x else y)

lemma if_P:

      P ==> (if P then a else b) = a

lemma if_not_P:

      ¬ P ==> (if P then a else b) = b

lemma split_if:

      P(if Q then x else y) <-> (Q --> P(x)) ∧ (¬ Q --> P(y))

lemmas split_if_eq1:

      (if Q then x else y) = b <-> (Q --> x = b) ∧ (¬ Q --> y = b)

lemmas split_if_eq1:

      (if Q then x else y) = b <-> (Q --> x = b) ∧ (¬ Q --> y = b)

lemmas split_if_eq2:

      a = (if Q then x else y) <-> (Q --> a = x) ∧ (¬ Q --> a = y)

lemmas split_if_eq2:

      a = (if Q then x else y) <-> (Q --> a = x) ∧ (¬ Q --> a = y)

lemmas split_if_mem1:

      (if Q then x else y) ∈ b <-> (Q --> x ∈ b) ∧ (¬ Q --> y ∈ b)

lemmas split_if_mem1:

      (if Q then x else y) ∈ b <-> (Q --> x ∈ b) ∧ (¬ Q --> y ∈ b)

lemmas split_if_mem2:

      a ∈ (if Q then x else y) <-> (Q --> a ∈ x) ∧ (¬ Q --> a ∈ y)

lemmas split_if_mem2:

      a ∈ (if Q then x else y) <-> (Q --> a ∈ x) ∧ (¬ Q --> a ∈ y)

lemmas split_ifs:

      (if Q then x else y) = b <-> (Q --> x = b) ∧ (¬ Q --> y = b)

      a = (if Q then x else y) <-> (Q --> a = x) ∧ (¬ Q --> a = y)

      (if Q then x else y) ∈ b <-> (Q --> x ∈ b) ∧ (¬ Q --> y ∈ b)

      a ∈ (if Q then x else y) <-> (Q --> a ∈ x) ∧ (¬ Q --> a ∈ y)

lemmas split_ifs:

      (if Q then x else y) = b <-> (Q --> x = b) ∧ (¬ Q --> y = b)

      a = (if Q then x else y) <-> (Q --> a = x) ∧ (¬ Q --> a = y)

      (if Q then x else y) ∈ b <-> (Q --> x ∈ b) ∧ (¬ Q --> y ∈ b)

      a ∈ (if Q then x else y) <-> (Q --> a ∈ x) ∧ (¬ Q --> a ∈ y)

lemma if_iff:

      a ∈ (if P then x else y) <-> P ∧ a ∈ x ∨ ¬ P ∧ a ∈ y

lemma if_type:

      [| P ==> a ∈ A; ¬ P ==> b ∈ A |] ==> (if P then a else b) ∈ A

lemma split_if_asm:

      P(if Q then x else y) <-> ¬ (Q ∧ ¬ P(x) ∨ ¬ Q ∧ ¬ P(y))

lemmas if_splits:

      P(if Q then x else y) <-> (Q --> P(x)) ∧ (¬ Q --> P(y))

      P(if Q then x else y) <-> ¬ (Q ∧ ¬ P(x) ∨ ¬ Q ∧ ¬ P(y))

lemmas if_splits:

      P(if Q then x else y) <-> (Q --> P(x)) ∧ (¬ Q --> P(y))

      P(if Q then x else y) <-> ¬ (Q ∧ ¬ P(x) ∨ ¬ Q ∧ ¬ P(y))

### Consequences of Foundation

lemma mem_asym:

      [| a ∈ b; ¬ P ==> b ∈ a |] ==> P

lemma mem_irrefl:

      a ∈ a ==> P

lemma mem_not_refl:

      a ∉ a

lemma mem_imp_not_eq:

      a ∈ A ==> a ≠ A

lemma eq_imp_not_mem:

      a = A ==> a ∉ A

### Rules for Successor

lemma succ_iff:

      i ∈ succ(j) <-> i = j ∨ i ∈ j

lemma succI1:

      i ∈ succ(i)

lemma succI2:

      i ∈ j ==> i ∈ succ(j)

lemma succE:

      [| i ∈ succ(j); i = j ==> P; i ∈ j ==> P |] ==> P

lemma succCI:

      (i ∉ j ==> i = j) ==> i ∈ succ(j)

lemma succ_not_0:

      succ(n) ≠ 0

lemmas succ_neq_0:

      succ(n) = 0 ==> R

lemmas succ_neq_0:

      succ(n) = 0 ==> R

lemmas succ_subsetD:

      succ(c) ⊆ B ==> c ∈ B

lemmas succ_subsetD:

      succ(c) ⊆ B ==> c ∈ B

lemmas succ_neq_self:

      succ(b) ≠ b

lemmas succ_neq_self:

      succ(b) ≠ b

lemma succ_inject_iff:

      succ(m) = succ(n) <-> m = n

lemmas succ_inject:

      succ(m) = succ(n) ==> m = n

lemmas succ_inject:

      succ(m) = succ(n) ==> m = n

### Miniscoping of the Bounded Universal Quantifier

lemma ball_simps1:

      (∀x∈A. P(x) ∧ Q) <-> (∀x∈A. P(x)) ∧ (A = 0 ∨ Q)

      (∀x∈A. P(x) ∨ Q) <-> (∀x∈A. P(x)) ∨ Q

      (∀x∈A. P(x) --> Q) <-> (∃x∈A. P(x)) --> Q

      ¬ (∀x∈A. P(x)) <-> (∃x∈A. ¬ P(x))

      (∀x∈0. P(x)) <-> True

      (∀x∈succ(i). P(x)) <-> P(i) ∧ (∀x∈i. P(x))

      (∀x∈cons(a, B). P(x)) <-> P(a) ∧ (∀x∈B. P(x))

      (∀x∈RepFun(A, f). P(x)) <-> (∀y∈A. P(f(y)))

      (∀x∈\<Union>A. P(x)) <-> (∀y∈A. ∀x∈y. P(x))

lemma ball_simps2:

      (∀x∈A. P ∧ Q(x)) <-> (A = 0 ∨ P) ∧ (∀x∈A. Q(x))

      (∀x∈A. P ∨ Q(x)) <-> P ∨ (∀x∈A. Q(x))

      (∀x∈A. P --> Q(x)) <-> P --> (∀x∈A. Q(x))

lemma ball_simps3:

      (∀x∈Collect(A, Q). P(x)) <-> (∀x∈A. Q(x) --> P(x))

lemmas ball_simps:

      (∀x∈A. P(x) ∧ Q) <-> (∀x∈A. P(x)) ∧ (A = 0 ∨ Q)

      (∀x∈A. P(x) ∨ Q) <-> (∀x∈A. P(x)) ∨ Q

      (∀x∈A. P(x) --> Q) <-> (∃x∈A. P(x)) --> Q

      ¬ (∀x∈A. P(x)) <-> (∃x∈A. ¬ P(x))

      (∀x∈0. P(x)) <-> True

      (∀x∈succ(i). P(x)) <-> P(i) ∧ (∀x∈i. P(x))

      (∀x∈cons(a, B). P(x)) <-> P(a) ∧ (∀x∈B. P(x))

      (∀x∈RepFun(A, f). P(x)) <-> (∀y∈A. P(f(y)))

      (∀x∈\<Union>A. P(x)) <-> (∀y∈A. ∀x∈y. P(x))

      (∀x∈A. P ∧ Q(x)) <-> (A = 0 ∨ P) ∧ (∀x∈A. Q(x))

      (∀x∈A. P ∨ Q(x)) <-> P ∨ (∀x∈A. Q(x))

      (∀x∈A. P --> Q(x)) <-> P --> (∀x∈A. Q(x))

      (∀x∈Collect(A, Q). P(x)) <-> (∀x∈A. Q(x) --> P(x))

lemmas ball_simps:

      (∀x∈A. P(x) ∧ Q) <-> (∀x∈A. P(x)) ∧ (A = 0 ∨ Q)

      (∀x∈A. P(x) ∨ Q) <-> (∀x∈A. P(x)) ∨ Q

      (∀x∈A. P(x) --> Q) <-> (∃x∈A. P(x)) --> Q

      ¬ (∀x∈A. P(x)) <-> (∃x∈A. ¬ P(x))

      (∀x∈0. P(x)) <-> True

      (∀x∈succ(i). P(x)) <-> P(i) ∧ (∀x∈i. P(x))

      (∀x∈cons(a, B). P(x)) <-> P(a) ∧ (∀x∈B. P(x))

      (∀x∈RepFun(A, f). P(x)) <-> (∀y∈A. P(f(y)))

      (∀x∈\<Union>A. P(x)) <-> (∀y∈A. ∀x∈y. P(x))

      (∀x∈A. P ∧ Q(x)) <-> (A = 0 ∨ P) ∧ (∀x∈A. Q(x))

      (∀x∈A. P ∨ Q(x)) <-> P ∨ (∀x∈A. Q(x))

      (∀x∈A. P --> Q(x)) <-> P --> (∀x∈A. Q(x))

      (∀x∈Collect(A, Q). P(x)) <-> (∀x∈A. Q(x) --> P(x))

lemma ball_conj_distrib:

      (∀x∈A. P(x) ∧ Q(x)) <-> (∀x∈A. P(x)) ∧ (∀x∈A. Q(x))

### Miniscoping of the Bounded Existential Quantifier

lemma bex_simps1:

      (∃x∈A. P(x) ∧ Q) <-> (∃x∈A. P(x)) ∧ Q

      (∃x∈A. P(x) ∨ Q) <-> (∃x∈A. P(x)) ∨ A ≠ 0 ∧ Q

      (∃x∈A. P(x) --> Q) <-> (∀x∈A. P(x)) --> A ≠ 0 ∧ Q

      (∃x∈0. P(x)) <-> False

      (∃x∈succ(i). P(x)) <-> P(i) ∨ (∃x∈i. P(x))

      (∃x∈cons(a, B). P(x)) <-> P(a) ∨ (∃x∈B. P(x))

      (∃x∈RepFun(A, f). P(x)) <-> (∃y∈A. P(f(y)))

      (∃x∈\<Union>A. P(x)) <-> (∃y∈A. ∃x∈y. P(x))

      ¬ (∃x∈A. P(x)) <-> (∀x∈A. ¬ P(x))

lemma bex_simps2:

      (∃x∈A. P ∧ Q(x)) <-> P ∧ (∃x∈A. Q(x))

      (∃x∈A. P ∨ Q(x)) <-> A ≠ 0 ∧ P ∨ (∃x∈A. Q(x))

      (∃x∈A. P --> Q(x)) <-> A = 0 ∨ P --> (∃x∈A. Q(x))

lemma bex_simps3:

      (∃x∈Collect(A, Q). P(x)) <-> (∃x∈A. Q(x) ∧ P(x))

lemmas bex_simps:

      (∃x∈A. P(x) ∧ Q) <-> (∃x∈A. P(x)) ∧ Q

      (∃x∈A. P(x) ∨ Q) <-> (∃x∈A. P(x)) ∨ A ≠ 0 ∧ Q

      (∃x∈A. P(x) --> Q) <-> (∀x∈A. P(x)) --> A ≠ 0 ∧ Q

      (∃x∈0. P(x)) <-> False

      (∃x∈succ(i). P(x)) <-> P(i) ∨ (∃x∈i. P(x))

      (∃x∈cons(a, B). P(x)) <-> P(a) ∨ (∃x∈B. P(x))

      (∃x∈RepFun(A, f). P(x)) <-> (∃y∈A. P(f(y)))

      (∃x∈\<Union>A. P(x)) <-> (∃y∈A. ∃x∈y. P(x))

      ¬ (∃x∈A. P(x)) <-> (∀x∈A. ¬ P(x))

      (∃x∈A. P ∧ Q(x)) <-> P ∧ (∃x∈A. Q(x))

      (∃x∈A. P ∨ Q(x)) <-> A ≠ 0 ∧ P ∨ (∃x∈A. Q(x))

      (∃x∈A. P --> Q(x)) <-> A = 0 ∨ P --> (∃x∈A. Q(x))

      (∃x∈Collect(A, Q). P(x)) <-> (∃x∈A. Q(x) ∧ P(x))

lemmas bex_simps:

      (∃x∈A. P(x) ∧ Q) <-> (∃x∈A. P(x)) ∧ Q

      (∃x∈A. P(x) ∨ Q) <-> (∃x∈A. P(x)) ∨ A ≠ 0 ∧ Q

      (∃x∈A. P(x) --> Q) <-> (∀x∈A. P(x)) --> A ≠ 0 ∧ Q

      (∃x∈0. P(x)) <-> False

      (∃x∈succ(i). P(x)) <-> P(i) ∨ (∃x∈i. P(x))

      (∃x∈cons(a, B). P(x)) <-> P(a) ∨ (∃x∈B. P(x))

      (∃x∈RepFun(A, f). P(x)) <-> (∃y∈A. P(f(y)))

      (∃x∈\<Union>A. P(x)) <-> (∃y∈A. ∃x∈y. P(x))

      ¬ (∃x∈A. P(x)) <-> (∀x∈A. ¬ P(x))

      (∃x∈A. P ∧ Q(x)) <-> P ∧ (∃x∈A. Q(x))

      (∃x∈A. P ∨ Q(x)) <-> A ≠ 0 ∧ P ∨ (∃x∈A. Q(x))

      (∃x∈A. P --> Q(x)) <-> A = 0 ∨ P --> (∃x∈A. Q(x))

      (∃x∈Collect(A, Q). P(x)) <-> (∃x∈A. Q(x) ∧ P(x))

lemma bex_disj_distrib:

      (∃x∈A. P(x) ∨ Q(x)) <-> (∃x∈A. P(x)) ∨ (∃x∈A. Q(x))

lemma bex_triv_one_point1:

      (∃x∈A. x = a) <-> a ∈ A

lemma bex_triv_one_point2:

      (∃x∈A. a = x) <-> a ∈ A

lemma bex_one_point1:

      (∃x∈A. x = a ∧ P(x)) <-> a ∈ A ∧ P(a)

lemma bex_one_point2:

      (∃x∈A. a = x ∧ P(x)) <-> a ∈ A ∧ P(a)

lemma ball_one_point1:

      (∀x∈A. x = a --> P(x)) <-> a ∈ A --> P(a)

lemma ball_one_point2:

      (∀x∈A. a = x --> P(x)) <-> a ∈ A --> P(a)

### Miniscoping of the Replacement Operator

lemma Rep_simps:

      {x . y ∈ 0, R(x, y)} = 0

      {x ∈ 0 . P(x)} = 0

      {x ∈ A . Q} = (if Q then A else 0)

      RepFun(0, f) = 0

      RepFun(succ(i), f) = cons(f(i), RepFun(i, f))

      RepFun(cons(a, B), f) = cons(f(a), RepFun(B, f))

### Miniscoping of Unions

lemma UN_simps1:

      (\<Union>x∈C. cons(a, B(x))) = (if C = 0 then 0 else cons(a, \<Union>x∈C. B(x)))

      (\<Union>x∈C. A(x) ∪ B') = (if C = 0 then 0 else (\<Union>x∈C. A(x)) ∪ B')

      (\<Union>x∈C. A' ∪ B(x)) = (if C = 0 then 0 else A' ∪ (\<Union>x∈C. B(x)))

      (\<Union>x∈C. A(x) ∩ B') = (\<Union>x∈C. A(x)) ∩ B'

      (\<Union>x∈C. A' ∩ B(x)) = A' ∩ (\<Union>x∈C. B(x))

      (\<Union>x∈C. A(x) - B') = (\<Union>x∈C. A(x)) - B'

      (\<Union>x∈C. A' - B(x)) = (if C = 0 then 0 else A' - (\<Inter>x∈C. B(x)))

lemma UN_simps2:

      (\<Union>x∈\<Union>A. B(x)) = (\<Union>y∈A. \<Union>x∈y. B(x))

      (\<Union>z∈\<Union>x∈A. B(x). C(z)) = (\<Union>x∈A. \<Union>z∈B(x). C(z))

      (\<Union>x∈RepFun(A, f). B(x)) = (\<Union>a∈A. B(f(a)))

lemmas UN_simps:

      (\<Union>x∈C. cons(a, B(x))) = (if C = 0 then 0 else cons(a, \<Union>x∈C. B(x)))

      (\<Union>x∈C. A(x) ∪ B') = (if C = 0 then 0 else (\<Union>x∈C. A(x)) ∪ B')

      (\<Union>x∈C. A' ∪ B(x)) = (if C = 0 then 0 else A' ∪ (\<Union>x∈C. B(x)))

      (\<Union>x∈C. A(x) ∩ B') = (\<Union>x∈C. A(x)) ∩ B'

      (\<Union>x∈C. A' ∩ B(x)) = A' ∩ (\<Union>x∈C. B(x))

      (\<Union>x∈C. A(x) - B') = (\<Union>x∈C. A(x)) - B'

      (\<Union>x∈C. A' - B(x)) = (if C = 0 then 0 else A' - (\<Inter>x∈C. B(x)))

      (\<Union>x∈\<Union>A. B(x)) = (\<Union>y∈A. \<Union>x∈y. B(x))

      (\<Union>z∈\<Union>x∈A. B(x). C(z)) = (\<Union>x∈A. \<Union>z∈B(x). C(z))

      (\<Union>x∈RepFun(A, f). B(x)) = (\<Union>a∈A. B(f(a)))

lemmas UN_simps:

      (\<Union>x∈C. cons(a, B(x))) = (if C = 0 then 0 else cons(a, \<Union>x∈C. B(x)))

      (\<Union>x∈C. A(x) ∪ B') = (if C = 0 then 0 else (\<Union>x∈C. A(x)) ∪ B')

      (\<Union>x∈C. A' ∪ B(x)) = (if C = 0 then 0 else A' ∪ (\<Union>x∈C. B(x)))

      (\<Union>x∈C. A(x) ∩ B') = (\<Union>x∈C. A(x)) ∩ B'

      (\<Union>x∈C. A' ∩ B(x)) = A' ∩ (\<Union>x∈C. B(x))

      (\<Union>x∈C. A(x) - B') = (\<Union>x∈C. A(x)) - B'

      (\<Union>x∈C. A' - B(x)) = (if C = 0 then 0 else A' - (\<Inter>x∈C. B(x)))

      (\<Union>x∈\<Union>A. B(x)) = (\<Union>y∈A. \<Union>x∈y. B(x))

      (\<Union>z∈\<Union>x∈A. B(x). C(z)) = (\<Union>x∈A. \<Union>z∈B(x). C(z))

      (\<Union>x∈RepFun(A, f). B(x)) = (\<Union>a∈A. B(f(a)))

lemma UN_extend_simps1:

      (\<Union>x∈C. A(x)) ∪ B = (if C = 0 then B else \<Union>x∈C. A(x) ∪ B)

      (\<Union>x∈C. A(x)) ∩ B = (\<Union>x∈C. A(x) ∩ B)

      (\<Union>x∈C. A(x)) - B = (\<Union>x∈C. A(x) - B)

lemma UN_extend_simps2:

      cons(a, \<Union>x∈C. B(x)) = (if C = 0 then {a} else \<Union>x∈C. cons(a, B(x)))

      A ∪ (\<Union>x∈C. B(x)) = (if C = 0 then A else \<Union>x∈C. A ∪ B(x))

      A ∩ (\<Union>x∈C. B(x)) = (\<Union>x∈C. A ∩ B(x))

      A - (\<Inter>x∈C. B(x)) = (if C = 0 then A else \<Union>x∈C. A - B(x))

      (\<Union>y∈A. \<Union>x∈y. B(x)) = (\<Union>x∈\<Union>A. B(x))

      (\<Union>a∈A. B(f(a))) = (\<Union>x∈RepFun(A, f). B(x))

lemma UN_UN_extend:

      (\<Union>x∈A. \<Union>z∈B(x). C(z)) = (\<Union>z∈\<Union>x∈A. B(x). C(z))

lemmas UN_extend_simps:

      (\<Union>x∈C. A(x)) ∪ B = (if C = 0 then B else \<Union>x∈C. A(x) ∪ B)

      (\<Union>x∈C. A(x)) ∩ B = (\<Union>x∈C. A(x) ∩ B)

      (\<Union>x∈C. A(x)) - B = (\<Union>x∈C. A(x) - B)

      cons(a, \<Union>x∈C. B(x)) = (if C = 0 then {a} else \<Union>x∈C. cons(a, B(x)))

      A ∪ (\<Union>x∈C. B(x)) = (if C = 0 then A else \<Union>x∈C. A ∪ B(x))

      A ∩ (\<Union>x∈C. B(x)) = (\<Union>x∈C. A ∩ B(x))

      A - (\<Inter>x∈C. B(x)) = (if C = 0 then A else \<Union>x∈C. A - B(x))

      (\<Union>y∈A. \<Union>x∈y. B(x)) = (\<Union>x∈\<Union>A. B(x))

      (\<Union>a∈A. B(f(a))) = (\<Union>x∈RepFun(A, f). B(x))

      (\<Union>x∈A. \<Union>z∈B(x). C(z)) = (\<Union>z∈\<Union>x∈A. B(x). C(z))

lemmas UN_extend_simps:

      (\<Union>x∈C. A(x)) ∪ B = (if C = 0 then B else \<Union>x∈C. A(x) ∪ B)

      (\<Union>x∈C. A(x)) ∩ B = (\<Union>x∈C. A(x) ∩ B)

      (\<Union>x∈C. A(x)) - B = (\<Union>x∈C. A(x) - B)

      cons(a, \<Union>x∈C. B(x)) = (if C = 0 then {a} else \<Union>x∈C. cons(a, B(x)))

      A ∪ (\<Union>x∈C. B(x)) = (if C = 0 then A else \<Union>x∈C. A ∪ B(x))

      A ∩ (\<Union>x∈C. B(x)) = (\<Union>x∈C. A ∩ B(x))

      A - (\<Inter>x∈C. B(x)) = (if C = 0 then A else \<Union>x∈C. A - B(x))

      (\<Union>y∈A. \<Union>x∈y. B(x)) = (\<Union>x∈\<Union>A. B(x))

      (\<Union>a∈A. B(f(a))) = (\<Union>x∈RepFun(A, f). B(x))

      (\<Union>x∈A. \<Union>z∈B(x). C(z)) = (\<Union>z∈\<Union>x∈A. B(x). C(z))

### Miniscoping of Intersections

lemma INT_simps1:

      (\<Inter>x∈C. A(x) ∩ B) = (\<Inter>x∈C. A(x)) ∩ B

      (\<Inter>x∈C. A(x) - B) = (\<Inter>x∈C. A(x)) - B

      (\<Inter>x∈C. A(x) ∪ B) = (if C = 0 then 0 else (\<Inter>x∈C. A(x)) ∪ B)

lemma INT_simps2:

      (\<Inter>x∈C. A ∩ B(x)) = A ∩ (\<Inter>x∈C. B(x))

      (\<Inter>x∈C. A - B(x)) = (if C = 0 then 0 else A - (\<Union>x∈C. B(x)))

      (\<Inter>x∈C. cons(a, B(x))) = (if C = 0 then 0 else cons(a, \<Inter>x∈C. B(x)))

      (\<Inter>x∈C. A ∪ B(x)) = (if C = 0 then 0 else A ∪ (\<Inter>x∈C. B(x)))

lemmas INT_simps:

      (\<Inter>x∈C. A(x) ∩ B) = (\<Inter>x∈C. A(x)) ∩ B

      (\<Inter>x∈C. A(x) - B) = (\<Inter>x∈C. A(x)) - B

      (\<Inter>x∈C. A(x) ∪ B) = (if C = 0 then 0 else (\<Inter>x∈C. A(x)) ∪ B)

      (\<Inter>x∈C. A ∩ B(x)) = A ∩ (\<Inter>x∈C. B(x))

      (\<Inter>x∈C. A - B(x)) = (if C = 0 then 0 else A - (\<Union>x∈C. B(x)))

      (\<Inter>x∈C. cons(a, B(x))) = (if C = 0 then 0 else cons(a, \<Inter>x∈C. B(x)))

      (\<Inter>x∈C. A ∪ B(x)) = (if C = 0 then 0 else A ∪ (\<Inter>x∈C. B(x)))

lemmas INT_simps:

      (\<Inter>x∈C. A(x) ∩ B) = (\<Inter>x∈C. A(x)) ∩ B

      (\<Inter>x∈C. A(x) - B) = (\<Inter>x∈C. A(x)) - B

      (\<Inter>x∈C. A(x) ∪ B) = (if C = 0 then 0 else (\<Inter>x∈C. A(x)) ∪ B)

      (\<Inter>x∈C. A ∩ B(x)) = A ∩ (\<Inter>x∈C. B(x))

      (\<Inter>x∈C. A - B(x)) = (if C = 0 then 0 else A - (\<Union>x∈C. B(x)))

      (\<Inter>x∈C. cons(a, B(x))) = (if C = 0 then 0 else cons(a, \<Inter>x∈C. B(x)))

      (\<Inter>x∈C. A ∪ B(x)) = (if C = 0 then 0 else A ∪ (\<Inter>x∈C. B(x)))

lemma INT_extend_simps1:

      (\<Inter>x∈C. A(x)) ∩ B = (\<Inter>x∈C. A(x) ∩ B)

      (\<Inter>x∈C. A(x)) - B = (\<Inter>x∈C. A(x) - B)

      (\<Inter>x∈C. A(x)) ∪ B = (if C = 0 then B else \<Inter>x∈C. A(x) ∪ B)

lemma INT_extend_simps2:

      A ∩ (\<Inter>x∈C. B(x)) = (\<Inter>x∈C. A ∩ B(x))

      A - (\<Union>x∈C. B(x)) = (if C = 0 then A else \<Inter>x∈C. A - B(x))

      cons(a, \<Inter>x∈C. B(x)) = (if C = 0 then {a} else \<Inter>x∈C. cons(a, B(x)))

      A ∪ (\<Inter>x∈C. B(x)) = (if C = 0 then A else \<Inter>x∈C. A ∪ B(x))

lemmas INT_extend_simps:

      (\<Inter>x∈C. A(x)) ∩ B = (\<Inter>x∈C. A(x) ∩ B)

      (\<Inter>x∈C. A(x)) - B = (\<Inter>x∈C. A(x) - B)

      (\<Inter>x∈C. A(x)) ∪ B = (if C = 0 then B else \<Inter>x∈C. A(x) ∪ B)

      A ∩ (\<Inter>x∈C. B(x)) = (\<Inter>x∈C. A ∩ B(x))

      A - (\<Union>x∈C. B(x)) = (if C = 0 then A else \<Inter>x∈C. A - B(x))

      cons(a, \<Inter>x∈C. B(x)) = (if C = 0 then {a} else \<Inter>x∈C. cons(a, B(x)))

      A ∪ (\<Inter>x∈C. B(x)) = (if C = 0 then A else \<Inter>x∈C. A ∪ B(x))

lemmas INT_extend_simps:

      (\<Inter>x∈C. A(x)) ∩ B = (\<Inter>x∈C. A(x) ∩ B)

      (\<Inter>x∈C. A(x)) - B = (\<Inter>x∈C. A(x) - B)

      (\<Inter>x∈C. A(x)) ∪ B = (if C = 0 then B else \<Inter>x∈C. A(x) ∪ B)

      A ∩ (\<Inter>x∈C. B(x)) = (\<Inter>x∈C. A ∩ B(x))

      A - (\<Union>x∈C. B(x)) = (if C = 0 then A else \<Inter>x∈C. A - B(x))

      cons(a, \<Inter>x∈C. B(x)) = (if C = 0 then {a} else \<Inter>x∈C. cons(a, B(x)))

      A ∪ (\<Inter>x∈C. B(x)) = (if C = 0 then A else \<Inter>x∈C. A ∪ B(x))

### Other simprules

lemma misc_simps:

      0 ∪ A = A

      A ∪ 0 = A

      0 ∩ A = 0

      A ∩ 0 = 0

      0 - A = 0

      A - 0 = A

      \<Union>0 = 0

      \<Union>cons(b, A) = b ∪ \<Union>A

      \<Inter>{b} = b