# HG changeset patch # User paulson # Date 1064565297 -7200 # Node ID 144f45277d5a8c37d6bed25d1c936a5f9e424548 # Parent f20fbb1416732b9643b644c9b71db8ac14688d56 misc tidying diff -r f20fbb141673 -r 144f45277d5a src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Fri Sep 26 10:34:28 2003 +0200 +++ b/src/HOL/Datatype.thy Fri Sep 26 10:34:57 2003 +0200 @@ -55,11 +55,9 @@ show P apply (rule r) apply (rule ext) - apply (cut_tac x = "Inl x" in a [THEN fun_cong]) - apply simp + apply (cut_tac x = "Inl x" in a [THEN fun_cong], simp) apply (rule ext) - apply (cut_tac x = "Inr x" in a [THEN fun_cong]) - apply simp + apply (cut_tac x = "Inr x" in a [THEN fun_cong], simp) done qed @@ -89,8 +87,7 @@ lemma prod_cases3 [case_names fields, cases type]: "(!!a b c. y = (a, b, c) ==> P) ==> P" apply (cases y) - apply (case_tac b) - apply blast + apply (case_tac b, blast) done lemma prod_induct3 [case_names fields, induct type]: @@ -100,8 +97,7 @@ lemma prod_cases4 [case_names fields, cases type]: "(!!a b c d. y = (a, b, c, d) ==> P) ==> P" apply (cases y) - apply (case_tac c) - apply blast + apply (case_tac c, blast) done lemma prod_induct4 [case_names fields, induct type]: @@ -111,8 +107,7 @@ lemma prod_cases5 [case_names fields, cases type]: "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P" apply (cases y) - apply (case_tac d) - apply blast + apply (case_tac d, blast) done lemma prod_induct5 [case_names fields, induct type]: @@ -122,8 +117,7 @@ lemma prod_cases6 [case_names fields, cases type]: "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P" apply (cases y) - apply (case_tac e) - apply blast + apply (case_tac e, blast) done lemma prod_induct6 [case_names fields, induct type]: @@ -133,8 +127,7 @@ lemma prod_cases7 [case_names fields, cases type]: "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P" apply (cases y) - apply (case_tac f) - apply blast + apply (case_tac f, blast) done lemma prod_induct7 [case_names fields, induct type]: diff -r f20fbb141673 -r 144f45277d5a src/HOL/Divides.thy --- a/src/HOL/Divides.thy Fri Sep 26 10:34:28 2003 +0200 +++ b/src/HOL/Divides.thy Fri Sep 26 10:34:57 2003 +0200 @@ -90,8 +90,7 @@ "0 < n \ (n * q <= m \ m < n * (Suc q)) = (q = ((m::nat) div n))" apply (rule iffI) apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient) - apply (simp_all add: quorem_def) - apply arith + apply (simp_all add: quorem_def, arith) apply (rule conjI) apply (rule_tac P="%x. n * (m div n) \ x" in subst [OF mod_div_equality [of _ n]]) @@ -99,8 +98,7 @@ apply (rule_tac P="%x. x < n + n * (m div n)" in subst [OF mod_div_equality [of _ n]]) apply (simp only: add: mult_ac add_ac) - apply (rule add_less_mono1) - apply simp + apply (rule add_less_mono1, simp) done theorem split_div': diff -r f20fbb141673 -r 144f45277d5a src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Fri Sep 26 10:34:28 2003 +0200 +++ b/src/HOL/Finite_Set.thy Fri Sep 26 10:34:57 2003 +0200 @@ -115,8 +115,7 @@ lemma finite_insert [simp]: "finite (insert a A) = finite A" apply (subst insert_is_Un) - apply (simp only: finite_Un) - apply blast + apply (simp only: finite_Un, blast) done lemma finite_empty_induct: @@ -158,8 +157,7 @@ apply (subst Diff_insert) apply (case_tac "a : A - B") apply (rule finite_insert [symmetric, THEN trans]) - apply (subst insert_Diff) - apply simp_all + apply (subst insert_Diff, simp_all) done @@ -171,8 +169,7 @@ lemma finite_range_imageI: "finite (range g) ==> finite (range (%x. f (g x)))" - apply (drule finite_imageI) - apply simp + apply (drule finite_imageI, simp) done lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A" @@ -186,11 +183,9 @@ apply (subgoal_tac "EX y:A. f y = x & F = f ` (A - {y})") apply clarify apply (simp (no_asm_use) add: inj_on_def) - apply (blast dest!: aux [THEN iffD1]) - apply atomize + apply (blast dest!: aux [THEN iffD1], atomize) apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl) - apply (frule subsetD [OF equalityD2 insertI1]) - apply clarify + apply (frule subsetD [OF equalityD2 insertI1], clarify) apply (rule_tac x = xa in bexI) apply (simp_all add: inj_on_image_set_diff) done @@ -240,8 +235,7 @@ "finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)" apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)") apply (erule ssubst) - apply (erule finite_SigmaI) - apply auto + apply (erule finite_SigmaI, auto) done instance unit :: finite @@ -281,8 +275,7 @@ apply (erule finite_imageD [unfolded inj_on_def]) apply (simp split add: split_split) apply (erule finite_imageI) - apply (simp add: converse_def image_def) - apply auto + apply (simp add: converse_def image_def, auto) apply (rule bexI) prefer 2 apply assumption apply simp @@ -314,8 +307,7 @@ "(ALL i:N. i < (n::nat)) ==> finite N" -- {* A bounded set of natural numbers is finite. *} apply (rule finite_subset) - apply (rule_tac [2] finite_lessThan) - apply auto + apply (rule_tac [2] finite_lessThan, auto) done @@ -373,10 +365,8 @@ lemma cardR_determ_aux1: "(A, m): cardR ==> (!!n a. m = Suc n ==> a:A ==> (A - {a}, n) : cardR)" - apply (induct set: cardR) - apply auto - apply (simp add: insert_Diff_if) - apply auto + apply (induct set: cardR, auto) + apply (simp add: insert_Diff_if, auto) apply (drule cardR_SucD) apply (blast intro!: cardR.intros) done @@ -390,8 +380,7 @@ apply (rename_tac B b m) apply (case_tac "a = b") apply (subgoal_tac "A = B") - prefer 2 apply (blast elim: equalityE) - apply blast + prefer 2 apply (blast elim: equalityE, blast) apply (subgoal_tac "EX C. A = insert b C & B = insert a C") prefer 2 apply (rule_tac x = "A Int B" in exI) @@ -433,10 +422,8 @@ lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})" apply auto - apply (drule_tac a = x in mk_disjoint_insert) - apply clarify - apply (rotate_tac -1) - apply auto + apply (drule_tac a = x in mk_disjoint_insert, clarify) + apply (rotate_tac -1, auto) done lemma card_insert_if: @@ -444,10 +431,7 @@ by (simp add: insert_absorb) lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A" - apply (rule_tac t = A in insert_Diff [THEN subst]) - apply assumption - apply simp - done +by (rule_tac t = A in insert_Diff [THEN subst], assumption, simp) lemma card_Diff_singleton: "finite A ==> x: A ==> card (A - {x}) = card A - 1" @@ -464,16 +448,12 @@ by (simp add: card_insert_if) lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)" - apply (induct set: Finites) - apply simp - apply clarify + apply (induct set: Finites, simp, clarify) apply (subgoal_tac "finite A & A - {x} <= F") - prefer 2 apply (blast intro: finite_subset) - apply atomize + prefer 2 apply (blast intro: finite_subset, atomize) apply (drule_tac x = "A - {x}" in spec) apply (simp add: card_Diff_singleton_if split add: split_if_asm) - apply (case_tac "card A") - apply auto + apply (case_tac "card A", auto) done lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B" @@ -482,16 +462,14 @@ done lemma card_mono: "finite B ==> A <= B ==> card A <= card B" - apply (case_tac "A = B") - apply simp + apply (case_tac "A = B", simp) apply (simp add: linorder_not_less [symmetric]) apply (blast dest: card_seteq intro: order_less_imp_le) done lemma card_Un_Int: "finite A ==> finite B ==> card A + card B = card (A Un B) + card (A Int B)" - apply (induct set: Finites) - apply simp + apply (induct set: Finites, simp) apply (simp add: insert_absorb Int_insert_left) done @@ -530,30 +508,22 @@ done lemma card_psubset: "finite B ==> A \ B ==> card A < card B ==> A < B" - apply (erule psubsetI) - apply blast - done +by (erule psubsetI, blast) subsubsection {* Cardinality of image *} lemma card_image_le: "finite A ==> card (f ` A) <= card A" - apply (induct set: Finites) - apply simp + apply (induct set: Finites, simp) apply (simp add: le_SucI finite_imageI card_insert_if) done lemma card_image: "finite A ==> inj_on f A ==> card (f ` A) = card A" - apply (induct set: Finites) - apply simp_all - apply atomize + apply (induct set: Finites, simp_all, atomize) apply safe - apply (unfold inj_on_def) - apply blast + apply (unfold inj_on_def, blast) apply (subst card_insert_disjoint) - apply (erule finite_imageI) - apply blast - apply blast + apply (erule finite_imageI, blast, blast) done lemma endo_inj_surj: "finite A ==> f ` A \ A ==> inj_on f A ==> f ` A = A" @@ -565,10 +535,8 @@ lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A" (* FIXME numeral 2 (!?) *) apply (induct set: Finites) apply (simp_all add: Pow_insert) - apply (subst card_Un_disjoint) - apply blast - apply (blast intro: finite_imageI) - apply blast + apply (subst card_Un_disjoint, blast) + apply (blast intro: finite_imageI, blast) apply (subgoal_tac "inj_on (insert x) (Pow F)") apply (simp add: card_image Pow_insert) apply (unfold inj_on_def) @@ -585,9 +553,7 @@ ALL c : C. k dvd card c ==> (ALL c1: C. ALL c2: C. c1 ~= c2 --> c1 Int c2 = {}) ==> k dvd card (Union C)" - apply (induct set: Finites) - apply simp_all - apply clarify + apply (induct set: Finites, simp_all, clarify) apply (subst card_Un_disjoint) apply (auto simp add: dvd_add disjoint_eq_subset_Compl) done @@ -615,9 +581,7 @@ "fold f e A == THE x. (A, x) : foldSet f e" lemma Diff1_foldSet: "(A - {x}, y) : foldSet f e ==> x: A ==> (A, f x y) : foldSet f e" - apply (erule insert_Diff [THEN subst], rule foldSet.intros) - apply auto - done +by (erule insert_Diff [THEN subst], rule foldSet.intros, auto) lemma foldSet_imp_finite [simp]: "(A, x) : foldSet f e ==> finite A" by (induct set: foldSet) auto @@ -637,23 +601,18 @@ (ALL y. (A, y) : foldSet f e --> y = x)" apply (induct n) apply (auto simp add: less_Suc_eq) - apply (erule foldSet.cases) - apply blast - apply (erule foldSet.cases) - apply blast - apply clarify + apply (erule foldSet.cases, blast) + apply (erule foldSet.cases, blast, clarify) txt {* force simplification of @{text "card A < card (insert ...)"}. *} apply (erule rev_mp) apply (simp add: less_Suc_eq_le) apply (rule impI) apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb") apply (subgoal_tac "Aa = Ab") - prefer 2 apply (blast elim!: equalityE) - apply blast + prefer 2 apply (blast elim!: equalityE, blast) txt {* case @{prop "xa \ xb"}. *} apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab") - prefer 2 apply (blast elim!: equalityE) - apply clarify + prefer 2 apply (blast elim!: equalityE, clarify) apply (subgoal_tac "Aa = insert xb Ab - {xa}") prefer 2 apply blast apply (subgoal_tac "card Aa <= card Ab") @@ -700,16 +659,14 @@ done lemma (in LC) fold_commute: "finite A ==> (!!e. f x (fold f e A) = fold f (f x e) A)" - apply (induct set: Finites) - apply simp + apply (induct set: Finites, simp) apply (simp add: left_commute fold_insert) done lemma (in LC) fold_nest_Un_Int: "finite A ==> finite B ==> fold f (fold f e B) A = fold f (fold f e (A Int B)) (A Un B)" - apply (induct set: Finites) - apply simp + apply (induct set: Finites, simp) apply (simp add: fold_insert fold_commute Int_insert_left insert_absorb) done @@ -757,8 +714,7 @@ lemma (in ACe) fold_Un_Int: "finite A ==> finite B ==> fold f e A \ fold f e B = fold f e (A Un B) \ fold f e (A Int B)" - apply (induct set: Finites) - apply simp + apply (induct set: Finites, simp) apply (simp add: AC insert_absorb Int_insert_left LC.fold_insert [OF LC.intro]) done @@ -823,8 +779,7 @@ lemma setsum_0: "setsum (\i. 0) A = 0" apply (case_tac "finite A") prefer 2 apply (simp add: setsum_def) - apply (erule finite_induct) - apply auto + apply (erule finite_induct, auto) done lemma setsum_eq_0_iff [simp]: @@ -835,8 +790,7 @@ apply (case_tac "finite A") prefer 2 apply (simp add: setsum_def) apply (erule rev_mp) - apply (erule finite_induct) - apply auto + apply (erule finite_induct, auto) done lemma card_eq_setsum: "finite A ==> card A = setsum (\x. 1) A" @@ -846,15 +800,13 @@ lemma setsum_Un_Int: "finite A ==> finite B ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B" -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *} - apply (induct set: Finites) - apply simp + apply (induct set: Finites, simp) apply (simp add: plus_ac0 Int_insert_left insert_absorb) done lemma setsum_Un_disjoint: "finite A ==> finite B ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B" - apply (subst setsum_Un_Int [symmetric]) - apply auto + apply (subst setsum_Un_Int [symmetric], auto) done lemma setsum_UN_disjoint: @@ -863,9 +815,7 @@ "finite I ==> (ALL i:I. finite (A i)) ==> (ALL i:I. ALL j:I. i \ j --> A i Int A j = {}) ==> setsum f (UNION I A) = setsum (\i. setsum f (A i)) I" - apply (induct set: Finites) - apply simp - apply atomize + apply (induct set: Finites, simp, atomize) apply (subgoal_tac "ALL i:F. x \ i") prefer 2 apply blast apply (subgoal_tac "A x Int UNION F A = {}") @@ -876,16 +826,14 @@ lemma setsum_addf: "setsum (\x. f x + g x) A = (setsum f A + setsum g A)" apply (case_tac "finite A") prefer 2 apply (simp add: setsum_def) - apply (erule finite_induct) - apply auto + apply (erule finite_induct, auto) apply (simp add: plus_ac0) done lemma setsum_Un: "finite A ==> finite B ==> (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)" -- {* For the natural numbers, we have subtraction. *} - apply (subst setsum_Un_Int [symmetric]) - apply auto + apply (subst setsum_Un_Int [symmetric], auto) done lemma setsum_diff1: "(setsum f (A - {a}) :: nat) = @@ -894,21 +842,17 @@ prefer 2 apply (simp add: setsum_def) apply (erule finite_induct) apply (auto simp add: insert_Diff_if) - apply (drule_tac a = a in mk_disjoint_insert) - apply auto + apply (drule_tac a = a in mk_disjoint_insert, auto) done lemma setsum_cong: "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B" apply (case_tac "finite B") - prefer 2 apply (simp add: setsum_def) - apply simp + prefer 2 apply (simp add: setsum_def, simp) apply (subgoal_tac "ALL C. C <= B --> (ALL x:C. f x = g x) --> setsum f C = setsum g C") apply simp - apply (erule finite_induct) - apply simp - apply (simp add: subset_insert_iff) - apply clarify + apply (erule finite_induct, simp) + apply (simp add: subset_insert_iff, clarify) apply (subgoal_tac "finite C") prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl]) apply (subgoal_tac "C = insert x (C - {x})") @@ -1019,8 +963,7 @@ apply safe apply (auto intro: finite_subset [THEN card_insert_disjoint]) apply (drule_tac x = "xa - {x}" in spec) - apply (subgoal_tac "x ~: xa") - apply auto + apply (subgoal_tac "x ~: xa", auto) apply (erule rev_mp, subst card_Diff_singleton) apply (auto intro: finite_subset) done @@ -1057,8 +1000,7 @@ lemma n_sub_lemma: "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)" apply (induct k) - apply (simp add: card_s_0_eq_empty) - apply atomize + apply (simp add: card_s_0_eq_empty, atomize) apply (rotate_tac -1, erule finite_induct) apply (simp_all (no_asm_simp) cong add: conj_cong add: card_s_0_eq_empty choose_deconstruct) diff -r f20fbb141673 -r 144f45277d5a src/HOL/HOL.thy --- a/src/HOL/HOL.thy Fri Sep 26 10:34:28 2003 +0200 +++ b/src/HOL/HOL.thy Fri Sep 26 10:34:57 2003 +0200 @@ -489,14 +489,11 @@ lemma split_if: "P (if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" apply (rule case_split [of Q]) apply (subst if_P) - prefer 3 apply (subst if_not_P) - apply blast+ + prefer 3 apply (subst if_not_P, blast+) done lemma split_if_asm: "P (if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))" - apply (subst split_if) - apply blast - done +by (subst split_if, blast) lemmas if_splits = split_if split_if_asm @@ -504,14 +501,10 @@ by (rule split_if) lemma if_cancel: "(if c then x else x) = x" - apply (subst split_if) - apply blast - done +by (subst split_if, blast) lemma if_eq_cancel: "(if x = y then y else x) = x" - apply (subst split_if) - apply blast - done +by (subst split_if, blast) lemma if_bool_eq_conj: "(if P then Q else R) = ((P-->Q) & (~P-->R))" -- {* This form is useful for expanding @{text if}s on the RIGHT of the @{text "==>"} symbol. *} @@ -519,8 +512,7 @@ lemma if_bool_eq_disj: "(if P then Q else R) = ((P&Q) | (~P&R))" -- {* And this form is useful for expanding @{text if}s on the LEFT. *} - apply (subst split_if) - apply blast + apply (subst split_if, blast) done lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) rules @@ -552,8 +544,7 @@ apply (erule impE) apply (rule allI) apply (rule_tac P = "xa = x" in case_split_thm) - apply (drule_tac [3] x = x in fun_cong) - apply simp_all + apply (drule_tac [3] x = x in fun_cong, simp_all) done text{*Needs only HOL-lemmas:*} @@ -706,8 +697,7 @@ lemma order_le_less: "((x::'a::order) <= y) = (x < y | x = y)" -- {* NOT suitable for iff, since it can cause PROOF FAILED. *} - apply (simp add: order_less_le) - apply blast + apply (simp add: order_less_le, blast) done lemmas order_le_imp_less_or_eq = order_le_less [THEN iffD1, standard] @@ -723,8 +713,7 @@ lemma order_less_asym: "x < (y::'a::order) ==> (~P ==> y < x) ==> P" apply (drule order_less_not_sym) - apply (erule contrapos_np) - apply simp + apply (erule contrapos_np, simp) done @@ -806,14 +795,12 @@ lemma linorder_less_linear: "!!x::'a::linorder. x P) ==> (x = y ==> P) ==> (y < x ==> P) ==> P" - apply (insert linorder_less_linear) - apply blast + apply (insert linorder_less_linear, blast) done lemma linorder_not_less: "!!x::'a::linorder. (~ x < y) = (y <= x)" @@ -829,14 +816,10 @@ done lemma linorder_neq_iff: "!!x::'a::linorder. (x ~= y) = (x (x < y ==> R) ==> (y < x ==> R) ==> R" - apply (simp add: linorder_neq_iff) - apply blast - done +by (simp add: linorder_neq_iff, blast) subsubsection "Min and max on (linear) orders" diff -r f20fbb141673 -r 144f45277d5a src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Fri Sep 26 10:34:28 2003 +0200 +++ b/src/HOL/Hilbert_Choice.thy Fri Sep 26 10:34:57 2003 +0200 @@ -72,17 +72,13 @@ ==> (!!x. P x ==> \y. P y --> m x \ m y ==> Q x) ==> Q (LeastM m P)" apply (unfold LeastM_def) - apply (rule someI2_ex) - apply blast - apply blast + apply (rule someI2_ex, blast, blast) done lemma LeastM_equality: "P k ==> (!!x. P x ==> m k <= m x) ==> m (LEAST x WRT m. P x) = (m k::'a::order)" - apply (rule LeastMI2) - apply assumption - apply blast + apply (rule LeastMI2, assumption, blast) apply (blast intro!: order_antisym) done @@ -90,16 +86,14 @@ "wf r ==> ALL x y. ((x,y):r^+) = ((y,x)~:r^*) ==> P k ==> EX x. P x & (!y. P y --> (m x,m y):r^*)" apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]]) - apply (drule_tac x = "m`Collect P" in spec) - apply force + apply (drule_tac x = "m`Collect P" in spec, force) done lemma ex_has_least_nat: "P k ==> EX x. P x & (ALL y. P y --> m x <= (m y::nat))" apply (simp only: pred_nat_trancl_eq_le [symmetric]) apply (rule wf_pred_nat [THEN wf_linord_ex_has_least]) - apply (simp add: less_eq not_le_iff_less pred_nat_trancl_eq_le) - apply assumption + apply (simp add: less_eq not_le_iff_less pred_nat_trancl_eq_le, assumption) done lemma LeastM_nat_lemma: @@ -112,10 +106,7 @@ lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1, standard] lemma LeastM_nat_le: "P x ==> m (LeastM m P) <= (m x::nat)" - apply (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp]) - apply assumption - apply assumption - done +by (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp], assumption, assumption) subsection {* Greatest value operator *} @@ -139,32 +130,26 @@ ==> (!!x. P x ==> \y. P y --> m y \ m x ==> Q x) ==> Q (GreatestM m P)" apply (unfold GreatestM_def) - apply (rule someI2_ex) - apply blast - apply blast + apply (rule someI2_ex, blast, blast) done lemma GreatestM_equality: "P k ==> (!!x. P x ==> m x <= m k) ==> m (GREATEST x WRT m. P x) = (m k::'a::order)" - apply (rule_tac m = m in GreatestMI2) - apply assumption - apply blast + apply (rule_tac m = m in GreatestMI2, assumption, blast) apply (blast intro!: order_antisym) done lemma Greatest_equality: "P (k::'a::order) ==> (!!x. P x ==> x <= k) ==> (GREATEST x. P x) = k" apply (unfold Greatest_def) - apply (erule GreatestM_equality) - apply blast + apply (erule GreatestM_equality, blast) done lemma ex_has_greatest_nat_lemma: "P k ==> ALL x. P x --> (EX y. P y & ~ ((m y::nat) <= m x)) ==> EX y. P y & ~ (m y < m k + n)" - apply (induct_tac n) - apply force + apply (induct_tac n, force) apply (force simp add: le_Suc_eq) done @@ -173,8 +158,7 @@ ==> EX x. P x & (ALL y. P y --> (m y::nat) <= m x)" apply (rule ccontr) apply (cut_tac P = P and n = "b - m k" in ex_has_greatest_nat_lemma) - apply (subgoal_tac [3] "m k <= b") - apply auto + apply (subgoal_tac [3] "m k <= b", auto) done lemma GreatestM_nat_lemma: @@ -182,8 +166,7 @@ ==> P (GreatestM m P) & (ALL y. P y --> (m y::nat) <= m (GreatestM m P))" apply (unfold GreatestM_def) apply (rule someI_ex) - apply (erule ex_has_greatest_nat) - apply assumption + apply (erule ex_has_greatest_nat, assumption) done lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1, standard] @@ -199,15 +182,13 @@ lemma GreatestI: "P (k::nat) ==> ALL y. P y --> y < b ==> P (GREATEST x. P x)" apply (unfold Greatest_def) - apply (rule GreatestM_natI) - apply auto + apply (rule GreatestM_natI, auto) done lemma Greatest_le: "P x ==> ALL y. P y --> y < b ==> (x::nat) <= (GREATEST x. P x)" apply (unfold Greatest_def) - apply (rule GreatestM_nat_le) - apply auto + apply (rule GreatestM_nat_le, auto) done diff -r f20fbb141673 -r 144f45277d5a src/HOL/List.thy --- a/src/HOL/List.thy Fri Sep 26 10:34:28 2003 +0200 +++ b/src/HOL/List.thy Fri Sep 26 10:34:57 2003 +0200 @@ -282,16 +282,13 @@ lemma Suc_length_conv: "(Suc n = length xs) = (\y ys. xs = y # ys \ length ys = n)" -apply (induct xs) - apply simp -apply simp +apply (induct xs, simp, simp) apply blast done lemma impossible_Cons [rule_format]: "length xs <= length ys --> xs = x # ys = False" -apply (induct xs) -apply auto +apply (induct xs, auto) done @@ -319,12 +316,8 @@ "!!ys. length xs = length ys \ length us = length vs ==> (xs@us = ys@vs) = (xs=ys \ us=vs)" apply (induct xs) - apply (case_tac ys) -apply simp - apply force -apply (case_tac ys) - apply force -apply simp + apply (case_tac ys, simp, force) +apply (case_tac ys, force, simp) done lemma same_append_eq [iff]: "(xs @ ys = xs @ zs) = (ys = zs)" @@ -486,12 +479,9 @@ by (rules dest: map_injective injD intro: inj_onI) lemma inj_mapD: "inj (map f) ==> inj f" -apply (unfold inj_on_def) -apply clarify +apply (unfold inj_on_def, clarify) apply (erule_tac x = "[x]" in ballE) - apply (erule_tac x = "[y]" in ballE) -apply simp - apply blast + apply (erule_tac x = "[y]" in ballE, simp, blast) apply blast done @@ -514,11 +504,8 @@ by (induct xs) auto lemma rev_is_rev_conv [iff]: "!!ys. (rev xs = rev ys) = (xs = ys)" -apply (induct xs) - apply force -apply (case_tac ys) - apply simp -apply force +apply (induct xs, force) +apply (case_tac ys, simp, force) done lemma rev_induct [case_names Nil snoc]: @@ -545,9 +532,7 @@ by (induct xs) auto lemma hd_in_set: "l = x#xs \ x\set l" -apply (case_tac l) -apply auto -done +by (case_tac l, auto) lemma set_subset_Cons: "set xs \ set (x # xs)" by auto @@ -568,21 +553,16 @@ by (induct xs) auto lemma set_upt [simp]: "set[i..j(] = {k. i \ k \ k < j}" -apply (induct j) - apply simp_all -apply(erule ssubst) -apply auto +apply (induct j, simp_all) +apply (erule ssubst, auto) done lemma in_set_conv_decomp: "(x : set xs) = (\ys zs. xs = ys @ x # zs)" -apply (induct xs) - apply simp -apply simp +apply (induct xs, simp, simp) apply (rule iffI) apply (blast intro: eq_Nil_appendI Cons_eq_appendI) apply (erule exE)+ -apply (case_tac ys) -apply auto +apply (case_tac ys, auto) done lemma in_lists_conv_set: "(xs : lists A) = (\x \ set xs. x : A)" @@ -674,33 +654,23 @@ lemma nth_append: "!!n. (xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))" -apply(induct "xs") - apply simp -apply (case_tac n) - apply auto +apply (induct "xs", simp) +apply (case_tac n, auto) done lemma nth_map [simp]: "!!n. n < length xs ==> (map f xs)!n = f(xs!n)" -apply(induct xs) - apply simp -apply (case_tac n) - apply auto +apply (induct xs, simp) +apply (case_tac n, auto) done lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}" -apply (induct_tac xs) - apply simp -apply simp +apply (induct_tac xs, simp, simp) apply safe -apply (rule_tac x = 0 in exI) -apply simp - apply (rule_tac x = "Suc i" in exI) - apply simp -apply (case_tac i) - apply simp +apply (rule_tac x = 0 in exI, simp) + apply (rule_tac x = "Suc i" in exI, simp) +apply (case_tac i, simp) apply (rename_tac j) -apply (rule_tac x = j in exI) -apply simp +apply (rule_tac x = j in exI, simp) done lemma list_ball_nth: "[| n < length xs; !x : set xs. P x|] ==> P(xs!n)" @@ -738,8 +708,7 @@ by (induct xs) (auto split: nat.split) lemma list_update_id[simp]: "!!i. i < length xs \ xs[i := xs!i] = xs" -apply(induct xs) - apply simp +apply (induct xs, simp) apply(simp split:nat.splits) done @@ -749,8 +718,7 @@ lemma list_update_append1: "!!i. i < size xs \ (xs @ ys)[i:=x] = xs[i:=x] @ ys" -apply(induct xs) - apply simp +apply (induct xs, simp) apply(simp split:nat.split) done @@ -816,17 +784,14 @@ by(induct xs, simp_all add:drop_Cons drop_Suc split:nat.split) lemma nth_via_drop: "!!n. drop n xs = y#ys \ xs!n = y" -apply(induct xs) - apply simp +apply (induct xs, simp) apply(simp add:drop_Cons nth_Cons split:nat.splits) done lemma take_Suc_conv_app_nth: "!!i. i < length xs \ take (Suc i) xs = take i xs @ [xs!i]" -apply(induct xs) - apply simp -apply(case_tac i) -apply auto +apply (induct xs, simp) +apply (case_tac i, auto) done lemma length_take [simp]: "!!xs. length (take n xs) = min (length xs) n" @@ -850,78 +815,56 @@ by (induct n) (auto, case_tac xs, auto) lemma take_take [simp]: "!!xs n. take n (take m xs) = take (min n m) xs" -apply (induct m) - apply auto -apply (case_tac xs) - apply auto -apply (case_tac na) - apply auto +apply (induct m, auto) +apply (case_tac xs, auto) +apply (case_tac na, auto) done lemma drop_drop [simp]: "!!xs. drop n (drop m xs) = drop (n + m) xs" -apply (induct m) - apply auto -apply (case_tac xs) - apply auto +apply (induct m, auto) +apply (case_tac xs, auto) done lemma take_drop: "!!xs n. take n (drop m xs) = drop m (take (n + m) xs)" -apply (induct m) - apply auto -apply (case_tac xs) - apply auto +apply (induct m, auto) +apply (case_tac xs, auto) done lemma append_take_drop_id [simp]: "!!xs. take n xs @ drop n xs = xs" -apply (induct n) - apply auto -apply (case_tac xs) - apply auto +apply (induct n, auto) +apply (case_tac xs, auto) done lemma take_map: "!!xs. take n (map f xs) = map f (take n xs)" -apply (induct n) - apply auto -apply (case_tac xs) - apply auto +apply (induct n, auto) +apply (case_tac xs, auto) done lemma drop_map: "!!xs. drop n (map f xs) = map f (drop n xs)" -apply (induct n) - apply auto -apply (case_tac xs) - apply auto +apply (induct n, auto) +apply (case_tac xs, auto) done lemma rev_take: "!!i. rev (take i xs) = drop (length xs - i) (rev xs)" -apply (induct xs) - apply auto -apply (case_tac i) - apply auto +apply (induct xs, auto) +apply (case_tac i, auto) done lemma rev_drop: "!!i. rev (drop i xs) = take (length xs - i) (rev xs)" -apply (induct xs) - apply auto -apply (case_tac i) - apply auto +apply (induct xs, auto) +apply (case_tac i, auto) done lemma nth_take [simp]: "!!n i. i < n ==> (take n xs)!i = xs!i" -apply (induct xs) - apply auto -apply (case_tac n) - apply(blast ) -apply (case_tac i) - apply auto +apply (induct xs, auto) +apply (case_tac n, blast) +apply (case_tac i, auto) done lemma nth_drop [simp]: "!!xs i. n + i <= length xs ==> (drop n xs)!i = xs!(n + i)" -apply (induct n) - apply auto -apply (case_tac xs) - apply auto +apply (induct n, auto) +apply (case_tac xs, auto) done lemma set_take_subset: "\n. set(take n xs) \ set xs" @@ -938,11 +881,8 @@ lemma append_eq_conv_conj: "!!zs. (xs @ ys = zs) = (xs = take (length xs) zs \ ys = drop (length xs) zs)" -apply(induct xs) - apply simp -apply clarsimp -apply (case_tac zs) -apply auto +apply (induct xs, simp, clarsimp) +apply (case_tac zs, auto) done lemma take_add [rule_format]: @@ -1004,28 +944,22 @@ lemma length_zip [simp]: "!!xs. length (zip xs ys) = min (length xs) (length ys)" -apply(induct ys) - apply simp -apply (case_tac xs) - apply auto +apply (induct ys, simp) +apply (case_tac xs, auto) done lemma zip_append1: "!!xs. zip (xs @ ys) zs = zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)" -apply (induct zs) - apply simp -apply (case_tac xs) - apply simp_all +apply (induct zs, simp) +apply (case_tac xs, simp_all) done lemma zip_append2: "!!ys. zip xs (ys @ zs) = zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs" -apply (induct xs) - apply simp -apply (case_tac ys) - apply simp_all +apply (induct xs, simp) +apply (case_tac ys, simp_all) done lemma zip_append [simp]: @@ -1035,16 +969,13 @@ lemma zip_rev: "!!xs. length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)" -apply(induct ys) - apply simp -apply (case_tac xs) - apply simp_all +apply (induct ys, simp) +apply (case_tac xs, simp_all) done lemma nth_zip [simp]: "!!i xs. [| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)" -apply (induct ys) - apply simp +apply (induct ys, simp) apply (case_tac xs) apply (simp_all add: nth.simps split: nat.split) done @@ -1059,10 +990,8 @@ lemma zip_replicate [simp]: "!!j. zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)" -apply (induct i) - apply auto -apply (case_tac j) - apply auto +apply (induct i, auto) +apply (case_tac j, auto) done @@ -1105,8 +1034,7 @@ apply (rule iffI) apply (rule_tac x = "take (length xs) zs" in exI) apply (rule_tac x = "drop (length xs) zs" in exI) - apply (force split: nat_diff_split simp add: min_def) -apply clarify + apply (force split: nat_diff_split simp add: min_def, clarify) apply (simp add: ball_Un) done @@ -1118,18 +1046,15 @@ apply (rule iffI) apply (rule_tac x = "take (length ys) xs" in exI) apply (rule_tac x = "drop (length ys) xs" in exI) - apply (force split: nat_diff_split simp add: min_def) -apply clarify + apply (force split: nat_diff_split simp add: min_def, clarify) apply (simp add: ball_Un) done lemma list_all2_append: "\b. length a = length b \ list_all2 P (a@c) (b@d) = (list_all2 P a b \ list_all2 P c d)" - apply (induct a) - apply simp - apply (case_tac b) - apply auto + apply (induct a, simp) + apply (case_tac b, auto) done lemma list_all2_appendI [intro?, trans]: @@ -1185,20 +1110,15 @@ lemma list_all2_dropI [intro?]: "\n bs. list_all2 P as bs \ list_all2 P (drop n as) (drop n bs)" - apply (induct as) - apply simp + apply (induct as, simp) apply (clarsimp simp add: list_all2_Cons1) - apply (case_tac n) - apply simp - apply simp + apply (case_tac n, simp, simp) done lemma list_all2_mono [intro?]: "\y. list_all2 P x y \ (\x y. P x y \ Q x y) \ list_all2 Q x y" - apply (induct x) - apply simp - apply (case_tac y) - apply auto + apply (induct x, simp) + apply (case_tac y, auto) done @@ -1231,7 +1151,7 @@ Nil: "(a, [],a) : fold_rel R" Cons: "[|(a,x,b) : R; (b,xs,c) : fold_rel R|] ==> (a,x#xs,c) : fold_rel R" inductive_cases fold_rel_elim_case [elim!]: - "(a, [] , b) : fold_rel R" + "(a, [] , b) : fold_rel R" "(a, x#xs, b) : fold_rel R" lemma fold_rel_Nil [intro!]: "a = b ==> (a, [], b) : fold_rel R" @@ -1255,8 +1175,7 @@ lemma upt_conv_Cons: "i < j ==> [i..j(] = i # [Suc i..j(]" apply(rule trans) apply(subst upt_rec) - prefer 2 apply(rule refl) -apply simp + prefer 2 apply (rule refl, simp) done lemma upt_add_eq_append: "i<=j ==> [i..j+k(] = [i..j(]@[j..j+k(]" @@ -1272,8 +1191,7 @@ done lemma take_upt [simp]: "!!i. i+m <= n ==> take m [i..n(] = [i..i+m(]" -apply (induct m) - apply simp +apply (induct m, simp) apply (subst upt_rec) apply (rule sym) apply (subst upt_rec) @@ -1293,13 +1211,10 @@ "!!xs ys. k <= length xs ==> k <= length ys ==> (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys" apply (atomize, induct k) -apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib) -apply clarify +apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib, clarify) txt {* Both lists must be non-empty *} -apply (case_tac xs) - apply simp -apply (case_tac ys) - apply clarify +apply (case_tac xs, simp) +apply (case_tac ys, clarify) apply (simp (no_asm_use)) apply clarify txt {* prenexing's needed, not miniscoping *} @@ -1318,9 +1233,7 @@ "\ (\x y. \P x y; Q y x\ \ x = y); list_all2 P xs ys; list_all2 Q ys xs \ \ xs = ys" apply (simp add: list_all2_conv_all_nth) - apply (rule nth_equalityI) - apply blast - apply simp + apply (rule nth_equalityI, blast, simp) done lemma take_equalityI: "(\i. take i xs = take i ys) ==> xs = ys" @@ -1350,27 +1263,19 @@ it is useful. *} lemma distinct_conv_nth: "distinct xs = (\i j. i < size xs \ j < size xs \ i \ j --> xs!i \ xs!j)" -apply (induct_tac xs) - apply simp -apply simp -apply (rule iffI) - apply clarsimp +apply (induct_tac xs, simp, simp) +apply (rule iffI, clarsimp) apply (case_tac i) -apply (case_tac j) - apply simp +apply (case_tac j, simp) apply (simp add: set_conv_nth) apply (case_tac j) -apply (clarsimp simp add: set_conv_nth) - apply simp +apply (clarsimp simp add: set_conv_nth, simp) apply (rule conjI) apply (clarsimp simp add: set_conv_nth) apply (erule_tac x = 0 in allE) - apply (erule_tac x = "Suc i" in allE) - apply simp -apply clarsimp + apply (erule_tac x = "Suc i" in allE, simp, clarsimp) apply (erule_tac x = "Suc i" in allE) -apply (erule_tac x = "Suc j" in allE) -apply simp +apply (erule_tac x = "Suc j" in allE, simp) done @@ -1387,8 +1292,7 @@ by (induct n) auto lemma rev_replicate [simp]: "rev (replicate n x) = replicate n x" -apply(induct n) - apply simp +apply (induct n, simp) apply (simp add: replicate_app_Cons_same) done @@ -1405,8 +1309,7 @@ by (atomize (full), induct n) auto lemma nth_replicate[simp]: "!!i. i < n ==> (replicate n x)!i = x" -apply(induct n) - apply simp +apply (induct n, simp) apply (simp add: nth_Cons split: nat.split) done @@ -1451,14 +1354,11 @@ subsection {* Lexicographic orderings on lists *} lemma wf_lexn: "wf r ==> wf (lexn r n)" -apply (induct_tac n) - apply simp -apply simp +apply (induct_tac n, simp, simp) apply(rule wf_subset) prefer 2 apply (rule Int_lower1) apply(rule wf_prod_fun_image) - prefer 2 apply (rule inj_onI) -apply auto + prefer 2 apply (rule inj_onI, auto) done lemma lexn_length: @@ -1468,8 +1368,7 @@ lemma wf_lex [intro!]: "wf r ==> wf (lex r)" apply (unfold lex_def) apply (rule wf_UN) -apply (blast intro: wf_lexn) -apply clarify +apply (blast intro: wf_lexn, clarify) apply (rename_tac m n) apply (subgoal_tac "m \ n") prefer 2 apply blast @@ -1480,17 +1379,10 @@ "lexn r n = {(xs,ys). length xs = n \ length ys = n \ (\xys x y xs' ys'. xs= xys @ x#xs' \ ys= xys @ y # ys' \ (x, y):r)}" -apply (induct_tac n) - apply simp - apply blast -apply (simp add: image_Collect lex_prod_def) -apply safe -apply blast - apply (rule_tac x = "ab # xys" in exI) - apply simp -apply (case_tac xys) - apply simp_all -apply blast +apply (induct_tac n, simp, blast) +apply (simp add: image_Collect lex_prod_def, safe, blast) + apply (rule_tac x = "ab # xys" in exI, simp) +apply (case_tac xys, simp_all, blast) done lemma lex_conv: @@ -1518,11 +1410,8 @@ ((x, y) : r \ length xs = length ys | x = y \ (xs, ys) : lex r)" apply (simp add: lex_conv) apply (rule iffI) - prefer 2 apply (blast intro: Cons_eq_appendI) -apply clarify -apply (case_tac xys) - apply simp -apply simp + prefer 2 apply (blast intro: Cons_eq_appendI, clarify) +apply (case_tac xys, simp, simp) apply blast done @@ -1543,8 +1432,7 @@ lemma sublist_append: "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}" apply (unfold sublist_def) -apply (induct l' rule: rev_induct) - apply simp +apply (induct l' rule: rev_induct, simp) apply (simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma) apply (simp add: add_commute) done @@ -1560,8 +1448,7 @@ by (simp add: sublist_Cons) lemma sublist_upt_eq_take [simp]: "sublist l {..n(} = take n l" -apply (induct l rule: rev_induct) - apply simp +apply (induct l rule: rev_induct, simp) apply (simp split: nat_diff_split add: sublist_append) done diff -r f20fbb141673 -r 144f45277d5a src/HOL/Map.thy --- a/src/HOL/Map.thy Fri Sep 26 10:34:28 2003 +0200 +++ b/src/HOL/Map.thy Fri Sep 26 10:34:57 2003 +0200 @@ -111,7 +111,7 @@ lemma map_upd_nonempty[simp]: "t(k|->x) ~= empty" apply safe -apply (drule_tac x = "k" in fun_cong) +apply (drule_tac x = k in fun_cong) apply (simp (no_asm_use)) done @@ -126,7 +126,7 @@ apply (unfold image_def) apply (simp (no_asm_use) add: full_SetCompr_eq) apply (rule finite_subset) -prefer 2 apply (assumption) +prefer 2 apply assumption apply auto done @@ -156,22 +156,16 @@ subsection {* @{term chg_map} *} lemma chg_map_new[simp]: "m a = None ==> chg_map f a m = m" -apply (unfold chg_map_def) -apply auto -done +by (unfold chg_map_def, auto) lemma chg_map_upd[simp]: "m a = Some b ==> chg_map f a m = m(a|->f b)" -apply (unfold chg_map_def) -apply auto -done +by (unfold chg_map_def, auto) subsection {* @{term map_of} *} lemma map_of_SomeD [rule_format (no_asm)]: "map_of xs k = Some y --> (k,y):set xs" -apply (induct_tac "xs") -apply auto -done +by (induct_tac "xs", auto) lemma map_of_mapk_SomeI [rule_format (no_asm)]: "inj f ==> map_of t k = Some x --> map_of (map (split (%k. Pair (f k))) t) (f k) = Some x" @@ -180,31 +174,26 @@ done lemma weak_map_of_SomeI [rule_format (no_asm)]: "(k, x) : set l --> (? x. map_of l k = Some x)" -apply (induct_tac "l") -apply auto -done +by (induct_tac "l", auto) lemma map_of_filter_in: "[| map_of xs k = Some z; P k z |] ==> map_of (filter (split P) xs) k = Some z" apply (rule mp) -prefer 2 apply (assumption) +prefer 2 apply assumption apply (erule thin_rl) -apply (induct_tac "xs") -apply auto +apply (induct_tac "xs", auto) done lemma finite_range_map_of: "finite (range (map_of l))" apply (induct_tac "l") apply (simp_all (no_asm) add: image_constant) apply (rule finite_subset) -prefer 2 apply (assumption) +prefer 2 apply assumption apply auto done lemma map_of_map: "map_of (map (%(a,b). (a,f b)) xs) x = option_map f (map_of xs x)" -apply (induct_tac "xs") -apply auto -done +by (induct_tac "xs", auto) subsection {* @{term option_map} related *} @@ -249,9 +238,7 @@ declare map_add_SomeD [dest!] lemma map_add_find_right[simp]: "!!xx. n k = Some xx ==> (m ++ n) k = Some xx" -apply (subst map_add_Some_iff) -apply fast -done +by (subst map_add_Some_iff, fast) lemma map_add_None [iff]: "((m ++ n) k = None) = (n k = None & m k = None)" apply (unfold map_add_def) @@ -260,8 +247,7 @@ lemma map_add_upd[simp]: "f ++ g(x|->y) = (f ++ g)(x|->y)" apply (unfold map_add_def) -apply (rule ext) -apply auto +apply (rule ext, auto) done lemma map_add_upds[simp]: "m1 ++ (m2(xs[\]ys)) = (m1++m2)(xs[\]ys)" @@ -278,8 +264,7 @@ declare fun_upd_apply [simp del] lemma finite_range_map_of_map_add: "finite (range f) ==> finite (range (f ++ map_of l))" -apply (induct_tac "l") -apply auto +apply (induct_tac "l", auto) apply (erule finite_range_updI) done declare fun_upd_apply [simp] @@ -351,18 +336,14 @@ m(xs@[x] [\] ys) = m(xs [\] ys)(x \ ys!size xs)" apply(induct xs) apply(clarsimp simp add:neq_Nil_conv) -apply(case_tac ys) - apply simp -apply simp +apply (case_tac ys, simp, simp) done lemma map_upds_list_update2_drop[simp]: "\m ys i. \size xs \ i; i < size ys\ \ m(xs[\]ys[i:=y]) = m(xs[\]ys)" -apply(induct xs) - apply simp -apply(case_tac ys) - apply simp +apply (induct xs, simp) +apply (case_tac ys, simp) apply(simp split:nat.split) done @@ -370,8 +351,7 @@ (f(x|->y))(xs [|->] ys) = (if x : set(take (length ys) xs) then f(xs [|->] ys) else (f(xs [|->] ys))(x|->y))" -apply(induct xs) - apply simp +apply (induct xs, simp) apply(case_tac ys) apply(auto split:split_if simp:fun_upd_twist) done @@ -384,8 +364,7 @@ lemma map_upds_apply_nontin[simp]: "!!ys. x ~: set xs ==> (f(xs[|->]ys)) x = f x" -apply(induct xs) - apply simp +apply (induct xs, simp) apply(case_tac ys) apply(auto simp: map_upd_upds_conv_if) done @@ -393,10 +372,8 @@ lemma restrict_map_upds[simp]: "!!m ys. \ length xs = length ys; set xs \ D \ \ m(xs [\] ys)\D = (m\(D - set xs))(xs [\] ys)" -apply(induct xs) - apply simp -apply(case_tac ys) - apply simp +apply (induct xs, simp) +apply (case_tac ys, simp) apply(simp add:Diff_insert[symmetric] insert_absorb) apply(simp add: map_upd_upds_conv_if) done @@ -415,20 +392,14 @@ subsection {* @{term dom} *} lemma domI: "m a = Some b ==> a : dom m" -apply (unfold dom_def) -apply auto -done +by (unfold dom_def, auto) (* declare domI [intro]? *) lemma domD: "a : dom m ==> ? b. m a = Some b" -apply (unfold dom_def) -apply auto -done +by (unfold dom_def, auto) lemma domIff[iff]: "(a : dom m) = (m a ~= None)" -apply (unfold dom_def) -apply auto -done +by (unfold dom_def, auto) declare domIff [simp del] lemma dom_empty[simp]: "dom empty = {}" @@ -453,16 +424,12 @@ lemma dom_map_upds[simp]: "!!m ys. dom(m(xs[|->]ys)) = set(take (length ys) xs) Un dom m" -apply(induct xs) - apply simp -apply(case_tac ys) - apply auto +apply (induct xs, simp) +apply (case_tac ys, auto) done lemma dom_map_add[simp]: "dom(m++n) = dom n Un dom m" -apply (unfold dom_def) -apply auto -done +by (unfold dom_def, auto) lemma dom_overwrite[simp]: "dom(f(g|A)) = (dom f - {a. a : A - dom g}) Un {a. a : A Int dom g}" @@ -485,8 +452,7 @@ done lemma ran_map_upd[simp]: "m a = None ==> ran(m(a|->b)) = insert b (ran m)" -apply (unfold ran_def) -apply auto +apply (unfold ran_def, auto) apply (subgoal_tac "~ (aa = a) ") apply auto done @@ -507,10 +473,8 @@ lemma map_le_upds[simp]: "!!f g bs. f \\<^sub>m g ==> f(as [|->] bs) \\<^sub>m g(as [|->] bs)" -apply(induct as) - apply simp -apply(case_tac bs) - apply auto +apply (induct as, simp) +apply (case_tac bs, auto) done lemma map_le_implies_dom_le: "(f \\<^sub>m g) \ (dom f \ dom g)" @@ -525,11 +489,8 @@ lemma map_le_antisym: "\ f \\<^sub>m g; g \\<^sub>m f \ \ f = g" apply (unfold map_le_def) apply (rule ext) - apply (case_tac "x \ dom f") - apply simp - apply (case_tac "x \ dom g") - apply simp - apply fastsimp + apply (case_tac "x \ dom f", simp) + apply (case_tac "x \ dom g", simp, fastsimp) done lemma map_le_map_add [simp]: "f \\<^sub>m (g ++ f)" diff -r f20fbb141673 -r 144f45277d5a src/HOL/Nat.thy --- a/src/HOL/Nat.thy Fri Sep 26 10:34:28 2003 +0200 +++ b/src/HOL/Nat.thy Fri Sep 26 10:34:57 2003 +0200 @@ -39,7 +39,7 @@ global typedef (open Nat) - nat = "Nat" by (rule exI, rule Nat.Zero_RepI) + nat = Nat by (rule exI, rule Nat.Zero_RepI) instance nat :: ord .. instance nat :: zero .. @@ -148,27 +148,23 @@ theorem diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==> (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n" - apply (rule_tac x = "m" in spec) + apply (rule_tac x = m in spec) apply (induct_tac n) prefer 2 apply (rule allI) - apply (induct_tac x) - apply rules+ + apply (induct_tac x, rules+) done subsection {* Basic properties of "less than" *} lemma wf_pred_nat: "wf pred_nat" - apply (unfold wf_def pred_nat_def) - apply clarify - apply (induct_tac x) - apply blast+ + apply (unfold wf_def pred_nat_def, clarify) + apply (induct_tac x, blast+) done lemma wf_less: "wf {(x, y::nat). x < y}" apply (unfold less_def) - apply (rule wf_pred_nat [THEN wf_trancl, THEN wf_subset]) - apply blast + apply (rule wf_pred_nat [THEN wf_trancl, THEN wf_subset], blast) done lemma less_eq: "((m, n) : pred_nat^+) = (m < n)" @@ -180,8 +176,7 @@ lemma less_trans: "i < j ==> j < k ==> i < (k::nat)" apply (unfold less_def) - apply (rule trans_trancl [THEN transD]) - apply assumption+ + apply (rule trans_trancl [THEN transD], assumption+) done lemma lessI [iff]: "n < Suc n" @@ -190,8 +185,7 @@ done lemma less_SucI: "i < j ==> i < Suc j" - apply (rule less_trans) - apply assumption + apply (rule less_trans, assumption) apply (rule lessI) done @@ -234,12 +228,10 @@ assumes major: "i < k" and p1: "k = Suc i ==> P" and p2: "!!j. i < j ==> k = Suc j ==> P" shows P - apply (rule major [unfolded less_def pred_nat_def, THEN tranclE]) - apply simp_all + apply (rule major [unfolded less_def pred_nat_def, THEN tranclE], simp_all) apply (erule p1) apply (rule p2) - apply (simp add: less_def pred_nat_def) - apply assumption + apply (simp add: less_def pred_nat_def, assumption) done lemma not_less0 [iff]: "~ n < (0::nat)" @@ -251,10 +243,8 @@ lemma less_SucE: assumes major: "m < Suc n" and less: "m < n ==> P" and eq: "m = n ==> P" shows P apply (rule major [THEN lessE]) - apply (rule eq) - apply blast - apply (rule less) - apply blast + apply (rule eq, blast) + apply (rule less, blast) done lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)" @@ -308,8 +298,7 @@ and minor: "!!j. i < j ==> k = Suc j ==> P" shows P apply (rule major [THEN lessE]) apply (erule lessI [THEN minor]) - apply (erule Suc_lessD [THEN minor]) - apply assumption + apply (erule Suc_lessD [THEN minor], assumption) done lemma Suc_less_SucD: "Suc m < Suc n ==> m < n" @@ -323,8 +312,7 @@ lemma less_trans_Suc: assumes le: "i < j" shows "j < k ==> Suc i < k" - apply (induct k) - apply simp_all + apply (induct k, simp_all) apply (insert le) apply (simp add: less_Suc_eq) apply (blast dest: Suc_lessD) @@ -332,9 +320,7 @@ text {* Can be used with @{text less_Suc_eq} to get @{term "n = m | n < m"} *} lemma not_less_eq: "(~ m < n) = (n < Suc m)" - apply (rule_tac m = "m" and n = "n" in diff_induct) - apply simp_all - done +by (rule_tac m = m and n = n in diff_induct, simp_all) text {* Complete induction, aka course-of-values induction *} lemma nat_less_induct: @@ -342,8 +328,7 @@ apply (rule_tac a=n in wf_induct) apply (rule wf_pred_nat [THEN wf_trancl]) apply (rule prem) - apply (unfold less_def) - apply assumption + apply (unfold less_def, assumption) done lemmas less_induct = nat_less_induct [rule_format, case_names less] @@ -559,8 +544,7 @@ lemma not_gr0 [iff]: "!!n::nat. (~ (0 < n)) = (n = 0)" apply (rule iffI) - apply (rule ccontr) - apply simp_all + apply (rule ccontr, simp_all) done lemma Suc_le_D: "(Suc n <= m') ==> (? m. m' = Suc m)" @@ -584,14 +568,12 @@ lemmas not_less_Least = wellorder_not_less_Least lemma Least_Suc: "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" - apply (case_tac "n") - apply auto + apply (case_tac "n", auto) apply (frule LeastI) apply (drule_tac P = "%x. P (Suc x) " in LeastI) apply (subgoal_tac " (LEAST x. P x) <= Suc (LEAST x. P (Suc x))") apply (erule_tac [2] Least_le) - apply (case_tac "LEAST x. P x") - apply auto + apply (case_tac "LEAST x. P x", auto) apply (drule_tac P = "%x. P (Suc x) " in Least_le) apply (blast intro: order_antisym) done @@ -714,8 +696,7 @@ done lemma le_add2: "n <= ((m + n)::nat)" - apply (induct m) - apply simp_all + apply (induct m, simp_all) apply (erule le_SucI) done @@ -747,8 +728,7 @@ by (rule less_le_trans, assumption, rule le_add2) lemma add_lessD1: "i + j < (k::nat) ==> i < k" - apply (induct j) - apply simp_all + apply (induct j, simp_all) apply (blast dest: Suc_lessD) done @@ -785,10 +765,8 @@ text {* strict, in both arguments *} lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)" - apply (rule add_less_mono1 [THEN less_trans]) - apply assumption+ - apply (induct_tac j) - apply simp_all + apply (rule add_less_mono1 [THEN less_trans], assumption+) + apply (induct_tac j, simp_all) done text {* A [clumsy] way of lifting @{text "<"} @@ -803,8 +781,7 @@ text {* non-strict, in 1st argument *} lemma add_le_mono1: "i <= j ==> i + k <= j + (k::nat)" apply (rule_tac f = "%j. j + k" in less_mono_imp_le_mono) - apply (erule add_less_mono1) - apply assumption + apply (erule add_less_mono1, assumption) done text {* non-strict, in both arguments *} @@ -853,8 +830,7 @@ lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)" apply (induct_tac m) - apply (induct_tac [2] n) - apply simp_all + apply (induct_tac [2] n, simp_all) done @@ -899,8 +875,7 @@ by (simp add: diff_diff_left) lemma diff_Suc_less [simp]: "0 n - Suc i < n" - apply (case_tac "n") - apply safe + apply (case_tac "n", safe) apply (simp add: le_simps) done @@ -947,8 +922,7 @@ lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0" apply (rule diff_self_eq_0 [THEN subst]) - apply (rule zero_induct_lemma) - apply rules+ + apply (rule zero_induct_lemma, rules+) done lemma diff_cancel: "(k + m) - (k + n) = m - (n::nat)" @@ -992,8 +966,7 @@ text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *} lemma mult_less_mono2: "(i::nat) < j ==> 0 < k ==> k * i < k * j" - apply (erule_tac m1 = "0" in less_imp_Suc_add [THEN exE]) - apply simp + apply (erule_tac m1 = 0 in less_imp_Suc_add [THEN exE], simp) apply (induct_tac x) apply (simp_all add: add_less_mono) done @@ -1003,34 +976,27 @@ lemma zero_less_mult_iff [simp]: "(0 < (m::nat) * n) = (0 < m & 0 < n)" apply (induct m) - apply (case_tac [2] n) - apply simp_all + apply (case_tac [2] n, simp_all) done lemma one_le_mult_iff [simp]: "(Suc 0 <= m * n) = (1 <= m & 1 <= n)" apply (induct m) - apply (case_tac [2] n) - apply simp_all + apply (case_tac [2] n, simp_all) done lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = 1 & n = 1)" - apply (induct_tac m) - apply simp - apply (induct_tac n) - apply simp - apply fastsimp + apply (induct_tac m, simp) + apply (induct_tac n, simp, fastsimp) done lemma one_eq_mult_iff [simp]: "(Suc 0 = m * n) = (m = 1 & n = 1)" apply (rule trans) - apply (rule_tac [2] mult_eq_1_iff) - apply fastsimp + apply (rule_tac [2] mult_eq_1_iff, fastsimp) done lemma mult_less_cancel2: "((m::nat) * k < n * k) = (0 < k & m < n)" apply (safe intro!: mult_less_mono1) - apply (case_tac k) - apply auto + apply (case_tac k, auto) apply (simp del: le_0_eq add: linorder_not_le [symmetric]) apply (blast intro: mult_le_mono1) done @@ -1041,19 +1007,13 @@ declare mult_less_cancel2 [simp] lemma mult_le_cancel1 [simp]: "(k * (m::nat) <= k * n) = (0 < k --> m <= n)" - apply (simp add: linorder_not_less [symmetric]) - apply auto - done +by (simp add: linorder_not_less [symmetric], auto) lemma mult_le_cancel2 [simp]: "((m::nat) * k <= n * k) = (0 < k --> m <= n)" - apply (simp add: linorder_not_less [symmetric]) - apply auto - done +by (simp add: linorder_not_less [symmetric], auto) lemma mult_cancel2: "(m * k = n * k) = (m = n | (k = (0::nat)))" - apply (cut_tac less_linear) - apply safe - apply auto + apply (cut_tac less_linear, safe, auto) apply (drule mult_less_mono1, assumption, simp)+ done diff -r f20fbb141673 -r 144f45277d5a src/HOL/NatArith.thy --- a/src/HOL/NatArith.thy Fri Sep 26 10:34:28 2003 +0200 +++ b/src/HOL/NatArith.thy Fri Sep 26 10:34:57 2003 +0200 @@ -13,10 +13,8 @@ lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m <= n)" -apply (simp add: less_eq reflcl_trancl [symmetric] - del: reflcl_trancl) -apply arith -done +by (simp add: less_eq reflcl_trancl [symmetric] + del: reflcl_trancl, arith) lemma nat_diff_split: "P(a - b::nat) = ((a P 0) & (ALL d. a = b + d --> P d))" diff -r f20fbb141673 -r 144f45277d5a src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Fri Sep 26 10:34:28 2003 +0200 +++ b/src/HOL/Product_Type.thy Fri Sep 26 10:34:57 2003 +0200 @@ -154,8 +154,7 @@ lemma Pair_Rep_inject: "Pair_Rep a b = Pair_Rep a' b' ==> a = a' & b = b'" apply (unfold Pair_Rep_def) - apply (drule fun_cong [THEN fun_cong]) - apply blast + apply (drule fun_cong [THEN fun_cong], blast) done lemma inj_on_Abs_Prod: "inj_on Abs_Prod Prod" @@ -302,8 +301,7 @@ lemma split_Pair_apply: "split (%x y. f (x, y)) = f" -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *} apply (rule ext) - apply (tactic {* pair_tac "x" 1 *}) - apply simp + apply (tactic {* pair_tac "x" 1 *}, simp) done lemma split_paired_The: "(THE x. P x) = (THE (a, b). P (a, b))" @@ -314,9 +312,7 @@ by (simp add: split_def) lemma Pair_fst_snd_eq: "!!s t. (s = t) = (fst s = fst t & snd s = snd t)" - apply (simp only: split_tupled_all) - apply simp - done +by (simp only: split_tupled_all, simp) lemma prod_eqI [intro?]: "fst p = fst q ==> snd p = snd q ==> p = q" by (simp add: Pair_fst_snd_eq) @@ -396,8 +392,7 @@ lemma split_split: "R (split c p) = (ALL x y. p = (x, y) --> R (c x y))" -- {* For use with @{text split} and the Simplifier. *} apply (subst surjective_pairing) - apply (subst split_conv) - apply blast + apply (subst split_conv, blast) done text {* @@ -408,9 +403,7 @@ *} lemma split_split_asm: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))" - apply (subst split_split) - apply simp - done +by (subst split_split, simp) text {* @@ -453,9 +446,7 @@ by simp lemma mem_splitI2: "!!p. [| !!a b. p = (a, b) ==> z: c a b |] ==> z: split c p" - apply (simp only: split_tupled_all) - apply simp - done +by (simp only: split_tupled_all, simp) lemma mem_splitE: "[| z: split c p; !!x y. [| p = (x,y); z: c x y |] ==> Q |] ==> Q" proof - @@ -483,19 +474,14 @@ " lemma split_eta_SetCompr [simp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P" - apply (rule ext) - apply fast - done +by (rule ext, fast) lemma split_eta_SetCompr2 [simp]: "(%u. EX x y. u = (x, y) & P x y) = split P" - apply (rule ext) - apply fast - done +by (rule ext, fast) lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)" -- {* Allows simplifications of nested splits in case of independent predicates. *} - apply (rule ext) - apply blast + apply (rule ext, blast) done lemma split_comp_eq [simp]: @@ -511,10 +497,10 @@ ### Cannot add premise as rewrite rule because it contains (type) unknowns: ### ?y = .x Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)" -by (rtac some_equality 1); -by ( Simp_tac 1); -by (split_all_tac 1); -by (Asm_full_simp_tac 1); +by (rtac some_equality 1) +by ( Simp_tac 1) +by (split_all_tac 1) +by (Asm_full_simp_tac 1) qed "The_split_eq"; *) @@ -532,20 +518,17 @@ lemma prod_fun_compose: "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)" apply (rule ext) - apply (tactic {* pair_tac "x" 1 *}) - apply simp + apply (tactic {* pair_tac "x" 1 *}, simp) done lemma prod_fun_ident [simp]: "prod_fun (%x. x) (%y. y) = (%z. z)" apply (rule ext) - apply (tactic {* pair_tac "z" 1 *}) - apply simp + apply (tactic {* pair_tac "z" 1 *}, simp) done lemma prod_fun_imageI [intro]: "(a, b) : r ==> (f a, g b) : prod_fun f g ` r" apply (rule image_eqI) - apply (rule prod_fun [symmetric]) - apply assumption + apply (rule prod_fun [symmetric], assumption) done lemma prod_fun_imageE [elim!]: @@ -599,14 +582,10 @@ *} lemma SigmaD1: "(a, b) : Sigma A B ==> a : A" - apply (erule SigmaE) - apply blast - done +by (erule SigmaE, blast) lemma SigmaD2: "(a, b) : Sigma A B ==> b : B a" - apply (erule SigmaE) - apply blast - done +by (erule SigmaE, blast) lemma SigmaE2: "[| (a, b) : Sigma A B; diff -r f20fbb141673 -r 144f45277d5a src/HOL/Set.thy --- a/src/HOL/Set.thy Fri Sep 26 10:34:28 2003 +0200 +++ b/src/HOL/Set.thy Fri Sep 26 10:34:57 2003 +0200 @@ -779,8 +779,7 @@ lemma subset_image_iff: "(B \ f`A) = (EX AA. AA \ A & B = f`AA)" apply safe prefer 2 apply fast - apply (rule_tac x = "{a. a : A & f a : B}" in exI) - apply fast + apply (rule_tac x = "{a. a : A & f a : B}" in exI, fast) done lemma image_subsetI: "(!!x. x \ A ==> f x \ B) ==> f`A \ B" @@ -1044,8 +1043,7 @@ lemma mk_disjoint_insert: "a \ A ==> \B. A = insert a B & a \ B" -- {* use new @{text B} rather than @{text "A - {a}"} to avoid infinite unfolding *} - apply (rule_tac x = "A - {a}" in exI) - apply blast + apply (rule_tac x = "A - {a}" in exI, blast) done lemma insert_Collect: "insert a (Collect P) = {u. u \ a --> P u}" @@ -1103,9 +1101,7 @@ by auto lemma range_composition [simp]: "range (\x. f (g x)) = f`range g" - apply (subst image_image) - apply simp - done +by (subst image_image, simp) text {* \medskip @{text Int} *} @@ -1345,7 +1341,7 @@ lemma Inter_UNIV_conv [iff]: "(\A = UNIV) = (\x\A. x = UNIV)" "(UNIV = \A) = (\x\A. x = UNIV)" - by(blast)+ + by blast+ text {* @@ -1578,8 +1574,7 @@ lemma all_bool_eq: "(\b::bool. P b) = (P True & P False)" apply auto - apply (tactic {* case_tac "b" 1 *}) - apply auto + apply (tactic {* case_tac "b" 1 *}, auto) done lemma bool_induct: "P True \ P False \ P x" @@ -1587,8 +1582,7 @@ lemma ex_bool_eq: "(\b::bool. P b) = (P True | P False)" apply auto - apply (tactic {* case_tac "b" 1 *}) - apply auto + apply (tactic {* case_tac "b" 1 *}, auto) done lemma Un_eq_UN: "A \ B = (\b. if b then A else B)" @@ -1596,14 +1590,12 @@ lemma UN_bool_eq: "(\b::bool. A b) = (A True \ A False)" apply auto - apply (tactic {* case_tac "b" 1 *}) - apply auto + apply (tactic {* case_tac "b" 1 *}, auto) done lemma INT_bool_eq: "(\b::bool. A b) = (A True \ A False)" apply auto - apply (tactic {* case_tac "b" 1 *}) - apply auto + apply (tactic {* case_tac "b" 1 *}, auto) done @@ -1800,8 +1792,7 @@ lemma in_mono: "A \ B ==> x \ A --> x \ B" apply (rule impI) - apply (erule subsetD) - apply assumption + apply (erule subsetD, assumption) done lemma conj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 & P2) --> (Q1 & Q2)" @@ -1843,8 +1834,7 @@ ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)" -- {* Courtesy of Stephan Merz *} apply clarify - apply (erule_tac P = "%x. x : S" in LeastI2) - apply fast + apply (erule_tac P = "%x. x : S" in LeastI2, fast) apply (rule LeastI2) apply (auto elim: monoD intro!: order_antisym) done diff -r f20fbb141673 -r 144f45277d5a src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Fri Sep 26 10:34:28 2003 +0200 +++ b/src/HOL/Transitive_Closure.thy Fri Sep 26 10:34:57 2003 +0200 @@ -57,8 +57,7 @@ apply (rule subsetI) apply (simp only: split_tupled_all) apply (erule rtrancl.induct) - apply (rule_tac [2] rtrancl_into_rtrancl) - apply blast+ + apply (rule_tac [2] rtrancl_into_rtrancl, blast+) done theorem rtrancl_induct [consumes 1, induct set: rtrancl]: @@ -126,15 +125,11 @@ done lemma rtrancl_subset_rtrancl: "r \ s^* ==> r^* \ s^*" - apply (drule rtrancl_mono) - apply simp - done +by (drule rtrancl_mono, simp) lemma rtrancl_subset: "R \ S ==> S \ R^* ==> S^* = R^*" apply (drule rtrancl_mono) - apply (drule rtrancl_mono) - apply simp - apply blast + apply (drule rtrancl_mono, simp, blast) done lemma rtrancl_Un_rtrancl: "(R^* \ S^*)^* = (R \ S)^*" @@ -145,12 +140,9 @@ lemma rtrancl_r_diff_Id: "(r - Id)^* = r^*" apply (rule sym) - apply (rule rtrancl_subset) - apply blast - apply clarify + apply (rule rtrancl_subset, blast, clarify) apply (rename_tac a b) - apply (case_tac "a = b") - apply blast + apply (case_tac "a = b", blast) apply (blast intro!: r_into_rtrancl) done @@ -239,8 +231,7 @@ lemma rtrancl_into_trancl2: "[| (a,b) : r; (b,c) : r^* |] ==> (a,c) : r^+" -- {* intro rule from @{text r} and @{text rtrancl} *} - apply (erule rtranclE) - apply rules + apply (erule rtranclE, rules) apply (rule rtrancl_trans [THEN rtrancl_into_trancl1]) apply (assumption | rule r_into_rtrancl)+ done @@ -296,8 +287,7 @@ apply (rule equalityI) apply (rule subsetI) apply (simp only: split_tupled_all) - apply (erule trancl_induct) - apply blast + apply (erule trancl_induct, blast) apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl r_into_trancl trancl_trans) apply (rule subsetI) apply (blast intro: trancl_mono rtrancl_mono @@ -336,8 +326,7 @@ qed lemma tranclD: "(x, y) \ R^+ ==> EX z. (x, z) \ R \ (z, y) \ R^*" - apply (erule converse_trancl_induct) - apply auto + apply (erule converse_trancl_induct, auto) apply (blast intro: rtrancl_trans) done @@ -349,8 +338,7 @@ lemma trancl_subset_Sigma_aux: "(a, b) \ r^* ==> r \ A \ A ==> a = b \ a \ A" - apply (erule rtrancl_induct) - apply auto + apply (erule rtrancl_induct, auto) done lemma trancl_subset_Sigma: "r \ A \ A ==> r^+ \ A \ A" @@ -368,15 +356,11 @@ lemma trancl_reflcl [simp]: "(r^=)^+ = r^*" apply safe - apply (drule trancl_into_rtrancl) - apply simp - apply (erule rtranclE) - apply safe - apply (rule r_into_trancl) - apply simp + apply (drule trancl_into_rtrancl, simp) + apply (erule rtranclE, safe) + apply (rule r_into_trancl, simp) apply (rule rtrancl_into_trancl1) - apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD]) - apply fast + apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD], fast) done lemma trancl_empty [simp]: "{}^+ = {}" @@ -433,8 +417,7 @@ apply (drule tranclD) apply (erule exE, erule conjE) apply (drule rtrancl_trans, assumption) - apply (drule rtrancl_into_trancl2, assumption) - apply assumption + apply (drule rtrancl_into_trancl2, assumption, assumption) done lemmas transitive_closure_trans [trans] =