summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 21 Feb 2011 23:47:19 +0100 | |

changeset 41807 | ab5d2d81f9fb |

parent 41806 | 173e1b50d5c5 |

child 41816 | 7a55699805dc |

tuned proofs -- eliminated prems;

--- a/src/HOL/Decision_Procs/Commutative_Ring.thy Mon Feb 21 18:29:47 2011 +0100 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Mon Feb 21 23:47:19 2011 +0100 @@ -308,7 +308,7 @@ assumes "norm P1 = norm P2" shows "Ipolex l P1 = Ipolex l P2" proof - - from prems have "Ipol l (norm P1) = Ipol l (norm P2)" by simp + from assms have "Ipol l (norm P1) = Ipol l (norm P2)" by simp then show ?thesis by (simp only: norm_ci) qed

--- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Mon Feb 21 18:29:47 2011 +0100 +++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Mon Feb 21 23:47:19 2011 +0100 @@ -50,23 +50,25 @@ assumes A:"isnorm (PX P x Q)" and "isnorm Q2" shows "isnorm (PX P x Q2)" proof(cases P) - case (PX p1 y p2) from prems show ?thesis by(cases x, auto, cases p2, auto) + case (PX p1 y p2) with assms show ?thesis by(cases x, auto, cases p2, auto) next - case Pc from prems show ?thesis by(cases x, auto) + case Pc with assms show ?thesis by (cases x) auto next - case Pinj from prems show ?thesis by(cases x, auto) + case Pinj with assms show ?thesis by (cases x) auto qed -lemma norm_PXtrans2: assumes A:"isnorm (PX P x Q)" and "isnorm Q2" shows "isnorm (PX P (Suc (n+x)) Q2)" -proof(cases P) +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) - from prems show ?thesis by(cases x, auto, cases p2, auto) + with assms show ?thesis by (cases x, auto, cases p2, auto) next case Pc - from prems show ?thesis by(cases x, auto) + with assms show ?thesis by (cases x) auto next case Pinj - from prems show ?thesis by(cases x, auto) + with assms show ?thesis by (cases x) auto qed text {* mkPX conserves normalizedness (@{text "_cn"}) *} @@ -75,15 +77,17 @@ shows "isnorm (mkPX P x Q)" proof(cases P) case (Pc c) - from prems show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def) + with assms show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def) next case (Pinj i Q) - from prems show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def) + with assms show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def) next case (PX P1 y P2) - from prems have Y0:"y>0" by(cases y, auto) - from prems have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2]) - with prems Y0 show ?thesis by (cases x, auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto) + with assms have Y0: "y>0" by (cases y) auto + 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) qed text {* add conserves normalizedness *} @@ -94,118 +98,127 @@ case (3 i P2 c) thus ?case by (cases P2, simp_all, cases i, simp_all) next case (4 c P2 i Q2) - from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) - with prems show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto) + 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, case_tac pol2, auto) next case (5 P2 i Q2 c) - from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) - with prems show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto) + 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, case_tac pol2, auto) next case (6 x P2 y Q2) - from prems have Y0:"y>0" by (cases y, auto simp add: norm_Pinj_0_False) - from prems have X0:"x>0" by (cases x, auto simp add: norm_Pinj_0_False) + 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 \<or> x = y \<or> x > y" by arith moreover - { assume "x<y" hence "EX d. y=d+x" by arith - then obtain d where "y=d+x".. + { assume "x<y" hence "EX d. y =d + x" by arith + then obtain d where y: "y = d + x" .. moreover - note prems X0 + note 6 X0 moreover - from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) + from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) moreover - with prems have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto) - ultimately have ?case by (simp add: mkPinj_cn)} + 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 prems have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) + from 6 have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) moreover - note prems Y0 + note 6 Y0 moreover ultimately have ?case by (simp add: mkPinj_cn) } moreover - { assume "x>y" hence "EX d. x=d+y" by arith - then obtain d where "x=d+y".. + { assume "x>y" hence "EX d. x = d + y" by arith + then obtain d where x: "x = d + y".. moreover - note prems Y0 + note 6 Y0 moreover - from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) + from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) moreover - with prems have "isnorm (Pinj d P2)" by (cases d, simp, cases P2, auto) + 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 next case (7 x P2 Q2 y R) have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith moreover - { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)} + { assume "x = 0" + with 7 have ?case by (auto simp add: norm_Pinj_0_False) } moreover - { assume "x=1" - from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) - with prems have "isnorm (R \<oplus> P2)" by simp - with prems have ?case by (simp add: norm_PXtrans[of Q2 y _]) } + { assume "x = 1" + 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 \<oplus> P2)" by simp + with 7 `x = 1` have ?case by (simp add: norm_PXtrans[of Q2 y _]) } moreover { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith then obtain d where X:"x=Suc (Suc d)" .. - from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) - with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto) - with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp fact - with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) } + 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 \<oplus> Pinj (x - 1) P2)" by simp + with `isnorm (PX Q2 y R)` X have ?case by (simp add: norm_PXtrans[of Q2 y _]) } ultimately show ?case by blast next case (8 Q2 y R x P2) have "x = 0 \<or> x = 1 \<or> x > 1" by arith moreover - { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)} + { assume "x = 0" with 8 have ?case by (auto simp add: norm_Pinj_0_False) } moreover - { assume "x=1" - from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) - with prems have "isnorm (R \<oplus> P2)" by simp - with prems have ?case by (simp add: norm_PXtrans[of Q2 y _]) } + { assume "x = 1" + 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 \<oplus> P2)" by simp + with 8 `x = 1` have ?case by (simp add: norm_PXtrans[of Q2 y _]) } moreover { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith - then obtain d where X:"x=Suc (Suc d)" .. - from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) - with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto) - with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp fact - with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) } + then obtain d where X: "x = Suc (Suc d)" .. + 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)" by (cases P2) auto + with 8 `x > 1` NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp + with `isnorm (PX Q2 y R)` X have ?case by (simp add: norm_PXtrans[of Q2 y _]) } ultimately show ?case by blast next case (9 P1 x P2 Q1 y Q2) - from prems have Y0:"y>0" by(cases y, auto) - from prems have X0:"x>0" by(cases x, auto) - from prems have NP1:"isnorm P1" and NP2:"isnorm P2" by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2]) - from prems have NQ1:"isnorm Q1" and NQ2:"isnorm Q2" by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2]) + then have Y0: "y>0" by (cases y) auto + with 9 have X0: "x>0" by (cases x) auto + with 9 have NP1: "isnorm P1" and NP2: "isnorm P2" + 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 \<or> x = y \<or> x < y" by arith moreover - {assume sm1:"y < x" hence "EX d. x=d+y" by arith - then obtain d where sm2:"x=d+y".. - note prems NQ1 NP1 NP2 NQ2 sm1 sm2 + { assume sm1: "y < x" hence "EX d. x = d + y" by arith + then obtain d where sm2: "x = d + y" .. + note 9 NQ1 NP1 NP2 NQ2 sm1 sm2 moreover have "isnorm (PX P1 d (Pc 0))" - proof(cases P1) + proof (cases P1) case (PX p1 y p2) - with prems show ?thesis by(cases d, simp,cases p2, auto) - next case Pc from prems show ?thesis by(cases d, auto) - next case Pinj from prems show ?thesis by(cases d, auto) + with 9 sm1 sm2 show ?thesis by - (cases d, simp, cases p2, auto) + next + case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto + next + case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto qed ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)" by auto - with Y0 sm1 sm2 have ?case by (simp add: mkPX_cn)} + with Y0 sm1 sm2 have ?case by (simp add: mkPX_cn) } moreover - {assume "x=y" - from prems NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)" by auto - with Y0 prems have ?case by (simp add: mkPX_cn) } + { assume "x = y" + with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)" by auto + with `x = y` Y0 have ?case by (simp add: mkPX_cn) } moreover - {assume sm1:"x<y" hence "EX d. y=d+x" by arith - then obtain d where sm2:"y=d+x".. - note prems NQ1 NP1 NP2 NQ2 sm1 sm2 + { assume sm1: "x < y" hence "EX d. y = d + x" by arith + then obtain d where sm2: "y = d + x" .. + note 9 NQ1 NP1 NP2 NQ2 sm1 sm2 moreover have "isnorm (PX Q1 d (Pc 0))" - proof(cases Q1) + proof (cases Q1) case (PX p1 y p2) - with prems show ?thesis by(cases d, simp,cases p2, auto) - next case Pc from prems show ?thesis by(cases d, auto) - next case Pinj from prems show ?thesis by(cases d, auto) + with 9 sm1 sm2 show ?thesis by - (cases d, simp, cases p2, auto) + next + case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto + next + case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto qed ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)" by auto with X0 sm1 sm2 have ?case by (simp add: mkPX_cn)} @@ -222,138 +235,141 @@ by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn) next case (4 c P2 i Q2) - from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) - with prems show ?case - by - (case_tac "c=0",simp_all,case_tac "i=0",simp_all add: mkPX_cn) + 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) next case (5 P2 i Q2 c) - from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) - with prems show ?case - by - (case_tac "c=0",simp_all,case_tac "i=0",simp_all add: mkPX_cn) + 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) next case (6 x P2 y Q2) have "x < y \<or> x = y \<or> x > y" by arith moreover - { assume "x<y" hence "EX d. y=d+x" by arith - then obtain d where "y=d+x".. + { assume "x < y" hence "EX d. y = d + x" by arith + then obtain d where y: "y = d + x" .. moreover - note prems + note 6 moreover - from prems have "x>0" by (cases x, auto simp add: norm_Pinj_0_False) + from 6 have "x > 0" by (cases x) (auto simp add: norm_Pinj_0_False) moreover - from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) + from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) moreover - with prems have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto) - ultimately have ?case by (simp add: mkPinj_cn)} + 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" + { assume "x = y" moreover - from prems have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) + from 6 have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) moreover - with prems have "y>0" by (cases y, auto simp add: norm_Pinj_0_False) + from 6 have "y>0" by (cases y) (auto simp add: norm_Pinj_0_False) moreover - note prems + note 6 moreover ultimately have ?case by (simp add: mkPinj_cn) } moreover - { assume "x>y" hence "EX d. x=d+y" by arith - then obtain d where "x=d+y".. + { assume "x > y" hence "EX d. x = d + y" by arith + then obtain d where x: "x = d + y" .. moreover - note prems + note 6 moreover - from prems have "y>0" by (cases y, auto simp add: norm_Pinj_0_False) + from 6 have "y > 0" by (cases y) (auto simp add: norm_Pinj_0_False) moreover - from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) + from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) moreover - with prems have "isnorm (Pinj d P2)" by (cases d, simp, cases P2, auto) + 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 next case (7 x P2 Q2 y R) - from prems have Y0:"y>0" by(cases y, auto) - have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith + then have Y0: "y > 0" by (cases y) auto + have "x = 0 \<or> x = 1 \<or> x > 1" by arith moreover - { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)} + { assume "x = 0" with 7 have ?case by (auto simp add: norm_Pinj_0_False) } moreover - { assume "x=1" - from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) - with prems have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R]) - with Y0 prems have ?case by (simp add: mkPX_cn)} + { assume "x = 1" + 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 \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R]) + with 7 `x = 1` Y0 have ?case by (simp add: mkPX_cn) } moreover - { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith - then obtain d where X:"x=Suc (Suc d)" .. - from prems have NR:"isnorm R" "isnorm Q2" by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R]) - moreover - from prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto) + { assume "x > 1" hence "EX d. x = Suc (Suc d)" by arith + then obtain d where X: "x = Suc (Suc d)" .. + from 7 have NR: "isnorm R" "isnorm Q2" + by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R]) moreover - from prems have "isnorm (Pinj x P2)" by(cases P2, auto) + from 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto + moreover + from 7 have "isnorm (Pinj x P2)" by (cases P2) auto moreover - note prems + note 7 X ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto - with Y0 X have ?case by (simp add: mkPX_cn)} + with Y0 X have ?case by (simp add: mkPX_cn) } ultimately show ?case by blast next case (8 Q2 y R x P2) - from prems have Y0:"y>0" by(cases y, auto) - have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith + then have Y0: "y>0" by (cases y) auto + have "x = 0 \<or> x = 1 \<or> x > 1" by arith moreover - { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)} + { assume "x = 0" with 8 have ?case by (auto simp add: norm_Pinj_0_False) } moreover - { assume "x=1" - from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) - with prems have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R]) - with Y0 prems have ?case by (simp add: mkPX_cn) } + { assume "x = 1" + 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 \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R]) + with 8 `x = 1` Y0 have ?case by (simp add: mkPX_cn) } moreover - { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith - then obtain d where X:"x=Suc (Suc d)" .. - from prems have NR:"isnorm R" "isnorm Q2" by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R]) + { assume "x > 1" hence "EX d. x = Suc (Suc d)" by arith + then obtain d where X: "x = Suc (Suc d)" .. + from 8 have NR: "isnorm R" "isnorm Q2" + by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R]) moreover - from prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto) + from 8 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto moreover - from prems have "isnorm (Pinj x P2)" by(cases P2, auto) + from 8 X have "isnorm (Pinj x P2)" by (cases P2) auto moreover - note prems + note 8 X ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto with Y0 X have ?case by (simp add: mkPX_cn) } ultimately show ?case by blast next case (9 P1 x P2 Q1 y Q2) - from prems have X0:"x>0" by(cases x, auto) - from prems have Y0:"y>0" by(cases y, auto) - note prems + from 9 have X0: "x > 0" by (cases x) auto + from 9 have Y0: "y > 0" by (cases y) auto + note 9 moreover - from prems have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x 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 prems have "isnorm Q1" "isnorm Q2" by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2]) + 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 \<otimes> Q1)" "isnorm (P2 \<otimes> Q2)" "isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)" by (auto simp add: mkPinj_cn) - with prems X0 Y0 have + with 9 X0 Y0 have "isnorm (mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2))" "isnorm (mkPX (P1 \<otimes> mkPinj (Suc 0) Q2) x (Pc 0))" "isnorm (mkPX (Q1 \<otimes> mkPinj (Suc 0) P2) y (Pc 0))" by (auto simp add: mkPX_cn) thus ?case by (simp add: add_cn) -qed(simp) +qed simp text {* neg conserves normalizedness *} lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)" proof (induct P) case (Pinj i P2) - from prems have "isnorm P2" by (simp add: norm_Pinj[of i P2]) - with prems show ?case by(cases P2, auto, cases i, auto) + then have "isnorm P2" by (simp add: norm_Pinj[of i P2]) + with Pinj show ?case by - (cases P2, auto, cases i, auto) next - case (PX P1 x P2) - from prems have "isnorm P2" "isnorm P1" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2]) - with prems show ?case - proof(cases P1) + case (PX P1 x P2) note PX1 = this + from PX have "isnorm P2" "isnorm P1" + by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2]) + with PX show ?case + proof (cases P1) case (PX p1 y p2) - with prems show ?thesis by(cases x, auto, cases p2, auto) + with PX1 show ?thesis by - (cases x, auto, cases p2, auto) next case Pinj - with prems show ?thesis by(cases x, auto) - qed(cases x, auto) -qed(simp) + with PX1 show ?thesis by (cases x) auto + qed (cases x, auto) +qed simp text {* sub conserves normalizedness *} lemma sub_cn:"isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)" @@ -361,17 +377,18 @@ text {* sqr conserves normalizizedness *} lemma sqr_cn:"isnorm P \<Longrightarrow> isnorm (sqr P)" -proof(induct P) +proof (induct P) case (Pinj i Q) - from prems show ?case by(cases Q, auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn) + then show ?case + by - (cases Q, auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn) next case (PX P1 x P2) - from prems 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]) - with prems have - "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))" - and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))" - by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn) - thus ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn) + 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]) + with PX have "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))" + 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) qed simp text {* pow conserves normalizedness *} @@ -379,12 +396,12 @@ proof (induct n arbitrary: P rule: nat_less_induct) case (1 k) show ?case - proof (cases "k=0") + proof (cases "k = 0") case False - then have K2:"k div 2 < k" by (cases k, auto) - from prems have "isnorm (sqr P)" by (simp add: sqr_cn) - with prems K2 show ?thesis - by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn) + then have K2: "k div 2 < k" by (cases k) auto + from 1 have "isnorm (sqr P)" by (simp add: sqr_cn) + with 1 False K2 show ?thesis + by - (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn) qed simp qed

--- a/src/HOL/Decision_Procs/Cooper.thy Mon Feb 21 18:29:47 2011 +0100 +++ b/src/HOL/Decision_Procs/Cooper.thy Mon Feb 21 23:47:19 2011 +0100 @@ -495,11 +495,11 @@ | "not F = T" | "not p = NOT p" lemma not: "Ifm bbs bs (not p) = Ifm bbs bs (NOT p)" -by (cases p) auto + by (cases p) auto lemma not_qf: "qfree p \<Longrightarrow> qfree (not p)" -by (cases p, auto) + by (cases p) auto lemma not_bn: "bound0 p \<Longrightarrow> bound0 (not p)" -by (cases p, auto) + by (cases p) auto definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where "conj p q \<equiv> (if (p = F \<or> q=F) then F else if p=T then q else if q=T then p else And p q)" @@ -755,12 +755,12 @@ let ?b = "snd (zsplit0 a)" have abj: "zsplit0 a = (?j,?b)" by simp {assume "m\<noteq>0" - with prems(1)[OF abj] prems(2) have ?case by (auto simp add: Let_def split_def)} + with 3(1)[OF abj] 3(2) have ?case by (auto simp add: Let_def split_def)} moreover {assume m0: "m =0" - from abj have th: "a'=?b \<and> n=i+?j" using prems + with abj have th: "a'=?b \<and> n=i+?j" using 3 by (simp add: Let_def split_def) - from abj prems have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \<and> ?N ?b" by blast + from abj 3 m0 have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \<and> ?N ?b" by blast from th have "?I x (CN 0 n a') = ?I x (CN 0 (i+?j) ?b)" by simp also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))" by (simp add: left_distrib) finally have "?I x (CN 0 n a') = ?I x (CN 0 i a)" using th2 by simp @@ -770,9 +770,9 @@ case (4 t n a) let ?nt = "fst (zsplit0 t)" let ?at = "snd (zsplit0 t)" - have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=-?nt" using prems + have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=-?nt" using 4 by (simp add: Let_def split_def) - from abj prems have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast + from abj 4 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast from th2[simplified] th[simplified] show ?case by simp next case (5 s t n a) @@ -782,12 +782,12 @@ let ?at = "snd (zsplit0 t)" have abjs: "zsplit0 s = (?ns,?as)" by simp moreover have abjt: "zsplit0 t = (?nt,?at)" by simp - ultimately have th: "a=Add ?as ?at \<and> n=?ns + ?nt" using prems + ultimately have th: "a=Add ?as ?at \<and> n=?ns + ?nt" using 5 by (simp add: Let_def split_def) from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast - from prems have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)" by auto + from 5 have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)" by auto with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast - from abjs prems have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast + from abjs 5 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast from th3[simplified] th2[simplified] th[simplified] show ?case by (simp add: left_distrib) next @@ -798,22 +798,22 @@ let ?at = "snd (zsplit0 t)" have abjs: "zsplit0 s = (?ns,?as)" by simp moreover have abjt: "zsplit0 t = (?nt,?at)" by simp - ultimately have th: "a=Sub ?as ?at \<and> n=?ns - ?nt" using prems + ultimately have th: "a=Sub ?as ?at \<and> n=?ns - ?nt" using 6 by (simp add: Let_def split_def) from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast - from prems have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)" by auto + from 6 have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)" by auto with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast - from abjs prems have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast + from abjs 6 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast from th3[simplified] th2[simplified] th[simplified] show ?case by (simp add: left_diff_distrib) next case (7 i t n a) let ?nt = "fst (zsplit0 t)" let ?at = "snd (zsplit0 t)" - have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Mul i ?at \<and> n=i*?nt" using prems + have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Mul i ?at \<and> n=i*?nt" using 7 by (simp add: Let_def split_def) - from abj prems have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast - hence " ?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)" by simp + from abj 7 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast + hence "?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)" by simp also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: right_distrib) finally show ?case using th th2 by simp qed @@ -905,9 +905,9 @@ from zsplit0_I[OF spl, where x="i" and bs="bs"] have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto let ?N = "\<lambda> t. Inum (i#bs) t" - from prems Ia nb show ?case + from 5 Ia nb show ?case apply (auto simp add: Let_def split_def algebra_simps) - apply (cases "?r",auto) + apply (cases "?r", auto) apply (case_tac nat, auto) done next @@ -918,9 +918,9 @@ from zsplit0_I[OF spl, where x="i" and bs="bs"] have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto let ?N = "\<lambda> t. Inum (i#bs) t" - from prems Ia nb show ?case + from 6 Ia nb show ?case apply (auto simp add: Let_def split_def algebra_simps) - apply (cases "?r",auto) + apply (cases "?r", auto) apply (case_tac nat, auto) done next @@ -931,9 +931,9 @@ from zsplit0_I[OF spl, where x="i" and bs="bs"] have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto let ?N = "\<lambda> t. Inum (i#bs) t" - from prems Ia nb show ?case + from 7 Ia nb show ?case apply (auto simp add: Let_def split_def algebra_simps) - apply (cases "?r",auto) + apply (cases "?r", auto) apply (case_tac nat, auto) done next @@ -944,9 +944,9 @@ from zsplit0_I[OF spl, where x="i" and bs="bs"] have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto let ?N = "\<lambda> t. Inum (i#bs) t" - from prems Ia nb show ?case + from 8 Ia nb show ?case apply (auto simp add: Let_def split_def algebra_simps) - apply (cases "?r",auto) + apply (cases "?r", auto) apply (case_tac nat, auto) done next @@ -957,9 +957,9 @@ from zsplit0_I[OF spl, where x="i" and bs="bs"] have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto let ?N = "\<lambda> t. Inum (i#bs) t" - from prems Ia nb show ?case + from 9 Ia nb show ?case apply (auto simp add: Let_def split_def algebra_simps) - apply (cases "?r",auto) + apply (cases "?r", auto) apply (case_tac nat, auto) done next @@ -970,7 +970,7 @@ from zsplit0_I[OF spl, where x="i" and bs="bs"] have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto let ?N = "\<lambda> t. Inum (i#bs) t" - from prems Ia nb show ?case + from 10 Ia nb show ?case apply (auto simp add: Let_def split_def algebra_simps) apply (cases "?r",auto) apply (case_tac nat, auto) @@ -986,7 +986,7 @@ have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0) \<or> (j\<noteq> 0 \<and> ?c<0)" by arith moreover {assume "j=0" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def) - hence ?case using prems by (simp del: zlfm.simps)} + hence ?case using 11 `j = 0` by (simp del: zlfm.simps) } moreover {assume "?c=0" and "j\<noteq>0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] @@ -1015,7 +1015,7 @@ have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0) \<or> (j\<noteq> 0 \<and> ?c<0)" by arith moreover {assume "j=0" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def) - hence ?case using prems by (simp del: zlfm.simps)} + hence ?case using assms 12 `j = 0` by (simp del: zlfm.simps)} moreover {assume "?c=0" and "j\<noteq>0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] @@ -1100,20 +1100,20 @@ proof (induct p rule: iszlfm.induct) case (1 p q) let ?d = "\<delta> (And p q)" - from prems lcm_pos_int have dp: "?d >0" by simp - have d1: "\<delta> p dvd \<delta> (And p q)" using prems by simp - hence th: "d\<delta> p ?d" using delta_mono prems(3-4) by(simp only: iszlfm.simps) - have "\<delta> q dvd \<delta> (And p q)" using prems by simp - hence th': "d\<delta> q ?d" using delta_mono prems by(simp only: iszlfm.simps) + from 1 lcm_pos_int have dp: "?d >0" by simp + have d1: "\<delta> p dvd \<delta> (And p q)" using 1 by simp + hence th: "d\<delta> p ?d" using delta_mono 1(2,3) by(simp only: iszlfm.simps) + have "\<delta> q dvd \<delta> (And p q)" using 1 by simp + hence th': "d\<delta> q ?d" using delta_mono 1 by(simp only: iszlfm.simps) from th th' dp show ?case by simp next case (2 p q) let ?d = "\<delta> (And p q)" - from prems lcm_pos_int have dp: "?d >0" by simp - have "\<delta> p dvd \<delta> (And p q)" using prems by simp - hence th: "d\<delta> p ?d" using delta_mono prems by(simp only: iszlfm.simps) - have "\<delta> q dvd \<delta> (And p q)" using prems by simp - hence th': "d\<delta> q ?d" using delta_mono prems by(simp only: iszlfm.simps) + from 2 lcm_pos_int have dp: "?d >0" by simp + have "\<delta> p dvd \<delta> (And p q)" using 2 by simp + hence th: "d\<delta> p ?d" using delta_mono 2 by(simp only: iszlfm.simps) + have "\<delta> q dvd \<delta> (And p q)" using 2 by simp + hence th': "d\<delta> q ?d" using delta_mono 2 by(simp only: iszlfm.simps) from th th' dp show ?case by simp qed simp_all @@ -1200,7 +1200,7 @@ "mirror p = p" (* Lemmas for the correctness of \<sigma>\<rho> *) lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)" -by simp + by simp lemma minusinf_inf: assumes linp: "iszlfm p" @@ -1374,14 +1374,14 @@ lemma mirror_l: "iszlfm p \<and> d\<beta> p 1 \<Longrightarrow> iszlfm (mirror p) \<and> d\<beta> (mirror p) 1" -by (induct p rule: mirror.induct, auto) + by (induct p rule: mirror.induct) auto lemma mirror_\<delta>: "iszlfm p \<Longrightarrow> \<delta> (mirror p) = \<delta> p" -by (induct p rule: mirror.induct,auto) + by (induct p rule: mirror.induct) auto lemma \<beta>_numbound0: assumes lp: "iszlfm p" shows "\<forall> b\<in> set (\<beta> p). numbound0 b" - using lp by (induct p rule: \<beta>.induct,auto) + using lp by (induct p rule: \<beta>.induct) auto lemma d\<beta>_mono: assumes linp: "iszlfm p" @@ -1389,12 +1389,12 @@ and d: "l dvd l'" shows "d\<beta> p l'" using dr linp dvd_trans[of _ "l" "l'", simplified d] -by (induct p rule: iszlfm.induct) simp_all + by (induct p rule: iszlfm.induct) simp_all lemma \<alpha>_l: assumes lp: "iszlfm p" shows "\<forall> b\<in> set (\<alpha> p). numbound0 b" using lp -by(induct p rule: \<alpha>.induct, auto) + by(induct p rule: \<alpha>.induct) auto lemma \<zeta>: assumes linp: "iszlfm p" @@ -1402,16 +1402,16 @@ using linp proof(induct p rule: iszlfm.induct) case (1 p q) - from prems have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp - from prems have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp - from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] + from 1 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp + from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp + from 1 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] dl1 dl2 show ?case by (auto simp add: lcm_pos_int) next case (2 p q) - from prems have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp - from prems have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp - from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] + from 2 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp + from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp + from 2 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] dl1 dl2 show ?case by (auto simp add: lcm_pos_int) qed (auto simp add: lcm_pos_int) @@ -1585,31 +1585,31 @@ shows "?P (x - d)" using lp u d dp nob p proof(induct p rule: iszlfm.induct) - case (5 c e) hence c1: "c=1" and bn:"numbound0 e" by simp+ - with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] prems - show ?case by simp + case (5 c e) hence c1: "c=1" and bn:"numbound0 e" by simp_all + with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 5 + show ?case by simp next - case (6 c e) hence c1: "c=1" and bn:"numbound0 e" by simp+ - with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] prems - show ?case by simp + case (6 c e) hence c1: "c=1" and bn:"numbound0 e" by simp_all + with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 6 + show ?case by simp next - case (7 c e) hence p: "Ifm bbs (x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" by simp+ - let ?e = "Inum (x # bs) e" - {assume "(x-d) +?e > 0" hence ?case using c1 - numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp} - moreover - {assume H: "\<not> (x-d) + ?e > 0" - let ?v="Neg e" - have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp - from prems(11)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] - have nob: "\<not> (\<exists> j\<in> {1 ..d}. x = - ?e + j)" by auto - from H p have "x + ?e > 0 \<and> x + ?e \<le> d" by (simp add: c1) - hence "x + ?e \<ge> 1 \<and> x + ?e \<le> d" by simp - hence "\<exists> (j::int) \<in> {1 .. d}. j = x + ?e" by simp - hence "\<exists> (j::int) \<in> {1 .. d}. x = (- ?e + j)" - by (simp add: algebra_simps) - with nob have ?case by auto} - ultimately show ?case by blast + case (7 c e) hence p: "Ifm bbs (x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" by simp_all + let ?e = "Inum (x # bs) e" + {assume "(x-d) +?e > 0" hence ?case using c1 + numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp} + moreover + {assume H: "\<not> (x-d) + ?e > 0" + let ?v="Neg e" + have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp + from 7(5)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] + have nob: "\<not> (\<exists> j\<in> {1 ..d}. x = - ?e + j)" by auto + from H p have "x + ?e > 0 \<and> x + ?e \<le> d" by (simp add: c1) + hence "x + ?e \<ge> 1 \<and> x + ?e \<le> d" by simp + hence "\<exists> (j::int) \<in> {1 .. d}. j = x + ?e" by simp + hence "\<exists> (j::int) \<in> {1 .. d}. x = (- ?e + j)" + by (simp add: algebra_simps) + with nob have ?case by auto} + ultimately show ?case by blast next case (8 c e) hence p: "Ifm bbs (x #bs) (Ge (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" by simp+ @@ -1621,7 +1621,7 @@ {assume H: "\<not> (x-d) + ?e \<ge> 0" let ?v="Sub (C -1) e" have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))" by simp - from prems(11)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] + from 8(5)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] have nob: "\<not> (\<exists> j\<in> {1 ..d}. x = - ?e - 1 + j)" by auto from H p have "x + ?e \<ge> 0 \<and> x + ?e < d" by (simp add: c1) hence "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d" by simp @@ -1634,7 +1634,7 @@ let ?e = "Inum (x # bs) e" let ?v="(Sub (C -1) e)" have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp - from p have "x= - ?e" by (simp add: c1) with prems(11) show ?case using dp + from p have "x= - ?e" by (simp add: c1) with 3(5) show ?case using dp by simp (erule ballE[where x="1"], simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"]) next @@ -1649,12 +1649,12 @@ hence "x = - Inum (((x -d)) # bs) e + d" by simp hence "x = - Inum (a # bs) e + d" by (simp add: numbound0_I[OF bn,where b="x - d"and b'="a"and bs="bs"]) - with prems(11) have ?case using dp by simp} + with 4(5) have ?case using dp by simp} ultimately show ?case by blast next case (9 j c e) hence p: "Ifm bbs (x #bs) (Dvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp+ let ?e = "Inum (x # bs) e" - from prems have id: "j dvd d" by simp + from 9 have id: "j dvd d" by simp from c1 have "?p x = (j dvd (x+ ?e))" by simp also have "\<dots> = (j dvd x - d + ?e)" using zdvd_period[OF id, where x="x" and c="-1" and t="?e"] by simp @@ -1663,7 +1663,7 @@ next case (10 j c e) hence p: "Ifm bbs (x #bs) (NDvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp+ let ?e = "Inum (x # bs) e" - from prems have id: "j dvd d" by simp + from 10 have id: "j dvd d" by simp from c1 have "?p x = (\<not> j dvd (x+ ?e))" by simp also have "\<dots> = (\<not> j dvd x - d + ?e)" using zdvd_period[OF id, where x="x" and c="-1" and t="?e"] by simp

--- a/src/HOL/Decision_Procs/Ferrack.thy Mon Feb 21 18:29:47 2011 +0100 +++ b/src/HOL/Decision_Procs/Ferrack.thy Mon Feb 21 23:47:19 2011 +0100 @@ -495,14 +495,16 @@ assumes gt: "dvdnumcoeff t g" and gp: "g > 0" shows "real g *(Inum bs (reducecoeffh t g)) = Inum bs t" using gt -proof(induct t rule: reducecoeffh.induct) - case (1 i) hence gd: "g dvd i" by simp +proof (induct t rule: reducecoeffh.induct) + case (1 i) + hence gd: "g dvd i" by simp from gp have gnz: "g \<noteq> 0" by simp - from prems show ?case by (simp add: real_of_int_div[OF gnz gd]) + with assms show ?case by (simp add: real_of_int_div[OF gnz gd]) next - case (2 n c t) hence gd: "g dvd c" by simp + case (2 n c t) + hence gd: "g dvd c" by simp from gp have gnz: "g \<noteq> 0" by simp - from prems show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps) + from assms 2 show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps) qed (auto simp add: numgcd_def gp) fun ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" where @@ -511,14 +513,14 @@ | "ismaxcoeff t = (\<lambda>x. True)" lemma ismaxcoeff_mono: "ismaxcoeff t c \<Longrightarrow> c \<le> c' \<Longrightarrow> ismaxcoeff t c'" -by (induct t rule: ismaxcoeff.induct, auto) + by (induct t rule: ismaxcoeff.induct) auto lemma maxcoeff_ismaxcoeff: "ismaxcoeff t (maxcoeff t)" proof (induct t rule: maxcoeff.induct) case (2 n c t) hence H:"ismaxcoeff t (maxcoeff t)" . - have thh: "maxcoeff t \<le> max (abs c) (maxcoeff t)" by (simp add: le_maxI2) - from ismaxcoeff_mono[OF H thh] show ?case by (simp add: le_maxI1) + have thh: "maxcoeff t \<le> max (abs c) (maxcoeff t)" by simp + from ismaxcoeff_mono[OF H thh] show ?case by simp qed simp_all lemma zgcd_gt1: "gcd i j > (1::int) \<Longrightarrow> ((abs i > 1 \<and> abs j > 1) \<or> (abs i = 0 \<and> abs j > 1) \<or> (abs i > 1 \<and> abs j = 0))" @@ -534,30 +536,31 @@ lemma dvdnumcoeff_aux: assumes "ismaxcoeff t m" and mp:"m \<ge> 0" and "numgcdh t m > 1" shows "dvdnumcoeff t (numgcdh t m)" -using prems +using assms proof(induct t rule: numgcdh.induct) case (2 n c t) let ?g = "numgcdh t m" - from prems have th:"gcd c ?g > 1" by simp + from 2 have th:"gcd c ?g > 1" by simp from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"] have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp - moreover {assume "abs c > 1" and gp: "?g > 1" with prems + moreover {assume "abs c > 1" and gp: "?g > 1" with 2 have th: "dvdnumcoeff t ?g" by simp have th': "gcd c ?g dvd ?g" by simp from dvdnumcoeff_trans[OF th' th] have ?case by simp } moreover {assume "abs c = 0 \<and> ?g > 1" - with prems have th: "dvdnumcoeff t ?g" by simp + with 2 have th: "dvdnumcoeff t ?g" by simp have th': "gcd c ?g dvd ?g" by simp from dvdnumcoeff_trans[OF th' th] have ?case by simp hence ?case by simp } moreover {assume "abs c > 1" and g0:"?g = 0" - from numgcdh0[OF g0] have "m=0". with prems have ?case by simp } + from numgcdh0[OF g0] have "m=0". with 2 g0 have ?case by simp } ultimately show ?case by blast qed auto lemma dvdnumcoeff_aux2: - assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0" - using prems + assumes "numgcd t > 1" + shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0" + using assms proof (simp add: numgcd_def) let ?mc = "maxcoeff t" let ?g = "numgcdh t ?mc" @@ -679,10 +682,10 @@ lemma maxcoeff_nz: "nozerocoeff t \<Longrightarrow> maxcoeff t = 0 \<Longrightarrow> t = C 0" proof (induct t rule: maxcoeff.induct) case (2 n c t) - hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+ - have "max (abs c) (maxcoeff t) \<ge> abs c" by (simp add: le_maxI1) + hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp_all + have "max (abs c) (maxcoeff t) \<ge> abs c" by simp with cnz have "max (abs c) (maxcoeff t) > 0" by arith - with prems show ?case by simp + with 2 show ?case by simp qed auto lemma numgcd_nz: assumes nz: "nozerocoeff t" and g0: "numgcd t = 0" shows "t = C 0" @@ -710,7 +713,7 @@ {assume nz: "n = 0" hence ?thesis by (simp add: Let_def simp_num_pair_def)} moreover { assume nnz: "n \<noteq> 0" - {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci)} + {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci) } moreover {assume g1:"?g>1" hence g0: "?g > 0" by simp from g1 nnz have gp0: "?g' \<noteq> 0" by simp @@ -726,45 +729,48 @@ have gpdgp: "?g' dvd ?g'" by simp from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] have th2:"real ?g' * ?t = Inum bs ?t'" by simp - from prems have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def) + from g1 g'1 have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def) also have "\<dots> = (real ?g' * ?t) / (real ?g' * (real (n div ?g')))" by simp also have "\<dots> = (Inum bs ?t' / real n)" using real_of_int_div[OF gp0 gpdd] th2 gp0 by simp - finally have "?lhs = Inum bs t / real n" by (simp add: simpnum_ci) - then have ?thesis using prems by (simp add: simp_num_pair_def)} - ultimately have ?thesis by blast} - ultimately have ?thesis by blast} + finally have "?lhs = Inum bs t / real n" by simp + then have ?thesis by (simp add: simp_num_pair_def) } + ultimately have ?thesis by blast } + ultimately have ?thesis by blast } ultimately show ?thesis by blast qed lemma simp_num_pair_l: assumes tnb: "numbound0 t" and np: "n >0" and tn: "simp_num_pair (t,n) = (t',n')" shows "numbound0 t' \<and> n' >0" proof- - let ?t' = "simpnum t" + let ?t' = "simpnum t" let ?g = "numgcd ?t'" let ?g' = "gcd n ?g" - {assume nz: "n = 0" hence ?thesis using prems by (simp add: Let_def simp_num_pair_def)} + { assume nz: "n = 0" hence ?thesis using assms by (simp add: Let_def simp_num_pair_def) } moreover { assume nnz: "n \<noteq> 0" - {assume "\<not> ?g > 1" hence ?thesis using prems by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)} + { assume "\<not> ?g > 1" hence ?thesis using assms + by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0) } moreover - {assume g1:"?g>1" hence g0: "?g > 0" by simp + { assume g1:"?g>1" hence g0: "?g > 0" by simp from g1 nnz have gp0: "?g' \<noteq> 0" by simp hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith hence "?g'= 1 \<or> ?g' > 1" by arith - moreover {assume "?g'=1" hence ?thesis using prems - by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)} - moreover {assume g'1:"?g'>1" + moreover { + assume "?g' = 1" hence ?thesis using assms g1 + by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0) } + moreover { + assume g'1: "?g' > 1" have gpdg: "?g' dvd ?g" by simp - have gpdd: "?g' dvd n" by simp + have gpdd: "?g' dvd n" by simp have gpdgp: "?g' dvd ?g'" by simp from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" . from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]] have "n div ?g' >0" by simp - hence ?thesis using prems - by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0 simpnum_numbound0)} - ultimately have ?thesis by blast} - ultimately have ?thesis by blast} + hence ?thesis using assms g1 g'1 + by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0 simpnum_numbound0) } + ultimately have ?thesis by blast } + ultimately have ?thesis by blast } ultimately show ?thesis by blast qed @@ -962,14 +968,14 @@ let ?sa = "rsplit0 a" let ?sb = "rsplit0 b" let ?ca = "fst ?sa" let ?cb = "fst ?sb" let ?ta = "snd ?sa" let ?tb = "snd ?sb" - from prems have nb: "numbound0 (snd(rsplit0 (Add a b)))" + from 2 have nb: "numbound0 (snd(rsplit0 (Add a b)))" by (cases "rsplit0 a") (auto simp add: Let_def split_def) have "Inum bs ((split (CN 0)) (rsplit0 (Add a b))) = Inum bs ((split (CN 0)) ?sa)+Inum bs ((split (CN 0)) ?sb)" by (simp add: Let_def split_def algebra_simps) - also have "\<dots> = Inum bs a + Inum bs b" using prems by (cases "rsplit0 a") auto + also have "\<dots> = Inum bs a + Inum bs b" using 2 by (cases "rsplit0 a") auto finally show ?case using nb by simp -qed (auto simp add: Let_def split_def algebra_simps , simp add: right_distrib[symmetric]) +qed (auto simp add: Let_def split_def algebra_simps, simp add: right_distrib[symmetric]) (* Linearize a formula*) definition @@ -1081,8 +1087,8 @@ case (2 p q) thus ?case by (auto,rule_tac x= "min z za" in exI) auto next case (3 c e) - from prems have nb: "numbound0 e" by simp - from prems have cp: "real c > 0" by simp + from 3 have nb: "numbound0 e" by simp + from 3 have cp: "real c > 0" by simp fix a let ?e="Inum (a#bs) e" let ?z = "(- ?e) / real c" @@ -1098,8 +1104,8 @@ thus ?case by blast next case (4 c e) - from prems have nb: "numbound0 e" by simp - from prems have cp: "real c > 0" by simp + from 4 have nb: "numbound0 e" by simp + from 4 have cp: "real c > 0" by simp fix a let ?e="Inum (a#bs) e" let ?z = "(- ?e) / real c" @@ -1115,8 +1121,8 @@ thus ?case by blast next case (5 c e) - from prems have nb: "numbound0 e" by simp - from prems have cp: "real c > 0" by simp + from 5 have nb: "numbound0 e" by simp + from 5 have cp: "real c > 0" by simp fix a let ?e="Inum (a#bs) e" let ?z = "(- ?e) / real c" @@ -1131,8 +1137,8 @@ thus ?case by blast next case (6 c e) - from prems have nb: "numbound0 e" by simp - from prems have cp: "real c > 0" by simp + from 6 have nb: "numbound0 e" by simp + from lp 6 have cp: "real c > 0" by simp fix a let ?e="Inum (a#bs) e" let ?z = "(- ?e) / real c" @@ -1147,8 +1153,8 @@ thus ?case by blast next case (7 c e) - from prems have nb: "numbound0 e" by simp - from prems have cp: "real c > 0" by simp + from 7 have nb: "numbound0 e" by simp + from 7 have cp: "real c > 0" by simp fix a let ?e="Inum (a#bs) e" let ?z = "(- ?e) / real c" @@ -1163,8 +1169,8 @@ thus ?case by blast next case (8 c e) - from prems have nb: "numbound0 e" by simp - from prems have cp: "real c > 0" by simp + from 8 have nb: "numbound0 e" by simp + from 8 have cp: "real c > 0" by simp fix a let ?e="Inum (a#bs) e" let ?z = "(- ?e) / real c" @@ -1189,8 +1195,8 @@ case (2 p q) thus ?case by (auto,rule_tac x= "max z za" in exI) auto next case (3 c e) - from prems have nb: "numbound0 e" by simp - from prems have cp: "real c > 0" by simp + from 3 have nb: "numbound0 e" by simp + from 3 have cp: "real c > 0" by simp fix a let ?e="Inum (a#bs) e" let ?z = "(- ?e) / real c" @@ -1206,8 +1212,8 @@ thus ?case by blast next case (4 c e) - from prems have nb: "numbound0 e" by simp - from prems have cp: "real c > 0" by simp + from 4 have nb: "numbound0 e" by simp + from 4 have cp: "real c > 0" by simp fix a let ?e="Inum (a#bs) e" let ?z = "(- ?e) / real c" @@ -1223,8 +1229,8 @@ thus ?case by blast next case (5 c e) - from prems have nb: "numbound0 e" by simp - from prems have cp: "real c > 0" by simp + from 5 have nb: "numbound0 e" by simp + from 5 have cp: "real c > 0" by simp fix a let ?e="Inum (a#bs) e" let ?z = "(- ?e) / real c" @@ -1239,8 +1245,8 @@ thus ?case by blast next case (6 c e) - from prems have nb: "numbound0 e" by simp - from prems have cp: "real c > 0" by simp + from 6 have nb: "numbound0 e" by simp + from 6 have cp: "real c > 0" by simp fix a let ?e="Inum (a#bs) e" let ?z = "(- ?e) / real c" @@ -1255,8 +1261,8 @@ thus ?case by blast next case (7 c e) - from prems have nb: "numbound0 e" by simp - from prems have cp: "real c > 0" by simp + from 7 have nb: "numbound0 e" by simp + from 7 have cp: "real c > 0" by simp fix a let ?e="Inum (a#bs) e" let ?z = "(- ?e) / real c" @@ -1271,8 +1277,8 @@ thus ?case by blast next case (8 c e) - from prems have nb: "numbound0 e" by simp - from prems have cp: "real c > 0" by simp + from 8 have nb: "numbound0 e" by simp + from 8 have cp: "real c > 0" by simp fix a let ?e="Inum (a#bs) e" let ?z = "(- ?e) / real c" @@ -1356,7 +1362,7 @@ shows "(Ifm (x#bs) (usubst p (t,n)) = Ifm (((Inum (x#bs) t)/(real n))#bs) p) \<and> bound0 (usubst p (t,n))" (is "(?I x (usubst p (t,n)) = ?I ?u p) \<and> ?B p" is "(_ = ?I (?t/?n) p) \<and> _" is "(_ = ?I (?N x t /_) p) \<and> _") using lp proof(induct p rule: usubst.induct) - case (5 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ + case (5 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all have "?I ?u (Lt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) < 0)" using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) < 0)" @@ -1366,7 +1372,7 @@ using np by simp finally show ?case using nbt nb by (simp add: algebra_simps) next - case (6 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ + case (6 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all have "?I ?u (Le (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<le> 0)" using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<le> 0)" @@ -1376,7 +1382,7 @@ using np by simp finally show ?case using nbt nb by (simp add: algebra_simps) next - case (7 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ + case (7 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all have "?I ?u (Gt (CN 0 c e)) = (real c *(?t/?n) + (?N x e) > 0)" using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) > 0)" @@ -1386,7 +1392,7 @@ using np by simp finally show ?case using nbt nb by (simp add: algebra_simps) next - case (8 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ + case (8 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all have "?I ?u (Ge (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<ge> 0)" using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp also have "\<dots> = (?n*(real c *(?t/?n)) + ?n*(?N x e) \<ge> 0)" @@ -1396,7 +1402,7 @@ using np by simp finally show ?case using nbt nb by (simp add: algebra_simps) next - case (3 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ + case (3 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all from np have np: "real n \<noteq> 0" by simp have "?I ?u (Eq (CN 0 c e)) = (real c *(?t/?n) + (?N x e) = 0)" using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp @@ -1407,7 +1413,7 @@ using np by simp finally show ?case using nbt nb by (simp add: algebra_simps) next - case (4 c e) from prems have cp: "c >0" and nb: "numbound0 e" by simp+ + case (4 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all from np have np: "real n \<noteq> 0" by simp have "?I ?u (NEq (CN 0 c e)) = (real c *(?t/?n) + (?N x e) \<noteq> 0)" using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp @@ -1467,99 +1473,99 @@ using lp px noS proof (induct p rule: isrlfm.induct) case (5 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ - from prems have "x * real c + ?N x e < 0" by (simp add: algebra_simps) - hence pxc: "x < (- ?N x e) / real c" - by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="-?N x e"]) - from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto - with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto - hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto - moreover {assume y: "y < (-?N x e)/ real c" - hence "y * real c < - ?N x e" - by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) - hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) - hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} - moreover {assume y: "y > (- ?N x e) / real c" - with yu have eu: "u > (- ?N x e) / real c" by auto - with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto) - with lx pxc have "False" by auto - hence ?case by simp } - ultimately show ?case by blast + from 5 have "x * real c + ?N x e < 0" by (simp add: algebra_simps) + hence pxc: "x < (- ?N x e) / real c" + by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="-?N x e"]) + from 5 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto + with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto + hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto + moreover {assume y: "y < (-?N x e)/ real c" + hence "y * real c < - ?N x e" + by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) + hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) + hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} + moreover {assume y: "y > (- ?N x e) / real c" + with yu have eu: "u > (- ?N x e) / real c" by auto + with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto) + with lx pxc have "False" by auto + hence ?case by simp } + ultimately show ?case by blast next case (6 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp + - from prems have "x * real c + ?N x e \<le> 0" by (simp add: algebra_simps) - hence pxc: "x \<le> (- ?N x e) / real c" - by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="-?N x e"]) - from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto - with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto - hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto - moreover {assume y: "y < (-?N x e)/ real c" - hence "y * real c < - ?N x e" - by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) - hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) - hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} - moreover {assume y: "y > (- ?N x e) / real c" - with yu have eu: "u > (- ?N x e) / real c" by auto - with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto) - with lx pxc have "False" by auto - hence ?case by simp } - ultimately show ?case by blast + from 6 have "x * real c + ?N x e \<le> 0" by (simp add: algebra_simps) + hence pxc: "x \<le> (- ?N x e) / real c" + by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="-?N x e"]) + from 6 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto + with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto + hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto + moreover {assume y: "y < (-?N x e)/ real c" + hence "y * real c < - ?N x e" + by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) + hence "real c * y + ?N x e < 0" by (simp add: algebra_simps) + hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} + moreover {assume y: "y > (- ?N x e) / real c" + with yu have eu: "u > (- ?N x e) / real c" by auto + with noSc ly yu have "(- ?N x e) / real c \<le> l" by (cases "(- ?N x e) / real c > l", auto) + with lx pxc have "False" by auto + hence ?case by simp } + ultimately show ?case by blast next case (7 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ - from prems have "x * real c + ?N x e > 0" by (simp add: algebra_simps) - hence pxc: "x > (- ?N x e) / real c" - by (simp only: pos_divide_less_eq[OF cp, where a="x" and b="-?N x e"]) - from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto - with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto - hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto - moreover {assume y: "y > (-?N x e)/ real c" - hence "y * real c > - ?N x e" - by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) - hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) - hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} - moreover {assume y: "y < (- ?N x e) / real c" - with ly have eu: "l < (- ?N x e) / real c" by auto - with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto) - with xu pxc have "False" by auto - hence ?case by simp } - ultimately show ?case by blast + from 7 have "x * real c + ?N x e > 0" by (simp add: algebra_simps) + hence pxc: "x > (- ?N x e) / real c" + by (simp only: pos_divide_less_eq[OF cp, where a="x" and b="-?N x e"]) + from 7 have noSc: "\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto + with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto + hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto + moreover {assume y: "y > (-?N x e)/ real c" + hence "y * real c > - ?N x e" + by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) + hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) + hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} + moreover {assume y: "y < (- ?N x e) / real c" + with ly have eu: "l < (- ?N x e) / real c" by auto + with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto) + with xu pxc have "False" by auto + hence ?case by simp } + ultimately show ?case by blast next case (8 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ - from prems have "x * real c + ?N x e \<ge> 0" by (simp add: algebra_simps) - hence pxc: "x \<ge> (- ?N x e) / real c" - by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="-?N x e"]) - from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto - with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto - hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto - moreover {assume y: "y > (-?N x e)/ real c" - hence "y * real c > - ?N x e" - by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) - hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) - hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} - moreover {assume y: "y < (- ?N x e) / real c" - with ly have eu: "l < (- ?N x e) / real c" by auto - with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto) - with xu pxc have "False" by auto - hence ?case by simp } - ultimately show ?case by blast + from 8 have "x * real c + ?N x e \<ge> 0" by (simp add: algebra_simps) + hence pxc: "x \<ge> (- ?N x e) / real c" + by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="-?N x e"]) + from 8 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto + with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto + hence "y < (- ?N x e) / real c \<or> y > (-?N x e) / real c" by auto + moreover {assume y: "y > (-?N x e)/ real c" + hence "y * real c > - ?N x e" + by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric]) + hence "real c * y + ?N x e > 0" by (simp add: algebra_simps) + hence ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp} + moreover {assume y: "y < (- ?N x e) / real c" + with ly have eu: "l < (- ?N x e) / real c" by auto + with noSc ly yu have "(- ?N x e) / real c \<ge> u" by (cases "(- ?N x e) / real c > l", auto) + with xu pxc have "False" by auto + hence ?case by simp } + ultimately show ?case by blast next case (3 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ - from cp have cnz: "real c \<noteq> 0" by simp - from prems have "x * real c + ?N x e = 0" by (simp add: algebra_simps) - hence pxc: "x = (- ?N x e) / real c" - by (simp only: nonzero_eq_divide_eq[OF cnz, where a="x" and b="-?N x e"]) - from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto - with lx xu have yne: "x \<noteq> - ?N x e / real c" by auto - with pxc show ?case by simp + from cp have cnz: "real c \<noteq> 0" by simp + from 3 have "x * real c + ?N x e = 0" by (simp add: algebra_simps) + hence pxc: "x = (- ?N x e) / real c" + by (simp only: nonzero_eq_divide_eq[OF cnz, where a="x" and b="-?N x e"]) + from 3 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto + with lx xu have yne: "x \<noteq> - ?N x e / real c" by auto + with pxc show ?case by simp next case (4 c e) hence cp: "real c > 0" and nb: "numbound0 e" by simp+ - from cp have cnz: "real c \<noteq> 0" by simp - from prems have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto - with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto - hence "y* real c \<noteq> -?N x e" - by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="-?N x e"]) simp - hence "y* real c + ?N x e \<noteq> 0" by (simp add: algebra_simps) - thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] - by (simp add: algebra_simps) + from cp have cnz: "real c \<noteq> 0" by simp + from 4 have noSc:"\<forall> t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real c" by auto + with ly yu have yne: "y \<noteq> - ?N x e / real c" by auto + hence "y* real c \<noteq> -?N x e" + by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="-?N x e"]) simp + hence "y* real c + ?N x e \<noteq> 0" by (simp add: algebra_simps) + thus ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] + by (simp add: algebra_simps) qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="y" and b'="x"]) lemma finite_set_intervals:

--- a/src/HOL/Decision_Procs/MIR.thy Mon Feb 21 18:29:47 2011 +0100 +++ b/src/HOL/Decision_Procs/MIR.thy Mon Feb 21 23:47:19 2011 +0100 @@ -46,7 +46,7 @@ proof(induct rule: iupt.induct) case (1 a b) show ?case - using prems by (simp add: simp_from_to) + using 1 by (simp add: simp_from_to) qed lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)" @@ -119,7 +119,7 @@ assume "?r" hence "(i\<Colon>int) dvd \<lfloor>x\<Colon>real\<rfloor>" .. hence "\<exists> k. real (floor x) = real (i*k)" by (simp only: real_of_int_inject) (simp add: dvd_def) - thus ?l using prems by (simp add: rdvd_def) + thus ?l using `?r` by (simp add: rdvd_def) qed lemma int_rdvd_iff: "(real (i::int) rdvd real t) = (i dvd t)" @@ -705,16 +705,17 @@ proof(induct t rule: reducecoeffh.induct) case (1 i) hence gd: "g dvd i" by simp from gp have gnz: "g \<noteq> 0" by simp - from prems show ?case by (simp add: real_of_int_div[OF gnz gd]) + from assms 1 show ?case by (simp add: real_of_int_div[OF gnz gd]) next case (2 n c t) hence gd: "g dvd c" by simp from gp have gnz: "g \<noteq> 0" by simp - from prems show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps) + from assms 2 show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps) next case (3 c s t) hence gd: "g dvd c" by simp from gp have gnz: "g \<noteq> 0" by simp - from prems show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps) + from assms 3 show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps) qed (auto simp add: numgcd_def gp) + consts ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" recdef ismaxcoeff "measure size" "ismaxcoeff (C i) = (\<lambda> x. abs i \<le> x)" @@ -729,7 +730,7 @@ proof (induct t rule: maxcoeff.induct) case (2 n c t) hence H:"ismaxcoeff t (maxcoeff t)" . - have thh: "maxcoeff t \<le> max (abs c) (maxcoeff t)" by (simp add: le_maxI2) + have thh: "maxcoeff t \<le> max (abs c) (maxcoeff t)" by simp from ismaxcoeff_mono[OF H thh] show ?case by (simp add: le_maxI1) next case (3 c t s) @@ -747,60 +748,60 @@ apply auto done lemma numgcdh0:"numgcdh t m = 0 \<Longrightarrow> m =0" - by (induct t rule: numgcdh.induct, auto) + by (induct t rule: numgcdh.induct) auto lemma dvdnumcoeff_aux: assumes "ismaxcoeff t m" and mp:"m \<ge> 0" and "numgcdh t m > 1" shows "dvdnumcoeff t (numgcdh t m)" -using prems +using assms proof(induct t rule: numgcdh.induct) case (2 n c t) let ?g = "numgcdh t m" - from prems have th:"gcd c ?g > 1" by simp + from 2 have th:"gcd c ?g > 1" by simp from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"] have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp - moreover {assume "abs c > 1" and gp: "?g > 1" with prems + moreover {assume "abs c > 1" and gp: "?g > 1" with 2 have th: "dvdnumcoeff t ?g" by simp have th': "gcd c ?g dvd ?g" by simp from dvdnumcoeff_trans[OF th' th] have ?case by simp } moreover {assume "abs c = 0 \<and> ?g > 1" - with prems have th: "dvdnumcoeff t ?g" by simp + with 2 have th: "dvdnumcoeff t ?g" by simp have th': "gcd c ?g dvd ?g" by simp from dvdnumcoeff_trans[OF th' th] have ?case by simp hence ?case by simp } moreover {assume "abs c > 1" and g0:"?g = 0" - from numgcdh0[OF g0] have "m=0". with prems have ?case by simp } + from numgcdh0[OF g0] have "m=0". with 2 g0 have ?case by simp } ultimately show ?case by blast next case (3 c s t) let ?g = "numgcdh t m" - from prems have th:"gcd c ?g > 1" by simp + from 3 have th:"gcd c ?g > 1" by simp from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"] have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp - moreover {assume "abs c > 1" and gp: "?g > 1" with prems + moreover {assume "abs c > 1" and gp: "?g > 1" with 3 have th: "dvdnumcoeff t ?g" by simp have th': "gcd c ?g dvd ?g" by simp from dvdnumcoeff_trans[OF th' th] have ?case by simp } moreover {assume "abs c = 0 \<and> ?g > 1" - with prems have th: "dvdnumcoeff t ?g" by simp + with 3 have th: "dvdnumcoeff t ?g" by simp have th': "gcd c ?g dvd ?g" by simp from dvdnumcoeff_trans[OF th' th] have ?case by simp hence ?case by simp } moreover {assume "abs c > 1" and g0:"?g = 0" - from numgcdh0[OF g0] have "m=0". with prems have ?case by simp } + from numgcdh0[OF g0] have "m=0". with 3 g0 have ?case by simp } ultimately show ?case by blast qed auto lemma dvdnumcoeff_aux2: assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0" - using prems + using assms proof (simp add: numgcd_def) let ?mc = "maxcoeff t" let ?g = "numgcdh t ?mc" have th1: "ismaxcoeff t ?mc" by (rule maxcoeff_ismaxcoeff) have th2: "?mc \<ge> 0" by (rule maxcoeff_pos) assume H: "numgcdh t ?mc > 1" - from dvdnumcoeff_aux[OF th1 th2 H] show "dvdnumcoeff t ?g" . + from dvdnumcoeff_aux[OF th1 th2 H] show "dvdnumcoeff t ?g" . qed lemma reducecoeff: "real (numgcd t) * (Inum bs (reducecoeff t)) = Inum bs t" @@ -911,32 +912,33 @@ in (bv, CF c a bi))" "split_int a = (a,C 0)" -lemma split_int:"\<And> tv ti. split_int t = (tv,ti) \<Longrightarrow> (Inum bs (Add tv ti) = Inum bs t) \<and> isint ti bs" +lemma split_int: "\<And>tv ti. split_int t = (tv,ti) \<Longrightarrow> (Inum bs (Add tv ti) = Inum bs t) \<and> isint ti bs" proof (induct t rule: split_int.induct) case (2 c n b tv ti) let ?bv = "fst (split_int b)" let ?bi = "snd (split_int b)" have "split_int b = (?bv,?bi)" by simp - with prems(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+ - from prems(2) have tibi: "ti = ?bi" by (simp add: Let_def split_def) - from prems(2) b[symmetric] bii show ?case by (auto simp add: Let_def split_def) + with 2(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+ + from 2(2) have tibi: "ti = ?bi" by (simp add: Let_def split_def) + from 2(2) b[symmetric] bii show ?case by (auto simp add: Let_def split_def) next case (3 c a b tv ti) let ?bv = "fst (split_int b)" let ?bi = "snd (split_int b)" have "split_int b = (?bv,?bi)" by simp - with prems(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+ - from prems(2) have tibi: "ti = CF c a ?bi" by (simp add: Let_def split_def) - from prems(2) b[symmetric] bii show ?case by (auto simp add: Let_def split_def isint_Floor isint_add isint_Mul isint_CF) + with 3(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+ + from 3(2) have tibi: "ti = CF c a ?bi" + by (simp add: Let_def split_def) + from 3(2) b[symmetric] bii show ?case + by (auto simp add: Let_def split_def isint_Floor isint_add isint_Mul isint_CF) qed (auto simp add: Let_def isint_iff isint_Floor isint_add isint_Mul split_def algebra_simps) lemma split_int_nb: "numbound0 t \<Longrightarrow> numbound0 (fst (split_int t)) \<and> numbound0 (snd (split_int t)) " -by (induct t rule: split_int.induct, auto simp add: Let_def split_def) - -definition - numfloor:: "num \<Rightarrow> num" + by (induct t rule: split_int.induct) (auto simp add: Let_def split_def) + +definition numfloor:: "num \<Rightarrow> num" where - numfloor_def: "numfloor t = (let (tv,ti) = split_int t in + "numfloor t = (let (tv,ti) = split_int t in (case tv of C i \<Rightarrow> numadd (tv,ti) | _ \<Rightarrow> numadd(CF 1 tv (C 0),ti)))" @@ -1022,13 +1024,13 @@ hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+ have "max (abs c) (maxcoeff t) \<ge> abs c" by (simp add: le_maxI1) with cnz have "max (abs c) (maxcoeff t) > 0" by arith - with prems show ?case by simp + with 2 show ?case by simp next case (3 c s t) hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+ have "max (abs c) (maxcoeff t) \<ge> abs c" by (simp add: le_maxI1) with cnz have "max (abs c) (maxcoeff t) > 0" by arith - with prems show ?case by simp + with 3 show ?case by simp qed auto lemma numgcd_nz: assumes nz: "nozerocoeff t" and g0: "numgcd t = 0" shows "t = C 0" @@ -1072,34 +1074,35 @@ have gpdgp: "?g' dvd ?g'" by simp from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] have th2:"real ?g' * ?t = Inum bs ?t'" by simp - from prems have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def) + from nnz g1 g'1 have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def) also have "\<dots> = (real ?g' * ?t) / (real ?g' * (real (n div ?g')))" by simp also have "\<dots> = (Inum bs ?t' / real n)" using real_of_int_div[OF gp0 gpdd] th2 gp0 by simp finally have "?lhs = Inum bs t / real n" by simp - then have ?thesis using prems by (simp add: simp_num_pair_def)} - ultimately have ?thesis by blast} - ultimately have ?thesis by blast} + then have ?thesis using nnz g1 g'1 by (simp add: simp_num_pair_def) } + ultimately have ?thesis by blast } + ultimately have ?thesis by blast } ultimately show ?thesis by blast qed -lemma simp_num_pair_l: assumes tnb: "numbound0 t" and np: "n >0" and tn: "simp_num_pair (t,n) = (t',n')" +lemma simp_num_pair_l: + assumes tnb: "numbound0 t" and np: "n >0" and tn: "simp_num_pair (t,n) = (t',n')" shows "numbound0 t' \<and> n' >0" proof- - let ?t' = "simpnum t" + let ?t' = "simpnum t" let ?g = "numgcd ?t'" let ?g' = "gcd n ?g" - {assume nz: "n = 0" hence ?thesis using prems by (simp add: Let_def simp_num_pair_def)} + { assume nz: "n = 0" hence ?thesis using assms by (simp add: Let_def simp_num_pair_def) } moreover { assume nnz: "n \<noteq> 0" - {assume "\<not> ?g > 1" hence ?thesis using prems by (auto simp add: Let_def simp_num_pair_def)} + {assume "\<not> ?g > 1" hence ?thesis using assms by (auto simp add: Let_def simp_num_pair_def) } moreover {assume g1:"?g>1" hence g0: "?g > 0" by simp from g1 nnz have gp0: "?g' \<noteq> 0" by simp hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith hence "?g'= 1 \<or> ?g' > 1" by arith - moreover {assume "?g'=1" hence ?thesis using prems - by (auto simp add: Let_def simp_num_pair_def)} + moreover {assume "?g'=1" hence ?thesis using assms g1 g0 + by (auto simp add: Let_def simp_num_pair_def) } moreover {assume g'1:"?g'>1" have gpdg: "?g' dvd ?g" by simp have gpdd: "?g' dvd n" by simp @@ -1107,10 +1110,10 @@ from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" . from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]] have "n div ?g' >0" by simp - hence ?thesis using prems + hence ?thesis using assms g1 g'1 by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0)} - ultimately have ?thesis by blast} - ultimately have ?thesis by blast} + ultimately have ?thesis by blast } + ultimately have ?thesis by blast } ultimately show ?thesis by blast qed @@ -1131,43 +1134,43 @@ "not (Or p q) = And (not p) (not q)" "not p = NOT p" lemma not[simp]: "Ifm bs (not p) = Ifm bs (NOT p)" -by (induct p) auto + by (induct p) auto lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)" -by (induct p, auto) + by (induct p) auto lemma not_nb[simp]: "bound0 p \<Longrightarrow> bound0 (not p)" -by (induct p, auto) + by (induct p) auto definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where "conj p q \<equiv> (if (p = F \<or> q=F) then F else if p=T then q else if q=T then p else if p = q then p else And p q)" lemma conj[simp]: "Ifm bs (conj p q) = Ifm bs (And p q)" -by (cases "p=F \<or> q=F",simp_all add: conj_def) (cases p,simp_all) + by (cases "p=F \<or> q=F", simp_all add: conj_def) (cases p, simp_all) lemma conj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (conj p q)" -using conj_def by auto + using conj_def by auto lemma conj_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (conj p q)" -using conj_def by auto + using conj_def by auto definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where "disj p q \<equiv> (if (p = T \<or> q=T) then T else if p=F then q else if q=F then p else if p=q then p else Or p q)" lemma disj[simp]: "Ifm bs (disj p q) = Ifm bs (Or p q)" -by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases p,simp_all) + by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases p,simp_all) lemma disj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (disj p q)" -using disj_def by auto + using disj_def by auto lemma disj_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (disj p q)" -using disj_def by auto + using disj_def by auto definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm" where "imp p q \<equiv> (if (p = F \<or> q=T \<or> p=q) then T else if p=T then q else if q=F then not p else Imp p q)" lemma imp[simp]: "Ifm bs (imp p q) = Ifm bs (Imp p q)" -by (cases "p=F \<or> q=T",simp_all add: imp_def) + by (cases "p=F \<or> q=T",simp_all add: imp_def) lemma imp_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)" -using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def) + using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def) lemma imp_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (imp p q)" -using imp_def by (cases "p=F \<or> q=T \<or> p=q",simp_all add: imp_def) + using imp_def by (cases "p=F \<or> q=T \<or> p=q",simp_all add: imp_def) definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" where "iff p q \<equiv> (if (p = q) then T else if (p = not q \<or> not p = q) then F else @@ -1245,7 +1248,8 @@ have gpdgp: "?g' dvd ?g'" by simp from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] have th2:"real ?g' * ?t = Inum bs t" by simp - from prems have "Ifm bs (Dvd (fst (simpdvd d t)) (snd(simpdvd d t))) = Ifm bs (Dvd (d div ?g') ?tt)" + from assms g1 g0 g'1 + have "Ifm bs (Dvd (fst (simpdvd d t)) (snd(simpdvd d t))) = Ifm bs (Dvd (d div ?g') ?tt)" by (simp add: simpdvd_def Let_def) also have "\<dots> = (real d rdvd (Inum bs t))" using rdvd_reduce[OF gpdd gpdgp g'p, where t="?t", simplified zdiv_self[OF gp0]] @@ -1544,9 +1548,8 @@ lemma qelim_ci: assumes qe_inv: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bs (qe p) = Ifm bs (E p))" shows "\<And> bs. qfree (qelim p qe) \<and> (Ifm bs (qelim p qe) = Ifm bs p)" -using qe_inv DJ_qe[OF CJNB_qe[OF qe_inv]] -by(induct p rule: qelim.induct) -(auto simp del: simpfm.simps) + using qe_inv DJ_qe[OF CJNB_qe[OF qe_inv]] + by (induct p rule: qelim.induct) (auto simp del: simpfm.simps) text {* The @{text "\<int>"} Part *} @@ -1584,7 +1587,7 @@ case (5 t n a) let ?nt = "fst (zsplit0 t)" let ?at = "snd (zsplit0 t)" - have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=-?nt" using prems + have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=-?nt" using 5 by (simp add: Let_def split_def) from abj prems have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast from th2[simplified] th[simplified] show ?case by simp

--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Feb 21 18:29:47 2011 +0100 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Feb 21 23:47:19 2011 +0100 @@ -144,11 +144,10 @@ {assume nxs: "n \<ge> length (x#xs)" hence ?case using removen_same[OF nxs] by simp} moreover {assume nxs: "\<not> (n \<ge> length (x#xs))" - {assume mln: "m < n" hence ?case using prems by (cases m, auto)} + {assume mln: "m < n" hence ?case using Cons by (cases m, auto)} moreover {assume mln: "\<not> (m < n)" - - {assume mxs: "m \<le> length (x#xs)" hence ?case using prems by (cases m, auto)} + {assume mxs: "m \<le> length (x#xs)" hence ?case using Cons by (cases m, auto)} moreover {assume mxs: "\<not> (m \<le> length (x#xs))" have th: "length (removen n (x#xs)) = length xs" @@ -162,15 +161,13 @@ ultimately have ?case by blast } ultimately have ?case by blast - - } ultimately show ?case by blast + } ultimately show ?case by blast qed lemma decrtm: assumes bnd: "tmboundslt (length bs) t" 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 add: removen_nth) primrec tmsubst0:: "tm \<Rightarrow> tm \<Rightarrow> tm" where "tmsubst0 t (CP c) = CP c" @@ -182,10 +179,10 @@ | "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)" lemma tmsubst0: shows "Itm vs (x#bs) (tmsubst0 t a) = Itm vs ((Itm vs (x#bs) t)#bs) a" -by (induct a rule: tm.induct,auto simp add: nth_pos2) + by (induct a rule: tm.induct) (auto simp add: nth_pos2) lemma tmsubst0_nb: "tmbound0 t \<Longrightarrow> tmbound0 (tmsubst0 t a)" -by (induct a rule: tm.induct,auto simp add: nth_pos2) + by (induct a rule: tm.induct) (auto simp add: nth_pos2) primrec tmsubst:: "nat \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm" where "tmsubst n t (CP c) = CP c" @@ -569,13 +566,13 @@ proof(induct p arbitrary: bs n rule: fm.induct) case (E p bs n) {fix y - from prems have bnd: "boundslt (length (y#bs)) p" + from E have bnd: "boundslt (length (y#bs)) p" and nb: "bound (Suc n) p" and le: "Suc n \<le> length (y#bs)" by simp+ from E.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" . } thus ?case by simp next case (A p bs n) {fix y - from prems have bnd: "boundslt (length (y#bs)) p" + from A have bnd: "boundslt (length (y#bs)) p" and nb: "bound (Suc n) p" and le: "Suc n \<le> length (y#bs)" by simp+ from A.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" . } thus ?case by simp @@ -620,16 +617,16 @@ proof(induct p arbitrary: bs m rule: fm.induct) case (E p bs m) {fix x - from prems have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p" + from E have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p" and nle: "Suc m < length (x#bs)" by auto - from prems(4)[OF bnd nb nle] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p". + from E(1)[OF bnd nb nle] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p". } thus ?case by auto next case (A p bs m) {fix x - from prems have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p" + from A have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p" and nle: "Suc m < length (x#bs)" by auto - from prems(4)[OF bnd nb nle] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p". + from A(1)[OF bnd nb nle] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p". } thus ?case by auto qed (auto simp add: decrtm removen_nth) @@ -680,18 +677,18 @@ proof (induct p arbitrary: bs n t rule: fm.induct) case (E p bs n) {fix x - from prems have bn: "boundslt (length (x#bs)) p" by simp - from prems have nlm: "Suc n \<le> length (x#bs)" by simp - from prems(3)[OF bn nlm] have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p" by simp + from E have bn: "boundslt (length (x#bs)) p" by simp + from E have nlm: "Suc n \<le> length (x#bs)" by simp + from E(1)[OF bn nlm] have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p" by simp hence "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs (x#bs[n:= Itm vs bs t]) p" by (simp add: incrtm0[where x="x" and bs="bs" and t="t"]) } thus ?case by simp next case (A p bs n) {fix x - from prems have bn: "boundslt (length (x#bs)) p" by simp - from prems have nlm: "Suc n \<le> length (x#bs)" by simp - from prems(3)[OF bn nlm] have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p" by simp + from A have bn: "boundslt (length (x#bs)) p" by simp + from A have nlm: "Suc n \<le> length (x#bs)" by simp + from A(1)[OF bn nlm] have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p" by simp hence "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs (x#bs[n:= Itm vs bs t]) p" by (simp add: incrtm0[where x="x" and bs="bs" and t="t"]) } thus ?case by simp @@ -1371,7 +1368,7 @@ case 2 thus ?case by (auto,rule_tac x="min z za" in exI, auto) next case (3 c e) hence nbe: "tmbound0 e" by simp - from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all + from 3 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a] let ?c = "Ipoly vs c" let ?e = "Itm vs (y#bs) e" @@ -1393,7 +1390,7 @@ ultimately show ?case by blast next case (4 c e) hence nbe: "tmbound0 e" by simp - from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all + from 4 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a] let ?c = "Ipoly vs c" let ?e = "Itm vs (y#bs) e" @@ -1414,7 +1411,7 @@ ultimately show ?case by blast next case (5 c e) hence nbe: "tmbound0 e" by simp - from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all + from 5 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" by (simp add: polyneg_norm) note eqs = lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] lt[OF nc(2), where ?'a = 'a] let ?c = "Ipoly vs c" @@ -1436,7 +1433,7 @@ ultimately show ?case by blast next case (6 c e) hence nbe: "tmbound0 e" by simp - from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all + from 6 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" by (simp add: polyneg_norm) note eqs = lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] le[OF nc(2), where ?'a = 'a] let ?c = "Ipoly vs c" @@ -1467,7 +1464,7 @@ case 2 thus ?case by (auto,rule_tac x="max z za" in exI, auto) next case (3 c e) hence nbe: "tmbound0 e" by simp - from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all + from 3 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a] let ?c = "Ipoly vs c" let ?e = "Itm vs (y#bs) e" @@ -1488,8 +1485,8 @@ using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto} hence ?case by auto} ultimately show ?case by blast next - case (4 c e) hence nbe: "tmbound0 e" by simp - from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all + case (4 c e) hence nbe: "tmbound0 e" by simp + from 4 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a] let ?c = "Ipoly vs c" let ?e = "Itm vs (y#bs) e" @@ -1509,8 +1506,8 @@ using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto} ultimately show ?case by blast next - case (5 c e) hence nbe: "tmbound0 e" by simp - from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all + case (5 c e) hence nbe: "tmbound0 e" by simp + from 5 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" by (simp add: polyneg_norm) note eqs = lt[OF nc(1), where ?'a = 'a] lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] lt[OF nc(2), where ?'a = 'a] let ?c = "Ipoly vs c" @@ -1532,7 +1529,7 @@ ultimately show ?case by blast next case (6 c e) hence nbe: "tmbound0 e" by simp - from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all + from 6 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" by (simp add: polyneg_norm) note eqs = lt[OF nc(1), where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] le[OF nc(2), where ?'a = 'a] let ?c = "Ipoly vs c"

--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Mon Feb 21 18:29:47 2011 +0100 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Mon Feb 21 23:47:19 2011 +0100 @@ -253,53 +253,53 @@ \<Longrightarrow> isnpolyh (polyadd(p,q)) (min n0 n1)" proof(induct p q arbitrary: n0 n1 rule: polyadd.induct) case (2 a b c' n' p' n0 n1) - from prems have th1: "isnpolyh (C (a,b)) (Suc n')" by simp - from prems(3) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \<ge> n1" by simp_all + from 2 have th1: "isnpolyh (C (a,b)) (Suc n')" by simp + from 2(3) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \<ge> n1" by simp_all with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp - with prems(1)[OF th1 th2] have th3:"isnpolyh (C (a,b) +\<^sub>p c') (Suc n')" by simp + with 2(1)[OF th1 th2] have th3:"isnpolyh (C (a,b) +\<^sub>p c') (Suc n')" by simp from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp - thus ?case using prems th3 by simp + thus ?case using 2 th3 by simp next case (3 c' n' p' a b n1 n0) - from prems have th1: "isnpolyh (C (a,b)) (Suc n')" by simp - from prems(2) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \<ge> n1" by simp_all + from 3 have th1: "isnpolyh (C (a,b)) (Suc n')" by simp + from 3(2) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \<ge> n1" by simp_all with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp - with prems(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C (a,b)) (Suc n')" by simp + with 3(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C (a,b)) (Suc n')" by simp from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp - thus ?case using prems th3 by simp + thus ?case using 3 th3 by simp next case (4 c n p c' n' p' n0 n1) hence nc: "isnpolyh c (Suc n)" and np: "isnpolyh p n" by simp_all - from prems have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" by simp_all - from prems have ngen0: "n \<ge> n0" by simp - from prems have n'gen1: "n' \<ge> n1" by simp + from 4 have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" by simp_all + from 4 have ngen0: "n \<ge> n0" by simp + from 4 have n'gen1: "n' \<ge> n1" by simp have "n < n' \<or> n' < n \<or> n = n'" by auto moreover {assume eq: "n = n'" - with prems(2)[OF nc nc'] + with 4(2)[OF nc nc'] have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)" by auto hence ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)" using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1 by auto - from eq prems(1)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp + from eq 4(1)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp have minle: "min n0 n1 \<le> n'" using ngen0 n'gen1 eq by simp - from minle npp' ncc'n01 prems ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)} + from minle npp' ncc'n01 eq ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)} moreover {assume lt: "n < n'" have "min n0 n1 \<le> n0" by simp - with prems have th1:"min n0 n1 \<le> n" by auto - from prems have th21: "isnpolyh c (Suc n)" by simp - from prems have th22: "isnpolyh (CN c' n' p') n'" by simp + with 4 have th1:"min n0 n1 \<le> n" by auto + from 4 have th21: "isnpolyh c (Suc n)" by simp + from 4 have th22: "isnpolyh (CN c' n' p') n'" by simp from lt have th23: "min (Suc n) n' = Suc n" by arith - from prems(4)[OF th21 th22] + from 4(4)[OF th21 th22] have "isnpolyh (polyadd (c, CN c' n' p')) (Suc n)" using th23 by simp - with prems th1 have ?case by simp } + with 4 lt th1 have ?case by simp } moreover {assume gt: "n' < n" hence gt': "n' < n \<and> \<not> n < n'" by simp have "min n0 n1 \<le> n1" by simp - with prems have th1:"min n0 n1 \<le> n'" by auto - from prems have th21: "isnpolyh c' (Suc n')" by simp_all - from prems have th22: "isnpolyh (CN c n p) n" by simp + with 4 have th1:"min n0 n1 \<le> n'" by auto + from 4 have th21: "isnpolyh c' (Suc n')" by simp_all + from 4 have th22: "isnpolyh (CN c n p) n" by simp from gt have th23: "min n (Suc n') = Suc n'" by arith - from prems(3)[OF th22 th21] + from 4(3)[OF th22 th21] have "isnpolyh (polyadd (CN c n p,c')) (Suc n')" using th23 by simp - with prems th1 have ?case by simp} + with 4 gt th1 have ?case by simp} ultimately show ?case by blast qed auto @@ -370,14 +370,15 @@ \<Longrightarrow> degreen p m = degreen q m" proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct) case (4 c n p c' n' p' m n0 n1 x) - {assume nn': "n' < n" hence ?case using prems by simp} + {assume nn': "n' < n" hence ?case using 4 by simp} moreover {assume nn':"\<not> n' < n" hence "n < n' \<or> n = n'" by arith - moreover {assume "n < n'" with prems have ?case by simp } - moreover {assume eq: "n = n'" hence ?case using prems + moreover {assume "n < n'" with 4 have ?case by simp } + moreover {assume eq: "n = n'" hence ?case using 4 apply (cases "p +\<^sub>p p' = 0\<^sub>p") apply (auto simp add: Let_def) - by blast + apply blast + done } ultimately have ?case by blast} ultimately show ?case by blast @@ -664,13 +665,13 @@ qed lemma polypow_normh: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n" proof (induct k arbitrary: n rule: polypow.induct) case (2 k n) let ?q = "polypow (Suc k div 2) p" let ?d = "polymul (?q,?q)" - from prems have th1:"isnpolyh ?q n" and th2: "isnpolyh p n" by blast+ + from 2 have th1:"isnpolyh ?q n" and th2: "isnpolyh p n" by blast+ from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n" by simp from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul(p,?d)) n" by simp from dn on show ?case by (simp add: Let_def) @@ -695,7 +696,7 @@ lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)" -by (simp add: shift1_def polymul) + by (simp add: shift1_def) lemma shift1_isnpoly: assumes pn: "isnpoly p" and pnz: "p \<noteq> 0\<^sub>p" shows "isnpoly (shift1 p) " @@ -713,7 +714,7 @@ using f np by (induct k arbitrary: p, auto) lemma funpow_shift1: "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (Mul (Pw (Bound 0) n) p)" - by (induct n arbitrary: p, simp_all add: shift1_isnpoly shift1 power_Suc ) + by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1) lemma shift1_isnpolyh: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> isnpolyh (shift1 p) 0" using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def) @@ -731,10 +732,10 @@ using np proof (induct p arbitrary: n rule: behead.induct) case (1 c p n) hence pn: "isnpolyh p n" by simp - from prems(2)[OF pn] + from 1(1)[OF pn] have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" . then show ?case using "1.hyps" apply (simp add: Let_def,cases "behead p = 0\<^sub>p") - by (simp_all add: th[symmetric] field_simps power_Suc) + by (simp_all add: th[symmetric] field_simps) qed (auto simp add: Let_def) lemma behead_isnpolyh: @@ -747,7 +748,7 @@ case (goal1 c n p n') hence "n = Suc (n - 1)" by simp hence "isnpolyh p (Suc (n - 1))" using `isnpolyh p n` by simp - with prems(2) show ?case by simp + with goal1(2) show ?case by simp qed lemma isconstant_polybound0: "isnpolyh p n0 \<Longrightarrow> isconstant p \<longleftrightarrow> polybound0 p" @@ -838,7 +839,7 @@ qed lemma decr_maxindex: "polybound0 p \<Longrightarrow> maxindex (decrpoly p) = maxindex p - 1" - by (induct p, auto) + by (induct p) auto lemma wf_bs_insensitive: "length bs = length bs' \<Longrightarrow> wf_bs bs p = wf_bs bs' p" unfolding wf_bs_def by simp @@ -1033,7 +1034,7 @@ isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all lemma polymul_1[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and np: "isnpolyh p n0" shows "p *\<^sub>p 1\<^sub>p = p" and "1\<^sub>p *\<^sub>p p = p" using isnpolyh_unique[OF polymul_normh[OF np one_normh] np] isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all @@ -1101,17 +1102,17 @@ next case (2 a b c' n' p') let ?c = "(a,b)" - from prems have "degree (C ?c) = degree (CN c' n' p')" by simp + from 2 have "degree (C ?c) = degree (CN c' n' p')" by simp hence nz:"n' > 0" by (cases n', auto) hence "head (CN c' n' p') = CN c' n' p'" by (cases n', auto) - with prems show ?case by simp + with 2 show ?case by simp next case (3 c n p a' b') let ?c' = "(a',b')" - from prems have "degree (C ?c') = degree (CN c n p)" by simp + from 3 have "degree (C ?c') = degree (CN c n p)" by simp hence nz:"n > 0" by (cases n, auto) hence "head (CN c n p) = CN c n p" by (cases n, auto) - with prems show ?case by simp + with 3 show ?case by simp next case (4 c n p c' n' p') hence H: "isnpolyh (CN c n p) n0" "isnpolyh (CN c' n' p') n1" @@ -1126,36 +1127,40 @@ moreover {assume nn': "n = n'" have "n = 0 \<or> n >0" by arith - moreover {assume nz: "n = 0" hence ?case using prems by (auto simp add: Let_def degcmc')} + moreover {assume nz: "n = 0" hence ?case using 4 nn' by (auto simp add: Let_def degcmc')} moreover {assume nz: "n > 0" - with nn' H(3) have cc':"c = c'" and pp': "p = p'" by (cases n, auto)+ - hence ?case using polysub_same_0[OF p'nh, simplified polysub_def split_def fst_conv snd_conv] polysub_same_0[OF c'nh, simplified polysub_def split_def fst_conv snd_conv] using nn' prems by (simp add: Let_def)} + with nn' H(3) have cc': "c = c'" and pp': "p = p'" by (cases n, auto)+ + hence ?case + using polysub_same_0 [OF p'nh, simplified polysub_def split_def fst_conv snd_conv] + polysub_same_0 [OF c'nh, simplified polysub_def split_def fst_conv snd_conv] + using 4 nn' by (simp add: Let_def) } ultimately have ?case by blast} moreover {assume nn': "n < n'" hence n'p: "n' > 0" by simp hence headcnp':"head (CN c' n' p') = CN c' n' p'" by (cases n', simp_all) - have degcnp': "degree (CN c' n' p') = 0" and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')" using prems by (cases n', simp_all) - hence "n > 0" by (cases n, simp_all) - hence headcnp: "head (CN c n p) = CN c n p" by (cases n, auto) - from H(3) headcnp headcnp' nn' have ?case by auto} + have degcnp': "degree (CN c' n' p') = 0" and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')" + using 4 nn' by (cases n', simp_all) + hence "n > 0" by (cases n) simp_all + hence headcnp: "head (CN c n p) = CN c n p" by (cases n) auto + from H(3) headcnp headcnp' nn' have ?case by auto } moreover {assume nn': "n > n'" hence np: "n > 0" by simp - hence headcnp:"head (CN c n p) = CN c n p" by (cases n, simp_all) - from prems have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp - from np have degcnp: "degree (CN c n p) = 0" by (cases n, simp_all) + hence headcnp: "head (CN c n p) = CN c n p" by (cases n) simp_all + from 4 have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp + from np have degcnp: "degree (CN c n p) = 0" by (cases n) simp_all with degcnpeq have "n' > 0" by (cases n', simp_all) - hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n', auto) - from H(3) headcnp headcnp' nn' have ?case by auto} + hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n') auto + from H(3) headcnp headcnp' nn' have ?case by auto } ultimately show ?case by blast qed auto lemma shift1_head : "isnpolyh p n0 \<Longrightarrow> head (shift1 p) = head p" -by (induct p arbitrary: n0 rule: head.induct, simp_all add: shift1_def) + by (induct p arbitrary: n0 rule: head.induct) (simp_all add: shift1_def) lemma funpow_shift1_head: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> head (funpow k shift1 p) = head p" proof(induct k arbitrary: n0 p) case (Suc k n0 p) hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh) - with prems have "head (funpow k shift1 (shift1 p)) = head (shift1 p)" + with Suc have "head (funpow k shift1 (shift1 p)) = head (shift1 p)" and "head (shift1 p) = head p" by (simp_all add: shift1_head) thus ?case by (simp add: funpow_swap1) qed auto @@ -1194,19 +1199,20 @@ apply (metis head_nz) apply (metis head_nz) apply (metis degree.simps(9) gr0_conv_Suc head.simps(1) less_Suc0 not_less_eq) -by (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans) +apply (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans) +done lemma polymul_head_polyeq: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "\<lbrakk>isnpolyh p n0; isnpolyh q n1 ; p \<noteq> 0\<^sub>p ; q \<noteq> 0\<^sub>p \<rbrakk> \<Longrightarrow> head (p *\<^sub>p q) = head p *\<^sub>p head q" proof (induct p q arbitrary: n0 n1 rule: polymul.induct) case (2 a b c' n' p' n0 n1) hence "isnpolyh (head (CN c' n' p')) n1" "isnormNum (a,b)" by (simp_all add: head_isnpolyh) - thus ?case using prems by (cases n', auto) + thus ?case using 2 by (cases n') auto next case (3 c n p a' b' n0 n1) hence "isnpolyh (head (CN c n p)) n0" "isnormNum (a',b')" by (simp_all add: head_isnpolyh) - thus ?case using prems by (cases n, auto) + thus ?case using 3 by (cases n) auto next case (4 c n p c' n' p' n0 n1) hence norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')" @@ -1215,15 +1221,14 @@ have "n < n' \<or> n' < n \<or> n = n'" by arith moreover {assume nn': "n < n'" hence ?case - thm prems - using norm - prems(6)[rule_format, OF nn' norm(1,6)] - prems(7)[rule_format, OF nn' norm(2,6)] by (simp, cases n, simp,cases n', simp_all)} + using norm + 4(5)[rule_format, OF nn' norm(1,6)] + 4(6)[rule_format, OF nn' norm(2,6)] by (simp, cases n, simp,cases n', simp_all) } moreover {assume nn': "n'< n" hence stupid: "n' < n \<and> \<not> n < n'" by simp - hence ?case using norm prems(4) [rule_format, OF stupid norm(5,3)] - prems(5)[rule_format, OF stupid norm(5,4)] - by (simp,cases n',simp,cases n,auto)} + hence ?case using norm 4(3) [rule_format, OF stupid norm(5,3)] + 4(4)[rule_format, OF stupid norm(5,4)] + by (simp,cases n',simp,cases n,auto) } moreover {assume nn': "n' = n" hence stupid: "\<not> n' < n \<and> \<not> n < n'" by simp from nn' polymul_normh[OF norm(5,4)] @@ -1247,8 +1252,8 @@ have dth:"degree (CN c 0 p *\<^sub>p c') < degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" by simp hence dth':"degree (CN c 0 p *\<^sub>p c') \<noteq> degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" by simp from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth - have ?case using norm prems(2)[rule_format, OF stupid norm(5,3)] - prems(3)[rule_format, OF stupid norm(5,4)] nn' nz by simp } + have ?case using norm 4(1)[rule_format, OF stupid norm(5,3)] + 4(2)[rule_format, OF stupid norm(5,4)] nn' nz by simp } ultimately have ?case by (cases n) auto} ultimately show ?case by blast qed simp_all @@ -1603,12 +1608,13 @@ definition "swapnorm n m t = polynate (swap n m t)" -lemma swapnorm: assumes nbs: "n < length bs" and mbs: "m < length bs" +lemma swapnorm: + assumes nbs: "n < length bs" and mbs: "m < length bs" shows "((Ipoly bs (swapnorm n m t) :: 'a\<Colon>{field_char_0, field_inverse_zero})) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t" - using swap[OF prems] swapnorm_def by simp + using swap[OF assms] swapnorm_def by simp lemma swapnorm_isnpoly[simp]: - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "isnpoly (swapnorm n m p)" unfolding swapnorm_def by simp @@ -1625,9 +1631,9 @@ "isweaknpoly p = False" lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \<Longrightarrow> isweaknpoly p" - by (induct p arbitrary: n0, auto) + by (induct p arbitrary: n0) auto lemma swap_isweanpoly: "isweaknpoly p \<Longrightarrow> isweaknpoly (swap n m p)" - by (induct p, auto) + by (induct p) auto end \ No newline at end of file