src/ZF/ord.ML
changeset 14 1c0926788772
parent 6 8ce8c4d13d4d
child 30 d49df4181f0d
equal deleted inserted replaced
13:b73f7e42135e 14:1c0926788772
    45 by (fast_tac (ZF_cs addSDs [prem1 RS Transset_Pair_D]) 1);
    45 by (fast_tac (ZF_cs addSDs [prem1 RS Transset_Pair_D]) 1);
    46 val Transset_includes_range = result();
    46 val Transset_includes_range = result();
    47 
    47 
    48 val [prem1,prem2] = goalw (merge_theories(Ord.thy,Sum.thy)) [sum_def]
    48 val [prem1,prem2] = goalw (merge_theories(Ord.thy,Sum.thy)) [sum_def]
    49     "[| Transset(C); A+B <= C |] ==> A <= C & B <= C";
    49     "[| Transset(C); A+B <= C |] ==> A <= C & B <= C";
    50 br (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1;
    50 by (rtac (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1);
    51 by (REPEAT (etac (prem1 RS Transset_includes_range) 1
    51 by (REPEAT (etac (prem1 RS Transset_includes_range) 1
    52      ORELSE resolve_tac [conjI, singletonI] 1));
    52      ORELSE resolve_tac [conjI, singletonI] 1));
    53 val Transset_includes_summands = result();
    53 val Transset_includes_summands = result();
    54 
    54 
    55 val [prem] = goalw (merge_theories(Ord.thy,Sum.thy)) [sum_def]
    55 val [prem] = goalw (merge_theories(Ord.thy,Sum.thy)) [sum_def]
    56     "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
    56     "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
    57 br (Int_Un_distrib RS ssubst) 1;
    57 by (rtac (Int_Un_distrib RS ssubst) 1);
    58 by (fast_tac (ZF_cs addSDs [prem RS Transset_Pair_D]) 1);
    58 by (fast_tac (ZF_cs addSDs [prem RS Transset_Pair_D]) 1);
    59 val Transset_sum_Int_subset = result();
    59 val Transset_sum_Int_subset = result();
    60 
    60 
    61 (** Closure properties **)
    61 (** Closure properties **)
    62 
    62 
   279 val [prem] = goal Ord.thy "Ord(i) ==> 0: succ(i)";
   279 val [prem] = goal Ord.thy "Ord(i) ==> 0: succ(i)";
   280 by (rtac (empty_subsetI RS Ord_member) 1);
   280 by (rtac (empty_subsetI RS Ord_member) 1);
   281 by (fast_tac ZF_cs 1);
   281 by (fast_tac ZF_cs 1);
   282 by (rtac (prem RS Ord_succ) 1);
   282 by (rtac (prem RS Ord_succ) 1);
   283 by (rtac Ord_0 1);
   283 by (rtac Ord_0 1);
   284 val Ord_0_mem_succ = result();
   284 val Ord_0_in_succ = result();
   285 
   285 
   286 goal Ord.thy "!!i j. [| Ord(i);  Ord(j) |] ==> j:i <-> j<=i & ~(i<=j)";
   286 goal Ord.thy "!!i j. [| Ord(i);  Ord(j) |] ==> j:i <-> j<=i & ~(i<=j)";
   287 by (rtac iffI 1);
   287 by (rtac iffI 1);
   288 by (rtac conjI 1);
   288 by (rtac conjI 1);
   289 by (etac OrdmemD 1);
   289 by (etac OrdmemD 1);
   291 by (etac subsetD 2);
   291 by (etac subsetD 2);
   292 by (REPEAT (eresolve_tac [asm_rl, conjE, Ord_member] 1));
   292 by (REPEAT (eresolve_tac [asm_rl, conjE, Ord_member] 1));
   293 val Ord_member_iff = result();
   293 val Ord_member_iff = result();
   294 
   294 
   295 goal Ord.thy "!!i. Ord(i) ==> 0:i  <-> ~ i=0";
   295 goal Ord.thy "!!i. Ord(i) ==> 0:i  <-> ~ i=0";
   296 be (Ord_0 RSN (2,Ord_member_iff) RS iff_trans) 1;
   296 by (etac (Ord_0 RSN (2,Ord_member_iff) RS iff_trans) 1);
   297 by (fast_tac eq_cs 1);
   297 by (fast_tac eq_cs 1);
   298 val Ord_0_member_iff = result();
   298 val Ord_0_member_iff = result();
   299 
   299 
   300 (** For ordinals, i: succ(j) means 'less-than or equals' **)
   300 (** For ordinals, i: succ(j) means 'less-than or equals' **)
   301 
   301 
   305 by (rtac (mem_anti_refl RS notI) 2);
   305 by (rtac (mem_anti_refl RS notI) 2);
   306 by (etac subsetD 2);
   306 by (etac subsetD 2);
   307 by (ALLGOALS (fast_tac ZF_cs));
   307 by (ALLGOALS (fast_tac ZF_cs));
   308 val member_succI = result();
   308 val member_succI = result();
   309 
   309 
       
   310 (*Recall Ord_succ_subsetI, namely  [| i:j;  Ord(j) |] ==> succ(i) <= j *)
   310 goalw Ord.thy [Transset_def,Ord_def]
   311 goalw Ord.thy [Transset_def,Ord_def]
   311     "!!i j. [| i : succ(j);  Ord(j) |] ==> i<=j";
   312     "!!i j. [| i : succ(j);  Ord(j) |] ==> i<=j";
   312 by (fast_tac ZF_cs 1);
   313 by (fast_tac ZF_cs 1);
   313 val member_succD = result();
   314 val member_succD = result();
   314 
   315 
   350 
   351 
   351 goal Ord.thy "!!i j. [| i<=j;  Ord(i);  Ord(j) |] ==> succ(i) <= succ(j)";
   352 goal Ord.thy "!!i j. [| i<=j;  Ord(i);  Ord(j) |] ==> succ(i) <= succ(j)";
   352 by (rtac (member_succI RS succ_mem_succI RS member_succD) 1);
   353 by (rtac (member_succI RS succ_mem_succI RS member_succD) 1);
   353 by (REPEAT (ares_tac [Ord_succ] 1));
   354 by (REPEAT (ares_tac [Ord_succ] 1));
   354 val Ord_succ_mono = result();
   355 val Ord_succ_mono = result();
       
   356 
       
   357 (** Union and Intersection **)
   355 
   358 
   356 goal Ord.thy "!!i j k. [| i:k;  j:k;  Ord(k) |] ==> i Un j : k";
   359 goal Ord.thy "!!i j k. [| i:k;  j:k;  Ord(k) |] ==> i Un j : k";
   357 by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);
   360 by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);
   358 by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
   361 by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
   359 by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1);
   362 by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1);