19203
|
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
|