src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
author wenzelm
Wed Sep 07 16:37:50 2011 +0200 (2011-09-07)
changeset 44779 98d597c4193d
parent 41807 ab5d2d81f9fb
child 53374 a14d2a854c02
permissions -rw-r--r--
tuned proofs;
haftmann@31021
     1
(*  Author:     Bernhard Haeupler
chaieb@17378
     2
wenzelm@17388
     3
This theory is about of the relative completeness of method comm-ring
wenzelm@17388
     4
method.  As long as the reified atomic polynomials of type 'a pol are
wenzelm@17388
     5
in normal form, the cring method is complete.
wenzelm@17388
     6
*)
wenzelm@17388
     7
wenzelm@17388
     8
header {* Proof of the relative completeness of method comm-ring *}
chaieb@17378
     9
chaieb@17378
    10
theory Commutative_Ring_Complete
wenzelm@17508
    11
imports Commutative_Ring
chaieb@17378
    12
begin
haftmann@22742
    13
haftmann@22742
    14
text {* Formalization of normal form *}
wenzelm@44779
    15
fun isnorm :: "'a::comm_ring pol \<Rightarrow> bool"
haftmann@22742
    16
where
haftmann@22742
    17
    "isnorm (Pc c) \<longleftrightarrow> True"
haftmann@22742
    18
  | "isnorm (Pinj i (Pc c)) \<longleftrightarrow> False"
haftmann@22742
    19
  | "isnorm (Pinj i (Pinj j Q)) \<longleftrightarrow> False"
haftmann@22742
    20
  | "isnorm (Pinj 0 P) \<longleftrightarrow> False"
haftmann@22742
    21
  | "isnorm (Pinj i (PX Q1 j Q2)) \<longleftrightarrow> isnorm (PX Q1 j Q2)"
haftmann@22742
    22
  | "isnorm (PX P 0 Q) \<longleftrightarrow> False"
haftmann@22742
    23
  | "isnorm (PX (Pc c) i Q) \<longleftrightarrow> c \<noteq> 0 \<and> isnorm Q"
haftmann@22742
    24
  | "isnorm (PX (PX P1 j (Pc c)) i Q) \<longleftrightarrow> c \<noteq> 0 \<and> isnorm (PX P1 j (Pc c)) \<and> isnorm Q"
haftmann@22742
    25
  | "isnorm (PX P i Q) \<longleftrightarrow> isnorm P \<and> isnorm Q"
chaieb@17378
    26
chaieb@17378
    27
(* Some helpful lemmas *)
wenzelm@44779
    28
lemma norm_Pinj_0_False: "isnorm (Pinj 0 P) = False"
wenzelm@44779
    29
  by (cases P) auto
chaieb@17378
    30
wenzelm@44779
    31
lemma norm_PX_0_False: "isnorm (PX (Pc 0) i Q) = False"
wenzelm@44779
    32
  by (cases i) auto
chaieb@17378
    33
wenzelm@44779
    34
lemma norm_Pinj: "isnorm (Pinj i Q) \<Longrightarrow> isnorm Q"
wenzelm@44779
    35
  by (cases i) (simp add: norm_Pinj_0_False norm_PX_0_False, cases Q, auto)
chaieb@17378
    36
wenzelm@44779
    37
lemma norm_PX2: "isnorm (PX P i Q) \<Longrightarrow> isnorm Q"
wenzelm@44779
    38
  by (cases i) (auto, cases P, auto, case_tac pol2, auto)
wenzelm@44779
    39
wenzelm@44779
    40
lemma norm_PX1: "isnorm (PX P i Q) \<Longrightarrow> isnorm P"
wenzelm@44779
    41
  by (cases i) (auto, cases P, auto, case_tac pol2, auto)
chaieb@17378
    42
wenzelm@44779
    43
lemma mkPinj_cn: "y ~= 0 \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (mkPinj y Q)"
wenzelm@44779
    44
  apply (auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split)
wenzelm@44779
    45
  apply (case_tac nat, auto simp add: norm_Pinj_0_False)
wenzelm@44779
    46
  apply (case_tac pol, auto)
wenzelm@44779
    47
  apply (case_tac y, auto)
wenzelm@44779
    48
  done
chaieb@17378
    49
chaieb@17378
    50
lemma norm_PXtrans: 
wenzelm@44779
    51
  assumes A: "isnorm (PX P x Q)" and "isnorm Q2" 
chaieb@17378
    52
  shows "isnorm (PX P x Q2)"
wenzelm@44779
    53
proof (cases P)
wenzelm@44779
    54
  case (PX p1 y p2)
wenzelm@44779
    55
  with assms show ?thesis by (cases x) (auto, cases p2, auto)
chaieb@17378
    56
next
wenzelm@44779
    57
  case Pc
wenzelm@44779
    58
  with assms show ?thesis by (cases x) auto
chaieb@17378
    59
next
wenzelm@44779
    60
  case Pinj
wenzelm@44779
    61
  with assms show ?thesis by (cases x) auto
chaieb@17378
    62
qed
chaieb@17378
    63
 
wenzelm@41807
    64
lemma norm_PXtrans2:
wenzelm@41807
    65
  assumes "isnorm (PX P x Q)" and "isnorm Q2"
wenzelm@41807
    66
  shows "isnorm (PX P (Suc (n+x)) Q2)"
wenzelm@41807
    67
proof (cases P)
chaieb@17378
    68
  case (PX p1 y p2)
wenzelm@44779
    69
  with assms show ?thesis by (cases x) (auto, cases p2, auto)
chaieb@17378
    70
next
chaieb@17378
    71
  case Pc
wenzelm@41807
    72
  with assms show ?thesis by (cases x) auto
chaieb@17378
    73
next
chaieb@17378
    74
  case Pinj
wenzelm@41807
    75
  with assms show ?thesis by (cases x) auto
chaieb@17378
    76
qed
chaieb@17378
    77
wenzelm@23266
    78
text {* mkPX conserves normalizedness (@{text "_cn"}) *}
chaieb@17378
    79
lemma mkPX_cn: 
chaieb@17378
    80
  assumes "x \<noteq> 0" and "isnorm P" and "isnorm Q" 
chaieb@17378
    81
  shows "isnorm (mkPX P x Q)"
chaieb@17378
    82
proof(cases P)
chaieb@17378
    83
  case (Pc c)
wenzelm@41807
    84
  with assms show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
chaieb@17378
    85
next
chaieb@17378
    86
  case (Pinj i Q)
wenzelm@41807
    87
  with assms show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
chaieb@17378
    88
next
chaieb@17378
    89
  case (PX P1 y P2)
wenzelm@44779
    90
  with assms have Y0: "y > 0" by (cases y) auto
wenzelm@41807
    91
  from assms PX have "isnorm P1" "isnorm P2"
wenzelm@41807
    92
    by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2])
wenzelm@41807
    93
  from assms PX Y0 show ?thesis
wenzelm@44779
    94
    by (cases x) (auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
chaieb@17378
    95
qed
chaieb@17378
    96
haftmann@22742
    97
text {* add conserves normalizedness *}
wenzelm@44779
    98
lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
wenzelm@44779
    99
proof (induct P Q rule: add.induct)
wenzelm@44779
   100
  case (2 c i P2)
wenzelm@44779
   101
  thus ?case by (cases P2) (simp_all, cases i, simp_all)
chaieb@17378
   102
next
wenzelm@44779
   103
  case (3 i P2 c)
wenzelm@44779
   104
  thus ?case by (cases P2) (simp_all, cases i, simp_all)
chaieb@17378
   105
next
chaieb@17378
   106
  case (4 c P2 i Q2)
wenzelm@44779
   107
  then have "isnorm P2" "isnorm Q2"
wenzelm@44779
   108
    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
wenzelm@44779
   109
  with 4 show ?case
wenzelm@44779
   110
    by (cases i) (simp, cases P2, auto, case_tac pol2, auto)
chaieb@17378
   111
next
chaieb@17378
   112
  case (5 P2 i Q2 c)
wenzelm@44779
   113
  then have "isnorm P2" "isnorm Q2"
wenzelm@44779
   114
    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
wenzelm@44779
   115
  with 5 show ?case
wenzelm@44779
   116
    by (cases i) (simp, cases P2, auto, case_tac pol2, auto)
chaieb@17378
   117
next
chaieb@17378
   118
  case (6 x P2 y Q2)
wenzelm@41807
   119
  then have Y0: "y>0" by (cases y) (auto simp add: norm_Pinj_0_False)
wenzelm@41807
   120
  with 6 have X0: "x>0" by (cases x) (auto simp add: norm_Pinj_0_False)
chaieb@17378
   121
  have "x < y \<or> x = y \<or> x > y" by arith
chaieb@17378
   122
  moreover
wenzelm@41807
   123
  { assume "x<y" hence "EX d. y =d + x" by arith
wenzelm@41807
   124
    then obtain d where y: "y = d + x" ..
chaieb@17378
   125
    moreover
wenzelm@41807
   126
    note 6 X0
chaieb@17378
   127
    moreover
wenzelm@44779
   128
    from 6 have "isnorm P2" "isnorm Q2"
wenzelm@44779
   129
      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
chaieb@17378
   130
    moreover
wenzelm@44779
   131
    from 6 `x < y` y have "isnorm (Pinj d Q2)"
wenzelm@44779
   132
      by (cases d, simp, cases Q2, auto)
wenzelm@41807
   133
    ultimately have ?case by (simp add: mkPinj_cn) }
chaieb@17378
   134
  moreover
chaieb@17378
   135
  { assume "x=y"
chaieb@17378
   136
    moreover
wenzelm@44779
   137
    from 6 have "isnorm P2" "isnorm Q2"
wenzelm@44779
   138
      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
chaieb@17378
   139
    moreover
wenzelm@41807
   140
    note 6 Y0
chaieb@17378
   141
    moreover
chaieb@17378
   142
    ultimately have ?case by (simp add: mkPinj_cn) }
chaieb@17378
   143
  moreover
wenzelm@41807
   144
  { assume "x>y" hence "EX d. x = d + y" by arith
wenzelm@41807
   145
    then obtain d where x: "x = d + y"..
chaieb@17378
   146
    moreover
wenzelm@41807
   147
    note 6 Y0
chaieb@17378
   148
    moreover
wenzelm@44779
   149
    from 6 have "isnorm P2" "isnorm Q2"
wenzelm@44779
   150
      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
chaieb@17378
   151
    moreover
wenzelm@44779
   152
    from 6 `x > y` x have "isnorm (Pinj d P2)"
wenzelm@44779
   153
      by (cases d) (simp, cases P2, auto)
wenzelm@44779
   154
    ultimately have ?case by (simp add: mkPinj_cn) }
chaieb@17378
   155
  ultimately show ?case by blast
chaieb@17378
   156
next
chaieb@17378
   157
  case (7 x P2 Q2 y R)
wenzelm@44779
   158
  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
chaieb@17378
   159
  moreover
wenzelm@41807
   160
  { assume "x = 0"
wenzelm@41807
   161
    with 7 have ?case by (auto simp add: norm_Pinj_0_False) }
chaieb@17378
   162
  moreover
wenzelm@41807
   163
  { assume "x = 1"
wenzelm@44779
   164
    from 7 have "isnorm R" "isnorm P2"
wenzelm@44779
   165
      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@41807
   166
    with 7 `x = 1` have "isnorm (R \<oplus> P2)" by simp
wenzelm@44779
   167
    with 7 `x = 1` have ?case
wenzelm@44779
   168
      by (simp add: norm_PXtrans[of Q2 y _]) }
chaieb@17378
   169
  moreover
chaieb@17378
   170
  { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
wenzelm@44779
   171
    then obtain d where X: "x=Suc (Suc d)" ..
wenzelm@41807
   172
    with 7 have NR: "isnorm R" "isnorm P2"
wenzelm@41807
   173
      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@41807
   174
    with 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
wenzelm@41807
   175
    with 7 X NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
wenzelm@44779
   176
    with `isnorm (PX Q2 y R)` X have ?case
wenzelm@44779
   177
      by (simp add: norm_PXtrans[of Q2 y _]) }
chaieb@17378
   178
  ultimately show ?case by blast
chaieb@17378
   179
next
chaieb@17378
   180
  case (8 Q2 y R x P2)
haftmann@22742
   181
  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
chaieb@17378
   182
  moreover
wenzelm@41807
   183
  { assume "x = 0" with 8 have ?case by (auto simp add: norm_Pinj_0_False) }
chaieb@17378
   184
  moreover
wenzelm@41807
   185
  { assume "x = 1"
wenzelm@41807
   186
    with 8 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@41807
   187
    with 8 `x = 1` have "isnorm (R \<oplus> P2)" by simp
wenzelm@41807
   188
    with 8 `x = 1` have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
chaieb@17378
   189
  moreover
chaieb@17378
   190
  { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
wenzelm@41807
   191
    then obtain d where X: "x = Suc (Suc d)" ..
wenzelm@41807
   192
    with 8 have NR: "isnorm R" "isnorm P2"
wenzelm@41807
   193
      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@41807
   194
    with 8 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
wenzelm@41807
   195
    with 8 `x > 1` NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
wenzelm@41807
   196
    with `isnorm (PX Q2 y R)` X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
chaieb@17378
   197
  ultimately show ?case by blast
chaieb@17378
   198
next
chaieb@17378
   199
  case (9 P1 x P2 Q1 y Q2)
wenzelm@41807
   200
  then have Y0: "y>0" by (cases y) auto
wenzelm@41807
   201
  with 9 have X0: "x>0" by (cases x) auto
wenzelm@41807
   202
  with 9 have NP1: "isnorm P1" and NP2: "isnorm P2"
wenzelm@41807
   203
    by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])
wenzelm@44779
   204
  with 9 have NQ1: "isnorm Q1" and NQ2: "isnorm Q2"
wenzelm@41807
   205
    by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])
chaieb@17378
   206
  have "y < x \<or> x = y \<or> x < y" by arith
chaieb@17378
   207
  moreover
wenzelm@41807
   208
  { assume sm1: "y < x" hence "EX d. x = d + y" by arith
wenzelm@41807
   209
    then obtain d where sm2: "x = d + y" ..
wenzelm@41807
   210
    note 9 NQ1 NP1 NP2 NQ2 sm1 sm2
chaieb@17378
   211
    moreover
chaieb@17378
   212
    have "isnorm (PX P1 d (Pc 0))" 
wenzelm@41807
   213
    proof (cases P1)
chaieb@17378
   214
      case (PX p1 y p2)
wenzelm@44779
   215
      with 9 sm1 sm2 show ?thesis by (cases d) (simp, cases p2, auto)
wenzelm@41807
   216
    next
wenzelm@41807
   217
      case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto
wenzelm@41807
   218
    next
wenzelm@41807
   219
      case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto
chaieb@17378
   220
    qed
haftmann@22742
   221
    ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)" by auto
wenzelm@41807
   222
    with Y0 sm1 sm2 have ?case by (simp add: mkPX_cn) }
chaieb@17378
   223
  moreover
wenzelm@41807
   224
  { assume "x = y"
wenzelm@41807
   225
    with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)" by auto
wenzelm@41807
   226
    with `x = y` Y0 have ?case by (simp add: mkPX_cn) }
chaieb@17378
   227
  moreover
wenzelm@41807
   228
  { assume sm1: "x < y" hence "EX d. y = d + x" by arith
wenzelm@41807
   229
    then obtain d where sm2: "y = d + x" ..
wenzelm@41807
   230
    note 9 NQ1 NP1 NP2 NQ2 sm1 sm2
chaieb@17378
   231
    moreover
chaieb@17378
   232
    have "isnorm (PX Q1 d (Pc 0))" 
wenzelm@41807
   233
    proof (cases Q1)
chaieb@17378
   234
      case (PX p1 y p2)
wenzelm@44779
   235
      with 9 sm1 sm2 show ?thesis by (cases d) (simp, cases p2, auto)
wenzelm@41807
   236
    next
wenzelm@41807
   237
      case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto
wenzelm@41807
   238
    next
wenzelm@41807
   239
      case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto
chaieb@17378
   240
    qed
haftmann@22742
   241
    ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)" by auto
wenzelm@44779
   242
    with X0 sm1 sm2 have ?case by (simp add: mkPX_cn) }
chaieb@17378
   243
  ultimately show ?case by blast
haftmann@22742
   244
qed simp
chaieb@17378
   245
haftmann@22742
   246
text {* mul concerves normalizedness *}
wenzelm@44779
   247
lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
wenzelm@44779
   248
proof (induct P Q rule: mul.induct)
chaieb@17378
   249
  case (2 c i P2) thus ?case 
wenzelm@44779
   250
    by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
chaieb@17378
   251
next
chaieb@17378
   252
  case (3 i P2 c) thus ?case 
wenzelm@44779
   253
    by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
chaieb@17378
   254
next
chaieb@17378
   255
  case (4 c P2 i Q2)
wenzelm@44779
   256
  then have "isnorm P2" "isnorm Q2"
wenzelm@44779
   257
    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
wenzelm@41807
   258
  with 4 show ?case 
wenzelm@44779
   259
    by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
chaieb@17378
   260
next
chaieb@17378
   261
  case (5 P2 i Q2 c)
wenzelm@44779
   262
  then have "isnorm P2" "isnorm Q2"
wenzelm@44779
   263
    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
wenzelm@41807
   264
  with 5 show ?case
wenzelm@44779
   265
    by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
chaieb@17378
   266
next
chaieb@17378
   267
  case (6 x P2 y Q2)
chaieb@17378
   268
  have "x < y \<or> x = y \<or> x > y" by arith
chaieb@17378
   269
  moreover
wenzelm@41807
   270
  { assume "x < y" hence "EX d. y = d + x" by arith
wenzelm@41807
   271
    then obtain d where y: "y = d + x" ..
chaieb@17378
   272
    moreover
wenzelm@41807
   273
    note 6
chaieb@17378
   274
    moreover
wenzelm@41807
   275
    from 6 have "x > 0" by (cases x) (auto simp add: norm_Pinj_0_False)
chaieb@17378
   276
    moreover
wenzelm@41807
   277
    from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
chaieb@17378
   278
    moreover
wenzelm@44779
   279
    from 6 `x < y` y have "isnorm (Pinj d Q2)" by (cases d) (simp, cases Q2, auto) 
wenzelm@41807
   280
    ultimately have ?case by (simp add: mkPinj_cn) }
chaieb@17378
   281
  moreover
wenzelm@41807
   282
  { assume "x = y"
chaieb@17378
   283
    moreover
wenzelm@41807
   284
    from 6 have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
chaieb@17378
   285
    moreover
wenzelm@41807
   286
    from 6 have "y>0" by (cases y) (auto simp add: norm_Pinj_0_False)
chaieb@17378
   287
    moreover
wenzelm@41807
   288
    note 6
chaieb@17378
   289
    moreover
chaieb@17378
   290
    ultimately have ?case by (simp add: mkPinj_cn) }
chaieb@17378
   291
  moreover
wenzelm@41807
   292
  { assume "x > y" hence "EX d. x = d + y" by arith
wenzelm@41807
   293
    then obtain d where x: "x = d + y" ..
chaieb@17378
   294
    moreover
wenzelm@41807
   295
    note 6
chaieb@17378
   296
    moreover
wenzelm@41807
   297
    from 6 have "y > 0" by (cases y) (auto simp add: norm_Pinj_0_False)
chaieb@17378
   298
    moreover
wenzelm@41807
   299
    from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
chaieb@17378
   300
    moreover
wenzelm@44779
   301
    from 6 `x > y` x have "isnorm (Pinj d P2)" by (cases d) (simp, cases P2, auto)
chaieb@17378
   302
    ultimately have ?case by (simp add: mkPinj_cn) }
chaieb@17378
   303
  ultimately show ?case by blast
chaieb@17378
   304
next
chaieb@17378
   305
  case (7 x P2 Q2 y R)
wenzelm@41807
   306
  then have Y0: "y > 0" by (cases y) auto
wenzelm@41807
   307
  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
chaieb@17378
   308
  moreover
wenzelm@41807
   309
  { assume "x = 0" with 7 have ?case by (auto simp add: norm_Pinj_0_False) }
chaieb@17378
   310
  moreover
wenzelm@41807
   311
  { assume "x = 1"
wenzelm@41807
   312
    from 7 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@41807
   313
    with 7 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
wenzelm@41807
   314
    with 7 `x = 1` Y0 have ?case by (simp add: mkPX_cn) }
chaieb@17378
   315
  moreover
wenzelm@41807
   316
  { assume "x > 1" hence "EX d. x = Suc (Suc d)" by arith
wenzelm@41807
   317
    then obtain d where X: "x = Suc (Suc d)" ..
wenzelm@41807
   318
    from 7 have NR: "isnorm R" "isnorm Q2"
wenzelm@41807
   319
      by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
chaieb@17378
   320
    moreover
wenzelm@41807
   321
    from 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
wenzelm@41807
   322
    moreover
wenzelm@41807
   323
    from 7 have "isnorm (Pinj x P2)" by (cases P2) auto
chaieb@17378
   324
    moreover
wenzelm@41807
   325
    note 7 X
haftmann@22742
   326
    ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto
wenzelm@41807
   327
    with Y0 X have ?case by (simp add: mkPX_cn) }
chaieb@17378
   328
  ultimately show ?case by blast
chaieb@17378
   329
next
chaieb@17378
   330
  case (8 Q2 y R x P2)
wenzelm@41807
   331
  then have Y0: "y>0" by (cases y) auto
wenzelm@41807
   332
  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
chaieb@17378
   333
  moreover
wenzelm@41807
   334
  { assume "x = 0" with 8 have ?case by (auto simp add: norm_Pinj_0_False) }
chaieb@17378
   335
  moreover
wenzelm@41807
   336
  { assume "x = 1"
wenzelm@41807
   337
    from 8 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@41807
   338
    with 8 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
wenzelm@41807
   339
    with 8 `x = 1` Y0 have ?case by (simp add: mkPX_cn) }
chaieb@17378
   340
  moreover
wenzelm@41807
   341
  { assume "x > 1" hence "EX d. x = Suc (Suc d)" by arith
wenzelm@41807
   342
    then obtain d where X: "x = Suc (Suc d)" ..
wenzelm@41807
   343
    from 8 have NR: "isnorm R" "isnorm Q2"
wenzelm@41807
   344
      by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
chaieb@17378
   345
    moreover
wenzelm@41807
   346
    from 8 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
chaieb@17378
   347
    moreover
wenzelm@41807
   348
    from 8 X have "isnorm (Pinj x P2)" by (cases P2) auto
chaieb@17378
   349
    moreover
wenzelm@41807
   350
    note 8 X
haftmann@22742
   351
    ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto
chaieb@17378
   352
    with Y0 X have ?case by (simp add: mkPX_cn) }
chaieb@17378
   353
  ultimately show ?case by blast
chaieb@17378
   354
next
chaieb@17378
   355
  case (9 P1 x P2 Q1 y Q2)
wenzelm@41807
   356
  from 9 have X0: "x > 0" by (cases x) auto
wenzelm@41807
   357
  from 9 have Y0: "y > 0" by (cases y) auto
wenzelm@41807
   358
  note 9
chaieb@17378
   359
  moreover
wenzelm@41807
   360
  from 9 have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
chaieb@17378
   361
  moreover 
wenzelm@41807
   362
  from 9 have "isnorm Q1" "isnorm Q2" by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2])
haftmann@22742
   363
  ultimately have "isnorm (P1 \<otimes> Q1)" "isnorm (P2 \<otimes> Q2)"
haftmann@22742
   364
    "isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)" 
chaieb@17378
   365
    by (auto simp add: mkPinj_cn)
wenzelm@41807
   366
  with 9 X0 Y0 have
haftmann@22742
   367
    "isnorm (mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2))"
haftmann@22742
   368
    "isnorm (mkPX (P1 \<otimes> mkPinj (Suc 0) Q2) x (Pc 0))"  
haftmann@22742
   369
    "isnorm (mkPX (Q1 \<otimes> mkPinj (Suc 0) P2) y (Pc 0))" 
chaieb@17378
   370
    by (auto simp add: mkPX_cn)
chaieb@17378
   371
  thus ?case by (simp add: add_cn)
wenzelm@41807
   372
qed simp
chaieb@17378
   373
haftmann@22742
   374
text {* neg conserves normalizedness *}
chaieb@17378
   375
lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"
haftmann@22742
   376
proof (induct P)
chaieb@17378
   377
  case (Pinj i P2)
wenzelm@41807
   378
  then have "isnorm P2" by (simp add: norm_Pinj[of i P2])
wenzelm@44779
   379
  with Pinj show ?case by (cases P2) (auto, cases i, auto)
chaieb@17378
   380
next
wenzelm@41807
   381
  case (PX P1 x P2) note PX1 = this
wenzelm@41807
   382
  from PX have "isnorm P2" "isnorm P1"
wenzelm@41807
   383
    by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
wenzelm@41807
   384
  with PX show ?case
wenzelm@41807
   385
  proof (cases P1)
chaieb@17378
   386
    case (PX p1 y p2)
wenzelm@44779
   387
    with PX1 show ?thesis by (cases x) (auto, cases p2, auto)
chaieb@17378
   388
  next
chaieb@17378
   389
    case Pinj
wenzelm@41807
   390
    with PX1 show ?thesis by (cases x) auto
wenzelm@41807
   391
  qed (cases x, auto)
wenzelm@41807
   392
qed simp
chaieb@17378
   393
haftmann@22742
   394
text {* sub conserves normalizedness *}
wenzelm@44779
   395
lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
wenzelm@44779
   396
  by (simp add: sub_def add_cn neg_cn)
chaieb@17378
   397
haftmann@22742
   398
text {* sqr conserves normalizizedness *}
wenzelm@44779
   399
lemma sqr_cn: "isnorm P \<Longrightarrow> isnorm (sqr P)"
wenzelm@41807
   400
proof (induct P)
wenzelm@44779
   401
  case Pc
wenzelm@44779
   402
  then show ?case by simp
wenzelm@44779
   403
next
chaieb@17378
   404
  case (Pinj i Q)
wenzelm@41807
   405
  then show ?case
wenzelm@44779
   406
    by (cases Q) (auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
chaieb@17378
   407
next 
chaieb@17378
   408
  case (PX P1 x P2)
wenzelm@41807
   409
  then have "x + x ~= 0" "isnorm P2" "isnorm P1"
wenzelm@41807
   410
    by (cases x, auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
wenzelm@41807
   411
  with PX have "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))"
wenzelm@41807
   412
      and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
wenzelm@41807
   413
    by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
wenzelm@41807
   414
  then show ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
wenzelm@44779
   415
qed
chaieb@17378
   416
haftmann@22742
   417
text {* pow conserves normalizedness *}
wenzelm@44779
   418
lemma pow_cn: "isnorm P \<Longrightarrow> isnorm (pow n P)"
wenzelm@44779
   419
proof (induct n arbitrary: P rule: less_induct)
wenzelm@44779
   420
  case (less k)
chaieb@17378
   421
  show ?case 
wenzelm@41807
   422
  proof (cases "k = 0")
wenzelm@44779
   423
    case True
wenzelm@44779
   424
    then show ?thesis by simp
wenzelm@44779
   425
  next
chaieb@17378
   426
    case False
wenzelm@41807
   427
    then have K2: "k div 2 < k" by (cases k) auto
wenzelm@44779
   428
    from less have "isnorm (sqr P)" by (simp add: sqr_cn)
wenzelm@44779
   429
    with less False K2 show ?thesis
wenzelm@44779
   430
      by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
wenzelm@44779
   431
  qed
chaieb@17378
   432
qed
chaieb@17378
   433
wenzelm@17388
   434
end