--- a/src/HOL/ZF/Games.thy Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/ZF/Games.thy Thu Jun 25 23:33:47 2015 +0200
@@ -418,22 +418,22 @@
proof (induct x rule: wf_induct[OF wf_option_of])
case (1 "g")
show ?case
- proof (auto)
- {case (goal1 y)
- from goal1 have "(y, g) \<in> option_of" by (auto)
+ proof (auto, goals)
+ {case prems: (1 y)
+ from prems have "(y, g) \<in> option_of" by (auto)
with 1 have "ge_game (y, y)" by auto
- with goal1 have "\<not> ge_game (g, y)"
+ with prems have "\<not> ge_game (g, y)"
by (subst ge_game_eq, auto)
- with goal1 show ?case by auto}
+ with prems show ?case by auto}
note right = this
- {case (goal2 y)
- from goal2 have "(y, g) \<in> option_of" by (auto)
+ {case prems: (2 y)
+ from prems have "(y, g) \<in> option_of" by (auto)
with 1 have "ge_game (y, y)" by auto
- with goal2 have "\<not> ge_game (y, g)"
+ with prems have "\<not> ge_game (y, g)"
by (subst ge_game_eq, auto)
- with goal2 show ?case by auto}
+ with prems show ?case by auto}
note left = this
- {case goal3
+ {case 3
from left right show ?case
by (subst ge_game_eq, auto)
}
@@ -462,8 +462,8 @@
proof (induct a rule: induct_game)
case (1 a)
show ?case
- proof (rule allI | rule impI)+
- case (goal1 x y z)
+ proof ((rule allI | rule impI)+, goals)
+ case prems: (1 x y z)
show ?case
proof -
{ fix xr
@@ -471,10 +471,10 @@
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: goal1 a)
+ apply (auto intro: xr lprod_3_1 simp add: prems a)
done
moreover from xr have "\<not> ge_game (y, xr)"
- by (simp add: goal1(2)[simplified ge_game_eq[of x y], rule_format, of xr, simplified 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
@@ -483,10 +483,10 @@
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: goal1 a)
+ apply (auto intro: zl lprod_3_2 simp add: prems a)
done
moreover from zl have "\<not> ge_game (zl, y)"
- by (simp add: goal1(3)[simplified ge_game_eq[of y z], rule_format, of zl, simplified zl])
+ 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
@@ -542,21 +542,18 @@
lemma plus_game_zero_right[simp]: "plus_game G zero_game = G"
proof -
- {
- fix G H
- have "H = zero_game \<longrightarrow> plus_game G H = G "
- proof (induct G H rule: plus_game.induct, rule impI)
- case (goal1 G H)
- note induct_hyp = this[simplified goal1, simplified] and this
- show ?case
- apply (simp only: plus_game.simps[where G=G and H=H])
- apply (simp add: game_ext_eq goal1)
- apply (auto simp add:
- zimage_cong [where f = "\<lambda> g. plus_game g zero_game" and g = "id"]
- induct_hyp)
- done
- qed
- }
+ have "H = zero_game \<longrightarrow> plus_game G H = G " for G H
+ proof (induct G H rule: plus_game.induct, rule impI, goals)
+ 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 = "\<lambda> g. plus_game g zero_game" and g = "id"]
+ induct_hyp)
+ done
+ qed
then show ?thesis by auto
qed
@@ -585,36 +582,33 @@
lemma plus_game_assoc: "plus_game (plus_game F G) H = plus_game F (plus_game G H)"
proof -
- {
- fix a
- have "\<forall> F G H. a = [F, G, H] \<longrightarrow> plus_game (plus_game F G) H = plus_game F (plus_game G H)"
- proof (induct a rule: induct_game, (rule impI | rule allI)+)
- case (goal1 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 = goal1(1)[simplified goal1(2), rule_format]
- have F: "zin opt (options F) \<Longrightarrow> 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) \<Longrightarrow> 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) \<Longrightarrow> 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 \<and> 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
- }
+ have "\<forall>F G H. a = [F, G, H] \<longrightarrow> 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)+, goals)
+ 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) \<Longrightarrow> 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) \<Longrightarrow> 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) \<Longrightarrow> 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 \<and> 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
@@ -632,58 +626,38 @@
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])
- case (goal1 x)
- { fix y
- assume "zin y (options x)"
- then have "eq_game (plus_game y (neg_game y)) zero_game"
- by (auto simp add: goal1)
- }
- note ihyp = this
- {
- fix y
- assume y: "zin y (right_options x)"
- have "\<not> (ge_game (zero_game, plus_game y (neg_game x)))"
- 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
- }
- note case1 = this
- {
- fix y
- assume y: "zin y (left_options x)"
- have "\<not> (ge_game (zero_game, plus_game x (neg_game 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
- }
- note case2 = this
- {
- fix y
- assume y: "zin y (left_options x)"
- have "\<not> (ge_game (plus_game y (neg_game x), zero_game))"
- 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
- }
- note case3 = this
- {
- fix y
- assume y: "zin y (right_options x)"
- have "\<not> (ge_game (plus_game x (neg_game y), zero_game))"
- 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
- }
- note case4 = this
+proof (induct x rule: wf_induct[OF wf_option_of], goals)
+ 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: "\<not> (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: "\<not> (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: "\<not> (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: "\<not> (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"])
@@ -695,112 +669,109 @@
lemma ge_plus_game_left: "ge_game (y,z) = ge_game (plus_game x y, plus_game x z)"
proof -
- { fix a
- have "\<forall> x y z. a = [x,y,z] \<longrightarrow> ge_game (y,z) = ge_game (plus_game x y, plus_game x z)"
- proof (induct a rule: induct_game, (rule impI | rule allI)+)
- case (goal1 a x y z)
- note induct_hyp = goal1(1)[rule_format, simplified goal1(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 "\<not> (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 "\<not> (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 "\<not> (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 "\<not> (ge_game (zl, y))"
- apply (subst goal1(1)[rule_format, where y="[x, zl, y]", of "x" "zl" "y"])
- apply (simp_all add: goal1(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)
+ have "\<forall>x y z. a = [x,y,z] \<longrightarrow> 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)+, goals)
+ 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 "\<not> (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 "\<not> (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
- 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: "\<not> (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)
+ }
+ note yr = this
+ { fix zl
+ assume zl: "zin zl (left_options z)"
+ from hyp have "\<not> (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 "\<not> (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
- 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: "\<not> (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)"
+ }
+ note zl = this
+ show "ge_game (y, 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)
+ 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: "\<not> (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: "\<not> (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 left_imp_right = this
- show ?case by (auto intro: right_imp_left left_imp_right)
- qed
- }
- note a = this[of "[x, y, z]"]
- then show ?thesis 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)"
@@ -808,34 +779,31 @@
lemma ge_neg_game: "ge_game (neg_game x, neg_game y) = ge_game (y, x)"
proof -
- { fix a
- have "\<forall> x y. a = [x, y] \<longrightarrow> ge_game (neg_game x, neg_game y) = ge_game (y, x)"
- proof (induct a rule: induct_game, (rule impI | rule allI)+)
- case (goal1 a x y)
- note ihyp = goal1(1)[rule_format, simplified goal1(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
- }
- note a = this[of "[x,y]"]
- then show ?thesis by blast
+ have "\<forall>x y. a = [x, y] \<longrightarrow> ge_game (neg_game x, neg_game y) = ge_game (y, x)" for a
+ proof (induct a rule: induct_game, (rule impI | rule allI)+, goals)
+ 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
@@ -974,4 +942,3 @@
qed
end
-