src/ZF/QUniv.ML
changeset 838 120edb26ee93
parent 803 4c8333ab3eae
child 1461 6bcb44e4d6e5
equal deleted inserted replaced
837:778f01546669 838:120edb26ee93
     5 
     5 
     6 For quniv.thy.  A small universe for lazy recursive types
     6 For quniv.thy.  A small universe for lazy recursive types
     7 *)
     7 *)
     8 
     8 
     9 open QUniv;
     9 open QUniv;
       
    10 
       
    11 (** Properties involving Transset and Sum **)
       
    12 
       
    13 val [prem1,prem2] = goalw QUniv.thy [sum_def]
       
    14     "[| Transset(C); A+B <= C |] ==> A <= C & B <= C";
       
    15 by (rtac (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1);
       
    16 by (REPEAT (etac (prem1 RS Transset_includes_range) 1
       
    17      ORELSE resolve_tac [conjI, singletonI] 1));
       
    18 qed "Transset_includes_summands";
       
    19 
       
    20 val [prem] = goalw QUniv.thy [sum_def]
       
    21     "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
       
    22 by (rtac (Int_Un_distrib RS ssubst) 1);
       
    23 by (fast_tac (ZF_cs addSDs [prem RS Transset_Pair_D]) 1);
       
    24 qed "Transset_sum_Int_subset";
    10 
    25 
    11 (** Introduction and elimination rules avoid tiresome folding/unfolding **)
    26 (** Introduction and elimination rules avoid tiresome folding/unfolding **)
    12 
    27 
    13 goalw QUniv.thy [quniv_def]
    28 goalw QUniv.thy [quniv_def]
    14     "!!X A. X <= univ(eclose(A)) ==> X : quniv(A)";
    29     "!!X A. X <= univ(eclose(A)) ==> X : quniv(A)";