theory Winning2NE
imports Main
begin
(*Work based on article 
"From winning strategy to Nash equilibrium"
by Stéphane Le Roux
Includes extension of this work: the order is lifted without prior linear extension*)

(*Lemmas about minima and maxima in finite sets*)
(*every finite non-empty partial order has a maximum*)
(*I use les instead of less because less is predefined*)
lemma existsMax :
  assumes les_transitive : "\<And>a b c. les a b \<Longrightarrow> les b c \<Longrightarrow> les a c"
      and les_irreflexive : "\<And> a. \<not>(les a a)"
      and finite_X : "finite X"
  shows "X\<noteq>{} \<longrightarrow> (\<exists>x\<in>X. \<forall>y\<in>X. \<not>(les x y))"
proof - (* (induct X) does not work, why?*)
  (*Induction proof*)
  have "finite X" by (rule finite_X) 
  moreover (*Base*)
  have base : "{}\<noteq>{} \<longrightarrow> (\<exists>x\<in>{}. \<forall>y\<in>{}. \<not>(les x y))" by simp
  moreover (*step*)
  { fix A and a
    assume finite_A : "finite A"
       and ihy : "A\<noteq>{} \<longrightarrow> (\<exists>x\<in>A. \<forall>y\<in>A. \<not>(les x y))"
    have ist : "insert a A\<noteq>{} \<longrightarrow> (\<exists>x\<in>insert a A. \<forall>y\<in>insert a A. \<not>(les x y))"
    proof (cases "A={}") (*that's really the step*)
      assume "A\<noteq>{}"
      with ihy have  "\<exists>x\<in>A. \<forall>y\<in>A. \<not>(les x y)" by (rule mp)
      then obtain xm where xmA : "xm\<in>A" and isMax : "\<forall>y\<in>A. \<not>(les xm y)" by (rule bexE)
      have "\<exists>x\<in>insert a A. \<forall>y\<in>insert a A. \<not>(les x y)"
      proof (cases "les xm a")
        assume "\<not>(les xm a)"
        hence "\<forall>y\<in>insert a A. \<not>(les xm y)" using isMax by simp
        moreover 
        have "xm\<in> insert a A" using xmA by simp
        ultimately show "\<exists>x\<in>insert a A. \<forall>y\<in>insert a A. \<not>(les x y)" by (rule bexI)
        next
        assume xmLa : "les xm a"
        { fix y
          { assume yA : "y\<in>A"
            hence not_xmLy : "\<not>(les xm y)" using isMax by simp
            moreover
            { assume "les a y" 
              with xmLa have "les xm y" by (rule les_transitive)
              with not_xmLy have "False" by simp
            } 
            hence "\<not>(les a y)" by (rule notI)
          }
          hence "y\<in>A \<longrightarrow> \<not>(les a y)" by (rule impI)
        }
        hence "\<forall>y\<in>A. \<not>(les a y)" by simp
        moreover have "\<not>(les a a)" by (rule les_irreflexive) 
        ultimately have " \<forall>y\<in>insert a A. \<not>(les a y)" by simp
        moreover
        have "a\<in> insert a A" by simp
        ultimately show "\<exists>x\<in>insert a A. \<forall>y\<in>insert a A. \<not>(les x y)" by (rule bexI)
      qed
      thus "insert a A\<noteq>{} \<longrightarrow> (\<exists>x\<in>insert a A. \<forall>y\<in>insert a A. \<not>(les x y))" by (rule impI) 
    next
      assume "A={}" (*that's really the base case*)
      hence a_singl : "{a} = insert a A" by simp
      { fix y
        have "\<not>(les a a)" by (rule les_irreflexive)
        hence "y\<in>{a}\<longrightarrow> \<not>(les a y)" by simp
        with a_singl have "y\<in>insert a A\<longrightarrow> \<not>(les a y)" by (rule subst)
      }
      hence "\<forall>y. y\<in>insert a A \<longrightarrow> \<not>(les a y)" by (rule allI)
      hence "\<forall>y\<in>insert a A. \<not>(les a y)" by simp    
      moreover
      have "a\<in>insert a A" by simp
      ultimately have "\<exists>x\<in>insert a A. \<forall>y\<in>insert a A. \<not>(les x y)" by (rule bexI)
      thus "insert a A\<noteq>{} \<longrightarrow> (\<exists>x\<in>insert a A. \<forall>y\<in>insert a A. \<not>(les x y))" by (rule impI)
    qed
  }
  ultimately show ?thesis by (rule finite.induct)
qed

(*Symmetric to existsMax*)
lemma existsMin :
  assumes les_transitive : "\<And>a b c. les a b \<Longrightarrow> les b c \<Longrightarrow> les a c"
      and les_irreflexive : "\<And> a. \<not>(les a a)"
      and finite_X : "finite X"
  shows "X\<noteq>{} \<longrightarrow> (\<exists>x\<in>X. \<forall>y\<in>X. \<not>(les y x))"
proof -
  have lesmax_transitive : "\<And>a b c. les b a \<Longrightarrow> les c b \<Longrightarrow> les c a"
  proof -
    show "\<And>a b c. les b a \<Longrightarrow> les c b \<Longrightarrow> les c a" using les_transitive by blast
  qed
  show "X\<noteq>{} \<longrightarrow> (\<exists>x\<in>X. \<forall>y\<in>X. \<not>(les y x))" using 
    lesmax_transitive and les_irreflexive and finite_X by (rule existsMax)
qed
 
(*13.2.17 : Generalisation of existsMax: either an element is a minimum or it has a 
minimum below it. This time I first prove it for min since that is what I need.*)
(*at least half a day's work*)
lemma isMinOrHasMin :
  assumes les_trans : "\<And>a b c. les a b \<Longrightarrow> les b c \<Longrightarrow> les a c"
      and les_irr : "\<And> a. \<not>les a a"
      and finite_X : "finite X"
  shows "\<forall>x\<in>X. (\<forall>y\<in>X. \<not>les y x)\<or>(\<exists>z\<in>X. les z x \<and>(\<forall>y\<in>X. \<not>les y z))"
proof - (* (induct X) does not work, why?*)
  (*Induction proof*)
  have "finite X" by (rule finite_X) 
  moreover (*Base (pseudo)*)
  have base : "\<forall>x\<in>{}. (\<forall>y\<in>{}. \<not>les y x)\<or>(\<exists>z\<in>{}. les z x \<and>(\<forall>y\<in>{}. \<not>les y z))" by simp
  moreover (*step*)
  { fix A and a
    assume finite_A : "finite A"
       and IH : "\<forall>x\<in>A. (\<forall>y\<in>A. \<not>les y x)\<or>(\<exists>z\<in>A. les z x \<and>(\<forall>y\<in>A. \<not>les y z))"
    have IS : "(\<forall>x\<in>insert a A. (\<forall>y\<in>insert a A. \<not>les y x)\<or>
                               (\<exists>z\<in>insert a A. les z x \<and>(\<forall>y\<in>insert a A. \<not>les y z)))"
    proof (rule ballI)
      fix x 
      assume xaA : "x\<in>insert a A"
      show "(\<forall>y\<in>insert a A. \<not>les y x) \<or> (\<exists>z\<in>insert a A. les z x \<and>(\<forall>y\<in>insert a A. \<not>les y z))"
      proof (cases "x\<in>A")
        assume "x\<in>A"
        with IH have "(\<forall>y\<in>A. \<not>les y x)\<or>(\<exists>z\<in>A. les z x \<and>(\<forall>y\<in>A. \<not>les y z))" by (rule bspec) 
        moreover (*case distinction over the above disjunction*)
        {
          assume xminA : "\<forall>y\<in>A. \<not>les y x" (*x is minimum in A*)
          have ?thesis
          proof (cases "les a x")
            assume a_newmin : "les a x" (*a replaces x as minimum in insert a A*)
            have "\<forall>y\<in>insert a A. \<not>les y a" (*a is minimum in insert a A*)
            proof (rule ballI)
              fix y
              assume "y\<in>insert a A"
              hence "y=a\<or>y\<in>A" by simp
              moreover (*case distinction over the above disjunction*)
              { 
                assume "y=a"
                hence "\<not>les y a" using les_irr by simp
              }
              moreover
              {
                assume yA : "y\<in>A"
                {
                  assume "les y a" (*y would be smaller than minimum in insert a A*)
                  hence "les y x" using a_newmin by (rule les_trans)
                  with xminA and yA have "False" by simp
                }
                hence "\<not>les y a" by (rule notI)
              }
              ultimately show "\<not>les y a" by (rule disjE)
            qed
            with a_newmin have "les a x \<and>(\<forall>y\<in>insert a A. \<not>les y a)" by (rule conjI)
            hence "\<exists>z\<in>insert a A. les z x \<and>(\<forall>y\<in>insert a A. \<not>les y z)" by blast
            thus ?thesis by (rule disjI2)
            next 
            assume x_stays_min : "\<not>les a x"
            with xminA have "\<forall>y\<in>insert a A. \<not>les y x" by simp
            thus ?thesis by (rule disjI1)
          qed
        }
        moreover
        {
          assume xNotMinA : "(\<exists>z\<in>A. les z x \<and>(\<forall>y\<in>A. \<not>les y z))"
          then obtain z where zA : "z\<in>A" and zx_zminA : "les z x \<and> (\<forall>y\<in>A. \<not>les y z)" by (rule bexE)
          have zx : "les z x" using zx_zminA by (rule conjunct1)
          have zminA : "(\<forall>y\<in>A. \<not>les y z)" using zx_zminA by (rule conjunct2)
          have ?thesis
          proof (cases "les a z")
            assume a_newmin : "les a z" (*a replaces z as minimum in insert a A*)
            hence ax : "les a x" using zx by (rule les_trans) (*needed later*)
            have "\<forall>y\<in>insert a A. \<not>les y a" (*a is minimum in insert a A*)
            proof (rule ballI)
              fix y
              assume "y\<in>insert a A"
              hence "y=a\<or>y\<in>A" by simp
              moreover (*case distinction over the above disjunction*)
              { 
                assume "y=a"
                hence "\<not>les y a" using les_irr by simp
              }
              moreover
              {
                assume yA : "y\<in>A"
                {
                  assume "les y a" (*y would be smaller than minimum in insert a A*)
                  hence "les y z" using a_newmin by (rule les_trans)
                  with zminA and yA have "False" by simp
                }
                hence "\<not>les y a" by (rule notI)
              }
              ultimately show "\<not>les y a" by (rule disjE)
            qed
            with ax have "les a x \<and>(\<forall>y\<in>insert a A. \<not>les y a)" by (rule conjI)
            hence "\<exists>z\<in>insert a A. les z x \<and>(\<forall>y\<in>insert a A. \<not>les y z)" by blast
            thus ?thesis by (rule disjI2)
            next  (*z remains minimum in insert a A*)
            assume z_stays_min : "\<not>les a z"
            with zminA have "\<forall>y\<in>insert a A. \<not>les y z" by simp
            with zx have "les z x \<and> (\<forall>y\<in>insert a A. \<not>les y z)" by (rule conjI)
            with zA have "(\<exists>z\<in>insert a A. les z x \<and> (\<forall>y\<in>insert a A. \<not>les y z))" by blast
            thus ?thesis by (rule disjI2)
          qed
        } 
        ultimately show ?thesis by (rule disjE)
        next
        assume "x\<notin>A"
        hence x_a : "x=a" using xaA by simp 
        show ?thesis
        proof (cases "\<forall>y\<in>A. \<not>les y x")
          assume "\<forall>y\<in>A. \<not>les y x" (*x=a is the minimum in insert a A*)
          with les_irr and x_a have "\<forall>y\<in>insert a A. \<not>les y x" by simp
          thus ?thesis by (rule disjI1)
          next 
          assume "\<not>(\<forall>y\<in>A. \<not>les y x)" (*x=a is not the minimum in insert a A*)
          hence "\<exists>y\<in>A. les y x" by simp
          then obtain y where yA : "y\<in>A" and yx : "les y x" by (rule bexE)
          have not_xy : "\<not>les x y" (*needed twice below. NO, JUST ONCE*)
          proof (rule notI)
            assume "les x y"
            with yx have "les y y" by (rule les_trans)
            with les_irr show "False" by (rule notE)
          qed
          (*instantiate x in IH with y: y is min in A or has min below it:*)
          have "(\<forall>y'\<in>A. \<not>les y' y)\<or>(\<exists>z\<in>A. les z y \<and>(\<forall>y'\<in>A. \<not>les y' z))" using IH and yA by (rule bspec)
          moreover  (*case distinction over the above disjunction*)
          {
            assume ymin : "\<forall>y'\<in>A. \<not>les y' y"
            moreover
            have "\<not>les x y" by (rule not_xy)
            ultimately have "(\<forall>y'\<in>A. \<not>les y' y) \<and> \<not>les x y" by (rule conjI)
            hence "\<forall>y'\<in>insert a A. \<not>les y' y" using x_a by blast
            hence "les y x \<and> (\<forall>y'\<in>insert a A. \<not>les y' y)" using yx by blast
            hence "(\<exists>z\<in>insert a A. les z x \<and> (\<forall>y'\<in>insert a A. \<not>les y' z))" using yA by blast
            hence ?thesis by (rule disjI2)
          }
          moreover
          {
            assume "(\<exists>z\<in>A. les z y \<and>(\<forall>y'\<in>A. \<not>les y' z))" (*y has minimum below it*)
            then obtain z where zA : "z\<in>A" and zy_zminA : "les z y \<and>(\<forall>y'\<in>A. \<not>les y' z)" by (rule bexE)
            have zy : "les z y" using zy_zminA by (rule conjunct1)
            have zx : "les z x" using zy and yx by (rule les_trans)
            have zminA2 : "(\<forall>y'\<in>A. \<not>les y' z)" using zy_zminA by (rule conjunct2)
            moreover
            {
              assume "les a z"
              hence "les a x" using zx by (rule les_trans)
              with x_a have "les a a" by (rule subst)
              with les_irr have "False" by (rule notE)
            }
            hence "\<not>les a z" by (rule notI)
            ultimately have "(\<forall>y'\<in>A. \<not>les y' z) \<and> \<not>les a z" by (rule conjI)
            hence "\<forall>y'\<in>insert a A. \<not>les y' z" using x_a by blast
            hence "les z x  \<and> (\<forall>y'\<in>insert a A. \<not>les y' z)" using zx by blast
            hence "(\<exists>z\<in>insert a A. les z x \<and> (\<forall>y'\<in>insert a A. \<not>les y' z))" using zA by blast
            hence ?thesis by (rule disjI2)
          }
          ultimately show ?thesis by (rule disjE)
        qed
      qed
    qed   
  }
  ultimately show ?thesis by (rule finite.induct)
qed

(*For defining lifting we need upper cone of a point and of a set:*)
text_raw {*\DefineSnippet{uconelessP}{*}
definition
  ucone :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> ('a set)"
  where "ucone les x = {z. les x z}" 

definition
  uCone :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a set) \<Rightarrow> ('a set)"
  where "uCone les Y = \<Union> ((ucone les) ` Y)" 

definition 
(*Lifting without prior extension*)
  lessP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a set) \<Rightarrow> ('a set) \<Rightarrow> bool"
  where "lessP les A B = (finite A \<and> 
     (\<exists>A'\<subseteq>A-B. A'\<noteq>{} \<and> A-(A'\<union>(uCone les A')) = B-(A'\<union>(uCone les A'))))"
text_raw {*}%EndSnippet*}

definition 
(*2.1 in paper but note that < is automatically a strict linear order*)
  lessPOrig :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a set) \<Rightarrow> ('a set) \<Rightarrow> bool"
  where "lessPOrig les A B = (\<exists>a\<in>A-B. \<forall>b\<in>B-A. les a b)"

lemma twoLiftings :
  assumes AB_orig : "lessPOrig les A B"
      and finiteA : "finite A"
  shows "lessP les A B"
proof -
  have "lessPOrig les A B" by (rule AB_orig)
  with lessPOrig_def have "(\<exists>a\<in>A-B. \<forall>b\<in>B-A. les a b)" by (rule subst)
  then obtain a where aAB : "a\<in>A-B" and aMin : "\<forall>b\<in>B-A. les a b" by (rule bexE)
(*will show that A-B is witness for "lessP les A B"*)
  have ABnonempty : "A-B\<noteq>{}" using aAB by blast
  have ABsubset : "A-B \<subseteq>A-B" by simp
  have BA_uConeSubset : "B-A\<subseteq>uCone les (A-B)"
  proof (rule subsetI)
    fix x
    assume "x\<in>B-A"
    with aMin have "les a x" by (rule bspec)
    hence "x\<in>{z. les a z}" by simp
    with ucone_def[symmetric] have "x\<in>ucone les a" by (rule subst)
    hence "x\<in> \<Union> ((ucone les) ` (A-B))" using aAB by blast
    with uCone_def[symmetric] show "x\<in> uCone les (A-B)" by (rule subst)
  qed
(*Now show A-((A-B)\<union>(uCone les (A-B))) = B-((A-B)\<union>(uCone les (A-B)))
Approach: show that "A - " and "B -" can both be replaced by A\<inter>B*)
  have Amin_AB : "A-(A-B) = A\<inter>B" by blast
  have Bmin_AB : "B-(B-A) = A\<inter>B" by blast
  have "A-((A-B)\<union>(uCone les (A-B))) = (A-(A-B)) - (uCone les (A-B))" by blast (*simple set theory*)
  also have "... = ((A-(A-B)) - (A-B)) - (uCone les (A-B))" by blast (*making expression more complicated*)
  also have "... = ((A\<inter>B) - (A-B)) - (uCone les (A-B))" using Amin_AB by blast
  also have "... = (A\<inter>B) - ((A-B)\<union>(uCone les (A-B)))" by blast
(*Now massage this to get to expression for B. I had to do this first in reverse to see how it goes.*)
  also have "... = (B- (B-A))- ((A-B)\<union>(uCone les (A-B)))" using Bmin_AB by blast
  also have "... = B-((A-B)\<union>(uCone les (A-B)))" using BA_uConeSubset by blast 
  finally have "A-((A-B)\<union>(uCone les (A-B))) = B-((A-B)\<union>(uCone les (A-B)))" .
  with ABnonempty have "A-B\<noteq>{} \<and> A-((A-B)\<union>(uCone les (A-B))) = B-((A-B)\<union>(uCone les (A-B)))" by (rule conjI)
  hence "(\<exists>A'\<subseteq>A-B. A'\<noteq>{} \<and> A-(A'\<union>(uCone les A')) = B-(A'\<union>(uCone les A')))" using ABsubset by blast
  with finiteA have "finite A \<and> (\<exists>A'\<subseteq>A-B. A'\<noteq>{} \<and> A-(A'\<union>(uCone les A')) = B-(A'\<union>(uCone les A')))" 
     by (rule conjI)
  with lessP_def[symmetric] show ?thesis by (rule subst)
qed


text_raw {*\DefineSnippet{liftirreflexive}{*}
lemma lift_irreflexive : (*Lemma 3 in note*)
  shows "\<not>(lessP les A A)"
text_raw {*}%EndSnippet*}
proof -
  {
    assume "lessP les A A"
    with lessP_def have "finite A \<and> (\<exists>A'\<subseteq>A-A. A'\<noteq>{} \<and> A-(A'\<union>(uCone les A')) = A-(A'\<union>(uCone les A')))" by (rule subst)
    hence "False" by blast
  }
  thus ?thesis by (rule notI)
qed

(*Used in lift_transitive*)
lemma subsetCones : 
  assumes A_sub : "A\<subseteq>AuB"
      and les_trans : "\<And>a b c. les a b \<Longrightarrow> les b c \<Longrightarrow> les a c"
      and les_irr : "\<And> a. \<not>les a a"
      and finiteAB : "finite AuB"
  shows "A\<union>(uCone les A) \<subseteq> {x\<in>AuB. \<forall>y\<in>AuB. \<not>(les y x)} \<union>
                 (uCone les {x\<in>AuB. \<forall>y\<in>AuB. \<not>(les y x)})" 
     (is "A\<union>(uCone les A) \<subseteq> ?A'' \<union> (uCone les ?A'')")
proof (rule subsetI)
  fix x
  assume "x\<in> A\<union>(uCone les A)"
  hence "x\<in>A\<or> x\<in>(uCone les A)" by simp
(*transform this disjunction into another one that distinguishes minimal and non-minimal x:*)
  hence "x\<in>A\<and>(\<forall>y\<in>AuB. \<not>(les y x)) \<or> x\<in>A\<and>\<not>(\<forall>y\<in>AuB. \<not>(les y x)) \<or> x\<in>(uCone les A)" by blast
  moreover (*case distinction over the above disjunction*)
  { (*x is minimal*)
    assume xA_xMin : "x\<in>A\<and>(\<forall>y\<in>AuB. \<not>(les y x))"
    hence xAB : "x\<in>AuB" using A_sub by blast
    have xMin : "(\<forall>y\<in>AuB. \<not>(les y x))" using xA_xMin by (rule conjunct2)
    hence "x\<in>?A''"  using xAB by blast  
    hence "x \<in> ?A''\<union>(uCone les ?A'')" by simp
  }
  moreover
  { (*x is not minimal*)
    assume xNotMinGeneral : "x\<in>A\<and>\<not>(\<forall>y\<in>AuB. \<not>(les y x)) \<or> x\<in>(uCone les A)"
    have "(\<exists>z\<in> AuB. les z x \<and>(\<forall>y\<in>AuB. \<not>les y z))" (*There is a minimal z below x*)
    proof (cases "x\<in>A\<and>\<not>(\<forall>y\<in>AuB. \<not>(les y x))")
    { (*x is in A'*) 
      assume xA_xNotMin :"x\<in>A\<and>\<not>(\<forall>y\<in>AuB. \<not>(les y x))"
      hence xAB : "x\<in>AuB" using A_sub by blast
      have xNotMin : "\<not>(\<forall>y\<in>AuB. \<not>(les y x))" using xA_xNotMin by (rule conjunct2)
      moreover
      have "\<forall>x\<in>AuB. (\<forall>y\<in>AuB. \<not>les y x)\<or>(\<exists>z\<in> AuB. les z x \<and>(\<forall>y\<in>AuB. \<not>les y z))"
         using les_trans and les_irr and finiteAB by (rule isMinOrHasMin)
      hence "(\<forall>y\<in>AuB. \<not>les y x)\<or>(\<exists>z\<in> AuB. les z x \<and>(\<forall>y\<in>AuB. \<not>les y z))" 
         using xAB by (rule bspec)
      ultimately show "(\<exists>z\<in> AuB. les z x \<and>(\<forall>y\<in>AuB. \<not>les y z))" by blast
    }
    next
    { (*x is in uCone les A'*)
      assume "\<not>(x\<in>A\<and>\<not>(\<forall>y\<in>AuB. \<not>(les y x)))"
      hence "x\<in>(uCone les A)" using xNotMinGeneral by blast
      with uCone_def have "x\<in> \<Union> ((ucone les) ` A)" by (rule subst)
      hence "\<exists>z2\<in>A. x\<in> (ucone les z2)" by simp
      then obtain z2 where z2A : "z2\<in>A" and x_ucone_z2 : "x\<in> (ucone les z2)" by (rule bexE)
      have "x\<in>{x'. les z2 x'}" using ucone_def and x_ucone_z2 by (rule subst)
      hence z2x : "les z2 x" by simp
      have z2AB : "z2\<in>AuB" using z2A and A_sub by blast
      have "\<forall>x\<in>AuB. (\<forall>y\<in>AuB. \<not>les y x)\<or>(\<exists>z\<in> AuB. les z x \<and>(\<forall>y\<in>AuB. \<not>les y z))"
         using les_trans and les_irr and finiteAB by (rule isMinOrHasMin)
      hence "(\<forall>y\<in>AuB. \<not>les y z2)\<or>(\<exists>z\<in> AuB. les z z2 \<and>(\<forall>y\<in>AuB. \<not>les y z))" using z2AB by (rule bspec)
      moreover
(*Now show that there is a minimal z below x, in both cases of the line above.*)
      {
        assume "\<forall>y\<in>AuB. \<not>les y z2"
        with z2x have "les z2 x \<and> (\<forall>y\<in>AuB. \<not>les y z2)" by (rule conjI)
        hence ?thesis  using  z2AB by (rule bexI)
      }
      moreover
      {
        assume "(\<exists>z\<in> AuB. les z z2 \<and>(\<forall>y\<in>AuB. \<not>les y z))"
        then obtain z where zAB : "z\<in> AuB" and zz2_zMin : "les z z2 \<and>(\<forall>y\<in>AuB. \<not>les y z)" by (rule bexE)
        have zMin : "\<forall>y\<in>AuB. \<not>les y z"  using zz2_zMin by (rule conjunct2)
        have zz2 : "les z z2" using zz2_zMin by (rule conjunct1)
        hence zx : "les z x" using z2x by (rule les_trans)
        hence zx_zMin : "les z x \<and>(\<forall>y\<in>AuB. \<not>les y z)" using zMin by (rule conjI)
        hence ?thesis using zAB by (rule bexI)
      }
      ultimately show ?thesis by (rule disjE)
    }
    qed
    then obtain z where zAB : "z\<in> AuB" and zx_zMin : "les z x \<and>(\<forall>y\<in>AuB. \<not>les y z)" by (rule bexE)
    have zMin : "(\<forall>y\<in>AuB. \<not>(les y z))" using zx_zMin by (rule conjunct2)
    hence zA'' : "z\<in>?A''"  using zAB by blast 
    have zx : "les z x" using zx_zMin by (rule conjunct1)
    hence "x\<in>{z'. les z z'}" by simp
    with ucone_def[symmetric] have "x\<in>ucone les z" by (rule subst)
    hence "x\<in> \<Union> ((ucone les) ` ?A'')" using zA'' by blast 
    with uCone_def[symmetric] have "x\<in>uCone les ?A''" by (rule subst)
    hence "x \<in> ?A''\<union>(uCone les ?A'')" by simp
  }
  ultimately show "x \<in> ?A''\<union>(uCone les ?A'')" by (rule disjE)
qed

(*1 to 2 days of work*)
text_raw {*\DefineSnippet{lifttransitive}{*}
lemma lift_transitive : (*Lemma 3 in note*)  
  assumes les_irr : "\<And>x. \<not> (les x x)"
      and les_trans : "\<And>x y z. (les x y) \<Longrightarrow> (les y z) \<Longrightarrow> (les x z)"
(*not needed: *)
(*    and les_antisym : "\<And>x y. (les x y) \<longrightarrow> \<not>(les y x)"*)
      and AB : "lessP les A B"
      and BC : "lessP les B C"     
  shows "lessP les A C"
text_raw {*}%EndSnippet*}
proof -
(*first 20 or so lines resemble very much proof of liftAlt_asym*)
(*Exhibit witness for "lessP les A B" and show its finiteness*)
  have "lessP les A B" by (rule AB)
  with lessP_def have lessP_AB_unfold : 
     "(finite A \<and> (\<exists>A'\<subseteq>A-B. A'\<noteq>{} \<and> A-(A'\<union>(uCone les A')) = B-(A'\<union>(uCone les A'))))" by (rule subst) 
  hence finiteA : "finite A" by (rule conjunct1)
  have "(\<exists>A'\<subseteq>A-B. A'\<noteq>{} \<and> A-(A'\<union>(uCone les A')) = B-(A'\<union>(uCone les A')))" using lessP_AB_unfold by 
     (rule conjunct2)
  then obtain A' where A_witn : "A'\<subseteq>A-B \<and> A'\<noteq>{} \<and> A-(A'\<union>(uCone les A')) = B-(A'\<union>(uCone les A'))"  by (rule exE)
  hence A_B : "A-(A'\<union>(uCone les A')) = B-(A'\<union>(uCone les A'))" by simp
  have AAminusB : "A'\<subseteq>A-B" using A_witn by (rule conjunct1)
  hence AA : "A'\<subseteq>A" by blast
  with finiteA have "finite A'" by (rule rev_finite_subset)
  moreover
(*Exhibit witness for "lessP les B C" and show its finiteness*)
  have "lessP les B C" by (rule BC)
  with lessP_def have lessP_BC_unfold : 
     "(finite B \<and> (\<exists>B'\<subseteq>B-C. B'\<noteq>{} \<and> B-(B'\<union>(uCone les B')) = C-(B'\<union>(uCone les B'))))" by (rule subst)
  hence finiteB : "finite B" by (rule conjunct1)
  have "(\<exists>B'\<subseteq>B-C. B'\<noteq>{} \<and> B-(B'\<union>(uCone les B')) = C-(B'\<union>(uCone les B')))" using lessP_BC_unfold by (rule conjunct2)
  then obtain B' where B_witn : "B'\<subseteq>B-C \<and> B'\<noteq>{} \<and> B-(B'\<union>(uCone les B')) = C-(B'\<union>(uCone les B'))" by (rule exE)
  hence B_C : "B-(B'\<union>(uCone les B')) = C-(B'\<union>(uCone les B'))" by simp
  have BBminusC : "B'\<subseteq>B-C" using B_witn by (rule conjunct1)
  hence BB : "B'\<subseteq>B" by blast
  with finiteB have "finite B'" by (rule rev_finite_subset)
(*Finiteness of A'\<union>B'*)
  ultimately have finiteAB : "finite (A'\<union>B')" by (rule finite_UnI)
  with les_trans and les_irr have "A'\<union>B'\<noteq>{} \<longrightarrow> (\<exists>x\<in>A'\<union>B'. \<forall>y\<in>A'\<union>B'. \<not>(les y x))" by (rule existsMin)
  moreover
(*Non-emptyness of A'\<union>B'*)
  {
    have "A'\<noteq>{}" using A_witn by simp
    moreover have "B'\<noteq>{}" using B_witn by simp
    ultimately have "A'\<union>B'\<noteq>{}" by simp
  }
(*In consequence non-emptyness of A''=minimal elements of A'\<union>B'*)
  ultimately have "\<exists>x\<in>A'\<union>B'. \<forall>y\<in>A'\<union>B'. \<not>(les y x)" by (rule mp)
  hence Adashnonempty : "{x\<in>A'\<union>B'. \<forall>y\<in>A'\<union>B'. \<not>(les y x)}\<noteq>{}" (is "?A''\<noteq>{}") by blast
(*Will show that A'' witnesses "lessP les A C". Previous line is first part of that*)
  have Adash_AminusC : "?A''\<subseteq>A-C" (*Second part needed for  A'' to witness "lessP les A C"*)
  proof (rule subsetI)
    fix x
    {
      assume xAdash : "x\<in>?A''"
      hence xAorB : "x\<in>A' \<or> x\<in>B'" by blast 
      have  xMin : "\<forall>y\<in>A'\<union>B'. \<not>(les y x)" using xAdash by blast
      show "x\<in>A-C"
      proof (*not having - here means that Isabelle displays two subgoals x\<in>A and x\<notin>C.
              I show those in reverse order wrt Stephane's note.*)
        show "x\<in>A"
        proof (cases "x\<in>A'")
          assume "x\<in>A'"
          thus "x\<in>A" using AA by blast
        next
          assume xnotAdash : "x\<notin>A'"
          hence "x\<in>B'" using xAorB by simp
          hence xB : "x\<in>B" using BB by blast
          have "x\<notin>uCone les A'"
          proof -
            { 
              assume "x\<in>uCone les A'"
              with uCone_def have "x\<in> \<Union> ((ucone les) ` A')" by (rule subst)
              hence "\<exists>a\<in>A'. x\<in> ucone les a" by blast
              then obtain a where aA : "a\<in>A'" and x_ucone_a : "x\<in> ucone les a" by (rule bexE)
              have "x\<in> {z. les a z}" using ucone_def and x_ucone_a by (rule subst)  
              hence "les a x" by simp
              with aA and xMin have "False" by blast
            }
            thus "x\<notin>uCone les A'" by (rule notI) 
          qed
          with xnotAdash have "x\<notin>A'\<union>uCone les A'" by blast
          moreover 
          have "x\<in>B" by (rule xB) 
          ultimately show "x\<in>A" using A_B by blast
        qed
        show "x\<notin>C"
        proof (cases "x\<in>B'")
          assume "x\<in>B'"
          thus "x\<notin>C" using BBminusC by blast
        next
          assume xnotBdash : "x\<notin>B'"
          hence "x\<in>A'" using xAorB by simp
          hence xnotB : "x\<notin>B" using AAminusB by blast
          have "x\<notin>uCone les B'"
          proof -
            { 
              assume "x\<in>uCone les B'"
              with uCone_def have "x\<in> \<Union> ((ucone les) ` B')" by (rule subst)
              hence "\<exists>b\<in>B'. x\<in> ucone les b" by blast
              then obtain b where bB : "b\<in>B'" and x_ucone_b : "x\<in> ucone les b" by (rule bexE)
              have "x\<in> {z. les b z}" using ucone_def and x_ucone_b by (rule subst)  
              hence "les b x" by simp
              with bB and xMin have "False" by blast
            }
            thus "x\<notin>uCone les B'" by (rule notI)
          qed
          with xnotBdash have "x\<notin>B'\<union>uCone les B'" by blast
          moreover
          have "x\<notin>B" by (rule xnotB) 
          ultimately show "x\<notin>C" using B_C by blast
        qed
      qed
    }
  qed (*?A''\<subseteq>A-C*)
(*Preliminary for showing A - (?A''\<union>(uCone les ?A'')) = C - (?A''\<union>(uCone les ?A'')), 
which is third part needed for  A'' to witness "lessP les A C" : *)
  have "A'\<subseteq>A'\<union>B'" by simp
  hence AuConeSubset : "A'\<union>(uCone les A') \<subseteq> ?A''\<union>(uCone les ?A'')" using 
     les_trans and les_irr and finiteAB by (rule subsetCones)
  have "B'\<subseteq>A'\<union>B'" by simp
  hence BuConeSubset : "B'\<union>(uCone les B') \<subseteq> ?A''\<union>(uCone les ?A'')" using 
     les_trans and les_irr and finiteAB by (rule subsetCones)
  have A_C : "A - (?A''\<union>(uCone les ?A'')) = C - (?A''\<union>(uCone les ?A''))" 
     (*Third part needed for  A'' to witness "lessP les A C"*)
  proof (rule subset_antisym)
    show "A - (?A''\<union>(uCone les ?A'')) \<subseteq> C - (?A''\<union>(uCone les ?A''))"
    proof (rule subsetI)
      fix x
      assume xAminusA'' : "x \<in> A - (?A''\<union>(uCone les ?A''))"
      hence xA : "x \<in> A" by simp
      moreover
      have xNotuCone : "x \<notin> ?A''\<union>(uCone les ?A'')" using  xAminusA'' by simp
      hence "x \<notin> A'\<union>(uCone les A')" using AuConeSubset by blast
      ultimately have "x \<in> A-(A'\<union>(uCone les A'))" by simp
      with A_B have "x \<in> B-(A'\<union>(uCone les A'))" by (rule subst)
      hence xB : "x \<in> B" by simp
      moreover
      have "x \<notin> B'\<union>(uCone les B')" using BuConeSubset and xNotuCone  by blast
      ultimately have "x \<in> B-(B'\<union>(uCone les B'))" by simp
      with B_C have "x \<in> C-(B'\<union>(uCone les B'))" by (rule subst)
      hence "x \<in> C" by simp
      thus "x \<in> C - (?A''\<union>(uCone les ?A''))" using xNotuCone by simp
    qed
    show "C - (?A''\<union>(uCone les ?A'')) \<subseteq> A - (?A''\<union>(uCone les ?A''))"
    proof (rule subsetI)
      fix x
      assume xCminusA'' : "x \<in> C - (?A''\<union>(uCone les ?A''))"
      hence xC : "x \<in> C" by simp
      moreover
      have xNotuCone : "x \<notin> ?A''\<union>(uCone les ?A'')" using  xCminusA'' by simp
      hence "x \<notin> B'\<union>(uCone les B')" using BuConeSubset by blast
      ultimately have "x \<in> C-(B'\<union>(uCone les B'))" by simp
      with B_C[symmetric] have "x \<in> B-(B'\<union>(uCone les B'))" by (rule subst)
      hence xB : "x \<in> B" by simp
      moreover
      have "x \<notin> A'\<union>(uCone les A')" using AuConeSubset and xNotuCone by blast
      ultimately have "x \<in> B-(A'\<union>(uCone les A'))" by simp
      with A_B[symmetric] have "x \<in> A-(A'\<union>(uCone les A'))" by (rule subst)
      hence "x \<in> A" by simp
      thus "x \<in> A - (?A''\<union>(uCone les ?A''))" using xNotuCone by simp
    qed
  qed
(*Now put the results together:*)
  have "?A''\<noteq>{} \<and> A - (?A''\<union>(uCone les ?A'')) = C - (?A''\<union>(uCone les ?A''))" 
     using Adashnonempty and A_C by (rule conjI)
  hence "(\<exists>A''\<subseteq>A-C. A''\<noteq>{} \<and> A-(A''\<union>(uCone les A'')) = C-(A''\<union>(uCone les A'')))" using Adash_AminusC by blast
  with finiteA have "(finite A \<and> (\<exists>A''\<subseteq>A-C. A''\<noteq>{} \<and> A-(A''\<union>(uCone les A'')) = C-(A''\<union>(uCone les A''))))"
     by (rule conjI)
  with lessP_def[symmetric] show ?thesis by (rule subst)
qed

(*I also have an independent proof (at the end of the file) but in fact it is a simple corollary 
of transitivity and irreflexivity:*)
lemma lift_asym : (*Lemma 3 in note*)
  assumes les_irr : "\<And>x. \<not> (les x x)"
      and les_trans : "\<And>x y z. (les x y) \<Longrightarrow> (les y z) \<Longrightarrow> (les x z)"
      and AB : "lessP les A B"
      and finiteA : "finite A"
      and finiteB : "finite B"
  assumes AB : "lessP les A B"
  shows "\<not>(lessP les B A)"
proof -
  { assume BA : "lessP les B A"
    have "lessP les B B" using les_irr and les_trans and BA and AB by (rule lift_transitive)
    moreover have "\<not>(lessP les B B)" by (rule lift_irreflexive)
    ultimately have "False" by simp
  }
  thus ?thesis by (rule notI)
qed

(*Used once in proof of main theorem but maybe in an irrelevant branch*)
lemma lift_subset : 
  assumes BsubA : "B \<subset> A"
    and finiteA : "finite A"
  shows "lessP les A B"
proof -
  have "A-B\<noteq>{}" using BsubA by blast (*A-B is witness for "lessP les A B"*)
  moreover have "A-(A-B) = B-(A-B)"  using BsubA by blast
  hence "A-((A-B)\<union>(uCone les (A-B))) = B-((A-B)\<union>(uCone les (A-B)))" by blast
  moreover have "A-B\<subseteq>A-B" by simp
  ultimately have "(\<exists>A'\<subseteq>A-B. A'\<noteq>{} \<and> A-(A'\<union>(uCone les A')) = B-(A'\<union>(uCone les A')))" by blast
  with finiteA have "(finite A \<and> (\<exists>A'\<subseteq>A-B. A'\<noteq>{} \<and> A-(A'\<union>(uCone les A')) = B-(A'\<union>(uCone les A'))))"
     by (rule conjI)
  thus ?thesis using lessP_def by blast  
qed

(*construction needed later in proof of main theorem:
Given a set A and an element a, put in all elements from U that are better 
than a, and remove a*)
text_raw {*\DefineSnippet{replaceWithPreferred}{*}
definition 
  replaceWithPreferred :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
  where "replaceWithPreferred les a A U = (A \<union> {a'\<in>U. les a a'})-{a}"
text_raw {*}%EndSnippet*}

(*24.2.17*)
lemma replaceStaysFinite :
  assumes finiteA : "finite A"
  and finiteU : "finite U"
  shows "finite (replaceWithPreferred les a A U)"
proof -
  have "finite {a'\<in>U. les a a'}" using finiteU by simp
  hence "finite (A \<union> {a'\<in>U. les a a'})" using finiteA by simp
  hence "finite ((A \<union> {a'\<in>U. les a a'})-{a})" by simp
  with replaceWithPreferred_def[symmetric] show ?thesis by (rule subst)
qed

(*24.2.17*)
lemma replaceRetrieve : 
  assumes aA : "a\<in>A"
  shows "A - (replaceWithPreferred les a A U) = {a}"
proof -
thm subst[of "replaceWithPreferred les a A U" "A \<union> {a'\<in>U. les a a'}" "\<lambda>x. A -x = A -x"]
thm arg_cong[of "replaceWithPreferred les a A U" "A \<union> {a'\<in>U. les a a'}" "\<lambda>x. A -x"]
  have "A - (replaceWithPreferred les a A U) = A - ((A \<union> {a'\<in>U. les a a'})-{a})" 
    using replaceWithPreferred_def by (rule arg_cong[of "replaceWithPreferred les a A U" "(A \<union> {a'\<in>U. les a a'})-{a}" "\<lambda>x. A -x"])
    (*can't find unifier?*)
    also have "... = {a}" using aA by blast
    finally show ?thesis .
qed

(*The set A' constructed from player1's preferred set is even better than A.
This truly deserves a lemma of its own*)
text_raw {*\DefineSnippet{replaceIsPreferred}{*}
lemma replaceIsPreferred : 
  assumes a_A : "a\<in>A"
  and finiteA : "finite A"
  shows "lessP les A (replaceWithPreferred les a A U)"
text_raw {*}%EndSnippet*}
proof - 
  have "replaceWithPreferred les a A U = (A \<union> {a'\<in>U. les a a'})-{a}" by (rule replaceWithPreferred_def)
  also have "((A \<union> {a'\<in>U. les a a'})-{a}) - A = ((A \<union> {a'\<in>U. les a a'})-A) - {a}" by blast
  also have "(A \<union> {a'\<in>U. les a a'})-A = {a'\<in>U-A. les a a'}" by blast
  finally have "(replaceWithPreferred les a A U) - A = {a'\<in>U-A. les a a'}-{a}" .
  hence "\<forall>b\<in>(replaceWithPreferred les a A U) - A. les a b" by blast
  moreover 
  {
    have "replaceWithPreferred les a A U = (A \<union> {a'\<in>U. les a a'})-{a}" by (rule replaceWithPreferred_def)
    also have "A - ... = {a}" using a_A by blast
    finally have "A - replaceWithPreferred les a A U = {a}" .
  }
  hence "a \<in> A - replaceWithPreferred les a A U" by blast 
  ultimately have "\<exists>a' \<in> A - replaceWithPreferred les a A U. 
                   \<forall>b \<in> (replaceWithPreferred les a A U) - A. les a' b" by (rule bexI)
  with lessPOrig_def[symmetric] have "lessPOrig les A (replaceWithPreferred les a A U)" by (rule subst)
  thus ?thesis using finiteA by (rule twoLiftings)
qed

text_raw {*\DefineSnippet{gameform}{*}
(*We define "game form"*)
type_synonym ('O,'S1,'S2) game_form = "('S1 * 'S2) \<Rightarrow> 'O"
(*But that's just the outcome function*)
text_raw {*}%EndSnippet*}

text_raw {*\DefineSnippet{game}{*}
(*A game is a game form plus the preferences of each player*)
type_synonym ('O,'S1,'S2) game = 
   "('O \<Rightarrow> 'O \<Rightarrow> bool) * ('O \<Rightarrow> 'O \<Rightarrow> bool) * (('O,'S1,'S2) game_form)"
text_raw {*}%EndSnippet*}

definition 
  pref1 :: "('O,'S1,'S2) game \<Rightarrow> ('O \<Rightarrow> 'O \<Rightarrow> bool)"
  where "pref1 = fst"

definition 
  pref2 :: "('O,'S1,'S2) game \<Rightarrow> ('O \<Rightarrow> 'O \<Rightarrow> bool)"
  where "pref2 = (fst \<circ> snd)"

definition 
  form :: "('O,'S1,'S2) game \<Rightarrow> ('S1 * 'S2) \<Rightarrow> 'O"
  where "form = (snd \<circ> snd)"

text_raw {*\DefineSnippet{isNash}{*}
definition
  isNash :: "(('O,'S1,'S2) game) \<Rightarrow> 'S1 \<Rightarrow> 'S2 \<Rightarrow> bool"
  where "isNash g s1 s2 = 
     ((\<forall>s1'. \<not>(pref1 g) ((form g) (s1,s2)) ((form g) (s1',s2))) \<and>
      (\<forall>s2'. \<not>(pref2 g) ((form g) (s1,s2)) ((form g) (s1,s2'))))"
text_raw {*}%EndSnippet*}

(*added for R-extension*)
(*win/lose game determined via R1 and R2*)
(*Probably someone_wins (below) could be adapted to use this concept, without 
big difficulty*)
text_raw {*\DefineSnippet{determined}{*}
definition 
  determined :: "((bool,'S1,'S2) game) \<Rightarrow> ('S1 set) \<Rightarrow> ('S2 set) \<Rightarrow> bool"
  where "determined g R1 R2 = ((\<exists>s1\<in>R1. \<forall>s2. (form g) (s1,s2) = True) \<or>
                               (\<exists>s2\<in>R2. \<forall>s1. (form g) (s1,s2) = False))"
text_raw {*}%EndSnippet*}

(*I also defined a predicate isWLGame but this is never used in sequel since 
derivedWLGame fulfils it by construction*)
text_raw {*\DefineSnippet{derivedWLGame}{*}
definition
  derivedWLGame :: "(('O,'S1,'S2) game_form) \<Rightarrow> ('O set) \<Rightarrow> ((bool,'S1,'S2) game)"
  where "derivedWLGame gf Ou = 
     ((\<lambda> ou p. p\<and>\<not>ou), (\<lambda> ou p. ou\<and>\<not>p), (\<lambda>ou. ou\<in>Ou)\<circ>gf)"
text_raw {*}%EndSnippet*}

(*added for R-extension*)
(*needed at all?*)
lemma extractForm :
  shows "form (derivedWLGame gf Ou) = (\<lambda>ou. ou\<in>Ou)\<circ>gf"
proof -
  have "form (derivedWLGame gf Ou) = form ((\<lambda> ou p. p\<and>\<not>ou), (\<lambda> ou p. ou\<and>\<not>p), (\<lambda>ou. ou\<in>Ou)\<circ>gf)" 
     using derivedWLGame_def by (rule arg_cong)
  also have "... = (snd\<circ>snd) ((\<lambda> ou p. p\<and>\<not>ou), (\<lambda> ou p. ou\<and>\<not>p), (\<lambda>ou. ou\<in>Ou)\<circ>gf)"
     using form_def by (rule arg_cong)
  also have "... = (\<lambda>ou. ou\<in>Ou)\<circ>gf" by simp
  finally show "form (derivedWLGame gf Ou) = (\<lambda>ou. ou\<in>Ou)\<circ>gf" .
qed

(*In a win-lose game, existence of a Nash equilibrium means that 
one of the players has a winning strategy.
One direction of Remark 1.4/Remark 4
I had doubts whether we need this lemma but it appears to be used several times.
Needed?*)
text_raw {*\DefineSnippet{someonewins}{*}
lemma someone_wins : 
  assumes isNashWL : "isNash ((derivedWLGame gf Ou)::((bool,'S1,'S2) game)) s1 s2" 
     (is "isNash ?wlG s1 s2")
  shows "(\<forall>s2'. (form ?wlG) (s1,s2') = True) \<or> (\<forall>s1'. (form ?wlG) (s1',s2) = False)"
text_raw {*}%EndSnippet*}
proof (cases "(form ?wlG) (s1,s2) = True") (*Whether player1 wins*)
  assume wins1 : "(form ?wlG) (s1,s2) = True" (*player 1 wins*)
  have "(\<forall>s2'. (form ?wlG) (s1,s2') = True)"
  proof - 
    have "((\<forall>s1'. \<not>(pref1 ?wlG) ((form ?wlG) (s1,s2)) ((form ?wlG) (s1',s2))) \<and>
           (\<forall>s2'. \<not>(pref2 ?wlG) ((form ?wlG) (s1,s2)) ((form ?wlG) (s1,s2'))))" 
       using isNash_def and isNashWL by (rule subst)
    hence "(\<forall>s2'. \<not>(pref2 ?wlG) ((form ?wlG) (s1,s2)) ((form ?wlG) (s1,s2')))" by (rule conjunct2)
    with derivedWLGame_def have "(\<forall>s2'. \<not>(pref2 ((\<lambda> ou p. p\<and>\<not>ou), (\<lambda> ou p. ou\<and>\<not>p), (\<lambda>ou. ou\<in>Ou)\<circ>gf) 
                                             ((form ?wlG) (s1,s2)) ((form ?wlG) (s1,s2'))))" by (rule subst)
    with pref2_def have "(\<forall>s2'. \<not>((fst \<circ> snd) ((\<lambda> ou p. p\<and>\<not>ou), (\<lambda> ou p. ou\<and>\<not>p), (\<lambda>ou. ou\<in>Ou)\<circ>gf) 
                                           ((form ?wlG) (s1,s2)) ((form ?wlG) (s1,s2'))))" by (rule subst[of pref2])
    hence "(\<forall>s2'. \<not>(\<lambda> ou p. ou\<and>\<not>p) ((form ?wlG) (s1,s2)) ((form ?wlG) (s1,s2')))" by simp
    hence "(\<forall>s2'. \<not>( ((form ?wlG) (s1,s2)) \<and> \<not>((form ?wlG) (s1,s2'))))" by simp (*beta reduction*)
    thus "(\<forall>s2'. ((form ?wlG) (s1,s2')) = True)" using wins1 by blast
  qed
  thus ?thesis by (rule disjI1)
  next   (*rest symmetric*)
  assume "\<not>((form ?wlG) (s1,s2) = True)"  
  hence wins2 : "(form ?wlG) (s1,s2) = False" by simp (*player 2 wins*) 
  have "(\<forall>s1'. (form ?wlG) (s1',s2) = False)"
  proof - 
    have "((\<forall>s1'. \<not>(pref1 ?wlG) ((form ?wlG) (s1,s2)) ((form ?wlG) (s1',s2))) \<and>
           (\<forall>s2'. \<not>(pref2 ?wlG) ((form ?wlG) (s1,s2)) ((form ?wlG) (s1,s2'))))" 
       using isNash_def and isNashWL by (rule subst)
    hence "(\<forall>s1'. \<not>(pref1 ?wlG) ((form ?wlG) (s1,s2)) ((form ?wlG) (s1',s2)))" by (rule conjunct1)
    with derivedWLGame_def have "(\<forall>s1'. \<not>(pref1 ((\<lambda> ou p. p\<and>\<not>ou), (\<lambda> ou p. ou\<and>\<not>p), (\<lambda>ou. ou\<in>Ou)\<circ>gf) 
                                             ((form ?wlG) (s1,s2)) ((form ?wlG) (s1',s2))))" by (rule subst)
    with pref1_def have "(\<forall>s1'. \<not>(fst ((\<lambda> ou p. p\<and>\<not>ou), (\<lambda> ou p. ou\<and>\<not>p), (\<lambda>ou. ou\<in>Ou)\<circ>gf) 
                                    ((form ?wlG) (s1,s2)) ((form ?wlG) (s1',s2))))" by (rule subst[of pref1])
    hence "(\<forall>s1'. \<not>(\<lambda> ou p. p\<and>\<not>ou) ((form ?wlG) (s1,s2)) ((form ?wlG) (s1',s2)))" by simp
    hence "(\<forall>s1'. \<not>( ((form ?wlG) (s1',s2)) \<and> \<not>((form ?wlG) (s1,s2))))" by simp (*beta reduction*)
    thus "(\<forall>s1'. ((form ?wlG) (s1',s2)) = False)" using wins2 by blast
  qed
  thus ?thesis by (rule disjI2)
qed

(*added for R-extension*)
(*game form determined via R1 and R2*)
text_raw {*\DefineSnippet{determinedForm}{*}
definition 
  determinedForm :: "(('O,'S1,'S2) game_form) \<Rightarrow> ('S1 set) \<Rightarrow> ('S2 set) \<Rightarrow> bool"
  where "determinedForm gf R1 R2 = (\<forall> Ou. determined (derivedWLGame gf Ou) R1 R2)"
text_raw {*}%EndSnippet*}
  
(*Note that the bigger a set the easier it is to enforce.*)
(*notion from paper but in my formal development I prefer an exact notion of enforcement.*)
definition
  canEnforce1 ::  "(('O,'S1,'S2) game_form) \<Rightarrow> ('O set) \<Rightarrow> bool"
  where "canEnforce1 f Ou = (\<exists>s1. \<forall>s2. f(s1,s2)\<in>Ou)"
definition
  canEnforce2 ::  "(('O,'S1,'S2) game_form) \<Rightarrow> ('O set) \<Rightarrow> bool"
  where "canEnforce2 f Ou = (\<exists>s2. \<forall>s1. f(s1,s2)\<in>Ou)"

(*This is aimed at exact enforcement not an overapproximation*)
text_raw {*\DefineSnippet{enforceSet}{*}
definition
  enforceSet1 ::  "(('O,'S1,'S2) game_form) \<Rightarrow> 'S1 \<Rightarrow> ('O set)"
  where "enforceSet1 f s1 = {ou. \<exists>s2. f(s1,s2) = ou}"
text_raw {*}%EndSnippet*}
definition
  enforceSet2 ::  "(('O,'S1,'S2) game_form) \<Rightarrow> 'S2 \<Rightarrow> ('O set)"
  where "enforceSet2 f s2 = {ou. \<exists>s1. f(s1,s2) = ou}"

lemma enforceSet1_range :
  shows "enforceSet1 f s1 \<subseteq> range f"
proof -
  have "enforceSet1 f s1 = {ou. \<exists>s2. f(s1,s2) = ou}" by (rule enforceSet1_def)
  also have "... = {ou. \<exists>s\<in> ({s1}\<times>UNIV). ou = f s}" using enforceSet1_def by blast
  also have "... \<subseteq> range f" by blast
  finally show ?thesis .
qed

lemma enforceSet1_nonempty :
  shows "\<forall>s1. enforceSet1 f s1 \<noteq> {}"
proof -
  {
    fix s1
    have "enforceSet1 f s1 = {ou. \<exists>s2. f(s1,s2) = ou}" by (rule enforceSet1_def)
    also have "... = {ou. \<exists>s\<in> ({s1}\<times>UNIV). ou = f s}" using enforceSet1_def by blast
    also have "... \<noteq> {}" by blast
    finally have "enforceSet1 f s1 \<noteq> {}" .
  }
  thus ?thesis by (rule allI)
qed

lemma enforceSet2_nonempty :
  shows "\<forall>s2. enforceSet2 f s2 \<noteq> {}"
proof -
  {
    fix s2
    have "enforceSet2 f s2 = {ou. \<exists>s1. f(s1,s2) = ou}" by (rule enforceSet2_def)
    also have "... = {ou. \<exists>s\<in> (UNIV\<times>{s2}). ou = f s}" using enforceSet2_def by blast
    also have "... \<noteq> {}" by blast
    finally have "enforceSet2 f s2 \<noteq> {}" .
  }
  thus ?thesis by (rule allI)
qed
(*needed at all?*)
text_raw {*\DefineSnippet{enforceSets}{*}
definition
  enforceSets1 ::  "(('O,'S1,'S2) game_form) \<Rightarrow> ('O set set)"
  where "enforceSets1 f = range (enforceSet1 f)"
text_raw {*}%EndSnippet*}
(*If you prefer : {Ou. \<exists>s1. enforceSet1 f s1 = Ou}*)
definition
  enforceSets2 ::  "(('O,'S1,'S2) game_form) \<Rightarrow> ('O set set)"
  where "enforceSets2 f = range (enforceSet2 f)"

(*image_is_empty could be used*)
lemma enforceSets1_nonempty :
  shows "enforceSets1 f \<noteq> {}"
proof - 
  have "enforceSets1 f = (enforceSet1 f) ` UNIV" by (rule enforceSets1_def)
  thus ?thesis by blast
qed

(*This is not used. I use enforceSets1_witness instead*)
lemma enforceSets1_members_nonempty :
  shows "{} \<notin> enforceSets1 f"
proof -
  {
    assume wrong_hyp : "{} \<in> enforceSets1 f"
    have "\<not>(\<exists>s1. enforceSet1 f s1 = {})" using enforceSet1_nonempty by simp
    moreover
    have "{}\<in>(enforceSet1 f) ` UNIV" using enforceSets1_def and wrong_hyp by (rule subst)
    hence "\<exists>s1. enforceSet1 f s1 = {}" by blast 
    ultimately have "False" by (rule notE)
  }
  thus ?thesis by (rule notI)
qed

(*proof reuses idea from enforceSets1_members_nonempty*)
lemma enforceSets1_witness :
  assumes M_enforceSets1 : "M\<in>enforceSets1 f"
  shows "\<exists>s1. enforceSet1 f s1 = M"
proof -    
  have "M\<in>(enforceSet1 f) ` UNIV" using enforceSets1_def and M_enforceSets1 by (rule subst)
  thus ?thesis by blast 
qed


(*added for R-extension*)
lemma enforceSets2_witness :
  assumes M_enforceSets2 : "M\<in>enforceSets2 f"
  shows "\<exists>s2. enforceSet2 f s2 = M"
proof -    
  have "M\<in>(enforceSet2 f) ` UNIV" using enforceSets2_def and M_enforceSets2 by (rule subst)
  thus ?thesis by blast 
qed

lemma enforceSets1_range :
  shows "enforceSets1 f \<subseteq> Pow (range f)"
proof -
  have "\<And>s1. enforceSet1 f s1 \<subseteq> range f" by (rule enforceSet1_range) 
  hence "range (enforceSet1 f) \<subseteq> Pow (range f)" by blast
  with enforceSets1_def[symmetric] show ?thesis by (rule subst)
qed

(*Added for R-extension*)
lemma enforceSetsR1_range :
  shows "(enforceSet1 f) ` R1 \<subseteq> Pow (range f)"
proof -
  have "\<And>s1. enforceSet1 f s1 \<subseteq> range f" by (rule enforceSet1_range) 
  hence "range (enforceSet1 f) \<subseteq> Pow (range f)" by blast
  thus "(enforceSet1 f) `R1  \<subseteq> Pow (range f)" by blast
qed

(*added for R-extension*)
(*needed?*)
lemma enforceComplements :
  assumes enforcesM : "M \<in> enforceSets1 (form g)"
  shows "\<forall>M2\<subseteq>range (form g) - M. M2\<notin> enforceSets2 (form g)"
proof 
  fix M2
  have "\<exists>s1. enforceSet1 (form g) s1 = M" using enforcesM by (rule enforceSets1_witness)
  then obtain s1 where s1EnforcesM : "enforceSet1 (form g) s1 = M" by (rule exE)
  {
  assume M2DisjM : "M2\<subseteq>range (form g) - M"
  have "M2\<notin> enforceSets2 (form g)"
  proof 
    assume "M2 \<in> enforceSets2 (form g)"
    hence "\<exists>s2. enforceSet2 (form g) s2 = M2" by (rule enforceSets2_witness)
    then obtain s2 where s2EnforcesM2 : "enforceSet2 (form g) s2 = M2" by (rule exE)
    with enforceSet2_def have "{ou. \<exists>s1. (form g)(s1,s2) = ou}  = M2" by (rule subst)
    hence "(form g)(s1,s2) \<in> M2" by blast 
    hence "(form g)(s1,s2) \<notin> M" using M2DisjM by blast
    moreover 
    have "{ou. \<exists>s2. (form g)(s1,s2) = ou}  = M" using enforceSet1_def and s1EnforcesM by (rule subst)
    hence "(form g)(s1,s2) \<in> M" by blast
    ultimately show False by (rule notE)
  qed 
  }
  thus "M2\<subseteq>range (form g) - M \<longrightarrow> M2\<notin> enforceSets2 (form g)" by (rule impI)
qed

(*Added for R-extension*)
(*One direction of Lemma 6 in paper*)
text_raw {*\DefineSnippet{determinedFormViaImplEnforceOutc}{*}
lemma determined_form_via_impl_enforce_outc : 
  assumes det : "determinedForm gf R1 R2"
  shows "(\<forall> Ou. (\<exists>s1\<in>R1. enforceSet1 gf s1 \<subseteq> Ou)\<or>
                (\<exists>s2\<in>R2. enforceSet2 gf s2 \<subseteq> (range gf) - Ou))"
text_raw {*}%EndSnippet*}
proof 
  fix Ou
  have "(\<forall> Ou. determined (derivedWLGame gf Ou) R1 R2)" using determinedForm_def and det by (rule subst)
  hence "determined (derivedWLGame gf Ou) R1 R2" by (rule spec)
  with determined_def have 
     "((\<exists>s1\<in>R1. \<forall>s2. (form (derivedWLGame gf Ou)) (s1,s2) = True) \<or>
       (\<exists>s2\<in>R2. \<forall>s1. (form (derivedWLGame gf Ou)) (s1,s2) = False))" by (rule subst)
  moreover
  {
    assume "\<exists>s1\<in>R1. \<forall>s2. (form (derivedWLGame gf Ou)) (s1,s2) = True"
    with extractForm have "\<exists>s1\<in>R1. \<forall>s2. ((\<lambda>ou. ou\<in>Ou)\<circ>gf) (s1,s2) = True" 
       by (rule subst[of "form (derivedWLGame gf Ou)"])
    then obtain s1 where s1R1 : "s1\<in>R1" and 
       s1winning : "\<forall>s2. ((\<lambda>ou. ou\<in>Ou)\<circ>gf) (s1,s2) = True" by (rule bexE)
    have "\<forall>s2. gf (s1,s2) \<in> Ou" using s1winning by simp
    hence "{ou. \<exists>s2. gf (s1,s2) = ou} \<subseteq> Ou" by blast 
    with enforceSet1_def[symmetric] have "enforceSet1 gf s1 \<subseteq> Ou" by (rule subst)
    hence "\<exists>s1\<in>R1. enforceSet1 gf s1 \<subseteq> Ou" using s1R1 by (rule bexI)
    hence "(\<exists>s1\<in>R1. enforceSet1 gf s1 \<subseteq> Ou)\<or>(\<exists>s2\<in>R2. enforceSet2 gf s2 \<subseteq> (range gf) - Ou)" by (rule disjI1)
  }
  moreover
  {
    assume "\<exists>s2\<in>R2. \<forall>s1. (form (derivedWLGame gf Ou)) (s1,s2) = False"
    with extractForm have "\<exists>s2\<in>R2. \<forall>s1. ((\<lambda>ou. ou\<in>Ou)\<circ>gf) (s1,s2) = False" 
       by (rule subst[of "form (derivedWLGame gf Ou)"])
    then obtain s2 where s2R2 : "s2\<in>R2" and 
       s2winning : "\<forall>s1. ((\<lambda>ou. ou\<in>Ou)\<circ>gf) (s1,s2) = False" by (rule bexE)
    have "\<forall>s1. gf (s1,s2) \<notin> Ou" using s2winning by simp
    hence "{ou. \<exists>s1. gf (s1,s2) = ou} \<subseteq> (range gf) - Ou" by blast 
    with enforceSet2_def[symmetric] have "enforceSet2 gf s2 \<subseteq> (range gf) - Ou" by (rule subst)
    hence "\<exists>s2\<in>R2. enforceSet2 gf s2 \<subseteq> (range gf) - Ou" using s2R2 by (rule bexI)
    hence "(\<exists>s1\<in>R1. enforceSet1 gf s1 \<subseteq> Ou)\<or>(\<exists>s2\<in>R2. enforceSet2 gf s2 \<subseteq> (range gf) - Ou)" by (rule disjI2) 
  }
  ultimately show "(\<exists>s1\<in>R1. enforceSet1 gf s1 \<subseteq> Ou)\<or>(\<exists>s2\<in>R2. enforceSet2 gf s2 \<subseteq> (range gf) - Ou)"
     by (rule disjE)
qed

(*Corollary of determined_form_via_imp_enforce_outc*)
lemma via_nonempty :
  assumes det : "determinedForm gf R1 R2"
  shows "R1\<noteq>{}\<and>R2\<noteq>{}"
proof 
  have "(\<forall> Ou. (\<exists>s1\<in>R1. enforceSet1 gf s1 \<subseteq> Ou)\<or>(\<exists>s2\<in>R2. enforceSet2 gf s2 \<subseteq> (range gf) - Ou))" 
     using det by (rule determined_form_via_impl_enforce_outc)
  hence "(\<exists>s1\<in>R1. enforceSet1 gf s1 \<subseteq> (range gf))\<or>
         (\<exists>s2\<in>R2. enforceSet2 gf s2 \<subseteq> (range gf) - (range gf))" by (rule spec)
  hence "(\<exists>s1\<in>R1. enforceSet1 gf s1 \<subseteq> (range gf))\<or>
         (\<exists>s2\<in>R2. enforceSet2 gf s2 = {})" by simp  
  moreover 
  have "\<forall>s2. enforceSet2 gf s2 \<noteq> {}" by (rule enforceSet2_nonempty)
  hence "\<not> (\<exists>s2\<in>R2. enforceSet2 gf s2 = {})" by simp
  ultimately 
  have "\<exists>s1\<in>R1. enforceSet1 gf s1 \<subseteq> (range gf)" by blast (*A\<or>B, \<not>B \<Longrightarrow> A*)
  thus "R1 \<noteq> {}" by blast
  next (* subgoal R2 \<noteq> {}"*)
    have "(\<forall> Ou. (\<exists>s1\<in>R1. enforceSet1 gf s1 \<subseteq> Ou)\<or>(\<exists>s2\<in>R2. enforceSet2 gf s2 \<subseteq> (range gf) - Ou))" 
     using det by (rule determined_form_via_impl_enforce_outc)
  hence "(\<exists>s1\<in>R1. enforceSet1 gf s1 \<subseteq> {})\<or>
         (\<exists>s2\<in>R2. enforceSet2 gf s2 \<subseteq> (range gf) - {})" by (rule spec)
  hence "(\<exists>s1\<in>R1. enforceSet1 gf s1 = {})\<or>
         (\<exists>s2\<in>R2. enforceSet2 gf s2 \<subseteq> (range gf) - {})" by simp
  moreover
  have "\<forall>s1. enforceSet1 gf s1 \<noteq> {}" by (rule enforceSet1_nonempty)
  hence "\<not> (\<exists>s1\<in>R1. enforceSet1 gf s1 = {})" by simp
  ultimately 
  have "\<exists>s2\<in>R2. enforceSet2 gf s2 \<subseteq> (range gf) - {}" by blast (*A\<or>B, \<not>B \<Longrightarrow> A*)
  thus "R2 \<noteq> {}" by blast
qed

text_raw {*\DefineSnippet{equilibriumtransferfinite}{*}
theorem equilibrium_transfer_finite :
  assumes finiteO : "finite (range (form g))"
      and trans1 : "\<And>a b c. (pref1 g) a b \<Longrightarrow> (pref1 g) b c \<Longrightarrow> (pref1 g) a c"
      and irref1 : "\<And>a. \<not>(pref1 g) a a" 
      and trans2 : "\<And>a b c. (pref2 g) a b \<Longrightarrow> (pref2 g) b c \<Longrightarrow> (pref2 g) a c"
      and irref2 : "\<And>a. \<not>(pref2 g) a a" 
      and det : "determinedForm (form g) R1 R2" 
  shows "\<exists>s1\<in>R1. \<exists>s2\<in>R2. isNash g s1 s2" 
text_raw {*}%EndSnippet*}
proof -
  have "R1\<noteq>{}\<and>R2\<noteq>{}" using det by (rule via_nonempty) 
  hence nonemptyR1 : "R1\<noteq>{}" by (rule conjunct1)
  have enforceSetsR1Finite : "finite ((enforceSet1 (form g)) ` R1)"
  proof -
    have "(enforceSet1 (form g)) ` R1 \<subseteq> Pow (range (form g))" by (rule enforceSetsR1_range)
    moreover have "finite (range (form g))" by (rule finiteO)
    with finite_Pow_iff[symmetric] have "finite (Pow (range (form g)))" by (rule subst)
    ultimately show "finite ((enforceSet1 (form g)) ` R1)" by (rule finite_subset)
  qed
  have pref1_lift_trans : 
     "\<And>A B C. (lessP (pref1 g) A B) \<Longrightarrow> (lessP (pref1 g) B C) \<Longrightarrow> (lessP (pref1 g) A C)" using
     lift_transitive and trans1 and irref1 by blast
  have "(enforceSet1 (form g)) ` R1 \<noteq>{} \<longrightarrow> 
         (\<exists>M\<in>(enforceSet1 (form g)) ` R1. (\<forall>M'\<in>(enforceSet1 (form g)) ` R1. \<not>(lessP (pref1 g) M M')))"
       using pref1_lift_trans and lift_irreflexive and enforceSetsR1Finite by (rule existsMax)  
  moreover have "(enforceSet1 (form g)) ` R1\<noteq>{}" using nonemptyR1 by blast
(*M is preferred set player1 can enforce using R1*)
  ultimately have max1set : 
     "\<exists>M\<in>(enforceSet1 (form g)) ` R1. (\<forall>M'\<in>(enforceSet1 (form g)) ` R1. \<not>(lessP (pref1 g) M M'))" 
     by (rule mp)
  then obtain M where M_enforceSetsR1 : "M\<in>(enforceSet1 (form g)) ` R1" and
                       M_is_max1 : "\<forall>M'\<in>(enforceSet1 (form g)) ` R1. \<not>(lessP (pref1 g) M M')" by (rule bexE)
  have "\<exists>s1\<in> R1. enforceSet1 (form g) s1 = M" using M_enforceSetsR1 by blast
  (*Will need s1 later ? Yes.*)
  then obtain s1 where s1R1 : "s1\<in>R1" and s1_witness : "enforceSet1 (form g) s1 = M" by (rule bexE)
  have "M\<subseteq>range (form g)" using s1_witness and enforceSet1_range by (rule subst) 
  hence finiteM : "finite M" using finiteO by (rule finite_subset)
  with trans2 and irref2 have 
     "M\<noteq>{} \<longrightarrow> (\<exists>m\<in>M. (\<forall>y'\<in>M. \<not>((pref2 g) m y')))" by (rule existsMax)
  moreover have "enforceSet1 (form g) s1 \<noteq> {}" using enforceSet1_nonempty by (rule spec)
  with s1_witness have "M\<noteq>{}" by (rule subst) 
  ultimately have "(\<exists>m\<in>M. (\<forall>y'\<in>M. \<not>((pref2 g) m y')))" by (rule mp)
  then obtain m where m_M : "m\<in>M" and m_is_max2 : "\<forall>y'\<in>M. \<not>((pref2 g) m y')" by (rule bexE)
  let ?M' = "replaceWithPreferred (pref1 g) m M (range (form g))"
  have finiteM' : "finite ?M'" using finiteM and finiteO by (rule replaceStaysFinite)
  have cannot_enforce_Mdash : "\<forall>Msub. Msub\<subseteq>?M' \<longrightarrow> Msub \<notin> (enforceSet1 (form g)) ` R1"
  proof -
    {
      fix Msub 
      {
        assume Msub_sub : "Msub\<subseteq>?M'"
        {
          assume "Msub \<in> (enforceSet1 (form g)) ` R1"      
          with M_is_max1 have "\<not>(lessP (pref1 g) M Msub)" by (rule bspec) 
          moreover have "lessP (pref1 g) M Msub"
(*Don't we have
lessP (pref1 g) M ?M' by construction AND
lessP (pref1 g) ?M Msub because Msub\<subseteq>?M
and hence
lessP (pref1 g) M Msub by transitivity ?
*)
          proof (cases "Msub\<subset>?M'")
            assume "Msub\<subset>?M'"
            hence Mdash_Msub : "lessP (pref1 g) ?M' Msub" using finiteM' by (rule lift_subset)
            have M_Mdash : "lessP (pref1 g) M ?M'" using m_M and finiteM by (rule replaceIsPreferred)
            show "lessP (pref1 g) M Msub" using irref1 and trans1 and M_Mdash and Mdash_Msub by (rule lift_transitive)
          next
            assume "\<not> Msub\<subset>?M'"
            hence "?M' = Msub" using Msub_sub by blast
            moreover have "lessP (pref1 g) M ?M'" using m_M and finiteM by (rule replaceIsPreferred)
            ultimately show "lessP  (pref1 g) M Msub" by (rule subst)
          qed
          ultimately have "False" by (rule notE)
        } 
        hence "Msub \<notin> (enforceSet1 (form g)) ` R1" by (rule notI)
      }
      hence "Msub\<subseteq>?M' \<longrightarrow> Msub \<notin> (enforceSet1 (form g)) ` R1" by (rule impI) 
    }
    thus "\<forall>Msub. Msub\<subseteq>?M' \<longrightarrow> Msub \<notin> (enforceSet1 (form g)) ` R1" by (rule allI)
  qed
(*Just a bit of massage of cannot_enforce_Mdash*)
  hence "\<forall>Msub. Msub\<subseteq>?M' \<longrightarrow> \<not> (\<exists>s1\<in>R1. Msub = enforceSet1 (form g) s1)" by blast
  hence cannot_enforce_Mdash_alt : "\<not> (\<exists>s1\<in>R1. enforceSet1 (form g) s1 \<subseteq>?M')" by blast
(*Since player 1 cannot enforce ?M', player can enforce the complement*)
  have "(\<forall> Ou. (\<exists>s1\<in>R1. enforceSet1 (form g) s1 \<subseteq> Ou)\<or>
               (\<exists>s2\<in>R2. enforceSet2 (form g) s2 \<subseteq> (range (form g)) - Ou))" 
     using det by (rule determined_form_via_impl_enforce_outc)
  hence "(\<exists>s1\<in>R1. enforceSet1 (form g) s1 \<subseteq> ?M')\<or>
         (\<exists>s2\<in>R2. enforceSet2 (form g) s2 \<subseteq> (range (form g)) - ?M')" by (rule spec)
  hence "(\<exists>s2\<in>R2. enforceSet2 (form g) s2 \<subseteq> (range (form g)) - ?M')" 
     using cannot_enforce_Mdash_alt by blast
  then obtain s2 where s2R2 : "s2\<in>R2" and 
     s2_witness : "enforceSet2 (form g) s2 \<subseteq> (range (form g)) - ?M'" by (rule bexE)
  have outcome_m : "(form g) (s1,s2) = m"
  proof -
    have "(form g) (s1,s2) \<in> {ou. \<exists>s2. (form g) (s1,s2) = ou}" by blast
    with enforceSet1_def[symmetric] have "(form g) (s1,s2) \<in> enforceSet1 (form g) s1" by (rule subst)
    with s1_witness have outcome_M : "(form g) (s1,s2) \<in> M" by (rule subst)
    moreover
    have "(form g) (s1,s2) \<in> {ou. \<exists>s1. (form g) (s1,s2) = ou}" by blast
    with enforceSet2_def[symmetric] have "(form g) (s1,s2) \<in> enforceSet2 (form g) s2" by (rule subst)
    with s2_witness have outcome_not_Mdash : "(form g) (s1,s2) \<notin> ?M'" by blast 
    ultimately have "(form g) (s1,s2) \<in> M-?M'" by simp
    moreover
    have "M-?M' = {m}" using m_M by (rule replaceRetrieve)
    ultimately show "(form g) (s1,s2) = m" using replaceWithPreferred_def by blast 
  qed
  have s1s2nd_is_Nash : "isNash g s1 s2"
  proof - 
    have "(\<forall>s1'. \<not>(pref1 g) ((form g) (s1,s2)) ((form g) (s1',s2)))" (*first half of Nash def*)
    proof (rule allI)
      fix s1'
      {
        assume "(pref1 g) ((form g) (s1,s2)) ((form g) (s1',s2))"
        with outcome_m have m_s1' : "(pref1 g) m ((form g) (s1',s2))" by (rule subst)
        hence "((form g) (s1',s2))\<in>{a'\<in>(range (form g)). (pref1 g) m a'}" by simp (*wow*)
        hence "((form g) (s1',s2))\<in>M \<union>{a'\<in>(range (form g)). (pref1 g) m a'}" by simp
(*M => M - m ? SLR*)
        hence "((form g) (s1',s2))\<in>{m} \<or> 
               ((form g) (s1',s2))\<in>(M \<union>{a'\<in>(range (form g)). (pref1 g) m a'})-{m}" by simp (*wow*)
        moreover
        {
          assume "((form g) (s1',s2))\<in>{m}"
          hence "((form g) (s1',s2)) = m" by simp
          hence "(pref1 g) m m" using m_s1' by (rule subst)
          hence "False" using irref1 by simp
        }
        moreover
        {
          assume "((form g) (s1',s2))\<in>(M \<union>{a'\<in>(range (form g)). (pref1 g) m a'})-{m}"
          also have "(M \<union>{a'\<in>(range (form g)).  (pref1 g) m a'})-{m} = ?M'" by (rule replaceWithPreferred_def[symmetric])
          finally have "((form g) (s1',s2))\<in>?M'" .
          moreover 
          have "(form g) (s1',s2) \<in> {ou. \<exists>s1. (form g) (s1,s2) = ou}" by blast
          with enforceSet2_def[symmetric] have "(form g) (s1',s2) \<in> enforceSet2 (form g) s2" by (rule subst)
          ultimately have "(enforceSet2 (form g) s2) \<inter> ?M' \<noteq> {}" by blast
          hence "False" using s2_witness by blast
        }
        ultimately have "False" by (rule disjE)
      }
      thus "\<not> (pref1 g) ((form g) (s1,s2)) ((form g) (s1',s2))" by (rule notI)
    qed  
    moreover
    have "(\<forall>s2'. \<not>(pref2 g) ((form g) (s1,s2)) ((form g) (s1,s2')))" (*second half of Nash def*)
    proof (rule allI)
      fix s2'
      have "M = enforceSet1 (form g) s1" by (rule s1_witness[symmetric])
      also have "... = {ou. \<exists>s2. (form g) (s1,s2) = ou}" by (rule enforceSet1_def)
      finally have "M = {ou. \<exists>s2. (form g) (s1,s2) = ou}" .
      hence "((form g) (s1,s2'))\<in>M" by blast
      moreover
      have "\<forall>y'\<in>M. \<not>((pref2 g) m y')" by (rule m_is_max2)
      ultimately have "\<not>((pref2 g) m ((form g) (s1,s2')))" by (rule bspec[rotated 1])
(*I also tried to prove the hypothesis of bspec in a different order but did not work.*)
      with outcome_m[symmetric] show "\<not>((pref2 g) ((form g) (s1,s2)) ((form g) (s1,s2')))" by (rule subst)
    qed
    ultimately have "(\<forall>s1'. \<not>(pref1 g) ((form g) (s1,s2)) ((form g) (s1',s2))) \<and>
                     (\<forall>s2'. \<not>(pref2 g) ((form g) (s1,s2)) ((form g) (s1,s2')))" by (rule conjI)
    with isNash_def[symmetric] show "isNash g s1 s2" by (rule subst)
  qed
  hence "\<exists>s2 \<in> R2. isNash g s1 s2" using s2R2 by (rule bexI)
  thus "\<exists>s1\<in>R1. \<exists>s2\<in>R2. isNash g s1 s2" using s1R1 by (rule bexI)
qed


(*
ARCHIVE OF UNNEEDED PROOFS: 
*)

(*Same as  lift_antisym but with independent, quite complicated proof.*)
lemma liftAlt_asym : (*Lemma 3 in note*)
(*It's not so elegant that the lemma has so many hypotheses but the aim is to require only what is 
really needed for the proof.*)
  assumes les_irr : "\<And>x. \<not> (les x x)"
      and les_trans : "\<And>x y z. (les x y) \<Longrightarrow> (les y z) \<Longrightarrow> (les x z)"
      and AB : "lessP les A B"
      and finiteA : "finite A"
      and finiteB : "finite B"
  shows "\<not>(lessP les B A)"
proof -
  {
    assume "lessP les B A" (*to derive a contradiction*)
    with lessP_def have  
       "(finite B \<and> (\<exists>B'\<subseteq>B-A. B'\<noteq>{} \<and> B-(B'\<union>(uCone les B')) = A-(B'\<union>(uCone les B'))))" by (rule subst)
    hence "\<exists>B'\<subseteq>B-A. B'\<noteq>{} \<and> B-(B'\<union>(uCone les B')) = A-(B'\<union>(uCone les B'))" by (rule conjunct2)
    then obtain B' where B_witn : "B'\<subseteq>B-A \<and> B'\<noteq>{} \<and> B-(B'\<union>(uCone les B')) = A-(B'\<union>(uCone les B'))" by (rule exE)
    have "lessP les A B" by (rule AB)
    with lessP_def have 
       "(finite A \<and> (\<exists>A'\<subseteq>A-B. A'\<noteq>{} \<and> A-(A'\<union>(uCone les A')) = B-(A'\<union>(uCone les A'))))" by (rule subst) 
    hence "\<exists>A'\<subseteq>A-B. A'\<noteq>{} \<and> A-(A'\<union>(uCone les A')) = B-(A'\<union>(uCone les A'))" by (rule conjunct2)
    then obtain A' where A_witn : "A'\<subseteq>A-B \<and> A'\<noteq>{} \<and> A-(A'\<union>(uCone les A')) = B-(A'\<union>(uCone les A'))"  by (rule exE)
(*finiteness of A'\<union>B'*)
    hence AAminusB : "A'\<subseteq>A-B" by (rule conjunct1)
    hence AA : "A'\<subseteq>A" by blast
    with finiteA have "finite A'" by (rule rev_finite_subset)
    moreover
    have BBminusA : "B'\<subseteq>B-A" using B_witn by (rule conjunct1)
    hence BB : "B'\<subseteq>B" by blast
    with finiteB have "finite B'" by (rule rev_finite_subset)
    ultimately have finiteWitn : "finite (A'\<union>B')" by (rule finite_UnI)
    with les_trans and les_irr have 
       "A'\<union>B'\<noteq>{} \<longrightarrow> (\<exists>x\<in>A'\<union>B'. \<forall>y\<in>A'\<union>B'. \<not>(les y x))" by (rule existsMin)
    moreover
(*Non-emptyness of A'\<union>B'*)
    {
      have "A'\<noteq>{}" using A_witn by simp
      moreover have "B'\<noteq>{}" using B_witn by simp
      ultimately have "A'\<union>B'\<noteq>{}" by simp
    }
    ultimately have "\<exists>x\<in>A'\<union>B'. \<forall>y\<in>A'\<union>B'. \<not>(les y x)" by (rule mp)
    then obtain x where xAB : "x\<in>A'\<union>B'" and xMin : "\<forall>y\<in>A'\<union>B'. \<not>(les y x)" by (rule bexE)
    have xAorB : "x\<in>A' \<or> x\<in>B'" using xAB by simp
    moreover
    {
      assume xA' : "x\<in>A'"
      hence xnotB : "x\<notin>B" using AAminusB by blast
      hence "x\<notin>B'" using BB by blast
      moreover
      have "x\<notin> uCone les B'"
      proof -
        {
          assume "x\<in> uCone les B'" 
          with uCone_def have "x\<in> \<Union> ((ucone les) ` B')" by (rule subst)
          hence "\<exists>b\<in>B'. x\<in> ucone les b" by blast
          then obtain b where bB : "b\<in>B'" and x_ucone_b : "x\<in> ucone les b" by (rule bexE)
          have "x\<in> {z. les b z}" using ucone_def and x_ucone_b by (rule subst)  
          hence "les b x" by simp
          with bB and xMin have "False" by blast
        }
        thus "x\<notin> uCone les B'" by (rule notI)
      qed
      ultimately have "x\<notin>B'\<union>uCone les B'" by simp
      moreover 
      have "A-(B'\<union>(uCone les B')) = B-(B'\<union>(uCone les B'))" using B_witn by simp
      moreover
      have "x\<in>A" using xA' and AA by blast
      ultimately have "x\<in>B" by blast
      with xnotB have "False" by (rule notE)
    }
    moreover (*symmetric, in paper you simply write wlog*)
    {
      assume xB' : "x\<in>B'"
      hence xnotA : "x\<notin>A" using BBminusA by blast
      hence "x\<notin>A'" using AA by blast
      moreover
      have "x\<notin> uCone les A'"
      proof -
        {
          assume "x\<in> uCone les A'" 
          with uCone_def have "x\<in> \<Union> ((ucone les) ` A')" by (rule subst)
          hence "\<exists>a\<in>A'. x\<in> ucone les a" by blast
          then obtain a where aA : "a\<in>A'" and x_ucone_a : "x\<in> ucone les a" by (rule bexE)
          have "x\<in> {z. les a z}" using ucone_def and x_ucone_a by (rule subst)  
          hence "les a x" by simp
          with aA and xMin have "False" by blast
        }
        thus "x\<notin> uCone les A'" by (rule notI)
      qed
      ultimately have "x\<notin>A'\<union>uCone les A'" by simp
      moreover 
      have "A-(A'\<union>(uCone les A')) = B-(A'\<union>(uCone les A'))" using A_witn by simp
      moreover
      have "x\<in>B" using xB' and BB by blast
      ultimately have "x\<in>A" by blast
      with xnotA have "False" by (rule notE)    
    }
    ultimately have "False" by (rule disjE)
  } 
  thus ?thesis by (rule notI)
qed

(*Win-lose game: player prefers True, player 2 prefers False*)
definition
  isWLGame :: "((bool,'S1,'S2) game) \<Rightarrow> bool"
  where "isWLGame g = (((pref1 g) = (\<lambda> ou p. p\<and>\<not>ou)) \<and> 
                       ((pref2 g) = (\<lambda> ou p. \<not>p\<and>ou)))"
(*useful for intuition but maybe never used in since derivedWLGame 
fulfils it by construction*)


(*"Corollary" of someone_wins: In a win-lose game, existence of a Nash equilibrium 
means that the losing player is indifferent and hence any deviation on his part 
still gives a Nash equilibrium.
Wow, the corollary has 88 lines of proof!*)
(*It's never used, why did I think it might be useful?*)
lemma nash_indifferent : 
  assumes isNashWL : "isNash ((derivedWLGame gf Ou)::((bool,'S1,'S2) game)) s1 s2" (is "isNash ?wlG s1 s2")
  shows "(\<forall>s2''. isNash (?wlG::(bool,'S1,'S2) game) s1 s2'')   \<or>
         (\<forall>s1''. isNash ?wlG  s1'' s2)"
proof (cases "(\<forall>s2''. form ?wlG (s1,s2'') = True)") (*To exploit someone_wins*)
  assume wins1 : "(\<forall>s2''. form ?wlG (s1,s2'') = True)"  (*player 1 wins*)
  have "(\<forall>s2''. isNash ?wlG s1 s2'')"
  proof (rule allI)
    fix s2''
    have "(\<forall>s1'. \<not>(pref1 ?wlG) ((form ?wlG) (s1,s2'')) ((form ?wlG) (s1',s2'')))" (*first half of Nash def*)
    proof (rule allI)
      fix s1'
      have "True =  form ?wlG (s1,s2'')" using wins1 by simp
      moreover
      have "\<not>((\<lambda> ou p. p \<and>\<not>ou) True ((form ?wlG) (s1',s2'')))" by simp (*pl1 wins so s1' cannot be better*)
      ultimately have "\<not>((\<lambda> ou p. p \<and>\<not>ou) (form ?wlG (s1,s2'')) ((form ?wlG) (s1',s2'')))" by (rule subst)
      hence "\<not>((fst ((\<lambda> ou p. p\<and>\<not>ou), (\<lambda> ou p. ou\<and>\<not>p), (\<lambda>ou. ou\<in>Ou)\<circ>gf))
                  (form ?wlG (s1,s2'')) ((form ?wlG) (s1',s2'')))" by simp
      with derivedWLGame_def[symmetric] have "\<not>((fst ?wlG)
                  (form ?wlG (s1,s2'')) ((form ?wlG) (s1',s2'')))" by (rule subst)
      with pref1_def[symmetric] show "\<not>((pref1 ?wlG)
                  (form ?wlG (s1,s2'')) ((form ?wlG) (s1',s2'')))" by (rule subst[of fst pref1])
    qed
    moreover
    have "(\<forall>s2'. \<not>(pref2 ?wlG) ((form ?wlG) (s1,s2'')) ((form ?wlG) (s1,s2')))" (*second half of Nash def*)
    proof (rule allI)
      fix s2'
      have true1 : "True =  form ?wlG (s1,s2'')" using wins1 by simp
      have true2 : "True =  form ?wlG (s1,s2')" using wins1 by simp
      have "\<not>((\<lambda> ou p. ou\<and>\<not>p) True True)" by simp (*pl2 loses anyway*)
      with true1 have "\<not>((\<lambda> ou p. ou\<and>\<not>p) (form ?wlG (s1,s2'')) True)" by (rule subst)
      with true2 have "\<not>((\<lambda> ou p. ou\<and>\<not>p) (form ?wlG (s1,s2'')) (form ?wlG (s1,s2')))" by (rule subst)
      hence "\<not>(((fst \<circ> snd) ((\<lambda> ou p. p\<and>\<not>ou), (\<lambda> ou p. ou\<and>\<not>p), (\<lambda>ou. ou\<in>Ou)\<circ>gf))
                  (form ?wlG (s1,s2'')) ((form ?wlG) (s1,s2')))" by simp
      with derivedWLGame_def[symmetric] have "\<not>(((fst \<circ> snd) ?wlG)
                  (form ?wlG (s1,s2'')) ((form ?wlG) (s1,s2')))" by (rule subst)
      thm subst[of "(fst \<circ> snd)" pref2 "\<lambda>x.\<not>((x ?wlG)
                  (form ?wlG (s1,s2'')) ((form ?wlG) (s1,s2')))"]
      with pref2_def[symmetric] show "\<not>((pref2 ?wlG)
                  (form ?wlG (s1,s2'')) ((form ?wlG) (s1,s2')))"  by (rule subst[of "fst \<circ> snd" pref2])
    qed
    ultimately have 
      "(\<forall>s1'. \<not>(pref1 ?wlG) ((form ?wlG) (s1,s2'')) ((form ?wlG) (s1',s2''))) \<and>
       (\<forall>s2'. \<not>(pref2 ?wlG) ((form ?wlG) (s1,s2'')) ((form ?wlG) (s1,s2')))" by (rule conjI)
    with isNash_def[symmetric] show "isNash ?wlG s1 s2''" by (rule subst)
  qed 
  thus ?thesis by (rule disjI1)
  next 
  assume loses1 : "\<not>(\<forall>s2''. form ?wlG (s1,s2'') = True)"
  have "isNash ?wlG s1 s2" by (rule isNashWL)
  hence "(\<forall>s2''. (form ?wlG (s1,s2'') = True)) \<or> 
         (\<forall>s1''. (form ?wlG) (s1'',s2) = False)" by (rule someone_wins)
  hence wins2 : "(\<forall>s1''. (form ?wlG) (s1'',s2) = False)" using loses1 by blast(*player 2 wins*)
  (*Rest symmetric to "player 1 wins". But since there are two dimensions of symmetry this is fiddly!*)
  have "(\<forall>s1''. isNash ?wlG  s1'' s2)"
  proof (rule allI)
    fix s1''
    have "(\<forall>s1'. \<not>(pref1 ?wlG) ((form ?wlG) (s1'',s2)) ((form ?wlG) (s1',s2)))" (*first half of Nash def*)
    proof (rule allI)
      fix s1'
      have false1 : "False =  form ?wlG (s1'',s2)" using wins2 by simp
      have false2 : "False =  form ?wlG (s1',s2)" using wins2 by simp
      have "\<not>((\<lambda> ou p. p \<and>\<not>ou) False False)" by simp (*pl1 loses anyway*)
      with false1 have "\<not>((\<lambda> ou p. p \<and>\<not>ou) (form ?wlG (s1'',s2)) False)" by (rule subst)
      with false2 have "\<not>((\<lambda> ou p. p \<and>\<not>ou) (form ?wlG (s1'',s2)) (form ?wlG (s1',s2)))" by (rule subst)
      hence "\<not>((fst ((\<lambda> ou p. p\<and>\<not>ou), (\<lambda> ou p. ou\<and>\<not>p), (\<lambda>ou. ou\<in>Ou)\<circ>gf))
                  (form ?wlG (s1'',s2)) ((form ?wlG) (s1',s2)))" by simp
      with derivedWLGame_def[symmetric] have "\<not>((fst ?wlG)
                  (form ?wlG (s1'',s2)) ((form ?wlG) (s1',s2)))" by (rule subst)
      with pref1_def[symmetric] show "\<not>((pref1 ?wlG)
                  (form ?wlG (s1'',s2)) ((form ?wlG) (s1',s2)))"  by (rule subst[of fst pref1])
    qed
    moreover
    have "(\<forall>s2'. \<not>(pref2 ?wlG) ((form ?wlG) (s1'',s2)) ((form ?wlG) (s1'',s2')))" (*second half of Nash def*)
    proof (rule allI)
      fix s2'
      have "False = ((form ?wlG) (s1'',s2))" using wins2 by simp
      moreover
      have "\<not>((\<lambda> ou p. ou\<and>\<not>p) False ((form ?wlG) (s1'',s2')))" by simp (*pl2 wins so s2' cannot be better*)
      ultimately have "\<not>((\<lambda> ou p. ou\<and>\<not>p) (form ?wlG (s1'',s2)) ((form ?wlG) (s1'',s2')))" by (rule subst)
      hence "\<not>(((fst \<circ> snd) ((\<lambda> ou p. p\<and>\<not>ou), (\<lambda> ou p. ou\<and>\<not>p), (\<lambda>ou. ou\<in>Ou)\<circ>gf))
                  (form ?wlG (s1'',s2)) ((form ?wlG) (s1'',s2')))" by simp
      with derivedWLGame_def[symmetric] have "\<not>(((fst \<circ> snd) ?wlG)
                  (form ?wlG (s1'',s2)) ((form ?wlG) (s1'',s2')))" by (rule subst)
      with pref2_def[symmetric] show "\<not>((pref2 ?wlG)
                  (form ?wlG (s1'',s2)) ((form ?wlG) (s1'',s2')))" by (rule subst[of "fst \<circ> snd" pref2])
    qed
    ultimately have 
      "(\<forall>s1'. \<not>(pref1 ?wlG) ((form ?wlG) (s1'',s2)) ((form ?wlG) (s1',s2))) \<and>
       (\<forall>s2'. \<not>(pref2 ?wlG) ((form ?wlG) (s1'',s2)) ((form ?wlG) (s1'',s2')))" by (rule conjI)
    with isNash_def[symmetric] show "isNash ?wlG s1'' s2" by (rule subst)
  qed 
  thus ?thesis by (rule disjI2)
qed
 
(*Not true at all!*)
(*
lemma enforceComplements2 :
  assumes notEnforcesM2 : "\<forall>M2' \<in> enforceSets2 (form g). \<not> M2' \<subseteq> M2"
  shows "\<exists>M\<in>enforceSets1 (form g). M \<inter> M2={}"
proof -*)

(*Added for R-extension, but probably not even needed.*)
(*
lemma enforceViaR : (*Formalises first paragraph of proof of Lemma 2.4/Theorem 8*)
  assumes determined : "\<forall>Ou. \<exists>s1\<in>R1. \<exists>s2\<in>R2. isNash (derivedWLGame (form g) Ou) s1 s2"
      and enforces1 : "M\<in>enforceSets1 (form g)"
  shows "\<exists>s1\<in>R1. enforceSet1 (form g) s1 \<subseteq> M"
proof -*)

end