misc tidying
authorpaulson
Fri Sep 26 10:34:57 2003 +0200 (2003-09-26)
changeset 14208144f45277d5a
parent 14207 f20fbb141673
child 14209 180cd69a5dbb
misc tidying
src/HOL/Datatype.thy
src/HOL/Divides.thy
src/HOL/Finite_Set.thy
src/HOL/HOL.thy
src/HOL/Hilbert_Choice.thy
src/HOL/List.thy
src/HOL/Map.thy
src/HOL/Nat.thy
src/HOL/NatArith.thy
src/HOL/Product_Type.thy
src/HOL/Set.thy
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/Datatype.thy	Fri Sep 26 10:34:28 2003 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Fri Sep 26 10:34:57 2003 +0200
     1.3 @@ -55,11 +55,9 @@
     1.4    show P
     1.5      apply (rule r)
     1.6       apply (rule ext)
     1.7 -     apply (cut_tac x = "Inl x" in a [THEN fun_cong])
     1.8 -     apply simp
     1.9 +     apply (cut_tac x = "Inl x" in a [THEN fun_cong], simp)
    1.10      apply (rule ext)
    1.11 -    apply (cut_tac x = "Inr x" in a [THEN fun_cong])
    1.12 -    apply simp
    1.13 +    apply (cut_tac x = "Inr x" in a [THEN fun_cong], simp)
    1.14      done
    1.15  qed
    1.16  
    1.17 @@ -89,8 +87,7 @@
    1.18  lemma prod_cases3 [case_names fields, cases type]:
    1.19      "(!!a b c. y = (a, b, c) ==> P) ==> P"
    1.20    apply (cases y)
    1.21 -  apply (case_tac b)
    1.22 -  apply blast
    1.23 +  apply (case_tac b, blast)
    1.24    done
    1.25  
    1.26  lemma prod_induct3 [case_names fields, induct type]:
    1.27 @@ -100,8 +97,7 @@
    1.28  lemma prod_cases4 [case_names fields, cases type]:
    1.29      "(!!a b c d. y = (a, b, c, d) ==> P) ==> P"
    1.30    apply (cases y)
    1.31 -  apply (case_tac c)
    1.32 -  apply blast
    1.33 +  apply (case_tac c, blast)
    1.34    done
    1.35  
    1.36  lemma prod_induct4 [case_names fields, induct type]:
    1.37 @@ -111,8 +107,7 @@
    1.38  lemma prod_cases5 [case_names fields, cases type]:
    1.39      "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P"
    1.40    apply (cases y)
    1.41 -  apply (case_tac d)
    1.42 -  apply blast
    1.43 +  apply (case_tac d, blast)
    1.44    done
    1.45  
    1.46  lemma prod_induct5 [case_names fields, induct type]:
    1.47 @@ -122,8 +117,7 @@
    1.48  lemma prod_cases6 [case_names fields, cases type]:
    1.49      "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P"
    1.50    apply (cases y)
    1.51 -  apply (case_tac e)
    1.52 -  apply blast
    1.53 +  apply (case_tac e, blast)
    1.54    done
    1.55  
    1.56  lemma prod_induct6 [case_names fields, induct type]:
    1.57 @@ -133,8 +127,7 @@
    1.58  lemma prod_cases7 [case_names fields, cases type]:
    1.59      "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P"
    1.60    apply (cases y)
    1.61 -  apply (case_tac f)
    1.62 -  apply blast
    1.63 +  apply (case_tac f, blast)
    1.64    done
    1.65  
    1.66  lemma prod_induct7 [case_names fields, induct type]:
     2.1 --- a/src/HOL/Divides.thy	Fri Sep 26 10:34:28 2003 +0200
     2.2 +++ b/src/HOL/Divides.thy	Fri Sep 26 10:34:57 2003 +0200
     2.3 @@ -90,8 +90,7 @@
     2.4    "0 < n \<Longrightarrow> (n * q <= m \<and> m < n * (Suc q)) = (q = ((m::nat) div n))"
     2.5    apply (rule iffI)
     2.6    apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
     2.7 -  apply (simp_all add: quorem_def)
     2.8 -  apply arith
     2.9 +  apply (simp_all add: quorem_def, arith)
    2.10    apply (rule conjI)
    2.11    apply (rule_tac P="%x. n * (m div n) \<le> x" in
    2.12      subst [OF mod_div_equality [of _ n]])
    2.13 @@ -99,8 +98,7 @@
    2.14    apply (rule_tac P="%x. x < n + n * (m div n)" in
    2.15      subst [OF mod_div_equality [of _ n]])
    2.16    apply (simp only: add: mult_ac add_ac)
    2.17 -  apply (rule add_less_mono1)
    2.18 -  apply simp
    2.19 +  apply (rule add_less_mono1, simp)
    2.20    done
    2.21  
    2.22  theorem split_div':
     3.1 --- a/src/HOL/Finite_Set.thy	Fri Sep 26 10:34:28 2003 +0200
     3.2 +++ b/src/HOL/Finite_Set.thy	Fri Sep 26 10:34:57 2003 +0200
     3.3 @@ -115,8 +115,7 @@
     3.4  
     3.5  lemma finite_insert [simp]: "finite (insert a A) = finite A"
     3.6    apply (subst insert_is_Un)
     3.7 -  apply (simp only: finite_Un)
     3.8 -  apply blast
     3.9 +  apply (simp only: finite_Un, blast)
    3.10    done
    3.11  
    3.12  lemma finite_empty_induct:
    3.13 @@ -158,8 +157,7 @@
    3.14    apply (subst Diff_insert)
    3.15    apply (case_tac "a : A - B")
    3.16     apply (rule finite_insert [symmetric, THEN trans])
    3.17 -   apply (subst insert_Diff)
    3.18 -    apply simp_all
    3.19 +   apply (subst insert_Diff, simp_all)
    3.20    done
    3.21  
    3.22  
    3.23 @@ -171,8 +169,7 @@
    3.24  
    3.25  lemma finite_range_imageI:
    3.26      "finite (range g) ==> finite (range (%x. f (g x)))"
    3.27 -  apply (drule finite_imageI)
    3.28 -  apply simp
    3.29 +  apply (drule finite_imageI, simp)
    3.30    done
    3.31  
    3.32  lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
    3.33 @@ -186,11 +183,9 @@
    3.34      apply (subgoal_tac "EX y:A. f y = x & F = f ` (A - {y})")
    3.35       apply clarify
    3.36       apply (simp (no_asm_use) add: inj_on_def)
    3.37 -     apply (blast dest!: aux [THEN iffD1])
    3.38 -    apply atomize
    3.39 +     apply (blast dest!: aux [THEN iffD1], atomize)
    3.40      apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl)
    3.41 -    apply (frule subsetD [OF equalityD2 insertI1])
    3.42 -    apply clarify
    3.43 +    apply (frule subsetD [OF equalityD2 insertI1], clarify)
    3.44      apply (rule_tac x = xa in bexI)
    3.45       apply (simp_all add: inj_on_image_set_diff)
    3.46      done
    3.47 @@ -240,8 +235,7 @@
    3.48      "finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)"
    3.49    apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)")
    3.50     apply (erule ssubst)
    3.51 -   apply (erule finite_SigmaI)
    3.52 -   apply auto
    3.53 +   apply (erule finite_SigmaI, auto)
    3.54    done
    3.55  
    3.56  instance unit :: finite
    3.57 @@ -281,8 +275,7 @@
    3.58      apply (erule finite_imageD [unfolded inj_on_def])
    3.59      apply (simp split add: split_split)
    3.60     apply (erule finite_imageI)
    3.61 -  apply (simp add: converse_def image_def)
    3.62 -  apply auto
    3.63 +  apply (simp add: converse_def image_def, auto)
    3.64    apply (rule bexI)
    3.65     prefer 2 apply assumption
    3.66    apply simp
    3.67 @@ -314,8 +307,7 @@
    3.68      "(ALL i:N. i < (n::nat)) ==> finite N"
    3.69    -- {* A bounded set of natural numbers is finite. *}
    3.70    apply (rule finite_subset)
    3.71 -   apply (rule_tac [2] finite_lessThan)
    3.72 -  apply auto
    3.73 +   apply (rule_tac [2] finite_lessThan, auto)
    3.74    done
    3.75  
    3.76  
    3.77 @@ -373,10 +365,8 @@
    3.78  
    3.79  lemma cardR_determ_aux1:
    3.80      "(A, m): cardR ==> (!!n a. m = Suc n ==> a:A ==> (A - {a}, n) : cardR)"
    3.81 -  apply (induct set: cardR)
    3.82 -   apply auto
    3.83 -  apply (simp add: insert_Diff_if)
    3.84 -  apply auto
    3.85 +  apply (induct set: cardR, auto)
    3.86 +  apply (simp add: insert_Diff_if, auto)
    3.87    apply (drule cardR_SucD)
    3.88    apply (blast intro!: cardR.intros)
    3.89    done
    3.90 @@ -390,8 +380,7 @@
    3.91    apply (rename_tac B b m)
    3.92    apply (case_tac "a = b")
    3.93     apply (subgoal_tac "A = B")
    3.94 -    prefer 2 apply (blast elim: equalityE)
    3.95 -   apply blast
    3.96 +    prefer 2 apply (blast elim: equalityE, blast)
    3.97    apply (subgoal_tac "EX C. A = insert b C & B = insert a C")
    3.98     prefer 2
    3.99     apply (rule_tac x = "A Int B" in exI)
   3.100 @@ -433,10 +422,8 @@
   3.101  
   3.102  lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})"
   3.103    apply auto
   3.104 -  apply (drule_tac a = x in mk_disjoint_insert)
   3.105 -  apply clarify
   3.106 -  apply (rotate_tac -1)
   3.107 -  apply auto
   3.108 +  apply (drule_tac a = x in mk_disjoint_insert, clarify)
   3.109 +  apply (rotate_tac -1, auto)
   3.110    done
   3.111  
   3.112  lemma card_insert_if:
   3.113 @@ -444,10 +431,7 @@
   3.114    by (simp add: insert_absorb)
   3.115  
   3.116  lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
   3.117 -  apply (rule_tac t = A in insert_Diff [THEN subst])
   3.118 -   apply assumption
   3.119 -  apply simp
   3.120 -  done
   3.121 +by (rule_tac t = A in insert_Diff [THEN subst], assumption, simp)
   3.122  
   3.123  lemma card_Diff_singleton:
   3.124      "finite A ==> x: A ==> card (A - {x}) = card A - 1"
   3.125 @@ -464,16 +448,12 @@
   3.126    by (simp add: card_insert_if)
   3.127  
   3.128  lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
   3.129 -  apply (induct set: Finites)
   3.130 -   apply simp
   3.131 -  apply clarify
   3.132 +  apply (induct set: Finites, simp, clarify)
   3.133    apply (subgoal_tac "finite A & A - {x} <= F")
   3.134 -   prefer 2 apply (blast intro: finite_subset)
   3.135 -  apply atomize
   3.136 +   prefer 2 apply (blast intro: finite_subset, atomize)
   3.137    apply (drule_tac x = "A - {x}" in spec)
   3.138    apply (simp add: card_Diff_singleton_if split add: split_if_asm)
   3.139 -  apply (case_tac "card A")
   3.140 -   apply auto
   3.141 +  apply (case_tac "card A", auto)
   3.142    done
   3.143  
   3.144  lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
   3.145 @@ -482,16 +462,14 @@
   3.146    done
   3.147  
   3.148  lemma card_mono: "finite B ==> A <= B ==> card A <= card B"
   3.149 -  apply (case_tac "A = B")
   3.150 -   apply simp
   3.151 +  apply (case_tac "A = B", simp)
   3.152    apply (simp add: linorder_not_less [symmetric])
   3.153    apply (blast dest: card_seteq intro: order_less_imp_le)
   3.154    done
   3.155  
   3.156  lemma card_Un_Int: "finite A ==> finite B
   3.157      ==> card A + card B = card (A Un B) + card (A Int B)"
   3.158 -  apply (induct set: Finites)
   3.159 -   apply simp
   3.160 +  apply (induct set: Finites, simp)
   3.161    apply (simp add: insert_absorb Int_insert_left)
   3.162    done
   3.163  
   3.164 @@ -530,30 +508,22 @@
   3.165    done
   3.166  
   3.167  lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
   3.168 -  apply (erule psubsetI)
   3.169 -  apply blast
   3.170 -  done
   3.171 +by (erule psubsetI, blast)
   3.172  
   3.173  
   3.174  subsubsection {* Cardinality of image *}
   3.175  
   3.176  lemma card_image_le: "finite A ==> card (f ` A) <= card A"
   3.177 -  apply (induct set: Finites)
   3.178 -   apply simp
   3.179 +  apply (induct set: Finites, simp)
   3.180    apply (simp add: le_SucI finite_imageI card_insert_if)
   3.181    done
   3.182  
   3.183  lemma card_image: "finite A ==> inj_on f A ==> card (f ` A) = card A"
   3.184 -  apply (induct set: Finites)
   3.185 -   apply simp_all
   3.186 -  apply atomize
   3.187 +  apply (induct set: Finites, simp_all, atomize)
   3.188    apply safe
   3.189 -   apply (unfold inj_on_def)
   3.190 -   apply blast
   3.191 +   apply (unfold inj_on_def, blast)
   3.192    apply (subst card_insert_disjoint)
   3.193 -    apply (erule finite_imageI)
   3.194 -   apply blast
   3.195 -  apply blast
   3.196 +    apply (erule finite_imageI, blast, blast)
   3.197    done
   3.198  
   3.199  lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
   3.200 @@ -565,10 +535,8 @@
   3.201  lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
   3.202    apply (induct set: Finites)
   3.203     apply (simp_all add: Pow_insert)
   3.204 -  apply (subst card_Un_disjoint)
   3.205 -     apply blast
   3.206 -    apply (blast intro: finite_imageI)
   3.207 -   apply blast
   3.208 +  apply (subst card_Un_disjoint, blast)
   3.209 +    apply (blast intro: finite_imageI, blast)
   3.210    apply (subgoal_tac "inj_on (insert x) (Pow F)")
   3.211     apply (simp add: card_image Pow_insert)
   3.212    apply (unfold inj_on_def)
   3.213 @@ -585,9 +553,7 @@
   3.214      ALL c : C. k dvd card c ==>
   3.215      (ALL c1: C. ALL c2: C. c1 ~= c2 --> c1 Int c2 = {}) ==>
   3.216    k dvd card (Union C)"
   3.217 -  apply (induct set: Finites)
   3.218 -   apply simp_all
   3.219 -  apply clarify
   3.220 +  apply (induct set: Finites, simp_all, clarify)
   3.221    apply (subst card_Un_disjoint)
   3.222    apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
   3.223    done
   3.224 @@ -615,9 +581,7 @@
   3.225    "fold f e A == THE x. (A, x) : foldSet f e"
   3.226  
   3.227  lemma Diff1_foldSet: "(A - {x}, y) : foldSet f e ==> x: A ==> (A, f x y) : foldSet f e"
   3.228 -  apply (erule insert_Diff [THEN subst], rule foldSet.intros)
   3.229 -   apply auto
   3.230 -  done
   3.231 +by (erule insert_Diff [THEN subst], rule foldSet.intros, auto)
   3.232  
   3.233  lemma foldSet_imp_finite [simp]: "(A, x) : foldSet f e ==> finite A"
   3.234    by (induct set: foldSet) auto
   3.235 @@ -637,23 +601,18 @@
   3.236      (ALL y. (A, y) : foldSet f e --> y = x)"
   3.237    apply (induct n)
   3.238     apply (auto simp add: less_Suc_eq)
   3.239 -  apply (erule foldSet.cases)
   3.240 -   apply blast
   3.241 -  apply (erule foldSet.cases)
   3.242 -   apply blast
   3.243 -  apply clarify
   3.244 +  apply (erule foldSet.cases, blast)
   3.245 +  apply (erule foldSet.cases, blast, clarify)
   3.246    txt {* force simplification of @{text "card A < card (insert ...)"}. *}
   3.247    apply (erule rev_mp)
   3.248    apply (simp add: less_Suc_eq_le)
   3.249    apply (rule impI)
   3.250    apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
   3.251     apply (subgoal_tac "Aa = Ab")
   3.252 -    prefer 2 apply (blast elim!: equalityE)
   3.253 -   apply blast
   3.254 +    prefer 2 apply (blast elim!: equalityE, blast)
   3.255    txt {* case @{prop "xa \<notin> xb"}. *}
   3.256    apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
   3.257 -   prefer 2 apply (blast elim!: equalityE)
   3.258 -  apply clarify
   3.259 +   prefer 2 apply (blast elim!: equalityE, clarify)
   3.260    apply (subgoal_tac "Aa = insert xb Ab - {xa}")
   3.261     prefer 2 apply blast
   3.262    apply (subgoal_tac "card Aa <= card Ab")
   3.263 @@ -700,16 +659,14 @@
   3.264    done
   3.265  
   3.266  lemma (in LC) fold_commute: "finite A ==> (!!e. f x (fold f e A) = fold f (f x e) A)"
   3.267 -  apply (induct set: Finites)
   3.268 -   apply simp
   3.269 +  apply (induct set: Finites, simp)
   3.270    apply (simp add: left_commute fold_insert)
   3.271    done
   3.272  
   3.273  lemma (in LC) fold_nest_Un_Int:
   3.274    "finite A ==> finite B
   3.275      ==> fold f (fold f e B) A = fold f (fold f e (A Int B)) (A Un B)"
   3.276 -  apply (induct set: Finites)
   3.277 -   apply simp
   3.278 +  apply (induct set: Finites, simp)
   3.279    apply (simp add: fold_insert fold_commute Int_insert_left insert_absorb)
   3.280    done
   3.281  
   3.282 @@ -757,8 +714,7 @@
   3.283  lemma (in ACe) fold_Un_Int:
   3.284    "finite A ==> finite B ==>
   3.285      fold f e A \<cdot> fold f e B = fold f e (A Un B) \<cdot> fold f e (A Int B)"
   3.286 -  apply (induct set: Finites)
   3.287 -   apply simp
   3.288 +  apply (induct set: Finites, simp)
   3.289    apply (simp add: AC insert_absorb Int_insert_left
   3.290      LC.fold_insert [OF LC.intro])
   3.291    done
   3.292 @@ -823,8 +779,7 @@
   3.293  lemma setsum_0: "setsum (\<lambda>i. 0) A = 0"
   3.294    apply (case_tac "finite A")
   3.295     prefer 2 apply (simp add: setsum_def)
   3.296 -  apply (erule finite_induct)
   3.297 -   apply auto
   3.298 +  apply (erule finite_induct, auto)
   3.299    done
   3.300  
   3.301  lemma setsum_eq_0_iff [simp]:
   3.302 @@ -835,8 +790,7 @@
   3.303    apply (case_tac "finite A")
   3.304     prefer 2 apply (simp add: setsum_def)
   3.305    apply (erule rev_mp)
   3.306 -  apply (erule finite_induct)
   3.307 -   apply auto
   3.308 +  apply (erule finite_induct, auto)
   3.309    done
   3.310  
   3.311  lemma card_eq_setsum: "finite A ==> card A = setsum (\<lambda>x. 1) A"
   3.312 @@ -846,15 +800,13 @@
   3.313  lemma setsum_Un_Int: "finite A ==> finite B
   3.314      ==> setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   3.315    -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   3.316 -  apply (induct set: Finites)
   3.317 -   apply simp
   3.318 +  apply (induct set: Finites, simp)
   3.319    apply (simp add: plus_ac0 Int_insert_left insert_absorb)
   3.320    done
   3.321  
   3.322  lemma setsum_Un_disjoint: "finite A ==> finite B
   3.323    ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
   3.324 -  apply (subst setsum_Un_Int [symmetric])
   3.325 -    apply auto
   3.326 +  apply (subst setsum_Un_Int [symmetric], auto)
   3.327    done
   3.328  
   3.329  lemma setsum_UN_disjoint:
   3.330 @@ -863,9 +815,7 @@
   3.331      "finite I ==> (ALL i:I. finite (A i)) ==>
   3.332          (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   3.333        setsum f (UNION I A) = setsum (\<lambda>i. setsum f (A i)) I"
   3.334 -  apply (induct set: Finites)
   3.335 -   apply simp
   3.336 -  apply atomize
   3.337 +  apply (induct set: Finites, simp, atomize)
   3.338    apply (subgoal_tac "ALL i:F. x \<noteq> i")
   3.339     prefer 2 apply blast
   3.340    apply (subgoal_tac "A x Int UNION F A = {}")
   3.341 @@ -876,16 +826,14 @@
   3.342  lemma setsum_addf: "setsum (\<lambda>x. f x + g x) A = (setsum f A + setsum g A)"
   3.343    apply (case_tac "finite A")
   3.344     prefer 2 apply (simp add: setsum_def)
   3.345 -  apply (erule finite_induct)
   3.346 -   apply auto
   3.347 +  apply (erule finite_induct, auto)
   3.348    apply (simp add: plus_ac0)
   3.349    done
   3.350  
   3.351  lemma setsum_Un: "finite A ==> finite B ==>
   3.352      (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   3.353    -- {* For the natural numbers, we have subtraction. *}
   3.354 -  apply (subst setsum_Un_Int [symmetric])
   3.355 -    apply auto
   3.356 +  apply (subst setsum_Un_Int [symmetric], auto)
   3.357    done
   3.358  
   3.359  lemma setsum_diff1: "(setsum f (A - {a}) :: nat) =
   3.360 @@ -894,21 +842,17 @@
   3.361     prefer 2 apply (simp add: setsum_def)
   3.362    apply (erule finite_induct)
   3.363     apply (auto simp add: insert_Diff_if)
   3.364 -  apply (drule_tac a = a in mk_disjoint_insert)
   3.365 -  apply auto
   3.366 +  apply (drule_tac a = a in mk_disjoint_insert, auto)
   3.367    done
   3.368  
   3.369  lemma setsum_cong:
   3.370    "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   3.371    apply (case_tac "finite B")
   3.372 -   prefer 2 apply (simp add: setsum_def)
   3.373 -  apply simp
   3.374 +   prefer 2 apply (simp add: setsum_def, simp)
   3.375    apply (subgoal_tac "ALL C. C <= B --> (ALL x:C. f x = g x) --> setsum f C = setsum g C")
   3.376     apply simp
   3.377 -  apply (erule finite_induct)
   3.378 -  apply simp
   3.379 -  apply (simp add: subset_insert_iff)
   3.380 -  apply clarify
   3.381 +  apply (erule finite_induct, simp)
   3.382 +  apply (simp add: subset_insert_iff, clarify)
   3.383    apply (subgoal_tac "finite C")
   3.384     prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
   3.385    apply (subgoal_tac "C = insert x (C - {x})")
   3.386 @@ -1019,8 +963,7 @@
   3.387    apply safe
   3.388     apply (auto intro: finite_subset [THEN card_insert_disjoint])
   3.389    apply (drule_tac x = "xa - {x}" in spec)
   3.390 -  apply (subgoal_tac "x ~: xa")
   3.391 -   apply auto
   3.392 +  apply (subgoal_tac "x ~: xa", auto)
   3.393    apply (erule rev_mp, subst card_Diff_singleton)
   3.394    apply (auto intro: finite_subset)
   3.395    done
   3.396 @@ -1057,8 +1000,7 @@
   3.397  lemma n_sub_lemma:
   3.398    "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
   3.399    apply (induct k)
   3.400 -   apply (simp add: card_s_0_eq_empty)
   3.401 -  apply atomize
   3.402 +   apply (simp add: card_s_0_eq_empty, atomize)
   3.403    apply (rotate_tac -1, erule finite_induct)
   3.404     apply (simp_all (no_asm_simp) cong add: conj_cong
   3.405       add: card_s_0_eq_empty choose_deconstruct)
     4.1 --- a/src/HOL/HOL.thy	Fri Sep 26 10:34:28 2003 +0200
     4.2 +++ b/src/HOL/HOL.thy	Fri Sep 26 10:34:57 2003 +0200
     4.3 @@ -489,14 +489,11 @@
     4.4  lemma split_if: "P (if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"
     4.5    apply (rule case_split [of Q])
     4.6     apply (subst if_P)
     4.7 -    prefer 3 apply (subst if_not_P)
     4.8 -     apply blast+
     4.9 +    prefer 3 apply (subst if_not_P, blast+)
    4.10    done
    4.11  
    4.12  lemma split_if_asm: "P (if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
    4.13 -  apply (subst split_if)
    4.14 -  apply blast
    4.15 -  done
    4.16 +by (subst split_if, blast)
    4.17  
    4.18  lemmas if_splits = split_if split_if_asm
    4.19  
    4.20 @@ -504,14 +501,10 @@
    4.21    by (rule split_if)
    4.22  
    4.23  lemma if_cancel: "(if c then x else x) = x"
    4.24 -  apply (subst split_if)
    4.25 -  apply blast
    4.26 -  done
    4.27 +by (subst split_if, blast)
    4.28  
    4.29  lemma if_eq_cancel: "(if x = y then y else x) = x"
    4.30 -  apply (subst split_if)
    4.31 -  apply blast
    4.32 -  done
    4.33 +by (subst split_if, blast)
    4.34  
    4.35  lemma if_bool_eq_conj: "(if P then Q else R) = ((P-->Q) & (~P-->R))"
    4.36    -- {* This form is useful for expanding @{text if}s on the RIGHT of the @{text "==>"} symbol. *}
    4.37 @@ -519,8 +512,7 @@
    4.38  
    4.39  lemma if_bool_eq_disj: "(if P then Q else R) = ((P&Q) | (~P&R))"
    4.40    -- {* And this form is useful for expanding @{text if}s on the LEFT. *}
    4.41 -  apply (subst split_if)
    4.42 -  apply blast
    4.43 +  apply (subst split_if, blast)
    4.44    done
    4.45  
    4.46  lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) rules
    4.47 @@ -552,8 +544,7 @@
    4.48    apply (erule impE)
    4.49    apply (rule allI)
    4.50    apply (rule_tac P = "xa = x" in case_split_thm)
    4.51 -  apply (drule_tac [3] x = x in fun_cong)
    4.52 -  apply simp_all
    4.53 +  apply (drule_tac [3] x = x in fun_cong, simp_all)
    4.54    done
    4.55  
    4.56  text{*Needs only HOL-lemmas:*}
    4.57 @@ -706,8 +697,7 @@
    4.58  
    4.59  lemma order_le_less: "((x::'a::order) <= y) = (x < y | x = y)"
    4.60      -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
    4.61 -  apply (simp add: order_less_le)
    4.62 -  apply blast
    4.63 +  apply (simp add: order_less_le, blast)
    4.64    done
    4.65  
    4.66  lemmas order_le_imp_less_or_eq = order_le_less [THEN iffD1, standard]
    4.67 @@ -723,8 +713,7 @@
    4.68  
    4.69  lemma order_less_asym: "x < (y::'a::order) ==> (~P ==> y < x) ==> P"
    4.70    apply (drule order_less_not_sym)
    4.71 -  apply (erule contrapos_np)
    4.72 -  apply simp
    4.73 +  apply (erule contrapos_np, simp)
    4.74    done
    4.75  
    4.76  
    4.77 @@ -806,14 +795,12 @@
    4.78  
    4.79  lemma linorder_less_linear: "!!x::'a::linorder. x<y | x=y | y<x"
    4.80    apply (simp add: order_less_le)
    4.81 -  apply (insert linorder_linear)
    4.82 -  apply blast
    4.83 +  apply (insert linorder_linear, blast)
    4.84    done
    4.85  
    4.86  lemma linorder_cases [case_names less equal greater]:
    4.87      "((x::'a::linorder) < y ==> P) ==> (x = y ==> P) ==> (y < x ==> P) ==> P"
    4.88 -  apply (insert linorder_less_linear)
    4.89 -  apply blast
    4.90 +  apply (insert linorder_less_linear, blast)
    4.91    done
    4.92  
    4.93  lemma linorder_not_less: "!!x::'a::linorder. (~ x < y) = (y <= x)"
    4.94 @@ -829,14 +816,10 @@
    4.95    done
    4.96  
    4.97  lemma linorder_neq_iff: "!!x::'a::linorder. (x ~= y) = (x<y | y<x)"
    4.98 -  apply (cut_tac x = x and y = y in linorder_less_linear)
    4.99 -  apply auto
   4.100 -  done
   4.101 +by (cut_tac x = x and y = y in linorder_less_linear, auto)
   4.102  
   4.103  lemma linorder_neqE: "x ~= (y::'a::linorder) ==> (x < y ==> R) ==> (y < x ==> R) ==> R"
   4.104 -  apply (simp add: linorder_neq_iff)
   4.105 -  apply blast
   4.106 -  done
   4.107 +by (simp add: linorder_neq_iff, blast)
   4.108  
   4.109  
   4.110  subsubsection "Min and max on (linear) orders"
     5.1 --- a/src/HOL/Hilbert_Choice.thy	Fri Sep 26 10:34:28 2003 +0200
     5.2 +++ b/src/HOL/Hilbert_Choice.thy	Fri Sep 26 10:34:57 2003 +0200
     5.3 @@ -72,17 +72,13 @@
     5.4      ==> (!!x. P x ==> \<forall>y. P y --> m x \<le> m y ==> Q x)
     5.5      ==> Q (LeastM m P)"
     5.6    apply (unfold LeastM_def)
     5.7 -  apply (rule someI2_ex)
     5.8 -   apply blast
     5.9 -  apply blast
    5.10 +  apply (rule someI2_ex, blast, blast)
    5.11    done
    5.12  
    5.13  lemma LeastM_equality:
    5.14    "P k ==> (!!x. P x ==> m k <= m x)
    5.15      ==> m (LEAST x WRT m. P x) = (m k::'a::order)"
    5.16 -  apply (rule LeastMI2)
    5.17 -    apply assumption
    5.18 -   apply blast
    5.19 +  apply (rule LeastMI2, assumption, blast)
    5.20    apply (blast intro!: order_antisym)
    5.21    done
    5.22  
    5.23 @@ -90,16 +86,14 @@
    5.24    "wf r ==> ALL x y. ((x,y):r^+) = ((y,x)~:r^*) ==> P k
    5.25      ==> EX x. P x & (!y. P y --> (m x,m y):r^*)"
    5.26    apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]])
    5.27 -  apply (drule_tac x = "m`Collect P" in spec)
    5.28 -  apply force
    5.29 +  apply (drule_tac x = "m`Collect P" in spec, force)
    5.30    done
    5.31  
    5.32  lemma ex_has_least_nat:
    5.33      "P k ==> EX x. P x & (ALL y. P y --> m x <= (m y::nat))"
    5.34    apply (simp only: pred_nat_trancl_eq_le [symmetric])
    5.35    apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
    5.36 -   apply (simp add: less_eq not_le_iff_less pred_nat_trancl_eq_le)
    5.37 -  apply assumption
    5.38 +   apply (simp add: less_eq not_le_iff_less pred_nat_trancl_eq_le, assumption)
    5.39    done
    5.40  
    5.41  lemma LeastM_nat_lemma:
    5.42 @@ -112,10 +106,7 @@
    5.43  lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1, standard]
    5.44  
    5.45  lemma LeastM_nat_le: "P x ==> m (LeastM m P) <= (m x::nat)"
    5.46 -  apply (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp])
    5.47 -   apply assumption
    5.48 -  apply assumption
    5.49 -  done
    5.50 +by (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp], assumption, assumption)
    5.51  
    5.52  
    5.53  subsection {* Greatest value operator *}
    5.54 @@ -139,32 +130,26 @@
    5.55      ==> (!!x. P x ==> \<forall>y. P y --> m y \<le> m x ==> Q x)
    5.56      ==> Q (GreatestM m P)"
    5.57    apply (unfold GreatestM_def)
    5.58 -  apply (rule someI2_ex)
    5.59 -   apply blast
    5.60 -  apply blast
    5.61 +  apply (rule someI2_ex, blast, blast)
    5.62    done
    5.63  
    5.64  lemma GreatestM_equality:
    5.65   "P k ==> (!!x. P x ==> m x <= m k)
    5.66      ==> m (GREATEST x WRT m. P x) = (m k::'a::order)"
    5.67 -  apply (rule_tac m = m in GreatestMI2)
    5.68 -    apply assumption
    5.69 -   apply blast
    5.70 +  apply (rule_tac m = m in GreatestMI2, assumption, blast)
    5.71    apply (blast intro!: order_antisym)
    5.72    done
    5.73  
    5.74  lemma Greatest_equality:
    5.75    "P (k::'a::order) ==> (!!x. P x ==> x <= k) ==> (GREATEST x. P x) = k"
    5.76    apply (unfold Greatest_def)
    5.77 -  apply (erule GreatestM_equality)
    5.78 -  apply blast
    5.79 +  apply (erule GreatestM_equality, blast)
    5.80    done
    5.81  
    5.82  lemma ex_has_greatest_nat_lemma:
    5.83    "P k ==> ALL x. P x --> (EX y. P y & ~ ((m y::nat) <= m x))
    5.84      ==> EX y. P y & ~ (m y < m k + n)"
    5.85 -  apply (induct_tac n)
    5.86 -   apply force
    5.87 +  apply (induct_tac n, force)
    5.88    apply (force simp add: le_Suc_eq)
    5.89    done
    5.90  
    5.91 @@ -173,8 +158,7 @@
    5.92      ==> EX x. P x & (ALL y. P y --> (m y::nat) <= m x)"
    5.93    apply (rule ccontr)
    5.94    apply (cut_tac P = P and n = "b - m k" in ex_has_greatest_nat_lemma)
    5.95 -    apply (subgoal_tac [3] "m k <= b")
    5.96 -     apply auto
    5.97 +    apply (subgoal_tac [3] "m k <= b", auto)
    5.98    done
    5.99  
   5.100  lemma GreatestM_nat_lemma:
   5.101 @@ -182,8 +166,7 @@
   5.102      ==> P (GreatestM m P) & (ALL y. P y --> (m y::nat) <= m (GreatestM m P))"
   5.103    apply (unfold GreatestM_def)
   5.104    apply (rule someI_ex)
   5.105 -  apply (erule ex_has_greatest_nat)
   5.106 -  apply assumption
   5.107 +  apply (erule ex_has_greatest_nat, assumption)
   5.108    done
   5.109  
   5.110  lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1, standard]
   5.111 @@ -199,15 +182,13 @@
   5.112  
   5.113  lemma GreatestI: "P (k::nat) ==> ALL y. P y --> y < b ==> P (GREATEST x. P x)"
   5.114    apply (unfold Greatest_def)
   5.115 -  apply (rule GreatestM_natI)
   5.116 -   apply auto
   5.117 +  apply (rule GreatestM_natI, auto)
   5.118    done
   5.119  
   5.120  lemma Greatest_le:
   5.121      "P x ==> ALL y. P y --> y < b ==> (x::nat) <= (GREATEST x. P x)"
   5.122    apply (unfold Greatest_def)
   5.123 -  apply (rule GreatestM_nat_le)
   5.124 -   apply auto
   5.125 +  apply (rule GreatestM_nat_le, auto)
   5.126    done
   5.127  
   5.128  
     6.1 --- a/src/HOL/List.thy	Fri Sep 26 10:34:28 2003 +0200
     6.2 +++ b/src/HOL/List.thy	Fri Sep 26 10:34:57 2003 +0200
     6.3 @@ -282,16 +282,13 @@
     6.4  
     6.5  lemma Suc_length_conv:
     6.6  "(Suc n = length xs) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
     6.7 -apply (induct xs)
     6.8 - apply simp
     6.9 -apply simp
    6.10 +apply (induct xs, simp, simp)
    6.11  apply blast
    6.12  done
    6.13  
    6.14  lemma impossible_Cons [rule_format]: 
    6.15    "length xs <= length ys --> xs = x # ys = False"
    6.16 -apply (induct xs)
    6.17 -apply auto
    6.18 +apply (induct xs, auto)
    6.19  done
    6.20  
    6.21  
    6.22 @@ -319,12 +316,8 @@
    6.23   "!!ys. length xs = length ys \<or> length us = length vs
    6.24   ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
    6.25  apply (induct xs)
    6.26 - apply (case_tac ys)
    6.27 -apply simp
    6.28 - apply force
    6.29 -apply (case_tac ys)
    6.30 - apply force
    6.31 -apply simp
    6.32 + apply (case_tac ys, simp, force)
    6.33 +apply (case_tac ys, force, simp)
    6.34  done
    6.35  
    6.36  lemma same_append_eq [iff]: "(xs @ ys = xs @ zs) = (ys = zs)"
    6.37 @@ -486,12 +479,9 @@
    6.38  by (rules dest: map_injective injD intro: inj_onI)
    6.39  
    6.40  lemma inj_mapD: "inj (map f) ==> inj f"
    6.41 -apply (unfold inj_on_def)
    6.42 -apply clarify
    6.43 +apply (unfold inj_on_def, clarify)
    6.44  apply (erule_tac x = "[x]" in ballE)
    6.45 - apply (erule_tac x = "[y]" in ballE)
    6.46 -apply simp
    6.47 - apply blast
    6.48 + apply (erule_tac x = "[y]" in ballE, simp, blast)
    6.49  apply blast
    6.50  done
    6.51  
    6.52 @@ -514,11 +504,8 @@
    6.53  by (induct xs) auto
    6.54  
    6.55  lemma rev_is_rev_conv [iff]: "!!ys. (rev xs = rev ys) = (xs = ys)"
    6.56 -apply (induct xs)
    6.57 - apply force
    6.58 -apply (case_tac ys)
    6.59 - apply simp
    6.60 -apply force
    6.61 +apply (induct xs, force)
    6.62 +apply (case_tac ys, simp, force)
    6.63  done
    6.64  
    6.65  lemma rev_induct [case_names Nil snoc]:
    6.66 @@ -545,9 +532,7 @@
    6.67  by (induct xs) auto
    6.68  
    6.69  lemma hd_in_set: "l = x#xs \<Longrightarrow> x\<in>set l"
    6.70 -apply (case_tac l)
    6.71 -apply auto
    6.72 -done
    6.73 +by (case_tac l, auto)
    6.74  
    6.75  lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)"
    6.76  by auto
    6.77 @@ -568,21 +553,16 @@
    6.78  by (induct xs) auto
    6.79  
    6.80  lemma set_upt [simp]: "set[i..j(] = {k. i \<le> k \<and> k < j}"
    6.81 -apply (induct j)
    6.82 - apply simp_all
    6.83 -apply(erule ssubst)
    6.84 -apply auto
    6.85 +apply (induct j, simp_all)
    6.86 +apply (erule ssubst, auto)
    6.87  done
    6.88  
    6.89  lemma in_set_conv_decomp: "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs)"
    6.90 -apply (induct xs)
    6.91 - apply simp
    6.92 -apply simp
    6.93 +apply (induct xs, simp, simp)
    6.94  apply (rule iffI)
    6.95   apply (blast intro: eq_Nil_appendI Cons_eq_appendI)
    6.96  apply (erule exE)+
    6.97 -apply (case_tac ys)
    6.98 -apply auto
    6.99 +apply (case_tac ys, auto)
   6.100  done
   6.101  
   6.102  lemma in_lists_conv_set: "(xs : lists A) = (\<forall>x \<in> set xs. x : A)"
   6.103 @@ -674,33 +654,23 @@
   6.104  
   6.105  lemma nth_append:
   6.106  "!!n. (xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"
   6.107 -apply(induct "xs")
   6.108 - apply simp
   6.109 -apply (case_tac n)
   6.110 - apply auto
   6.111 +apply (induct "xs", simp)
   6.112 +apply (case_tac n, auto)
   6.113  done
   6.114  
   6.115  lemma nth_map [simp]: "!!n. n < length xs ==> (map f xs)!n = f(xs!n)"
   6.116 -apply(induct xs)
   6.117 - apply simp
   6.118 -apply (case_tac n)
   6.119 - apply auto
   6.120 +apply (induct xs, simp)
   6.121 +apply (case_tac n, auto)
   6.122  done
   6.123  
   6.124  lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
   6.125 -apply (induct_tac xs)
   6.126 - apply simp
   6.127 -apply simp
   6.128 +apply (induct_tac xs, simp, simp)
   6.129  apply safe
   6.130 -apply (rule_tac x = 0 in exI)
   6.131 -apply simp
   6.132 - apply (rule_tac x = "Suc i" in exI)
   6.133 - apply simp
   6.134 -apply (case_tac i)
   6.135 - apply simp
   6.136 +apply (rule_tac x = 0 in exI, simp)
   6.137 + apply (rule_tac x = "Suc i" in exI, simp)
   6.138 +apply (case_tac i, simp)
   6.139  apply (rename_tac j)
   6.140 -apply (rule_tac x = j in exI)
   6.141 -apply simp
   6.142 +apply (rule_tac x = j in exI, simp)
   6.143  done
   6.144  
   6.145  lemma list_ball_nth: "[| n < length xs; !x : set xs. P x|] ==> P(xs!n)"
   6.146 @@ -738,8 +708,7 @@
   6.147  by (induct xs) (auto split: nat.split)
   6.148  
   6.149  lemma list_update_id[simp]: "!!i. i < length xs \<Longrightarrow> xs[i := xs!i] = xs"
   6.150 -apply(induct xs)
   6.151 - apply simp
   6.152 +apply (induct xs, simp)
   6.153  apply(simp split:nat.splits)
   6.154  done
   6.155  
   6.156 @@ -749,8 +718,7 @@
   6.157  
   6.158  lemma list_update_append1:
   6.159   "!!i. i < size xs \<Longrightarrow> (xs @ ys)[i:=x] = xs[i:=x] @ ys"
   6.160 -apply(induct xs)
   6.161 - apply simp
   6.162 +apply (induct xs, simp)
   6.163  apply(simp split:nat.split)
   6.164  done
   6.165  
   6.166 @@ -816,17 +784,14 @@
   6.167  by(induct xs, simp_all add:drop_Cons drop_Suc split:nat.split)
   6.168  
   6.169  lemma nth_via_drop: "!!n. drop n xs = y#ys \<Longrightarrow> xs!n = y"
   6.170 -apply(induct xs)
   6.171 - apply simp
   6.172 +apply (induct xs, simp)
   6.173  apply(simp add:drop_Cons nth_Cons split:nat.splits)
   6.174  done
   6.175  
   6.176  lemma take_Suc_conv_app_nth:
   6.177   "!!i. i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
   6.178 -apply(induct xs)
   6.179 - apply simp
   6.180 -apply(case_tac i)
   6.181 -apply auto
   6.182 +apply (induct xs, simp)
   6.183 +apply (case_tac i, auto)
   6.184  done
   6.185  
   6.186  lemma length_take [simp]: "!!xs. length (take n xs) = min (length xs) n"
   6.187 @@ -850,78 +815,56 @@
   6.188  by (induct n) (auto, case_tac xs, auto)
   6.189  
   6.190  lemma take_take [simp]: "!!xs n. take n (take m xs) = take (min n m) xs"
   6.191 -apply (induct m)
   6.192 - apply auto
   6.193 -apply (case_tac xs)
   6.194 - apply auto
   6.195 -apply (case_tac na)
   6.196 - apply auto
   6.197 +apply (induct m, auto)
   6.198 +apply (case_tac xs, auto)
   6.199 +apply (case_tac na, auto)
   6.200  done
   6.201  
   6.202  lemma drop_drop [simp]: "!!xs. drop n (drop m xs) = drop (n + m) xs"
   6.203 -apply (induct m)
   6.204 - apply auto
   6.205 -apply (case_tac xs)
   6.206 - apply auto
   6.207 +apply (induct m, auto)
   6.208 +apply (case_tac xs, auto)
   6.209  done
   6.210  
   6.211  lemma take_drop: "!!xs n. take n (drop m xs) = drop m (take (n + m) xs)"
   6.212 -apply (induct m)
   6.213 - apply auto
   6.214 -apply (case_tac xs)
   6.215 - apply auto
   6.216 +apply (induct m, auto)
   6.217 +apply (case_tac xs, auto)
   6.218  done
   6.219  
   6.220  lemma append_take_drop_id [simp]: "!!xs. take n xs @ drop n xs = xs"
   6.221 -apply (induct n)
   6.222 - apply auto
   6.223 -apply (case_tac xs)
   6.224 - apply auto
   6.225 +apply (induct n, auto)
   6.226 +apply (case_tac xs, auto)
   6.227  done
   6.228  
   6.229  lemma take_map: "!!xs. take n (map f xs) = map f (take n xs)"
   6.230 -apply (induct n)
   6.231 - apply auto
   6.232 -apply (case_tac xs)
   6.233 - apply auto
   6.234 +apply (induct n, auto)
   6.235 +apply (case_tac xs, auto)
   6.236  done
   6.237  
   6.238  lemma drop_map: "!!xs. drop n (map f xs) = map f (drop n xs)"
   6.239 -apply (induct n)
   6.240 - apply auto
   6.241 -apply (case_tac xs)
   6.242 - apply auto
   6.243 +apply (induct n, auto)
   6.244 +apply (case_tac xs, auto)
   6.245  done
   6.246  
   6.247  lemma rev_take: "!!i. rev (take i xs) = drop (length xs - i) (rev xs)"
   6.248 -apply (induct xs)
   6.249 - apply auto
   6.250 -apply (case_tac i)
   6.251 - apply auto
   6.252 +apply (induct xs, auto)
   6.253 +apply (case_tac i, auto)
   6.254  done
   6.255  
   6.256  lemma rev_drop: "!!i. rev (drop i xs) = take (length xs - i) (rev xs)"
   6.257 -apply (induct xs)
   6.258 - apply auto
   6.259 -apply (case_tac i)
   6.260 - apply auto
   6.261 +apply (induct xs, auto)
   6.262 +apply (case_tac i, auto)
   6.263  done
   6.264  
   6.265  lemma nth_take [simp]: "!!n i. i < n ==> (take n xs)!i = xs!i"
   6.266 -apply (induct xs)
   6.267 - apply auto
   6.268 -apply (case_tac n)
   6.269 - apply(blast )
   6.270 -apply (case_tac i)
   6.271 - apply auto
   6.272 +apply (induct xs, auto)
   6.273 +apply (case_tac n, blast)
   6.274 +apply (case_tac i, auto)
   6.275  done
   6.276  
   6.277  lemma nth_drop [simp]:
   6.278  "!!xs i. n + i <= length xs ==> (drop n xs)!i = xs!(n + i)"
   6.279 -apply (induct n)
   6.280 - apply auto
   6.281 -apply (case_tac xs)
   6.282 - apply auto
   6.283 +apply (induct n, auto)
   6.284 +apply (case_tac xs, auto)
   6.285  done
   6.286  
   6.287  lemma set_take_subset: "\<And>n. set(take n xs) \<subseteq> set xs"
   6.288 @@ -938,11 +881,8 @@
   6.289  
   6.290  lemma append_eq_conv_conj:
   6.291  "!!zs. (xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"
   6.292 -apply(induct xs)
   6.293 - apply simp
   6.294 -apply clarsimp
   6.295 -apply (case_tac zs)
   6.296 -apply auto
   6.297 +apply (induct xs, simp, clarsimp)
   6.298 +apply (case_tac zs, auto)
   6.299  done
   6.300  
   6.301  lemma take_add [rule_format]: 
   6.302 @@ -1004,28 +944,22 @@
   6.303  
   6.304  lemma length_zip [simp]:
   6.305  "!!xs. length (zip xs ys) = min (length xs) (length ys)"
   6.306 -apply(induct ys)
   6.307 - apply simp
   6.308 -apply (case_tac xs)
   6.309 - apply auto
   6.310 +apply (induct ys, simp)
   6.311 +apply (case_tac xs, auto)
   6.312  done
   6.313  
   6.314  lemma zip_append1:
   6.315  "!!xs. zip (xs @ ys) zs =
   6.316  zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)"
   6.317 -apply (induct zs)
   6.318 - apply simp
   6.319 -apply (case_tac xs)
   6.320 - apply simp_all
   6.321 +apply (induct zs, simp)
   6.322 +apply (case_tac xs, simp_all)
   6.323  done
   6.324  
   6.325  lemma zip_append2:
   6.326  "!!ys. zip xs (ys @ zs) =
   6.327  zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs"
   6.328 -apply (induct xs)
   6.329 - apply simp
   6.330 -apply (case_tac ys)
   6.331 - apply simp_all
   6.332 +apply (induct xs, simp)
   6.333 +apply (case_tac ys, simp_all)
   6.334  done
   6.335  
   6.336  lemma zip_append [simp]:
   6.337 @@ -1035,16 +969,13 @@
   6.338  
   6.339  lemma zip_rev:
   6.340  "!!xs. length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
   6.341 -apply(induct ys)
   6.342 - apply simp
   6.343 -apply (case_tac xs)
   6.344 - apply simp_all
   6.345 +apply (induct ys, simp)
   6.346 +apply (case_tac xs, simp_all)
   6.347  done
   6.348  
   6.349  lemma nth_zip [simp]:
   6.350  "!!i xs. [| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
   6.351 -apply (induct ys)
   6.352 - apply simp
   6.353 +apply (induct ys, simp)
   6.354  apply (case_tac xs)
   6.355   apply (simp_all add: nth.simps split: nat.split)
   6.356  done
   6.357 @@ -1059,10 +990,8 @@
   6.358  
   6.359  lemma zip_replicate [simp]:
   6.360  "!!j. zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)"
   6.361 -apply (induct i)
   6.362 - apply auto
   6.363 -apply (case_tac j)
   6.364 - apply auto
   6.365 +apply (induct i, auto)
   6.366 +apply (case_tac j, auto)
   6.367  done
   6.368  
   6.369  
   6.370 @@ -1105,8 +1034,7 @@
   6.371  apply (rule iffI)
   6.372   apply (rule_tac x = "take (length xs) zs" in exI)
   6.373   apply (rule_tac x = "drop (length xs) zs" in exI)
   6.374 - apply (force split: nat_diff_split simp add: min_def)
   6.375 -apply clarify
   6.376 + apply (force split: nat_diff_split simp add: min_def, clarify)
   6.377  apply (simp add: ball_Un)
   6.378  done
   6.379  
   6.380 @@ -1118,18 +1046,15 @@
   6.381  apply (rule iffI)
   6.382   apply (rule_tac x = "take (length ys) xs" in exI)
   6.383   apply (rule_tac x = "drop (length ys) xs" in exI)
   6.384 - apply (force split: nat_diff_split simp add: min_def)
   6.385 -apply clarify
   6.386 + apply (force split: nat_diff_split simp add: min_def, clarify)
   6.387  apply (simp add: ball_Un)
   6.388  done
   6.389  
   6.390  lemma list_all2_append:
   6.391    "\<And>b. length a = length b \<Longrightarrow>
   6.392    list_all2 P (a@c) (b@d) = (list_all2 P a b \<and> list_all2 P c d)"
   6.393 -  apply (induct a)
   6.394 -   apply simp
   6.395 -  apply (case_tac b)
   6.396 -  apply auto
   6.397 +  apply (induct a, simp)
   6.398 +  apply (case_tac b, auto)
   6.399    done
   6.400  
   6.401  lemma list_all2_appendI [intro?, trans]:
   6.402 @@ -1185,20 +1110,15 @@
   6.403  
   6.404  lemma list_all2_dropI [intro?]:
   6.405    "\<And>n bs. list_all2 P as bs \<Longrightarrow> list_all2 P (drop n as) (drop n bs)"
   6.406 -  apply (induct as)
   6.407 -   apply simp
   6.408 +  apply (induct as, simp)
   6.409    apply (clarsimp simp add: list_all2_Cons1)
   6.410 -  apply (case_tac n)
   6.411 -   apply simp
   6.412 -  apply simp
   6.413 +  apply (case_tac n, simp, simp)
   6.414    done
   6.415  
   6.416  lemma list_all2_mono [intro?]:
   6.417    "\<And>y. list_all2 P x y \<Longrightarrow> (\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> list_all2 Q x y"
   6.418 -  apply (induct x)
   6.419 -   apply simp
   6.420 -  apply (case_tac y)
   6.421 -  apply auto
   6.422 +  apply (induct x, simp)
   6.423 +  apply (case_tac y, auto)
   6.424    done
   6.425  
   6.426  
   6.427 @@ -1231,7 +1151,7 @@
   6.428    Nil:  "(a, [],a) : fold_rel R"
   6.429    Cons: "[|(a,x,b) : R; (b,xs,c) : fold_rel R|] ==> (a,x#xs,c) : fold_rel R"
   6.430  inductive_cases fold_rel_elim_case [elim!]:
   6.431 -   "(a, []  , b) : fold_rel R"
   6.432 +   "(a, [] , b) : fold_rel R"
   6.433     "(a, x#xs, b) : fold_rel R"
   6.434  
   6.435  lemma fold_rel_Nil [intro!]: "a = b ==> (a, [], b) : fold_rel R" 
   6.436 @@ -1255,8 +1175,7 @@
   6.437  lemma upt_conv_Cons: "i < j ==> [i..j(] = i # [Suc i..j(]"
   6.438  apply(rule trans)
   6.439  apply(subst upt_rec)
   6.440 - prefer 2 apply(rule refl)
   6.441 -apply simp
   6.442 + prefer 2 apply (rule refl, simp)
   6.443  done
   6.444  
   6.445  lemma upt_add_eq_append: "i<=j ==> [i..j+k(] = [i..j(]@[j..j+k(]"
   6.446 @@ -1272,8 +1191,7 @@
   6.447  done
   6.448  
   6.449  lemma take_upt [simp]: "!!i. i+m <= n ==> take m [i..n(] = [i..i+m(]"
   6.450 -apply (induct m)
   6.451 - apply simp
   6.452 +apply (induct m, simp)
   6.453  apply (subst upt_rec)
   6.454  apply (rule sym)
   6.455  apply (subst upt_rec)
   6.456 @@ -1293,13 +1211,10 @@
   6.457    "!!xs ys. k <= length xs ==> k <= length ys ==>
   6.458       (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys"
   6.459  apply (atomize, induct k)
   6.460 -apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib)
   6.461 -apply clarify
   6.462 +apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib, clarify)
   6.463  txt {* Both lists must be non-empty *}
   6.464 -apply (case_tac xs)
   6.465 - apply simp
   6.466 -apply (case_tac ys)
   6.467 - apply clarify
   6.468 +apply (case_tac xs, simp)
   6.469 +apply (case_tac ys, clarify)
   6.470   apply (simp (no_asm_use))
   6.471  apply clarify
   6.472  txt {* prenexing's needed, not miniscoping *}
   6.473 @@ -1318,9 +1233,7 @@
   6.474    "\<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> 
   6.475    \<Longrightarrow> xs = ys"
   6.476    apply (simp add: list_all2_conv_all_nth) 
   6.477 -  apply (rule nth_equalityI)
   6.478 -   apply blast
   6.479 -  apply simp
   6.480 +  apply (rule nth_equalityI, blast, simp)
   6.481    done
   6.482  
   6.483  lemma take_equalityI: "(\<forall>i. take i xs = take i ys) ==> xs = ys"
   6.484 @@ -1350,27 +1263,19 @@
   6.485  it is useful. *}
   6.486  lemma distinct_conv_nth:
   6.487  "distinct xs = (\<forall>i j. i < size xs \<and> j < size xs \<and> i \<noteq> j --> xs!i \<noteq> xs!j)"
   6.488 -apply (induct_tac xs)
   6.489 - apply simp
   6.490 -apply simp
   6.491 -apply (rule iffI)
   6.492 - apply clarsimp
   6.493 +apply (induct_tac xs, simp, simp)
   6.494 +apply (rule iffI, clarsimp)
   6.495   apply (case_tac i)
   6.496 -apply (case_tac j)
   6.497 - apply simp
   6.498 +apply (case_tac j, simp)
   6.499  apply (simp add: set_conv_nth)
   6.500   apply (case_tac j)
   6.501 -apply (clarsimp simp add: set_conv_nth)
   6.502 - apply simp
   6.503 +apply (clarsimp simp add: set_conv_nth, simp)
   6.504  apply (rule conjI)
   6.505   apply (clarsimp simp add: set_conv_nth)
   6.506   apply (erule_tac x = 0 in allE)
   6.507 - apply (erule_tac x = "Suc i" in allE)
   6.508 - apply simp
   6.509 -apply clarsimp
   6.510 + apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
   6.511  apply (erule_tac x = "Suc i" in allE)
   6.512 -apply (erule_tac x = "Suc j" in allE)
   6.513 -apply simp
   6.514 +apply (erule_tac x = "Suc j" in allE, simp)
   6.515  done
   6.516  
   6.517  
   6.518 @@ -1387,8 +1292,7 @@
   6.519  by (induct n) auto
   6.520  
   6.521  lemma rev_replicate [simp]: "rev (replicate n x) = replicate n x"
   6.522 -apply(induct n)
   6.523 - apply simp
   6.524 +apply (induct n, simp)
   6.525  apply (simp add: replicate_app_Cons_same)
   6.526  done
   6.527  
   6.528 @@ -1405,8 +1309,7 @@
   6.529  by (atomize (full), induct n) auto
   6.530  
   6.531  lemma nth_replicate[simp]: "!!i. i < n ==> (replicate n x)!i = x"
   6.532 -apply(induct n)
   6.533 - apply simp
   6.534 +apply (induct n, simp)
   6.535  apply (simp add: nth_Cons split: nat.split)
   6.536  done
   6.537  
   6.538 @@ -1451,14 +1354,11 @@
   6.539  subsection {* Lexicographic orderings on lists *}
   6.540  
   6.541  lemma wf_lexn: "wf r ==> wf (lexn r n)"
   6.542 -apply (induct_tac n)
   6.543 - apply simp
   6.544 -apply simp
   6.545 +apply (induct_tac n, simp, simp)
   6.546  apply(rule wf_subset)
   6.547   prefer 2 apply (rule Int_lower1)
   6.548  apply(rule wf_prod_fun_image)
   6.549 - prefer 2 apply (rule inj_onI)
   6.550 -apply auto
   6.551 + prefer 2 apply (rule inj_onI, auto)
   6.552  done
   6.553  
   6.554  lemma lexn_length:
   6.555 @@ -1468,8 +1368,7 @@
   6.556  lemma wf_lex [intro!]: "wf r ==> wf (lex r)"
   6.557  apply (unfold lex_def)
   6.558  apply (rule wf_UN)
   6.559 -apply (blast intro: wf_lexn)
   6.560 -apply clarify
   6.561 +apply (blast intro: wf_lexn, clarify)
   6.562  apply (rename_tac m n)
   6.563  apply (subgoal_tac "m \<noteq> n")
   6.564   prefer 2 apply blast
   6.565 @@ -1480,17 +1379,10 @@
   6.566  "lexn r n =
   6.567  {(xs,ys). length xs = n \<and> length ys = n \<and>
   6.568  (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y):r)}"
   6.569 -apply (induct_tac n)
   6.570 - apply simp
   6.571 - apply blast
   6.572 -apply (simp add: image_Collect lex_prod_def)
   6.573 -apply safe
   6.574 -apply blast
   6.575 - apply (rule_tac x = "ab # xys" in exI)
   6.576 - apply simp
   6.577 -apply (case_tac xys)
   6.578 - apply simp_all
   6.579 -apply blast
   6.580 +apply (induct_tac n, simp, blast)
   6.581 +apply (simp add: image_Collect lex_prod_def, safe, blast)
   6.582 + apply (rule_tac x = "ab # xys" in exI, simp)
   6.583 +apply (case_tac xys, simp_all, blast)
   6.584  done
   6.585  
   6.586  lemma lex_conv:
   6.587 @@ -1518,11 +1410,8 @@
   6.588  ((x, y) : r \<and> length xs = length ys | x = y \<and> (xs, ys) : lex r)"
   6.589  apply (simp add: lex_conv)
   6.590  apply (rule iffI)
   6.591 - prefer 2 apply (blast intro: Cons_eq_appendI)
   6.592 -apply clarify
   6.593 -apply (case_tac xys)
   6.594 - apply simp
   6.595 -apply simp
   6.596 + prefer 2 apply (blast intro: Cons_eq_appendI, clarify)
   6.597 +apply (case_tac xys, simp, simp)
   6.598  apply blast
   6.599  done
   6.600  
   6.601 @@ -1543,8 +1432,7 @@
   6.602  lemma sublist_append:
   6.603  "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
   6.604  apply (unfold sublist_def)
   6.605 -apply (induct l' rule: rev_induct)
   6.606 - apply simp
   6.607 +apply (induct l' rule: rev_induct, simp)
   6.608  apply (simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma)
   6.609  apply (simp add: add_commute)
   6.610  done
   6.611 @@ -1560,8 +1448,7 @@
   6.612  by (simp add: sublist_Cons)
   6.613  
   6.614  lemma sublist_upt_eq_take [simp]: "sublist l {..n(} = take n l"
   6.615 -apply (induct l rule: rev_induct)
   6.616 - apply simp
   6.617 +apply (induct l rule: rev_induct, simp)
   6.618  apply (simp split: nat_diff_split add: sublist_append)
   6.619  done
   6.620  
     7.1 --- a/src/HOL/Map.thy	Fri Sep 26 10:34:28 2003 +0200
     7.2 +++ b/src/HOL/Map.thy	Fri Sep 26 10:34:57 2003 +0200
     7.3 @@ -111,7 +111,7 @@
     7.4  
     7.5  lemma map_upd_nonempty[simp]: "t(k|->x) ~= empty"
     7.6  apply safe
     7.7 -apply (drule_tac x = "k" in fun_cong)
     7.8 +apply (drule_tac x = k in fun_cong)
     7.9  apply (simp (no_asm_use))
    7.10  done
    7.11  
    7.12 @@ -126,7 +126,7 @@
    7.13  apply (unfold image_def)
    7.14  apply (simp (no_asm_use) add: full_SetCompr_eq)
    7.15  apply (rule finite_subset)
    7.16 -prefer 2 apply (assumption)
    7.17 +prefer 2 apply assumption
    7.18  apply auto
    7.19  done
    7.20  
    7.21 @@ -156,22 +156,16 @@
    7.22  subsection {* @{term chg_map} *}
    7.23  
    7.24  lemma chg_map_new[simp]: "m a = None   ==> chg_map f a m = m"
    7.25 -apply (unfold chg_map_def)
    7.26 -apply auto
    7.27 -done
    7.28 +by (unfold chg_map_def, auto)
    7.29  
    7.30  lemma chg_map_upd[simp]: "m a = Some b ==> chg_map f a m = m(a|->f b)"
    7.31 -apply (unfold chg_map_def)
    7.32 -apply auto
    7.33 -done
    7.34 +by (unfold chg_map_def, auto)
    7.35  
    7.36  
    7.37  subsection {* @{term map_of} *}
    7.38  
    7.39  lemma map_of_SomeD [rule_format (no_asm)]: "map_of xs k = Some y --> (k,y):set xs"
    7.40 -apply (induct_tac "xs")
    7.41 -apply  auto
    7.42 -done
    7.43 +by (induct_tac "xs", auto)
    7.44  
    7.45  lemma map_of_mapk_SomeI [rule_format (no_asm)]: "inj f ==> map_of t k = Some x -->  
    7.46     map_of (map (split (%k. Pair (f k))) t) (f k) = Some x"
    7.47 @@ -180,31 +174,26 @@
    7.48  done
    7.49  
    7.50  lemma weak_map_of_SomeI [rule_format (no_asm)]: "(k, x) : set l --> (? x. map_of l k = Some x)"
    7.51 -apply (induct_tac "l")
    7.52 -apply  auto
    7.53 -done
    7.54 +by (induct_tac "l", auto)
    7.55  
    7.56  lemma map_of_filter_in: 
    7.57  "[| map_of xs k = Some z; P k z |] ==> map_of (filter (split P) xs) k = Some z"
    7.58  apply (rule mp)
    7.59 -prefer 2 apply (assumption)
    7.60 +prefer 2 apply assumption
    7.61  apply (erule thin_rl)
    7.62 -apply (induct_tac "xs")
    7.63 -apply  auto
    7.64 +apply (induct_tac "xs", auto)
    7.65  done
    7.66  
    7.67  lemma finite_range_map_of: "finite (range (map_of l))"
    7.68  apply (induct_tac "l")
    7.69  apply  (simp_all (no_asm) add: image_constant)
    7.70  apply (rule finite_subset)
    7.71 -prefer 2 apply (assumption)
    7.72 +prefer 2 apply assumption
    7.73  apply auto
    7.74  done
    7.75  
    7.76  lemma map_of_map: "map_of (map (%(a,b). (a,f b)) xs) x = option_map f (map_of xs x)"
    7.77 -apply (induct_tac "xs")
    7.78 -apply auto
    7.79 -done
    7.80 +by (induct_tac "xs", auto)
    7.81  
    7.82  
    7.83  subsection {* @{term option_map} related *}
    7.84 @@ -249,9 +238,7 @@
    7.85  declare map_add_SomeD [dest!]
    7.86  
    7.87  lemma map_add_find_right[simp]: "!!xx. n k = Some xx ==> (m ++ n) k = Some xx"
    7.88 -apply (subst map_add_Some_iff)
    7.89 -apply fast
    7.90 -done
    7.91 +by (subst map_add_Some_iff, fast)
    7.92  
    7.93  lemma map_add_None [iff]: "((m ++ n) k = None) = (n k = None & m k = None)"
    7.94  apply (unfold map_add_def)
    7.95 @@ -260,8 +247,7 @@
    7.96  
    7.97  lemma map_add_upd[simp]: "f ++ g(x|->y) = (f ++ g)(x|->y)"
    7.98  apply (unfold map_add_def)
    7.99 -apply (rule ext)
   7.100 -apply auto
   7.101 +apply (rule ext, auto)
   7.102  done
   7.103  
   7.104  lemma map_add_upds[simp]: "m1 ++ (m2(xs[\<mapsto>]ys)) = (m1++m2)(xs[\<mapsto>]ys)"
   7.105 @@ -278,8 +264,7 @@
   7.106  declare fun_upd_apply [simp del]
   7.107  lemma finite_range_map_of_map_add:
   7.108   "finite (range f) ==> finite (range (f ++ map_of l))"
   7.109 -apply (induct_tac "l")
   7.110 -apply  auto
   7.111 +apply (induct_tac "l", auto)
   7.112  apply (erule finite_range_updI)
   7.113  done
   7.114  declare fun_upd_apply [simp]
   7.115 @@ -351,18 +336,14 @@
   7.116    m(xs@[x] [\<mapsto>] ys) = m(xs [\<mapsto>] ys)(x \<mapsto> ys!size xs)"
   7.117  apply(induct xs)
   7.118   apply(clarsimp simp add:neq_Nil_conv)
   7.119 -apply(case_tac ys)
   7.120 - apply simp
   7.121 -apply simp
   7.122 +apply (case_tac ys, simp, simp)
   7.123  done
   7.124  
   7.125  lemma map_upds_list_update2_drop[simp]:
   7.126   "\<And>m ys i. \<lbrakk>size xs \<le> i; i < size ys\<rbrakk>
   7.127       \<Longrightarrow> m(xs[\<mapsto>]ys[i:=y]) = m(xs[\<mapsto>]ys)"
   7.128 -apply(induct xs)
   7.129 - apply simp
   7.130 -apply(case_tac ys)
   7.131 - apply simp
   7.132 +apply (induct xs, simp)
   7.133 +apply (case_tac ys, simp)
   7.134  apply(simp split:nat.split)
   7.135  done
   7.136  
   7.137 @@ -370,8 +351,7 @@
   7.138   (f(x|->y))(xs [|->] ys) =
   7.139   (if x : set(take (length ys) xs) then f(xs [|->] ys)
   7.140                                    else (f(xs [|->] ys))(x|->y))"
   7.141 -apply(induct xs)
   7.142 - apply simp
   7.143 +apply (induct xs, simp)
   7.144  apply(case_tac ys)
   7.145   apply(auto split:split_if simp:fun_upd_twist)
   7.146  done
   7.147 @@ -384,8 +364,7 @@
   7.148  
   7.149  lemma map_upds_apply_nontin[simp]:
   7.150   "!!ys. x ~: set xs ==> (f(xs[|->]ys)) x = f x"
   7.151 -apply(induct xs)
   7.152 - apply simp
   7.153 +apply (induct xs, simp)
   7.154  apply(case_tac ys)
   7.155   apply(auto simp: map_upd_upds_conv_if)
   7.156  done
   7.157 @@ -393,10 +372,8 @@
   7.158  lemma restrict_map_upds[simp]: "!!m ys.
   7.159   \<lbrakk> length xs = length ys; set xs \<subseteq> D \<rbrakk>
   7.160   \<Longrightarrow> m(xs [\<mapsto>] ys)\<lfloor>D = (m\<lfloor>(D - set xs))(xs [\<mapsto>] ys)"
   7.161 -apply(induct xs)
   7.162 - apply simp
   7.163 -apply(case_tac ys)
   7.164 - apply simp
   7.165 +apply (induct xs, simp)
   7.166 +apply (case_tac ys, simp)
   7.167  apply(simp add:Diff_insert[symmetric] insert_absorb)
   7.168  apply(simp add: map_upd_upds_conv_if)
   7.169  done
   7.170 @@ -415,20 +392,14 @@
   7.171  subsection {* @{term dom} *}
   7.172  
   7.173  lemma domI: "m a = Some b ==> a : dom m"
   7.174 -apply (unfold dom_def)
   7.175 -apply auto
   7.176 -done
   7.177 +by (unfold dom_def, auto)
   7.178  (* declare domI [intro]? *)
   7.179  
   7.180  lemma domD: "a : dom m ==> ? b. m a = Some b"
   7.181 -apply (unfold dom_def)
   7.182 -apply auto
   7.183 -done
   7.184 +by (unfold dom_def, auto)
   7.185  
   7.186  lemma domIff[iff]: "(a : dom m) = (m a ~= None)"
   7.187 -apply (unfold dom_def)
   7.188 -apply auto
   7.189 -done
   7.190 +by (unfold dom_def, auto)
   7.191  declare domIff [simp del]
   7.192  
   7.193  lemma dom_empty[simp]: "dom empty = {}"
   7.194 @@ -453,16 +424,12 @@
   7.195  
   7.196  lemma dom_map_upds[simp]:
   7.197   "!!m ys. dom(m(xs[|->]ys)) = set(take (length ys) xs) Un dom m"
   7.198 -apply(induct xs)
   7.199 - apply simp
   7.200 -apply(case_tac ys)
   7.201 - apply auto
   7.202 +apply (induct xs, simp)
   7.203 +apply (case_tac ys, auto)
   7.204  done
   7.205  
   7.206  lemma dom_map_add[simp]: "dom(m++n) = dom n Un dom m"
   7.207 -apply (unfold dom_def)
   7.208 -apply auto
   7.209 -done
   7.210 +by (unfold dom_def, auto)
   7.211  
   7.212  lemma dom_overwrite[simp]:
   7.213   "dom(f(g|A)) = (dom f  - {a. a : A - dom g}) Un {a. a : A Int dom g}"
   7.214 @@ -485,8 +452,7 @@
   7.215  done
   7.216  
   7.217  lemma ran_map_upd[simp]: "m a = None ==> ran(m(a|->b)) = insert b (ran m)"
   7.218 -apply (unfold ran_def)
   7.219 -apply auto
   7.220 +apply (unfold ran_def, auto)
   7.221  apply (subgoal_tac "~ (aa = a) ")
   7.222  apply auto
   7.223  done
   7.224 @@ -507,10 +473,8 @@
   7.225  
   7.226  lemma map_le_upds[simp]:
   7.227   "!!f g bs. f \<subseteq>\<^sub>m g ==> f(as [|->] bs) \<subseteq>\<^sub>m g(as [|->] bs)"
   7.228 -apply(induct as)
   7.229 - apply simp
   7.230 -apply(case_tac bs)
   7.231 - apply auto
   7.232 +apply (induct as, simp)
   7.233 +apply (case_tac bs, auto)
   7.234  done
   7.235  
   7.236  lemma map_le_implies_dom_le: "(f \<subseteq>\<^sub>m g) \<Longrightarrow> (dom f \<subseteq> dom g)"
   7.237 @@ -525,11 +489,8 @@
   7.238  lemma map_le_antisym: "\<lbrakk> f \<subseteq>\<^sub>m g; g \<subseteq>\<^sub>m f \<rbrakk> \<Longrightarrow> f = g"
   7.239    apply (unfold map_le_def)
   7.240    apply (rule ext)
   7.241 -  apply (case_tac "x \<in> dom f")
   7.242 -    apply simp
   7.243 -  apply (case_tac "x \<in> dom g")
   7.244 -    apply simp
   7.245 -  apply fastsimp
   7.246 +  apply (case_tac "x \<in> dom f", simp)
   7.247 +  apply (case_tac "x \<in> dom g", simp, fastsimp)
   7.248  done
   7.249  
   7.250  lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m (g ++ f)"
     8.1 --- a/src/HOL/Nat.thy	Fri Sep 26 10:34:28 2003 +0200
     8.2 +++ b/src/HOL/Nat.thy	Fri Sep 26 10:34:57 2003 +0200
     8.3 @@ -39,7 +39,7 @@
     8.4  global
     8.5  
     8.6  typedef (open Nat)
     8.7 -  nat = "Nat" by (rule exI, rule Nat.Zero_RepI)
     8.8 +  nat = Nat by (rule exI, rule Nat.Zero_RepI)
     8.9  
    8.10  instance nat :: ord ..
    8.11  instance nat :: zero ..
    8.12 @@ -148,27 +148,23 @@
    8.13  
    8.14  theorem diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
    8.15      (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
    8.16 -  apply (rule_tac x = "m" in spec)
    8.17 +  apply (rule_tac x = m in spec)
    8.18    apply (induct_tac n)
    8.19    prefer 2
    8.20    apply (rule allI)
    8.21 -  apply (induct_tac x)
    8.22 -  apply rules+
    8.23 +  apply (induct_tac x, rules+)
    8.24    done
    8.25  
    8.26  subsection {* Basic properties of "less than" *}
    8.27  
    8.28  lemma wf_pred_nat: "wf pred_nat"
    8.29 -  apply (unfold wf_def pred_nat_def)
    8.30 -  apply clarify
    8.31 -  apply (induct_tac x)
    8.32 -  apply blast+
    8.33 +  apply (unfold wf_def pred_nat_def, clarify)
    8.34 +  apply (induct_tac x, blast+)
    8.35    done
    8.36  
    8.37  lemma wf_less: "wf {(x, y::nat). x < y}"
    8.38    apply (unfold less_def)
    8.39 -  apply (rule wf_pred_nat [THEN wf_trancl, THEN wf_subset])
    8.40 -  apply blast
    8.41 +  apply (rule wf_pred_nat [THEN wf_trancl, THEN wf_subset], blast)
    8.42    done
    8.43  
    8.44  lemma less_eq: "((m, n) : pred_nat^+) = (m < n)"
    8.45 @@ -180,8 +176,7 @@
    8.46  
    8.47  lemma less_trans: "i < j ==> j < k ==> i < (k::nat)"
    8.48    apply (unfold less_def)
    8.49 -  apply (rule trans_trancl [THEN transD])
    8.50 -  apply assumption+
    8.51 +  apply (rule trans_trancl [THEN transD], assumption+)
    8.52    done
    8.53  
    8.54  lemma lessI [iff]: "n < Suc n"
    8.55 @@ -190,8 +185,7 @@
    8.56    done
    8.57  
    8.58  lemma less_SucI: "i < j ==> i < Suc j"
    8.59 -  apply (rule less_trans)
    8.60 -  apply assumption
    8.61 +  apply (rule less_trans, assumption)
    8.62    apply (rule lessI)
    8.63    done
    8.64  
    8.65 @@ -234,12 +228,10 @@
    8.66    assumes major: "i < k"
    8.67    and p1: "k = Suc i ==> P" and p2: "!!j. i < j ==> k = Suc j ==> P"
    8.68    shows P
    8.69 -  apply (rule major [unfolded less_def pred_nat_def, THEN tranclE])
    8.70 -  apply simp_all
    8.71 +  apply (rule major [unfolded less_def pred_nat_def, THEN tranclE], simp_all)
    8.72    apply (erule p1)
    8.73    apply (rule p2)
    8.74 -  apply (simp add: less_def pred_nat_def)
    8.75 -  apply assumption
    8.76 +  apply (simp add: less_def pred_nat_def, assumption)
    8.77    done
    8.78  
    8.79  lemma not_less0 [iff]: "~ n < (0::nat)"
    8.80 @@ -251,10 +243,8 @@
    8.81  lemma less_SucE: assumes major: "m < Suc n"
    8.82    and less: "m < n ==> P" and eq: "m = n ==> P" shows P
    8.83    apply (rule major [THEN lessE])
    8.84 -  apply (rule eq)
    8.85 -  apply blast
    8.86 -  apply (rule less)
    8.87 -  apply blast
    8.88 +  apply (rule eq, blast)
    8.89 +  apply (rule less, blast)
    8.90    done
    8.91  
    8.92  lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)"
    8.93 @@ -308,8 +298,7 @@
    8.94    and minor: "!!j. i < j ==> k = Suc j ==> P" shows P
    8.95    apply (rule major [THEN lessE])
    8.96    apply (erule lessI [THEN minor])
    8.97 -  apply (erule Suc_lessD [THEN minor])
    8.98 -  apply assumption
    8.99 +  apply (erule Suc_lessD [THEN minor], assumption)
   8.100    done
   8.101  
   8.102  lemma Suc_less_SucD: "Suc m < Suc n ==> m < n"
   8.103 @@ -323,8 +312,7 @@
   8.104  
   8.105  lemma less_trans_Suc:
   8.106    assumes le: "i < j" shows "j < k ==> Suc i < k"
   8.107 -  apply (induct k)
   8.108 -  apply simp_all
   8.109 +  apply (induct k, simp_all)
   8.110    apply (insert le)
   8.111    apply (simp add: less_Suc_eq)
   8.112    apply (blast dest: Suc_lessD)
   8.113 @@ -332,9 +320,7 @@
   8.114  
   8.115  text {* Can be used with @{text less_Suc_eq} to get @{term "n = m | n < m"} *}
   8.116  lemma not_less_eq: "(~ m < n) = (n < Suc m)"
   8.117 -  apply (rule_tac m = "m" and n = "n" in diff_induct)
   8.118 -  apply simp_all
   8.119 -  done
   8.120 +by (rule_tac m = m and n = n in diff_induct, simp_all)
   8.121  
   8.122  text {* Complete induction, aka course-of-values induction *}
   8.123  lemma nat_less_induct:
   8.124 @@ -342,8 +328,7 @@
   8.125    apply (rule_tac a=n in wf_induct)
   8.126    apply (rule wf_pred_nat [THEN wf_trancl])
   8.127    apply (rule prem)
   8.128 -  apply (unfold less_def)
   8.129 -  apply assumption
   8.130 +  apply (unfold less_def, assumption)
   8.131    done
   8.132  
   8.133  lemmas less_induct = nat_less_induct [rule_format, case_names less]
   8.134 @@ -559,8 +544,7 @@
   8.135  
   8.136  lemma not_gr0 [iff]: "!!n::nat. (~ (0 < n)) = (n = 0)"
   8.137    apply (rule iffI)
   8.138 -  apply (rule ccontr)
   8.139 -  apply simp_all
   8.140 +  apply (rule ccontr, simp_all)
   8.141    done
   8.142  
   8.143  lemma Suc_le_D: "(Suc n <= m') ==> (? m. m' = Suc m)"
   8.144 @@ -584,14 +568,12 @@
   8.145  lemmas not_less_Least = wellorder_not_less_Least
   8.146  
   8.147  lemma Least_Suc: "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
   8.148 -  apply (case_tac "n")
   8.149 -  apply auto
   8.150 +  apply (case_tac "n", auto)
   8.151    apply (frule LeastI)
   8.152    apply (drule_tac P = "%x. P (Suc x) " in LeastI)
   8.153    apply (subgoal_tac " (LEAST x. P x) <= Suc (LEAST x. P (Suc x))")
   8.154    apply (erule_tac [2] Least_le)
   8.155 -  apply (case_tac "LEAST x. P x")
   8.156 -  apply auto
   8.157 +  apply (case_tac "LEAST x. P x", auto)
   8.158    apply (drule_tac P = "%x. P (Suc x) " in Least_le)
   8.159    apply (blast intro: order_antisym)
   8.160    done
   8.161 @@ -714,8 +696,7 @@
   8.162    done
   8.163  
   8.164  lemma le_add2: "n <= ((m + n)::nat)"
   8.165 -  apply (induct m)
   8.166 -  apply simp_all
   8.167 +  apply (induct m, simp_all)
   8.168    apply (erule le_SucI)
   8.169    done
   8.170  
   8.171 @@ -747,8 +728,7 @@
   8.172    by (rule less_le_trans, assumption, rule le_add2)
   8.173  
   8.174  lemma add_lessD1: "i + j < (k::nat) ==> i < k"
   8.175 -  apply (induct j)
   8.176 -  apply simp_all
   8.177 +  apply (induct j, simp_all)
   8.178    apply (blast dest: Suc_lessD)
   8.179    done
   8.180  
   8.181 @@ -785,10 +765,8 @@
   8.182  
   8.183  text {* strict, in both arguments *}
   8.184  lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
   8.185 -  apply (rule add_less_mono1 [THEN less_trans])
   8.186 -  apply assumption+
   8.187 -  apply (induct_tac j)
   8.188 -  apply simp_all
   8.189 +  apply (rule add_less_mono1 [THEN less_trans], assumption+)
   8.190 +  apply (induct_tac j, simp_all)
   8.191    done
   8.192  
   8.193  text {* A [clumsy] way of lifting @{text "<"}
   8.194 @@ -803,8 +781,7 @@
   8.195  text {* non-strict, in 1st argument *}
   8.196  lemma add_le_mono1: "i <= j ==> i + k <= j + (k::nat)"
   8.197    apply (rule_tac f = "%j. j + k" in less_mono_imp_le_mono)
   8.198 -  apply (erule add_less_mono1)
   8.199 -  apply assumption
   8.200 +  apply (erule add_less_mono1, assumption)
   8.201    done
   8.202  
   8.203  text {* non-strict, in both arguments *}
   8.204 @@ -853,8 +830,7 @@
   8.205  
   8.206  lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
   8.207    apply (induct_tac m)
   8.208 -  apply (induct_tac [2] n)
   8.209 -  apply simp_all
   8.210 +  apply (induct_tac [2] n, simp_all)
   8.211    done
   8.212  
   8.213  
   8.214 @@ -899,8 +875,7 @@
   8.215    by (simp add: diff_diff_left)
   8.216  
   8.217  lemma diff_Suc_less [simp]: "0<n ==> n - Suc i < n"
   8.218 -  apply (case_tac "n")
   8.219 -  apply safe
   8.220 +  apply (case_tac "n", safe)
   8.221    apply (simp add: le_simps)
   8.222    done
   8.223  
   8.224 @@ -947,8 +922,7 @@
   8.225  
   8.226  lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"
   8.227    apply (rule diff_self_eq_0 [THEN subst])
   8.228 -  apply (rule zero_induct_lemma)
   8.229 -  apply rules+
   8.230 +  apply (rule zero_induct_lemma, rules+)
   8.231    done
   8.232  
   8.233  lemma diff_cancel: "(k + m) - (k + n) = m - (n::nat)"
   8.234 @@ -992,8 +966,7 @@
   8.235  
   8.236  text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}
   8.237  lemma mult_less_mono2: "(i::nat) < j ==> 0 < k ==> k * i < k * j"
   8.238 -  apply (erule_tac m1 = "0" in less_imp_Suc_add [THEN exE])
   8.239 -  apply simp
   8.240 +  apply (erule_tac m1 = 0 in less_imp_Suc_add [THEN exE], simp)
   8.241    apply (induct_tac x)
   8.242    apply (simp_all add: add_less_mono)
   8.243    done
   8.244 @@ -1003,34 +976,27 @@
   8.245  
   8.246  lemma zero_less_mult_iff [simp]: "(0 < (m::nat) * n) = (0 < m & 0 < n)"
   8.247    apply (induct m)
   8.248 -  apply (case_tac [2] n)
   8.249 -  apply simp_all
   8.250 +  apply (case_tac [2] n, simp_all)
   8.251    done
   8.252  
   8.253  lemma one_le_mult_iff [simp]: "(Suc 0 <= m * n) = (1 <= m & 1 <= n)"
   8.254    apply (induct m)
   8.255 -  apply (case_tac [2] n)
   8.256 -  apply simp_all
   8.257 +  apply (case_tac [2] n, simp_all)
   8.258    done
   8.259  
   8.260  lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = 1 & n = 1)"
   8.261 -  apply (induct_tac m)
   8.262 -  apply simp
   8.263 -  apply (induct_tac n)
   8.264 -  apply simp
   8.265 -  apply fastsimp
   8.266 +  apply (induct_tac m, simp)
   8.267 +  apply (induct_tac n, simp, fastsimp)
   8.268    done
   8.269  
   8.270  lemma one_eq_mult_iff [simp]: "(Suc 0 = m * n) = (m = 1 & n = 1)"
   8.271    apply (rule trans)
   8.272 -  apply (rule_tac [2] mult_eq_1_iff)
   8.273 -  apply fastsimp
   8.274 +  apply (rule_tac [2] mult_eq_1_iff, fastsimp)
   8.275    done
   8.276  
   8.277  lemma mult_less_cancel2: "((m::nat) * k < n * k) = (0 < k & m < n)"
   8.278    apply (safe intro!: mult_less_mono1)
   8.279 -  apply (case_tac k)
   8.280 -  apply auto
   8.281 +  apply (case_tac k, auto)
   8.282    apply (simp del: le_0_eq add: linorder_not_le [symmetric])
   8.283    apply (blast intro: mult_le_mono1)
   8.284    done
   8.285 @@ -1041,19 +1007,13 @@
   8.286  declare mult_less_cancel2 [simp]
   8.287  
   8.288  lemma mult_le_cancel1 [simp]: "(k * (m::nat) <= k * n) = (0 < k --> m <= n)"
   8.289 -  apply (simp add: linorder_not_less [symmetric])
   8.290 -  apply auto
   8.291 -  done
   8.292 +by (simp add: linorder_not_less [symmetric], auto)
   8.293  
   8.294  lemma mult_le_cancel2 [simp]: "((m::nat) * k <= n * k) = (0 < k --> m <= n)"
   8.295 -  apply (simp add: linorder_not_less [symmetric])
   8.296 -  apply auto
   8.297 -  done
   8.298 +by (simp add: linorder_not_less [symmetric], auto)
   8.299  
   8.300  lemma mult_cancel2: "(m * k = n * k) = (m = n | (k = (0::nat)))"
   8.301 -  apply (cut_tac less_linear)
   8.302 -  apply safe
   8.303 -  apply auto
   8.304 +  apply (cut_tac less_linear, safe, auto)
   8.305    apply (drule mult_less_mono1, assumption, simp)+
   8.306    done
   8.307  
     9.1 --- a/src/HOL/NatArith.thy	Fri Sep 26 10:34:28 2003 +0200
     9.2 +++ b/src/HOL/NatArith.thy	Fri Sep 26 10:34:57 2003 +0200
     9.3 @@ -13,10 +13,8 @@
     9.4  
     9.5  
     9.6  lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m <= n)"
     9.7 -apply (simp add: less_eq reflcl_trancl [symmetric]
     9.8 -            del: reflcl_trancl)
     9.9 -apply arith
    9.10 -done
    9.11 +by (simp add: less_eq reflcl_trancl [symmetric]
    9.12 +            del: reflcl_trancl, arith)
    9.13  
    9.14  lemma nat_diff_split:
    9.15      "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
    10.1 --- a/src/HOL/Product_Type.thy	Fri Sep 26 10:34:28 2003 +0200
    10.2 +++ b/src/HOL/Product_Type.thy	Fri Sep 26 10:34:57 2003 +0200
    10.3 @@ -154,8 +154,7 @@
    10.4  
    10.5  lemma Pair_Rep_inject: "Pair_Rep a b = Pair_Rep a' b' ==> a = a' & b = b'"
    10.6    apply (unfold Pair_Rep_def)
    10.7 -  apply (drule fun_cong [THEN fun_cong])
    10.8 -  apply blast
    10.9 +  apply (drule fun_cong [THEN fun_cong], blast)
   10.10    done
   10.11  
   10.12  lemma inj_on_Abs_Prod: "inj_on Abs_Prod Prod"
   10.13 @@ -302,8 +301,7 @@
   10.14  lemma split_Pair_apply: "split (%x y. f (x, y)) = f"
   10.15    -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *}
   10.16    apply (rule ext)
   10.17 -  apply (tactic {* pair_tac "x" 1 *})
   10.18 -  apply simp
   10.19 +  apply (tactic {* pair_tac "x" 1 *}, simp)
   10.20    done
   10.21  
   10.22  lemma split_paired_The: "(THE x. P x) = (THE (a, b). P (a, b))"
   10.23 @@ -314,9 +312,7 @@
   10.24    by (simp add: split_def)
   10.25  
   10.26  lemma Pair_fst_snd_eq: "!!s t. (s = t) = (fst s = fst t & snd s = snd t)"
   10.27 -  apply (simp only: split_tupled_all)
   10.28 -  apply simp
   10.29 -  done
   10.30 +by (simp only: split_tupled_all, simp)
   10.31  
   10.32  lemma prod_eqI [intro?]: "fst p = fst q ==> snd p = snd q ==> p = q"
   10.33    by (simp add: Pair_fst_snd_eq)
   10.34 @@ -396,8 +392,7 @@
   10.35  lemma split_split: "R (split c p) = (ALL x y. p = (x, y) --> R (c x y))"
   10.36    -- {* For use with @{text split} and the Simplifier. *}
   10.37    apply (subst surjective_pairing)
   10.38 -  apply (subst split_conv)
   10.39 -  apply blast
   10.40 +  apply (subst split_conv, blast)
   10.41    done
   10.42  
   10.43  text {*
   10.44 @@ -408,9 +403,7 @@
   10.45  *}
   10.46  
   10.47  lemma split_split_asm: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))"
   10.48 -  apply (subst split_split)
   10.49 -  apply simp
   10.50 -  done
   10.51 +by (subst split_split, simp)
   10.52  
   10.53  
   10.54  text {*
   10.55 @@ -453,9 +446,7 @@
   10.56    by simp
   10.57  
   10.58  lemma mem_splitI2: "!!p. [| !!a b. p = (a, b) ==> z: c a b |] ==> z: split c p"
   10.59 -  apply (simp only: split_tupled_all)
   10.60 -  apply simp
   10.61 -  done
   10.62 +by (simp only: split_tupled_all, simp)
   10.63  
   10.64  lemma mem_splitE: "[| z: split c p; !!x y. [| p = (x,y); z: c x y |] ==> Q |] ==> Q"
   10.65  proof -
   10.66 @@ -483,19 +474,14 @@
   10.67  "
   10.68  
   10.69  lemma split_eta_SetCompr [simp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
   10.70 -  apply (rule ext)
   10.71 -  apply fast
   10.72 -  done
   10.73 +by (rule ext, fast)
   10.74  
   10.75  lemma split_eta_SetCompr2 [simp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
   10.76 -  apply (rule ext)
   10.77 -  apply fast
   10.78 -  done
   10.79 +by (rule ext, fast)
   10.80  
   10.81  lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"
   10.82    -- {* Allows simplifications of nested splits in case of independent predicates. *}
   10.83 -  apply (rule ext)
   10.84 -  apply blast
   10.85 +  apply (rule ext, blast)
   10.86    done
   10.87  
   10.88  lemma split_comp_eq [simp]: 
   10.89 @@ -511,10 +497,10 @@
   10.90  ### Cannot add premise as rewrite rule because it contains (type) unknowns:
   10.91  ### ?y = .x
   10.92  Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)"
   10.93 -by (rtac some_equality 1);
   10.94 -by ( Simp_tac 1);
   10.95 -by (split_all_tac 1);
   10.96 -by (Asm_full_simp_tac 1);
   10.97 +by (rtac some_equality 1)
   10.98 +by ( Simp_tac 1)
   10.99 +by (split_all_tac 1)
  10.100 +by (Asm_full_simp_tac 1)
  10.101  qed "The_split_eq";
  10.102  *)
  10.103  
  10.104 @@ -532,20 +518,17 @@
  10.105  
  10.106  lemma prod_fun_compose: "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)"
  10.107    apply (rule ext)
  10.108 -  apply (tactic {* pair_tac "x" 1 *})
  10.109 -  apply simp
  10.110 +  apply (tactic {* pair_tac "x" 1 *}, simp)
  10.111    done
  10.112  
  10.113  lemma prod_fun_ident [simp]: "prod_fun (%x. x) (%y. y) = (%z. z)"
  10.114    apply (rule ext)
  10.115 -  apply (tactic {* pair_tac "z" 1 *})
  10.116 -  apply simp
  10.117 +  apply (tactic {* pair_tac "z" 1 *}, simp)
  10.118    done
  10.119  
  10.120  lemma prod_fun_imageI [intro]: "(a, b) : r ==> (f a, g b) : prod_fun f g ` r"
  10.121    apply (rule image_eqI)
  10.122 -  apply (rule prod_fun [symmetric])
  10.123 -  apply assumption
  10.124 +  apply (rule prod_fun [symmetric], assumption)
  10.125    done
  10.126  
  10.127  lemma prod_fun_imageE [elim!]:
  10.128 @@ -599,14 +582,10 @@
  10.129  *}
  10.130  
  10.131  lemma SigmaD1: "(a, b) : Sigma A B ==> a : A"
  10.132 -  apply (erule SigmaE)
  10.133 -  apply blast
  10.134 -  done
  10.135 +by (erule SigmaE, blast)
  10.136  
  10.137  lemma SigmaD2: "(a, b) : Sigma A B ==> b : B a"
  10.138 -  apply (erule SigmaE)
  10.139 -  apply blast
  10.140 -  done
  10.141 +by (erule SigmaE, blast)
  10.142  
  10.143  lemma SigmaE2:
  10.144      "[| (a, b) : Sigma A B;
    11.1 --- a/src/HOL/Set.thy	Fri Sep 26 10:34:28 2003 +0200
    11.2 +++ b/src/HOL/Set.thy	Fri Sep 26 10:34:57 2003 +0200
    11.3 @@ -779,8 +779,7 @@
    11.4  lemma subset_image_iff: "(B \<subseteq> f`A) = (EX AA. AA \<subseteq> A & B = f`AA)"
    11.5    apply safe
    11.6     prefer 2 apply fast
    11.7 -  apply (rule_tac x = "{a. a : A & f a : B}" in exI)
    11.8 -  apply fast
    11.9 +  apply (rule_tac x = "{a. a : A & f a : B}" in exI, fast)
   11.10    done
   11.11  
   11.12  lemma image_subsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f`A \<subseteq> B"
   11.13 @@ -1044,8 +1043,7 @@
   11.14  
   11.15  lemma mk_disjoint_insert: "a \<in> A ==> \<exists>B. A = insert a B & a \<notin> B"
   11.16    -- {* use new @{text B} rather than @{text "A - {a}"} to avoid infinite unfolding *}
   11.17 -  apply (rule_tac x = "A - {a}" in exI)
   11.18 -  apply blast
   11.19 +  apply (rule_tac x = "A - {a}" in exI, blast)
   11.20    done
   11.21  
   11.22  lemma insert_Collect: "insert a (Collect P) = {u. u \<noteq> a --> P u}"
   11.23 @@ -1103,9 +1101,7 @@
   11.24    by auto
   11.25  
   11.26  lemma range_composition [simp]: "range (\<lambda>x. f (g x)) = f`range g"
   11.27 -  apply (subst image_image)
   11.28 -  apply simp
   11.29 -  done
   11.30 +by (subst image_image, simp)
   11.31  
   11.32  
   11.33  text {* \medskip @{text Int} *}
   11.34 @@ -1345,7 +1341,7 @@
   11.35  lemma Inter_UNIV_conv [iff]:
   11.36    "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
   11.37    "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
   11.38 -  by(blast)+
   11.39 +  by blast+
   11.40  
   11.41  
   11.42  text {*
   11.43 @@ -1578,8 +1574,7 @@
   11.44  
   11.45  lemma all_bool_eq: "(\<forall>b::bool. P b) = (P True & P False)"
   11.46    apply auto
   11.47 -  apply (tactic {* case_tac "b" 1 *})
   11.48 -   apply auto
   11.49 +  apply (tactic {* case_tac "b" 1 *}, auto)
   11.50    done
   11.51  
   11.52  lemma bool_induct: "P True \<Longrightarrow> P False \<Longrightarrow> P x"
   11.53 @@ -1587,8 +1582,7 @@
   11.54  
   11.55  lemma ex_bool_eq: "(\<exists>b::bool. P b) = (P True | P False)"
   11.56    apply auto
   11.57 -  apply (tactic {* case_tac "b" 1 *})
   11.58 -   apply auto
   11.59 +  apply (tactic {* case_tac "b" 1 *}, auto)
   11.60    done
   11.61  
   11.62  lemma Un_eq_UN: "A \<union> B = (\<Union>b. if b then A else B)"
   11.63 @@ -1596,14 +1590,12 @@
   11.64  
   11.65  lemma UN_bool_eq: "(\<Union>b::bool. A b) = (A True \<union> A False)"
   11.66    apply auto
   11.67 -  apply (tactic {* case_tac "b" 1 *})
   11.68 -   apply auto
   11.69 +  apply (tactic {* case_tac "b" 1 *}, auto)
   11.70    done
   11.71  
   11.72  lemma INT_bool_eq: "(\<Inter>b::bool. A b) = (A True \<inter> A False)"
   11.73    apply auto
   11.74 -  apply (tactic {* case_tac "b" 1 *})
   11.75 -  apply auto
   11.76 +  apply (tactic {* case_tac "b" 1 *}, auto)
   11.77    done
   11.78  
   11.79  
   11.80 @@ -1800,8 +1792,7 @@
   11.81  
   11.82  lemma in_mono: "A \<subseteq> B ==> x \<in> A --> x \<in> B"
   11.83    apply (rule impI)
   11.84 -  apply (erule subsetD)
   11.85 -  apply assumption
   11.86 +  apply (erule subsetD, assumption)
   11.87    done
   11.88  
   11.89  lemma conj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 & P2) --> (Q1 & Q2)"
   11.90 @@ -1843,8 +1834,7 @@
   11.91      ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
   11.92      -- {* Courtesy of Stephan Merz *}
   11.93    apply clarify
   11.94 -  apply (erule_tac P = "%x. x : S" in LeastI2)
   11.95 -   apply fast
   11.96 +  apply (erule_tac P = "%x. x : S" in LeastI2, fast)
   11.97    apply (rule LeastI2)
   11.98    apply (auto elim: monoD intro!: order_antisym)
   11.99    done
    12.1 --- a/src/HOL/Transitive_Closure.thy	Fri Sep 26 10:34:28 2003 +0200
    12.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Sep 26 10:34:57 2003 +0200
    12.3 @@ -57,8 +57,7 @@
    12.4    apply (rule subsetI)
    12.5    apply (simp only: split_tupled_all)
    12.6    apply (erule rtrancl.induct)
    12.7 -   apply (rule_tac [2] rtrancl_into_rtrancl)
    12.8 -    apply blast+
    12.9 +   apply (rule_tac [2] rtrancl_into_rtrancl, blast+)
   12.10    done
   12.11  
   12.12  theorem rtrancl_induct [consumes 1, induct set: rtrancl]:
   12.13 @@ -126,15 +125,11 @@
   12.14    done
   12.15  
   12.16  lemma rtrancl_subset_rtrancl: "r \<subseteq> s^* ==> r^* \<subseteq> s^*"
   12.17 -  apply (drule rtrancl_mono)
   12.18 -  apply simp
   12.19 -  done
   12.20 +by (drule rtrancl_mono, simp)
   12.21  
   12.22  lemma rtrancl_subset: "R \<subseteq> S ==> S \<subseteq> R^* ==> S^* = R^*"
   12.23    apply (drule rtrancl_mono)
   12.24 -  apply (drule rtrancl_mono)
   12.25 -  apply simp
   12.26 -  apply blast
   12.27 +  apply (drule rtrancl_mono, simp, blast)
   12.28    done
   12.29  
   12.30  lemma rtrancl_Un_rtrancl: "(R^* \<union> S^*)^* = (R \<union> S)^*"
   12.31 @@ -145,12 +140,9 @@
   12.32  
   12.33  lemma rtrancl_r_diff_Id: "(r - Id)^* = r^*"
   12.34    apply (rule sym)
   12.35 -  apply (rule rtrancl_subset)
   12.36 -   apply blast
   12.37 -  apply clarify
   12.38 +  apply (rule rtrancl_subset, blast, clarify)
   12.39    apply (rename_tac a b)
   12.40 -  apply (case_tac "a = b")
   12.41 -   apply blast
   12.42 +  apply (case_tac "a = b", blast)
   12.43    apply (blast intro!: r_into_rtrancl)
   12.44    done
   12.45  
   12.46 @@ -239,8 +231,7 @@
   12.47  
   12.48  lemma rtrancl_into_trancl2: "[| (a,b) : r;  (b,c) : r^* |]   ==>  (a,c) : r^+"
   12.49    -- {* intro rule from @{text r} and @{text rtrancl} *}
   12.50 -  apply (erule rtranclE)
   12.51 -   apply rules
   12.52 +  apply (erule rtranclE, rules)
   12.53    apply (rule rtrancl_trans [THEN rtrancl_into_trancl1])
   12.54     apply (assumption | rule r_into_rtrancl)+
   12.55    done
   12.56 @@ -296,8 +287,7 @@
   12.57    apply (rule equalityI)
   12.58     apply (rule subsetI)
   12.59     apply (simp only: split_tupled_all)
   12.60 -   apply (erule trancl_induct)
   12.61 -    apply blast
   12.62 +   apply (erule trancl_induct, blast)
   12.63     apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl r_into_trancl trancl_trans)
   12.64    apply (rule subsetI)
   12.65    apply (blast intro: trancl_mono rtrancl_mono
   12.66 @@ -336,8 +326,7 @@
   12.67  qed
   12.68  
   12.69  lemma tranclD: "(x, y) \<in> R^+ ==> EX z. (x, z) \<in> R \<and> (z, y) \<in> R^*"
   12.70 -  apply (erule converse_trancl_induct)
   12.71 -   apply auto
   12.72 +  apply (erule converse_trancl_induct, auto)
   12.73    apply (blast intro: rtrancl_trans)
   12.74    done
   12.75  
   12.76 @@ -349,8 +338,7 @@
   12.77  
   12.78  lemma trancl_subset_Sigma_aux:
   12.79      "(a, b) \<in> r^* ==> r \<subseteq> A \<times> A ==> a = b \<or> a \<in> A"
   12.80 -  apply (erule rtrancl_induct)
   12.81 -   apply auto
   12.82 +  apply (erule rtrancl_induct, auto)
   12.83    done
   12.84  
   12.85  lemma trancl_subset_Sigma: "r \<subseteq> A \<times> A ==> r^+ \<subseteq> A \<times> A"
   12.86 @@ -368,15 +356,11 @@
   12.87  
   12.88  lemma trancl_reflcl [simp]: "(r^=)^+ = r^*"
   12.89    apply safe
   12.90 -   apply (drule trancl_into_rtrancl)
   12.91 -   apply simp
   12.92 -  apply (erule rtranclE)
   12.93 -   apply safe
   12.94 -   apply (rule r_into_trancl)
   12.95 -   apply simp
   12.96 +   apply (drule trancl_into_rtrancl, simp)
   12.97 +  apply (erule rtranclE, safe)
   12.98 +   apply (rule r_into_trancl, simp)
   12.99    apply (rule rtrancl_into_trancl1)
  12.100 -   apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD])
  12.101 -  apply fast
  12.102 +   apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD], fast)
  12.103    done
  12.104  
  12.105  lemma trancl_empty [simp]: "{}^+ = {}"
  12.106 @@ -433,8 +417,7 @@
  12.107    apply (drule tranclD)
  12.108    apply (erule exE, erule conjE)
  12.109    apply (drule rtrancl_trans, assumption)
  12.110 -  apply (drule rtrancl_into_trancl2, assumption)
  12.111 -  apply assumption
  12.112 +  apply (drule rtrancl_into_trancl2, assumption, assumption)
  12.113    done
  12.114  
  12.115  lemmas transitive_closure_trans [trans] =