src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
author wenzelm
Tue Sep 03 01:12:40 2013 +0200 (2013-09-03)
changeset 53374 a14d2a854c02
parent 44779 98d597c4193d
child 55754 d14072d53c1e
permissions -rw-r--r--
tuned proofs -- clarified flow of facts wrt. calculation;
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
    ultimately have ?case by (simp add: mkPinj_cn) }
chaieb@17378
   142
  moreover
wenzelm@41807
   143
  { assume "x>y" hence "EX d. x = d + y" by arith
wenzelm@41807
   144
    then obtain d where x: "x = d + y"..
chaieb@17378
   145
    moreover
wenzelm@41807
   146
    note 6 Y0
chaieb@17378
   147
    moreover
wenzelm@44779
   148
    from 6 have "isnorm P2" "isnorm Q2"
wenzelm@44779
   149
      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
chaieb@17378
   150
    moreover
wenzelm@44779
   151
    from 6 `x > y` x have "isnorm (Pinj d P2)"
wenzelm@44779
   152
      by (cases d) (simp, cases P2, auto)
wenzelm@44779
   153
    ultimately have ?case by (simp add: mkPinj_cn) }
chaieb@17378
   154
  ultimately show ?case by blast
chaieb@17378
   155
next
chaieb@17378
   156
  case (7 x P2 Q2 y R)
wenzelm@44779
   157
  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
chaieb@17378
   158
  moreover
wenzelm@41807
   159
  { assume "x = 0"
wenzelm@41807
   160
    with 7 have ?case by (auto simp add: norm_Pinj_0_False) }
chaieb@17378
   161
  moreover
wenzelm@41807
   162
  { assume "x = 1"
wenzelm@44779
   163
    from 7 have "isnorm R" "isnorm P2"
wenzelm@44779
   164
      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@41807
   165
    with 7 `x = 1` have "isnorm (R \<oplus> P2)" by simp
wenzelm@44779
   166
    with 7 `x = 1` have ?case
wenzelm@44779
   167
      by (simp add: norm_PXtrans[of Q2 y _]) }
chaieb@17378
   168
  moreover
chaieb@17378
   169
  { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
wenzelm@44779
   170
    then obtain d where X: "x=Suc (Suc d)" ..
wenzelm@41807
   171
    with 7 have NR: "isnorm R" "isnorm P2"
wenzelm@41807
   172
      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@41807
   173
    with 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
wenzelm@41807
   174
    with 7 X NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
wenzelm@44779
   175
    with `isnorm (PX Q2 y R)` X have ?case
wenzelm@44779
   176
      by (simp add: norm_PXtrans[of Q2 y _]) }
chaieb@17378
   177
  ultimately show ?case by blast
chaieb@17378
   178
next
chaieb@17378
   179
  case (8 Q2 y R x P2)
haftmann@22742
   180
  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
chaieb@17378
   181
  moreover
wenzelm@41807
   182
  { assume "x = 0" with 8 have ?case by (auto simp add: norm_Pinj_0_False) }
chaieb@17378
   183
  moreover
wenzelm@41807
   184
  { assume "x = 1"
wenzelm@41807
   185
    with 8 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@41807
   186
    with 8 `x = 1` have "isnorm (R \<oplus> P2)" by simp
wenzelm@41807
   187
    with 8 `x = 1` have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
chaieb@17378
   188
  moreover
chaieb@17378
   189
  { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
wenzelm@41807
   190
    then obtain d where X: "x = Suc (Suc d)" ..
wenzelm@41807
   191
    with 8 have NR: "isnorm R" "isnorm P2"
wenzelm@41807
   192
      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@41807
   193
    with 8 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
wenzelm@41807
   194
    with 8 `x > 1` NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
wenzelm@41807
   195
    with `isnorm (PX Q2 y R)` X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
chaieb@17378
   196
  ultimately show ?case by blast
chaieb@17378
   197
next
chaieb@17378
   198
  case (9 P1 x P2 Q1 y Q2)
wenzelm@41807
   199
  then have Y0: "y>0" by (cases y) auto
wenzelm@41807
   200
  with 9 have X0: "x>0" by (cases x) auto
wenzelm@41807
   201
  with 9 have NP1: "isnorm P1" and NP2: "isnorm P2"
wenzelm@41807
   202
    by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])
wenzelm@44779
   203
  with 9 have NQ1: "isnorm Q1" and NQ2: "isnorm Q2"
wenzelm@41807
   204
    by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])
chaieb@17378
   205
  have "y < x \<or> x = y \<or> x < y" by arith
chaieb@17378
   206
  moreover
wenzelm@41807
   207
  { assume sm1: "y < x" hence "EX d. x = d + y" by arith
wenzelm@41807
   208
    then obtain d where sm2: "x = d + y" ..
wenzelm@41807
   209
    note 9 NQ1 NP1 NP2 NQ2 sm1 sm2
chaieb@17378
   210
    moreover
chaieb@17378
   211
    have "isnorm (PX P1 d (Pc 0))" 
wenzelm@41807
   212
    proof (cases P1)
chaieb@17378
   213
      case (PX p1 y p2)
wenzelm@44779
   214
      with 9 sm1 sm2 show ?thesis by (cases d) (simp, cases p2, auto)
wenzelm@41807
   215
    next
wenzelm@41807
   216
      case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto
wenzelm@41807
   217
    next
wenzelm@41807
   218
      case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto
chaieb@17378
   219
    qed
haftmann@22742
   220
    ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)" by auto
wenzelm@41807
   221
    with Y0 sm1 sm2 have ?case by (simp add: mkPX_cn) }
chaieb@17378
   222
  moreover
wenzelm@41807
   223
  { assume "x = y"
wenzelm@41807
   224
    with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)" by auto
wenzelm@41807
   225
    with `x = y` Y0 have ?case by (simp add: mkPX_cn) }
chaieb@17378
   226
  moreover
wenzelm@41807
   227
  { assume sm1: "x < y" hence "EX d. y = d + x" by arith
wenzelm@41807
   228
    then obtain d where sm2: "y = d + x" ..
wenzelm@41807
   229
    note 9 NQ1 NP1 NP2 NQ2 sm1 sm2
chaieb@17378
   230
    moreover
chaieb@17378
   231
    have "isnorm (PX Q1 d (Pc 0))" 
wenzelm@41807
   232
    proof (cases Q1)
chaieb@17378
   233
      case (PX p1 y p2)
wenzelm@44779
   234
      with 9 sm1 sm2 show ?thesis by (cases d) (simp, cases p2, auto)
wenzelm@41807
   235
    next
wenzelm@41807
   236
      case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto
wenzelm@41807
   237
    next
wenzelm@41807
   238
      case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto
chaieb@17378
   239
    qed
haftmann@22742
   240
    ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)" by auto
wenzelm@44779
   241
    with X0 sm1 sm2 have ?case by (simp add: mkPX_cn) }
chaieb@17378
   242
  ultimately show ?case by blast
haftmann@22742
   243
qed simp
chaieb@17378
   244
haftmann@22742
   245
text {* mul concerves normalizedness *}
wenzelm@44779
   246
lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
wenzelm@44779
   247
proof (induct P Q rule: mul.induct)
chaieb@17378
   248
  case (2 c i P2) thus ?case 
wenzelm@44779
   249
    by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
chaieb@17378
   250
next
chaieb@17378
   251
  case (3 i P2 c) thus ?case 
wenzelm@44779
   252
    by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
chaieb@17378
   253
next
chaieb@17378
   254
  case (4 c P2 i Q2)
wenzelm@44779
   255
  then have "isnorm P2" "isnorm Q2"
wenzelm@44779
   256
    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
wenzelm@41807
   257
  with 4 show ?case 
wenzelm@44779
   258
    by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
chaieb@17378
   259
next
chaieb@17378
   260
  case (5 P2 i Q2 c)
wenzelm@44779
   261
  then have "isnorm P2" "isnorm Q2"
wenzelm@44779
   262
    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
wenzelm@41807
   263
  with 5 show ?case
wenzelm@44779
   264
    by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
chaieb@17378
   265
next
chaieb@17378
   266
  case (6 x P2 y Q2)
chaieb@17378
   267
  have "x < y \<or> x = y \<or> x > y" by arith
chaieb@17378
   268
  moreover
wenzelm@41807
   269
  { assume "x < y" hence "EX d. y = d + x" by arith
wenzelm@41807
   270
    then obtain d where y: "y = d + x" ..
chaieb@17378
   271
    moreover
wenzelm@41807
   272
    note 6
chaieb@17378
   273
    moreover
wenzelm@41807
   274
    from 6 have "x > 0" by (cases x) (auto simp add: norm_Pinj_0_False)
chaieb@17378
   275
    moreover
wenzelm@41807
   276
    from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
chaieb@17378
   277
    moreover
wenzelm@44779
   278
    from 6 `x < y` y have "isnorm (Pinj d Q2)" by (cases d) (simp, cases Q2, auto) 
wenzelm@41807
   279
    ultimately have ?case by (simp add: mkPinj_cn) }
chaieb@17378
   280
  moreover
wenzelm@41807
   281
  { assume "x = y"
chaieb@17378
   282
    moreover
wenzelm@41807
   283
    from 6 have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
chaieb@17378
   284
    moreover
wenzelm@41807
   285
    from 6 have "y>0" by (cases y) (auto simp add: norm_Pinj_0_False)
chaieb@17378
   286
    moreover
wenzelm@41807
   287
    note 6
chaieb@17378
   288
    ultimately have ?case by (simp add: mkPinj_cn) }
chaieb@17378
   289
  moreover
wenzelm@41807
   290
  { assume "x > y" hence "EX d. x = d + y" by arith
wenzelm@41807
   291
    then obtain d where x: "x = d + y" ..
chaieb@17378
   292
    moreover
wenzelm@41807
   293
    note 6
chaieb@17378
   294
    moreover
wenzelm@41807
   295
    from 6 have "y > 0" by (cases y) (auto simp add: norm_Pinj_0_False)
chaieb@17378
   296
    moreover
wenzelm@41807
   297
    from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
chaieb@17378
   298
    moreover
wenzelm@44779
   299
    from 6 `x > y` x have "isnorm (Pinj d P2)" by (cases d) (simp, cases P2, auto)
chaieb@17378
   300
    ultimately have ?case by (simp add: mkPinj_cn) }
chaieb@17378
   301
  ultimately show ?case by blast
chaieb@17378
   302
next
chaieb@17378
   303
  case (7 x P2 Q2 y R)
wenzelm@41807
   304
  then have Y0: "y > 0" by (cases y) auto
wenzelm@41807
   305
  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
chaieb@17378
   306
  moreover
wenzelm@41807
   307
  { assume "x = 0" with 7 have ?case by (auto simp add: norm_Pinj_0_False) }
chaieb@17378
   308
  moreover
wenzelm@41807
   309
  { assume "x = 1"
wenzelm@41807
   310
    from 7 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@41807
   311
    with 7 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
wenzelm@41807
   312
    with 7 `x = 1` Y0 have ?case by (simp add: mkPX_cn) }
chaieb@17378
   313
  moreover
wenzelm@41807
   314
  { assume "x > 1" hence "EX d. x = Suc (Suc d)" by arith
wenzelm@41807
   315
    then obtain d where X: "x = Suc (Suc d)" ..
wenzelm@41807
   316
    from 7 have NR: "isnorm R" "isnorm Q2"
wenzelm@41807
   317
      by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
chaieb@17378
   318
    moreover
wenzelm@41807
   319
    from 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
wenzelm@41807
   320
    moreover
wenzelm@41807
   321
    from 7 have "isnorm (Pinj x P2)" by (cases P2) auto
chaieb@17378
   322
    moreover
wenzelm@41807
   323
    note 7 X
haftmann@22742
   324
    ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto
wenzelm@41807
   325
    with Y0 X have ?case by (simp add: mkPX_cn) }
chaieb@17378
   326
  ultimately show ?case by blast
chaieb@17378
   327
next
chaieb@17378
   328
  case (8 Q2 y R x P2)
wenzelm@41807
   329
  then have Y0: "y>0" by (cases y) auto
wenzelm@41807
   330
  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
chaieb@17378
   331
  moreover
wenzelm@41807
   332
  { assume "x = 0" with 8 have ?case by (auto simp add: norm_Pinj_0_False) }
chaieb@17378
   333
  moreover
wenzelm@41807
   334
  { assume "x = 1"
wenzelm@41807
   335
    from 8 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@41807
   336
    with 8 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
wenzelm@41807
   337
    with 8 `x = 1` Y0 have ?case by (simp add: mkPX_cn) }
chaieb@17378
   338
  moreover
wenzelm@41807
   339
  { assume "x > 1" hence "EX d. x = Suc (Suc d)" by arith
wenzelm@41807
   340
    then obtain d where X: "x = Suc (Suc d)" ..
wenzelm@41807
   341
    from 8 have NR: "isnorm R" "isnorm Q2"
wenzelm@41807
   342
      by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
chaieb@17378
   343
    moreover
wenzelm@41807
   344
    from 8 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
chaieb@17378
   345
    moreover
wenzelm@41807
   346
    from 8 X have "isnorm (Pinj x P2)" by (cases P2) auto
chaieb@17378
   347
    moreover
wenzelm@41807
   348
    note 8 X
haftmann@22742
   349
    ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto
chaieb@17378
   350
    with Y0 X have ?case by (simp add: mkPX_cn) }
chaieb@17378
   351
  ultimately show ?case by blast
chaieb@17378
   352
next
chaieb@17378
   353
  case (9 P1 x P2 Q1 y Q2)
wenzelm@41807
   354
  from 9 have X0: "x > 0" by (cases x) auto
wenzelm@41807
   355
  from 9 have Y0: "y > 0" by (cases y) auto
wenzelm@41807
   356
  note 9
chaieb@17378
   357
  moreover
wenzelm@41807
   358
  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
   359
  moreover 
wenzelm@41807
   360
  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
   361
  ultimately have "isnorm (P1 \<otimes> Q1)" "isnorm (P2 \<otimes> Q2)"
haftmann@22742
   362
    "isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)" 
chaieb@17378
   363
    by (auto simp add: mkPinj_cn)
wenzelm@41807
   364
  with 9 X0 Y0 have
haftmann@22742
   365
    "isnorm (mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2))"
haftmann@22742
   366
    "isnorm (mkPX (P1 \<otimes> mkPinj (Suc 0) Q2) x (Pc 0))"  
haftmann@22742
   367
    "isnorm (mkPX (Q1 \<otimes> mkPinj (Suc 0) P2) y (Pc 0))" 
chaieb@17378
   368
    by (auto simp add: mkPX_cn)
chaieb@17378
   369
  thus ?case by (simp add: add_cn)
wenzelm@41807
   370
qed simp
chaieb@17378
   371
haftmann@22742
   372
text {* neg conserves normalizedness *}
chaieb@17378
   373
lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"
haftmann@22742
   374
proof (induct P)
chaieb@17378
   375
  case (Pinj i P2)
wenzelm@41807
   376
  then have "isnorm P2" by (simp add: norm_Pinj[of i P2])
wenzelm@44779
   377
  with Pinj show ?case by (cases P2) (auto, cases i, auto)
chaieb@17378
   378
next
wenzelm@41807
   379
  case (PX P1 x P2) note PX1 = this
wenzelm@41807
   380
  from PX have "isnorm P2" "isnorm P1"
wenzelm@41807
   381
    by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
wenzelm@41807
   382
  with PX show ?case
wenzelm@41807
   383
  proof (cases P1)
chaieb@17378
   384
    case (PX p1 y p2)
wenzelm@44779
   385
    with PX1 show ?thesis by (cases x) (auto, cases p2, auto)
chaieb@17378
   386
  next
chaieb@17378
   387
    case Pinj
wenzelm@41807
   388
    with PX1 show ?thesis by (cases x) auto
wenzelm@41807
   389
  qed (cases x, auto)
wenzelm@41807
   390
qed simp
chaieb@17378
   391
haftmann@22742
   392
text {* sub conserves normalizedness *}
wenzelm@44779
   393
lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
wenzelm@44779
   394
  by (simp add: sub_def add_cn neg_cn)
chaieb@17378
   395
haftmann@22742
   396
text {* sqr conserves normalizizedness *}
wenzelm@44779
   397
lemma sqr_cn: "isnorm P \<Longrightarrow> isnorm (sqr P)"
wenzelm@41807
   398
proof (induct P)
wenzelm@44779
   399
  case Pc
wenzelm@44779
   400
  then show ?case by simp
wenzelm@44779
   401
next
chaieb@17378
   402
  case (Pinj i Q)
wenzelm@41807
   403
  then show ?case
wenzelm@44779
   404
    by (cases Q) (auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
chaieb@17378
   405
next 
chaieb@17378
   406
  case (PX P1 x P2)
wenzelm@41807
   407
  then have "x + x ~= 0" "isnorm P2" "isnorm P1"
wenzelm@41807
   408
    by (cases x, auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
wenzelm@41807
   409
  with PX have "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))"
wenzelm@41807
   410
      and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
wenzelm@41807
   411
    by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
wenzelm@41807
   412
  then show ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
wenzelm@44779
   413
qed
chaieb@17378
   414
haftmann@22742
   415
text {* pow conserves normalizedness *}
wenzelm@44779
   416
lemma pow_cn: "isnorm P \<Longrightarrow> isnorm (pow n P)"
wenzelm@44779
   417
proof (induct n arbitrary: P rule: less_induct)
wenzelm@44779
   418
  case (less k)
chaieb@17378
   419
  show ?case 
wenzelm@41807
   420
  proof (cases "k = 0")
wenzelm@44779
   421
    case True
wenzelm@44779
   422
    then show ?thesis by simp
wenzelm@44779
   423
  next
chaieb@17378
   424
    case False
wenzelm@41807
   425
    then have K2: "k div 2 < k" by (cases k) auto
wenzelm@44779
   426
    from less have "isnorm (sqr P)" by (simp add: sqr_cn)
wenzelm@44779
   427
    with less False K2 show ?thesis
wenzelm@44779
   428
      by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
wenzelm@44779
   429
  qed
chaieb@17378
   430
qed
chaieb@17378
   431
wenzelm@17388
   432
end