--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Apr 11 18:46:49 2024 +0000
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Apr 12 22:19:27 2024 +0100
@@ -208,7 +208,7 @@
and nb: "tmbound m t"
and nle: "m \<le> length bs"
shows "Itm vs (removen m bs) (decrtm m t) = Itm vs bs t"
- using bnd nb nle by (induct t rule: tm.induct) (auto simp add: removen_nth)
+ using bnd nb nle by (induct t rule: tm.induct) (auto simp: removen_nth)
primrec tmsubst0:: "tm \<Rightarrow> tm \<Rightarrow> tm"
where
@@ -276,25 +276,33 @@
| "tmadd a b = Add a b"
lemma tmadd [simp]: "Itm vs bs (tmadd t s) = Itm vs bs (Add t s)"
- apply (induct t s rule: tmadd.induct)
- apply (simp_all add: Let_def)
- apply (case_tac "c1 +\<^sub>p c2 = 0\<^sub>p")
- apply (case_tac "n1 \<le> n2")
- apply simp_all
- apply (case_tac "n1 = n2")
- apply (simp_all add: algebra_simps)
- apply (simp only: distrib_left [symmetric] polyadd [symmetric])
- apply simp
- done
+proof (induct t s rule: tmadd.induct)
+ case (1 n1 c1 r1 n2 c2 r2)
+ show ?case
+ proof (cases "c1 +\<^sub>p c2 = 0\<^sub>p")
+ case 0: True
+ show ?thesis
+ proof (cases "n1 \<le> n2")
+ case True
+ with 0 show ?thesis
+ apply (simp add: 1)
+ by (metis INum_int(2) Ipoly.simps(1) comm_semiring_class.distrib mult_eq_0_iff polyadd)
+ qed (use 0 1 in auto)
+ next
+ case False
+ then show ?thesis
+ using 1 comm_semiring_class.distrib by auto
+ qed
+qed auto
lemma tmadd_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 s \<Longrightarrow> tmbound0 (tmadd t s)"
- by (induct t s rule: tmadd.induct) (auto simp add: Let_def)
+ by (induct t s rule: tmadd.induct) (auto simp: Let_def)
lemma tmadd_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n s \<Longrightarrow> tmbound n (tmadd t s)"
- by (induct t s rule: tmadd.induct) (auto simp add: Let_def)
+ by (induct t s rule: tmadd.induct) (auto simp: Let_def)
lemma tmadd_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n s \<Longrightarrow> tmboundslt n (tmadd t s)"
- by (induct t s rule: tmadd.induct) (auto simp add: Let_def)
+ by (induct t s rule: tmadd.induct) (auto simp: Let_def)
lemma tmadd_allpolys_npoly[simp]:
"allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmadd t s)"
@@ -316,7 +324,7 @@
by (induct t arbitrary: n rule: tmmul.induct) auto
lemma tmmul_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (tmmul t i)"
- by (induct t arbitrary: i rule: tmmul.induct) (auto simp add: Let_def)
+ by (induct t arbitrary: i rule: tmmul.induct) (auto simp: Let_def)
lemma tmmul_allpolys_npoly[simp]:
assumes "SORT_CONSTRAINT('a::field_char_0)"
@@ -381,21 +389,19 @@
lemma polynate_stupid:
assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a)"
- apply (subst polynate[symmetric])
- apply simp
- done
+ by (metis INum_int(2) Ipoly.simps(1) polynate)
lemma simptm_ci[simp]: "Itm vs bs (simptm t) = Itm vs bs t"
- by (induct t rule: simptm.induct) (auto simp add: Let_def polynate_stupid)
+ by (induct t rule: simptm.induct) (auto simp: Let_def polynate_stupid)
lemma simptm_tmbound0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 (simptm t)"
- by (induct t rule: simptm.induct) (auto simp add: Let_def)
+ by (induct t rule: simptm.induct) (auto simp: Let_def)
lemma simptm_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n (simptm t)"
- by (induct t rule: simptm.induct) (auto simp add: Let_def)
+ by (induct t rule: simptm.induct) (auto simp: Let_def)
lemma simptm_nlt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (simptm t)"
- by (induct t rule: simptm.induct) (auto simp add: Let_def)
+ by (induct t rule: simptm.induct) (auto simp: Let_def)
lemma [simp]: "isnpoly 0\<^sub>p"
and [simp]: "isnpoly (C (1, 1))"
@@ -404,7 +410,7 @@
lemma simptm_allpolys_npoly[simp]:
assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "allpolys isnpoly (simptm p)"
- by (induct p rule: simptm.induct) (auto simp add: Let_def)
+ by (induct p rule: simptm.induct) (auto simp: Let_def)
declare let_cong[fundef_cong del]
@@ -422,24 +428,15 @@
declare let_cong[fundef_cong]
lemma split0_stupid[simp]: "\<exists>x y. (x, y) = split0 p"
- apply (rule exI[where x="fst (split0 p)"])
- apply (rule exI[where x="snd (split0 p)"])
- apply simp
- done
+ using prod.collapse by blast
lemma split0:
"tmbound 0 (snd (split0 t)) \<and> Itm vs bs (CNP 0 (fst (split0 t)) (snd (split0 t))) = Itm vs bs t"
- apply (induct t rule: split0.induct)
- apply simp
- apply (simp add: Let_def split_def field_simps)
- apply (simp add: Let_def split_def field_simps)
- apply (simp add: Let_def split_def field_simps)
- apply (simp add: Let_def split_def field_simps)
- apply (simp add: Let_def split_def field_simps)
- apply (simp add: Let_def split_def mult.assoc distrib_left[symmetric])
- apply (simp add: Let_def split_def field_simps)
- apply (simp add: Let_def split_def field_simps)
- done
+proof (induct t rule: split0.induct)
+ case (7 c t)
+ then show ?case
+ by (simp add: Let_def split_def mult.assoc flip: distrib_left)
+qed (auto simp: Let_def split_def field_simps)
lemma split0_ci: "split0 t = (c',t') \<Longrightarrow> Itm vs bs t = Itm vs bs (CNP 0 c' t')"
proof -
@@ -472,21 +469,21 @@
lemma split0_nb:
assumes nb: "tmbound n t"
shows "tmbound n (snd (split0 t))"
- using nb by (induct t rule: split0.induct) (auto simp add: Let_def split_def)
+ using nb by (induct t rule: split0.induct) (auto simp: Let_def split_def)
lemma split0_blt:
assumes nb: "tmboundslt n t"
shows "tmboundslt n (snd (split0 t))"
- using nb by (induct t rule: split0.induct) (auto simp add: Let_def split_def)
+ using nb by (induct t rule: split0.induct) (auto simp: Let_def split_def)
lemma tmbound_split0: "tmbound 0 t \<Longrightarrow> Ipoly vs (fst (split0 t)) = 0"
- by (induct t rule: split0.induct) (auto simp add: Let_def split_def)
+ by (induct t rule: split0.induct) (auto simp: Let_def split_def)
lemma tmboundslt_split0: "tmboundslt n t \<Longrightarrow> Ipoly vs (fst (split0 t)) = 0 \<or> n > 0"
- by (induct t rule: split0.induct) (auto simp add: Let_def split_def)
+ by (induct t rule: split0.induct) (auto simp: Let_def split_def)
lemma tmboundslt0_split0: "tmboundslt 0 t \<Longrightarrow> Ipoly vs (fst (split0 t)) = 0"
- by (induct t rule: split0.induct) (auto simp add: Let_def split_def)
+ by (induct t rule: split0.induct) (auto simp: Let_def split_def)
lemma allpolys_split0: "allpolys isnpoly p \<Longrightarrow> allpolys isnpoly (snd (split0 p))"
by (induct p rule: split0.induct) (auto simp add: isnpoly_def Let_def split_def)
@@ -764,7 +761,7 @@
from A(1)[OF bnd nb nle] show ?thesis .
qed
then show ?case by auto
-qed (auto simp add: decrtm removen_nth)
+qed (auto simp: decrtm removen_nth)
primrec subst0 :: "tm \<Rightarrow> fm \<Rightarrow> fm"
where
@@ -849,7 +846,7 @@
by (simp add: incrtm0[where x="x" and bs="bs" and t="t"])
qed
then show ?case by simp
-qed (auto simp add: tmsubst)
+qed (auto simp: tmsubst)
lemma subst_nb:
assumes "tmbound m t"
@@ -926,36 +923,38 @@
where "evaldjf f ps \<equiv> foldr (djf f) ps F"
lemma djf_Or: "Ifm vs bs (djf f p q) = Ifm vs bs (Or (f p) q)"
- apply (cases "q = T")
- apply (simp add: djf_def)
- apply (cases "q = F")
- apply (simp add: djf_def)
- apply (cases "f p")
- apply (simp_all add: Let_def djf_def)
- done
+ by (cases "f p") (simp_all add: Let_def djf_def)
lemma evaldjf_ex: "Ifm vs bs (evaldjf f ps) \<longleftrightarrow> (\<exists>p \<in> set ps. Ifm vs bs (f p))"
by (induct ps) (simp_all add: evaldjf_def djf_Or)
lemma evaldjf_bound0:
- assumes "\<forall>x\<in> set xs. bound0 (f x)"
+ assumes "\<forall>x \<in> set xs. bound0 (f x)"
shows "bound0 (evaldjf f xs)"
using assms
- apply (induct xs)
- apply (auto simp add: evaldjf_def djf_def Let_def)
- apply (case_tac "f a")
- apply auto
- done
+proof (induct xs)
+ case Nil
+ then show ?case
+ by (simp add: evaldjf_def)
+next
+ case (Cons a xs)
+ then show ?case
+ by (cases "f a") (simp_all add: evaldjf_def djf_def Let_def)
+qed
lemma evaldjf_qf:
assumes "\<forall>x\<in> set xs. qfree (f x)"
shows "qfree (evaldjf f xs)"
using assms
- apply (induct xs)
- apply (auto simp add: evaldjf_def djf_def Let_def)
- apply (case_tac "f a")
- apply auto
- done
+proof (induct xs)
+ case Nil
+ then show ?case
+ by (simp add: evaldjf_def)
+next
+ case (Cons a xs)
+ then show ?case
+ by (cases "f a") (simp_all add: evaldjf_def djf_def Let_def)
+qed
fun disjuncts :: "fm \<Rightarrow> fm list"
where
@@ -1100,71 +1099,32 @@
definition "neq p = not (eq p)"
lemma lt: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (lt p) = Ifm vs bs (Lt p)"
- apply (simp add: lt_def)
- apply (cases p)
- apply simp_all
- apply (rename_tac poly, case_tac poly)
- apply (simp_all add: isnpoly_def)
- done
+ by (auto simp: lt_def isnpoly_def split: tm.split poly.split)
lemma le: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (le p) = Ifm vs bs (Le p)"
- apply (simp add: le_def)
- apply (cases p)
- apply simp_all
- apply (rename_tac poly, case_tac poly)
- apply (simp_all add: isnpoly_def)
- done
+ by (auto simp: le_def isnpoly_def split: tm.split poly.split)
lemma eq: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (eq p) = Ifm vs bs (Eq p)"
- apply (simp add: eq_def)
- apply (cases p)
- apply simp_all
- apply (rename_tac poly, case_tac poly)
- apply (simp_all add: isnpoly_def)
- done
+ by (auto simp: eq_def isnpoly_def split: tm.split poly.split)
lemma neq: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (neq p) = Ifm vs bs (NEq p)"
by (simp add: neq_def eq)
lemma lt_lin: "tmbound0 p \<Longrightarrow> islin (lt p)"
- apply (simp add: lt_def)
- apply (cases p)
- apply simp_all
- apply (rename_tac poly, case_tac poly)
- apply simp_all
- apply (rename_tac nat a b, case_tac nat)
- apply simp_all
- done
+ using islin_stupid
+ by(auto simp: lt_def isnpoly_def split: tm.split poly.split)
lemma le_lin: "tmbound0 p \<Longrightarrow> islin (le p)"
- apply (simp add: le_def)
- apply (cases p)
- apply simp_all
- apply (rename_tac poly, case_tac poly)
- apply simp_all
- apply (rename_tac nat a b, case_tac nat)
- apply simp_all
- done
+ using islin_stupid
+ by(auto simp: le_def isnpoly_def split: tm.split poly.split)
lemma eq_lin: "tmbound0 p \<Longrightarrow> islin (eq p)"
- apply (simp add: eq_def)
- apply (cases p)
- apply simp_all
- apply (rename_tac poly, case_tac poly)
- apply simp_all
- apply (rename_tac nat a b, case_tac nat)
- apply simp_all
- done
+ using islin_stupid
+ by(auto simp: eq_def isnpoly_def split: tm.split poly.split)
lemma neq_lin: "tmbound0 p \<Longrightarrow> islin (neq p)"
- apply (simp add: neq_def eq_def)
- apply (cases p)
- apply simp_all
- apply (rename_tac poly, case_tac poly)
- apply simp_all
- apply (rename_tac nat a b, case_tac nat)
- apply simp_all
- done
+ using islin_stupid
+ by(auto simp: neq_def eq_def isnpoly_def split: tm.split poly.split)
definition "simplt t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then lt s else Lt (CNP 0 c s))"
definition "simple t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then le s else Le (CNP 0 c s))"
@@ -1176,7 +1136,7 @@
shows "islin (simplt t)"
unfolding simplt_def
using split0_nb0'
- by (auto simp add: lt_lin Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
+ by (auto simp: lt_lin Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
islin_stupid allpolys_split0[OF simptm_allpolys_npoly])
lemma simple_islin [simp]:
@@ -1184,7 +1144,7 @@
shows "islin (simple t)"
unfolding simple_def
using split0_nb0'
- by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
+ by (auto simp: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
islin_stupid allpolys_split0[OF simptm_allpolys_npoly] le_lin)
lemma simpeq_islin [simp]:
@@ -1192,7 +1152,7 @@
shows "islin (simpeq t)"
unfolding simpeq_def
using split0_nb0'
- by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
+ by (auto simp: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
islin_stupid allpolys_split0[OF simptm_allpolys_npoly] eq_lin)
lemma simpneq_islin [simp]:
@@ -1200,7 +1160,7 @@
shows "islin (simpneq t)"
unfolding simpneq_def
using split0_nb0'
- by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
+ by (auto simp: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
islin_stupid allpolys_split0[OF simptm_allpolys_npoly] neq_lin)
lemma really_stupid: "\<not> (\<forall>c1 s'. (c1, s') \<noteq> split0 s)"
@@ -1213,7 +1173,7 @@
and "allpolys isnpoly (snd (split0 t))"
using *
by (induct t rule: split0.induct)
- (auto simp add: Let_def split_def polyadd_norm polymul_norm polyneg_norm
+ (auto simp: Let_def split_def polyadd_norm polymul_norm polyneg_norm
polysub_norm really_stupid)
lemma simplt[simp]: "Ifm vs bs (simplt t) = Ifm vs bs (Lt t)"
@@ -1291,44 +1251,24 @@
qed
lemma lt_nb: "tmbound0 t \<Longrightarrow> bound0 (lt t)"
- apply (simp add: lt_def)
- apply (cases t)
- apply auto
- apply (rename_tac poly, case_tac poly)
- apply auto
- done
+ by(auto simp: lt_def split: tm.split poly.split)
lemma le_nb: "tmbound0 t \<Longrightarrow> bound0 (le t)"
- apply (simp add: le_def)
- apply (cases t)
- apply auto
- apply (rename_tac poly, case_tac poly)
- apply auto
- done
+ by(auto simp: le_def split: tm.split poly.split)
lemma eq_nb: "tmbound0 t \<Longrightarrow> bound0 (eq t)"
- apply (simp add: eq_def)
- apply (cases t)
- apply auto
- apply (rename_tac poly, case_tac poly)
- apply auto
- done
+ by(auto simp: eq_def split: tm.split poly.split)
lemma neq_nb: "tmbound0 t \<Longrightarrow> bound0 (neq t)"
- apply (simp add: neq_def eq_def)
- apply (cases t)
- apply auto
- apply (rename_tac poly, case_tac poly)
- apply auto
- done
-
+ by(auto simp: neq_def eq_def split: tm.split poly.split)
+
+(*THE FOLLOWING PROOFS MIGHT BE COMBINED*)
lemma simplt_nb[simp]:
- assumes "SORT_CONSTRAINT('a::field_char_0)"
- shows "tmbound0 t \<Longrightarrow> bound0 (simplt t)"
+ assumes "SORT_CONSTRAINT('a::field_char_0)" and t: "tmbound0 t"
+ shows "bound0 (simplt t)"
proof (simp add: simplt_def Let_def split_def)
- assume "tmbound0 t"
- then have *: "tmbound0 (simptm t)"
- by simp
+ have *: "tmbound0 (simptm t)"
+ using t by simp
let ?c = "fst (split0 (simptm t))"
from tmbound_split0[OF *[unfolded tmbound0_tmbound_iff[symmetric]]]
have th: "\<forall>bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p"
@@ -1344,12 +1284,11 @@
qed
lemma simple_nb[simp]:
- assumes "SORT_CONSTRAINT('a::field_char_0)"
- shows "tmbound0 t \<Longrightarrow> bound0 (simple t)"
+ assumes "SORT_CONSTRAINT('a::field_char_0)" and t: "tmbound0 t"
+ shows "bound0 (simple t)"
proof(simp add: simple_def Let_def split_def)
- assume "tmbound0 t"
- then have *: "tmbound0 (simptm t)"
- by simp
+ have *: "tmbound0 (simptm t)"
+ using t by simp
let ?c = "fst (split0 (simptm t))"
from tmbound_split0[OF *[unfolded tmbound0_tmbound_iff[symmetric]]]
have th: "\<forall>bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p"
@@ -1365,12 +1304,11 @@
qed
lemma simpeq_nb[simp]:
- assumes "SORT_CONSTRAINT('a::field_char_0)"
- shows "tmbound0 t \<Longrightarrow> bound0 (simpeq t)"
+ assumes "SORT_CONSTRAINT('a::field_char_0)" and t: "tmbound0 t"
+ shows "bound0 (simpeq t)"
proof (simp add: simpeq_def Let_def split_def)
- assume "tmbound0 t"
- then have *: "tmbound0 (simptm t)"
- by simp
+ have *: "tmbound0 (simptm t)"
+ using t by simp
let ?c = "fst (split0 (simptm t))"
from tmbound_split0[OF *[unfolded tmbound0_tmbound_iff[symmetric]]]
have th: "\<forall>bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p"
@@ -1386,12 +1324,11 @@
qed
lemma simpneq_nb[simp]:
- assumes "SORT_CONSTRAINT('a::field_char_0)"
- shows "tmbound0 t \<Longrightarrow> bound0 (simpneq t)"
+ assumes "SORT_CONSTRAINT('a::field_char_0)" and t: "tmbound0 t"
+ shows "bound0 (simpneq t)"
proof (simp add: simpneq_def Let_def split_def)
- assume "tmbound0 t"
- then have *: "tmbound0 (simptm t)"
- by simp
+ have *: "tmbound0 (simptm t)"
+ using t by simp
let ?c = "fst (split0 (simptm t))"
from tmbound_split0[OF *[unfolded tmbound0_tmbound_iff[symmetric]]]
have th: "\<forall>bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p"
@@ -1419,35 +1356,30 @@
where "list_disj ps \<equiv> foldr disj ps F"
lemma list_conj: "Ifm vs bs (list_conj ps) = (\<forall>p\<in> set ps. Ifm vs bs p)"
- by (induct ps) (auto simp add: list_conj_def)
+ by (induct ps) (auto simp: list_conj_def)
lemma list_conj_qf: " \<forall>p\<in> set ps. qfree p \<Longrightarrow> qfree (list_conj ps)"
- by (induct ps) (auto simp add: list_conj_def)
+ by (induct ps) (auto simp: list_conj_def)
lemma list_disj: "Ifm vs bs (list_disj ps) = (\<exists>p\<in> set ps. Ifm vs bs p)"
- by (induct ps) (auto simp add: list_disj_def)
+ by (induct ps) (auto simp: list_disj_def)
lemma conj_boundslt: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (conj p q)"
unfolding conj_def by auto
lemma conjs_nb: "bound n p \<Longrightarrow> \<forall>q\<in> set (conjs p). bound n q"
- apply (induct p rule: conjs.induct)
- apply (unfold conjs.simps)
- apply (unfold set_append)
- apply (unfold ball_Un)
- apply (unfold bound.simps)
- apply auto
- done
+proof (induct p rule: conjs.induct)
+ case (1 p q)
+ then show ?case
+ unfolding conjs.simps bound.simps by fastforce
+qed auto
lemma conjs_boundslt: "boundslt n p \<Longrightarrow> \<forall>q\<in> set (conjs p). boundslt n q"
- apply (induct p rule: conjs.induct)
- apply (unfold conjs.simps)
- apply (unfold set_append)
- apply (unfold ball_Un)
- apply (unfold boundslt.simps)
- apply blast
- apply simp_all
- done
+proof (induct p rule: conjs.induct)
+ case (1 p q)
+ then show ?case
+ unfolding conjs.simps bound.simps by fastforce
+qed auto
lemma list_conj_boundslt: " \<forall>p\<in> set ps. boundslt n p \<Longrightarrow> boundslt n (list_conj ps)"
by (induct ps) (auto simp: list_conj_def)
@@ -1503,7 +1435,7 @@
also fix y have "\<dots> = (\<exists>x. (Ifm vs (y#bs) ?cyes) \<and> (Ifm vs (x#bs) ?cno))"
using bound0_I[OF yes_nb, where bs="bs" and b'="y"] by blast
also have "\<dots> = (Ifm vs bs (decr0 ?cyes) \<and> Ifm vs bs (E ?cno))"
- by (auto simp add: decr0[OF yes_nb] simp del: partition_filter_conv)
+ by (auto simp: decr0[OF yes_nb] simp del: partition_filter_conv)
also have "\<dots> = (Ifm vs bs (conj (decr0 ?cyes) (qe ?cno)))"
using qe[rule_format, OF no_qf] by auto
finally have "Ifm vs bs (E p) = Ifm vs bs (CJNB qe p)"
@@ -1546,25 +1478,13 @@
by (induct p rule: simpfm.induct) auto
lemma lt_qf[simp]: "qfree (lt t)"
- apply (cases t)
- apply (auto simp add: lt_def)
- apply (rename_tac poly, case_tac poly)
- apply auto
- done
+ by(auto simp: lt_def split: tm.split poly.split)
lemma le_qf[simp]: "qfree (le t)"
- apply (cases t)
- apply (auto simp add: le_def)
- apply (rename_tac poly, case_tac poly)
- apply auto
- done
+ by(auto simp: le_def split: tm.split poly.split)
lemma eq_qf[simp]: "qfree (eq t)"
- apply (cases t)
- apply (auto simp add: eq_def)
- apply (rename_tac poly, case_tac poly)
- apply auto
- done
+ by(auto simp: eq_def split: tm.split poly.split)
lemma neq_qf[simp]: "qfree (neq t)"
by (simp add: neq_def)
@@ -1671,19 +1591,19 @@
shows "\<exists>z. \<forall>x < z. Ifm vs (x#bs) (minusinf p) \<longleftrightarrow> Ifm vs (x#bs) p"
using assms
proof (induct p rule: minusinf.induct)
- case 1
+ case (1 p q)
+ then obtain zp zq where zp: "\<forall>x<zp. Ifm vs (x # bs) (minusinf p) = Ifm vs (x # bs) p"
+ and zq: "\<forall>x<zq. Ifm vs (x # bs) (minusinf q) = Ifm vs (x # bs) q"
+ by force
then show ?case
- apply auto
- apply (rule_tac x="min z za" in exI)
- apply auto
- done
+ by (rule_tac x="min zp zq" in exI) auto
next
- case 2
+ case (2 p q)
+ then obtain zp zq where zp: "\<forall>x<zp. Ifm vs (x # bs) (minusinf p) = Ifm vs (x # bs) p"
+ and zq: "\<forall>x<zq. Ifm vs (x # bs) (minusinf q) = Ifm vs (x # bs) q"
+ by force
then show ?case
- apply auto
- apply (rule_tac x="min z za" in exI)
- apply auto
- done
+ by (rule_tac x="min zp zq" in exI) auto
next
case (3 c e)
then have nbe: "tmbound0 e"
@@ -1876,19 +1796,19 @@
shows "\<exists>z. \<forall>x > z. Ifm vs (x#bs) (plusinf p) \<longleftrightarrow> Ifm vs (x#bs) p"
using assms
proof (induct p rule: plusinf.induct)
- case 1
+ case (1 p q)
+ then obtain zp zq where zp: "\<forall>x>zp. Ifm vs (x # bs) (plusinf p) = Ifm vs (x # bs) p"
+ and zq: "\<forall>x>zq. Ifm vs (x # bs) (plusinf q) = Ifm vs (x # bs) q"
+ by force
then show ?case
- apply auto
- apply (rule_tac x="max z za" in exI)
- apply auto
- done
+ by (rule_tac x="max zp zq" in exI) auto
next
- case 2
+ case (2 p q)
+ then obtain zp zq where zp: "\<forall>x>zp. Ifm vs (x # bs) (plusinf p) = Ifm vs (x # bs) p"
+ and zq: "\<forall>x>zq. Ifm vs (x # bs) (plusinf q) = Ifm vs (x # bs) q"
+ by force
then show ?case
- apply auto
- apply (rule_tac x="max z za" in exI)
- apply auto
- done
+ by (rule_tac x="max zp zq" in exI) auto
next
case (3 c e)
then have nbe: "tmbound0 e"
@@ -2072,10 +1992,10 @@
qed auto
lemma minusinf_nb: "islin p \<Longrightarrow> bound0 (minusinf p)"
- by (induct p rule: minusinf.induct) (auto simp add: eq_nb lt_nb le_nb)
+ by (induct p rule: minusinf.induct) (auto simp: eq_nb lt_nb le_nb)
lemma plusinf_nb: "islin p \<Longrightarrow> bound0 (plusinf p)"
- by (induct p rule: minusinf.induct) (auto simp add: eq_nb lt_nb le_nb)
+ by (induct p rule: minusinf.induct) (auto simp: eq_nb lt_nb le_nb)
lemma minusinf_ex:
assumes lp: "islin p"
@@ -2140,16 +2060,14 @@
Ipoly vs c < 0 \<and> Ipoly vs c * x \<le> - Itm vs (x#bs) s \<or>
Ipoly vs c > 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s"
using lp nmi ex
- apply (induct p rule: minusinf.induct)
- apply (auto simp add: eq le lt polyneg_norm)
- apply (auto simp add: linorder_not_less order_le_less)
- done
+ by (induct p rule: minusinf.induct)
+ (auto simp: eq le lt polyneg_norm linorder_not_less order_le_less)
then obtain c s where csU: "(c, s) \<in> set (uset p)"
and x: "(Ipoly vs c < 0 \<and> Ipoly vs c * x \<le> - Itm vs (x#bs) s) \<or>
(Ipoly vs c > 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s)" by blast
then have "x \<ge> (- Itm vs (x#bs) s) / Ipoly vs c"
using divide_le_eq[of "- Itm vs (x#bs) s" "Ipoly vs c" x]
- by (auto simp add: mult.commute)
+ by (auto simp: mult.commute)
then show ?thesis
using csU by auto
qed
@@ -2183,10 +2101,8 @@
Ipoly vs c < 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s \<or>
Ipoly vs c > 0 \<and> Ipoly vs c * x \<le> - Itm vs (x#bs) s"
using lp nmi ex
- apply (induct p rule: minusinf.induct)
- apply (auto simp add: eq le lt polyneg_norm)
- apply (auto simp add: linorder_not_less order_le_less)
- done
+ by (induct p rule: minusinf.induct)
+ (auto simp: eq le lt polyneg_norm linorder_not_less order_le_less)
then obtain c s
where c_s: "(c, s) \<in> set (uset p)"
and "Ipoly vs c < 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s \<or>
@@ -2194,7 +2110,7 @@
by blast
then have "x \<le> (- Itm vs (x#bs) s) / Ipoly vs c"
using le_divide_eq[of x "- Itm vs (x#bs) s" "Ipoly vs c"]
- by (auto simp add: mult.commute)
+ by (auto simp: mult.commute)
then show ?thesis
using c_s by auto
qed
@@ -2248,7 +2164,7 @@
case N: 2
from px pos_less_divide_eq[OF N, where a="x" and b="-?Nt x s"]
have px': "x < - ?Nt x s / ?N c"
- by (auto simp add: not_less field_simps)
+ by (auto simp: not_less field_simps)
from ycs show ?thesis
proof
assume y: "y < - ?Nt x s / ?N c"
@@ -2272,7 +2188,7 @@
case N: 3
from px neg_divide_less_eq[OF N, where a="x" and b="-?Nt x s"]
have px': "x > - ?Nt x s / ?N c"
- by (auto simp add: not_less field_simps)
+ by (auto simp: not_less field_simps)
from ycs show ?thesis
proof
assume y: "y > - ?Nt x s / ?N c"
@@ -2449,7 +2365,7 @@
show ?thesis
by (simp add: field_simps tmbound0_I[OF lin(3), of vs x bs y] sum_eq[symmetric])
qed
-qed (auto simp add: tmbound0_I[where vs=vs and bs="bs" and b="y" and b'="x"]
+qed (auto simp: tmbound0_I[where vs=vs and bs="bs" and b="y" and b'="x"]
bound0_I[where vs=vs and bs="bs" and b="y" and b'="x"])
lemma inf_uset:
@@ -3261,7 +3177,7 @@
Ifm vs (((- Itm vs (x#bs) t / Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) p"
using lp
by (induct p rule: islin.induct)
- (auto simp add: tmbound0_I
+ (auto simp: tmbound0_I
[where b = "(- (Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>) - (Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>)) / 2"
and b' = x and bs = bs and vs = vs]
msubsteq msubstneq msubstlt [OF nc nd] msubstle [OF nc nd])
@@ -3272,7 +3188,7 @@
and "tmbound0 s"
shows "bound0 (msubst p ((c,t),(d,s)))"
using assms
- by (induct p rule: islin.induct) (auto simp add: msubsteq_nb msubstneq_nb msubstlt_nb msubstle_nb)
+ by (induct p rule: islin.induct) (auto simp: msubsteq_nb msubstneq_nb msubstlt_nb msubstle_nb)
lemma fr_eq_msubst:
assumes lp: "islin p"
@@ -3315,7 +3231,7 @@
lemma simpfm_lin:
assumes "SORT_CONSTRAINT('a::field_char_0)"
shows "qfree p \<Longrightarrow> islin (simpfm p)"
- by (induct p rule: simpfm.induct) (auto simp add: conj_lin disj_lin)
+ by (induct p rule: simpfm.induct) (auto simp: conj_lin disj_lin)
definition "ferrack p \<equiv>
let
@@ -3395,10 +3311,7 @@
by simp
also have "\<dots> \<longleftrightarrow> ?rhs"
using decr0[OF th1, of vs x bs]
- apply (simp add: ferrack_def Let_def)
- apply (cases "?mp = T \<or> ?pp = T")
- apply auto
- done
+ by (cases "?mp = T \<or> ?pp = T") (auto simp: ferrack_def Let_def)
finally show ?thesis
using thqf by blast
qed
@@ -3468,11 +3381,8 @@
case z: 4
from z have ?F
using ct
- apply -
- apply (rule bexI[where x = "(c,t)"])
- apply simp_all
- apply (rule bexI[where x = "(d,s)"])
- apply simp_all
+ apply (intro bexI[where x = "(c,t)"]; simp)
+ apply (intro bexI[where x = "(d,s)"]; simp)
done
then show ?thesis by blast
qed
@@ -3553,7 +3463,7 @@
Ifm vs (Itm vs (x#bs) t / Ipoly vs c #bs) p"
using lp pos
by (induct p rule: islin.induct)
- (auto simp add: msubsteq2 msubstltpos[OF pos] msubstlepos[OF pos]
+ (auto simp: msubsteq2 msubstltpos[OF pos] msubstlepos[OF pos]
tmbound0_I[of _ vs "Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>" bs x]
bound0_I[of _ vs "Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>" bs x] field_simps)
@@ -3573,7 +3483,7 @@
shows "Ifm vs (x#bs) (msubstneg p c t) = Ifm vs (Itm vs (x#bs) t / Ipoly vs c #bs) p"
using lp pos
by (induct p rule: islin.induct)
- (auto simp add: msubsteq2 msubstltneg[OF pos] msubstleneg[OF pos]
+ (auto simp: msubsteq2 msubstltneg[OF pos] msubstleneg[OF pos]
tmbound0_I[of _ vs "Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>" bs x]
bound0_I[of _ vs "Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>" bs x] field_simps)
@@ -3596,12 +3506,12 @@
case c: 1
from c msubstneg_I[OF lp c, of x bs t] lt[OF anc(1), of vs "x#bs"] lt[OF anc(2), of vs "x#bs"]
show ?thesis
- by (auto simp add: msubst2_def)
+ by (auto simp: msubst2_def)
next
case c: 2
from c msubstpos_I[OF lp c, of x bs t] lt[OF anc(1), of vs "x#bs"] lt[OF anc(2), of vs "x#bs"]
show ?thesis
- by (auto simp add: msubst2_def)
+ by (auto simp: msubst2_def)
qed
qed
@@ -3624,7 +3534,7 @@
shows "bound0 (msubstpos p c t)"
using lp tnb
by (induct p c t rule: msubstpos.induct)
- (auto simp add: msubsteq2_nb msubstltpos_nb msubstlepos_nb)
+ (auto simp: msubsteq2_nb msubstltpos_nb msubstlepos_nb)
lemma msubstneg_nb:
assumes "SORT_CONSTRAINT('a::field_char_0)"
@@ -3633,7 +3543,7 @@
shows "bound0 (msubstneg p c t)"
using lp tnb
by (induct p c t rule: msubstneg.induct)
- (auto simp add: msubsteq2_nb msubstltneg_nb msubstleneg_nb)
+ (auto simp: msubsteq2_nb msubstltneg_nb msubstleneg_nb)
lemma msubst2_nb:
assumes "SORT_CONSTRAINT('a::field_char_0)"
@@ -3652,7 +3562,7 @@
by simp
lemma islin_qf: "islin p \<Longrightarrow> qfree p"
- by (induct p rule: islin.induct) (auto simp add: bound0_qf)
+ by (induct p rule: islin.induct) (auto simp: bound0_qf)
lemma fr_eq_msubst2:
assumes lp: "islin p"
@@ -3689,7 +3599,7 @@
by (simp add: polyneg_norm nn)
then have nn2: "\<lparr>n *\<^sub>p(C (-2,1)) \<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>n \<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
using H(2) nn' nn
- by (auto simp add: msubst2_def lt zero_less_mult_iff mult_less_0_iff)
+ by (auto simp: msubst2_def lt zero_less_mult_iff mult_less_0_iff)
from msubst2[OF lp nn nn2(1), of x bs t]
have "\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> Ifm vs (- Itm vs (x # bs) t / (\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> * 2) # bs) p"
using H(2) nn2 by (simp add: mult_minus2_right)
@@ -3731,7 +3641,7 @@
by (simp_all add: polyneg_norm nn)
have nn': "\<lparr>(C (-2, 1) *\<^sub>p c*\<^sub>p d)\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
using H(3)
- by (auto simp add: msubst2_def lt[OF stupid(1)]
+ by (auto simp: msubst2_def lt[OF stupid(1)]
lt[OF stupid(2)] zero_less_mult_iff mult_less_0_iff)
from msubst2[OF lp nn nn'(1), of x bs ] H(3) nn'
have "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and>
@@ -3862,7 +3772,7 @@
proof
assume H: ?lhs
then have z: "\<lparr>C (-2, 1) *\<^sub>p b *\<^sub>p d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>C (-2, 1) *\<^sub>p d *\<^sub>p b\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
- by (auto simp add: msubst2_def lt[OF stupid(3)] lt[OF stupid(1)]
+ by (auto simp: msubst2_def lt[OF stupid(3)] lt[OF stupid(1)]
mult_less_0_iff zero_less_mult_iff)
from msubst2[OF lq norm2(1) z(1), of x bs] msubst2[OF lq norm2(2) z(2), of x bs] H
show ?rhs
@@ -3870,7 +3780,7 @@
next
assume H: ?rhs
then have z: "\<lparr>C (-2, 1) *\<^sub>p b *\<^sub>p d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>C (-2, 1) *\<^sub>p d *\<^sub>p b\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
- by (auto simp add: msubst2_def lt[OF stupid(4)] lt[OF stupid(2)]
+ by (auto simp: msubst2_def lt[OF stupid(4)] lt[OF stupid(2)]
mult_less_0_iff zero_less_mult_iff)
from msubst2[OF lq norm2(1) z(1), of x bs] msubst2[OF lq norm2(2) z(2), of x bs] H
show ?lhs
@@ -3898,13 +3808,16 @@
also have "\<dots> \<longleftrightarrow> ?I ?R"
by (simp add: list_disj_def evaldjf_ex split_def)
also have "\<dots> \<longleftrightarrow> ?rhs"
- unfolding ferrack2_def
- apply (cases "?mp = T")
- apply (simp add: list_disj_def)
- apply (cases "?pp = T")
- apply (simp add: list_disj_def)
- apply (simp_all add: Let_def decr0[OF nb])
- done
+ proof (cases "?mp = T \<or> ?pp = T")
+ case True
+ then show ?thesis
+ unfolding ferrack2_def
+ by (force simp add: ferrack2_def list_disj_def)
+ next
+ case False
+ then show ?thesis
+ by (simp add: ferrack2_def Let_def decr0[OF nb])
+ qed
finally show ?thesis using decr0_qf[OF nb]
by (simp add: ferrack2_def Let_def)
qed
@@ -3915,7 +3828,7 @@
have this: "\<forall>bs p. qfree p \<longrightarrow> qfree (ferrack2 p) \<and> Ifm vs bs (ferrack2 p) = Ifm vs bs (E p)"
by blast
from qelim[OF this, of "prep p" bs] show ?thesis
- unfolding frpar2_def by (auto simp add: prep)
+ unfolding frpar2_def by (auto simp: prep)
qed
oracle frpar_oracle =
@@ -4092,57 +4005,9 @@
\<close> "parametric QE for linear Arithmetic over fields, Version 2"
lemma "\<exists>(x::'a::linordered_field). y \<noteq> -1 \<longrightarrow> (y + 1) * x < 0"
- apply (frpar type: 'a pars: y)
- apply (simp add: field_simps)
- apply (rule spec[where x=y])
- apply (frpar type: 'a pars: "z::'a")
- apply simp
- done
+ by (metis mult.commute neg_less_0_iff_less nonzero_divide_eq_eq sum_eq zero_less_two)
lemma "\<exists>(x::'a::linordered_field). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
- apply (frpar2 type: 'a pars: y)
- apply (simp add: field_simps)
- apply (rule spec[where x=y])
- apply (frpar2 type: 'a pars: "z::'a")
- apply simp
- done
-
-text \<open>Collins/Jones Problem\<close>
-(*
-lemma "\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
-proof -
- have "(\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
-by (simp add: field_simps)
-have "?rhs"
-
- apply (frpar type: "'a::{linordered_field, number_ring}" pars: "a::'a::{linordered_field, number_ring}" "b::'a::{linordered_field, number_ring}")
- apply (simp add: field_simps)
-oops
-*)
-(*
-lemma "ALL (x::'a::{linordered_field, number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
-apply (frpar type: "'a::{linordered_field, number_ring}" pars: "t::'a::{linordered_field, number_ring}")
-oops
-*)
-
-text \<open>Collins/Jones Problem\<close>
-
-(*
-lemma "\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
-proof -
- have "(\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
-by (simp add: field_simps)
-have "?rhs"
- apply (frpar2 type: "'a::{linordered_field, number_ring}" pars: "a::'a::{linordered_field, number_ring}" "b::'a::{linordered_field, number_ring}")
- apply simp
-oops
-*)
-
-(*
-lemma "ALL (x::'a::{linordered_field, number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
-apply (frpar2 type: "'a::{linordered_field, number_ring}" pars: "t::'a::{linordered_field, number_ring}")
-apply (simp add: field_simps linorder_neq_iff[symmetric])
-apply ferrack
-oops
-*)
+ by (metis mult.right_neutral mult_minus1_right neg_0_le_iff_le nle_le not_less sum_eq)
+
end
--- a/src/HOL/Decision_Procs/Polynomial_List.thy Thu Apr 11 18:46:49 2024 +0000
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy Fri Apr 12 22:19:27 2024 +0100
@@ -5,7 +5,8 @@
section \<open>Univariate Polynomials as lists\<close>
theory Polynomial_List
-imports Complex_Main
+ imports Complex_Main
+
begin
text \<open>Application of polynomial as a function.\<close>
@@ -264,13 +265,9 @@
by blast
have "r = 0"
using p0 by (simp only: Cons qr poly_mult poly_add) simp
- with Cons qr show ?thesis
- apply -
- apply (rule exI[where x = q])
- apply auto
- apply (cases q)
- apply auto
- done
+ with Cons qr have "p = [- a, 1] *** q"
+ by (simp add: local.padd_commut)
+ then show ?thesis ..
qed
ultimately show ?thesis using Cons by blast
qed
@@ -344,11 +341,8 @@
by blast
from y have "y = a \<or> poly q y = 0"
by (simp only: q poly_mult_eq_zero_disj poly_add) (simp add: algebra_simps)
- with i[of y] y(1) y(2) show ?thesis
- apply auto
- apply (erule_tac x = "m" in allE)
- apply auto
- done
+ with i[of y] y show ?thesis
+ using le_Suc_eq by auto
qed
then show ?case by blast
qed
@@ -360,12 +354,7 @@
lemma (in idom) poly_roots_finite_lemma1:
"poly p x \<noteq> poly [] x \<Longrightarrow> \<exists>N i. \<forall>x. poly p x = 0 \<longrightarrow> (\<exists>n::nat. n < N \<and> x = i n)"
- apply (drule poly_roots_index_length)
- apply safe
- apply (rule_tac x = "Suc (length p)" in exI)
- apply (rule_tac x = i in exI)
- apply (simp add: less_Suc_eq_le)
- done
+ by (metis le_imp_less_Suc poly_roots_index_length)
lemma (in idom) idom_finite_lemma:
assumes "\<forall>x. P x \<longrightarrow> (\<exists>n. n < length j \<and> x = j!n)"
@@ -379,15 +368,8 @@
lemma (in idom) poly_roots_finite_lemma2:
"poly p x \<noteq> poly [] x \<Longrightarrow> \<exists>i. \<forall>x. poly p x = 0 \<longrightarrow> x \<in> set i"
- apply (drule poly_roots_index_length)
- apply safe
- apply (rule_tac x = "map (\<lambda>n. i n) [0 ..< Suc (length p)]" in exI)
- apply (auto simp add: image_iff)
- apply (erule_tac x="x" in allE)
- apply clarsimp
- apply (case_tac "n = length p")
- apply (auto simp add: order_le_less)
- done
+ using poly_roots_index_length atMost_iff atMost_upto imageI set_map
+ by metis
lemma (in ring_char_0) UNIV_ring_char_0_infinte: "\<not> finite (UNIV :: 'a set)"
proof
@@ -408,21 +390,12 @@
(is "?lhs \<longleftrightarrow> ?rhs")
proof
show ?rhs if ?lhs
- using that
- apply -
- apply (erule contrapos_np)
- apply (rule ext)
- apply (rule ccontr)
- apply (clarify dest!: poly_roots_finite_lemma2)
- using finite_subset
proof -
- fix x i
- assume F: "\<not> finite {x. poly p x = 0}"
- and P: "\<forall>x. poly p x = 0 \<longrightarrow> x \<in> set i"
- from P have "{x. poly p x = 0} \<subseteq> set i"
- by auto
- with finite_subset F show False
- by auto
+ have False if F: "\<not> finite {x. poly p x = 0}"
+ and P: "\<forall>x. poly p x = 0 \<longrightarrow> x \<in> set i" for i
+ by (smt (verit, del_insts) in_set_conv_nth local.idom_finite_lemma that)
+ with that show ?thesis
+ using local.poly_roots_finite_lemma2 by blast
qed
show ?lhs if ?rhs
using UNIV_ring_char_0_infinte that by auto
@@ -473,18 +446,15 @@
qed
lemma (in idom) poly_exp_eq_zero[simp]: "poly (p %^ n) = poly [] \<longleftrightarrow> poly p = poly [] \<and> n \<noteq> 0"
- apply (simp only: fun_eq_iff add: HOL.all_simps [symmetric])
- apply (rule arg_cong [where f = All])
- apply (rule ext)
- apply (induct n)
- apply (auto simp add: poly_exp poly_mult)
- done
+ by (simp add: local.poly_exp fun_eq_iff)
lemma (in comm_ring_1) poly_prime_eq_zero[simp]: "poly [a, 1] \<noteq> poly []"
- apply (simp add: fun_eq_iff)
- apply (rule_tac x = "minus one a" in exI)
- apply (simp add: add.commute [of a])
- done
+proof -
+ have "\<exists>x. a + x \<noteq> 0"
+ by (metis add_cancel_left_right zero_neq_one)
+ then show ?thesis
+ by (simp add: fun_eq_iff)
+qed
lemma (in idom) poly_exp_prime_eq_zero: "poly ([a, 1] %^ n) \<noteq> poly []"
by auto
@@ -492,26 +462,18 @@
text \<open>A more constructive notion of polynomials being trivial.\<close>
-lemma (in idom_char_0) poly_zero_lemma': "poly (h # t) = poly [] \<Longrightarrow> h = 0 \<and> poly t = poly []"
- apply (simp add: fun_eq_iff)
- apply (case_tac "h = zero")
- apply (drule_tac [2] x = zero in spec)
- apply auto
- apply (cases "poly t = poly []")
- apply simp
+lemma (in idom_char_0) poly_zero_lemma':
+ assumes "poly (h # t) = poly []" shows "h = 0 \<and> poly t = poly []"
proof -
- fix x
- assume H: "\<forall>x. x = 0 \<or> poly t x = 0"
- assume pnz: "poly t \<noteq> poly []"
- let ?S = "{x. poly t x = 0}"
- from H have "\<forall>x. x \<noteq> 0 \<longrightarrow> poly t x = 0"
- by blast
- then have th: "?S \<supseteq> UNIV - {0}"
- by auto
- from poly_roots_finite pnz have th': "finite ?S"
- by blast
- from finite_subset[OF th th'] UNIV_ring_char_0_infinte show "poly t x = 0"
- by simp
+ have "poly t x = 0" if H: "\<forall>x. x = 0 \<or> poly t x = 0" and pnz: "poly t \<noteq> poly []" for x
+ proof -
+ from H have "{x. poly t x = 0} \<supseteq> UNIV - {0}"
+ by auto
+ then show ?thesis
+ using finite_subset local.poly_roots_finite pnz by fastforce
+ qed
+ with assms show ?thesis
+ by (simp add: fun_eq_iff) (metis add_cancel_right_left mult_eq_0_iff)
qed
lemma (in idom_char_0) poly_zero: "poly p = poly [] \<longleftrightarrow> (\<forall>c \<in> set p. c = 0)"
@@ -520,12 +482,8 @@
then show ?case by simp
next
case Cons
- show ?case
- apply (rule iffI)
- apply (drule poly_zero_lemma')
- using Cons
- apply auto
- done
+ then show ?case
+ by (smt (verit) list.set_intros pmult_by_x poly_entire poly_zero_lemma' set_ConsD)
qed
lemma (in idom_char_0) poly_0: "\<forall>c \<in> set p. c = 0 \<Longrightarrow> poly p x = 0"
@@ -535,41 +493,33 @@
text \<open>Basics of divisibility.\<close>
lemma (in idom) poly_primes: "[a, 1] divides (p *** q) \<longleftrightarrow> [a, 1] divides p \<or> [a, 1] divides q"
- apply (auto simp add: divides_def fun_eq_iff poly_mult poly_add poly_cmult distrib_right [symmetric])
- apply (drule_tac x = "uminus a" in spec)
- apply (simp add: poly_linear_divides poly_add poly_cmult distrib_right [symmetric])
- apply (cases "p = []")
- apply (rule exI[where x="[]"])
- apply simp
- apply (cases "q = []")
- apply (erule allE[where x="[]"])
- apply simp
-
- apply clarsimp
- apply (cases "\<exists>q. p = a %* q +++ (0 # q)")
- apply (clarsimp simp add: poly_add poly_cmult)
- apply (rule_tac x = qa in exI)
- apply (simp add: distrib_right [symmetric])
- apply clarsimp
-
- apply (auto simp add: poly_linear_divides poly_add poly_cmult distrib_right [symmetric])
- apply (rule_tac x = "pmult qa q" in exI)
- apply (rule_tac [2] x = "pmult p qa" in exI)
- apply (auto simp add: poly_add poly_mult poly_cmult ac_simps)
- done
+proof -
+ have "\<exists>q. \<forall>x. poly p x = (a + x) * poly q x"
+ if "poly p (uminus a) * poly q (uminus a) = (a + (uminus a)) * poly qa (uminus a)"
+ and "\<forall>qa. \<exists>x. poly q x \<noteq> (a + x) * poly qa x"
+ for qa
+ using that
+ apply (simp add: poly_linear_divides poly_add)
+ by (metis add_cancel_left_right combine_common_factor mult_eq_0_iff poly.poly_Cons poly.poly_Nil poly_add poly_cmult)
+ moreover have "\<exists>qb. \<forall>x. (a + x) * poly qa x * poly q x = (a + x) * poly qb x" for qa
+ by (metis local.poly_mult mult_assoc)
+ moreover have "\<exists>q. \<forall>x. poly p x * ((a + x) * poly qa x) = (a + x) * poly q x" for qa
+ by (metis mult.left_commute local.poly_mult)
+ ultimately show ?thesis
+ by (auto simp: divides_def divisors_zero fun_eq_iff poly_mult poly_add poly_cmult simp flip: distrib_right)
+qed
lemma (in comm_semiring_1) poly_divides_refl[simp]: "p divides p"
- apply (simp add: divides_def)
- apply (rule_tac x = "[one]" in exI)
- apply (auto simp add: poly_mult fun_eq_iff)
- done
+proof -
+ have "poly p = poly (p *** [1])"
+ by (auto simp add: poly_mult fun_eq_iff)
+ then show ?thesis
+ using local.dividesI by blast
+qed
lemma (in comm_semiring_1) poly_divides_trans: "p divides q \<Longrightarrow> q divides r \<Longrightarrow> p divides r"
- apply (simp add: divides_def)
- apply safe
- apply (rule_tac x = "pmult qa qaa" in exI)
- apply (auto simp add: poly_mult fun_eq_iff mult.assoc)
- done
+ unfolding divides_def
+ by (metis ext local.poly_mult local.poly_mult_assoc)
lemma (in comm_semiring_1) poly_divides_exp: "m \<le> n \<Longrightarrow> (p %^ m) divides (p %^ n)"
by (auto simp: le_iff_add divides_def poly_exp_add fun_eq_iff)
@@ -577,34 +527,35 @@
lemma (in comm_semiring_1) poly_exp_divides: "(p %^ n) divides q \<Longrightarrow> m \<le> n \<Longrightarrow> (p %^ m) divides q"
by (blast intro: poly_divides_exp poly_divides_trans)
-lemma (in comm_semiring_0) poly_divides_add: "p divides q \<Longrightarrow> p divides r \<Longrightarrow> p divides (q +++ r)"
- apply (auto simp add: divides_def)
- apply (rule_tac x = "padd qa qaa" in exI)
- apply (auto simp add: poly_add fun_eq_iff poly_mult distrib_left)
- done
+lemma (in comm_semiring_0) poly_divides_add:
+ assumes "p divides q" and "p divides r" shows "p divides (q +++ r)"
+proof -
+ have "\<And>qa qb. \<lbrakk>poly q = poly (p *** qa); poly r = poly (p *** qb)\<rbrakk>
+ \<Longrightarrow> poly (q +++ r) = poly (p *** (qa +++ qb))"
+ by (auto simp add: poly_add fun_eq_iff poly_mult distrib_left)
+ with assms show ?thesis
+ by (auto simp add: divides_def)
+qed
-lemma (in comm_ring_1) poly_divides_diff: "p divides q \<Longrightarrow> p divides (q +++ r) \<Longrightarrow> p divides r"
- apply (auto simp add: divides_def)
- apply (rule_tac x = "padd qaa (poly_minus qa)" in exI)
- apply (auto simp add: poly_add fun_eq_iff poly_mult poly_minus algebra_simps)
- done
+lemma (in comm_ring_1) poly_divides_diff:
+ assumes "p divides q" and "p divides (q +++ r)"
+ shows "p divides r"
+proof -
+ have "\<And>qa qb. \<lbrakk>poly q = poly (p *** qa); poly (q +++ r) = poly (p *** qb)\<rbrakk>
+ \<Longrightarrow> poly r = poly (p *** (qb +++ -- qa))"
+ by (auto simp add: poly_add fun_eq_iff poly_mult poly_minus algebra_simps)
+ with assms show ?thesis
+ by (auto simp add: divides_def)
+qed
lemma (in comm_ring_1) poly_divides_diff2: "p divides r \<Longrightarrow> p divides (q +++ r) \<Longrightarrow> p divides q"
- apply (erule poly_divides_diff)
- apply (auto simp add: poly_add fun_eq_iff poly_mult divides_def ac_simps)
- done
+ by (metis local.padd_commut local.poly_divides_diff)
lemma (in semiring_0) poly_divides_zero: "poly p = poly [] \<Longrightarrow> q divides p"
- apply (simp add: divides_def)
- apply (rule exI[where x = "[]"])
- apply (auto simp add: fun_eq_iff poly_mult)
- done
+ by (metis ext dividesI poly.poly_Nil poly_mult_Nil2)
lemma (in semiring_0) poly_divides_zero2 [simp]: "q divides []"
- apply (simp add: divides_def)
- apply (rule_tac x = "[]" in exI)
- apply (auto simp add: fun_eq_iff)
- done
+ using local.poly_divides_zero by force
text \<open>At last, we can consider the order of a root.\<close>
@@ -629,11 +580,7 @@
from True[unfolded poly_linear_divides] pN obtain q where q: "p = [-a, 1] *** q"
by blast
from q h True have qh: "length q = n" "poly q \<noteq> poly []"
- apply simp_all
- apply (simp only: fun_eq_iff)
- apply (rule ccontr)
- apply (simp add: fun_eq_iff poly_add poly_cmult)
- done
+ using h(2) local.poly_entire q by fastforce+
from Suc.hyps[OF qh] obtain m r where mr: "q = mulexp m [-a,1] r" "poly r a \<noteq> 0"
by blast
from mr q have "p = mulexp (Suc m) [-a,1] r \<and> poly r a \<noteq> 0"
@@ -641,12 +588,8 @@
then show ?thesis by blast
next
case False
- then show ?thesis
- using Suc.prems
- apply simp
- apply (rule exI[where x="0::nat"])
- apply simp
- done
+ with Suc.prems show ?thesis
+ by (smt (verit, best) local.mulexp.mulexp_zero)
qed
qed
@@ -719,12 +662,7 @@
lemma (in idom_char_0) poly_order:
"poly p \<noteq> poly [] \<Longrightarrow> \<exists>!n. ([-a, 1] %^ n) divides p \<and> \<not> (([-a, 1] %^ Suc n) divides p)"
- apply (auto intro: poly_order_exists simp add: less_linear simp del: pmult_Cons pexp_Suc)
- apply (cut_tac x = y and y = n in less_linear)
- apply (drule_tac m = n in poly_exp_divides)
- apply (auto dest: Suc_le_eq [THEN iffD2, THEN [2] poly_exp_divides]
- simp del: pmult_Cons pexp_Suc)
- done
+ by (meson Suc_le_eq linorder_neqE_nat local.poly_exp_divides poly_order_exists)
text \<open>Order\<close>
@@ -736,10 +674,7 @@
"([-a, 1] %^ n) divides p \<and> \<not> (([-a, 1] %^ Suc n) divides p) \<longleftrightarrow>
n = order a p \<and> poly p \<noteq> poly []"
unfolding order_def
- apply (rule iffI)
- apply (blast dest: poly_divides_zero intro!: some1_equality [symmetric] poly_order)
- apply (blast intro!: poly_order [THEN [2] some1_equalityD])
- done
+ by (metis (no_types, lifting) local.poly_divides_zero local.poly_order someI)
lemma (in idom_char_0) order2:
"poly p \<noteq> poly [] \<Longrightarrow>
@@ -767,97 +702,89 @@
by (induct n arbitrary: a p) (auto simp add: divides_def poly_mult simp del: pmult_Cons)
lemma (in idom_char_0) order_root: "poly p a = 0 \<longleftrightarrow> poly p = poly [] \<or> order a p \<noteq> 0"
- apply (cases "poly p = poly []")
- apply auto
- apply (simp add: poly_linear_divides del: pmult_Cons)
- apply safe
- apply (drule_tac [!] a = a in order2)
- apply (rule ccontr)
- apply (simp add: divides_def poly_mult fun_eq_iff del: pmult_Cons)
- apply blast
- using neq0_conv apply (blast intro: lemma_order_root)
- done
+proof (cases "poly p = poly []")
+ case False
+ then show ?thesis
+ by (metis (mono_tags, lifting) dividesI lemma_order_root order2 pexp_one poly_linear_divides neq0_conv)
+qed auto
lemma (in idom_char_0) order_divides:
"([-a, 1] %^ n) divides p \<longleftrightarrow> poly p = poly [] \<or> n \<le> order a p"
- apply (cases "poly p = poly []")
- apply auto
- apply (simp add: divides_def fun_eq_iff poly_mult)
- apply (rule_tac x = "[]" in exI)
- apply (auto dest!: order2 [where a=a] intro: poly_exp_divides simp del: pexp_Suc)
- done
+proof (cases "poly p = poly []")
+ case True
+ then show ?thesis
+ using local.poly_divides_zero by force
+next
+ case False
+ then show ?thesis
+ by (meson local.order2 local.poly_exp_divides not_less_eq_eq)
+qed
lemma (in idom_char_0) order_decomp:
- "poly p \<noteq> poly [] \<Longrightarrow> \<exists>q. poly p = poly (([-a, 1] %^ order a p) *** q) \<and> \<not> [-a, 1] divides q"
- unfolding divides_def
- apply (drule order2 [where a = a])
- apply (simp add: divides_def del: pexp_Suc pmult_Cons)
- apply safe
- apply (rule_tac x = q in exI)
- apply safe
- apply (drule_tac x = qa in spec)
- apply (auto simp add: poly_mult fun_eq_iff poly_exp ac_simps simp del: pmult_Cons)
- done
+ assumes "poly p \<noteq> poly []"
+ shows "\<exists>q. poly p = poly (([-a, 1] %^ order a p) *** q) \<and> \<not> [-a, 1] divides q"
+proof -
+ obtain q where q: "poly p = poly ([- a, 1] %^ order a p *** q)"
+ using assms local.order2 divides_def by blast
+ have False if "poly q = poly ([- a, 1] *** qa)" for qa
+ proof -
+ have "poly p \<noteq> poly ([- a, 1] %^ Suc (order a p) *** qa)"
+ using assms local.divides_def local.order2 by blast
+ with q that show False
+ by (auto simp add: poly_mult ac_simps simp del: pmult_Cons)
+ qed
+ with q show ?thesis
+ unfolding divides_def by blast
+qed
text \<open>Important composition properties of orders.\<close>
lemma order_mult:
fixes a :: "'a::idom_char_0"
- shows "poly (p *** q) \<noteq> poly [] \<Longrightarrow> order a (p *** q) = order a p + order a q"
- apply (cut_tac a = a and p = "p *** q" and n = "order a p + order a q" in order)
- apply (auto simp add: poly_entire simp del: pmult_Cons)
- apply (drule_tac a = a in order2)+
- apply safe
- apply (simp add: divides_def fun_eq_iff poly_exp_add poly_mult del: pmult_Cons, safe)
- apply (rule_tac x = "qa *** qaa" in exI)
- apply (simp add: poly_mult ac_simps del: pmult_Cons)
- apply (drule_tac a = a in order_decomp)+
- apply safe
- apply (subgoal_tac "[-a, 1] divides (qa *** qaa) ")
- apply (simp add: poly_primes del: pmult_Cons)
- apply (auto simp add: divides_def simp del: pmult_Cons)
- apply (rule_tac x = qb in exI)
- apply (subgoal_tac "poly ([-a, 1] %^ (order a p) *** (qa *** qaa)) =
- poly ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))")
- apply (drule poly_mult_left_cancel [THEN iffD1])
- apply force
- apply (subgoal_tac "poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** (qa *** qaa))) =
- poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))) ")
- apply (drule poly_mult_left_cancel [THEN iffD1])
- apply force
- apply (simp add: fun_eq_iff poly_exp_add poly_mult ac_simps del: pmult_Cons)
- done
-
-lemma (in idom_char_0) order_mult:
assumes "poly (p *** q) \<noteq> poly []"
shows "order a (p *** q) = order a p + order a q"
- using assms
- apply (cut_tac a = a and p = "pmult p q" and n = "order a p + order a q" in order)
- apply (auto simp add: poly_entire simp del: pmult_Cons)
- apply (drule_tac a = a in order2)+
- apply safe
- apply (simp add: divides_def fun_eq_iff poly_exp_add poly_mult del: pmult_Cons)
- apply safe
- apply (rule_tac x = "pmult qa qaa" in exI)
- apply (simp add: poly_mult ac_simps del: pmult_Cons)
- apply (drule_tac a = a in order_decomp)+
- apply safe
- apply (subgoal_tac "[uminus a, one] divides pmult qa qaa")
- apply (simp add: poly_primes del: pmult_Cons)
- apply (auto simp add: divides_def simp del: pmult_Cons)
- apply (rule_tac x = qb in exI)
- apply (subgoal_tac "poly (pmult (pexp [uminus a, one] (order a p)) (pmult qa qaa)) =
- poly (pmult (pexp [uminus a, one] (order a p)) (pmult [uminus a, one] qb))")
- apply (drule poly_mult_left_cancel [THEN iffD1], force)
- apply (subgoal_tac "poly (pmult (pexp [uminus a, one] (order a q))
- (pmult (pexp [uminus a, one] (order a p)) (pmult qa qaa))) =
- poly (pmult (pexp [uminus a, one] (order a q))
- (pmult (pexp [uminus a, one] (order a p)) (pmult [uminus a, one] qb)))")
- apply (drule poly_mult_left_cancel [THEN iffD1], force)
- apply (simp add: fun_eq_iff poly_exp_add poly_mult ac_simps del: pmult_Cons)
- done
+proof -
+ have p: "poly p \<noteq> poly []" and q: "poly q \<noteq> poly []"
+ using assms poly_entire by auto
+ obtain p' where p':
+ "\<And>x. poly p x = poly ([- a, 1] %^ order a p) x * poly p' x"
+ "\<not> [- a, 1] divides p'"
+ by (metis order_decomp p poly_mult)
+ obtain q' where q':
+ "\<And>x. poly q x = poly ([- a, 1] %^ order a q) x * poly q' x"
+ "\<not> [- a, 1] divides q'"
+ by (metis order_decomp q poly_mult)
+ have "[- a, 1] %^ (order a p + order a q) divides (p *** q)"
+ proof -
+ have *: "poly p x * poly q x =
+ poly ([- a, 1] %^ order a p) x * poly ([- a, 1] %^ order a q) x * poly (p' *** q') x" for x
+ using p' q' by (simp add: poly_mult)
+ then show ?thesis
+ unfolding divides_def poly_exp_add poly_mult using * by blast
+ qed
+ moreover have False
+ if pq: "order a (p *** q) \<noteq> order a p + order a q"
+ and dv: "[- a, 1] *** [- a, 1] %^ (order a p + order a q) divides (p *** q)"
+ proof -
+ obtain pq' :: "'a list"
+ where pq': "poly (p *** q) = poly ([- a, 1] *** [- a, 1] %^ (order a p + order a q) *** pq')"
+ using dv unfolding divides_def by auto
+ have "poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** (p' *** q'))) =
+ poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** ([-a, 1] *** pq')))"
+ using p' q' pq pq'
+ by (simp add: fun_eq_iff poly_exp_add poly_mult ac_simps del: pmult_Cons)
+ then have "poly ([-a, 1] %^ (order a p) *** (p' *** q')) = poly ([-a, 1] %^ (order a p) *** ([-a, 1] *** pq'))"
+ by (simp add: poly_mult_left_cancel)
+ then have "[-a, 1] divides (p' *** q')"
+ unfolding divides_def by (meson poly_exp_prime_eq_zero poly_mult_left_cancel)
+ with p' q' show ?thesis
+ by (simp add: poly_primes)
+ qed
+ ultimately show ?thesis
+ by (metis order pexp_Suc)
+qed
lemma (in idom_char_0) order_root2: "poly p \<noteq> poly [] \<Longrightarrow> poly p a = 0 \<longleftrightarrow> order a p \<noteq> 0"
- by (rule order_root [THEN ssubst]) auto
+ using order_root by presburger
lemma (in semiring_1) pmult_one[simp]: "[1] *** p = p"
by auto
@@ -866,21 +793,18 @@
by (simp add: fun_eq_iff)
lemma (in idom_char_0) rsquarefree_decomp:
- "rsquarefree p \<Longrightarrow> poly p a = 0 \<Longrightarrow> \<exists>q. poly p = poly ([-a, 1] *** q) \<and> poly q a \<noteq> 0"
- apply (simp add: rsquarefree_def)
- apply safe
- apply (frule_tac a = a in order_decomp)
- apply (drule_tac x = a in spec)
- apply (drule_tac a = a in order_root2 [symmetric])
- apply (auto simp del: pmult_Cons)
- apply (rule_tac x = q in exI, safe)
- apply (simp add: poly_mult fun_eq_iff)
- apply (drule_tac p1 = q in poly_linear_divides [THEN iffD1])
- apply (simp add: divides_def del: pmult_Cons, safe)
- apply (drule_tac x = "[]" in spec)
- apply (auto simp add: fun_eq_iff)
- done
-
+ assumes "rsquarefree p" and "poly p a = 0"
+ shows "\<exists>q. poly p = poly ([-a, 1] *** q) \<and> poly q a \<noteq> 0"
+proof -
+ have "order a p = Suc 0"
+ using assms local.order_root2 rsquarefree_def by force
+ moreover
+ obtain q where "poly p = poly ([- a, 1] %^ order a p *** q)"
+ "\<not> [- a, 1] divides q"
+ using assms(1) order_decomp rsquarefree_def by blast
+ ultimately show ?thesis
+ using dividesI poly_linear_divides by auto
+qed
text \<open>Normalization of a polynomial.\<close>
@@ -952,28 +876,12 @@
then show ?case
proof (induct p)
case Nil
- then have "poly [] = poly (c # cs)"
- by blast
- then have "poly (c#cs) = poly []"
- by simp
then show ?case
- by (simp only: poly_zero lemma_degree_zero) simp
+ by (metis local.poly_zero_lemma')
next
case (Cons d ds)
- then have eq: "poly (d # ds) = poly (c # cs)"
- by blast
- then have eq': "\<And>x. poly (d # ds) x = poly (c # cs) x"
- by simp
- then have "poly (d # ds) 0 = poly (c # cs) 0"
- by blast
- then have dc: "d = c"
- by auto
- with eq have "poly ds = poly cs"
- unfolding poly_Cons_eq by simp
- with Cons.prems have "pnormalize ds = pnormalize cs"
- by blast
- with dc show ?case
- by simp
+ then show ?case
+ by (metis pnormalize.pnormalize_Cons local.poly_Cons_eq)
qed
qed
@@ -987,15 +895,16 @@
lemma (in semiring_0) last_linear_mul_lemma:
"last ((a %* p) +++ (x # (b %* p))) = (if p = [] then x else b * last p)"
- apply (induct p arbitrary: a x b)
- apply auto
- subgoal for a p c x b
- apply (subgoal_tac "padd (cmult c p) (times b a # cmult b p) \<noteq> []")
- apply simp
- apply (induct p)
- apply auto
- done
- done
+proof (induct p arbitrary: a x b)
+ case Nil
+ then show ?case by auto
+next
+ case (Cons a p c x b)
+ then have "padd (cmult c p) (times b a # cmult b p) \<noteq> []"
+ by (metis local.padd.padd_Nil local.padd_Cons_Cons neq_Nil_conv)
+ then show ?case
+ by (simp add: local.Cons)
+qed
lemma (in semiring_1) last_linear_mul:
assumes p: "p \<noteq> []"
@@ -1051,18 +960,11 @@
case True
then show ?thesis
using degree_unique[OF True] by (simp add: degree_def)
- next
- case False
- then show ?thesis
- by (auto simp add: poly_Nil_ext)
- qed
+ qed (auto simp add: poly_Nil_ext)
next
case (Suc n a p)
have eq: "poly ([a, 1] %^(Suc n) *** p) = poly ([a, 1] %^ n *** ([a, 1] *** p))"
- apply (rule ext)
- apply (simp add: poly_mult poly_add poly_cmult)
- apply (simp add: ac_simps distrib_left)
- done
+ by (force simp add: poly_mult poly_add poly_cmult ac_simps distrib_left)
note deq = degree_unique[OF eq]
show ?case
proof (cases "poly p = poly []")
@@ -1080,9 +982,7 @@
from ap have ap': "poly ([a, 1] *** p) = poly [] \<longleftrightarrow> False"
by blast
have th0: "degree ([a, 1]%^n *** ([a, 1] *** p)) = degree ([a, 1] *** p) + n"
- apply (simp only: Suc.hyps[of a "pmult [a,one] p"] ap')
- apply simp
- done
+ unfolding Suc.hyps[of a "pmult [a,one] p"] ap' by simp
from degree_unique[OF eq] ap False th0 linear_mul_degree[OF False, of a]
show ?thesis
by (auto simp del: poly.simps)
@@ -1118,12 +1018,12 @@
then show ?case by simp
next
case (Cons a p)
- then show ?case
- apply auto
- apply (rule_tac y = "\<bar>a\<bar> + \<bar>x * poly p x\<bar>" in order_trans)
- apply (rule abs_triangle_ineq)
- apply (auto intro!: mult_mono simp add: abs_mult)
- done
+ have "\<bar>a + x * poly p x\<bar> \<le> \<bar>a\<bar> + \<bar>x * poly p x\<bar>"
+ using abs_triangle_ineq by blast
+ also have "\<dots> \<le> \<bar>a\<bar> + k * poly (map abs p) k"
+ by (simp add: Cons.hyps Cons.prems abs_mult mult_mono')
+ finally show ?case
+ using Cons by auto
qed
lemma (in semiring_0) poly_Sing: "poly [c] x = c"