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