# HG changeset patch
# User obua
# Date 1141743811 -3600
# Node ID 7785075206842dd29075f7737a84677e5bf90478
# Parent  0b9eb4b0ad98a65267396ef74fd327a0e6a65f08
Added HOL-ZF to Isabelle.

diff -r 0b9eb4b0ad98 -r 778507520684 src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Tue Mar 07 14:09:48 2006 +0100
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Tue Mar 07 16:03:31 2006 +0100
@@ -30,7 +30,8 @@
   DEF_NUM_REP
   TYDEF_sum
   DEF_INL
-  DEF_INR;
+  DEF_INR
+  TYDEF_option;
 
 type_maps
   ind > Nat.ind
@@ -39,7 +40,8 @@
   N_1 >  Product_Type.unit
   prod > "*"
   num > nat
-  sum > "+";
+  sum > "+"
+  option > Datatype.option;
 
 const_renames
   "==" > "eqeq"
diff -r 0b9eb4b0ad98 -r 778507520684 src/HOL/Import/replay.ML
--- a/src/HOL/Import/replay.ML	Tue Mar 07 14:09:48 2006 +0100
+++ b/src/HOL/Import/replay.ML	Tue Mar 07 16:03:31 2006 +0100
@@ -369,7 +369,13 @@
 		     (entry::cached, normal)
 		 end)
 	    else
-		raise ERR "import_thms" ("cached theorems are not in-sync, expected: "^thmname^", found: "^thmname')
+		let
+		    val _ = writeln ("cached theorems are not in-sync,  expected: "^thmname^", found: "^thmname')
+		    val _ = writeln ("proceeding with next uncached theorem...")
+		in
+		    ([], thmname::names)
+		end
+	(*	raise ERR "import_thms" ("cached theorems are not in-sync, expected: "^thmname^", found: "^thmname')*)
 	  | zip (thmname::_) (DeltaEntry _ :: _) = 
  	    raise ERR "import_thms" ("expected theorem '"^thmname^"', but found a delta")
 	fun zip' xs (History ys) = 
diff -r 0b9eb4b0ad98 -r 778507520684 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Mar 07 14:09:48 2006 +0100
+++ b/src/HOL/IsaMakefile	Tue Mar 07 16:03:31 2006 +0100
@@ -40,7 +40,8 @@
   HOL-UNITY \
   HOL-Unix \
   HOL-W0 \
-  HOL-ex
+  HOL-ZF \
+  HOL-ex 
     # ^ this is the sort position
 
 all: test images
@@ -451,6 +452,14 @@
   Unix/document/root.bib Unix/document/root.tex
 	@$(ISATOOL) usedir $(OUT)/HOL Unix
 
+## HOL-ZF
+
+HOL-ZF: HOL $(LOG)/HOL-ZF.gz
+
+$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML  \
+  ZF/Helper.thy ZF/LProd.thy ZF/HOLZF.thy \
+  ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex
+	@$(ISATOOL) usedir $(OUT)/HOL ZF
 
 ## HOL-Modelcheck
 
diff -r 0b9eb4b0ad98 -r 778507520684 src/HOL/ZF/Games.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ZF/Games.thy	Tue Mar 07 16:03:31 2006 +0100
@@ -0,0 +1,961 @@
+(*  Title:      HOL/ZF/Games.thy
+    ID:         $Id$
+    Author:     Steven Obua
+
+    An application of HOLZF: Partizan Games.
+    See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan
+*)
+
+theory Games 
+imports MainZF
+begin
+
+constdefs
+  fixgames :: "ZF set \<Rightarrow> ZF set"
+  "fixgames A \<equiv> { Opair l r | l r. explode l \<subseteq> A & explode r \<subseteq> A}"
+  games_lfp :: "ZF set"
+  "games_lfp \<equiv> lfp fixgames"
+  games_gfp :: "ZF set"
+  "games_gfp \<equiv> gfp fixgames"
+
+lemma mono_fixgames: "mono (fixgames)"
+  apply (auto simp add: mono_def fixgames_def)
+  apply (rule_tac x=l in exI)
+  apply (rule_tac x=r in exI)
+  apply auto
+  done
+
+lemma games_lfp_unfold: "games_lfp = fixgames games_lfp"
+  by (auto simp add: def_lfp_unfold games_lfp_def mono_fixgames)
+
+lemma games_gfp_unfold: "games_gfp = fixgames games_gfp"
+  by (auto simp add: def_gfp_unfold games_gfp_def mono_fixgames)
+
+lemma games_lfp_nonempty: "Opair Empty Empty \<in> games_lfp"
+proof -
+  have "fixgames {} \<subseteq> games_lfp" 
+    apply (subst games_lfp_unfold)
+    apply (simp add: mono_fixgames[simplified mono_def, rule_format])
+    done
+  moreover have "fixgames {} = {Opair Empty Empty}"
+    by (simp add: fixgames_def explode_Empty)
+  finally show ?thesis
+    by auto
+qed
+
+constdefs
+  left_option :: "ZF \<Rightarrow> ZF \<Rightarrow> bool"
+  "left_option g opt \<equiv> (Elem opt (Fst g))"
+  right_option :: "ZF \<Rightarrow> ZF \<Rightarrow> bool"
+  "right_option g opt \<equiv> (Elem opt (Snd g))"
+  is_option_of :: "(ZF * ZF) set"
+  "is_option_of \<equiv> { (opt, g) | opt g. g \<in> games_gfp \<and> (left_option g opt \<or> right_option g opt) }"
+
+lemma games_lfp_subset_gfp: "games_lfp \<subseteq> games_gfp"
+proof -
+  have "games_lfp \<subseteq> fixgames games_lfp" 
+    by (simp add: games_lfp_unfold[symmetric])
+  then show ?thesis
+    by (simp add: games_gfp_def gfp_upperbound)
+qed
+
+lemma games_option_stable: 
+  assumes fixgames: "games = fixgames games"
+  and g: "g \<in> games"
+  and opt: "left_option g opt \<or> right_option g opt"
+  shows "opt \<in> games"
+proof -
+  from g fixgames have "g \<in> fixgames games" by auto
+  then have "\<exists> l r. g = Opair l r \<and> explode l \<subseteq> games \<and> explode r \<subseteq> games"
+    by (simp add: fixgames_def)
+  then obtain l where "\<exists> r. g = Opair l r \<and> explode l \<subseteq> games \<and> explode r \<subseteq> games" ..
+  then obtain r where lr: "g = Opair l r \<and> explode l \<subseteq> games \<and> explode r \<subseteq> games" ..
+  with opt show ?thesis
+    by (auto intro: Elem_explode_in simp add: left_option_def right_option_def Fst Snd)
+qed
+    
+lemma option2elem: "(opt,g) \<in> is_option_of  \<Longrightarrow> \<exists> u v. Elem opt u \<and> Elem u v \<and> Elem v g"
+  apply (simp add: is_option_of_def)
+  apply (subgoal_tac "(g \<in> games_gfp) = (g \<in> (fixgames games_gfp))")
+  prefer 2
+  apply (simp add: games_gfp_unfold[symmetric])
+  apply (auto simp add: fixgames_def left_option_def right_option_def Fst Snd)
+  apply (rule_tac x=l in exI, insert Elem_Opair_exists, blast)
+  apply (rule_tac x=r in exI, insert Elem_Opair_exists, blast) 
+  done
+
+lemma is_option_of_subset_is_Elem_of: "is_option_of \<subseteq> (is_Elem_of^+)"
+proof -
+  {
+    fix opt
+    fix g
+    assume "(opt, g) \<in> is_option_of"
+    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^+)" 
+      apply -
+      apply (drule option2elem)
+      apply (auto simp add: r_into_trancl' is_Elem_of_def)
+      done
+    then have "(opt, g) \<in> (is_Elem_of^+)"
+      by (blast intro: trancl_into_rtrancl trancl_rtrancl_trancl)
+  } 
+  then show ?thesis by auto
+qed
+
+lemma wfzf_is_option_of: "wfzf is_option_of"
+proof - 
+  have "wfzf (is_Elem_of^+)" by (simp add: wfzf_trancl wfzf_is_Elem_of)
+  then show ?thesis 
+    apply (rule wfzf_subset)
+    apply (rule is_option_of_subset_is_Elem_of)
+    done
+  qed
+  
+lemma games_gfp_imp_lfp: "g \<in> games_gfp \<longrightarrow> g \<in> games_lfp"
+proof -
+  have unfold_gfp: "\<And> x. x \<in> games_gfp \<Longrightarrow> x \<in> (fixgames games_gfp)" 
+    by (simp add: games_gfp_unfold[symmetric])
+  have unfold_lfp: "\<And> x. (x \<in> games_lfp) = (x \<in> (fixgames games_lfp))"
+    by (simp add: games_lfp_unfold[symmetric])
+  show ?thesis
+    apply (rule wf_induct[OF wfzf_implies_wf[OF wfzf_is_option_of]])
+    apply (auto simp add: is_option_of_def)
+    apply (drule_tac unfold_gfp)
+    apply (simp add: fixgames_def)
+    apply (auto simp add: left_option_def Fst right_option_def Snd)
+    apply (subgoal_tac "explode l \<subseteq> games_lfp")
+    apply (subgoal_tac "explode r \<subseteq> games_lfp")
+    apply (subst unfold_lfp)
+    apply (auto simp add: fixgames_def)
+    apply (simp_all add: explode_Elem Elem_explode_in)
+    done
+qed
+
+theorem games_lfp_eq_gfp: "games_lfp = games_gfp"
+  apply (auto simp add: games_gfp_imp_lfp)
+  apply (insert games_lfp_subset_gfp)
+  apply auto
+  done
+
+theorem unique_games: "(g = fixgames g) = (g = games_lfp)"
+proof -
+  {
+    fix g 
+    assume g: "g = fixgames g"
+    from g have "fixgames g \<subseteq> g" by auto
+    then have l:"games_lfp \<subseteq> g" 
+      by (simp add: games_lfp_def lfp_lowerbound)
+    from g have "g \<subseteq> fixgames g" by auto
+    then have u:"g \<subseteq> games_gfp" 
+      by (simp add: games_gfp_def gfp_upperbound)
+    from l u games_lfp_eq_gfp[symmetric] have "g = games_lfp"
+      by auto
+  }
+  note games = this
+  show ?thesis
+    apply (rule iff[rule_format])
+    apply (erule games)
+    apply (simp add: games_lfp_unfold[symmetric])
+    done
+qed
+
+lemma games_lfp_option_stable: 
+  assumes g: "g \<in> games_lfp"
+  and opt: "left_option g opt \<or> right_option g opt"
+  shows "opt \<in> games_lfp"
+  apply (rule games_option_stable[where g=g])
+  apply (simp add: games_lfp_unfold[symmetric])
+  apply (simp_all add: prems)
+  done
+
+lemma is_option_of_imp_games:
+  assumes hyp: "(opt, g) \<in> is_option_of"
+  shows "opt \<in> games_lfp \<and> g \<in> games_lfp"
+proof -
+  from hyp have g_game: "g \<in> games_lfp" 
+    by (simp add: is_option_of_def games_lfp_eq_gfp)
+  from hyp have "left_option g opt \<or> right_option g opt"
+    by (auto simp add: is_option_of_def)
+  with g_game games_lfp_option_stable[OF g_game, OF this] show ?thesis
+    by auto
+qed
+ 
+lemma games_lfp_represent: "x \<in> games_lfp \<Longrightarrow> \<exists> l r. x = Opair l r"
+  apply (rule exI[where x="Fst x"])
+  apply (rule exI[where x="Snd x"])
+  apply (subgoal_tac "x \<in> (fixgames games_lfp)")
+  apply (simp add: fixgames_def)
+  apply (auto simp add: Fst Snd)
+  apply (simp add: games_lfp_unfold[symmetric])
+  done
+
+typedef game = games_lfp
+  by (blast intro: games_lfp_nonempty)
+
+constdefs
+  left_options :: "game \<Rightarrow> game zet"
+  "left_options g \<equiv> zimage Abs_game (zexplode (Fst (Rep_game g)))"
+  right_options :: "game \<Rightarrow> game zet"
+  "right_options g \<equiv> zimage Abs_game (zexplode (Snd (Rep_game g)))"
+  options :: "game \<Rightarrow> game zet"
+  "options g \<equiv> zunion (left_options g) (right_options g)"
+  Game :: "game zet \<Rightarrow> game zet \<Rightarrow> game"
+  "Game L R \<equiv> Abs_game (Opair (zimplode (zimage Rep_game L)) (zimplode (zimage Rep_game R)))"
+  
+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"
+  apply (subst Ext)
+  apply (simp add: Repl)
+  apply auto
+  apply (subst Abs_game_inverse, simp_all add: game_def)
+  apply (rule_tac x=za in exI)
+  apply (subst Abs_game_inverse, simp_all add: game_def)
+  done
+
+lemma game_split: "g = Game (left_options g) (right_options g)"
+proof -
+  have "\<exists> l r. Rep_game g = Opair l r"
+    apply (insert Rep_game[of g])
+    apply (simp add: game_def games_lfp_represent)
+    done
+  then obtain l r where lr: "Rep_game g = Opair l r" by auto
+  have partizan_g: "Rep_game g \<in> games_lfp" 
+    apply (insert Rep_game[of g])
+    apply (simp add: game_def)
+    done
+  have "\<forall> e. Elem e l \<longrightarrow> left_option (Rep_game g) e"
+    by (simp add: lr left_option_def Fst)
+  then have partizan_l: "\<forall> e. Elem e l \<longrightarrow> e \<in> games_lfp"
+    apply auto
+    apply (rule games_lfp_option_stable[where g="Rep_game g", OF partizan_g])
+    apply auto
+    done
+  have "\<forall> e. Elem e r \<longrightarrow> right_option (Rep_game g) e"
+    by (simp add: lr right_option_def Snd)
+  then have partizan_r: "\<forall> e. Elem e r \<longrightarrow> e \<in> games_lfp"
+    apply auto
+    apply (rule games_lfp_option_stable[where g="Rep_game g", OF partizan_g])
+    apply auto
+    done   
+  let ?L = "zimage (Abs_game) (zexplode l)"
+  let ?R = "zimage (Abs_game) (zexplode r)"
+  have L:"?L = left_options g"
+    by (simp add: left_options_def lr Fst)
+  have R:"?R = right_options g"
+    by (simp add: right_options_def lr Snd)
+  have "g = Game ?L ?R"
+    apply (simp add: Game_def Rep_game_inject[symmetric] comp_zimage_eq zimage_zexplode_eq zimplode_zexplode)
+    apply (simp add: Repl_Rep_game_Abs_game partizan_l partizan_r)
+    apply (subst Abs_game_inverse)
+    apply (simp_all add: lr[symmetric] Rep_game) 
+    done
+  then show ?thesis
+    by (simp add: L R)
+qed
+
+lemma Opair_in_games_lfp: 
+  assumes l: "explode l \<subseteq> games_lfp"
+  and r: "explode r \<subseteq> games_lfp"
+  shows "Opair l r \<in> games_lfp"
+proof -
+  note f = unique_games[of games_lfp, simplified]
+  show ?thesis
+    apply (subst f)
+    apply (simp add: fixgames_def)
+    apply (rule exI[where x=l])
+    apply (rule exI[where x=r])
+    apply (auto simp add: l r)
+    done
+qed
+
+lemma left_options[simp]: "left_options (Game l r) = l"
+  apply (simp add: left_options_def Game_def)
+  apply (subst Abs_game_inverse)
+  apply (simp add: game_def)
+  apply (rule Opair_in_games_lfp)
+  apply (auto simp add: explode_Elem Elem_zimplode zimage_iff Rep_game[simplified game_def])
+  apply (simp add: Fst zexplode_zimplode comp_zimage_eq)
+  apply (simp add: zet_ext_eq zimage_iff Rep_game_inverse)
+  done
+
+lemma right_options[simp]: "right_options (Game l r) = r"
+  apply (simp add: right_options_def Game_def)
+  apply (subst Abs_game_inverse)
+  apply (simp add: game_def)
+  apply (rule Opair_in_games_lfp)
+  apply (auto simp add: explode_Elem Elem_zimplode zimage_iff Rep_game[simplified game_def])
+  apply (simp add: Snd zexplode_zimplode comp_zimage_eq)
+  apply (simp add: zet_ext_eq zimage_iff Rep_game_inverse)
+  done  
+
+lemma Game_ext: "(Game l1 r1 = Game l2 r2) = ((l1 = l2) \<and> (r1 = r2))"
+  apply auto
+  apply (subst left_options[where l=l1 and r=r1,symmetric])
+  apply (subst left_options[where l=l2 and r=r2,symmetric])
+  apply simp
+  apply (subst right_options[where l=l1 and r=r1,symmetric])
+  apply (subst right_options[where l=l2 and r=r2,symmetric])
+  apply simp
+  done
+
+constdefs
+  option_of :: "(game * game) set"
+  "option_of \<equiv> image (\<lambda> (option, g). (Abs_game option, Abs_game g)) is_option_of"
+
+lemma option_to_is_option_of: "((option, g) \<in> option_of) = ((Rep_game option, Rep_game g) \<in> is_option_of)"
+  apply (auto simp add: option_of_def)
+  apply (subst Abs_game_inverse)
+  apply (simp add: is_option_of_imp_games game_def)
+  apply (subst Abs_game_inverse)
+  apply (simp add: is_option_of_imp_games game_def)
+  apply simp
+  apply (auto simp add: Bex_def image_def)  
+  apply (rule exI[where x="Rep_game option"])
+  apply (rule exI[where x="Rep_game g"])
+  apply (simp add: Rep_game_inverse)
+  done
+  
+lemma wf_is_option_of: "wf is_option_of"
+  apply (rule wfzf_implies_wf)
+  apply (simp add: wfzf_is_option_of)
+  done
+
+lemma wf_option_of[recdef_wf, simp, intro]: "wf option_of"
+proof -
+  have option_of: "option_of = inv_image is_option_of Rep_game"
+    apply (rule set_ext)
+    apply (case_tac "x")
+    by (simp add: inv_image_def option_to_is_option_of) 
+  show ?thesis
+    apply (simp add: option_of)
+    apply (auto intro: wf_inv_image wf_is_option_of)
+    done
+qed
+  
+lemma right_option_is_option[simp, intro]: "zin x (right_options g) \<Longrightarrow> zin x (options g)"
+  by (simp add: options_def zunion)
+
+lemma left_option_is_option[simp, intro]: "zin x (left_options g) \<Longrightarrow> zin x (options g)"
+  by (simp add: options_def zunion)
+
+lemma zin_options[simp, intro]: "zin x (options g) \<Longrightarrow> (x, g) \<in> option_of"
+  apply (simp add: options_def zunion left_options_def right_options_def option_of_def 
+    image_def is_option_of_def zimage_iff zin_zexplode_eq) 
+  apply (cases g)
+  apply (cases x)
+  apply (auto simp add: Abs_game_inverse games_lfp_eq_gfp[symmetric] game_def 
+    right_option_def[symmetric] left_option_def[symmetric])
+  done
+
+consts
+  neg_game :: "game \<Rightarrow> game"
+
+recdef neg_game "option_of"
+  "neg_game g = Game (zimage neg_game (right_options g)) (zimage neg_game (left_options g))"
+
+declare neg_game.simps[simp del]
+
+lemma "neg_game (neg_game g) = g"
+  apply (induct g rule: neg_game.induct)
+  apply (subst neg_game.simps)+
+  apply (simp add: right_options left_options comp_zimage_eq)
+  apply (subgoal_tac "zimage (neg_game o neg_game) (left_options g) = left_options g")
+  apply (subgoal_tac "zimage (neg_game o neg_game) (right_options g) = right_options g")
+  apply (auto simp add: game_split[symmetric])
+  apply (auto simp add: zet_ext_eq zimage_iff)
+  done
+
+consts
+  ge_game :: "(game * game) \<Rightarrow> bool" 
+
+recdef ge_game "(gprod_2_1 option_of)"
+  "ge_game (G, H) = (\<forall> x. if zin x (right_options G) then (
+                          if zin x (left_options H) then \<not> (ge_game (H, x) \<or> (ge_game (x, G))) 
+                                                    else \<not> (ge_game (H, x)))
+                          else (if zin x (left_options H) then \<not> (ge_game (x, G)) else True))"
+(hints simp: gprod_2_1_def)
+
+declare ge_game.simps [simp del]
+
+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)))"
+  apply (subst ge_game.simps[where G=G and H=H])
+  apply (auto)
+  done
+
+lemma ge_game_leftright_refl[rule_format]: 
+  "\<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)"
+proof (induct x rule: wf_induct[OF wf_option_of]) 
+  case (1 "g")
+  { 
+    fix y
+    assume y: "zin y (right_options g)"
+    have "\<not> ge_game (g, y)"
+    proof -
+      have "(y, g) \<in> option_of" by (auto intro: y)
+      with 1 have "ge_game (y, y)" by auto
+      with y show ?thesis by (subst ge_game_def, auto)
+    qed
+  }
+  note right = this
+  { 
+    fix y
+    assume y: "zin y (left_options g)"
+    have "\<not> ge_game (y, g)"
+    proof -
+      have "(y, g) \<in> option_of" by (auto intro: y)
+      with 1 have "ge_game (y, y)" by auto
+      with y show ?thesis by (subst ge_game_def, auto)
+    qed
+  } 
+  note left = this
+  from left right show ?case
+    by (auto, subst ge_game_def, auto)
+qed
+
+lemma ge_game_refl: "ge_game (x,x)" by (simp add: ge_game_leftright_refl)
+
+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)"
+proof (induct x rule: wf_induct[OF wf_option_of]) 
+  case (1 "g")  
+  show ?case
+  proof (auto)
+    {case (goal1 y) 
+      from goal1 have "(y, g) \<in> option_of" by (auto)
+      with 1 have "ge_game (y, y)" by auto
+      with goal1 have "\<not> ge_game (g, y)" 
+	by (subst ge_game_def, auto)
+      with goal1 show ?case by auto}
+    note right = this
+    {case (goal2 y)
+      from goal2 have "(y, g) \<in> option_of" by (auto)
+      with 1 have "ge_game (y, y)" by auto
+      with goal2 have "\<not> ge_game (y, g)" 
+	by (subst ge_game_def, auto)
+      with goal2 show ?case by auto}
+    note left = this
+    {case goal3
+      from left right show ?case
+	by (subst ge_game_def, auto)
+    }
+  qed
+qed
+	
+constdefs
+  eq_game :: "game \<Rightarrow> game \<Rightarrow> bool"
+  "eq_game G H \<equiv> ge_game (G, H) \<and> ge_game (H, G)" 
+
+lemma eq_game_sym: "(eq_game G H) = (eq_game H G)"
+  by (auto simp add: eq_game_def)
+
+lemma eq_game_refl: "eq_game G G"
+  by (simp add: ge_game_refl eq_game_def)
+
+lemma induct_game: "(\<And>x. \<forall>y. (y, x) \<in> lprod option_of \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a"
+  by (erule wf_induct[OF wf_lprod[OF wf_option_of]])
+
+lemma ge_game_trans:
+  assumes "ge_game (x, y)" "ge_game (y, z)" 
+  shows "ge_game (x, z)"
+proof -  
+  { 
+    fix a
+    have "\<forall> x y z. a = [x,y,z] \<longrightarrow> ge_game (x,y) \<longrightarrow> ge_game (y,z) \<longrightarrow> ge_game (x, z)"
+    proof (induct a rule: induct_game)
+      case (1 a)
+      show ?case
+      proof (rule allI | rule impI)+
+	case (goal1 x y z)
+	show ?case
+	proof -
+	  { fix xr
+            assume xr:"zin xr (right_options x)"
+	    assume "ge_game (z, xr)"
+	    have "ge_game (y, xr)"
+	      apply (rule 1[rule_format, where y="[y,z,xr]"])
+	      apply (auto intro: xr lprod_3_1 simp add: prems)
+	      done
+	    moreover from xr have "\<not> ge_game (y, xr)"
+	      by (simp add: goal1(2)[simplified ge_game_def[of x y], rule_format, of xr, simplified xr])
+	    ultimately have "False" by auto      
+	  }
+	  note xr = this
+	  { fix zl
+	    assume zl:"zin zl (left_options z)"
+	    assume "ge_game (zl, x)"
+	    have "ge_game (zl, y)"
+	      apply (rule 1[rule_format, where y="[zl,x,y]"])
+	      apply (auto intro: zl lprod_3_2 simp add: prems)
+	      done
+	    moreover from zl have "\<not> ge_game (zl, y)"
+	      by (simp add: goal1(3)[simplified ge_game_def[of y z], rule_format, of zl, simplified zl])
+	    ultimately have "False" by auto
+	  }
+	  note zl = this
+	  show ?thesis
+	    by (auto simp add: ge_game_def[of x z] intro: xr zl)
+	qed
+      qed
+    qed
+  } 
+  note trans = this[of "[x, y, z]", simplified, rule_format]    
+  with prems show ?thesis by blast
+qed
+
+lemma eq_game_trans: "eq_game a b \<Longrightarrow> eq_game b c \<Longrightarrow> eq_game a c"
+  by (auto simp add: eq_game_def intro: ge_game_trans)
+
+constdefs
+  zero_game :: game
+  "zero_game \<equiv> Game zempty zempty"
+
+consts 
+  plus_game :: "game * game \<Rightarrow> game"
+
+recdef plus_game "gprod_2_2 option_of"
+  "plus_game (G, H) = Game (zunion (zimage (\<lambda> g. plus_game (g, H)) (left_options G))
+                                   (zimage (\<lambda> h. plus_game (G, h)) (left_options H)))
+                           (zunion (zimage (\<lambda> g. plus_game (g, H)) (right_options G))
+                                   (zimage (\<lambda> h. plus_game (G, h)) (right_options H)))"
+(hints simp add: gprod_2_2_def)
+
+declare plus_game.simps[simp del]
+
+lemma plus_game_comm: "plus_game (G, H) = plus_game (H, G)"
+proof (induct G H rule: plus_game.induct)
+  case (1 G H)
+  show ?case
+    by (auto simp add: 
+      plus_game.simps[where G=G and H=H] 
+      plus_game.simps[where G=H and H=G]
+      Game_ext zet_ext_eq zunion zimage_iff prems)
+qed
+
+lemma game_ext_eq: "(G = H) = (left_options G = left_options H \<and> right_options G = right_options H)"
+proof -
+  have "(G = H) = (Game (left_options G) (right_options G) = Game (left_options H) (right_options H))"
+    by (simp add: game_split[symmetric])
+  then show ?thesis by auto
+qed
+
+lemma left_zero_game[simp]: "left_options (zero_game) = zempty"
+  by (simp add: zero_game_def)
+
+lemma right_zero_game[simp]: "right_options (zero_game) = zempty"
+  by (simp add: zero_game_def)
+
+lemma plus_game_zero_right[simp]: "plus_game (G, zero_game) = G"
+proof -
+  { 
+    fix G H
+    have "H = zero_game \<longrightarrow> plus_game (G, H) = G "
+    proof (induct G H rule: plus_game.induct, rule impI)
+      case (goal1 G H)
+      note induct_hyp = prems[simplified goal1, simplified] and prems
+      show ?case
+	apply (simp only: plus_game.simps[where G=G and H=H])
+	apply (simp add: game_ext_eq prems)
+	apply (auto simp add: 
+	  zimage_cong[where f = "\<lambda> g. plus_game (g, zero_game)" and g = "id"] 
+	  induct_hyp)
+	done
+    qed
+  }
+  then show ?thesis by auto
+qed
+
+lemma plus_game_zero_left: "plus_game (zero_game, G) = G"
+  by (simp add: plus_game_comm)
+
+lemma left_imp_options[simp]: "zin opt (left_options g) \<Longrightarrow> zin opt (options g)"
+  by (simp add: options_def zunion)
+
+lemma right_imp_options[simp]: "zin opt (right_options g) \<Longrightarrow> zin opt (options g)"
+  by (simp add: options_def zunion)
+
+lemma left_options_plus: 
+  "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))" 
+  by (subst plus_game.simps, simp)
+
+lemma right_options_plus:
+  "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))"
+  by (subst plus_game.simps, simp)
+
+lemma left_options_neg: "left_options (neg_game u) = zimage neg_game (right_options u)"	 
+  by (subst neg_game.simps, simp)
+
+lemma right_options_neg: "right_options (neg_game u) = zimage neg_game (left_options u)"
+  by (subst neg_game.simps, simp)
+  
+lemma plus_game_assoc: "plus_game (plus_game (F, G), H) = plus_game (F, plus_game (G, H))"
+proof -
+  { 
+    fix a
+    have "\<forall> F G H. a = [F, G, H] \<longrightarrow> plus_game (plus_game (F, G), H) = plus_game (F, plus_game (G, H))"
+    proof (induct a rule: induct_game, (rule impI | rule allI)+)
+      case (goal1 x F G H)
+      let ?L = "plus_game (plus_game (F, G), H)"
+      let ?R = "plus_game (F, plus_game (G, H))"
+      note options_plus = left_options_plus right_options_plus
+      {
+	fix opt
+	note hyp = goal1(1)[simplified goal1(2), rule_format] 
+	have F: "zin opt (options F)  \<Longrightarrow> plus_game (plus_game (opt, G), H) = plus_game (opt, plus_game (G, H))"
+	  by (blast intro: hyp lprod_3_3)
+	have G: "zin opt (options G) \<Longrightarrow> plus_game (plus_game (F, opt), H) = plus_game (F, plus_game (opt, H))"
+	  by (blast intro: hyp lprod_3_4)
+	have H: "zin opt (options H) \<Longrightarrow> plus_game (plus_game (F, G), opt) = plus_game (F, plus_game (G, opt))" 
+	  by (blast intro: hyp lprod_3_5)
+	note F and G and H
+      }
+      note induct_hyp = this
+      have "left_options ?L = left_options ?R \<and> right_options ?L = right_options ?R"
+	by (auto simp add: 
+	  plus_game.simps[where G="plus_game (F,G)" and H=H]
+	  plus_game.simps[where G="F" and H="plus_game (G,H)"] 
+	  zet_ext_eq zunion zimage_iff options_plus
+	  induct_hyp left_imp_options right_imp_options)
+      then show ?case
+	by (simp add: game_ext_eq)
+    qed
+  }
+  then show ?thesis by auto
+qed
+
+lemma neg_plus_game: "neg_game (plus_game (G, H)) = plus_game(neg_game G, neg_game H)"
+proof (induct G H rule: plus_game.induct)
+  case (1 G H)
+  note opt_ops = 
+    left_options_plus right_options_plus 
+    left_options_neg right_options_neg  
+  show ?case
+    by (auto simp add: opt_ops
+      neg_game.simps[of "plus_game (G,H)"]
+      plus_game.simps[of "neg_game G" "neg_game H"]
+      Game_ext zet_ext_eq zunion zimage_iff prems)
+qed
+
+lemma eq_game_plus_inverse: "eq_game (plus_game (x, neg_game x)) zero_game"
+proof (induct x rule: wf_induct[OF wf_option_of])
+  case (goal1 x)
+  { fix y
+    assume "zin y (options x)"
+    then have "eq_game (plus_game (y, neg_game y)) zero_game"
+      by (auto simp add: prems)
+  }
+  note ihyp = this
+  {
+    fix y
+    assume y: "zin y (right_options x)"
+    have "\<not> (ge_game (zero_game, plus_game (y, neg_game x)))"
+      apply (subst ge_game.simps, simp)
+      apply (rule exI[where x="plus_game (y, neg_game y)"])
+      apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
+      apply (auto simp add: left_options_plus left_options_neg zunion zimage_iff intro: prems)
+      done
+  }
+  note case1 = this
+  {
+    fix y
+    assume y: "zin y (left_options x)"
+    have "\<not> (ge_game (zero_game, plus_game (x, neg_game y)))"
+      apply (subst ge_game.simps, simp)
+      apply (rule exI[where x="plus_game (y, neg_game y)"])
+      apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
+      apply (auto simp add: left_options_plus zunion zimage_iff intro: prems)
+      done
+  }
+  note case2 = this
+  {
+    fix y
+    assume y: "zin y (left_options x)"
+    have "\<not> (ge_game (plus_game (y, neg_game x), zero_game))"
+      apply (subst ge_game.simps, simp)
+      apply (rule exI[where x="plus_game (y, neg_game y)"])
+      apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
+      apply (auto simp add: right_options_plus right_options_neg zunion zimage_iff intro: prems)
+      done
+  }
+  note case3 = this
+  {
+    fix y
+    assume y: "zin y (right_options x)"
+    have "\<not> (ge_game (plus_game (x, neg_game y), zero_game))"
+      apply (subst ge_game.simps, simp)
+      apply (rule exI[where x="plus_game (y, neg_game y)"])
+      apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
+      apply (auto simp add: right_options_plus zunion zimage_iff intro: prems)
+      done
+  }
+  note case4 = this
+  show ?case
+    apply (simp add: eq_game_def)
+    apply (simp add: ge_game.simps[of "plus_game (x, neg_game x)" "zero_game"])
+    apply (simp add: ge_game.simps[of "zero_game" "plus_game (x, neg_game x)"])
+    apply (simp add: right_options_plus left_options_plus right_options_neg left_options_neg zunion zimage_iff)
+    apply (auto simp add: case1 case2 case3 case4)
+    done
+qed
+
+lemma ge_plus_game_left: "ge_game (y,z) = ge_game(plus_game (x, y), plus_game (x, z))"
+proof -
+  { fix a
+    have "\<forall> x y z. a = [x,y,z] \<longrightarrow> ge_game (y,z) = ge_game(plus_game (x, y), plus_game (x, z))"
+    proof (induct a rule: induct_game, (rule impI | rule allI)+)
+      case (goal1 a x y z)
+      note induct_hyp = goal1(1)[rule_format, simplified goal1(2)]
+      { 
+	assume hyp: "ge_game(plus_game (x, y), plus_game (x, z))"
+	have "ge_game (y, z)"
+	proof -
+	  { fix yr
+	    assume yr: "zin yr (right_options y)"
+	    from hyp have "\<not> (ge_game (plus_game (x, z), plus_game (x, yr)))"
+	      by (auto simp add: ge_game_def[of "plus_game (x,y)" "plus_game(x,z)"]
+		right_options_plus zunion zimage_iff intro: yr)
+	    then have "\<not> (ge_game (z, yr))"
+	      apply (subst induct_hyp[where y="[x, z, yr]", of "x" "z" "yr"])
+	      apply (simp_all add: yr lprod_3_6)
+	      done
+	  }
+	  note yr = this
+	  { fix zl
+	    assume zl: "zin zl (left_options z)"
+	    from hyp have "\<not> (ge_game (plus_game (x, zl), plus_game (x, y)))"
+	      by (auto simp add: ge_game_def[of "plus_game (x,y)" "plus_game(x,z)"]
+		left_options_plus zunion zimage_iff intro: zl)
+	    then have "\<not> (ge_game (zl, y))"
+	      apply (subst goal1(1)[rule_format, where y="[x, zl, y]", of "x" "zl" "y"])
+	      apply (simp_all add: goal1(2) zl lprod_3_7)
+	      done
+	  }	
+	  note zl = this
+	  show "ge_game (y, z)"
+	    apply (subst ge_game_def)
+	    apply (auto simp add: yr zl)
+	    done
+	qed      
+      }
+      note right_imp_left = this
+      {
+	assume yz: "ge_game (y, z)"
+	{
+	  fix x'
+	  assume x': "zin x' (right_options x)"
+	  assume hyp: "ge_game (plus_game (x, z), plus_game (x', y))"
+	  then have n: "\<not> (ge_game (plus_game (x', y), plus_game (x', z)))"
+	    by (auto simp add: ge_game_def[of "plus_game (x,z)" "plus_game (x', y)"] 
+	      right_options_plus zunion zimage_iff intro: x')
+	  have t: "ge_game (plus_game (x', y), plus_game (x', z))"
+	    apply (subst induct_hyp[symmetric])
+	    apply (auto intro: lprod_3_3 x' yz)
+	    done
+	  from n t have "False" by blast
+	}    
+	note case1 = this
+	{
+	  fix x'
+	  assume x': "zin x' (left_options x)"
+	  assume hyp: "ge_game (plus_game (x', z), plus_game (x, y))"
+	  then have n: "\<not> (ge_game (plus_game (x', y), plus_game (x', z)))"
+	    by (auto simp add: ge_game_def[of "plus_game (x',z)" "plus_game (x, y)"] 
+	      left_options_plus zunion zimage_iff intro: x')
+	  have t: "ge_game (plus_game (x', y), plus_game (x', z))"
+	    apply (subst induct_hyp[symmetric])
+	    apply (auto intro: lprod_3_3 x' yz)
+	    done
+	  from n t have "False" by blast
+	}
+	note case3 = this
+	{
+	  fix y'
+	  assume y': "zin y' (right_options y)"
+	  assume hyp: "ge_game (plus_game(x, z), plus_game (x, y'))"
+	  then have "ge_game(z, y')"
+	    apply (subst induct_hyp[of "[x, z, y']" "x" "z" "y'"])
+	    apply (auto simp add: hyp lprod_3_6 y')
+	    done
+	  with yz have "ge_game (y, y')"
+	    by (blast intro: ge_game_trans)      
+	  with y' have "False" by (auto simp add: ge_game_leftright_refl)
+	}
+	note case2 = this
+	{
+	  fix z'
+	  assume z': "zin z' (left_options z)"
+	  assume hyp: "ge_game (plus_game(x, z'), plus_game (x, y))"
+	  then have "ge_game(z', y)"
+	    apply (subst induct_hyp[of "[x, z', y]" "x" "z'" "y"])
+	    apply (auto simp add: hyp lprod_3_7 z')
+	    done    
+	  with yz have "ge_game (z', z)"
+	    by (blast intro: ge_game_trans)      
+	  with z' have "False" by (auto simp add: ge_game_leftright_refl)
+	}
+	note case4 = this   
+	have "ge_game(plus_game (x, y), plus_game (x, z))"
+	  apply (subst ge_game_def)
+	  apply (auto simp add: right_options_plus left_options_plus zunion zimage_iff)
+	  apply (auto intro: case1 case2 case3 case4)
+	  done
+      }
+      note left_imp_right = this
+      show ?case by (auto intro: right_imp_left left_imp_right)
+    qed
+  }
+  note a = this[of "[x, y, z]"]
+  then show ?thesis by blast
+qed
+
+lemma ge_plus_game_right: "ge_game (y,z) = ge_game(plus_game (y, x), plus_game (z, x))"
+  by (simp add: ge_plus_game_left plus_game_comm)
+
+lemma ge_neg_game: "ge_game (neg_game x, neg_game y) = ge_game (y, x)"
+proof -
+  { fix a
+    have "\<forall> x y. a = [x, y] \<longrightarrow> ge_game (neg_game x, neg_game y) = ge_game (y, x)"
+    proof (induct a rule: induct_game, (rule impI | rule allI)+)
+      case (goal1 a x y)
+      note ihyp = goal1(1)[rule_format, simplified goal1(2)]
+      { fix xl
+	assume xl: "zin xl (left_options x)"
+	have "ge_game (neg_game y, neg_game xl) = ge_game (xl, y)"
+	  apply (subst ihyp)
+	  apply (auto simp add: lprod_2_1 xl)
+	  done
+      }
+      note xl = this
+      { fix yr
+	assume yr: "zin yr (right_options y)"
+	have "ge_game (neg_game yr, neg_game x) = ge_game (x, yr)"
+	  apply (subst ihyp)
+	  apply (auto simp add: lprod_2_2 yr)
+	  done
+      }
+      note yr = this
+      show ?case
+	by (auto simp add: ge_game_def[of "neg_game x" "neg_game y"] ge_game_def[of "y" "x"]
+	  right_options_neg left_options_neg zimage_iff  xl yr)
+    qed
+  }
+  note a = this[of "[x,y]"]
+  then show ?thesis by blast
+qed
+
+constdefs 
+  eq_game_rel :: "(game * game) set"
+  "eq_game_rel \<equiv> { (p, q) . eq_game p q }"
+
+typedef Pg = "UNIV//eq_game_rel"
+  by (auto simp add: quotient_def)
+
+lemma equiv_eq_game[simp]: "equiv UNIV eq_game_rel"
+  by (auto simp add: equiv_def refl_def sym_def trans_def eq_game_rel_def
+    eq_game_sym intro: eq_game_refl eq_game_trans)
+
+instance Pg :: "{ord,zero,plus,minus}" ..
+
+defs (overloaded)
+  Pg_zero_def: "0 \<equiv> Abs_Pg (eq_game_rel `` {zero_game})"
+  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)"
+  Pg_less_def: "G < H \<equiv> G \<le> H \<and> G \<noteq> (H::Pg)"
+  Pg_minus_def: "- G \<equiv> contents (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
+  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)})})"
+  Pg_diff_def: "G - H \<equiv> G + (- (H::Pg))"
+
+lemma Rep_Abs_eq_Pg[simp]: "Rep_Pg (Abs_Pg (eq_game_rel `` {g})) = eq_game_rel `` {g}"
+  apply (subst Abs_Pg_inverse)
+  apply (auto simp add: Pg_def quotient_def)
+  done
+
+lemma char_Pg_le[simp]: "(Abs_Pg (eq_game_rel `` {g}) \<le> Abs_Pg (eq_game_rel `` {h})) = (ge_game (h, g))"
+  apply (simp add: Pg_le_def)
+  apply (auto simp add: eq_game_rel_def eq_game_def intro: ge_game_trans ge_game_refl)
+  done
+
+lemma char_Pg_eq[simp]: "(Abs_Pg (eq_game_rel `` {g}) = Abs_Pg (eq_game_rel `` {h})) = (eq_game g h)"
+  apply (simp add: Rep_Pg_inject [symmetric])
+  apply (subst eq_equiv_class_iff[of UNIV])
+  apply (simp_all)
+  apply (simp add: eq_game_rel_def)
+  done
+
+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)})"
+proof -
+  have "(\<lambda> g h. {Abs_Pg (eq_game_rel `` {plus_game (g, h)})}) respects2 eq_game_rel" 
+    apply (simp add: congruent2_def)
+    apply (auto simp add: eq_game_rel_def eq_game_def)
+    apply (rule_tac y="plus_game (y1, z2)" in ge_game_trans)
+    apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+
+    apply (rule_tac y="plus_game (z1, y2)" in ge_game_trans)
+    apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+
+    done
+  then show ?thesis
+    by (simp add: Pg_plus_def UN_equiv_class2[OF equiv_eq_game equiv_eq_game]) 
+qed
+    
+lemma char_Pg_minus[simp]: "- Abs_Pg (eq_game_rel `` {g}) = Abs_Pg (eq_game_rel `` {neg_game g})"
+proof -
+  have "(\<lambda> g. {Abs_Pg (eq_game_rel `` {neg_game g})}) respects eq_game_rel"
+    apply (simp add: congruent_def)
+    apply (auto simp add: eq_game_rel_def eq_game_def ge_neg_game)
+    done    
+  then show ?thesis
+    by (simp add: Pg_minus_def UN_equiv_class[OF equiv_eq_game])
+qed
+
+lemma eq_Abs_Pg[rule_format, cases type: Pg]: "(\<forall> g. z = Abs_Pg (eq_game_rel `` {g}) \<longrightarrow> P) \<longrightarrow> P"
+  apply (cases z, simp)
+  apply (simp add: Rep_Pg_inject[symmetric])
+  apply (subst Abs_Pg_inverse, simp)
+  apply (auto simp add: Pg_def quotient_def)
+  done
+
+instance Pg :: pordered_ab_group_add 
+proof
+  fix a b c :: Pg
+  show "(a < b) = (a \<le> b \<and> a \<noteq> b)" by (simp add: Pg_less_def)
+  show "a - b = a + (- b)" by (simp add: Pg_diff_def)
+  {
+    assume ab: "a \<le> b"
+    assume ba: "b \<le> a"
+    from ab ba show "a = b"
+      apply (cases a, cases b)
+      apply (simp add: eq_game_def)
+      done
+  }
+  show "a + b = b + a"
+    apply (cases a, cases b)
+    apply (simp add: eq_game_def plus_game_comm)
+    done
+  show "a + b + c = a + (b + c)"
+    apply (cases a, cases b, cases c)
+    apply (simp add: eq_game_def plus_game_assoc)
+    done
+  show "0 + a = a"
+    apply (cases a)
+    apply (simp add: Pg_zero_def plus_game_zero_left)
+    done
+  show "- a + a = 0"
+    apply (cases a)
+    apply (simp add: Pg_zero_def eq_game_plus_inverse plus_game_comm)
+    done
+  show "a \<le> a"
+    apply (cases a)
+    apply (simp add: ge_game_refl)
+    done
+  {
+    assume ab: "a \<le> b"
+    assume bc: "b \<le> c"
+    from ab bc show "a \<le> c"
+      apply (cases a, cases b, cases c)
+      apply (auto intro: ge_game_trans)
+      done
+  }
+  {
+    assume ab: "a \<le> b"
+    from ab show "c + a \<le> c + b"
+      apply (cases a, cases b, cases c)
+      apply (simp add: ge_plus_game_left[symmetric])
+      done
+  }
+qed
+
+end
diff -r 0b9eb4b0ad98 -r 778507520684 src/HOL/ZF/HOLZF.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ZF/HOLZF.thy	Tue Mar 07 16:03:31 2006 +0100
@@ -0,0 +1,917 @@
+(*  Title:      HOL/ZF/HOLZF.thy
+    ID:         $Id$
+    Author:     Steven Obua
+
+    Axiomatizes the ZFC universe as an HOL type.
+    See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan
+*)
+
+theory HOLZF 
+imports Helper
+begin
+
+typedecl ZF
+
+consts
+  Empty :: ZF
+  Elem :: "ZF \<Rightarrow> ZF \<Rightarrow> bool"
+  Sum :: "ZF \<Rightarrow> ZF"
+  Power :: "ZF \<Rightarrow> ZF"
+  Repl :: "ZF \<Rightarrow> (ZF \<Rightarrow> ZF) \<Rightarrow> ZF"
+  Inf :: ZF
+
+constdefs
+  Upair:: "ZF \<Rightarrow> ZF \<Rightarrow> ZF"
+  "Upair a b == Repl (Power (Power Empty)) (% x. if x = Empty then a else b)"
+  Singleton:: "ZF \<Rightarrow> ZF"
+  "Singleton x == Upair x x"
+  union :: "ZF \<Rightarrow> ZF \<Rightarrow> ZF"
+  "union A B == Sum (Upair A B)"
+  SucNat:: "ZF \<Rightarrow> ZF"
+  "SucNat x == union x (Singleton x)"
+  subset :: "ZF \<Rightarrow> ZF \<Rightarrow> bool"
+  "subset A B == ! x. Elem x A \<longrightarrow> Elem x B"
+
+finalconsts 
+  Empty Elem Sum Power Repl Inf
+
+axioms
+  Empty: "Not (Elem x Empty)"
+  Ext: "(x = y) = (! z. Elem z x = Elem z y)"
+  Sum: "Elem z (Sum x) = (? y. Elem z y & Elem y x)"
+  Power: "Elem y (Power x) = (subset y x)"
+  Repl: "Elem b (Repl A f) = (? a. Elem a A & b = f a)"
+  Regularity: "A \<noteq> Empty \<longrightarrow> (? x. Elem x A & (! y. Elem y x \<longrightarrow> Not (Elem y A)))"
+  Infinity: "Elem Empty Inf & (! x. Elem x Inf \<longrightarrow> Elem (SucNat x) Inf)"
+
+constdefs
+  Sep:: "ZF \<Rightarrow> (ZF \<Rightarrow> bool) \<Rightarrow> ZF"
+  "Sep A p == (if (!x. Elem x A \<longrightarrow> Not (p x)) then Empty else 
+  (let z = (\<some> x. Elem x A & p x) in
+   let f = % x. (if p x then x else z) in Repl A f))" 
+
+thm Power[unfolded subset_def]
+
+theorem Sep: "Elem b (Sep A p) = (Elem b A & p b)"
+  apply (auto simp add: Sep_def Empty)
+  apply (auto simp add: Let_def Repl)
+  apply (rule someI2, auto)+
+  done
+
+lemma subset_empty: "subset Empty A"
+  by (simp add: subset_def Empty)
+
+theorem Upair: "Elem x (Upair a b) = (x = a | x = b)"
+  apply (auto simp add: Upair_def Repl)
+  apply (rule exI[where x=Empty])
+  apply (simp add: Power subset_empty)
+  apply (rule exI[where x="Power Empty"])
+  apply (auto)
+  apply (auto simp add: Ext Power subset_def Empty)
+  apply (drule spec[where x=Empty], simp add: Empty)+
+  done
+
+lemma Singleton: "Elem x (Singleton y) = (x = y)"
+  by (simp add: Singleton_def Upair)
+
+constdefs 
+  Opair:: "ZF \<Rightarrow> ZF \<Rightarrow> ZF"
+  "Opair a b == Upair (Upair a a) (Upair a b)"
+
+lemma Upair_singleton: "(Upair a a = Upair c d) = (a = c & a = d)"
+  by (auto simp add: Ext[where x="Upair a a"] Upair)
+
+lemma Upair_fsteq: "(Upair a b = Upair a c) = ((a = b & a = c) | (b = c))"
+  by (auto simp add: Ext[where x="Upair a b"] Upair)
+
+lemma Upair_comm: "Upair a b = Upair b a"
+  by (auto simp add: Ext Upair)
+
+theorem Opair: "(Opair a b = Opair c d) = (a = c & b = d)"
+  proof -
+    have fst: "(Opair a b = Opair c d) \<Longrightarrow> a = c"
+      apply (simp add: Opair_def)
+      apply (simp add: Ext[where x="Upair (Upair a a) (Upair a b)"])
+      apply (drule spec[where x="Upair a a"])
+      apply (auto simp add: Upair Upair_singleton)
+      done
+    show ?thesis
+      apply (auto)
+      apply (erule fst)
+      apply (frule fst)
+      apply (auto simp add: Opair_def Upair_fsteq)
+      done
+  qed
+
+constdefs 
+  Replacement :: "ZF \<Rightarrow> (ZF \<Rightarrow> ZF option) \<Rightarrow> ZF"
+  "Replacement A f == Repl (Sep A (% a. f a \<noteq> None)) (the o f)"
+
+theorem Replacement: "Elem y (Replacement A f) = (? x. Elem x A & f x = Some y)"
+  by (auto simp add: Replacement_def Repl Sep) 
+
+constdefs
+  Fst :: "ZF \<Rightarrow> ZF"
+  "Fst q == SOME x. ? y. q = Opair x y"
+  Snd :: "ZF \<Rightarrow> ZF"
+  "Snd q == SOME y. ? x. q = Opair x y"
+
+theorem Fst: "Fst (Opair x y) = x"
+  apply (simp add: Fst_def)
+  apply (rule someI2)
+  apply (simp_all add: Opair)
+  done
+
+theorem Snd: "Snd (Opair x y) = y"
+  apply (simp add: Snd_def)
+  apply (rule someI2)
+  apply (simp_all add: Opair)
+  done
+
+constdefs 
+  isOpair :: "ZF \<Rightarrow> bool"
+  "isOpair q == ? x y. q = Opair x y"
+
+lemma isOpair: "isOpair (Opair x y) = True"
+  by (auto simp add: isOpair_def)
+
+lemma FstSnd: "isOpair x \<Longrightarrow> Opair (Fst x) (Snd x) = x"
+  by (auto simp add: isOpair_def Fst Snd)
+  
+constdefs
+  CartProd :: "ZF \<Rightarrow> ZF \<Rightarrow> ZF"
+  "CartProd A B == Sum(Repl A (% a. Repl B (% b. Opair a b)))"
+
+lemma CartProd: "Elem x (CartProd A B) = (? a b. Elem a A & Elem b B & x = (Opair a b))"
+  apply (auto simp add: CartProd_def Sum Repl)
+  apply (rule_tac x="Repl B (Opair a)" in exI)
+  apply (auto simp add: Repl)
+  done
+
+constdefs
+  explode :: "ZF \<Rightarrow> ZF set"
+  "explode z == { x. Elem x z }"
+
+lemma explode_Empty: "(explode x = {}) = (x = Empty)"
+  by (auto simp add: explode_def Ext Empty)
+
+lemma explode_Elem: "(x \<in> explode X) = (Elem x X)"
+  by (simp add: explode_def)
+
+lemma Elem_explode_in: "\<lbrakk> Elem a A; explode A \<subseteq> B\<rbrakk> \<Longrightarrow> a \<in> B"
+  by (auto simp add: explode_def)
+
+lemma explode_CartProd_eq: "explode (CartProd a b) = (% (x,y). Opair x y) ` ((explode a) \<times> (explode b))"
+  by (simp add: explode_def expand_set_eq CartProd image_def)
+
+lemma explode_Repl_eq: "explode (Repl A f) = image f (explode A)"
+  by (simp add: explode_def Repl image_def)
+
+constdefs
+  Domain :: "ZF \<Rightarrow> ZF"
+  "Domain f == Replacement f (% p. if isOpair p then Some (Fst p) else None)"
+  Range :: "ZF \<Rightarrow> ZF"
+  "Range f == Replacement f (% p. if isOpair p then Some (Snd p) else None)"
+
+theorem Domain: "Elem x (Domain f) = (? y. Elem (Opair x y) f)"
+  apply (auto simp add: Domain_def Replacement)
+  apply (rule_tac x="Snd x" in exI)
+  apply (simp add: FstSnd)
+  apply (rule_tac x="Opair x y" in exI)
+  apply (simp add: isOpair Fst)
+  done
+
+theorem Range: "Elem y (Range f) = (? x. Elem (Opair x y) f)"
+  apply (auto simp add: Range_def Replacement)
+  apply (rule_tac x="Fst x" in exI)
+  apply (simp add: FstSnd)
+  apply (rule_tac x="Opair x y" in exI)
+  apply (simp add: isOpair Snd)
+  done
+
+theorem union: "Elem x (union A B) = (Elem x A | Elem x B)"
+  by (auto simp add: union_def Sum Upair)
+
+constdefs
+  Field :: "ZF \<Rightarrow> ZF"
+  "Field A == union (Domain A) (Range A)"
+
+constdefs
+  "\<acute>"         :: "ZF \<Rightarrow> ZF => ZF"    (infixl 90) --{*function application*} 
+  app_def:  "f \<acute> x == (THE y. Elem (Opair x y) f)"
+
+constdefs
+  isFun :: "ZF \<Rightarrow> bool"
+  "isFun f == (! x y1 y2. Elem (Opair x y1) f & Elem (Opair x y2) f \<longrightarrow> y1 = y2)"
+
+constdefs
+  Lambda :: "ZF \<Rightarrow> (ZF \<Rightarrow> ZF) \<Rightarrow> ZF"
+  "Lambda A f == Repl A (% x. Opair x (f x))"
+
+lemma Lambda_app: "Elem x A \<Longrightarrow> (Lambda A f)\<acute>x = f x"
+  by (simp add: app_def Lambda_def Repl Opair)
+
+lemma isFun_Lambda: "isFun (Lambda A f)"
+  by (auto simp add: isFun_def Lambda_def Repl Opair)
+
+lemma domain_Lambda: "Domain (Lambda A f) = A"
+  apply (auto simp add: Domain_def)
+  apply (subst Ext)
+  apply (auto simp add: Replacement)
+  apply (simp add: Lambda_def Repl)
+  apply (auto simp add: Fst)
+  apply (simp add: Lambda_def Repl)
+  apply (rule_tac x="Opair z (f z)" in exI)
+  apply (auto simp add: Fst isOpair_def)
+  done
+
+lemma Lambda_ext: "(Lambda s f = Lambda t g) = (s = t & (! x. Elem x s \<longrightarrow> f x = g x))"
+proof -
+  have "Lambda s f = Lambda t g \<Longrightarrow> s = t"
+    apply (subst domain_Lambda[where A = s and f = f, symmetric])
+    apply (subst domain_Lambda[where A = t and f = g, symmetric])
+    apply auto
+    done
+  then show ?thesis
+    apply auto
+    apply (subst Lambda_app[where f=f, symmetric], simp)
+    apply (subst Lambda_app[where f=g, symmetric], simp)
+    apply auto
+    apply (auto simp add: Lambda_def Repl Ext)
+    apply (auto simp add: Ext[symmetric])
+    done
+qed
+
+constdefs 
+  PFun :: "ZF \<Rightarrow> ZF \<Rightarrow> ZF"
+  "PFun A B == Sep (Power (CartProd A B)) isFun"
+  Fun :: "ZF \<Rightarrow> ZF \<Rightarrow> ZF"
+  "Fun A B == Sep (PFun A B) (\<lambda> f. Domain f = A)"
+
+lemma Fun_Range: "Elem f (Fun U V) \<Longrightarrow> subset (Range f) V"
+  apply (simp add: Fun_def Sep PFun_def Power subset_def CartProd)
+  apply (auto simp add: Domain Range)
+  apply (erule_tac x="Opair xa x" in allE)
+  apply (auto simp add: Opair)
+  done
+
+lemma Elem_Elem_PFun: "Elem F (PFun U V) \<Longrightarrow> Elem p F \<Longrightarrow> isOpair p & Elem (Fst p) U & Elem (Snd p) V"
+  apply (simp add: PFun_def Sep Power subset_def, clarify)
+  apply (erule_tac x=p in allE)
+  apply (auto simp add: CartProd isOpair Fst Snd)
+  done
+
+lemma Fun_implies_PFun[simp]: "Elem f (Fun U V) \<Longrightarrow> Elem f (PFun U V)"
+  by (simp add: Fun_def Sep)
+
+lemma Elem_Elem_Fun: "Elem F (Fun U V) \<Longrightarrow> Elem p F \<Longrightarrow> isOpair p & Elem (Fst p) U & Elem (Snd p) V" 
+  by (auto simp add: Elem_Elem_PFun dest: Fun_implies_PFun)
+
+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"
+  apply (frule Elem_Elem_PFun[where p=x], simp)
+  apply (frule Elem_Elem_PFun[where p=y], simp)
+  apply (subgoal_tac "isFun F")
+  apply (simp add: isFun_def isOpair_def)  
+  apply (auto simp add: Fst Snd, blast)
+  apply (auto simp add: PFun_def Sep)
+  done
+
+ML {* simp_depth_limit := 2 *}
+lemma Fun_total: "\<lbrakk>Elem F (Fun U V); Elem a U\<rbrakk> \<Longrightarrow> \<exists>x. Elem (Opair a x) F"
+  by (auto simp add: Fun_def Sep Domain)
+ML {* simp_depth_limit := 1000 *}
+
+
+lemma unique_fun_value: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> ?! y. Elem (Opair x y) f"
+  by (auto simp add: Domain isFun_def)
+
+lemma fun_value_in_range: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> Elem (f\<acute>x) (Range f)"
+  apply (auto simp add: Range)
+  apply (drule unique_fun_value)
+  apply simp
+  apply (simp add: app_def)
+  apply (rule exI[where x=x])
+  apply (auto simp add: the_equality)
+  done
+
+lemma fun_range_witness: "\<lbrakk>isFun f; Elem y (Range f)\<rbrakk> \<Longrightarrow> ? x. Elem x (Domain f) & f\<acute>x = y"
+  apply (auto simp add: Range)
+  apply (rule_tac x="x" in exI)
+  apply (auto simp add: app_def the_equality isFun_def Domain)
+  done
+
+lemma Elem_Fun_Lambda: "Elem F (Fun U V) \<Longrightarrow> ? f. F = Lambda U f"
+  apply (rule exI[where x= "% x. (THE y. Elem (Opair x y) F)"])
+  apply (simp add: Ext Lambda_def Repl Domain)
+  apply (simp add: Ext[symmetric])
+  apply auto
+  apply (frule Elem_Elem_Fun)
+  apply auto
+  apply (rule_tac x="Fst z" in exI)
+  apply (simp add: isOpair_def)
+  apply (auto simp add: Fst Snd Opair)
+  apply (rule theI2')
+  apply auto
+  apply (drule Fun_implies_PFun)
+  apply (drule_tac x="Opair x ya" and y="Opair x yb" in PFun_inj)
+  apply (auto simp add: Fst Snd)
+  apply (drule Fun_implies_PFun)
+  apply (drule_tac x="Opair x y" and y="Opair x ya" in PFun_inj)
+  apply (auto simp add: Fst Snd)
+  apply (rule theI2')
+  apply (auto simp add: Fun_total)
+  apply (drule Fun_implies_PFun)
+  apply (drule_tac x="Opair a x" and y="Opair a y" in PFun_inj)
+  apply (auto simp add: Fst Snd)
+  done
+ 
+lemma Elem_Lambda_Fun: "Elem (Lambda A f) (Fun U V) = (A = U & (! x. Elem x A \<longrightarrow> Elem (f x) V))"
+proof -
+  have "Elem (Lambda A f) (Fun U V) \<Longrightarrow> A = U"
+    by (simp add: Fun_def Sep domain_Lambda)
+  then show ?thesis
+    apply auto
+    apply (drule Fun_Range)
+    apply (subgoal_tac "f x = ((Lambda U f) \<acute> x)")
+    prefer 2
+    apply (simp add: Lambda_app)
+    apply simp
+    apply (subgoal_tac "Elem (Lambda U f \<acute> x) (Range (Lambda U f))")
+    apply (simp add: subset_def)
+    apply (rule fun_value_in_range)
+    apply (simp_all add: isFun_Lambda domain_Lambda)
+    apply (simp add: Fun_def Sep PFun_def Power domain_Lambda isFun_Lambda)
+    apply (auto simp add: subset_def CartProd)
+    apply (rule_tac x="Fst x" in exI)
+    apply (auto simp add: Lambda_def Repl Fst)
+    done
+qed    
+
+
+constdefs
+  is_Elem_of :: "(ZF * ZF) set"
+  "is_Elem_of == { (a,b) | a b. Elem a b }"
+
+lemma cond_wf_Elem:
+  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"
+  shows "P a"
+proof -
+  {
+    fix P
+    fix U
+    fix a
+    assume P_induct: "(\<forall>x. (\<forall>y. Elem y x \<longrightarrow> Elem y U \<longrightarrow> P y) \<longrightarrow> (Elem x U \<longrightarrow> P x))"
+    assume a_in_U: "Elem a U"
+    have "P a"
+      proof -
+	term "P"
+	term Sep
+	let ?Z = "Sep U (Not o P)"
+	have "?Z = Empty \<longrightarrow> P a" by (simp add: Ext Sep Empty a_in_U)	
+	moreover have "?Z \<noteq> Empty \<longrightarrow> False"
+	  proof 
+	    assume not_empty: "?Z \<noteq> Empty" 
+	    note thereis_x = Regularity[where A="?Z", simplified not_empty, simplified]
+	    then obtain x where x_def: "Elem x ?Z & (! y. Elem y x \<longrightarrow> Not (Elem y ?Z))" ..
+            then have x_induct:"! y. Elem y x \<longrightarrow> Elem y U \<longrightarrow> P y" by (simp add: Sep)
+	    have "Elem x U \<longrightarrow> P x" 
+	      by (rule impE[OF spec[OF P_induct, where x=x], OF x_induct], assumption)
+	    moreover have "Elem x U & Not(P x)"
+	      apply (insert x_def)
+	      apply (simp add: Sep)
+	      done
+	    ultimately show "False" by auto
+	  qed
+	ultimately show "P a" by auto
+      qed
+  }
+  with hyps show ?thesis by blast
+qed    
+
+lemma cond2_wf_Elem:
+  assumes 
+     special_P: "? U. ! x. Not(Elem x U) \<longrightarrow> (P x)"
+     and P_induct: "\<forall>x. (\<forall>y. Elem y x \<longrightarrow> P y) \<longrightarrow> P x"
+  shows
+     "P a"
+proof -
+  have "? U Q. P = (\<lambda> x. (Elem x U \<longrightarrow> Q x))"
+  proof -
+    from special_P obtain U where U:"! x. Not(Elem x U) \<longrightarrow> (P x)" ..
+    show ?thesis
+      apply (rule_tac exI[where x=U])
+      apply (rule exI[where x="P"])
+      apply (rule ext)
+      apply (auto simp add: U)
+      done
+  qed    
+  then obtain U where "? Q. P = (\<lambda> x. (Elem x U \<longrightarrow> Q x))" ..
+  then obtain Q where UQ: "P = (\<lambda> x. (Elem x U \<longrightarrow> Q x))" ..
+  show ?thesis
+    apply (auto simp add: UQ)
+    apply (rule cond_wf_Elem)
+    apply (rule P_induct[simplified UQ])
+    apply simp
+    done
+qed
+
+consts
+  nat2Nat :: "nat \<Rightarrow> ZF"
+
+primrec
+nat2Nat_0[intro]:  "nat2Nat 0 = Empty"
+nat2Nat_Suc[intro]:  "nat2Nat (Suc n) = SucNat (nat2Nat n)"
+
+constdefs
+  Nat2nat :: "ZF \<Rightarrow> nat"
+  "Nat2nat == inv nat2Nat"
+
+lemma Elem_nat2Nat_inf[intro]: "Elem (nat2Nat n) Inf"
+  apply (induct n)
+  apply (simp_all add: Infinity)
+  done
+
+constdefs
+  Nat :: ZF
+  "Nat == Sep Inf (\<lambda> N. ? n. nat2Nat n = N)"
+
+lemma Elem_nat2Nat_Nat[intro]: "Elem (nat2Nat n) Nat"
+  by (auto simp add: Nat_def Sep)
+
+lemma Elem_Empty_Nat: "Elem Empty Nat"
+  by (auto simp add: Nat_def Sep Infinity)
+
+lemma Elem_SucNat_Nat: "Elem N Nat \<Longrightarrow> Elem (SucNat N) Nat"
+  by (auto simp add: Nat_def Sep Infinity)
+  
+lemma no_infinite_Elem_down_chain:
+  "Not (? f. isFun f & Domain f = Nat & (! N. Elem N Nat \<longrightarrow> Elem (f\<acute>(SucNat N)) (f\<acute>N)))"
+proof -
+  {
+    fix f
+    assume f:"isFun f & Domain f = Nat & (! N. Elem N Nat \<longrightarrow> Elem (f\<acute>(SucNat N)) (f\<acute>N))"
+    let ?r = "Range f"
+    have "?r \<noteq> Empty"
+      apply (auto simp add: Ext Empty)
+      apply (rule exI[where x="f\<acute>Empty"])
+      apply (rule fun_value_in_range)
+      apply (auto simp add: f Elem_Empty_Nat)
+      done
+    then have "? x. Elem x ?r & (! y. Elem y x \<longrightarrow> Not(Elem y ?r))"
+      by (simp add: Regularity)
+    then obtain x where x: "Elem x ?r & (! y. Elem y x \<longrightarrow> Not(Elem y ?r))" ..
+    then have "? N. Elem N (Domain f) & f\<acute>N = x" 
+      apply (rule_tac fun_range_witness)
+      apply (simp_all add: f)
+      done
+    then have "? N. Elem N Nat & f\<acute>N = x" 
+      by (simp add: f)
+    then obtain N where N: "Elem N Nat & f\<acute>N = x" ..
+    from N have N': "Elem N Nat" by auto
+    let ?y = "f\<acute>(SucNat N)"
+    have Elem_y_r: "Elem ?y ?r"
+      by (simp_all add: f Elem_SucNat_Nat N fun_value_in_range)
+    have "Elem ?y (f\<acute>N)" by (auto simp add: f N')
+    then have "Elem ?y x" by (simp add: N)
+    with x have "Not (Elem ?y ?r)" by auto
+    with Elem_y_r have "False" by auto
+  }
+  then show ?thesis by auto
+qed
+
+lemma Upair_nonEmpty: "Upair a b \<noteq> Empty"
+  by (auto simp add: Ext Empty Upair)  
+
+lemma Singleton_nonEmpty: "Singleton x \<noteq> Empty"
+  by (auto simp add: Singleton_def Upair_nonEmpty)
+
+lemma antisym_Elem: "Not(Elem a b & Elem b a)"
+proof -
+  {
+    fix a b
+    assume ab: "Elem a b"
+    assume ba: "Elem b a"
+    let ?Z = "Upair a b"
+    have "?Z \<noteq> Empty" by (simp add: Upair_nonEmpty)
+    then have "? x. Elem x ?Z & (! y. Elem y x \<longrightarrow> Not(Elem y ?Z))"
+      by (simp add: Regularity)
+    then obtain x where x:"Elem x ?Z & (! y. Elem y x \<longrightarrow> Not(Elem y ?Z))" ..
+    then have "x = a \<or> x = b" by (simp add: Upair)
+    moreover have "x = a \<longrightarrow> Not (Elem b ?Z)"
+      by (auto simp add: x ba)
+    moreover have "x = b \<longrightarrow> Not (Elem a ?Z)"
+      by (auto simp add: x ab)
+    ultimately have "False"
+      by (auto simp add: Upair)
+  }    
+  then show ?thesis by auto
+qed
+
+lemma irreflexiv_Elem: "Not(Elem a a)"
+  by (simp add: antisym_Elem[of a a, simplified])
+
+lemma antisym_Elem: "Elem a b \<Longrightarrow> Not (Elem b a)"
+  apply (insert antisym_Elem[of a b])
+  apply auto
+  done
+
+consts
+  NatInterval :: "nat \<Rightarrow> nat \<Rightarrow> ZF"
+
+primrec
+  "NatInterval n 0 = Singleton (nat2Nat n)"
+  "NatInterval n (Suc m) = union (NatInterval n m) (Singleton (nat2Nat (n+m+1)))"
+
+lemma n_Elem_NatInterval[rule_format]: "! q. q <= m \<longrightarrow> Elem (nat2Nat (n+q)) (NatInterval n m)"
+  apply (induct m)
+  apply (auto simp add: Singleton union)
+  apply (case_tac "q <= m")
+  apply auto
+  apply (subgoal_tac "q = Suc m")
+  apply auto
+  done
+
+lemma NatInterval_not_Empty: "NatInterval n m \<noteq> Empty"
+  by (auto intro:   n_Elem_NatInterval[where q = 0, simplified] simp add: Empty Ext)
+
+lemma increasing_nat2Nat[rule_format]: "0 < n \<longrightarrow> Elem (nat2Nat (n - 1)) (nat2Nat n)"
+  apply (case_tac "? m. n = Suc m")
+  apply (auto simp add: SucNat_def union Singleton)
+  apply (drule spec[where x="n - 1"])
+  apply arith
+  done
+
+lemma represent_NatInterval[rule_format]: "Elem x (NatInterval n m) \<longrightarrow> (? u. n \<le> u & u \<le> n+m & nat2Nat u = x)"
+  apply (induct m)
+  apply (auto simp add: Singleton union)
+  apply (rule_tac x="Suc (n+m)" in exI)
+  apply auto
+  done
+
+lemma inj_nat2Nat: "inj nat2Nat"
+proof -
+  {
+    fix n m :: nat
+    assume nm: "nat2Nat n = nat2Nat (n+m)"
+    assume mg0: "0 < m"
+    let ?Z = "NatInterval n m"
+    have "?Z \<noteq> Empty" by (simp add: NatInterval_not_Empty)
+    then have "? x. (Elem x ?Z) & (! y. Elem y x \<longrightarrow> Not (Elem y ?Z))" 
+      by (auto simp add: Regularity)
+    then obtain x where x:"Elem x ?Z & (! y. Elem y x \<longrightarrow> Not (Elem y ?Z))" ..
+    then have "? u. n \<le> u & u \<le> n+m & nat2Nat u = x" 
+      by (simp add: represent_NatInterval)
+    then obtain u where u: "n \<le> u & u \<le> n+m & nat2Nat u = x" ..
+    have "n < u \<longrightarrow> False"
+    proof 
+      assume n_less_u: "n < u"
+      let ?y = "nat2Nat (u - 1)"
+      have "Elem ?y (nat2Nat u)"
+	apply (rule increasing_nat2Nat)
+	apply (insert n_less_u)
+	apply arith
+	done
+      with u have "Elem ?y x" by auto
+      with x have "Not (Elem ?y ?Z)" by auto
+      moreover have "Elem ?y ?Z" 
+	apply (insert n_Elem_NatInterval[where q = "u - n - 1" and n=n and m=m])
+	apply (insert n_less_u)
+	apply (insert u)
+	apply auto
+	apply arith
+	done
+      ultimately show False by auto
+    qed
+    moreover have "u = n \<longrightarrow> False"
+    proof 
+      assume "u = n"
+      with u have "nat2Nat n = x" by auto
+      then have nm_eq_x: "nat2Nat (n+m) = x" by (simp add: nm)
+      let ?y = "nat2Nat (n+m - 1)"
+      have "Elem ?y (nat2Nat (n+m))"
+	apply (rule increasing_nat2Nat)
+	apply (insert mg0)
+	apply arith
+	done
+      with nm_eq_x have "Elem ?y x" by auto
+      with x have "Not (Elem ?y ?Z)" by auto
+      moreover have "Elem ?y ?Z" 
+	apply (insert n_Elem_NatInterval[where q = "m - 1" and n=n and m=m])
+	apply (insert mg0)
+	apply auto
+	done
+      ultimately show False by auto      
+    qed
+    ultimately have "False" using u by arith
+  }
+  note lemma_nat2Nat = this
+  show ?thesis
+    apply (auto simp add: inj_on_def)
+    apply (case_tac "x = y")
+    apply auto
+    apply (case_tac "x < y")
+    apply (case_tac "? m. y = x + m & 0 < m")
+    apply (auto intro: lemma_nat2Nat, arith)
+    apply (case_tac "y < x")
+    apply (case_tac "? m. x = y + m & 0 < m")
+    apply auto
+    apply (drule sym)
+    apply (auto intro: lemma_nat2Nat, arith)
+    done
+qed
+
+lemma Nat2nat_nat2Nat[simp]: "Nat2nat (nat2Nat n) = n"
+  by (simp add: Nat2nat_def inv_f_f[OF inj_nat2Nat])
+
+lemma nat2Nat_Nat2nat[simp]: "Elem n Nat \<Longrightarrow> nat2Nat (Nat2nat n) = n"
+  apply (simp add: Nat2nat_def)
+  apply (rule_tac f_inv_f)
+  apply (auto simp add: image_def Nat_def Sep)
+  done
+
+lemma Nat2nat_SucNat: "Elem N Nat \<Longrightarrow> Nat2nat (SucNat N) = Suc (Nat2nat N)"
+  apply (auto simp add: Nat_def Sep Nat2nat_def)
+  apply (auto simp add: inv_f_f[OF inj_nat2Nat])
+  apply (simp only: nat2Nat.simps[symmetric])
+  apply (simp only: inv_f_f[OF inj_nat2Nat])
+  done
+  
+
+(*lemma Elem_induct: "(\<And>x. \<forall>y. Elem y x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a"
+  by (erule wf_induct[OF wf_is_Elem_of, simplified is_Elem_of_def, simplified])*)
+
+lemma Elem_Opair_exists: "? z. Elem x z & Elem y z & Elem z (Opair x y)"
+  apply (rule exI[where x="Upair x y"])
+  by (simp add: Upair Opair_def)
+
+lemma UNIV_is_not_in_ZF: "UNIV \<noteq> explode R"
+proof
+  let ?Russell = "{ x. Not(Elem x x) }"
+  have "?Russell = UNIV" by (simp add: irreflexiv_Elem)
+  moreover assume "UNIV = explode R"
+  ultimately have russell: "?Russell = explode R" by simp
+  then show "False"
+  proof(cases "Elem R R")
+    case True     
+    then show ?thesis 
+      by (insert irreflexiv_Elem, auto)
+  next
+    case False
+    then have "R \<in> ?Russell" by auto
+    then have "Elem R R" by (simp add: russell explode_def)
+    with False show ?thesis by auto
+  qed
+qed
+
+constdefs 
+  SpecialR :: "(ZF * ZF) set"
+  "SpecialR \<equiv> { (x, y) . x \<noteq> Empty \<and> y = Empty}"
+
+lemma "wf SpecialR"
+  apply (subst wf_def)
+  apply (auto simp add: SpecialR_def)
+  done
+
+constdefs
+  Ext :: "('a * 'b) set \<Rightarrow> 'b \<Rightarrow> 'a set"
+  "Ext R y \<equiv> { x . (x, y) \<in> R }" 
+
+lemma Ext_Elem: "Ext is_Elem_of = explode"
+  by (auto intro: ext simp add: Ext_def is_Elem_of_def explode_def)
+
+lemma "Ext SpecialR Empty \<noteq> explode z"
+proof 
+  have "Ext SpecialR Empty = UNIV - {Empty}"
+    by (auto simp add: Ext_def SpecialR_def)
+  moreover assume "Ext SpecialR Empty = explode z"
+  ultimately have "UNIV = explode(union z (Singleton Empty)) "
+    by (auto simp add: explode_def union Singleton)
+  then show "False" by (simp add: UNIV_is_not_in_ZF)
+qed
+
+constdefs 
+  implode :: "ZF set \<Rightarrow> ZF"
+  "implode == inv explode"
+
+lemma inj_explode: "inj explode"
+  by (auto simp add: inj_on_def explode_def Ext)
+
+lemma implode_explode[simp]: "implode (explode x) = x"
+  by (simp add: implode_def inj_explode)
+
+constdefs
+  regular :: "(ZF * ZF) set \<Rightarrow> bool"
+  "regular R == ! A. A \<noteq> Empty \<longrightarrow> (? x. Elem x A & (! y. (y, x) \<in> R \<longrightarrow> Not (Elem y A)))"
+  implodeable_Ext :: "(ZF * ZF) set \<Rightarrow> bool"
+  "implodeable_Ext R == ! y. Ext R y \<in> range explode"
+  wfzf :: "(ZF * ZF) set \<Rightarrow> bool"
+  "wfzf R == regular R & implodeable_Ext R"
+
+lemma regular_Elem: "regular is_Elem_of"
+  by (simp add: regular_def is_Elem_of_def Regularity)
+
+lemma implodeable_Elem: "implodeable_Ext is_Elem_of"
+  by (auto simp add: implodeable_Ext_def image_def Ext_Elem)
+
+lemma wfzf_is_Elem_of: "wfzf is_Elem_of"
+  by (auto simp add: wfzf_def regular_Elem implodeable_Elem)
+
+constdefs
+  SeqSum :: "(nat \<Rightarrow> ZF) \<Rightarrow> ZF"
+  "SeqSum f == Sum (Repl Nat (f o Nat2nat))"
+
+lemma SeqSum: "Elem x (SeqSum f) = (? n. Elem x (f n))"
+  apply (auto simp add: SeqSum_def Sum Repl)
+  apply (rule_tac x = "f n" in exI)
+  apply auto
+  done
+
+constdefs
+  Ext_ZF :: "(ZF * ZF) set \<Rightarrow> ZF \<Rightarrow> ZF"
+  "Ext_ZF R s == implode (Ext R s)"
+
+lemma Elem_implode: "A \<in> range explode \<Longrightarrow> Elem x (implode A) = (x \<in> A)"
+  apply (auto)
+  apply (simp_all add: explode_def)
+  done
+
+lemma Elem_Ext_ZF: "implodeable_Ext R \<Longrightarrow> Elem x (Ext_ZF R s) = ((x,s) \<in> R)"
+  apply (simp add: Ext_ZF_def)
+  apply (subst Elem_implode)
+  apply (simp add: implodeable_Ext_def)
+  apply (simp add: Ext_def)
+  done
+
+consts
+  Ext_ZF_n :: "(ZF * ZF) set \<Rightarrow> ZF \<Rightarrow> nat \<Rightarrow> ZF"
+
+primrec
+  "Ext_ZF_n R s 0 = Ext_ZF R s"
+  "Ext_ZF_n R s (Suc n) = Sum (Repl (Ext_ZF_n R s n) (Ext_ZF R))"
+
+constdefs
+  Ext_ZF_hull :: "(ZF * ZF) set \<Rightarrow> ZF \<Rightarrow> ZF"
+  "Ext_ZF_hull R s == SeqSum (Ext_ZF_n R s)"
+
+lemma Elem_Ext_ZF_hull:
+  assumes implodeable_R: "implodeable_Ext R" 
+  shows "Elem x (Ext_ZF_hull R S) = (? n. Elem x (Ext_ZF_n R S n))"
+  by (simp add: Ext_ZF_hull_def SeqSum)
+  
+lemma Elem_Elem_Ext_ZF_hull:
+  assumes implodeable_R: "implodeable_Ext R" 
+          and x_hull: "Elem x (Ext_ZF_hull R S)"
+          and y_R_x: "(y, x) \<in> R"
+  shows "Elem y (Ext_ZF_hull R S)"
+proof -
+  from Elem_Ext_ZF_hull[OF implodeable_R] x_hull 
+  have "? n. Elem x (Ext_ZF_n R S n)" by auto
+  then obtain n where n:"Elem x (Ext_ZF_n R S n)" ..
+  with y_R_x have "Elem y (Ext_ZF_n R S (Suc n))"
+    apply (auto simp add: Repl Sum)
+    apply (rule_tac x="Ext_ZF R x" in exI) 
+    apply (auto simp add: Elem_Ext_ZF[OF implodeable_R])
+    done
+  with Elem_Ext_ZF_hull[OF implodeable_R, where x=y] show ?thesis
+    by (auto simp del: Ext_ZF_n.simps)
+qed
+
+lemma wfzf_minimal:
+  assumes hyps: "wfzf R" "C \<noteq> {}"
+  shows "\<exists>x. x \<in> C \<and> (\<forall>y. (y, x) \<in> R \<longrightarrow> y \<notin> C)"
+proof -
+  from hyps have "\<exists>S. S \<in> C" by auto
+  then obtain S where S:"S \<in> C" by auto  
+  let ?T = "Sep (Ext_ZF_hull R S) (\<lambda> s. s \<in> C)"
+  from hyps have implodeable_R: "implodeable_Ext R" by (simp add: wfzf_def)
+  show ?thesis
+  proof (cases "?T = Empty")
+    case True
+    then have "\<forall> z. \<not> (Elem z (Sep (Ext_ZF R S) (\<lambda> s. s \<in> C)))"      
+      apply (auto simp add: Ext Empty Sep Ext_ZF_hull_def SeqSum)
+      apply (erule_tac x="z" in allE, auto)
+      apply (erule_tac x=0 in allE, auto)
+      done
+    then show ?thesis 
+      apply (rule_tac exI[where x=S])
+      apply (auto simp add: Sep Empty S)
+      apply (erule_tac x=y in allE)
+      apply (simp add: implodeable_R Elem_Ext_ZF)
+      done
+  next
+    case False
+    from hyps have regular_R: "regular R" by (simp add: wfzf_def)
+    from 
+      regular_R[simplified regular_def, rule_format, OF False, simplified Sep] 
+      Elem_Elem_Ext_ZF_hull[OF implodeable_R]
+    show ?thesis by blast
+  qed
+qed
+
+lemma wfzf_implies_wf: "wfzf R \<Longrightarrow> wf R"
+proof (subst wf_def, rule allI)
+  assume wfzf: "wfzf R"
+  fix P :: "ZF \<Rightarrow> bool"
+  let ?C = "{x. P x}"
+  {
+    assume induct: "(\<forall>x. (\<forall>y. (y, x) \<in> R \<longrightarrow> P y) \<longrightarrow> P x)"
+    let ?C = "{x. \<not> (P x)}"
+    have "?C = {}"
+    proof (rule ccontr)
+      assume C: "?C \<noteq> {}"
+      from
+	wfzf_minimal[OF wfzf C]
+      obtain x where x: "x \<in> ?C \<and> (\<forall>y. (y, x) \<in> R \<longrightarrow> y \<notin> ?C)" ..
+      then have "P x"
+	apply (rule_tac induct[rule_format])
+	apply auto
+	done
+      with x show "False" by auto
+    qed
+    then have "! x. P x" by auto
+  }
+  then show "(\<forall>x. (\<forall>y. (y, x) \<in> R \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> (! x. P x)" by blast
+qed
+
+lemma wf_is_Elem_of: "wf is_Elem_of"
+  by (auto simp add: wfzf_is_Elem_of wfzf_implies_wf)
+
+lemma in_Ext_RTrans_implies_Elem_Ext_ZF_hull:  
+  "implodeable_Ext R \<Longrightarrow> x \<in> (Ext (R^+) s) \<Longrightarrow> Elem x (Ext_ZF_hull R s)"
+  apply (simp add: Ext_def Elem_Ext_ZF_hull)
+  apply (erule converse_trancl_induct[where r="R"])
+  apply (rule exI[where x=0])
+  apply (simp add: Elem_Ext_ZF)
+  apply auto
+  apply (rule_tac x="Suc n" in exI)
+  apply (simp add: Sum Repl)
+  apply (rule_tac x="Ext_ZF R z" in exI)
+  apply (auto simp add: Elem_Ext_ZF)
+  done
+
+lemma implodeable_Ext_trancl: "implodeable_Ext R \<Longrightarrow> implodeable_Ext (R^+)"
+  apply (subst implodeable_Ext_def)
+  apply (auto simp add: image_def)
+  apply (rule_tac x="Sep (Ext_ZF_hull R y) (\<lambda> z. z \<in> (Ext (R^+) y))" in exI)
+  apply (auto simp add: explode_def Sep set_ext 
+    in_Ext_RTrans_implies_Elem_Ext_ZF_hull)
+  done
+ 
+lemma Elem_Ext_ZF_hull_implies_in_Ext_RTrans[rule_format]:
+  "implodeable_Ext R \<Longrightarrow> ! x. Elem x (Ext_ZF_n R s n) \<longrightarrow> x \<in> (Ext (R^+) s)"
+  apply (induct_tac n)
+  apply (auto simp add: Elem_Ext_ZF Ext_def Sum Repl)
+  done
+
+lemma "implodeable_Ext R \<Longrightarrow> Ext_ZF (R^+) s = Ext_ZF_hull R s"
+  apply (frule implodeable_Ext_trancl)
+  apply (auto simp add: Ext)
+  apply (erule in_Ext_RTrans_implies_Elem_Ext_ZF_hull)
+  apply (simp add: Elem_Ext_ZF Ext_def)
+  apply (auto simp add: Elem_Ext_ZF Elem_Ext_ZF_hull)
+  apply (erule Elem_Ext_ZF_hull_implies_in_Ext_RTrans[simplified Ext_def, simplified], assumption)
+  done
+
+lemma wf_implies_regular: "wf R \<Longrightarrow> regular R"
+proof (simp add: regular_def, rule allI)
+  assume wf: "wf R"
+  fix A
+  show "A \<noteq> Empty \<longrightarrow> (\<exists>x. Elem x A \<and> (\<forall>y. (y, x) \<in> R \<longrightarrow> \<not> Elem y A))"
+  proof
+    assume A: "A \<noteq> Empty"
+    then have "? x. x \<in> explode A" 
+      by (auto simp add: explode_def Ext Empty)
+    then obtain x where x:"x \<in> explode A" ..   
+    from iffD1[OF wf_eq_minimal wf, rule_format, where Q="explode A", OF x]
+    obtain z where "z \<in> explode A \<and> (\<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> explode A)" by auto    
+    then show "\<exists>x. Elem x A \<and> (\<forall>y. (y, x) \<in> R \<longrightarrow> \<not> Elem y A)"      
+      apply (rule_tac exI[where x = z])
+      apply (simp add: explode_def)
+      done
+  qed
+qed
+
+lemma wf_eq_wfzf: "(wf R \<and> implodeable_Ext R) = wfzf R"
+  apply (auto simp add: wfzf_implies_wf)
+  apply (auto simp add: wfzf_def wf_implies_regular)
+  done
+
+lemma wfzf_trancl: "wfzf R \<Longrightarrow> wfzf (R^+)"
+  by (auto simp add: wf_eq_wfzf[symmetric] implodeable_Ext_trancl wf_trancl)
+
+lemma Ext_subset_mono: "R \<subseteq> S \<Longrightarrow> Ext R y \<subseteq> Ext S y"
+  by (auto simp add: Ext_def)
+
+lemma implodeable_Ext_subset: "implodeable_Ext R \<Longrightarrow> S \<subseteq> R \<Longrightarrow> implodeable_Ext S"
+  apply (auto simp add: implodeable_Ext_def)
+  apply (erule_tac x=y in allE)
+  apply (drule_tac y=y in Ext_subset_mono)
+  apply (auto simp add: image_def)
+  apply (rule_tac x="Sep x (% z. z \<in> (Ext S y))" in exI) 
+  apply (auto simp add: explode_def Sep)
+  done
+
+lemma wfzf_subset: "wfzf S \<Longrightarrow> R \<subseteq> S \<Longrightarrow> wfzf R"
+  by (auto intro: implodeable_Ext_subset wf_subset simp add: wf_eq_wfzf[symmetric])  
+
+end
diff -r 0b9eb4b0ad98 -r 778507520684 src/HOL/ZF/Helper.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ZF/Helper.thy	Tue Mar 07 16:03:31 2006 +0100
@@ -0,0 +1,32 @@
+(*  Title:      HOL/ZF/Helper.thy
+    ID:         $Id$
+    Author:     Steven Obua
+
+    Some helpful lemmas that probably will end up elsewhere. 
+*)
+
+theory Helper 
+imports Main
+begin
+
+lemma theI2' : "?! x. P x \<Longrightarrow> (!! x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (THE x. P x)"
+  apply auto
+  apply (subgoal_tac "P (THE x. P x)")
+  apply blast
+  apply (rule theI)
+  apply auto
+  done
+
+lemma in_range_superfluous: "(z \<in> range f & z \<in> (f ` x)) = (z \<in> f ` x)" 
+  by auto
+
+lemma f_x_in_range_f: "f x \<in> range f"
+  by (blast intro: image_eqI)
+
+lemma comp_inj: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (g o f)"
+  by (blast intro: comp_inj_on subset_inj_on)
+
+lemma comp_image_eq: "(g o f) ` x = g ` f ` x"
+  by auto
+  
+end
\ No newline at end of file
diff -r 0b9eb4b0ad98 -r 778507520684 src/HOL/ZF/LProd.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ZF/LProd.thy	Tue Mar 07 16:03:31 2006 +0100
@@ -0,0 +1,189 @@
+(*  Title:      HOL/ZF/LProd.thy
+    ID:         $Id$
+    Author:     Steven Obua
+
+    Introduces the lprod relation.
+    See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan
+*)
+
+theory LProd 
+imports Multiset
+begin
+
+consts
+  lprod :: "('a * 'a) set \<Rightarrow> ('a list * 'a list) set"
+
+inductive "lprod R"
+intros
+  lprod_single[intro!]: "(a, b) \<in> R \<Longrightarrow> ([a], [b]) \<in> lprod R"
+  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"
+
+lemma "(as,bs) \<in> lprod R \<Longrightarrow> length as = length bs"
+  apply (induct as bs rule: lprod.induct)
+  apply auto
+  done
+
+lemma "(as, bs) \<in> lprod R \<Longrightarrow> 1 \<le> length as \<and> 1 \<le> length bs"
+  apply (induct as bs rule: lprod.induct)
+  apply auto
+  done
+
+lemma lprod_subset_elem: "(as, bs) \<in> lprod S \<Longrightarrow> S \<subseteq> R \<Longrightarrow> (as, bs) \<in> lprod R"
+  apply (induct as bs rule: lprod.induct)
+  apply (auto)
+  done
+
+lemma lprod_subset: "S \<subseteq> R \<Longrightarrow> lprod S \<subseteq> lprod R"
+  by (auto intro: lprod_subset_elem)
+
+lemma lprod_implies_mult: "(as, bs) \<in> lprod R \<Longrightarrow> trans R \<Longrightarrow> (multiset_of as, multiset_of bs) \<in> mult R"
+proof (induct as bs rule: lprod.induct)
+  case (lprod_single a b)
+  note step = one_step_implies_mult[
+    where r=R and I="{#}" and K="{#a#}" and J="{#b#}", simplified]    
+  show ?case by (auto intro: lprod_single step)
+next
+  case (lprod_list a ah at b bh bt) 
+  from prems have transR: "trans R" by auto
+  have as: "multiset_of (ah @ a # at) = multiset_of (ah @ at) + {#a#}" (is "_ = ?ma + _")
+    by (simp add: ring_eq_simps)
+  have bs: "multiset_of (bh @ b # bt) = multiset_of (bh @ bt) + {#b#}" (is "_ = ?mb + _")
+    by (simp add: ring_eq_simps)
+  from prems have "(?ma, ?mb) \<in> mult R"
+    by auto
+  with mult_implies_one_step[OF transR] have 
+    "\<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)"
+    by blast
+  then obtain I J K where 
+    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)"
+    by blast   
+  show ?case
+  proof (cases "a = b")
+    case True    
+    have "((I + {#b#}) + K, (I + {#b#}) + J) \<in> mult R"
+      apply (rule one_step_implies_mult[OF transR])
+      apply (auto simp add: decomposed)
+      done
+    then show ?thesis
+      apply (simp only: as bs)
+      apply (simp only: decomposed True)
+      apply (simp add: ring_eq_simps)
+      done
+  next
+    case False
+    from False lprod_list have False: "(a, b) \<in> R" by blast
+    have "(I + (K + {#a#}), I + (J + {#b#})) \<in> mult R"
+      apply (rule one_step_implies_mult[OF transR])
+      apply (auto simp add: False decomposed)
+      done
+    then show ?thesis
+      apply (simp only: as bs)
+      apply (simp only: decomposed)
+      apply (simp add: ring_eq_simps)
+      done
+  qed
+qed
+
+lemma wf_lprod[recdef_wf,simp,intro]:
+  assumes wf_R: "wf R"
+  shows "wf (lprod R)"
+proof -
+  have subset: "lprod (R^+) \<subseteq> inv_image (mult (R^+)) multiset_of"
+    by (auto simp add: inv_image_def lprod_implies_mult trans_trancl)
+  note lprodtrancl = wf_subset[OF wf_inv_image[where r="mult (R^+)" and f="multiset_of", 
+    OF wf_mult[OF wf_trancl[OF wf_R]]], OF subset]
+  note lprod = wf_subset[OF lprodtrancl, where p="lprod R", OF lprod_subset, simplified]
+  show ?thesis by (auto intro: lprod)
+qed
+
+constdefs
+  gprod_2_2 :: "('a * 'a) set \<Rightarrow> (('a * 'a) * ('a * 'a)) set"
+  "gprod_2_2 R \<equiv> { ((a,b), (c,d)) . (a = c \<and> (b,d) \<in> R) \<or> (b = d \<and> (a,c) \<in> R) }"
+  gprod_2_1 :: "('a * 'a) set \<Rightarrow> (('a * 'a) * ('a * 'a)) set"
+  "gprod_2_1 R \<equiv>  { ((a,b), (c,d)) . (a = d \<and> (b,c) \<in> R) \<or> (b = c \<and> (a,d) \<in> R) }"
+
+lemma lprod_2_3: "(a, b) \<in> R \<Longrightarrow> ([a, c], [b, c]) \<in> lprod R"
+  by (auto intro: lprod_list[where a=c and b=c and 
+    ah = "[a]" and at = "[]" and bh="[b]" and bt="[]", simplified]) 
+
+lemma lprod_2_4: "(a, b) \<in> R \<Longrightarrow> ([c, a], [c, b]) \<in> lprod R"
+  by (auto intro: lprod_list[where a=c and b=c and 
+    ah = "[]" and at = "[a]" and bh="[]" and bt="[b]", simplified])
+
+lemma lprod_2_1: "(a, b) \<in> R \<Longrightarrow> ([c, a], [b, c]) \<in> lprod R"
+  by (auto intro: lprod_list[where a=c and b=c and 
+    ah = "[]" and at = "[a]" and bh="[b]" and bt="[]", simplified]) 
+
+lemma lprod_2_2: "(a, b) \<in> R \<Longrightarrow> ([a, c], [c, b]) \<in> lprod R"
+  by (auto intro: lprod_list[where a=c and b=c and 
+    ah = "[a]" and at = "[]" and bh="[]" and bt="[b]", simplified])
+
+lemma [recdef_wf, simp, intro]: 
+  assumes wfR: "wf R" shows "wf (gprod_2_1 R)"
+proof -
+  have "gprod_2_1 R \<subseteq> inv_image (lprod R) (\<lambda> (a,b). [a,b])"
+    by (auto simp add: inv_image_def gprod_2_1_def lprod_2_1 lprod_2_2)
+  with wfR show ?thesis
+    by (rule_tac wf_subset, auto)
+qed
+
+lemma [recdef_wf, simp, intro]: 
+  assumes wfR: "wf R" shows "wf (gprod_2_2 R)"
+proof -
+  have "gprod_2_2 R \<subseteq> inv_image (lprod R) (\<lambda> (a,b). [a,b])"
+    by (auto simp add: inv_image_def gprod_2_2_def lprod_2_3 lprod_2_4)
+  with wfR show ?thesis
+    by (rule_tac wf_subset, auto)
+qed
+
+lemma lprod_3_1: assumes "(x', x) \<in> R" shows "([y, z, x'], [x, y, z]) \<in> lprod R"
+  apply (rule lprod_list[where a="y" and b="y" and ah="[]" and at="[z,x']" and bh="[x]" and bt="[z]", simplified])
+  apply (auto simp add: lprod_2_1 prems)
+  done
+
+lemma lprod_3_2: assumes "(z',z) \<in> R" shows "([z', x, y], [x,y,z]) \<in> lprod R"
+  apply (rule lprod_list[where a="y" and b="y" and ah="[z',x]" and at="[]" and bh="[x]" and bt="[z]", simplified])
+  apply (auto simp add: lprod_2_2 prems)
+  done
+
+lemma lprod_3_3: assumes xr: "(xr, x) \<in> R" shows "([xr, y, z], [x, y, z]) \<in> lprod R"
+  apply (rule lprod_list[where a="y" and b="y" and ah="[xr]" and at="[z]" and bh="[x]" and bt="[z]", simplified])
+  apply (simp add: xr lprod_2_3)
+  done
+
+lemma lprod_3_4: assumes yr: "(yr, y) \<in> R" shows "([x, yr, z], [x, y, z]) \<in> lprod R"
+  apply (rule lprod_list[where a="x" and b="x" and ah="[]" and at="[yr,z]" and bh="[]" and bt="[y,z]", simplified])
+  apply (simp add: yr lprod_2_3)
+  done
+
+lemma lprod_3_5: assumes zr: "(zr, z) \<in> R" shows "([x, y, zr], [x, y, z]) \<in> lprod R"
+  apply (rule lprod_list[where a="x" and b="x" and ah="[]" and at="[y,zr]" and bh="[]" and bt="[y,z]", simplified])
+  apply (simp add: zr lprod_2_4)
+  done
+
+lemma lprod_3_6: assumes y': "(y', y) \<in> R" shows "([x, z, y'], [x, y, z]) \<in> lprod R"
+  apply (rule lprod_list[where a="z" and b="z" and ah="[x]" and at="[y']" and bh="[x,y]" and bt="[]", simplified])
+  apply (simp add: y' lprod_2_4)
+  done
+
+lemma lprod_3_7: assumes z': "(z',z) \<in> R" shows "([x, z', y], [x, y, z]) \<in> lprod R"
+  apply (rule lprod_list[where a="y" and b="y" and ah="[x, z']" and at="[]" and bh="[x]" and bt="[z]", simplified])
+  apply (simp add: z' lprod_2_4)
+  done
+
+constdefs
+   perm :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> bool"
+   "perm f A \<equiv> inj_on f A \<and> f ` A = A"
+
+lemma "((as,bs) \<in> lprod R) = 
+  (\<exists> f. perm f {0 ..< (length as)} \<and> 
+  (\<forall> j. j < length as \<longrightarrow> ((nth as j, nth bs (f j)) \<in> R \<or> (nth as j = nth bs (f j)))) \<and> 
+  (\<exists> i. i < length as \<and> (nth as i, nth bs (f i)) \<in> R))"
+oops
+
+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" 
+oops
+
+
+
+end
\ No newline at end of file
diff -r 0b9eb4b0ad98 -r 778507520684 src/HOL/ZF/MainZF.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ZF/MainZF.thy	Tue Mar 07 16:03:31 2006 +0100
@@ -0,0 +1,12 @@
+(*  Title:      HOL/ZF/MainZF.thy
+    ID:         $Id$
+    Author:     Steven Obua
+
+    Starting point for using HOLZF.
+    See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan
+*)
+
+theory MainZF
+imports Zet LProd
+begin
+end
\ No newline at end of file
diff -r 0b9eb4b0ad98 -r 778507520684 src/HOL/ZF/Zet.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ZF/Zet.thy	Tue Mar 07 16:03:31 2006 +0100
@@ -0,0 +1,221 @@
+(*  Title:      HOL/ZF/Zet.thy
+    ID:         $Id$
+    Author:     Steven Obua
+
+    Introduces a type 'a zet of ZF representable sets.
+    See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan
+*)
+
+theory Zet 
+imports HOLZF
+begin
+
+typedef 'a zet = "{A :: 'a set | A f z. inj_on f A \<and> f ` A \<subseteq> explode z}"
+  by blast
+
+constdefs
+  zin :: "'a \<Rightarrow> 'a zet \<Rightarrow> bool"
+  "zin x A == x \<in> (Rep_zet A)"
+
+lemma zet_ext_eq: "(A = B) = (! x. zin x A = zin x B)"
+  by (auto simp add: Rep_zet_inject[symmetric] zin_def)
+
+constdefs
+  zimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a zet \<Rightarrow> 'b zet"
+  "zimage f A == Abs_zet (image f (Rep_zet A))"
+
+lemma zet_def': "zet = {A :: 'a set | A f z. inj_on f A \<and> f ` A = explode z}"
+  apply (rule set_ext)
+  apply (auto simp add: zet_def)
+  apply (rule_tac x=f in exI)
+  apply auto
+  apply (rule_tac x="Sep z (\<lambda> y. y \<in> (f ` x))" in exI)
+  apply (auto simp add: explode_def Sep)
+  done
+
+lemma image_Inv_f_f: "inj_on f B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (Inv B f) ` f ` A = A"
+  apply (rule set_ext)
+  apply (auto simp add: Inv_f_f image_def)
+  apply (rule_tac x="f x" in exI)
+  apply (auto simp add: Inv_f_f)
+  done
+  
+lemma image_zet_rep: "A \<in> zet \<Longrightarrow> ? z . g ` A = explode z"
+  apply (auto simp add: zet_def')
+  apply (rule_tac x="Repl z (g o (Inv A f))" in exI)
+  apply (simp add: explode_Repl_eq)
+  apply (subgoal_tac "explode z = f ` A")
+  apply (simp_all add: comp_image_eq image_Inv_f_f)  
+  done
+
+lemma Inv_f_f_mem:       
+  assumes "x \<in> A"
+  shows "Inv A g (g x) \<in> A"
+  apply (simp add: Inv_def)
+  apply (rule someI2)
+  apply (auto!)
+  done
+
+lemma zet_image_mem:
+  assumes Azet: "A \<in> zet"
+  shows "g ` A \<in> zet"
+proof -
+  from Azet have "? (f :: _ \<Rightarrow> ZF). inj_on f A" 
+    by (auto simp add: zet_def')
+  then obtain f where injf: "inj_on (f :: _ \<Rightarrow> ZF) A"  
+    by auto
+  let ?w = "f o (Inv A g)"
+  have subset: "(Inv A g) ` (g ` A) \<subseteq> A"
+    by (auto simp add: Inv_f_f_mem)
+  have "inj_on (Inv A g) (g ` A)" by (simp add: inj_on_Inv)
+  then have injw: "inj_on ?w (g ` A)"
+    apply (rule comp_inj_on)
+    apply (rule subset_inj_on[where B=A])
+    apply (auto simp add: subset injf)
+    done
+  show ?thesis
+    apply (simp add: zet_def' comp_image_eq[symmetric])
+    apply (rule exI[where x="?w"])
+    apply (simp add: injw image_zet_rep Azet)
+    done
+qed
+
+lemma Rep_zimage_eq: "Rep_zet (zimage f A) = image f (Rep_zet A)"
+  apply (simp add: zimage_def)
+  apply (subst Abs_zet_inverse)
+  apply (simp_all add: Rep_zet zet_image_mem)
+  done
+
+lemma zimage_iff: "zin y (zimage f A) = (? x. zin x A & y = f x)"
+  by (auto simp add: zin_def Rep_zimage_eq)
+
+constdefs
+  zimplode :: "ZF zet \<Rightarrow> ZF"
+  "zimplode A == implode (Rep_zet A)"
+  zexplode :: "ZF \<Rightarrow> ZF zet"
+  "zexplode z == Abs_zet (explode z)"
+
+lemma Rep_zet_eq_explode: "? z. Rep_zet A = explode z"
+  by (rule image_zet_rep[where g="\<lambda> x. x",OF Rep_zet, simplified])
+
+lemma zexplode_zimplode: "zexplode (zimplode A) = A"
+  apply (simp add: zimplode_def zexplode_def)
+  apply (simp add: implode_def)
+  apply (subst f_inv_f[where y="Rep_zet A"])
+  apply (auto simp add: Rep_zet_inverse Rep_zet_eq_explode image_def)
+  done
+
+lemma explode_mem_zet: "explode z \<in> zet"
+  apply (simp add: zet_def')
+  apply (rule_tac x="% x. x" in exI)
+  apply (auto simp add: inj_on_def)
+  done
+
+lemma zimplode_zexplode: "zimplode (zexplode z) = z"
+  apply (simp add: zimplode_def zexplode_def)
+  apply (subst Abs_zet_inverse)
+  apply (auto simp add: explode_mem_zet implode_explode)
+  done  
+
+lemma zin_zexplode_eq: "zin x (zexplode A) = Elem x A"
+  apply (simp add: zin_def zexplode_def)
+  apply (subst Abs_zet_inverse)
+  apply (simp_all add: explode_Elem explode_mem_zet) 
+  done
+
+lemma comp_zimage_eq: "zimage g (zimage f A) = zimage (g o f) A"
+  apply (simp add: zimage_def)
+  apply (subst Abs_zet_inverse)
+  apply (simp_all add: comp_image_eq zet_image_mem Rep_zet)
+  done
+    
+constdefs
+  zunion :: "'a zet \<Rightarrow> 'a zet \<Rightarrow> 'a zet"
+  "zunion a b \<equiv> Abs_zet ((Rep_zet a) \<union> (Rep_zet b))"
+  zsubset :: "'a zet \<Rightarrow> 'a zet \<Rightarrow> bool"
+  "zsubset a b \<equiv> ! x. zin x a \<longrightarrow> zin x b"
+
+lemma explode_union: "explode (union a b) = (explode a) \<union> (explode b)"
+  apply (rule set_ext)
+  apply (simp add: explode_def union)
+  done
+
+lemma Rep_zet_zunion: "Rep_zet (zunion a b) = (Rep_zet a) \<union> (Rep_zet b)"
+proof -
+  from Rep_zet[of a] have "? f z. inj_on f (Rep_zet a) \<and> f ` (Rep_zet a) = explode z"
+    by (auto simp add: zet_def')
+  then obtain fa za where a:"inj_on fa (Rep_zet a) \<and> fa ` (Rep_zet a) = explode za"
+    by blast
+  from a have fa: "inj_on fa (Rep_zet a)" by blast
+  from a have za: "fa ` (Rep_zet a) = explode za" by blast
+  from Rep_zet[of b] have "? f z. inj_on f (Rep_zet b) \<and> f ` (Rep_zet b) = explode z"
+    by (auto simp add: zet_def')
+  then obtain fb zb where b:"inj_on fb (Rep_zet b) \<and> fb ` (Rep_zet b) = explode zb"
+    by blast
+  from b have fb: "inj_on fb (Rep_zet b)" by blast
+  from b have zb: "fb ` (Rep_zet b) = explode zb" by blast 
+  let ?f = "(\<lambda> x. if x \<in> (Rep_zet a) then Opair (fa x) (Empty) else Opair (fb x) (Singleton Empty))" 
+  let ?z = "CartProd (union za zb) (Upair Empty (Singleton Empty))"
+  have se: "Singleton Empty \<noteq> Empty"
+    apply (auto simp add: Ext Singleton)
+    apply (rule exI[where x=Empty])
+    apply (simp add: Empty)
+    done
+  show ?thesis
+    apply (simp add: zunion_def)
+    apply (subst Abs_zet_inverse)
+    apply (auto simp add: zet_def)
+    apply (rule exI[where x = ?f])
+    apply (rule conjI)
+    apply (auto simp add: inj_on_def Opair inj_onD[OF fa] inj_onD[OF fb] se se[symmetric])
+    apply (rule exI[where x = ?z])
+    apply (insert za zb)
+    apply (auto simp add: explode_def CartProd union Upair Opair)
+    done
+qed
+
+lemma zunion: "zin x (zunion a b) = ((zin x a) \<or> (zin x b))"
+  by (auto simp add: zin_def Rep_zet_zunion)
+
+lemma zimage_zexplode_eq: "zimage f (zexplode z) = zexplode (Repl z f)"
+  by (simp add: zet_ext_eq zin_zexplode_eq Repl zimage_iff)
+
+lemma range_explode_eq_zet: "range explode = zet"
+  apply (rule set_ext)
+  apply (auto simp add: explode_mem_zet)
+  apply (drule image_zet_rep)
+  apply (simp add: image_def)
+  apply auto
+  apply (rule_tac x=z in exI)
+  apply auto
+  done
+
+lemma Elem_zimplode: "(Elem x (zimplode z)) = (zin x z)"
+  apply (simp add: zimplode_def)
+  apply (subst Elem_implode)
+  apply (simp_all add: zin_def Rep_zet range_explode_eq_zet)
+  done
+
+constdefs
+  zempty :: "'a zet"
+  "zempty \<equiv> Abs_zet {}"
+
+lemma zempty[simp]: "\<not> (zin x zempty)"
+  by (auto simp add: zin_def zempty_def Abs_zet_inverse zet_def)
+
+lemma zimage_zempty[simp]: "zimage f zempty = zempty"
+  by (auto simp add: zet_ext_eq zimage_iff)
+
+lemma zunion_zempty_left[simp]: "zunion zempty a = a"
+  by (simp add: zet_ext_eq zunion)
+
+lemma zunion_zempty_right[simp]: "zunion a zempty = a"
+  by (simp add: zet_ext_eq zunion)
+
+lemma zimage_id[simp]: "zimage id A = A"
+  by (simp add: zet_ext_eq zimage_iff)
+
+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"
+  by (auto simp add: zet_ext_eq zimage_iff)
+
+end
diff -r 0b9eb4b0ad98 -r 778507520684 src/HOL/ZF/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ZF/document/root.tex	Tue Mar 07 16:03:31 2006 +0100
@@ -0,0 +1,28 @@
+
+% $Id$
+
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym}
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+\newcommand{\ganz}{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}
+
+\begin{document}
+
+\title{ZF}
+\author{Steven Obua}
+\maketitle
+
+%\tableofcontents
+
+\parindent 0pt\parskip 0.5ex
+
+\input{session}
+
+\end{document}