src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
 changeset 44779 98d597c4193d parent 41807 ab5d2d81f9fb child 53374 a14d2a854c02
```     1.1 --- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Wed Sep 07 11:36:39 2011 +0200
1.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Wed Sep 07 16:37:50 2011 +0200
1.3 @@ -12,8 +12,7 @@
1.4  begin
1.5
1.6  text {* Formalization of normal form *}
1.7 -fun
1.8 -  isnorm :: "('a::{comm_ring}) pol \<Rightarrow> bool"
1.9 +fun isnorm :: "'a::comm_ring pol \<Rightarrow> bool"
1.10  where
1.11      "isnorm (Pc c) \<longleftrightarrow> True"
1.12    | "isnorm (Pinj i (Pc c)) \<longleftrightarrow> False"
1.13 @@ -26,35 +25,40 @@
1.14    | "isnorm (PX P i Q) \<longleftrightarrow> isnorm P \<and> isnorm Q"
1.15
1.16  (* Some helpful lemmas *)
1.17 -lemma norm_Pinj_0_False:"isnorm (Pinj 0 P) = False"
1.18 -by(cases P, auto)
1.19 +lemma norm_Pinj_0_False: "isnorm (Pinj 0 P) = False"
1.20 +  by (cases P) auto
1.21
1.22 -lemma norm_PX_0_False:"isnorm (PX (Pc 0) i Q) = False"
1.23 -by(cases i, auto)
1.24 +lemma norm_PX_0_False: "isnorm (PX (Pc 0) i Q) = False"
1.25 +  by (cases i) auto
1.26
1.27 -lemma norm_Pinj:"isnorm (Pinj i Q) \<Longrightarrow> isnorm Q"
1.28 -by(cases i,simp add: norm_Pinj_0_False norm_PX_0_False,cases Q) auto
1.29 +lemma norm_Pinj: "isnorm (Pinj i Q) \<Longrightarrow> isnorm Q"
1.30 +  by (cases i) (simp add: norm_Pinj_0_False norm_PX_0_False, cases Q, auto)
1.31
1.32 -lemma norm_PX2:"isnorm (PX P i Q) \<Longrightarrow> isnorm Q"
1.33 -by(cases i, auto, cases P, auto, case_tac pol2, auto)
1.34 +lemma norm_PX2: "isnorm (PX P i Q) \<Longrightarrow> isnorm Q"
1.35 +  by (cases i) (auto, cases P, auto, case_tac pol2, auto)
1.36 +
1.37 +lemma norm_PX1: "isnorm (PX P i Q) \<Longrightarrow> isnorm P"
1.38 +  by (cases i) (auto, cases P, auto, case_tac pol2, auto)
1.39
1.40 -lemma norm_PX1:"isnorm (PX P i Q) \<Longrightarrow> isnorm P"
1.41 -by(cases i, auto, cases P, auto, case_tac pol2, auto)
1.42 -
1.43 -lemma mkPinj_cn:"\<lbrakk>y~=0; isnorm Q\<rbrakk> \<Longrightarrow> isnorm (mkPinj y Q)"
1.44 -apply(auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split)
1.45 -apply(case_tac nat, auto simp add: norm_Pinj_0_False)
1.46 -by(case_tac pol, auto) (case_tac y, auto)
1.47 +lemma mkPinj_cn: "y ~= 0 \<Longrightarrow> isnorm Q \<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 +  apply (case_tac pol, auto)
1.51 +  apply (case_tac y, auto)
1.52 +  done
1.53
1.54  lemma norm_PXtrans:
1.55 -  assumes A:"isnorm (PX P x Q)" and "isnorm Q2"
1.56 +  assumes A: "isnorm (PX P x Q)" and "isnorm Q2"
1.57    shows "isnorm (PX P x Q2)"
1.58 -proof(cases P)
1.59 -  case (PX p1 y p2) with assms show ?thesis by(cases x, auto, cases p2, auto)
1.60 +proof (cases P)
1.61 +  case (PX p1 y p2)
1.62 +  with assms show ?thesis by (cases x) (auto, cases p2, auto)
1.63  next
1.64 -  case Pc with assms show ?thesis by (cases x) auto
1.65 +  case Pc
1.66 +  with assms show ?thesis by (cases x) auto
1.67  next
1.68 -  case Pinj with assms show ?thesis by (cases x) auto
1.69 +  case Pinj
1.70 +  with assms show ?thesis by (cases x) auto
1.71  qed
1.72
1.73  lemma norm_PXtrans2:
1.74 @@ -62,7 +66,7 @@
1.75    shows "isnorm (PX P (Suc (n+x)) Q2)"
1.76  proof (cases P)
1.77    case (PX p1 y p2)
1.78 -  with assms show ?thesis by (cases x, auto, cases p2, auto)
1.79 +  with assms show ?thesis by (cases x) (auto, cases p2, auto)
1.80  next
1.81    case Pc
1.82    with assms show ?thesis by (cases x) auto
1.83 @@ -83,27 +87,33 @@
1.84    with assms show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
1.85  next
1.86    case (PX P1 y P2)
1.87 -  with assms have Y0: "y>0" by (cases y) auto
1.88 +  with assms have Y0: "y > 0" by (cases y) auto
1.89    from assms PX have "isnorm P1" "isnorm P2"
1.90      by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2])
1.91    from assms PX Y0 show ?thesis
1.92 -    by (cases x, auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
1.93 +    by (cases x) (auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
1.94  qed
1.95
1.96  text {* add conserves normalizedness *}
1.97 -lemma add_cn:"isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
1.98 -proof(induct P Q rule: add.induct)
1.99 -  case (2 c i P2) thus ?case by (cases P2, simp_all, cases i, simp_all)
1.100 +lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
1.101 +proof (induct P Q rule: add.induct)
1.102 +  case (2 c i P2)
1.103 +  thus ?case by (cases P2) (simp_all, cases i, simp_all)
1.104  next
1.105 -  case (3 i P2 c) thus ?case by (cases P2, simp_all, cases i, simp_all)
1.106 +  case (3 i P2 c)
1.107 +  thus ?case by (cases P2) (simp_all, cases i, simp_all)
1.108  next
1.109    case (4 c P2 i Q2)
1.110 -  then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
1.111 -  with 4 show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto)
1.112 +  then have "isnorm P2" "isnorm Q2"
1.113 +    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
1.114 +  with 4 show ?case
1.115 +    by (cases i) (simp, cases P2, auto, case_tac pol2, auto)
1.116  next
1.117    case (5 P2 i Q2 c)
1.118 -  then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
1.119 -  with 5 show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto)
1.120 +  then have "isnorm P2" "isnorm Q2"
1.121 +    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
1.122 +  with 5 show ?case
1.123 +    by (cases i) (simp, cases P2, auto, case_tac pol2, auto)
1.124  next
1.125    case (6 x P2 y Q2)
1.126    then have Y0: "y>0" by (cases y) (auto simp add: norm_Pinj_0_False)
1.127 @@ -115,14 +125,17 @@
1.128      moreover
1.129      note 6 X0
1.130      moreover
1.131 -    from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
1.132 +    from 6 have "isnorm P2" "isnorm Q2"
1.133 +      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
1.134      moreover
1.135 -    from 6 `x < y` y have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto)
1.136 +    from 6 `x < y` y have "isnorm (Pinj d Q2)"
1.137 +      by (cases d, simp, cases Q2, auto)
1.138      ultimately have ?case by (simp add: mkPinj_cn) }
1.139    moreover
1.140    { assume "x=y"
1.141      moreover
1.142 -    from 6 have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
1.143 +    from 6 have "isnorm P2" "isnorm Q2"
1.144 +      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
1.145      moreover
1.146      note 6 Y0
1.147      moreover
1.148 @@ -133,30 +146,35 @@
1.149      moreover
1.150      note 6 Y0
1.151      moreover
1.152 -    from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
1.153 +    from 6 have "isnorm P2" "isnorm Q2"
1.154 +      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
1.155      moreover
1.156 -    from 6 `x > y` x have "isnorm (Pinj d P2)" by (cases d, simp, cases P2, auto)
1.157 -    ultimately have ?case by (simp add: mkPinj_cn)}
1.158 +    from 6 `x > y` x have "isnorm (Pinj d P2)"
1.159 +      by (cases d) (simp, cases P2, auto)
1.160 +    ultimately have ?case by (simp add: mkPinj_cn) }
1.161    ultimately show ?case by blast
1.162  next
1.163    case (7 x P2 Q2 y R)
1.164 -  have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith
1.165 +  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
1.166    moreover
1.167    { assume "x = 0"
1.168      with 7 have ?case by (auto simp add: norm_Pinj_0_False) }
1.169    moreover
1.170    { assume "x = 1"
1.171 -    from 7 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
1.172 +    from 7 have "isnorm R" "isnorm P2"
1.173 +      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
1.174      with 7 `x = 1` have "isnorm (R \<oplus> P2)" by simp
1.175 -    with 7 `x = 1` have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
1.176 +    with 7 `x = 1` have ?case
1.177 +      by (simp add: norm_PXtrans[of Q2 y _]) }
1.178    moreover
1.179    { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
1.180 -    then obtain d where X:"x=Suc (Suc d)" ..
1.181 +    then obtain d where X: "x=Suc (Suc d)" ..
1.182      with 7 have NR: "isnorm R" "isnorm P2"
1.183        by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
1.184      with 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
1.185      with 7 X NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
1.186 -    with `isnorm (PX Q2 y R)` X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
1.187 +    with `isnorm (PX Q2 y R)` X have ?case
1.188 +      by (simp add: norm_PXtrans[of Q2 y _]) }
1.189    ultimately show ?case by blast
1.190  next
1.191    case (8 Q2 y R x P2)
1.192 @@ -183,7 +201,7 @@
1.193    with 9 have X0: "x>0" by (cases x) auto
1.194    with 9 have NP1: "isnorm P1" and NP2: "isnorm P2"
1.195      by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])
1.196 -  with 9 have NQ1:"isnorm Q1" and NQ2: "isnorm Q2"
1.197 +  with 9 have NQ1: "isnorm Q1" and NQ2: "isnorm Q2"
1.198      by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])
1.199    have "y < x \<or> x = y \<or> x < y" by arith
1.200    moreover
1.201 @@ -194,7 +212,7 @@
1.202      have "isnorm (PX P1 d (Pc 0))"
1.203      proof (cases P1)
1.204        case (PX p1 y p2)
1.205 -      with 9 sm1 sm2 show ?thesis by - (cases d, simp, cases p2, auto)
1.206 +      with 9 sm1 sm2 show ?thesis by (cases d) (simp, cases p2, auto)
1.207      next
1.208        case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto
1.209      next
1.210 @@ -214,35 +232,37 @@
1.211      have "isnorm (PX Q1 d (Pc 0))"
1.212      proof (cases Q1)
1.213        case (PX p1 y p2)
1.214 -      with 9 sm1 sm2 show ?thesis by - (cases d, simp, cases p2, auto)
1.215 +      with 9 sm1 sm2 show ?thesis by (cases d) (simp, cases p2, auto)
1.216      next
1.217        case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto
1.218      next
1.219        case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto
1.220      qed
1.221      ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)" by auto
1.222 -    with X0 sm1 sm2 have ?case by (simp add: mkPX_cn)}
1.223 +    with X0 sm1 sm2 have ?case by (simp add: mkPX_cn) }
1.224    ultimately show ?case by blast
1.225  qed simp
1.226
1.227  text {* mul concerves normalizedness *}
1.228 -lemma mul_cn :"isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
1.229 -proof(induct P Q rule: mul.induct)
1.230 +lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
1.231 +proof (induct P Q rule: mul.induct)
1.232    case (2 c i P2) thus ?case
1.233 -    by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn)
1.234 +    by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
1.235  next
1.236    case (3 i P2 c) thus ?case
1.237 -    by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn)
1.238 +    by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
1.239  next
1.240    case (4 c P2 i Q2)
1.241 -  then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
1.242 +  then have "isnorm P2" "isnorm Q2"
1.243 +    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
1.244    with 4 show ?case
1.245 -    by - (cases "c = 0", simp_all, cases "i = 0", simp_all add: mkPX_cn)
1.246 +    by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
1.247  next
1.248    case (5 P2 i Q2 c)
1.249 -  then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
1.250 +  then have "isnorm P2" "isnorm Q2"
1.251 +    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
1.252    with 5 show ?case
1.253 -    by - (cases "c = 0", simp_all, cases "i = 0", simp_all add: mkPX_cn)
1.254 +    by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
1.255  next
1.256    case (6 x P2 y Q2)
1.257    have "x < y \<or> x = y \<or> x > y" by arith
1.258 @@ -256,7 +276,7 @@
1.259      moreover
1.260      from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
1.261      moreover
1.262 -    from 6 `x < y` y have "isnorm (Pinj d Q2)" by - (cases d, simp, cases Q2, auto)
1.263 +    from 6 `x < y` y have "isnorm (Pinj d Q2)" by (cases d) (simp, cases Q2, auto)
1.264      ultimately have ?case by (simp add: mkPinj_cn) }
1.265    moreover
1.266    { assume "x = y"
1.267 @@ -278,7 +298,7 @@
1.268      moreover
1.269      from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
1.270      moreover
1.271 -    from 6 `x > y` x have "isnorm (Pinj d P2)" by - (cases d, simp, cases P2, auto)
1.272 +    from 6 `x > y` x have "isnorm (Pinj d P2)" by (cases d) (simp, cases P2, auto)
1.273      ultimately have ?case by (simp add: mkPinj_cn) }
1.274    ultimately show ?case by blast
1.275  next
1.276 @@ -356,7 +376,7 @@
1.277  proof (induct P)
1.278    case (Pinj i P2)
1.279    then have "isnorm P2" by (simp add: norm_Pinj[of i P2])
1.280 -  with Pinj show ?case by - (cases P2, auto, cases i, auto)
1.281 +  with Pinj show ?case by (cases P2) (auto, cases i, auto)
1.282  next
1.283    case (PX P1 x P2) note PX1 = this
1.284    from PX have "isnorm P2" "isnorm P1"
1.285 @@ -364,7 +384,7 @@
1.286    with PX show ?case
1.287    proof (cases P1)
1.288      case (PX p1 y p2)
1.289 -    with PX1 show ?thesis by - (cases x, auto, cases p2, auto)
1.290 +    with PX1 show ?thesis by (cases x) (auto, cases p2, auto)
1.291    next
1.292      case Pinj
1.293      with PX1 show ?thesis by (cases x) auto
1.294 @@ -372,15 +392,18 @@
1.295  qed simp
1.296
1.297  text {* sub conserves normalizedness *}
1.298 -lemma sub_cn:"isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
1.300 +lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
1.302
1.303  text {* sqr conserves normalizizedness *}
1.304 -lemma sqr_cn:"isnorm P \<Longrightarrow> isnorm (sqr P)"
1.305 +lemma sqr_cn: "isnorm P \<Longrightarrow> isnorm (sqr P)"
1.306  proof (induct P)
1.307 +  case Pc
1.308 +  then show ?case by simp
1.309 +next
1.310    case (Pinj i Q)
1.311    then show ?case
1.312 -    by - (cases Q, auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
1.313 +    by (cases Q) (auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
1.314  next
1.315    case (PX P1 x P2)
1.316    then have "x + x ~= 0" "isnorm P2" "isnorm P1"
1.317 @@ -389,20 +412,23 @@
1.318        and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
1.320    then show ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
1.321 -qed simp
1.322 +qed
1.323
1.324  text {* pow conserves normalizedness *}
1.325 -lemma pow_cn:"isnorm P \<Longrightarrow> isnorm (pow n P)"
1.326 -proof (induct n arbitrary: P rule: nat_less_induct)
1.327 -  case (1 k)
1.328 +lemma pow_cn: "isnorm P \<Longrightarrow> isnorm (pow n P)"
1.329 +proof (induct n arbitrary: P rule: less_induct)
1.330 +  case (less k)
1.331    show ?case
1.332    proof (cases "k = 0")
1.333 +    case True
1.334 +    then show ?thesis by simp
1.335 +  next
1.336      case False
1.337      then have K2: "k div 2 < k" by (cases k) auto
1.338 -    from 1 have "isnorm (sqr P)" by (simp add: sqr_cn)
1.339 -    with 1 False K2 show ?thesis
1.340 -      by - (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
1.341 -  qed simp
1.342 +    from less have "isnorm (sqr P)" by (simp add: sqr_cn)
1.343 +    with less False K2 show ?thesis
1.344 +      by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
1.345 +  qed
1.346  qed
1.347
1.348  end
```