--- a/src/HOL/Decision_Procs/Commutative_Ring.thy Thu Feb 27 21:27:58 2014 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Thu Feb 27 21:31:58 2014 +0100
@@ -143,7 +143,7 @@
| "pow n P =
(if even n then pow (n div 2) (sqr P)
else P \<otimes> pow (n div 2) (sqr P))"
-
+
lemma pow_if:
"pow n P =
(if n = 0 then Pc 1 else if even n then pow (n div 2) (sqr P)
--- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Thu Feb 27 21:27:58 2014 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Thu Feb 27 21:31:58 2014 +0100
@@ -59,9 +59,9 @@
apply (case_tac y, auto)
done
-lemma norm_PXtrans:
+lemma norm_PXtrans:
assumes A: "isnorm (PX P x Q)"
- and "isnorm Q2"
+ and "isnorm Q2"
shows "isnorm (PX P x Q2)"
proof (cases P)
case (PX p1 y p2)
@@ -78,31 +78,34 @@
case Pinj
with assms show ?thesis by (cases x) auto
qed
-
-lemma norm_PXtrans2:
- assumes "isnorm (PX P x Q)" and "isnorm Q2"
- shows "isnorm (PX P (Suc (n + x)) Q2)"
-proof (cases P)
- case (PX p1 y p2)
- with assms show ?thesis
- apply (cases x)
- apply auto
- apply (cases p2)
- apply auto
- done
-next
- case Pc
- with assms show ?thesis by (cases x) auto
-next
- case Pinj
- with assms show ?thesis by (cases x) auto
-qed
+lemma norm_PXtrans2:
+ assumes "isnorm (PX P x Q)"
+ and "isnorm Q2"
+ shows "isnorm (PX P (Suc (n + x)) Q2)"
+proof (cases P)
+ case (PX p1 y p2)
+ with assms show ?thesis
+ apply (cases x)
+ apply auto
+ apply (cases p2)
+ apply auto
+ done
+next
+ case Pc
+ with assms show ?thesis
+ by (cases x) auto
+next
+ case Pinj
+ with assms show ?thesis
+ by (cases x) auto
+qed
+
text {* mkPX conserves normalizedness (@{text "_cn"}) *}
-lemma mkPX_cn:
+lemma mkPX_cn:
assumes "x \<noteq> 0"
and "isnorm P"
- and "isnorm Q"
+ and "isnorm Q"
shows "isnorm (mkPX P x Q)"
proof (cases P)
case (Pc c)
@@ -114,7 +117,8 @@
by (cases x) (auto simp add: mkPinj_cn mkPX_def)
next
case (PX P1 y P2)
- with assms have Y0: "y > 0" by (cases y) 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
@@ -125,10 +129,12 @@
lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
proof (induct P Q rule: add.induct)
case (2 c i P2)
- then show ?case by (cases P2) (simp_all, cases i, simp_all)
+ then show ?case
+ by (cases P2) (simp_all, cases i, simp_all)
next
case (3 i P2 c)
- then show ?case by (cases P2) (simp_all, cases i, simp_all)
+ then show ?case
+ by (cases P2) (simp_all, cases i, simp_all)
next
case (4 c P2 i Q2)
then have "isnorm P2" "isnorm Q2"
@@ -143,11 +149,13 @@
by (cases i) (simp, cases P2, auto, case_tac pol2, auto)
next
case (6 x P2 y Q2)
- then have Y0: "y>0" by (cases y) (auto simp add: norm_Pinj_0_False)
- with 6 have X0: "x>0" by (cases x) (auto simp add: norm_Pinj_0_False)
+ 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"
+ moreover {
+ assume "x < y"
then have "\<exists>d. y = d + x" by arith
then obtain d where y: "y = d + x" ..
moreover
@@ -158,18 +166,22 @@
moreover
from 6 `x < y` y have "isnorm (Pinj d Q2)"
by (cases d, simp, cases Q2, auto)
- ultimately have ?case by (simp add: mkPinj_cn) }
- moreover
- { assume "x = y"
+ ultimately have ?case by (simp add: mkPinj_cn)
+ }
+ moreover {
+ assume "x = y"
moreover
from 6 have "isnorm P2" "isnorm Q2"
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
moreover
note 6 Y0
- ultimately have ?case by (simp add: mkPinj_cn) }
- moreover
- { assume "x > y" then have "\<exists>d. x = d + y" by arith
- then obtain d where x: "x = d + y"..
+ ultimately have ?case by (simp add: mkPinj_cn)
+ }
+ moreover {
+ assume "x > y"
+ then have "\<exists>d. x = d + y"
+ by arith
+ then obtain d where x: "x = d + y" ..
moreover
note 6 Y0
moreover
@@ -178,111 +190,150 @@
moreover
from 6 `x > y` x have "isnorm (Pinj d P2)"
by (cases d) (simp, cases P2, auto)
- ultimately have ?case by (simp add: mkPinj_cn) }
+ ultimately 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 7 have ?case by (auto simp add: norm_Pinj_0_False) }
- moreover
- { assume "x = 1"
+ moreover {
+ assume "x = 0"
+ with 7 have ?case by (auto simp add: norm_Pinj_0_False)
+ }
+ moreover {
+ 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" then have "\<exists>d. x=Suc (Suc d)" by arith
+ by (simp add: norm_PXtrans[of Q2 y _])
+ }
+ moreover {
+ assume "x > 1" then have "\<exists>d. x=Suc (Suc d)" by arith
then obtain d where X: "x=Suc (Suc d)" ..
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 _]) }
+ 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 8 have ?case by (auto simp add: norm_Pinj_0_False) }
- moreover
- { 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" then have "\<exists>d. x=Suc (Suc d)" by arith
+ moreover {
+ assume "x = 0"
+ with 8 have ?case
+ by (auto simp add: norm_Pinj_0_False)
+ }
+ moreover {
+ 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"
+ then have "\<exists>d. x = Suc (Suc d)" by arith
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 _]) }
+ 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)
- then have Y0: "y>0" by (cases y) auto
- with 9 have X0: "x>0" by (cases x) auto
+ 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" then have "\<exists>d. x = d + y" by arith
+ moreover {
+ assume sm1: "y < x"
+ then have "\<exists>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))"
+ have "isnorm (PX P1 d (Pc 0))"
proof (cases P1)
case (PX p1 y p2)
- with 9 sm1 sm2 show ?thesis by (cases d) (simp, cases p2, 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
+ 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
+ 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) }
- moreover
- { 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" then have "\<exists>d. y = d + x" by arith
+ 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)
+ }
+ moreover {
+ 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"
+ then have "\<exists>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))"
+ have "isnorm (PX Q1 d (Pc 0))"
proof (cases Q1)
case (PX p1 y p2)
- with 9 sm1 sm2 show ?thesis by (cases d) (simp, cases p2, 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
+ 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
+ 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) }
+ 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)
+ }
ultimately show ?case by blast
qed simp
text {* mul concerves normalizedness *}
lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
proof (induct P Q rule: mul.induct)
- case (2 c i P2) then show ?case
+ case (2 c i P2)
+ then show ?case
by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
next
- case (3 i P2 c) then show ?case
+ case (3 i P2 c)
+ then show ?case
by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
next
case (4 c P2 i Q2)
then have "isnorm P2" "isnorm Q2"
by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
- with 4 show ?case
+ 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)
@@ -293,89 +344,129 @@
next
case (6 x P2 y Q2)
have "x < y \<or> x = y \<or> x > y" by arith
- moreover
- { assume "x < y" then have "\<exists>d. y = d + x" by arith
+ moreover {
+ assume "x < y"
+ then have "\<exists>d. y = d + x" by arith
then obtain d where y: "y = d + x" ..
moreover
note 6
moreover
- from 6 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 6 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
- 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"
+ from 6 `x < y` y have "isnorm (Pinj d Q2)"
+ by (cases d) (simp, cases Q2, auto)
+ ultimately have ?case by (simp add: mkPinj_cn)
+ }
+ moreover {
+ assume "x = y"
moreover
- from 6 have "isnorm P2" "isnorm Q2" 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
- from 6 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 6
- ultimately have ?case by (simp add: mkPinj_cn) }
- moreover
- { assume "x > y" then have "\<exists>d. x = d + y" by arith
+ ultimately have ?case by (simp add: mkPinj_cn)
+ }
+ moreover {
+ assume "x > y"
+ then have "\<exists>d. x = d + y" by arith
then obtain d where x: "x = d + y" ..
moreover
note 6
moreover
- from 6 have "y > 0" by (cases y) (auto simp add: norm_Pinj_0_False)
+ from 6 have "y > 0"
+ by (cases y) (auto simp add: norm_Pinj_0_False)
moreover
- from 6 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
- 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) }
+ 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)
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 7 have ?case by (auto simp add: norm_Pinj_0_False) }
- moreover
- { 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" then have "\<exists>d. x = Suc (Suc d)" by arith
+ moreover {
+ assume "x = 0"
+ with 7 have ?case
+ by (auto simp add: norm_Pinj_0_False)
+ }
+ moreover {
+ 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"
+ then have "\<exists>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 7 X have "isnorm (Pinj (x - 1) 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
+ from 7 have "isnorm (Pinj x P2)"
+ by (cases P2) auto
moreover
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) }
+ 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 (8 Q2 y R x P2)
- then have Y0: "y > 0" by (cases y) auto
+ 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 8 have ?case by (auto simp add: norm_Pinj_0_False) }
- moreover
- { 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" then have "\<exists>d. x = Suc (Suc d)" by arith
+ moreover {
+ assume "x = 0"
+ with 8 have ?case
+ by (auto simp add: norm_Pinj_0_False)
+ }
+ moreover {
+ 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"
+ then have "\<exists>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 8 X 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 8 X have "isnorm (Pinj x P2)" by (cases P2) auto
+ from 8 X have "isnorm (Pinj x P2)"
+ by (cases P2) auto
moreover
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 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)
@@ -383,16 +474,18 @@
from 9 have Y0: "y > 0" by (cases y) auto
note 9
moreover
- from 9 have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
- moreover
- from 9 have "isnorm Q1" "isnorm Q2" by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2])
+ from 9 have "isnorm P1" "isnorm P2"
+ by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
+ moreover
+ from 9 have "isnorm Q1" "isnorm Q2"
+ by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2])
ultimately have "isnorm (P1 \<otimes> Q1)" "isnorm (P2 \<otimes> Q2)"
- "isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)"
+ "isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)"
by (auto simp add: mkPinj_cn)
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))"
+ "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)
then show ?case by (simp add: add_cn)
qed simp
@@ -401,8 +494,10 @@
lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"
proof (induct P)
case (Pinj i P2)
- then have "isnorm P2" by (simp add: norm_Pinj[of i P2])
- with Pinj 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) note PX1 = this
from PX have "isnorm P2" "isnorm P1"
@@ -410,10 +505,12 @@
with PX show ?case
proof (cases P1)
case (PX p1 y p2)
- with PX1 show ?thesis by (cases x) (auto, cases p2, auto)
+ with PX1 show ?thesis
+ by (cases x) (auto, cases p2, auto)
next
case Pinj
- with PX1 show ?thesis by (cases x) auto
+ with PX1 show ?thesis
+ by (cases x) auto
qed (cases x, auto)
qed simp
@@ -430,21 +527,22 @@
case (Pinj i Q)
then show ?case
by (cases Q) (auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
-next
+next
case (PX P1 x P2)
then have "x + x \<noteq> 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)
+ then show ?case
+ by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
qed
text {* pow conserves normalizedness *}
lemma pow_cn: "isnorm P \<Longrightarrow> isnorm (pow n P)"
proof (induct n arbitrary: P rule: less_induct)
case (less k)
- show ?case
+ show ?case
proof (cases "k = 0")
case True
then show ?thesis by simp
--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Thu Feb 27 21:27:58 2014 +0100
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Thu Feb 27 21:31:58 2014 +0100
@@ -22,31 +22,40 @@
fun polexT t = Type (@{type_name Commutative_Ring.polex}, [t]);
(* pol *)
-fun pol_Pc t = Const (@{const_name Commutative_Ring.pol.Pc}, t --> polT t);
-fun pol_Pinj t = Const (@{const_name Commutative_Ring.pol.Pinj}, HOLogic.natT --> polT t --> polT t);
-fun pol_PX t = Const (@{const_name Commutative_Ring.pol.PX}, polT t --> HOLogic.natT --> polT t --> polT t);
+fun pol_Pc t =
+ Const (@{const_name Commutative_Ring.pol.Pc}, t --> polT t);
+fun pol_Pinj t =
+ Const (@{const_name Commutative_Ring.pol.Pinj}, HOLogic.natT --> polT t --> polT t);
+fun pol_PX t =
+ Const (@{const_name Commutative_Ring.pol.PX}, polT t --> HOLogic.natT --> polT t --> polT t);
(* polex *)
-fun polex_add t = Const (@{const_name Commutative_Ring.polex.Add}, polexT t --> polexT t --> polexT t);
-fun polex_sub t = Const (@{const_name Commutative_Ring.polex.Sub}, polexT t --> polexT t --> polexT t);
-fun polex_mul t = Const (@{const_name Commutative_Ring.polex.Mul}, polexT t --> polexT t --> polexT t);
-fun polex_neg t = Const (@{const_name Commutative_Ring.polex.Neg}, polexT t --> polexT t);
-fun polex_pol t = Const (@{const_name Commutative_Ring.polex.Pol}, polT t --> polexT t);
-fun polex_pow t = Const (@{const_name Commutative_Ring.polex.Pow}, polexT t --> HOLogic.natT --> polexT t);
+fun polex_add t =
+ Const (@{const_name Commutative_Ring.polex.Add}, polexT t --> polexT t --> polexT t);
+fun polex_sub t =
+ Const (@{const_name Commutative_Ring.polex.Sub}, polexT t --> polexT t --> polexT t);
+fun polex_mul t =
+ Const (@{const_name Commutative_Ring.polex.Mul}, polexT t --> polexT t --> polexT t);
+fun polex_neg t =
+ Const (@{const_name Commutative_Ring.polex.Neg}, polexT t --> polexT t);
+fun polex_pol t =
+ Const (@{const_name Commutative_Ring.polex.Pol}, polT t --> polexT t);
+fun polex_pow t =
+ Const (@{const_name Commutative_Ring.polex.Pow}, polexT t --> HOLogic.natT --> polexT t);
(* reification of polynoms : primitive cring expressions *)
fun reif_pol T vs (t as Free _) =
let
val one = @{term "1::nat"};
val i = find_index (fn t' => t' = t) vs
- in if i = 0
- then pol_PX T $ (pol_Pc T $ cring_one T)
- $ one $ (pol_Pc T $ cring_zero T)
- else pol_Pinj T $ HOLogic.mk_nat i
- $ (pol_PX T $ (pol_Pc T $ cring_one T)
- $ one $ (pol_Pc T $ cring_zero T))
+ in
+ if i = 0 then
+ pol_PX T $ (pol_Pc T $ cring_one T) $ one $ (pol_Pc T $ cring_zero T)
+ else
+ pol_Pinj T $ HOLogic.mk_nat i $
+ (pol_PX T $ (pol_Pc T $ cring_one T) $ one $ (pol_Pc T $ cring_zero T))
end
- | reif_pol T vs t = pol_Pc T $ t;
+ | reif_pol T _ t = pol_Pc T $ t;
(* reification of polynom expressions *)
fun reif_polex T vs (Const (@{const_name Groups.plus}, _) $ a $ b) =
@@ -62,34 +71,33 @@
| reif_polex T vs t = polex_pol T $ reif_pol T vs t;
(* reification of the equation *)
-val cr_sort = @{sort "comm_ring_1"};
+val cr_sort = @{sort comm_ring_1};
-fun reif_eq thy (eq as Const(@{const_name HOL.eq}, Type("fun", [T, _])) $ lhs $ rhs) =
- if Sign.of_sort thy (T, cr_sort) then
+fun reif_eq ctxt (eq as Const (@{const_name HOL.eq}, Type (@{type_name fun}, [T, _])) $ lhs $ rhs) =
+ if Sign.of_sort (Proof_Context.theory_of ctxt) (T, cr_sort) then
let
+ val thy = Proof_Context.theory_of ctxt;
val fs = Misc_Legacy.term_frees eq;
val cvs = cterm_of thy (HOLogic.mk_list T fs);
val clhs = cterm_of thy (reif_polex T fs lhs);
val crhs = cterm_of thy (reif_polex T fs rhs);
val ca = ctyp_of thy T;
in (ca, cvs, clhs, crhs) end
- else error ("reif_eq: not an equation over " ^ Syntax.string_of_sort_global thy cr_sort)
+ else error ("reif_eq: not an equation over " ^ Syntax.string_of_sort ctxt cr_sort)
| reif_eq _ _ = error "reif_eq: not an equation";
(* The cring tactic *)
(* Attention: You have to make sure that no t^0 is in the goal!! *)
(* Use simply rewriting t^0 = 1 *)
val cring_simps =
- [@{thm mkPX_def}, @{thm mkPinj_def}, @{thm sub_def}, @{thm power_add},
- @{thm even_def}, @{thm pow_if}, sym OF [@{thm power_add}]];
+ @{thms mkPX_def mkPinj_def sub_def power_add even_def pow_if power_add [symmetric]};
fun tac ctxt = SUBGOAL (fn (g, i) =>
let
- val thy = Proof_Context.theory_of ctxt;
val cring_ctxt = ctxt addsimps cring_simps; (*FIXME really the full simpset!?*)
- val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g)
+ val (ca, cvs, clhs, crhs) = reif_eq ctxt (HOLogic.dest_Trueprop g);
val norm_eq_th =
- simplify cring_ctxt (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq})
+ simplify cring_ctxt (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq});
in
cut_tac norm_eq_th i
THEN (simp_tac cring_ctxt i)