# HG changeset patch # User paulson # Date 1713216220 -3600 # Node ID 2fa018321400d82223ad3237afb4a2636e309364 # Parent 577a2896ace90cee5b05a9895858b286c7a92bdf Streamlining of many more archaic proofs diff -r 577a2896ace9 -r 2fa018321400 src/HOL/Decision_Procs/Commutative_Ring_Complete.thy --- 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) \ 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) \ isnorm Q" - apply (cases i) - apply auto - apply (cases P) - apply auto - subgoal for \ 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) \ isnorm P" - apply (cases i) - apply auto - apply (cases P) - apply auto - subgoal for \ pol2 by (cases pol2) auto - done - -lemma mkPinj_cn: "y \ 0 \ isnorm Q \ 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 \ 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 \\mkPX\ conserves normalizedness (\_cn\)\ +text \\mkPX\ preserves the normal property (\_cn\)\ lemma mkPX_cn: assumes "x \ 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 \P = PX P1 y P2\ + show ?thesis + using assms PX by (auto simp add: mkPX_def norm_PXtrans2) + qed qed -text \\add\ conserves normalizedness\ +text \\add\ preserves the normal property\ lemma add_cn: "isnorm P \ isnorm Q \ isnorm (P \+\ 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 \ 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 \ 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 \neg conserves normalizedness\ +text \neg preserves the normal property\ lemma neg_cn: "isnorm P \ isnorm (neg P)" proof (induct P) case Pc @@ -520,7 +469,7 @@ qed (cases x, auto) qed -text \sub conserves normalizedness\ +text \sub preserves the normal property\ lemma sub_cn: "isnorm p \ isnorm q \ isnorm (p \-\ 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 \ 0" "isnorm P2" "isnorm P1" @@ -548,7 +493,7 @@ by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn) qed -text \\pow\ conserves normalizedness\ +text \\pow\ preserves the normal property\ lemma pow_cn: "isnorm P \ isnorm (pow n P)" proof (induct n arbitrary: P rule: less_induct) case (less k) diff -r 577a2896ace9 -r 2fa018321400 src/HOL/Decision_Procs/MIR.thy --- 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: "\ x\ set xs. bound0 (f x)" + assumes "\x \ 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: "\ x\ set xs. qfree (f x)" + assumes "\x \ 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 \ fm list" where @@ -1750,7 +1741,9 @@ {assume cp: "?c > 0" and cnz: "?c\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 "\ = (?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 "\ = (?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\0" hence l: "?L (?l (Lt a))" @@ -2761,28 +2754,27 @@ shows "\ b\ set (\ p). isint b bs" using lp by (induct p rule: iszlfm.induct) (auto simp add: isint_neg isint_sub) -lemma cpmi_eq: "0 < D \ (\z::int. \x. x < z \ (P x = P1 x)) -\ \x. \(\(j::int) \ {1..D}. \(b::int) \ B. P(b+j)) \ P (x) \ P (x - D) -\ (\(x::int). \(k::int). ((P1 x)= (P1 (x-k*D)))) -\ (\(x::int). P(x)) = ((\(j::int) \ {1..D} . (P1(j))) | (\(j::int) \ {1..D}. \(b::int) \ B. P (b+j)))" -apply(rule iffI) -prefer 2 -apply(drule minusinfinity) -apply assumption+ -apply(fastforce) -apply clarsimp -apply(subgoal_tac "\k. 0<=k \ \x. P x \ P (x - k*D)") -apply(frule_tac x = x and z=z in decr_lemma) -apply(subgoal_tac "P1(x - (\x - z\ + 1) * D)") -prefer 2 -apply(subgoal_tac "0 <= (\x - z\ + 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 "\z::int. \xx. \ (\j\{1..D}. \b\B. P (b + j)) \ P x \ P (x - D)" + and "\x k. P1 x = P1 (x - k * D)" + shows "(\x. P x) \ ((\j\{1..D}. P1 j) \ (\j\{1..D}. \b\B. P (b + j)))" (is "_=?R") +proof + assume L: "\x. P x" + show "(\j\{1..D}. P1 j) \ (\j\{1..D}. \b\B. P (b + j))" + proof clarsimp + assume \
: "\j\{1..D}. \b\B. \ P (b + j)" + then have "\k. 0\k \ \x. P x \ P (x - k*D)" + by (simp add: assms decr_mult_lemma) + with L \
assms show "\j\{1..D}. P1 j" + using periodic_finite_ex [OF \D>0\, of P1] + by (metis abs_1 abs_add_abs abs_ge_zero decr_lemma) + qed +next + assume ?R then show "\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: "\ j\ {1 .. c*d}. real_of_int (c*i) \ - ?N i e + real_of_int j" @@ -3419,7 +3410,7 @@ ((UNION {(p,n,s). (p,n,s) \ ?SS a \ n=0} (\ (p,n,s). {(p,0,Floor s)})) Un (UNION {(p,n,s). (p,n,s) \ ?SS a \ n>0} (\ (p,n,s). {?f(p,n,s) j| j. j\ {0 .. n}})) Un (UNION {(p,n,s). (p,n,s) \ ?SS a \ n<0} (\ (p,n,s). {?f(p,n,s) j| j. j\ {n .. 0}})))" - by blast + by force finally have FS: "?SS (Floor a) = ((UNION {(p,n,s). (p,n,s) \ ?SS a \ n=0} (\ (p,n,s). {(p,0,Floor s)})) Un @@ -3576,7 +3567,7 @@ ((UNION {(p,n,s). (p,n,s) \ ?SS a \ n=0} (\ (p,n,s). {(p,0,Floor s)})) Un (UNION {(p,n,s). (p,n,s) \ ?SS a \ n>0} (\ (p,n,s). {?f(p,n,s) j| j. j\ {0 .. n}})) Un (UNION {(p,n,s). (p,n,s) \ ?SS a \ n<0} (\ (p,n,s). {?f(p,n,s) j| j. j\ {n .. 0}})))" - by blast + by force finally have FS: "?SS (Floor a) = ((UNION {(p,n,s). (p,n,s) \ ?SS a \ n=0} (\ (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 "(\ x. ?I x ?q ) = ((?I x (minusinf ?rq)) \ (?I x (plusinf ?rq )) \ (\ (t,n) \ set (\ ?rq). \ (s,m) \ set (\ ?rq ). ?I x (\ ?rq (Add (Mul m t) (Mul n s), 2*n*m))))" @@ -4936,9 +4928,7 @@ \ (\((t, n), s, m). (Inum (x # bs) t / real_of_int n + Inum (x # bs) s / real_of_int m) / 2) ` (set U \ 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) \ set U" and smU:"(s,m) \ 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 \_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 = "\ p" assume ?rhs then obtain e c j where ecR: "(e,c) \ set (\ p)" and jD:"j \ {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 \_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': diff -r 577a2896ace9 -r 2fa018321400 src/HOL/Decision_Procs/Rat_Pair.thy --- 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 \ 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 \ 0 \ 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 \coprime b a\ \coprime b' a'\ 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 \ (1)\<^sub>N *\<^sub>N c = c" "isnormNum c \ 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