--- a/src/ZF/Ordinal.thy Tue Aug 27 11:07:54 2002 +0200
+++ b/src/ZF/Ordinal.thy Tue Aug 27 11:09:33 2002 +0200
@@ -328,11 +328,12 @@
done
(*Induction over an ordinal*)
-lemmas Ord_induct = Transset_induct [OF _ Ord_is_Transset]
+lemmas Ord_induct [consumes 2] = Transset_induct [OF _ Ord_is_Transset]
+lemmas Ord_induct_rule = Ord_induct [rule_format, consumes 2]
(*Induction over the class of ordinals -- a useful corollary of Ord_induct*)
-lemma trans_induct:
+lemma trans_induct [consumes 1]:
"[| Ord(i);
!!x.[| Ord(x); ALL y:x. P(y) |] ==> P(x) |]
==> P(i)"
@@ -340,6 +341,8 @@
apply (blast intro: Ord_succ [THEN Ord_in_Ord])
done
+lemmas trans_induct_rule = trans_induct [rule_format, consumes 1]
+
(*** Fundamental properties of the epsilon ordering (< on ordinals) ***)
@@ -684,7 +687,7 @@
|] ==> P"
by (drule Ord_cases_disj, blast)
-lemma trans_induct3:
+lemma trans_induct3 [case_names 0 succ limit, consumes 1]:
"[| Ord(i);
P(0);
!!x. [| Ord(x); P(x) |] ==> P(succ(x));
@@ -694,6 +697,8 @@
apply (erule Ord_cases, blast+)
done
+lemmas trans_induct3_rule = trans_induct3 [rule_format, case_names 0 succ limit, consumes 1]
+
text{*A set of ordinals is either empty, contains its own union, or its
union is a limit ordinal.*}
lemma Ord_set_cases:
@@ -721,14 +726,6 @@
apply (blast intro!: equalityI)
done
-(*special induction rules for the "induct" method*)
-lemmas Ord_induct = Ord_induct [consumes 2]
- and Ord_induct_rule = Ord_induct [rule_format, consumes 2]
- and trans_induct = trans_induct [consumes 1]
- and trans_induct_rule = trans_induct [rule_format, consumes 1]
- and trans_induct3 = trans_induct3 [case_names 0 succ limit, consumes 1]
- and trans_induct3_rule = trans_induct3 [rule_format, case_names 0 succ limit, consumes 1]
-
ML
{*
val Memrel_def = thm "Memrel_def";
--- a/src/ZF/QPair.thy Tue Aug 27 11:07:54 2002 +0200
+++ b/src/ZF/QPair.thy Tue Aug 27 11:09:33 2002 +0200
@@ -93,13 +93,6 @@
by (simp add: QSigma_def)
-(*The general elimination rule*)
-lemma QSigmaE:
- "[| c: QSigma(A,B);
- !!x y.[| x:A; y:B(x); c=<x;y> |] ==> P
- |] ==> P"
-by (simp add: QSigma_def, blast)
-
(** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
lemma QSigmaE [elim!]:
--- a/src/ZF/Trancl.thy Tue Aug 27 11:07:54 2002 +0200
+++ b/src/ZF/Trancl.thy Tue Aug 27 11:09:33 2002 +0200
@@ -49,7 +49,7 @@
"[| !!x. x:A ==> <x,x> ~: r |] ==> irrefl(A,r)"
by (simp add: irrefl_def)
-lemma symI: "[| irrefl(A,r); x:A |] ==> <x,x> ~: r"
+lemma irreflE: "[| irrefl(A,r); x:A |] ==> <x,x> ~: r"
by (simp add: irrefl_def)
subsubsection{*symmetry*}
@@ -58,7 +58,7 @@
"[| !!x y.<x,y>: r ==> <y,x>: r |] ==> sym(r)"
by (unfold sym_def, blast)
-lemma antisymI: "[| sym(r); <x,y>: r |] ==> <y,x>: r"
+lemma symE: "[| sym(r); <x,y>: r |] ==> <y,x>: r"
by (unfold sym_def, blast)
subsubsection{*antisymmetry*}
@@ -139,7 +139,7 @@
(** standard induction rule **)
-lemma rtrancl_full_induct:
+lemma rtrancl_full_induct [case_names initial step, consumes 1]:
"[| <a,b> : r^*;
!!x. x: field(r) ==> P(<x,x>);
!!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |] ==> P(<x,z>) |]
@@ -149,7 +149,7 @@
(*nice induction rule.
Tried adding the typing hypotheses y,z:field(r), but these
caused expensive case splits!*)
-lemma rtrancl_induct:
+lemma rtrancl_induct [case_names initial step, induct set: rtrancl]:
"[| <a,b> : r^*;
P(a);
!!y z.[| <a,y> : r^*; <y,z> : r; P(y) |] ==> P(z)
@@ -228,7 +228,7 @@
done
(*Nice induction rule for trancl*)
-lemma trancl_induct:
+lemma trancl_induct [case_names initial step, induct set: trancl]:
"[| <a,b> : r^+;
!!y. [| <a,y> : r |] ==> P(y);
!!y z.[| <a,y> : r^+; <y,z> : r; P(y) |] ==> P(z)
@@ -353,7 +353,7 @@
apply (safe dest!: trancl_converseD intro!: trancl_converseI)
done
-lemma converse_trancl_induct:
+lemma converse_trancl_induct [case_names initial step, consumes 1]:
"[| <a, b>:r^+; !!y. <y, b> :r ==> P(y);
!!y z. [| <y, z> : r; <z, b> : r^+; P(z) |] ==> P(y) |]
==> P(a)"
@@ -363,12 +363,6 @@
apply (auto simp add: trancl_converse)
done
-lemmas rtrancl_induct = rtrancl_induct [case_names initial step, induct set: rtrancl]
- and trancl_induct = trancl_induct [case_names initial step, induct set: trancl]
- and converse_trancl_induct = converse_trancl_induct [case_names initial step, consumes 1]
- and rtrancl_full_induct = rtrancl_full_induct [case_names initial step, consumes 1]
-
-
ML
{*
val refl_def = thm "refl_def";
--- a/src/ZF/Univ.thy Tue Aug 27 11:07:54 2002 +0200
+++ b/src/ZF/Univ.thy Tue Aug 27 11:09:33 2002 +0200
@@ -192,8 +192,6 @@
apply (blast intro: ltI Limit_is_Ord)
done
-lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard]
-
lemma singleton_in_VLimit:
"[| a \<in> Vfrom(A,i); Limit(i) |] ==> {a} \<in> Vfrom(A,i)"
apply (erule Limit_VfromE, assumption)
--- a/src/ZF/WF.thy Tue Aug 27 11:07:54 2002 +0200
+++ b/src/ZF/WF.thy Tue Aug 27 11:09:33 2002 +0200
@@ -100,7 +100,7 @@
(** Well-founded Induction **)
(*Consider the least z in domain(r) such that P(z) does not hold...*)
-lemma wf_induct:
+lemma wf_induct [induct set: wf]:
"[| wf(r);
!!x.[| ALL y. <y,x>: r --> P(y) |] ==> P(x)
|] ==> P(a)"
@@ -109,9 +109,7 @@
apply blast
done
-(*fixed up for induct method*)
-lemmas wf_induct = wf_induct [induct set: wf]
- and wf_induct_rule = wf_induct [rule_format, induct set: wf]
+lemmas wf_induct_rule = wf_induct [rule_format, induct set: wf]
(*The form of this rule is designed to match wfI*)
lemma wf_induct2:
@@ -125,7 +123,7 @@
lemma field_Int_square: "field(r Int A*A) <= A"
by blast
-lemma wf_on_induct:
+lemma wf_on_induct [consumes 2, induct set: wf_on]:
"[| wf[A](r); a:A;
!!x.[| x: A; ALL y:A. <y,x>: r --> P(y) |] ==> P(x)
|] ==> P(a)"
@@ -134,10 +132,8 @@
apply (rule field_Int_square, blast)
done
-(*fixed up for induct method*)
-lemmas wf_on_induct = wf_on_induct [consumes 2, induct set: wf_on]
- and wf_on_induct_rule =
- wf_on_induct [rule_format, consumes 2, induct set: wf_on]
+lemmas wf_on_induct_rule =
+ wf_on_induct [rule_format, consumes 2, induct set: wf_on]
(*If r allows well-founded induction then wf(r)*)