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.299 -by (simp add: sub_def add_cn neg_cn)
   1.300 +lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
   1.301 +  by (simp add: sub_def add_cn neg_cn)
   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.319      by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
   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