|
1 (* Title: HOL/ZF/Games.thy |
|
2 ID: $Id$ |
|
3 Author: Steven Obua |
|
4 |
|
5 An application of HOLZF: Partizan Games. |
|
6 See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan |
|
7 *) |
|
8 |
|
9 theory Games |
|
10 imports MainZF |
|
11 begin |
|
12 |
|
13 constdefs |
|
14 fixgames :: "ZF set \<Rightarrow> ZF set" |
|
15 "fixgames A \<equiv> { Opair l r | l r. explode l \<subseteq> A & explode r \<subseteq> A}" |
|
16 games_lfp :: "ZF set" |
|
17 "games_lfp \<equiv> lfp fixgames" |
|
18 games_gfp :: "ZF set" |
|
19 "games_gfp \<equiv> gfp fixgames" |
|
20 |
|
21 lemma mono_fixgames: "mono (fixgames)" |
|
22 apply (auto simp add: mono_def fixgames_def) |
|
23 apply (rule_tac x=l in exI) |
|
24 apply (rule_tac x=r in exI) |
|
25 apply auto |
|
26 done |
|
27 |
|
28 lemma games_lfp_unfold: "games_lfp = fixgames games_lfp" |
|
29 by (auto simp add: def_lfp_unfold games_lfp_def mono_fixgames) |
|
30 |
|
31 lemma games_gfp_unfold: "games_gfp = fixgames games_gfp" |
|
32 by (auto simp add: def_gfp_unfold games_gfp_def mono_fixgames) |
|
33 |
|
34 lemma games_lfp_nonempty: "Opair Empty Empty \<in> games_lfp" |
|
35 proof - |
|
36 have "fixgames {} \<subseteq> games_lfp" |
|
37 apply (subst games_lfp_unfold) |
|
38 apply (simp add: mono_fixgames[simplified mono_def, rule_format]) |
|
39 done |
|
40 moreover have "fixgames {} = {Opair Empty Empty}" |
|
41 by (simp add: fixgames_def explode_Empty) |
|
42 finally show ?thesis |
|
43 by auto |
|
44 qed |
|
45 |
|
46 constdefs |
|
47 left_option :: "ZF \<Rightarrow> ZF \<Rightarrow> bool" |
|
48 "left_option g opt \<equiv> (Elem opt (Fst g))" |
|
49 right_option :: "ZF \<Rightarrow> ZF \<Rightarrow> bool" |
|
50 "right_option g opt \<equiv> (Elem opt (Snd g))" |
|
51 is_option_of :: "(ZF * ZF) set" |
|
52 "is_option_of \<equiv> { (opt, g) | opt g. g \<in> games_gfp \<and> (left_option g opt \<or> right_option g opt) }" |
|
53 |
|
54 lemma games_lfp_subset_gfp: "games_lfp \<subseteq> games_gfp" |
|
55 proof - |
|
56 have "games_lfp \<subseteq> fixgames games_lfp" |
|
57 by (simp add: games_lfp_unfold[symmetric]) |
|
58 then show ?thesis |
|
59 by (simp add: games_gfp_def gfp_upperbound) |
|
60 qed |
|
61 |
|
62 lemma games_option_stable: |
|
63 assumes fixgames: "games = fixgames games" |
|
64 and g: "g \<in> games" |
|
65 and opt: "left_option g opt \<or> right_option g opt" |
|
66 shows "opt \<in> games" |
|
67 proof - |
|
68 from g fixgames have "g \<in> fixgames games" by auto |
|
69 then have "\<exists> l r. g = Opair l r \<and> explode l \<subseteq> games \<and> explode r \<subseteq> games" |
|
70 by (simp add: fixgames_def) |
|
71 then obtain l where "\<exists> r. g = Opair l r \<and> explode l \<subseteq> games \<and> explode r \<subseteq> games" .. |
|
72 then obtain r where lr: "g = Opair l r \<and> explode l \<subseteq> games \<and> explode r \<subseteq> games" .. |
|
73 with opt show ?thesis |
|
74 by (auto intro: Elem_explode_in simp add: left_option_def right_option_def Fst Snd) |
|
75 qed |
|
76 |
|
77 lemma option2elem: "(opt,g) \<in> is_option_of \<Longrightarrow> \<exists> u v. Elem opt u \<and> Elem u v \<and> Elem v g" |
|
78 apply (simp add: is_option_of_def) |
|
79 apply (subgoal_tac "(g \<in> games_gfp) = (g \<in> (fixgames games_gfp))") |
|
80 prefer 2 |
|
81 apply (simp add: games_gfp_unfold[symmetric]) |
|
82 apply (auto simp add: fixgames_def left_option_def right_option_def Fst Snd) |
|
83 apply (rule_tac x=l in exI, insert Elem_Opair_exists, blast) |
|
84 apply (rule_tac x=r in exI, insert Elem_Opair_exists, blast) |
|
85 done |
|
86 |
|
87 lemma is_option_of_subset_is_Elem_of: "is_option_of \<subseteq> (is_Elem_of^+)" |
|
88 proof - |
|
89 { |
|
90 fix opt |
|
91 fix g |
|
92 assume "(opt, g) \<in> is_option_of" |
|
93 then have "\<exists> u v. (opt, u) \<in> (is_Elem_of^+) \<and> (u,v) \<in> (is_Elem_of^+) \<and> (v,g) \<in> (is_Elem_of^+)" |
|
94 apply - |
|
95 apply (drule option2elem) |
|
96 apply (auto simp add: r_into_trancl' is_Elem_of_def) |
|
97 done |
|
98 then have "(opt, g) \<in> (is_Elem_of^+)" |
|
99 by (blast intro: trancl_into_rtrancl trancl_rtrancl_trancl) |
|
100 } |
|
101 then show ?thesis by auto |
|
102 qed |
|
103 |
|
104 lemma wfzf_is_option_of: "wfzf is_option_of" |
|
105 proof - |
|
106 have "wfzf (is_Elem_of^+)" by (simp add: wfzf_trancl wfzf_is_Elem_of) |
|
107 then show ?thesis |
|
108 apply (rule wfzf_subset) |
|
109 apply (rule is_option_of_subset_is_Elem_of) |
|
110 done |
|
111 qed |
|
112 |
|
113 lemma games_gfp_imp_lfp: "g \<in> games_gfp \<longrightarrow> g \<in> games_lfp" |
|
114 proof - |
|
115 have unfold_gfp: "\<And> x. x \<in> games_gfp \<Longrightarrow> x \<in> (fixgames games_gfp)" |
|
116 by (simp add: games_gfp_unfold[symmetric]) |
|
117 have unfold_lfp: "\<And> x. (x \<in> games_lfp) = (x \<in> (fixgames games_lfp))" |
|
118 by (simp add: games_lfp_unfold[symmetric]) |
|
119 show ?thesis |
|
120 apply (rule wf_induct[OF wfzf_implies_wf[OF wfzf_is_option_of]]) |
|
121 apply (auto simp add: is_option_of_def) |
|
122 apply (drule_tac unfold_gfp) |
|
123 apply (simp add: fixgames_def) |
|
124 apply (auto simp add: left_option_def Fst right_option_def Snd) |
|
125 apply (subgoal_tac "explode l \<subseteq> games_lfp") |
|
126 apply (subgoal_tac "explode r \<subseteq> games_lfp") |
|
127 apply (subst unfold_lfp) |
|
128 apply (auto simp add: fixgames_def) |
|
129 apply (simp_all add: explode_Elem Elem_explode_in) |
|
130 done |
|
131 qed |
|
132 |
|
133 theorem games_lfp_eq_gfp: "games_lfp = games_gfp" |
|
134 apply (auto simp add: games_gfp_imp_lfp) |
|
135 apply (insert games_lfp_subset_gfp) |
|
136 apply auto |
|
137 done |
|
138 |
|
139 theorem unique_games: "(g = fixgames g) = (g = games_lfp)" |
|
140 proof - |
|
141 { |
|
142 fix g |
|
143 assume g: "g = fixgames g" |
|
144 from g have "fixgames g \<subseteq> g" by auto |
|
145 then have l:"games_lfp \<subseteq> g" |
|
146 by (simp add: games_lfp_def lfp_lowerbound) |
|
147 from g have "g \<subseteq> fixgames g" by auto |
|
148 then have u:"g \<subseteq> games_gfp" |
|
149 by (simp add: games_gfp_def gfp_upperbound) |
|
150 from l u games_lfp_eq_gfp[symmetric] have "g = games_lfp" |
|
151 by auto |
|
152 } |
|
153 note games = this |
|
154 show ?thesis |
|
155 apply (rule iff[rule_format]) |
|
156 apply (erule games) |
|
157 apply (simp add: games_lfp_unfold[symmetric]) |
|
158 done |
|
159 qed |
|
160 |
|
161 lemma games_lfp_option_stable: |
|
162 assumes g: "g \<in> games_lfp" |
|
163 and opt: "left_option g opt \<or> right_option g opt" |
|
164 shows "opt \<in> games_lfp" |
|
165 apply (rule games_option_stable[where g=g]) |
|
166 apply (simp add: games_lfp_unfold[symmetric]) |
|
167 apply (simp_all add: prems) |
|
168 done |
|
169 |
|
170 lemma is_option_of_imp_games: |
|
171 assumes hyp: "(opt, g) \<in> is_option_of" |
|
172 shows "opt \<in> games_lfp \<and> g \<in> games_lfp" |
|
173 proof - |
|
174 from hyp have g_game: "g \<in> games_lfp" |
|
175 by (simp add: is_option_of_def games_lfp_eq_gfp) |
|
176 from hyp have "left_option g opt \<or> right_option g opt" |
|
177 by (auto simp add: is_option_of_def) |
|
178 with g_game games_lfp_option_stable[OF g_game, OF this] show ?thesis |
|
179 by auto |
|
180 qed |
|
181 |
|
182 lemma games_lfp_represent: "x \<in> games_lfp \<Longrightarrow> \<exists> l r. x = Opair l r" |
|
183 apply (rule exI[where x="Fst x"]) |
|
184 apply (rule exI[where x="Snd x"]) |
|
185 apply (subgoal_tac "x \<in> (fixgames games_lfp)") |
|
186 apply (simp add: fixgames_def) |
|
187 apply (auto simp add: Fst Snd) |
|
188 apply (simp add: games_lfp_unfold[symmetric]) |
|
189 done |
|
190 |
|
191 typedef game = games_lfp |
|
192 by (blast intro: games_lfp_nonempty) |
|
193 |
|
194 constdefs |
|
195 left_options :: "game \<Rightarrow> game zet" |
|
196 "left_options g \<equiv> zimage Abs_game (zexplode (Fst (Rep_game g)))" |
|
197 right_options :: "game \<Rightarrow> game zet" |
|
198 "right_options g \<equiv> zimage Abs_game (zexplode (Snd (Rep_game g)))" |
|
199 options :: "game \<Rightarrow> game zet" |
|
200 "options g \<equiv> zunion (left_options g) (right_options g)" |
|
201 Game :: "game zet \<Rightarrow> game zet \<Rightarrow> game" |
|
202 "Game L R \<equiv> Abs_game (Opair (zimplode (zimage Rep_game L)) (zimplode (zimage Rep_game R)))" |
|
203 |
|
204 lemma Repl_Rep_game_Abs_game: "\<forall> e. Elem e z \<longrightarrow> e \<in> games_lfp \<Longrightarrow> Repl z (Rep_game o Abs_game) = z" |
|
205 apply (subst Ext) |
|
206 apply (simp add: Repl) |
|
207 apply auto |
|
208 apply (subst Abs_game_inverse, simp_all add: game_def) |
|
209 apply (rule_tac x=za in exI) |
|
210 apply (subst Abs_game_inverse, simp_all add: game_def) |
|
211 done |
|
212 |
|
213 lemma game_split: "g = Game (left_options g) (right_options g)" |
|
214 proof - |
|
215 have "\<exists> l r. Rep_game g = Opair l r" |
|
216 apply (insert Rep_game[of g]) |
|
217 apply (simp add: game_def games_lfp_represent) |
|
218 done |
|
219 then obtain l r where lr: "Rep_game g = Opair l r" by auto |
|
220 have partizan_g: "Rep_game g \<in> games_lfp" |
|
221 apply (insert Rep_game[of g]) |
|
222 apply (simp add: game_def) |
|
223 done |
|
224 have "\<forall> e. Elem e l \<longrightarrow> left_option (Rep_game g) e" |
|
225 by (simp add: lr left_option_def Fst) |
|
226 then have partizan_l: "\<forall> e. Elem e l \<longrightarrow> e \<in> games_lfp" |
|
227 apply auto |
|
228 apply (rule games_lfp_option_stable[where g="Rep_game g", OF partizan_g]) |
|
229 apply auto |
|
230 done |
|
231 have "\<forall> e. Elem e r \<longrightarrow> right_option (Rep_game g) e" |
|
232 by (simp add: lr right_option_def Snd) |
|
233 then have partizan_r: "\<forall> e. Elem e r \<longrightarrow> e \<in> games_lfp" |
|
234 apply auto |
|
235 apply (rule games_lfp_option_stable[where g="Rep_game g", OF partizan_g]) |
|
236 apply auto |
|
237 done |
|
238 let ?L = "zimage (Abs_game) (zexplode l)" |
|
239 let ?R = "zimage (Abs_game) (zexplode r)" |
|
240 have L:"?L = left_options g" |
|
241 by (simp add: left_options_def lr Fst) |
|
242 have R:"?R = right_options g" |
|
243 by (simp add: right_options_def lr Snd) |
|
244 have "g = Game ?L ?R" |
|
245 apply (simp add: Game_def Rep_game_inject[symmetric] comp_zimage_eq zimage_zexplode_eq zimplode_zexplode) |
|
246 apply (simp add: Repl_Rep_game_Abs_game partizan_l partizan_r) |
|
247 apply (subst Abs_game_inverse) |
|
248 apply (simp_all add: lr[symmetric] Rep_game) |
|
249 done |
|
250 then show ?thesis |
|
251 by (simp add: L R) |
|
252 qed |
|
253 |
|
254 lemma Opair_in_games_lfp: |
|
255 assumes l: "explode l \<subseteq> games_lfp" |
|
256 and r: "explode r \<subseteq> games_lfp" |
|
257 shows "Opair l r \<in> games_lfp" |
|
258 proof - |
|
259 note f = unique_games[of games_lfp, simplified] |
|
260 show ?thesis |
|
261 apply (subst f) |
|
262 apply (simp add: fixgames_def) |
|
263 apply (rule exI[where x=l]) |
|
264 apply (rule exI[where x=r]) |
|
265 apply (auto simp add: l r) |
|
266 done |
|
267 qed |
|
268 |
|
269 lemma left_options[simp]: "left_options (Game l r) = l" |
|
270 apply (simp add: left_options_def Game_def) |
|
271 apply (subst Abs_game_inverse) |
|
272 apply (simp add: game_def) |
|
273 apply (rule Opair_in_games_lfp) |
|
274 apply (auto simp add: explode_Elem Elem_zimplode zimage_iff Rep_game[simplified game_def]) |
|
275 apply (simp add: Fst zexplode_zimplode comp_zimage_eq) |
|
276 apply (simp add: zet_ext_eq zimage_iff Rep_game_inverse) |
|
277 done |
|
278 |
|
279 lemma right_options[simp]: "right_options (Game l r) = r" |
|
280 apply (simp add: right_options_def Game_def) |
|
281 apply (subst Abs_game_inverse) |
|
282 apply (simp add: game_def) |
|
283 apply (rule Opair_in_games_lfp) |
|
284 apply (auto simp add: explode_Elem Elem_zimplode zimage_iff Rep_game[simplified game_def]) |
|
285 apply (simp add: Snd zexplode_zimplode comp_zimage_eq) |
|
286 apply (simp add: zet_ext_eq zimage_iff Rep_game_inverse) |
|
287 done |
|
288 |
|
289 lemma Game_ext: "(Game l1 r1 = Game l2 r2) = ((l1 = l2) \<and> (r1 = r2))" |
|
290 apply auto |
|
291 apply (subst left_options[where l=l1 and r=r1,symmetric]) |
|
292 apply (subst left_options[where l=l2 and r=r2,symmetric]) |
|
293 apply simp |
|
294 apply (subst right_options[where l=l1 and r=r1,symmetric]) |
|
295 apply (subst right_options[where l=l2 and r=r2,symmetric]) |
|
296 apply simp |
|
297 done |
|
298 |
|
299 constdefs |
|
300 option_of :: "(game * game) set" |
|
301 "option_of \<equiv> image (\<lambda> (option, g). (Abs_game option, Abs_game g)) is_option_of" |
|
302 |
|
303 lemma option_to_is_option_of: "((option, g) \<in> option_of) = ((Rep_game option, Rep_game g) \<in> is_option_of)" |
|
304 apply (auto simp add: option_of_def) |
|
305 apply (subst Abs_game_inverse) |
|
306 apply (simp add: is_option_of_imp_games game_def) |
|
307 apply (subst Abs_game_inverse) |
|
308 apply (simp add: is_option_of_imp_games game_def) |
|
309 apply simp |
|
310 apply (auto simp add: Bex_def image_def) |
|
311 apply (rule exI[where x="Rep_game option"]) |
|
312 apply (rule exI[where x="Rep_game g"]) |
|
313 apply (simp add: Rep_game_inverse) |
|
314 done |
|
315 |
|
316 lemma wf_is_option_of: "wf is_option_of" |
|
317 apply (rule wfzf_implies_wf) |
|
318 apply (simp add: wfzf_is_option_of) |
|
319 done |
|
320 |
|
321 lemma wf_option_of[recdef_wf, simp, intro]: "wf option_of" |
|
322 proof - |
|
323 have option_of: "option_of = inv_image is_option_of Rep_game" |
|
324 apply (rule set_ext) |
|
325 apply (case_tac "x") |
|
326 by (simp add: inv_image_def option_to_is_option_of) |
|
327 show ?thesis |
|
328 apply (simp add: option_of) |
|
329 apply (auto intro: wf_inv_image wf_is_option_of) |
|
330 done |
|
331 qed |
|
332 |
|
333 lemma right_option_is_option[simp, intro]: "zin x (right_options g) \<Longrightarrow> zin x (options g)" |
|
334 by (simp add: options_def zunion) |
|
335 |
|
336 lemma left_option_is_option[simp, intro]: "zin x (left_options g) \<Longrightarrow> zin x (options g)" |
|
337 by (simp add: options_def zunion) |
|
338 |
|
339 lemma zin_options[simp, intro]: "zin x (options g) \<Longrightarrow> (x, g) \<in> option_of" |
|
340 apply (simp add: options_def zunion left_options_def right_options_def option_of_def |
|
341 image_def is_option_of_def zimage_iff zin_zexplode_eq) |
|
342 apply (cases g) |
|
343 apply (cases x) |
|
344 apply (auto simp add: Abs_game_inverse games_lfp_eq_gfp[symmetric] game_def |
|
345 right_option_def[symmetric] left_option_def[symmetric]) |
|
346 done |
|
347 |
|
348 consts |
|
349 neg_game :: "game \<Rightarrow> game" |
|
350 |
|
351 recdef neg_game "option_of" |
|
352 "neg_game g = Game (zimage neg_game (right_options g)) (zimage neg_game (left_options g))" |
|
353 |
|
354 declare neg_game.simps[simp del] |
|
355 |
|
356 lemma "neg_game (neg_game g) = g" |
|
357 apply (induct g rule: neg_game.induct) |
|
358 apply (subst neg_game.simps)+ |
|
359 apply (simp add: right_options left_options comp_zimage_eq) |
|
360 apply (subgoal_tac "zimage (neg_game o neg_game) (left_options g) = left_options g") |
|
361 apply (subgoal_tac "zimage (neg_game o neg_game) (right_options g) = right_options g") |
|
362 apply (auto simp add: game_split[symmetric]) |
|
363 apply (auto simp add: zet_ext_eq zimage_iff) |
|
364 done |
|
365 |
|
366 consts |
|
367 ge_game :: "(game * game) \<Rightarrow> bool" |
|
368 |
|
369 recdef ge_game "(gprod_2_1 option_of)" |
|
370 "ge_game (G, H) = (\<forall> x. if zin x (right_options G) then ( |
|
371 if zin x (left_options H) then \<not> (ge_game (H, x) \<or> (ge_game (x, G))) |
|
372 else \<not> (ge_game (H, x))) |
|
373 else (if zin x (left_options H) then \<not> (ge_game (x, G)) else True))" |
|
374 (hints simp: gprod_2_1_def) |
|
375 |
|
376 declare ge_game.simps [simp del] |
|
377 |
|
378 lemma ge_game_def: "ge_game (G, H) = (\<forall> x. (zin x (right_options G) \<longrightarrow> \<not> ge_game (H, x)) \<and> (zin x (left_options H) \<longrightarrow> \<not> ge_game (x, G)))" |
|
379 apply (subst ge_game.simps[where G=G and H=H]) |
|
380 apply (auto) |
|
381 done |
|
382 |
|
383 lemma ge_game_leftright_refl[rule_format]: |
|
384 "\<forall> y. (zin y (right_options x) \<longrightarrow> \<not> ge_game (x, y)) \<and> (zin y (left_options x) \<longrightarrow> \<not> (ge_game (y, x))) \<and> ge_game (x, x)" |
|
385 proof (induct x rule: wf_induct[OF wf_option_of]) |
|
386 case (1 "g") |
|
387 { |
|
388 fix y |
|
389 assume y: "zin y (right_options g)" |
|
390 have "\<not> ge_game (g, y)" |
|
391 proof - |
|
392 have "(y, g) \<in> option_of" by (auto intro: y) |
|
393 with 1 have "ge_game (y, y)" by auto |
|
394 with y show ?thesis by (subst ge_game_def, auto) |
|
395 qed |
|
396 } |
|
397 note right = this |
|
398 { |
|
399 fix y |
|
400 assume y: "zin y (left_options g)" |
|
401 have "\<not> ge_game (y, g)" |
|
402 proof - |
|
403 have "(y, g) \<in> option_of" by (auto intro: y) |
|
404 with 1 have "ge_game (y, y)" by auto |
|
405 with y show ?thesis by (subst ge_game_def, auto) |
|
406 qed |
|
407 } |
|
408 note left = this |
|
409 from left right show ?case |
|
410 by (auto, subst ge_game_def, auto) |
|
411 qed |
|
412 |
|
413 lemma ge_game_refl: "ge_game (x,x)" by (simp add: ge_game_leftright_refl) |
|
414 |
|
415 lemma "\<forall> y. (zin y (right_options x) \<longrightarrow> \<not> ge_game (x, y)) \<and> (zin y (left_options x) \<longrightarrow> \<not> (ge_game (y, x))) \<and> ge_game (x, x)" |
|
416 proof (induct x rule: wf_induct[OF wf_option_of]) |
|
417 case (1 "g") |
|
418 show ?case |
|
419 proof (auto) |
|
420 {case (goal1 y) |
|
421 from goal1 have "(y, g) \<in> option_of" by (auto) |
|
422 with 1 have "ge_game (y, y)" by auto |
|
423 with goal1 have "\<not> ge_game (g, y)" |
|
424 by (subst ge_game_def, auto) |
|
425 with goal1 show ?case by auto} |
|
426 note right = this |
|
427 {case (goal2 y) |
|
428 from goal2 have "(y, g) \<in> option_of" by (auto) |
|
429 with 1 have "ge_game (y, y)" by auto |
|
430 with goal2 have "\<not> ge_game (y, g)" |
|
431 by (subst ge_game_def, auto) |
|
432 with goal2 show ?case by auto} |
|
433 note left = this |
|
434 {case goal3 |
|
435 from left right show ?case |
|
436 by (subst ge_game_def, auto) |
|
437 } |
|
438 qed |
|
439 qed |
|
440 |
|
441 constdefs |
|
442 eq_game :: "game \<Rightarrow> game \<Rightarrow> bool" |
|
443 "eq_game G H \<equiv> ge_game (G, H) \<and> ge_game (H, G)" |
|
444 |
|
445 lemma eq_game_sym: "(eq_game G H) = (eq_game H G)" |
|
446 by (auto simp add: eq_game_def) |
|
447 |
|
448 lemma eq_game_refl: "eq_game G G" |
|
449 by (simp add: ge_game_refl eq_game_def) |
|
450 |
|
451 lemma induct_game: "(\<And>x. \<forall>y. (y, x) \<in> lprod option_of \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a" |
|
452 by (erule wf_induct[OF wf_lprod[OF wf_option_of]]) |
|
453 |
|
454 lemma ge_game_trans: |
|
455 assumes "ge_game (x, y)" "ge_game (y, z)" |
|
456 shows "ge_game (x, z)" |
|
457 proof - |
|
458 { |
|
459 fix a |
|
460 have "\<forall> x y z. a = [x,y,z] \<longrightarrow> ge_game (x,y) \<longrightarrow> ge_game (y,z) \<longrightarrow> ge_game (x, z)" |
|
461 proof (induct a rule: induct_game) |
|
462 case (1 a) |
|
463 show ?case |
|
464 proof (rule allI | rule impI)+ |
|
465 case (goal1 x y z) |
|
466 show ?case |
|
467 proof - |
|
468 { fix xr |
|
469 assume xr:"zin xr (right_options x)" |
|
470 assume "ge_game (z, xr)" |
|
471 have "ge_game (y, xr)" |
|
472 apply (rule 1[rule_format, where y="[y,z,xr]"]) |
|
473 apply (auto intro: xr lprod_3_1 simp add: prems) |
|
474 done |
|
475 moreover from xr have "\<not> ge_game (y, xr)" |
|
476 by (simp add: goal1(2)[simplified ge_game_def[of x y], rule_format, of xr, simplified xr]) |
|
477 ultimately have "False" by auto |
|
478 } |
|
479 note xr = this |
|
480 { fix zl |
|
481 assume zl:"zin zl (left_options z)" |
|
482 assume "ge_game (zl, x)" |
|
483 have "ge_game (zl, y)" |
|
484 apply (rule 1[rule_format, where y="[zl,x,y]"]) |
|
485 apply (auto intro: zl lprod_3_2 simp add: prems) |
|
486 done |
|
487 moreover from zl have "\<not> ge_game (zl, y)" |
|
488 by (simp add: goal1(3)[simplified ge_game_def[of y z], rule_format, of zl, simplified zl]) |
|
489 ultimately have "False" by auto |
|
490 } |
|
491 note zl = this |
|
492 show ?thesis |
|
493 by (auto simp add: ge_game_def[of x z] intro: xr zl) |
|
494 qed |
|
495 qed |
|
496 qed |
|
497 } |
|
498 note trans = this[of "[x, y, z]", simplified, rule_format] |
|
499 with prems show ?thesis by blast |
|
500 qed |
|
501 |
|
502 lemma eq_game_trans: "eq_game a b \<Longrightarrow> eq_game b c \<Longrightarrow> eq_game a c" |
|
503 by (auto simp add: eq_game_def intro: ge_game_trans) |
|
504 |
|
505 constdefs |
|
506 zero_game :: game |
|
507 "zero_game \<equiv> Game zempty zempty" |
|
508 |
|
509 consts |
|
510 plus_game :: "game * game \<Rightarrow> game" |
|
511 |
|
512 recdef plus_game "gprod_2_2 option_of" |
|
513 "plus_game (G, H) = Game (zunion (zimage (\<lambda> g. plus_game (g, H)) (left_options G)) |
|
514 (zimage (\<lambda> h. plus_game (G, h)) (left_options H))) |
|
515 (zunion (zimage (\<lambda> g. plus_game (g, H)) (right_options G)) |
|
516 (zimage (\<lambda> h. plus_game (G, h)) (right_options H)))" |
|
517 (hints simp add: gprod_2_2_def) |
|
518 |
|
519 declare plus_game.simps[simp del] |
|
520 |
|
521 lemma plus_game_comm: "plus_game (G, H) = plus_game (H, G)" |
|
522 proof (induct G H rule: plus_game.induct) |
|
523 case (1 G H) |
|
524 show ?case |
|
525 by (auto simp add: |
|
526 plus_game.simps[where G=G and H=H] |
|
527 plus_game.simps[where G=H and H=G] |
|
528 Game_ext zet_ext_eq zunion zimage_iff prems) |
|
529 qed |
|
530 |
|
531 lemma game_ext_eq: "(G = H) = (left_options G = left_options H \<and> right_options G = right_options H)" |
|
532 proof - |
|
533 have "(G = H) = (Game (left_options G) (right_options G) = Game (left_options H) (right_options H))" |
|
534 by (simp add: game_split[symmetric]) |
|
535 then show ?thesis by auto |
|
536 qed |
|
537 |
|
538 lemma left_zero_game[simp]: "left_options (zero_game) = zempty" |
|
539 by (simp add: zero_game_def) |
|
540 |
|
541 lemma right_zero_game[simp]: "right_options (zero_game) = zempty" |
|
542 by (simp add: zero_game_def) |
|
543 |
|
544 lemma plus_game_zero_right[simp]: "plus_game (G, zero_game) = G" |
|
545 proof - |
|
546 { |
|
547 fix G H |
|
548 have "H = zero_game \<longrightarrow> plus_game (G, H) = G " |
|
549 proof (induct G H rule: plus_game.induct, rule impI) |
|
550 case (goal1 G H) |
|
551 note induct_hyp = prems[simplified goal1, simplified] and prems |
|
552 show ?case |
|
553 apply (simp only: plus_game.simps[where G=G and H=H]) |
|
554 apply (simp add: game_ext_eq prems) |
|
555 apply (auto simp add: |
|
556 zimage_cong[where f = "\<lambda> g. plus_game (g, zero_game)" and g = "id"] |
|
557 induct_hyp) |
|
558 done |
|
559 qed |
|
560 } |
|
561 then show ?thesis by auto |
|
562 qed |
|
563 |
|
564 lemma plus_game_zero_left: "plus_game (zero_game, G) = G" |
|
565 by (simp add: plus_game_comm) |
|
566 |
|
567 lemma left_imp_options[simp]: "zin opt (left_options g) \<Longrightarrow> zin opt (options g)" |
|
568 by (simp add: options_def zunion) |
|
569 |
|
570 lemma right_imp_options[simp]: "zin opt (right_options g) \<Longrightarrow> zin opt (options g)" |
|
571 by (simp add: options_def zunion) |
|
572 |
|
573 lemma left_options_plus: |
|
574 "left_options (plus_game (u, v)) = zunion (zimage (\<lambda>g. plus_game (g, v)) (left_options u)) (zimage (\<lambda>h. plus_game (u, h)) (left_options v))" |
|
575 by (subst plus_game.simps, simp) |
|
576 |
|
577 lemma right_options_plus: |
|
578 "right_options (plus_game (u, v)) = zunion (zimage (\<lambda>g. plus_game (g, v)) (right_options u)) (zimage (\<lambda>h. plus_game (u, h)) (right_options v))" |
|
579 by (subst plus_game.simps, simp) |
|
580 |
|
581 lemma left_options_neg: "left_options (neg_game u) = zimage neg_game (right_options u)" |
|
582 by (subst neg_game.simps, simp) |
|
583 |
|
584 lemma right_options_neg: "right_options (neg_game u) = zimage neg_game (left_options u)" |
|
585 by (subst neg_game.simps, simp) |
|
586 |
|
587 lemma plus_game_assoc: "plus_game (plus_game (F, G), H) = plus_game (F, plus_game (G, H))" |
|
588 proof - |
|
589 { |
|
590 fix a |
|
591 have "\<forall> F G H. a = [F, G, H] \<longrightarrow> plus_game (plus_game (F, G), H) = plus_game (F, plus_game (G, H))" |
|
592 proof (induct a rule: induct_game, (rule impI | rule allI)+) |
|
593 case (goal1 x F G H) |
|
594 let ?L = "plus_game (plus_game (F, G), H)" |
|
595 let ?R = "plus_game (F, plus_game (G, H))" |
|
596 note options_plus = left_options_plus right_options_plus |
|
597 { |
|
598 fix opt |
|
599 note hyp = goal1(1)[simplified goal1(2), rule_format] |
|
600 have F: "zin opt (options F) \<Longrightarrow> plus_game (plus_game (opt, G), H) = plus_game (opt, plus_game (G, H))" |
|
601 by (blast intro: hyp lprod_3_3) |
|
602 have G: "zin opt (options G) \<Longrightarrow> plus_game (plus_game (F, opt), H) = plus_game (F, plus_game (opt, H))" |
|
603 by (blast intro: hyp lprod_3_4) |
|
604 have H: "zin opt (options H) \<Longrightarrow> plus_game (plus_game (F, G), opt) = plus_game (F, plus_game (G, opt))" |
|
605 by (blast intro: hyp lprod_3_5) |
|
606 note F and G and H |
|
607 } |
|
608 note induct_hyp = this |
|
609 have "left_options ?L = left_options ?R \<and> right_options ?L = right_options ?R" |
|
610 by (auto simp add: |
|
611 plus_game.simps[where G="plus_game (F,G)" and H=H] |
|
612 plus_game.simps[where G="F" and H="plus_game (G,H)"] |
|
613 zet_ext_eq zunion zimage_iff options_plus |
|
614 induct_hyp left_imp_options right_imp_options) |
|
615 then show ?case |
|
616 by (simp add: game_ext_eq) |
|
617 qed |
|
618 } |
|
619 then show ?thesis by auto |
|
620 qed |
|
621 |
|
622 lemma neg_plus_game: "neg_game (plus_game (G, H)) = plus_game(neg_game G, neg_game H)" |
|
623 proof (induct G H rule: plus_game.induct) |
|
624 case (1 G H) |
|
625 note opt_ops = |
|
626 left_options_plus right_options_plus |
|
627 left_options_neg right_options_neg |
|
628 show ?case |
|
629 by (auto simp add: opt_ops |
|
630 neg_game.simps[of "plus_game (G,H)"] |
|
631 plus_game.simps[of "neg_game G" "neg_game H"] |
|
632 Game_ext zet_ext_eq zunion zimage_iff prems) |
|
633 qed |
|
634 |
|
635 lemma eq_game_plus_inverse: "eq_game (plus_game (x, neg_game x)) zero_game" |
|
636 proof (induct x rule: wf_induct[OF wf_option_of]) |
|
637 case (goal1 x) |
|
638 { fix y |
|
639 assume "zin y (options x)" |
|
640 then have "eq_game (plus_game (y, neg_game y)) zero_game" |
|
641 by (auto simp add: prems) |
|
642 } |
|
643 note ihyp = this |
|
644 { |
|
645 fix y |
|
646 assume y: "zin y (right_options x)" |
|
647 have "\<not> (ge_game (zero_game, plus_game (y, neg_game x)))" |
|
648 apply (subst ge_game.simps, simp) |
|
649 apply (rule exI[where x="plus_game (y, neg_game y)"]) |
|
650 apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def]) |
|
651 apply (auto simp add: left_options_plus left_options_neg zunion zimage_iff intro: prems) |
|
652 done |
|
653 } |
|
654 note case1 = this |
|
655 { |
|
656 fix y |
|
657 assume y: "zin y (left_options x)" |
|
658 have "\<not> (ge_game (zero_game, plus_game (x, neg_game y)))" |
|
659 apply (subst ge_game.simps, simp) |
|
660 apply (rule exI[where x="plus_game (y, neg_game y)"]) |
|
661 apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def]) |
|
662 apply (auto simp add: left_options_plus zunion zimage_iff intro: prems) |
|
663 done |
|
664 } |
|
665 note case2 = this |
|
666 { |
|
667 fix y |
|
668 assume y: "zin y (left_options x)" |
|
669 have "\<not> (ge_game (plus_game (y, neg_game x), zero_game))" |
|
670 apply (subst ge_game.simps, simp) |
|
671 apply (rule exI[where x="plus_game (y, neg_game y)"]) |
|
672 apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def]) |
|
673 apply (auto simp add: right_options_plus right_options_neg zunion zimage_iff intro: prems) |
|
674 done |
|
675 } |
|
676 note case3 = this |
|
677 { |
|
678 fix y |
|
679 assume y: "zin y (right_options x)" |
|
680 have "\<not> (ge_game (plus_game (x, neg_game y), zero_game))" |
|
681 apply (subst ge_game.simps, simp) |
|
682 apply (rule exI[where x="plus_game (y, neg_game y)"]) |
|
683 apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def]) |
|
684 apply (auto simp add: right_options_plus zunion zimage_iff intro: prems) |
|
685 done |
|
686 } |
|
687 note case4 = this |
|
688 show ?case |
|
689 apply (simp add: eq_game_def) |
|
690 apply (simp add: ge_game.simps[of "plus_game (x, neg_game x)" "zero_game"]) |
|
691 apply (simp add: ge_game.simps[of "zero_game" "plus_game (x, neg_game x)"]) |
|
692 apply (simp add: right_options_plus left_options_plus right_options_neg left_options_neg zunion zimage_iff) |
|
693 apply (auto simp add: case1 case2 case3 case4) |
|
694 done |
|
695 qed |
|
696 |
|
697 lemma ge_plus_game_left: "ge_game (y,z) = ge_game(plus_game (x, y), plus_game (x, z))" |
|
698 proof - |
|
699 { fix a |
|
700 have "\<forall> x y z. a = [x,y,z] \<longrightarrow> ge_game (y,z) = ge_game(plus_game (x, y), plus_game (x, z))" |
|
701 proof (induct a rule: induct_game, (rule impI | rule allI)+) |
|
702 case (goal1 a x y z) |
|
703 note induct_hyp = goal1(1)[rule_format, simplified goal1(2)] |
|
704 { |
|
705 assume hyp: "ge_game(plus_game (x, y), plus_game (x, z))" |
|
706 have "ge_game (y, z)" |
|
707 proof - |
|
708 { fix yr |
|
709 assume yr: "zin yr (right_options y)" |
|
710 from hyp have "\<not> (ge_game (plus_game (x, z), plus_game (x, yr)))" |
|
711 by (auto simp add: ge_game_def[of "plus_game (x,y)" "plus_game(x,z)"] |
|
712 right_options_plus zunion zimage_iff intro: yr) |
|
713 then have "\<not> (ge_game (z, yr))" |
|
714 apply (subst induct_hyp[where y="[x, z, yr]", of "x" "z" "yr"]) |
|
715 apply (simp_all add: yr lprod_3_6) |
|
716 done |
|
717 } |
|
718 note yr = this |
|
719 { fix zl |
|
720 assume zl: "zin zl (left_options z)" |
|
721 from hyp have "\<not> (ge_game (plus_game (x, zl), plus_game (x, y)))" |
|
722 by (auto simp add: ge_game_def[of "plus_game (x,y)" "plus_game(x,z)"] |
|
723 left_options_plus zunion zimage_iff intro: zl) |
|
724 then have "\<not> (ge_game (zl, y))" |
|
725 apply (subst goal1(1)[rule_format, where y="[x, zl, y]", of "x" "zl" "y"]) |
|
726 apply (simp_all add: goal1(2) zl lprod_3_7) |
|
727 done |
|
728 } |
|
729 note zl = this |
|
730 show "ge_game (y, z)" |
|
731 apply (subst ge_game_def) |
|
732 apply (auto simp add: yr zl) |
|
733 done |
|
734 qed |
|
735 } |
|
736 note right_imp_left = this |
|
737 { |
|
738 assume yz: "ge_game (y, z)" |
|
739 { |
|
740 fix x' |
|
741 assume x': "zin x' (right_options x)" |
|
742 assume hyp: "ge_game (plus_game (x, z), plus_game (x', y))" |
|
743 then have n: "\<not> (ge_game (plus_game (x', y), plus_game (x', z)))" |
|
744 by (auto simp add: ge_game_def[of "plus_game (x,z)" "plus_game (x', y)"] |
|
745 right_options_plus zunion zimage_iff intro: x') |
|
746 have t: "ge_game (plus_game (x', y), plus_game (x', z))" |
|
747 apply (subst induct_hyp[symmetric]) |
|
748 apply (auto intro: lprod_3_3 x' yz) |
|
749 done |
|
750 from n t have "False" by blast |
|
751 } |
|
752 note case1 = this |
|
753 { |
|
754 fix x' |
|
755 assume x': "zin x' (left_options x)" |
|
756 assume hyp: "ge_game (plus_game (x', z), plus_game (x, y))" |
|
757 then have n: "\<not> (ge_game (plus_game (x', y), plus_game (x', z)))" |
|
758 by (auto simp add: ge_game_def[of "plus_game (x',z)" "plus_game (x, y)"] |
|
759 left_options_plus zunion zimage_iff intro: x') |
|
760 have t: "ge_game (plus_game (x', y), plus_game (x', z))" |
|
761 apply (subst induct_hyp[symmetric]) |
|
762 apply (auto intro: lprod_3_3 x' yz) |
|
763 done |
|
764 from n t have "False" by blast |
|
765 } |
|
766 note case3 = this |
|
767 { |
|
768 fix y' |
|
769 assume y': "zin y' (right_options y)" |
|
770 assume hyp: "ge_game (plus_game(x, z), plus_game (x, y'))" |
|
771 then have "ge_game(z, y')" |
|
772 apply (subst induct_hyp[of "[x, z, y']" "x" "z" "y'"]) |
|
773 apply (auto simp add: hyp lprod_3_6 y') |
|
774 done |
|
775 with yz have "ge_game (y, y')" |
|
776 by (blast intro: ge_game_trans) |
|
777 with y' have "False" by (auto simp add: ge_game_leftright_refl) |
|
778 } |
|
779 note case2 = this |
|
780 { |
|
781 fix z' |
|
782 assume z': "zin z' (left_options z)" |
|
783 assume hyp: "ge_game (plus_game(x, z'), plus_game (x, y))" |
|
784 then have "ge_game(z', y)" |
|
785 apply (subst induct_hyp[of "[x, z', y]" "x" "z'" "y"]) |
|
786 apply (auto simp add: hyp lprod_3_7 z') |
|
787 done |
|
788 with yz have "ge_game (z', z)" |
|
789 by (blast intro: ge_game_trans) |
|
790 with z' have "False" by (auto simp add: ge_game_leftright_refl) |
|
791 } |
|
792 note case4 = this |
|
793 have "ge_game(plus_game (x, y), plus_game (x, z))" |
|
794 apply (subst ge_game_def) |
|
795 apply (auto simp add: right_options_plus left_options_plus zunion zimage_iff) |
|
796 apply (auto intro: case1 case2 case3 case4) |
|
797 done |
|
798 } |
|
799 note left_imp_right = this |
|
800 show ?case by (auto intro: right_imp_left left_imp_right) |
|
801 qed |
|
802 } |
|
803 note a = this[of "[x, y, z]"] |
|
804 then show ?thesis by blast |
|
805 qed |
|
806 |
|
807 lemma ge_plus_game_right: "ge_game (y,z) = ge_game(plus_game (y, x), plus_game (z, x))" |
|
808 by (simp add: ge_plus_game_left plus_game_comm) |
|
809 |
|
810 lemma ge_neg_game: "ge_game (neg_game x, neg_game y) = ge_game (y, x)" |
|
811 proof - |
|
812 { fix a |
|
813 have "\<forall> x y. a = [x, y] \<longrightarrow> ge_game (neg_game x, neg_game y) = ge_game (y, x)" |
|
814 proof (induct a rule: induct_game, (rule impI | rule allI)+) |
|
815 case (goal1 a x y) |
|
816 note ihyp = goal1(1)[rule_format, simplified goal1(2)] |
|
817 { fix xl |
|
818 assume xl: "zin xl (left_options x)" |
|
819 have "ge_game (neg_game y, neg_game xl) = ge_game (xl, y)" |
|
820 apply (subst ihyp) |
|
821 apply (auto simp add: lprod_2_1 xl) |
|
822 done |
|
823 } |
|
824 note xl = this |
|
825 { fix yr |
|
826 assume yr: "zin yr (right_options y)" |
|
827 have "ge_game (neg_game yr, neg_game x) = ge_game (x, yr)" |
|
828 apply (subst ihyp) |
|
829 apply (auto simp add: lprod_2_2 yr) |
|
830 done |
|
831 } |
|
832 note yr = this |
|
833 show ?case |
|
834 by (auto simp add: ge_game_def[of "neg_game x" "neg_game y"] ge_game_def[of "y" "x"] |
|
835 right_options_neg left_options_neg zimage_iff xl yr) |
|
836 qed |
|
837 } |
|
838 note a = this[of "[x,y]"] |
|
839 then show ?thesis by blast |
|
840 qed |
|
841 |
|
842 constdefs |
|
843 eq_game_rel :: "(game * game) set" |
|
844 "eq_game_rel \<equiv> { (p, q) . eq_game p q }" |
|
845 |
|
846 typedef Pg = "UNIV//eq_game_rel" |
|
847 by (auto simp add: quotient_def) |
|
848 |
|
849 lemma equiv_eq_game[simp]: "equiv UNIV eq_game_rel" |
|
850 by (auto simp add: equiv_def refl_def sym_def trans_def eq_game_rel_def |
|
851 eq_game_sym intro: eq_game_refl eq_game_trans) |
|
852 |
|
853 instance Pg :: "{ord,zero,plus,minus}" .. |
|
854 |
|
855 defs (overloaded) |
|
856 Pg_zero_def: "0 \<equiv> Abs_Pg (eq_game_rel `` {zero_game})" |
|
857 Pg_le_def: "G \<le> H \<equiv> \<exists> g h. g \<in> Rep_Pg G \<and> h \<in> Rep_Pg H \<and> ge_game (h, g)" |
|
858 Pg_less_def: "G < H \<equiv> G \<le> H \<and> G \<noteq> (H::Pg)" |
|
859 Pg_minus_def: "- G \<equiv> contents (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})" |
|
860 Pg_plus_def: "G + H \<equiv> contents (\<Union> g \<in> Rep_Pg G. \<Union> h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game (g,h)})})" |
|
861 Pg_diff_def: "G - H \<equiv> G + (- (H::Pg))" |
|
862 |
|
863 lemma Rep_Abs_eq_Pg[simp]: "Rep_Pg (Abs_Pg (eq_game_rel `` {g})) = eq_game_rel `` {g}" |
|
864 apply (subst Abs_Pg_inverse) |
|
865 apply (auto simp add: Pg_def quotient_def) |
|
866 done |
|
867 |
|
868 lemma char_Pg_le[simp]: "(Abs_Pg (eq_game_rel `` {g}) \<le> Abs_Pg (eq_game_rel `` {h})) = (ge_game (h, g))" |
|
869 apply (simp add: Pg_le_def) |
|
870 apply (auto simp add: eq_game_rel_def eq_game_def intro: ge_game_trans ge_game_refl) |
|
871 done |
|
872 |
|
873 lemma char_Pg_eq[simp]: "(Abs_Pg (eq_game_rel `` {g}) = Abs_Pg (eq_game_rel `` {h})) = (eq_game g h)" |
|
874 apply (simp add: Rep_Pg_inject [symmetric]) |
|
875 apply (subst eq_equiv_class_iff[of UNIV]) |
|
876 apply (simp_all) |
|
877 apply (simp add: eq_game_rel_def) |
|
878 done |
|
879 |
|
880 lemma char_Pg_plus[simp]: "Abs_Pg (eq_game_rel `` {g}) + Abs_Pg (eq_game_rel `` {h}) = Abs_Pg (eq_game_rel `` {plus_game (g, h)})" |
|
881 proof - |
|
882 have "(\<lambda> g h. {Abs_Pg (eq_game_rel `` {plus_game (g, h)})}) respects2 eq_game_rel" |
|
883 apply (simp add: congruent2_def) |
|
884 apply (auto simp add: eq_game_rel_def eq_game_def) |
|
885 apply (rule_tac y="plus_game (y1, z2)" in ge_game_trans) |
|
886 apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+ |
|
887 apply (rule_tac y="plus_game (z1, y2)" in ge_game_trans) |
|
888 apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+ |
|
889 done |
|
890 then show ?thesis |
|
891 by (simp add: Pg_plus_def UN_equiv_class2[OF equiv_eq_game equiv_eq_game]) |
|
892 qed |
|
893 |
|
894 lemma char_Pg_minus[simp]: "- Abs_Pg (eq_game_rel `` {g}) = Abs_Pg (eq_game_rel `` {neg_game g})" |
|
895 proof - |
|
896 have "(\<lambda> g. {Abs_Pg (eq_game_rel `` {neg_game g})}) respects eq_game_rel" |
|
897 apply (simp add: congruent_def) |
|
898 apply (auto simp add: eq_game_rel_def eq_game_def ge_neg_game) |
|
899 done |
|
900 then show ?thesis |
|
901 by (simp add: Pg_minus_def UN_equiv_class[OF equiv_eq_game]) |
|
902 qed |
|
903 |
|
904 lemma eq_Abs_Pg[rule_format, cases type: Pg]: "(\<forall> g. z = Abs_Pg (eq_game_rel `` {g}) \<longrightarrow> P) \<longrightarrow> P" |
|
905 apply (cases z, simp) |
|
906 apply (simp add: Rep_Pg_inject[symmetric]) |
|
907 apply (subst Abs_Pg_inverse, simp) |
|
908 apply (auto simp add: Pg_def quotient_def) |
|
909 done |
|
910 |
|
911 instance Pg :: pordered_ab_group_add |
|
912 proof |
|
913 fix a b c :: Pg |
|
914 show "(a < b) = (a \<le> b \<and> a \<noteq> b)" by (simp add: Pg_less_def) |
|
915 show "a - b = a + (- b)" by (simp add: Pg_diff_def) |
|
916 { |
|
917 assume ab: "a \<le> b" |
|
918 assume ba: "b \<le> a" |
|
919 from ab ba show "a = b" |
|
920 apply (cases a, cases b) |
|
921 apply (simp add: eq_game_def) |
|
922 done |
|
923 } |
|
924 show "a + b = b + a" |
|
925 apply (cases a, cases b) |
|
926 apply (simp add: eq_game_def plus_game_comm) |
|
927 done |
|
928 show "a + b + c = a + (b + c)" |
|
929 apply (cases a, cases b, cases c) |
|
930 apply (simp add: eq_game_def plus_game_assoc) |
|
931 done |
|
932 show "0 + a = a" |
|
933 apply (cases a) |
|
934 apply (simp add: Pg_zero_def plus_game_zero_left) |
|
935 done |
|
936 show "- a + a = 0" |
|
937 apply (cases a) |
|
938 apply (simp add: Pg_zero_def eq_game_plus_inverse plus_game_comm) |
|
939 done |
|
940 show "a \<le> a" |
|
941 apply (cases a) |
|
942 apply (simp add: ge_game_refl) |
|
943 done |
|
944 { |
|
945 assume ab: "a \<le> b" |
|
946 assume bc: "b \<le> c" |
|
947 from ab bc show "a \<le> c" |
|
948 apply (cases a, cases b, cases c) |
|
949 apply (auto intro: ge_game_trans) |
|
950 done |
|
951 } |
|
952 { |
|
953 assume ab: "a \<le> b" |
|
954 from ab show "c + a \<le> c + b" |
|
955 apply (cases a, cases b, cases c) |
|
956 apply (simp add: ge_plus_game_left[symmetric]) |
|
957 done |
|
958 } |
|
959 qed |
|
960 |
|
961 end |