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