--- a/src/HOL/Library/AList_Mapping.thy Wed Aug 10 15:42:52 2016 +0200
+++ b/src/HOL/Library/AList_Mapping.thy Wed Aug 10 16:55:49 2016 +0200
@@ -22,7 +22,7 @@
by transfer simp
lemma is_empty_Mapping [code]: "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs"
- by (case_tac xs) (simp_all add: is_empty_def null_def)
+ by (cases xs) (simp_all add: is_empty_def null_def)
lemma update_Mapping [code]: "Mapping.update k v (Mapping xs) = Mapping (AList.update k v xs)"
by transfer (simp add: update_conv')
--- a/src/HOL/Library/Complete_Partial_Order2.thy Wed Aug 10 15:42:52 2016 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy Wed Aug 10 16:55:49 2016 +0200
@@ -58,11 +58,17 @@
lemma Sup_minus_bot:
assumes chain: "Complete_Partial_Order.chain op \<le> A"
shows "\<Squnion>(A - {\<Squnion>{}}) = \<Squnion>A"
-apply(rule antisym)
- apply(blast intro: ccpo_Sup_least chain_Diff[OF chain] ccpo_Sup_upper[OF chain])
-apply(rule ccpo_Sup_least[OF chain])
-apply(case_tac "x = \<Squnion>{}")
-by(blast intro: ccpo_Sup_least chain_empty ccpo_Sup_upper[OF chain_Diff[OF chain]])+
+ (is "?lhs = ?rhs")
+proof (rule antisym)
+ show "?lhs \<le> ?rhs"
+ by (blast intro: ccpo_Sup_least chain_Diff[OF chain] ccpo_Sup_upper[OF chain])
+ show "?rhs \<le> ?lhs"
+ proof (rule ccpo_Sup_least [OF chain])
+ show "x \<in> A \<Longrightarrow> x \<le> ?lhs" for x
+ by (cases "x = \<Squnion>{}")
+ (blast intro: ccpo_Sup_least chain_empty ccpo_Sup_upper[OF chain_Diff[OF chain]])+
+ qed
+qed
lemma mono_lub:
fixes le_b (infix "\<sqsubseteq>" 60)
--- a/src/HOL/Library/Convex.thy Wed Aug 10 15:42:52 2016 +0200
+++ b/src/HOL/Library/Convex.thy Wed Aug 10 16:55:49 2016 +0200
@@ -287,18 +287,20 @@
assumes "finite s"
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)"
unfolding convex_explicit
-proof safe
- fix t u
- 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"
- and as: "finite t" "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = (1::real)"
- have *: "s \<inter> t = t"
- using as(2) by auto
- have if_distrib_arg: "\<And>P f g x. (if P then f else g) x = (if P then f x else g x)"
- by simp
- show "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
- using sum[THEN spec[where x="\<lambda>x. if x\<in>t then u x else 0"]] as *
- by (auto simp: assms setsum.If_cases if_distrib if_distrib_arg)
-qed (erule_tac x=s in allE, erule_tac x=u in allE, auto)
+ apply safe
+ subgoal for u by (erule allE [where x=s], erule allE [where x=u]) auto
+ subgoal for t u
+ proof -
+ have if_distrib_arg: "\<And>P f g x. (if P then f else g) x = (if P then f x else g x)"
+ by simp
+ 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"
+ assume *: "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1"
+ assume "t \<subseteq> s"
+ then have "s \<inter> t = t" by auto
+ 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"
+ by (auto simp: assms setsum.If_cases if_distrib if_distrib_arg)
+ qed
+ done
subsection \<open>Functions that are convex on a set\<close>
--- a/src/HOL/Library/Countable_Set.thy Wed Aug 10 15:42:52 2016 +0200
+++ b/src/HOL/Library/Countable_Set.thy Wed Aug 10 16:55:49 2016 +0200
@@ -304,10 +304,9 @@
(is "?lhs = ?rhs")
proof
assume ?lhs
- then show ?rhs
- apply (rule_tac x="inv_into A f ` B" in exI)
- apply (auto simp: f_inv_into_f subset_iff image_inv_into_cancel inv_into_into)
- done
+ show ?rhs
+ by (rule exI [where x="inv_into A f ` B"])
+ (use \<open>?lhs\<close> in \<open>auto simp: f_inv_into_f subset_iff image_inv_into_cancel inv_into_into\<close>)
next
assume ?rhs
then show ?lhs by force
--- a/src/HOL/Library/FSet.thy Wed Aug 10 15:42:52 2016 +0200
+++ b/src/HOL/Library/FSet.thy Wed Aug 10 16:55:49 2016 +0200
@@ -528,7 +528,7 @@
using assms by transfer (metis Set.set_insert finite_insert)
lemma mk_disjoint_finsert: "a |\<in>| A \<Longrightarrow> \<exists>B. A = finsert a B \<and> a |\<notin>| B"
- by (rule_tac x = "A |-| {|a|}" in exI, blast)
+ by (rule exI [where x = "A |-| {|a|}"]) blast
subsubsection \<open>\<open>fimage\<close>\<close>
--- a/src/HOL/Library/IArray.thy Wed Aug 10 15:42:52 2016 +0200
+++ b/src/HOL/Library/IArray.thy Wed Aug 10 16:55:49 2016 +0200
@@ -71,15 +71,15 @@
lemma [code]:
"set_iarray as = set (IArray.list_of as)"
- by (case_tac as) auto
+ by (cases as) auto
lemma [code]:
"map_iarray f as = IArray (map f (IArray.list_of as))"
- by (case_tac as) auto
+ by (cases as) auto
lemma [code]:
"rel_iarray r as bs = list_all2 r (IArray.list_of as) (IArray.list_of bs)"
- by (case_tac as) (case_tac bs, auto)
+ by (cases as, cases bs) auto
lemma [code]:
"HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
--- a/src/HOL/Library/Indicator_Function.thy Wed Aug 10 15:42:52 2016 +0200
+++ b/src/HOL/Library/Indicator_Function.thy Wed Aug 10 16:55:49 2016 +0200
@@ -97,12 +97,12 @@
case True
then obtain i where "x \<in> A i"
by auto
- then have
+ then have *:
"\<And>n. (indicator (A (n + i)) x :: 'a) = 1"
"(indicator (\<Union>i. A i) x :: 'a) = 1"
using incseqD[OF \<open>incseq A\<close>, of i "n + i" for n] \<open>x \<in> A i\<close> by (auto simp: indicator_def)
- then show ?thesis
- by (rule_tac LIMSEQ_offset[of _ i]) simp
+ show ?thesis
+ by (rule LIMSEQ_offset[of _ i]) (use * in simp)
next
case False
then show ?thesis by (simp add: indicator_def)
@@ -125,12 +125,12 @@
case True
then obtain i where "x \<notin> A i"
by auto
- then have
+ then have *:
"\<And>n. (indicator (A (n + i)) x :: 'a) = 0"
"(indicator (\<Inter>i. A i) x :: 'a) = 0"
using decseqD[OF \<open>decseq A\<close>, of i "n + i" for n] \<open>x \<notin> A i\<close> by (auto simp: indicator_def)
- then show ?thesis
- by (rule_tac LIMSEQ_offset[of _ i]) simp
+ show ?thesis
+ by (rule LIMSEQ_offset[of _ i]) (use * in simp)
next
case False
then show ?thesis by (simp add: indicator_def)
--- a/src/HOL/Library/Permutation.thy Wed Aug 10 15:42:52 2016 +0200
+++ b/src/HOL/Library/Permutation.thy Wed Aug 10 16:55:49 2016 +0200
@@ -95,7 +95,7 @@
by auto
proposition cons_perm_imp_perm: "z # xs <~~> z # ys \<Longrightarrow> xs <~~> ys"
- by (drule_tac z = z in perm_remove_perm) auto
+ by (drule perm_remove_perm [where z = z]) auto
proposition cons_perm_eq [iff]: "z#xs <~~> z#ys \<longleftrightarrow> xs <~~> ys"
by (blast intro: cons_perm_imp_perm)
--- a/src/HOL/Library/Polynomial.thy Wed Aug 10 15:42:52 2016 +0200
+++ b/src/HOL/Library/Polynomial.thy Wed Aug 10 16:55:49 2016 +0200
@@ -1330,11 +1330,17 @@
lemma synthetic_div_eq_0_iff:
"synthetic_div p c = 0 \<longleftrightarrow> degree p = 0"
- by (induct p, simp, case_tac p, simp)
+proof (induct p)
+ case 0
+ then show ?case by simp
+next
+ case (pCons a p)
+ then show ?case by (cases p) simp
+qed
lemma degree_synthetic_div:
"degree (synthetic_div p c) = degree p - 1"
- by (induct p, simp, simp add: synthetic_div_eq_0_iff)
+ by (induct p) (simp_all add: synthetic_div_eq_0_iff)
lemma synthetic_div_correct:
"p + smult c (synthetic_div p c) = pCons (poly p c) (synthetic_div p c)"
@@ -3479,35 +3485,40 @@
qed (insert assms, auto)
lemma poly_pinfty_gt_lc:
- fixes p:: "real poly"
- assumes "lead_coeff p > 0"
- shows "\<exists> n. \<forall> x \<ge> n. poly p x \<ge> lead_coeff p" using assms
+ fixes p :: "real poly"
+ assumes "lead_coeff p > 0"
+ shows "\<exists> n. \<forall> x \<ge> n. poly p x \<ge> lead_coeff p"
+ using assms
proof (induct p)
case 0
- thus ?case by auto
+ then show ?case by auto
next
case (pCons a p)
- have "\<lbrakk>a\<noteq>0;p=0\<rbrakk> \<Longrightarrow> ?case" by auto
- moreover have "p\<noteq>0 \<Longrightarrow> ?case"
+ from this(1) consider "a \<noteq> 0" "p = 0" | "p \<noteq> 0" by auto
+ then show ?case
+ proof cases
+ case 1
+ then show ?thesis by auto
+ next
+ case 2
+ with pCons obtain n1 where gte_lcoeff: "\<forall>x\<ge>n1. lead_coeff p \<le> poly p x"
+ by auto
+ from pCons(3) \<open>p \<noteq> 0\<close> have gt_0: "lead_coeff p > 0" by auto
+ define n where "n = max n1 (1 + \<bar>a\<bar> / lead_coeff p)"
+ have "lead_coeff (pCons a p) \<le> poly (pCons a p) x" if "n \<le> x" for x
proof -
- assume "p\<noteq>0"
- then obtain n1 where gte_lcoeff:"\<forall>x\<ge>n1. lead_coeff p \<le> poly p x" using that pCons by auto
- have gt_0:"lead_coeff p >0" using pCons(3) \<open>p\<noteq>0\<close> by auto
- define n where "n = max n1 (1+ \<bar>a\<bar>/(lead_coeff p))"
- show ?thesis
- proof (rule_tac x=n in exI,rule,rule)
- fix x assume "n \<le> x"
- hence "lead_coeff p \<le> poly p x"
- using gte_lcoeff unfolding n_def by auto
- hence " \<bar>a\<bar>/(lead_coeff p) \<ge> \<bar>a\<bar>/(poly p x)" and "poly p x>0" using gt_0
- by (intro frac_le,auto)
- hence "x\<ge>1+ \<bar>a\<bar>/(poly p x)" using \<open>n\<le>x\<close>[unfolded n_def] by auto
- thus "lead_coeff (pCons a p) \<le> poly (pCons a p) x"
- using \<open>lead_coeff p \<le> poly p x\<close> \<open>poly p x>0\<close> \<open>p\<noteq>0\<close>
- by (auto simp add:field_simps)
- qed
+ from gte_lcoeff that have "lead_coeff p \<le> poly p x"
+ by (auto simp: n_def)
+ with gt_0 have "\<bar>a\<bar> / lead_coeff p \<ge> \<bar>a\<bar> / poly p x" and "poly p x > 0"
+ by (auto intro: frac_le)
+ with \<open>n\<le>x\<close>[unfolded n_def] have "x \<ge> 1 + \<bar>a\<bar> / poly p x"
+ by auto
+ with \<open>lead_coeff p \<le> poly p x\<close> \<open>poly p x > 0\<close> \<open>p \<noteq> 0\<close>
+ show "lead_coeff (pCons a p) \<le> poly (pCons a p) x"
+ by (auto simp: field_simps)
qed
- ultimately show ?case by fastforce
+ then show ?thesis by blast
+ qed
qed
@@ -3831,9 +3842,7 @@
"rsquarefree p = (p \<noteq> 0 & (\<forall>a. (order a p = 0) | (order a p = 1)))"
lemma pderiv_iszero: "pderiv p = 0 \<Longrightarrow> \<exists>h. p = [:h :: 'a :: {semidom,semiring_char_0}:]"
-apply (simp add: pderiv_eq_0_iff)
-apply (case_tac p, auto split: if_splits)
-done
+ by (cases p) (auto simp: pderiv_eq_0_iff split: if_splits)
lemma rsquarefree_roots:
fixes p :: "'a :: field_char_0 poly"
--- a/src/HOL/Library/Quotient_List.thy Wed Aug 10 15:42:52 2016 +0200
+++ b/src/HOL/Library/Quotient_List.thy Wed Aug 10 16:55:49 2016 +0200
@@ -145,7 +145,6 @@
shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"
by (simp add: fun_eq_iff foldl_prs_aux [OF a b])
-(* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *)
lemma foldl_rsp[quot_respect]:
assumes q1: "Quotient3 R1 Abs1 Rep1"
and q2: "Quotient3 R2 Abs2 Rep2"
--- a/src/HOL/Library/RBT_Impl.thy Wed Aug 10 15:42:52 2016 +0200
+++ b/src/HOL/Library/RBT_Impl.thy Wed Aug 10 16:55:49 2016 +0200
@@ -531,23 +531,18 @@
by (simp add: rbt_insertwk_is_rbt rbt_insertw_def)
lemma rbt_lookup_rbt_insertw:
- assumes "is_rbt t"
- 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))"
-using assms
-unfolding rbt_insertw_def
-by (rule_tac ext) (cases "rbt_lookup t k", auto simp:rbt_lookup_rbt_insertwk dom_def)
+ "is_rbt t \<Longrightarrow>
+ rbt_lookup (rbt_insert_with f k v t) =
+ (rbt_lookup t)(k \<mapsto> (if k \<in> dom (rbt_lookup t) then f (the (rbt_lookup t k)) v else v))"
+ by (rule ext, cases "rbt_lookup t k") (auto simp: rbt_lookup_rbt_insertwk dom_def rbt_insertw_def)
lemma rbt_insert_rbt_sorted: "rbt_sorted t \<Longrightarrow> rbt_sorted (rbt_insert k v t)"
by (simp add: rbt_insertwk_rbt_sorted rbt_insert_def)
theorem rbt_insert_is_rbt [simp]: "is_rbt t \<Longrightarrow> is_rbt (rbt_insert k v t)"
by (simp add: rbt_insertwk_is_rbt rbt_insert_def)
-lemma rbt_lookup_rbt_insert:
- assumes "is_rbt t"
- shows "rbt_lookup (rbt_insert k v t) = (rbt_lookup t)(k\<mapsto>v)"
-unfolding rbt_insert_def
-using assms
-by (rule_tac ext) (simp add: rbt_lookup_rbt_insertwk split:option.split)
+lemma rbt_lookup_rbt_insert: "is_rbt t \<Longrightarrow> rbt_lookup (rbt_insert k v t) = (rbt_lookup t)(k\<mapsto>v)"
+ by (rule ext) (simp add: rbt_insert_def rbt_lookup_rbt_insertwk split: option.split)
end
--- a/src/HOL/Library/RBT_Mapping.thy Wed Aug 10 15:42:52 2016 +0200
+++ b/src/HOL/Library/RBT_Mapping.thy Wed Aug 10 16:55:49 2016 +0200
@@ -43,7 +43,10 @@
lemma map_entry_Mapping [code]:
"Mapping.map_entry k f (Mapping t) = Mapping (RBT.map_entry k f t)"
- apply (transfer fixing: t) by (case_tac "RBT.lookup t k") auto
+ apply (transfer fixing: t)
+ apply (case_tac "RBT.lookup t k")
+ apply auto
+ done
lemma keys_Mapping [code]:
"Mapping.keys (Mapping t) = set (RBT.keys t)"
--- a/src/HOL/Library/RBT_Set.thy Wed Aug 10 15:42:52 2016 +0200
+++ b/src/HOL/Library/RBT_Set.thy Wed Aug 10 16:55:49 2016 +0200
@@ -273,12 +273,14 @@
assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t1 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
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)"
shows "P t"
-using assms
- apply (induction t)
- apply simp
- apply (case_tac "t1 = rbt.Empty")
- apply simp_all
-done
+ using assms
+proof (induct t)
+ case Empty
+ then show ?case by simp
+next
+ case (Branch x1 t1 x3 x4 t2)
+ then show ?case by (cases "t1 = rbt.Empty") simp_all
+qed
lemma rbt_min_opt_in_set:
fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
@@ -372,12 +374,14 @@
assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t2 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
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)"
shows "P t"
-using assms
- apply (induction t)
- apply simp
- apply (case_tac "t2 = rbt.Empty")
- apply simp_all
-done
+ using assms
+proof (induct t)
+ case Empty
+ then show ?case by simp
+next
+ case (Branch x1 t1 x3 x4 t2)
+ then show ?case by (cases "t2 = rbt.Empty") simp_all
+qed
lemma rbt_max_opt_in_set:
fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
@@ -468,27 +472,26 @@
using assms unfolding is_empty_empty by transfer (auto intro: rbt_min_eq_rbt_min_opt)
lemma fold_keys_min_top_eq:
- fixes t :: "('a :: {linorder, bounded_lattice_top}, unit) rbt"
+ fixes t :: "('a::{linorder,bounded_lattice_top}, unit) rbt"
assumes "\<not> (RBT.is_empty t)"
shows "fold_keys min t top = fold1_keys min t"
proof -
have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold min (RBT_Impl.keys t) top =
- List.fold min (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) top"
+ List.fold min (hd (RBT_Impl.keys t) # tl (RBT_Impl.keys t)) top"
by (simp add: hd_Cons_tl[symmetric])
- { fix x :: "_ :: {linorder, bounded_lattice_top}" and xs
- have "List.fold min (x#xs) top = List.fold min xs x"
+ have **: "List.fold min (x # xs) top = List.fold min xs x" for x :: 'a and xs
by (simp add: inf_min[symmetric])
- } note ** = this
- show ?thesis using assms
+ show ?thesis
+ using assms
unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
apply transfer
apply (case_tac t)
- apply simp
+ apply simp
apply (subst *)
- apply simp
+ apply simp
apply (subst **)
apply simp
- done
+ done
qed
(* maximum *)
@@ -506,27 +509,26 @@
using assms unfolding is_empty_empty by transfer (auto intro: rbt_max_eq_rbt_max_opt)
lemma fold_keys_max_bot_eq:
- fixes t :: "('a :: {linorder, bounded_lattice_bot}, unit) rbt"
+ fixes t :: "('a::{linorder,bounded_lattice_bot}, unit) rbt"
assumes "\<not> (RBT.is_empty t)"
shows "fold_keys max t bot = fold1_keys max t"
proof -
have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold max (RBT_Impl.keys t) bot =
- List.fold max (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) bot"
+ List.fold max (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) bot"
by (simp add: hd_Cons_tl[symmetric])
- { fix x :: "_ :: {linorder, bounded_lattice_bot}" and xs
- have "List.fold max (x#xs) bot = List.fold max xs x"
+ have **: "List.fold max (x # xs) bot = List.fold max xs x" for x :: 'a and xs
by (simp add: sup_max[symmetric])
- } note ** = this
- show ?thesis using assms
+ show ?thesis
+ using assms
unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
apply transfer
apply (case_tac t)
- apply simp
+ apply simp
apply (subst *)
- apply simp
+ apply simp
apply (subst **)
apply simp
- done
+ done
qed
end
--- a/src/HOL/Library/Stream.thy Wed Aug 10 15:42:52 2016 +0200
+++ b/src/HOL/Library/Stream.thy Wed Aug 10 16:55:49 2016 +0200
@@ -393,7 +393,7 @@
then show "s = sconst x"
proof (coinduction arbitrary: s)
case Eq_stream
- then have "shd s = x" "sset (stl s) \<subseteq> {x}" by (case_tac [!] s) auto
+ then have "shd s = x" "sset (stl s) \<subseteq> {x}" by (cases s; auto)+
then have "sset (stl s) = {x}" by (cases "stl s") auto
with \<open>shd s = x\<close> show ?case by auto
qed
--- a/src/HOL/Library/Sublist.thy Wed Aug 10 15:42:52 2016 +0200
+++ b/src/HOL/Library/Sublist.thy Wed Aug 10 16:55:49 2016 +0200
@@ -156,10 +156,13 @@
by (simp_all add: strict_prefix_def cong: conj_cong)
lemma take_strict_prefix: "strict_prefix xs ys \<Longrightarrow> strict_prefix (take n xs) ys"
- apply (induct n arbitrary: xs ys)
- apply (case_tac ys; simp)
- apply (metis prefix_order.less_trans strict_prefixI take_is_prefix)
- done
+proof (induct n arbitrary: xs ys)
+ case 0
+ then show ?case by (cases ys) simp_all
+next
+ case (Suc n)
+ then show ?case by (metis prefix_order.less_trans strict_prefixI take_is_prefix)
+qed
lemma not_prefix_cases:
assumes pfx: "\<not> prefix ps ls"
@@ -197,7 +200,8 @@
and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> prefix xs ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)"
shows "P ps ls" using np
proof (induct ls arbitrary: ps)
- case Nil then show ?case
+ case Nil
+ then show ?case
by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base)
next
case (Cons y ys)
@@ -215,7 +219,13 @@
"prefixes (x#xs) = [] # map (op # x) (prefixes xs)"
lemma in_set_prefixes[simp]: "xs \<in> set (prefixes ys) \<longleftrightarrow> prefix xs ys"
-by (induction "xs" arbitrary: "ys"; rename_tac "ys", case_tac "ys"; auto)
+proof (induct xs arbitrary: ys)
+ case Nil
+ then show ?case by (cases ys) auto
+next
+ case (Cons a xs)
+ then show ?case by (cases ys) auto
+qed
lemma length_prefixes[simp]: "length (prefixes xs) = length xs+1"
by (induction xs) auto