src/HOL/ZF/Games.thy
author wenzelm
Thu May 24 17:25:53 2012 +0200 (2012-05-24)
changeset 47988 e4b69e10b990
parent 46752 e9e7209eb375
child 49834 b27bbb021df1
permissions -rw-r--r--
tuned proofs;
     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 definition fixgames :: "ZF set \<Rightarrow> ZF set" where
    13   "fixgames A \<equiv> { Opair l r | l r. explode l \<subseteq> A & explode r \<subseteq> A}"
    14 
    15 definition games_lfp :: "ZF set" where
    16   "games_lfp \<equiv> lfp fixgames"
    17 
    18 definition games_gfp :: "ZF set" where
    19   "games_gfp \<equiv> gfp fixgames"
    20 
    21 lemma mono_fixgames: "mono (fixgames)"
    22   apply (auto simp add: mono_def fixgames_def)
    23   apply (rule_tac x=l in exI)
    24   apply (rule_tac x=r in exI)
    25   apply auto
    26   done
    27 
    28 lemma games_lfp_unfold: "games_lfp = fixgames games_lfp"
    29   by (auto simp add: def_lfp_unfold games_lfp_def mono_fixgames)
    30 
    31 lemma games_gfp_unfold: "games_gfp = fixgames games_gfp"
    32   by (auto simp add: def_gfp_unfold games_gfp_def mono_fixgames)
    33 
    34 lemma games_lfp_nonempty: "Opair Empty Empty \<in> games_lfp"
    35 proof -
    36   have "fixgames {} \<subseteq> games_lfp" 
    37     apply (subst games_lfp_unfold)
    38     apply (simp add: mono_fixgames[simplified mono_def, rule_format])
    39     done
    40   moreover have "fixgames {} = {Opair Empty Empty}"
    41     by (simp add: fixgames_def explode_Empty)
    42   finally show ?thesis
    43     by auto
    44 qed
    45 
    46 definition left_option :: "ZF \<Rightarrow> ZF \<Rightarrow> bool" where
    47   "left_option g opt \<equiv> (Elem opt (Fst g))"
    48 
    49 definition right_option :: "ZF \<Rightarrow> ZF \<Rightarrow> bool" where
    50   "right_option g opt \<equiv> (Elem opt (Snd g))"
    51 
    52 definition is_option_of :: "(ZF * ZF) set" where
    53   "is_option_of \<equiv> { (opt, g) | opt g. g \<in> games_gfp \<and> (left_option g opt \<or> right_option g opt) }"
    54 
    55 lemma games_lfp_subset_gfp: "games_lfp \<subseteq> games_gfp"
    56 proof -
    57   have "games_lfp \<subseteq> fixgames games_lfp" 
    58     by (simp add: games_lfp_unfold[symmetric])
    59   then show ?thesis
    60     by (simp add: games_gfp_def gfp_upperbound)
    61 qed
    62 
    63 lemma games_option_stable: 
    64   assumes fixgames: "games = fixgames games"
    65   and g: "g \<in> games"
    66   and opt: "left_option g opt \<or> right_option g opt"
    67   shows "opt \<in> games"
    68 proof -
    69   from g fixgames have "g \<in> fixgames games" by auto
    70   then have "\<exists> l r. g = Opair l r \<and> explode l \<subseteq> games \<and> explode r \<subseteq> games"
    71     by (simp add: fixgames_def)
    72   then obtain l where "\<exists> r. g = Opair l r \<and> explode l \<subseteq> games \<and> explode r \<subseteq> games" ..
    73   then obtain r where lr: "g = Opair l r \<and> explode l \<subseteq> games \<and> explode r \<subseteq> games" ..
    74   with opt show ?thesis
    75     by (auto intro: Elem_explode_in simp add: left_option_def right_option_def Fst Snd)
    76 qed
    77     
    78 lemma option2elem: "(opt,g) \<in> is_option_of  \<Longrightarrow> \<exists> u v. Elem opt u \<and> Elem u v \<and> Elem v g"
    79   apply (simp add: is_option_of_def)
    80   apply (subgoal_tac "(g \<in> games_gfp) = (g \<in> (fixgames games_gfp))")
    81   prefer 2
    82   apply (simp add: games_gfp_unfold[symmetric])
    83   apply (auto simp add: fixgames_def left_option_def right_option_def Fst Snd)
    84   apply (rule_tac x=l in exI, insert Elem_Opair_exists, blast)
    85   apply (rule_tac x=r in exI, insert Elem_Opair_exists, blast) 
    86   done
    87 
    88 lemma is_option_of_subset_is_Elem_of: "is_option_of \<subseteq> (is_Elem_of^+)"
    89 proof -
    90   {
    91     fix opt
    92     fix g
    93     assume "(opt, g) \<in> is_option_of"
    94     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^+)" 
    95       apply -
    96       apply (drule option2elem)
    97       apply (auto simp add: r_into_trancl' is_Elem_of_def)
    98       done
    99     then have "(opt, g) \<in> (is_Elem_of^+)"
   100       by (blast intro: trancl_into_rtrancl trancl_rtrancl_trancl)
   101   } 
   102   then show ?thesis by auto
   103 qed
   104 
   105 lemma wfzf_is_option_of: "wfzf is_option_of"
   106 proof - 
   107   have "wfzf (is_Elem_of^+)" by (simp add: wfzf_trancl wfzf_is_Elem_of)
   108   then show ?thesis 
   109     apply (rule wfzf_subset)
   110     apply (rule is_option_of_subset_is_Elem_of)
   111     done
   112   qed
   113   
   114 lemma games_gfp_imp_lfp: "g \<in> games_gfp \<longrightarrow> g \<in> games_lfp"
   115 proof -
   116   have unfold_gfp: "\<And> x. x \<in> games_gfp \<Longrightarrow> x \<in> (fixgames games_gfp)" 
   117     by (simp add: games_gfp_unfold[symmetric])
   118   have unfold_lfp: "\<And> x. (x \<in> games_lfp) = (x \<in> (fixgames games_lfp))"
   119     by (simp add: games_lfp_unfold[symmetric])
   120   show ?thesis
   121     apply (rule wf_induct[OF wfzf_implies_wf[OF wfzf_is_option_of]])
   122     apply (auto simp add: is_option_of_def)
   123     apply (drule_tac unfold_gfp)
   124     apply (simp add: fixgames_def)
   125     apply (auto simp add: left_option_def Fst right_option_def Snd)
   126     apply (subgoal_tac "explode l \<subseteq> games_lfp")
   127     apply (subgoal_tac "explode r \<subseteq> games_lfp")
   128     apply (subst unfold_lfp)
   129     apply (auto simp add: fixgames_def)
   130     apply (simp_all add: explode_Elem Elem_explode_in)
   131     done
   132 qed
   133 
   134 theorem games_lfp_eq_gfp: "games_lfp = games_gfp"
   135   apply (auto simp add: games_gfp_imp_lfp)
   136   apply (insert games_lfp_subset_gfp)
   137   apply auto
   138   done
   139 
   140 theorem unique_games: "(g = fixgames g) = (g = games_lfp)"
   141 proof -
   142   {
   143     fix g 
   144     assume g: "g = fixgames g"
   145     from g have "fixgames g \<subseteq> g" by auto
   146     then have l:"games_lfp \<subseteq> g" 
   147       by (simp add: games_lfp_def lfp_lowerbound)
   148     from g have "g \<subseteq> fixgames g" by auto
   149     then have u:"g \<subseteq> games_gfp" 
   150       by (simp add: games_gfp_def gfp_upperbound)
   151     from l u games_lfp_eq_gfp[symmetric] have "g = games_lfp"
   152       by auto
   153   }
   154   note games = this
   155   show ?thesis
   156     apply (rule iff[rule_format])
   157     apply (erule games)
   158     apply (simp add: games_lfp_unfold[symmetric])
   159     done
   160 qed
   161 
   162 lemma games_lfp_option_stable: 
   163   assumes g: "g \<in> games_lfp"
   164   and opt: "left_option g opt \<or> right_option g opt"
   165   shows "opt \<in> games_lfp"
   166   apply (rule games_option_stable[where g=g])
   167   apply (simp add: games_lfp_unfold[symmetric])
   168   apply (simp_all add: assms)
   169   done
   170 
   171 lemma is_option_of_imp_games:
   172   assumes hyp: "(opt, g) \<in> is_option_of"
   173   shows "opt \<in> games_lfp \<and> g \<in> games_lfp"
   174 proof -
   175   from hyp have g_game: "g \<in> games_lfp" 
   176     by (simp add: is_option_of_def games_lfp_eq_gfp)
   177   from hyp have "left_option g opt \<or> right_option g opt"
   178     by (auto simp add: is_option_of_def)
   179   with g_game games_lfp_option_stable[OF g_game, OF this] show ?thesis
   180     by auto
   181 qed
   182  
   183 lemma games_lfp_represent: "x \<in> games_lfp \<Longrightarrow> \<exists> l r. x = Opair l r"
   184   apply (rule exI[where x="Fst x"])
   185   apply (rule exI[where x="Snd x"])
   186   apply (subgoal_tac "x \<in> (fixgames games_lfp)")
   187   apply (simp add: fixgames_def)
   188   apply (auto simp add: Fst Snd)
   189   apply (simp add: games_lfp_unfold[symmetric])
   190   done
   191 
   192 definition "game = games_lfp"
   193 
   194 typedef (open) game = game
   195   unfolding game_def by (blast intro: games_lfp_nonempty)
   196 
   197 definition left_options :: "game \<Rightarrow> game zet" where
   198   "left_options g \<equiv> zimage Abs_game (zexplode (Fst (Rep_game g)))"
   199 
   200 definition right_options :: "game \<Rightarrow> game zet" where
   201   "right_options g \<equiv> zimage Abs_game (zexplode (Snd (Rep_game g)))"
   202 
   203 definition options :: "game \<Rightarrow> game zet" where
   204   "options g \<equiv> zunion (left_options g) (right_options g)"
   205 
   206 definition Game :: "game zet \<Rightarrow> game zet \<Rightarrow> game" where
   207   "Game L R \<equiv> Abs_game (Opair (zimplode (zimage Rep_game L)) (zimplode (zimage Rep_game R)))"
   208   
   209 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"
   210   apply (subst Ext)
   211   apply (simp add: Repl)
   212   apply auto
   213   apply (subst Abs_game_inverse, simp_all add: game_def)
   214   apply (rule_tac x=za in exI)
   215   apply (subst Abs_game_inverse, simp_all add: game_def)
   216   done
   217 
   218 lemma game_split: "g = Game (left_options g) (right_options g)"
   219 proof -
   220   have "\<exists> l r. Rep_game g = Opair l r"
   221     apply (insert Rep_game[of g])
   222     apply (simp add: game_def games_lfp_represent)
   223     done
   224   then obtain l r where lr: "Rep_game g = Opair l r" by auto
   225   have partizan_g: "Rep_game g \<in> games_lfp" 
   226     apply (insert Rep_game[of g])
   227     apply (simp add: game_def)
   228     done
   229   have "\<forall> e. Elem e l \<longrightarrow> left_option (Rep_game g) e"
   230     by (simp add: lr left_option_def Fst)
   231   then have partizan_l: "\<forall> e. Elem e l \<longrightarrow> e \<in> games_lfp"
   232     apply auto
   233     apply (rule games_lfp_option_stable[where g="Rep_game g", OF partizan_g])
   234     apply auto
   235     done
   236   have "\<forall> e. Elem e r \<longrightarrow> right_option (Rep_game g) e"
   237     by (simp add: lr right_option_def Snd)
   238   then have partizan_r: "\<forall> e. Elem e r \<longrightarrow> e \<in> games_lfp"
   239     apply auto
   240     apply (rule games_lfp_option_stable[where g="Rep_game g", OF partizan_g])
   241     apply auto
   242     done   
   243   let ?L = "zimage (Abs_game) (zexplode l)"
   244   let ?R = "zimage (Abs_game) (zexplode r)"
   245   have L:"?L = left_options g"
   246     by (simp add: left_options_def lr Fst)
   247   have R:"?R = right_options g"
   248     by (simp add: right_options_def lr Snd)
   249   have "g = Game ?L ?R"
   250     apply (simp add: Game_def Rep_game_inject[symmetric] comp_zimage_eq zimage_zexplode_eq zimplode_zexplode)
   251     apply (simp add: Repl_Rep_game_Abs_game partizan_l partizan_r)
   252     apply (subst Abs_game_inverse)
   253     apply (simp_all add: lr[symmetric] Rep_game) 
   254     done
   255   then show ?thesis
   256     by (simp add: L R)
   257 qed
   258 
   259 lemma Opair_in_games_lfp: 
   260   assumes l: "explode l \<subseteq> games_lfp"
   261   and r: "explode r \<subseteq> games_lfp"
   262   shows "Opair l r \<in> games_lfp"
   263 proof -
   264   note f = unique_games[of games_lfp, simplified]
   265   show ?thesis
   266     apply (subst f)
   267     apply (simp add: fixgames_def)
   268     apply (rule exI[where x=l])
   269     apply (rule exI[where x=r])
   270     apply (auto simp add: l r)
   271     done
   272 qed
   273 
   274 lemma left_options[simp]: "left_options (Game l r) = l"
   275   apply (simp add: left_options_def Game_def)
   276   apply (subst Abs_game_inverse)
   277   apply (simp add: game_def)
   278   apply (rule Opair_in_games_lfp)
   279   apply (auto simp add: explode_Elem Elem_zimplode zimage_iff Rep_game[simplified game_def])
   280   apply (simp add: Fst zexplode_zimplode comp_zimage_eq)
   281   apply (simp add: zet_ext_eq zimage_iff Rep_game_inverse)
   282   done
   283 
   284 lemma right_options[simp]: "right_options (Game l r) = r"
   285   apply (simp add: right_options_def Game_def)
   286   apply (subst Abs_game_inverse)
   287   apply (simp add: game_def)
   288   apply (rule Opair_in_games_lfp)
   289   apply (auto simp add: explode_Elem Elem_zimplode zimage_iff Rep_game[simplified game_def])
   290   apply (simp add: Snd zexplode_zimplode comp_zimage_eq)
   291   apply (simp add: zet_ext_eq zimage_iff Rep_game_inverse)
   292   done  
   293 
   294 lemma Game_ext: "(Game l1 r1 = Game l2 r2) = ((l1 = l2) \<and> (r1 = r2))"
   295   apply auto
   296   apply (subst left_options[where l=l1 and r=r1,symmetric])
   297   apply (subst left_options[where l=l2 and r=r2,symmetric])
   298   apply simp
   299   apply (subst right_options[where l=l1 and r=r1,symmetric])
   300   apply (subst right_options[where l=l2 and r=r2,symmetric])
   301   apply simp
   302   done
   303 
   304 definition option_of :: "(game * game) set" where
   305   "option_of \<equiv> image (\<lambda> (option, g). (Abs_game option, Abs_game g)) is_option_of"
   306 
   307 lemma option_to_is_option_of: "((option, g) \<in> option_of) = ((Rep_game option, Rep_game g) \<in> is_option_of)"
   308   apply (auto simp add: option_of_def)
   309   apply (subst Abs_game_inverse)
   310   apply (simp add: is_option_of_imp_games game_def)
   311   apply (subst Abs_game_inverse)
   312   apply (simp add: is_option_of_imp_games game_def)
   313   apply simp
   314   apply (auto simp add: Bex_def image_def)  
   315   apply (rule exI[where x="Rep_game option"])
   316   apply (rule exI[where x="Rep_game g"])
   317   apply (simp add: Rep_game_inverse)
   318   done
   319   
   320 lemma wf_is_option_of: "wf is_option_of"
   321   apply (rule wfzf_implies_wf)
   322   apply (simp add: wfzf_is_option_of)
   323   done
   324 
   325 lemma wf_option_of[simp, intro]: "wf option_of"
   326 proof -
   327   have option_of: "option_of = inv_image is_option_of Rep_game"
   328     apply (rule set_eqI)
   329     apply (case_tac "x")
   330     by (simp add: option_to_is_option_of) 
   331   show ?thesis
   332     apply (simp add: option_of)
   333     apply (auto intro: wf_is_option_of)
   334     done
   335 qed
   336   
   337 lemma right_option_is_option[simp, intro]: "zin x (right_options g) \<Longrightarrow> zin x (options g)"
   338   by (simp add: options_def zunion)
   339 
   340 lemma left_option_is_option[simp, intro]: "zin x (left_options g) \<Longrightarrow> zin x (options g)"
   341   by (simp add: options_def zunion)
   342 
   343 lemma zin_options[simp, intro]: "zin x (options g) \<Longrightarrow> (x, g) \<in> option_of"
   344   apply (simp add: options_def zunion left_options_def right_options_def option_of_def 
   345     image_def is_option_of_def zimage_iff zin_zexplode_eq) 
   346   apply (cases g)
   347   apply (cases x)
   348   apply (auto simp add: Abs_game_inverse games_lfp_eq_gfp[symmetric] game_def 
   349     right_option_def[symmetric] left_option_def[symmetric])
   350   done
   351 
   352 function
   353   neg_game :: "game \<Rightarrow> game"
   354 where
   355   [simp del]: "neg_game g = Game (zimage neg_game (right_options g)) (zimage neg_game (left_options g))"
   356 by auto
   357 termination by (relation "option_of") auto
   358 
   359 lemma "neg_game (neg_game g) = g"
   360   apply (induct g rule: neg_game.induct)
   361   apply (subst neg_game.simps)+
   362   apply (simp add: comp_zimage_eq)
   363   apply (subgoal_tac "zimage (neg_game o neg_game) (left_options g) = left_options g")
   364   apply (subgoal_tac "zimage (neg_game o neg_game) (right_options g) = right_options g")
   365   apply (auto simp add: game_split[symmetric])
   366   apply (auto simp add: zet_ext_eq zimage_iff)
   367   done
   368 
   369 function
   370   ge_game :: "(game * game) \<Rightarrow> bool" 
   371 where
   372   [simp del]: "ge_game (G, H) = (\<forall> x. if zin x (right_options G) then (
   373                           if zin x (left_options H) then \<not> (ge_game (H, x) \<or> (ge_game (x, G))) 
   374                                                     else \<not> (ge_game (H, x)))
   375                           else (if zin x (left_options H) then \<not> (ge_game (x, G)) else True))"
   376 by auto
   377 termination by (relation "(gprod_2_1 option_of)") 
   378  (simp, auto simp: gprod_2_1_def)
   379 
   380 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)))"
   381   apply (subst ge_game.simps[where G=G and H=H])
   382   apply (auto)
   383   done
   384 
   385 lemma ge_game_leftright_refl[rule_format]: 
   386   "\<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)"
   387 proof (induct x rule: wf_induct[OF wf_option_of]) 
   388   case (1 "g")
   389   { 
   390     fix y
   391     assume y: "zin y (right_options g)"
   392     have "\<not> ge_game (g, y)"
   393     proof -
   394       have "(y, g) \<in> option_of" by (auto intro: y)
   395       with 1 have "ge_game (y, y)" by auto
   396       with y show ?thesis by (subst ge_game_eq, auto)
   397     qed
   398   }
   399   note right = this
   400   { 
   401     fix y
   402     assume y: "zin y (left_options g)"
   403     have "\<not> ge_game (y, g)"
   404     proof -
   405       have "(y, g) \<in> option_of" by (auto intro: y)
   406       with 1 have "ge_game (y, y)" by auto
   407       with y show ?thesis by (subst ge_game_eq, auto)
   408     qed
   409   } 
   410   note left = this
   411   from left right show ?case
   412     by (auto, subst ge_game_eq, auto)
   413 qed
   414 
   415 lemma ge_game_refl: "ge_game (x,x)" by (simp add: ge_game_leftright_refl)
   416 
   417 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)"
   418 proof (induct x rule: wf_induct[OF wf_option_of]) 
   419   case (1 "g")  
   420   show ?case
   421   proof (auto)
   422     {case (goal1 y) 
   423       from goal1 have "(y, g) \<in> option_of" by (auto)
   424       with 1 have "ge_game (y, y)" by auto
   425       with goal1 have "\<not> ge_game (g, y)" 
   426         by (subst ge_game_eq, auto)
   427       with goal1 show ?case by auto}
   428     note right = this
   429     {case (goal2 y)
   430       from goal2 have "(y, g) \<in> option_of" by (auto)
   431       with 1 have "ge_game (y, y)" by auto
   432       with goal2 have "\<not> ge_game (y, g)" 
   433         by (subst ge_game_eq, auto)
   434       with goal2 show ?case by auto}
   435     note left = this
   436     {case goal3
   437       from left right show ?case
   438         by (subst ge_game_eq, auto)
   439     }
   440   qed
   441 qed
   442         
   443 definition eq_game :: "game \<Rightarrow> game \<Rightarrow> bool" where
   444   "eq_game G H \<equiv> ge_game (G, H) \<and> ge_game (H, G)" 
   445 
   446 lemma eq_game_sym: "(eq_game G H) = (eq_game H G)"
   447   by (auto simp add: eq_game_def)
   448 
   449 lemma eq_game_refl: "eq_game G G"
   450   by (simp add: ge_game_refl eq_game_def)
   451 
   452 lemma induct_game: "(\<And>x. \<forall>y. (y, x) \<in> lprod option_of \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a"
   453   by (erule wf_induct[OF wf_lprod[OF wf_option_of]])
   454 
   455 lemma ge_game_trans:
   456   assumes "ge_game (x, y)" "ge_game (y, z)" 
   457   shows "ge_game (x, z)"
   458 proof -  
   459   { 
   460     fix a
   461     have "\<forall> x y z. a = [x,y,z] \<longrightarrow> ge_game (x,y) \<longrightarrow> ge_game (y,z) \<longrightarrow> ge_game (x, z)"
   462     proof (induct a rule: induct_game)
   463       case (1 a)
   464       show ?case
   465       proof (rule allI | rule impI)+
   466         case (goal1 x y z)
   467         show ?case
   468         proof -
   469           { fix xr
   470             assume xr:"zin xr (right_options x)"
   471             assume a: "ge_game (z, xr)"
   472             have "ge_game (y, xr)"
   473               apply (rule 1[rule_format, where y="[y,z,xr]"])
   474               apply (auto intro: xr lprod_3_1 simp add: goal1 a)
   475               done
   476             moreover from xr have "\<not> ge_game (y, xr)"
   477               by (simp add: goal1(2)[simplified ge_game_eq[of x y], rule_format, of xr, simplified xr])
   478             ultimately have "False" by auto      
   479           }
   480           note xr = this
   481           { fix zl
   482             assume zl:"zin zl (left_options z)"
   483             assume a: "ge_game (zl, x)"
   484             have "ge_game (zl, y)"
   485               apply (rule 1[rule_format, where y="[zl,x,y]"])
   486               apply (auto intro: zl lprod_3_2 simp add: goal1 a)
   487               done
   488             moreover from zl have "\<not> ge_game (zl, y)"
   489               by (simp add: goal1(3)[simplified ge_game_eq[of y z], rule_format, of zl, simplified zl])
   490             ultimately have "False" by auto
   491           }
   492           note zl = this
   493           show ?thesis
   494             by (auto simp add: ge_game_eq[of x z] intro: xr zl)
   495         qed
   496       qed
   497     qed
   498   } 
   499   note trans = this[of "[x, y, z]", simplified, rule_format]    
   500   with assms show ?thesis by blast
   501 qed
   502 
   503 lemma eq_game_trans: "eq_game a b \<Longrightarrow> eq_game b c \<Longrightarrow> eq_game a c"
   504   by (auto simp add: eq_game_def intro: ge_game_trans)
   505 
   506 definition zero_game :: game
   507  where  "zero_game \<equiv> Game zempty zempty"
   508 
   509 function 
   510   plus_game :: "game \<Rightarrow> game \<Rightarrow> game"
   511 where
   512   [simp del]: "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 by auto
   517 termination by (relation "gprod_2_2 option_of")
   518   (simp, auto simp: gprod_2_2_def)
   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 1)
   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 = this[simplified goal1, simplified] and this
   551       show ?case
   552         apply (simp only: plus_game.simps[where G=G and H=H])
   553         apply (simp add: game_ext_eq goal1)
   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 1)
   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: goal1)
   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: y)
   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: y)
   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: y)
   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: y)
   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 definition eq_game_rel :: "(game * game) set" where
   842   "eq_game_rel \<equiv> { (p, q) . eq_game p q }"
   843 
   844 definition "Pg = UNIV//eq_game_rel"
   845 
   846 typedef (open) Pg = Pg
   847   unfolding Pg_def by (auto simp add: quotient_def)
   848 
   849 lemma equiv_eq_game[simp]: "equiv UNIV eq_game_rel"
   850   by (auto simp add: equiv_def refl_on_def sym_def trans_def eq_game_rel_def
   851     eq_game_sym intro: eq_game_refl eq_game_trans)
   852 
   853 instantiation Pg :: "{ord, zero, plus, minus, uminus}"
   854 begin
   855 
   856 definition
   857   Pg_zero_def: "0 = Abs_Pg (eq_game_rel `` {zero_game})"
   858 
   859 definition
   860   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))"
   861 
   862 definition
   863   Pg_less_def: "G < H \<longleftrightarrow> G \<le> H \<and> G \<noteq> (H::Pg)"
   864 
   865 definition
   866   Pg_minus_def: "- G = the_elem (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
   867 
   868 definition
   869   Pg_plus_def: "G + H = the_elem (\<Union> g \<in> Rep_Pg G. \<Union> h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game g h})})"
   870 
   871 definition
   872   Pg_diff_def: "G - H = G + (- (H::Pg))"
   873 
   874 instance ..
   875 
   876 end
   877 
   878 lemma Rep_Abs_eq_Pg[simp]: "Rep_Pg (Abs_Pg (eq_game_rel `` {g})) = eq_game_rel `` {g}"
   879   apply (subst Abs_Pg_inverse)
   880   apply (auto simp add: Pg_def quotient_def)
   881   done
   882 
   883 lemma char_Pg_le[simp]: "(Abs_Pg (eq_game_rel `` {g}) \<le> Abs_Pg (eq_game_rel `` {h})) = (ge_game (h, g))"
   884   apply (simp add: Pg_le_def)
   885   apply (auto simp add: eq_game_rel_def eq_game_def intro: ge_game_trans ge_game_refl)
   886   done
   887 
   888 lemma char_Pg_eq[simp]: "(Abs_Pg (eq_game_rel `` {g}) = Abs_Pg (eq_game_rel `` {h})) = (eq_game g h)"
   889   apply (simp add: Rep_Pg_inject [symmetric])
   890   apply (subst eq_equiv_class_iff[of UNIV])
   891   apply (simp_all)
   892   apply (simp add: eq_game_rel_def)
   893   done
   894 
   895 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})"
   896 proof -
   897   have "(\<lambda> g h. {Abs_Pg (eq_game_rel `` {plus_game g h})}) respects2 eq_game_rel" 
   898     apply (simp add: congruent2_def)
   899     apply (auto simp add: eq_game_rel_def eq_game_def)
   900     apply (rule_tac y="plus_game a ba" in ge_game_trans)
   901     apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+
   902     apply (rule_tac y="plus_game b aa" in ge_game_trans)
   903     apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+
   904     done
   905   then show ?thesis
   906     by (simp add: Pg_plus_def UN_equiv_class2[OF equiv_eq_game equiv_eq_game]) 
   907 qed
   908     
   909 lemma char_Pg_minus[simp]: "- Abs_Pg (eq_game_rel `` {g}) = Abs_Pg (eq_game_rel `` {neg_game g})"
   910 proof -
   911   have "(\<lambda> g. {Abs_Pg (eq_game_rel `` {neg_game g})}) respects eq_game_rel"
   912     apply (simp add: congruent_def)
   913     apply (auto simp add: eq_game_rel_def eq_game_def ge_neg_game)
   914     done    
   915   then show ?thesis
   916     by (simp add: Pg_minus_def UN_equiv_class[OF equiv_eq_game])
   917 qed
   918 
   919 lemma eq_Abs_Pg[rule_format, cases type: Pg]: "(\<forall> g. z = Abs_Pg (eq_game_rel `` {g}) \<longrightarrow> P) \<longrightarrow> P"
   920   apply (cases z, simp)
   921   apply (simp add: Rep_Pg_inject[symmetric])
   922   apply (subst Abs_Pg_inverse, simp)
   923   apply (auto simp add: Pg_def quotient_def)
   924   done
   925 
   926 instance Pg :: ordered_ab_group_add 
   927 proof
   928   fix a b c :: Pg
   929   show "a - b = a + (- b)" by (simp add: Pg_diff_def)
   930   {
   931     assume ab: "a \<le> b"
   932     assume ba: "b \<le> a"
   933     from ab ba show "a = b"
   934       apply (cases a, cases b)
   935       apply (simp add: eq_game_def)
   936       done
   937   }
   938   then show "(a < b) = (a \<le> b \<and> \<not> b \<le> a)" by (auto simp add: Pg_less_def)
   939   show "a + b = b + a"
   940     apply (cases a, cases b)
   941     apply (simp add: eq_game_def plus_game_comm)
   942     done
   943   show "a + b + c = a + (b + c)"
   944     apply (cases a, cases b, cases c)
   945     apply (simp add: eq_game_def plus_game_assoc)
   946     done
   947   show "0 + a = a"
   948     apply (cases a)
   949     apply (simp add: Pg_zero_def plus_game_zero_left)
   950     done
   951   show "- a + a = 0"
   952     apply (cases a)
   953     apply (simp add: Pg_zero_def eq_game_plus_inverse plus_game_comm)
   954     done
   955   show "a \<le> a"
   956     apply (cases a)
   957     apply (simp add: ge_game_refl)
   958     done
   959   {
   960     assume ab: "a \<le> b"
   961     assume bc: "b \<le> c"
   962     from ab bc show "a \<le> c"
   963       apply (cases a, cases b, cases c)
   964       apply (auto intro: ge_game_trans)
   965       done
   966   }
   967   {
   968     assume ab: "a \<le> b"
   969     from ab show "c + a \<le> c + b"
   970       apply (cases a, cases b, cases c)
   971       apply (simp add: ge_plus_game_left[symmetric])
   972       done
   973   }
   974 qed
   975 
   976 end
   977