--- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Sun Apr 14 22:38:17 2024 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Mon Apr 15 22:23:40 2024 +0100
@@ -34,43 +34,49 @@
by (cases i) auto
lemma norm_Pinj: "isnorm (Pinj i Q) \<Longrightarrow> isnorm Q"
- by (cases i) (simp add: norm_Pinj_0_False norm_PX_0_False, cases Q, auto)
+ using isnorm.elims(2) by fastforce
lemma norm_PX2: "isnorm (PX P i Q) \<Longrightarrow> isnorm Q"
- apply (cases i)
- apply auto
- apply (cases P)
- apply auto
- subgoal for \<dots> pol2 by (cases pol2) auto
- done
+ using isnorm.elims(1) by auto
+
+lemma norm_PX1: assumes "isnorm (PX P i Q)" shows "isnorm P"
+proof (cases P)
+ case (Pc x1)
+ then show ?thesis
+ by auto
+qed (use assms isnorm.elims(1) in auto)
-lemma norm_PX1: "isnorm (PX P i Q) \<Longrightarrow> isnorm P"
- apply (cases i)
- apply auto
- apply (cases P)
- apply auto
- subgoal for \<dots> pol2 by (cases pol2) auto
- done
-
-lemma mkPinj_cn: "y \<noteq> 0 \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (mkPinj y Q)"
- apply (auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split)
- apply (rename_tac nat a, case_tac nat, auto simp add: norm_Pinj_0_False)
- apply (rename_tac pol a, case_tac pol, auto)
- apply (case_tac y, auto)
- done
+lemma mkPinj_cn:
+ assumes "y \<noteq> 0" and "isnorm Q"
+ shows "isnorm (mkPinj y Q)"
+proof (cases Q)
+ case Pc
+ with assms show ?thesis
+ by (simp add: mkPinj_def)
+next
+ case Pinj
+ with assms show ?thesis
+ using isnorm.elims(2) isnorm.simps(5) mkPinj_def by fastforce
+next
+ case PX
+ with assms show ?thesis
+ using isnorm.elims(1) mkPinj_def by auto
+qed
lemma norm_PXtrans:
- assumes A: "isnorm (PX P x Q)"
+ assumes "isnorm (PX P x Q)" and "isnorm Q2"
+ shows "isnorm (PX P x Q2)"
+ using assms isnorm.elims(3) by fastforce
+
+
+lemma norm_PXtrans2:
+ assumes "isnorm (PX P x Q)"
and "isnorm Q2"
- shows "isnorm (PX P x Q2)"
+ shows "isnorm (PX P (Suc (n + x)) Q2)"
proof (cases P)
case (PX p1 y p2)
with assms show ?thesis
- apply (cases x)
- apply auto
- apply (cases p2)
- apply auto
- done
+ using isnorm.elims(2) by fastforce
next
case Pc
with assms show ?thesis
@@ -81,29 +87,7 @@
by (cases x) auto
qed
-lemma norm_PXtrans2:
- assumes "isnorm (PX P x Q)"
- and "isnorm Q2"
- shows "isnorm (PX P (Suc (n + x)) Q2)"
-proof (cases P)
- case (PX p1 y p2)
- with assms show ?thesis
- apply (cases x)
- apply auto
- apply (cases p2)
- apply auto
- done
-next
- case Pc
- with assms show ?thesis
- by (cases x) auto
-next
- case Pinj
- with assms show ?thesis
- by (cases x) auto
-qed
-
-text \<open>\<open>mkPX\<close> conserves normalizedness (\<open>_cn\<close>)\<close>
+text \<open>\<open>mkPX\<close> preserves the normal property (\<open>_cn\<close>)\<close>
lemma mkPX_cn:
assumes "x \<noteq> 0"
and "isnorm P"
@@ -124,14 +108,23 @@
from assms PX have "isnorm P1" "isnorm P2"
by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2])
from assms PX Y0 show ?thesis
- apply (cases x)
- apply (auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _])
- apply (cases P2)
- apply auto
- done
+ proof (cases P2)
+ case (Pc x1)
+ then show ?thesis
+ using assms gr0_conv_Suc PX by (auto simp add: mkPX_def norm_PXtrans2)
+ next
+ case (Pinj x21 x22)
+ with assms gr0_conv_Suc PX show ?thesis
+ by (auto simp: mkPX_def)
+ next
+ case (PX x31 x32 x33)
+ with assms gr0_conv_Suc \<open>P = PX P1 y P2\<close>
+ show ?thesis
+ using assms PX by (auto simp add: mkPX_def norm_PXtrans2)
+ qed
qed
-text \<open>\<open>add\<close> conserves normalizedness\<close>
+text \<open>\<open>add\<close> preserves the normal property\<close>
lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<langle>+\<rangle> Q)"
proof (induct P Q rule: add.induct)
case 1
@@ -139,41 +132,23 @@
next
case (2 c i P2)
then show ?case
- apply (cases P2)
- apply simp_all
- apply (cases i)
- apply simp_all
- done
+ using isnorm.elims(2) by fastforce
next
case (3 i P2 c)
then show ?case
- apply (cases P2)
- apply simp_all
- apply (cases i)
- apply simp_all
- done
+ using isnorm.elims(2) by fastforce
next
case (4 c P2 i Q2)
then have "isnorm P2" "isnorm Q2"
by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
with 4 show ?case
- apply (cases i)
- apply simp
- apply (cases P2)
- apply auto
- subgoal for \<dots> pol2 by (cases pol2) auto
- done
+ using isnorm.elims(2) by fastforce
next
case (5 P2 i Q2 c)
then have "isnorm P2" "isnorm Q2"
by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
with 5 show ?case
- apply (cases i)
- apply simp
- apply (cases P2)
- apply auto
- subgoal for \<dots> pol2 by (cases pol2) auto
- done
+ using isnorm.elims(2) by fastforce
next
case (6 x P2 y Q2)
then have Y0: "y > 0"
@@ -336,39 +311,19 @@
next
case (2 c i P2)
then show ?case
- apply (cases P2)
- apply simp_all
- apply (cases i)
- apply (simp_all add: mkPinj_cn)
- done
+ by (metis mkPinj_cn mul.simps(2) norm_Pinj norm_Pinj_0_False)
next
case (3 i P2 c)
then show ?case
- apply (cases P2)
- apply simp_all
- apply (cases i)
- apply (simp_all add: mkPinj_cn)
- done
+ by (metis mkPinj_cn mul.simps(3) norm_Pinj norm_Pinj_0_False)
next
case (4 c P2 i Q2)
- then have "isnorm P2" "isnorm Q2"
- by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
- with 4 show ?case
- apply (cases "c = 0")
- apply simp_all
- apply (cases "i = 0")
- apply (simp_all add: mkPX_cn)
- done
+ then show ?case
+ by (metis isnorm.simps(6) mkPX_cn mul.simps(4) norm_PX1 norm_PX2)
next
case (5 P2 i Q2 c)
- then have "isnorm P2" "isnorm Q2"
- by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
- with 5 show ?case
- apply (cases "c = 0")
- apply simp_all
- apply (cases "i = 0")
- apply (simp_all add: mkPX_cn)
- done
+ then show ?case
+ by (metis isnorm.simps(6) mkPX_cn mul.simps(5) norm_PX1 norm_PX2)
next
case (6 x P2 y Q2)
consider "x < y" | "x = y" | "x > y" by arith
@@ -382,11 +337,8 @@
from 6 have **: "isnorm P2" "isnorm Q2"
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
from 6 xy y have "isnorm (Pinj d Q2)"
- apply (cases d)
- apply simp
- apply (cases Q2)
- apply auto
- done
+ apply simp
+ by (smt (verit, ccfv_SIG) "**"(2) Suc_pred isnorm.elims(1) isnorm.simps(2) isnorm.simps(3) isnorm.simps(5))
with 6 * ** y show ?thesis
by (simp add: mkPinj_cn)
next
@@ -405,12 +357,9 @@
by (cases y) (auto simp add: norm_Pinj_0_False)
from 6 have **: "isnorm P2" "isnorm Q2"
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
- from 6 xy x have "isnorm (Pinj d P2)"
- apply (cases d)
+ with 6 xy x have "isnorm (Pinj d P2)"
apply simp
- apply (cases P2)
- apply auto
- done
+ by (smt (verit, ccfv_SIG) Suc_pred isnorm.elims(1) isnorm.simps(2) isnorm.simps(3) isnorm.simps(5))
with 6 xy * ** x show ?thesis
by (simp add: mkPinj_cn)
qed
@@ -493,7 +442,7 @@
by (simp add: add_cn)
qed
-text \<open>neg conserves normalizedness\<close>
+text \<open>neg preserves the normal property\<close>
lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"
proof (induct P)
case Pc
@@ -520,7 +469,7 @@
qed (cases x, auto)
qed
-text \<open>sub conserves normalizedness\<close>
+text \<open>sub preserves the normal property\<close>
lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<langle>-\<rangle> q)"
by (simp add: sub_def add_cn neg_cn)
@@ -532,11 +481,7 @@
next
case (Pinj i Q)
then show ?case
- apply (cases Q)
- apply (auto simp add: mkPX_cn mkPinj_cn)
- apply (cases i)
- apply (auto simp add: mkPX_cn mkPinj_cn)
- done
+ by (metis Commutative_Ring.sqr.simps(2) mkPinj_cn norm_Pinj norm_Pinj_0_False)
next
case (PX P1 x P2)
then have "x + x \<noteq> 0" "isnorm P2" "isnorm P1"
@@ -548,7 +493,7 @@
by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
qed
-text \<open>\<open>pow\<close> conserves normalizedness\<close>
+text \<open>\<open>pow\<close> preserves the normal property\<close>
lemma pow_cn: "isnorm P \<Longrightarrow> isnorm (pow n P)"
proof (induct n arbitrary: P rule: less_induct)
case (less k)
--- a/src/HOL/Decision_Procs/MIR.thy Sun Apr 14 22:38:17 2024 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Mon Apr 15 22:23:40 2024 +0100
@@ -73,10 +73,7 @@
qed
lemma rdvd_minus: "(real_of_int (d::int) rdvd t) = (real_of_int d rdvd -t)"
- apply (auto simp add: rdvd_def)
- apply (rule_tac x="-k" in exI, simp)
- apply (rule_tac x="-k" in exI, simp)
- done
+ by (metis equation_minus_iff mult_minus_right of_int_minus rdvd_def)
lemma rdvd_left_0_eq: "(0 rdvd t) = (t=0)"
by (auto simp add: rdvd_def)
@@ -459,24 +456,18 @@
by (induct ps) (simp_all add: evaldjf_def djf_Or)
lemma evaldjf_bound0:
- assumes nb: "\<forall> x\<in> set xs. bound0 (f x)"
+ assumes "\<forall>x \<in> set xs. bound0 (f x)"
shows "bound0 (evaldjf f xs)"
- using nb
- apply (induct xs)
- apply (auto simp add: evaldjf_def djf_def Let_def)
- apply (case_tac "f a")
- apply auto
- done
+ using assms
+ by (induct xs) (auto simp add: evaldjf_def djf_def Let_def split: fm.split)
+
lemma evaldjf_qf:
- assumes nb: "\<forall> x\<in> set xs. qfree (f x)"
+ assumes "\<forall>x \<in> set xs. qfree (f x)"
shows "qfree (evaldjf f xs)"
- using nb
- apply (induct xs)
- apply (auto simp add: evaldjf_def djf_def Let_def)
- apply (case_tac "f a")
- apply auto
- done
+ using assms
+ by (induct xs) (auto simp add: evaldjf_def djf_def Let_def split: fm.split)
+
fun disjuncts :: "fm \<Rightarrow> fm list"
where
@@ -1750,7 +1741,9 @@
{assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Lt a))"
by (simp add: nb Let_def split_def isint_Floor isint_neg)
have "?I (Lt a) = (real_of_int (?c * i) + (?N ?r) < 0)" using Ia by (simp add: Let_def split_def)
- also have "\<dots> = (?I (?l (Lt a)))" apply (simp only: split_int_less_real'[where a="?c*i" and b="?N ?r"]) by (simp add: Ia cp cnz Let_def split_def)
+ also have "\<dots> = (?I (?l (Lt a)))"
+ unfolding split_int_less_real'[where a="?c*i" and b="?N ?r"]
+ by (simp add: Ia cp cnz Let_def split_def)
finally have ?case using l by simp}
moreover
{assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Lt a))"
@@ -2761,28 +2754,27 @@
shows "\<forall> b\<in> set (\<beta> p). isint b bs"
using lp by (induct p rule: iszlfm.induct) (auto simp add: isint_neg isint_sub)
-lemma cpmi_eq: "0 < D \<Longrightarrow> (\<exists>z::int. \<forall>x. x < z \<longrightarrow> (P x = P1 x))
-\<Longrightarrow> \<forall>x. \<not>(\<exists>(j::int) \<in> {1..D}. \<exists>(b::int) \<in> B. P(b+j)) \<longrightarrow> P (x) \<longrightarrow> P (x - D)
-\<Longrightarrow> (\<forall>(x::int). \<forall>(k::int). ((P1 x)= (P1 (x-k*D))))
-\<Longrightarrow> (\<exists>(x::int). P(x)) = ((\<exists>(j::int) \<in> {1..D} . (P1(j))) | (\<exists>(j::int) \<in> {1..D}. \<exists>(b::int) \<in> B. P (b+j)))"
-apply(rule iffI)
-prefer 2
-apply(drule minusinfinity)
-apply assumption+
-apply(fastforce)
-apply clarsimp
-apply(subgoal_tac "\<And>k. 0<=k \<Longrightarrow> \<forall>x. P x \<longrightarrow> P (x - k*D)")
-apply(frule_tac x = x and z=z in decr_lemma)
-apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)")
-prefer 2
-apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
-prefer 2 apply arith
- apply fastforce
-apply(drule (1) periodic_finite_ex)
-apply blast
-apply(blast dest:decr_mult_lemma)
-done
-
+lemma cpmi_eq:
+ assumes "0 < D"
+ and "\<exists>z::int. \<forall>x<z. P x = P1 x"
+ and "\<forall>x. \<not> (\<exists>j\<in>{1..D}. \<exists>b\<in>B. P (b + j)) \<longrightarrow> P x \<longrightarrow> P (x - D)"
+ and "\<forall>x k. P1 x = P1 (x - k * D)"
+ shows "(\<exists>x. P x) \<longleftrightarrow> ((\<exists>j\<in>{1..D}. P1 j) \<or> (\<exists>j\<in>{1..D}. \<exists>b\<in>B. P (b + j)))" (is "_=?R")
+proof
+ assume L: "\<exists>x. P x"
+ show "(\<exists>j\<in>{1..D}. P1 j) \<or> (\<exists>j\<in>{1..D}. \<exists>b\<in>B. P (b + j))"
+ proof clarsimp
+ assume \<section>: "\<forall>j\<in>{1..D}. \<forall>b\<in>B. \<not> P (b + j)"
+ then have "\<And>k. 0\<le>k \<Longrightarrow> \<forall>x. P x \<longrightarrow> P (x - k*D)"
+ by (simp add: assms decr_mult_lemma)
+ with L \<section> assms show "\<exists>j\<in>{1..D}. P1 j"
+ using periodic_finite_ex [OF \<open>D>0\<close>, of P1]
+ by (metis abs_1 abs_add_abs abs_ge_zero decr_lemma)
+ qed
+next
+ assume ?R then show "\<exists>x. P x"
+ using decr_lemma assms by blast
+qed
theorem cp_thm:
assumes lp: "iszlfm p (a #bs)"
@@ -3126,9 +3118,8 @@
from 6 mult_strict_left_mono[OF dp cp, simplified of_int_less_iff[symmetric]
of_int_mult]
show ?case using 6 dp
- apply (simp add: numbound0_I[where bs="bs" and b="real_of_int i - real_of_int d" and b'="real_of_int i"]
- algebra_simps del: mult_pos_pos)
- using order_trans by fastforce
+ by (fastforce simp: numbound0_I[where bs="bs" and b="i - real_of_int d" and b'="i"]
+ algebra_simps intro: order_trans)
next
case (7 c e) hence cp: "c >0" and nb: "numbound0 e" and ei: "isint e (real_of_int i#bs)"
and nob: "\<forall> j\<in> {1 .. c*d}. real_of_int (c*i) \<noteq> - ?N i e + real_of_int j"
@@ -3419,7 +3410,7 @@
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un
(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {0 .. n}})) Un
(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {n .. 0}})))"
- by blast
+ by force
finally
have FS: "?SS (Floor a) =
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un
@@ -3576,7 +3567,7 @@
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un
(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {0 .. n}})) Un
(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {n .. 0}})))"
- by blast
+ by force
finally
have FS: "?SS (Floor a) =
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un
@@ -4880,7 +4871,8 @@
have MF: "?M = False"
apply (simp add: Let_def reducecoeff_def numgcd_def rsplit_def ge_def lt_def conj_def disj_def)
by (cases "rlfm p = And (Ge (CN 0 1 (C 0))) (Lt (CN 0 1 (C (- 1))))", simp_all)
- have PF: "?P = False" apply (simp add: Let_def reducecoeff_def numgcd_def rsplit_def ge_def lt_def conj_def disj_def)
+ have PF: "?P = False"
+ apply (simp add: Let_def reducecoeff_def numgcd_def rsplit_def ge_def lt_def conj_def disj_def)
by (cases "rlfm p = And (Ge (CN 0 1 (C 0))) (Lt (CN 0 1 (C (- 1))))", simp_all)
have "(\<exists> x. ?I x ?q ) =
((?I x (minusinf ?rq)) \<or> (?I x (plusinf ?rq )) \<or> (\<exists> (t,n) \<in> set (\<Upsilon> ?rq). \<exists> (s,m) \<in> set (\<Upsilon> ?rq ). ?I x (\<upsilon> ?rq (Add (Mul m t) (Mul n s), 2*n*m))))"
@@ -4936,9 +4928,7 @@
\<in> (\<lambda>((t, n), s, m).
(Inum (x # bs) t / real_of_int n + Inum (x # bs) s / real_of_int m) / 2) `
(set U \<times> set U)"using mnz nnz th
- apply (auto simp add: th add_divide_distrib algebra_simps split_def image_def)
- by (rule_tac x="(s,m)" in bexI,simp_all)
- (rule_tac x="(t,n)" in bexI,simp_all add: mult.commute)
+ by (force simp add: th add_divide_distrib algebra_simps split_def image_def)
next
fix t n s m
assume tnU: "(t,n) \<in> set U" and smU:"(s,m) \<in> set U"
@@ -5299,9 +5289,8 @@
from ee' have tt': "Inum (a#bs) (Add e (C j)) = Inum (a#bs) (Add e' (C j))" by simp
from \<sigma>_cong[OF lp tt', where c="c"] px have px':"?sp c e' j" by simp
- from ecRo jD px' show ?rhs apply (auto simp: cc')
- by (rule_tac x="(e', c')" in bexI,simp_all)
- (rule_tac x="j" in bexI, simp_all add: cc'[symmetric])
+ from ecRo jD px' show ?rhs
+ using cc' by blast
next
let ?d = "\<delta> p"
assume ?rhs then obtain e c j where ecR: "(e,c) \<in> set (\<rho> p)" and jD:"j \<in> {1 .. c*?d}"
@@ -5313,9 +5302,8 @@
and cc':"c = c'" by blast
from ee' have tt': "Inum (a#bs) (Add e (C j)) = Inum (a#bs) (Add e' (C j))" by simp
from \<sigma>_cong[OF lp tt', where c="c"] px have px':"?sp c e' j" by simp
- from ecRo jD px' show ?lhs apply (auto simp: cc')
- by (rule_tac x="(e', c')" in bexI,simp_all)
- (rule_tac x="j" in bexI, simp_all add: cc'[symmetric])
+ from ecRo jD px' show ?lhs
+ using cc' by blast
qed
lemma rl_thm':
--- a/src/HOL/Decision_Procs/Rat_Pair.thy Sun Apr 14 22:38:17 2024 +0100
+++ b/src/HOL/Decision_Procs/Rat_Pair.thy Mon Apr 15 22:23:40 2024 +0100
@@ -140,10 +140,7 @@
qed
lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)"
- apply (simp add: Ninv_def isnormNum_def split_def)
- apply (cases "fst x = 0")
- apply (auto simp add: gcd.commute)
- done
+ by (simp add: Ninv_def isnormNum_def split_def gcd.commute split: if_split_asm)
lemma isnormNum_int[simp]: "isnormNum 0\<^sub>N" "isnormNum ((1::int)\<^sub>N)" "i \<noteq> 0 \<Longrightarrow> isnormNum (i)\<^sub>N"
by (simp_all add: isnormNum_def)
@@ -201,12 +198,7 @@
then have "coprime a b" "coprime b a" "coprime a' b'" "coprime b' a'"
by (simp_all add: coprime_iff_gcd_eq_1)
from eq have raw_dvd: "a dvd a' * b" "b dvd b' * a" "a' dvd a * b'" "b' dvd b * a'"
- apply -
- apply algebra
- apply algebra
- apply simp
- apply algebra
- done
+ by (algebra|simp)+
then have eq1: "b = b'"
using pos \<open>coprime b a\<close> \<open>coprime b' a'\<close>
by (auto simp add: coprime_dvd_mult_left_iff intro: associated_eqI)
@@ -282,15 +274,7 @@
proof cases
case 1
then show ?thesis
- apply (cases "a = 0")
- apply (simp_all add: x y Nadd_def)
- apply (cases "b = 0")
- apply (simp_all add: INum_def)
- apply (cases "a'= 0")
- apply simp_all
- apply (cases "b'= 0")
- apply simp_all
- done
+ by (auto simp: x y INum_def Nadd_def normNum_def Let_def of_int_div)
next
case neq: 2
show ?thesis
@@ -480,13 +464,7 @@
and "(a, 0) +\<^sub>N y = normNum y"
and "x +\<^sub>N (0, b) = normNum x"
and "x +\<^sub>N (a, 0) = normNum x"
- apply (simp add: Nadd_def split_def)
- apply (simp add: Nadd_def split_def)
- apply (subst Nadd_commute)
- apply (simp add: Nadd_def split_def)
- apply (subst Nadd_commute)
- apply (simp add: Nadd_def split_def)
- done
+ by (simp_all add: Nadd_def normNum_def split_def)
lemma normNum_nilpotent_aux[simp]:
assumes "SORT_CONSTRAINT('a::field_char_0)"
@@ -599,18 +577,13 @@
obtain a' b' where y: "y = (a', b')" by (cases y)
have n0: "isnormNum 0\<^sub>N" by simp
show ?thesis using nx ny
- apply (simp only: isnormNum_unique[where ?'a = 'a, OF Nmul_normN[OF nx ny] n0, symmetric]
- Nmul[where ?'a = 'a])
- apply (simp add: x y INum_def split_def isnormNum_def split: if_split_asm)
- done
+ by (metis (no_types, opaque_lifting) INum_int(2) Nmul Nmul0(1) Nmul0(2) isnormNum0 mult_eq_0_iff)
qed
lemma Nneg_Nneg[simp]: "~\<^sub>N (~\<^sub>N c) = c"
by (simp add: Nneg_def split_def)
lemma Nmul1[simp]: "isnormNum c \<Longrightarrow> (1)\<^sub>N *\<^sub>N c = c" "isnormNum c \<Longrightarrow> c *\<^sub>N (1)\<^sub>N = c"
- apply (simp_all add: Nmul_def Let_def split_def isnormNum_def)
- apply (cases "fst c = 0", simp_all, cases c, simp_all)+
- done
+ by (simp add: Nmul_def Let_def split_def isnormNum_def, metis div_0 div_by_1 surjective_pairing)+
end