src/ZF/Ordinal.thy
changeset 13162 660a71e712af
parent 13155 dcbf6cb95534
child 13172 03a5afa7b888
     1.1 --- a/src/ZF/Ordinal.thy	Fri May 17 16:48:11 2002 +0200
     1.2 +++ b/src/ZF/Ordinal.thy	Fri May 17 16:54:25 2002 +0200
     1.3 @@ -456,6 +456,17 @@
     1.4  apply (blast intro: elim: ltE) +
     1.5  done
     1.6  
     1.7 +lemma succ_lt_iff: "succ(i) < j \<longleftrightarrow> i<j & succ(i) \<noteq> j"
     1.8 +apply auto 
     1.9 +apply (blast intro: lt_trans le_refl dest: lt_Ord) 
    1.10 +apply (frule lt_Ord) 
    1.11 +apply (rule not_le_iff_lt [THEN iffD1]) 
    1.12 +  apply (blast intro: lt_Ord2)
    1.13 + apply blast  
    1.14 +apply (simp add: lt_Ord lt_Ord2 le_iff) 
    1.15 +apply (blast dest: lt_asym) 
    1.16 +done
    1.17 +
    1.18  (** Union and Intersection **)
    1.19  
    1.20  lemma Un_upper1_le: "[| Ord(i); Ord(j) |] ==> i le i Un j"
    1.21 @@ -488,6 +499,26 @@
    1.22  apply (auto simp add: Int_commute le_subset_iff subset_Int_iff lt_Ord) 
    1.23  done
    1.24  
    1.25 +lemma Ord_Un_if:
    1.26 +     "[| Ord(i); Ord(j) |] ==> i \<union> j = (if j<i then i else j)"
    1.27 +by (simp add: not_lt_iff_le le_imp_subset leI
    1.28 +              subset_Un_iff [symmetric]  subset_Un_iff2 [symmetric]) 
    1.29 +
    1.30 +lemma succ_Un_distrib:
    1.31 +     "[| Ord(i); Ord(j) |] ==> succ(i \<union> j) = succ(i) \<union> succ(j)"
    1.32 +by (simp add: Ord_Un_if lt_Ord le_Ord2) 
    1.33 +
    1.34 +lemma lt_Un_iff:
    1.35 +     "[| Ord(i); Ord(j) |] ==> k < i \<union> j <-> k < i | k < j";
    1.36 +apply (simp add: Ord_Un_if not_lt_iff_le) 
    1.37 +apply (blast intro: leI lt_trans2)+ 
    1.38 +done
    1.39 +
    1.40 +lemma le_Un_iff:
    1.41 +     "[| Ord(i); Ord(j) |] ==> k \<le> i \<union> j <-> k \<le> i | k \<le> j";
    1.42 +by (simp add: succ_Un_distrib lt_Un_iff [symmetric]) 
    1.43 +
    1.44 +
    1.45  (*FIXME: the Intersection duals are missing!*)
    1.46  
    1.47  (*** Results about limits ***)
    1.48 @@ -600,6 +631,14 @@
    1.49  apply (erule Ord_cases, blast+)
    1.50  done
    1.51  
    1.52 +(*special induction rules for the "induct" method*)
    1.53 +lemmas Ord_induct = Ord_induct [consumes 2]
    1.54 +  and Ord_induct_rule = Ord_induct [rule_format, consumes 2]
    1.55 +  and trans_induct = trans_induct [consumes 1]
    1.56 +  and trans_induct_rule = trans_induct [rule_format, consumes 1]
    1.57 +  and trans_induct3 = trans_induct3 [case_names 0 succ limit, consumes 1]
    1.58 +  and trans_induct3_rule = trans_induct3 [rule_format, case_names 0 succ limit, consumes 1]
    1.59 +
    1.60  ML 
    1.61  {*
    1.62  val Memrel_def = thm "Memrel_def";