1.1 --- a/src/HOL/ex/Commutative_Ring_Complete.thy Fri Oct 30 01:32:06 2009 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,391 +0,0 @@
1.4 -(* Author: Bernhard Haeupler
1.5 -
1.6 -This theory is about of the relative completeness of method comm-ring
1.7 -method. As long as the reified atomic polynomials of type 'a pol are
1.8 -in normal form, the cring method is complete.
1.9 -*)
1.10 -
1.11 -header {* Proof of the relative completeness of method comm-ring *}
1.12 -
1.13 -theory Commutative_Ring_Complete
1.14 -imports Commutative_Ring
1.15 -begin
1.16 -
1.17 -text {* Formalization of normal form *}
1.18 -fun
1.19 - isnorm :: "('a::{comm_ring}) pol \<Rightarrow> bool"
1.20 -where
1.21 - "isnorm (Pc c) \<longleftrightarrow> True"
1.22 - | "isnorm (Pinj i (Pc c)) \<longleftrightarrow> False"
1.23 - | "isnorm (Pinj i (Pinj j Q)) \<longleftrightarrow> False"
1.24 - | "isnorm (Pinj 0 P) \<longleftrightarrow> False"
1.25 - | "isnorm (Pinj i (PX Q1 j Q2)) \<longleftrightarrow> isnorm (PX Q1 j Q2)"
1.26 - | "isnorm (PX P 0 Q) \<longleftrightarrow> False"
1.27 - | "isnorm (PX (Pc c) i Q) \<longleftrightarrow> c \<noteq> 0 \<and> isnorm Q"
1.28 - | "isnorm (PX (PX P1 j (Pc c)) i Q) \<longleftrightarrow> c \<noteq> 0 \<and> isnorm (PX P1 j (Pc c)) \<and> isnorm Q"
1.29 - | "isnorm (PX P i Q) \<longleftrightarrow> isnorm P \<and> isnorm Q"
1.30 -
1.31 -(* Some helpful lemmas *)
1.32 -lemma norm_Pinj_0_False:"isnorm (Pinj 0 P) = False"
1.33 -by(cases P, auto)
1.34 -
1.35 -lemma norm_PX_0_False:"isnorm (PX (Pc 0) i Q) = False"
1.36 -by(cases i, auto)
1.37 -
1.38 -lemma norm_Pinj:"isnorm (Pinj i Q) \<Longrightarrow> isnorm Q"
1.39 -by(cases i,simp add: norm_Pinj_0_False norm_PX_0_False,cases Q) auto
1.40 -
1.41 -lemma norm_PX2:"isnorm (PX P i Q) \<Longrightarrow> isnorm Q"
1.42 -by(cases i, auto, cases P, auto, case_tac pol2, auto)
1.43 -
1.44 -lemma norm_PX1:"isnorm (PX P i Q) \<Longrightarrow> isnorm P"
1.45 -by(cases i, auto, cases P, auto, case_tac pol2, auto)
1.46 -
1.47 -lemma mkPinj_cn:"\<lbrakk>y~=0; isnorm Q\<rbrakk> \<Longrightarrow> isnorm (mkPinj y Q)"
1.48 -apply(auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split)
1.49 -apply(case_tac nat, auto simp add: norm_Pinj_0_False)
1.50 -by(case_tac pol, auto) (case_tac y, auto)
1.51 -
1.52 -lemma norm_PXtrans:
1.53 - assumes A:"isnorm (PX P x Q)" and "isnorm Q2"
1.54 - shows "isnorm (PX P x Q2)"
1.55 -proof(cases P)
1.56 - case (PX p1 y p2) from prems show ?thesis by(cases x, auto, cases p2, auto)
1.57 -next
1.58 - case Pc from prems show ?thesis by(cases x, auto)
1.59 -next
1.60 - case Pinj from prems show ?thesis by(cases x, auto)
1.61 -qed
1.62 -
1.63 -lemma norm_PXtrans2: assumes A:"isnorm (PX P x Q)" and "isnorm Q2" shows "isnorm (PX P (Suc (n+x)) Q2)"
1.64 -proof(cases P)
1.65 - case (PX p1 y p2)
1.66 - from prems show ?thesis by(cases x, auto, cases p2, auto)
1.67 -next
1.68 - case Pc
1.69 - from prems show ?thesis by(cases x, auto)
1.70 -next
1.71 - case Pinj
1.72 - from prems show ?thesis by(cases x, auto)
1.73 -qed
1.74 -
1.75 -text {* mkPX conserves normalizedness (@{text "_cn"}) *}
1.76 -lemma mkPX_cn:
1.77 - assumes "x \<noteq> 0" and "isnorm P" and "isnorm Q"
1.78 - shows "isnorm (mkPX P x Q)"
1.79 -proof(cases P)
1.80 - case (Pc c)
1.81 - from prems show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
1.82 -next
1.83 - case (Pinj i Q)
1.84 - from prems show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
1.85 -next
1.86 - case (PX P1 y P2)
1.87 - from prems have Y0:"y>0" by(cases y, auto)
1.88 - from prems have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2])
1.89 - with prems Y0 show ?thesis by (cases x, auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
1.90 -qed
1.91 -
1.92 -text {* add conserves normalizedness *}
1.93 -lemma add_cn:"isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
1.94 -proof(induct P Q rule: add.induct)
1.95 - case (2 c i P2) thus ?case by (cases P2, simp_all, cases i, simp_all)
1.96 -next
1.97 - case (3 i P2 c) thus ?case by (cases P2, simp_all, cases i, simp_all)
1.98 -next
1.99 - case (4 c P2 i Q2)
1.100 - from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
1.101 - with prems show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto)
1.102 -next
1.103 - case (5 P2 i Q2 c)
1.104 - from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
1.105 - with prems show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto)
1.106 -next
1.107 - case (6 x P2 y Q2)
1.108 - from prems have Y0:"y>0" by (cases y, auto simp add: norm_Pinj_0_False)
1.109 - from prems have X0:"x>0" by (cases x, auto simp add: norm_Pinj_0_False)
1.110 - have "x < y \<or> x = y \<or> x > y" by arith
1.111 - moreover
1.112 - { assume "x<y" hence "EX d. y=d+x" by arith
1.113 - then obtain d where "y=d+x"..
1.114 - moreover
1.115 - note prems X0
1.116 - moreover
1.117 - from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
1.118 - moreover
1.119 - with prems have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto)
1.120 - ultimately have ?case by (simp add: mkPinj_cn)}
1.121 - moreover
1.122 - { assume "x=y"
1.123 - moreover
1.124 - from prems have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
1.125 - moreover
1.126 - note prems Y0
1.127 - moreover
1.128 - ultimately have ?case by (simp add: mkPinj_cn) }
1.129 - moreover
1.130 - { assume "x>y" hence "EX d. x=d+y" by arith
1.131 - then obtain d where "x=d+y"..
1.132 - moreover
1.133 - note prems Y0
1.134 - moreover
1.135 - from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
1.136 - moreover
1.137 - with prems have "isnorm (Pinj d P2)" by (cases d, simp, cases P2, auto)
1.138 - ultimately have ?case by (simp add: mkPinj_cn)}
1.139 - ultimately show ?case by blast
1.140 -next
1.141 - case (7 x P2 Q2 y R)
1.142 - have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith
1.143 - moreover
1.144 - { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
1.145 - moreover
1.146 - { assume "x=1"
1.147 - from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
1.148 - with prems have "isnorm (R \<oplus> P2)" by simp
1.149 - with prems have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
1.150 - moreover
1.151 - { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
1.152 - then obtain d where X:"x=Suc (Suc d)" ..
1.153 - from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
1.154 - with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
1.155 - with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp fact
1.156 - with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
1.157 - ultimately show ?case by blast
1.158 -next
1.159 - case (8 Q2 y R x P2)
1.160 - have "x = 0 \<or> x = 1 \<or> x > 1" by arith
1.161 - moreover
1.162 - { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
1.163 - moreover
1.164 - { assume "x=1"
1.165 - from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
1.166 - with prems have "isnorm (R \<oplus> P2)" by simp
1.167 - with prems have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
1.168 - moreover
1.169 - { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
1.170 - then obtain d where X:"x=Suc (Suc d)" ..
1.171 - from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
1.172 - with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
1.173 - with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp fact
1.174 - with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
1.175 - ultimately show ?case by blast
1.176 -next
1.177 - case (9 P1 x P2 Q1 y Q2)
1.178 - from prems have Y0:"y>0" by(cases y, auto)
1.179 - from prems have X0:"x>0" by(cases x, auto)
1.180 - from prems have NP1:"isnorm P1" and NP2:"isnorm P2" by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])
1.181 - from prems have NQ1:"isnorm Q1" and NQ2:"isnorm Q2" by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])
1.182 - have "y < x \<or> x = y \<or> x < y" by arith
1.183 - moreover
1.184 - {assume sm1:"y < x" hence "EX d. x=d+y" by arith
1.185 - then obtain d where sm2:"x=d+y"..
1.186 - note prems NQ1 NP1 NP2 NQ2 sm1 sm2
1.187 - moreover
1.188 - have "isnorm (PX P1 d (Pc 0))"
1.189 - proof(cases P1)
1.190 - case (PX p1 y p2)
1.191 - with prems show ?thesis by(cases d, simp,cases p2, auto)
1.192 - next case Pc from prems show ?thesis by(cases d, auto)
1.193 - next case Pinj from prems show ?thesis by(cases d, auto)
1.194 - qed
1.195 - ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)" by auto
1.196 - with Y0 sm1 sm2 have ?case by (simp add: mkPX_cn)}
1.197 - moreover
1.198 - {assume "x=y"
1.199 - from prems NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)" by auto
1.200 - with Y0 prems have ?case by (simp add: mkPX_cn) }
1.201 - moreover
1.202 - {assume sm1:"x<y" hence "EX d. y=d+x" by arith
1.203 - then obtain d where sm2:"y=d+x"..
1.204 - note prems NQ1 NP1 NP2 NQ2 sm1 sm2
1.205 - moreover
1.206 - have "isnorm (PX Q1 d (Pc 0))"
1.207 - proof(cases Q1)
1.208 - case (PX p1 y p2)
1.209 - with prems show ?thesis by(cases d, simp,cases p2, auto)
1.210 - next case Pc from prems show ?thesis by(cases d, auto)
1.211 - next case Pinj from prems show ?thesis by(cases d, auto)
1.212 - qed
1.213 - ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)" by auto
1.214 - with X0 sm1 sm2 have ?case by (simp add: mkPX_cn)}
1.215 - ultimately show ?case by blast
1.216 -qed simp
1.217 -
1.218 -text {* mul concerves normalizedness *}
1.219 -lemma mul_cn :"isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
1.220 -proof(induct P Q rule: mul.induct)
1.221 - case (2 c i P2) thus ?case
1.222 - by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn)
1.223 -next
1.224 - case (3 i P2 c) thus ?case
1.225 - by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn)
1.226 -next
1.227 - case (4 c P2 i Q2)
1.228 - from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
1.229 - with prems show ?case
1.230 - by - (case_tac "c=0",simp_all,case_tac "i=0",simp_all add: mkPX_cn)
1.231 -next
1.232 - case (5 P2 i Q2 c)
1.233 - from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
1.234 - with prems show ?case
1.235 - by - (case_tac "c=0",simp_all,case_tac "i=0",simp_all add: mkPX_cn)
1.236 -next
1.237 - case (6 x P2 y Q2)
1.238 - have "x < y \<or> x = y \<or> x > y" by arith
1.239 - moreover
1.240 - { assume "x<y" hence "EX d. y=d+x" by arith
1.241 - then obtain d where "y=d+x"..
1.242 - moreover
1.243 - note prems
1.244 - moreover
1.245 - from prems have "x>0" by (cases x, auto simp add: norm_Pinj_0_False)
1.246 - moreover
1.247 - from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
1.248 - moreover
1.249 - with prems have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto)
1.250 - ultimately have ?case by (simp add: mkPinj_cn)}
1.251 - moreover
1.252 - { assume "x=y"
1.253 - moreover
1.254 - from prems have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
1.255 - moreover
1.256 - with prems have "y>0" by (cases y, auto simp add: norm_Pinj_0_False)
1.257 - moreover
1.258 - note prems
1.259 - moreover
1.260 - ultimately have ?case by (simp add: mkPinj_cn) }
1.261 - moreover
1.262 - { assume "x>y" hence "EX d. x=d+y" by arith
1.263 - then obtain d where "x=d+y"..
1.264 - moreover
1.265 - note prems
1.266 - moreover
1.267 - from prems have "y>0" by (cases y, auto simp add: norm_Pinj_0_False)
1.268 - moreover
1.269 - from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
1.270 - moreover
1.271 - with prems have "isnorm (Pinj d P2)" by (cases d, simp, cases P2, auto)
1.272 - ultimately have ?case by (simp add: mkPinj_cn) }
1.273 - ultimately show ?case by blast
1.274 -next
1.275 - case (7 x P2 Q2 y R)
1.276 - from prems have Y0:"y>0" by(cases y, auto)
1.277 - have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith
1.278 - moreover
1.279 - { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
1.280 - moreover
1.281 - { assume "x=1"
1.282 - from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
1.283 - with prems have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
1.284 - with Y0 prems have ?case by (simp add: mkPX_cn)}
1.285 - moreover
1.286 - { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
1.287 - then obtain d where X:"x=Suc (Suc d)" ..
1.288 - from prems have NR:"isnorm R" "isnorm Q2" by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
1.289 - moreover
1.290 - from prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
1.291 - moreover
1.292 - from prems have "isnorm (Pinj x P2)" by(cases P2, auto)
1.293 - moreover
1.294 - note prems
1.295 - ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto
1.296 - with Y0 X have ?case by (simp add: mkPX_cn)}
1.297 - ultimately show ?case by blast
1.298 -next
1.299 - case (8 Q2 y R x P2)
1.300 - from prems have Y0:"y>0" by(cases y, auto)
1.301 - have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith
1.302 - moreover
1.303 - { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
1.304 - moreover
1.305 - { assume "x=1"
1.306 - from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
1.307 - with prems have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
1.308 - with Y0 prems have ?case by (simp add: mkPX_cn) }
1.309 - moreover
1.310 - { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
1.311 - then obtain d where X:"x=Suc (Suc d)" ..
1.312 - from prems have NR:"isnorm R" "isnorm Q2" by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
1.313 - moreover
1.314 - from prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
1.315 - moreover
1.316 - from prems have "isnorm (Pinj x P2)" by(cases P2, auto)
1.317 - moreover
1.318 - note prems
1.319 - ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto
1.320 - with Y0 X have ?case by (simp add: mkPX_cn) }
1.321 - ultimately show ?case by blast
1.322 -next
1.323 - case (9 P1 x P2 Q1 y Q2)
1.324 - from prems have X0:"x>0" by(cases x, auto)
1.325 - from prems have Y0:"y>0" by(cases y, auto)
1.326 - note prems
1.327 - moreover
1.328 - from prems have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
1.329 - moreover
1.330 - from prems have "isnorm Q1" "isnorm Q2" by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2])
1.331 - ultimately have "isnorm (P1 \<otimes> Q1)" "isnorm (P2 \<otimes> Q2)"
1.332 - "isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)"
1.333 - by (auto simp add: mkPinj_cn)
1.334 - with prems X0 Y0 have
1.335 - "isnorm (mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2))"
1.336 - "isnorm (mkPX (P1 \<otimes> mkPinj (Suc 0) Q2) x (Pc 0))"
1.337 - "isnorm (mkPX (Q1 \<otimes> mkPinj (Suc 0) P2) y (Pc 0))"
1.338 - by (auto simp add: mkPX_cn)
1.339 - thus ?case by (simp add: add_cn)
1.340 -qed(simp)
1.341 -
1.342 -text {* neg conserves normalizedness *}
1.343 -lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"
1.344 -proof (induct P)
1.345 - case (Pinj i P2)
1.346 - from prems have "isnorm P2" by (simp add: norm_Pinj[of i P2])
1.347 - with prems show ?case by(cases P2, auto, cases i, auto)
1.348 -next
1.349 - case (PX P1 x P2)
1.350 - from prems have "isnorm P2" "isnorm P1" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
1.351 - with prems show ?case
1.352 - proof(cases P1)
1.353 - case (PX p1 y p2)
1.354 - with prems show ?thesis by(cases x, auto, cases p2, auto)
1.355 - next
1.356 - case Pinj
1.357 - with prems show ?thesis by(cases x, auto)
1.358 - qed(cases x, auto)
1.359 -qed(simp)
1.360 -
1.361 -text {* sub conserves normalizedness *}
1.362 -lemma sub_cn:"isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
1.363 -by (simp add: sub_def add_cn neg_cn)
1.364 -
1.365 -text {* sqr conserves normalizizedness *}
1.366 -lemma sqr_cn:"isnorm P \<Longrightarrow> isnorm (sqr P)"
1.367 -proof(induct P)
1.368 - case (Pinj i Q)
1.369 - from prems show ?case by(cases Q, auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
1.370 -next
1.371 - case (PX P1 x P2)
1.372 - 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])
1.373 - with prems have
1.374 - "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))"
1.375 - and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
1.376 - by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
1.377 - thus ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
1.378 -qed simp
1.379 -
1.380 -text {* pow conserves normalizedness *}
1.381 -lemma pow_cn:"isnorm P \<Longrightarrow> isnorm (pow n P)"
1.382 -proof (induct n arbitrary: P rule: nat_less_induct)
1.383 - case (1 k)
1.384 - show ?case
1.385 - proof (cases "k=0")
1.386 - case False
1.387 - then have K2:"k div 2 < k" by (cases k, auto)
1.388 - from prems have "isnorm (sqr P)" by (simp add: sqr_cn)
1.389 - with prems K2 show ?thesis
1.390 - by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
1.391 - qed simp
1.392 -qed
1.393 -
1.394 -end