# HG changeset patch # User lcp # Date 788197822 -3600 # Node ID 120edb26ee9322effcc54fc23b1fa59c1008f357 # Parent 778f0154666978fdf0b5a0b95645842229a257f0 Moved Transset_includes_summands and Transset_sum_Int_subset here from Ordinal.ML diff -r 778f01546669 -r 120edb26ee93 src/ZF/QUniv.ML --- a/src/ZF/QUniv.ML Fri Dec 23 16:49:48 1994 +0100 +++ b/src/ZF/QUniv.ML Fri Dec 23 16:50:22 1994 +0100 @@ -8,6 +8,21 @@ open QUniv; +(** Properties involving Transset and Sum **) + +val [prem1,prem2] = goalw QUniv.thy [sum_def] + "[| Transset(C); A+B <= C |] ==> A <= C & B <= C"; +by (rtac (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1); +by (REPEAT (etac (prem1 RS Transset_includes_range) 1 + ORELSE resolve_tac [conjI, singletonI] 1)); +qed "Transset_includes_summands"; + +val [prem] = goalw QUniv.thy [sum_def] + "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)"; +by (rtac (Int_Un_distrib RS ssubst) 1); +by (fast_tac (ZF_cs addSDs [prem RS Transset_Pair_D]) 1); +qed "Transset_sum_Int_subset"; + (** Introduction and elimination rules avoid tiresome folding/unfolding **) goalw QUniv.thy [quniv_def]