--- 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]:
--- 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 \<Longrightarrow> (n * q <= m \<and> 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) \<le> 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':
--- 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 \<subseteq> 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 \<subseteq> 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 \<notin> 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 \<cdot> fold f e B = fold f e (A Un B) \<cdot> 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 (\<lambda>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 (\<lambda>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 \<noteq> j --> A i Int A j = {}) ==>
setsum f (UNION I A) = setsum (\<lambda>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 \<noteq> i")
prefer 2 apply blast
apply (subgoal_tac "A x Int UNION F A = {}")
@@ -876,16 +826,14 @@
lemma setsum_addf: "setsum (\<lambda>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)
--- 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<y | x=y | y<x"
apply (simp add: order_less_le)
- apply (insert linorder_linear)
- apply blast
+ apply (insert linorder_linear, blast)
done
lemma linorder_cases [case_names less equal greater]:
"((x::'a::linorder) < y ==> 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<y | y<x)"
- apply (cut_tac x = x and y = y in linorder_less_linear)
- apply auto
- done
+by (cut_tac x = x and y = y in linorder_less_linear, auto)
lemma linorder_neqE: "x ~= (y::'a::linorder) ==> (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"
--- 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 ==> \<forall>y. P y --> m x \<le> 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 ==> \<forall>y. P y --> m y \<le> 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
--- 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) = (\<exists>y ys. xs = y # ys \<and> 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 \<or> length us = length vs
==> (xs@us = ys@vs) = (xs=ys \<and> 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 \<Longrightarrow> x\<in>set l"
-apply (case_tac l)
-apply auto
-done
+by (case_tac l, auto)
lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)"
by auto
@@ -568,21 +553,16 @@
by (induct xs) auto
lemma set_upt [simp]: "set[i..j(] = {k. i \<le> k \<and> 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) = (\<exists>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) = (\<forall>x \<in> 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 \<Longrightarrow> 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 \<Longrightarrow> (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 \<Longrightarrow> 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 \<Longrightarrow> 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: "\<And>n. set(take n xs) \<subseteq> set xs"
@@ -938,11 +881,8 @@
lemma append_eq_conv_conj:
"!!zs. (xs @ ys = zs) = (xs = take (length xs) zs \<and> 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:
"\<And>b. length a = length b \<Longrightarrow>
list_all2 P (a@c) (b@d) = (list_all2 P a b \<and> 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?]:
"\<And>n bs. list_all2 P as bs \<Longrightarrow> 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?]:
"\<And>y. list_all2 P x y \<Longrightarrow> (\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> 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 @@
"\<lbrakk> (\<And>x y. \<lbrakk>P x y; Q y x\<rbrakk> \<Longrightarrow> x = y); list_all2 P xs ys; list_all2 Q ys xs \<rbrakk>
\<Longrightarrow> 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: "(\<forall>i. take i xs = take i ys) ==> xs = ys"
@@ -1350,27 +1263,19 @@
it is useful. *}
lemma distinct_conv_nth:
"distinct xs = (\<forall>i j. i < size xs \<and> j < size xs \<and> i \<noteq> j --> xs!i \<noteq> 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 \<noteq> n")
prefer 2 apply blast
@@ -1480,17 +1379,10 @@
"lexn r n =
{(xs,ys). length xs = n \<and> length ys = n \<and>
(\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (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 \<and> length xs = length ys | x = y \<and> (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
--- 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[\<mapsto>]ys)) = (m1++m2)(xs[\<mapsto>]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] [\<mapsto>] ys) = m(xs [\<mapsto>] ys)(x \<mapsto> 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]:
"\<And>m ys i. \<lbrakk>size xs \<le> i; i < size ys\<rbrakk>
\<Longrightarrow> m(xs[\<mapsto>]ys[i:=y]) = m(xs[\<mapsto>]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.
\<lbrakk> length xs = length ys; set xs \<subseteq> D \<rbrakk>
\<Longrightarrow> m(xs [\<mapsto>] ys)\<lfloor>D = (m\<lfloor>(D - set xs))(xs [\<mapsto>] 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 \<subseteq>\<^sub>m g ==> f(as [|->] bs) \<subseteq>\<^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 \<subseteq>\<^sub>m g) \<Longrightarrow> (dom f \<subseteq> dom g)"
@@ -525,11 +489,8 @@
lemma map_le_antisym: "\<lbrakk> f \<subseteq>\<^sub>m g; g \<subseteq>\<^sub>m f \<rbrakk> \<Longrightarrow> f = g"
apply (unfold map_le_def)
apply (rule ext)
- apply (case_tac "x \<in> dom f")
- apply simp
- apply (case_tac "x \<in> dom g")
- apply simp
- apply fastsimp
+ apply (case_tac "x \<in> dom f", simp)
+ apply (case_tac "x \<in> dom g", simp, fastsimp)
done
lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m (g ++ f)"
--- 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 ==> 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
--- 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<b --> P 0) & (ALL d. a = b + d --> P d))"
--- 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;
--- 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 \<subseteq> f`A) = (EX AA. AA \<subseteq> 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 \<in> A ==> f x \<in> B) ==> f`A \<subseteq> B"
@@ -1044,8 +1043,7 @@
lemma mk_disjoint_insert: "a \<in> A ==> \<exists>B. A = insert a B & a \<notin> 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 \<noteq> a --> P u}"
@@ -1103,9 +1101,7 @@
by auto
lemma range_composition [simp]: "range (\<lambda>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]:
"(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
"(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
- by(blast)+
+ by blast+
text {*
@@ -1578,8 +1574,7 @@
lemma all_bool_eq: "(\<forall>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 \<Longrightarrow> P False \<Longrightarrow> P x"
@@ -1587,8 +1582,7 @@
lemma ex_bool_eq: "(\<exists>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 \<union> B = (\<Union>b. if b then A else B)"
@@ -1596,14 +1590,12 @@
lemma UN_bool_eq: "(\<Union>b::bool. A b) = (A True \<union> A False)"
apply auto
- apply (tactic {* case_tac "b" 1 *})
- apply auto
+ apply (tactic {* case_tac "b" 1 *}, auto)
done
lemma INT_bool_eq: "(\<Inter>b::bool. A b) = (A True \<inter> 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 \<subseteq> B ==> x \<in> A --> x \<in> 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
--- 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 \<subseteq> s^* ==> r^* \<subseteq> s^*"
- apply (drule rtrancl_mono)
- apply simp
- done
+by (drule rtrancl_mono, simp)
lemma rtrancl_subset: "R \<subseteq> S ==> S \<subseteq> 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^* \<union> S^*)^* = (R \<union> 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) \<in> R^+ ==> EX z. (x, z) \<in> R \<and> (z, y) \<in> 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) \<in> r^* ==> r \<subseteq> A \<times> A ==> a = b \<or> a \<in> A"
- apply (erule rtrancl_induct)
- apply auto
+ apply (erule rtrancl_induct, auto)
done
lemma trancl_subset_Sigma: "r \<subseteq> A \<times> A ==> r^+ \<subseteq> A \<times> 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] =