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