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