merged, resolving spurious conflicts and giving up Reflected_Multivariate_Polynomial.thy from ab5d2d81f9fb;
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy Mon Feb 21 23:14:36 2011 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Mon Feb 21 23:54:53 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 23:14:36 2011 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Mon Feb 21 23:54:53 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 23:14:36 2011 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy Mon Feb 21 23:54:53 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 23:14:36 2011 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy Mon Feb 21 23:54:53 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 23:14:36 2011 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Mon Feb 21 23:54:53 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 23:14:36 2011 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Feb 21 23:54:53 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"