(* Title: HOL/ZF/Games.thy
Author: Steven Obua
An application of HOLZF: Partizan Games. See "Partizan Games in
Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan
*)
theory Games
imports MainZF
begin
definition fixgames :: "ZF set \ ZF set" where
"fixgames A \ { Opair l r | l r. explode l \ A & explode r \ A}"
definition games_lfp :: "ZF set" where
"games_lfp \ lfp fixgames"
definition games_gfp :: "ZF set" where
"games_gfp \ gfp fixgames"
lemma mono_fixgames: "mono (fixgames)"
apply (auto simp add: mono_def fixgames_def)
apply (rule_tac x=l in exI)
apply (rule_tac x=r in exI)
apply auto
done
lemma games_lfp_unfold: "games_lfp = fixgames games_lfp"
by (auto simp add: def_lfp_unfold games_lfp_def mono_fixgames)
lemma games_gfp_unfold: "games_gfp = fixgames games_gfp"
by (auto simp add: def_gfp_unfold games_gfp_def mono_fixgames)
lemma games_lfp_nonempty: "Opair Empty Empty \ games_lfp"
proof -
have "fixgames {} \ games_lfp"
apply (subst games_lfp_unfold)
apply (simp add: mono_fixgames[simplified mono_def, rule_format])
done
moreover have "fixgames {} = {Opair Empty Empty}"
by (simp add: fixgames_def explode_Empty)
finally show ?thesis
by auto
qed
definition left_option :: "ZF \ ZF \ bool" where
"left_option g opt \ (Elem opt (Fst g))"
definition right_option :: "ZF \ ZF \ bool" where
"right_option g opt \ (Elem opt (Snd g))"
definition is_option_of :: "(ZF * ZF) set" where
"is_option_of \ { (opt, g) | opt g. g \ games_gfp \ (left_option g opt \ right_option g opt) }"
lemma games_lfp_subset_gfp: "games_lfp \ games_gfp"
proof -
have "games_lfp \ fixgames games_lfp"
by (simp add: games_lfp_unfold[symmetric])
then show ?thesis
by (simp add: games_gfp_def gfp_upperbound)
qed
lemma games_option_stable:
assumes fixgames: "games = fixgames games"
and g: "g \ games"
and opt: "left_option g opt \ right_option g opt"
shows "opt \ games"
proof -
from g fixgames have "g \ fixgames games" by auto
then have "\ l r. g = Opair l r \ explode l \ games \ explode r \ games"
by (simp add: fixgames_def)
then obtain l where "\ r. g = Opair l r \ explode l \ games \ explode r \ games" ..
then obtain r where lr: "g = Opair l r \ explode l \ games \ explode r \ games" ..
with opt show ?thesis
by (auto intro: Elem_explode_in simp add: left_option_def right_option_def Fst Snd)
qed
lemma option2elem: "(opt,g) \ is_option_of \ \ u v. Elem opt u \ Elem u v \ Elem v g"
apply (simp add: is_option_of_def)
apply (subgoal_tac "(g \ games_gfp) = (g \ (fixgames games_gfp))")
prefer 2
apply (simp add: games_gfp_unfold[symmetric])
apply (auto simp add: fixgames_def left_option_def right_option_def Fst Snd)
apply (rule_tac x=l in exI, insert Elem_Opair_exists, blast)
apply (rule_tac x=r in exI, insert Elem_Opair_exists, blast)
done
lemma is_option_of_subset_is_Elem_of: "is_option_of \ (is_Elem_of\<^sup>+)"
proof -
{
fix opt
fix g
assume "(opt, g) \ is_option_of"
then have "\ u v. (opt, u) \ (is_Elem_of\<^sup>+) \ (u,v) \ (is_Elem_of\<^sup>+) \ (v,g) \ (is_Elem_of\<^sup>+)"
apply -
apply (drule option2elem)
apply (auto simp add: r_into_trancl' is_Elem_of_def)
done
then have "(opt, g) \ (is_Elem_of\<^sup>+)"
by (blast intro: trancl_into_rtrancl trancl_rtrancl_trancl)
}
then show ?thesis by auto
qed
lemma wfzf_is_option_of: "wfzf is_option_of"
proof -
have "wfzf (is_Elem_of\<^sup>+)" by (simp add: wfzf_trancl wfzf_is_Elem_of)
then show ?thesis
apply (rule wfzf_subset)
apply (rule is_option_of_subset_is_Elem_of)
done
qed
lemma games_gfp_imp_lfp: "g \ games_gfp \ g \ games_lfp"
proof -
have unfold_gfp: "\ x. x \ games_gfp \ x \ (fixgames games_gfp)"
by (simp add: games_gfp_unfold[symmetric])
have unfold_lfp: "\ x. (x \ games_lfp) = (x \ (fixgames games_lfp))"
by (simp add: games_lfp_unfold[symmetric])
show ?thesis
apply (rule wf_induct[OF wfzf_implies_wf[OF wfzf_is_option_of]])
apply (auto simp add: is_option_of_def)
apply (drule_tac unfold_gfp)
apply (simp add: fixgames_def)
apply (auto simp add: left_option_def Fst right_option_def Snd)
apply (subgoal_tac "explode l \ games_lfp")
apply (subgoal_tac "explode r \ games_lfp")
apply (subst unfold_lfp)
apply (auto simp add: fixgames_def)
apply (simp_all add: explode_Elem Elem_explode_in)
done
qed
theorem games_lfp_eq_gfp: "games_lfp = games_gfp"
apply (auto simp add: games_gfp_imp_lfp)
apply (insert games_lfp_subset_gfp)
apply auto
done
theorem unique_games: "(g = fixgames g) = (g = games_lfp)"
proof -
{
fix g
assume g: "g = fixgames g"
from g have "fixgames g \ g" by auto
then have l:"games_lfp \ g"
by (simp add: games_lfp_def lfp_lowerbound)
from g have "g \ fixgames g" by auto
then have u:"g \ games_gfp"
by (simp add: games_gfp_def gfp_upperbound)
from l u games_lfp_eq_gfp[symmetric] have "g = games_lfp"
by auto
}
note games = this
show ?thesis
apply (rule iffI)
apply (erule games)
apply (simp add: games_lfp_unfold[symmetric])
done
qed
lemma games_lfp_option_stable:
assumes g: "g \ games_lfp"
and opt: "left_option g opt \ right_option g opt"
shows "opt \ games_lfp"
apply (rule games_option_stable[where g=g])
apply (simp add: games_lfp_unfold[symmetric])
apply (simp_all add: assms)
done
lemma is_option_of_imp_games:
assumes hyp: "(opt, g) \ is_option_of"
shows "opt \ games_lfp \ g \ games_lfp"
proof -
from hyp have g_game: "g \ games_lfp"
by (simp add: is_option_of_def games_lfp_eq_gfp)
from hyp have "left_option g opt \ right_option g opt"
by (auto simp add: is_option_of_def)
with g_game games_lfp_option_stable[OF g_game, OF this] show ?thesis
by auto
qed
lemma games_lfp_represent: "x \ games_lfp \ \ l r. x = Opair l r"
apply (rule exI[where x="Fst x"])
apply (rule exI[where x="Snd x"])
apply (subgoal_tac "x \ (fixgames games_lfp)")
apply (simp add: fixgames_def)
apply (auto simp add: Fst Snd)
apply (simp add: games_lfp_unfold[symmetric])
done
definition "game = games_lfp"
typedef game = game
unfolding game_def by (blast intro: games_lfp_nonempty)
definition left_options :: "game \ game zet" where
"left_options g \ zimage Abs_game (zexplode (Fst (Rep_game g)))"
definition right_options :: "game \ game zet" where
"right_options g \ zimage Abs_game (zexplode (Snd (Rep_game g)))"
definition options :: "game \ game zet" where
"options g \ zunion (left_options g) (right_options g)"
definition Game :: "game zet \ game zet \ game" where
"Game L R \ Abs_game (Opair (zimplode (zimage Rep_game L)) (zimplode (zimage Rep_game R)))"
lemma Repl_Rep_game_Abs_game: "\ e. Elem e z \ e \ games_lfp \ Repl z (Rep_game o Abs_game) = z"
apply (subst Ext)
apply (simp add: Repl)
apply auto
apply (subst Abs_game_inverse, simp_all add: game_def)
apply (rule_tac x=za in exI)
apply (subst Abs_game_inverse, simp_all add: game_def)
done
lemma game_split: "g = Game (left_options g) (right_options g)"
proof -
have "\ l r. Rep_game g = Opair l r"
apply (insert Rep_game[of g])
apply (simp add: game_def games_lfp_represent)
done
then obtain l r where lr: "Rep_game g = Opair l r" by auto
have partizan_g: "Rep_game g \ games_lfp"
apply (insert Rep_game[of g])
apply (simp add: game_def)
done
have "\ e. Elem e l \ left_option (Rep_game g) e"
by (simp add: lr left_option_def Fst)
then have partizan_l: "\ e. Elem e l \ e \ games_lfp"
apply auto
apply (rule games_lfp_option_stable[where g="Rep_game g", OF partizan_g])
apply auto
done
have "\ e. Elem e r \ right_option (Rep_game g) e"
by (simp add: lr right_option_def Snd)
then have partizan_r: "\ e. Elem e r \ e \ games_lfp"
apply auto
apply (rule games_lfp_option_stable[where g="Rep_game g", OF partizan_g])
apply auto
done
let ?L = "zimage (Abs_game) (zexplode l)"
let ?R = "zimage (Abs_game) (zexplode r)"
have L:"?L = left_options g"
by (simp add: left_options_def lr Fst)
have R:"?R = right_options g"
by (simp add: right_options_def lr Snd)
have "g = Game ?L ?R"
apply (simp add: Game_def Rep_game_inject[symmetric] comp_zimage_eq zimage_zexplode_eq zimplode_zexplode)
apply (simp add: Repl_Rep_game_Abs_game partizan_l partizan_r)
apply (subst Abs_game_inverse)
apply (simp_all add: lr[symmetric] Rep_game)
done
then show ?thesis
by (simp add: L R)
qed
lemma Opair_in_games_lfp:
assumes l: "explode l \ games_lfp"
and r: "explode r \ games_lfp"
shows "Opair l r \ games_lfp"
proof -
note f = unique_games[of games_lfp, simplified]
show ?thesis
apply (subst f)
apply (simp add: fixgames_def)
apply (rule exI[where x=l])
apply (rule exI[where x=r])
apply (auto simp add: l r)
done
qed
lemma left_options[simp]: "left_options (Game l r) = l"
apply (simp add: left_options_def Game_def)
apply (subst Abs_game_inverse)
apply (simp add: game_def)
apply (rule Opair_in_games_lfp)
apply (auto simp add: explode_Elem Elem_zimplode zimage_iff Rep_game[simplified game_def])
apply (simp add: Fst zexplode_zimplode comp_zimage_eq)
apply (simp add: zet_ext_eq zimage_iff Rep_game_inverse)
done
lemma right_options[simp]: "right_options (Game l r) = r"
apply (simp add: right_options_def Game_def)
apply (subst Abs_game_inverse)
apply (simp add: game_def)
apply (rule Opair_in_games_lfp)
apply (auto simp add: explode_Elem Elem_zimplode zimage_iff Rep_game[simplified game_def])
apply (simp add: Snd zexplode_zimplode comp_zimage_eq)
apply (simp add: zet_ext_eq zimage_iff Rep_game_inverse)
done
lemma Game_ext: "(Game l1 r1 = Game l2 r2) = ((l1 = l2) \ (r1 = r2))"
apply auto
apply (subst left_options[where l=l1 and r=r1,symmetric])
apply (subst left_options[where l=l2 and r=r2,symmetric])
apply simp
apply (subst right_options[where l=l1 and r=r1,symmetric])
apply (subst right_options[where l=l2 and r=r2,symmetric])
apply simp
done
definition option_of :: "(game * game) set" where
"option_of \ image (\ (option, g). (Abs_game option, Abs_game g)) is_option_of"
lemma option_to_is_option_of: "((option, g) \ option_of) = ((Rep_game option, Rep_game g) \ is_option_of)"
apply (auto simp add: option_of_def)
apply (subst Abs_game_inverse)
apply (simp add: is_option_of_imp_games game_def)
apply (subst Abs_game_inverse)
apply (simp add: is_option_of_imp_games game_def)
apply simp
apply (auto simp add: Bex_def image_def)
apply (rule exI[where x="Rep_game option"])
apply (rule exI[where x="Rep_game g"])
apply (simp add: Rep_game_inverse)
done
lemma wf_is_option_of: "wf is_option_of"
apply (rule wfzf_implies_wf)
apply (simp add: wfzf_is_option_of)
done
lemma wf_option_of[simp, intro]: "wf option_of"
proof -
have option_of: "option_of = inv_image is_option_of Rep_game"
apply (rule set_eqI)
apply (case_tac "x")
by (simp add: option_to_is_option_of)
show ?thesis
apply (simp add: option_of)
apply (auto intro: wf_is_option_of)
done
qed
lemma right_option_is_option[simp, intro]: "zin x (right_options g) \ zin x (options g)"
by (simp add: options_def zunion)
lemma left_option_is_option[simp, intro]: "zin x (left_options g) \ zin x (options g)"
by (simp add: options_def zunion)
lemma zin_options[simp, intro]: "zin x (options g) \ (x, g) \ option_of"
apply (simp add: options_def zunion left_options_def right_options_def option_of_def
image_def is_option_of_def zimage_iff zin_zexplode_eq)
apply (cases g)
apply (cases x)
apply (auto simp add: Abs_game_inverse games_lfp_eq_gfp[symmetric] game_def
right_option_def[symmetric] left_option_def[symmetric])
done
function
neg_game :: "game \ game"
where
[simp del]: "neg_game g = Game (zimage neg_game (right_options g)) (zimage neg_game (left_options g))"
by auto
termination by (relation "option_of") auto
lemma "neg_game (neg_game g) = g"
apply (induct g rule: neg_game.induct)
apply (subst neg_game.simps)+
apply (simp add: comp_zimage_eq)
apply (subgoal_tac "zimage (neg_game o neg_game) (left_options g) = left_options g")
apply (subgoal_tac "zimage (neg_game o neg_game) (right_options g) = right_options g")
apply (auto simp add: game_split[symmetric])
apply (auto simp add: zet_ext_eq zimage_iff)
done
function
ge_game :: "(game * game) \ bool"
where
[simp del]: "ge_game (G, H) = (\ x. if zin x (right_options G) then (
if zin x (left_options H) then \<not> (ge_game (H, x) \<or> (ge_game (x, G)))
else \<not> (ge_game (H, x)))
else (if zin x (left_options H) then \<not> (ge_game (x, G)) else True))"
by auto
termination by (relation "(gprod_2_1 option_of)")
(simp, auto simp: gprod_2_1_def)
lemma ge_game_eq: "ge_game (G, H) = (\ x. (zin x (right_options G) \ \ ge_game (H, x)) \ (zin x (left_options H) \ \ ge_game (x, G)))"
apply (subst ge_game.simps[where G=G and H=H])
apply (auto)
done
lemma ge_game_leftright_refl[rule_format]:
"\ y. (zin y (right_options x) \ \ ge_game (x, y)) \ (zin y (left_options x) \ \ (ge_game (y, x))) \ ge_game (x, x)"
proof (induct x rule: wf_induct[OF wf_option_of])
case (1 "g")
{
fix y
assume y: "zin y (right_options g)"
have "\ ge_game (g, y)"
proof -
have "(y, g) \ option_of" by (auto intro: y)
with 1 have "ge_game (y, y)" by auto
with y show ?thesis by (subst ge_game_eq, auto)
qed
}
note right = this
{
fix y
assume y: "zin y (left_options g)"
have "\ ge_game (y, g)"
proof -
have "(y, g) \ option_of" by (auto intro: y)
with 1 have "ge_game (y, y)" by auto
with y show ?thesis by (subst ge_game_eq, auto)
qed
}
note left = this
from left right show ?case
by (auto, subst ge_game_eq, auto)
qed
lemma ge_game_refl: "ge_game (x,x)" by (simp add: ge_game_leftright_refl)
lemma "\ y. (zin y (right_options x) \ \ ge_game (x, y)) \ (zin y (left_options x) \ \ (ge_game (y, x))) \ ge_game (x, x)"
proof (induct x rule: wf_induct[OF wf_option_of])
case (1 "g")
show ?case
proof (auto, goal_cases)
{case prems: (1 y)
from prems have "(y, g) \ option_of" by (auto)
with 1 have "ge_game (y, y)" by auto
with prems have "\ ge_game (g, y)"
by (subst ge_game_eq, auto)
with prems show ?case by auto}
note right = this
{case prems: (2 y)
from prems have "(y, g) \ option_of" by (auto)
with 1 have "ge_game (y, y)" by auto
with prems have "\ ge_game (y, g)"
by (subst ge_game_eq, auto)
with prems show ?case by auto}
note left = this
{case 3
from left right show ?case
by (subst ge_game_eq, auto)
}
qed
qed
definition eq_game :: "game \ game \ bool" where
"eq_game G H \ ge_game (G, H) \ ge_game (H, G)"
lemma eq_game_sym: "(eq_game G H) = (eq_game H G)"
by (auto simp add: eq_game_def)
lemma eq_game_refl: "eq_game G G"
by (simp add: ge_game_refl eq_game_def)
lemma induct_game: "(\x. \y. (y, x) \ lprod option_of \ P y \ P x) \ P a"
by (erule wf_induct[OF wf_lprod[OF wf_option_of]])
lemma ge_game_trans:
assumes "ge_game (x, y)" "ge_game (y, z)"
shows "ge_game (x, z)"
proof -
{
fix a
have "\ x y z. a = [x,y,z] \ ge_game (x,y) \ ge_game (y,z) \ ge_game (x, z)"
proof (induct a rule: induct_game)
case (1 a)
show ?case
proof ((rule allI | rule impI)+, goal_cases)
case prems: (1 x y z)
show ?case
proof -
{ fix xr
assume xr:"zin xr (right_options x)"
assume a: "ge_game (z, xr)"
have "ge_game (y, xr)"
apply (rule 1[rule_format, where y="[y,z,xr]"])
apply (auto intro: xr lprod_3_1 simp add: prems a)
done
moreover from xr have "\ ge_game (y, xr)"
by (simp add: prems(2)[simplified ge_game_eq[of x y], rule_format, of xr, simplified xr])
ultimately have "False" by auto
}
note xr = this
{ fix zl
assume zl:"zin zl (left_options z)"
assume a: "ge_game (zl, x)"
have "ge_game (zl, y)"
apply (rule 1[rule_format, where y="[zl,x,y]"])
apply (auto intro: zl lprod_3_2 simp add: prems a)
done
moreover from zl have "\ ge_game (zl, y)"
by (simp add: prems(3)[simplified ge_game_eq[of y z], rule_format, of zl, simplified zl])
ultimately have "False" by auto
}
note zl = this
show ?thesis
by (auto simp add: ge_game_eq[of x z] intro: xr zl)
qed
qed
qed
}
note trans = this[of "[x, y, z]", simplified, rule_format]
with assms show ?thesis by blast
qed
lemma eq_game_trans: "eq_game a b \ eq_game b c \ eq_game a c"
by (auto simp add: eq_game_def intro: ge_game_trans)
definition zero_game :: game
where "zero_game \ Game zempty zempty"
function
plus_game :: "game \ game \ game"
where
[simp del]: "plus_game G H = Game (zunion (zimage (\ g. plus_game g H) (left_options G))
(zimage (\<lambda> h. plus_game G h) (left_options H)))
(zunion (zimage (\<lambda> g. plus_game g H) (right_options G))
(zimage (\<lambda> h. plus_game G h) (right_options H)))"
by auto
termination by (relation "gprod_2_2 option_of")
(simp, auto simp: gprod_2_2_def)
lemma plus_game_comm: "plus_game G H = plus_game H G"
proof (induct G H rule: plus_game.induct)
case (1 G H)
show ?case
by (auto simp add:
plus_game.simps[where G=G and H=H]
plus_game.simps[where G=H and H=G]
Game_ext zet_ext_eq zunion zimage_iff 1)
qed
lemma game_ext_eq: "(G = H) = (left_options G = left_options H \ right_options G = right_options H)"
proof -
have "(G = H) = (Game (left_options G) (right_options G) = Game (left_options H) (right_options H))"
by (simp add: game_split[symmetric])
then show ?thesis by auto
qed
lemma left_zero_game[simp]: "left_options (zero_game) = zempty"
by (simp add: zero_game_def)
lemma right_zero_game[simp]: "right_options (zero_game) = zempty"
by (simp add: zero_game_def)
lemma plus_game_zero_right[simp]: "plus_game G zero_game = G"
proof -
have "H = zero_game \ plus_game G H = G " for G H
proof (induct G H rule: plus_game.induct, rule impI, goal_cases)
case prems: (1 G H)
note induct_hyp = this[simplified prems, simplified] and this
show ?case
apply (simp only: plus_game.simps[where G=G and H=H])
apply (simp add: game_ext_eq prems)
apply (auto simp add:
zimage_cong [where f = "\ g. plus_game g zero_game" and g = "id"]
induct_hyp)
done
qed
then show ?thesis by auto
qed
lemma plus_game_zero_left: "plus_game zero_game G = G"
by (simp add: plus_game_comm)
lemma left_imp_options[simp]: "zin opt (left_options g) \ zin opt (options g)"
by (simp add: options_def zunion)
lemma right_imp_options[simp]: "zin opt (right_options g) \ zin opt (options g)"
by (simp add: options_def zunion)
lemma left_options_plus:
"left_options (plus_game u v) = zunion (zimage (\g. plus_game g v) (left_options u)) (zimage (\h. plus_game u h) (left_options v))"
by (subst plus_game.simps, simp)
lemma right_options_plus:
"right_options (plus_game u v) = zunion (zimage (\g. plus_game g v) (right_options u)) (zimage (\h. plus_game u h) (right_options v))"
by (subst plus_game.simps, simp)
lemma left_options_neg: "left_options (neg_game u) = zimage neg_game (right_options u)"
by (subst neg_game.simps, simp)
lemma right_options_neg: "right_options (neg_game u) = zimage neg_game (left_options u)"
by (subst neg_game.simps, simp)
lemma plus_game_assoc: "plus_game (plus_game F G) H = plus_game F (plus_game G H)"
proof -
have "\F G H. a = [F, G, H] \ plus_game (plus_game F G) H = plus_game F (plus_game G H)" for a
proof (induct a rule: induct_game, (rule impI | rule allI)+, goal_cases)
case prems: (1 x F G H)
let ?L = "plus_game (plus_game F G) H"
let ?R = "plus_game F (plus_game G H)"
note options_plus = left_options_plus right_options_plus
{
fix opt
note hyp = prems(1)[simplified prems(2), rule_format]
have F: "zin opt (options F) \ plus_game (plus_game opt G) H = plus_game opt (plus_game G H)"
by (blast intro: hyp lprod_3_3)
have G: "zin opt (options G) \ plus_game (plus_game F opt) H = plus_game F (plus_game opt H)"
by (blast intro: hyp lprod_3_4)
have H: "zin opt (options H) \ plus_game (plus_game F G) opt = plus_game F (plus_game G opt)"
by (blast intro: hyp lprod_3_5)
note F and G and H
}
note induct_hyp = this
have "left_options ?L = left_options ?R \ right_options ?L = right_options ?R"
by (auto simp add:
plus_game.simps[where G="plus_game F G" and H=H]
plus_game.simps[where G="F" and H="plus_game G H"]
zet_ext_eq zunion zimage_iff options_plus
induct_hyp left_imp_options right_imp_options)
then show ?case
by (simp add: game_ext_eq)
qed
then show ?thesis by auto
qed
lemma neg_plus_game: "neg_game (plus_game G H) = plus_game (neg_game G) (neg_game H)"
proof (induct G H rule: plus_game.induct)
case (1 G H)
note opt_ops =
left_options_plus right_options_plus
left_options_neg right_options_neg
show ?case
by (auto simp add: opt_ops
neg_game.simps[of "plus_game G H"]
plus_game.simps[of "neg_game G" "neg_game H"]
Game_ext zet_ext_eq zunion zimage_iff 1)
qed
lemma eq_game_plus_inverse: "eq_game (plus_game x (neg_game x)) zero_game"
proof (induct x rule: wf_induct[OF wf_option_of], goal_cases)
case prems: (1 x)
then have ihyp: "eq_game (plus_game y (neg_game y)) zero_game" if "zin y (options x)" for y
using that by (auto simp add: prems)
have case1: "\ (ge_game (zero_game, plus_game y (neg_game x)))"
if y: "zin y (right_options x)" for y
apply (subst ge_game.simps, simp)
apply (rule exI[where x="plus_game y (neg_game y)"])
apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
apply (auto simp add: left_options_plus left_options_neg zunion zimage_iff intro: y)
done
have case2: "\ (ge_game (zero_game, plus_game x (neg_game y)))"
if y: "zin y (left_options x)" for y
apply (subst ge_game.simps, simp)
apply (rule exI[where x="plus_game y (neg_game y)"])
apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
apply (auto simp add: left_options_plus zunion zimage_iff intro: y)
done
have case3: "\ (ge_game (plus_game y (neg_game x), zero_game))"
if y: "zin y (left_options x)" for y
apply (subst ge_game.simps, simp)
apply (rule exI[where x="plus_game y (neg_game y)"])
apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
apply (auto simp add: right_options_plus right_options_neg zunion zimage_iff intro: y)
done
have case4: "\ (ge_game (plus_game x (neg_game y), zero_game))"
if y: "zin y (right_options x)" for y
apply (subst ge_game.simps, simp)
apply (rule exI[where x="plus_game y (neg_game y)"])
apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
apply (auto simp add: right_options_plus zunion zimage_iff intro: y)
done
show ?case
apply (simp add: eq_game_def)
apply (simp add: ge_game.simps[of "plus_game x (neg_game x)" "zero_game"])
apply (simp add: ge_game.simps[of "zero_game" "plus_game x (neg_game x)"])
apply (simp add: right_options_plus left_options_plus right_options_neg left_options_neg zunion zimage_iff)
apply (auto simp add: case1 case2 case3 case4)
done
qed
lemma ge_plus_game_left: "ge_game (y,z) = ge_game (plus_game x y, plus_game x z)"
proof -
have "\x y z. a = [x,y,z] \ ge_game (y,z) = ge_game (plus_game x y, plus_game x z)" for a
proof (induct a rule: induct_game, (rule impI | rule allI)+, goal_cases)
case prems: (1 a x y z)
note induct_hyp = prems(1)[rule_format, simplified prems(2)]
{
assume hyp: "ge_game(plus_game x y, plus_game x z)"
have "ge_game (y, z)"
proof -
{ fix yr
assume yr: "zin yr (right_options y)"
from hyp have "\ (ge_game (plus_game x z, plus_game x yr))"
by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
right_options_plus zunion zimage_iff intro: yr)
then have "\ (ge_game (z, yr))"
apply (subst induct_hyp[where y="[x, z, yr]", of "x" "z" "yr"])
apply (simp_all add: yr lprod_3_6)
done
}
note yr = this
{ fix zl
assume zl: "zin zl (left_options z)"
from hyp have "\ (ge_game (plus_game x zl, plus_game x y))"
by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
left_options_plus zunion zimage_iff intro: zl)
then have "\ (ge_game (zl, y))"
apply (subst prems(1)[rule_format, where y="[x, zl, y]", of "x" "zl" "y"])
apply (simp_all add: prems(2) zl lprod_3_7)
done
}
note zl = this
show "ge_game (y, z)"
apply (subst ge_game_eq)
apply (auto simp add: yr zl)
done
qed
}
note right_imp_left = this
{
assume yz: "ge_game (y, z)"
{
fix x'
assume x': "zin x' (right_options x)"
assume hyp: "ge_game (plus_game x z, plus_game x' y)"
then have n: "\ (ge_game (plus_game x' y, plus_game x' z))"
by (auto simp add: ge_game_eq[of "plus_game x z" "plus_game x' y"]
right_options_plus zunion zimage_iff intro: x')
have t: "ge_game (plus_game x' y, plus_game x' z)"
apply (subst induct_hyp[symmetric])
apply (auto intro: lprod_3_3 x' yz)
done
from n t have "False" by blast
}
note case1 = this
{
fix x'
assume x': "zin x' (left_options x)"
assume hyp: "ge_game (plus_game x' z, plus_game x y)"
then have n: "\ (ge_game (plus_game x' y, plus_game x' z))"
by (auto simp add: ge_game_eq[of "plus_game x' z" "plus_game x y"]
left_options_plus zunion zimage_iff intro: x')
have t: "ge_game (plus_game x' y, plus_game x' z)"
apply (subst induct_hyp[symmetric])
apply (auto intro: lprod_3_3 x' yz)
done
from n t have "False" by blast
}
note case3 = this
{
fix y'
assume y': "zin y' (right_options y)"
assume hyp: "ge_game (plus_game x z, plus_game x y')"
then have "ge_game(z, y')"
apply (subst induct_hyp[of "[x, z, y']" "x" "z" "y'"])
apply (auto simp add: hyp lprod_3_6 y')
done
with yz have "ge_game (y, y')"
by (blast intro: ge_game_trans)
with y' have "False" by (auto simp add: ge_game_leftright_refl)
}
note case2 = this
{
fix z'
assume z': "zin z' (left_options z)"
assume hyp: "ge_game (plus_game x z', plus_game x y)"
then have "ge_game(z', y)"
apply (subst induct_hyp[of "[x, z', y]" "x" "z'" "y"])
apply (auto simp add: hyp lprod_3_7 z')
done
with yz have "ge_game (z', z)"
by (blast intro: ge_game_trans)
with z' have "False" by (auto simp add: ge_game_leftright_refl)
}
note case4 = this
have "ge_game(plus_game x y, plus_game x z)"
apply (subst ge_game_eq)
apply (auto simp add: right_options_plus left_options_plus zunion zimage_iff)
apply (auto intro: case1 case2 case3 case4)
done
}
note left_imp_right = this
show ?case by (auto intro: right_imp_left left_imp_right)
qed
from this[of "[x, y, z]"] show ?thesis by blast
qed
lemma ge_plus_game_right: "ge_game (y,z) = ge_game(plus_game y x, plus_game z x)"
by (simp add: ge_plus_game_left plus_game_comm)
lemma ge_neg_game: "ge_game (neg_game x, neg_game y) = ge_game (y, x)"
proof -
have "\x y. a = [x, y] \ ge_game (neg_game x, neg_game y) = ge_game (y, x)" for a
proof (induct a rule: induct_game, (rule impI | rule allI)+, goal_cases)
case prems: (1 a x y)
note ihyp = prems(1)[rule_format, simplified prems(2)]
{ fix xl
assume xl: "zin xl (left_options x)"
have "ge_game (neg_game y, neg_game xl) = ge_game (xl, y)"
apply (subst ihyp)
apply (auto simp add: lprod_2_1 xl)
done
}
note xl = this
{ fix yr
assume yr: "zin yr (right_options y)"
have "ge_game (neg_game yr, neg_game x) = ge_game (x, yr)"
apply (subst ihyp)
apply (auto simp add: lprod_2_2 yr)
done
}
note yr = this
show ?case
by (auto simp add: ge_game_eq[of "neg_game x" "neg_game y"] ge_game_eq[of "y" "x"]
right_options_neg left_options_neg zimage_iff xl yr)
qed
from this[of "[x,y]"] show ?thesis by blast
qed
definition eq_game_rel :: "(game * game) set" where
"eq_game_rel \ { (p, q) . eq_game p q }"
definition "Pg = UNIV//eq_game_rel"
typedef Pg = Pg
unfolding Pg_def by (auto simp add: quotient_def)
lemma equiv_eq_game[simp]: "equiv UNIV eq_game_rel"
by (auto simp add: equiv_def refl_on_def sym_def trans_def eq_game_rel_def
eq_game_sym intro: eq_game_refl eq_game_trans)
instantiation Pg :: "{ord, zero, plus, minus, uminus}"
begin
definition
Pg_zero_def: "0 = Abs_Pg (eq_game_rel `` {zero_game})"
definition
Pg_le_def: "G \ H \ (\ g h. g \ Rep_Pg G \ h \ Rep_Pg H \ ge_game (h, g))"
definition
Pg_less_def: "G < H \ G \ H \ G \ (H::Pg)"
definition
Pg_minus_def: "- G = the_elem (\g \ Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
definition
Pg_plus_def: "G + H = the_elem (\g \ Rep_Pg G. \h \ Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game g h})})"
definition
Pg_diff_def: "G - H = G + (- (H::Pg))"
instance ..
end
lemma Rep_Abs_eq_Pg[simp]: "Rep_Pg (Abs_Pg (eq_game_rel `` {g})) = eq_game_rel `` {g}"
apply (subst Abs_Pg_inverse)
apply (auto simp add: Pg_def quotient_def)
done
lemma char_Pg_le[simp]: "(Abs_Pg (eq_game_rel `` {g}) \ Abs_Pg (eq_game_rel `` {h})) = (ge_game (h, g))"
apply (simp add: Pg_le_def)
apply (auto simp add: eq_game_rel_def eq_game_def intro: ge_game_trans ge_game_refl)
done
lemma char_Pg_eq[simp]: "(Abs_Pg (eq_game_rel `` {g}) = Abs_Pg (eq_game_rel `` {h})) = (eq_game g h)"
apply (simp add: Rep_Pg_inject [symmetric])
apply (subst eq_equiv_class_iff[of UNIV])
apply (simp_all)
apply (simp add: eq_game_rel_def)
done
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})"
proof -
have "(\ g h. {Abs_Pg (eq_game_rel `` {plus_game g h})}) respects2 eq_game_rel"
apply (simp add: congruent2_def)
apply (auto simp add: eq_game_rel_def eq_game_def)
apply (rule_tac y="plus_game a ba" in ge_game_trans)
apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+
apply (rule_tac y="plus_game b aa" in ge_game_trans)
apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+
done
then show ?thesis
by (simp add: Pg_plus_def UN_equiv_class2[OF equiv_eq_game equiv_eq_game])
qed
lemma char_Pg_minus[simp]: "- Abs_Pg (eq_game_rel `` {g}) = Abs_Pg (eq_game_rel `` {neg_game g})"
proof -
have "(\ g. {Abs_Pg (eq_game_rel `` {neg_game g})}) respects eq_game_rel"
apply (simp add: congruent_def)
apply (auto simp add: eq_game_rel_def eq_game_def ge_neg_game)
done
then show ?thesis
by (simp add: Pg_minus_def UN_equiv_class[OF equiv_eq_game])
qed
lemma eq_Abs_Pg[rule_format, cases type: Pg]: "(\ g. z = Abs_Pg (eq_game_rel `` {g}) \ P) \ P"
apply (cases z, simp)
apply (simp add: Rep_Pg_inject[symmetric])
apply (subst Abs_Pg_inverse, simp)
apply (auto simp add: Pg_def quotient_def)
done
instance Pg :: ordered_ab_group_add
proof
fix a b c :: Pg
show "a - b = a + (- b)" by (simp add: Pg_diff_def)
{
assume ab: "a \ b"
assume ba: "b \ a"
from ab ba show "a = b"
apply (cases a, cases b)
apply (simp add: eq_game_def)
done
}
then show "(a < b) = (a \ b \ \ b \ a)" by (auto simp add: Pg_less_def)
show "a + b = b + a"
apply (cases a, cases b)
apply (simp add: eq_game_def plus_game_comm)
done
show "a + b + c = a + (b + c)"
apply (cases a, cases b, cases c)
apply (simp add: eq_game_def plus_game_assoc)
done
show "0 + a = a"
apply (cases a)
apply (simp add: Pg_zero_def plus_game_zero_left)
done
show "- a + a = 0"
apply (cases a)
apply (simp add: Pg_zero_def eq_game_plus_inverse plus_game_comm)
done
show "a \ a"
apply (cases a)
apply (simp add: ge_game_refl)
done
{
assume ab: "a \ b"
assume bc: "b \ c"
from ab bc show "a \ c"
apply (cases a, cases b, cases c)
apply (auto intro: ge_game_trans)
done
}
{
assume ab: "a \ b"
from ab show "c + a \ c + b"
apply (cases a, cases b, cases c)
apply (simp add: ge_plus_game_left[symmetric])
done
}
qed
end
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
