src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
author wenzelm
Tue Feb 25 23:12:48 2014 +0100 (2014-02-25)
changeset 55754 d14072d53c1e
parent 53374 a14d2a854c02
child 55793 52c8f934ea6f
permissions -rw-r--r--
tuned specifications and 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
chaieb@17378
    62
lemma norm_PXtrans: 
wenzelm@55754
    63
  assumes A: "isnorm (PX P x Q)"
wenzelm@55754
    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@41807
    82
lemma norm_PXtrans2:
wenzelm@41807
    83
  assumes "isnorm (PX P x Q)" and "isnorm Q2"
wenzelm@55754
    84
  shows "isnorm (PX P (Suc (n + x)) Q2)"
wenzelm@41807
    85
proof (cases P)
chaieb@17378
    86
  case (PX p1 y p2)
wenzelm@55754
    87
  with assms show ?thesis
wenzelm@55754
    88
    apply (cases x)
wenzelm@55754
    89
    apply auto
wenzelm@55754
    90
    apply (cases p2)
wenzelm@55754
    91
    apply auto
wenzelm@55754
    92
    done
chaieb@17378
    93
next
chaieb@17378
    94
  case Pc
wenzelm@41807
    95
  with assms show ?thesis by (cases x) auto
chaieb@17378
    96
next
chaieb@17378
    97
  case Pinj
wenzelm@41807
    98
  with assms show ?thesis by (cases x) auto
chaieb@17378
    99
qed
chaieb@17378
   100
wenzelm@23266
   101
text {* mkPX conserves normalizedness (@{text "_cn"}) *}
chaieb@17378
   102
lemma mkPX_cn: 
wenzelm@55754
   103
  assumes "x \<noteq> 0"
wenzelm@55754
   104
    and "isnorm P"
wenzelm@55754
   105
    and "isnorm Q" 
chaieb@17378
   106
  shows "isnorm (mkPX P x Q)"
wenzelm@55754
   107
proof (cases P)
chaieb@17378
   108
  case (Pc c)
wenzelm@55754
   109
  with assms show ?thesis
wenzelm@55754
   110
    by (cases x) (auto simp add: mkPinj_cn mkPX_def)
chaieb@17378
   111
next
chaieb@17378
   112
  case (Pinj i Q)
wenzelm@55754
   113
  with assms show ?thesis
wenzelm@55754
   114
    by (cases x) (auto simp add: mkPinj_cn mkPX_def)
chaieb@17378
   115
next
chaieb@17378
   116
  case (PX P1 y P2)
wenzelm@44779
   117
  with assms have Y0: "y > 0" by (cases y) auto
wenzelm@41807
   118
  from assms PX have "isnorm P1" "isnorm P2"
wenzelm@41807
   119
    by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2])
wenzelm@41807
   120
  from assms PX Y0 show ?thesis
wenzelm@44779
   121
    by (cases x) (auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
chaieb@17378
   122
qed
chaieb@17378
   123
haftmann@22742
   124
text {* add conserves normalizedness *}
wenzelm@44779
   125
lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
wenzelm@44779
   126
proof (induct P Q rule: add.induct)
wenzelm@44779
   127
  case (2 c i P2)
wenzelm@55754
   128
  then show ?case by (cases P2) (simp_all, cases i, simp_all)
chaieb@17378
   129
next
wenzelm@44779
   130
  case (3 i P2 c)
wenzelm@55754
   131
  then show ?case by (cases P2) (simp_all, cases i, simp_all)
chaieb@17378
   132
next
chaieb@17378
   133
  case (4 c P2 i Q2)
wenzelm@44779
   134
  then have "isnorm P2" "isnorm Q2"
wenzelm@44779
   135
    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
wenzelm@44779
   136
  with 4 show ?case
wenzelm@44779
   137
    by (cases i) (simp, cases P2, auto, case_tac pol2, auto)
chaieb@17378
   138
next
chaieb@17378
   139
  case (5 P2 i Q2 c)
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 5 show ?case
wenzelm@44779
   143
    by (cases i) (simp, cases P2, auto, case_tac pol2, auto)
chaieb@17378
   144
next
chaieb@17378
   145
  case (6 x P2 y Q2)
wenzelm@41807
   146
  then have Y0: "y>0" by (cases y) (auto simp add: norm_Pinj_0_False)
wenzelm@41807
   147
  with 6 have X0: "x>0" by (cases x) (auto simp add: norm_Pinj_0_False)
chaieb@17378
   148
  have "x < y \<or> x = y \<or> x > y" by arith
chaieb@17378
   149
  moreover
wenzelm@55754
   150
  { assume "x < y"
wenzelm@55754
   151
    then have "\<exists>d. y = d + x" by arith
wenzelm@41807
   152
    then obtain d where y: "y = d + x" ..
chaieb@17378
   153
    moreover
wenzelm@41807
   154
    note 6 X0
chaieb@17378
   155
    moreover
wenzelm@44779
   156
    from 6 have "isnorm P2" "isnorm Q2"
wenzelm@44779
   157
      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
chaieb@17378
   158
    moreover
wenzelm@44779
   159
    from 6 `x < y` y have "isnorm (Pinj d Q2)"
wenzelm@44779
   160
      by (cases d, simp, cases Q2, auto)
wenzelm@41807
   161
    ultimately have ?case by (simp add: mkPinj_cn) }
chaieb@17378
   162
  moreover
wenzelm@55754
   163
  { assume "x = y"
chaieb@17378
   164
    moreover
wenzelm@44779
   165
    from 6 have "isnorm P2" "isnorm Q2"
wenzelm@44779
   166
      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
chaieb@17378
   167
    moreover
wenzelm@41807
   168
    note 6 Y0
chaieb@17378
   169
    ultimately have ?case by (simp add: mkPinj_cn) }
chaieb@17378
   170
  moreover
wenzelm@55754
   171
  { assume "x > y" then have "\<exists>d. x = d + y" by arith
wenzelm@41807
   172
    then obtain d where x: "x = d + y"..
chaieb@17378
   173
    moreover
wenzelm@41807
   174
    note 6 Y0
chaieb@17378
   175
    moreover
wenzelm@44779
   176
    from 6 have "isnorm P2" "isnorm Q2"
wenzelm@44779
   177
      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
chaieb@17378
   178
    moreover
wenzelm@44779
   179
    from 6 `x > y` x have "isnorm (Pinj d P2)"
wenzelm@44779
   180
      by (cases d) (simp, cases P2, auto)
wenzelm@44779
   181
    ultimately have ?case by (simp add: mkPinj_cn) }
chaieb@17378
   182
  ultimately show ?case by blast
chaieb@17378
   183
next
chaieb@17378
   184
  case (7 x P2 Q2 y R)
wenzelm@44779
   185
  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
chaieb@17378
   186
  moreover
wenzelm@41807
   187
  { assume "x = 0"
wenzelm@41807
   188
    with 7 have ?case by (auto simp add: norm_Pinj_0_False) }
chaieb@17378
   189
  moreover
wenzelm@41807
   190
  { assume "x = 1"
wenzelm@44779
   191
    from 7 have "isnorm R" "isnorm P2"
wenzelm@44779
   192
      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@41807
   193
    with 7 `x = 1` have "isnorm (R \<oplus> P2)" by simp
wenzelm@44779
   194
    with 7 `x = 1` have ?case
wenzelm@44779
   195
      by (simp add: norm_PXtrans[of Q2 y _]) }
chaieb@17378
   196
  moreover
wenzelm@55754
   197
  { assume "x > 1" then have "\<exists>d. x=Suc (Suc d)" by arith
wenzelm@44779
   198
    then obtain d where X: "x=Suc (Suc d)" ..
wenzelm@41807
   199
    with 7 have NR: "isnorm R" "isnorm P2"
wenzelm@41807
   200
      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@41807
   201
    with 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
wenzelm@41807
   202
    with 7 X NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
wenzelm@44779
   203
    with `isnorm (PX Q2 y R)` X have ?case
wenzelm@44779
   204
      by (simp add: norm_PXtrans[of Q2 y _]) }
chaieb@17378
   205
  ultimately show ?case by blast
chaieb@17378
   206
next
chaieb@17378
   207
  case (8 Q2 y R x P2)
haftmann@22742
   208
  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
chaieb@17378
   209
  moreover
wenzelm@41807
   210
  { assume "x = 0" with 8 have ?case by (auto simp add: norm_Pinj_0_False) }
chaieb@17378
   211
  moreover
wenzelm@41807
   212
  { assume "x = 1"
wenzelm@41807
   213
    with 8 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@41807
   214
    with 8 `x = 1` have "isnorm (R \<oplus> P2)" by simp
wenzelm@41807
   215
    with 8 `x = 1` have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
chaieb@17378
   216
  moreover
wenzelm@55754
   217
  { assume "x > 1" then have "\<exists>d. x=Suc (Suc d)" by arith
wenzelm@41807
   218
    then obtain d where X: "x = Suc (Suc d)" ..
wenzelm@41807
   219
    with 8 have NR: "isnorm R" "isnorm P2"
wenzelm@41807
   220
      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@41807
   221
    with 8 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
wenzelm@41807
   222
    with 8 `x > 1` NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
wenzelm@41807
   223
    with `isnorm (PX Q2 y R)` X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
chaieb@17378
   224
  ultimately show ?case by blast
chaieb@17378
   225
next
chaieb@17378
   226
  case (9 P1 x P2 Q1 y Q2)
wenzelm@41807
   227
  then have Y0: "y>0" by (cases y) auto
wenzelm@41807
   228
  with 9 have X0: "x>0" by (cases x) auto
wenzelm@41807
   229
  with 9 have NP1: "isnorm P1" and NP2: "isnorm P2"
wenzelm@41807
   230
    by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])
wenzelm@44779
   231
  with 9 have NQ1: "isnorm Q1" and NQ2: "isnorm Q2"
wenzelm@41807
   232
    by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])
chaieb@17378
   233
  have "y < x \<or> x = y \<or> x < y" by arith
chaieb@17378
   234
  moreover
wenzelm@55754
   235
  { assume sm1: "y < x" then have "\<exists>d. x = d + y" by arith
wenzelm@41807
   236
    then obtain d where sm2: "x = d + y" ..
wenzelm@41807
   237
    note 9 NQ1 NP1 NP2 NQ2 sm1 sm2
chaieb@17378
   238
    moreover
chaieb@17378
   239
    have "isnorm (PX P1 d (Pc 0))" 
wenzelm@41807
   240
    proof (cases P1)
chaieb@17378
   241
      case (PX p1 y p2)
wenzelm@44779
   242
      with 9 sm1 sm2 show ?thesis by (cases d) (simp, cases p2, auto)
wenzelm@41807
   243
    next
wenzelm@41807
   244
      case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto
wenzelm@41807
   245
    next
wenzelm@41807
   246
      case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto
chaieb@17378
   247
    qed
haftmann@22742
   248
    ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)" by auto
wenzelm@41807
   249
    with Y0 sm1 sm2 have ?case by (simp add: mkPX_cn) }
chaieb@17378
   250
  moreover
wenzelm@41807
   251
  { assume "x = y"
wenzelm@41807
   252
    with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)" by auto
wenzelm@41807
   253
    with `x = y` Y0 have ?case by (simp add: mkPX_cn) }
chaieb@17378
   254
  moreover
wenzelm@55754
   255
  { assume sm1: "x < y" then have "\<exists>d. y = d + x" by arith
wenzelm@41807
   256
    then obtain d where sm2: "y = d + x" ..
wenzelm@41807
   257
    note 9 NQ1 NP1 NP2 NQ2 sm1 sm2
chaieb@17378
   258
    moreover
chaieb@17378
   259
    have "isnorm (PX Q1 d (Pc 0))" 
wenzelm@41807
   260
    proof (cases Q1)
chaieb@17378
   261
      case (PX p1 y p2)
wenzelm@44779
   262
      with 9 sm1 sm2 show ?thesis by (cases d) (simp, cases p2, auto)
wenzelm@41807
   263
    next
wenzelm@41807
   264
      case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto
wenzelm@41807
   265
    next
wenzelm@41807
   266
      case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto
chaieb@17378
   267
    qed
haftmann@22742
   268
    ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)" by auto
wenzelm@44779
   269
    with X0 sm1 sm2 have ?case by (simp add: mkPX_cn) }
chaieb@17378
   270
  ultimately show ?case by blast
haftmann@22742
   271
qed simp
chaieb@17378
   272
haftmann@22742
   273
text {* mul concerves normalizedness *}
wenzelm@44779
   274
lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
wenzelm@44779
   275
proof (induct P Q rule: mul.induct)
wenzelm@55754
   276
  case (2 c i P2) then show ?case 
wenzelm@44779
   277
    by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
chaieb@17378
   278
next
wenzelm@55754
   279
  case (3 i P2 c) then show ?case 
wenzelm@44779
   280
    by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
chaieb@17378
   281
next
chaieb@17378
   282
  case (4 c P2 i Q2)
wenzelm@44779
   283
  then have "isnorm P2" "isnorm Q2"
wenzelm@44779
   284
    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
wenzelm@41807
   285
  with 4 show ?case 
wenzelm@44779
   286
    by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
chaieb@17378
   287
next
chaieb@17378
   288
  case (5 P2 i Q2 c)
wenzelm@44779
   289
  then have "isnorm P2" "isnorm Q2"
wenzelm@44779
   290
    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
wenzelm@41807
   291
  with 5 show ?case
wenzelm@44779
   292
    by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
chaieb@17378
   293
next
chaieb@17378
   294
  case (6 x P2 y Q2)
chaieb@17378
   295
  have "x < y \<or> x = y \<or> x > y" by arith
chaieb@17378
   296
  moreover
wenzelm@55754
   297
  { assume "x < y" then have "\<exists>d. y = d + x" by arith
wenzelm@41807
   298
    then obtain d where y: "y = d + x" ..
chaieb@17378
   299
    moreover
wenzelm@41807
   300
    note 6
chaieb@17378
   301
    moreover
wenzelm@41807
   302
    from 6 have "x > 0" by (cases x) (auto simp add: norm_Pinj_0_False)
chaieb@17378
   303
    moreover
wenzelm@41807
   304
    from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
chaieb@17378
   305
    moreover
wenzelm@44779
   306
    from 6 `x < y` y have "isnorm (Pinj d Q2)" by (cases d) (simp, cases Q2, auto) 
wenzelm@41807
   307
    ultimately have ?case by (simp add: mkPinj_cn) }
chaieb@17378
   308
  moreover
wenzelm@41807
   309
  { assume "x = y"
chaieb@17378
   310
    moreover
wenzelm@41807
   311
    from 6 have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
chaieb@17378
   312
    moreover
wenzelm@41807
   313
    from 6 have "y>0" by (cases y) (auto simp add: norm_Pinj_0_False)
chaieb@17378
   314
    moreover
wenzelm@41807
   315
    note 6
chaieb@17378
   316
    ultimately have ?case by (simp add: mkPinj_cn) }
chaieb@17378
   317
  moreover
wenzelm@55754
   318
  { assume "x > y" then have "\<exists>d. x = d + y" by arith
wenzelm@41807
   319
    then obtain d where x: "x = d + y" ..
chaieb@17378
   320
    moreover
wenzelm@41807
   321
    note 6
chaieb@17378
   322
    moreover
wenzelm@41807
   323
    from 6 have "y > 0" by (cases y) (auto simp add: norm_Pinj_0_False)
chaieb@17378
   324
    moreover
wenzelm@41807
   325
    from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
chaieb@17378
   326
    moreover
wenzelm@44779
   327
    from 6 `x > y` x have "isnorm (Pinj d P2)" by (cases d) (simp, cases P2, auto)
chaieb@17378
   328
    ultimately have ?case by (simp add: mkPinj_cn) }
chaieb@17378
   329
  ultimately show ?case by blast
chaieb@17378
   330
next
chaieb@17378
   331
  case (7 x P2 Q2 y R)
wenzelm@41807
   332
  then have Y0: "y > 0" by (cases y) auto
wenzelm@41807
   333
  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
chaieb@17378
   334
  moreover
wenzelm@41807
   335
  { assume "x = 0" with 7 have ?case by (auto simp add: norm_Pinj_0_False) }
chaieb@17378
   336
  moreover
wenzelm@41807
   337
  { assume "x = 1"
wenzelm@41807
   338
    from 7 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@41807
   339
    with 7 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
wenzelm@41807
   340
    with 7 `x = 1` Y0 have ?case by (simp add: mkPX_cn) }
chaieb@17378
   341
  moreover
wenzelm@55754
   342
  { assume "x > 1" then have "\<exists>d. x = Suc (Suc d)" by arith
wenzelm@41807
   343
    then obtain d where X: "x = Suc (Suc d)" ..
wenzelm@41807
   344
    from 7 have NR: "isnorm R" "isnorm Q2"
wenzelm@41807
   345
      by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
chaieb@17378
   346
    moreover
wenzelm@41807
   347
    from 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
wenzelm@41807
   348
    moreover
wenzelm@41807
   349
    from 7 have "isnorm (Pinj x P2)" by (cases P2) auto
chaieb@17378
   350
    moreover
wenzelm@41807
   351
    note 7 X
haftmann@22742
   352
    ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto
wenzelm@41807
   353
    with Y0 X have ?case by (simp add: mkPX_cn) }
chaieb@17378
   354
  ultimately show ?case by blast
chaieb@17378
   355
next
chaieb@17378
   356
  case (8 Q2 y R x P2)
wenzelm@55754
   357
  then have Y0: "y > 0" by (cases y) auto
wenzelm@41807
   358
  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
chaieb@17378
   359
  moreover
wenzelm@41807
   360
  { assume "x = 0" with 8 have ?case by (auto simp add: norm_Pinj_0_False) }
chaieb@17378
   361
  moreover
wenzelm@41807
   362
  { assume "x = 1"
wenzelm@41807
   363
    from 8 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
wenzelm@41807
   364
    with 8 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
wenzelm@41807
   365
    with 8 `x = 1` Y0 have ?case by (simp add: mkPX_cn) }
chaieb@17378
   366
  moreover
wenzelm@55754
   367
  { assume "x > 1" then have "\<exists>d. x = Suc (Suc d)" by arith
wenzelm@41807
   368
    then obtain d where X: "x = Suc (Suc d)" ..
wenzelm@41807
   369
    from 8 have NR: "isnorm R" "isnorm Q2"
wenzelm@41807
   370
      by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
chaieb@17378
   371
    moreover
wenzelm@41807
   372
    from 8 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
chaieb@17378
   373
    moreover
wenzelm@41807
   374
    from 8 X have "isnorm (Pinj x P2)" by (cases P2) auto
chaieb@17378
   375
    moreover
wenzelm@41807
   376
    note 8 X
haftmann@22742
   377
    ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto
chaieb@17378
   378
    with Y0 X have ?case by (simp add: mkPX_cn) }
chaieb@17378
   379
  ultimately show ?case by blast
chaieb@17378
   380
next
chaieb@17378
   381
  case (9 P1 x P2 Q1 y Q2)
wenzelm@41807
   382
  from 9 have X0: "x > 0" by (cases x) auto
wenzelm@41807
   383
  from 9 have Y0: "y > 0" by (cases y) auto
wenzelm@41807
   384
  note 9
chaieb@17378
   385
  moreover
wenzelm@41807
   386
  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
   387
  moreover 
wenzelm@41807
   388
  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
   389
  ultimately have "isnorm (P1 \<otimes> Q1)" "isnorm (P2 \<otimes> Q2)"
haftmann@22742
   390
    "isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)" 
chaieb@17378
   391
    by (auto simp add: mkPinj_cn)
wenzelm@41807
   392
  with 9 X0 Y0 have
haftmann@22742
   393
    "isnorm (mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2))"
haftmann@22742
   394
    "isnorm (mkPX (P1 \<otimes> mkPinj (Suc 0) Q2) x (Pc 0))"  
haftmann@22742
   395
    "isnorm (mkPX (Q1 \<otimes> mkPinj (Suc 0) P2) y (Pc 0))" 
chaieb@17378
   396
    by (auto simp add: mkPX_cn)
wenzelm@55754
   397
  then show ?case by (simp add: add_cn)
wenzelm@41807
   398
qed simp
chaieb@17378
   399
haftmann@22742
   400
text {* neg conserves normalizedness *}
chaieb@17378
   401
lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"
haftmann@22742
   402
proof (induct P)
chaieb@17378
   403
  case (Pinj i P2)
wenzelm@41807
   404
  then have "isnorm P2" by (simp add: norm_Pinj[of i P2])
wenzelm@44779
   405
  with Pinj show ?case by (cases P2) (auto, cases i, auto)
chaieb@17378
   406
next
wenzelm@41807
   407
  case (PX P1 x P2) note PX1 = this
wenzelm@41807
   408
  from PX have "isnorm P2" "isnorm P1"
wenzelm@41807
   409
    by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
wenzelm@41807
   410
  with PX show ?case
wenzelm@41807
   411
  proof (cases P1)
chaieb@17378
   412
    case (PX p1 y p2)
wenzelm@44779
   413
    with PX1 show ?thesis by (cases x) (auto, cases p2, auto)
chaieb@17378
   414
  next
chaieb@17378
   415
    case Pinj
wenzelm@41807
   416
    with PX1 show ?thesis by (cases x) auto
wenzelm@41807
   417
  qed (cases x, auto)
wenzelm@41807
   418
qed simp
chaieb@17378
   419
haftmann@22742
   420
text {* sub conserves normalizedness *}
wenzelm@44779
   421
lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
wenzelm@44779
   422
  by (simp add: sub_def add_cn neg_cn)
chaieb@17378
   423
haftmann@22742
   424
text {* sqr conserves normalizizedness *}
wenzelm@44779
   425
lemma sqr_cn: "isnorm P \<Longrightarrow> isnorm (sqr P)"
wenzelm@41807
   426
proof (induct P)
wenzelm@44779
   427
  case Pc
wenzelm@44779
   428
  then show ?case by simp
wenzelm@44779
   429
next
chaieb@17378
   430
  case (Pinj i Q)
wenzelm@41807
   431
  then show ?case
wenzelm@44779
   432
    by (cases Q) (auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
chaieb@17378
   433
next 
chaieb@17378
   434
  case (PX P1 x P2)
wenzelm@55754
   435
  then have "x + x \<noteq> 0" "isnorm P2" "isnorm P1"
wenzelm@41807
   436
    by (cases x, auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
wenzelm@41807
   437
  with PX have "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))"
wenzelm@41807
   438
      and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
wenzelm@41807
   439
    by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
wenzelm@41807
   440
  then show ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
wenzelm@44779
   441
qed
chaieb@17378
   442
haftmann@22742
   443
text {* pow conserves normalizedness *}
wenzelm@44779
   444
lemma pow_cn: "isnorm P \<Longrightarrow> isnorm (pow n P)"
wenzelm@44779
   445
proof (induct n arbitrary: P rule: less_induct)
wenzelm@44779
   446
  case (less k)
chaieb@17378
   447
  show ?case 
wenzelm@41807
   448
  proof (cases "k = 0")
wenzelm@44779
   449
    case True
wenzelm@44779
   450
    then show ?thesis by simp
wenzelm@44779
   451
  next
chaieb@17378
   452
    case False
wenzelm@41807
   453
    then have K2: "k div 2 < k" by (cases k) auto
wenzelm@44779
   454
    from less have "isnorm (sqr P)" by (simp add: sqr_cn)
wenzelm@44779
   455
    with less False K2 show ?thesis
wenzelm@44779
   456
      by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
wenzelm@44779
   457
  qed
chaieb@17378
   458
qed
chaieb@17378
   459
wenzelm@17388
   460
end