added lemmas
authornipkow
Wed Dec 13 09:04:43 2017 +0100 (17 months ago)
changeset 67168bea1258d9a27
parent 67167 88d1c9d86f48
child 67169 1fabca1c2199
added lemmas
src/HOL/Data_Structures/List_Ins_Del.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/Data_Structures/List_Ins_Del.thy	Tue Dec 12 10:01:14 2017 +0100
     1.2 +++ b/src/HOL/Data_Structures/List_Ins_Del.thy	Wed Dec 13 09:04:43 2017 +0100
     1.3 @@ -53,12 +53,12 @@
     1.4  by(induction xs) auto
     1.5  
     1.6  lemma distinct_if_sorted: "sorted xs \<Longrightarrow> distinct xs"
     1.7 -apply(induction xs rule: sorted_wrt_induct)
     1.8 +apply(induction xs rule: induct_list012)
     1.9  apply auto
    1.10  by (metis in_set_conv_decomp_first less_imp_not_less sorted_mid_iff2)
    1.11  
    1.12  lemma sorted_ins_list: "sorted xs \<Longrightarrow> sorted(ins_list x xs)"
    1.13 -by(induction xs rule: sorted_wrt_induct) auto
    1.14 +by(induction xs rule: induct_list012) auto
    1.15  
    1.16  lemma ins_list_sorted: "sorted (xs @ [a]) \<Longrightarrow>
    1.17    ins_list x (xs @ a # ys) =
    1.18 @@ -105,7 +105,7 @@
    1.19  done
    1.20  
    1.21  lemma sorted_del_list: "sorted xs \<Longrightarrow> sorted(del_list x xs)"
    1.22 -apply(induction xs rule: sorted_wrt_induct)
    1.23 +apply(induction xs rule: induct_list012)
    1.24  apply auto
    1.25  by (meson order.strict_trans sorted_Cons_iff)
    1.26  
     2.1 --- a/src/HOL/List.thy	Tue Dec 12 10:01:14 2017 +0100
     2.2 +++ b/src/HOL/List.thy	Wed Dec 13 09:04:43 2017 +0100
     2.3 @@ -793,28 +793,13 @@
     2.4    "(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs"
     2.5  by (fact measure_induct)
     2.6  
     2.7 +lemma induct_list012:
     2.8 +  "\<lbrakk>P []; \<And>x. P [x]; \<And>x y zs. P (y # zs) \<Longrightarrow> P (x # y # zs)\<rbrakk> \<Longrightarrow> P xs"
     2.9 +by induction_schema (pat_completeness, lexicographic_order)
    2.10 +
    2.11  lemma list_nonempty_induct [consumes 1, case_names single cons]:
    2.12 -  assumes "xs \<noteq> []"
    2.13 -  assumes single: "\<And>x. P [x]"
    2.14 -  assumes cons: "\<And>x xs. xs \<noteq> [] \<Longrightarrow> P xs \<Longrightarrow> P (x # xs)"
    2.15 -  shows "P xs"
    2.16 -using \<open>xs \<noteq> []\<close> proof (induct xs)
    2.17 -  case Nil then show ?case by simp
    2.18 -next
    2.19 -  case (Cons x xs)
    2.20 -  show ?case
    2.21 -  proof (cases xs)
    2.22 -    case Nil
    2.23 -    with single show ?thesis by simp
    2.24 -  next
    2.25 -    case Cons
    2.26 -    show ?thesis
    2.27 -    proof (rule cons)
    2.28 -      from Cons show "xs \<noteq> []" by simp
    2.29 -      with Cons.hyps show "P xs" .
    2.30 -    qed
    2.31 -  qed
    2.32 -qed
    2.33 +  "\<lbrakk> xs \<noteq> []; \<And>x. P [x]; \<And>x xs. xs \<noteq> [] \<Longrightarrow> P xs \<Longrightarrow> P (x # xs)\<rbrakk> \<Longrightarrow> P xs"
    2.34 +by(induction xs rule: induct_list012) auto
    2.35  
    2.36  lemma inj_split_Cons: "inj_on (\<lambda>(xs, n). n#xs) X"
    2.37    by (auto intro!: inj_onI)
    2.38 @@ -1986,7 +1971,7 @@
    2.39  by(induct xs)(auto simp:neq_Nil_conv)
    2.40  
    2.41  lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
    2.42 -by (induct xs, simp, case_tac xs, simp_all)
    2.43 +by (induction xs rule: induct_list012) simp_all
    2.44  
    2.45  lemma last_list_update:
    2.46    "xs \<noteq> [] \<Longrightarrow> last(xs[k:=x]) = (if k = size xs - 1 then x else last xs)"
    2.47 @@ -2430,11 +2415,7 @@
    2.48  
    2.49  lemma takeWhile_not_last:
    2.50    "distinct xs \<Longrightarrow> takeWhile (\<lambda>y. y \<noteq> last xs) xs = butlast xs"
    2.51 -apply(induct xs)
    2.52 - apply simp
    2.53 -apply(case_tac xs)
    2.54 -apply(auto)
    2.55 -done
    2.56 +by(induction xs rule: induct_list012) auto
    2.57  
    2.58  lemma takeWhile_cong [fundef_cong]:
    2.59    "[| l = k; !!x. x : set l ==> P x = Q x |]
    2.60 @@ -3229,6 +3210,9 @@
    2.61  lemma upto_Nil[simp]: "[i..j] = [] \<longleftrightarrow> j < i"
    2.62  by (simp add: upto.simps)
    2.63  
    2.64 +lemma upto_Nil2[simp]: "[] = [i..j] \<longleftrightarrow> j < i"
    2.65 +by (simp add: upto.simps)
    2.66 +
    2.67  lemma upto_rec1: "i \<le> j \<Longrightarrow> [i..j] = i#[i+1..j]"
    2.68  by(simp add: upto.simps)
    2.69  
    2.70 @@ -4910,10 +4894,6 @@
    2.71  
    2.72  subsubsection \<open>@{const sorted_wrt}\<close>
    2.73  
    2.74 -lemma sorted_wrt_induct:
    2.75 -  "\<lbrakk>P []; \<And>x. P [x]; \<And>x y zs. P (y # zs) \<Longrightarrow> P (x # y # zs)\<rbrakk> \<Longrightarrow> P xs"
    2.76 -by induction_schema (pat_completeness, lexicographic_order)
    2.77 -
    2.78  lemma sorted_wrt_Cons:
    2.79  assumes "transp P"
    2.80  shows   "sorted_wrt P (x # xs) = ((\<forall>y \<in> set xs. P x y) \<and> sorted_wrt P xs)"
    2.81 @@ -4921,7 +4901,7 @@
    2.82  
    2.83  lemma sorted_wrt_ConsI:
    2.84    "\<lbrakk> \<And>y. y \<in> set xs \<Longrightarrow> P x y; sorted_wrt P xs \<rbrakk> \<Longrightarrow> sorted_wrt P (x # xs)"
    2.85 -by (induction xs rule: sorted_wrt_induct) simp_all
    2.86 +by (induction xs rule: induct_list012) simp_all
    2.87  
    2.88  lemma sorted_wrt_append:
    2.89  assumes "transp P"
    2.90 @@ -4931,15 +4911,15 @@
    2.91  
    2.92  lemma sorted_wrt_backwards:
    2.93    "sorted_wrt P (xs @ [y, z]) = (P y z \<and> sorted_wrt P (xs @ [y]))"
    2.94 -by (induction xs rule: sorted_wrt_induct) auto
    2.95 +by (induction xs rule: induct_list012) auto
    2.96  
    2.97  lemma sorted_wrt_rev:
    2.98    "sorted_wrt P (rev xs) = sorted_wrt (\<lambda>x y. P y x) xs"
    2.99 -by (induction xs rule: sorted_wrt_induct) (simp_all add: sorted_wrt_backwards)
   2.100 +by (induction xs rule: induct_list012) (simp_all add: sorted_wrt_backwards)
   2.101  
   2.102  lemma sorted_wrt_mono:
   2.103    "(\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> sorted_wrt P xs \<Longrightarrow> sorted_wrt Q xs"
   2.104 -by(induction xs rule: sorted_wrt_induct)(auto)
   2.105 +by(induction xs rule: induct_list012)(auto)
   2.106  
   2.107  text \<open>Strictly Ascending Sequences of Natural Numbers\<close>
   2.108  
   2.109 @@ -4976,7 +4956,7 @@
   2.110    proof (induct xs rule: sorted.induct)
   2.111      case (Cons xs x) thus ?case by (cases xs) simp_all
   2.112    qed simp
   2.113 -qed (induct xs rule: sorted_wrt_induct, simp_all)
   2.114 +qed (induct xs rule: induct_list012, simp_all)
   2.115  
   2.116  lemma sorted_tl:
   2.117    "sorted xs \<Longrightarrow> sorted (tl xs)"