# HG changeset patch # User wenzelm # Date 1030439373 -7200 # Node ID ca6debb89d77e66fd6b04ecd570b6922a557330a # Parent 70de987e9fe3ce4c42c8c7044f282f575c3677b8 avoid duplicate fact bindings; diff -r 70de987e9fe3 -r ca6debb89d77 src/ZF/Ordinal.thy --- 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"; diff -r 70de987e9fe3 -r ca6debb89d77 src/ZF/QPair.thy --- 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= |] ==> P - |] ==> P" -by (simp add: QSigma_def, blast) - (** Elimination rules for :A*B -- introducing no eigenvariables **) lemma QSigmaE [elim!]: diff -r 70de987e9fe3 -r ca6debb89d77 src/ZF/Trancl.thy --- 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 ==> ~: r |] ==> irrefl(A,r)" by (simp add: irrefl_def) -lemma symI: "[| irrefl(A,r); x:A |] ==> ~: r" +lemma irreflE: "[| irrefl(A,r); x:A |] ==> ~: r" by (simp add: irrefl_def) subsubsection{*symmetry*} @@ -58,7 +58,7 @@ "[| !!x y.: r ==> : r |] ==> sym(r)" by (unfold sym_def, blast) -lemma antisymI: "[| sym(r); : r |] ==> : r" +lemma symE: "[| sym(r); : r |] ==> : 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]: "[| : r^*; !!x. x: field(r) ==> P(); !!x y z.[| P(); : r^*; : r |] ==> P() |] @@ -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]: "[| : r^*; P(a); !!y z.[| : r^*; : 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]: "[| : r^+; !!y. [| : r |] ==> P(y); !!y z.[| : r^+; : 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]: "[| :r^+; !!y. :r ==> P(y); !!y z. [| : r; : 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"; diff -r 70de987e9fe3 -r ca6debb89d77 src/ZF/Univ.thy --- 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 \ Vfrom(A,i); Limit(i) |] ==> {a} \ Vfrom(A,i)" apply (erule Limit_VfromE, assumption) diff -r 70de987e9fe3 -r ca6debb89d77 src/ZF/WF.thy --- 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. : 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. : 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)*)