src/ZF/Ordinal.thy
changeset 13534 ca6debb89d77
parent 13396 11219ca224ab
child 13544 895994073bdf
     1.1 --- a/src/ZF/Ordinal.thy	Tue Aug 27 11:07:54 2002 +0200
     1.2 +++ b/src/ZF/Ordinal.thy	Tue Aug 27 11:09:33 2002 +0200
     1.3 @@ -328,11 +328,12 @@
     1.4  done
     1.5  
     1.6  (*Induction over an ordinal*)
     1.7 -lemmas Ord_induct = Transset_induct [OF _ Ord_is_Transset]
     1.8 +lemmas Ord_induct [consumes 2] = Transset_induct [OF _ Ord_is_Transset]
     1.9 +lemmas Ord_induct_rule = Ord_induct [rule_format, consumes 2]
    1.10  
    1.11  (*Induction over the class of ordinals -- a useful corollary of Ord_induct*)
    1.12  
    1.13 -lemma trans_induct:
    1.14 +lemma trans_induct [consumes 1]:
    1.15      "[| Ord(i);  
    1.16          !!x.[| Ord(x);  ALL y:x. P(y) |] ==> P(x) |]
    1.17       ==>  P(i)"
    1.18 @@ -340,6 +341,8 @@
    1.19  apply (blast intro: Ord_succ [THEN Ord_in_Ord]) 
    1.20  done
    1.21  
    1.22 +lemmas trans_induct_rule = trans_induct [rule_format, consumes 1]
    1.23 +
    1.24  
    1.25  (*** Fundamental properties of the epsilon ordering (< on ordinals) ***)
    1.26  
    1.27 @@ -684,7 +687,7 @@
    1.28       |] ==> P"
    1.29  by (drule Ord_cases_disj, blast)  
    1.30  
    1.31 -lemma trans_induct3:
    1.32 +lemma trans_induct3 [case_names 0 succ limit, consumes 1]:
    1.33       "[| Ord(i);                 
    1.34           P(0);                   
    1.35           !!x. [| Ord(x);  P(x) |] ==> P(succ(x));        
    1.36 @@ -694,6 +697,8 @@
    1.37  apply (erule Ord_cases, blast+)
    1.38  done
    1.39  
    1.40 +lemmas trans_induct3_rule = trans_induct3 [rule_format, case_names 0 succ limit, consumes 1]
    1.41 +
    1.42  text{*A set of ordinals is either empty, contains its own union, or its
    1.43  union is a limit ordinal.*}
    1.44  lemma Ord_set_cases:
    1.45 @@ -721,14 +726,6 @@
    1.46  apply (blast intro!: equalityI)
    1.47  done
    1.48  
    1.49 -(*special induction rules for the "induct" method*)
    1.50 -lemmas Ord_induct = Ord_induct [consumes 2]
    1.51 -  and Ord_induct_rule = Ord_induct [rule_format, consumes 2]
    1.52 -  and trans_induct = trans_induct [consumes 1]
    1.53 -  and trans_induct_rule = trans_induct [rule_format, consumes 1]
    1.54 -  and trans_induct3 = trans_induct3 [case_names 0 succ limit, consumes 1]
    1.55 -  and trans_induct3_rule = trans_induct3 [rule_format, case_names 0 succ limit, consumes 1]
    1.56 -
    1.57  ML 
    1.58  {*
    1.59  val Memrel_def = thm "Memrel_def";