# 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 \<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':
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 \<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)
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<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"
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 ==> \<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
 
 
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) = (\<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
 
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[\<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)"
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 ==> 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<b --> 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 \<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
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 \<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] =