# HG changeset patch
# User wenzelm
# Date 1491424149 -7200
# Node ID faeccede95349eafcc993396bc30626be599d289
# Parent  83586780598b0f2281c30e8bd701bd0cf55f1263# Parent  079a6f850c0265c06227e143b4ca7bdc1e292a38
merged

diff -r 079a6f850c02 -r faeccede9534 src/HOL/Library/More_List.thy
--- 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)
diff -r 079a6f850c02 -r faeccede9534 src/HOL/Library/Polynomial.thy
--- 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:
diff -r 079a6f850c02 -r faeccede9534 src/HOL/Library/Polynomial_Factorial.thy
--- 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
diff -r 079a6f850c02 -r faeccede9534 src/HOL/Tools/Function/function.ML
--- 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
diff -r 079a6f850c02 -r faeccede9534 src/HOL/Tools/Function/function_common.ML
--- 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