src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
author nipkow
Tue Feb 23 16:25:08 2016 +0100 (2016-02-23)
changeset 62390 842917225d56
parent 61586 5197a2ecb658
child 64962 bf41e1109db3
permissions -rw-r--r--
more canonical names
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@60533
     8
section \<open>Proof of the relative completeness of method comm-ring\<close>
chaieb@17378
     9
chaieb@17378
    10
theory Commutative_Ring_Complete
wenzelm@17508
    11
imports Commutative_Ring
chaieb@17378
    12
begin
haftmann@22742
    13
wenzelm@60533
    14
text \<open>Formalization of normal form\<close>
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@60708
    42
  subgoal for \<dots> pol2 by (cases pol2) auto
wenzelm@55754
    43
  done
wenzelm@44779
    44
wenzelm@44779
    45
lemma norm_PX1: "isnorm (PX P i Q) \<Longrightarrow> isnorm P"
wenzelm@55754
    46
  apply (cases i)
wenzelm@55754
    47
  apply auto
wenzelm@55754
    48
  apply (cases P)
wenzelm@55754
    49
  apply auto
wenzelm@60708
    50
  subgoal for \<dots> pol2 by (cases pol2) auto
wenzelm@55754
    51
  done
chaieb@17378
    52
wenzelm@55754
    53
lemma mkPinj_cn: "y \<noteq> 0 \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (mkPinj y Q)"
wenzelm@44779
    54
  apply (auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split)
blanchet@58259
    55
  apply (rename_tac nat a, case_tac nat, auto simp add: norm_Pinj_0_False)
blanchet@58259
    56
  apply (rename_tac pol a, case_tac pol, auto)
wenzelm@44779
    57
  apply (case_tac y, auto)
wenzelm@44779
    58
  done
chaieb@17378
    59
wenzelm@55793
    60
lemma norm_PXtrans:
wenzelm@55754
    61
  assumes A: "isnorm (PX P x Q)"
wenzelm@55793
    62
    and "isnorm Q2"
chaieb@17378
    63
  shows "isnorm (PX P x Q2)"
wenzelm@44779
    64
proof (cases P)
wenzelm@44779
    65
  case (PX p1 y p2)
wenzelm@55754
    66
  with assms show ?thesis
wenzelm@55754
    67
    apply (cases x)
wenzelm@55754
    68
    apply auto
wenzelm@55754
    69
    apply (cases p2)
wenzelm@55754
    70
    apply auto
wenzelm@55754
    71
    done
chaieb@17378
    72
next
wenzelm@44779
    73
  case Pc
wenzelm@60535
    74
  with assms show ?thesis
wenzelm@60535
    75
    by (cases x) auto
chaieb@17378
    76
next
wenzelm@44779
    77
  case Pinj
wenzelm@60535
    78
  with assms show ?thesis
wenzelm@60535
    79
    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@61586
   104
text \<open>mkPX conserves normalizedness (\<open>_cn\<close>)\<close>
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@60535
   125
    apply (cases x)
wenzelm@60535
   126
    apply (auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _])
wenzelm@60535
   127
    apply (cases P2)
wenzelm@60535
   128
    apply auto
wenzelm@60535
   129
    done
chaieb@17378
   130
qed
chaieb@17378
   131
wenzelm@60533
   132
text \<open>add conserves normalizedness\<close>
wenzelm@44779
   133
lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
wenzelm@44779
   134
proof (induct P Q rule: add.induct)
wenzelm@60535
   135
  case 1
wenzelm@60535
   136
  then show ?case by simp
wenzelm@60535
   137
next
wenzelm@44779
   138
  case (2 c i P2)
wenzelm@55793
   139
  then show ?case
wenzelm@60535
   140
    apply (cases P2)
wenzelm@60535
   141
    apply simp_all
wenzelm@60535
   142
    apply (cases i)
wenzelm@60535
   143
    apply simp_all
wenzelm@60535
   144
    done
chaieb@17378
   145
next
wenzelm@44779
   146
  case (3 i P2 c)
wenzelm@55793
   147
  then show ?case
wenzelm@60535
   148
    apply (cases P2)
wenzelm@60535
   149
    apply simp_all
wenzelm@60535
   150
    apply (cases i)
wenzelm@60535
   151
    apply simp_all
wenzelm@60535
   152
    done
chaieb@17378
   153
next
chaieb@17378
   154
  case (4 c P2 i Q2)
wenzelm@44779
   155
  then have "isnorm P2" "isnorm Q2"
wenzelm@44779
   156
    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
wenzelm@44779
   157
  with 4 show ?case
wenzelm@60535
   158
    apply (cases i)
wenzelm@60535
   159
    apply simp
wenzelm@60535
   160
    apply (cases P2)
wenzelm@60535
   161
    apply auto
wenzelm@60708
   162
    subgoal for \<dots> pol2 by (cases pol2) auto
wenzelm@60535
   163
    done
chaieb@17378
   164
next
chaieb@17378
   165
  case (5 P2 i Q2 c)
wenzelm@44779
   166
  then have "isnorm P2" "isnorm Q2"
wenzelm@44779
   167
    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
wenzelm@44779
   168
  with 5 show ?case
wenzelm@60535
   169
    apply (cases i)
wenzelm@60535
   170
    apply simp
wenzelm@60535
   171
    apply (cases P2)
wenzelm@60535
   172
    apply auto
wenzelm@60708
   173
    subgoal for \<dots> pol2 by (cases pol2) auto
wenzelm@60535
   174
    done
chaieb@17378
   175
next
chaieb@17378
   176
  case (6 x P2 y Q2)
wenzelm@55793
   177
  then have Y0: "y > 0"
wenzelm@55793
   178
    by (cases y) (auto simp add: norm_Pinj_0_False)
wenzelm@55793
   179
  with 6 have X0: "x > 0"
wenzelm@55793
   180
    by (cases x) (auto simp add: norm_Pinj_0_False)
wenzelm@60535
   181
  consider "x < y" | "x = y" | "x > y" by arith
wenzelm@60535
   182
  then show ?case
wenzelm@60535
   183
  proof cases
wenzelm@60567
   184
    case xy: 1
wenzelm@60535
   185
    then obtain d where y: "y = d + x"
wenzelm@60535
   186
      by atomize_elim arith
wenzelm@60535
   187
    from 6 have *: "isnorm P2" "isnorm Q2"
wenzelm@44779
   188
      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
wenzelm@60567
   189
    from 6 xy y have "isnorm (Pinj d Q2)"
wenzelm@44779
   190
      by (cases d, simp, cases Q2, auto)
wenzelm@60535
   191
    with 6 X0 y * show ?thesis
wenzelm@60535
   192
      by (simp add: mkPinj_cn)
wenzelm@60535
   193
  next
wenzelm@60567
   194
    case xy: 2
wenzelm@44779
   195
    from 6 have "isnorm P2" "isnorm Q2"
wenzelm@44779
   196
      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
wenzelm@60567
   197
    with xy 6 Y0 show ?thesis
wenzelm@60535
   198
      by (simp add: mkPinj_cn)
wenzelm@60535
   199
  next
wenzelm@60567
   200
    case xy: 3
wenzelm@60535
   201
    then obtain d where x: "x = d + y"
wenzelm@60535
   202
      by atomize_elim arith
wenzelm@60535
   203
    from 6 have *: "isnorm P2" "isnorm Q2"
wenzelm@44779
   204
      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
wenzelm@60567
   205
    from 6 xy x have "isnorm (Pinj d P2)"
wenzelm@44779
   206
      by (cases d) (simp, cases P2, auto)
wenzelm@60567
   207
    with xy 6 Y0 * x show ?thesis by (simp add: mkPinj_cn)
wenzelm@60535
   208
  qed
chaieb@17378
   209
next
chaieb@17378
   210
  case (7 x P2 Q2 y R)
wenzelm@60535
   211
  consider "x = 0" | "x = 1" | d where "x = Suc (Suc d)"
wenzelm@60535
   212
    by atomize_elim arith
wenzelm@60535
   213
  then show ?case
wenzelm@60535
   214
  proof cases
wenzelm@60767
   215
    case 1
wenzelm@60535
   216
    with 7 show ?thesis
wenzelm@60535
   217
      by (auto simp add: norm_Pinj_0_False)
wenzelm@60535
   218
  next
wenzelm@60567
   219
    case x: 2
wenzelm@44779
   220
    from 7 have "isnorm R" "isnorm P2"
wenzelm@44779
   221
      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@60567
   222
    with 7 x have "isnorm (R \<oplus> P2)"
wenzelm@60535
   223
      by simp
wenzelm@60567
   224
    with 7 x show ?thesis
wenzelm@55793
   225
      by (simp add: norm_PXtrans[of Q2 y _])
wenzelm@60535
   226
  next
wenzelm@60567
   227
    case x: 3
wenzelm@41807
   228
    with 7 have NR: "isnorm R" "isnorm P2"
wenzelm@41807
   229
      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@60567
   230
    with 7 x have "isnorm (Pinj (x - 1) P2)"
wenzelm@60535
   231
      by (cases P2) auto
wenzelm@60567
   232
    with 7 x NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
wenzelm@60535
   233
      by simp
wenzelm@60567
   234
    with \<open>isnorm (PX Q2 y R)\<close> x show ?thesis
wenzelm@55793
   235
      by (simp add: norm_PXtrans[of Q2 y _])
wenzelm@60535
   236
  qed
chaieb@17378
   237
next
chaieb@17378
   238
  case (8 Q2 y R x P2)
wenzelm@60535
   239
  consider "x = 0" | "x = 1" | "x > 1"
wenzelm@60535
   240
    by arith
wenzelm@60535
   241
  then show ?case
wenzelm@60535
   242
  proof cases
wenzelm@60535
   243
    case 1
wenzelm@60535
   244
    with 8 show ?thesis
wenzelm@55793
   245
      by (auto simp add: norm_Pinj_0_False)
wenzelm@60535
   246
  next
wenzelm@60567
   247
    case x: 2
wenzelm@55793
   248
    with 8 have "isnorm R" "isnorm P2"
wenzelm@55793
   249
      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@60567
   250
    with 8 x have "isnorm (R \<oplus> P2)"
wenzelm@55793
   251
      by simp
wenzelm@60567
   252
    with 8 x show ?thesis
wenzelm@55793
   253
      by (simp add: norm_PXtrans[of Q2 y _])
wenzelm@60535
   254
  next
wenzelm@60567
   255
    case x: 3
wenzelm@60535
   256
    then obtain d where x: "x = Suc (Suc d)" by atomize_elim arith
wenzelm@41807
   257
    with 8 have NR: "isnorm R" "isnorm P2"
wenzelm@41807
   258
      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@60535
   259
    with 8 x have "isnorm (Pinj (x - 1) P2)"
wenzelm@55793
   260
      by (cases P2) auto
wenzelm@60567
   261
    with 8 x NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
wenzelm@55793
   262
      by simp
wenzelm@60535
   263
    with \<open>isnorm (PX Q2 y R)\<close> x show ?thesis
wenzelm@55793
   264
      by (simp add: norm_PXtrans[of Q2 y _])
wenzelm@60535
   265
  qed
chaieb@17378
   266
next
chaieb@17378
   267
  case (9 P1 x P2 Q1 y Q2)
wenzelm@55793
   268
  then have Y0: "y > 0" by (cases y) auto
wenzelm@55793
   269
  with 9 have X0: "x > 0" by (cases x) auto
wenzelm@41807
   270
  with 9 have NP1: "isnorm P1" and NP2: "isnorm P2"
wenzelm@41807
   271
    by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])
wenzelm@44779
   272
  with 9 have NQ1: "isnorm Q1" and NQ2: "isnorm Q2"
wenzelm@41807
   273
    by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])
wenzelm@60535
   274
  consider "y < x" | "x = y" | "x < y" by arith
wenzelm@60535
   275
  then show ?case
wenzelm@60535
   276
  proof cases
wenzelm@60567
   277
    case xy: 1
wenzelm@60535
   278
    then obtain d where x: "x = d + y"
wenzelm@60535
   279
      by atomize_elim arith
wenzelm@55793
   280
    have "isnorm (PX P1 d (Pc 0))"
wenzelm@41807
   281
    proof (cases P1)
chaieb@17378
   282
      case (PX p1 y p2)
wenzelm@60567
   283
      with 9 xy x show ?thesis
wenzelm@55793
   284
        by (cases d) (simp, cases p2, auto)
wenzelm@41807
   285
    next
wenzelm@55793
   286
      case Pc
wenzelm@60567
   287
      with 9 xy x show ?thesis
wenzelm@55793
   288
        by (cases d) auto
wenzelm@41807
   289
    next
wenzelm@55793
   290
      case Pinj
wenzelm@60567
   291
      with 9 xy x show ?thesis
wenzelm@55793
   292
        by (cases d) auto
chaieb@17378
   293
    qed
wenzelm@60567
   294
    with 9 NQ1 NP1 NP2 NQ2 xy x have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)"
wenzelm@55793
   295
      by auto
wenzelm@60567
   296
    with Y0 xy x show ?thesis
wenzelm@55793
   297
      by (simp add: mkPX_cn)
wenzelm@60535
   298
  next
wenzelm@60567
   299
    case xy: 2
wenzelm@55793
   300
    with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)"
wenzelm@55793
   301
      by auto
wenzelm@60567
   302
    with xy Y0 show ?thesis
wenzelm@55793
   303
      by (simp add: mkPX_cn)
wenzelm@60535
   304
  next
wenzelm@60567
   305
    case xy: 3
wenzelm@60535
   306
    then obtain d where y: "y = d + x"
wenzelm@60535
   307
      by atomize_elim arith
wenzelm@55793
   308
    have "isnorm (PX Q1 d (Pc 0))"
wenzelm@41807
   309
    proof (cases Q1)
chaieb@17378
   310
      case (PX p1 y p2)
wenzelm@60567
   311
      with 9 xy y show ?thesis
wenzelm@55793
   312
        by (cases d) (simp, cases p2, auto)
wenzelm@41807
   313
    next
wenzelm@55793
   314
      case Pc
wenzelm@60567
   315
      with 9 xy y show ?thesis
wenzelm@55793
   316
        by (cases d) auto
wenzelm@41807
   317
    next
wenzelm@55793
   318
      case Pinj
wenzelm@60567
   319
      with 9 xy y show ?thesis
wenzelm@55793
   320
        by (cases d) auto
chaieb@17378
   321
    qed
wenzelm@60567
   322
    with 9 NQ1 NP1 NP2 NQ2 xy y have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)"
wenzelm@55793
   323
      by auto
wenzelm@60567
   324
    with X0 xy y show ?thesis
wenzelm@55793
   325
      by (simp add: mkPX_cn)
wenzelm@60535
   326
  qed
wenzelm@60535
   327
qed
chaieb@17378
   328
wenzelm@60533
   329
text \<open>mul concerves normalizedness\<close>
wenzelm@44779
   330
lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
wenzelm@44779
   331
proof (induct P Q rule: mul.induct)
wenzelm@60535
   332
  case 1
wenzelm@60535
   333
  then show ?case by simp
wenzelm@60535
   334
next
wenzelm@55793
   335
  case (2 c i P2)
wenzelm@55793
   336
  then show ?case
wenzelm@60535
   337
    apply (cases P2)
wenzelm@60535
   338
    apply simp_all
wenzelm@60535
   339
    apply (cases i)
wenzelm@60535
   340
    apply (simp_all add: mkPinj_cn)
wenzelm@60535
   341
    done
chaieb@17378
   342
next
wenzelm@55793
   343
  case (3 i P2 c)
wenzelm@55793
   344
  then show ?case
wenzelm@60535
   345
    apply (cases P2)
wenzelm@60535
   346
    apply simp_all
wenzelm@60535
   347
    apply (cases i)
wenzelm@60535
   348
    apply (simp_all add: mkPinj_cn)
wenzelm@60535
   349
    done
chaieb@17378
   350
next
chaieb@17378
   351
  case (4 c P2 i Q2)
wenzelm@44779
   352
  then have "isnorm P2" "isnorm Q2"
wenzelm@44779
   353
    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
wenzelm@55793
   354
  with 4 show ?case
wenzelm@60535
   355
    apply (cases "c = 0")
wenzelm@60535
   356
    apply simp_all
wenzelm@60535
   357
    apply (cases "i = 0")
wenzelm@60535
   358
    apply (simp_all add: mkPX_cn)
wenzelm@60535
   359
    done
chaieb@17378
   360
next
chaieb@17378
   361
  case (5 P2 i Q2 c)
wenzelm@44779
   362
  then have "isnorm P2" "isnorm Q2"
wenzelm@44779
   363
    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
wenzelm@41807
   364
  with 5 show ?case
wenzelm@60535
   365
    apply (cases "c = 0")
wenzelm@60535
   366
    apply simp_all
wenzelm@60535
   367
    apply (cases "i = 0")
wenzelm@60535
   368
    apply (simp_all add: mkPX_cn)
wenzelm@60535
   369
    done
chaieb@17378
   370
next
chaieb@17378
   371
  case (6 x P2 y Q2)
wenzelm@60535
   372
  consider "x < y" | "x = y" | "x > y" by arith
wenzelm@60535
   373
  then show ?case
wenzelm@60535
   374
  proof cases
wenzelm@60567
   375
    case xy: 1
wenzelm@60535
   376
    then obtain d where y: "y = d + x"
wenzelm@60535
   377
      by atomize_elim arith
wenzelm@60535
   378
    from 6 have *: "x > 0"
wenzelm@55793
   379
      by (cases x) (auto simp add: norm_Pinj_0_False)
wenzelm@60535
   380
    from 6 have **: "isnorm P2" "isnorm Q2"
wenzelm@55793
   381
      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
wenzelm@60567
   382
    from 6 xy y have "isnorm (Pinj d Q2)"
wenzelm@60535
   383
      apply (cases d)
wenzelm@60535
   384
      apply simp
wenzelm@60535
   385
      apply (cases Q2)
wenzelm@60535
   386
      apply auto
wenzelm@60535
   387
      done
wenzelm@60535
   388
    with 6 * ** y show ?thesis
wenzelm@60535
   389
      by (simp add: mkPinj_cn)
wenzelm@60535
   390
  next
wenzelm@60567
   391
    case xy: 2
wenzelm@60535
   392
    from 6 have *: "isnorm P2" "isnorm Q2"
wenzelm@55793
   393
      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
wenzelm@60535
   394
    from 6 have **: "y > 0"
wenzelm@60535
   395
      by (cases y) (auto simp add: norm_Pinj_0_False)
wenzelm@60567
   396
    with 6 xy * ** show ?thesis
wenzelm@60535
   397
      by (simp add: mkPinj_cn)
wenzelm@60535
   398
  next
wenzelm@60567
   399
    case xy: 3
wenzelm@60535
   400
    then obtain d where x: "x = d + y"
wenzelm@60535
   401
      by atomize_elim arith
wenzelm@60535
   402
    from 6 have *: "y > 0"
wenzelm@55793
   403
      by (cases y) (auto simp add: norm_Pinj_0_False)
wenzelm@60535
   404
    from 6 have **: "isnorm P2" "isnorm Q2"
wenzelm@55793
   405
      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
wenzelm@60567
   406
    from 6 xy x have "isnorm (Pinj d P2)"
wenzelm@60535
   407
      apply (cases d)
wenzelm@60535
   408
      apply simp
wenzelm@60535
   409
      apply (cases P2)
wenzelm@60535
   410
      apply auto
wenzelm@60535
   411
      done
wenzelm@60567
   412
    with 6 xy * ** x show ?thesis
wenzelm@60535
   413
      by (simp add: mkPinj_cn)
wenzelm@60535
   414
  qed
chaieb@17378
   415
next
chaieb@17378
   416
  case (7 x P2 Q2 y R)
wenzelm@41807
   417
  then have Y0: "y > 0" by (cases y) auto
wenzelm@60535
   418
  consider "x = 0" | "x = 1" | d where "x = Suc (Suc d)"
wenzelm@60535
   419
    by atomize_elim arith
wenzelm@60535
   420
  then show ?case
wenzelm@60535
   421
  proof cases
wenzelm@60535
   422
    case 1
wenzelm@60535
   423
    with 7 show ?thesis
wenzelm@55793
   424
      by (auto simp add: norm_Pinj_0_False)
wenzelm@60535
   425
  next
wenzelm@60567
   426
    case x: 2
wenzelm@55793
   427
    from 7 have "isnorm R" "isnorm P2"
wenzelm@55793
   428
      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@60567
   429
    with 7 x have "isnorm (R \<otimes> P2)" "isnorm Q2"
wenzelm@55793
   430
      by (auto simp add: norm_PX1[of Q2 y R])
wenzelm@60567
   431
    with 7 x Y0 show ?thesis
wenzelm@55793
   432
      by (simp add: mkPX_cn)
wenzelm@60535
   433
  next
wenzelm@60567
   434
    case x: 3
wenzelm@60535
   435
    from 7 have *: "isnorm R" "isnorm Q2"
wenzelm@41807
   436
      by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
wenzelm@60567
   437
    from 7 x have "isnorm (Pinj (x - 1) P2)"
wenzelm@55793
   438
      by (cases P2) auto
wenzelm@60567
   439
    with 7 x * have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)"
wenzelm@55793
   440
      by auto
wenzelm@60567
   441
    with Y0 x show ?thesis
wenzelm@55793
   442
      by (simp add: mkPX_cn)
wenzelm@60535
   443
  qed
chaieb@17378
   444
next
chaieb@17378
   445
  case (8 Q2 y R x P2)
wenzelm@55793
   446
  then have Y0: "y > 0"
wenzelm@55793
   447
    by (cases y) auto
wenzelm@60535
   448
  consider "x = 0" | "x = 1" | d where "x = Suc (Suc d)"
wenzelm@60535
   449
    by atomize_elim arith
wenzelm@60535
   450
  then show ?case
wenzelm@60535
   451
  proof cases
wenzelm@60535
   452
    case 1
wenzelm@60535
   453
    with 8 show ?thesis
wenzelm@55793
   454
      by (auto simp add: norm_Pinj_0_False)
wenzelm@60535
   455
  next
wenzelm@60567
   456
    case x: 2
wenzelm@55793
   457
    from 8 have "isnorm R" "isnorm P2"
wenzelm@55793
   458
      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@60567
   459
    with 8 x have "isnorm (R \<otimes> P2)" "isnorm Q2"
wenzelm@55793
   460
      by (auto simp add: norm_PX1[of Q2 y R])
wenzelm@60567
   461
    with 8 x Y0 show ?thesis
wenzelm@55793
   462
      by (simp add: mkPX_cn)
wenzelm@60535
   463
  next
wenzelm@60567
   464
    case x: 3
wenzelm@60535
   465
    from 8 have *: "isnorm R" "isnorm Q2"
wenzelm@41807
   466
      by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
wenzelm@60567
   467
    from 8 x have "isnorm (Pinj (x - 1) P2)"
wenzelm@55793
   468
      by (cases P2) auto
wenzelm@60567
   469
    with 8 x * have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)"
wenzelm@55793
   470
      by auto
wenzelm@60567
   471
    with Y0 x show ?thesis
wenzelm@60535
   472
      by (simp add: mkPX_cn)
wenzelm@60535
   473
  qed
chaieb@17378
   474
next
chaieb@17378
   475
  case (9 P1 x P2 Q1 y Q2)
wenzelm@41807
   476
  from 9 have X0: "x > 0" by (cases x) auto
wenzelm@41807
   477
  from 9 have Y0: "y > 0" by (cases y) auto
wenzelm@60535
   478
  from 9 have *: "isnorm P1" "isnorm P2"
wenzelm@55793
   479
    by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
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])
wenzelm@60535
   482
  with 9 * 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@60535
   490
  then show ?case
wenzelm@60535
   491
    by (simp add: add_cn)
wenzelm@60535
   492
qed
chaieb@17378
   493
wenzelm@60533
   494
text \<open>neg conserves normalizedness\<close>
chaieb@17378
   495
lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"
haftmann@22742
   496
proof (induct P)
wenzelm@60535
   497
  case Pc
wenzelm@60535
   498
  then show ?case by simp
wenzelm@60535
   499
next
chaieb@17378
   500
  case (Pinj i P2)
wenzelm@55793
   501
  then have "isnorm P2"
wenzelm@55793
   502
    by (simp add: norm_Pinj[of i P2])
wenzelm@55793
   503
  with Pinj show ?case
wenzelm@55793
   504
    by (cases P2) (auto, cases i, auto)
chaieb@17378
   505
next
wenzelm@41807
   506
  case (PX P1 x P2) note PX1 = this
wenzelm@41807
   507
  from PX have "isnorm P2" "isnorm P1"
wenzelm@41807
   508
    by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
wenzelm@41807
   509
  with PX show ?case
wenzelm@41807
   510
  proof (cases P1)
chaieb@17378
   511
    case (PX p1 y p2)
wenzelm@55793
   512
    with PX1 show ?thesis
wenzelm@55793
   513
      by (cases x) (auto, cases p2, auto)
chaieb@17378
   514
  next
chaieb@17378
   515
    case Pinj
wenzelm@55793
   516
    with PX1 show ?thesis
wenzelm@55793
   517
      by (cases x) auto
wenzelm@41807
   518
  qed (cases x, auto)
wenzelm@60535
   519
qed
chaieb@17378
   520
wenzelm@60533
   521
text \<open>sub conserves normalizedness\<close>
wenzelm@44779
   522
lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
wenzelm@44779
   523
  by (simp add: sub_def add_cn neg_cn)
chaieb@17378
   524
wenzelm@60533
   525
text \<open>sqr conserves normalizizedness\<close>
wenzelm@44779
   526
lemma sqr_cn: "isnorm P \<Longrightarrow> isnorm (sqr P)"
wenzelm@41807
   527
proof (induct P)
wenzelm@44779
   528
  case Pc
wenzelm@44779
   529
  then show ?case by simp
wenzelm@44779
   530
next
chaieb@17378
   531
  case (Pinj i Q)
wenzelm@41807
   532
  then show ?case
wenzelm@60535
   533
    apply (cases Q)
wenzelm@60535
   534
    apply (auto simp add: mkPX_cn mkPinj_cn)
wenzelm@60535
   535
    apply (cases i)
wenzelm@60535
   536
    apply (auto simp add: mkPX_cn mkPinj_cn)
wenzelm@60535
   537
    done
wenzelm@55793
   538
next
chaieb@17378
   539
  case (PX P1 x P2)
wenzelm@55754
   540
  then have "x + x \<noteq> 0" "isnorm P2" "isnorm P1"
wenzelm@60535
   541
    apply (cases x)
wenzelm@60535
   542
    using PX
wenzelm@60535
   543
    apply (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
wenzelm@60535
   544
    done
wenzelm@41807
   545
  with PX have "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))"
wenzelm@60535
   546
    and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
wenzelm@41807
   547
    by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
wenzelm@55793
   548
  then show ?case
wenzelm@55793
   549
    by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
wenzelm@44779
   550
qed
chaieb@17378
   551
wenzelm@60533
   552
text \<open>pow conserves normalizedness\<close>
wenzelm@44779
   553
lemma pow_cn: "isnorm P \<Longrightarrow> isnorm (pow n P)"
wenzelm@44779
   554
proof (induct n arbitrary: P rule: less_induct)
wenzelm@44779
   555
  case (less k)
wenzelm@55793
   556
  show ?case
wenzelm@41807
   557
  proof (cases "k = 0")
wenzelm@44779
   558
    case True
wenzelm@44779
   559
    then show ?thesis by simp
wenzelm@44779
   560
  next
chaieb@17378
   561
    case False
wenzelm@60535
   562
    then have K2: "k div 2 < k"
wenzelm@60535
   563
      by (cases k) auto
wenzelm@60535
   564
    from less have "isnorm (sqr P)"
wenzelm@60535
   565
      by (simp add: sqr_cn)
wenzelm@44779
   566
    with less False K2 show ?thesis
haftmann@58712
   567
      by (cases "even k") (auto simp add: mul_cn elim: evenE oddE)
wenzelm@44779
   568
  qed
chaieb@17378
   569
qed
chaieb@17378
   570
wenzelm@17388
   571
end