tuned proofs;
authorwenzelm
Wed Aug 10 14:50:59 2016 +0200 (2016-08-10)
changeset 63649e690d6f2185b
parent 63648 f9f3006a5579
child 63651 f8e79d14d61f
tuned proofs;
src/HOL/Library/AList_Mapping.thy
src/HOL/Library/Complete_Partial_Order2.thy
src/HOL/Library/Convex.thy
src/HOL/Library/Countable_Set.thy
src/HOL/Library/FSet.thy
src/HOL/Library/IArray.thy
src/HOL/Library/Indicator_Function.thy
src/HOL/Library/Permutation.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Quotient_List.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/Library/RBT_Mapping.thy
src/HOL/Library/RBT_Set.thy
src/HOL/Library/Stream.thy
src/HOL/Library/Sublist.thy
     1.1 --- a/src/HOL/Library/AList_Mapping.thy	Wed Aug 10 09:33:54 2016 +0200
     1.2 +++ b/src/HOL/Library/AList_Mapping.thy	Wed Aug 10 14:50:59 2016 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4    by transfer simp
     1.5  
     1.6  lemma is_empty_Mapping [code]: "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs"
     1.7 -  by (case_tac xs) (simp_all add: is_empty_def null_def)
     1.8 +  by (cases xs) (simp_all add: is_empty_def null_def)
     1.9  
    1.10  lemma update_Mapping [code]: "Mapping.update k v (Mapping xs) = Mapping (AList.update k v xs)"
    1.11    by transfer (simp add: update_conv')
     2.1 --- a/src/HOL/Library/Complete_Partial_Order2.thy	Wed Aug 10 09:33:54 2016 +0200
     2.2 +++ b/src/HOL/Library/Complete_Partial_Order2.thy	Wed Aug 10 14:50:59 2016 +0200
     2.3 @@ -58,11 +58,17 @@
     2.4  lemma Sup_minus_bot: 
     2.5    assumes chain: "Complete_Partial_Order.chain op \<le> A"
     2.6    shows "\<Squnion>(A - {\<Squnion>{}}) = \<Squnion>A"
     2.7 -apply(rule antisym)
     2.8 - apply(blast intro: ccpo_Sup_least chain_Diff[OF chain] ccpo_Sup_upper[OF chain])
     2.9 -apply(rule ccpo_Sup_least[OF chain])
    2.10 -apply(case_tac "x = \<Squnion>{}")
    2.11 -by(blast intro: ccpo_Sup_least chain_empty ccpo_Sup_upper[OF chain_Diff[OF chain]])+
    2.12 +    (is "?lhs = ?rhs")
    2.13 +proof (rule antisym)
    2.14 +  show "?lhs \<le> ?rhs"
    2.15 +    by (blast intro: ccpo_Sup_least chain_Diff[OF chain] ccpo_Sup_upper[OF chain])
    2.16 +  show "?rhs \<le> ?lhs"
    2.17 +  proof (rule ccpo_Sup_least [OF chain])
    2.18 +    show "x \<in> A \<Longrightarrow> x \<le> ?lhs" for x
    2.19 +      by (cases "x = \<Squnion>{}")
    2.20 +        (blast intro: ccpo_Sup_least chain_empty ccpo_Sup_upper[OF chain_Diff[OF chain]])+
    2.21 +  qed
    2.22 +qed
    2.23  
    2.24  lemma mono_lub:
    2.25    fixes le_b (infix "\<sqsubseteq>" 60)
     3.1 --- a/src/HOL/Library/Convex.thy	Wed Aug 10 09:33:54 2016 +0200
     3.2 +++ b/src/HOL/Library/Convex.thy	Wed Aug 10 14:50:59 2016 +0200
     3.3 @@ -287,18 +287,20 @@
     3.4    assumes "finite s"
     3.5    shows "convex s \<longleftrightarrow> (\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<longrightarrow> setsum (\<lambda>x. u x *\<^sub>R x) s \<in> s)"
     3.6    unfolding convex_explicit
     3.7 -proof safe
     3.8 -  fix t u
     3.9 -  assume sum: "\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> s"
    3.10 -    and as: "finite t" "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = (1::real)"
    3.11 -  have *: "s \<inter> t = t"
    3.12 -    using as(2) by auto
    3.13 -  have if_distrib_arg: "\<And>P f g x. (if P then f else g) x = (if P then f x else g x)"
    3.14 -    by simp
    3.15 -  show "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
    3.16 -    using sum[THEN spec[where x="\<lambda>x. if x\<in>t then u x else 0"]] as *
    3.17 -    by (auto simp: assms setsum.If_cases if_distrib if_distrib_arg)
    3.18 -qed (erule_tac x=s in allE, erule_tac x=u in allE, auto)
    3.19 +  apply safe
    3.20 +  subgoal for u by (erule allE [where x=s], erule allE [where x=u]) auto
    3.21 +  subgoal for t u
    3.22 +  proof -
    3.23 +    have if_distrib_arg: "\<And>P f g x. (if P then f else g) x = (if P then f x else g x)"
    3.24 +      by simp
    3.25 +    assume sum: "\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> s"
    3.26 +    assume *: "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1"
    3.27 +    assume "t \<subseteq> s"
    3.28 +    then have "s \<inter> t = t" by auto
    3.29 +    with sum[THEN spec[where x="\<lambda>x. if x\<in>t then u x else 0"]] * show "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
    3.30 +      by (auto simp: assms setsum.If_cases if_distrib if_distrib_arg)
    3.31 +  qed
    3.32 +  done 
    3.33  
    3.34  
    3.35  subsection \<open>Functions that are convex on a set\<close>
     4.1 --- a/src/HOL/Library/Countable_Set.thy	Wed Aug 10 09:33:54 2016 +0200
     4.2 +++ b/src/HOL/Library/Countable_Set.thy	Wed Aug 10 14:50:59 2016 +0200
     4.3 @@ -304,10 +304,9 @@
     4.4     (is "?lhs = ?rhs")
     4.5  proof
     4.6    assume ?lhs
     4.7 -  then show ?rhs
     4.8 -    apply (rule_tac x="inv_into A f ` B" in exI)
     4.9 -    apply (auto simp: f_inv_into_f subset_iff image_inv_into_cancel inv_into_into)
    4.10 -    done
    4.11 +  show ?rhs
    4.12 +    by (rule exI [where x="inv_into A f ` B"])
    4.13 +      (use \<open>?lhs\<close> in \<open>auto simp: f_inv_into_f subset_iff image_inv_into_cancel inv_into_into\<close>)
    4.14  next
    4.15    assume ?rhs
    4.16    then show ?lhs by force
     5.1 --- a/src/HOL/Library/FSet.thy	Wed Aug 10 09:33:54 2016 +0200
     5.2 +++ b/src/HOL/Library/FSet.thy	Wed Aug 10 14:50:59 2016 +0200
     5.3 @@ -528,7 +528,7 @@
     5.4  using assms by transfer (metis Set.set_insert finite_insert)
     5.5  
     5.6  lemma mk_disjoint_finsert: "a |\<in>| A \<Longrightarrow> \<exists>B. A = finsert a B \<and> a |\<notin>| B"
     5.7 -  by (rule_tac x = "A |-| {|a|}" in exI, blast)
     5.8 +  by (rule exI [where x = "A |-| {|a|}"]) blast
     5.9  
    5.10  
    5.11  subsubsection \<open>\<open>fimage\<close>\<close>
     6.1 --- a/src/HOL/Library/IArray.thy	Wed Aug 10 09:33:54 2016 +0200
     6.2 +++ b/src/HOL/Library/IArray.thy	Wed Aug 10 14:50:59 2016 +0200
     6.3 @@ -71,15 +71,15 @@
     6.4  
     6.5  lemma [code]:
     6.6    "set_iarray as = set (IArray.list_of as)"
     6.7 -  by (case_tac as) auto
     6.8 +  by (cases as) auto
     6.9  
    6.10  lemma [code]:
    6.11    "map_iarray f as = IArray (map f (IArray.list_of as))"
    6.12 -  by (case_tac as) auto
    6.13 +  by (cases as) auto
    6.14  
    6.15  lemma [code]:
    6.16    "rel_iarray r as bs = list_all2 r (IArray.list_of as) (IArray.list_of bs)"
    6.17 -  by (case_tac as) (case_tac bs, auto)
    6.18 +  by (cases as, cases bs) auto
    6.19  
    6.20  lemma [code]:
    6.21    "HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
     7.1 --- a/src/HOL/Library/Indicator_Function.thy	Wed Aug 10 09:33:54 2016 +0200
     7.2 +++ b/src/HOL/Library/Indicator_Function.thy	Wed Aug 10 14:50:59 2016 +0200
     7.3 @@ -97,12 +97,12 @@
     7.4    case True
     7.5    then obtain i where "x \<in> A i"
     7.6      by auto
     7.7 -  then have
     7.8 +  then have *:
     7.9      "\<And>n. (indicator (A (n + i)) x :: 'a) = 1"
    7.10      "(indicator (\<Union>i. A i) x :: 'a) = 1"
    7.11      using incseqD[OF \<open>incseq A\<close>, of i "n + i" for n] \<open>x \<in> A i\<close> by (auto simp: indicator_def)
    7.12 -  then show ?thesis
    7.13 -    by (rule_tac LIMSEQ_offset[of _ i]) simp
    7.14 +  show ?thesis
    7.15 +    by (rule LIMSEQ_offset[of _ i]) (use * in simp)
    7.16  next
    7.17    case False
    7.18    then show ?thesis by (simp add: indicator_def)
    7.19 @@ -125,12 +125,12 @@
    7.20    case True
    7.21    then obtain i where "x \<notin> A i"
    7.22      by auto
    7.23 -  then have
    7.24 +  then have *:
    7.25      "\<And>n. (indicator (A (n + i)) x :: 'a) = 0"
    7.26      "(indicator (\<Inter>i. A i) x :: 'a) = 0"
    7.27      using decseqD[OF \<open>decseq A\<close>, of i "n + i" for n] \<open>x \<notin> A i\<close> by (auto simp: indicator_def)
    7.28 -  then show ?thesis
    7.29 -    by (rule_tac LIMSEQ_offset[of _ i]) simp
    7.30 +  show ?thesis
    7.31 +    by (rule LIMSEQ_offset[of _ i]) (use * in simp)
    7.32  next
    7.33    case False
    7.34    then show ?thesis by (simp add: indicator_def)
     8.1 --- a/src/HOL/Library/Permutation.thy	Wed Aug 10 09:33:54 2016 +0200
     8.2 +++ b/src/HOL/Library/Permutation.thy	Wed Aug 10 14:50:59 2016 +0200
     8.3 @@ -95,7 +95,7 @@
     8.4    by auto
     8.5  
     8.6  proposition cons_perm_imp_perm: "z # xs <~~> z # ys \<Longrightarrow> xs <~~> ys"
     8.7 -  by (drule_tac z = z in perm_remove_perm) auto
     8.8 +  by (drule perm_remove_perm [where z = z]) auto
     8.9  
    8.10  proposition cons_perm_eq [iff]: "z#xs <~~> z#ys \<longleftrightarrow> xs <~~> ys"
    8.11    by (blast intro: cons_perm_imp_perm)
     9.1 --- a/src/HOL/Library/Polynomial.thy	Wed Aug 10 09:33:54 2016 +0200
     9.2 +++ b/src/HOL/Library/Polynomial.thy	Wed Aug 10 14:50:59 2016 +0200
     9.3 @@ -1330,11 +1330,17 @@
     9.4  
     9.5  lemma synthetic_div_eq_0_iff:
     9.6    "synthetic_div p c = 0 \<longleftrightarrow> degree p = 0"
     9.7 -  by (induct p, simp, case_tac p, simp)
     9.8 +proof (induct p)
     9.9 +  case 0
    9.10 +  then show ?case by simp
    9.11 +next
    9.12 +  case (pCons a p)
    9.13 +  then show ?case by (cases p) simp
    9.14 +qed
    9.15  
    9.16  lemma degree_synthetic_div:
    9.17    "degree (synthetic_div p c) = degree p - 1"
    9.18 -  by (induct p, simp, simp add: synthetic_div_eq_0_iff)
    9.19 +  by (induct p) (simp_all add: synthetic_div_eq_0_iff)
    9.20  
    9.21  lemma synthetic_div_correct:
    9.22    "p + smult c (synthetic_div p c) = pCons (poly p c) (synthetic_div p c)"
    9.23 @@ -3479,35 +3485,40 @@
    9.24  qed (insert assms, auto)
    9.25  
    9.26  lemma poly_pinfty_gt_lc:
    9.27 -  fixes p:: "real poly"
    9.28 -  assumes  "lead_coeff p > 0" 
    9.29 -  shows "\<exists> n. \<forall> x \<ge> n. poly p x \<ge> lead_coeff p" using assms
    9.30 +  fixes p :: "real poly"
    9.31 +  assumes "lead_coeff p > 0" 
    9.32 +  shows "\<exists> n. \<forall> x \<ge> n. poly p x \<ge> lead_coeff p"
    9.33 +  using assms
    9.34  proof (induct p)
    9.35    case 0
    9.36 -  thus ?case by auto
    9.37 +  then show ?case by auto
    9.38  next
    9.39    case (pCons a p)
    9.40 -  have "\<lbrakk>a\<noteq>0;p=0\<rbrakk> \<Longrightarrow> ?case" by auto
    9.41 -  moreover have "p\<noteq>0 \<Longrightarrow> ?case"
    9.42 +  from this(1) consider "a \<noteq> 0" "p = 0" | "p \<noteq> 0" by auto
    9.43 +  then show ?case
    9.44 +  proof cases
    9.45 +    case 1
    9.46 +    then show ?thesis by auto
    9.47 +  next
    9.48 +    case 2
    9.49 +    with pCons obtain n1 where gte_lcoeff: "\<forall>x\<ge>n1. lead_coeff p \<le> poly p x"
    9.50 +      by auto
    9.51 +    from pCons(3) \<open>p \<noteq> 0\<close> have gt_0: "lead_coeff p > 0" by auto
    9.52 +    define n where "n = max n1 (1 + \<bar>a\<bar> / lead_coeff p)"
    9.53 +    have "lead_coeff (pCons a p) \<le> poly (pCons a p) x" if "n \<le> x" for x
    9.54      proof -
    9.55 -      assume "p\<noteq>0"
    9.56 -      then obtain n1 where gte_lcoeff:"\<forall>x\<ge>n1. lead_coeff p \<le> poly p x" using that pCons by auto
    9.57 -      have gt_0:"lead_coeff p >0" using pCons(3) \<open>p\<noteq>0\<close> by auto
    9.58 -      define n where "n = max n1 (1+ \<bar>a\<bar>/(lead_coeff p))"
    9.59 -      show ?thesis 
    9.60 -        proof (rule_tac x=n in exI,rule,rule) 
    9.61 -          fix x assume "n \<le> x"
    9.62 -          hence "lead_coeff p \<le> poly p x" 
    9.63 -            using gte_lcoeff unfolding n_def by auto
    9.64 -          hence " \<bar>a\<bar>/(lead_coeff p) \<ge> \<bar>a\<bar>/(poly p x)" and "poly p x>0" using gt_0
    9.65 -            by (intro frac_le,auto)
    9.66 -          hence "x\<ge>1+ \<bar>a\<bar>/(poly p x)" using \<open>n\<le>x\<close>[unfolded n_def] by auto
    9.67 -          thus "lead_coeff (pCons a p) \<le> poly (pCons a p) x"
    9.68 -            using \<open>lead_coeff p \<le> poly p x\<close> \<open>poly p x>0\<close> \<open>p\<noteq>0\<close>
    9.69 -            by (auto simp add:field_simps)
    9.70 -        qed
    9.71 +      from gte_lcoeff that have "lead_coeff p \<le> poly p x"
    9.72 +        by (auto simp: n_def)
    9.73 +      with gt_0 have "\<bar>a\<bar> / lead_coeff p \<ge> \<bar>a\<bar> / poly p x" and "poly p x > 0"
    9.74 +        by (auto intro: frac_le)
    9.75 +      with \<open>n\<le>x\<close>[unfolded n_def] have "x \<ge> 1 + \<bar>a\<bar> / poly p x"
    9.76 +        by auto
    9.77 +      with \<open>lead_coeff p \<le> poly p x\<close> \<open>poly p x > 0\<close> \<open>p \<noteq> 0\<close>
    9.78 +      show "lead_coeff (pCons a p) \<le> poly (pCons a p) x"
    9.79 +        by (auto simp: field_simps)
    9.80      qed
    9.81 -  ultimately show ?case by fastforce
    9.82 +    then show ?thesis by blast
    9.83 +  qed
    9.84  qed
    9.85  
    9.86  
    9.87 @@ -3831,9 +3842,7 @@
    9.88    "rsquarefree p = (p \<noteq> 0 & (\<forall>a. (order a p = 0) | (order a p = 1)))"
    9.89  
    9.90  lemma pderiv_iszero: "pderiv p = 0 \<Longrightarrow> \<exists>h. p = [:h :: 'a :: {semidom,semiring_char_0}:]"
    9.91 -apply (simp add: pderiv_eq_0_iff)
    9.92 -apply (case_tac p, auto split: if_splits)
    9.93 -done
    9.94 +  by (cases p) (auto simp: pderiv_eq_0_iff split: if_splits)
    9.95  
    9.96  lemma rsquarefree_roots:
    9.97    fixes p :: "'a :: field_char_0 poly"
    10.1 --- a/src/HOL/Library/Quotient_List.thy	Wed Aug 10 09:33:54 2016 +0200
    10.2 +++ b/src/HOL/Library/Quotient_List.thy	Wed Aug 10 14:50:59 2016 +0200
    10.3 @@ -145,7 +145,6 @@
    10.4    shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"
    10.5    by (simp add: fun_eq_iff foldl_prs_aux [OF a b])
    10.6  
    10.7 -(* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *)
    10.8  lemma foldl_rsp[quot_respect]:
    10.9    assumes q1: "Quotient3 R1 Abs1 Rep1"
   10.10    and     q2: "Quotient3 R2 Abs2 Rep2"
    11.1 --- a/src/HOL/Library/RBT_Impl.thy	Wed Aug 10 09:33:54 2016 +0200
    11.2 +++ b/src/HOL/Library/RBT_Impl.thy	Wed Aug 10 14:50:59 2016 +0200
    11.3 @@ -531,23 +531,18 @@
    11.4    by (simp add: rbt_insertwk_is_rbt rbt_insertw_def)
    11.5  
    11.6  lemma rbt_lookup_rbt_insertw:
    11.7 -  assumes "is_rbt t"
    11.8 -  shows "rbt_lookup (rbt_insert_with f k v t) = (rbt_lookup t)(k \<mapsto> (if k:dom (rbt_lookup t) then f (the (rbt_lookup t k)) v else v))"
    11.9 -using assms
   11.10 -unfolding rbt_insertw_def
   11.11 -by (rule_tac ext) (cases "rbt_lookup t k", auto simp:rbt_lookup_rbt_insertwk dom_def)
   11.12 +  "is_rbt t \<Longrightarrow>
   11.13 +    rbt_lookup (rbt_insert_with f k v t) =
   11.14 +      (rbt_lookup t)(k \<mapsto> (if k \<in> dom (rbt_lookup t) then f (the (rbt_lookup t k)) v else v))"
   11.15 +  by (rule ext, cases "rbt_lookup t k") (auto simp: rbt_lookup_rbt_insertwk dom_def rbt_insertw_def)
   11.16  
   11.17  lemma rbt_insert_rbt_sorted: "rbt_sorted t \<Longrightarrow> rbt_sorted (rbt_insert k v t)"
   11.18    by (simp add: rbt_insertwk_rbt_sorted rbt_insert_def)
   11.19  theorem rbt_insert_is_rbt [simp]: "is_rbt t \<Longrightarrow> is_rbt (rbt_insert k v t)"
   11.20    by (simp add: rbt_insertwk_is_rbt rbt_insert_def)
   11.21  
   11.22 -lemma rbt_lookup_rbt_insert: 
   11.23 -  assumes "is_rbt t"
   11.24 -  shows "rbt_lookup (rbt_insert k v t) = (rbt_lookup t)(k\<mapsto>v)"
   11.25 -unfolding rbt_insert_def
   11.26 -using assms
   11.27 -by (rule_tac ext) (simp add: rbt_lookup_rbt_insertwk split:option.split)
   11.28 +lemma rbt_lookup_rbt_insert: "is_rbt t \<Longrightarrow> rbt_lookup (rbt_insert k v t) = (rbt_lookup t)(k\<mapsto>v)"
   11.29 +  by (rule ext) (simp add: rbt_insert_def rbt_lookup_rbt_insertwk split: option.split)
   11.30  
   11.31  end
   11.32  
    12.1 --- a/src/HOL/Library/RBT_Mapping.thy	Wed Aug 10 09:33:54 2016 +0200
    12.2 +++ b/src/HOL/Library/RBT_Mapping.thy	Wed Aug 10 14:50:59 2016 +0200
    12.3 @@ -43,7 +43,10 @@
    12.4  
    12.5  lemma map_entry_Mapping [code]:
    12.6    "Mapping.map_entry k f (Mapping t) = Mapping (RBT.map_entry k f t)"
    12.7 -  apply (transfer fixing: t) by (case_tac "RBT.lookup t k") auto
    12.8 +  apply (transfer fixing: t)
    12.9 +  apply (case_tac "RBT.lookup t k")
   12.10 +   apply auto
   12.11 +  done
   12.12  
   12.13  lemma keys_Mapping [code]:
   12.14    "Mapping.keys (Mapping t) = set (RBT.keys t)"
    13.1 --- a/src/HOL/Library/RBT_Set.thy	Wed Aug 10 09:33:54 2016 +0200
    13.2 +++ b/src/HOL/Library/RBT_Set.thy	Wed Aug 10 14:50:59 2016 +0200
    13.3 @@ -273,12 +273,14 @@
    13.4    assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t1 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
    13.5    assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t1 \<noteq> rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
    13.6    shows "P t"
    13.7 -using assms
    13.8 -  apply (induction t)
    13.9 -  apply simp
   13.10 -  apply (case_tac "t1 = rbt.Empty")
   13.11 -  apply simp_all
   13.12 -done
   13.13 +  using assms
   13.14 +proof (induct t)
   13.15 +  case Empty
   13.16 +  then show ?case by simp
   13.17 +next
   13.18 +  case (Branch x1 t1 x3 x4 t2)
   13.19 +  then show ?case by (cases "t1 = rbt.Empty") simp_all
   13.20 +qed
   13.21  
   13.22  lemma rbt_min_opt_in_set: 
   13.23    fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
   13.24 @@ -372,12 +374,14 @@
   13.25    assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t2 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
   13.26    assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t2 \<noteq> rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
   13.27    shows "P t"
   13.28 -using assms
   13.29 -  apply (induction t)
   13.30 -  apply simp
   13.31 -  apply (case_tac "t2 = rbt.Empty")
   13.32 -  apply simp_all
   13.33 -done
   13.34 +  using assms
   13.35 +proof (induct t)
   13.36 +  case Empty
   13.37 +  then show ?case by simp
   13.38 +next
   13.39 +  case (Branch x1 t1 x3 x4 t2)
   13.40 +  then show ?case by (cases "t2 = rbt.Empty") simp_all
   13.41 +qed
   13.42  
   13.43  lemma rbt_max_opt_in_set: 
   13.44    fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
   13.45 @@ -468,27 +472,26 @@
   13.46  using assms unfolding is_empty_empty by transfer (auto intro: rbt_min_eq_rbt_min_opt)
   13.47  
   13.48  lemma fold_keys_min_top_eq:
   13.49 -  fixes t :: "('a :: {linorder, bounded_lattice_top}, unit) rbt"
   13.50 +  fixes t :: "('a::{linorder,bounded_lattice_top}, unit) rbt"
   13.51    assumes "\<not> (RBT.is_empty t)"
   13.52    shows "fold_keys min t top = fold1_keys min t"
   13.53  proof -
   13.54    have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold min (RBT_Impl.keys t) top = 
   13.55 -    List.fold min (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) top"
   13.56 +      List.fold min (hd (RBT_Impl.keys t) # tl (RBT_Impl.keys t)) top"
   13.57      by (simp add: hd_Cons_tl[symmetric])
   13.58 -  { fix x :: "_ :: {linorder, bounded_lattice_top}" and xs
   13.59 -    have "List.fold min (x#xs) top = List.fold min xs x"
   13.60 +  have **: "List.fold min (x # xs) top = List.fold min xs x" for x :: 'a and xs
   13.61      by (simp add: inf_min[symmetric])
   13.62 -  } note ** = this
   13.63 -  show ?thesis using assms
   13.64 +  show ?thesis
   13.65 +    using assms
   13.66      unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
   13.67      apply transfer 
   13.68      apply (case_tac t) 
   13.69 -    apply simp 
   13.70 +     apply simp 
   13.71      apply (subst *)
   13.72 -    apply simp
   13.73 +     apply simp
   13.74      apply (subst **)
   13.75      apply simp
   13.76 -  done
   13.77 +    done
   13.78  qed
   13.79  
   13.80  (* maximum *)
   13.81 @@ -506,27 +509,26 @@
   13.82  using assms unfolding is_empty_empty by transfer (auto intro: rbt_max_eq_rbt_max_opt)
   13.83  
   13.84  lemma fold_keys_max_bot_eq:
   13.85 -  fixes t :: "('a :: {linorder, bounded_lattice_bot}, unit) rbt"
   13.86 +  fixes t :: "('a::{linorder,bounded_lattice_bot}, unit) rbt"
   13.87    assumes "\<not> (RBT.is_empty t)"
   13.88    shows "fold_keys max t bot = fold1_keys max t"
   13.89  proof -
   13.90    have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold max (RBT_Impl.keys t) bot = 
   13.91 -    List.fold max (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) bot"
   13.92 +      List.fold max (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) bot"
   13.93      by (simp add: hd_Cons_tl[symmetric])
   13.94 -  { fix x :: "_ :: {linorder, bounded_lattice_bot}" and xs
   13.95 -    have "List.fold max (x#xs) bot = List.fold max xs x"
   13.96 +  have **: "List.fold max (x # xs) bot = List.fold max xs x" for x :: 'a and xs
   13.97      by (simp add: sup_max[symmetric])
   13.98 -  } note ** = this
   13.99 -  show ?thesis using assms
  13.100 +  show ?thesis
  13.101 +    using assms
  13.102      unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
  13.103      apply transfer 
  13.104      apply (case_tac t) 
  13.105 -    apply simp 
  13.106 +     apply simp 
  13.107      apply (subst *)
  13.108 -    apply simp
  13.109 +     apply simp
  13.110      apply (subst **)
  13.111      apply simp
  13.112 -  done
  13.113 +    done
  13.114  qed
  13.115  
  13.116  end
    14.1 --- a/src/HOL/Library/Stream.thy	Wed Aug 10 09:33:54 2016 +0200
    14.2 +++ b/src/HOL/Library/Stream.thy	Wed Aug 10 14:50:59 2016 +0200
    14.3 @@ -393,7 +393,7 @@
    14.4    then show "s = sconst x"
    14.5    proof (coinduction arbitrary: s)
    14.6      case Eq_stream
    14.7 -    then have "shd s = x" "sset (stl s) \<subseteq> {x}" by (case_tac [!] s) auto
    14.8 +    then have "shd s = x" "sset (stl s) \<subseteq> {x}" by (cases s; auto)+
    14.9      then have "sset (stl s) = {x}" by (cases "stl s") auto
   14.10      with \<open>shd s = x\<close> show ?case by auto
   14.11    qed
    15.1 --- a/src/HOL/Library/Sublist.thy	Wed Aug 10 09:33:54 2016 +0200
    15.2 +++ b/src/HOL/Library/Sublist.thy	Wed Aug 10 14:50:59 2016 +0200
    15.3 @@ -156,10 +156,13 @@
    15.4    by (simp_all add: strict_prefix_def cong: conj_cong)
    15.5  
    15.6  lemma take_strict_prefix: "strict_prefix xs ys \<Longrightarrow> strict_prefix (take n xs) ys"
    15.7 -  apply (induct n arbitrary: xs ys)
    15.8 -   apply (case_tac ys; simp)
    15.9 -  apply (metis prefix_order.less_trans strict_prefixI take_is_prefix)
   15.10 -  done
   15.11 +proof (induct n arbitrary: xs ys)
   15.12 +  case 0
   15.13 +  then show ?case by (cases ys) simp_all
   15.14 +next
   15.15 +  case (Suc n)
   15.16 +  then show ?case by (metis prefix_order.less_trans strict_prefixI take_is_prefix)
   15.17 +qed
   15.18  
   15.19  lemma not_prefix_cases:
   15.20    assumes pfx: "\<not> prefix ps ls"
   15.21 @@ -197,7 +200,8 @@
   15.22      and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> prefix xs ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)"
   15.23    shows "P ps ls" using np
   15.24  proof (induct ls arbitrary: ps)
   15.25 -  case Nil then show ?case
   15.26 +  case Nil
   15.27 +  then show ?case
   15.28      by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base)
   15.29  next
   15.30    case (Cons y ys)
   15.31 @@ -215,7 +219,13 @@
   15.32  "prefixes (x#xs) = [] # map (op # x) (prefixes xs)"
   15.33  
   15.34  lemma in_set_prefixes[simp]: "xs \<in> set (prefixes ys) \<longleftrightarrow> prefix xs ys"
   15.35 -by (induction "xs" arbitrary: "ys"; rename_tac "ys", case_tac "ys"; auto)
   15.36 +proof (induct xs arbitrary: ys)
   15.37 +  case Nil
   15.38 +  then show ?case by (cases ys) auto
   15.39 +next
   15.40 +  case (Cons a xs)
   15.41 +  then show ?case by (cases ys) auto
   15.42 +qed
   15.43  
   15.44  lemma length_prefixes[simp]: "length (prefixes xs) = length xs+1"
   15.45  by (induction xs) auto