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