--- a/src/HOL/Library/More_List.thy Wed Apr 05 22:25:18 2017 +0200
+++ b/src/HOL/Library/More_List.thy Wed Apr 05 22:29:09 2017 +0200
@@ -39,10 +39,6 @@
"strip_while P (x # xs) = x # strip_while P xs \<longleftrightarrow> \<not> (P x \<and> (\<forall>x\<in>set xs. P x))"
by (induct xs rule: rev_induct) (simp_all add: strip_while_def)
-lemma strip_while_not_last [simp]:
- "\<not> P (last xs) \<Longrightarrow> strip_while P xs = xs"
- by (cases xs rule: rev_cases) simp_all
-
lemma split_strip_while_append:
fixes xs :: "'a list"
obtains ys zs :: "'a list"
@@ -64,6 +60,32 @@
"strip_while P (map f xs) = map f (strip_while (P \<circ> f) xs)"
by (simp add: strip_while_def rev_map dropWhile_map)
+lemma strip_while_dropWhile_commute:
+ "strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs)"
+proof (induct xs)
+ case Nil
+ then show ?case
+ by simp
+next
+ case (Cons x xs)
+ show ?case
+ proof (cases "\<forall>y\<in>set xs. P y")
+ case True
+ with dropWhile_append2 [of "rev xs"] show ?thesis
+ by (auto simp add: strip_while_def dest: set_dropWhileD)
+ next
+ case False
+ then obtain y where "y \<in> set xs" and "\<not> P y"
+ by blast
+ with Cons dropWhile_append3 [of P y "rev xs"] show ?thesis
+ by (simp add: strip_while_def)
+ qed
+qed
+
+lemma dropWhile_strip_while_commute:
+ "dropWhile P (strip_while Q xs) = strip_while Q (dropWhile P xs)"
+ by (simp add: strip_while_dropWhile_commute)
+
definition no_leading :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
where
@@ -134,6 +156,10 @@
"no_trailing P (x # xs) \<longleftrightarrow> no_trailing P xs \<and> (xs = [] \<longrightarrow> \<not> P x)"
by simp
+lemma no_trailing_append:
+ "no_trailing P (xs @ ys) \<longleftrightarrow> no_trailing P ys \<and> (ys = [] \<longrightarrow> no_trailing P xs)"
+ by (induct xs) simp_all
+
lemma no_trailing_append_Cons [simp]:
"no_trailing P (xs @ y # ys) \<longleftrightarrow> no_trailing P (y # ys)"
by simp
@@ -142,6 +168,10 @@
"no_trailing P (strip_while P xs)"
by (induct xs rule: rev_induct) simp_all
+lemma strip_while_idem [simp]:
+ "no_trailing P xs \<Longrightarrow> strip_while P xs = xs"
+ by (cases xs rule: rev_cases) simp_all
+
lemma strip_while_eq_obtain_trailing:
assumes "strip_while P xs = ys"
obtains zs where "xs = ys @ zs" and "\<And>z. z \<in> set zs \<Longrightarrow> P z" and "no_trailing P ys"
@@ -172,9 +202,18 @@
qed
lemma no_trailing_map:
- "no_trailing P (map f xs) = no_trailing (P \<circ> f) xs"
+ "no_trailing P (map f xs) \<longleftrightarrow> no_trailing (P \<circ> f) xs"
by (simp add: last_map no_trailing_unfold)
+lemma no_trailing_drop [simp]:
+ "no_trailing P (drop n xs)" if "no_trailing P xs"
+proof -
+ from that have "no_trailing P (take n xs @ drop n xs)"
+ by simp
+ then show ?thesis
+ by (simp only: no_trailing_append)
+qed
+
lemma no_trailing_upt [simp]:
"no_trailing P [n..<m] \<longleftrightarrow> (n < m \<longrightarrow> \<not> P (m - 1))"
by (auto simp add: no_trailing_unfold)
--- a/src/HOL/Library/Polynomial.thy Wed Apr 05 22:25:18 2017 +0200
+++ b/src/HOL/Library/Polynomial.thy Wed Apr 05 22:29:09 2017 +0200
@@ -103,7 +103,8 @@
begin
lift_definition zero_poly :: "'a poly"
- is "\<lambda>_. 0" by (rule MOST_I) simp
+ is "\<lambda>_. 0"
+ by (rule MOST_I) simp
instance ..
@@ -377,11 +378,13 @@
with Cons show ?case by auto
qed
-lemma last_coeffs_not_0: "p \<noteq> 0 \<Longrightarrow> last (coeffs p) \<noteq> 0"
- by (induct p) (auto simp add: cCons_def)
-
-lemma strip_while_coeffs [simp]: "strip_while (HOL.eq 0) (coeffs p) = coeffs p"
- by (cases "p = 0") (auto dest: last_coeffs_not_0 intro: strip_while_not_last)
+lemma no_trailing_coeffs [simp]:
+ "no_trailing (HOL.eq 0) (coeffs p)"
+ by (induct p) auto
+
+lemma strip_while_coeffs [simp]:
+ "strip_while (HOL.eq 0) (coeffs p) = coeffs p"
+ by simp
lemma coeffs_eq_iff: "p = q \<longleftrightarrow> coeffs p = coeffs q"
(is "?P \<longleftrightarrow> ?Q")
@@ -402,11 +405,12 @@
lemma coeffs_eqI:
assumes coeff: "\<And>n. coeff p n = nth_default 0 xs n"
- assumes zero: "xs \<noteq> [] \<Longrightarrow> last xs \<noteq> 0"
+ assumes zero: "no_trailing (HOL.eq 0) xs"
shows "coeffs p = xs"
proof -
- from coeff have "p = Poly xs" by (simp add: poly_eq_iff)
- with zero show ?thesis by simp (cases xs; simp)
+ from coeff have "p = Poly xs"
+ by (simp add: poly_eq_iff)
+ with zero show ?thesis by simp
qed
lemma degree_eq_length_coeffs [code]: "degree p = length (coeffs p) - 1"
@@ -737,28 +741,26 @@
have *: "nth_default 0 (plus_coeffs xs ys) n = nth_default 0 xs n + nth_default 0 ys n"
for xs ys :: "'a list" and n
proof (induct xs ys arbitrary: n rule: plus_coeffs.induct)
- case 3
- then show ?case by (cases n) (auto simp: cCons_def)
- qed simp_all
- have **: "last (plus_coeffs xs ys) \<noteq> 0"
- if "xs \<noteq> [] \<Longrightarrow> last xs \<noteq> 0" and "ys \<noteq> [] \<Longrightarrow> last ys \<noteq> 0" and "plus_coeffs xs ys \<noteq> []"
- for xs ys :: "'a list"
- using that
- proof (induct xs ys rule: plus_coeffs.induct)
- case 3
- then show ?case by (auto simp add: cCons_def) metis
+ case (3 x xs y ys n)
+ then show ?case
+ by (cases n) (auto simp add: cCons_def)
qed simp_all
+ have **: "no_trailing (HOL.eq 0) (plus_coeffs xs ys)"
+ if "no_trailing (HOL.eq 0) xs" and "no_trailing (HOL.eq 0) ys"
+ for xs ys :: "'a list"
+ using that by (induct xs ys rule: plus_coeffs.induct) (simp_all add: cCons_def)
show ?thesis
- apply (rule coeffs_eqI)
- apply (simp add: * nth_default_coeffs_eq)
- apply (rule **)
- apply (auto dest: last_coeffs_not_0)
- done
+ by (rule coeffs_eqI) (auto simp add: * nth_default_coeffs_eq intro: **)
qed
-lemma coeffs_uminus [code abstract]: "coeffs (- p) = map (\<lambda>a. - a) (coeffs p)"
- by (rule coeffs_eqI)
- (simp_all add: not_0_coeffs_not_Nil last_map last_coeffs_not_0 nth_default_map_eq nth_default_coeffs_eq)
+lemma coeffs_uminus [code abstract]:
+ "coeffs (- p) = map uminus (coeffs p)"
+proof -
+ have eq_0: "HOL.eq 0 \<circ> uminus = HOL.eq (0::'a)"
+ by (simp add: fun_eq_iff)
+ show ?thesis
+ by (rule coeffs_eqI) (simp_all add: nth_default_map_eq nth_default_coeffs_eq no_trailing_map eq_0)
+qed
lemma [code]: "p - q = p + - q"
for p q :: "'a::ab_group_add poly"
@@ -885,9 +887,12 @@
lemma coeffs_smult [code abstract]:
"coeffs (smult a p) = (if a = 0 then [] else map (Groups.times a) (coeffs p))"
for p :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
- by (rule coeffs_eqI)
- (auto simp add: not_0_coeffs_not_Nil last_map last_coeffs_not_0
- nth_default_map_eq nth_default_coeffs_eq)
+proof -
+ have eq_0: "HOL.eq 0 \<circ> times a = HOL.eq (0::'a)" if "a \<noteq> 0"
+ using that by (simp add: fun_eq_iff)
+ show ?thesis
+ by (rule coeffs_eqI) (auto simp add: no_trailing_map nth_default_map_eq nth_default_coeffs_eq eq_0)
+qed
lemma smult_eq_iff:
fixes b :: "'a :: field"
@@ -1120,16 +1125,15 @@
"coeffs (map_poly f p) = strip_while (op = 0) (map f (coeffs p))"
by (simp add: map_poly_def)
-lemma set_coeffs_map_poly:
- "(\<And>x. f x = 0 \<longleftrightarrow> x = 0) \<Longrightarrow> set (coeffs (map_poly f p)) = f ` set (coeffs p)"
- by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0)
-
lemma coeffs_map_poly':
assumes "\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
shows "coeffs (map_poly f p) = map f (coeffs p)"
- by (cases "p = 0")
- (auto simp: assms coeffs_map_poly last_map last_coeffs_not_0
- intro!: strip_while_not_last split: if_splits)
+ using assms by (simp add: coeffs_map_poly no_trailing_map strip_while_idem_iff)
+ (metis comp_def no_leading_def no_trailing_coeffs)
+
+lemma set_coeffs_map_poly:
+ "(\<And>x. f x = 0 \<longleftrightarrow> x = 0) \<Longrightarrow> set (coeffs (map_poly f p)) = f ` set (coeffs p)"
+ by (simp add: coeffs_map_poly')
lemma degree_map_poly:
assumes "\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
@@ -2146,7 +2150,8 @@
lemma poly_shift_monom: "poly_shift n (monom c m) = (if m \<ge> n then monom c (m - n) else 0)"
by (auto simp add: poly_eq_iff coeff_poly_shift)
-lemma coeffs_shift_poly [code abstract]: "coeffs (poly_shift n p) = drop n (coeffs p)"
+lemma coeffs_shift_poly [code abstract]:
+ "coeffs (poly_shift n p) = drop n (coeffs p)"
proof (cases "p = 0")
case True
then show ?thesis by simp
@@ -2154,7 +2159,7 @@
case False
then show ?thesis
by (intro coeffs_eqI)
- (simp_all add: coeff_poly_shift nth_default_drop last_coeffs_not_0 nth_default_coeffs_eq)
+ (simp_all add: coeff_poly_shift nth_default_drop nth_default_coeffs_eq)
qed
@@ -2192,7 +2197,7 @@
unfolding no_trailing_unfold by auto
then show ?thesis
by (intro coeffs_eqI)
- (simp_all add: coeff_poly_cutoff last_coeffs_not_0 nth_default_take nth_default_coeffs_eq)
+ (simp_all add: coeff_poly_cutoff nth_default_take nth_default_coeffs_eq)
qed
@@ -2308,7 +2313,8 @@
for xs :: "_::{comm_semiring_0,semiring_no_zero_divisors} poly list"
by (induct xs) (simp_all add: reflect_poly_mult)
-lemma reflect_poly_Poly_nz: "xs \<noteq> [] \<Longrightarrow> last xs \<noteq> 0 \<Longrightarrow> reflect_poly (Poly xs) = Poly (rev xs)"
+lemma reflect_poly_Poly_nz:
+ "no_trailing (HOL.eq 0) xs \<Longrightarrow> reflect_poly (Poly xs) = Poly (rev xs)"
by (simp add: reflect_poly_def)
lemmas reflect_poly_simps =
@@ -4137,39 +4143,36 @@
qed simp
qed simp
-lemma pseudo_divmod_impl[code]: "pseudo_divmod (f::'a::comm_ring_1 poly) g =
- map_prod poly_of_list poly_of_list (pseudo_divmod_list (coeffs f) (coeffs g))"
+lemma pseudo_divmod_impl [code]:
+ "pseudo_divmod f g = map_prod poly_of_list poly_of_list (pseudo_divmod_list (coeffs f) (coeffs g))"
+ for f g :: "'a::comm_ring_1 poly"
proof (cases "g = 0")
case False
- then have coeffs_g_nonempty:"(coeffs g) \<noteq> []"
- by simp
- then have lastcoeffs: "last (coeffs g) = coeff g (degree g)"
- by (simp add: hd_rev last_coeffs_eq_coeff_degree not_0_coeffs_not_Nil)
- obtain q r where qr:
- "pseudo_divmod_main_list
- (last (coeffs g)) (rev [])
- (rev (coeffs f)) (rev (coeffs g))
- (1 + length (coeffs f) - length (coeffs g)) = (q, rev (rev r))"
+ then have "last (coeffs g) \<noteq> 0"
+ and "last (coeffs g) = lead_coeff g"
+ and "coeffs g \<noteq> []"
+ by (simp_all add: last_coeffs_eq_coeff_degree)
+ moreover obtain q r where qr: "pseudo_divmod_main_list
+ (last (coeffs g)) (rev [])
+ (rev (coeffs f)) (rev (coeffs g))
+ (1 + length (coeffs f) -
+ length (coeffs g)) = (q, rev (rev r))"
by force
- then have qr':
- "pseudo_divmod_main_list
- (hd (rev (coeffs g))) []
- (rev (coeffs f)) (rev (coeffs g))
- (1 + length (coeffs f) - length (coeffs g)) = (q, r)"
- using hd_rev[OF coeffs_g_nonempty] by auto
- from False have cg: "coeffs g = [] \<longleftrightarrow> False"
- by auto
- from False have last_non0: "last (coeffs g) \<noteq> 0"
- by (simp add: last_coeffs_not_0)
- from False show ?thesis
- unfolding pseudo_divmod_def pseudo_divmod_list_def Let_def qr' map_prod_def split cg if_False
- pseudo_divmod_main_list_invar[OF last_non0 _ _ qr,unfolded lastcoeffs,simplified,symmetric,OF False]
- poly_of_list_def
- by (auto simp: degree_eq_length_coeffs)
+ ultimately have "(Poly q, Poly (rev r)) = pseudo_divmod_main (lead_coeff g) 0 f g
+ (length (coeffs f) - Suc 0) (Suc (length (coeffs f)) - length (coeffs g))"
+ by (subst pseudo_divmod_main_list_invar [symmetric]) auto
+ moreover have "pseudo_divmod_main_list
+ (hd (rev (coeffs g))) []
+ (rev (coeffs f)) (rev (coeffs g))
+ (1 + length (coeffs f) -
+ length (coeffs g)) = (q, r)"
+ using qr hd_rev [OF \<open>coeffs g \<noteq> []\<close>] by simp
+ ultimately show ?thesis
+ by (auto simp: degree_eq_length_coeffs pseudo_divmod_def pseudo_divmod_list_def Let_def)
next
case True
then show ?thesis
- by (auto simp: pseudo_divmod_def pseudo_divmod_list_def)
+ by (auto simp add: pseudo_divmod_def pseudo_divmod_list_def)
qed
lemma pseudo_mod_main_list:
--- a/src/HOL/Library/Polynomial_Factorial.thy Wed Apr 05 22:25:18 2017 +0200
+++ b/src/HOL/Library/Polynomial_Factorial.thy Wed Apr 05 22:29:09 2017 +0200
@@ -16,8 +16,8 @@
subsection \<open>Various facts about polynomials\<close>
-lemma prod_mset_const_poly: "prod_mset (image_mset (\<lambda>x. [:f x:]) A) = [:prod_mset (image_mset f A):]"
- by (induction A) (simp_all add: one_poly_def mult_ac)
+lemma prod_mset_const_poly: " (\<Prod>x\<in>#A. [:f x:]) = [:prod_mset (image_mset f A):]"
+ by (induct A) (simp_all add: one_poly_def ac_simps)
lemma irreducible_const_poly_iff:
fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
@@ -168,14 +168,15 @@
by (auto elim!: dvdE)
lemma prod_mset_fract_poly:
- "prod_mset (image_mset (\<lambda>x. fract_poly (f x)) A) = fract_poly (prod_mset (image_mset f A))"
- by (induction A) (simp_all add: mult_ac)
+ "(\<Prod>x\<in>#A. map_poly to_fract (f x)) = fract_poly (prod_mset (image_mset f A))"
+ by (induct A) (simp_all add: ac_simps)
lemma is_unit_fract_poly_iff:
"p dvd 1 \<longleftrightarrow> fract_poly p dvd 1 \<and> content p = 1"
proof safe
assume A: "p dvd 1"
- with fract_poly_dvd[of p 1] show "is_unit (fract_poly p)" by simp
+ with fract_poly_dvd [of p 1] show "is_unit (fract_poly p)"
+ by simp
from A show "content p = 1"
by (auto simp: is_unit_poly_iff normalize_1_iff)
next
--- a/src/HOL/Tools/Function/function.ML Wed Apr 05 22:25:18 2017 +0200
+++ b/src/HOL/Tools/Function/function.ML Wed Apr 05 22:29:09 2017 +0200
@@ -120,7 +120,7 @@
val info =
{ add_simps=addsmps, fnames=fnames, case_names=cnames, psimps=psimps',
- pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
+ pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination', totality=NONE,
fs=fs, R=R, dom=dom, defname=defname, is_partial=true, cases=flat cases',
pelims=pelims',elims=NONE}
@@ -202,7 +202,8 @@
|-> (fn ((simps,(_,inducts)), elims) => fn lthy =>
let val info' = { is_partial=false, defname=defname, fnames=fnames, add_simps=add_simps,
case_names=case_names, fs=fs, R=R, dom=dom, psimps=psimps, pinducts=pinducts,
- simps=SOME simps, inducts=SOME inducts, termination=termination, cases=cases, pelims=pelims, elims=SOME elims}
+ simps=SOME simps, inducts=SOME inducts, termination=termination, totality=SOME totality,
+ cases=cases, pelims=pelims, elims=SOME elims}
in
(info',
lthy
--- a/src/HOL/Tools/Function/function_common.ML Wed Apr 05 22:25:18 2017 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Wed Apr 05 22:29:09 2017 +0200
@@ -22,6 +22,7 @@
simps : thm list option,
inducts : thm list option,
termination : thm,
+ totality : thm option,
cases : thm list,
pelims: thm list list,
elims: thm list list option}
@@ -46,6 +47,7 @@
simps : thm list option,
inducts : thm list option,
termination : thm,
+ totality : thm option,
cases : thm list,
pelims : thm list list,
elims : thm list list option}
@@ -291,7 +293,7 @@
domintros : thm list option}
fun transform_function_data phi ({add_simps, case_names, fnames, fs, R, dom, psimps, pinducts,
- simps, inducts, termination, defname, is_partial, cases, pelims, elims} : info) =
+ simps, inducts, termination, totality, defname, is_partial, cases, pelims, elims} : info) =
let
val term = Morphism.term phi
val thm = Morphism.thm phi
@@ -301,7 +303,8 @@
fs = map term fs, R = term R, dom = term dom, psimps = fact psimps,
pinducts = fact pinducts, simps = Option.map fact simps,
inducts = Option.map fact inducts, termination = thm termination,
- defname = Morphism.binding phi defname, is_partial=is_partial, cases = fact cases,
+ totality = Option.map thm totality, defname = Morphism.binding phi defname,
+ is_partial = is_partial, cases = fact cases,
elims = Option.map (map fact) elims, pelims = map fact pelims }
end