# HG changeset patch # User wenzelm # Date 1434814191 -7200 # Node ID 25a3c522cc8f65805a129feec90ef4b1932f9d60 # Parent b2add2b08412b50f9a1d98622ef30a784db8fcf2 tuned proofs; diff -r b2add2b08412 -r 25a3c522cc8f src/HOL/Decision_Procs/Commutative_Ring_Complete.thy --- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Sat Jun 20 16:42:15 2015 +0200 +++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Sat Jun 20 17:29:51 2015 +0200 @@ -73,10 +73,12 @@ done next case Pc - with assms show ?thesis by (cases x) auto + with assms show ?thesis + by (cases x) auto next case Pinj - with assms show ?thesis by (cases x) auto + with assms show ?thesis + by (cases x) auto qed lemma norm_PXtrans2: @@ -122,134 +124,149 @@ 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 - by (cases x) (auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto) + apply (cases x) + apply (auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _]) + apply (cases P2) + apply auto + done qed text \add conserves normalizedness\ lemma add_cn: "isnorm P \ isnorm Q \ isnorm (P \ Q)" proof (induct P Q rule: add.induct) + case 1 + then show ?case by simp +next case (2 c i P2) then show ?case - by (cases P2) (simp_all, cases i, simp_all) + apply (cases P2) + apply simp_all + apply (cases i) + apply simp_all + done next case (3 i P2 c) then show ?case - by (cases P2) (simp_all, cases i, simp_all) + apply (cases P2) + apply simp_all + apply (cases i) + apply simp_all + done 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 - by (cases i) (simp, cases P2, auto, rename_tac pol2, case_tac pol2, auto) + apply (cases i) + apply simp + apply (cases P2) + apply auto + apply (rename_tac pol2, case_tac pol2) + apply auto + done 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 - by (cases i) (simp, cases P2, auto, rename_tac pol2, case_tac pol2, auto) + apply (cases i) + apply simp + apply (cases P2) + apply auto + apply (rename_tac pol2, case_tac pol2) + apply auto + done next case (6 x P2 y Q2) then have Y0: "y > 0" by (cases y) (auto simp add: norm_Pinj_0_False) with 6 have X0: "x > 0" by (cases x) (auto simp add: norm_Pinj_0_False) - have "x < y \ x = y \ x > y" by arith - moreover { - assume "x < y" - then have "\d. y = d + x" by arith - then obtain d where y: "y = d + x" .. - moreover - note 6 X0 - moreover - from 6 have "isnorm P2" "isnorm Q2" + consider "x < y" | "x = y" | "x > y" by arith + then show ?case + proof cases + case 1 + then obtain d where y: "y = d + x" + by atomize_elim arith + from 6 have *: "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) - moreover - from 6 \x < y\ y have "isnorm (Pinj d Q2)" + from 6 1 y have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto) - ultimately have ?case by (simp add: mkPinj_cn) - } - moreover { - assume "x = y" - moreover + with 6 X0 y * show ?thesis + by (simp add: mkPinj_cn) + next + case 2 from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) - moreover - note 6 Y0 - ultimately have ?case by (simp add: mkPinj_cn) - } - moreover { - assume "x > y" - then have "\d. x = d + y" - by arith - then obtain d where x: "x = d + y" .. - moreover - note 6 Y0 - moreover - from 6 have "isnorm P2" "isnorm Q2" + with 2 6 Y0 show ?thesis + by (simp add: mkPinj_cn) + next + case 3 + then obtain d where x: "x = d + y" + by atomize_elim arith + from 6 have *: "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) - moreover - from 6 \x > y\ x have "isnorm (Pinj d P2)" + from 6 3 x have "isnorm (Pinj d P2)" by (cases d) (simp, cases P2, auto) - ultimately have ?case by (simp add: mkPinj_cn) - } - ultimately show ?case by blast + with 3 6 Y0 * x show ?thesis by (simp add: mkPinj_cn) + qed next case (7 x P2 Q2 y R) - have "x = 0 \ x = 1 \ x > 1" by arith - moreover { - assume "x = 0" - with 7 have ?case by (auto simp add: norm_Pinj_0_False) - } - moreover { - assume "x = 1" + consider "x = 0" | "x = 1" | d where "x = Suc (Suc d)" + by atomize_elim arith + then show ?case + proof cases + case 1 + with 7 show ?thesis + by (auto simp add: norm_Pinj_0_False) + next + case 2 from 7 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) - with 7 \x = 1\ have "isnorm (R \ P2)" by simp - with 7 \x = 1\ have ?case + with 7 2 have "isnorm (R \ P2)" + by simp + with 7 2 show ?thesis by (simp add: norm_PXtrans[of Q2 y _]) - } - moreover { - assume "x > 1" then have "\d. x=Suc (Suc d)" by arith - then obtain d where X: "x=Suc (Suc d)" .. + next + case 3 with 7 have NR: "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) - with 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto - with 7 X NR have "isnorm (R \ Pinj (x - 1) P2)" by simp - with \isnorm (PX Q2 y R)\ X have ?case + with 7 3 have "isnorm (Pinj (x - 1) P2)" + by (cases P2) auto + with 7 3 NR have "isnorm (R \ Pinj (x - 1) P2)" + by simp + with \isnorm (PX Q2 y R)\ 3 show ?thesis by (simp add: norm_PXtrans[of Q2 y _]) - } - ultimately show ?case by blast + qed next case (8 Q2 y R x P2) - have "x = 0 \ x = 1 \ x > 1" by arith - moreover { - assume "x = 0" - with 8 have ?case + consider "x = 0" | "x = 1" | "x > 1" + by arith + then show ?case + proof cases + case 1 + with 8 show ?thesis by (auto simp add: norm_Pinj_0_False) - } - moreover { - assume "x = 1" + next + case 2 with 8 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) - with 8 \x = 1\ have "isnorm (R \ P2)" + with 8 2 have "isnorm (R \ P2)" by simp - with 8 \x = 1\ have ?case + with 8 2 show ?thesis by (simp add: norm_PXtrans[of Q2 y _]) - } - moreover { - assume "x > 1" - then have "\d. x = Suc (Suc d)" by arith - then obtain d where X: "x = Suc (Suc d)" .. + next + case 3 + then obtain d where x: "x = Suc (Suc d)" by atomize_elim arith with 8 have NR: "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) - with 8 X have "isnorm (Pinj (x - 1) P2)" + with 8 x have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto - with 8 \x > 1\ NR have "isnorm (R \ Pinj (x - 1) P2)" + with 8 3 NR have "isnorm (R \ Pinj (x - 1) P2)" by simp - with \isnorm (PX Q2 y R)\ X have ?case + with \isnorm (PX Q2 y R)\ x show ?thesis by (simp add: norm_PXtrans[of Q2 y _]) - } - ultimately show ?case by blast + qed next case (9 P1 x P2 Q1 y Q2) then have Y0: "y > 0" by (cases y) auto @@ -258,228 +275,215 @@ by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2]) with 9 have NQ1: "isnorm Q1" and NQ2: "isnorm Q2" by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2]) - have "y < x \ x = y \ x < y" by arith - moreover { - assume sm1: "y < x" - then have "\d. x = d + y" by arith - then obtain d where sm2: "x = d + y" .. - note 9 NQ1 NP1 NP2 NQ2 sm1 sm2 - moreover + consider "y < x" | "x = y" | "x < y" by arith + then show ?case + proof cases + case 1 + then obtain d where x: "x = d + y" + by atomize_elim arith have "isnorm (PX P1 d (Pc 0))" proof (cases P1) case (PX p1 y p2) - with 9 sm1 sm2 show ?thesis + with 9 1 x show ?thesis by (cases d) (simp, cases p2, auto) next case Pc - with 9 sm1 sm2 show ?thesis + with 9 1 x show ?thesis by (cases d) auto next case Pinj - with 9 sm1 sm2 show ?thesis + with 9 1 x show ?thesis by (cases d) auto qed - ultimately have "isnorm (P2 \ Q2)" "isnorm (PX P1 (x - y) (Pc 0) \ Q1)" + with 9 NQ1 NP1 NP2 NQ2 1 x have "isnorm (P2 \ Q2)" "isnorm (PX P1 (x - y) (Pc 0) \ Q1)" by auto - with Y0 sm1 sm2 have ?case + with Y0 1 x show ?thesis by (simp add: mkPX_cn) - } - moreover { - assume "x = y" + next + case 2 with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \ Q2)" "isnorm (P1 \ Q1)" by auto - with \x = y\ Y0 have ?case + with 2 Y0 show ?thesis by (simp add: mkPX_cn) - } - moreover { - assume sm1: "x < y" - then have "\d. y = d + x" by arith - then obtain d where sm2: "y = d + x" .. - note 9 NQ1 NP1 NP2 NQ2 sm1 sm2 - moreover + next + case 3 + then obtain d where y: "y = d + x" + by atomize_elim arith have "isnorm (PX Q1 d (Pc 0))" proof (cases Q1) case (PX p1 y p2) - with 9 sm1 sm2 show ?thesis + with 9 3 y show ?thesis by (cases d) (simp, cases p2, auto) next case Pc - with 9 sm1 sm2 show ?thesis + with 9 3 y show ?thesis by (cases d) auto next case Pinj - with 9 sm1 sm2 show ?thesis + with 9 3 y show ?thesis by (cases d) auto qed - ultimately have "isnorm (P2 \ Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \ P1)" + with 9 NQ1 NP1 NP2 NQ2 3 y have "isnorm (P2 \ Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \ P1)" by auto - with X0 sm1 sm2 have ?case + with X0 3 y show ?thesis by (simp add: mkPX_cn) - } - ultimately show ?case by blast -qed simp + qed +qed text \mul concerves normalizedness\ lemma mul_cn: "isnorm P \ isnorm Q \ isnorm (P \ Q)" proof (induct P Q rule: mul.induct) + case 1 + then show ?case by simp +next case (2 c i P2) then show ?case - by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn) + apply (cases P2) + apply simp_all + apply (cases i) + apply (simp_all add: mkPinj_cn) + done next case (3 i P2 c) then show ?case - by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn) + apply (cases P2) + apply simp_all + apply (cases i) + apply (simp_all add: mkPinj_cn) + done 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 - by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn) + apply (cases "c = 0") + apply simp_all + apply (cases "i = 0") + apply (simp_all add: mkPX_cn) + done 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 - by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn) + apply (cases "c = 0") + apply simp_all + apply (cases "i = 0") + apply (simp_all add: mkPX_cn) + done next case (6 x P2 y Q2) - have "x < y \ x = y \ x > y" by arith - moreover { - assume "x < y" - then have "\d. y = d + x" by arith - then obtain d where y: "y = d + x" .. - moreover - note 6 - moreover - from 6 have "x > 0" + consider "x < y" | "x = y" | "x > y" by arith + then show ?case + proof cases + case 1 + then obtain d where y: "y = d + x" + by atomize_elim arith + from 6 have *: "x > 0" by (cases x) (auto simp add: norm_Pinj_0_False) - moreover - from 6 have "isnorm P2" "isnorm Q2" + from 6 have **: "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) - moreover - from 6 \x < y\ y have "isnorm (Pinj d Q2)" - by (cases d) (simp, cases Q2, auto) - ultimately have ?case by (simp add: mkPinj_cn) - } - moreover { - assume "x = y" - moreover - from 6 have "isnorm P2" "isnorm Q2" + from 6 1 y have "isnorm (Pinj d Q2)" + apply (cases d) + apply simp + apply (cases Q2) + apply auto + done + with 6 * ** y show ?thesis + by (simp add: mkPinj_cn) + next + case 2 + from 6 have *: "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) - moreover - from 6 have "y>0" + from 6 have **: "y > 0" + by (cases y) (auto simp add: norm_Pinj_0_False) + with 6 2 * **show ?thesis + by (simp add: mkPinj_cn) + next + case 3 + then obtain d where x: "x = d + y" + by atomize_elim arith + from 6 have *: "y > 0" by (cases y) (auto simp add: norm_Pinj_0_False) - moreover - note 6 - ultimately have ?case by (simp add: mkPinj_cn) - } - moreover { - assume "x > y" - then have "\d. x = d + y" by arith - then obtain d where x: "x = d + y" .. - moreover - note 6 - moreover - from 6 have "y > 0" - by (cases y) (auto simp add: norm_Pinj_0_False) - moreover - from 6 have "isnorm P2" "isnorm Q2" + from 6 have **: "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) - moreover - from 6 \x > y\ x have "isnorm (Pinj d P2)" - by (cases d) (simp, cases P2, auto) - ultimately have ?case by (simp add: mkPinj_cn) - } - ultimately show ?case by blast + from 6 3 x have "isnorm (Pinj d P2)" + apply (cases d) + apply simp + apply (cases P2) + apply auto + done + with 6 3 * ** x show ?thesis + by (simp add: mkPinj_cn) + qed next case (7 x P2 Q2 y R) then have Y0: "y > 0" by (cases y) auto - have "x = 0 \ x = 1 \ x > 1" by arith - moreover { - assume "x = 0" - with 7 have ?case + consider "x = 0" | "x = 1" | d where "x = Suc (Suc d)" + by atomize_elim arith + then show ?case + proof cases + case 1 + with 7 show ?thesis by (auto simp add: norm_Pinj_0_False) - } - moreover { - assume "x = 1" + next + case 2 from 7 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) - with 7 \x = 1\ have "isnorm (R \ P2)" "isnorm Q2" + with 7 2 have "isnorm (R \ P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R]) - with 7 \x = 1\ Y0 have ?case + with 7 2 Y0 show ?thesis by (simp add: mkPX_cn) - } - moreover { - assume "x > 1" - then have "\d. x = Suc (Suc d)" - by arith - then obtain d where X: "x = Suc (Suc d)" .. - from 7 have NR: "isnorm R" "isnorm Q2" + next + case 3 + from 7 have *: "isnorm R" "isnorm Q2" by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R]) - moreover - from 7 X have "isnorm (Pinj (x - 1) P2)" - by (cases P2) auto - moreover - from 7 have "isnorm (Pinj x P2)" + from 7 3 have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto - moreover - note 7 X - ultimately have "isnorm (R \ Pinj (x - 1) P2)" "isnorm (Pinj x P2 \ Q2)" + with 7 3 * have "isnorm (R \ Pinj (x - 1) P2)" "isnorm (Pinj x P2 \ Q2)" by auto - with Y0 X have ?case + with Y0 3 show ?thesis by (simp add: mkPX_cn) - } - ultimately show ?case by blast + qed next case (8 Q2 y R x P2) then have Y0: "y > 0" by (cases y) auto - have "x = 0 \ x = 1 \ x > 1" by arith - moreover { - assume "x = 0" - with 8 have ?case + consider "x = 0" | "x = 1" | d where "x = Suc (Suc d)" + by atomize_elim arith + then show ?case + proof cases + case 1 + with 8 show ?thesis by (auto simp add: norm_Pinj_0_False) - } - moreover { - assume "x = 1" + next + case 2 from 8 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) - with 8 \x = 1\ have "isnorm (R \ P2)" "isnorm Q2" + with 8 2 have "isnorm (R \ P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R]) - with 8 \x = 1\ Y0 have ?case + with 8 2 Y0 show ?thesis by (simp add: mkPX_cn) - } - moreover { - assume "x > 1" - then have "\d. x = Suc (Suc d)" by arith - then obtain d where X: "x = Suc (Suc d)" .. - from 8 have NR: "isnorm R" "isnorm Q2" + next + case 3 + from 8 have *: "isnorm R" "isnorm Q2" by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R]) - moreover - from 8 X have "isnorm (Pinj (x - 1) P2)" - by (cases P2) auto - moreover - from 8 X have "isnorm (Pinj x P2)" + from 8 3 have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto - moreover - note 8 X - ultimately have "isnorm (R \ Pinj (x - 1) P2)" "isnorm (Pinj x P2 \ Q2)" + with 8 3 * have "isnorm (R \ Pinj (x - 1) P2)" "isnorm (Pinj x P2 \ Q2)" by auto - with Y0 X have ?case by (simp add: mkPX_cn) - } - ultimately show ?case by blast + with Y0 3 show ?thesis + by (simp add: mkPX_cn) + qed next case (9 P1 x P2 Q1 y Q2) from 9 have X0: "x > 0" by (cases x) auto from 9 have Y0: "y > 0" by (cases y) auto - note 9 - moreover - from 9 have "isnorm P1" "isnorm P2" + from 9 have *: "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2]) - moreover from 9 have "isnorm Q1" "isnorm Q2" by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2]) - ultimately have "isnorm (P1 \ Q1)" "isnorm (P2 \ Q2)" + with 9 * have "isnorm (P1 \ Q1)" "isnorm (P2 \ Q2)" "isnorm (P1 \ mkPinj 1 Q2)" "isnorm (Q1 \ mkPinj 1 P2)" by (auto simp add: mkPinj_cn) with 9 X0 Y0 have @@ -487,12 +491,16 @@ "isnorm (mkPX (P1 \ mkPinj (Suc 0) Q2) x (Pc 0))" "isnorm (mkPX (Q1 \ mkPinj (Suc 0) P2) y (Pc 0))" by (auto simp add: mkPX_cn) - then show ?case by (simp add: add_cn) -qed simp + then show ?case + by (simp add: add_cn) +qed text \neg conserves normalizedness\ lemma neg_cn: "isnorm P \ isnorm (neg P)" proof (induct P) + case Pc + then show ?case by simp +next case (Pinj i P2) then have "isnorm P2" by (simp add: norm_Pinj[of i P2]) @@ -512,7 +520,7 @@ with PX1 show ?thesis by (cases x) auto qed (cases x, auto) -qed simp +qed text \sub conserves normalizedness\ lemma sub_cn: "isnorm p \ isnorm q \ isnorm (p \ q)" @@ -526,13 +534,20 @@ next case (Pinj i Q) then show ?case - by (cases Q) (auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn) + apply (cases Q) + apply (auto simp add: mkPX_cn mkPinj_cn) + apply (cases i) + apply (auto simp add: mkPX_cn mkPinj_cn) + done next case (PX P1 x P2) then have "x + x \ 0" "isnorm P2" "isnorm P1" - by (cases x, auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2]) + apply (cases x) + using PX + apply (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2]) + done with PX have "isnorm (mkPX (Pc (1 + 1) \ P1 \ mkPinj (Suc 0) P2) x (Pc 0))" - and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))" + and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))" by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn) then show ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn) @@ -548,8 +563,10 @@ then show ?thesis by simp next case False - then have K2: "k div 2 < k" by (cases k) auto - from less have "isnorm (sqr P)" by (simp add: sqr_cn) + then have K2: "k div 2 < k" + by (cases k) auto + from less have "isnorm (sqr P)" + by (simp add: sqr_cn) with less False K2 show ?thesis by (cases "even k") (auto simp add: mul_cn elim: evenE oddE) qed