Added HOL-ZF to Isabelle.
authorobua
Tue Mar 07 16:03:31 2006 +0100 (2006-03-07)
changeset 19203778507520684
parent 19202 0b9eb4b0ad98
child 19204 b8f7de7ef629
Added HOL-ZF to Isabelle.
src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
src/HOL/Import/replay.ML
src/HOL/IsaMakefile
src/HOL/ZF/Games.thy
src/HOL/ZF/HOLZF.thy
src/HOL/ZF/Helper.thy
src/HOL/ZF/LProd.thy
src/HOL/ZF/MainZF.thy
src/HOL/ZF/Zet.thy
src/HOL/ZF/document/root.tex
     1.1 --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Tue Mar 07 14:09:48 2006 +0100
     1.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Tue Mar 07 16:03:31 2006 +0100
     1.3 @@ -30,7 +30,8 @@
     1.4    DEF_NUM_REP
     1.5    TYDEF_sum
     1.6    DEF_INL
     1.7 -  DEF_INR;
     1.8 +  DEF_INR
     1.9 +  TYDEF_option;
    1.10  
    1.11  type_maps
    1.12    ind > Nat.ind
    1.13 @@ -39,7 +40,8 @@
    1.14    N_1 >  Product_Type.unit
    1.15    prod > "*"
    1.16    num > nat
    1.17 -  sum > "+";
    1.18 +  sum > "+"
    1.19 +  option > Datatype.option;
    1.20  
    1.21  const_renames
    1.22    "==" > "eqeq"
     2.1 --- a/src/HOL/Import/replay.ML	Tue Mar 07 14:09:48 2006 +0100
     2.2 +++ b/src/HOL/Import/replay.ML	Tue Mar 07 16:03:31 2006 +0100
     2.3 @@ -369,7 +369,13 @@
     2.4  		     (entry::cached, normal)
     2.5  		 end)
     2.6  	    else
     2.7 -		raise ERR "import_thms" ("cached theorems are not in-sync, expected: "^thmname^", found: "^thmname')
     2.8 +		let
     2.9 +		    val _ = writeln ("cached theorems are not in-sync,  expected: "^thmname^", found: "^thmname')
    2.10 +		    val _ = writeln ("proceeding with next uncached theorem...")
    2.11 +		in
    2.12 +		    ([], thmname::names)
    2.13 +		end
    2.14 +	(*	raise ERR "import_thms" ("cached theorems are not in-sync, expected: "^thmname^", found: "^thmname')*)
    2.15  	  | zip (thmname::_) (DeltaEntry _ :: _) = 
    2.16   	    raise ERR "import_thms" ("expected theorem '"^thmname^"', but found a delta")
    2.17  	fun zip' xs (History ys) = 
     3.1 --- a/src/HOL/IsaMakefile	Tue Mar 07 14:09:48 2006 +0100
     3.2 +++ b/src/HOL/IsaMakefile	Tue Mar 07 16:03:31 2006 +0100
     3.3 @@ -40,7 +40,8 @@
     3.4    HOL-UNITY \
     3.5    HOL-Unix \
     3.6    HOL-W0 \
     3.7 -  HOL-ex
     3.8 +  HOL-ZF \
     3.9 +  HOL-ex 
    3.10      # ^ this is the sort position
    3.11  
    3.12  all: test images
    3.13 @@ -451,6 +452,14 @@
    3.14    Unix/document/root.bib Unix/document/root.tex
    3.15  	@$(ISATOOL) usedir $(OUT)/HOL Unix
    3.16  
    3.17 +## HOL-ZF
    3.18 +
    3.19 +HOL-ZF: HOL $(LOG)/HOL-ZF.gz
    3.20 +
    3.21 +$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML  \
    3.22 +  ZF/Helper.thy ZF/LProd.thy ZF/HOLZF.thy \
    3.23 +  ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex
    3.24 +	@$(ISATOOL) usedir $(OUT)/HOL ZF
    3.25  
    3.26  ## HOL-Modelcheck
    3.27  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/ZF/Games.thy	Tue Mar 07 16:03:31 2006 +0100
     4.3 @@ -0,0 +1,961 @@
     4.4 +(*  Title:      HOL/ZF/Games.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Steven Obua
     4.7 +
     4.8 +    An application of HOLZF: Partizan Games.
     4.9 +    See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan
    4.10 +*)
    4.11 +
    4.12 +theory Games 
    4.13 +imports MainZF
    4.14 +begin
    4.15 +
    4.16 +constdefs
    4.17 +  fixgames :: "ZF set \<Rightarrow> ZF set"
    4.18 +  "fixgames A \<equiv> { Opair l r | l r. explode l \<subseteq> A & explode r \<subseteq> A}"
    4.19 +  games_lfp :: "ZF set"
    4.20 +  "games_lfp \<equiv> lfp fixgames"
    4.21 +  games_gfp :: "ZF set"
    4.22 +  "games_gfp \<equiv> gfp fixgames"
    4.23 +
    4.24 +lemma mono_fixgames: "mono (fixgames)"
    4.25 +  apply (auto simp add: mono_def fixgames_def)
    4.26 +  apply (rule_tac x=l in exI)
    4.27 +  apply (rule_tac x=r in exI)
    4.28 +  apply auto
    4.29 +  done
    4.30 +
    4.31 +lemma games_lfp_unfold: "games_lfp = fixgames games_lfp"
    4.32 +  by (auto simp add: def_lfp_unfold games_lfp_def mono_fixgames)
    4.33 +
    4.34 +lemma games_gfp_unfold: "games_gfp = fixgames games_gfp"
    4.35 +  by (auto simp add: def_gfp_unfold games_gfp_def mono_fixgames)
    4.36 +
    4.37 +lemma games_lfp_nonempty: "Opair Empty Empty \<in> games_lfp"
    4.38 +proof -
    4.39 +  have "fixgames {} \<subseteq> games_lfp" 
    4.40 +    apply (subst games_lfp_unfold)
    4.41 +    apply (simp add: mono_fixgames[simplified mono_def, rule_format])
    4.42 +    done
    4.43 +  moreover have "fixgames {} = {Opair Empty Empty}"
    4.44 +    by (simp add: fixgames_def explode_Empty)
    4.45 +  finally show ?thesis
    4.46 +    by auto
    4.47 +qed
    4.48 +
    4.49 +constdefs
    4.50 +  left_option :: "ZF \<Rightarrow> ZF \<Rightarrow> bool"
    4.51 +  "left_option g opt \<equiv> (Elem opt (Fst g))"
    4.52 +  right_option :: "ZF \<Rightarrow> ZF \<Rightarrow> bool"
    4.53 +  "right_option g opt \<equiv> (Elem opt (Snd g))"
    4.54 +  is_option_of :: "(ZF * ZF) set"
    4.55 +  "is_option_of \<equiv> { (opt, g) | opt g. g \<in> games_gfp \<and> (left_option g opt \<or> right_option g opt) }"
    4.56 +
    4.57 +lemma games_lfp_subset_gfp: "games_lfp \<subseteq> games_gfp"
    4.58 +proof -
    4.59 +  have "games_lfp \<subseteq> fixgames games_lfp" 
    4.60 +    by (simp add: games_lfp_unfold[symmetric])
    4.61 +  then show ?thesis
    4.62 +    by (simp add: games_gfp_def gfp_upperbound)
    4.63 +qed
    4.64 +
    4.65 +lemma games_option_stable: 
    4.66 +  assumes fixgames: "games = fixgames games"
    4.67 +  and g: "g \<in> games"
    4.68 +  and opt: "left_option g opt \<or> right_option g opt"
    4.69 +  shows "opt \<in> games"
    4.70 +proof -
    4.71 +  from g fixgames have "g \<in> fixgames games" by auto
    4.72 +  then have "\<exists> l r. g = Opair l r \<and> explode l \<subseteq> games \<and> explode r \<subseteq> games"
    4.73 +    by (simp add: fixgames_def)
    4.74 +  then obtain l where "\<exists> r. g = Opair l r \<and> explode l \<subseteq> games \<and> explode r \<subseteq> games" ..
    4.75 +  then obtain r where lr: "g = Opair l r \<and> explode l \<subseteq> games \<and> explode r \<subseteq> games" ..
    4.76 +  with opt show ?thesis
    4.77 +    by (auto intro: Elem_explode_in simp add: left_option_def right_option_def Fst Snd)
    4.78 +qed
    4.79 +    
    4.80 +lemma option2elem: "(opt,g) \<in> is_option_of  \<Longrightarrow> \<exists> u v. Elem opt u \<and> Elem u v \<and> Elem v g"
    4.81 +  apply (simp add: is_option_of_def)
    4.82 +  apply (subgoal_tac "(g \<in> games_gfp) = (g \<in> (fixgames games_gfp))")
    4.83 +  prefer 2
    4.84 +  apply (simp add: games_gfp_unfold[symmetric])
    4.85 +  apply (auto simp add: fixgames_def left_option_def right_option_def Fst Snd)
    4.86 +  apply (rule_tac x=l in exI, insert Elem_Opair_exists, blast)
    4.87 +  apply (rule_tac x=r in exI, insert Elem_Opair_exists, blast) 
    4.88 +  done
    4.89 +
    4.90 +lemma is_option_of_subset_is_Elem_of: "is_option_of \<subseteq> (is_Elem_of^+)"
    4.91 +proof -
    4.92 +  {
    4.93 +    fix opt
    4.94 +    fix g
    4.95 +    assume "(opt, g) \<in> is_option_of"
    4.96 +    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^+)" 
    4.97 +      apply -
    4.98 +      apply (drule option2elem)
    4.99 +      apply (auto simp add: r_into_trancl' is_Elem_of_def)
   4.100 +      done
   4.101 +    then have "(opt, g) \<in> (is_Elem_of^+)"
   4.102 +      by (blast intro: trancl_into_rtrancl trancl_rtrancl_trancl)
   4.103 +  } 
   4.104 +  then show ?thesis by auto
   4.105 +qed
   4.106 +
   4.107 +lemma wfzf_is_option_of: "wfzf is_option_of"
   4.108 +proof - 
   4.109 +  have "wfzf (is_Elem_of^+)" by (simp add: wfzf_trancl wfzf_is_Elem_of)
   4.110 +  then show ?thesis 
   4.111 +    apply (rule wfzf_subset)
   4.112 +    apply (rule is_option_of_subset_is_Elem_of)
   4.113 +    done
   4.114 +  qed
   4.115 +  
   4.116 +lemma games_gfp_imp_lfp: "g \<in> games_gfp \<longrightarrow> g \<in> games_lfp"
   4.117 +proof -
   4.118 +  have unfold_gfp: "\<And> x. x \<in> games_gfp \<Longrightarrow> x \<in> (fixgames games_gfp)" 
   4.119 +    by (simp add: games_gfp_unfold[symmetric])
   4.120 +  have unfold_lfp: "\<And> x. (x \<in> games_lfp) = (x \<in> (fixgames games_lfp))"
   4.121 +    by (simp add: games_lfp_unfold[symmetric])
   4.122 +  show ?thesis
   4.123 +    apply (rule wf_induct[OF wfzf_implies_wf[OF wfzf_is_option_of]])
   4.124 +    apply (auto simp add: is_option_of_def)
   4.125 +    apply (drule_tac unfold_gfp)
   4.126 +    apply (simp add: fixgames_def)
   4.127 +    apply (auto simp add: left_option_def Fst right_option_def Snd)
   4.128 +    apply (subgoal_tac "explode l \<subseteq> games_lfp")
   4.129 +    apply (subgoal_tac "explode r \<subseteq> games_lfp")
   4.130 +    apply (subst unfold_lfp)
   4.131 +    apply (auto simp add: fixgames_def)
   4.132 +    apply (simp_all add: explode_Elem Elem_explode_in)
   4.133 +    done
   4.134 +qed
   4.135 +
   4.136 +theorem games_lfp_eq_gfp: "games_lfp = games_gfp"
   4.137 +  apply (auto simp add: games_gfp_imp_lfp)
   4.138 +  apply (insert games_lfp_subset_gfp)
   4.139 +  apply auto
   4.140 +  done
   4.141 +
   4.142 +theorem unique_games: "(g = fixgames g) = (g = games_lfp)"
   4.143 +proof -
   4.144 +  {
   4.145 +    fix g 
   4.146 +    assume g: "g = fixgames g"
   4.147 +    from g have "fixgames g \<subseteq> g" by auto
   4.148 +    then have l:"games_lfp \<subseteq> g" 
   4.149 +      by (simp add: games_lfp_def lfp_lowerbound)
   4.150 +    from g have "g \<subseteq> fixgames g" by auto
   4.151 +    then have u:"g \<subseteq> games_gfp" 
   4.152 +      by (simp add: games_gfp_def gfp_upperbound)
   4.153 +    from l u games_lfp_eq_gfp[symmetric] have "g = games_lfp"
   4.154 +      by auto
   4.155 +  }
   4.156 +  note games = this
   4.157 +  show ?thesis
   4.158 +    apply (rule iff[rule_format])
   4.159 +    apply (erule games)
   4.160 +    apply (simp add: games_lfp_unfold[symmetric])
   4.161 +    done
   4.162 +qed
   4.163 +
   4.164 +lemma games_lfp_option_stable: 
   4.165 +  assumes g: "g \<in> games_lfp"
   4.166 +  and opt: "left_option g opt \<or> right_option g opt"
   4.167 +  shows "opt \<in> games_lfp"
   4.168 +  apply (rule games_option_stable[where g=g])
   4.169 +  apply (simp add: games_lfp_unfold[symmetric])
   4.170 +  apply (simp_all add: prems)
   4.171 +  done
   4.172 +
   4.173 +lemma is_option_of_imp_games:
   4.174 +  assumes hyp: "(opt, g) \<in> is_option_of"
   4.175 +  shows "opt \<in> games_lfp \<and> g \<in> games_lfp"
   4.176 +proof -
   4.177 +  from hyp have g_game: "g \<in> games_lfp" 
   4.178 +    by (simp add: is_option_of_def games_lfp_eq_gfp)
   4.179 +  from hyp have "left_option g opt \<or> right_option g opt"
   4.180 +    by (auto simp add: is_option_of_def)
   4.181 +  with g_game games_lfp_option_stable[OF g_game, OF this] show ?thesis
   4.182 +    by auto
   4.183 +qed
   4.184 + 
   4.185 +lemma games_lfp_represent: "x \<in> games_lfp \<Longrightarrow> \<exists> l r. x = Opair l r"
   4.186 +  apply (rule exI[where x="Fst x"])
   4.187 +  apply (rule exI[where x="Snd x"])
   4.188 +  apply (subgoal_tac "x \<in> (fixgames games_lfp)")
   4.189 +  apply (simp add: fixgames_def)
   4.190 +  apply (auto simp add: Fst Snd)
   4.191 +  apply (simp add: games_lfp_unfold[symmetric])
   4.192 +  done
   4.193 +
   4.194 +typedef game = games_lfp
   4.195 +  by (blast intro: games_lfp_nonempty)
   4.196 +
   4.197 +constdefs
   4.198 +  left_options :: "game \<Rightarrow> game zet"
   4.199 +  "left_options g \<equiv> zimage Abs_game (zexplode (Fst (Rep_game g)))"
   4.200 +  right_options :: "game \<Rightarrow> game zet"
   4.201 +  "right_options g \<equiv> zimage Abs_game (zexplode (Snd (Rep_game g)))"
   4.202 +  options :: "game \<Rightarrow> game zet"
   4.203 +  "options g \<equiv> zunion (left_options g) (right_options g)"
   4.204 +  Game :: "game zet \<Rightarrow> game zet \<Rightarrow> game"
   4.205 +  "Game L R \<equiv> Abs_game (Opair (zimplode (zimage Rep_game L)) (zimplode (zimage Rep_game R)))"
   4.206 +  
   4.207 +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"
   4.208 +  apply (subst Ext)
   4.209 +  apply (simp add: Repl)
   4.210 +  apply auto
   4.211 +  apply (subst Abs_game_inverse, simp_all add: game_def)
   4.212 +  apply (rule_tac x=za in exI)
   4.213 +  apply (subst Abs_game_inverse, simp_all add: game_def)
   4.214 +  done
   4.215 +
   4.216 +lemma game_split: "g = Game (left_options g) (right_options g)"
   4.217 +proof -
   4.218 +  have "\<exists> l r. Rep_game g = Opair l r"
   4.219 +    apply (insert Rep_game[of g])
   4.220 +    apply (simp add: game_def games_lfp_represent)
   4.221 +    done
   4.222 +  then obtain l r where lr: "Rep_game g = Opair l r" by auto
   4.223 +  have partizan_g: "Rep_game g \<in> games_lfp" 
   4.224 +    apply (insert Rep_game[of g])
   4.225 +    apply (simp add: game_def)
   4.226 +    done
   4.227 +  have "\<forall> e. Elem e l \<longrightarrow> left_option (Rep_game g) e"
   4.228 +    by (simp add: lr left_option_def Fst)
   4.229 +  then have partizan_l: "\<forall> e. Elem e l \<longrightarrow> e \<in> games_lfp"
   4.230 +    apply auto
   4.231 +    apply (rule games_lfp_option_stable[where g="Rep_game g", OF partizan_g])
   4.232 +    apply auto
   4.233 +    done
   4.234 +  have "\<forall> e. Elem e r \<longrightarrow> right_option (Rep_game g) e"
   4.235 +    by (simp add: lr right_option_def Snd)
   4.236 +  then have partizan_r: "\<forall> e. Elem e r \<longrightarrow> e \<in> games_lfp"
   4.237 +    apply auto
   4.238 +    apply (rule games_lfp_option_stable[where g="Rep_game g", OF partizan_g])
   4.239 +    apply auto
   4.240 +    done   
   4.241 +  let ?L = "zimage (Abs_game) (zexplode l)"
   4.242 +  let ?R = "zimage (Abs_game) (zexplode r)"
   4.243 +  have L:"?L = left_options g"
   4.244 +    by (simp add: left_options_def lr Fst)
   4.245 +  have R:"?R = right_options g"
   4.246 +    by (simp add: right_options_def lr Snd)
   4.247 +  have "g = Game ?L ?R"
   4.248 +    apply (simp add: Game_def Rep_game_inject[symmetric] comp_zimage_eq zimage_zexplode_eq zimplode_zexplode)
   4.249 +    apply (simp add: Repl_Rep_game_Abs_game partizan_l partizan_r)
   4.250 +    apply (subst Abs_game_inverse)
   4.251 +    apply (simp_all add: lr[symmetric] Rep_game) 
   4.252 +    done
   4.253 +  then show ?thesis
   4.254 +    by (simp add: L R)
   4.255 +qed
   4.256 +
   4.257 +lemma Opair_in_games_lfp: 
   4.258 +  assumes l: "explode l \<subseteq> games_lfp"
   4.259 +  and r: "explode r \<subseteq> games_lfp"
   4.260 +  shows "Opair l r \<in> games_lfp"
   4.261 +proof -
   4.262 +  note f = unique_games[of games_lfp, simplified]
   4.263 +  show ?thesis
   4.264 +    apply (subst f)
   4.265 +    apply (simp add: fixgames_def)
   4.266 +    apply (rule exI[where x=l])
   4.267 +    apply (rule exI[where x=r])
   4.268 +    apply (auto simp add: l r)
   4.269 +    done
   4.270 +qed
   4.271 +
   4.272 +lemma left_options[simp]: "left_options (Game l r) = l"
   4.273 +  apply (simp add: left_options_def Game_def)
   4.274 +  apply (subst Abs_game_inverse)
   4.275 +  apply (simp add: game_def)
   4.276 +  apply (rule Opair_in_games_lfp)
   4.277 +  apply (auto simp add: explode_Elem Elem_zimplode zimage_iff Rep_game[simplified game_def])
   4.278 +  apply (simp add: Fst zexplode_zimplode comp_zimage_eq)
   4.279 +  apply (simp add: zet_ext_eq zimage_iff Rep_game_inverse)
   4.280 +  done
   4.281 +
   4.282 +lemma right_options[simp]: "right_options (Game l r) = r"
   4.283 +  apply (simp add: right_options_def Game_def)
   4.284 +  apply (subst Abs_game_inverse)
   4.285 +  apply (simp add: game_def)
   4.286 +  apply (rule Opair_in_games_lfp)
   4.287 +  apply (auto simp add: explode_Elem Elem_zimplode zimage_iff Rep_game[simplified game_def])
   4.288 +  apply (simp add: Snd zexplode_zimplode comp_zimage_eq)
   4.289 +  apply (simp add: zet_ext_eq zimage_iff Rep_game_inverse)
   4.290 +  done  
   4.291 +
   4.292 +lemma Game_ext: "(Game l1 r1 = Game l2 r2) = ((l1 = l2) \<and> (r1 = r2))"
   4.293 +  apply auto
   4.294 +  apply (subst left_options[where l=l1 and r=r1,symmetric])
   4.295 +  apply (subst left_options[where l=l2 and r=r2,symmetric])
   4.296 +  apply simp
   4.297 +  apply (subst right_options[where l=l1 and r=r1,symmetric])
   4.298 +  apply (subst right_options[where l=l2 and r=r2,symmetric])
   4.299 +  apply simp
   4.300 +  done
   4.301 +
   4.302 +constdefs
   4.303 +  option_of :: "(game * game) set"
   4.304 +  "option_of \<equiv> image (\<lambda> (option, g). (Abs_game option, Abs_game g)) is_option_of"
   4.305 +
   4.306 +lemma option_to_is_option_of: "((option, g) \<in> option_of) = ((Rep_game option, Rep_game g) \<in> is_option_of)"
   4.307 +  apply (auto simp add: option_of_def)
   4.308 +  apply (subst Abs_game_inverse)
   4.309 +  apply (simp add: is_option_of_imp_games game_def)
   4.310 +  apply (subst Abs_game_inverse)
   4.311 +  apply (simp add: is_option_of_imp_games game_def)
   4.312 +  apply simp
   4.313 +  apply (auto simp add: Bex_def image_def)  
   4.314 +  apply (rule exI[where x="Rep_game option"])
   4.315 +  apply (rule exI[where x="Rep_game g"])
   4.316 +  apply (simp add: Rep_game_inverse)
   4.317 +  done
   4.318 +  
   4.319 +lemma wf_is_option_of: "wf is_option_of"
   4.320 +  apply (rule wfzf_implies_wf)
   4.321 +  apply (simp add: wfzf_is_option_of)
   4.322 +  done
   4.323 +
   4.324 +lemma wf_option_of[recdef_wf, simp, intro]: "wf option_of"
   4.325 +proof -
   4.326 +  have option_of: "option_of = inv_image is_option_of Rep_game"
   4.327 +    apply (rule set_ext)
   4.328 +    apply (case_tac "x")
   4.329 +    by (simp add: inv_image_def option_to_is_option_of) 
   4.330 +  show ?thesis
   4.331 +    apply (simp add: option_of)
   4.332 +    apply (auto intro: wf_inv_image wf_is_option_of)
   4.333 +    done
   4.334 +qed
   4.335 +  
   4.336 +lemma right_option_is_option[simp, intro]: "zin x (right_options g) \<Longrightarrow> zin x (options g)"
   4.337 +  by (simp add: options_def zunion)
   4.338 +
   4.339 +lemma left_option_is_option[simp, intro]: "zin x (left_options g) \<Longrightarrow> zin x (options g)"
   4.340 +  by (simp add: options_def zunion)
   4.341 +
   4.342 +lemma zin_options[simp, intro]: "zin x (options g) \<Longrightarrow> (x, g) \<in> option_of"
   4.343 +  apply (simp add: options_def zunion left_options_def right_options_def option_of_def 
   4.344 +    image_def is_option_of_def zimage_iff zin_zexplode_eq) 
   4.345 +  apply (cases g)
   4.346 +  apply (cases x)
   4.347 +  apply (auto simp add: Abs_game_inverse games_lfp_eq_gfp[symmetric] game_def 
   4.348 +    right_option_def[symmetric] left_option_def[symmetric])
   4.349 +  done
   4.350 +
   4.351 +consts
   4.352 +  neg_game :: "game \<Rightarrow> game"
   4.353 +
   4.354 +recdef neg_game "option_of"
   4.355 +  "neg_game g = Game (zimage neg_game (right_options g)) (zimage neg_game (left_options g))"
   4.356 +
   4.357 +declare neg_game.simps[simp del]
   4.358 +
   4.359 +lemma "neg_game (neg_game g) = g"
   4.360 +  apply (induct g rule: neg_game.induct)
   4.361 +  apply (subst neg_game.simps)+
   4.362 +  apply (simp add: right_options left_options comp_zimage_eq)
   4.363 +  apply (subgoal_tac "zimage (neg_game o neg_game) (left_options g) = left_options g")
   4.364 +  apply (subgoal_tac "zimage (neg_game o neg_game) (right_options g) = right_options g")
   4.365 +  apply (auto simp add: game_split[symmetric])
   4.366 +  apply (auto simp add: zet_ext_eq zimage_iff)
   4.367 +  done
   4.368 +
   4.369 +consts
   4.370 +  ge_game :: "(game * game) \<Rightarrow> bool" 
   4.371 +
   4.372 +recdef ge_game "(gprod_2_1 option_of)"
   4.373 +  "ge_game (G, H) = (\<forall> x. if zin x (right_options G) then (
   4.374 +                          if zin x (left_options H) then \<not> (ge_game (H, x) \<or> (ge_game (x, G))) 
   4.375 +                                                    else \<not> (ge_game (H, x)))
   4.376 +                          else (if zin x (left_options H) then \<not> (ge_game (x, G)) else True))"
   4.377 +(hints simp: gprod_2_1_def)
   4.378 +
   4.379 +declare ge_game.simps [simp del]
   4.380 +
   4.381 +lemma ge_game_def: "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)))"
   4.382 +  apply (subst ge_game.simps[where G=G and H=H])
   4.383 +  apply (auto)
   4.384 +  done
   4.385 +
   4.386 +lemma ge_game_leftright_refl[rule_format]: 
   4.387 +  "\<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)"
   4.388 +proof (induct x rule: wf_induct[OF wf_option_of]) 
   4.389 +  case (1 "g")
   4.390 +  { 
   4.391 +    fix y
   4.392 +    assume y: "zin y (right_options g)"
   4.393 +    have "\<not> ge_game (g, y)"
   4.394 +    proof -
   4.395 +      have "(y, g) \<in> option_of" by (auto intro: y)
   4.396 +      with 1 have "ge_game (y, y)" by auto
   4.397 +      with y show ?thesis by (subst ge_game_def, auto)
   4.398 +    qed
   4.399 +  }
   4.400 +  note right = this
   4.401 +  { 
   4.402 +    fix y
   4.403 +    assume y: "zin y (left_options g)"
   4.404 +    have "\<not> ge_game (y, g)"
   4.405 +    proof -
   4.406 +      have "(y, g) \<in> option_of" by (auto intro: y)
   4.407 +      with 1 have "ge_game (y, y)" by auto
   4.408 +      with y show ?thesis by (subst ge_game_def, auto)
   4.409 +    qed
   4.410 +  } 
   4.411 +  note left = this
   4.412 +  from left right show ?case
   4.413 +    by (auto, subst ge_game_def, auto)
   4.414 +qed
   4.415 +
   4.416 +lemma ge_game_refl: "ge_game (x,x)" by (simp add: ge_game_leftright_refl)
   4.417 +
   4.418 +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)"
   4.419 +proof (induct x rule: wf_induct[OF wf_option_of]) 
   4.420 +  case (1 "g")  
   4.421 +  show ?case
   4.422 +  proof (auto)
   4.423 +    {case (goal1 y) 
   4.424 +      from goal1 have "(y, g) \<in> option_of" by (auto)
   4.425 +      with 1 have "ge_game (y, y)" by auto
   4.426 +      with goal1 have "\<not> ge_game (g, y)" 
   4.427 +	by (subst ge_game_def, auto)
   4.428 +      with goal1 show ?case by auto}
   4.429 +    note right = this
   4.430 +    {case (goal2 y)
   4.431 +      from goal2 have "(y, g) \<in> option_of" by (auto)
   4.432 +      with 1 have "ge_game (y, y)" by auto
   4.433 +      with goal2 have "\<not> ge_game (y, g)" 
   4.434 +	by (subst ge_game_def, auto)
   4.435 +      with goal2 show ?case by auto}
   4.436 +    note left = this
   4.437 +    {case goal3
   4.438 +      from left right show ?case
   4.439 +	by (subst ge_game_def, auto)
   4.440 +    }
   4.441 +  qed
   4.442 +qed
   4.443 +	
   4.444 +constdefs
   4.445 +  eq_game :: "game \<Rightarrow> game \<Rightarrow> bool"
   4.446 +  "eq_game G H \<equiv> ge_game (G, H) \<and> ge_game (H, G)" 
   4.447 +
   4.448 +lemma eq_game_sym: "(eq_game G H) = (eq_game H G)"
   4.449 +  by (auto simp add: eq_game_def)
   4.450 +
   4.451 +lemma eq_game_refl: "eq_game G G"
   4.452 +  by (simp add: ge_game_refl eq_game_def)
   4.453 +
   4.454 +lemma induct_game: "(\<And>x. \<forall>y. (y, x) \<in> lprod option_of \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a"
   4.455 +  by (erule wf_induct[OF wf_lprod[OF wf_option_of]])
   4.456 +
   4.457 +lemma ge_game_trans:
   4.458 +  assumes "ge_game (x, y)" "ge_game (y, z)" 
   4.459 +  shows "ge_game (x, z)"
   4.460 +proof -  
   4.461 +  { 
   4.462 +    fix a
   4.463 +    have "\<forall> x y z. a = [x,y,z] \<longrightarrow> ge_game (x,y) \<longrightarrow> ge_game (y,z) \<longrightarrow> ge_game (x, z)"
   4.464 +    proof (induct a rule: induct_game)
   4.465 +      case (1 a)
   4.466 +      show ?case
   4.467 +      proof (rule allI | rule impI)+
   4.468 +	case (goal1 x y z)
   4.469 +	show ?case
   4.470 +	proof -
   4.471 +	  { fix xr
   4.472 +            assume xr:"zin xr (right_options x)"
   4.473 +	    assume "ge_game (z, xr)"
   4.474 +	    have "ge_game (y, xr)"
   4.475 +	      apply (rule 1[rule_format, where y="[y,z,xr]"])
   4.476 +	      apply (auto intro: xr lprod_3_1 simp add: prems)
   4.477 +	      done
   4.478 +	    moreover from xr have "\<not> ge_game (y, xr)"
   4.479 +	      by (simp add: goal1(2)[simplified ge_game_def[of x y], rule_format, of xr, simplified xr])
   4.480 +	    ultimately have "False" by auto      
   4.481 +	  }
   4.482 +	  note xr = this
   4.483 +	  { fix zl
   4.484 +	    assume zl:"zin zl (left_options z)"
   4.485 +	    assume "ge_game (zl, x)"
   4.486 +	    have "ge_game (zl, y)"
   4.487 +	      apply (rule 1[rule_format, where y="[zl,x,y]"])
   4.488 +	      apply (auto intro: zl lprod_3_2 simp add: prems)
   4.489 +	      done
   4.490 +	    moreover from zl have "\<not> ge_game (zl, y)"
   4.491 +	      by (simp add: goal1(3)[simplified ge_game_def[of y z], rule_format, of zl, simplified zl])
   4.492 +	    ultimately have "False" by auto
   4.493 +	  }
   4.494 +	  note zl = this
   4.495 +	  show ?thesis
   4.496 +	    by (auto simp add: ge_game_def[of x z] intro: xr zl)
   4.497 +	qed
   4.498 +      qed
   4.499 +    qed
   4.500 +  } 
   4.501 +  note trans = this[of "[x, y, z]", simplified, rule_format]    
   4.502 +  with prems show ?thesis by blast
   4.503 +qed
   4.504 +
   4.505 +lemma eq_game_trans: "eq_game a b \<Longrightarrow> eq_game b c \<Longrightarrow> eq_game a c"
   4.506 +  by (auto simp add: eq_game_def intro: ge_game_trans)
   4.507 +
   4.508 +constdefs
   4.509 +  zero_game :: game
   4.510 +  "zero_game \<equiv> Game zempty zempty"
   4.511 +
   4.512 +consts 
   4.513 +  plus_game :: "game * game \<Rightarrow> game"
   4.514 +
   4.515 +recdef plus_game "gprod_2_2 option_of"
   4.516 +  "plus_game (G, H) = Game (zunion (zimage (\<lambda> g. plus_game (g, H)) (left_options G))
   4.517 +                                   (zimage (\<lambda> h. plus_game (G, h)) (left_options H)))
   4.518 +                           (zunion (zimage (\<lambda> g. plus_game (g, H)) (right_options G))
   4.519 +                                   (zimage (\<lambda> h. plus_game (G, h)) (right_options H)))"
   4.520 +(hints simp add: gprod_2_2_def)
   4.521 +
   4.522 +declare plus_game.simps[simp del]
   4.523 +
   4.524 +lemma plus_game_comm: "plus_game (G, H) = plus_game (H, G)"
   4.525 +proof (induct G H rule: plus_game.induct)
   4.526 +  case (1 G H)
   4.527 +  show ?case
   4.528 +    by (auto simp add: 
   4.529 +      plus_game.simps[where G=G and H=H] 
   4.530 +      plus_game.simps[where G=H and H=G]
   4.531 +      Game_ext zet_ext_eq zunion zimage_iff prems)
   4.532 +qed
   4.533 +
   4.534 +lemma game_ext_eq: "(G = H) = (left_options G = left_options H \<and> right_options G = right_options H)"
   4.535 +proof -
   4.536 +  have "(G = H) = (Game (left_options G) (right_options G) = Game (left_options H) (right_options H))"
   4.537 +    by (simp add: game_split[symmetric])
   4.538 +  then show ?thesis by auto
   4.539 +qed
   4.540 +
   4.541 +lemma left_zero_game[simp]: "left_options (zero_game) = zempty"
   4.542 +  by (simp add: zero_game_def)
   4.543 +
   4.544 +lemma right_zero_game[simp]: "right_options (zero_game) = zempty"
   4.545 +  by (simp add: zero_game_def)
   4.546 +
   4.547 +lemma plus_game_zero_right[simp]: "plus_game (G, zero_game) = G"
   4.548 +proof -
   4.549 +  { 
   4.550 +    fix G H
   4.551 +    have "H = zero_game \<longrightarrow> plus_game (G, H) = G "
   4.552 +    proof (induct G H rule: plus_game.induct, rule impI)
   4.553 +      case (goal1 G H)
   4.554 +      note induct_hyp = prems[simplified goal1, simplified] and prems
   4.555 +      show ?case
   4.556 +	apply (simp only: plus_game.simps[where G=G and H=H])
   4.557 +	apply (simp add: game_ext_eq prems)
   4.558 +	apply (auto simp add: 
   4.559 +	  zimage_cong[where f = "\<lambda> g. plus_game (g, zero_game)" and g = "id"] 
   4.560 +	  induct_hyp)
   4.561 +	done
   4.562 +    qed
   4.563 +  }
   4.564 +  then show ?thesis by auto
   4.565 +qed
   4.566 +
   4.567 +lemma plus_game_zero_left: "plus_game (zero_game, G) = G"
   4.568 +  by (simp add: plus_game_comm)
   4.569 +
   4.570 +lemma left_imp_options[simp]: "zin opt (left_options g) \<Longrightarrow> zin opt (options g)"
   4.571 +  by (simp add: options_def zunion)
   4.572 +
   4.573 +lemma right_imp_options[simp]: "zin opt (right_options g) \<Longrightarrow> zin opt (options g)"
   4.574 +  by (simp add: options_def zunion)
   4.575 +
   4.576 +lemma left_options_plus: 
   4.577 +  "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))" 
   4.578 +  by (subst plus_game.simps, simp)
   4.579 +
   4.580 +lemma right_options_plus:
   4.581 +  "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))"
   4.582 +  by (subst plus_game.simps, simp)
   4.583 +
   4.584 +lemma left_options_neg: "left_options (neg_game u) = zimage neg_game (right_options u)"	 
   4.585 +  by (subst neg_game.simps, simp)
   4.586 +
   4.587 +lemma right_options_neg: "right_options (neg_game u) = zimage neg_game (left_options u)"
   4.588 +  by (subst neg_game.simps, simp)
   4.589 +  
   4.590 +lemma plus_game_assoc: "plus_game (plus_game (F, G), H) = plus_game (F, plus_game (G, H))"
   4.591 +proof -
   4.592 +  { 
   4.593 +    fix a
   4.594 +    have "\<forall> F G H. a = [F, G, H] \<longrightarrow> plus_game (plus_game (F, G), H) = plus_game (F, plus_game (G, H))"
   4.595 +    proof (induct a rule: induct_game, (rule impI | rule allI)+)
   4.596 +      case (goal1 x F G H)
   4.597 +      let ?L = "plus_game (plus_game (F, G), H)"
   4.598 +      let ?R = "plus_game (F, plus_game (G, H))"
   4.599 +      note options_plus = left_options_plus right_options_plus
   4.600 +      {
   4.601 +	fix opt
   4.602 +	note hyp = goal1(1)[simplified goal1(2), rule_format] 
   4.603 +	have F: "zin opt (options F)  \<Longrightarrow> plus_game (plus_game (opt, G), H) = plus_game (opt, plus_game (G, H))"
   4.604 +	  by (blast intro: hyp lprod_3_3)
   4.605 +	have G: "zin opt (options G) \<Longrightarrow> plus_game (plus_game (F, opt), H) = plus_game (F, plus_game (opt, H))"
   4.606 +	  by (blast intro: hyp lprod_3_4)
   4.607 +	have H: "zin opt (options H) \<Longrightarrow> plus_game (plus_game (F, G), opt) = plus_game (F, plus_game (G, opt))" 
   4.608 +	  by (blast intro: hyp lprod_3_5)
   4.609 +	note F and G and H
   4.610 +      }
   4.611 +      note induct_hyp = this
   4.612 +      have "left_options ?L = left_options ?R \<and> right_options ?L = right_options ?R"
   4.613 +	by (auto simp add: 
   4.614 +	  plus_game.simps[where G="plus_game (F,G)" and H=H]
   4.615 +	  plus_game.simps[where G="F" and H="plus_game (G,H)"] 
   4.616 +	  zet_ext_eq zunion zimage_iff options_plus
   4.617 +	  induct_hyp left_imp_options right_imp_options)
   4.618 +      then show ?case
   4.619 +	by (simp add: game_ext_eq)
   4.620 +    qed
   4.621 +  }
   4.622 +  then show ?thesis by auto
   4.623 +qed
   4.624 +
   4.625 +lemma neg_plus_game: "neg_game (plus_game (G, H)) = plus_game(neg_game G, neg_game H)"
   4.626 +proof (induct G H rule: plus_game.induct)
   4.627 +  case (1 G H)
   4.628 +  note opt_ops = 
   4.629 +    left_options_plus right_options_plus 
   4.630 +    left_options_neg right_options_neg  
   4.631 +  show ?case
   4.632 +    by (auto simp add: opt_ops
   4.633 +      neg_game.simps[of "plus_game (G,H)"]
   4.634 +      plus_game.simps[of "neg_game G" "neg_game H"]
   4.635 +      Game_ext zet_ext_eq zunion zimage_iff prems)
   4.636 +qed
   4.637 +
   4.638 +lemma eq_game_plus_inverse: "eq_game (plus_game (x, neg_game x)) zero_game"
   4.639 +proof (induct x rule: wf_induct[OF wf_option_of])
   4.640 +  case (goal1 x)
   4.641 +  { fix y
   4.642 +    assume "zin y (options x)"
   4.643 +    then have "eq_game (plus_game (y, neg_game y)) zero_game"
   4.644 +      by (auto simp add: prems)
   4.645 +  }
   4.646 +  note ihyp = this
   4.647 +  {
   4.648 +    fix y
   4.649 +    assume y: "zin y (right_options x)"
   4.650 +    have "\<not> (ge_game (zero_game, plus_game (y, neg_game x)))"
   4.651 +      apply (subst ge_game.simps, simp)
   4.652 +      apply (rule exI[where x="plus_game (y, neg_game y)"])
   4.653 +      apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
   4.654 +      apply (auto simp add: left_options_plus left_options_neg zunion zimage_iff intro: prems)
   4.655 +      done
   4.656 +  }
   4.657 +  note case1 = this
   4.658 +  {
   4.659 +    fix y
   4.660 +    assume y: "zin y (left_options x)"
   4.661 +    have "\<not> (ge_game (zero_game, plus_game (x, neg_game y)))"
   4.662 +      apply (subst ge_game.simps, simp)
   4.663 +      apply (rule exI[where x="plus_game (y, neg_game y)"])
   4.664 +      apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
   4.665 +      apply (auto simp add: left_options_plus zunion zimage_iff intro: prems)
   4.666 +      done
   4.667 +  }
   4.668 +  note case2 = this
   4.669 +  {
   4.670 +    fix y
   4.671 +    assume y: "zin y (left_options x)"
   4.672 +    have "\<not> (ge_game (plus_game (y, neg_game x), zero_game))"
   4.673 +      apply (subst ge_game.simps, simp)
   4.674 +      apply (rule exI[where x="plus_game (y, neg_game y)"])
   4.675 +      apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
   4.676 +      apply (auto simp add: right_options_plus right_options_neg zunion zimage_iff intro: prems)
   4.677 +      done
   4.678 +  }
   4.679 +  note case3 = this
   4.680 +  {
   4.681 +    fix y
   4.682 +    assume y: "zin y (right_options x)"
   4.683 +    have "\<not> (ge_game (plus_game (x, neg_game y), zero_game))"
   4.684 +      apply (subst ge_game.simps, simp)
   4.685 +      apply (rule exI[where x="plus_game (y, neg_game y)"])
   4.686 +      apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
   4.687 +      apply (auto simp add: right_options_plus zunion zimage_iff intro: prems)
   4.688 +      done
   4.689 +  }
   4.690 +  note case4 = this
   4.691 +  show ?case
   4.692 +    apply (simp add: eq_game_def)
   4.693 +    apply (simp add: ge_game.simps[of "plus_game (x, neg_game x)" "zero_game"])
   4.694 +    apply (simp add: ge_game.simps[of "zero_game" "plus_game (x, neg_game x)"])
   4.695 +    apply (simp add: right_options_plus left_options_plus right_options_neg left_options_neg zunion zimage_iff)
   4.696 +    apply (auto simp add: case1 case2 case3 case4)
   4.697 +    done
   4.698 +qed
   4.699 +
   4.700 +lemma ge_plus_game_left: "ge_game (y,z) = ge_game(plus_game (x, y), plus_game (x, z))"
   4.701 +proof -
   4.702 +  { fix a
   4.703 +    have "\<forall> x y z. a = [x,y,z] \<longrightarrow> ge_game (y,z) = ge_game(plus_game (x, y), plus_game (x, z))"
   4.704 +    proof (induct a rule: induct_game, (rule impI | rule allI)+)
   4.705 +      case (goal1 a x y z)
   4.706 +      note induct_hyp = goal1(1)[rule_format, simplified goal1(2)]
   4.707 +      { 
   4.708 +	assume hyp: "ge_game(plus_game (x, y), plus_game (x, z))"
   4.709 +	have "ge_game (y, z)"
   4.710 +	proof -
   4.711 +	  { fix yr
   4.712 +	    assume yr: "zin yr (right_options y)"
   4.713 +	    from hyp have "\<not> (ge_game (plus_game (x, z), plus_game (x, yr)))"
   4.714 +	      by (auto simp add: ge_game_def[of "plus_game (x,y)" "plus_game(x,z)"]
   4.715 +		right_options_plus zunion zimage_iff intro: yr)
   4.716 +	    then have "\<not> (ge_game (z, yr))"
   4.717 +	      apply (subst induct_hyp[where y="[x, z, yr]", of "x" "z" "yr"])
   4.718 +	      apply (simp_all add: yr lprod_3_6)
   4.719 +	      done
   4.720 +	  }
   4.721 +	  note yr = this
   4.722 +	  { fix zl
   4.723 +	    assume zl: "zin zl (left_options z)"
   4.724 +	    from hyp have "\<not> (ge_game (plus_game (x, zl), plus_game (x, y)))"
   4.725 +	      by (auto simp add: ge_game_def[of "plus_game (x,y)" "plus_game(x,z)"]
   4.726 +		left_options_plus zunion zimage_iff intro: zl)
   4.727 +	    then have "\<not> (ge_game (zl, y))"
   4.728 +	      apply (subst goal1(1)[rule_format, where y="[x, zl, y]", of "x" "zl" "y"])
   4.729 +	      apply (simp_all add: goal1(2) zl lprod_3_7)
   4.730 +	      done
   4.731 +	  }	
   4.732 +	  note zl = this
   4.733 +	  show "ge_game (y, z)"
   4.734 +	    apply (subst ge_game_def)
   4.735 +	    apply (auto simp add: yr zl)
   4.736 +	    done
   4.737 +	qed      
   4.738 +      }
   4.739 +      note right_imp_left = this
   4.740 +      {
   4.741 +	assume yz: "ge_game (y, z)"
   4.742 +	{
   4.743 +	  fix x'
   4.744 +	  assume x': "zin x' (right_options x)"
   4.745 +	  assume hyp: "ge_game (plus_game (x, z), plus_game (x', y))"
   4.746 +	  then have n: "\<not> (ge_game (plus_game (x', y), plus_game (x', z)))"
   4.747 +	    by (auto simp add: ge_game_def[of "plus_game (x,z)" "plus_game (x', y)"] 
   4.748 +	      right_options_plus zunion zimage_iff intro: x')
   4.749 +	  have t: "ge_game (plus_game (x', y), plus_game (x', z))"
   4.750 +	    apply (subst induct_hyp[symmetric])
   4.751 +	    apply (auto intro: lprod_3_3 x' yz)
   4.752 +	    done
   4.753 +	  from n t have "False" by blast
   4.754 +	}    
   4.755 +	note case1 = this
   4.756 +	{
   4.757 +	  fix x'
   4.758 +	  assume x': "zin x' (left_options x)"
   4.759 +	  assume hyp: "ge_game (plus_game (x', z), plus_game (x, y))"
   4.760 +	  then have n: "\<not> (ge_game (plus_game (x', y), plus_game (x', z)))"
   4.761 +	    by (auto simp add: ge_game_def[of "plus_game (x',z)" "plus_game (x, y)"] 
   4.762 +	      left_options_plus zunion zimage_iff intro: x')
   4.763 +	  have t: "ge_game (plus_game (x', y), plus_game (x', z))"
   4.764 +	    apply (subst induct_hyp[symmetric])
   4.765 +	    apply (auto intro: lprod_3_3 x' yz)
   4.766 +	    done
   4.767 +	  from n t have "False" by blast
   4.768 +	}
   4.769 +	note case3 = this
   4.770 +	{
   4.771 +	  fix y'
   4.772 +	  assume y': "zin y' (right_options y)"
   4.773 +	  assume hyp: "ge_game (plus_game(x, z), plus_game (x, y'))"
   4.774 +	  then have "ge_game(z, y')"
   4.775 +	    apply (subst induct_hyp[of "[x, z, y']" "x" "z" "y'"])
   4.776 +	    apply (auto simp add: hyp lprod_3_6 y')
   4.777 +	    done
   4.778 +	  with yz have "ge_game (y, y')"
   4.779 +	    by (blast intro: ge_game_trans)      
   4.780 +	  with y' have "False" by (auto simp add: ge_game_leftright_refl)
   4.781 +	}
   4.782 +	note case2 = this
   4.783 +	{
   4.784 +	  fix z'
   4.785 +	  assume z': "zin z' (left_options z)"
   4.786 +	  assume hyp: "ge_game (plus_game(x, z'), plus_game (x, y))"
   4.787 +	  then have "ge_game(z', y)"
   4.788 +	    apply (subst induct_hyp[of "[x, z', y]" "x" "z'" "y"])
   4.789 +	    apply (auto simp add: hyp lprod_3_7 z')
   4.790 +	    done    
   4.791 +	  with yz have "ge_game (z', z)"
   4.792 +	    by (blast intro: ge_game_trans)      
   4.793 +	  with z' have "False" by (auto simp add: ge_game_leftright_refl)
   4.794 +	}
   4.795 +	note case4 = this   
   4.796 +	have "ge_game(plus_game (x, y), plus_game (x, z))"
   4.797 +	  apply (subst ge_game_def)
   4.798 +	  apply (auto simp add: right_options_plus left_options_plus zunion zimage_iff)
   4.799 +	  apply (auto intro: case1 case2 case3 case4)
   4.800 +	  done
   4.801 +      }
   4.802 +      note left_imp_right = this
   4.803 +      show ?case by (auto intro: right_imp_left left_imp_right)
   4.804 +    qed
   4.805 +  }
   4.806 +  note a = this[of "[x, y, z]"]
   4.807 +  then show ?thesis by blast
   4.808 +qed
   4.809 +
   4.810 +lemma ge_plus_game_right: "ge_game (y,z) = ge_game(plus_game (y, x), plus_game (z, x))"
   4.811 +  by (simp add: ge_plus_game_left plus_game_comm)
   4.812 +
   4.813 +lemma ge_neg_game: "ge_game (neg_game x, neg_game y) = ge_game (y, x)"
   4.814 +proof -
   4.815 +  { fix a
   4.816 +    have "\<forall> x y. a = [x, y] \<longrightarrow> ge_game (neg_game x, neg_game y) = ge_game (y, x)"
   4.817 +    proof (induct a rule: induct_game, (rule impI | rule allI)+)
   4.818 +      case (goal1 a x y)
   4.819 +      note ihyp = goal1(1)[rule_format, simplified goal1(2)]
   4.820 +      { fix xl
   4.821 +	assume xl: "zin xl (left_options x)"
   4.822 +	have "ge_game (neg_game y, neg_game xl) = ge_game (xl, y)"
   4.823 +	  apply (subst ihyp)
   4.824 +	  apply (auto simp add: lprod_2_1 xl)
   4.825 +	  done
   4.826 +      }
   4.827 +      note xl = this
   4.828 +      { fix yr
   4.829 +	assume yr: "zin yr (right_options y)"
   4.830 +	have "ge_game (neg_game yr, neg_game x) = ge_game (x, yr)"
   4.831 +	  apply (subst ihyp)
   4.832 +	  apply (auto simp add: lprod_2_2 yr)
   4.833 +	  done
   4.834 +      }
   4.835 +      note yr = this
   4.836 +      show ?case
   4.837 +	by (auto simp add: ge_game_def[of "neg_game x" "neg_game y"] ge_game_def[of "y" "x"]
   4.838 +	  right_options_neg left_options_neg zimage_iff  xl yr)
   4.839 +    qed
   4.840 +  }
   4.841 +  note a = this[of "[x,y]"]
   4.842 +  then show ?thesis by blast
   4.843 +qed
   4.844 +
   4.845 +constdefs 
   4.846 +  eq_game_rel :: "(game * game) set"
   4.847 +  "eq_game_rel \<equiv> { (p, q) . eq_game p q }"
   4.848 +
   4.849 +typedef Pg = "UNIV//eq_game_rel"
   4.850 +  by (auto simp add: quotient_def)
   4.851 +
   4.852 +lemma equiv_eq_game[simp]: "equiv UNIV eq_game_rel"
   4.853 +  by (auto simp add: equiv_def refl_def sym_def trans_def eq_game_rel_def
   4.854 +    eq_game_sym intro: eq_game_refl eq_game_trans)
   4.855 +
   4.856 +instance Pg :: "{ord,zero,plus,minus}" ..
   4.857 +
   4.858 +defs (overloaded)
   4.859 +  Pg_zero_def: "0 \<equiv> Abs_Pg (eq_game_rel `` {zero_game})"
   4.860 +  Pg_le_def: "G \<le> H \<equiv> \<exists> g h. g \<in> Rep_Pg G \<and> h \<in> Rep_Pg H \<and> ge_game (h, g)"
   4.861 +  Pg_less_def: "G < H \<equiv> G \<le> H \<and> G \<noteq> (H::Pg)"
   4.862 +  Pg_minus_def: "- G \<equiv> contents (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
   4.863 +  Pg_plus_def: "G + H \<equiv> contents (\<Union> g \<in> Rep_Pg G. \<Union> h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game (g,h)})})"
   4.864 +  Pg_diff_def: "G - H \<equiv> G + (- (H::Pg))"
   4.865 +
   4.866 +lemma Rep_Abs_eq_Pg[simp]: "Rep_Pg (Abs_Pg (eq_game_rel `` {g})) = eq_game_rel `` {g}"
   4.867 +  apply (subst Abs_Pg_inverse)
   4.868 +  apply (auto simp add: Pg_def quotient_def)
   4.869 +  done
   4.870 +
   4.871 +lemma char_Pg_le[simp]: "(Abs_Pg (eq_game_rel `` {g}) \<le> Abs_Pg (eq_game_rel `` {h})) = (ge_game (h, g))"
   4.872 +  apply (simp add: Pg_le_def)
   4.873 +  apply (auto simp add: eq_game_rel_def eq_game_def intro: ge_game_trans ge_game_refl)
   4.874 +  done
   4.875 +
   4.876 +lemma char_Pg_eq[simp]: "(Abs_Pg (eq_game_rel `` {g}) = Abs_Pg (eq_game_rel `` {h})) = (eq_game g h)"
   4.877 +  apply (simp add: Rep_Pg_inject [symmetric])
   4.878 +  apply (subst eq_equiv_class_iff[of UNIV])
   4.879 +  apply (simp_all)
   4.880 +  apply (simp add: eq_game_rel_def)
   4.881 +  done
   4.882 +
   4.883 +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)})"
   4.884 +proof -
   4.885 +  have "(\<lambda> g h. {Abs_Pg (eq_game_rel `` {plus_game (g, h)})}) respects2 eq_game_rel" 
   4.886 +    apply (simp add: congruent2_def)
   4.887 +    apply (auto simp add: eq_game_rel_def eq_game_def)
   4.888 +    apply (rule_tac y="plus_game (y1, z2)" in ge_game_trans)
   4.889 +    apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+
   4.890 +    apply (rule_tac y="plus_game (z1, y2)" in ge_game_trans)
   4.891 +    apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+
   4.892 +    done
   4.893 +  then show ?thesis
   4.894 +    by (simp add: Pg_plus_def UN_equiv_class2[OF equiv_eq_game equiv_eq_game]) 
   4.895 +qed
   4.896 +    
   4.897 +lemma char_Pg_minus[simp]: "- Abs_Pg (eq_game_rel `` {g}) = Abs_Pg (eq_game_rel `` {neg_game g})"
   4.898 +proof -
   4.899 +  have "(\<lambda> g. {Abs_Pg (eq_game_rel `` {neg_game g})}) respects eq_game_rel"
   4.900 +    apply (simp add: congruent_def)
   4.901 +    apply (auto simp add: eq_game_rel_def eq_game_def ge_neg_game)
   4.902 +    done    
   4.903 +  then show ?thesis
   4.904 +    by (simp add: Pg_minus_def UN_equiv_class[OF equiv_eq_game])
   4.905 +qed
   4.906 +
   4.907 +lemma eq_Abs_Pg[rule_format, cases type: Pg]: "(\<forall> g. z = Abs_Pg (eq_game_rel `` {g}) \<longrightarrow> P) \<longrightarrow> P"
   4.908 +  apply (cases z, simp)
   4.909 +  apply (simp add: Rep_Pg_inject[symmetric])
   4.910 +  apply (subst Abs_Pg_inverse, simp)
   4.911 +  apply (auto simp add: Pg_def quotient_def)
   4.912 +  done
   4.913 +
   4.914 +instance Pg :: pordered_ab_group_add 
   4.915 +proof
   4.916 +  fix a b c :: Pg
   4.917 +  show "(a < b) = (a \<le> b \<and> a \<noteq> b)" by (simp add: Pg_less_def)
   4.918 +  show "a - b = a + (- b)" by (simp add: Pg_diff_def)
   4.919 +  {
   4.920 +    assume ab: "a \<le> b"
   4.921 +    assume ba: "b \<le> a"
   4.922 +    from ab ba show "a = b"
   4.923 +      apply (cases a, cases b)
   4.924 +      apply (simp add: eq_game_def)
   4.925 +      done
   4.926 +  }
   4.927 +  show "a + b = b + a"
   4.928 +    apply (cases a, cases b)
   4.929 +    apply (simp add: eq_game_def plus_game_comm)
   4.930 +    done
   4.931 +  show "a + b + c = a + (b + c)"
   4.932 +    apply (cases a, cases b, cases c)
   4.933 +    apply (simp add: eq_game_def plus_game_assoc)
   4.934 +    done
   4.935 +  show "0 + a = a"
   4.936 +    apply (cases a)
   4.937 +    apply (simp add: Pg_zero_def plus_game_zero_left)
   4.938 +    done
   4.939 +  show "- a + a = 0"
   4.940 +    apply (cases a)
   4.941 +    apply (simp add: Pg_zero_def eq_game_plus_inverse plus_game_comm)
   4.942 +    done
   4.943 +  show "a \<le> a"
   4.944 +    apply (cases a)
   4.945 +    apply (simp add: ge_game_refl)
   4.946 +    done
   4.947 +  {
   4.948 +    assume ab: "a \<le> b"
   4.949 +    assume bc: "b \<le> c"
   4.950 +    from ab bc show "a \<le> c"
   4.951 +      apply (cases a, cases b, cases c)
   4.952 +      apply (auto intro: ge_game_trans)
   4.953 +      done
   4.954 +  }
   4.955 +  {
   4.956 +    assume ab: "a \<le> b"
   4.957 +    from ab show "c + a \<le> c + b"
   4.958 +      apply (cases a, cases b, cases c)
   4.959 +      apply (simp add: ge_plus_game_left[symmetric])
   4.960 +      done
   4.961 +  }
   4.962 +qed
   4.963 +
   4.964 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/ZF/HOLZF.thy	Tue Mar 07 16:03:31 2006 +0100
     5.3 @@ -0,0 +1,917 @@
     5.4 +(*  Title:      HOL/ZF/HOLZF.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     Steven Obua
     5.7 +
     5.8 +    Axiomatizes the ZFC universe as an HOL type.
     5.9 +    See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan
    5.10 +*)
    5.11 +
    5.12 +theory HOLZF 
    5.13 +imports Helper
    5.14 +begin
    5.15 +
    5.16 +typedecl ZF
    5.17 +
    5.18 +consts
    5.19 +  Empty :: ZF
    5.20 +  Elem :: "ZF \<Rightarrow> ZF \<Rightarrow> bool"
    5.21 +  Sum :: "ZF \<Rightarrow> ZF"
    5.22 +  Power :: "ZF \<Rightarrow> ZF"
    5.23 +  Repl :: "ZF \<Rightarrow> (ZF \<Rightarrow> ZF) \<Rightarrow> ZF"
    5.24 +  Inf :: ZF
    5.25 +
    5.26 +constdefs
    5.27 +  Upair:: "ZF \<Rightarrow> ZF \<Rightarrow> ZF"
    5.28 +  "Upair a b == Repl (Power (Power Empty)) (% x. if x = Empty then a else b)"
    5.29 +  Singleton:: "ZF \<Rightarrow> ZF"
    5.30 +  "Singleton x == Upair x x"
    5.31 +  union :: "ZF \<Rightarrow> ZF \<Rightarrow> ZF"
    5.32 +  "union A B == Sum (Upair A B)"
    5.33 +  SucNat:: "ZF \<Rightarrow> ZF"
    5.34 +  "SucNat x == union x (Singleton x)"
    5.35 +  subset :: "ZF \<Rightarrow> ZF \<Rightarrow> bool"
    5.36 +  "subset A B == ! x. Elem x A \<longrightarrow> Elem x B"
    5.37 +
    5.38 +finalconsts 
    5.39 +  Empty Elem Sum Power Repl Inf
    5.40 +
    5.41 +axioms
    5.42 +  Empty: "Not (Elem x Empty)"
    5.43 +  Ext: "(x = y) = (! z. Elem z x = Elem z y)"
    5.44 +  Sum: "Elem z (Sum x) = (? y. Elem z y & Elem y x)"
    5.45 +  Power: "Elem y (Power x) = (subset y x)"
    5.46 +  Repl: "Elem b (Repl A f) = (? a. Elem a A & b = f a)"
    5.47 +  Regularity: "A \<noteq> Empty \<longrightarrow> (? x. Elem x A & (! y. Elem y x \<longrightarrow> Not (Elem y A)))"
    5.48 +  Infinity: "Elem Empty Inf & (! x. Elem x Inf \<longrightarrow> Elem (SucNat x) Inf)"
    5.49 +
    5.50 +constdefs
    5.51 +  Sep:: "ZF \<Rightarrow> (ZF \<Rightarrow> bool) \<Rightarrow> ZF"
    5.52 +  "Sep A p == (if (!x. Elem x A \<longrightarrow> Not (p x)) then Empty else 
    5.53 +  (let z = (\<some> x. Elem x A & p x) in
    5.54 +   let f = % x. (if p x then x else z) in Repl A f))" 
    5.55 +
    5.56 +thm Power[unfolded subset_def]
    5.57 +
    5.58 +theorem Sep: "Elem b (Sep A p) = (Elem b A & p b)"
    5.59 +  apply (auto simp add: Sep_def Empty)
    5.60 +  apply (auto simp add: Let_def Repl)
    5.61 +  apply (rule someI2, auto)+
    5.62 +  done
    5.63 +
    5.64 +lemma subset_empty: "subset Empty A"
    5.65 +  by (simp add: subset_def Empty)
    5.66 +
    5.67 +theorem Upair: "Elem x (Upair a b) = (x = a | x = b)"
    5.68 +  apply (auto simp add: Upair_def Repl)
    5.69 +  apply (rule exI[where x=Empty])
    5.70 +  apply (simp add: Power subset_empty)
    5.71 +  apply (rule exI[where x="Power Empty"])
    5.72 +  apply (auto)
    5.73 +  apply (auto simp add: Ext Power subset_def Empty)
    5.74 +  apply (drule spec[where x=Empty], simp add: Empty)+
    5.75 +  done
    5.76 +
    5.77 +lemma Singleton: "Elem x (Singleton y) = (x = y)"
    5.78 +  by (simp add: Singleton_def Upair)
    5.79 +
    5.80 +constdefs 
    5.81 +  Opair:: "ZF \<Rightarrow> ZF \<Rightarrow> ZF"
    5.82 +  "Opair a b == Upair (Upair a a) (Upair a b)"
    5.83 +
    5.84 +lemma Upair_singleton: "(Upair a a = Upair c d) = (a = c & a = d)"
    5.85 +  by (auto simp add: Ext[where x="Upair a a"] Upair)
    5.86 +
    5.87 +lemma Upair_fsteq: "(Upair a b = Upair a c) = ((a = b & a = c) | (b = c))"
    5.88 +  by (auto simp add: Ext[where x="Upair a b"] Upair)
    5.89 +
    5.90 +lemma Upair_comm: "Upair a b = Upair b a"
    5.91 +  by (auto simp add: Ext Upair)
    5.92 +
    5.93 +theorem Opair: "(Opair a b = Opair c d) = (a = c & b = d)"
    5.94 +  proof -
    5.95 +    have fst: "(Opair a b = Opair c d) \<Longrightarrow> a = c"
    5.96 +      apply (simp add: Opair_def)
    5.97 +      apply (simp add: Ext[where x="Upair (Upair a a) (Upair a b)"])
    5.98 +      apply (drule spec[where x="Upair a a"])
    5.99 +      apply (auto simp add: Upair Upair_singleton)
   5.100 +      done
   5.101 +    show ?thesis
   5.102 +      apply (auto)
   5.103 +      apply (erule fst)
   5.104 +      apply (frule fst)
   5.105 +      apply (auto simp add: Opair_def Upair_fsteq)
   5.106 +      done
   5.107 +  qed
   5.108 +
   5.109 +constdefs 
   5.110 +  Replacement :: "ZF \<Rightarrow> (ZF \<Rightarrow> ZF option) \<Rightarrow> ZF"
   5.111 +  "Replacement A f == Repl (Sep A (% a. f a \<noteq> None)) (the o f)"
   5.112 +
   5.113 +theorem Replacement: "Elem y (Replacement A f) = (? x. Elem x A & f x = Some y)"
   5.114 +  by (auto simp add: Replacement_def Repl Sep) 
   5.115 +
   5.116 +constdefs
   5.117 +  Fst :: "ZF \<Rightarrow> ZF"
   5.118 +  "Fst q == SOME x. ? y. q = Opair x y"
   5.119 +  Snd :: "ZF \<Rightarrow> ZF"
   5.120 +  "Snd q == SOME y. ? x. q = Opair x y"
   5.121 +
   5.122 +theorem Fst: "Fst (Opair x y) = x"
   5.123 +  apply (simp add: Fst_def)
   5.124 +  apply (rule someI2)
   5.125 +  apply (simp_all add: Opair)
   5.126 +  done
   5.127 +
   5.128 +theorem Snd: "Snd (Opair x y) = y"
   5.129 +  apply (simp add: Snd_def)
   5.130 +  apply (rule someI2)
   5.131 +  apply (simp_all add: Opair)
   5.132 +  done
   5.133 +
   5.134 +constdefs 
   5.135 +  isOpair :: "ZF \<Rightarrow> bool"
   5.136 +  "isOpair q == ? x y. q = Opair x y"
   5.137 +
   5.138 +lemma isOpair: "isOpair (Opair x y) = True"
   5.139 +  by (auto simp add: isOpair_def)
   5.140 +
   5.141 +lemma FstSnd: "isOpair x \<Longrightarrow> Opair (Fst x) (Snd x) = x"
   5.142 +  by (auto simp add: isOpair_def Fst Snd)
   5.143 +  
   5.144 +constdefs
   5.145 +  CartProd :: "ZF \<Rightarrow> ZF \<Rightarrow> ZF"
   5.146 +  "CartProd A B == Sum(Repl A (% a. Repl B (% b. Opair a b)))"
   5.147 +
   5.148 +lemma CartProd: "Elem x (CartProd A B) = (? a b. Elem a A & Elem b B & x = (Opair a b))"
   5.149 +  apply (auto simp add: CartProd_def Sum Repl)
   5.150 +  apply (rule_tac x="Repl B (Opair a)" in exI)
   5.151 +  apply (auto simp add: Repl)
   5.152 +  done
   5.153 +
   5.154 +constdefs
   5.155 +  explode :: "ZF \<Rightarrow> ZF set"
   5.156 +  "explode z == { x. Elem x z }"
   5.157 +
   5.158 +lemma explode_Empty: "(explode x = {}) = (x = Empty)"
   5.159 +  by (auto simp add: explode_def Ext Empty)
   5.160 +
   5.161 +lemma explode_Elem: "(x \<in> explode X) = (Elem x X)"
   5.162 +  by (simp add: explode_def)
   5.163 +
   5.164 +lemma Elem_explode_in: "\<lbrakk> Elem a A; explode A \<subseteq> B\<rbrakk> \<Longrightarrow> a \<in> B"
   5.165 +  by (auto simp add: explode_def)
   5.166 +
   5.167 +lemma explode_CartProd_eq: "explode (CartProd a b) = (% (x,y). Opair x y) ` ((explode a) \<times> (explode b))"
   5.168 +  by (simp add: explode_def expand_set_eq CartProd image_def)
   5.169 +
   5.170 +lemma explode_Repl_eq: "explode (Repl A f) = image f (explode A)"
   5.171 +  by (simp add: explode_def Repl image_def)
   5.172 +
   5.173 +constdefs
   5.174 +  Domain :: "ZF \<Rightarrow> ZF"
   5.175 +  "Domain f == Replacement f (% p. if isOpair p then Some (Fst p) else None)"
   5.176 +  Range :: "ZF \<Rightarrow> ZF"
   5.177 +  "Range f == Replacement f (% p. if isOpair p then Some (Snd p) else None)"
   5.178 +
   5.179 +theorem Domain: "Elem x (Domain f) = (? y. Elem (Opair x y) f)"
   5.180 +  apply (auto simp add: Domain_def Replacement)
   5.181 +  apply (rule_tac x="Snd x" in exI)
   5.182 +  apply (simp add: FstSnd)
   5.183 +  apply (rule_tac x="Opair x y" in exI)
   5.184 +  apply (simp add: isOpair Fst)
   5.185 +  done
   5.186 +
   5.187 +theorem Range: "Elem y (Range f) = (? x. Elem (Opair x y) f)"
   5.188 +  apply (auto simp add: Range_def Replacement)
   5.189 +  apply (rule_tac x="Fst x" in exI)
   5.190 +  apply (simp add: FstSnd)
   5.191 +  apply (rule_tac x="Opair x y" in exI)
   5.192 +  apply (simp add: isOpair Snd)
   5.193 +  done
   5.194 +
   5.195 +theorem union: "Elem x (union A B) = (Elem x A | Elem x B)"
   5.196 +  by (auto simp add: union_def Sum Upair)
   5.197 +
   5.198 +constdefs
   5.199 +  Field :: "ZF \<Rightarrow> ZF"
   5.200 +  "Field A == union (Domain A) (Range A)"
   5.201 +
   5.202 +constdefs
   5.203 +  "\<acute>"         :: "ZF \<Rightarrow> ZF => ZF"    (infixl 90) --{*function application*} 
   5.204 +  app_def:  "f \<acute> x == (THE y. Elem (Opair x y) f)"
   5.205 +
   5.206 +constdefs
   5.207 +  isFun :: "ZF \<Rightarrow> bool"
   5.208 +  "isFun f == (! x y1 y2. Elem (Opair x y1) f & Elem (Opair x y2) f \<longrightarrow> y1 = y2)"
   5.209 +
   5.210 +constdefs
   5.211 +  Lambda :: "ZF \<Rightarrow> (ZF \<Rightarrow> ZF) \<Rightarrow> ZF"
   5.212 +  "Lambda A f == Repl A (% x. Opair x (f x))"
   5.213 +
   5.214 +lemma Lambda_app: "Elem x A \<Longrightarrow> (Lambda A f)\<acute>x = f x"
   5.215 +  by (simp add: app_def Lambda_def Repl Opair)
   5.216 +
   5.217 +lemma isFun_Lambda: "isFun (Lambda A f)"
   5.218 +  by (auto simp add: isFun_def Lambda_def Repl Opair)
   5.219 +
   5.220 +lemma domain_Lambda: "Domain (Lambda A f) = A"
   5.221 +  apply (auto simp add: Domain_def)
   5.222 +  apply (subst Ext)
   5.223 +  apply (auto simp add: Replacement)
   5.224 +  apply (simp add: Lambda_def Repl)
   5.225 +  apply (auto simp add: Fst)
   5.226 +  apply (simp add: Lambda_def Repl)
   5.227 +  apply (rule_tac x="Opair z (f z)" in exI)
   5.228 +  apply (auto simp add: Fst isOpair_def)
   5.229 +  done
   5.230 +
   5.231 +lemma Lambda_ext: "(Lambda s f = Lambda t g) = (s = t & (! x. Elem x s \<longrightarrow> f x = g x))"
   5.232 +proof -
   5.233 +  have "Lambda s f = Lambda t g \<Longrightarrow> s = t"
   5.234 +    apply (subst domain_Lambda[where A = s and f = f, symmetric])
   5.235 +    apply (subst domain_Lambda[where A = t and f = g, symmetric])
   5.236 +    apply auto
   5.237 +    done
   5.238 +  then show ?thesis
   5.239 +    apply auto
   5.240 +    apply (subst Lambda_app[where f=f, symmetric], simp)
   5.241 +    apply (subst Lambda_app[where f=g, symmetric], simp)
   5.242 +    apply auto
   5.243 +    apply (auto simp add: Lambda_def Repl Ext)
   5.244 +    apply (auto simp add: Ext[symmetric])
   5.245 +    done
   5.246 +qed
   5.247 +
   5.248 +constdefs 
   5.249 +  PFun :: "ZF \<Rightarrow> ZF \<Rightarrow> ZF"
   5.250 +  "PFun A B == Sep (Power (CartProd A B)) isFun"
   5.251 +  Fun :: "ZF \<Rightarrow> ZF \<Rightarrow> ZF"
   5.252 +  "Fun A B == Sep (PFun A B) (\<lambda> f. Domain f = A)"
   5.253 +
   5.254 +lemma Fun_Range: "Elem f (Fun U V) \<Longrightarrow> subset (Range f) V"
   5.255 +  apply (simp add: Fun_def Sep PFun_def Power subset_def CartProd)
   5.256 +  apply (auto simp add: Domain Range)
   5.257 +  apply (erule_tac x="Opair xa x" in allE)
   5.258 +  apply (auto simp add: Opair)
   5.259 +  done
   5.260 +
   5.261 +lemma Elem_Elem_PFun: "Elem F (PFun U V) \<Longrightarrow> Elem p F \<Longrightarrow> isOpair p & Elem (Fst p) U & Elem (Snd p) V"
   5.262 +  apply (simp add: PFun_def Sep Power subset_def, clarify)
   5.263 +  apply (erule_tac x=p in allE)
   5.264 +  apply (auto simp add: CartProd isOpair Fst Snd)
   5.265 +  done
   5.266 +
   5.267 +lemma Fun_implies_PFun[simp]: "Elem f (Fun U V) \<Longrightarrow> Elem f (PFun U V)"
   5.268 +  by (simp add: Fun_def Sep)
   5.269 +
   5.270 +lemma Elem_Elem_Fun: "Elem F (Fun U V) \<Longrightarrow> Elem p F \<Longrightarrow> isOpair p & Elem (Fst p) U & Elem (Snd p) V" 
   5.271 +  by (auto simp add: Elem_Elem_PFun dest: Fun_implies_PFun)
   5.272 +
   5.273 +lemma PFun_inj: "Elem F (PFun U V) \<Longrightarrow> Elem x F \<Longrightarrow> Elem y F \<Longrightarrow> Fst x = Fst y \<Longrightarrow> Snd x = Snd y"
   5.274 +  apply (frule Elem_Elem_PFun[where p=x], simp)
   5.275 +  apply (frule Elem_Elem_PFun[where p=y], simp)
   5.276 +  apply (subgoal_tac "isFun F")
   5.277 +  apply (simp add: isFun_def isOpair_def)  
   5.278 +  apply (auto simp add: Fst Snd, blast)
   5.279 +  apply (auto simp add: PFun_def Sep)
   5.280 +  done
   5.281 +
   5.282 +ML {* simp_depth_limit := 2 *}
   5.283 +lemma Fun_total: "\<lbrakk>Elem F (Fun U V); Elem a U\<rbrakk> \<Longrightarrow> \<exists>x. Elem (Opair a x) F"
   5.284 +  by (auto simp add: Fun_def Sep Domain)
   5.285 +ML {* simp_depth_limit := 1000 *}
   5.286 +
   5.287 +
   5.288 +lemma unique_fun_value: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> ?! y. Elem (Opair x y) f"
   5.289 +  by (auto simp add: Domain isFun_def)
   5.290 +
   5.291 +lemma fun_value_in_range: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> Elem (f\<acute>x) (Range f)"
   5.292 +  apply (auto simp add: Range)
   5.293 +  apply (drule unique_fun_value)
   5.294 +  apply simp
   5.295 +  apply (simp add: app_def)
   5.296 +  apply (rule exI[where x=x])
   5.297 +  apply (auto simp add: the_equality)
   5.298 +  done
   5.299 +
   5.300 +lemma fun_range_witness: "\<lbrakk>isFun f; Elem y (Range f)\<rbrakk> \<Longrightarrow> ? x. Elem x (Domain f) & f\<acute>x = y"
   5.301 +  apply (auto simp add: Range)
   5.302 +  apply (rule_tac x="x" in exI)
   5.303 +  apply (auto simp add: app_def the_equality isFun_def Domain)
   5.304 +  done
   5.305 +
   5.306 +lemma Elem_Fun_Lambda: "Elem F (Fun U V) \<Longrightarrow> ? f. F = Lambda U f"
   5.307 +  apply (rule exI[where x= "% x. (THE y. Elem (Opair x y) F)"])
   5.308 +  apply (simp add: Ext Lambda_def Repl Domain)
   5.309 +  apply (simp add: Ext[symmetric])
   5.310 +  apply auto
   5.311 +  apply (frule Elem_Elem_Fun)
   5.312 +  apply auto
   5.313 +  apply (rule_tac x="Fst z" in exI)
   5.314 +  apply (simp add: isOpair_def)
   5.315 +  apply (auto simp add: Fst Snd Opair)
   5.316 +  apply (rule theI2')
   5.317 +  apply auto
   5.318 +  apply (drule Fun_implies_PFun)
   5.319 +  apply (drule_tac x="Opair x ya" and y="Opair x yb" in PFun_inj)
   5.320 +  apply (auto simp add: Fst Snd)
   5.321 +  apply (drule Fun_implies_PFun)
   5.322 +  apply (drule_tac x="Opair x y" and y="Opair x ya" in PFun_inj)
   5.323 +  apply (auto simp add: Fst Snd)
   5.324 +  apply (rule theI2')
   5.325 +  apply (auto simp add: Fun_total)
   5.326 +  apply (drule Fun_implies_PFun)
   5.327 +  apply (drule_tac x="Opair a x" and y="Opair a y" in PFun_inj)
   5.328 +  apply (auto simp add: Fst Snd)
   5.329 +  done
   5.330 + 
   5.331 +lemma Elem_Lambda_Fun: "Elem (Lambda A f) (Fun U V) = (A = U & (! x. Elem x A \<longrightarrow> Elem (f x) V))"
   5.332 +proof -
   5.333 +  have "Elem (Lambda A f) (Fun U V) \<Longrightarrow> A = U"
   5.334 +    by (simp add: Fun_def Sep domain_Lambda)
   5.335 +  then show ?thesis
   5.336 +    apply auto
   5.337 +    apply (drule Fun_Range)
   5.338 +    apply (subgoal_tac "f x = ((Lambda U f) \<acute> x)")
   5.339 +    prefer 2
   5.340 +    apply (simp add: Lambda_app)
   5.341 +    apply simp
   5.342 +    apply (subgoal_tac "Elem (Lambda U f \<acute> x) (Range (Lambda U f))")
   5.343 +    apply (simp add: subset_def)
   5.344 +    apply (rule fun_value_in_range)
   5.345 +    apply (simp_all add: isFun_Lambda domain_Lambda)
   5.346 +    apply (simp add: Fun_def Sep PFun_def Power domain_Lambda isFun_Lambda)
   5.347 +    apply (auto simp add: subset_def CartProd)
   5.348 +    apply (rule_tac x="Fst x" in exI)
   5.349 +    apply (auto simp add: Lambda_def Repl Fst)
   5.350 +    done
   5.351 +qed    
   5.352 +
   5.353 +
   5.354 +constdefs
   5.355 +  is_Elem_of :: "(ZF * ZF) set"
   5.356 +  "is_Elem_of == { (a,b) | a b. Elem a b }"
   5.357 +
   5.358 +lemma cond_wf_Elem:
   5.359 +  assumes hyps:"\<forall>x. (\<forall>y. Elem y x \<longrightarrow> Elem y U \<longrightarrow> P y) \<longrightarrow> Elem x U \<longrightarrow> P x" "Elem a U"
   5.360 +  shows "P a"
   5.361 +proof -
   5.362 +  {
   5.363 +    fix P
   5.364 +    fix U
   5.365 +    fix a
   5.366 +    assume P_induct: "(\<forall>x. (\<forall>y. Elem y x \<longrightarrow> Elem y U \<longrightarrow> P y) \<longrightarrow> (Elem x U \<longrightarrow> P x))"
   5.367 +    assume a_in_U: "Elem a U"
   5.368 +    have "P a"
   5.369 +      proof -
   5.370 +	term "P"
   5.371 +	term Sep
   5.372 +	let ?Z = "Sep U (Not o P)"
   5.373 +	have "?Z = Empty \<longrightarrow> P a" by (simp add: Ext Sep Empty a_in_U)	
   5.374 +	moreover have "?Z \<noteq> Empty \<longrightarrow> False"
   5.375 +	  proof 
   5.376 +	    assume not_empty: "?Z \<noteq> Empty" 
   5.377 +	    note thereis_x = Regularity[where A="?Z", simplified not_empty, simplified]
   5.378 +	    then obtain x where x_def: "Elem x ?Z & (! y. Elem y x \<longrightarrow> Not (Elem y ?Z))" ..
   5.379 +            then have x_induct:"! y. Elem y x \<longrightarrow> Elem y U \<longrightarrow> P y" by (simp add: Sep)
   5.380 +	    have "Elem x U \<longrightarrow> P x" 
   5.381 +	      by (rule impE[OF spec[OF P_induct, where x=x], OF x_induct], assumption)
   5.382 +	    moreover have "Elem x U & Not(P x)"
   5.383 +	      apply (insert x_def)
   5.384 +	      apply (simp add: Sep)
   5.385 +	      done
   5.386 +	    ultimately show "False" by auto
   5.387 +	  qed
   5.388 +	ultimately show "P a" by auto
   5.389 +      qed
   5.390 +  }
   5.391 +  with hyps show ?thesis by blast
   5.392 +qed    
   5.393 +
   5.394 +lemma cond2_wf_Elem:
   5.395 +  assumes 
   5.396 +     special_P: "? U. ! x. Not(Elem x U) \<longrightarrow> (P x)"
   5.397 +     and P_induct: "\<forall>x. (\<forall>y. Elem y x \<longrightarrow> P y) \<longrightarrow> P x"
   5.398 +  shows
   5.399 +     "P a"
   5.400 +proof -
   5.401 +  have "? U Q. P = (\<lambda> x. (Elem x U \<longrightarrow> Q x))"
   5.402 +  proof -
   5.403 +    from special_P obtain U where U:"! x. Not(Elem x U) \<longrightarrow> (P x)" ..
   5.404 +    show ?thesis
   5.405 +      apply (rule_tac exI[where x=U])
   5.406 +      apply (rule exI[where x="P"])
   5.407 +      apply (rule ext)
   5.408 +      apply (auto simp add: U)
   5.409 +      done
   5.410 +  qed    
   5.411 +  then obtain U where "? Q. P = (\<lambda> x. (Elem x U \<longrightarrow> Q x))" ..
   5.412 +  then obtain Q where UQ: "P = (\<lambda> x. (Elem x U \<longrightarrow> Q x))" ..
   5.413 +  show ?thesis
   5.414 +    apply (auto simp add: UQ)
   5.415 +    apply (rule cond_wf_Elem)
   5.416 +    apply (rule P_induct[simplified UQ])
   5.417 +    apply simp
   5.418 +    done
   5.419 +qed
   5.420 +
   5.421 +consts
   5.422 +  nat2Nat :: "nat \<Rightarrow> ZF"
   5.423 +
   5.424 +primrec
   5.425 +nat2Nat_0[intro]:  "nat2Nat 0 = Empty"
   5.426 +nat2Nat_Suc[intro]:  "nat2Nat (Suc n) = SucNat (nat2Nat n)"
   5.427 +
   5.428 +constdefs
   5.429 +  Nat2nat :: "ZF \<Rightarrow> nat"
   5.430 +  "Nat2nat == inv nat2Nat"
   5.431 +
   5.432 +lemma Elem_nat2Nat_inf[intro]: "Elem (nat2Nat n) Inf"
   5.433 +  apply (induct n)
   5.434 +  apply (simp_all add: Infinity)
   5.435 +  done
   5.436 +
   5.437 +constdefs
   5.438 +  Nat :: ZF
   5.439 +  "Nat == Sep Inf (\<lambda> N. ? n. nat2Nat n = N)"
   5.440 +
   5.441 +lemma Elem_nat2Nat_Nat[intro]: "Elem (nat2Nat n) Nat"
   5.442 +  by (auto simp add: Nat_def Sep)
   5.443 +
   5.444 +lemma Elem_Empty_Nat: "Elem Empty Nat"
   5.445 +  by (auto simp add: Nat_def Sep Infinity)
   5.446 +
   5.447 +lemma Elem_SucNat_Nat: "Elem N Nat \<Longrightarrow> Elem (SucNat N) Nat"
   5.448 +  by (auto simp add: Nat_def Sep Infinity)
   5.449 +  
   5.450 +lemma no_infinite_Elem_down_chain:
   5.451 +  "Not (? f. isFun f & Domain f = Nat & (! N. Elem N Nat \<longrightarrow> Elem (f\<acute>(SucNat N)) (f\<acute>N)))"
   5.452 +proof -
   5.453 +  {
   5.454 +    fix f
   5.455 +    assume f:"isFun f & Domain f = Nat & (! N. Elem N Nat \<longrightarrow> Elem (f\<acute>(SucNat N)) (f\<acute>N))"
   5.456 +    let ?r = "Range f"
   5.457 +    have "?r \<noteq> Empty"
   5.458 +      apply (auto simp add: Ext Empty)
   5.459 +      apply (rule exI[where x="f\<acute>Empty"])
   5.460 +      apply (rule fun_value_in_range)
   5.461 +      apply (auto simp add: f Elem_Empty_Nat)
   5.462 +      done
   5.463 +    then have "? x. Elem x ?r & (! y. Elem y x \<longrightarrow> Not(Elem y ?r))"
   5.464 +      by (simp add: Regularity)
   5.465 +    then obtain x where x: "Elem x ?r & (! y. Elem y x \<longrightarrow> Not(Elem y ?r))" ..
   5.466 +    then have "? N. Elem N (Domain f) & f\<acute>N = x" 
   5.467 +      apply (rule_tac fun_range_witness)
   5.468 +      apply (simp_all add: f)
   5.469 +      done
   5.470 +    then have "? N. Elem N Nat & f\<acute>N = x" 
   5.471 +      by (simp add: f)
   5.472 +    then obtain N where N: "Elem N Nat & f\<acute>N = x" ..
   5.473 +    from N have N': "Elem N Nat" by auto
   5.474 +    let ?y = "f\<acute>(SucNat N)"
   5.475 +    have Elem_y_r: "Elem ?y ?r"
   5.476 +      by (simp_all add: f Elem_SucNat_Nat N fun_value_in_range)
   5.477 +    have "Elem ?y (f\<acute>N)" by (auto simp add: f N')
   5.478 +    then have "Elem ?y x" by (simp add: N)
   5.479 +    with x have "Not (Elem ?y ?r)" by auto
   5.480 +    with Elem_y_r have "False" by auto
   5.481 +  }
   5.482 +  then show ?thesis by auto
   5.483 +qed
   5.484 +
   5.485 +lemma Upair_nonEmpty: "Upair a b \<noteq> Empty"
   5.486 +  by (auto simp add: Ext Empty Upair)  
   5.487 +
   5.488 +lemma Singleton_nonEmpty: "Singleton x \<noteq> Empty"
   5.489 +  by (auto simp add: Singleton_def Upair_nonEmpty)
   5.490 +
   5.491 +lemma antisym_Elem: "Not(Elem a b & Elem b a)"
   5.492 +proof -
   5.493 +  {
   5.494 +    fix a b
   5.495 +    assume ab: "Elem a b"
   5.496 +    assume ba: "Elem b a"
   5.497 +    let ?Z = "Upair a b"
   5.498 +    have "?Z \<noteq> Empty" by (simp add: Upair_nonEmpty)
   5.499 +    then have "? x. Elem x ?Z & (! y. Elem y x \<longrightarrow> Not(Elem y ?Z))"
   5.500 +      by (simp add: Regularity)
   5.501 +    then obtain x where x:"Elem x ?Z & (! y. Elem y x \<longrightarrow> Not(Elem y ?Z))" ..
   5.502 +    then have "x = a \<or> x = b" by (simp add: Upair)
   5.503 +    moreover have "x = a \<longrightarrow> Not (Elem b ?Z)"
   5.504 +      by (auto simp add: x ba)
   5.505 +    moreover have "x = b \<longrightarrow> Not (Elem a ?Z)"
   5.506 +      by (auto simp add: x ab)
   5.507 +    ultimately have "False"
   5.508 +      by (auto simp add: Upair)
   5.509 +  }    
   5.510 +  then show ?thesis by auto
   5.511 +qed
   5.512 +
   5.513 +lemma irreflexiv_Elem: "Not(Elem a a)"
   5.514 +  by (simp add: antisym_Elem[of a a, simplified])
   5.515 +
   5.516 +lemma antisym_Elem: "Elem a b \<Longrightarrow> Not (Elem b a)"
   5.517 +  apply (insert antisym_Elem[of a b])
   5.518 +  apply auto
   5.519 +  done
   5.520 +
   5.521 +consts
   5.522 +  NatInterval :: "nat \<Rightarrow> nat \<Rightarrow> ZF"
   5.523 +
   5.524 +primrec
   5.525 +  "NatInterval n 0 = Singleton (nat2Nat n)"
   5.526 +  "NatInterval n (Suc m) = union (NatInterval n m) (Singleton (nat2Nat (n+m+1)))"
   5.527 +
   5.528 +lemma n_Elem_NatInterval[rule_format]: "! q. q <= m \<longrightarrow> Elem (nat2Nat (n+q)) (NatInterval n m)"
   5.529 +  apply (induct m)
   5.530 +  apply (auto simp add: Singleton union)
   5.531 +  apply (case_tac "q <= m")
   5.532 +  apply auto
   5.533 +  apply (subgoal_tac "q = Suc m")
   5.534 +  apply auto
   5.535 +  done
   5.536 +
   5.537 +lemma NatInterval_not_Empty: "NatInterval n m \<noteq> Empty"
   5.538 +  by (auto intro:   n_Elem_NatInterval[where q = 0, simplified] simp add: Empty Ext)
   5.539 +
   5.540 +lemma increasing_nat2Nat[rule_format]: "0 < n \<longrightarrow> Elem (nat2Nat (n - 1)) (nat2Nat n)"
   5.541 +  apply (case_tac "? m. n = Suc m")
   5.542 +  apply (auto simp add: SucNat_def union Singleton)
   5.543 +  apply (drule spec[where x="n - 1"])
   5.544 +  apply arith
   5.545 +  done
   5.546 +
   5.547 +lemma represent_NatInterval[rule_format]: "Elem x (NatInterval n m) \<longrightarrow> (? u. n \<le> u & u \<le> n+m & nat2Nat u = x)"
   5.548 +  apply (induct m)
   5.549 +  apply (auto simp add: Singleton union)
   5.550 +  apply (rule_tac x="Suc (n+m)" in exI)
   5.551 +  apply auto
   5.552 +  done
   5.553 +
   5.554 +lemma inj_nat2Nat: "inj nat2Nat"
   5.555 +proof -
   5.556 +  {
   5.557 +    fix n m :: nat
   5.558 +    assume nm: "nat2Nat n = nat2Nat (n+m)"
   5.559 +    assume mg0: "0 < m"
   5.560 +    let ?Z = "NatInterval n m"
   5.561 +    have "?Z \<noteq> Empty" by (simp add: NatInterval_not_Empty)
   5.562 +    then have "? x. (Elem x ?Z) & (! y. Elem y x \<longrightarrow> Not (Elem y ?Z))" 
   5.563 +      by (auto simp add: Regularity)
   5.564 +    then obtain x where x:"Elem x ?Z & (! y. Elem y x \<longrightarrow> Not (Elem y ?Z))" ..
   5.565 +    then have "? u. n \<le> u & u \<le> n+m & nat2Nat u = x" 
   5.566 +      by (simp add: represent_NatInterval)
   5.567 +    then obtain u where u: "n \<le> u & u \<le> n+m & nat2Nat u = x" ..
   5.568 +    have "n < u \<longrightarrow> False"
   5.569 +    proof 
   5.570 +      assume n_less_u: "n < u"
   5.571 +      let ?y = "nat2Nat (u - 1)"
   5.572 +      have "Elem ?y (nat2Nat u)"
   5.573 +	apply (rule increasing_nat2Nat)
   5.574 +	apply (insert n_less_u)
   5.575 +	apply arith
   5.576 +	done
   5.577 +      with u have "Elem ?y x" by auto
   5.578 +      with x have "Not (Elem ?y ?Z)" by auto
   5.579 +      moreover have "Elem ?y ?Z" 
   5.580 +	apply (insert n_Elem_NatInterval[where q = "u - n - 1" and n=n and m=m])
   5.581 +	apply (insert n_less_u)
   5.582 +	apply (insert u)
   5.583 +	apply auto
   5.584 +	apply arith
   5.585 +	done
   5.586 +      ultimately show False by auto
   5.587 +    qed
   5.588 +    moreover have "u = n \<longrightarrow> False"
   5.589 +    proof 
   5.590 +      assume "u = n"
   5.591 +      with u have "nat2Nat n = x" by auto
   5.592 +      then have nm_eq_x: "nat2Nat (n+m) = x" by (simp add: nm)
   5.593 +      let ?y = "nat2Nat (n+m - 1)"
   5.594 +      have "Elem ?y (nat2Nat (n+m))"
   5.595 +	apply (rule increasing_nat2Nat)
   5.596 +	apply (insert mg0)
   5.597 +	apply arith
   5.598 +	done
   5.599 +      with nm_eq_x have "Elem ?y x" by auto
   5.600 +      with x have "Not (Elem ?y ?Z)" by auto
   5.601 +      moreover have "Elem ?y ?Z" 
   5.602 +	apply (insert n_Elem_NatInterval[where q = "m - 1" and n=n and m=m])
   5.603 +	apply (insert mg0)
   5.604 +	apply auto
   5.605 +	done
   5.606 +      ultimately show False by auto      
   5.607 +    qed
   5.608 +    ultimately have "False" using u by arith
   5.609 +  }
   5.610 +  note lemma_nat2Nat = this
   5.611 +  show ?thesis
   5.612 +    apply (auto simp add: inj_on_def)
   5.613 +    apply (case_tac "x = y")
   5.614 +    apply auto
   5.615 +    apply (case_tac "x < y")
   5.616 +    apply (case_tac "? m. y = x + m & 0 < m")
   5.617 +    apply (auto intro: lemma_nat2Nat, arith)
   5.618 +    apply (case_tac "y < x")
   5.619 +    apply (case_tac "? m. x = y + m & 0 < m")
   5.620 +    apply auto
   5.621 +    apply (drule sym)
   5.622 +    apply (auto intro: lemma_nat2Nat, arith)
   5.623 +    done
   5.624 +qed
   5.625 +
   5.626 +lemma Nat2nat_nat2Nat[simp]: "Nat2nat (nat2Nat n) = n"
   5.627 +  by (simp add: Nat2nat_def inv_f_f[OF inj_nat2Nat])
   5.628 +
   5.629 +lemma nat2Nat_Nat2nat[simp]: "Elem n Nat \<Longrightarrow> nat2Nat (Nat2nat n) = n"
   5.630 +  apply (simp add: Nat2nat_def)
   5.631 +  apply (rule_tac f_inv_f)
   5.632 +  apply (auto simp add: image_def Nat_def Sep)
   5.633 +  done
   5.634 +
   5.635 +lemma Nat2nat_SucNat: "Elem N Nat \<Longrightarrow> Nat2nat (SucNat N) = Suc (Nat2nat N)"
   5.636 +  apply (auto simp add: Nat_def Sep Nat2nat_def)
   5.637 +  apply (auto simp add: inv_f_f[OF inj_nat2Nat])
   5.638 +  apply (simp only: nat2Nat.simps[symmetric])
   5.639 +  apply (simp only: inv_f_f[OF inj_nat2Nat])
   5.640 +  done
   5.641 +  
   5.642 +
   5.643 +(*lemma Elem_induct: "(\<And>x. \<forall>y. Elem y x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a"
   5.644 +  by (erule wf_induct[OF wf_is_Elem_of, simplified is_Elem_of_def, simplified])*)
   5.645 +
   5.646 +lemma Elem_Opair_exists: "? z. Elem x z & Elem y z & Elem z (Opair x y)"
   5.647 +  apply (rule exI[where x="Upair x y"])
   5.648 +  by (simp add: Upair Opair_def)
   5.649 +
   5.650 +lemma UNIV_is_not_in_ZF: "UNIV \<noteq> explode R"
   5.651 +proof
   5.652 +  let ?Russell = "{ x. Not(Elem x x) }"
   5.653 +  have "?Russell = UNIV" by (simp add: irreflexiv_Elem)
   5.654 +  moreover assume "UNIV = explode R"
   5.655 +  ultimately have russell: "?Russell = explode R" by simp
   5.656 +  then show "False"
   5.657 +  proof(cases "Elem R R")
   5.658 +    case True     
   5.659 +    then show ?thesis 
   5.660 +      by (insert irreflexiv_Elem, auto)
   5.661 +  next
   5.662 +    case False
   5.663 +    then have "R \<in> ?Russell" by auto
   5.664 +    then have "Elem R R" by (simp add: russell explode_def)
   5.665 +    with False show ?thesis by auto
   5.666 +  qed
   5.667 +qed
   5.668 +
   5.669 +constdefs 
   5.670 +  SpecialR :: "(ZF * ZF) set"
   5.671 +  "SpecialR \<equiv> { (x, y) . x \<noteq> Empty \<and> y = Empty}"
   5.672 +
   5.673 +lemma "wf SpecialR"
   5.674 +  apply (subst wf_def)
   5.675 +  apply (auto simp add: SpecialR_def)
   5.676 +  done
   5.677 +
   5.678 +constdefs
   5.679 +  Ext :: "('a * 'b) set \<Rightarrow> 'b \<Rightarrow> 'a set"
   5.680 +  "Ext R y \<equiv> { x . (x, y) \<in> R }" 
   5.681 +
   5.682 +lemma Ext_Elem: "Ext is_Elem_of = explode"
   5.683 +  by (auto intro: ext simp add: Ext_def is_Elem_of_def explode_def)
   5.684 +
   5.685 +lemma "Ext SpecialR Empty \<noteq> explode z"
   5.686 +proof 
   5.687 +  have "Ext SpecialR Empty = UNIV - {Empty}"
   5.688 +    by (auto simp add: Ext_def SpecialR_def)
   5.689 +  moreover assume "Ext SpecialR Empty = explode z"
   5.690 +  ultimately have "UNIV = explode(union z (Singleton Empty)) "
   5.691 +    by (auto simp add: explode_def union Singleton)
   5.692 +  then show "False" by (simp add: UNIV_is_not_in_ZF)
   5.693 +qed
   5.694 +
   5.695 +constdefs 
   5.696 +  implode :: "ZF set \<Rightarrow> ZF"
   5.697 +  "implode == inv explode"
   5.698 +
   5.699 +lemma inj_explode: "inj explode"
   5.700 +  by (auto simp add: inj_on_def explode_def Ext)
   5.701 +
   5.702 +lemma implode_explode[simp]: "implode (explode x) = x"
   5.703 +  by (simp add: implode_def inj_explode)
   5.704 +
   5.705 +constdefs
   5.706 +  regular :: "(ZF * ZF) set \<Rightarrow> bool"
   5.707 +  "regular R == ! A. A \<noteq> Empty \<longrightarrow> (? x. Elem x A & (! y. (y, x) \<in> R \<longrightarrow> Not (Elem y A)))"
   5.708 +  implodeable_Ext :: "(ZF * ZF) set \<Rightarrow> bool"
   5.709 +  "implodeable_Ext R == ! y. Ext R y \<in> range explode"
   5.710 +  wfzf :: "(ZF * ZF) set \<Rightarrow> bool"
   5.711 +  "wfzf R == regular R & implodeable_Ext R"
   5.712 +
   5.713 +lemma regular_Elem: "regular is_Elem_of"
   5.714 +  by (simp add: regular_def is_Elem_of_def Regularity)
   5.715 +
   5.716 +lemma implodeable_Elem: "implodeable_Ext is_Elem_of"
   5.717 +  by (auto simp add: implodeable_Ext_def image_def Ext_Elem)
   5.718 +
   5.719 +lemma wfzf_is_Elem_of: "wfzf is_Elem_of"
   5.720 +  by (auto simp add: wfzf_def regular_Elem implodeable_Elem)
   5.721 +
   5.722 +constdefs
   5.723 +  SeqSum :: "(nat \<Rightarrow> ZF) \<Rightarrow> ZF"
   5.724 +  "SeqSum f == Sum (Repl Nat (f o Nat2nat))"
   5.725 +
   5.726 +lemma SeqSum: "Elem x (SeqSum f) = (? n. Elem x (f n))"
   5.727 +  apply (auto simp add: SeqSum_def Sum Repl)
   5.728 +  apply (rule_tac x = "f n" in exI)
   5.729 +  apply auto
   5.730 +  done
   5.731 +
   5.732 +constdefs
   5.733 +  Ext_ZF :: "(ZF * ZF) set \<Rightarrow> ZF \<Rightarrow> ZF"
   5.734 +  "Ext_ZF R s == implode (Ext R s)"
   5.735 +
   5.736 +lemma Elem_implode: "A \<in> range explode \<Longrightarrow> Elem x (implode A) = (x \<in> A)"
   5.737 +  apply (auto)
   5.738 +  apply (simp_all add: explode_def)
   5.739 +  done
   5.740 +
   5.741 +lemma Elem_Ext_ZF: "implodeable_Ext R \<Longrightarrow> Elem x (Ext_ZF R s) = ((x,s) \<in> R)"
   5.742 +  apply (simp add: Ext_ZF_def)
   5.743 +  apply (subst Elem_implode)
   5.744 +  apply (simp add: implodeable_Ext_def)
   5.745 +  apply (simp add: Ext_def)
   5.746 +  done
   5.747 +
   5.748 +consts
   5.749 +  Ext_ZF_n :: "(ZF * ZF) set \<Rightarrow> ZF \<Rightarrow> nat \<Rightarrow> ZF"
   5.750 +
   5.751 +primrec
   5.752 +  "Ext_ZF_n R s 0 = Ext_ZF R s"
   5.753 +  "Ext_ZF_n R s (Suc n) = Sum (Repl (Ext_ZF_n R s n) (Ext_ZF R))"
   5.754 +
   5.755 +constdefs
   5.756 +  Ext_ZF_hull :: "(ZF * ZF) set \<Rightarrow> ZF \<Rightarrow> ZF"
   5.757 +  "Ext_ZF_hull R s == SeqSum (Ext_ZF_n R s)"
   5.758 +
   5.759 +lemma Elem_Ext_ZF_hull:
   5.760 +  assumes implodeable_R: "implodeable_Ext R" 
   5.761 +  shows "Elem x (Ext_ZF_hull R S) = (? n. Elem x (Ext_ZF_n R S n))"
   5.762 +  by (simp add: Ext_ZF_hull_def SeqSum)
   5.763 +  
   5.764 +lemma Elem_Elem_Ext_ZF_hull:
   5.765 +  assumes implodeable_R: "implodeable_Ext R" 
   5.766 +          and x_hull: "Elem x (Ext_ZF_hull R S)"
   5.767 +          and y_R_x: "(y, x) \<in> R"
   5.768 +  shows "Elem y (Ext_ZF_hull R S)"
   5.769 +proof -
   5.770 +  from Elem_Ext_ZF_hull[OF implodeable_R] x_hull 
   5.771 +  have "? n. Elem x (Ext_ZF_n R S n)" by auto
   5.772 +  then obtain n where n:"Elem x (Ext_ZF_n R S n)" ..
   5.773 +  with y_R_x have "Elem y (Ext_ZF_n R S (Suc n))"
   5.774 +    apply (auto simp add: Repl Sum)
   5.775 +    apply (rule_tac x="Ext_ZF R x" in exI) 
   5.776 +    apply (auto simp add: Elem_Ext_ZF[OF implodeable_R])
   5.777 +    done
   5.778 +  with Elem_Ext_ZF_hull[OF implodeable_R, where x=y] show ?thesis
   5.779 +    by (auto simp del: Ext_ZF_n.simps)
   5.780 +qed
   5.781 +
   5.782 +lemma wfzf_minimal:
   5.783 +  assumes hyps: "wfzf R" "C \<noteq> {}"
   5.784 +  shows "\<exists>x. x \<in> C \<and> (\<forall>y. (y, x) \<in> R \<longrightarrow> y \<notin> C)"
   5.785 +proof -
   5.786 +  from hyps have "\<exists>S. S \<in> C" by auto
   5.787 +  then obtain S where S:"S \<in> C" by auto  
   5.788 +  let ?T = "Sep (Ext_ZF_hull R S) (\<lambda> s. s \<in> C)"
   5.789 +  from hyps have implodeable_R: "implodeable_Ext R" by (simp add: wfzf_def)
   5.790 +  show ?thesis
   5.791 +  proof (cases "?T = Empty")
   5.792 +    case True
   5.793 +    then have "\<forall> z. \<not> (Elem z (Sep (Ext_ZF R S) (\<lambda> s. s \<in> C)))"      
   5.794 +      apply (auto simp add: Ext Empty Sep Ext_ZF_hull_def SeqSum)
   5.795 +      apply (erule_tac x="z" in allE, auto)
   5.796 +      apply (erule_tac x=0 in allE, auto)
   5.797 +      done
   5.798 +    then show ?thesis 
   5.799 +      apply (rule_tac exI[where x=S])
   5.800 +      apply (auto simp add: Sep Empty S)
   5.801 +      apply (erule_tac x=y in allE)
   5.802 +      apply (simp add: implodeable_R Elem_Ext_ZF)
   5.803 +      done
   5.804 +  next
   5.805 +    case False
   5.806 +    from hyps have regular_R: "regular R" by (simp add: wfzf_def)
   5.807 +    from 
   5.808 +      regular_R[simplified regular_def, rule_format, OF False, simplified Sep] 
   5.809 +      Elem_Elem_Ext_ZF_hull[OF implodeable_R]
   5.810 +    show ?thesis by blast
   5.811 +  qed
   5.812 +qed
   5.813 +
   5.814 +lemma wfzf_implies_wf: "wfzf R \<Longrightarrow> wf R"
   5.815 +proof (subst wf_def, rule allI)
   5.816 +  assume wfzf: "wfzf R"
   5.817 +  fix P :: "ZF \<Rightarrow> bool"
   5.818 +  let ?C = "{x. P x}"
   5.819 +  {
   5.820 +    assume induct: "(\<forall>x. (\<forall>y. (y, x) \<in> R \<longrightarrow> P y) \<longrightarrow> P x)"
   5.821 +    let ?C = "{x. \<not> (P x)}"
   5.822 +    have "?C = {}"
   5.823 +    proof (rule ccontr)
   5.824 +      assume C: "?C \<noteq> {}"
   5.825 +      from
   5.826 +	wfzf_minimal[OF wfzf C]
   5.827 +      obtain x where x: "x \<in> ?C \<and> (\<forall>y. (y, x) \<in> R \<longrightarrow> y \<notin> ?C)" ..
   5.828 +      then have "P x"
   5.829 +	apply (rule_tac induct[rule_format])
   5.830 +	apply auto
   5.831 +	done
   5.832 +      with x show "False" by auto
   5.833 +    qed
   5.834 +    then have "! x. P x" by auto
   5.835 +  }
   5.836 +  then show "(\<forall>x. (\<forall>y. (y, x) \<in> R \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> (! x. P x)" by blast
   5.837 +qed
   5.838 +
   5.839 +lemma wf_is_Elem_of: "wf is_Elem_of"
   5.840 +  by (auto simp add: wfzf_is_Elem_of wfzf_implies_wf)
   5.841 +
   5.842 +lemma in_Ext_RTrans_implies_Elem_Ext_ZF_hull:  
   5.843 +  "implodeable_Ext R \<Longrightarrow> x \<in> (Ext (R^+) s) \<Longrightarrow> Elem x (Ext_ZF_hull R s)"
   5.844 +  apply (simp add: Ext_def Elem_Ext_ZF_hull)
   5.845 +  apply (erule converse_trancl_induct[where r="R"])
   5.846 +  apply (rule exI[where x=0])
   5.847 +  apply (simp add: Elem_Ext_ZF)
   5.848 +  apply auto
   5.849 +  apply (rule_tac x="Suc n" in exI)
   5.850 +  apply (simp add: Sum Repl)
   5.851 +  apply (rule_tac x="Ext_ZF R z" in exI)
   5.852 +  apply (auto simp add: Elem_Ext_ZF)
   5.853 +  done
   5.854 +
   5.855 +lemma implodeable_Ext_trancl: "implodeable_Ext R \<Longrightarrow> implodeable_Ext (R^+)"
   5.856 +  apply (subst implodeable_Ext_def)
   5.857 +  apply (auto simp add: image_def)
   5.858 +  apply (rule_tac x="Sep (Ext_ZF_hull R y) (\<lambda> z. z \<in> (Ext (R^+) y))" in exI)
   5.859 +  apply (auto simp add: explode_def Sep set_ext 
   5.860 +    in_Ext_RTrans_implies_Elem_Ext_ZF_hull)
   5.861 +  done
   5.862 + 
   5.863 +lemma Elem_Ext_ZF_hull_implies_in_Ext_RTrans[rule_format]:
   5.864 +  "implodeable_Ext R \<Longrightarrow> ! x. Elem x (Ext_ZF_n R s n) \<longrightarrow> x \<in> (Ext (R^+) s)"
   5.865 +  apply (induct_tac n)
   5.866 +  apply (auto simp add: Elem_Ext_ZF Ext_def Sum Repl)
   5.867 +  done
   5.868 +
   5.869 +lemma "implodeable_Ext R \<Longrightarrow> Ext_ZF (R^+) s = Ext_ZF_hull R s"
   5.870 +  apply (frule implodeable_Ext_trancl)
   5.871 +  apply (auto simp add: Ext)
   5.872 +  apply (erule in_Ext_RTrans_implies_Elem_Ext_ZF_hull)
   5.873 +  apply (simp add: Elem_Ext_ZF Ext_def)
   5.874 +  apply (auto simp add: Elem_Ext_ZF Elem_Ext_ZF_hull)
   5.875 +  apply (erule Elem_Ext_ZF_hull_implies_in_Ext_RTrans[simplified Ext_def, simplified], assumption)
   5.876 +  done
   5.877 +
   5.878 +lemma wf_implies_regular: "wf R \<Longrightarrow> regular R"
   5.879 +proof (simp add: regular_def, rule allI)
   5.880 +  assume wf: "wf R"
   5.881 +  fix A
   5.882 +  show "A \<noteq> Empty \<longrightarrow> (\<exists>x. Elem x A \<and> (\<forall>y. (y, x) \<in> R \<longrightarrow> \<not> Elem y A))"
   5.883 +  proof
   5.884 +    assume A: "A \<noteq> Empty"
   5.885 +    then have "? x. x \<in> explode A" 
   5.886 +      by (auto simp add: explode_def Ext Empty)
   5.887 +    then obtain x where x:"x \<in> explode A" ..   
   5.888 +    from iffD1[OF wf_eq_minimal wf, rule_format, where Q="explode A", OF x]
   5.889 +    obtain z where "z \<in> explode A \<and> (\<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> explode A)" by auto    
   5.890 +    then show "\<exists>x. Elem x A \<and> (\<forall>y. (y, x) \<in> R \<longrightarrow> \<not> Elem y A)"      
   5.891 +      apply (rule_tac exI[where x = z])
   5.892 +      apply (simp add: explode_def)
   5.893 +      done
   5.894 +  qed
   5.895 +qed
   5.896 +
   5.897 +lemma wf_eq_wfzf: "(wf R \<and> implodeable_Ext R) = wfzf R"
   5.898 +  apply (auto simp add: wfzf_implies_wf)
   5.899 +  apply (auto simp add: wfzf_def wf_implies_regular)
   5.900 +  done
   5.901 +
   5.902 +lemma wfzf_trancl: "wfzf R \<Longrightarrow> wfzf (R^+)"
   5.903 +  by (auto simp add: wf_eq_wfzf[symmetric] implodeable_Ext_trancl wf_trancl)
   5.904 +
   5.905 +lemma Ext_subset_mono: "R \<subseteq> S \<Longrightarrow> Ext R y \<subseteq> Ext S y"
   5.906 +  by (auto simp add: Ext_def)
   5.907 +
   5.908 +lemma implodeable_Ext_subset: "implodeable_Ext R \<Longrightarrow> S \<subseteq> R \<Longrightarrow> implodeable_Ext S"
   5.909 +  apply (auto simp add: implodeable_Ext_def)
   5.910 +  apply (erule_tac x=y in allE)
   5.911 +  apply (drule_tac y=y in Ext_subset_mono)
   5.912 +  apply (auto simp add: image_def)
   5.913 +  apply (rule_tac x="Sep x (% z. z \<in> (Ext S y))" in exI) 
   5.914 +  apply (auto simp add: explode_def Sep)
   5.915 +  done
   5.916 +
   5.917 +lemma wfzf_subset: "wfzf S \<Longrightarrow> R \<subseteq> S \<Longrightarrow> wfzf R"
   5.918 +  by (auto intro: implodeable_Ext_subset wf_subset simp add: wf_eq_wfzf[symmetric])  
   5.919 +
   5.920 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/ZF/Helper.thy	Tue Mar 07 16:03:31 2006 +0100
     6.3 @@ -0,0 +1,32 @@
     6.4 +(*  Title:      HOL/ZF/Helper.thy
     6.5 +    ID:         $Id$
     6.6 +    Author:     Steven Obua
     6.7 +
     6.8 +    Some helpful lemmas that probably will end up elsewhere. 
     6.9 +*)
    6.10 +
    6.11 +theory Helper 
    6.12 +imports Main
    6.13 +begin
    6.14 +
    6.15 +lemma theI2' : "?! x. P x \<Longrightarrow> (!! x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (THE x. P x)"
    6.16 +  apply auto
    6.17 +  apply (subgoal_tac "P (THE x. P x)")
    6.18 +  apply blast
    6.19 +  apply (rule theI)
    6.20 +  apply auto
    6.21 +  done
    6.22 +
    6.23 +lemma in_range_superfluous: "(z \<in> range f & z \<in> (f ` x)) = (z \<in> f ` x)" 
    6.24 +  by auto
    6.25 +
    6.26 +lemma f_x_in_range_f: "f x \<in> range f"
    6.27 +  by (blast intro: image_eqI)
    6.28 +
    6.29 +lemma comp_inj: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (g o f)"
    6.30 +  by (blast intro: comp_inj_on subset_inj_on)
    6.31 +
    6.32 +lemma comp_image_eq: "(g o f) ` x = g ` f ` x"
    6.33 +  by auto
    6.34 +  
    6.35 +end
    6.36 \ No newline at end of file
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/ZF/LProd.thy	Tue Mar 07 16:03:31 2006 +0100
     7.3 @@ -0,0 +1,189 @@
     7.4 +(*  Title:      HOL/ZF/LProd.thy
     7.5 +    ID:         $Id$
     7.6 +    Author:     Steven Obua
     7.7 +
     7.8 +    Introduces the lprod relation.
     7.9 +    See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan
    7.10 +*)
    7.11 +
    7.12 +theory LProd 
    7.13 +imports Multiset
    7.14 +begin
    7.15 +
    7.16 +consts
    7.17 +  lprod :: "('a * 'a) set \<Rightarrow> ('a list * 'a list) set"
    7.18 +
    7.19 +inductive "lprod R"
    7.20 +intros
    7.21 +  lprod_single[intro!]: "(a, b) \<in> R \<Longrightarrow> ([a], [b]) \<in> lprod R"
    7.22 +  lprod_list[intro!]: "(ah@at, bh@bt) \<in> lprod R \<Longrightarrow> (a,b) \<in> R \<or> a = b \<Longrightarrow> (ah@a#at, bh@b#bt) \<in> lprod R"
    7.23 +
    7.24 +lemma "(as,bs) \<in> lprod R \<Longrightarrow> length as = length bs"
    7.25 +  apply (induct as bs rule: lprod.induct)
    7.26 +  apply auto
    7.27 +  done
    7.28 +
    7.29 +lemma "(as, bs) \<in> lprod R \<Longrightarrow> 1 \<le> length as \<and> 1 \<le> length bs"
    7.30 +  apply (induct as bs rule: lprod.induct)
    7.31 +  apply auto
    7.32 +  done
    7.33 +
    7.34 +lemma lprod_subset_elem: "(as, bs) \<in> lprod S \<Longrightarrow> S \<subseteq> R \<Longrightarrow> (as, bs) \<in> lprod R"
    7.35 +  apply (induct as bs rule: lprod.induct)
    7.36 +  apply (auto)
    7.37 +  done
    7.38 +
    7.39 +lemma lprod_subset: "S \<subseteq> R \<Longrightarrow> lprod S \<subseteq> lprod R"
    7.40 +  by (auto intro: lprod_subset_elem)
    7.41 +
    7.42 +lemma lprod_implies_mult: "(as, bs) \<in> lprod R \<Longrightarrow> trans R \<Longrightarrow> (multiset_of as, multiset_of bs) \<in> mult R"
    7.43 +proof (induct as bs rule: lprod.induct)
    7.44 +  case (lprod_single a b)
    7.45 +  note step = one_step_implies_mult[
    7.46 +    where r=R and I="{#}" and K="{#a#}" and J="{#b#}", simplified]    
    7.47 +  show ?case by (auto intro: lprod_single step)
    7.48 +next
    7.49 +  case (lprod_list a ah at b bh bt) 
    7.50 +  from prems have transR: "trans R" by auto
    7.51 +  have as: "multiset_of (ah @ a # at) = multiset_of (ah @ at) + {#a#}" (is "_ = ?ma + _")
    7.52 +    by (simp add: ring_eq_simps)
    7.53 +  have bs: "multiset_of (bh @ b # bt) = multiset_of (bh @ bt) + {#b#}" (is "_ = ?mb + _")
    7.54 +    by (simp add: ring_eq_simps)
    7.55 +  from prems have "(?ma, ?mb) \<in> mult R"
    7.56 +    by auto
    7.57 +  with mult_implies_one_step[OF transR] have 
    7.58 +    "\<exists>I J K. ?mb = I + J \<and> ?ma = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> R)"
    7.59 +    by blast
    7.60 +  then obtain I J K where 
    7.61 +    decomposed: "?mb = I + J \<and> ?ma = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> R)"
    7.62 +    by blast   
    7.63 +  show ?case
    7.64 +  proof (cases "a = b")
    7.65 +    case True    
    7.66 +    have "((I + {#b#}) + K, (I + {#b#}) + J) \<in> mult R"
    7.67 +      apply (rule one_step_implies_mult[OF transR])
    7.68 +      apply (auto simp add: decomposed)
    7.69 +      done
    7.70 +    then show ?thesis
    7.71 +      apply (simp only: as bs)
    7.72 +      apply (simp only: decomposed True)
    7.73 +      apply (simp add: ring_eq_simps)
    7.74 +      done
    7.75 +  next
    7.76 +    case False
    7.77 +    from False lprod_list have False: "(a, b) \<in> R" by blast
    7.78 +    have "(I + (K + {#a#}), I + (J + {#b#})) \<in> mult R"
    7.79 +      apply (rule one_step_implies_mult[OF transR])
    7.80 +      apply (auto simp add: False decomposed)
    7.81 +      done
    7.82 +    then show ?thesis
    7.83 +      apply (simp only: as bs)
    7.84 +      apply (simp only: decomposed)
    7.85 +      apply (simp add: ring_eq_simps)
    7.86 +      done
    7.87 +  qed
    7.88 +qed
    7.89 +
    7.90 +lemma wf_lprod[recdef_wf,simp,intro]:
    7.91 +  assumes wf_R: "wf R"
    7.92 +  shows "wf (lprod R)"
    7.93 +proof -
    7.94 +  have subset: "lprod (R^+) \<subseteq> inv_image (mult (R^+)) multiset_of"
    7.95 +    by (auto simp add: inv_image_def lprod_implies_mult trans_trancl)
    7.96 +  note lprodtrancl = wf_subset[OF wf_inv_image[where r="mult (R^+)" and f="multiset_of", 
    7.97 +    OF wf_mult[OF wf_trancl[OF wf_R]]], OF subset]
    7.98 +  note lprod = wf_subset[OF lprodtrancl, where p="lprod R", OF lprod_subset, simplified]
    7.99 +  show ?thesis by (auto intro: lprod)
   7.100 +qed
   7.101 +
   7.102 +constdefs
   7.103 +  gprod_2_2 :: "('a * 'a) set \<Rightarrow> (('a * 'a) * ('a * 'a)) set"
   7.104 +  "gprod_2_2 R \<equiv> { ((a,b), (c,d)) . (a = c \<and> (b,d) \<in> R) \<or> (b = d \<and> (a,c) \<in> R) }"
   7.105 +  gprod_2_1 :: "('a * 'a) set \<Rightarrow> (('a * 'a) * ('a * 'a)) set"
   7.106 +  "gprod_2_1 R \<equiv>  { ((a,b), (c,d)) . (a = d \<and> (b,c) \<in> R) \<or> (b = c \<and> (a,d) \<in> R) }"
   7.107 +
   7.108 +lemma lprod_2_3: "(a, b) \<in> R \<Longrightarrow> ([a, c], [b, c]) \<in> lprod R"
   7.109 +  by (auto intro: lprod_list[where a=c and b=c and 
   7.110 +    ah = "[a]" and at = "[]" and bh="[b]" and bt="[]", simplified]) 
   7.111 +
   7.112 +lemma lprod_2_4: "(a, b) \<in> R \<Longrightarrow> ([c, a], [c, b]) \<in> lprod R"
   7.113 +  by (auto intro: lprod_list[where a=c and b=c and 
   7.114 +    ah = "[]" and at = "[a]" and bh="[]" and bt="[b]", simplified])
   7.115 +
   7.116 +lemma lprod_2_1: "(a, b) \<in> R \<Longrightarrow> ([c, a], [b, c]) \<in> lprod R"
   7.117 +  by (auto intro: lprod_list[where a=c and b=c and 
   7.118 +    ah = "[]" and at = "[a]" and bh="[b]" and bt="[]", simplified]) 
   7.119 +
   7.120 +lemma lprod_2_2: "(a, b) \<in> R \<Longrightarrow> ([a, c], [c, b]) \<in> lprod R"
   7.121 +  by (auto intro: lprod_list[where a=c and b=c and 
   7.122 +    ah = "[a]" and at = "[]" and bh="[]" and bt="[b]", simplified])
   7.123 +
   7.124 +lemma [recdef_wf, simp, intro]: 
   7.125 +  assumes wfR: "wf R" shows "wf (gprod_2_1 R)"
   7.126 +proof -
   7.127 +  have "gprod_2_1 R \<subseteq> inv_image (lprod R) (\<lambda> (a,b). [a,b])"
   7.128 +    by (auto simp add: inv_image_def gprod_2_1_def lprod_2_1 lprod_2_2)
   7.129 +  with wfR show ?thesis
   7.130 +    by (rule_tac wf_subset, auto)
   7.131 +qed
   7.132 +
   7.133 +lemma [recdef_wf, simp, intro]: 
   7.134 +  assumes wfR: "wf R" shows "wf (gprod_2_2 R)"
   7.135 +proof -
   7.136 +  have "gprod_2_2 R \<subseteq> inv_image (lprod R) (\<lambda> (a,b). [a,b])"
   7.137 +    by (auto simp add: inv_image_def gprod_2_2_def lprod_2_3 lprod_2_4)
   7.138 +  with wfR show ?thesis
   7.139 +    by (rule_tac wf_subset, auto)
   7.140 +qed
   7.141 +
   7.142 +lemma lprod_3_1: assumes "(x', x) \<in> R" shows "([y, z, x'], [x, y, z]) \<in> lprod R"
   7.143 +  apply (rule lprod_list[where a="y" and b="y" and ah="[]" and at="[z,x']" and bh="[x]" and bt="[z]", simplified])
   7.144 +  apply (auto simp add: lprod_2_1 prems)
   7.145 +  done
   7.146 +
   7.147 +lemma lprod_3_2: assumes "(z',z) \<in> R" shows "([z', x, y], [x,y,z]) \<in> lprod R"
   7.148 +  apply (rule lprod_list[where a="y" and b="y" and ah="[z',x]" and at="[]" and bh="[x]" and bt="[z]", simplified])
   7.149 +  apply (auto simp add: lprod_2_2 prems)
   7.150 +  done
   7.151 +
   7.152 +lemma lprod_3_3: assumes xr: "(xr, x) \<in> R" shows "([xr, y, z], [x, y, z]) \<in> lprod R"
   7.153 +  apply (rule lprod_list[where a="y" and b="y" and ah="[xr]" and at="[z]" and bh="[x]" and bt="[z]", simplified])
   7.154 +  apply (simp add: xr lprod_2_3)
   7.155 +  done
   7.156 +
   7.157 +lemma lprod_3_4: assumes yr: "(yr, y) \<in> R" shows "([x, yr, z], [x, y, z]) \<in> lprod R"
   7.158 +  apply (rule lprod_list[where a="x" and b="x" and ah="[]" and at="[yr,z]" and bh="[]" and bt="[y,z]", simplified])
   7.159 +  apply (simp add: yr lprod_2_3)
   7.160 +  done
   7.161 +
   7.162 +lemma lprod_3_5: assumes zr: "(zr, z) \<in> R" shows "([x, y, zr], [x, y, z]) \<in> lprod R"
   7.163 +  apply (rule lprod_list[where a="x" and b="x" and ah="[]" and at="[y,zr]" and bh="[]" and bt="[y,z]", simplified])
   7.164 +  apply (simp add: zr lprod_2_4)
   7.165 +  done
   7.166 +
   7.167 +lemma lprod_3_6: assumes y': "(y', y) \<in> R" shows "([x, z, y'], [x, y, z]) \<in> lprod R"
   7.168 +  apply (rule lprod_list[where a="z" and b="z" and ah="[x]" and at="[y']" and bh="[x,y]" and bt="[]", simplified])
   7.169 +  apply (simp add: y' lprod_2_4)
   7.170 +  done
   7.171 +
   7.172 +lemma lprod_3_7: assumes z': "(z',z) \<in> R" shows "([x, z', y], [x, y, z]) \<in> lprod R"
   7.173 +  apply (rule lprod_list[where a="y" and b="y" and ah="[x, z']" and at="[]" and bh="[x]" and bt="[z]", simplified])
   7.174 +  apply (simp add: z' lprod_2_4)
   7.175 +  done
   7.176 +
   7.177 +constdefs
   7.178 +   perm :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> bool"
   7.179 +   "perm f A \<equiv> inj_on f A \<and> f ` A = A"
   7.180 +
   7.181 +lemma "((as,bs) \<in> lprod R) = 
   7.182 +  (\<exists> f. perm f {0 ..< (length as)} \<and> 
   7.183 +  (\<forall> j. j < length as \<longrightarrow> ((nth as j, nth bs (f j)) \<in> R \<or> (nth as j = nth bs (f j)))) \<and> 
   7.184 +  (\<exists> i. i < length as \<and> (nth as i, nth bs (f i)) \<in> R))"
   7.185 +oops
   7.186 +
   7.187 +lemma "trans R \<Longrightarrow> (ah@a#at, bh@b#bt) \<in> lprod R \<Longrightarrow> (b, a) \<in> R \<or> a = b \<Longrightarrow> (ah@at, bh@bt) \<in> lprod R" 
   7.188 +oops
   7.189 +
   7.190 +
   7.191 +
   7.192 +end
   7.193 \ No newline at end of file
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/ZF/MainZF.thy	Tue Mar 07 16:03:31 2006 +0100
     8.3 @@ -0,0 +1,12 @@
     8.4 +(*  Title:      HOL/ZF/MainZF.thy
     8.5 +    ID:         $Id$
     8.6 +    Author:     Steven Obua
     8.7 +
     8.8 +    Starting point for using HOLZF.
     8.9 +    See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan
    8.10 +*)
    8.11 +
    8.12 +theory MainZF
    8.13 +imports Zet LProd
    8.14 +begin
    8.15 +end
    8.16 \ No newline at end of file
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/ZF/Zet.thy	Tue Mar 07 16:03:31 2006 +0100
     9.3 @@ -0,0 +1,221 @@
     9.4 +(*  Title:      HOL/ZF/Zet.thy
     9.5 +    ID:         $Id$
     9.6 +    Author:     Steven Obua
     9.7 +
     9.8 +    Introduces a type 'a zet of ZF representable sets.
     9.9 +    See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan
    9.10 +*)
    9.11 +
    9.12 +theory Zet 
    9.13 +imports HOLZF
    9.14 +begin
    9.15 +
    9.16 +typedef 'a zet = "{A :: 'a set | A f z. inj_on f A \<and> f ` A \<subseteq> explode z}"
    9.17 +  by blast
    9.18 +
    9.19 +constdefs
    9.20 +  zin :: "'a \<Rightarrow> 'a zet \<Rightarrow> bool"
    9.21 +  "zin x A == x \<in> (Rep_zet A)"
    9.22 +
    9.23 +lemma zet_ext_eq: "(A = B) = (! x. zin x A = zin x B)"
    9.24 +  by (auto simp add: Rep_zet_inject[symmetric] zin_def)
    9.25 +
    9.26 +constdefs
    9.27 +  zimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a zet \<Rightarrow> 'b zet"
    9.28 +  "zimage f A == Abs_zet (image f (Rep_zet A))"
    9.29 +
    9.30 +lemma zet_def': "zet = {A :: 'a set | A f z. inj_on f A \<and> f ` A = explode z}"
    9.31 +  apply (rule set_ext)
    9.32 +  apply (auto simp add: zet_def)
    9.33 +  apply (rule_tac x=f in exI)
    9.34 +  apply auto
    9.35 +  apply (rule_tac x="Sep z (\<lambda> y. y \<in> (f ` x))" in exI)
    9.36 +  apply (auto simp add: explode_def Sep)
    9.37 +  done
    9.38 +
    9.39 +lemma image_Inv_f_f: "inj_on f B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (Inv B f) ` f ` A = A"
    9.40 +  apply (rule set_ext)
    9.41 +  apply (auto simp add: Inv_f_f image_def)
    9.42 +  apply (rule_tac x="f x" in exI)
    9.43 +  apply (auto simp add: Inv_f_f)
    9.44 +  done
    9.45 +  
    9.46 +lemma image_zet_rep: "A \<in> zet \<Longrightarrow> ? z . g ` A = explode z"
    9.47 +  apply (auto simp add: zet_def')
    9.48 +  apply (rule_tac x="Repl z (g o (Inv A f))" in exI)
    9.49 +  apply (simp add: explode_Repl_eq)
    9.50 +  apply (subgoal_tac "explode z = f ` A")
    9.51 +  apply (simp_all add: comp_image_eq image_Inv_f_f)  
    9.52 +  done
    9.53 +
    9.54 +lemma Inv_f_f_mem:       
    9.55 +  assumes "x \<in> A"
    9.56 +  shows "Inv A g (g x) \<in> A"
    9.57 +  apply (simp add: Inv_def)
    9.58 +  apply (rule someI2)
    9.59 +  apply (auto!)
    9.60 +  done
    9.61 +
    9.62 +lemma zet_image_mem:
    9.63 +  assumes Azet: "A \<in> zet"
    9.64 +  shows "g ` A \<in> zet"
    9.65 +proof -
    9.66 +  from Azet have "? (f :: _ \<Rightarrow> ZF). inj_on f A" 
    9.67 +    by (auto simp add: zet_def')
    9.68 +  then obtain f where injf: "inj_on (f :: _ \<Rightarrow> ZF) A"  
    9.69 +    by auto
    9.70 +  let ?w = "f o (Inv A g)"
    9.71 +  have subset: "(Inv A g) ` (g ` A) \<subseteq> A"
    9.72 +    by (auto simp add: Inv_f_f_mem)
    9.73 +  have "inj_on (Inv A g) (g ` A)" by (simp add: inj_on_Inv)
    9.74 +  then have injw: "inj_on ?w (g ` A)"
    9.75 +    apply (rule comp_inj_on)
    9.76 +    apply (rule subset_inj_on[where B=A])
    9.77 +    apply (auto simp add: subset injf)
    9.78 +    done
    9.79 +  show ?thesis
    9.80 +    apply (simp add: zet_def' comp_image_eq[symmetric])
    9.81 +    apply (rule exI[where x="?w"])
    9.82 +    apply (simp add: injw image_zet_rep Azet)
    9.83 +    done
    9.84 +qed
    9.85 +
    9.86 +lemma Rep_zimage_eq: "Rep_zet (zimage f A) = image f (Rep_zet A)"
    9.87 +  apply (simp add: zimage_def)
    9.88 +  apply (subst Abs_zet_inverse)
    9.89 +  apply (simp_all add: Rep_zet zet_image_mem)
    9.90 +  done
    9.91 +
    9.92 +lemma zimage_iff: "zin y (zimage f A) = (? x. zin x A & y = f x)"
    9.93 +  by (auto simp add: zin_def Rep_zimage_eq)
    9.94 +
    9.95 +constdefs
    9.96 +  zimplode :: "ZF zet \<Rightarrow> ZF"
    9.97 +  "zimplode A == implode (Rep_zet A)"
    9.98 +  zexplode :: "ZF \<Rightarrow> ZF zet"
    9.99 +  "zexplode z == Abs_zet (explode z)"
   9.100 +
   9.101 +lemma Rep_zet_eq_explode: "? z. Rep_zet A = explode z"
   9.102 +  by (rule image_zet_rep[where g="\<lambda> x. x",OF Rep_zet, simplified])
   9.103 +
   9.104 +lemma zexplode_zimplode: "zexplode (zimplode A) = A"
   9.105 +  apply (simp add: zimplode_def zexplode_def)
   9.106 +  apply (simp add: implode_def)
   9.107 +  apply (subst f_inv_f[where y="Rep_zet A"])
   9.108 +  apply (auto simp add: Rep_zet_inverse Rep_zet_eq_explode image_def)
   9.109 +  done
   9.110 +
   9.111 +lemma explode_mem_zet: "explode z \<in> zet"
   9.112 +  apply (simp add: zet_def')
   9.113 +  apply (rule_tac x="% x. x" in exI)
   9.114 +  apply (auto simp add: inj_on_def)
   9.115 +  done
   9.116 +
   9.117 +lemma zimplode_zexplode: "zimplode (zexplode z) = z"
   9.118 +  apply (simp add: zimplode_def zexplode_def)
   9.119 +  apply (subst Abs_zet_inverse)
   9.120 +  apply (auto simp add: explode_mem_zet implode_explode)
   9.121 +  done  
   9.122 +
   9.123 +lemma zin_zexplode_eq: "zin x (zexplode A) = Elem x A"
   9.124 +  apply (simp add: zin_def zexplode_def)
   9.125 +  apply (subst Abs_zet_inverse)
   9.126 +  apply (simp_all add: explode_Elem explode_mem_zet) 
   9.127 +  done
   9.128 +
   9.129 +lemma comp_zimage_eq: "zimage g (zimage f A) = zimage (g o f) A"
   9.130 +  apply (simp add: zimage_def)
   9.131 +  apply (subst Abs_zet_inverse)
   9.132 +  apply (simp_all add: comp_image_eq zet_image_mem Rep_zet)
   9.133 +  done
   9.134 +    
   9.135 +constdefs
   9.136 +  zunion :: "'a zet \<Rightarrow> 'a zet \<Rightarrow> 'a zet"
   9.137 +  "zunion a b \<equiv> Abs_zet ((Rep_zet a) \<union> (Rep_zet b))"
   9.138 +  zsubset :: "'a zet \<Rightarrow> 'a zet \<Rightarrow> bool"
   9.139 +  "zsubset a b \<equiv> ! x. zin x a \<longrightarrow> zin x b"
   9.140 +
   9.141 +lemma explode_union: "explode (union a b) = (explode a) \<union> (explode b)"
   9.142 +  apply (rule set_ext)
   9.143 +  apply (simp add: explode_def union)
   9.144 +  done
   9.145 +
   9.146 +lemma Rep_zet_zunion: "Rep_zet (zunion a b) = (Rep_zet a) \<union> (Rep_zet b)"
   9.147 +proof -
   9.148 +  from Rep_zet[of a] have "? f z. inj_on f (Rep_zet a) \<and> f ` (Rep_zet a) = explode z"
   9.149 +    by (auto simp add: zet_def')
   9.150 +  then obtain fa za where a:"inj_on fa (Rep_zet a) \<and> fa ` (Rep_zet a) = explode za"
   9.151 +    by blast
   9.152 +  from a have fa: "inj_on fa (Rep_zet a)" by blast
   9.153 +  from a have za: "fa ` (Rep_zet a) = explode za" by blast
   9.154 +  from Rep_zet[of b] have "? f z. inj_on f (Rep_zet b) \<and> f ` (Rep_zet b) = explode z"
   9.155 +    by (auto simp add: zet_def')
   9.156 +  then obtain fb zb where b:"inj_on fb (Rep_zet b) \<and> fb ` (Rep_zet b) = explode zb"
   9.157 +    by blast
   9.158 +  from b have fb: "inj_on fb (Rep_zet b)" by blast
   9.159 +  from b have zb: "fb ` (Rep_zet b) = explode zb" by blast 
   9.160 +  let ?f = "(\<lambda> x. if x \<in> (Rep_zet a) then Opair (fa x) (Empty) else Opair (fb x) (Singleton Empty))" 
   9.161 +  let ?z = "CartProd (union za zb) (Upair Empty (Singleton Empty))"
   9.162 +  have se: "Singleton Empty \<noteq> Empty"
   9.163 +    apply (auto simp add: Ext Singleton)
   9.164 +    apply (rule exI[where x=Empty])
   9.165 +    apply (simp add: Empty)
   9.166 +    done
   9.167 +  show ?thesis
   9.168 +    apply (simp add: zunion_def)
   9.169 +    apply (subst Abs_zet_inverse)
   9.170 +    apply (auto simp add: zet_def)
   9.171 +    apply (rule exI[where x = ?f])
   9.172 +    apply (rule conjI)
   9.173 +    apply (auto simp add: inj_on_def Opair inj_onD[OF fa] inj_onD[OF fb] se se[symmetric])
   9.174 +    apply (rule exI[where x = ?z])
   9.175 +    apply (insert za zb)
   9.176 +    apply (auto simp add: explode_def CartProd union Upair Opair)
   9.177 +    done
   9.178 +qed
   9.179 +
   9.180 +lemma zunion: "zin x (zunion a b) = ((zin x a) \<or> (zin x b))"
   9.181 +  by (auto simp add: zin_def Rep_zet_zunion)
   9.182 +
   9.183 +lemma zimage_zexplode_eq: "zimage f (zexplode z) = zexplode (Repl z f)"
   9.184 +  by (simp add: zet_ext_eq zin_zexplode_eq Repl zimage_iff)
   9.185 +
   9.186 +lemma range_explode_eq_zet: "range explode = zet"
   9.187 +  apply (rule set_ext)
   9.188 +  apply (auto simp add: explode_mem_zet)
   9.189 +  apply (drule image_zet_rep)
   9.190 +  apply (simp add: image_def)
   9.191 +  apply auto
   9.192 +  apply (rule_tac x=z in exI)
   9.193 +  apply auto
   9.194 +  done
   9.195 +
   9.196 +lemma Elem_zimplode: "(Elem x (zimplode z)) = (zin x z)"
   9.197 +  apply (simp add: zimplode_def)
   9.198 +  apply (subst Elem_implode)
   9.199 +  apply (simp_all add: zin_def Rep_zet range_explode_eq_zet)
   9.200 +  done
   9.201 +
   9.202 +constdefs
   9.203 +  zempty :: "'a zet"
   9.204 +  "zempty \<equiv> Abs_zet {}"
   9.205 +
   9.206 +lemma zempty[simp]: "\<not> (zin x zempty)"
   9.207 +  by (auto simp add: zin_def zempty_def Abs_zet_inverse zet_def)
   9.208 +
   9.209 +lemma zimage_zempty[simp]: "zimage f zempty = zempty"
   9.210 +  by (auto simp add: zet_ext_eq zimage_iff)
   9.211 +
   9.212 +lemma zunion_zempty_left[simp]: "zunion zempty a = a"
   9.213 +  by (simp add: zet_ext_eq zunion)
   9.214 +
   9.215 +lemma zunion_zempty_right[simp]: "zunion a zempty = a"
   9.216 +  by (simp add: zet_ext_eq zunion)
   9.217 +
   9.218 +lemma zimage_id[simp]: "zimage id A = A"
   9.219 +  by (simp add: zet_ext_eq zimage_iff)
   9.220 +
   9.221 +lemma zimage_cong[recdef_cong]: "\<lbrakk> M = N; !! x. zin x N \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> zimage f M = zimage g N"
   9.222 +  by (auto simp add: zet_ext_eq zimage_iff)
   9.223 +
   9.224 +end
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/ZF/document/root.tex	Tue Mar 07 16:03:31 2006 +0100
    10.3 @@ -0,0 +1,28 @@
    10.4 +
    10.5 +% $Id$
    10.6 +
    10.7 +\documentclass[11pt,a4paper]{article}
    10.8 +\usepackage{isabelle,isabellesym}
    10.9 +
   10.10 +% this should be the last package used
   10.11 +\usepackage{pdfsetup}
   10.12 +
   10.13 +% urls in roman style, theory text in math-similar italics
   10.14 +\urlstyle{rm}
   10.15 +\isabellestyle{it}
   10.16 +
   10.17 +\newcommand{\ganz}{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}
   10.18 +
   10.19 +\begin{document}
   10.20 +
   10.21 +\title{ZF}
   10.22 +\author{Steven Obua}
   10.23 +\maketitle
   10.24 +
   10.25 +%\tableofcontents
   10.26 +
   10.27 +\parindent 0pt\parskip 0.5ex
   10.28 +
   10.29 +\input{session}
   10.30 +
   10.31 +\end{document}