src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
author wenzelm
Thu Feb 27 21:31:58 2014 +0100 (2014-02-27)
changeset 55793 52c8f934ea6f
parent 55754 d14072d53c1e
child 58259 52c35a59bbf5
permissions -rw-r--r--
tuned whitespace;
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
wenzelm@55754
    17
  "isnorm (Pc c) \<longleftrightarrow> True"
wenzelm@55754
    18
| "isnorm (Pinj i (Pc c)) \<longleftrightarrow> False"
wenzelm@55754
    19
| "isnorm (Pinj i (Pinj j Q)) \<longleftrightarrow> False"
wenzelm@55754
    20
| "isnorm (Pinj 0 P) \<longleftrightarrow> False"
wenzelm@55754
    21
| "isnorm (Pinj i (PX Q1 j Q2)) \<longleftrightarrow> isnorm (PX Q1 j Q2)"
wenzelm@55754
    22
| "isnorm (PX P 0 Q) \<longleftrightarrow> False"
wenzelm@55754
    23
| "isnorm (PX (Pc c) i Q) \<longleftrightarrow> c \<noteq> 0 \<and> isnorm Q"
wenzelm@55754
    24
| "isnorm (PX (PX P1 j (Pc c)) i Q) \<longleftrightarrow> c \<noteq> 0 \<and> isnorm (PX P1 j (Pc c)) \<and> isnorm Q"
wenzelm@55754
    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@55754
    38
  apply (cases i)
wenzelm@55754
    39
  apply auto
wenzelm@55754
    40
  apply (cases P)
wenzelm@55754
    41
  apply auto
wenzelm@55754
    42
  apply (case_tac pol2)
wenzelm@55754
    43
  apply auto
wenzelm@55754
    44
  done
wenzelm@44779
    45
wenzelm@44779
    46
lemma norm_PX1: "isnorm (PX P i Q) \<Longrightarrow> isnorm P"
wenzelm@55754
    47
  apply (cases i)
wenzelm@55754
    48
  apply auto
wenzelm@55754
    49
  apply (cases P)
wenzelm@55754
    50
  apply auto
wenzelm@55754
    51
  apply (case_tac pol2)
wenzelm@55754
    52
  apply auto
wenzelm@55754
    53
  done
chaieb@17378
    54
wenzelm@55754
    55
lemma mkPinj_cn: "y \<noteq> 0 \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (mkPinj y Q)"
wenzelm@44779
    56
  apply (auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split)
wenzelm@44779
    57
  apply (case_tac nat, auto simp add: norm_Pinj_0_False)
wenzelm@44779
    58
  apply (case_tac pol, auto)
wenzelm@44779
    59
  apply (case_tac y, auto)
wenzelm@44779
    60
  done
chaieb@17378
    61
wenzelm@55793
    62
lemma norm_PXtrans:
wenzelm@55754
    63
  assumes A: "isnorm (PX P x Q)"
wenzelm@55793
    64
    and "isnorm Q2"
chaieb@17378
    65
  shows "isnorm (PX P x Q2)"
wenzelm@44779
    66
proof (cases P)
wenzelm@44779
    67
  case (PX p1 y p2)
wenzelm@55754
    68
  with assms show ?thesis
wenzelm@55754
    69
    apply (cases x)
wenzelm@55754
    70
    apply auto
wenzelm@55754
    71
    apply (cases p2)
wenzelm@55754
    72
    apply auto
wenzelm@55754
    73
    done
chaieb@17378
    74
next
wenzelm@44779
    75
  case Pc
wenzelm@44779
    76
  with assms show ?thesis by (cases x) auto
chaieb@17378
    77
next
wenzelm@44779
    78
  case Pinj
wenzelm@44779
    79
  with assms show ?thesis by (cases x) auto
chaieb@17378
    80
qed
chaieb@17378
    81
wenzelm@55793
    82
lemma norm_PXtrans2:
wenzelm@55793
    83
  assumes "isnorm (PX P x Q)"
wenzelm@55793
    84
    and "isnorm Q2"
wenzelm@55793
    85
  shows "isnorm (PX P (Suc (n + x)) Q2)"
wenzelm@55793
    86
proof (cases P)
wenzelm@55793
    87
  case (PX p1 y p2)
wenzelm@55793
    88
  with assms show ?thesis
wenzelm@55793
    89
    apply (cases x)
wenzelm@55793
    90
    apply auto
wenzelm@55793
    91
    apply (cases p2)
wenzelm@55793
    92
    apply auto
wenzelm@55793
    93
    done
wenzelm@55793
    94
next
wenzelm@55793
    95
  case Pc
wenzelm@55793
    96
  with assms show ?thesis
wenzelm@55793
    97
    by (cases x) auto
wenzelm@55793
    98
next
wenzelm@55793
    99
  case Pinj
wenzelm@55793
   100
  with assms show ?thesis
wenzelm@55793
   101
    by (cases x) auto
wenzelm@55793
   102
qed
wenzelm@55793
   103
wenzelm@23266
   104
text {* mkPX conserves normalizedness (@{text "_cn"}) *}
wenzelm@55793
   105
lemma mkPX_cn:
wenzelm@55754
   106
  assumes "x \<noteq> 0"
wenzelm@55754
   107
    and "isnorm P"
wenzelm@55793
   108
    and "isnorm Q"
chaieb@17378
   109
  shows "isnorm (mkPX P x Q)"
wenzelm@55754
   110
proof (cases P)
chaieb@17378
   111
  case (Pc c)
wenzelm@55754
   112
  with assms show ?thesis
wenzelm@55754
   113
    by (cases x) (auto simp add: mkPinj_cn mkPX_def)
chaieb@17378
   114
next
chaieb@17378
   115
  case (Pinj i Q)
wenzelm@55754
   116
  with assms show ?thesis
wenzelm@55754
   117
    by (cases x) (auto simp add: mkPinj_cn mkPX_def)
chaieb@17378
   118
next
chaieb@17378
   119
  case (PX P1 y P2)
wenzelm@55793
   120
  with assms have Y0: "y > 0"
wenzelm@55793
   121
    by (cases y) auto
wenzelm@41807
   122
  from assms PX have "isnorm P1" "isnorm P2"
wenzelm@41807
   123
    by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2])
wenzelm@41807
   124
  from assms PX Y0 show ?thesis
wenzelm@44779
   125
    by (cases x) (auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
chaieb@17378
   126
qed
chaieb@17378
   127
haftmann@22742
   128
text {* add conserves normalizedness *}
wenzelm@44779
   129
lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
wenzelm@44779
   130
proof (induct P Q rule: add.induct)
wenzelm@44779
   131
  case (2 c i P2)
wenzelm@55793
   132
  then show ?case
wenzelm@55793
   133
    by (cases P2) (simp_all, cases i, simp_all)
chaieb@17378
   134
next
wenzelm@44779
   135
  case (3 i P2 c)
wenzelm@55793
   136
  then show ?case
wenzelm@55793
   137
    by (cases P2) (simp_all, cases i, simp_all)
chaieb@17378
   138
next
chaieb@17378
   139
  case (4 c P2 i Q2)
wenzelm@44779
   140
  then have "isnorm P2" "isnorm Q2"
wenzelm@44779
   141
    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
wenzelm@44779
   142
  with 4 show ?case
wenzelm@44779
   143
    by (cases i) (simp, cases P2, auto, case_tac pol2, auto)
chaieb@17378
   144
next
chaieb@17378
   145
  case (5 P2 i Q2 c)
wenzelm@44779
   146
  then have "isnorm P2" "isnorm Q2"
wenzelm@44779
   147
    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
wenzelm@44779
   148
  with 5 show ?case
wenzelm@44779
   149
    by (cases i) (simp, cases P2, auto, case_tac pol2, auto)
chaieb@17378
   150
next
chaieb@17378
   151
  case (6 x P2 y Q2)
wenzelm@55793
   152
  then have Y0: "y > 0"
wenzelm@55793
   153
    by (cases y) (auto simp add: norm_Pinj_0_False)
wenzelm@55793
   154
  with 6 have X0: "x > 0"
wenzelm@55793
   155
    by (cases x) (auto simp add: norm_Pinj_0_False)
chaieb@17378
   156
  have "x < y \<or> x = y \<or> x > y" by arith
wenzelm@55793
   157
  moreover {
wenzelm@55793
   158
    assume "x < y"
wenzelm@55754
   159
    then have "\<exists>d. y = d + x" by arith
wenzelm@41807
   160
    then obtain d where y: "y = d + x" ..
chaieb@17378
   161
    moreover
wenzelm@41807
   162
    note 6 X0
chaieb@17378
   163
    moreover
wenzelm@44779
   164
    from 6 have "isnorm P2" "isnorm Q2"
wenzelm@44779
   165
      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
chaieb@17378
   166
    moreover
wenzelm@44779
   167
    from 6 `x < y` y have "isnorm (Pinj d Q2)"
wenzelm@44779
   168
      by (cases d, simp, cases Q2, auto)
wenzelm@55793
   169
    ultimately have ?case by (simp add: mkPinj_cn)
wenzelm@55793
   170
  }
wenzelm@55793
   171
  moreover {
wenzelm@55793
   172
    assume "x = y"
chaieb@17378
   173
    moreover
wenzelm@44779
   174
    from 6 have "isnorm P2" "isnorm Q2"
wenzelm@44779
   175
      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
chaieb@17378
   176
    moreover
wenzelm@41807
   177
    note 6 Y0
wenzelm@55793
   178
    ultimately have ?case by (simp add: mkPinj_cn)
wenzelm@55793
   179
  }
wenzelm@55793
   180
  moreover {
wenzelm@55793
   181
    assume "x > y"
wenzelm@55793
   182
    then have "\<exists>d. x = d + y"
wenzelm@55793
   183
      by arith
wenzelm@55793
   184
    then obtain d where x: "x = d + y" ..
chaieb@17378
   185
    moreover
wenzelm@41807
   186
    note 6 Y0
chaieb@17378
   187
    moreover
wenzelm@44779
   188
    from 6 have "isnorm P2" "isnorm Q2"
wenzelm@44779
   189
      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
chaieb@17378
   190
    moreover
wenzelm@44779
   191
    from 6 `x > y` x have "isnorm (Pinj d P2)"
wenzelm@44779
   192
      by (cases d) (simp, cases P2, auto)
wenzelm@55793
   193
    ultimately have ?case by (simp add: mkPinj_cn)
wenzelm@55793
   194
  }
chaieb@17378
   195
  ultimately show ?case by blast
chaieb@17378
   196
next
chaieb@17378
   197
  case (7 x P2 Q2 y R)
wenzelm@44779
   198
  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
wenzelm@55793
   199
  moreover {
wenzelm@55793
   200
    assume "x = 0"
wenzelm@55793
   201
    with 7 have ?case by (auto simp add: norm_Pinj_0_False)
wenzelm@55793
   202
  }
wenzelm@55793
   203
  moreover {
wenzelm@55793
   204
    assume "x = 1"
wenzelm@44779
   205
    from 7 have "isnorm R" "isnorm P2"
wenzelm@44779
   206
      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@41807
   207
    with 7 `x = 1` have "isnorm (R \<oplus> P2)" by simp
wenzelm@44779
   208
    with 7 `x = 1` have ?case
wenzelm@55793
   209
      by (simp add: norm_PXtrans[of Q2 y _])
wenzelm@55793
   210
  }
wenzelm@55793
   211
  moreover {
wenzelm@55793
   212
    assume "x > 1" then have "\<exists>d. x=Suc (Suc d)" by arith
wenzelm@44779
   213
    then obtain d where X: "x=Suc (Suc d)" ..
wenzelm@41807
   214
    with 7 have NR: "isnorm R" "isnorm P2"
wenzelm@41807
   215
      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@41807
   216
    with 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
wenzelm@41807
   217
    with 7 X NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
wenzelm@44779
   218
    with `isnorm (PX Q2 y R)` X have ?case
wenzelm@55793
   219
      by (simp add: norm_PXtrans[of Q2 y _])
wenzelm@55793
   220
  }
chaieb@17378
   221
  ultimately show ?case by blast
chaieb@17378
   222
next
chaieb@17378
   223
  case (8 Q2 y R x P2)
haftmann@22742
   224
  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
wenzelm@55793
   225
  moreover {
wenzelm@55793
   226
    assume "x = 0"
wenzelm@55793
   227
    with 8 have ?case
wenzelm@55793
   228
      by (auto simp add: norm_Pinj_0_False)
wenzelm@55793
   229
  }
wenzelm@55793
   230
  moreover {
wenzelm@55793
   231
    assume "x = 1"
wenzelm@55793
   232
    with 8 have "isnorm R" "isnorm P2"
wenzelm@55793
   233
      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@55793
   234
    with 8 `x = 1` have "isnorm (R \<oplus> P2)"
wenzelm@55793
   235
      by simp
wenzelm@55793
   236
    with 8 `x = 1` have ?case
wenzelm@55793
   237
      by (simp add: norm_PXtrans[of Q2 y _])
wenzelm@55793
   238
  }
wenzelm@55793
   239
  moreover {
wenzelm@55793
   240
    assume "x > 1"
wenzelm@55793
   241
    then have "\<exists>d. x = Suc (Suc d)" by arith
wenzelm@41807
   242
    then obtain d where X: "x = Suc (Suc d)" ..
wenzelm@41807
   243
    with 8 have NR: "isnorm R" "isnorm P2"
wenzelm@41807
   244
      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@55793
   245
    with 8 X have "isnorm (Pinj (x - 1) P2)"
wenzelm@55793
   246
      by (cases P2) auto
wenzelm@55793
   247
    with 8 `x > 1` NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
wenzelm@55793
   248
      by simp
wenzelm@55793
   249
    with `isnorm (PX Q2 y R)` X have ?case
wenzelm@55793
   250
      by (simp add: norm_PXtrans[of Q2 y _])
wenzelm@55793
   251
  }
chaieb@17378
   252
  ultimately show ?case by blast
chaieb@17378
   253
next
chaieb@17378
   254
  case (9 P1 x P2 Q1 y Q2)
wenzelm@55793
   255
  then have Y0: "y > 0" by (cases y) auto
wenzelm@55793
   256
  with 9 have X0: "x > 0" by (cases x) auto
wenzelm@41807
   257
  with 9 have NP1: "isnorm P1" and NP2: "isnorm P2"
wenzelm@41807
   258
    by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])
wenzelm@44779
   259
  with 9 have NQ1: "isnorm Q1" and NQ2: "isnorm Q2"
wenzelm@41807
   260
    by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])
chaieb@17378
   261
  have "y < x \<or> x = y \<or> x < y" by arith
wenzelm@55793
   262
  moreover {
wenzelm@55793
   263
    assume sm1: "y < x"
wenzelm@55793
   264
    then have "\<exists>d. x = d + y" by arith
wenzelm@41807
   265
    then obtain d where sm2: "x = d + y" ..
wenzelm@41807
   266
    note 9 NQ1 NP1 NP2 NQ2 sm1 sm2
chaieb@17378
   267
    moreover
wenzelm@55793
   268
    have "isnorm (PX P1 d (Pc 0))"
wenzelm@41807
   269
    proof (cases P1)
chaieb@17378
   270
      case (PX p1 y p2)
wenzelm@55793
   271
      with 9 sm1 sm2 show ?thesis
wenzelm@55793
   272
        by (cases d) (simp, cases p2, auto)
wenzelm@41807
   273
    next
wenzelm@55793
   274
      case Pc
wenzelm@55793
   275
      with 9 sm1 sm2 show ?thesis
wenzelm@55793
   276
        by (cases d) auto
wenzelm@41807
   277
    next
wenzelm@55793
   278
      case Pinj
wenzelm@55793
   279
      with 9 sm1 sm2 show ?thesis
wenzelm@55793
   280
        by (cases d) auto
chaieb@17378
   281
    qed
wenzelm@55793
   282
    ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)"
wenzelm@55793
   283
      by auto
wenzelm@55793
   284
    with Y0 sm1 sm2 have ?case
wenzelm@55793
   285
      by (simp add: mkPX_cn)
wenzelm@55793
   286
  }
wenzelm@55793
   287
  moreover {
wenzelm@55793
   288
    assume "x = y"
wenzelm@55793
   289
    with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)"
wenzelm@55793
   290
      by auto
wenzelm@55793
   291
    with `x = y` Y0 have ?case
wenzelm@55793
   292
      by (simp add: mkPX_cn)
wenzelm@55793
   293
  }
wenzelm@55793
   294
  moreover {
wenzelm@55793
   295
    assume sm1: "x < y"
wenzelm@55793
   296
    then have "\<exists>d. y = d + x" by arith
wenzelm@41807
   297
    then obtain d where sm2: "y = d + x" ..
wenzelm@41807
   298
    note 9 NQ1 NP1 NP2 NQ2 sm1 sm2
chaieb@17378
   299
    moreover
wenzelm@55793
   300
    have "isnorm (PX Q1 d (Pc 0))"
wenzelm@41807
   301
    proof (cases Q1)
chaieb@17378
   302
      case (PX p1 y p2)
wenzelm@55793
   303
      with 9 sm1 sm2 show ?thesis
wenzelm@55793
   304
        by (cases d) (simp, cases p2, auto)
wenzelm@41807
   305
    next
wenzelm@55793
   306
      case Pc
wenzelm@55793
   307
      with 9 sm1 sm2 show ?thesis
wenzelm@55793
   308
        by (cases d) auto
wenzelm@41807
   309
    next
wenzelm@55793
   310
      case Pinj
wenzelm@55793
   311
      with 9 sm1 sm2 show ?thesis
wenzelm@55793
   312
        by (cases d) auto
chaieb@17378
   313
    qed
wenzelm@55793
   314
    ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)"
wenzelm@55793
   315
      by auto
wenzelm@55793
   316
    with X0 sm1 sm2 have ?case
wenzelm@55793
   317
      by (simp add: mkPX_cn)
wenzelm@55793
   318
  }
chaieb@17378
   319
  ultimately show ?case by blast
haftmann@22742
   320
qed simp
chaieb@17378
   321
haftmann@22742
   322
text {* mul concerves normalizedness *}
wenzelm@44779
   323
lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
wenzelm@44779
   324
proof (induct P Q rule: mul.induct)
wenzelm@55793
   325
  case (2 c i P2)
wenzelm@55793
   326
  then show ?case
wenzelm@44779
   327
    by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
chaieb@17378
   328
next
wenzelm@55793
   329
  case (3 i P2 c)
wenzelm@55793
   330
  then show ?case
wenzelm@44779
   331
    by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
chaieb@17378
   332
next
chaieb@17378
   333
  case (4 c P2 i Q2)
wenzelm@44779
   334
  then have "isnorm P2" "isnorm Q2"
wenzelm@44779
   335
    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
wenzelm@55793
   336
  with 4 show ?case
wenzelm@44779
   337
    by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
chaieb@17378
   338
next
chaieb@17378
   339
  case (5 P2 i Q2 c)
wenzelm@44779
   340
  then have "isnorm P2" "isnorm Q2"
wenzelm@44779
   341
    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
wenzelm@41807
   342
  with 5 show ?case
wenzelm@44779
   343
    by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
chaieb@17378
   344
next
chaieb@17378
   345
  case (6 x P2 y Q2)
chaieb@17378
   346
  have "x < y \<or> x = y \<or> x > y" by arith
wenzelm@55793
   347
  moreover {
wenzelm@55793
   348
    assume "x < y"
wenzelm@55793
   349
    then have "\<exists>d. y = d + x" by arith
wenzelm@41807
   350
    then obtain d where y: "y = d + x" ..
chaieb@17378
   351
    moreover
wenzelm@41807
   352
    note 6
chaieb@17378
   353
    moreover
wenzelm@55793
   354
    from 6 have "x > 0"
wenzelm@55793
   355
      by (cases x) (auto simp add: norm_Pinj_0_False)
chaieb@17378
   356
    moreover
wenzelm@55793
   357
    from 6 have "isnorm P2" "isnorm Q2"
wenzelm@55793
   358
      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
chaieb@17378
   359
    moreover
wenzelm@55793
   360
    from 6 `x < y` y have "isnorm (Pinj d Q2)"
wenzelm@55793
   361
      by (cases d) (simp, cases Q2, auto)
wenzelm@55793
   362
    ultimately have ?case by (simp add: mkPinj_cn)
wenzelm@55793
   363
  }
wenzelm@55793
   364
  moreover {
wenzelm@55793
   365
    assume "x = y"
chaieb@17378
   366
    moreover
wenzelm@55793
   367
    from 6 have "isnorm P2" "isnorm Q2"
wenzelm@55793
   368
      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
chaieb@17378
   369
    moreover
wenzelm@55793
   370
    from 6 have "y>0"
wenzelm@55793
   371
      by (cases y) (auto simp add: norm_Pinj_0_False)
chaieb@17378
   372
    moreover
wenzelm@41807
   373
    note 6
wenzelm@55793
   374
    ultimately have ?case by (simp add: mkPinj_cn)
wenzelm@55793
   375
  }
wenzelm@55793
   376
  moreover {
wenzelm@55793
   377
    assume "x > y"
wenzelm@55793
   378
    then have "\<exists>d. x = d + y" by arith
wenzelm@41807
   379
    then obtain d where x: "x = d + y" ..
chaieb@17378
   380
    moreover
wenzelm@41807
   381
    note 6
chaieb@17378
   382
    moreover
wenzelm@55793
   383
    from 6 have "y > 0"
wenzelm@55793
   384
      by (cases y) (auto simp add: norm_Pinj_0_False)
chaieb@17378
   385
    moreover
wenzelm@55793
   386
    from 6 have "isnorm P2" "isnorm Q2"
wenzelm@55793
   387
      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
chaieb@17378
   388
    moreover
wenzelm@55793
   389
    from 6 `x > y` x have "isnorm (Pinj d P2)"
wenzelm@55793
   390
      by (cases d) (simp, cases P2, auto)
wenzelm@55793
   391
    ultimately have ?case by (simp add: mkPinj_cn)
wenzelm@55793
   392
  }
chaieb@17378
   393
  ultimately show ?case by blast
chaieb@17378
   394
next
chaieb@17378
   395
  case (7 x P2 Q2 y R)
wenzelm@41807
   396
  then have Y0: "y > 0" by (cases y) auto
wenzelm@41807
   397
  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
wenzelm@55793
   398
  moreover {
wenzelm@55793
   399
    assume "x = 0"
wenzelm@55793
   400
    with 7 have ?case
wenzelm@55793
   401
      by (auto simp add: norm_Pinj_0_False)
wenzelm@55793
   402
  }
wenzelm@55793
   403
  moreover {
wenzelm@55793
   404
    assume "x = 1"
wenzelm@55793
   405
    from 7 have "isnorm R" "isnorm P2"
wenzelm@55793
   406
      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@55793
   407
    with 7 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2"
wenzelm@55793
   408
      by (auto simp add: norm_PX1[of Q2 y R])
wenzelm@55793
   409
    with 7 `x = 1` Y0 have ?case
wenzelm@55793
   410
      by (simp add: mkPX_cn)
wenzelm@55793
   411
  }
wenzelm@55793
   412
  moreover {
wenzelm@55793
   413
    assume "x > 1"
wenzelm@55793
   414
    then have "\<exists>d. x = Suc (Suc d)"
wenzelm@55793
   415
      by arith
wenzelm@41807
   416
    then obtain d where X: "x = Suc (Suc d)" ..
wenzelm@41807
   417
    from 7 have NR: "isnorm R" "isnorm Q2"
wenzelm@41807
   418
      by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
chaieb@17378
   419
    moreover
wenzelm@55793
   420
    from 7 X have "isnorm (Pinj (x - 1) P2)"
wenzelm@55793
   421
      by (cases P2) auto
wenzelm@41807
   422
    moreover
wenzelm@55793
   423
    from 7 have "isnorm (Pinj x P2)"
wenzelm@55793
   424
      by (cases P2) auto
chaieb@17378
   425
    moreover
wenzelm@41807
   426
    note 7 X
wenzelm@55793
   427
    ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)"
wenzelm@55793
   428
      by auto
wenzelm@55793
   429
    with Y0 X have ?case
wenzelm@55793
   430
      by (simp add: mkPX_cn)
wenzelm@55793
   431
  }
chaieb@17378
   432
  ultimately show ?case by blast
chaieb@17378
   433
next
chaieb@17378
   434
  case (8 Q2 y R x P2)
wenzelm@55793
   435
  then have Y0: "y > 0"
wenzelm@55793
   436
    by (cases y) auto
wenzelm@41807
   437
  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
wenzelm@55793
   438
  moreover {
wenzelm@55793
   439
    assume "x = 0"
wenzelm@55793
   440
    with 8 have ?case
wenzelm@55793
   441
      by (auto simp add: norm_Pinj_0_False)
wenzelm@55793
   442
  }
wenzelm@55793
   443
  moreover {
wenzelm@55793
   444
    assume "x = 1"
wenzelm@55793
   445
    from 8 have "isnorm R" "isnorm P2"
wenzelm@55793
   446
      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@55793
   447
    with 8 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2"
wenzelm@55793
   448
      by (auto simp add: norm_PX1[of Q2 y R])
wenzelm@55793
   449
    with 8 `x = 1` Y0 have ?case
wenzelm@55793
   450
      by (simp add: mkPX_cn)
wenzelm@55793
   451
  }
wenzelm@55793
   452
  moreover {
wenzelm@55793
   453
    assume "x > 1"
wenzelm@55793
   454
    then have "\<exists>d. x = Suc (Suc d)" by arith
wenzelm@41807
   455
    then obtain d where X: "x = Suc (Suc d)" ..
wenzelm@41807
   456
    from 8 have NR: "isnorm R" "isnorm Q2"
wenzelm@41807
   457
      by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
chaieb@17378
   458
    moreover
wenzelm@55793
   459
    from 8 X have "isnorm (Pinj (x - 1) P2)"
wenzelm@55793
   460
      by (cases P2) auto
chaieb@17378
   461
    moreover
wenzelm@55793
   462
    from 8 X have "isnorm (Pinj x P2)"
wenzelm@55793
   463
      by (cases P2) auto
chaieb@17378
   464
    moreover
wenzelm@41807
   465
    note 8 X
wenzelm@55793
   466
    ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)"
wenzelm@55793
   467
      by auto
wenzelm@55793
   468
    with Y0 X have ?case by (simp add: mkPX_cn)
wenzelm@55793
   469
  }
chaieb@17378
   470
  ultimately show ?case by blast
chaieb@17378
   471
next
chaieb@17378
   472
  case (9 P1 x P2 Q1 y Q2)
wenzelm@41807
   473
  from 9 have X0: "x > 0" by (cases x) auto
wenzelm@41807
   474
  from 9 have Y0: "y > 0" by (cases y) auto
wenzelm@41807
   475
  note 9
chaieb@17378
   476
  moreover
wenzelm@55793
   477
  from 9 have "isnorm P1" "isnorm P2"
wenzelm@55793
   478
    by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
wenzelm@55793
   479
  moreover
wenzelm@55793
   480
  from 9 have "isnorm Q1" "isnorm Q2"
wenzelm@55793
   481
    by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2])
haftmann@22742
   482
  ultimately have "isnorm (P1 \<otimes> Q1)" "isnorm (P2 \<otimes> Q2)"
wenzelm@55793
   483
    "isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)"
chaieb@17378
   484
    by (auto simp add: mkPinj_cn)
wenzelm@41807
   485
  with 9 X0 Y0 have
haftmann@22742
   486
    "isnorm (mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2))"
wenzelm@55793
   487
    "isnorm (mkPX (P1 \<otimes> mkPinj (Suc 0) Q2) x (Pc 0))"
wenzelm@55793
   488
    "isnorm (mkPX (Q1 \<otimes> mkPinj (Suc 0) P2) y (Pc 0))"
chaieb@17378
   489
    by (auto simp add: mkPX_cn)
wenzelm@55754
   490
  then show ?case by (simp add: add_cn)
wenzelm@41807
   491
qed simp
chaieb@17378
   492
haftmann@22742
   493
text {* neg conserves normalizedness *}
chaieb@17378
   494
lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"
haftmann@22742
   495
proof (induct P)
chaieb@17378
   496
  case (Pinj i P2)
wenzelm@55793
   497
  then have "isnorm P2"
wenzelm@55793
   498
    by (simp add: norm_Pinj[of i P2])
wenzelm@55793
   499
  with Pinj show ?case
wenzelm@55793
   500
    by (cases P2) (auto, cases i, auto)
chaieb@17378
   501
next
wenzelm@41807
   502
  case (PX P1 x P2) note PX1 = this
wenzelm@41807
   503
  from PX have "isnorm P2" "isnorm P1"
wenzelm@41807
   504
    by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
wenzelm@41807
   505
  with PX show ?case
wenzelm@41807
   506
  proof (cases P1)
chaieb@17378
   507
    case (PX p1 y p2)
wenzelm@55793
   508
    with PX1 show ?thesis
wenzelm@55793
   509
      by (cases x) (auto, cases p2, auto)
chaieb@17378
   510
  next
chaieb@17378
   511
    case Pinj
wenzelm@55793
   512
    with PX1 show ?thesis
wenzelm@55793
   513
      by (cases x) auto
wenzelm@41807
   514
  qed (cases x, auto)
wenzelm@41807
   515
qed simp
chaieb@17378
   516
haftmann@22742
   517
text {* sub conserves normalizedness *}
wenzelm@44779
   518
lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
wenzelm@44779
   519
  by (simp add: sub_def add_cn neg_cn)
chaieb@17378
   520
haftmann@22742
   521
text {* sqr conserves normalizizedness *}
wenzelm@44779
   522
lemma sqr_cn: "isnorm P \<Longrightarrow> isnorm (sqr P)"
wenzelm@41807
   523
proof (induct P)
wenzelm@44779
   524
  case Pc
wenzelm@44779
   525
  then show ?case by simp
wenzelm@44779
   526
next
chaieb@17378
   527
  case (Pinj i Q)
wenzelm@41807
   528
  then show ?case
wenzelm@44779
   529
    by (cases Q) (auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
wenzelm@55793
   530
next
chaieb@17378
   531
  case (PX P1 x P2)
wenzelm@55754
   532
  then have "x + x \<noteq> 0" "isnorm P2" "isnorm P1"
wenzelm@41807
   533
    by (cases x, auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
wenzelm@41807
   534
  with PX have "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))"
wenzelm@41807
   535
      and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
wenzelm@41807
   536
    by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
wenzelm@55793
   537
  then show ?case
wenzelm@55793
   538
    by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
wenzelm@44779
   539
qed
chaieb@17378
   540
haftmann@22742
   541
text {* pow conserves normalizedness *}
wenzelm@44779
   542
lemma pow_cn: "isnorm P \<Longrightarrow> isnorm (pow n P)"
wenzelm@44779
   543
proof (induct n arbitrary: P rule: less_induct)
wenzelm@44779
   544
  case (less k)
wenzelm@55793
   545
  show ?case
wenzelm@41807
   546
  proof (cases "k = 0")
wenzelm@44779
   547
    case True
wenzelm@44779
   548
    then show ?thesis by simp
wenzelm@44779
   549
  next
chaieb@17378
   550
    case False
wenzelm@41807
   551
    then have K2: "k div 2 < k" by (cases k) auto
wenzelm@44779
   552
    from less have "isnorm (sqr P)" by (simp add: sqr_cn)
wenzelm@44779
   553
    with less False K2 show ?thesis
wenzelm@44779
   554
      by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
wenzelm@44779
   555
  qed
chaieb@17378
   556
qed
chaieb@17378
   557
wenzelm@17388
   558
end