explicit theory with additional, less commonly used list operations
authorhaftmann
Sun Sep 07 09:49:05 2014 +0200 (2014-09-07)
changeset 581995fbe474b5da8
parent 58198 099ca49b5231
child 58200 d95055489fce
explicit theory with additional, less commonly used list operations
src/HOL/Library/Library.thy
src/HOL/Library/More_List.thy
src/HOL/Library/Poly_Deriv.thy
src/HOL/Library/Polynomial.thy
     1.1 --- a/src/HOL/Library/Library.thy	Sun Sep 07 09:49:01 2014 +0200
     1.2 +++ b/src/HOL/Library/Library.thy	Sun Sep 07 09:49:05 2014 +0200
     1.3 @@ -39,6 +39,7 @@
     1.4    Lubs_Glbs
     1.5    Mapping
     1.6    Monad_Syntax
     1.7 +  More_List
     1.8    Multiset
     1.9    Numeral_Type
    1.10    NthRoot_Limits
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/More_List.thy	Sun Sep 07 09:49:05 2014 +0200
     2.3 @@ -0,0 +1,155 @@
     2.4 +(* Author: Andreas Lochbihler, ETH Z├╝rich
     2.5 +   Author: Florian Haftmann, TU Muenchen  *)
     2.6 +
     2.7 +header \<open>Less common functions on lists\<close>
     2.8 +
     2.9 +theory More_List
    2.10 +imports Main
    2.11 +begin
    2.12 +
    2.13 +text \<open>FIXME adapted from @{file "~~/src/HOL/Library/Polynomial.thy"}; to be merged back\<close>
    2.14 +
    2.15 +definition strip_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
    2.16 +where
    2.17 +  "strip_while P = rev \<circ> dropWhile P \<circ> rev"
    2.18 +
    2.19 +lemma strip_while_Nil [simp]:
    2.20 +  "strip_while P [] = []"
    2.21 +  by (simp add: strip_while_def)
    2.22 +
    2.23 +lemma strip_while_append [simp]:
    2.24 +  "\<not> P x \<Longrightarrow> strip_while P (xs @ [x]) = xs @ [x]"
    2.25 +  by (simp add: strip_while_def)
    2.26 +
    2.27 +lemma strip_while_append_rec [simp]:
    2.28 +  "P x \<Longrightarrow> strip_while P (xs @ [x]) = strip_while P xs"
    2.29 +  by (simp add: strip_while_def)
    2.30 +
    2.31 +lemma strip_while_Cons [simp]:
    2.32 +  "\<not> P x \<Longrightarrow> strip_while P (x # xs) = x # strip_while P xs"
    2.33 +  by (induct xs rule: rev_induct) (simp_all add: strip_while_def)
    2.34 +
    2.35 +lemma strip_while_eq_Nil [simp]:
    2.36 +  "strip_while P xs = [] \<longleftrightarrow> (\<forall>x\<in>set xs. P x)"
    2.37 +  by (simp add: strip_while_def)
    2.38 +
    2.39 +lemma strip_while_eq_Cons_rec:
    2.40 +  "strip_while P (x # xs) = x # strip_while P xs \<longleftrightarrow> \<not> (P x \<and> (\<forall>x\<in>set xs. P x))"
    2.41 +  by (induct xs rule: rev_induct) (simp_all add: strip_while_def)
    2.42 +
    2.43 +lemma strip_while_not_last [simp]:
    2.44 +  "\<not> P (last xs) \<Longrightarrow> strip_while P xs = xs"
    2.45 +  by (cases xs rule: rev_cases) simp_all
    2.46 +
    2.47 +lemma split_strip_while_append:
    2.48 +  fixes xs :: "'a list"
    2.49 +  obtains ys zs :: "'a list"
    2.50 +  where "strip_while P xs = ys" and "\<forall>x\<in>set zs. P x" and "xs = ys @ zs"
    2.51 +proof (rule that)
    2.52 +  show "strip_while P xs = strip_while P xs" ..
    2.53 +  show "\<forall>x\<in>set (rev (takeWhile P (rev xs))). P x" by (simp add: takeWhile_eq_all_conv [symmetric])
    2.54 +  have "rev xs = rev (strip_while P xs @ rev (takeWhile P (rev xs)))"
    2.55 +    by (simp add: strip_while_def)
    2.56 +  then show "xs = strip_while P xs @ rev (takeWhile P (rev xs))"
    2.57 +    by (simp only: rev_is_rev_conv)
    2.58 +qed
    2.59 +
    2.60 +lemma strip_while_snoc [simp]:
    2.61 +  "strip_while P (xs @ [x]) = (if P x then strip_while P xs else xs @ [x])"
    2.62 +  by (simp add: strip_while_def)
    2.63 +
    2.64 +lemma strip_while_map:
    2.65 +  "strip_while P (map f xs) = map f (strip_while (P \<circ> f) xs)"
    2.66 +  by (simp add: strip_while_def rev_map dropWhile_map)
    2.67 +
    2.68 +lemma dropWhile_idI:
    2.69 +  "(xs \<noteq> [] \<Longrightarrow> \<not> P (hd xs)) \<Longrightarrow> dropWhile P xs = xs"
    2.70 +  by (metis dropWhile.simps(1) dropWhile.simps(2) list.collapse)
    2.71 +
    2.72 +lemma strip_while_idI:
    2.73 +  "(xs \<noteq> [] \<Longrightarrow> \<not> P (last xs)) \<Longrightarrow> strip_while P xs = xs"
    2.74 +  using dropWhile_idI [of "rev xs"] by (simp add: strip_while_def hd_rev)
    2.75 +
    2.76 +
    2.77 +definition nth_default :: "'a \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a"
    2.78 +where
    2.79 +  "nth_default x xs n = (if n < length xs then xs ! n else x)"
    2.80 +
    2.81 +lemma nth_default_Nil [simp]:
    2.82 +  "nth_default y [] n = y"
    2.83 +  by (simp add: nth_default_def)
    2.84 +
    2.85 +lemma nth_default_Cons_0 [simp]:
    2.86 +  "nth_default y (x # xs) 0 = x"
    2.87 +  by (simp add: nth_default_def)
    2.88 +
    2.89 +lemma nth_default_Cons_Suc [simp]:
    2.90 +  "nth_default y (x # xs) (Suc n) = nth_default y xs n"
    2.91 +  by (simp add: nth_default_def)
    2.92 +
    2.93 +lemma nth_default_map_eq:
    2.94 +  "f y = x \<Longrightarrow> nth_default x (map f xs) n = f (nth_default y xs n)"
    2.95 +  by (simp add: nth_default_def)
    2.96 +
    2.97 +lemma nth_default_strip_while_eq [simp]:
    2.98 +  "nth_default x (strip_while (HOL.eq x) xs) n = nth_default x xs n"
    2.99 +proof -
   2.100 +  from split_strip_while_append obtain ys zs
   2.101 +    where "strip_while (HOL.eq x) xs = ys" and "\<forall>z\<in>set zs. x = z" and "xs = ys @ zs" by blast
   2.102 +  then show ?thesis by (simp add: nth_default_def not_less nth_append)
   2.103 +qed
   2.104 +
   2.105 +lemma nth_default_Cons:
   2.106 +  "nth_default y (x # xs) n = (case n of 0 \<Rightarrow> x | Suc n' \<Rightarrow> nth_default y xs n')"
   2.107 +  by (simp split: nat.split)
   2.108 +
   2.109 +lemma nth_default_nth:
   2.110 +  "n < length xs \<Longrightarrow> nth_default y xs n = xs ! n"
   2.111 +  by (simp add: nth_default_def)
   2.112 +
   2.113 +lemma nth_default_beyond:
   2.114 +  "length xs \<le> n \<Longrightarrow> nth_default y xs n = y"
   2.115 +  by (simp add: nth_default_def)
   2.116 +
   2.117 +lemma range_nth_default [simp]:
   2.118 +  "range (nth_default dflt xs) = insert dflt (set xs)"
   2.119 +  by (auto simp add: nth_default_def[abs_def] in_set_conv_nth)
   2.120 +
   2.121 +lemma nth_strip_while:
   2.122 +  assumes "n < length (strip_while P xs)"
   2.123 +  shows "strip_while P xs ! n = xs ! n"
   2.124 +proof -
   2.125 +  have "length (dropWhile P (rev xs)) + length (takeWhile P (rev xs)) = length xs"
   2.126 +    by (subst add.commute)
   2.127 +      (simp add: arg_cong [where f=length, OF takeWhile_dropWhile_id, unfolded length_append])
   2.128 +  then show ?thesis using assms
   2.129 +    by (simp add: strip_while_def rev_nth dropWhile_nth)
   2.130 +qed
   2.131 +
   2.132 +lemma length_strip_while_le:
   2.133 +  "length (strip_while P xs) \<le> length xs"
   2.134 +  unfolding strip_while_def o_def length_rev
   2.135 +  by (subst (2) length_rev[symmetric])
   2.136 +    (simp add: strip_while_def length_dropWhile_le del: length_rev)
   2.137 +
   2.138 +lemma finite_nth_default_neq_default [simp]:
   2.139 +  "finite {k. nth_default dflt xs k \<noteq> dflt}"
   2.140 +  by (simp add: nth_default_def)
   2.141 +
   2.142 +lemma sorted_list_of_set_nth_default:
   2.143 +  "sorted_list_of_set {k. nth_default dflt xs k \<noteq> dflt} = map fst (filter (\<lambda>(_, x). x \<noteq> dflt) (zip [0..<length xs] xs))"
   2.144 +  by (rule sorted_distinct_set_unique) (auto simp add: nth_default_def in_set_conv_nth sorted_filter distinct_map_filter intro: rev_image_eqI)
   2.145 +
   2.146 +lemma nth_default_snoc_default [simp]:
   2.147 +  "nth_default dflt (xs @ [dflt]) = nth_default dflt xs"
   2.148 +  by (auto simp add: nth_default_def fun_eq_iff nth_append)
   2.149 +
   2.150 +lemma nth_default_strip_while_dflt [simp]:
   2.151 + "nth_default dflt (strip_while (op = dflt) xs) = nth_default dflt xs"
   2.152 +  by (induct xs rule: rev_induct) auto
   2.153 +
   2.154 +lemma nth_default_eq_dflt_iff:
   2.155 +  "nth_default dflt xs k = dflt \<longleftrightarrow> (k < length xs \<longrightarrow> xs ! k = dflt)"
   2.156 +  by (simp add: nth_default_def)
   2.157 +
   2.158 +end
     3.1 --- a/src/HOL/Library/Poly_Deriv.thy	Sun Sep 07 09:49:01 2014 +0200
     3.2 +++ b/src/HOL/Library/Poly_Deriv.thy	Sun Sep 07 09:49:05 2014 +0200
     3.3 @@ -130,8 +130,13 @@
     3.4    shows "n = order a p"
     3.5  unfolding Polynomial.order_def
     3.6  apply (rule Least_equality [symmetric])
     3.7 -apply (rule assms)
     3.8 -by (metis assms not_less_eq_eq power_le_dvd)
     3.9 +apply (fact assms)
    3.10 +apply (rule classical)
    3.11 +apply (erule notE)
    3.12 +unfolding not_less_eq_eq
    3.13 +using assms(1) apply (rule power_le_dvd)
    3.14 +apply assumption
    3.15 +done
    3.16  
    3.17  lemma lemma_order_pderiv1:
    3.18    "pderiv ([:- a, 1:] ^ Suc n * q) = [:- a, 1:] ^ Suc n * pderiv q +
     4.1 --- a/src/HOL/Library/Polynomial.thy	Sun Sep 07 09:49:01 2014 +0200
     4.2 +++ b/src/HOL/Library/Polynomial.thy	Sun Sep 07 09:49:05 2014 +0200
     4.3 @@ -7,86 +7,11 @@
     4.4  header {* Polynomials as type over a ring structure *}
     4.5  
     4.6  theory Polynomial
     4.7 -imports Main GCD
     4.8 +imports Main GCD "~~/src/HOL/Library/More_List"
     4.9  begin
    4.10  
    4.11  subsection {* Auxiliary: operations for lists (later) representing coefficients *}
    4.12  
    4.13 -definition strip_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
    4.14 -where
    4.15 -  "strip_while P = rev \<circ> dropWhile P \<circ> rev"
    4.16 -
    4.17 -lemma strip_while_Nil [simp]:
    4.18 -  "strip_while P [] = []"
    4.19 -  by (simp add: strip_while_def)
    4.20 -
    4.21 -lemma strip_while_append [simp]:
    4.22 -  "\<not> P x \<Longrightarrow> strip_while P (xs @ [x]) = xs @ [x]"
    4.23 -  by (simp add: strip_while_def)
    4.24 -
    4.25 -lemma strip_while_append_rec [simp]:
    4.26 -  "P x \<Longrightarrow> strip_while P (xs @ [x]) = strip_while P xs"
    4.27 -  by (simp add: strip_while_def)
    4.28 -
    4.29 -lemma strip_while_Cons [simp]:
    4.30 -  "\<not> P x \<Longrightarrow> strip_while P (x # xs) = x # strip_while P xs"
    4.31 -  by (induct xs rule: rev_induct) (simp_all add: strip_while_def)
    4.32 -
    4.33 -lemma strip_while_eq_Nil [simp]:
    4.34 -  "strip_while P xs = [] \<longleftrightarrow> (\<forall>x\<in>set xs. P x)"
    4.35 -  by (simp add: strip_while_def)
    4.36 -
    4.37 -lemma strip_while_eq_Cons_rec:
    4.38 -  "strip_while P (x # xs) = x # strip_while P xs \<longleftrightarrow> \<not> (P x \<and> (\<forall>x\<in>set xs. P x))"
    4.39 -  by (induct xs rule: rev_induct) (simp_all add: strip_while_def)
    4.40 -
    4.41 -lemma strip_while_not_last [simp]:
    4.42 -  "\<not> P (last xs) \<Longrightarrow> strip_while P xs = xs"
    4.43 -  by (cases xs rule: rev_cases) simp_all
    4.44 -
    4.45 -lemma split_strip_while_append:
    4.46 -  fixes xs :: "'a list"
    4.47 -  obtains ys zs :: "'a list"
    4.48 -  where "strip_while P xs = ys" and "\<forall>x\<in>set zs. P x" and "xs = ys @ zs"
    4.49 -proof (rule that)
    4.50 -  show "strip_while P xs = strip_while P xs" ..
    4.51 -  show "\<forall>x\<in>set (rev (takeWhile P (rev xs))). P x" by (simp add: takeWhile_eq_all_conv [symmetric])
    4.52 -  have "rev xs = rev (strip_while P xs @ rev (takeWhile P (rev xs)))"
    4.53 -    by (simp add: strip_while_def)
    4.54 -  then show "xs = strip_while P xs @ rev (takeWhile P (rev xs))"
    4.55 -    by (simp only: rev_is_rev_conv)
    4.56 -qed
    4.57 -
    4.58 -
    4.59 -definition nth_default :: "'a \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a"
    4.60 -where
    4.61 -  "nth_default x xs n = (if n < length xs then xs ! n else x)"
    4.62 -
    4.63 -lemma nth_default_Nil [simp]:
    4.64 -  "nth_default y [] n = y"
    4.65 -  by (simp add: nth_default_def)
    4.66 -
    4.67 -lemma nth_default_Cons_0 [simp]:
    4.68 -  "nth_default y (x # xs) 0 = x"
    4.69 -  by (simp add: nth_default_def)
    4.70 -
    4.71 -lemma nth_default_Cons_Suc [simp]:
    4.72 -  "nth_default y (x # xs) (Suc n) = nth_default y xs n"
    4.73 -  by (simp add: nth_default_def)
    4.74 -
    4.75 -lemma nth_default_map_eq:
    4.76 -  "f y = x \<Longrightarrow> nth_default x (map f xs) n = f (nth_default y xs n)"
    4.77 -  by (simp add: nth_default_def)
    4.78 -
    4.79 -lemma nth_default_strip_while_eq [simp]:
    4.80 -  "nth_default x (strip_while (HOL.eq x) xs) n = nth_default x xs n"
    4.81 -proof -
    4.82 -  from split_strip_while_append obtain ys zs
    4.83 -    where "strip_while (HOL.eq x) xs = ys" and "\<forall>z\<in>set zs. x = z" and "xs = ys @ zs" by blast
    4.84 -  then show ?thesis by (simp add: nth_default_def not_less nth_append)
    4.85 -qed
    4.86 -
    4.87 -
    4.88  definition cCons :: "'a::zero \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixr "##" 65)
    4.89  where
    4.90    "x ## xs = (if xs = [] \<and> x = 0 then [] else x # xs)"
    4.91 @@ -406,7 +331,8 @@
    4.92    { fix ms :: "nat list" and f :: "nat \<Rightarrow> 'a" and x :: "'a"
    4.93      assume "\<forall>m\<in>set ms. m > 0"
    4.94      then have "map (case_nat x f) ms = map f (map (\<lambda>n. n - 1) ms)"
    4.95 -      by (induct ms) (auto, metis Suc_pred' nat.case(2)) }
    4.96 +      by (induct ms) (auto split: nat.split)
    4.97 +  }
    4.98    note * = this
    4.99    show ?thesis
   4.100      by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt One_nat_def del: upt_Suc)