# HG changeset patch # User wenzelm # Date 1321816502 -3600 # Node ID 2a858377c3d2e2c395136613505087697a115d97 # Parent d5178f19b6718f1bb9a3f829fed048a8aaf9cfa0 eliminated obsolete "standard"; diff -r d5178f19b671 -r 2a858377c3d2 src/FOLP/IFOLP.thy --- a/src/FOLP/IFOLP.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/FOLP/IFOLP.thy Sun Nov 20 20:15:02 2011 +0100 @@ -504,7 +504,7 @@ lemmas pred_congs = pred1_cong pred2_cong pred3_cong (*special case for the equality predicate!*) -lemmas eq_cong = pred2_cong [where P = "op =", standard] +lemmas eq_cong = pred2_cong [where P = "op ="] (*** Simplifications of assumed implications. diff -r d5178f19b671 -r 2a858377c3d2 src/Sequents/LK.thy --- a/src/Sequents/LK.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/Sequents/LK.thy Sun Nov 20 20:15:02 2011 +0100 @@ -129,14 +129,14 @@ apply (tactic {* fast_tac LK_pack 1 *}) done -lemmas iff_reflection_F = P_iff_F [THEN iff_reflection, standard] +lemmas iff_reflection_F = P_iff_F [THEN iff_reflection] lemma P_iff_T: "|- P ==> |- (P <-> True)" apply (erule thinR [THEN cut]) apply (tactic {* fast_tac LK_pack 1 *}) done -lemmas iff_reflection_T = P_iff_T [THEN iff_reflection, standard] +lemmas iff_reflection_T = P_iff_T [THEN iff_reflection] lemma LK_extra_simps: diff -r d5178f19b671 -r 2a858377c3d2 src/Sequents/LK0.thy --- a/src/Sequents/LK0.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/Sequents/LK0.thy Sun Nov 20 20:15:02 2011 +0100 @@ -305,10 +305,10 @@ by (tactic {* safe_tac (LK_pack add_safes [@{thm subst}]) 1 *}) (* Symmetry of equality in hypotheses *) -lemmas symL = sym [THEN L_of_imp, standard] +lemmas symL = sym [THEN L_of_imp] (* Symmetry of equality in hypotheses *) -lemmas symR = sym [THEN R_of_imp, standard] +lemmas symR = sym [THEN R_of_imp] lemma transR: "[| $H|- $E, $F, a=b; $H|- $E, $F, b=c |] ==> $H|- $E, a=c, $F" by (rule trans [THEN R_of_imp, THEN mp_R]) diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/AC/HH.thy --- a/src/ZF/AC/HH.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/AC/HH.thy Sun Nov 20 20:15:02 2011 +0100 @@ -210,7 +210,7 @@ simplification is needed!*) lemmas bij_Least_HH_x = comp_bij [OF f_sing_lam_bij [OF _ lam_singI] - lam_sing_bij [THEN bij_converse_bij], standard] + lam_sing_bij [THEN bij_converse_bij]] subsection{*The proof of AC1 ==> WO2*} diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/AC/Hartog.thy --- a/src/ZF/AC/Hartog.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/AC/Hartog.thy Sun Nov 20 20:15:02 2011 +0100 @@ -65,7 +65,7 @@ apply (rule LeastI, auto) done -lemmas Hartog_lepoll_selfE = not_Hartog_lepoll_self [THEN notE, standard] +lemmas Hartog_lepoll_selfE = not_Hartog_lepoll_self [THEN notE] lemma Ord_Hartog: "Ord(Hartog(A))" by (unfold Hartog_def, rule Ord_Least) diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/AC/WO2_AC16.thy --- a/src/ZF/AC/WO2_AC16.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/AC/WO2_AC16.thy Sun Nov 20 20:15:02 2011 +0100 @@ -315,8 +315,7 @@ lemmas disj_Un_eqpoll_nat_sum = eqpoll_trans [THEN eqpoll_trans, - OF disj_Un_eqpoll_sum sum_eqpoll_cong nat_sum_eqpoll_sum, - standard]; + OF disj_Un_eqpoll_sum sum_eqpoll_cong nat_sum_eqpoll_sum]; lemma Un_in_Collect: "[| x \ Pow(A - B - h`i); x\m; diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/AC/WO6_WO1.thy --- a/src/ZF/AC/WO6_WO1.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/AC/WO6_WO1.thy Sun Nov 20 20:15:02 2011 +0100 @@ -217,10 +217,9 @@ apply (fast elim!: LeastI)+ done -lemmas nested_Least_instance = +lemmas nested_Least_instance = nested_LeastI [of "%g d. domain(uu(f,b,g,d)) \ 0 & - domain(uu(f,b,g,d)) \ m", - standard] (*generalizes the Variables!*) + domain(uu(f,b,g,d)) \ m"] for f b m lemma gg1_lepoll_m: "[| Ord(a); m \ nat; diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/Bool.thy --- a/src/ZF/Bool.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/Bool.thy Sun Nov 20 20:15:02 2011 +0100 @@ -53,7 +53,7 @@ by (simp add: bool_defs ) (** 1=0 ==> R **) -lemmas one_neq_0 = one_not_0 [THEN notE, standard] +lemmas one_neq_0 = one_not_0 [THEN notE] lemma boolE: "[| c: bool; c=1 ==> P; c=0 ==> P |] ==> P" @@ -82,17 +82,17 @@ lemma def_cond_0: "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d" by simp -lemmas not_1 = not_def [THEN def_cond_1, standard, simp] -lemmas not_0 = not_def [THEN def_cond_0, standard, simp] +lemmas not_1 = not_def [THEN def_cond_1, simp] +lemmas not_0 = not_def [THEN def_cond_0, simp] -lemmas and_1 = and_def [THEN def_cond_1, standard, simp] -lemmas and_0 = and_def [THEN def_cond_0, standard, simp] +lemmas and_1 = and_def [THEN def_cond_1, simp] +lemmas and_0 = and_def [THEN def_cond_0, simp] -lemmas or_1 = or_def [THEN def_cond_1, standard, simp] -lemmas or_0 = or_def [THEN def_cond_0, standard, simp] +lemmas or_1 = or_def [THEN def_cond_1, simp] +lemmas or_0 = or_def [THEN def_cond_0, simp] -lemmas xor_1 = xor_def [THEN def_cond_1, standard, simp] -lemmas xor_0 = xor_def [THEN def_cond_0, standard, simp] +lemmas xor_1 = xor_def [THEN def_cond_1, simp] +lemmas xor_0 = xor_def [THEN def_cond_0, simp] lemma not_type [TC]: "a:bool ==> not(a) : bool" by (simp add: not_def) diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/Cardinal.thy --- a/src/ZF/Cardinal.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/Cardinal.thy Sun Nov 20 20:15:02 2011 +0100 @@ -94,7 +94,7 @@ done (*A eqpoll A*) -lemmas eqpoll_refl = id_bij [THEN bij_imp_eqpoll, standard, simp] +lemmas eqpoll_refl = id_bij [THEN bij_imp_eqpoll, simp] lemma eqpoll_sym: "X \ Y ==> Y \ X" apply (unfold eqpoll_def) @@ -115,9 +115,9 @@ apply (erule id_subset_inj) done -lemmas lepoll_refl = subset_refl [THEN subset_imp_lepoll, standard, simp] +lemmas lepoll_refl = subset_refl [THEN subset_imp_lepoll, simp] -lemmas le_imp_lepoll = le_imp_subset [THEN subset_imp_lepoll, standard] +lemmas le_imp_lepoll = le_imp_subset [THEN subset_imp_lepoll] lemma eqpoll_imp_lepoll: "X \ Y ==> X \ Y" by (unfold eqpoll_def bij_def lepoll_def, blast) @@ -147,7 +147,7 @@ done (*0 \ Y*) -lemmas empty_lepollI = empty_subsetI [THEN subset_imp_lepoll, standard] +lemmas empty_lepollI = empty_subsetI [THEN subset_imp_lepoll] lemma lepoll_0_iff: "A \ 0 <-> A=0" by (blast intro: lepoll_0_is_0 lepoll_refl) @@ -159,7 +159,7 @@ done (*A eqpoll 0 ==> A=0*) -lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0, standard] +lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0] lemma eqpoll_0_iff: "A \ 0 <-> A=0" by (blast intro: eqpoll_0_is_0 eqpoll_refl) @@ -791,12 +791,12 @@ [unfolded Finite_def]]) done -lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite, standard] +lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite] lemma Finite_Int: "Finite(A) | Finite(B) ==> Finite(A Int B)" by (blast intro: subset_Finite) -lemmas Finite_Diff = Diff_subset [THEN subset_Finite, standard] +lemmas Finite_Diff = Diff_subset [THEN subset_Finite] lemma Finite_cons: "Finite(x) ==> Finite(cons(y,x))" apply (unfold Finite_def) diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/CardinalArith.thy --- a/src/ZF/CardinalArith.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/CardinalArith.thy Sun Nov 20 20:15:02 2011 +0100 @@ -753,9 +753,9 @@ apply (blast intro: Card_jump_cardinal K_lt_jump_cardinal Ord_jump_cardinal)+ done -lemmas Card_csucc = csucc_basic [THEN conjunct1, standard] +lemmas Card_csucc = csucc_basic [THEN conjunct1] -lemmas lt_csucc = csucc_basic [THEN conjunct2, standard] +lemmas lt_csucc = csucc_basic [THEN conjunct2] lemma Ord_0_lt_csucc: "Ord(K) ==> 0 < csucc(K)" by (blast intro: Ord_0_le lt_csucc lt_trans1) @@ -857,7 +857,7 @@ subsubsection{*Theorems by Krzysztof Grabczewski, proofs by lcp*} -lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel, standard] +lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel] lemma nat_sum_eqpoll_sum: "[| m:nat; n:nat |] ==> m + n \ m #+ n" apply (rule eqpoll_trans) diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/Cardinal_AC.thy --- a/src/ZF/Cardinal_AC.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/Cardinal_AC.thy Sun Nov 20 20:15:02 2011 +0100 @@ -17,7 +17,7 @@ done text{*The theorem @{term "||A|| = |A|"} *} -lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, standard, simp] +lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, simp] lemma cardinal_eqE: "|X| = |Y| ==> X eqpoll Y" apply (rule AC_well_ord [THEN exE]) diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/Coind/ECR.thy --- a/src/ZF/Coind/ECR.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/Coind/ECR.thy Sun Nov 20 20:15:02 2011 +0100 @@ -52,7 +52,7 @@ (* Properties of the pointwise extension to environments *) lemmas HasTyRel_non_zero = - HasTyRel.dom_subset [THEN subsetD, THEN SigmaD1, THEN ValNEE, standard] + HasTyRel.dom_subset [THEN subsetD, THEN SigmaD1, THEN ValNEE] lemma hastyenv_owr: "[| ve \ ValEnv; te \ TyEnv; hastyenv(ve,te); \ HasTyRel |] diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/Constructible/Formula.thy --- a/src/ZF/Constructible/Formula.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/Constructible/Formula.thy Sun Nov 20 20:15:02 2011 +0100 @@ -805,8 +805,8 @@ apply (blast intro: doubleton_in_Lset) done -lemmas Lset_UnI1 = Un_upper1 [THEN Lset_mono [THEN subsetD], standard] -lemmas Lset_UnI2 = Un_upper2 [THEN Lset_mono [THEN subsetD], standard] +lemmas Lset_UnI1 = Un_upper1 [THEN Lset_mono [THEN subsetD]] +lemmas Lset_UnI2 = Un_upper2 [THEN Lset_mono [THEN subsetD]] text{*Hard work is finding a single j:i such that {a,b}<=Lset(j)*} lemma doubleton_in_LLimit: diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/Epsilon.thy --- a/src/ZF/Epsilon.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/Epsilon.thy Sun Nov 20 20:15:02 2011 +0100 @@ -45,7 +45,7 @@ apply (rule nat_0I [THEN UN_upper]) done -lemmas arg_into_eclose = arg_subset_eclose [THEN subsetD, standard] +lemmas arg_into_eclose = arg_subset_eclose [THEN subsetD] lemma Transset_eclose: "Transset(eclose(A))" apply (unfold eclose_def Transset_def) @@ -58,13 +58,13 @@ (* x : eclose(A) ==> x <= eclose(A) *) lemmas eclose_subset = - Transset_eclose [unfolded Transset_def, THEN bspec, standard] + Transset_eclose [unfolded Transset_def, THEN bspec] (* [| A : eclose(B); c : A |] ==> c : eclose(B) *) -lemmas ecloseD = eclose_subset [THEN subsetD, standard] +lemmas ecloseD = eclose_subset [THEN subsetD] lemmas arg_in_eclose_sing = arg_subset_eclose [THEN singleton_subsetD] -lemmas arg_into_eclose_sing = arg_in_eclose_sing [THEN ecloseD, standard] +lemmas arg_into_eclose_sing = arg_in_eclose_sing [THEN ecloseD] (* This is epsilon-induction for eclose(A); see also eclose_induct_down... [| a: eclose(A); !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x) @@ -148,7 +148,7 @@ by (simp add: lt_def Ord_def under_Memrel) (* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *) -lemmas under_Memrel_eclose = Transset_eclose [THEN under_Memrel, standard] +lemmas under_Memrel_eclose = Transset_eclose [THEN under_Memrel] lemmas wfrec_ssubst = wf_Memrel [THEN wfrec, THEN ssubst] diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/Finite.thy --- a/src/ZF/Finite.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/Finite.thy Sun Nov 20 20:15:02 2011 +0100 @@ -48,7 +48,7 @@ done (* A : Fin(B) ==> A <= B *) -lemmas FinD = Fin.dom_subset [THEN subsetD, THEN PowD, standard] +lemmas FinD = Fin.dom_subset [THEN subsetD, THEN PowD] (** Induction on finite sets **) @@ -147,7 +147,7 @@ lemma FiniteFun_domain_Fin: "h: A -||>B ==> domain(h) : Fin(A)" by (erule FiniteFun.induct, simp, simp) -lemmas FiniteFun_apply_type = FiniteFun_is_fun [THEN apply_type, standard] +lemmas FiniteFun_apply_type = FiniteFun_is_fun [THEN apply_type] (*Every subset of a finite function is a finite function.*) lemma FiniteFun_subset_lemma [rule_format]: diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/Induct/Multiset.thy --- a/src/ZF/Induct/Multiset.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/Induct/Multiset.thy Sun Nov 20 20:15:02 2011 +0100 @@ -221,7 +221,7 @@ (** normalize **) -lemmas Collect_Finite = Collect_subset [THEN subset_Finite, standard] +lemmas Collect_Finite = Collect_subset [THEN subset_Finite] lemma normalize_idem [simp]: "normalize(normalize(f)) = normalize(f)" apply (simp add: normalize_def funrestrict_def mset_of_def) @@ -1136,7 +1136,7 @@ subsection{*Ordinal Multisets*} (* A \ B ==> field(Memrel(A)) \ field(Memrel(B)) *) -lemmas field_Memrel_mono = Memrel_mono [THEN field_mono, standard] +lemmas field_Memrel_mono = Memrel_mono [THEN field_mono] (* [| Aa \ Ba; A \ B |] ==> @@ -1187,7 +1187,7 @@ part_ord(field(Memrel(i))-||>nat-{0}, multirel(field(Memrel(i)), Memrel(i))) *) -lemmas part_ord_mless = part_ord_Memrel [THEN part_ord_multirel, standard] +lemmas part_ord_mless = part_ord_Memrel [THEN part_ord_multirel] (*irreflexivity*) @@ -1199,7 +1199,7 @@ done (* N R *) -lemmas mless_irrefl = mless_not_refl [THEN notE, standard, elim!] +lemmas mless_irrefl = mless_not_refl [THEN notE, elim!] (*transitivity*) lemma mless_trans: "[| K <# M; M <# N |] ==> K <# N" diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/Induct/Tree_Forest.thy --- a/src/ZF/Induct/Tree_Forest.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/Induct/Tree_Forest.thy Sun Nov 20 20:15:02 2011 +0100 @@ -19,9 +19,10 @@ (* FIXME *) lemmas tree'induct = - tree_forest.mutual_induct [THEN conjunct1, THEN spec, THEN [2] rev_mp, of concl: _ t, standard, consumes 1] + tree_forest.mutual_induct [THEN conjunct1, THEN spec, THEN [2] rev_mp, of concl: _ t, consumes 1] and forest'induct = - tree_forest.mutual_induct [THEN conjunct2, THEN spec, THEN [2] rev_mp, of concl: _ f, standard, consumes 1] + tree_forest.mutual_induct [THEN conjunct2, THEN spec, THEN [2] rev_mp, of concl: _ f, consumes 1] + for t declare tree_forest.intros [simp, TC] diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/IntArith.thy --- a/src/ZF/IntArith.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/IntArith.thy Sun Nov 20 20:15:02 2011 +0100 @@ -9,19 +9,22 @@ **) lemmas [simp] = - zminus_equation [where y = "integ_of(w)", standard] - equation_zminus [where x = "integ_of(w)", standard] + zminus_equation [where y = "integ_of(w)"] + equation_zminus [where x = "integ_of(w)"] + for w lemmas [iff] = - zminus_zless [where y = "integ_of(w)", standard] - zless_zminus [where x = "integ_of(w)", standard] + zminus_zless [where y = "integ_of(w)"] + zless_zminus [where x = "integ_of(w)"] + for w lemmas [iff] = - zminus_zle [where y = "integ_of(w)", standard] - zle_zminus [where x = "integ_of(w)", standard] + zminus_zle [where y = "integ_of(w)"] + zle_zminus [where x = "integ_of(w)"] + for w lemmas [simp] = - Let_def [where s = "integ_of(w)", standard] + Let_def [where s = "integ_of(w)"] for w (*** Simprocs for numeric literals ***) @@ -47,12 +50,13 @@ (** For cancel_numerals **) lemmas rel_iff_rel_0_rls = - zless_iff_zdiff_zless_0 [where y = "u $+ v", standard] - eq_iff_zdiff_eq_0 [where y = "u $+ v", standard] - zle_iff_zdiff_zle_0 [where y = "u $+ v", standard] + zless_iff_zdiff_zless_0 [where y = "u $+ v"] + eq_iff_zdiff_eq_0 [where y = "u $+ v"] + zle_iff_zdiff_zle_0 [where y = "u $+ v"] zless_iff_zdiff_zless_0 [where y = n] eq_iff_zdiff_eq_0 [where y = n] zle_iff_zdiff_zle_0 [where y = n] + for u v (* FIXME n (!?) *) lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))" apply (simp add: zdiff_def zadd_zmult_distrib) diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/IntDiv_ZF.thy --- a/src/ZF/IntDiv_ZF.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/IntDiv_ZF.thy Sun Nov 20 20:15:02 2011 +0100 @@ -791,8 +791,8 @@ apply (blast dest: zle_zless_trans)+ done -lemmas pos_mod_sign = pos_mod [THEN conjunct1, standard] -and pos_mod_bound = pos_mod [THEN conjunct2, standard] +lemmas pos_mod_sign = pos_mod [THEN conjunct1] + and pos_mod_bound = pos_mod [THEN conjunct2] lemma neg_mod: "b $< #0 ==> a zmod b $<= #0 & b $< a zmod b" apply (cut_tac a = "intify (a)" and b = "intify (b)" in divAlg_correct) @@ -801,8 +801,8 @@ apply (blast dest: zless_trans)+ done -lemmas neg_mod_sign = neg_mod [THEN conjunct1, standard] -and neg_mod_bound = neg_mod [THEN conjunct2, standard] +lemmas neg_mod_sign = neg_mod [THEN conjunct1] + and neg_mod_bound = neg_mod [THEN conjunct2] (** proving general properties of zdiv and zmod **) @@ -1111,16 +1111,16 @@ apply (blast dest!: zle_zless_trans)+ done -declare zdiv_pos_pos [of "integ_of (v)" "integ_of (w)", standard, simp] -declare zdiv_neg_pos [of "integ_of (v)" "integ_of (w)", standard, simp] -declare zdiv_pos_neg [of "integ_of (v)" "integ_of (w)", standard, simp] -declare zdiv_neg_neg [of "integ_of (v)" "integ_of (w)", standard, simp] -declare zmod_pos_pos [of "integ_of (v)" "integ_of (w)", standard, simp] -declare zmod_neg_pos [of "integ_of (v)" "integ_of (w)", standard, simp] -declare zmod_pos_neg [of "integ_of (v)" "integ_of (w)", standard, simp] -declare zmod_neg_neg [of "integ_of (v)" "integ_of (w)", standard, simp] -declare posDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", standard, simp] -declare negDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", standard, simp] +declare zdiv_pos_pos [of "integ_of (v)" "integ_of (w)", simp] for v w +declare zdiv_neg_pos [of "integ_of (v)" "integ_of (w)", simp] for v w +declare zdiv_pos_neg [of "integ_of (v)" "integ_of (w)", simp] for v w +declare zdiv_neg_neg [of "integ_of (v)" "integ_of (w)", simp] for v w +declare zmod_pos_pos [of "integ_of (v)" "integ_of (w)", simp] for v w +declare zmod_neg_pos [of "integ_of (v)" "integ_of (w)", simp] for v w +declare zmod_pos_neg [of "integ_of (v)" "integ_of (w)", simp] for v w +declare zmod_neg_neg [of "integ_of (v)" "integ_of (w)", simp] for v w +declare posDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", simp] for v w +declare negDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", simp] for v w (** Special-case simplification **) diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/Int_ZF.thy --- a/src/ZF/Int_ZF.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/Int_ZF.thy Sun Nov 20 20:15:02 2011 +0100 @@ -717,7 +717,7 @@ by (blast dest: zless_trans) (* [| z $< w; ~ P ==> w $< z |] ==> P *) -lemmas zless_asym = zless_not_sym [THEN swap, standard] +lemmas zless_asym = zless_not_sym [THEN swap] lemma zless_imp_zle: "z $< w ==> z $<= w" by (simp add: zle_def) @@ -867,16 +867,16 @@ (*"v $<= w ==> v$+z $<= w$+z"*) -lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2, standard] +lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2] (*"v $<= w ==> z$+v $<= z$+w"*) -lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2, standard] +lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2] (*"v $<= w ==> v$+z $<= w$+z"*) -lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2, standard] +lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2] (*"v $<= w ==> z$+v $<= z$+w"*) -lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2, standard] +lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2] lemma zadd_zle_mono: "[| w' $<= w; z' $<= z |] ==> w' $+ z' $<= w $+ z" by (erule zadd_zle_mono1 [THEN zle_trans], simp) diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/List_ZF.thy --- a/src/ZF/List_ZF.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/List_ZF.thy Sun Nov 20 20:15:02 2011 +0100 @@ -317,7 +317,7 @@ (** theorems about list(Collect(A,P)) -- used in Induct/Term.thy **) (* c : list(Collect(B,P)) ==> c : list(B) *) -lemmas list_CollectD = Collect_subset [THEN list_mono, THEN subsetD, standard] +lemmas list_CollectD = Collect_subset [THEN list_mono, THEN subsetD] lemma map_list_Collect: "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)" apply (induct_tac "l") diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/Nat_ZF.thy --- a/src/ZF/Nat_ZF.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/Nat_ZF.thy Sun Nov 20 20:15:02 2011 +0100 @@ -57,7 +57,7 @@ done (* nat = {0} Un {succ(x). x:nat} *) -lemmas nat_unfold = nat_bnd_mono [THEN nat_def [THEN def_lfp_unfold], standard] +lemmas nat_unfold = nat_bnd_mono [THEN nat_def [THEN def_lfp_unfold]] (** Type checking of 0 and successor **) @@ -80,7 +80,7 @@ lemma bool_subset_nat: "bool <= nat" by (blast elim!: boolE) -lemmas bool_into_nat = bool_subset_nat [THEN subsetD, standard] +lemmas bool_into_nat = bool_subset_nat [THEN subsetD] subsection{*Injectivity Properties and Induction*} @@ -98,10 +98,10 @@ by (erule nat_induct, auto) (* i: nat ==> 0 le i; same thing as 0 i le i; same thing as i f: A->B *} -lemmas bij_is_fun = bij_is_inj [THEN inj_is_fun, standard] +lemmas bij_is_fun = bij_is_inj [THEN inj_is_fun] lemma lam_bijective: "[| !!x. x:A ==> c(x): B; @@ -174,7 +174,7 @@ apply (blast intro: lam_type) done -lemmas id_inj = subset_refl [THEN id_subset_inj, standard] +lemmas id_inj = subset_refl [THEN id_subset_inj] lemma id_surj: "id(A): surj(A,A)" apply (unfold id_def surj_def) @@ -220,7 +220,7 @@ "[|f \ inj(A,B); f ` x = y; x \ A|] ==> converse(f) ` y = x" by auto -lemmas left_inverse_bij = bij_is_inj [THEN left_inverse, standard] +lemmas left_inverse_bij = bij_is_inj [THEN left_inverse] lemma right_inverse_lemma: "[| f: A->B; converse(f): C->A; b: C |] ==> f`(converse(f)`b) = b" diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/QPair.thy --- a/src/ZF/QPair.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/QPair.thy Sun Nov 20 20:15:02 2011 +0100 @@ -82,7 +82,7 @@ apply (rule sum_equal_iff) done -lemmas QPair_inject = QPair_iff [THEN iffD1, THEN conjE, standard, elim!] +lemmas QPair_inject = QPair_iff [THEN iffD1, THEN conjE, elim!] lemma QPair_inject1: " = ==> a=c" by blast @@ -249,8 +249,8 @@ (*Injection and freeness rules*) -lemmas QInl_inject = QInl_iff [THEN iffD1, standard] -lemmas QInr_inject = QInr_iff [THEN iffD1, standard] +lemmas QInl_inject = QInl_iff [THEN iffD1] +lemmas QInr_inject = QInr_iff [THEN iffD1] lemmas QInl_neq_QInr = QInl_QInr_iff [THEN iffD1, THEN FalseE, elim!] lemmas QInr_neq_QInl = QInr_QInl_iff [THEN iffD1, THEN FalseE, elim!] diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/QUniv.thy --- a/src/ZF/QUniv.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/QUniv.thy Sun Nov 20 20:15:02 2011 +0100 @@ -64,7 +64,7 @@ apply (rule univ_eclose_subset_quniv) done -lemmas univ_into_quniv = univ_subset_quniv [THEN subsetD, standard] +lemmas univ_into_quniv = univ_subset_quniv [THEN subsetD] lemma Pow_univ_subset_quniv: "Pow(univ(A)) <= quniv(A)" apply (unfold quniv_def) @@ -72,15 +72,15 @@ done lemmas univ_subset_into_quniv = - PowI [THEN Pow_univ_subset_quniv [THEN subsetD], standard] + PowI [THEN Pow_univ_subset_quniv [THEN subsetD]] -lemmas zero_in_quniv = zero_in_univ [THEN univ_into_quniv, standard] -lemmas one_in_quniv = one_in_univ [THEN univ_into_quniv, standard] -lemmas two_in_quniv = two_in_univ [THEN univ_into_quniv, standard] +lemmas zero_in_quniv = zero_in_univ [THEN univ_into_quniv] +lemmas one_in_quniv = one_in_univ [THEN univ_into_quniv] +lemmas two_in_quniv = two_in_univ [THEN univ_into_quniv] lemmas A_subset_quniv = subset_trans [OF A_subset_univ univ_subset_quniv] -lemmas A_into_quniv = A_subset_quniv [THEN subsetD, standard] +lemmas A_into_quniv = A_subset_quniv [THEN subsetD] (*** univ(A) closure for Quine-inspired pairs and injections ***) @@ -97,7 +97,7 @@ done lemmas naturals_subset_nat = - Ord_nat [THEN Ord_is_Transset, unfolded Transset_def, THEN bspec, standard] + Ord_nat [THEN Ord_is_Transset, unfolded Transset_def, THEN bspec] lemmas naturals_subset_univ = subset_trans [OF naturals_subset_nat nat_subset_univ] @@ -128,7 +128,7 @@ apply (erule PowD, blast) done -lemmas quniv_QPair_E = quniv_QPair_D [THEN conjE, standard] +lemmas quniv_QPair_E = quniv_QPair_D [THEN conjE] lemma quniv_QPair_iff: " : quniv(A) <-> a: quniv(A) & b: quniv(A)" by (blast intro: QPair_in_quniv dest: quniv_QPair_D) @@ -153,11 +153,11 @@ lemmas nat_subset_quniv = subset_trans [OF nat_subset_univ univ_subset_quniv] (* n:nat ==> n:quniv(A) *) -lemmas nat_into_quniv = nat_subset_quniv [THEN subsetD, standard] +lemmas nat_into_quniv = nat_subset_quniv [THEN subsetD] lemmas bool_subset_quniv = subset_trans [OF bool_subset_univ univ_subset_quniv] -lemmas bool_into_quniv = bool_subset_quniv [THEN subsetD, standard] +lemmas bool_into_quniv = bool_subset_quniv [THEN subsetD] (*Intersecting with Vfrom...*) diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/Resid/Confluence.thy --- a/src/ZF/Resid/Confluence.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/Resid/Confluence.thy Sun Nov 20 20:15:02 2011 +0100 @@ -52,13 +52,13 @@ done lemmas confluence_parallel_reduction = - parallel_moves [THEN strip_lemma_r, THEN strip_lemma_l, standard] + parallel_moves [THEN strip_lemma_r, THEN strip_lemma_l] lemma lemma1: "[|confluence(Spar_red)|]==> confluence(Sred)" by (unfold confluence_def, blast intro: par_red_red red_par_red) lemmas confluence_beta_reduction = - confluence_parallel_reduction [THEN lemma1, standard] + confluence_parallel_reduction [THEN lemma1] (**** Conversion ****) diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/Sum.thy --- a/src/ZF/Sum.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/Sum.thy Sun Nov 20 20:15:02 2011 +0100 @@ -94,8 +94,8 @@ (*Injection and freeness rules*) -lemmas Inl_inject = Inl_iff [THEN iffD1, standard] -lemmas Inr_inject = Inr_iff [THEN iffD1, standard] +lemmas Inl_inject = Inl_iff [THEN iffD1] +lemmas Inr_inject = Inr_iff [THEN iffD1] lemmas Inl_neq_Inr = Inl_Inr_iff [THEN iffD1, THEN FalseE, elim!] lemmas Inr_neq_Inl = Inr_Inl_iff [THEN iffD1, THEN FalseE, elim!] @@ -168,7 +168,7 @@ by blast lemmas Part_CollectE = - Part_Collect [THEN equalityD1, THEN subsetD, THEN CollectE, standard] + Part_Collect [THEN equalityD1, THEN subsetD, THEN CollectE] lemma Part_Inl: "Part(A+B,Inl) = {Inl(x). x: A}" by blast diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/Trancl.thy --- a/src/ZF/Trancl.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/Trancl.thy Sun Nov 20 20:15:02 2011 +0100 @@ -109,12 +109,12 @@ (* r^* = id(field(r)) Un ( r O r^* ) *) lemmas rtrancl_unfold = - rtrancl_bnd_mono [THEN rtrancl_def [THEN def_lfp_unfold], standard] + rtrancl_bnd_mono [THEN rtrancl_def [THEN def_lfp_unfold]] (** The relation rtrancl **) (* r^* <= field(r) * field(r) *) -lemmas rtrancl_type = rtrancl_def [THEN def_lfp_subset, standard] +lemmas rtrancl_type = rtrancl_def [THEN def_lfp_subset] lemma relation_rtrancl: "relation(r^*)" apply (simp add: relation_def) @@ -178,7 +178,7 @@ apply (blast intro: rtrancl_into_rtrancl) done -lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard] +lemmas rtrancl_trans = trans_rtrancl [THEN transD] (*elimination of rtrancl -- by induction on a special formula*) lemma rtranclE: @@ -203,7 +203,7 @@ lemmas trans_on_trancl = trans_trancl [THEN trans_imp_trans_on] -lemmas trancl_trans = trans_trancl [THEN transD, standard] +lemmas trancl_trans = trans_trancl [THEN transD] (** Conversions between trancl and rtrancl **) diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/UNITY/AllocBase.thy --- a/src/ZF/UNITY/AllocBase.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/UNITY/AllocBase.thy Sun Nov 20 20:15:02 2011 +0100 @@ -313,9 +313,9 @@ done lemmas Increasing_state_ofD1 = - gen_Increains_state_of_eq [THEN equalityD1, THEN subsetD, standard] + gen_Increains_state_of_eq [THEN equalityD1, THEN subsetD] lemmas Increasing_state_ofD2 = - gen_Increains_state_of_eq [THEN equalityD2, THEN subsetD, standard] + gen_Increains_state_of_eq [THEN equalityD2, THEN subsetD] lemma Follows_state_of_eq: "Follows(A, r, %s. f(state_of(s)), %s. g(state_of(s))) = @@ -324,9 +324,9 @@ done lemmas Follows_state_ofD1 = - Follows_state_of_eq [THEN equalityD1, THEN subsetD, standard] + Follows_state_of_eq [THEN equalityD1, THEN subsetD] lemmas Follows_state_ofD2 = - Follows_state_of_eq [THEN equalityD2, THEN subsetD, standard] + Follows_state_of_eq [THEN equalityD2, THEN subsetD] lemma nat_list_inj_type: "n\nat ==> nat_list_inj(n)\list(nat)" by (induct_tac "n", auto) @@ -373,7 +373,7 @@ by (simp add: Inter_Diff_var_iff) (* [| Finite(A); (\x\var-A. b\B(x)) |] ==> b\Inter(RepFun(var-A, B)) *) -lemmas Inter_var_DiffI = Inter_Diff_var_iff [THEN iffD2, standard] +lemmas Inter_var_DiffI = Inter_Diff_var_iff [THEN iffD2] declare Inter_var_DiffI [intro!] diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/UNITY/Constrains.thy --- a/src/ZF/UNITY/Constrains.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/UNITY/Constrains.thy Sun Nov 20 20:15:02 2011 +0100 @@ -347,8 +347,8 @@ lemma AlwaysD: "F \ Always(A) ==> Init(F)<=A & F \ Stable(A)" by (simp add: Always_def initially_def) -lemmas AlwaysE = AlwaysD [THEN conjE, standard] -lemmas Always_imp_Stable = AlwaysD [THEN conjunct2, standard] +lemmas AlwaysE = AlwaysD [THEN conjE] +lemmas Always_imp_Stable = AlwaysD [THEN conjunct2] (*The set of all reachable states is Always*) lemma Always_includes_reachable: "F \ Always(A) ==> reachable(F) <= A" @@ -364,7 +364,7 @@ apply (blast intro: constrains_imp_Constrains) done -lemmas Always_reachable = invariant_reachable [THEN invariant_imp_Always, standard] +lemmas Always_reachable = invariant_reachable [THEN invariant_imp_Always] lemma Always_eq_invariant_reachable: "Always(A) = {F \ program. F \ invariant(reachable(F) Int A)}" apply (simp (no_asm) add: Always_def invariant_def Stable_def Constrains_def2 stable_def initially_def) @@ -420,7 +420,7 @@ by (blast intro: Always_Constrains_pre [THEN iffD1]) (* [| F \ Always(I); F \ A Co A' |] ==> F \ A Co (I Int A') *) -lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2, standard] +lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2] (*The analogous proof of Always_LeadsTo_weaken doesn't terminate*) lemma Always_Constrains_weaken: @@ -451,7 +451,7 @@ (*Delete the nearest invariance assumption (which will be the second one used by Always_Int_I) *) -lemmas Always_thin = thin_rl [of "F \ Always(A)", standard] +lemmas Always_thin = thin_rl [of "F \ Always(A)"] ML {* diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/UNITY/FP.thy --- a/src/ZF/UNITY/FP.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/UNITY/FP.thy Sun Nov 20 20:15:02 2011 +0100 @@ -45,7 +45,7 @@ "[| \B. F \ stable (A Int B); st_set(A) |] ==> A \ FP_Orig(F)" by (unfold FP_Orig_def stable_def st_set_def, blast) -lemmas FP_Orig_weakest = allI [THEN FP_Orig_weakest2, standard] +lemmas FP_Orig_weakest = allI [THEN FP_Orig_weakest2] lemma stable_FP_Int: "F \ program ==> F \ stable (FP(F) Int B)" apply (subgoal_tac "FP (F) Int B = (\x\B. FP (F) Int {x}) ") diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/UNITY/GenPrefix.thy --- a/src/ZF/UNITY/GenPrefix.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/UNITY/GenPrefix.thy Sun Nov 20 20:15:02 2011 +0100 @@ -350,7 +350,7 @@ apply (auto simp add: trans_def) done -lemmas prefix_trans = trans_prefix [THEN transD, standard] +lemmas prefix_trans = trans_prefix [THEN transD] lemma trans_on_prefix: "trans[list(A)](prefix(A))" apply (unfold prefix_def) @@ -358,7 +358,7 @@ apply (auto simp add: trans_def) done -lemmas prefix_trans_on = trans_on_prefix [THEN trans_onD, standard] +lemmas prefix_trans_on = trans_on_prefix [THEN trans_onD] (* Monotonicity of "set" operator WRT prefix *) diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/UNITY/UNITY.thy --- a/src/ZF/UNITY/UNITY.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/UNITY/UNITY.thy Sun Nov 20 20:15:02 2011 +0100 @@ -167,7 +167,7 @@ lemma Init_type: "Init(F)\state" by (simp add: RawInit_type Init_def) -lemmas InitD = Init_type [THEN subsetD, standard] +lemmas InitD = Init_type [THEN subsetD] lemma st_set_Init [iff]: "st_set(Init(F))" apply (unfold st_set_def) @@ -562,7 +562,7 @@ by (unfold stable_def constrains_def st_set_def, blast) (* [| F \ stable(C); F \ (C \ A) co A |] ==> F \ stable(C \ A) *) -lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI, standard] +lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI] subsection{*The Operator @{term invariant}*} diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/UNITY/Union.thy --- a/src/ZF/UNITY/Union.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/UNITY/Union.thy Sun Nov 20 20:15:02 2011 +0100 @@ -427,7 +427,7 @@ lemma ok_commute: "(F ok G) <->(G ok F)" by (auto simp add: ok_def) -lemmas ok_sym = ok_commute [THEN iffD1, standard] +lemmas ok_sym = ok_commute [THEN iffD1] lemma ok_iff_OK: "OK({<0,F>,<1,G>,<2,H>}, snd) <-> (F ok G & (F Join G) ok H)" by (simp add: ok_def Join_def OK_def Int_assoc cons_absorb diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/UNITY/WFair.thy --- a/src/ZF/UNITY/WFair.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/UNITY/WFair.thy Sun Nov 20 20:15:02 2011 +0100 @@ -182,7 +182,7 @@ (* Added by Sidi, from Misra's notes, Progress chapter, exercise number 4 *) (* [| F \ program; A<=B; st_set(A); st_set(B) |] ==> A leadsTo B *) -lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis, standard] +lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis] lemma leadsTo_Trans: "[|F \ A leadsTo B; F \ B leadsTo C |]==>F \ A leadsTo C" apply (unfold leadsTo_def) @@ -565,7 +565,7 @@ done (* [| F \ program; st_set(B) |] ==> F \ wlt(F, B) leadsTo B *) -lemmas wlt_leadsTo = conjI [THEN wlt_leadsTo_iff [THEN iffD2], standard] +lemmas wlt_leadsTo = conjI [THEN wlt_leadsTo_iff [THEN iffD2]] lemma leadsTo_subset: "F \ A leadsTo B ==> A <= wlt(F, B)" apply (unfold wlt_def) @@ -665,7 +665,7 @@ apply blast+ done -lemmas completion = refl [THEN completion_aux, standard] +lemmas completion = refl [THEN completion_aux] lemma finite_completion_aux: "[| I \ Fin(X); F \ program; st_set(C) |] ==> diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/Univ.thy --- a/src/ZF/Univ.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/Univ.thy Sun Nov 20 20:15:02 2011 +0100 @@ -205,9 +205,9 @@ done lemmas Vfrom_UnI1 = - Un_upper1 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD], standard] + Un_upper1 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD]] lemmas Vfrom_UnI2 = - Un_upper2 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD], standard] + Un_upper2 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD]] text{*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*} lemma doubleton_in_VLimit: @@ -242,7 +242,7 @@ subsubsection{* Closure under Disjoint Union *} -lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard] +lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom] lemma one_in_VLimit: "Limit(i) ==> 1 \ Vfrom(A,i)" by (blast intro: nat_into_VLimit) @@ -409,8 +409,8 @@ lemma Vset: "Vset(i) = (\j\i. Pow(Vset(j)))" by (subst Vfrom, blast) -lemmas Vset_succ = Transset_0 [THEN Transset_Vfrom_succ, standard] -lemmas Transset_Vset = Transset_0 [THEN Transset_Vfrom, standard] +lemmas Vset_succ = Transset_0 [THEN Transset_Vfrom_succ] +lemmas Transset_Vset = Transset_0 [THEN Transset_Vfrom] subsubsection{* Characterisation of the elements of @{term "Vset(i)"} *} @@ -579,7 +579,7 @@ apply (rule A_subset_Vfrom) done -lemmas A_into_univ = A_subset_univ [THEN subsetD, standard] +lemmas A_into_univ = A_subset_univ [THEN subsetD] subsubsection{* Closure under Unordered and Ordered Pairs *} @@ -620,7 +620,7 @@ done text{* n:nat ==> n:univ(A) *} -lemmas nat_into_univ = nat_subset_univ [THEN subsetD, standard] +lemmas nat_into_univ = nat_subset_univ [THEN subsetD] subsubsection{* Instances for 1 and 2 *} @@ -638,7 +638,7 @@ apply (blast intro!: zero_in_univ one_in_univ) done -lemmas bool_into_univ = bool_subset_univ [THEN subsetD, standard] +lemmas bool_into_univ = bool_subset_univ [THEN subsetD] subsubsection{* Closure under Disjoint Union *} @@ -764,7 +764,7 @@ assumption, fast) text{*This weaker version says a, b exist at the same level*} -lemmas Vfrom_doubleton_D = Transset_Vfrom [THEN Transset_doubleton_D, standard] +lemmas Vfrom_doubleton_D = Transset_Vfrom [THEN Transset_doubleton_D] (** Using only the weaker theorem would prove \ Vfrom(X,i) implies a, b \ Vfrom(X,i), which is useless for induction. diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/WF.thy --- a/src/ZF/WF.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/WF.thy Sun Nov 20 20:15:02 2011 +0100 @@ -164,7 +164,7 @@ by (erule_tac a=a in wf_induct, blast) (* [| wf(r); : r; ~P ==> : r |] ==> P *) -lemmas wf_asym = wf_not_sym [THEN swap, standard] +lemmas wf_asym = wf_not_sym [THEN swap] lemma wf_on_not_refl: "[| wf[A](r); a: A |] ==> ~: r" by (erule_tac a=a in wf_on_induct, assumption, blast) @@ -212,8 +212,8 @@ text{*@{term "r-``{a}"} is the set of everything under @{term a} in @{term r}*} -lemmas underI = vimage_singleton_iff [THEN iffD2, standard] -lemmas underD = vimage_singleton_iff [THEN iffD1, standard] +lemmas underI = vimage_singleton_iff [THEN iffD2] +lemmas underD = vimage_singleton_iff [THEN iffD1] subsection{*The Predicate @{term is_recfun}*} diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/ZF.thy --- a/src/ZF/ZF.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/ZF.thy Sun Nov 20 20:15:02 2011 +0100 @@ -417,8 +417,8 @@ lemma equality_iffI: "(!!x. x\A <-> x\B) ==> A = B" by (rule equalityI, blast+) -lemmas equalityD1 = extension [THEN iffD1, THEN conjunct1, standard] -lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2, standard] +lemmas equalityD1 = extension [THEN iffD1, THEN conjunct1] +lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2] lemma equalityE: "[| A = B; [| A<=B; B<=A |] ==> P |] ==> P" by (blast dest: equalityD1 equalityD2) @@ -568,7 +568,7 @@ apply (best dest: equalityD2) done -lemmas emptyE [elim!] = not_mem_empty [THEN notE, standard] +lemmas emptyE [elim!] = not_mem_empty [THEN notE] lemma empty_subsetI [simp]: "0 <= A" diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/Zorn.thy --- a/src/ZF/Zorn.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/Zorn.thy Sun Nov 20 20:15:02 2011 +0100 @@ -77,9 +77,9 @@ lemma increasingD2: "[| f \ increasing(A); x<=A |] ==> x <= f`x" by (unfold increasing_def, blast) -lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI, standard] +lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI] -lemmas TFin_is_subset = TFin.dom_subset [THEN subsetD, THEN PowD, standard] +lemmas TFin_is_subset = TFin.dom_subset [THEN subsetD, THEN PowD] text{*Structural induction on @{term "TFin(S,next)"} *} diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/equalities.thy --- a/src/ZF/equalities.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/equalities.thy Sun Nov 20 20:15:02 2011 +0100 @@ -81,7 +81,7 @@ (*A safe special case of subset elimination, adding no new variables [| cons(a,B) \ C; [| a \ C; B \ C |] ==> R |] ==> R *) -lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE, standard] +lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE] lemma subset_empty_iff: "A\0 <-> A=0" by blast diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/ex/Limit.thy --- a/src/ZF/ex/Limit.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/ex/Limit.thy Sun Nov 20 20:15:02 2011 +0100 @@ -994,9 +994,9 @@ (* The following three theorems have cpo asms due to THE (uniqueness). *) -lemmas Rp_cont [TC] = embRp [THEN projpair_p_cont, standard] -lemmas embRp_eq = embRp [THEN projpair_eq, standard] -lemmas embRp_rel = embRp [THEN projpair_rel, standard] +lemmas Rp_cont [TC] = embRp [THEN projpair_p_cont] +lemmas embRp_eq = embRp [THEN projpair_eq] +lemmas embRp_rel = embRp [THEN projpair_rel] lemma embRp_eq_thm: diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/ex/Primes.thy --- a/src/ZF/ex/Primes.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/ex/Primes.thy Sun Nov 20 20:15:02 2011 +0100 @@ -40,8 +40,8 @@ "[|m dvd n; !!k. [|m \ nat; n \ nat; k \ nat; n = m#*k|] ==> P|] ==> P" by (blast dest!: dvdD) -lemmas dvd_imp_nat1 = dvdD [THEN conjunct1, standard] -lemmas dvd_imp_nat2 = dvdD [THEN conjunct2, THEN conjunct1, standard] +lemmas dvd_imp_nat1 = dvdD [THEN conjunct1] +lemmas dvd_imp_nat2 = dvdD [THEN conjunct2, THEN conjunct1] lemma dvd_0_right [simp]: "m \ nat ==> m dvd 0" @@ -122,8 +122,8 @@ done (* k dvd (m*k) *) -lemmas dvdI1 [simp] = dvd_refl [THEN dvd_mult, standard] -lemmas dvdI2 [simp] = dvd_refl [THEN dvd_mult2, standard] +lemmas dvdI1 [simp] = dvd_refl [THEN dvd_mult] +lemmas dvdI2 [simp] = dvd_refl [THEN dvd_mult2] lemma dvd_mod_imp_dvd_raw: "[| a \ nat; b \ nat; k dvd b; k dvd (a mod b) |] ==> k dvd a" diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/pair.thy --- a/src/ZF/pair.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/pair.thy Sun Nov 20 20:15:02 2011 +0100 @@ -43,17 +43,17 @@ lemma Pair_iff [simp]: " = <-> a=c & b=d" by (simp add: Pair_def doubleton_eq_iff, blast) -lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, standard, elim!] +lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, elim!] -lemmas Pair_inject1 = Pair_iff [THEN iffD1, THEN conjunct1, standard] -lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2, standard] +lemmas Pair_inject1 = Pair_iff [THEN iffD1, THEN conjunct1] +lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2] lemma Pair_not_0: " ~= 0" apply (unfold Pair_def) apply (blast elim: equalityE) done -lemmas Pair_neq_0 = Pair_not_0 [THEN notE, standard, elim!] +lemmas Pair_neq_0 = Pair_not_0 [THEN notE, elim!] declare sym [THEN Pair_neq_0, elim!] @@ -82,8 +82,8 @@ lemma SigmaI [TC,intro!]: "[| a:A; b:B(a) |] ==> : Sigma(A,B)" by simp -lemmas SigmaD1 = Sigma_iff [THEN iffD1, THEN conjunct1, standard] -lemmas SigmaD2 = Sigma_iff [THEN iffD1, THEN conjunct2, standard] +lemmas SigmaD1 = Sigma_iff [THEN iffD1, THEN conjunct1] +lemmas SigmaD2 = Sigma_iff [THEN iffD1, THEN conjunct2] (*The general elimination rule*) lemma SigmaE [elim!]: diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/upair.thy --- a/src/ZF/upair.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/upair.thy Sun Nov 20 20:15:02 2011 +0100 @@ -130,7 +130,7 @@ lemma cons_not_0 [simp]: "cons(a,B) ~= 0" by (blast elim: equalityE) -lemmas cons_neq_0 = cons_not_0 [THEN notE, standard] +lemmas cons_neq_0 = cons_not_0 [THEN notE] declare cons_not_0 [THEN not_sym, simp] @@ -143,7 +143,7 @@ lemma singletonI [intro!]: "a : {a}" by (rule consI1) -lemmas singletonE = singleton_iff [THEN iffD1, elim_format, standard, elim!] +lemmas singletonE = singleton_iff [THEN iffD1, elim_format, elim!] subsection{*Descriptions*} @@ -228,11 +228,11 @@ addsplits[split_if] **) -lemmas split_if_eq1 = split_if [of "%x. x = b", standard] -lemmas split_if_eq2 = split_if [of "%x. a = x", standard] +lemmas split_if_eq1 = split_if [of "%x. x = b"] for b +lemmas split_if_eq2 = split_if [of "%x. a = x"] for x -lemmas split_if_mem1 = split_if [of "%x. x : b", standard] -lemmas split_if_mem2 = split_if [of "%x. a : x", standard] +lemmas split_if_mem1 = split_if [of "%x. x : b"] for b +lemmas split_if_mem2 = split_if [of "%x. a : x"] for x lemmas split_ifs = split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2 @@ -303,7 +303,7 @@ lemma succ_not_0 [simp]: "succ(n) ~= 0" by (blast elim!: equalityE) -lemmas succ_neq_0 = succ_not_0 [THEN notE, standard, elim!] +lemmas succ_neq_0 = succ_not_0 [THEN notE, elim!] declare succ_not_0 [THEN not_sym, simp] declare sym [THEN succ_neq_0, elim!] @@ -312,12 +312,12 @@ lemmas succ_subsetD = succI1 [THEN [2] subsetD] (* succ(b) ~= b *) -lemmas succ_neq_self = succI1 [THEN mem_imp_not_eq, THEN not_sym, standard] +lemmas succ_neq_self = succI1 [THEN mem_imp_not_eq, THEN not_sym] lemma succ_inject_iff [simp]: "succ(m) = succ(n) <-> m=n" by (blast elim: mem_asym elim!: equalityE) -lemmas succ_inject = succ_inject_iff [THEN iffD1, standard, dest!] +lemmas succ_inject = succ_inject_iff [THEN iffD1, dest!] subsection{*Miniscoping of the Bounded Universal Quantifier*}