# HG changeset patch
# User paulson
# Date 1024480081 -7200
# Node ID 45be08fbdcff364d0ca753e7ff42be2b88b12369
# Parent  74d9144c452c607b3c4b9256255e5a58245762bb
new theory of inner models

diff -r 74d9144c452c -r 45be08fbdcff src/ZF/Constructible/Formula.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/Formula.thy	Wed Jun 19 11:48:01 2002 +0200
@@ -0,0 +1,1006 @@
+header {* First-Order Formulas and the Definition of the Class L *}
+
+theory Formula = Main:
+
+
+(*??for Bool.thy**)
+constdefs bool_of_o :: "o=>i"
+   "bool_of_o(P) == (if P then 1 else 0)"
+
+lemma [simp]: "bool_of_o(True) = 1"
+by (simp add: bool_of_o_def) 
+
+lemma [simp]: "bool_of_o(False) = 0"
+by (simp add: bool_of_o_def) 
+
+lemma [simp,TC]: "bool_of_o(P) \<in> bool"
+by (simp add: bool_of_o_def) 
+
+lemma [simp]: "(bool_of_o(P) = 1) <-> P"
+by (simp add: bool_of_o_def) 
+
+lemma [simp]: "(bool_of_o(P) = 0) <-> ~P"
+by (simp add: bool_of_o_def) 
+
+(*????????????????Cardinal.ML*)
+lemma Finite_cons_iff [iff]:  "Finite(cons(y,x)) <-> Finite(x)"
+by (blast intro: Finite_cons subset_Finite)
+
+lemma Finite_succ_iff [iff]:  "Finite(succ(x)) <-> Finite(x)"
+by (simp add: succ_def)
+
+declare Finite_0 [simp]
+
+lemma Finite_RepFun: "Finite(A) ==> Finite(RepFun(A,f))"
+by (erule Finite_induct, simp_all)
+
+lemma Finite_RepFun_lemma [rule_format]:
+     "[|Finite(x); !!x y. f(x)=f(y) ==> x=y|] 
+      ==> \<forall>A. x = RepFun(A,f) --> Finite(A)" 
+apply (erule Finite_induct)
+ apply clarify 
+ apply (case_tac "A=0", simp)
+ apply (blast del: allE, clarify) 
+apply (subgoal_tac "\<exists>z\<in>A. x = f(z)") 
+ prefer 2 apply (blast del: allE elim: equalityE, clarify) 
+apply (subgoal_tac "B = {f(u) . u \<in> A - {z}}")
+ apply (blast intro: Diff_sing_Finite) 
+apply (thin_tac "\<forall>A. ?P(A) --> Finite(A)") 
+apply (rule equalityI) 
+ apply (blast intro: elim: equalityE) 
+apply (blast intro: elim: equalityCE) 
+done
+
+text{*I don't know why, but if the premise is expressed using meta-connectives
+then  the simplifier cannot prove it automatically in conditional rewriting.*}
+lemma Finite_RepFun_iff:
+     "(\<forall>x y. f(x)=f(y) --> x=y) ==> Finite(RepFun(A,f)) <-> Finite(A)"
+by (blast intro: Finite_RepFun Finite_RepFun_lemma [of _ f]) 
+
+lemma Finite_Pow: "Finite(A) ==> Finite(Pow(A))"
+apply (erule Finite_induct) 
+apply (simp_all add: Pow_insert Finite_Un Finite_RepFun) 
+done
+
+lemma Finite_Pow_imp_Finite: "Finite(Pow(A)) ==> Finite(A)"
+apply (subgoal_tac "Finite({{x} . x \<in> A})")
+ apply (simp add: Finite_RepFun_iff ) 
+apply (blast intro: subset_Finite) 
+done
+
+lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) <-> Finite(A)"
+by (blast intro: Finite_Pow Finite_Pow_imp_Finite)
+
+lemma Finite_Vset: "i \<in> nat ==> Finite(Vset(i))";
+apply (erule nat_induct)
+ apply (simp add: Vfrom_0) 
+apply (simp add: Vset_succ) 
+done
+
+(*???Ordinal maybe, but some lemmas seem to be in CardinalArith??*)
+text{*Every ordinal is exceeded by some limit ordinal.*}
+lemma Ord_imp_greater_Limit: "Ord(i) ==> \<exists>k. i<k & Limit(k)"
+apply (rule_tac x="i ++ nat" in exI) 
+apply (blast intro: oadd_LimitI  oadd_lt_self  Limit_nat [THEN Limit_has_0])
+done
+
+lemma Ord2_imp_greater_Limit: "[|Ord(i); Ord(j)|] ==> \<exists>k. i<k & j<k & Limit(k)"
+apply (insert Ord_Un [of i j, THEN Ord_imp_greater_Limit]) 
+apply (simp add: Un_least_lt_iff) 
+done
+
+
+
+(*Internalized formulas of FOL. De Bruijn representation. 
+  Unbound variables get their denotations from an environment.*)
+
+consts   formula :: i
+datatype
+  "formula" = Member ("x: nat", "y: nat")
+            | Equal  ("x: nat", "y: nat")
+            | Neg ("p: formula")
+            | And ("p: formula", "q: formula")
+            | Forall ("p: formula")
+
+declare formula.intros [TC]
+
+constdefs Or :: "[i,i]=>i"
+    "Or(p,q) == Neg(And(Neg(p),Neg(q)))"
+
+constdefs Implies :: "[i,i]=>i"
+    "Implies(p,q) == Neg(And(p,Neg(q)))"
+
+constdefs Exists :: "i=>i"
+    "Exists(p) == Neg(Forall(Neg(p)))";
+
+lemma Or_type [TC]: "[| p \<in> formula; q \<in> formula |] ==> Or(p,q) \<in> formula"
+by (simp add: Or_def) 
+
+lemma Implies_type [TC]:
+     "[| p \<in> formula; q \<in> formula |] ==> Implies(p,q) \<in> formula"
+by (simp add: Implies_def) 
+
+lemma Exists_type [TC]: "p \<in> formula ==> Exists(p) \<in> formula"
+by (simp add: Exists_def) 
+
+
+consts   satisfies :: "[i,i]=>i"
+primrec (*explicit lambda is required because the environment varies*)
+  "satisfies(A,Member(x,y)) = 
+      (\<lambda>env \<in> list(A). bool_of_o (nth(x,env) \<in> nth(y,env)))"
+
+  "satisfies(A,Equal(x,y)) = 
+      (\<lambda>env \<in> list(A). bool_of_o (nth(x,env) = nth(y,env)))"
+
+  "satisfies(A,Neg(p)) = 
+      (\<lambda>env \<in> list(A). not(satisfies(A,p)`env))"
+
+  "satisfies(A,And(p,q)) =
+      (\<lambda>env \<in> list(A). (satisfies(A,p)`env) and (satisfies(A,q)`env))"
+
+  "satisfies(A,Forall(p)) = 
+      (\<lambda>env \<in> list(A). bool_of_o (\<forall>x\<in>A. satisfies(A,p) ` (Cons(x,env)) = 1))"
+
+
+lemma "p \<in> formula ==> satisfies(A,p) \<in> list(A) -> bool"
+by (induct_tac p, simp_all) 
+
+syntax sats :: "[i,i,i] => o"
+translations "sats(A,p,env)" == "satisfies(A,p)`env = 1"
+
+lemma [simp]:
+  "env \<in> list(A) 
+   ==> sats(A, Member(x,y), env) <-> nth(x,env) \<in> nth(y,env)"
+by simp
+
+lemma [simp]:
+  "env \<in> list(A) 
+   ==> sats(A, Equal(x,y), env) <-> nth(x,env) = nth(y,env)"
+by simp
+
+lemma sats_Neg_iff [simp]:
+  "env \<in> list(A) 
+   ==> sats(A, Neg(p), env) <-> ~ sats(A,p,env)"
+by (simp add: Bool.not_def cond_def) 
+
+lemma sats_And_iff [simp]:
+  "env \<in> list(A) 
+   ==> (sats(A, And(p,q), env)) <-> sats(A,p,env) & sats(A,q,env)"
+by (simp add: Bool.and_def cond_def) 
+
+lemma sats_Forall_iff [simp]:
+  "env \<in> list(A) 
+   ==> sats(A, Forall(p), env) <-> (\<forall>x\<in>A. sats(A, p, Cons(x,env)))"
+by simp
+
+declare satisfies.simps [simp del]; 
+
+(**** DIVIDING LINE BETWEEN PRIMITIVE AND DERIVED CONNECTIVES ****)
+
+lemma sats_Or_iff [simp]:
+  "env \<in> list(A) 
+   ==> (sats(A, Or(p,q), env)) <-> sats(A,p,env) | sats(A,q,env)"
+by (simp add: Or_def)
+
+lemma sats_Implies_iff [simp]:
+  "env \<in> list(A) 
+   ==> (sats(A, Implies(p,q), env)) <-> (sats(A,p,env) --> sats(A,q,env))"
+apply (simp add: Implies_def, blast) 
+done
+
+lemma sats_Exists_iff [simp]:
+  "env \<in> list(A) 
+   ==> sats(A, Exists(p), env) <-> (\<exists>x\<in>A. sats(A, p, Cons(x,env)))"
+by (simp add: Exists_def)
+
+
+
+
+(*pretty but unnecessary
+constdefs sat     :: "[i,i] => o"
+  "sat(A,p) == satisfies(A,p)`[] = 1"
+
+syntax "_sat"  :: "[i,i] => o"    (infixl "|=" 50)
+translations "A |= p" == "sat(A,p)"
+
+lemma [simp]: "(A |= Neg(p)) <-> ~ (A |= p)"
+by (simp add: sat_def)
+
+lemma [simp]: "(A |= And(p,q)) <-> A|=p & A|=q"
+by (simp add: sat_def)
+*) 
+
+
+constdefs incr_var :: "[i,i]=>i"
+    "incr_var(x,lev) == if x<lev then x else succ(x)"
+
+lemma incr_var_lt: "x<lev ==> incr_var(x,lev) = x"
+by (simp add: incr_var_def)
+
+lemma incr_var_le: "lev\<le>x ==> incr_var(x,lev) = succ(x)"
+apply (simp add: incr_var_def) 
+apply (blast dest: lt_trans1) 
+done
+
+consts   incr_bv :: "i=>i"
+primrec
+  "incr_bv(Member(x,y)) = 
+      (\<lambda>lev \<in> nat. Member (incr_var(x,lev), incr_var(y,lev)))"
+
+  "incr_bv(Equal(x,y)) = 
+      (\<lambda>lev \<in> nat. Equal (incr_var(x,lev), incr_var(y,lev)))"
+
+  "incr_bv(Neg(p)) = 
+      (\<lambda>lev \<in> nat. Neg(incr_bv(p)`lev))"
+
+  "incr_bv(And(p,q)) =
+      (\<lambda>lev \<in> nat. And (incr_bv(p)`lev, incr_bv(q)`lev))"
+
+  "incr_bv(Forall(p)) = 
+      (\<lambda>lev \<in> nat. Forall (incr_bv(p) ` succ(lev)))"
+
+
+constdefs incr_boundvars :: "i => i"
+    "incr_boundvars(p) == incr_bv(p)`0"
+
+
+lemma [TC]: "x \<in> nat ==> incr_var(x,lev) \<in> nat"
+by (simp add: incr_var_def) 
+
+lemma incr_bv_type [TC]: "p \<in> formula ==> incr_bv(p) \<in> nat -> formula"
+by (induct_tac p, simp_all) 
+
+lemma incr_boundvars_type [TC]: "p \<in> formula ==> incr_boundvars(p) \<in> formula"
+by (simp add: incr_boundvars_def) 
+
+(*Obviously DPow is closed under complements and finite intersections and
+unions.  Needs an inductive lemma to allow two lists of parameters to 
+be combined.*)
+
+lemma sats_incr_bv_iff [rule_format]:
+  "[| p \<in> formula; env \<in> list(A); x \<in> A |]
+   ==> \<forall>bvs \<in> list(A). 
+           sats(A, incr_bv(p) ` length(bvs), bvs @ Cons(x,env)) <-> 
+           sats(A, p, bvs@env)"
+apply (induct_tac p)
+apply (simp_all add: incr_var_def nth_append succ_lt_iff length_type)
+apply (auto simp add: diff_succ not_lt_iff_le)
+done
+
+(*UNUSED*)
+lemma sats_incr_boundvars_iff:
+  "[| p \<in> formula; env \<in> list(A); x \<in> A |]
+   ==> sats(A, incr_boundvars(p), Cons(x,env)) <-> sats(A, p, env)"
+apply (insert sats_incr_bv_iff [of p env A x Nil])
+apply (simp add: incr_boundvars_def) 
+done
+
+(*UNUSED
+lemma formula_add_params [rule_format]:
+  "[| p \<in> formula; n \<in> nat |]
+   ==> \<forall>bvs \<in> list(A). \<forall>env \<in> list(A). 
+         length(bvs) = n --> 
+         sats(A, iterates(incr_boundvars,n,p), bvs@env) <-> sats(A, p, env)"
+apply (induct_tac n, simp, clarify) 
+apply (erule list.cases)
+apply (auto simp add: sats_incr_boundvars_iff)  
+done
+*)
+
+consts   arity :: "i=>i"
+primrec
+  "arity(Member(x,y)) = succ(x) \<union> succ(y)"
+
+  "arity(Equal(x,y)) = succ(x) \<union> succ(y)"
+
+  "arity(Neg(p)) = arity(p)"
+
+  "arity(And(p,q)) = arity(p) \<union> arity(q)"
+
+  "arity(Forall(p)) = nat_case3(0, %x. x, arity(p))"
+
+
+lemma arity_type [TC]: "p \<in> formula ==> arity(p) \<in> nat"
+by (induct_tac p, simp_all) 
+
+lemma arity_Or [simp]: "arity(Or(p,q)) = arity(p) \<union> arity(q)"
+by (simp add: Or_def) 
+
+lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \<union> arity(q)"
+by (simp add: Implies_def) 
+
+lemma arity_Exists [simp]: "arity(Exists(p)) = nat_case3(0, %x. x, arity(p))"
+by (simp add: Exists_def) 
+
+
+lemma arity_sats_iff [rule_format]:
+  "[| p \<in> formula; extra \<in> list(A) |]
+   ==> \<forall>env \<in> list(A). 
+           arity(p) \<le> length(env) --> 
+           sats(A, p, env @ extra) <-> sats(A, p, env)"
+apply (induct_tac p)
+apply (simp_all add: nth_append Un_least_lt_iff arity_type 
+                split: split_nat_case3, auto) 
+done
+
+lemma arity_sats1_iff:
+  "[| arity(p) \<le> succ(length(env)); p \<in> formula; x \<in> A; env \<in> list(A); 
+    extra \<in> list(A) |]
+   ==> sats(A, p, Cons(x, env @ extra)) <-> sats(A, p, Cons(x, env))"
+apply (insert arity_sats_iff [of p extra A "Cons(x,env)"])
+apply simp 
+done
+
+(*the following two lemmas prevent huge case splits in arity_incr_bv_lemma*)
+lemma incr_var_lemma:
+     "[| x \<in> nat; y \<in> nat; lev \<le> x |]
+      ==> succ(x) \<union> incr_var(y,lev) = succ(x \<union> y)"
+apply (simp add: incr_var_def Ord_Un_if, auto)
+  apply (blast intro: leI)
+ apply (simp add: not_lt_iff_le)  
+ apply (blast intro: le_anti_sym) 
+apply (blast dest: lt_trans2) 
+done
+
+lemma incr_And_lemma:
+     "y < x ==> y \<union> succ(x) = succ(x \<union> y)"
+apply (simp add: Ord_Un_if lt_Ord lt_Ord2 succ_lt_iff) 
+apply (blast dest: lt_asym) 
+done
+
+lemma arity_incr_bv_lemma [rule_format]:
+  "p \<in> formula 
+   ==> \<forall>n \<in> nat. arity (incr_bv(p) ` n) = 
+                 (if n < arity(p) then succ(arity(p)) else arity(p))"
+apply (induct_tac p) 
+apply (simp_all add: imp_disj not_lt_iff_le Un_least_lt_iff lt_Un_iff le_Un_iff
+                     succ_Un_distrib [symmetric] incr_var_lt incr_var_le
+                     Un_commute incr_var_lemma arity_type 
+            split: split_nat_case3) 
+(*left with the And case*)
+apply safe
+ apply (blast intro: incr_And_lemma lt_trans1) 
+apply (subst incr_And_lemma)
+ apply (blast intro:  lt_trans1) 
+apply (simp add:  Un_commute)
+done
+
+lemma arity_incr_boundvars_eq:
+  "p \<in> formula
+   ==> arity(incr_boundvars(p)) =
+        (if 0 < arity(p) then succ(arity(p)) else arity(p))"
+apply (insert arity_incr_bv_lemma [of p 0])
+apply (simp add: incr_boundvars_def) 
+done
+
+lemma arity_iterates_incr_boundvars_eq:
+  "[| p \<in> formula; n \<in> nat |]
+   ==> arity(incr_boundvars^n(p)) =
+         (if 0 < arity(p) then n #+ arity(p) else arity(p))"
+apply (induct_tac n) 
+apply (simp_all add: arity_incr_boundvars_eq not_lt_iff_le) 
+done
+
+
+(**** TRYING INCR_BV1 AGAIN ****)
+
+constdefs incr_bv1 :: "i => i"
+    "incr_bv1(p) == incr_bv(p)`1"
+
+
+lemma incr_bv1_type [TC]: "p \<in> formula ==> incr_bv1(p) \<in> formula"
+by (simp add: incr_bv1_def) 
+
+(*For renaming all but the bound variable at level 0*)
+lemma sats_incr_bv1_iff [rule_format]:
+  "[| p \<in> formula; env \<in> list(A); x \<in> A; y \<in> A |]
+   ==> sats(A, incr_bv1(p), Cons(x, Cons(y, env))) <-> 
+       sats(A, p, Cons(x,env))"
+apply (insert sats_incr_bv_iff [of p env A y "Cons(x,Nil)"])
+apply (simp add: incr_bv1_def) 
+done
+
+lemma formula_add_params1 [rule_format]:
+  "[| p \<in> formula; n \<in> nat; x \<in> A |]
+   ==> \<forall>bvs \<in> list(A). \<forall>env \<in> list(A). 
+          length(bvs) = n --> 
+          sats(A, iterates(incr_bv1, n, p), Cons(x, bvs@env)) <-> 
+          sats(A, p, Cons(x,env))"
+apply (induct_tac n, simp, clarify) 
+apply (erule list.cases)
+apply (simp_all add: sats_incr_bv1_iff) 
+done
+
+
+lemma arity_incr_bv1_eq:
+  "p \<in> formula
+   ==> arity(incr_bv1(p)) =
+        (if 1 < arity(p) then succ(arity(p)) else arity(p))"
+apply (insert arity_incr_bv_lemma [of p 1])
+apply (simp add: incr_bv1_def) 
+done
+
+lemma arity_iterates_incr_bv1_eq:
+  "[| p \<in> formula; n \<in> nat |]
+   ==> arity(incr_bv1^n(p)) =
+         (if 1 < arity(p) then n #+ arity(p) else arity(p))"
+apply (induct_tac n) 
+apply (simp_all add: arity_incr_bv1_eq )
+apply (simp add: not_lt_iff_le)
+apply (blast intro: le_trans add_le_self2 arity_type) 
+done
+
+
+(*Definable powerset operation: Kunen's definition 1.1, page 165.*)
+constdefs DPow :: "i => i"
+  "DPow(A) == {X \<in> Pow(A). 
+               \<exists>env \<in> list(A). \<exists>p \<in> formula. 
+                 arity(p) \<le> succ(length(env)) & 
+                 X = {x\<in>A. sats(A, p, Cons(x,env))}}"
+
+lemma DPowI:
+  "[|X <= A;  env \<in> list(A);  p \<in> formula; 
+     arity(p) \<le> succ(length(env))|]
+   ==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"
+by (simp add: DPow_def, blast) 
+
+lemma DPowD:
+  "X \<in> DPow(A) 
+   ==> X <= A &
+       (\<exists>env \<in> list(A). 
+        \<exists>p \<in> formula. arity(p) \<le> succ(length(env)) & 
+                      X = {x\<in>A. sats(A, p, Cons(x,env))})"
+by (simp add: DPow_def) 
+
+lemmas DPow_imp_subset = DPowD [THEN conjunct1]
+
+(*Lemma 1.2*)
+lemma "[| p \<in> formula; env \<in> list(A); arity(p) \<le> succ(length(env)) |] 
+       ==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"
+by (blast intro: DPowI)
+
+lemma DPow_subset_Pow: "DPow(A) <= Pow(A)"
+by (simp add: DPow_def, blast)
+
+lemma empty_in_DPow: "0 \<in> DPow(A)"
+apply (simp add: DPow_def)
+apply (rule_tac x="Nil" in bexI) 
+ apply (rule_tac x="Neg(Equal(0,0))" in bexI) 
+  apply (auto simp add: Un_least_lt_iff) 
+done
+
+lemma Compl_in_DPow: "X \<in> DPow(A) ==> (A-X) \<in> DPow(A)"
+apply (simp add: DPow_def, clarify, auto) 
+apply (rule bexI) 
+ apply (rule_tac x="Neg(p)" in bexI) 
+  apply auto 
+done
+
+lemma Int_in_DPow: "[| X \<in> DPow(A); Y \<in> DPow(A) |] ==> X Int Y \<in> DPow(A)"
+apply (simp add: DPow_def, auto) 
+apply (rename_tac envp p envq q) 
+apply (rule_tac x="envp@envq" in bexI) 
+ apply (rule_tac x="And(p, iterates(incr_bv1,length(envp),q))" in bexI)
+  apply typecheck
+apply (rule conjI) 
+(*finally check the arity!*)
+ apply (simp add: arity_iterates_incr_bv1_eq length_app Un_least_lt_iff)
+ apply (force intro: add_le_self le_trans) 
+apply (simp add: arity_sats1_iff formula_add_params1, blast) 
+done
+
+lemma Un_in_DPow: "[| X \<in> DPow(A); Y \<in> DPow(A) |] ==> X Un Y \<in> DPow(A)"
+apply (subgoal_tac "X Un Y = A - ((A-X) Int (A-Y))") 
+apply (simp add: Int_in_DPow Compl_in_DPow) 
+apply (simp add: DPow_def, blast) 
+done
+
+lemma singleton_in_DPow: "x \<in> A ==> {x} \<in> DPow(A)"
+apply (simp add: DPow_def)
+apply (rule_tac x="Cons(x,Nil)" in bexI) 
+ apply (rule_tac x="Equal(0,1)" in bexI) 
+  apply typecheck
+apply (force simp add: succ_Un_distrib [symmetric])  
+done
+
+lemma cons_in_DPow: "[| a \<in> A; X \<in> DPow(A) |] ==> cons(a,X) \<in> DPow(A)"
+apply (rule cons_eq [THEN subst]) 
+apply (blast intro: singleton_in_DPow Un_in_DPow) 
+done
+
+(*Part of Lemma 1.3*)
+lemma Fin_into_DPow: "X \<in> Fin(A) ==> X \<in> DPow(A)"
+apply (erule Fin.induct) 
+ apply (rule empty_in_DPow) 
+apply (blast intro: cons_in_DPow) 
+done
+
+(*DPow is not monotonic.  For example, let A be some non-constructible set
+  of natural numbers, and let B be nat.  Then A<=B and obviously A : DPow(A)
+  but A ~: DPow(B).*)
+lemma DPow_mono: "A : DPow(B) ==> DPow(A) <= DPow(B)"
+apply (simp add: DPow_def, auto) 
+(*must use the formula defining A in B to relativize the new formula...*)
+oops
+
+lemma DPow_0: "DPow(0) = {0}" 
+by (blast intro: empty_in_DPow dest: DPow_imp_subset)
+
+lemma Finite_Pow_subset_Pow: "Finite(A) ==> Pow(A) <= DPow(A)" 
+by (blast intro: Fin_into_DPow Finite_into_Fin Fin_subset)
+
+lemma Finite_DPow_eq_Pow: "Finite(A) ==> DPow(A) = Pow(A)"
+apply (rule equalityI) 
+apply (rule DPow_subset_Pow) 
+apply (erule Finite_Pow_subset_Pow) 
+done
+
+(*This may be true but the proof looks difficult, requiring relativization 
+lemma DPow_insert: "DPow (cons(a,A)) = DPow(A) Un {cons(a,X) . X: DPow(A)}"
+apply (rule equalityI, safe)
+oops
+*)
+
+subsection{* Constant Lset: Levels of the Constructible Universe *}
+
+constdefs Lset :: "i=>i"
+    "Lset(i) == transrec(i, %x f. \<Union>y\<in>x. DPow(f`y))"
+
+text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
+lemma Lset: "Lset(i) = (UN j:i. DPow(Lset(j)))"
+by (subst Lset_def [THEN def_transrec], simp)
+
+lemma LsetI: "[|y\<in>x; A \<in> DPow(Lset(y))|] ==> A \<in> Lset(x)";
+by (subst Lset, blast)
+
+lemma LsetD: "A \<in> Lset(x) ==> \<exists>y\<in>x. A \<in> DPow(Lset(y))";
+apply (insert Lset [of x]) 
+apply (blast intro: elim: equalityE) 
+done
+
+subsubsection{* Transitivity *}
+
+lemma elem_subset_in_DPow: "[|X \<in> A; X \<subseteq> A|] ==> X \<in> DPow(A)"
+apply (simp add: Transset_def DPow_def)
+apply (rule_tac x="[X]" in bexI) 
+ apply (rule_tac x="Member(0,1)" in bexI) 
+  apply (auto simp add: Un_least_lt_iff) 
+done
+
+lemma Transset_subset_DPow: "Transset(A) ==> A <= DPow(A)"
+apply clarify  
+apply (simp add: Transset_def)
+apply (blast intro: elem_subset_in_DPow) 
+done
+
+lemma Transset_DPow: "Transset(A) ==> Transset(DPow(A))"
+apply (simp add: Transset_def) 
+apply (blast intro: elem_subset_in_DPow dest: DPowD) 
+done
+
+text{*Kunen's VI, 1.6 (a)*}
+lemma Transset_Lset: "Transset(Lset(i))"
+apply (rule_tac a=i in eps_induct)
+apply (subst Lset)
+apply (blast intro!: Transset_Union_family Transset_Un Transset_DPow)
+done
+
+subsubsection{* Monotonicity *}
+
+text{*Kunen's VI, 1.6 (b)*}
+lemma Lset_mono [rule_format]:
+     "ALL j. i<=j --> Lset(i) <= Lset(j)"
+apply (rule_tac a=i in eps_induct)
+apply (rule impI [THEN allI])
+apply (subst Lset)
+apply (subst Lset, blast) 
+done
+
+text{*This version lets us remove the premise @{term "Ord(i)"} sometimes.*}
+lemma Lset_mono_mem [rule_format]:
+     "ALL j. i:j --> Lset(i) <= Lset(j)"
+apply (rule_tac a=i in eps_induct)
+apply (rule impI [THEN allI])
+apply (subst Lset, auto) 
+apply (rule rev_bexI, assumption)
+apply (blast intro: elem_subset_in_DPow dest: LsetD DPowD) 
+done
+
+subsubsection{* 0, successor and limit equations fof Lset *}
+
+lemma Lset_0 [simp]: "Lset(0) = 0"
+by (subst Lset, blast)
+
+lemma Lset_succ_subset1: "DPow(Lset(i)) <= Lset(succ(i))"
+by (subst Lset, rule succI1 [THEN RepFunI, THEN Union_upper])
+
+lemma Lset_succ_subset2: "Lset(succ(i)) <= DPow(Lset(i))"
+apply (subst Lset, rule UN_least)
+apply (erule succE) 
+ apply blast 
+apply clarify
+apply (rule elem_subset_in_DPow)
+ apply (subst Lset)
+ apply blast 
+apply (blast intro: dest: DPowD Lset_mono_mem) 
+done
+
+lemma Lset_succ: "Lset(succ(i)) = DPow(Lset(i))"
+by (intro equalityI Lset_succ_subset1 Lset_succ_subset2) 
+
+lemma Lset_Union [simp]: "Lset(\<Union>(X)) = (\<Union>y\<in>X. Lset(y))"
+apply (subst Lset)
+apply (rule equalityI)
+ txt{*first inclusion*}
+ apply (rule UN_least)
+ apply (erule UnionE)
+ apply (rule subset_trans)
+  apply (erule_tac [2] UN_upper, subst Lset, erule UN_upper)
+txt{*opposite inclusion*}
+apply (rule UN_least)
+apply (subst Lset, blast)
+done
+
+subsubsection{* Lset applied to Limit ordinals *}
+
+lemma Limit_Lset_eq:
+    "Limit(i) ==> Lset(i) = (\<Union>y\<in>i. Lset(y))"
+by (simp add: Lset_Union [symmetric] Limit_Union_eq)
+
+lemma lt_LsetI: "[| a: Lset(j);  j<i |] ==> a : Lset(i)"
+by (blast dest: Lset_mono [OF le_imp_subset [OF leI]])
+
+lemma Limit_LsetE:
+    "[| a: Lset(i);  ~R ==> Limit(i);
+        !!x. [| x<i;  a: Lset(x) |] ==> R
+     |] ==> R"
+apply (rule classical)
+apply (rule Limit_Lset_eq [THEN equalityD1, THEN subsetD, THEN UN_E])
+  prefer 2 apply assumption
+ apply blast 
+apply (blast intro: ltI  Limit_is_Ord)
+done
+
+subsubsection{* Basic closure properties *}
+
+lemma zero_in_Lset: "y:x ==> 0 : Lset(x)"
+by (subst Lset, blast intro: empty_in_DPow)
+
+lemma notin_Lset: "x \<notin> Lset(x)"
+apply (rule_tac a=x in eps_induct)
+apply (subst Lset)
+apply (blast dest: DPowD)  
+done
+
+
+
+text{*Kunen's VI, 1.9 (b)*}
+
+constdefs subset_fm :: "[i,i]=>i"
+    "subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))"
+
+lemma subset_type [TC]: "[| x \<in> nat; y \<in> nat |] ==> subset_fm(x,y) \<in> formula"
+by (simp add: subset_fm_def) 
+
+lemma arity_subset_fm [simp]:
+     "[| x \<in> nat; y \<in> nat |] ==> arity(subset_fm(x,y)) = succ(x) \<union> succ(y)"
+by (simp add: subset_fm_def succ_Un_distrib [symmetric]) 
+
+lemma sats_subset_fm [simp]:
+   "[|x < length(env); y \<in> nat; env \<in> list(A); Transset(A)|]
+    ==> sats(A, subset_fm(x,y), env) <-> nth(x,env) \<subseteq> nth(y,env)"
+apply (frule lt_nat_in_nat, erule length_type) 
+apply (simp add: subset_fm_def Transset_def) 
+apply (blast intro: nth_type ) 
+done
+
+constdefs transset_fm :: "i=>i"
+   "transset_fm(x) == Forall(Implies(Member(0,succ(x)), subset_fm(0,succ(x))))"
+
+lemma transset_type [TC]: "x \<in> nat ==> transset_fm(x) \<in> formula"
+by (simp add: transset_fm_def) 
+
+lemma arity_transset_fm [simp]:
+     "x \<in> nat ==> arity(transset_fm(x)) = succ(x)"
+by (simp add: transset_fm_def succ_Un_distrib [symmetric]) 
+
+lemma sats_transset_fm [simp]:
+   "[|x < length(env); env \<in> list(A); Transset(A)|]
+    ==> sats(A, transset_fm(x), env) <-> Transset(nth(x,env))"
+apply (frule lt_nat_in_nat, erule length_type) 
+apply (simp add: transset_fm_def Transset_def) 
+apply (blast intro: nth_type ) 
+done
+
+constdefs ordinal_fm :: "i=>i"
+   "ordinal_fm(x) == 
+      And(transset_fm(x), Forall(Implies(Member(0,succ(x)), transset_fm(0))))"
+
+lemma ordinal_type [TC]: "x \<in> nat ==> ordinal_fm(x) \<in> formula"
+by (simp add: ordinal_fm_def) 
+
+lemma arity_ordinal_fm [simp]:
+     "x \<in> nat ==> arity(ordinal_fm(x)) = succ(x)"
+by (simp add: ordinal_fm_def succ_Un_distrib [symmetric]) 
+
+lemma sats_ordinal_fm [simp]:
+   "[|x < length(env); env \<in> list(A); Transset(A)|]
+    ==> sats(A, ordinal_fm(x), env) <-> Ord(nth(x,env))"
+apply (frule lt_nat_in_nat, erule length_type) 
+apply (simp add: ordinal_fm_def Ord_def Transset_def)
+apply (blast intro: nth_type ) 
+done
+
+text{*The subset consisting of the ordinals is definable.*}
+lemma Ords_in_DPow: "Transset(A) ==> {x \<in> A. Ord(x)} \<in> DPow(A)"
+apply (simp add: DPow_def Collect_subset) 
+apply (rule_tac x="Nil" in bexI) 
+ apply (rule_tac x="ordinal_fm(0)" in bexI) 
+apply (simp_all add: sats_ordinal_fm)
+done 
+
+lemma Ords_of_Lset_eq: "Ord(i) ==> {x\<in>Lset(i). Ord(x)} = i"
+apply (erule trans_induct3)
+  apply (simp_all add: Lset_succ Limit_Lset_eq Limit_Union_eq)
+txt{*The successor case remains.*} 
+apply (rule equalityI)
+txt{*First inclusion*}
+ apply clarify  
+ apply (erule Ord_linear_lt, assumption) 
+   apply (blast dest: DPow_imp_subset ltD notE [OF notin_Lset]) 
+  apply blast 
+ apply (blast dest: ltD)
+txt{*Opposite inclusion, @{term "succ(x) \<subseteq> DPow(Lset(x)) \<inter> ON"}*}
+apply auto
+txt{*Key case: *}
+  apply (erule subst, rule Ords_in_DPow [OF Transset_Lset]) 
+ apply (blast intro: elem_subset_in_DPow dest: OrdmemD elim: equalityE) 
+apply (blast intro: Ord_in_Ord) 
+done
+
+
+lemma Ord_subset_Lset: "Ord(i) ==> i \<subseteq> Lset(i)"
+by (subst Ords_of_Lset_eq [symmetric], assumption, fast)
+
+lemma Ord_in_Lset: "Ord(i) ==> i \<in> Lset(succ(i))"
+apply (simp add: Lset_succ)
+apply (subst Ords_of_Lset_eq [symmetric], assumption, 
+       rule Ords_in_DPow [OF Transset_Lset]) 
+done
+
+subsubsection{* Unions *}
+
+lemma Union_in_Lset:
+     "X \<in> Lset(j) ==> Union(X) \<in> Lset(succ(j))"
+apply (insert Transset_Lset)
+apply (rule LsetI [OF succI1])
+apply (simp add: Transset_def DPow_def) 
+apply (intro conjI, blast)
+txt{*Now to create the formula @{term "\<exists>y. y \<in> X \<and> x \<in> y"} *}
+apply (rule_tac x="Cons(X,Nil)" in bexI) 
+ apply (rule_tac x="Exists(And(Member(0,2), Member(1,0)))" in bexI) 
+  apply typecheck
+apply (simp add: succ_Un_distrib [symmetric], blast) 
+done
+
+lemma Union_in_LLimit:
+     "[| X: Lset(i);  Limit(i) |] ==> Union(X) : Lset(i)"
+apply (rule Limit_LsetE, assumption+)
+apply (blast intro: Limit_has_succ lt_LsetI Union_in_Lset)
+done
+
+subsubsection{* Finite sets and ordered pairs *}
+
+lemma singleton_in_Lset: "a: Lset(i) ==> {a} : Lset(succ(i))"
+by (simp add: Lset_succ singleton_in_DPow) 
+
+lemma doubleton_in_Lset:
+     "[| a: Lset(i);  b: Lset(i) |] ==> {a,b} : Lset(succ(i))"
+by (simp add: Lset_succ empty_in_DPow cons_in_DPow) 
+
+lemma Pair_in_Lset:
+    "[| a: Lset(i);  b: Lset(i); Ord(i) |] ==> <a,b> : Lset(succ(succ(i)))"
+apply (unfold Pair_def)
+apply (blast intro: doubleton_in_Lset) 
+done
+
+lemmas zero_in_LLimit = Limit_has_0 [THEN ltD, THEN zero_in_Lset, standard]
+
+lemma singleton_in_LLimit:
+    "[| a: Lset(i);  Limit(i) |] ==> {a} : Lset(i)"
+apply (erule Limit_LsetE, assumption)
+apply (erule singleton_in_Lset [THEN lt_LsetI])
+apply (blast intro: Limit_has_succ) 
+done
+
+lemmas Lset_UnI1 = Un_upper1 [THEN Lset_mono [THEN subsetD], standard]
+lemmas Lset_UnI2 = Un_upper2 [THEN Lset_mono [THEN subsetD], standard]
+
+text{*Hard work is finding a single j:i such that {a,b}<=Lset(j)*}
+lemma doubleton_in_LLimit:
+    "[| a: Lset(i);  b: Lset(i);  Limit(i) |] ==> {a,b} : Lset(i)"
+apply (erule Limit_LsetE, assumption)
+apply (erule Limit_LsetE, assumption)
+apply (blast intro:  lt_LsetI [OF doubleton_in_Lset]
+                     Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
+done
+
+lemma Pair_in_LLimit:
+    "[| a: Lset(i);  b: Lset(i);  Limit(i) |] ==> <a,b> : Lset(i)"
+txt{*Infer that a, b occur at ordinals x,xa < i.*}
+apply (erule Limit_LsetE, assumption)
+apply (erule Limit_LsetE, assumption)
+txt{*Infer that succ(succ(x Un xa)) < i *}
+apply (blast intro: lt_Ord lt_LsetI [OF Pair_in_Lset]
+                    Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
+done
+
+lemma product_LLimit: "Limit(i) ==> Lset(i) * Lset(i) <= Lset(i)"
+by (blast intro: Pair_in_LLimit)
+
+lemmas Sigma_subset_LLimit = subset_trans [OF Sigma_mono product_LLimit]
+
+lemma nat_subset_LLimit: "Limit(i) ==> nat \<subseteq> Lset(i)"
+by (blast dest: Ord_subset_Lset nat_le_Limit le_imp_subset Limit_is_Ord)
+
+lemma nat_into_LLimit: "[| n: nat;  Limit(i) |] ==> n : Lset(i)"
+by (blast intro: nat_subset_LLimit [THEN subsetD])
+
+
+subsubsection{* Closure under disjoint union *}
+
+lemmas zero_in_LLimit = Limit_has_0 [THEN ltD, THEN zero_in_Lset, standard]
+
+lemma one_in_LLimit: "Limit(i) ==> 1 : Lset(i)"
+by (blast intro: nat_into_LLimit)
+
+lemma Inl_in_LLimit:
+    "[| a: Lset(i); Limit(i) |] ==> Inl(a) : Lset(i)"
+apply (unfold Inl_def)
+apply (blast intro: zero_in_LLimit Pair_in_LLimit)
+done
+
+lemma Inr_in_LLimit:
+    "[| b: Lset(i); Limit(i) |] ==> Inr(b) : Lset(i)"
+apply (unfold Inr_def)
+apply (blast intro: one_in_LLimit Pair_in_LLimit)
+done
+
+lemma sum_LLimit: "Limit(i) ==> Lset(i) + Lset(i) <= Lset(i)"
+by (blast intro!: Inl_in_LLimit Inr_in_LLimit)
+
+lemmas sum_subset_LLimit = subset_trans [OF sum_mono sum_LLimit]
+
+
+text{*The constructible universe and its rank function*}
+constdefs
+  L :: "i=>o" --{*Kunen's definition VI, 1.5, page 167*}
+    "L(x) == \<exists>i. Ord(i) & x \<in> Lset(i)"
+  
+  lrank :: "i=>i" --{*Kunen's definition VI, 1.7*}
+    "lrank(x) == \<mu>i. x \<in> Lset(succ(i))"
+
+lemma L_I: "[|x \<in> Lset(i); Ord(i)|] ==> L(x)"
+by (simp add: L_def, blast)
+
+lemma L_D: "L(x) ==> \<exists>i. Ord(i) & x \<in> Lset(i)"
+by (simp add: L_def)
+
+lemma Ord_lrank [simp]: "Ord(lrank(a))"
+by (simp add: lrank_def)
+
+lemma Lset_lrank_lt [rule_format]: "Ord(i) ==> x \<in> Lset(i) --> lrank(x) < i"
+apply (erule trans_induct3)
+  apply simp   
+ apply (simp only: lrank_def) 
+ apply (blast intro: Least_le) 
+apply (simp_all add: Limit_Lset_eq) 
+apply (blast intro: ltI Limit_is_Ord lt_trans) 
+done
+
+text{*Kunen's VI, 1.8, and the proof is much less trivial than the text
+would suggest.  For a start it need the previous lemma, proved by induction.*}
+lemma Lset_iff_lrank_lt: "Ord(i) ==> x \<in> Lset(i) <-> L(x) & lrank(x) < i"
+apply (simp add: L_def, auto) 
+ apply (blast intro: Lset_lrank_lt) 
+ apply (unfold lrank_def) 
+apply (drule succI1 [THEN Lset_mono_mem, THEN subsetD]) 
+apply (drule_tac P="\<lambda>i. x \<in> Lset(succ(i))" in LeastI, assumption) 
+apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD]) 
+done
+
+lemma Lset_succ_lrank_iff [simp]: "x \<in> Lset(succ(lrank(x))) <-> L(x)"
+by (simp add: Lset_iff_lrank_lt)
+
+text{*Kunen's VI, 1.9 (a)*}
+lemma lrank_of_Ord: "Ord(i) ==> lrank(i) = i"
+apply (unfold lrank_def) 
+apply (rule Least_equality) 
+  apply (erule Ord_in_Lset) 
+ apply assumption
+apply (insert notin_Lset [of i]) 
+apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD]) 
+done
+
+text{*This is lrank(lrank(a)) = lrank(a) *}
+declare Ord_lrank [THEN lrank_of_Ord, simp]
+
+text{*Kunen's VI, 1.10 *}
+lemma Lset_in_Lset_succ: "Lset(i) \<in> Lset(succ(i))";
+apply (simp add: Lset_succ DPow_def) 
+apply (rule_tac x="Nil" in bexI) 
+ apply (rule_tac x="Equal(0,0)" in bexI) 
+apply auto 
+done
+
+lemma lrank_Lset: "Ord(i) ==> lrank(Lset(i)) = i"
+apply (unfold lrank_def) 
+apply (rule Least_equality) 
+  apply (rule Lset_in_Lset_succ) 
+ apply assumption
+apply clarify 
+apply (subgoal_tac "Lset(succ(ia)) <= Lset(i)")
+ apply (blast dest: mem_irrefl) 
+apply (blast intro!: le_imp_subset Lset_mono) 
+done
+
+text{*Kunen's VI, 1.11 *}
+lemma Lset_subset_Vset: "Ord(i) ==> Lset(i) <= Vset(i)";
+apply (erule trans_induct)
+apply (subst Lset) 
+apply (subst Vset) 
+apply (rule UN_mono [OF subset_refl]) 
+apply (rule subset_trans [OF DPow_subset_Pow]) 
+apply (rule Pow_mono, blast) 
+done
+
+text{*Kunen's VI, 1.12 *}
+lemma Lset_subset_Vset: "i \<in> nat ==> Lset(i) = Vset(i)";
+apply (erule nat_induct)
+ apply (simp add: Vfrom_0) 
+apply (simp add: Lset_succ Vset_succ Finite_Vset Finite_DPow_eq_Pow) 
+done
+
+subsection{*For L to satisfy the ZF axioms*}
+
+lemma Union_in_L: "L(X) ==> L(Union(X))"
+apply (simp add: L_def, clarify) 
+apply (drule Ord_imp_greater_Limit) 
+apply (blast intro: lt_LsetI Union_in_LLimit Limit_is_Ord) 
+done
+
+lemma doubleton_in_L: "[| L(a); L(b) |] ==> L({a, b})"
+apply (simp add: L_def, clarify) 
+apply (drule Ord2_imp_greater_Limit, assumption) 
+apply (blast intro: lt_LsetI doubleton_in_LLimit Limit_is_Ord) 
+done
+
+subsubsection{*For L to satisfy Powerset *}
+
+lemma LPow_env_typing:
+     "[| y : Lset(i); Ord(i); y \<subseteq> X |] ==> y \<in> (\<Union>y\<in>Pow(X). Lset(succ(lrank(y))))"
+by (auto intro: L_I iff: Lset_succ_lrank_iff) 
+
+lemma LPow_in_Lset:
+     "[|X \<in> Lset(i); Ord(i)|] ==> \<exists>j. Ord(j) & {y \<in> Pow(X). L(y)} \<in> Lset(j)"
+apply (rule_tac x="succ(\<Union>y \<in> Pow(X). succ(lrank(y)))" in exI)
+apply simp 
+apply (rule LsetI [OF succI1])
+apply (simp add: DPow_def) 
+apply (intro conjI, clarify) 
+apply (rule_tac a="x" in UN_I, simp+)  
+txt{*Now to create the formula @{term "y \<subseteq> X"} *}
+apply (rule_tac x="Cons(X,Nil)" in bexI) 
+ apply (rule_tac x="subset_fm(0,1)" in bexI) 
+  apply typecheck
+apply (rule conjI) 
+apply (simp add: succ_Un_distrib [symmetric]) 
+apply (rule equality_iffI) 
+apply (simp add: Transset_UN [OF Transset_Lset] list.Cons [OF LPow_env_typing])
+apply (auto intro: L_I iff: Lset_succ_lrank_iff) 
+done
+
+lemma LPow_in_L: "L(X) ==> L({y \<in> Pow(X). L(y)})"
+by (blast intro: L_I dest: L_D LPow_in_Lset)
+
+end
diff -r 74d9144c452c -r 45be08fbdcff src/ZF/Constructible/L_axioms.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/L_axioms.thy	Wed Jun 19 11:48:01 2002 +0200
@@ -0,0 +1,129 @@
+header {* The class L satisfies the axioms of ZF*}
+
+theory L_axioms = Formula + Relative:
+
+
+text {* The class L satisfies the premises of locale @{text M_axioms} *}
+
+lemma transL: "[| y\<in>x; L(x) |] ==> L(y)"
+apply (insert Transset_Lset) 
+apply (simp add: Transset_def L_def, blast) 
+done
+
+lemma nonempty: "L(0)"
+apply (simp add: L_def) 
+apply (blast intro: zero_in_Lset) 
+done
+
+lemma upair_ax: "upair_ax(L)"
+apply (simp add: upair_ax_def upair_def, clarify)
+apply (rule_tac x="{x,y}" in exI)  
+apply (simp add: doubleton_in_L) 
+done
+
+lemma Union_ax: "Union_ax(L)"
+apply (simp add: Union_ax_def big_union_def, clarify)
+apply (rule_tac x="Union(x)" in exI)  
+apply (simp add: Union_in_L, auto) 
+apply (blast intro: transL) 
+done
+
+lemma power_ax: "power_ax(L)"
+apply (simp add: power_ax_def powerset_def Relative.subset_def, clarify)
+apply (rule_tac x="{y \<in> Pow(x). L(y)}" in exI)  
+apply (simp add: LPow_in_L, auto)
+apply (blast intro: transL) 
+done
+
+subsubsection{*For L to satisfy Replacement *}
+
+(*Can't move these to Formula unless the definition of univalent is moved
+there too!*)
+
+lemma LReplace_in_Lset:
+     "[|X \<in> Lset(i); univalent(L,X,Q); Ord(i)|] 
+      ==> \<exists>j. Ord(j) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Lset(j)"
+apply (rule_tac x="\<Union>y \<in> Replace(X, %x y. Q(x,y) & L(y)). succ(lrank(y))" 
+       in exI)
+apply simp
+apply clarify 
+apply (rule_tac a="x" in UN_I)  
+ apply (simp_all add: Replace_iff univalent_def) 
+apply (blast dest: transL L_I) 
+done
+
+lemma LReplace_in_L: 
+     "[|L(X); univalent(L,X,Q)|] 
+      ==> \<exists>Y. L(Y) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Y"
+apply (drule L_D, clarify) 
+apply (drule LReplace_in_Lset, assumption+)
+apply (blast intro: L_I Lset_in_Lset_succ)
+done
+
+lemma replacement: "replacement(L,P)"
+apply (simp add: replacement_def, clarify)
+apply (frule LReplace_in_L, assumption+)
+apply clarify 
+apply (rule_tac x=Y in exI)   
+apply (simp add: Replace_iff univalent_def, blast) 
+done
+
+end
+
+(*
+
+  and Inter_separation:
+     "L(A) ==> separation(M, \<lambda>x. \<forall>y\<in>A. L(y) --> x\<in>y)"
+  and cartprod_separation:
+     "[| L(A); L(B) |] 
+      ==> separation(M, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. L(x) & L(y) & pair(M,x,y,z))"
+  and image_separation:
+     "[| L(A); L(r) |] 
+      ==> separation(M, \<lambda>y. \<exists>p\<in>r. L(p) & (\<exists>x\<in>A. L(x) & pair(M,x,y,p)))"
+  and vimage_separation:
+     "[| L(A); L(r) |] 
+      ==> separation(M, \<lambda>x. \<exists>p\<in>r. L(p) & (\<exists>y\<in>A. L(x) & pair(M,x,y,p)))"
+  and converse_separation:
+     "L(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r. L(p) & (\<exists>x y. L(x) & L(y) & 
+				     pair(M,x,y,p) & pair(M,y,x,z)))"
+  and restrict_separation:
+     "L(A) 
+      ==> separation(M, \<lambda>z. \<exists>x\<in>A. L(x) & (\<exists>y. L(y) & pair(M,x,y,z)))"
+  and comp_separation:
+     "[| L(r); L(s) |]
+      ==> separation(M, \<lambda>xz. \<exists>x y z. L(x) & L(y) & L(z) &
+			   (\<exists>xy\<in>s. \<exists>yz\<in>r. L(xy) & L(yz) & 
+		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz)))"
+  and pred_separation:
+     "[| L(r); L(x) |] ==> separation(M, \<lambda>y. \<exists>p\<in>r. L(p) & pair(M,y,x,p))"
+  and Memrel_separation:
+     "separation(M, \<lambda>z. \<exists>x y. L(x) & L(y) & pair(M,x,y,z) \<and> x \<in> y)"
+  and obase_separation:
+     --{*part of the order type formalization*}
+     "[| L(A); L(r) |] 
+      ==> separation(M, \<lambda>a. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) & 
+	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
+	     order_isomorphism(M,par,r,x,mx,g))"
+  and well_ord_iso_separation:
+     "[| L(A); L(f); L(r) |] 
+      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y. L(y) \<and> (\<exists>p. L(p) \<and> 
+		     fun_apply(M,f,x,y) \<and> pair(M,y,x,p) \<and> p \<in> r)))"
+  and obase_equals_separation:
+     "[| L(A); L(r) |] 
+      ==> separation
+      (M, \<lambda>x. x\<in>A --> ~(\<exists>y. L(y) & (\<exists>g. L(g) &
+	      ordinal(M,y) & (\<exists>my pxr. L(my) & L(pxr) &
+	      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
+	      order_isomorphism(M,pxr,r,y,my,g)))))"
+  and is_recfun_separation:
+     --{*for well-founded recursion.  NEEDS RELATIVIZATION*}
+     "[| L(A); L(f); L(g); L(a); L(b) |] 
+     ==> separation(M, \<lambda>x. x \<in> A --> \<langle>x,a\<rangle> \<in> r \<and> \<langle>x,b\<rangle> \<in> r \<and> f`x \<noteq> g`x)"
+  and omap_replacement:
+     "[| L(A); L(r) |] 
+      ==> strong_replacement(M,
+             \<lambda>a z. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) &
+	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
+	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
+
+*)
\ No newline at end of file
diff -r 74d9144c452c -r 45be08fbdcff src/ZF/Constructible/Normal.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/Normal.thy	Wed Jun 19 11:48:01 2002 +0200
@@ -0,0 +1,457 @@
+header {*Closed Unbounded Classes and Normal Functions*}
+
+theory Normal = Main:
+
+text{*
+One source is the book
+
+Frank R. Drake.
+\emph{Set Theory: An Introduction to Large Cardinals}.
+North-Holland, 1974.
+*}
+
+
+subsection {*Closed and Unbounded (c.u.) Classes of Ordinals*}
+
+constdefs
+  Closed :: "(i=>o) => o"
+    "Closed(P) == \<forall>I. I \<noteq> 0 --> (\<forall>i\<in>I. Ord(i) \<and> P(i)) --> P(\<Union>(I))"
+
+  Unbounded :: "(i=>o) => o"
+    "Unbounded(P) == \<forall>i. Ord(i) --> (\<exists>j. i<j \<and> P(j))"
+
+  Closed_Unbounded :: "(i=>o) => o"
+    "Closed_Unbounded(P) == Closed(P) \<and> Unbounded(P)"
+
+
+subsubsection{*Simple facts about c.u. classes*}
+
+lemma ClosedI:
+     "[| !!I. [| I \<noteq> 0; \<forall>i\<in>I. Ord(i) \<and> P(i) |] ==> P(\<Union>(I)) |] 
+      ==> Closed(P)"
+by (simp add: Closed_def)
+
+lemma ClosedD:
+     "[| Closed(P); I \<noteq> 0; !!i. i\<in>I ==> Ord(i); !!i. i\<in>I ==> P(i) |] 
+      ==> P(\<Union>(I))"
+by (simp add: Closed_def)
+
+lemma UnboundedD:
+     "[| Unbounded(P);  Ord(i) |] ==> \<exists>j. i<j \<and> P(j)"
+by (simp add: Unbounded_def)
+
+lemma Closed_Unbounded_imp_Unbounded: "Closed_Unbounded(C) ==> Unbounded(C)"
+by (simp add: Closed_Unbounded_def) 
+
+
+text{*The universal class, V, is closed and unbounded.
+      A bit odd, since C. U. concerns only ordinals, but it's used below!*}
+theorem Closed_Unbounded_V [simp]: "Closed_Unbounded(\<lambda>x. True)"
+by (unfold Closed_Unbounded_def Closed_def Unbounded_def, blast)
+
+text{*The class of ordinals, @{term Ord}, is closed and unbounded.*}
+theorem Closed_Unbounded_Ord   [simp]: "Closed_Unbounded(Ord)"
+by (unfold Closed_Unbounded_def Closed_def Unbounded_def, blast)
+
+text{*The class of limit ordinals, @{term Limit}, is closed and unbounded.*}
+theorem Closed_Unbounded_Limit [simp]: "Closed_Unbounded(Limit)"
+apply (simp add: Closed_Unbounded_def Closed_def Unbounded_def Limit_Union, 
+       clarify)
+apply (rule_tac x="i++nat" in exI)  
+apply (blast intro: oadd_lt_self oadd_LimitI Limit_nat Limit_has_0) 
+done
+
+text{*The class of cardinals, @{term Card}, is closed and unbounded.*}
+theorem Closed_Unbounded_Card  [simp]: "Closed_Unbounded(Card)"
+apply (simp add: Closed_Unbounded_def Closed_def Unbounded_def Card_Union)
+apply (blast intro: lt_csucc Card_csucc)
+done
+
+
+subsubsection{*The intersection of any set-indexed family of c.u. classes is
+      c.u.*}
+
+text{*The constructions below come from Kunen, \emph{Set Theory}, page 78.*}
+locale cub_family =
+  fixes P and A
+  fixes next_greater -- "the next ordinal satisfying class @{term A}"
+  fixes sup_greater  -- "sup of those ordinals over all @{term A}"
+  assumes closed:    "a\<in>A ==> Closed(P(a))"
+      and unbounded: "a\<in>A ==> Unbounded(P(a))"
+      and A_non0: "A\<noteq>0"
+  defines "next_greater(a,x) == \<mu>y. x<y \<and> P(a,y)"
+      and "sup_greater(x) == \<Union>a\<in>A. next_greater(a,x)"
+ 
+
+text{*Trivial that the intersection is closed.*}
+lemma (in cub_family) Closed_INT: "Closed(\<lambda>x. \<forall>i\<in>A. P(i,x))"
+by (blast intro: ClosedI ClosedD [OF closed])
+
+text{*All remaining effort goes to show that the intersection is unbounded.*}
+
+lemma (in cub_family) Ord_sup_greater:
+     "Ord(sup_greater(x))"
+by (simp add: sup_greater_def next_greater_def)
+
+lemma (in cub_family) Ord_next_greater:
+     "Ord(next_greater(a,x))"
+by (simp add: next_greater_def Ord_Least)
+
+text{*@{term next_greater} works as expected: it returns a larger value
+and one that belongs to class @{term "P(a)"}. *}
+lemma (in cub_family) next_greater_lemma:
+     "[| Ord(x); a\<in>A |] ==> P(a, next_greater(a,x)) \<and> x < next_greater(a,x)"
+apply (simp add: next_greater_def)
+apply (rule exE [OF UnboundedD [OF unbounded]])
+  apply assumption+
+apply (blast intro: LeastI2 lt_Ord2) 
+done
+
+lemma (in cub_family) next_greater_in_P:
+     "[| Ord(x); a\<in>A |] ==> P(a, next_greater(a,x))"
+by (blast dest: next_greater_lemma)
+
+lemma (in cub_family) next_greater_gt:
+     "[| Ord(x); a\<in>A |] ==> x < next_greater(a,x)"
+by (blast dest: next_greater_lemma)
+
+lemma (in cub_family) sup_greater_gt:
+     "Ord(x) ==> x < sup_greater(x)"
+apply (simp add: sup_greater_def)
+apply (insert A_non0)
+apply (blast intro: UN_upper_lt next_greater_gt Ord_next_greater)
+done
+
+lemma (in cub_family) next_greater_le_sup_greater:
+     "a\<in>A ==> next_greater(a,x) \<le> sup_greater(x)"
+apply (simp add: sup_greater_def) 
+apply (blast intro: UN_upper_le Ord_next_greater)
+done
+
+lemma (in cub_family) omega_sup_greater_eq_UN:
+     "[| Ord(x); a\<in>A |] 
+      ==> sup_greater^\<omega> (x) = 
+          (\<Union>n\<in>nat. next_greater(a, sup_greater^n (x)))"
+apply (simp add: iterates_omega_def)
+apply (rule le_anti_sym)
+apply (rule le_implies_UN_le_UN) 
+apply (blast intro: leI next_greater_gt Ord_iterates Ord_sup_greater)  
+txt{*Opposite bound:
+@{subgoals[display,indent=0,margin=65]}
+*}
+apply (rule UN_least_le) 
+apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)  
+apply (rule_tac a="succ(n)" in UN_upper_le)
+apply (simp_all add: next_greater_le_sup_greater) 
+apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)  
+done
+
+lemma (in cub_family) P_omega_sup_greater:
+     "[| Ord(x); a\<in>A |] ==> P(a, sup_greater^\<omega> (x))"
+apply (simp add: omega_sup_greater_eq_UN)
+apply (rule ClosedD [OF closed]) 
+apply (blast intro: ltD, auto)
+apply (blast intro: Ord_iterates Ord_next_greater Ord_sup_greater)
+apply (blast intro: next_greater_in_P Ord_iterates Ord_sup_greater)
+done
+
+lemma (in cub_family) omega_sup_greater_gt:
+     "Ord(x) ==> x < sup_greater^\<omega> (x)"
+apply (simp add: iterates_omega_def)
+apply (rule UN_upper_lt [of 1], simp_all) 
+ apply (blast intro: sup_greater_gt) 
+apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)
+done
+
+lemma (in cub_family) Unbounded_INT: "Unbounded(\<lambda>x. \<forall>a\<in>A. P(a,x))"
+apply (unfold Unbounded_def)  
+apply (blast intro!: omega_sup_greater_gt P_omega_sup_greater) 
+done
+
+lemma (in cub_family) Closed_Unbounded_INT: 
+     "Closed_Unbounded(\<lambda>x. \<forall>a\<in>A. P(a,x))"
+by (simp add: Closed_Unbounded_def Closed_INT Unbounded_INT)
+
+
+theorem Closed_Unbounded_INT:
+    "(!!a. a\<in>A ==> Closed_Unbounded(P(a)))
+     ==> Closed_Unbounded(\<lambda>x. \<forall>a\<in>A. P(a, x))"
+apply (case_tac "A=0", simp)
+apply (rule cub_family.Closed_Unbounded_INT)
+apply (simp_all add: Closed_Unbounded_def)
+done
+
+lemma Int_iff_INT2:
+     "P(x) \<and> Q(x)  <->  (\<forall>i\<in>2. (i=0 --> P(x)) \<and> (i=1 --> Q(x)))"
+by auto
+
+theorem Closed_Unbounded_Int:
+     "[| Closed_Unbounded(P); Closed_Unbounded(Q) |] 
+      ==> Closed_Unbounded(\<lambda>x. P(x) \<and> Q(x))"
+apply (simp only: Int_iff_INT2)
+apply (rule Closed_Unbounded_INT, auto) 
+done
+
+
+subsection {*Normal Functions*} 
+
+constdefs
+  mono_le_subset :: "(i=>i) => o"
+    "mono_le_subset(M) == \<forall>i j. i\<le>j --> M(i) \<subseteq> M(j)"
+
+  mono_Ord :: "(i=>i) => o"
+    "mono_Ord(F) == \<forall>i j. i<j --> F(i) < F(j)"
+
+  cont_Ord :: "(i=>i) => o"
+    "cont_Ord(F) == \<forall>l. Limit(l) --> F(l) = (\<Union>i<l. F(i))"
+
+  Normal :: "(i=>i) => o"
+    "Normal(F) == mono_Ord(F) \<and> cont_Ord(F)"
+
+
+subsubsection{*Immediate properties of the definitions*}
+
+lemma NormalI:
+     "[|!!i j. i<j ==> F(i) < F(j);  !!l. Limit(l) ==> F(l) = (\<Union>i<l. F(i))|]
+      ==> Normal(F)"
+by (simp add: Normal_def mono_Ord_def cont_Ord_def)
+
+lemma mono_Ord_imp_Ord: "[| Ord(i); mono_Ord(F) |] ==> Ord(F(i))"
+apply (simp add: mono_Ord_def) 
+apply (blast intro: lt_Ord) 
+done
+
+lemma mono_Ord_imp_mono: "[| i<j; mono_Ord(F) |] ==> F(i) < F(j)"
+by (simp add: mono_Ord_def)
+
+lemma Normal_imp_Ord [simp]: "[| Normal(F); Ord(i) |] ==> Ord(F(i))"
+by (simp add: Normal_def mono_Ord_imp_Ord) 
+
+lemma Normal_imp_cont: "[| Normal(F); Limit(l) |] ==> F(l) = (\<Union>i<l. F(i))"
+by (simp add: Normal_def cont_Ord_def)
+
+lemma Normal_imp_mono: "[| i<j; Normal(F) |] ==> F(i) < F(j)"
+by (simp add: Normal_def mono_Ord_def)
+
+lemma Normal_increasing: "[| Ord(i); Normal(F) |] ==> i\<le>F(i)"
+apply (induct i rule: trans_induct3_rule)
+  apply (simp add: subset_imp_le)
+ apply (subgoal_tac "F(x) < F(succ(x))")
+  apply (force intro: lt_trans1)
+ apply (simp add: Normal_def mono_Ord_def)
+apply (subgoal_tac "(\<Union>y<x. y) \<le> (\<Union>y<x. F(y))")
+ apply (simp add: Normal_imp_cont Limit_OUN_eq) 
+apply (blast intro: ltD le_implies_OUN_le_OUN)
+done
+
+
+subsubsection{*The class of fixedpoints is closed and unbounded*}
+
+text{*The proof is from Drake, pages 113--114.*}
+
+lemma mono_Ord_imp_le_subset: "mono_Ord(F) ==> mono_le_subset(F)"
+apply (simp add: mono_le_subset_def, clarify)
+apply (subgoal_tac "F(i)\<le>F(j)", blast dest: le_imp_subset) 
+apply (simp add: le_iff) 
+apply (blast intro: lt_Ord2 mono_Ord_imp_Ord mono_Ord_imp_mono) 
+done
+
+text{*The following equation is taken for granted in any set theory text.*}
+lemma cont_Ord_Union:
+     "[| cont_Ord(F); mono_le_subset(F); X=0 --> F(0)=0; \<forall>x\<in>X. Ord(x) |] 
+      ==> F(Union(X)) = (\<Union>y\<in>X. F(y))"
+apply (frule Ord_set_cases)
+apply (erule disjE, force) 
+apply (thin_tac "X=0 --> ?Q", auto)
+ txt{*The trival case of @{term "\<Union>X \<in> X"}*}
+ apply (rule equalityI, blast intro: Ord_Union_eq_succD) 
+ apply (simp add: mono_le_subset_def UN_subset_iff le_subset_iff) 
+ apply (blast elim: equalityE)
+txt{*The limit case, @{term "Limit(\<Union>X)"}:
+@{subgoals[display,indent=0,margin=65]}
+*}
+apply (simp add: OUN_Union_eq cont_Ord_def)
+apply (rule equalityI) 
+txt{*First inclusion:*}
+ apply (rule UN_least [OF OUN_least])
+ apply (simp add: mono_le_subset_def, blast intro: leI) 
+txt{*Second inclusion:*}
+apply (rule UN_least) 
+apply (frule Union_upper_le, blast, blast intro: Ord_Union)
+apply (erule leE, drule ltD, elim UnionE)
+ apply (simp add: OUnion_def)
+ apply blast+
+done
+
+lemma Normal_Union:
+     "[| X\<noteq>0; \<forall>x\<in>X. Ord(x); Normal(F) |] ==> F(Union(X)) = (\<Union>y\<in>X. F(y))"
+apply (simp add: Normal_def) 
+apply (blast intro: mono_Ord_imp_le_subset cont_Ord_Union) 
+done
+
+lemma Normal_imp_fp_Closed: "Normal(F) ==> Closed(\<lambda>i. F(i) = i)"
+apply (simp add: Closed_def ball_conj_distrib, clarify)
+apply (frule Ord_set_cases)
+apply (auto simp add: Normal_Union)
+done
+
+
+lemma iterates_Normal_increasing:
+     "[| n\<in>nat;  x < F(x);  Normal(F) |] 
+      ==> F^n (x) < F^(succ(n)) (x)"  
+apply (induct n rule: nat_induct)
+apply (simp_all add: Normal_imp_mono)
+done
+
+lemma Ord_iterates_Normal:
+     "[| n\<in>nat;  Normal(F);  Ord(x) |] ==> Ord(F^n (x))"  
+by (simp add: Ord_iterates) 
+
+text{*THIS RESULT IS UNUSED*}
+lemma iterates_omega_Limit:
+     "[| Normal(F);  x < F(x) |] ==> Limit(F^\<omega> (x))"  
+apply (frule lt_Ord) 
+apply (simp add: iterates_omega_def)
+apply (rule increasing_LimitI) 
+   --"this lemma is @{thm increasing_LimitI [no_vars]}"
+ apply (blast intro: UN_upper_lt [of "1"]   Normal_imp_Ord
+                     Ord_UN Ord_iterates lt_imp_0_lt
+                     iterates_Normal_increasing)
+apply clarify
+apply (rule bexI) 
+ apply (blast intro: Ord_in_Ord [OF Ord_iterates_Normal]) 
+apply (rule UN_I, erule nat_succI) 
+apply (blast intro:  iterates_Normal_increasing Ord_iterates_Normal
+                     ltD [OF lt_trans1, OF succ_leI, OF ltI]) 
+done
+
+lemma iterates_omega_fixedpoint:
+     "[| Normal(F); Ord(a) |] ==> F(F^\<omega> (a)) = F^\<omega> (a)" 
+apply (frule Normal_increasing, assumption)
+apply (erule leE) 
+ apply (simp_all add: iterates_omega_triv [OF sym])  (*for subgoal 2*)
+apply (simp add:  iterates_omega_def Normal_Union) 
+apply (rule equalityI, force simp add: nat_succI) 
+txt{*Opposite inclusion:
+@{subgoals[display,indent=0,margin=65]}
+*}
+apply clarify
+apply (rule UN_I, assumption) 
+apply (frule iterates_Normal_increasing, assumption, assumption, simp)
+apply (blast intro: Ord_trans ltD Ord_iterates_Normal Normal_imp_Ord [of F]) 
+done
+
+lemma iterates_omega_increasing:
+     "[| Normal(F); Ord(a) |] ==> a \<le> F^\<omega> (a)"   
+apply (unfold iterates_omega_def)
+apply (rule UN_upper_le [of 0], simp_all)
+done
+
+lemma Normal_imp_fp_Unbounded: "Normal(F) ==> Unbounded(\<lambda>i. F(i) = i)"
+apply (unfold Unbounded_def, clarify)
+apply (rule_tac x="F^\<omega> (succ(i))" in exI)
+apply (simp add: iterates_omega_fixedpoint) 
+apply (blast intro: lt_trans2 [OF _ iterates_omega_increasing])
+done
+
+
+theorem Normal_imp_fp_Closed_Unbounded: 
+     "Normal(F) ==> Closed_Unbounded(\<lambda>i. F(i) = i)"
+by (simp add: Closed_Unbounded_def Normal_imp_fp_Closed
+              Normal_imp_fp_Unbounded)
+
+
+subsubsection{*Function @{text normalize}*}
+
+text{*Function @{text normalize} maps a function @{text F} to a 
+      normal function that bounds it above.  The result is normal if and
+      only if @{text F} is continuous: succ is not bounded above by any 
+      normal function, by @{thm [source] Normal_imp_fp_Unbounded}.
+*}
+constdefs
+  normalize :: "[i=>i, i] => i"
+    "normalize(F,a) == transrec2(a, F(0), \<lambda>x r. F(succ(x)) Un succ(r))"
+
+
+lemma Ord_normalize [simp, intro]:
+     "[| Ord(a); !!x. Ord(x) ==> Ord(F(x)) |] ==> Ord(normalize(F, a))"
+apply (induct a rule: trans_induct3_rule)
+apply (simp_all add: ltD def_transrec2 [OF normalize_def])
+done
+
+lemma normalize_lemma [rule_format]:
+     "[| Ord(b); !!x. Ord(x) ==> Ord(F(x)) |] 
+      ==> \<forall>a. a < b --> normalize(F, a) < normalize(F, b)"
+apply (erule trans_induct3)
+  apply (simp_all add: le_iff def_transrec2 [OF normalize_def])
+ apply clarify
+apply (rule Un_upper2_lt) 
+  apply auto
+ apply (drule spec, drule mp, assumption) 
+ apply (erule leI) 
+apply (drule Limit_has_succ, assumption)
+apply (blast intro!: Ord_normalize intro: OUN_upper_lt ltD lt_Ord)
+done  
+
+lemma normalize_increasing:
+     "[| a < b;  !!x. Ord(x) ==> Ord(F(x)) |] 
+      ==> normalize(F, a) < normalize(F, b)"
+by (blast intro!: normalize_lemma intro: lt_Ord2) 
+
+theorem Normal_normalize:
+     "(!!x. Ord(x) ==> Ord(F(x))) ==> Normal(normalize(F))"
+apply (rule NormalI) 
+apply (blast intro!: normalize_increasing)
+apply (simp add: def_transrec2 [OF normalize_def])
+done
+
+theorem le_normalize:
+     "[| Ord(a); cont_Ord(F); !!x. Ord(x) ==> Ord(F(x)) |] 
+      ==> F(a) \<le> normalize(F,a)"
+apply (erule trans_induct3) 
+apply (simp_all add: def_transrec2 [OF normalize_def])
+apply (simp add: Un_upper1_le) 
+apply (simp add: cont_Ord_def) 
+apply (blast intro: ltD le_implies_OUN_le_OUN)
+done
+
+
+subsection {*The Alephs*}
+text {*This is the well-known transfinite enumeration of the cardinal 
+numbers.*}
+
+constdefs
+  Aleph :: "i => i"
+    "Aleph(a) == transrec2(a, nat, \<lambda>x r. csucc(r))"
+
+syntax (xsymbols)
+  Aleph :: "i => i"   ("\<aleph>_" [90] 90)
+
+lemma Card_Aleph [simp, intro]:
+     "Ord(a) ==> Card(Aleph(a))"
+apply (erule trans_induct3) 
+apply (simp_all add: Card_csucc Card_nat Card_is_Ord
+                     def_transrec2 [OF Aleph_def])
+done
+
+lemma Aleph_lemma [rule_format]:
+     "Ord(b) ==> \<forall>a. a < b --> Aleph(a) < Aleph(b)"
+apply (erule trans_induct3) 
+apply (simp_all add: le_iff def_transrec2 [OF Aleph_def])  
+apply (blast intro: lt_trans lt_csucc Card_is_Ord, clarify)
+apply (drule Limit_has_succ, assumption)
+apply (blast intro: Card_is_Ord Card_Aleph OUN_upper_lt ltD lt_Ord)
+done  
+
+lemma Aleph_increasing:
+     "a < b ==> Aleph(a) < Aleph(b)"
+by (blast intro!: Aleph_lemma intro: lt_Ord2) 
+
+theorem Normal_Aleph: "Normal(Aleph)"
+apply (rule NormalI) 
+apply (blast intro!: Aleph_increasing)
+apply (simp add: def_transrec2 [OF Aleph_def])
+done
+
+end
+
diff -r 74d9144c452c -r 45be08fbdcff src/ZF/Constructible/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/ROOT.ML	Wed Jun 19 11:48:01 2002 +0200
@@ -0,0 +1,4 @@
+use_thy "Reflection";
+use_thy "WFrec";
+use_thy "WF_extras";
+use_thy "L_axioms";
diff -r 74d9144c452c -r 45be08fbdcff src/ZF/Constructible/Reflection.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/Reflection.thy	Wed Jun 19 11:48:01 2002 +0200
@@ -0,0 +1,321 @@
+header {* The Reflection Theorem*}
+
+theory Reflection = Normal:
+
+lemma all_iff_not_ex_not: "(\<forall>x. P(x)) <-> (~ (\<exists>x. ~ P(x)))";
+by blast
+
+lemma ball_iff_not_bex_not: "(\<forall>x\<in>A. P(x)) <-> (~ (\<exists>x\<in>A. ~ P(x)))";
+by blast
+
+text{*From the notes of A. S. Kechris, page 6, and from 
+      Andrzej Mostowski, \emph{Constructible Sets with Applications},
+      North-Holland, 1969, page 23.*}
+
+
+subsection{*Basic Definitions*}
+
+text{*First part: the cumulative hierarchy defining the class @{text M}.  
+To avoid handling multiple arguments, we assume that @{text "Mset(l)"} is
+closed under ordered pairing provided @{text l} is limit.  Possibly this
+could be avoided: the induction hypothesis @{term Cl_reflects} 
+(in locale @{text ex_reflection}) could be weakened to
+@{term "\<forall>y\<in>Mset(a). \<forall>z\<in>Mset(a). P(<y,z>) <-> Q(a,<y,z>)"}, removing most
+uses of @{term Pair_in_Mset}.  But there isn't much point in doing so, since 
+ultimately the @{text ex_reflection} proof is packaged up using the
+predicate @{text Reflects}.
+*}
+locale reflection =
+  fixes Mset and M and Reflects
+  assumes Mset_mono_le : "mono_le_subset(Mset)"
+      and Mset_cont    : "cont_Ord(Mset)"
+      and Pair_in_Mset : "[| x \<in> Mset(a); y \<in> Mset(a); Limit(a) |] 
+                          ==> <x,y> \<in> Mset(a)"
+  defines "M(x) == \<exists>a. Ord(a) \<and> x \<in> Mset(a)"
+      and "Reflects(Cl,P,Q) == Closed_Unbounded(Cl) \<and>
+                              (\<forall>a. Cl(a) --> (\<forall>x\<in>Mset(a). P(x) <-> Q(a,x)))"
+  fixes F0 --{*ordinal for a specific value @{term y}*}
+  fixes FF --{*sup over the whole level, @{term "y\<in>Mset(a)"}*}
+  fixes ClEx --{*Reflecting ordinals for the formula @{term "\<exists>z. P"}*}
+  defines "F0(P,y) == \<mu>b. (\<exists>z. M(z) \<and> P(<y,z>)) --> 
+                               (\<exists>z\<in>Mset(b). P(<y,z>))"
+      and "FF(P)   == \<lambda>a. \<Union>y\<in>Mset(a). F0(P,y)"
+      and "ClEx(P) == \<lambda>a. Limit(a) \<and> normalize(FF(P),a) = a"
+
+lemma (in reflection) Mset_mono: "i\<le>j ==> Mset(i) <= Mset(j)"
+apply (insert Mset_mono_le) 
+apply (simp add: mono_le_subset_def leI) 
+done
+
+subsection{*Easy Cases of the Reflection Theorem*}
+
+theorem (in reflection) Triv_reflection [intro]:
+     "Reflects(Ord, P, \<lambda>a x. P(x))"
+by (simp add: Reflects_def)
+
+theorem (in reflection) Not_reflection [intro]:
+     "Reflects(Cl,P,Q) ==> Reflects(Cl, \<lambda>x. ~P(x), \<lambda>a x. ~Q(a,x))"
+by (simp add: Reflects_def); 
+
+theorem (in reflection) And_reflection [intro]:
+     "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |] 
+      ==> Reflects(\<lambda>a. Cl(a) \<and> C'(a), \<lambda>x. P(x) \<and> P'(x), 
+                                      \<lambda>a x. Q(a,x) \<and> Q'(a,x))"
+by (simp add: Reflects_def Closed_Unbounded_Int, blast)
+
+theorem (in reflection) Or_reflection [intro]:
+     "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |] 
+      ==> Reflects(\<lambda>a. Cl(a) \<and> C'(a), \<lambda>x. P(x) \<or> P'(x), 
+                                      \<lambda>a x. Q(a,x) \<or> Q'(a,x))"
+by (simp add: Reflects_def Closed_Unbounded_Int, blast)
+
+theorem (in reflection) Imp_reflection [intro]:
+     "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |] 
+      ==> Reflects(\<lambda>a. Cl(a) \<and> C'(a), 
+                   \<lambda>x. P(x) --> P'(x), 
+                   \<lambda>a x. Q(a,x) --> Q'(a,x))"
+by (simp add: Reflects_def Closed_Unbounded_Int, blast)
+
+theorem (in reflection) Iff_reflection [intro]:
+     "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |] 
+      ==> Reflects(\<lambda>a. Cl(a) \<and> C'(a), 
+                   \<lambda>x. P(x) <-> P'(x), 
+                   \<lambda>a x. Q(a,x) <-> Q'(a,x))"
+by (simp add: Reflects_def Closed_Unbounded_Int, blast) 
+
+subsection{*Reflection for Existential Quantifiers*}
+
+lemma (in reflection) F0_works:
+     "[| y\<in>Mset(a); Ord(a); M(z); P(<y,z>) |] ==> \<exists>z\<in>Mset(F0(P,y)). P(<y,z>)"
+apply (unfold F0_def M_def, clarify)
+apply (rule LeastI2)
+  apply (blast intro: Mset_mono [THEN subsetD])
+ apply (blast intro: lt_Ord2, blast)
+done
+
+lemma (in reflection) Ord_F0 [intro,simp]: "Ord(F0(P,y))"
+by (simp add: F0_def)
+
+lemma (in reflection) Ord_FF [intro,simp]: "Ord(FF(P,y))"
+by (simp add: FF_def)
+
+lemma (in reflection) cont_Ord_FF: "cont_Ord(FF(P))"
+apply (insert Mset_cont)
+apply (simp add: cont_Ord_def FF_def, blast)
+done
+
+text{*Recall that @{term F0} depends upon @{term "y\<in>Mset(a)"}, 
+while @{term FF} depends only upon @{term a}. *}
+lemma (in reflection) FF_works:
+     "[| M(z); y\<in>Mset(a); P(<y,z>); Ord(a) |] ==> \<exists>z\<in>Mset(FF(P,a)). P(<y,z>)"
+apply (simp add: FF_def)
+apply (simp_all add: cont_Ord_Union [of concl: Mset] 
+                     Mset_cont Mset_mono_le not_emptyI Ord_F0)
+apply (blast intro: F0_works)  
+done
+
+lemma (in reflection) FFN_works:
+     "[| M(z); y\<in>Mset(a); P(<y,z>); Ord(a) |] 
+      ==> \<exists>z\<in>Mset(normalize(FF(P),a)). P(<y,z>)"
+apply (drule FF_works [of concl: P], assumption+) 
+apply (blast intro: cont_Ord_FF le_normalize [THEN Mset_mono, THEN subsetD])
+done
+
+
+text{*Locale for the induction hypothesis*}
+
+locale ex_reflection = reflection +
+  fixes P  --"the original formula"
+  fixes Q  --"the reflected formula"
+  fixes Cl --"the class of reflecting ordinals"
+  assumes Cl_reflects: "[| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) <-> Q(a,x)"
+
+lemma (in ex_reflection) ClEx_downward:
+     "[| M(z); y\<in>Mset(a); P(<y,z>); Cl(a); ClEx(P,a) |] 
+      ==> \<exists>z\<in>Mset(a). Q(a,<y,z>)"
+apply (simp add: ClEx_def, clarify) 
+apply (frule Limit_is_Ord) 
+apply (frule FFN_works [of concl: P], assumption+) 
+apply (drule Cl_reflects, assumption+) 
+apply (auto simp add: Limit_is_Ord Pair_in_Mset)
+done
+
+lemma (in ex_reflection) ClEx_upward:
+     "[| z\<in>Mset(a); y\<in>Mset(a); Q(a,<y,z>); Cl(a); ClEx(P,a) |] 
+      ==> \<exists>z. M(z) \<and> P(<y,z>)"
+apply (simp add: ClEx_def M_def)
+apply (blast dest: Cl_reflects
+	     intro: Limit_is_Ord Pair_in_Mset)
+done
+
+text{*Class @{text ClEx} indeed consists of reflecting ordinals...*}
+lemma (in ex_reflection) ZF_ClEx_iff:
+     "[| y\<in>Mset(a); Cl(a); ClEx(P,a) |] 
+      ==> (\<exists>z. M(z) \<and> P(<y,z>)) <-> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
+by (blast intro: dest: ClEx_downward ClEx_upward) 
+
+text{*...and it is closed and unbounded*}
+lemma (in ex_reflection) ZF_Closed_Unbounded_ClEx:
+     "Closed_Unbounded(ClEx(P))"
+apply (simp add: ClEx_def)
+apply (fast intro: Closed_Unbounded_Int Normal_imp_fp_Closed_Unbounded
+                   Closed_Unbounded_Limit Normal_normalize)
+done
+
+text{*The same two theorems, exported to locale @{text reflection}.*}
+
+text{*Class @{text ClEx} indeed consists of reflecting ordinals...*}
+lemma (in reflection) ClEx_iff:
+     "[| y\<in>Mset(a); Cl(a); ClEx(P,a);
+        !!a. [| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) <-> Q(a,x) |] 
+      ==> (\<exists>z. M(z) \<and> P(<y,z>)) <-> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
+apply (unfold ClEx_def FF_def F0_def M_def)
+apply (rule Reflection.ZF_ClEx_iff [of Mset Cl], 
+       simp_all add: Mset_mono_le Mset_cont Pair_in_Mset)
+done
+
+lemma (in reflection) Closed_Unbounded_ClEx:
+     "(!!a. [| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) <-> Q(a,x))
+      ==> Closed_Unbounded(ClEx(P))"
+apply (unfold ClEx_def FF_def F0_def M_def)
+apply (rule Reflection.ZF_Closed_Unbounded_ClEx, 
+       simp_all add: Mset_mono_le Mset_cont Pair_in_Mset) 
+done
+
+lemma (in reflection) Ex_reflection_0:
+     "Reflects(Cl,P0,Q0) 
+      ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(P0,a), 
+                   \<lambda>x. \<exists>z. M(z) \<and> P0(<x,z>), 
+                   \<lambda>a x. \<exists>z\<in>Mset(a). Q0(a,<x,z>))" 
+apply (simp add: Reflects_def) 
+apply (intro conjI Closed_Unbounded_Int)
+  apply blast 
+ apply (rule reflection.Closed_Unbounded_ClEx [of Cl P0 Q0], blast, clarify) 
+apply (rule_tac Cl=Cl in  ClEx_iff, assumption+, blast) 
+done
+
+lemma (in reflection) All_reflection_0:
+     "Reflects(Cl,P0,Q0) 
+      ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x.~P0(x), a), 
+                   \<lambda>x. \<forall>z. M(z) --> P0(<x,z>), 
+                   \<lambda>a x. \<forall>z\<in>Mset(a). Q0(a,<x,z>))" 
+apply (simp only: all_iff_not_ex_not ball_iff_not_bex_not) 
+apply (rule Not_reflection, drule Not_reflection, simp) 
+apply (erule Ex_reflection_0)
+done
+
+theorem (in reflection) Ex_reflection [intro]:
+     "Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))) 
+      ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x. P(fst(x),snd(x)), a), 
+                   \<lambda>x. \<exists>z. M(z) \<and> P(x,z), 
+                   \<lambda>a x. \<exists>z\<in>Mset(a). Q(a,x,z))"
+by (rule Ex_reflection_0 [of _ " \<lambda>x. P(fst(x),snd(x))" 
+                               "\<lambda>a x. Q(a,fst(x),snd(x))", simplified])
+
+theorem (in reflection) All_reflection [intro]:
+     "Reflects(Cl,  \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
+      ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x. ~P(fst(x),snd(x)), a), 
+                   \<lambda>x. \<forall>z. M(z) --> P(x,z), 
+                   \<lambda>a x. \<forall>z\<in>Mset(a). Q(a,x,z))" 
+by (rule All_reflection_0 [of _ "\<lambda>x. P(fst(x),snd(x))" 
+                                "\<lambda>a x. Q(a,fst(x),snd(x))", simplified])
+
+text{*No point considering bounded quantifiers, where reflection is trivial.*}
+
+
+subsection{*Simple Examples of Reflection*}
+
+text{*Example 1: reflecting a simple formula.  The reflecting class is first
+given as the variable @{text ?Cl} and later retrieved from the final 
+proof state.*}
+lemma (in reflection) 
+     "Reflects(?Cl,
+               \<lambda>x. \<exists>y. M(y) \<and> x \<in> y, 
+               \<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)"
+by fast
+
+text{*Problem here: there needs to be a conjunction (class intersection)
+in the class of reflecting ordinals.  The @{term "Ord(a)"} is redundant,
+though harmless.*}
+lemma (in reflection) 
+     "Reflects(\<lambda>a. Ord(a) \<and> ClEx(\<lambda>x. fst(x) \<in> snd(x), a),   
+               \<lambda>x. \<exists>y. M(y) \<and> x \<in> y, 
+               \<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)" 
+by fast
+
+
+text{*Example 2*}
+lemma (in reflection) 
+     "Reflects(?Cl,
+               \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y), 
+               \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)" 
+by fast
+
+text{*Example 2'.  We give the reflecting class explicitly. *}
+lemma (in reflection) 
+  "Reflects
+    (\<lambda>a. (Ord(a) \<and>
+          ClEx(\<lambda>x. ~ (snd(x) \<subseteq> fst(fst(x)) --> snd(x) \<in> snd(fst(x))), a)) \<and>
+          ClEx(\<lambda>x. \<forall>z. M(z) --> z \<subseteq> fst(x) --> z \<in> snd(x), a),
+	    \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y), 
+	    \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)" 
+by fast
+
+text{*Example 2''.  We expand the subset relation.*}
+lemma (in reflection) 
+  "Reflects(?Cl,
+        \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> (\<forall>w. M(w) --> w\<in>z --> w\<in>x) --> z\<in>y),
+        \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). (\<forall>w\<in>Mset(a). w\<in>z --> w\<in>x) --> z\<in>y)"
+by fast
+
+text{*Example 2'''.  Single-step version, to reveal the reflecting class.*}
+lemma (in reflection) 
+     "Reflects(?Cl,
+               \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y), 
+               \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)" 
+apply (rule Ex_reflection) 
+txt{*
+@{goals[display,indent=0,margin=60]}
+*}
+apply (rule All_reflection) 
+txt{*
+@{goals[display,indent=0,margin=60]}
+*}
+apply (rule Triv_reflection) 
+txt{*
+@{goals[display,indent=0,margin=60]}
+*}
+done
+
+text{*Example 3.  Warning: the following examples make sense only
+if @{term P} is quantifier-free, since it is not being relativized.*}
+lemma (in reflection) 
+     "Reflects(?Cl,
+               \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> z \<in> y <-> z \<in> x \<and> P(z)), 
+               \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<in> y <-> z \<in> x \<and> P(z))"
+by fast
+
+text{*Example 3'*}
+lemma (in reflection) 
+     "Reflects(?Cl,
+               \<lambda>x. \<exists>y. M(y) \<and> y = Collect(x,P),
+               \<lambda>a x. \<exists>y\<in>Mset(a). y = Collect(x,P))";
+by fast
+
+text{*Example 3''*}
+lemma (in reflection) 
+     "Reflects(?Cl,
+               \<lambda>x. \<exists>y. M(y) \<and> y = Replace(x,P),
+               \<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))";
+by fast
+
+text{*Example 4: Axiom of Choice.  Possibly wrong, since @{text \<Pi>} needs
+to be relativized.*}
+lemma (in reflection) 
+     "Reflects(?Cl,
+               \<lambda>A. 0\<notin>A --> (\<exists>f. M(f) \<and> f \<in> (\<Pi>X \<in> A. X)),
+               \<lambda>a A. 0\<notin>A --> (\<exists>f\<in>Mset(a). f \<in> (\<Pi>X \<in> A. X)))"
+by fast
+
+end
+
diff -r 74d9144c452c -r 45be08fbdcff src/ZF/Constructible/Relative.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/Relative.thy	Wed Jun 19 11:48:01 2002 +0200
@@ -0,0 +1,956 @@
+header {*Relativization and Absoluteness*}
+
+theory Relative = Main:
+
+subsection{* Relativized versions of standard set-theoretic concepts *}
+
+constdefs
+  empty :: "[i=>o,i] => o"
+    "empty(M,z) == \<forall>x. M(x) --> x \<notin> z"
+
+  subset :: "[i=>o,i,i] => o"
+    "subset(M,A,B) == \<forall>x\<in>A. M(x) --> x \<in> B"
+
+  upair :: "[i=>o,i,i,i] => o"
+    "upair(M,a,b,z) == a \<in> z & b \<in> z & (\<forall>x\<in>z. M(x) --> x = a | x = b)"
+
+  pair :: "[i=>o,i,i,i] => o"
+    "pair(M,a,b,z) == \<exists>x. M(x) & upair(M,a,a,x) & 
+                          (\<exists>y. M(y) & upair(M,a,b,y) & upair(M,x,y,z))"
+
+  successor :: "[i=>o,i,i] => o"
+    "successor(M,a,z) == \<exists>x. M(x) & upair(M,a,a,x) & union(M,x,a,z)"
+
+  powerset :: "[i=>o,i,i] => o"
+    "powerset(M,A,z) == \<forall>x. M(x) --> (x \<in> z <-> subset(M,x,A))"
+
+  union :: "[i=>o,i,i,i] => o"
+    "union(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a | x \<in> b)"
+
+  inter :: "[i=>o,i,i,i] => o"
+    "inter(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a & x \<in> b)"
+
+  setdiff :: "[i=>o,i,i,i] => o"
+    "setdiff(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a & x \<notin> b)"
+
+  big_union :: "[i=>o,i,i] => o"
+    "big_union(M,A,z) == \<forall>x. M(x) --> (x \<in> z <-> (\<exists>y\<in>A. M(y) & x \<in> y))"
+
+  big_inter :: "[i=>o,i,i] => o"
+    "big_inter(M,A,z) == 
+             (A=0 --> z=0) &
+	     (A\<noteq>0 --> (\<forall>x. M(x) --> (x \<in> z <-> (\<forall>y\<in>A. M(y) --> x \<in> y))))"
+
+  cartprod :: "[i=>o,i,i,i] => o"
+    "cartprod(M,A,B,z) == 
+	\<forall>u. M(u) --> (u \<in> z <-> (\<exists>x\<in>A. M(x) & (\<exists>y\<in>B. M(y) & pair(M,x,y,u))))"
+
+  is_converse :: "[i=>o,i,i] => o"
+    "is_converse(M,r,z) == 
+	\<forall>x. M(x) --> 
+            (x \<in> z <-> 
+             (\<exists>w\<in>r. M(w) & 
+              (\<exists>u v. M(u) & M(v) & pair(M,u,v,w) & pair(M,v,u,x))))"
+
+  pre_image :: "[i=>o,i,i,i] => o"
+    "pre_image(M,r,A,z) == 
+	\<forall>x. M(x) --> (x \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>y\<in>A. M(y) & pair(M,x,y,w))))"
+
+  is_domain :: "[i=>o,i,i] => o"
+    "is_domain(M,r,z) == 
+	\<forall>x. M(x) --> (x \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>y. M(y) & pair(M,x,y,w))))"
+
+  image :: "[i=>o,i,i,i] => o"
+    "image(M,r,A,z) == 
+        \<forall>y. M(y) --> (y \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>x\<in>A. M(x) & pair(M,x,y,w))))"
+
+  is_range :: "[i=>o,i,i] => o"
+    --{*the cleaner 
+      @{term "\<exists>r'. M(r') & is_converse(M,r,r') & is_domain(M,r',z)"}
+      unfortunately needs an instance of separation in order to prove 
+        @{term "M(converse(r))"}.*}
+    "is_range(M,r,z) == 
+	\<forall>y. M(y) --> (y \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>x. M(x) & pair(M,x,y,w))))"
+
+  is_relation :: "[i=>o,i] => o"
+    "is_relation(M,r) == 
+        (\<forall>z\<in>r. M(z) --> (\<exists>x y. M(x) & M(y) & pair(M,x,y,z)))"
+
+  is_function :: "[i=>o,i] => o"
+    "is_function(M,r) == 
+	(\<forall>x y y' p p'. M(x) --> M(y) --> M(y') --> M(p) --> M(p') --> 
+                      pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r --> 
+                      y=y')"
+
+  fun_apply :: "[i=>o,i,i,i] => o"
+    "fun_apply(M,f,x,y) == 
+	(\<forall>y'. M(y') --> ((\<exists>u\<in>f. M(u) & pair(M,x,y',u)) <-> y=y'))"
+
+  typed_function :: "[i=>o,i,i,i] => o"
+    "typed_function(M,A,B,r) == 
+        is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
+        (\<forall>u\<in>r. M(u) --> (\<forall>x y. M(x) & M(y) & pair(M,x,y,u) --> y\<in>B))"
+
+  injection :: "[i=>o,i,i,i] => o"
+    "injection(M,A,B,f) == 
+	typed_function(M,A,B,f) &
+        (\<forall>x x' y p p'. M(x) --> M(x') --> M(y) --> M(p) --> M(p') --> 
+                      pair(M,x,y,p) --> pair(M,x',y,p') --> p\<in>f --> p'\<in>f --> 
+                      x=x')"
+
+  surjection :: "[i=>o,i,i,i] => o"
+    "surjection(M,A,B,f) == 
+        typed_function(M,A,B,f) &
+        (\<forall>y\<in>B. M(y) --> (\<exists>x\<in>A. M(x) & fun_apply(M,f,x,y)))"
+
+  bijection :: "[i=>o,i,i,i] => o"
+    "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)"
+
+  restriction :: "[i=>o,i,i,i] => o"
+    "restriction(M,r,A,z) == 
+	\<forall>x. M(x) --> 
+            (x \<in> z <-> 
+             (x \<in> r & (\<exists>u\<in>A. M(u) & (\<exists>v. M(v) & pair(M,u,v,x)))))"
+
+  transitive_set :: "[i=>o,i] => o"
+    "transitive_set(M,a) == \<forall>x\<in>a. M(x) --> subset(M,x,a)"
+
+  ordinal :: "[i=>o,i] => o"
+     --{*an ordinal is a transitive set of transitive sets*}
+    "ordinal(M,a) == transitive_set(M,a) & (\<forall>x\<in>a. M(x) --> transitive_set(M,x))"
+
+  limit_ordinal :: "[i=>o,i] => o"
+    --{*a limit ordinal is a non-empty, successor-closed ordinal*}
+    "limit_ordinal(M,a) == 
+	ordinal(M,a) & ~ empty(M,a) & 
+        (\<forall>x\<in>a. M(x) --> (\<exists>y\<in>a. M(y) & successor(M,x,y)))"
+
+  successor_ordinal :: "[i=>o,i] => o"
+    --{*a successor ordinal is any ordinal that is neither empty nor limit*}
+    "successor_ordinal(M,a) == 
+	ordinal(M,a) & ~ empty(M,a) & ~ limit_ordinal(M,a)"
+
+  finite_ordinal :: "[i=>o,i] => o"
+    --{*an ordinal is finite if neither it nor any of its elements are limit*}
+    "finite_ordinal(M,a) == 
+	ordinal(M,a) & ~ limit_ordinal(M,a) & 
+        (\<forall>x\<in>a. M(x) --> ~ limit_ordinal(M,x))"
+
+  omega :: "[i=>o,i] => o"
+    --{*omega is a limit ordinal none of whose elements are limit*}
+    "omega(M,a) == limit_ordinal(M,a) & (\<forall>x\<in>a. M(x) --> ~ limit_ordinal(M,x))"
+
+  number1 :: "[i=>o,i] => o"
+    "number1(M,a) == (\<exists>x. M(x) & empty(M,x) & successor(M,x,a))"
+
+  number2 :: "[i=>o,i] => o"
+    "number2(M,a) == (\<exists>x. M(x) & number1(M,x) & successor(M,x,a))"
+
+  number3 :: "[i=>o,i] => o"
+    "number3(M,a) == (\<exists>x. M(x) & number2(M,x) & successor(M,x,a))"
+
+
+subsection {*The relativized ZF axioms*}
+constdefs
+
+  extensionality :: "(i=>o) => o"
+    "extensionality(M) == 
+	\<forall>x y. M(x) --> M(y) --> (\<forall>z. M(z) --> (z \<in> x <-> z \<in> y)) --> x=y"
+
+  separation :: "[i=>o, i=>o] => o"
+    --{*Big problem: the formula @{text P} should only involve parameters
+        belonging to @{text M}.  Don't see how to enforce that.*}
+    "separation(M,P) == 
+	\<forall>z. M(z) --> (\<exists>y. M(y) & (\<forall>x. M(x) --> (x \<in> y <-> x \<in> z & P(x))))"
+
+  upair_ax :: "(i=>o) => o"
+    "upair_ax(M) == \<forall>x y. M(x) --> M(y) --> (\<exists>z. M(z) & upair(M,x,y,z))"
+
+  Union_ax :: "(i=>o) => o"
+    "Union_ax(M) == \<forall>x. M(x) --> (\<exists>z. M(z) & big_union(M,x,z))"
+
+  power_ax :: "(i=>o) => o"
+    "power_ax(M) == \<forall>x. M(x) --> (\<exists>z. M(z) & powerset(M,x,z))"
+
+  univalent :: "[i=>o, i, [i,i]=>o] => o"
+    "univalent(M,A,P) == 
+	(\<forall>x\<in>A. M(x) --> (\<forall>y z. M(y) --> M(z) --> P(x,y) & P(x,z) --> y=z))"
+
+  replacement :: "[i=>o, [i,i]=>o] => o"
+    "replacement(M,P) == 
+      \<forall>A. M(A) --> univalent(M,A,P) -->
+      (\<exists>Y. M(Y) & (\<forall>b. M(b) --> ((\<exists>x\<in>A. M(x) & P(x,b)) --> b \<in> Y)))"
+
+  strong_replacement :: "[i=>o, [i,i]=>o] => o"
+    "strong_replacement(M,P) == 
+      \<forall>A. M(A) --> univalent(M,A,P) -->
+      (\<exists>Y. M(Y) & (\<forall>b. M(b) --> (b \<in> Y <-> (\<exists>x\<in>A. M(x) & P(x,b)))))"
+
+  foundation_ax :: "(i=>o) => o"
+    "foundation_ax(M) == 
+	\<forall>x. M(x) --> (\<exists>y\<in>x. M(y))
+                 --> (\<exists>y\<in>x. M(y) & ~(\<exists>z\<in>x. M(z) & z \<in> y))"
+
+
+subsection{*A trivial consistency proof for $V_\omega$ *}
+
+text{*We prove that $V_\omega$ 
+      (or @{text univ} in Isabelle) satisfies some ZF axioms.
+     Kunen, Theorem IV 3.13, page 123.*}
+
+lemma univ0_downwards_mem: "[| y \<in> x; x \<in> univ(0) |] ==> y \<in> univ(0)"
+apply (insert Transset_univ [OF Transset_0])  
+apply (simp add: Transset_def, blast) 
+done
+
+lemma univ0_Ball_abs [simp]: 
+     "A \<in> univ(0) ==> (\<forall>x\<in>A. x \<in> univ(0) --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
+by (blast intro: univ0_downwards_mem) 
+
+lemma univ0_Bex_abs [simp]: 
+     "A \<in> univ(0) ==> (\<exists>x\<in>A. x \<in> univ(0) & P(x)) <-> (\<exists>x\<in>A. P(x))" 
+by (blast intro: univ0_downwards_mem) 
+
+text{*Congruence rule for separation: can assume the variable is in @{text M}*}
+lemma [cong]:
+     "(!!x. M(x) ==> P(x) <-> P'(x)) ==> separation(M,P) <-> separation(M,P')"
+by (simp add: separation_def) 
+
+text{*Congruence rules for replacement*}
+lemma [cong]:
+     "[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
+      ==> univalent(M,A,P) <-> univalent(M,A',P')"
+by (simp add: univalent_def) 
+
+lemma [cong]:
+     "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
+      ==> strong_replacement(M,P) <-> strong_replacement(M,P')" 
+by (simp add: strong_replacement_def) 
+
+text{*The extensionality axiom*}
+lemma "extensionality(\<lambda>x. x \<in> univ(0))"
+apply (simp add: extensionality_def)
+apply (blast intro: univ0_downwards_mem) 
+done
+
+text{*The separation axiom requires some lemmas*}
+lemma Collect_in_Vfrom:
+     "[| X \<in> Vfrom(A,j);  Transset(A) |] ==> Collect(X,P) \<in> Vfrom(A, succ(j))"
+apply (drule Transset_Vfrom)
+apply (rule subset_mem_Vfrom)
+apply (unfold Transset_def, blast)
+done
+
+lemma Collect_in_VLimit:
+     "[| X \<in> Vfrom(A,i);  Limit(i);  Transset(A) |] 
+      ==> Collect(X,P) \<in> Vfrom(A,i)"
+apply (rule Limit_VfromE, assumption+)
+apply (blast intro: Limit_has_succ VfromI Collect_in_Vfrom)
+done
+
+lemma Collect_in_univ:
+     "[| X \<in> univ(A);  Transset(A) |] ==> Collect(X,P) \<in> univ(A)"
+by (simp add: univ_def Collect_in_VLimit Limit_nat)
+
+lemma "separation(\<lambda>x. x \<in> univ(0), P)"
+apply (simp add: separation_def)
+apply (blast intro: Collect_in_univ Transset_0) 
+done
+
+text{*Unordered pairing axiom*}
+lemma "upair_ax(\<lambda>x. x \<in> univ(0))"
+apply (simp add: upair_ax_def upair_def)  
+apply (blast intro: doubleton_in_univ) 
+done
+
+text{*Union axiom*}
+lemma "Union_ax(\<lambda>x. x \<in> univ(0))"  
+apply (simp add: Union_ax_def big_union_def)  
+apply (blast intro: Union_in_univ Transset_0 univ0_downwards_mem) 
+done
+
+text{*Powerset axiom*}
+
+lemma Pow_in_univ:
+     "[| X \<in> univ(A);  Transset(A) |] ==> Pow(X) \<in> univ(A)"
+apply (simp add: univ_def Pow_in_VLimit Limit_nat)
+done
+
+lemma "power_ax(\<lambda>x. x \<in> univ(0))"  
+apply (simp add: power_ax_def powerset_def subset_def)  
+apply (blast intro: Pow_in_univ Transset_0 univ0_downwards_mem) 
+done
+
+text{*Foundation axiom*}
+lemma "foundation_ax(\<lambda>x. x \<in> univ(0))"  
+apply (simp add: foundation_ax_def, clarify)
+apply (cut_tac A=x in foundation, blast) 
+done
+
+lemma "replacement(\<lambda>x. x \<in> univ(0), P)"  
+apply (simp add: replacement_def, clarify) 
+oops
+text{*no idea: maybe prove by induction on the rank of A?*}
+
+text{*Still missing: Replacement, Choice*}
+
+subsection{*lemmas needed to reduce some set constructions to instances
+      of Separation*}
+
+lemma image_iff_Collect: "r `` A = {y \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>x\<in>A. p=<x,y>}"
+apply (rule equalityI, auto) 
+apply (simp add: Pair_def, blast) 
+done
+
+lemma vimage_iff_Collect:
+     "r -`` A = {x \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>y\<in>A. p=<x,y>}"
+apply (rule equalityI, auto) 
+apply (simp add: Pair_def, blast) 
+done
+
+text{*These two lemmas lets us prove @{text domain_closed} and 
+      @{text range_closed} without new instances of separation*}
+
+lemma domain_eq_vimage: "domain(r) = r -`` Union(Union(r))"
+apply (rule equalityI, auto)
+apply (rule vimageI, assumption)
+apply (simp add: Pair_def, blast) 
+done
+
+lemma range_eq_image: "range(r) = r `` Union(Union(r))"
+apply (rule equalityI, auto)
+apply (rule imageI, assumption)
+apply (simp add: Pair_def, blast) 
+done
+
+lemma replacementD:
+    "[| replacement(M,P); M(A);  univalent(M,A,P) |]
+     ==> \<exists>Y. M(Y) & (\<forall>b. M(b) --> ((\<exists>x\<in>A. M(x) & P(x,b)) --> b \<in> Y))"
+by (simp add: replacement_def) 
+
+lemma strong_replacementD:
+    "[| strong_replacement(M,P); M(A);  univalent(M,A,P) |]
+     ==> \<exists>Y. M(Y) & (\<forall>b. M(b) --> (b \<in> Y <-> (\<exists>x\<in>A. M(x) & P(x,b))))"
+by (simp add: strong_replacement_def) 
+
+lemma separationD:
+    "[| separation(M,P); M(z) |]
+     ==> \<exists>y. M(y) & (\<forall>x. M(x) --> (x \<in> y <-> x \<in> z & P(x)))"
+by (simp add: separation_def) 
+
+
+text{*More constants, for order types*}
+constdefs
+
+  order_isomorphism :: "[i=>o,i,i,i,i,i] => o"
+    "order_isomorphism(M,A,r,B,s,f) == 
+        bijection(M,A,B,f) & 
+        (\<forall>x\<in>A. \<forall>y\<in>A. \<forall>p fx fy q. 
+            M(x) --> M(y) --> M(p) --> M(fx) --> M(fy) --> M(q) --> 
+            pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) --> 
+            pair(M,fx,fy,q) --> (p\<in>r <-> q\<in>s))"
+
+
+  pred_set :: "[i=>o,i,i,i,i] => o"
+    "pred_set(M,A,x,r,B) == 
+	\<forall>y. M(y) --> (y \<in> B <-> (\<exists>p\<in>r. M(p) & y \<in> A & pair(M,y,x,p)))"
+
+  membership :: "[i=>o,i,i] => o" --{*membership relation*}
+    "membership(M,A,r) == 
+	\<forall>p. M(p) --> 
+             (p \<in> r <-> (\<exists>x\<in>A. \<exists>y\<in>A. M(x) & M(y) & x\<in>y & pair(M,x,y,p)))"
+
+
+subsection{*Absoluteness for a transitive class model*}
+
+text{*The class M is assumed to be transitive and to satisfy some
+      relativized ZF axioms*}
+locale M_axioms =
+  fixes M
+  assumes transM:           "[| y\<in>x; M(x) |] ==> M(y)"
+      and nonempty [simp]:  "M(0)"
+      and upair_ax:	    "upair_ax(M)"
+      and Union_ax:	    "Union_ax(M)"
+      and power_ax:         "power_ax(M)"
+      and replacement:      "replacement(M,P)"
+  and Inter_separation:
+     "M(A) ==> separation(M, \<lambda>x. \<forall>y\<in>A. M(y) --> x\<in>y)"
+  and cartprod_separation:
+     "[| M(A); M(B) |] 
+      ==> separation(M, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. M(x) & M(y) & pair(M,x,y,z))"
+  and image_separation:
+     "[| M(A); M(r) |] 
+      ==> separation(M, \<lambda>y. \<exists>p\<in>r. M(p) & (\<exists>x\<in>A. M(x) & pair(M,x,y,p)))"
+  and vimage_separation:
+     "[| M(A); M(r) |] 
+      ==> separation(M, \<lambda>x. \<exists>p\<in>r. M(p) & (\<exists>y\<in>A. M(x) & pair(M,x,y,p)))"
+  and converse_separation:
+     "M(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r. M(p) & (\<exists>x y. M(x) & M(y) & 
+				     pair(M,x,y,p) & pair(M,y,x,z)))"
+  and restrict_separation:
+     "M(A) 
+      ==> separation(M, \<lambda>z. \<exists>x\<in>A. M(x) & (\<exists>y. M(y) & pair(M,x,y,z)))"
+  and comp_separation:
+     "[| M(r); M(s) |]
+      ==> separation(M, \<lambda>xz. \<exists>x y z. M(x) & M(y) & M(z) &
+			   (\<exists>xy\<in>s. \<exists>yz\<in>r. M(xy) & M(yz) & 
+		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz)))"
+  and pred_separation:
+     "[| M(r); M(x) |] ==> separation(M, \<lambda>y. \<exists>p\<in>r. M(p) & pair(M,y,x,p))"
+  and Memrel_separation:
+     "separation(M, \<lambda>z. \<exists>x y. M(x) & M(y) & pair(M,x,y,z) \<and> x \<in> y)"
+  and obase_separation:
+     --{*part of the order type formalization*}
+     "[| M(A); M(r) |] 
+      ==> separation(M, \<lambda>a. \<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) & 
+	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
+	     order_isomorphism(M,par,r,x,mx,g))"
+  and well_ord_iso_separation:
+     "[| M(A); M(f); M(r) |] 
+      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y. M(y) \<and> (\<exists>p. M(p) \<and> 
+		     fun_apply(M,f,x,y) \<and> pair(M,y,x,p) \<and> p \<in> r)))"
+  and obase_equals_separation:
+     "[| M(A); M(r) |] 
+      ==> separation
+      (M, \<lambda>x. x\<in>A --> ~(\<exists>y. M(y) & (\<exists>g. M(g) &
+	      ordinal(M,y) & (\<exists>my pxr. M(my) & M(pxr) &
+	      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
+	      order_isomorphism(M,pxr,r,y,my,g)))))"
+  and is_recfun_separation:
+     --{*for well-founded recursion.  NEEDS RELATIVIZATION*}
+     "[| M(A); M(f); M(g); M(a); M(b) |] 
+     ==> separation(M, \<lambda>x. x \<in> A --> \<langle>x,a\<rangle> \<in> r \<and> \<langle>x,b\<rangle> \<in> r \<and> f`x \<noteq> g`x)"
+  and omap_replacement:
+     "[| M(A); M(r) |] 
+      ==> strong_replacement(M,
+             \<lambda>a z. \<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) &
+	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
+	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
+
+lemma (in M_axioms) Ball_abs [simp]: 
+     "M(A) ==> (\<forall>x\<in>A. M(x) --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
+by (blast intro: transM) 
+
+lemma (in M_axioms) Bex_abs [simp]: 
+     "M(A) ==> (\<exists>x\<in>A. M(x) & P(x)) <-> (\<exists>x\<in>A. P(x))" 
+by (blast intro: transM) 
+
+lemma (in M_axioms) Ball_iff_equiv: 
+     "M(A) ==> (\<forall>x. M(x) --> (x\<in>A <-> P(x))) <-> 
+               (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)" 
+by (blast intro: transM)
+
+lemma (in M_axioms) empty_abs [simp]: 
+     "M(z) ==> empty(M,z) <-> z=0"
+apply (simp add: empty_def)
+apply (blast intro: transM) 
+done
+
+lemma (in M_axioms) subset_abs [simp]: 
+     "M(A) ==> subset(M,A,B) <-> A \<subseteq> B"
+apply (simp add: subset_def) 
+apply (blast intro: transM) 
+done
+
+lemma (in M_axioms) upair_abs [simp]: 
+     "M(z) ==> upair(M,a,b,z) <-> z={a,b}"
+apply (simp add: upair_def) 
+apply (blast intro: transM) 
+done
+
+lemma (in M_axioms) upair_in_M_iff [iff]:
+     "M({a,b}) <-> M(a) & M(b)"
+apply (insert upair_ax, simp add: upair_ax_def) 
+apply (blast intro: transM) 
+done
+
+lemma (in M_axioms) singleton_in_M_iff [iff]:
+     "M({a}) <-> M(a)"
+by (insert upair_in_M_iff [of a a], simp) 
+
+lemma (in M_axioms) pair_abs [simp]: 
+     "M(z) ==> pair(M,a,b,z) <-> z=<a,b>"
+apply (simp add: pair_def ZF.Pair_def)
+apply (blast intro: transM) 
+done
+
+lemma (in M_axioms) pair_in_M_iff [iff]:
+     "M(<a,b>) <-> M(a) & M(b)"
+by (simp add: ZF.Pair_def)
+
+lemma (in M_axioms) pair_components_in_M:
+     "[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"
+apply (simp add: Pair_def)
+apply (blast dest: transM) 
+done
+
+lemma (in M_axioms) cartprod_abs [simp]: 
+     "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B"
+apply (simp add: cartprod_def)
+apply (rule iffI) 
+apply (blast intro!: equalityI intro: transM dest!: spec) 
+apply (blast dest: transM) 
+done
+
+lemma (in M_axioms) union_abs [simp]: 
+     "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b"
+apply (simp add: union_def) 
+apply (blast intro: transM) 
+done
+
+lemma (in M_axioms) inter_abs [simp]: 
+     "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) <-> z = a Int b"
+apply (simp add: inter_def) 
+apply (blast intro: transM) 
+done
+
+lemma (in M_axioms) setdiff_abs [simp]: 
+     "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) <-> z = a-b"
+apply (simp add: setdiff_def) 
+apply (blast intro: transM) 
+done
+
+lemma (in M_axioms) Union_abs [simp]: 
+     "[| M(A); M(z) |] ==> big_union(M,A,z) <-> z = Union(A)"
+apply (simp add: big_union_def) 
+apply (blast intro!: equalityI dest: transM) 
+done
+
+lemma (in M_axioms) Union_closed [intro]:
+     "M(A) ==> M(Union(A))"
+by (insert Union_ax, simp add: Union_ax_def) 
+
+lemma (in M_axioms) Un_closed [intro]:
+     "[| M(A); M(B) |] ==> M(A Un B)"
+by (simp only: Un_eq_Union, blast) 
+
+lemma (in M_axioms) cons_closed [intro]:
+     "[| M(a); M(A) |] ==> M(cons(a,A))"
+by (subst cons_eq [symmetric], blast) 
+
+lemma (in M_axioms) successor_abs [simp]: 
+     "[| M(a); M(z) |] ==> successor(M,a,z) <-> z=succ(a)"
+by (simp add: successor_def, blast)  
+
+lemma (in M_axioms) succ_in_M_iff [iff]:
+     "M(succ(a)) <-> M(a)"
+apply (simp add: succ_def) 
+apply (blast intro: transM) 
+done
+
+lemma (in M_axioms) separation_closed [intro]:
+     "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
+apply (insert separation, simp add: separation_def) 
+apply (drule spec [THEN mp], assumption, clarify) 
+apply (subgoal_tac "y = Collect(A,P)", blast)
+apply (blast dest: transM) 
+done
+
+text{*Probably the premise and conclusion are equivalent*}
+lemma (in M_axioms) strong_replacementI [rule_format]:
+    "[| \<forall>A. M(A) --> separation(M, %u. \<exists>x\<in>A. P(x,u)) |]
+     ==> strong_replacement(M,P)"
+apply (simp add: strong_replacement_def) 
+apply (clarify ); 
+apply (frule replacementD [OF replacement]) 
+apply assumption
+apply (clarify ); 
+apply (drule_tac x=A in spec)
+apply (clarify );  
+apply (drule_tac z=Y in separationD) 
+apply assumption; 
+apply (clarify ); 
+apply (blast dest: transM) 
+done
+
+
+(*The last premise expresses that P takes M to M*)
+lemma (in M_axioms) strong_replacement_closed [intro]:
+     "[| strong_replacement(M,P); M(A); univalent(M,A,P); 
+       !!x y. [| P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))"
+apply (simp add: strong_replacement_def) 
+apply (drule spec [THEN mp], auto) 
+apply (subgoal_tac "Replace(A,P) = Y")
+ apply (simp add: ); 
+apply (rule equality_iffI) 
+apply (simp add: Replace_iff) 
+apply safe;
+ apply (blast dest: transM) 
+apply (frule transM, assumption) 
+ apply (simp add: univalent_def);
+ apply (drule spec [THEN mp, THEN iffD1], assumption, assumption)
+ apply (blast dest: transM) 
+done
+
+(*The first premise can't simply be assumed as a schema.
+  It is essential to take care when asserting instances of Replacement.
+  Let K be a nonconstructible subset of nat and define
+  f(x) = x if x:K and f(x)=0 otherwise.  Then RepFun(nat,f) = cons(0,K), a 
+  nonconstructible set.  So we cannot assume that M(X) implies M(RepFun(X,f))
+  even for f : M -> M.
+*)
+lemma (in M_axioms) RepFun_closed [intro]:
+     "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x. M(x) --> M(f(x)) |]
+      ==> M(RepFun(A,f))"
+apply (simp add: RepFun_def) 
+apply (rule strong_replacement_closed) 
+apply (auto dest: transM  simp add: univalent_def) 
+done
+
+lemma (in M_axioms) converse_abs [simp]: 
+     "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
+apply (simp add: is_converse_def)
+apply (rule iffI)
+ apply (rule equalityI) 
+  apply (blast dest: transM) 
+ apply (clarify, frule transM, assumption, simp, blast) 
+done
+
+lemma (in M_axioms) image_abs [simp]: 
+     "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
+apply (simp add: image_def)
+apply (rule iffI) 
+ apply (blast intro!: equalityI dest: transM, blast) 
+done
+
+text{*What about @{text Pow_abs}?  Powerset is NOT absolute!
+      This result is one direction of absoluteness.*}
+
+lemma (in M_axioms) powerset_Pow: 
+     "powerset(M, x, Pow(x))"
+by (simp add: powerset_def)
+
+text{*But we can't prove that the powerset in @{text M} includes the
+      real powerset.*}
+lemma (in M_axioms) powerset_imp_subset_Pow: 
+     "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)"
+apply (simp add: powerset_def) 
+apply (blast dest: transM) 
+done
+
+lemma (in M_axioms) cartprod_iff_lemma:
+     "[| M(C); \<forall>u. M(u) --> u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}); 
+       powerset(M, A \<union> B, p1); powerset(M, p1, p2); M(p2) |]
+       ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
+apply (simp add: powerset_def) 
+apply (rule equalityI, clarify, simp) 
+ apply (frule transM, assumption, simp) 
+ apply blast 
+apply clarify
+apply (frule transM, assumption, force) 
+done
+
+lemma (in M_axioms) cartprod_iff:
+     "[| M(A); M(B); M(C) |] 
+      ==> cartprod(M,A,B,C) <-> 
+          (\<exists>p1 p2. M(p1) & M(p2) & powerset(M,A Un B,p1) & powerset(M,p1,p2) &
+                   C = {z \<in> p2. \<exists>x\<in>A. \<exists>y\<in>B. z = <x,y>})"
+apply (simp add: Pair_def cartprod_def, safe)
+defer 1 
+  apply (simp add: powerset_def) 
+ apply blast 
+txt{*Final, difficult case: the left-to-right direction of the theorem.*}
+apply (insert power_ax, simp add: power_ax_def) 
+apply (frule_tac x="A Un B" and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec) 
+apply (erule impE, blast, clarify) 
+apply (drule_tac x=z and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec) 
+apply (blast intro: cartprod_iff_lemma) 
+done
+
+lemma (in M_axioms) cartprod_closed_lemma:
+     "[| M(A); M(B) |] ==> \<exists>C. M(C) & cartprod(M,A,B,C)"
+apply (simp del: cartprod_abs add: cartprod_iff)
+apply (insert power_ax, simp add: power_ax_def) 
+apply (frule_tac x="A Un B" and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec) 
+apply (erule impE, blast, clarify) 
+apply (drule_tac x=z and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec) 
+apply (erule impE, blast, clarify)
+apply (intro exI conjI) 
+prefer 6 apply (rule refl) 
+prefer 4 apply assumption
+prefer 4 apply assumption
+apply (insert cartprod_separation [of A B], simp, blast+)
+done
+
+
+text{*All the lemmas above are necessary because Powerset is not absolute.
+      I should have used Replacement instead!*}
+lemma (in M_axioms) cartprod_closed [intro]: 
+     "[| M(A); M(B) |] ==> M(A*B)"
+by (frule cartprod_closed_lemma, assumption, force)
+
+lemma (in M_axioms) image_closed [intro]: 
+     "[| M(A); M(r) |] ==> M(r``A)"
+apply (simp add: image_iff_Collect)
+apply (insert image_separation [of A r], simp, blast) 
+done
+
+lemma (in M_axioms) vimage_abs [simp]: 
+     "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) <-> z = r-``A"
+apply (simp add: pre_image_def)
+apply (rule iffI) 
+ apply (blast intro!: equalityI dest: transM, blast) 
+done
+
+lemma (in M_axioms) vimage_closed [intro]: 
+     "[| M(A); M(r) |] ==> M(r-``A)"
+apply (simp add: vimage_iff_Collect)
+apply (insert vimage_separation [of A r], simp, blast) 
+done
+
+lemma (in M_axioms) domain_abs [simp]: 
+     "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)"
+apply (simp add: is_domain_def) 
+apply (blast intro!: equalityI dest: transM) 
+done
+
+lemma (in M_axioms) domain_closed [intro]: 
+     "M(r) ==> M(domain(r))"
+apply (simp add: domain_eq_vimage)
+apply (blast intro: vimage_closed) 
+done
+
+lemma (in M_axioms) range_abs [simp]: 
+     "[| M(r); M(z) |] ==> is_range(M,r,z) <-> z = range(r)"
+apply (simp add: is_range_def)
+apply (blast intro!: equalityI dest: transM)
+done
+
+lemma (in M_axioms) range_closed [intro]: 
+     "M(r) ==> M(range(r))"
+apply (simp add: range_eq_image)
+apply (blast intro: image_closed) 
+done
+
+lemma (in M_axioms) M_converse_iff:
+     "M(r) ==> 
+      converse(r) = 
+      {z \<in> range(r) * domain(r). 
+        \<exists>p\<in>r. \<exists>x. M(x) \<and> (\<exists>y. M(y) \<and> p = \<langle>x,y\<rangle> \<and> z = \<langle>y,x\<rangle>)}"
+by (blast dest: transM)
+
+lemma (in M_axioms) converse_closed [intro]: 
+     "M(r) ==> M(converse(r))"
+apply (simp add: M_converse_iff)
+apply (insert converse_separation [of r], simp) 
+apply (blast intro: image_closed) 
+done
+
+lemma (in M_axioms) relation_abs [simp]: 
+     "M(r) ==> is_relation(M,r) <-> relation(r)"
+apply (simp add: is_relation_def relation_def) 
+apply (blast dest!: bspec dest: pair_components_in_M)+
+done
+
+lemma (in M_axioms) function_abs [simp]: 
+     "M(r) ==> is_function(M,r) <-> function(r)"
+apply (simp add: is_function_def function_def, safe) 
+   apply (frule transM, assumption) 
+  apply (blast dest: pair_components_in_M)+
+done
+
+lemma (in M_axioms) apply_closed [intro]: 
+     "[|M(f); M(a)|] ==> M(f`a)"
+apply (simp add: apply_def) 
+apply (blast intro: elim:); 
+done
+
+lemma (in M_axioms) apply_abs: 
+     "[| function(f); M(f); M(y) |] 
+      ==> fun_apply(M,f,x,y) <-> x \<in> domain(f) & f`x = y"
+apply (simp add: fun_apply_def)
+apply (blast intro: function_apply_equality function_apply_Pair) 
+done
+
+lemma (in M_axioms) typed_apply_abs: 
+     "[| f \<in> A -> B; M(f); M(y) |] 
+      ==> fun_apply(M,f,x,y) <-> x \<in> A & f`x = y"
+by (simp add: apply_abs fun_is_function domain_of_fun) 
+
+lemma (in M_axioms) typed_function_abs [simp]: 
+     "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \<in> A -> B"
+apply (auto simp add: typed_function_def relation_def Pi_iff) 
+apply (blast dest: pair_components_in_M)+
+done
+
+lemma (in M_axioms) injection_abs [simp]: 
+     "[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \<in> inj(A,B)"
+apply (simp add: injection_def apply_iff inj_def apply_closed)
+apply (blast dest: transM [of _ A]); 
+done
+
+lemma (in M_axioms) surjection_abs [simp]: 
+     "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \<in> surj(A,B)"
+by (simp add: typed_apply_abs surjection_def surj_def)
+
+lemma (in M_axioms) bijection_abs [simp]: 
+     "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \<in> bij(A,B)"
+by (simp add: bijection_def bij_def)
+
+text{*no longer needed*}
+lemma (in M_axioms) restriction_is_function: 
+     "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] 
+      ==> function(z)"
+apply (rotate_tac 1)
+apply (simp add: restriction_def Ball_iff_equiv) 
+apply (unfold function_def, blast) 
+done
+
+lemma (in M_axioms) restriction_abs [simp]: 
+     "[| M(f); M(A); M(z) |] 
+      ==> restriction(M,f,A,z) <-> z = restrict(f,A)"
+apply (simp add: Ball_iff_equiv restriction_def restrict_def)
+apply (blast intro!: equalityI dest: transM) 
+done
+
+
+lemma (in M_axioms) M_restrict_iff:
+     "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y. M(y) & z = \<langle>x, y\<rangle>}"
+by (simp add: restrict_def, blast dest: transM)
+
+lemma (in M_axioms) restrict_closed [intro]: 
+     "[| M(A); M(r) |] ==> M(restrict(r,A))"
+apply (simp add: M_restrict_iff)
+apply (insert restrict_separation [of A], simp, blast) 
+done
+
+
+lemma (in M_axioms) M_comp_iff:
+     "[| M(r); M(s) |] 
+      ==> r O s = 
+          {xz \<in> domain(s) * range(r).  
+            \<exists>x. M(x) \<and> (\<exists>y. M(y) \<and> (\<exists>z. M(z) \<and> 
+                xz = \<langle>x,z\<rangle> \<and> \<langle>x,y\<rangle> \<in> s \<and> \<langle>y,z\<rangle> \<in> r))}"
+apply (simp add: comp_def)
+apply (rule equalityI) 
+ apply (clarify ); 
+ apply (simp add: ); 
+ apply  (blast dest:  transM)+
+done
+
+lemma (in M_axioms) comp_closed [intro]: 
+     "[| M(r); M(s) |] ==> M(r O s)"
+apply (simp add: M_comp_iff)
+apply (insert comp_separation [of r s], simp, blast) 
+done
+
+lemma (in M_axioms) nat_into_M [intro]:
+     "n \<in> nat ==> M(n)"
+by (induct n rule: nat_induct, simp_all)
+
+lemma (in M_axioms) Inl_in_M_iff [iff]:
+     "M(Inl(a)) <-> M(a)"
+by (simp add: Inl_def) 
+
+lemma (in M_axioms) Inr_in_M_iff [iff]:
+     "M(Inr(a)) <-> M(a)"
+by (simp add: Inr_def) 
+
+lemma (in M_axioms) Inter_abs [simp]: 
+     "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)"
+apply (simp add: big_inter_def Inter_def) 
+apply (blast intro!: equalityI dest: transM) 
+done
+
+lemma (in M_axioms) Inter_closed [intro]:
+     "M(A) ==> M(Inter(A))"
+by (insert Inter_separation, simp add: Inter_def, blast)
+
+lemma (in M_axioms) Int_closed [intro]:
+     "[| M(A); M(B) |] ==> M(A Int B)"
+apply (subgoal_tac "M({A,B})")
+apply (frule Inter_closed, force+); 
+done
+
+subsection{*Absoluteness for ordinals*}
+text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
+
+lemma (in M_axioms) lt_closed:
+     "[| j<i; M(i) |] ==> M(j)" 
+by (blast dest: ltD intro: transM) 
+
+lemma (in M_axioms) transitive_set_abs [simp]: 
+     "M(a) ==> transitive_set(M,a) <-> Transset(a)"
+by (simp add: transitive_set_def Transset_def)
+
+lemma (in M_axioms) ordinal_abs [simp]: 
+     "M(a) ==> ordinal(M,a) <-> Ord(a)"
+by (simp add: ordinal_def Ord_def)
+
+lemma (in M_axioms) limit_ordinal_abs [simp]: 
+     "M(a) ==> limit_ordinal(M,a) <-> Limit(a)"
+apply (simp add: limit_ordinal_def Ord_0_lt_iff Limit_def) 
+apply (simp add: lt_def, blast) 
+done
+
+lemma (in M_axioms) successor_ordinal_abs [simp]: 
+     "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\<exists>b. M(b) & a = succ(b))"
+apply (simp add: successor_ordinal_def, safe)
+apply (drule Ord_cases_disj, auto) 
+done
+
+lemma finite_Ord_is_nat:
+      "[| Ord(a); ~ Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a \<in> nat"
+by (induct a rule: trans_induct3, simp_all)
+
+lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
+by (induct a rule: nat_induct, auto)
+
+lemma (in M_axioms) finite_ordinal_abs [simp]: 
+     "M(a) ==> finite_ordinal(M,a) <-> a \<in> nat"
+apply (simp add: finite_ordinal_def)
+apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord 
+             dest: Ord_trans naturals_not_limit)
+done
+
+lemma Limit_non_Limit_implies_nat: "[| Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a = nat"
+apply (rule le_anti_sym) 
+apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord)  
+ apply (simp add: lt_def)  
+ apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat) 
+apply (erule nat_le_Limit)
+done
+
+lemma (in M_axioms) omega_abs [simp]: 
+     "M(a) ==> omega(M,a) <-> a = nat"
+apply (simp add: omega_def) 
+apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)
+done
+
+lemma (in M_axioms) number1_abs [simp]: 
+     "M(a) ==> number1(M,a) <-> a = 1"
+by (simp add: number1_def) 
+
+lemma (in M_axioms) number1_abs [simp]: 
+     "M(a) ==> number2(M,a) <-> a = succ(1)"
+by (simp add: number2_def) 
+
+lemma (in M_axioms) number3_abs [simp]: 
+     "M(a) ==> number3(M,a) <-> a = succ(succ(1))"
+by (simp add: number3_def) 
+
+text{*Kunen continued to 20...*}
+
+(*Could not get this to work.  The \<lambda>x\<in>nat is essential because everything 
+  but the recursion variable must stay unchanged.  But then the recursion
+  equations only hold for x\<in>nat (or in some other set) and not for the 
+  whole of the class M.
+  consts
+    natnumber_aux :: "[i=>o,i] => i"
+
+  primrec
+      "natnumber_aux(M,0) = (\<lambda>x\<in>nat. if empty(M,x) then 1 else 0)"
+      "natnumber_aux(M,succ(n)) = 
+	   (\<lambda>x\<in>nat. if (\<exists>y. M(y) & natnumber_aux(M,n)`y=1 & successor(M,y,x)) 
+		     then 1 else 0)"
+
+  constdefs
+    natnumber :: "[i=>o,i,i] => o"
+      "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1"
+
+  lemma (in M_axioms) [simp]: 
+       "natnumber(M,0,x) == x=0"
+*)
+
+
+end
diff -r 74d9144c452c -r 45be08fbdcff src/ZF/Constructible/WF_absolute.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/WF_absolute.thy	Wed Jun 19 11:48:01 2002 +0200
@@ -0,0 +1,210 @@
+theory WF_absolute = WF_extras + WFrec:
+
+
+subsection{*Transitive closure without fixedpoints*}
+
+(*Ordinal.thy: just after succ_le_iff?*)
+lemma Ord_succ_mem_iff: "Ord(j) ==> succ(i) \<in> succ(j) <-> i\<in>j"
+apply (insert succ_le_iff [of i j]) 
+apply (simp add: lt_def) 
+done
+
+constdefs
+  rtrancl_alt :: "[i,i]=>i"
+    "rtrancl_alt(A,r) == 
+       {p \<in> A*A. \<exists>n\<in>nat. \<exists>f \<in> succ(n) -> A.
+                 \<exists>x y. p = <x,y> &  f`0 = x & f`n = y &
+                       (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)}"
+
+lemma alt_rtrancl_lemma1 [rule_format]: 
+    "n \<in> nat
+     ==> \<forall>f \<in> succ(n) -> field(r). 
+         (\<forall>i\<in>n. \<langle>f`i, f ` succ(i)\<rangle> \<in> r) --> \<langle>f`0, f`n\<rangle> \<in> r^*"
+apply (induct_tac n) 
+apply (simp_all add: apply_funtype rtrancl_refl, clarify) 
+apply (rename_tac n f) 
+apply (rule rtrancl_into_rtrancl) 
+ prefer 2 apply assumption
+apply (drule_tac x="restrict(f,succ(n))" in bspec)
+ apply (blast intro: restrict_type2) 
+apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI) 
+done
+
+lemma rtrancl_alt_subset_rtrancl: "rtrancl_alt(field(r),r) <= r^*"
+apply (simp add: rtrancl_alt_def)
+apply (blast intro: alt_rtrancl_lemma1 )  
+done
+
+lemma rtrancl_subset_rtrancl_alt: "r^* <= rtrancl_alt(field(r),r)"
+apply (simp add: rtrancl_alt_def, clarify) 
+apply (frule rtrancl_type [THEN subsetD], clarify) 
+apply simp 
+apply (erule rtrancl_induct) 
+ txt{*Base case, trivial*}
+ apply (rule_tac x=0 in bexI) 
+  apply (rule_tac x="lam x:1. xa" in bexI) 
+   apply simp_all 
+txt{*Inductive step*}
+apply clarify 
+apply (rename_tac n f) 
+apply (rule_tac x="succ(n)" in bexI) 
+ apply (rule_tac x="lam i:succ(succ(n)). if i=succ(n) then z else f`i" in bexI)
+  apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI) 
+  apply (blast intro: mem_asym)  
+ apply typecheck 
+ apply auto 
+done
+
+lemma rtrancl_alt_eq_rtrancl: "rtrancl_alt(field(r),r) = r^*"
+by (blast del: subsetI
+	  intro: rtrancl_alt_subset_rtrancl rtrancl_subset_rtrancl_alt) 
+
+
+text{*Relativized to M: Every well-founded relation is a subset of some
+inverse image of an ordinal.  Key step is the construction (in M) of a 
+rank function.*}
+
+
+(*NEEDS RELATIVIZATION*)
+locale M_recursion = M_axioms +
+  assumes wfrank_separation':
+     "[| M(r); M(a); r \<subseteq> A*A |] ==>
+	separation
+	   (M, \<lambda>x. x \<in> A --> 
+		~(\<exists>f. M(f) \<and> 
+		      is_recfun(r, x, %x f. \<Union>y \<in> r-``{x}. succ(f`y), f)))"
+ and wfrank_strong_replacement':
+     "[| M(r); M(a); r \<subseteq> A*A |] ==>
+      strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+		  pair(M,x,y,z) & 
+		  is_recfun(r, x, %x f. \<Union>y \<in> r-``{x}. succ(f`y), f) & 
+		  y = (\<Union>y \<in> r-``{x}. succ(g`y)))"
+
+
+constdefs (*????????????????NEEDED?*)
+ is_wfrank_fun :: "[i=>o,i,i,i] => o"
+    "is_wfrank_fun(M,r,a,f) == 
+       function(f) & domain(f) = r-``{a} & 
+       (\<forall>x. M(x) --> <x,a> \<in> r --> f`x = (\<Union>y \<in> r-``{x}. succ(f`y)))"
+
+
+
+
+lemma (in M_recursion) exists_wfrank:
+    "[| wellfounded(M,r); r \<subseteq> A*A; a\<in>A; M(r); M(A) |]
+     ==> \<exists>f. M(f) & is_recfun(r, a, %x g. (\<Union>y \<in> r-``{x}. succ(g`y)), f)"
+apply (rule exists_is_recfun [of A r]) 
+apply (erule wellfounded_imp_wellfounded_on) 
+apply assumption; 
+apply (rule trans_Memrel [THEN trans_imp_trans_on], simp)  
+apply (rule succI1) 
+apply (blast intro: wfrank_separation') 
+apply (blast intro: wfrank_strong_replacement') 
+apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
+done
+
+lemma (in M_recursion) exists_wfrank_fun:
+    "[| Ord(j);  M(i);  M(j) |] ==> \<exists>f. M(f) & is_wfrank_fun(M,i,succ(j),f)"
+apply (rule exists_wfrank [THEN exE])
+apply (erule Ord_succ, assumption, simp) 
+apply (rename_tac f, clarify) 
+apply (frule is_recfun_type)
+apply (rule_tac x=f in exI) 
+apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
+                 is_wfrank_fun_eq Ord_trans [OF _ succI1])
+done
+
+lemma (in M_recursion) is_wfrank_fun_apply:
+    "[| x < j; M(i); M(j); M(f); is_wfrank_fun(M,r,a,f) |] 
+     ==> f`x = i Un (\<Union>k\<in>x. {f ` k})"
+apply (simp add: is_wfrank_fun_eq lt_Ord2) 
+apply (frule lt_closed, simp) 
+apply (subgoal_tac "x <= domain(f)")
+ apply (simp add: Ord_trans [OF _ succI1] image_function)
+ apply (blast intro: elim:); 
+apply (blast intro: dest!: leI [THEN le_imp_subset] ) 
+done
+
+lemma (in M_recursion) is_wfrank_fun_eq_wfrank [rule_format]:
+    "[| is_wfrank_fun(M,i,J,f); M(i); M(J); M(f); Ord(i); Ord(j) |] 
+     ==> j<J --> f`j = i++j"
+apply (erule_tac i=j in trans_induct, clarify) 
+apply (subgoal_tac "\<forall>k\<in>x. k<J")
+ apply (simp (no_asm_simp) add: is_wfrank_def wfrank_unfold is_wfrank_fun_apply)
+apply (blast intro: lt_trans ltI lt_Ord) 
+done
+
+lemma (in M_recursion) wfrank_abs_fun_apply_iff:
+    "[| M(i); M(J); M(f); M(k); j<J; is_wfrank_fun(M,i,J,f) |] 
+     ==> fun_apply(M,f,j,k) <-> f`j = k"
+by (auto simp add: lt_def is_wfrank_fun_eq subsetD apply_abs) 
+
+lemma (in M_recursion) Ord_wfrank_abs:
+    "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_wfrank(M,r,a,k) <-> k = i++j"
+apply (simp add: is_wfrank_def wfrank_abs_fun_apply_iff is_wfrank_fun_eq_wfrank)
+apply (frule exists_wfrank_fun [of j i], blast+)
+done
+
+lemma (in M_recursion) wfrank_abs:
+    "[| M(i); M(j); M(k) |] ==> is_wfrank(M,r,a,k) <-> k = i++j"
+apply (case_tac "Ord(i) & Ord(j)")
+ apply (simp add: Ord_wfrank_abs)
+apply (auto simp add: is_wfrank_def wfrank_eq_if_raw_wfrank)
+done
+
+lemma (in M_recursion) wfrank_closed [intro]:
+    "[| M(i); M(j) |] ==> M(i++j)"
+apply (simp add: wfrank_eq_if_raw_wfrank, clarify) 
+apply (simp add: raw_wfrank_eq_wfrank) 
+apply (frule exists_wfrank_fun [of j i], auto)
+apply (simp add: apply_closed is_wfrank_fun_eq_wfrank [symmetric]) 
+done
+
+
+
+constdefs
+  wfrank :: "[i,i]=>i"
+    "wfrank(r,a) == wfrec(r, a, %x f. \<Union>y \<in> r-``{x}. succ(f`y))"
+
+constdefs
+  wftype :: "i=>i"
+    "wftype(r) == \<Union>y \<in> range(r). succ(wfrank(r,y))"
+
+lemma (in M_axioms) wfrank: "wellfounded(M,r) ==> wfrank(r,a) = (\<Union>y \<in> r-``{a}. succ(wfrank(r,y)))"
+by (subst wfrank_def [THEN def_wfrec], simp_all)
+
+lemma (in M_axioms) Ord_wfrank: "wellfounded(M,r) ==> Ord(wfrank(r,a))"
+apply (rule_tac a="a" in wf_induct, assumption)
+apply (subst wfrank, assumption)
+apply (rule Ord_succ [THEN Ord_UN], blast) 
+done
+
+lemma (in M_axioms) wfrank_lt: "[|wellfounded(M,r); <a,b> \<in> r|] ==> wfrank(r,a) < wfrank(r,b)"
+apply (rule_tac a1 = "b" in wfrank [THEN ssubst], assumption)
+apply (rule UN_I [THEN ltI])
+apply (simp add: Ord_wfrank vimage_iff)+
+done
+
+lemma (in M_axioms) Ord_wftype: "wellfounded(M,r) ==> Ord(wftype(r))"
+by (simp add: wftype_def Ord_wfrank)
+
+lemma (in M_axioms) wftypeI: "\<lbrakk>wellfounded(M,r);  x \<in> field(r)\<rbrakk> \<Longrightarrow> wfrank(r,x) \<in> wftype(r)"
+apply (simp add: wftype_def) 
+apply (blast intro: wfrank_lt [THEN ltD]) 
+done
+
+
+lemma (in M_axioms) wf_imp_subset_rvimage:
+     "[|wellfounded(M,r); r \<subseteq> A*A|] ==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))"
+apply (rule_tac x="wftype(r)" in exI) 
+apply (rule_tac x="\<lambda>x\<in>A. wfrank(r,x)" in exI) 
+apply (simp add: Ord_wftype, clarify) 
+apply (frule subsetD, assumption, clarify) 
+apply (simp add: rvimage_iff wfrank_lt [THEN ltD])
+apply (blast intro: wftypeI  ) 
+done
+
+
+
+
+end
diff -r 74d9144c452c -r 45be08fbdcff src/ZF/Constructible/WFrec.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/WFrec.thy	Wed Jun 19 11:48:01 2002 +0200
@@ -0,0 +1,559 @@
+theory WFrec = Wellorderings:
+
+
+(*WF.thy??*)
+
+lemma is_recfunI:
+     "f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))) ==> is_recfun(r,a,H,f)"
+by (simp add: is_recfun_def) 
+
+lemma is_recfun_imp_function: "is_recfun(r,a,H,f) ==> function(f)"
+apply (simp add: is_recfun_def) 
+apply (erule ssubst)
+apply (rule function_lam) 
+done
+
+text{*Expresses @{text is_recfun} as a recursion equation*}
+lemma is_recfun_iff_equation:
+     "is_recfun(r,a,H,f) <->
+	   f \<in> r -`` {a} \<rightarrow> range(f) &
+	   (\<forall>x \<in> r-``{a}. f`x = H(x, restrict(f, r-``{x})))"  
+apply (rule iffI) 
+ apply (simp add: is_recfun_type apply_recfun Ball_def vimage_singleton_iff, 
+        clarify)  
+apply (simp add: is_recfun_def) 
+apply (rule fun_extension) 
+  apply assumption
+ apply (fast intro: lam_type, simp) 
+done
+
+lemma trans_on_Int_eq [simp]:
+      "[| trans[A](r); <y,x> \<in> r;  r \<subseteq> A*A |] 
+       ==> r -`` {y} \<inter> r -`` {x} = r -`` {y}"
+by (blast intro: trans_onD) 
+
+lemma trans_on_Int_eq2 [simp]:
+      "[| trans[A](r); <y,x> \<in> r;  r \<subseteq> A*A |] 
+       ==> r -`` {x} \<inter> r -`` {y} = r -`` {y}"
+by (blast intro: trans_onD) 
+
+
+constdefs
+   M_the_recfun :: "[i=>o, i, i, [i,i]=>i] => i"
+     "M_the_recfun(M,r,a,H) == (THE f. M(f) & is_recfun(r,a,H,f))"
+
+
+text{*Stated using @{term "trans[A](r)"} rather than
+      @{term "transitive_rel(M,A,r)"} because the latter rewrites to
+      the former anyway, by @{text transitive_rel_abs}.
+      As always, theorems should be expressed in simplified form.*}
+lemma (in M_axioms) is_recfun_equal [rule_format]: 
+    "[|is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  
+       wellfounded_on(M,A,r);  trans[A](r); 
+       M(A); M(f); M(g); M(a); M(b); 
+       r \<subseteq> A*A;  x\<in>A |] 
+     ==> <x,a> \<in> r --> <x,b> \<in> r --> f`x=g`x"
+apply (frule_tac f="f" in is_recfun_type) 
+apply (frule_tac f="g" in is_recfun_type) 
+apply (simp add: is_recfun_def)
+apply (erule wellfounded_on_induct2, assumption+) 
+apply (force intro: is_recfun_separation, clarify)
+apply (erule ssubst)+
+apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def)
+apply (rename_tac x1)
+apply (rule_tac t="%z. H(x1,z)" in subst_context) 
+apply (subgoal_tac "ALL y : r-``{x1}. ALL z. <y,z>:f <-> <y,z>:g")
+ apply (blast intro: trans_onD) 
+apply (simp add: apply_iff) 
+apply (blast intro: trans_onD sym) 
+done
+
+lemma (in M_axioms) is_recfun_cut: 
+    "[|is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  
+       wellfounded_on(M,A,r); trans[A](r); 
+       M(A); M(f); M(g); M(a); M(b); 
+       r \<subseteq> A*A;  <b,a>\<in>r |]   
+      ==> restrict(f, r-``{b}) = g"
+apply (frule_tac f="f" in is_recfun_type) 
+apply (rule fun_extension) 
+apply (blast intro: trans_onD restrict_type2) 
+apply (erule is_recfun_type, simp) 
+apply (blast intro: is_recfun_equal trans_onD) 
+done
+
+lemma (in M_axioms) is_recfun_functional:
+     "[|is_recfun(r,a,H,f);  is_recfun(r,a,H,g);  
+       wellfounded_on(M,A,r); trans[A](r); 
+       M(A); M(f); M(g); M(a); 
+       r \<subseteq> A*A |]   
+      ==> f=g"
+apply (rule fun_extension)
+apply (erule is_recfun_type)+
+apply (blast intro!: is_recfun_equal) 
+done
+
+text{*Tells us that is_recfun can (in principle) be relativized.*}
+lemma (in M_axioms) is_recfun_relativize:
+     "[| M(r); M(a); M(f); 
+       \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |] ==>
+       is_recfun(r,a,H,f) <->
+       (\<forall>z. z \<in> f <-> (\<exists>x y. M(x) & M(y) & z=<x,y> & <x,a> \<in> r & 
+                              y = H(x, restrict(f, r-``{x}))))";
+apply (simp add: is_recfun_def vimage_closed restrict_closed lam_def)
+apply (safe intro!: equalityI) 
+  apply (drule equalityD1 [THEN subsetD], assumption) 
+  apply clarify 
+  apply (rule_tac x=x in exI) 
+  apply (blast dest: pair_components_in_M) 
+ apply (blast elim!: equalityE dest: pair_components_in_M)
+ apply simp  
+ apply blast
+ apply simp 
+apply (subgoal_tac "function(f)")  
+ prefer 2
+ apply (simp add: function_def) 
+apply (frule pair_components_in_M, assumption) 
+  apply (simp add: is_recfun_imp_function function_restrictI restrict_closed vimage_closed) 
+done
+
+(* ideas for further weaking the H-closure premise:
+apply (drule spec [THEN spec]) 
+apply (erule mp)
+apply (intro conjI)
+apply (blast dest!: pair_components_in_M)
+apply (blast intro!: function_restrictI dest!: pair_components_in_M)
+apply (blast intro!: function_restrictI dest!: pair_components_in_M)
+apply (simp only: subset_iff domain_iff restrict_iff vimage_iff) 
+apply (simp add:  vimage_singleton_iff) 
+apply (intro allI impI conjI)
+apply (blast intro: transM dest!: pair_components_in_M)
+prefer 4;apply blast 
+*)
+
+lemma (in M_axioms) is_recfun_restrict:
+     "[| wellfounded_on(M,A,r); trans[A](r); is_recfun(r,x,H,f); \<langle>y,x\<rangle> \<in> r; 
+       M(A); M(r); M(f); 
+       \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)); r \<subseteq> A * A |]
+       ==> is_recfun(r, y, H, restrict(f, r -`` {y}))"
+apply (frule pair_components_in_M, assumption, clarify) 
+apply (simp (no_asm_simp) add: is_recfun_relativize vimage_closed restrict_closed
+     restrict_iff)
+apply safe
+  apply (simp_all add: vimage_singleton_iff is_recfun_type [THEN apply_iff]) 
+  apply (frule_tac x=xa in pair_components_in_M, assumption)
+  apply (frule_tac x=xa in apply_recfun, blast intro: trans_onD)  
+  apply (simp add: is_recfun_type [THEN apply_iff])
+  (*???COMBINE*) 
+  apply (simp add: is_recfun_imp_function function_restrictI restrict_closed vimage_closed) 
+apply (blast intro: apply_recfun dest: trans_onD)+
+done
+ 
+lemma (in M_axioms) restrict_Y_lemma:
+     "[| wellfounded_on(M,A,r); trans[A](r); M(A); M(r); r \<subseteq> A \<times> A;
+       \<forall>x g. M(x) \<and> M(g) & function(g) --> M(H(x,g));  M(Y);
+       \<forall>b. M(b) -->
+	   b \<in> Y <->
+	   (\<exists>x\<in>r -`` {a1}.
+	       \<exists>y. M(y) \<and>
+		   (\<exists>g. M(g) \<and> b = \<langle>x,y\<rangle> \<and> is_recfun(r,x,H,g) \<and> y = H(x,g)));
+          \<langle>x,a1\<rangle> \<in> r; M(f); is_recfun(r,x,H,f) |]
+       ==> restrict(Y, r -`` {x}) = f"
+apply (subgoal_tac "ALL y : r-``{x}. ALL z. <y,z>:Y <-> <y,z>:f") 
+apply (simp (no_asm_simp) add: restrict_def) 
+apply (thin_tac "All(?P)")+  --{*essential for efficiency*}
+apply (frule is_recfun_type [THEN fun_is_rel], blast)
+apply (frule pair_components_in_M, assumption, clarify) 
+apply (rule iffI)
+ apply (frule_tac y="<y,z>" in transM, assumption )
+ apply (rotate_tac -1)   
+ apply (clarsimp simp add: vimage_singleton_iff is_recfun_type [THEN apply_iff]
+			   apply_recfun is_recfun_cut) 
+txt{*Opposite inclusion: something in f, show in Y*}
+apply (frule_tac y="<y,z>" in transM, assumption, simp) 
+apply (rule_tac x=y in bexI)
+prefer 2 apply (blast dest: trans_onD)
+apply (rule_tac x=z in exI, simp) 
+apply (rule_tac x="restrict(f, r -`` {y})" in exI) 
+apply (simp add: vimage_closed restrict_closed is_recfun_restrict
+                 apply_recfun is_recfun_type [THEN apply_iff]) 
+done
+
+text{*Proof of the inductive step for @{text exists_is_recfun}, since
+      we must prove two versions.*}
+lemma (in M_axioms) exists_is_recfun_indstep:
+    "[|a1 \<in> A;  \<forall>y. \<langle>y, a1\<rangle> \<in> r --> (\<exists>f. M(f) & is_recfun(r, y, H, f)); 
+       wellfounded_on(M,A,r); trans[A](r); 
+       strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+                   pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
+       M(A); M(r); r \<subseteq> A * A;
+       \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g))|]   
+      ==> \<exists>f. M(f) & is_recfun(r,a1,H,f)"
+apply (frule_tac y=a1 in transM, assumption)
+apply (drule_tac A="r-``{a1}" in strong_replacementD)
+  apply blast
+ txt{*Discharge the "univalent" obligation of Replacement*}
+ apply (clarsimp simp add: univalent_def)
+ apply (blast dest!: is_recfun_functional)
+txt{*Show that the constructed object satisfies @{text is_recfun}*} 
+apply clarify 
+apply (rule_tac x=Y in exI)  
+apply (simp (no_asm_simp) add: is_recfun_relativize vimage_closed restrict_closed) 
+(*Tried using is_recfun_iff2 here.  Much more simplification takes place
+  because an assumption can kick in.  Not sure how to relate the new 
+  proof state to the current one.*)
+apply safe
+txt{*Show that elements of @{term Y} are in the right relationship.*}
+apply (frule_tac x=z and P="%b. M(b) --> ?Q(b)" in spec)
+apply (erule impE, blast intro: transM)
+txt{*We have an element of  @{term Y}, so we have x, y, z*} 
+apply (frule_tac y=z in transM, assumption, clarify)
+apply (simp add: vimage_closed restrict_closed restrict_Y_lemma [of A r H]) 
+txt{*one more case*}
+apply (simp add: vimage_closed restrict_closed )
+apply (rule_tac x=x in bexI) 
+prefer 2 apply blast 
+apply (rule_tac x="H(x, restrict(Y, r -`` {x}))" in exI) 
+apply (simp add: vimage_closed restrict_closed )
+apply (drule_tac x1=x in spec [THEN mp], assumption, clarify) 
+apply (rule_tac x=f in exI) 
+apply (simp add: restrict_Y_lemma [of A r H]) 
+done
+
+
+text{*Relativized version, when we have the (currently weaker) premise
+      @{term "wellfounded_on(M,A,r)"}*}
+lemma (in M_axioms) wellfounded_exists_is_recfun:
+    "[|wellfounded_on(M,A,r);  trans[A](r);  a\<in>A; 
+       separation(M, \<lambda>x. x \<in> A --> ~ (\<exists>f. M(f) \<and> is_recfun(r, x, H, f)));
+       strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+                   pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
+       M(A);  M(r);  r \<subseteq> A*A;  
+       \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |]   
+      ==> \<exists>f. M(f) & is_recfun(r,a,H,f)"
+apply (rule wellfounded_on_induct2, assumption+, clarify)
+apply (rule exists_is_recfun_indstep, assumption+)
+done
+
+lemma (in M_axioms) wf_exists_is_recfun:
+    "[|wf[A](r);  trans[A](r);  a\<in>A; 
+       strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+                   pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
+       M(A);  M(r);  r \<subseteq> A*A;  
+       \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |]   
+      ==> \<exists>f. M(f) & is_recfun(r,a,H,f)"
+apply (rule wf_on_induct2, assumption+)
+apply (frule wf_on_imp_relativized)  
+apply (rule exists_is_recfun_indstep, assumption+)
+done
+
+(*If some f satisfies is_recfun(r,a,H,-) then so does M_the_recfun(M,r,a,H) *)
+lemma (in M_axioms) M_is_the_recfun: 
+    "[|is_recfun(r,a,H,f);  
+       wellfounded_on(M,A,r); trans[A](r); 
+       M(A); M(f); M(a); r \<subseteq> A*A |]   
+     ==> M(M_the_recfun(M,r,a,H)) & 
+         is_recfun(r, a, H, M_the_recfun(M,r,a,H))"
+apply (unfold M_the_recfun_def)
+apply (rule ex1I [THEN theI2], fast)
+apply (blast intro: is_recfun_functional, blast) 
+done
+
+constdefs
+   M_is_recfun :: "[i=>o, i, i, [i=>o,i,i,i]=>o, i] => o"
+     "M_is_recfun(M,r,a,MH,f) == 
+      \<forall>z. M(z) -->
+          (z \<in> f <-> 
+           (\<exists>x y xa sx r_sx f_r_sx. 
+              M(x) & M(y) & M(xa) & M(sx) & M(r_sx) & M(f_r_sx) &
+	      pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) &
+              pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
+              xa \<in> r & MH(M, x, f_r_sx, y)))"
+
+lemma (in M_axioms) is_recfun_iff_M:
+     "[| M(r); M(a); M(f); \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g));
+       \<forall>x g y. M(x) --> M(g) --> M(y) --> MH(M,x,g,y) <-> y = H(x,g) |] ==>
+       is_recfun(r,a,H,f) <-> M_is_recfun(M,r,a,MH,f)"
+apply (simp add: vimage_closed restrict_closed M_is_recfun_def is_recfun_relativize)
+apply (rule all_cong, safe)
+ apply (thin_tac "\<forall>x. ?P(x)")+
+ apply (blast dest: transM)  (*or del: allE*)
+done
+
+lemma M_is_recfun_cong [cong]:
+     "[| r = r'; a = a'; f = f'; 
+       !!x g y. [| M(x); M(g); M(y) |] ==> MH(M,x,g,y) <-> MH'(M,x,g,y) |]
+      ==> M_is_recfun(M,r,a,MH,f) <-> M_is_recfun(M,r',a',MH',f')"
+by (simp add: M_is_recfun_def) 
+
+
+constdefs
+ (*This expresses ordinal addition as a formula in the LAST.  It also 
+   provides an abbreviation that can be used in the instance of strong
+   replacement below.  Here j is used to define the relation, namely
+   Memrel(succ(j)), while x determines the domain of f.*)
+ is_oadd_fun :: "[i=>o,i,i,i,i] => o"
+    "is_oadd_fun(M,i,j,x,f) == 
+       (\<forall>sj msj. M(sj) --> M(msj) --> 
+                 successor(M,j,sj) --> membership(M,sj,msj) --> 
+	         M_is_recfun(M, msj, x, 
+		     %M x g y. \<exists>gx. M(gx) & image(M,g,x,gx) & union(M,i,gx,y),
+		     f))"
+
+ is_oadd :: "[i=>o,i,i,i] => o"
+    "is_oadd(M,i,j,k) == 
+        (~ ordinal(M,i) & ~ ordinal(M,j) & k=0) |
+        (~ ordinal(M,i) & ordinal(M,j) & k=j) |
+        (ordinal(M,i) & ~ ordinal(M,j) & k=i) |
+        (ordinal(M,i) & ordinal(M,j) & 
+	 (\<exists>f fj sj. M(f) & M(fj) & M(sj) & 
+		    successor(M,j,sj) & is_oadd_fun(M,i,sj,sj,f) & 
+		    fun_apply(M,f,j,fj) & fj = k))"
+
+ (*NEEDS RELATIVIZATION*)
+ omult_eqns :: "[i,i,i,i] => o"
+    "omult_eqns(i,x,g,z) ==
+            Ord(x) & 
+	    (x=0 --> z=0) &
+            (\<forall>j. x = succ(j) --> z = g`j ++ i) &
+            (Limit(x) --> z = \<Union>(g``x))"
+
+ is_omult_fun :: "[i=>o,i,i,i] => o"
+    "is_omult_fun(M,i,j,f) == 
+	    (\<exists>df. M(df) & is_function(M,f) & 
+                  is_domain(M,f,df) & subset(M, j, df)) & 
+            (\<forall>x\<in>j. omult_eqns(i,x,f,f`x))"
+
+ is_omult :: "[i=>o,i,i,i] => o"
+    "is_omult(M,i,j,k) == 
+	\<exists>f fj sj. M(f) & M(fj) & M(sj) & 
+                  successor(M,j,sj) & is_omult_fun(M,i,sj,f) & 
+                  fun_apply(M,f,j,fj) & fj = k"
+
+
+locale M_recursion = M_axioms +
+  assumes oadd_strong_replacement:
+   "[| M(i); M(j) |] ==>
+    strong_replacement(M, 
+         \<lambda>x z. \<exists>y f fx. M(y) & M(f) & M(fx) & 
+		         pair(M,x,y,z) & is_oadd_fun(M,i,j,x,f) & 
+		         image(M,f,x,fx) & y = i Un fx)" 
+ and omult_strong_replacement':
+   "[| M(i); M(j) |] ==>
+    strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+	     pair(M,x,y,z) & 
+	     is_recfun(Memrel(succ(j)),x,%x g. THE z. omult_eqns(i,x,g,z),g) & 
+	     y = (THE z. omult_eqns(i, x, g, z)))" 
+
+
+
+text{*is_oadd_fun: Relating the pure "language of set theory" to Isabelle/ZF*}
+lemma (in M_recursion) is_oadd_fun_iff:
+   "[| a\<le>j; M(i); M(j); M(a); M(f) |] 
+    ==> is_oadd_fun(M,i,j,a,f) <->
+	f \<in> a \<rightarrow> range(f) & (\<forall>x. M(x) --> x < a --> f`x = i Un f``x)"
+apply (frule lt_Ord) 
+apply (simp add: is_oadd_fun_def Memrel_closed Un_closed 
+             is_recfun_iff_M [of concl: _ _ "%x g. i Un g``x", THEN iff_sym]
+             image_closed is_recfun_iff_equation  
+             Ball_def lt_trans [OF ltI, of _ a] lt_Memrel)
+apply (simp add: lt_def) 
+apply (blast dest: transM) 
+done
+
+
+lemma (in M_recursion) oadd_strong_replacement':
+    "[| M(i); M(j) |] ==>
+     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+		  pair(M,x,y,z) & 
+		  is_recfun(Memrel(succ(j)),x,%x g. i Un g``x,g) & 
+		  y = i Un g``x)" 
+apply (insert oadd_strong_replacement [of i j]) 
+apply (simp add: Memrel_closed Un_closed image_closed is_oadd_fun_def
+                 is_recfun_iff_M)  
+done
+
+
+lemma (in M_recursion) exists_oadd:
+    "[| Ord(j);  M(i);  M(j) |]
+     ==> \<exists>f. M(f) & is_recfun(Memrel(succ(j)), j, %x g. i Un g``x, f)"
+apply (rule wf_exists_is_recfun) 
+apply (rule wf_Memrel [THEN wf_imp_wf_on]) 
+apply (rule trans_Memrel [THEN trans_imp_trans_on], simp)  
+apply (rule succI1) 
+apply (blast intro: oadd_strong_replacement') 
+apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
+done
+
+lemma (in M_recursion) exists_oadd_fun:
+    "[| Ord(j);  M(i);  M(j) |] 
+     ==> \<exists>f. M(f) & is_oadd_fun(M,i,succ(j),succ(j),f)"
+apply (rule exists_oadd [THEN exE])
+apply (erule Ord_succ, assumption, simp) 
+apply (rename_tac f, clarify) 
+apply (frule is_recfun_type)
+apply (rule_tac x=f in exI) 
+apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
+                 is_oadd_fun_iff Ord_trans [OF _ succI1])
+done
+
+lemma (in M_recursion) is_oadd_fun_apply:
+    "[| x < j; M(i); M(j); M(f); is_oadd_fun(M,i,j,j,f) |] 
+     ==> f`x = i Un (\<Union>k\<in>x. {f ` k})"
+apply (simp add: is_oadd_fun_iff lt_Ord2, clarify) 
+apply (frule lt_closed, simp)
+apply (frule leI [THEN le_imp_subset])  
+apply (simp add: image_fun, blast) 
+done
+
+lemma (in M_recursion) is_oadd_fun_iff_oadd [rule_format]:
+    "[| is_oadd_fun(M,i,J,J,f); M(i); M(J); M(f); Ord(i); Ord(j) |] 
+     ==> j<J --> f`j = i++j"
+apply (erule_tac i=j in trans_induct, clarify) 
+apply (subgoal_tac "\<forall>k\<in>x. k<J")
+ apply (simp (no_asm_simp) add: is_oadd_def oadd_unfold is_oadd_fun_apply)
+apply (blast intro: lt_trans ltI lt_Ord) 
+done
+
+lemma (in M_recursion) oadd_abs_fun_apply_iff:
+    "[| M(i); M(J); M(f); M(k); j<J; is_oadd_fun(M,i,J,J,f) |] 
+     ==> fun_apply(M,f,j,k) <-> f`j = k"
+by (force simp add: lt_def is_oadd_fun_iff subsetD typed_apply_abs) 
+
+lemma (in M_recursion) Ord_oadd_abs:
+    "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_oadd(M,i,j,k) <-> k = i++j"
+apply (simp add: is_oadd_def oadd_abs_fun_apply_iff is_oadd_fun_iff_oadd)
+apply (frule exists_oadd_fun [of j i], blast+)
+done
+
+lemma (in M_recursion) oadd_abs:
+    "[| M(i); M(j); M(k) |] ==> is_oadd(M,i,j,k) <-> k = i++j"
+apply (case_tac "Ord(i) & Ord(j)")
+ apply (simp add: Ord_oadd_abs)
+apply (auto simp add: is_oadd_def oadd_eq_if_raw_oadd)
+done
+
+lemma (in M_recursion) oadd_closed [intro]:
+    "[| M(i); M(j) |] ==> M(i++j)"
+apply (simp add: oadd_eq_if_raw_oadd, clarify) 
+apply (simp add: raw_oadd_eq_oadd) 
+apply (frule exists_oadd_fun [of j i], auto)
+apply (simp add: apply_closed is_oadd_fun_iff_oadd [symmetric]) 
+done
+
+
+text{*Ordinal Multiplication*}
+
+lemma omult_eqns_unique:
+     "[| omult_eqns(i,x,g,z); omult_eqns(i,x,g,z') |] ==> z=z'";
+apply (simp add: omult_eqns_def, clarify) 
+apply (erule Ord_cases, simp_all) 
+done
+
+lemma omult_eqns_0: "omult_eqns(i,0,g,z) <-> z=0"
+by (simp add: omult_eqns_def)
+
+lemma the_omult_eqns_0: "(THE z. omult_eqns(i,0,g,z)) = 0"
+by (simp add: omult_eqns_0)
+
+lemma omult_eqns_succ: "omult_eqns(i,succ(j),g,z) <-> Ord(j) & z = g`j ++ i"
+by (simp add: omult_eqns_def)
+
+lemma the_omult_eqns_succ:
+     "Ord(j) ==> (THE z. omult_eqns(i,succ(j),g,z)) = g`j ++ i"
+by (simp add: omult_eqns_succ) 
+
+lemma omult_eqns_Limit:
+     "Limit(x) ==> omult_eqns(i,x,g,z) <-> z = \<Union>(g``x)"
+apply (simp add: omult_eqns_def) 
+apply (blast intro: Limit_is_Ord) 
+done
+
+lemma the_omult_eqns_Limit:
+     "Limit(x) ==> (THE z. omult_eqns(i,x,g,z)) = \<Union>(g``x)"
+by (simp add: omult_eqns_Limit)
+
+lemma omult_eqns_Not: "~ Ord(x) ==> ~ omult_eqns(i,x,g,z)"
+by (simp add: omult_eqns_def)
+
+
+lemma (in M_recursion) the_omult_eqns_closed:
+    "[| M(i); M(x); M(g); function(g) |] 
+     ==> M(THE z. omult_eqns(i, x, g, z))"
+apply (case_tac "Ord(x)")
+ prefer 2 apply (simp add: omult_eqns_Not) --{*trivial, non-Ord case*}
+apply (erule Ord_cases) 
+  apply (simp add: omult_eqns_0)
+ apply (simp add: omult_eqns_succ apply_closed oadd_closed) 
+apply (simp add: omult_eqns_Limit) 
+apply (simp add: Union_closed image_closed) 
+done
+
+lemma (in M_recursion) exists_omult:
+    "[| Ord(j);  M(i);  M(j) |]
+     ==> \<exists>f. M(f) & is_recfun(Memrel(succ(j)), j, %x g. THE z. omult_eqns(i,x,g,z), f)"
+apply (rule wf_exists_is_recfun) 
+apply (rule wf_Memrel [THEN wf_imp_wf_on]) 
+apply (rule trans_Memrel [THEN trans_imp_trans_on], simp)  
+apply (rule succI1) 
+apply (blast intro: omult_strong_replacement') 
+apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
+apply (blast intro: the_omult_eqns_closed) 
+done
+
+lemma (in M_recursion) exists_omult_fun:
+    "[| Ord(j);  M(i);  M(j) |] ==> \<exists>f. M(f) & is_omult_fun(M,i,succ(j),f)"
+apply (rule exists_omult [THEN exE])
+apply (erule Ord_succ, assumption, simp) 
+apply (rename_tac f, clarify) 
+apply (frule is_recfun_type)
+apply (rule_tac x=f in exI) 
+apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
+                 is_omult_fun_def Ord_trans [OF _ succI1])
+apply (force dest: Ord_in_Ord' 
+             simp add: omult_eqns_def the_omult_eqns_0 the_omult_eqns_succ
+                       the_omult_eqns_Limit) 
+done
+
+lemma (in M_recursion) is_omult_fun_apply_0:
+    "[| 0 < j; is_omult_fun(M,i,j,f) |] ==> f`0 = 0"
+by (simp add: is_omult_fun_def omult_eqns_def lt_def ball_conj_distrib)
+
+lemma (in M_recursion) is_omult_fun_apply_succ:
+    "[| succ(x) < j; is_omult_fun(M,i,j,f) |] ==> f`succ(x) = f`x ++ i"
+by (simp add: is_omult_fun_def omult_eqns_def lt_def, blast) 
+
+lemma (in M_recursion) is_omult_fun_apply_Limit:
+    "[| x < j; Limit(x); M(j); M(f); is_omult_fun(M,i,j,f) |] 
+     ==> f ` x = (\<Union>y\<in>x. f`y)"
+apply (simp add: is_omult_fun_def omult_eqns_def domain_closed lt_def, clarify)
+apply (drule subset_trans [OF OrdmemD], assumption+)  
+apply (simp add: ball_conj_distrib omult_Limit image_function)
+done
+
+lemma (in M_recursion) is_omult_fun_eq_omult:
+    "[| is_omult_fun(M,i,J,f); M(J); M(f); Ord(i); Ord(j) |] 
+     ==> j<J --> f`j = i**j"
+apply (erule_tac i=j in trans_induct3)
+apply (safe del: impCE)
+  apply (simp add: is_omult_fun_apply_0) 
+ apply (subgoal_tac "x<J") 
+  apply (simp add: is_omult_fun_apply_succ omult_succ)  
+ apply (blast intro: lt_trans) 
+apply (subgoal_tac "\<forall>k\<in>x. k<J")
+ apply (simp add: is_omult_fun_apply_Limit omult_Limit) 
+apply (blast intro: lt_trans ltI lt_Ord) 
+done
+
+lemma (in M_recursion) omult_abs_fun_apply_iff:
+    "[| M(i); M(J); M(f); M(k); j<J; is_omult_fun(M,i,J,f) |] 
+     ==> fun_apply(M,f,j,k) <-> f`j = k"
+by (auto simp add: lt_def is_omult_fun_def subsetD apply_abs) 
+
+lemma (in M_recursion) omult_abs:
+    "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_omult(M,i,j,k) <-> k = i**j"
+apply (simp add: is_omult_def omult_abs_fun_apply_iff is_omult_fun_eq_omult)
+apply (frule exists_omult_fun [of j i], blast+)
+done
+
+end
+
diff -r 74d9144c452c -r 45be08fbdcff src/ZF/Constructible/Wellorderings.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/Wellorderings.thy	Wed Jun 19 11:48:01 2002 +0200
@@ -0,0 +1,626 @@
+header {*Relativized Wellorderings*}
+
+theory Wellorderings = Relative:
+
+text{*We define functions analogous to @{term ordermap} @{term ordertype} 
+      but without using recursion.  Instead, there is a direct appeal
+      to Replacement.  This will be the basis for a version relativized
+      to some class @{text M}.  The main result is Theorem I 7.6 in Kunen,
+      page 17.*}
+
+
+subsection{*Wellorderings*}
+
+constdefs
+  irreflexive :: "[i=>o,i,i]=>o"
+    "irreflexive(M,A,r) == \<forall>x\<in>A. M(x) --> <x,x> \<notin> r"
+  
+  transitive_rel :: "[i=>o,i,i]=>o"
+    "transitive_rel(M,A,r) == 
+	\<forall>x\<in>A. M(x) --> (\<forall>y\<in>A. M(y) --> (\<forall>z\<in>A. M(z) --> 
+                          <x,y>\<in>r --> <y,z>\<in>r --> <x,z>\<in>r))"
+
+  linear_rel :: "[i=>o,i,i]=>o"
+    "linear_rel(M,A,r) == 
+	\<forall>x\<in>A. M(x) --> (\<forall>y\<in>A. M(y) --> <x,y>\<in>r | x=y | <y,x>\<in>r)"
+
+  wellfounded :: "[i=>o,i]=>o"
+    --{*EVERY non-empty set has an @{text r}-minimal element*}
+    "wellfounded(M,r) == 
+	\<forall>x. M(x) --> ~ empty(M,x) 
+                 --> (\<exists>y\<in>x. M(y) & ~(\<exists>z\<in>x. M(z) & <z,y> \<in> r))"
+  wellfounded_on :: "[i=>o,i,i]=>o"
+    --{*every non-empty SUBSET OF @{text A} has an @{text r}-minimal element*}
+    "wellfounded_on(M,A,r) == 
+	\<forall>x. M(x) --> ~ empty(M,x) --> subset(M,x,A)
+                 --> (\<exists>y\<in>x. M(y) & ~(\<exists>z\<in>x. M(z) & <z,y> \<in> r))"
+
+  wellordered :: "[i=>o,i,i]=>o"
+    --{*every non-empty subset of @{text A} has an @{text r}-minimal element*}
+    "wellordered(M,A,r) == 
+	transitive_rel(M,A,r) & linear_rel(M,A,r) & wellfounded_on(M,A,r)"
+
+
+subsubsection {*Trivial absoluteness proofs*}
+
+lemma (in M_axioms) irreflexive_abs [simp]: 
+     "M(A) ==> irreflexive(M,A,r) <-> irrefl(A,r)"
+by (simp add: irreflexive_def irrefl_def)
+
+lemma (in M_axioms) transitive_rel_abs [simp]: 
+     "M(A) ==> transitive_rel(M,A,r) <-> trans[A](r)"
+by (simp add: transitive_rel_def trans_on_def)
+
+lemma (in M_axioms) linear_rel_abs [simp]: 
+     "M(A) ==> linear_rel(M,A,r) <-> linear(A,r)"
+by (simp add: linear_rel_def linear_def)
+
+lemma (in M_axioms) wellordered_is_trans_on: 
+    "[| wellordered(M,A,r); M(A) |] ==> trans[A](r)"
+by (auto simp add: wellordered_def )
+
+lemma (in M_axioms) wellordered_is_linear: 
+    "[| wellordered(M,A,r); M(A) |] ==> linear(A,r)"
+by (auto simp add: wellordered_def )
+
+lemma (in M_axioms) wellordered_is_wellfounded_on: 
+    "[| wellordered(M,A,r); M(A) |] ==> wellfounded_on(M,A,r)"
+by (auto simp add: wellordered_def )
+
+lemma (in M_axioms) wellfounded_imp_wellfounded_on: 
+    "[| wellfounded(M,r); M(A) |] ==> wellfounded_on(M,A,r)"
+by (auto simp add: wellfounded_def wellfounded_on_def)
+
+
+subsubsection {*Well-founded relations*}
+
+lemma  (in M_axioms) wellfounded_on_iff_wellfounded:
+     "wellfounded_on(M,A,r) <-> wellfounded(M, r \<inter> A*A)"
+apply (simp add: wellfounded_on_def wellfounded_def, safe)
+ apply blast 
+apply (drule_tac x=x in spec, blast) 
+done
+
+lemma (in M_axioms) wellfounded_on_induct: 
+     "[| a\<in>A;  wellfounded_on(M,A,r);  M(A);  
+       separation(M, \<lambda>x. x\<in>A --> ~P(x));  
+       \<forall>x\<in>A. M(x) & (\<forall>y\<in>A. <y,x> \<in> r --> P(y)) --> P(x) |]
+      ==> P(a)";
+apply (simp (no_asm_use) add: wellfounded_on_def)
+apply (drule_tac x="{z\<in>A. z\<in>A --> ~P(z)}" in spec)
+apply (blast intro: transM) 
+done
+
+text{*The assumption @{term "r \<subseteq> A*A"} justifies strengthening the induction
+      hypothesis by removing the restriction to @{term A}.*}
+lemma (in M_axioms) wellfounded_on_induct2: 
+     "[| a\<in>A;  wellfounded_on(M,A,r);  M(A);  r \<subseteq> A*A;  
+       separation(M, \<lambda>x. x\<in>A --> ~P(x));  
+       \<forall>x\<in>A. M(x) & (\<forall>y. <y,x> \<in> r --> P(y)) --> P(x) |]
+      ==> P(a)";
+by (rule wellfounded_on_induct, assumption+, blast)
+
+
+subsubsection {*Kunen's lemma IV 3.14, page 123*}
+
+lemma (in M_axioms) linear_imp_relativized: 
+     "linear(A,r) ==> linear_rel(M,A,r)" 
+by (simp add: linear_def linear_rel_def) 
+
+lemma (in M_axioms) trans_on_imp_relativized: 
+     "trans[A](r) ==> transitive_rel(M,A,r)" 
+by (unfold transitive_rel_def trans_on_def, blast) 
+
+lemma (in M_axioms) wf_on_imp_relativized: 
+     "wf[A](r) ==> wellfounded_on(M,A,r)" 
+apply (simp add: wellfounded_on_def wf_def wf_on_def, clarify) 
+apply (drule_tac x="x" in spec, blast) 
+done
+
+lemma (in M_axioms) wf_imp_relativized: 
+     "wf(r) ==> wellfounded(M,r)" 
+apply (simp add: wellfounded_def wf_def, clarify) 
+apply (drule_tac x="x" in spec, blast) 
+done
+
+lemma (in M_axioms) well_ord_imp_relativized: 
+     "well_ord(A,r) ==> wellordered(M,A,r)" 
+by (simp add: wellordered_def well_ord_def tot_ord_def part_ord_def
+       linear_imp_relativized trans_on_imp_relativized wf_on_imp_relativized)
+
+
+subsection{* Relativized versions of order-isomorphisms and order types *}
+
+lemma (in M_axioms) order_isomorphism_abs [simp]: 
+     "[| M(A); M(B); M(f) |] 
+      ==> order_isomorphism(M,A,r,B,s,f) <-> f \<in> ord_iso(A,r,B,s)"
+by (simp add: typed_apply_abs [OF bij_is_fun] apply_closed 
+              order_isomorphism_def ord_iso_def)
+
+
+lemma (in M_axioms) pred_set_abs [simp]: 
+     "[| M(r); M(B) |] ==> pred_set(M,A,x,r,B) <-> B = Order.pred(A,x,r)"
+apply (simp add: pred_set_def Order.pred_def)
+apply (blast dest: transM) 
+done
+
+lemma (in M_axioms) pred_closed [intro]: 
+     "[| M(A); M(r); M(x) |] ==> M(Order.pred(A,x,r))"
+apply (simp add: Order.pred_def) 
+apply (insert pred_separation [of r x], simp, blast) 
+done
+
+lemma (in M_axioms) membership_abs [simp]: 
+     "[| M(r); M(A) |] ==> membership(M,A,r) <-> r = Memrel(A)"
+apply (simp add: membership_def Memrel_def, safe)
+  apply (rule equalityI) 
+   apply clarify 
+   apply (frule transM, assumption)
+   apply blast
+  apply clarify 
+  apply (subgoal_tac "M(<xb,ya>)", blast) 
+  apply (blast dest: transM) 
+ apply auto 
+done
+
+lemma (in M_axioms) M_Memrel_iff:
+     "M(A) ==> 
+      Memrel(A) = {z \<in> A*A. \<exists>x. M(x) \<and> (\<exists>y. M(y) \<and> z = \<langle>x,y\<rangle> \<and> x \<in> y)}"
+apply (simp add: Memrel_def) 
+apply (blast dest: transM)
+done 
+
+lemma (in M_axioms) Memrel_closed [intro]: 
+     "M(A) ==> M(Memrel(A))"
+apply (simp add: M_Memrel_iff) 
+apply (insert Memrel_separation, simp, blast)
+done
+
+
+subsection {* Main results of Kunen, Chapter 1 section 6 *}
+
+text{*Subset properties-- proved outside the locale*}
+
+lemma linear_rel_subset: 
+    "[| linear_rel(M,A,r);  B<=A |] ==> linear_rel(M,B,r)"
+by (unfold linear_rel_def, blast)
+
+lemma transitive_rel_subset: 
+    "[| transitive_rel(M,A,r);  B<=A |] ==> transitive_rel(M,B,r)"
+by (unfold transitive_rel_def, blast)
+
+lemma wellfounded_on_subset: 
+    "[| wellfounded_on(M,A,r);  B<=A |] ==> wellfounded_on(M,B,r)"
+by (unfold wellfounded_on_def subset_def, blast)
+
+lemma wellordered_subset: 
+    "[| wellordered(M,A,r);  B<=A |] ==> wellordered(M,B,r)"
+apply (unfold wellordered_def)
+apply (blast intro: linear_rel_subset transitive_rel_subset 
+		    wellfounded_on_subset)
+done
+
+text{*Inductive argument for Kunen's Lemma 6.1, etc.
+      Simple proof from Halmos, page 72*}
+lemma  (in M_axioms) wellordered_iso_subset_lemma: 
+     "[| wellordered(M,A,r);  f \<in> ord_iso(A,r, A',r);  A'<= A;  y \<in> A;  
+       M(A);  M(f);  M(r) |] ==> ~ <f`y, y> \<in> r"
+apply (unfold wellordered_def ord_iso_def)
+apply (elim conjE CollectE) 
+apply (erule wellfounded_on_induct, assumption+)
+ apply (insert well_ord_iso_separation [of A f r])
+ apply (simp add: typed_apply_abs [OF bij_is_fun] apply_closed, clarify) 
+apply (drule_tac a = x in bij_is_fun [THEN apply_type], assumption, blast)
+done
+
+
+text{*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment
+      of a well-ordering*}
+lemma (in M_axioms) wellordered_iso_predD:
+     "[| wellordered(M,A,r);  f \<in> ord_iso(A, r, Order.pred(A,x,r), r);  
+       M(A);  M(f);  M(r) |] ==> x \<notin> A"
+apply (rule notI) 
+apply (frule wellordered_iso_subset_lemma, assumption)
+apply (auto elim: predE)  
+(*Now we know  ~ (f`x < x) *)
+apply (drule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption)
+(*Now we also know f`x  \<in> pred(A,x,r);  contradiction! *)
+apply (simp add: Order.pred_def)
+done
+
+
+lemma (in M_axioms) wellordered_iso_pred_eq_lemma:
+     "[| f \<in> \<langle>Order.pred(A,y,r), r\<rangle> \<cong> \<langle>Order.pred(A,x,r), r\<rangle>;
+       wellordered(M,A,r); x\<in>A; y\<in>A; M(A); M(f); M(r) |] ==> <x,y> \<notin> r"
+apply (frule wellordered_is_trans_on, assumption)
+apply (rule notI) 
+apply (drule_tac x2=y and x=x and r2=r in 
+         wellordered_subset [OF _ pred_subset, THEN wellordered_iso_predD]) 
+apply (simp add: trans_pred_pred_eq) 
+apply (blast intro: predI dest: transM)+
+done
+
+
+text{*Simple consequence of Lemma 6.1*}
+lemma (in M_axioms) wellordered_iso_pred_eq:
+     "[| wellordered(M,A,r);
+       f \<in> ord_iso(Order.pred(A,a,r), r, Order.pred(A,c,r), r);   
+       M(A);  M(f);  M(r);  a\<in>A;  c\<in>A |] ==> a=c"
+apply (frule wellordered_is_trans_on, assumption)
+apply (frule wellordered_is_linear, assumption)
+apply (erule_tac x=a and y=c in linearE, auto) 
+apply (drule ord_iso_sym)
+(*two symmetric cases*)
+apply (blast dest: wellordered_iso_pred_eq_lemma)+ 
+done
+
+lemma (in M_axioms) wellfounded_on_asym:
+     "[| wellfounded_on(M,A,r);  <a,x>\<in>r;  a\<in>A; x\<in>A;  M(A) |] ==> <x,a>\<notin>r"
+apply (simp add: wellfounded_on_def) 
+apply (drule_tac x="{x,a}" in spec) 
+apply (simp add: cons_closed) 
+apply (blast dest: transM) 
+done
+
+lemma (in M_axioms) wellordered_asym:
+     "[| wellordered(M,A,r);  <a,x>\<in>r;  a\<in>A; x\<in>A;  M(A) |] ==> <x,a>\<notin>r"
+by (simp add: wellordered_def, blast dest: wellfounded_on_asym)
+
+
+text{*Surely a shorter proof using lemmas in @{text Order}?
+     Like well_ord_iso_preserving?*}
+lemma (in M_axioms) ord_iso_pred_imp_lt:
+     "[| f \<in> ord_iso(Order.pred(A,x,r), r, i, Memrel(i));
+       g \<in> ord_iso(Order.pred(A,y,r), r, j, Memrel(j));
+       wellordered(M,A,r);  x \<in> A;  y \<in> A; M(A); M(r); M(f); M(g); M(j);
+       Ord(i); Ord(j); \<langle>x,y\<rangle> \<in> r |]
+      ==> i < j"
+apply (frule wellordered_is_trans_on, assumption)
+apply (frule_tac y=y in transM, assumption) 
+apply (rule_tac i=i and j=j in Ord_linear_lt, auto)  
+txt{*case @{term "i=j"} yields a contradiction*}
+ apply (rule_tac x1=x and A1="Order.pred(A,y,r)" in 
+          wellordered_iso_predD [THEN notE]) 
+   apply (blast intro: wellordered_subset [OF _ pred_subset]) 
+  apply (simp add: trans_pred_pred_eq)
+  apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans) 
+ apply (simp_all add: pred_iff pred_closed converse_closed comp_closed)
+txt{*case @{term "j<i"} also yields a contradiction*}
+apply (frule restrict_ord_iso2, assumption+) 
+apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun]) 
+apply (frule apply_type, blast intro: ltD) 
+  --{*thus @{term "converse(f)`j \<in> Order.pred(A,x,r)"}*}
+apply (simp add: pred_iff) 
+apply (subgoal_tac
+       "\<exists>h. M(h) & h \<in> ord_iso(Order.pred(A,y,r), r, 
+                               Order.pred(A, converse(f)`j, r), r)")
+ apply (clarify, frule wellordered_iso_pred_eq, assumption+)
+ apply (blast dest: wellordered_asym)  
+apply (intro exI conjI) 
+ prefer 2 apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans)+
+done
+
+
+lemma ord_iso_converse1:
+     "[| f: ord_iso(A,r,B,s);  <b, f`a>: s;  a:A;  b:B |] 
+      ==> <converse(f) ` b, a> : r"
+apply (frule ord_iso_converse, assumption+) 
+apply (blast intro: ord_iso_is_bij [THEN bij_is_fun, THEN apply_funtype]) 
+apply (simp add: left_inverse_bij [OF ord_iso_is_bij])
+done
+
+
+subsection {* Order Types: A Direct Construction by Replacement*}
+
+text{*This follows Kunen's Theorem I 7.6, page 17.*}
+
+constdefs
+  
+  obase :: "[i=>o,i,i,i] => o"
+       --{*the domain of @{text om}, eventually shown to equal @{text A}*}
+   "obase(M,A,r,z) == 
+	\<forall>a. M(a) --> 
+         (a \<in> z <-> 
+          (a\<in>A & (\<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) & ordinal(M,x) & 
+                               membership(M,x,mx) & pred_set(M,A,a,r,par) &  
+                               order_isomorphism(M,par,r,x,mx,g))))"
+
+
+  omap :: "[i=>o,i,i,i] => o"  
+    --{*the function that maps wosets to order types*}
+   "omap(M,A,r,f) == 
+	\<forall>z. M(z) --> 
+         (z \<in> f <-> 
+          (\<exists>a\<in>A. M(a) & 
+           (\<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) & ordinal(M,x) & 
+                         pair(M,a,x,z) & membership(M,x,mx) & 
+                         pred_set(M,A,a,r,par) &  
+                         order_isomorphism(M,par,r,x,mx,g))))"
+
+
+  otype :: "[i=>o,i,i,i] => o"  --{*the order types themselves*}
+   "otype(M,A,r,i) == \<exists>f. M(f) & omap(M,A,r,f) & is_range(M,f,i)"
+
+
+
+lemma (in M_axioms) obase_iff:
+     "[| M(A); M(r); M(z) |] 
+      ==> obase(M,A,r,z) <-> 
+          z = {a\<in>A. \<exists>x g. M(x) & M(g) & Ord(x) & 
+                          g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))}"
+apply (simp add: obase_def Memrel_closed pred_closed)
+apply (rule iffI) 
+ prefer 2 apply blast 
+apply (rule equalityI) 
+ apply (clarify, frule transM, assumption, rotate_tac -1, simp) 
+apply (clarify, frule transM, assumption, force)
+done
+
+text{*Can also be proved with the premise @{term "M(z)"} instead of
+      @{term "M(f)"}, but that version is less useful.*}
+lemma (in M_axioms) omap_iff:
+     "[| omap(M,A,r,f); M(A); M(r); M(f) |] 
+      ==> z \<in> f <->
+      (\<exists>a\<in>A. \<exists>x g. M(x) & M(g) & z = <a,x> & Ord(x) & 
+                   g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
+apply (rotate_tac 1) 
+apply (simp add: omap_def Memrel_closed pred_closed) 
+apply (rule iffI) 
+apply (drule_tac x=z in spec, blast dest: transM)+ 
+done
+
+lemma (in M_axioms) omap_unique:
+     "[| omap(M,A,r,f); omap(M,A,r,f'); M(A); M(r); M(f); M(f') |] ==> f' = f" 
+apply (rule equality_iffI) 
+apply (simp add: omap_iff) 
+done
+
+lemma (in M_axioms) omap_yields_Ord:
+     "[| omap(M,A,r,f); \<langle>a,x\<rangle> \<in> f; M(a); M(x) |]  ==> Ord(x)"
+apply (simp add: omap_def, blast) 
+done
+
+lemma (in M_axioms) otype_iff:
+     "[| otype(M,A,r,i); M(A); M(r); M(i) |] 
+      ==> x \<in> i <-> 
+          (\<exists>a\<in>A. \<exists>g. M(x) & M(g) & Ord(x) & 
+                     g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
+apply (simp add: otype_def, auto)
+  apply (blast dest: transM)
+ apply (blast dest!: omap_iff intro: transM)
+apply (rename_tac a g) 
+apply (rule_tac a=a in rangeI) 
+apply (frule transM, assumption)
+apply (simp add: omap_iff, blast)
+done
+
+lemma (in M_axioms) otype_eq_range:
+     "[| omap(M,A,r,f); otype(M,A,r,i); M(A); M(r); M(f); M(i) |] ==> i = range(f)"
+apply (auto simp add: otype_def omap_iff)
+apply (blast dest: omap_unique) 
+done
+
+
+lemma (in M_axioms) Ord_otype:
+     "[| otype(M,A,r,i); trans[A](r); M(A); M(r); M(i) |] ==> Ord(i)"
+apply (rotate_tac 1) 
+apply (rule OrdI) 
+prefer 2 
+    apply (simp add: Ord_def otype_def omap_def) 
+    apply clarify 
+    apply (frule pair_components_in_M, assumption) 
+    apply blast 
+apply (auto simp add: Transset_def otype_iff) 
+ apply (blast intro: transM)
+apply (rename_tac y a g)
+apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun, 
+			  THEN apply_funtype],  assumption)  
+apply (rule_tac x="converse(g)`y" in bexI)
+ apply (frule_tac a="converse(g) ` y" in ord_iso_restrict_pred, assumption) 
+apply (safe elim!: predE) 
+apply (intro conjI exI) 
+prefer 3
+  apply (blast intro: restrict_ord_iso ord_iso_sym ltI)
+ apply (blast intro: transM)
+ apply (blast intro: Ord_in_Ord)
+done
+
+lemma (in M_axioms) domain_omap:
+     "[| omap(M,A,r,f);  obase(M,A,r,B); M(A); M(r); M(B); M(f) |] 
+      ==> domain(f) = B"
+apply (rotate_tac 2) 
+apply (simp add: domain_closed obase_iff) 
+apply (rule equality_iffI) 
+apply (simp add: domain_iff omap_iff, blast) 
+done
+
+lemma (in M_axioms) omap_subset: 
+     "[| omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
+       M(A); M(r); M(f); M(B); M(i) |] ==> f \<subseteq> B * i"
+apply (rotate_tac 3, clarify) 
+apply (simp add: omap_iff obase_iff) 
+apply (force simp add: otype_iff) 
+done
+
+lemma (in M_axioms) omap_funtype: 
+     "[| omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
+       M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> B -> i"
+apply (rotate_tac 3) 
+apply (simp add: domain_omap omap_subset Pi_iff function_def omap_iff) 
+apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans) 
+done
+
+
+lemma (in M_axioms) wellordered_omap_bij:
+     "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
+       M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> bij(B,i)"
+apply (insert omap_funtype [of A r f B i]) 
+apply (auto simp add: bij_def inj_def) 
+prefer 2  apply (blast intro: fun_is_surj dest: otype_eq_range) 
+apply (frule_tac a="w" in apply_Pair, assumption) 
+apply (frule_tac a="x" in apply_Pair, assumption) 
+apply (simp add: omap_iff) 
+apply (blast intro: wellordered_iso_pred_eq ord_iso_sym ord_iso_trans) 
+done
+
+
+text{*This is not the final result: we must show @{term "oB(A,r) = A"}*}
+lemma (in M_axioms) omap_ord_iso:
+     "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
+       M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> ord_iso(B,r,i,Memrel(i))"
+apply (rule ord_isoI)
+ apply (erule wellordered_omap_bij, assumption+) 
+apply (insert omap_funtype [of A r f B i], simp) 
+apply (frule_tac a="x" in apply_Pair, assumption) 
+apply (frule_tac a="y" in apply_Pair, assumption) 
+apply (auto simp add: omap_iff)
+ txt{*direction 1: assuming @{term "\<langle>x,y\<rangle> \<in> r"}*}
+ apply (blast intro: ltD ord_iso_pred_imp_lt)
+ txt{*direction 2: proving @{term "\<langle>x,y\<rangle> \<in> r"} using linearity of @{term r}*}
+apply (rename_tac x y g ga) 
+apply (frule wellordered_is_linear, assumption, 
+       erule_tac x=x and y=y in linearE, assumption+) 
+txt{*the case @{term "x=y"} leads to immediate contradiction*} 
+apply (blast elim: mem_irrefl) 
+txt{*the case @{term "\<langle>y,x\<rangle> \<in> r"}: handle like the opposite direction*}
+apply (blast dest: ord_iso_pred_imp_lt ltD elim: mem_asym) 
+done
+
+lemma (in M_axioms) Ord_omap_image_pred:
+     "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
+       M(A); M(r); M(f); M(B); M(i); b \<in> A |] ==> Ord(f `` Order.pred(A,b,r))"
+apply (frule wellordered_is_trans_on, assumption)
+apply (rule OrdI) 
+	prefer 2 apply (simp add: image_iff omap_iff Ord_def, blast) 
+txt{*Hard part is to show that the image is a transitive set.*}
+apply (rotate_tac 3)
+apply (simp add: Transset_def, clarify) 
+apply (simp add: image_iff pred_iff apply_iff [OF omap_funtype [of A r f B i]])
+apply (rename_tac c j, clarify)
+apply (frule omap_funtype [of A r f B, THEN apply_funtype], assumption+)
+apply (subgoal_tac "j : i") 
+	prefer 2 apply (blast intro: Ord_trans Ord_otype)
+apply (subgoal_tac "converse(f) ` j : B") 
+	prefer 2 
+	apply (blast dest: wellordered_omap_bij [THEN bij_converse_bij, 
+                                      THEN bij_is_fun, THEN apply_funtype])
+apply (rule_tac x="converse(f) ` j" in bexI) 
+ apply (simp add: right_inverse_bij [OF wellordered_omap_bij]) 
+apply (intro predI conjI)
+ apply (erule_tac b=c in trans_onD) 
+ apply (rule ord_iso_converse1 [OF omap_ord_iso [of A r f B i]])
+apply (auto simp add: obase_iff)
+done
+
+lemma (in M_axioms) restrict_omap_ord_iso:
+     "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
+       D \<subseteq> B; M(A); M(r); M(f); M(B); M(i) |] 
+      ==> restrict(f,D) \<in> (\<langle>D,r\<rangle> \<cong> \<langle>f``D, Memrel(f``D)\<rangle>)"
+apply (frule ord_iso_restrict_image [OF omap_ord_iso [of A r f B i]], 
+       assumption+)
+apply (drule ord_iso_sym [THEN subset_ord_iso_Memrel]) 
+apply (blast dest: subsetD [OF omap_subset]) 
+apply (drule ord_iso_sym, simp) 
+done
+
+lemma (in M_axioms) obase_equals: 
+     "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i);
+       M(A); M(r); M(f); M(B); M(i) |] ==> B = A"
+apply (rotate_tac 4)
+apply (rule equalityI, force simp add: obase_iff, clarify) 
+apply (subst obase_iff [of A r B, THEN iffD1], assumption+, simp) 
+apply (frule wellordered_is_wellfounded_on, assumption)
+apply (erule wellfounded_on_induct, assumption+)
+ apply (insert obase_equals_separation, simp add: Memrel_closed pred_closed, clarify) 
+apply (rename_tac b) 
+apply (subgoal_tac "Order.pred(A,b,r) <= B") 
+ prefer 2 apply (force simp add: pred_iff obase_iff)  
+apply (intro conjI exI) 
+    prefer 4 apply (blast intro: restrict_omap_ord_iso) 
+apply (blast intro: Ord_omap_image_pred)+
+done
+
+
+
+text{*Main result: @{term om} gives the order-isomorphism 
+      @{term "\<langle>A,r\<rangle> \<cong> \<langle>i, Memrel(i)\<rangle>"} *}
+theorem (in M_axioms) omap_ord_iso_otype:
+     "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i);
+       M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> ord_iso(A, r, i, Memrel(i))"
+apply (frule omap_ord_iso, assumption+) 
+apply (frule obase_equals, assumption+, blast) 
+done
+
+lemma (in M_axioms) obase_exists:
+     "[| M(A); M(r) |] ==> \<exists>z. M(z) & obase(M,A,r,z)"
+apply (simp add: obase_def) 
+apply (insert obase_separation [of A r])
+apply (simp add: separation_def)  
+done
+
+lemma (in M_axioms) omap_exists:
+     "[| M(A); M(r) |] ==> \<exists>z. M(z) & omap(M,A,r,z)"
+apply (insert obase_exists [of A r]) 
+apply (simp add: omap_def) 
+apply (insert omap_replacement [of A r])
+apply (simp add: strong_replacement_def, clarify) 
+apply (drule_tac x=z in spec, clarify) 
+apply (simp add: Memrel_closed pred_closed obase_iff)
+apply (erule impE) 
+ apply (clarsimp simp add: univalent_def)
+ apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans, clarify)  
+apply (rule_tac x=Y in exI) 
+apply (simp add: Memrel_closed pred_closed obase_iff, blast)   
+done
+
+lemma (in M_axioms) otype_exists:
+     "[| wellordered(M,A,r); M(A); M(r) |] ==> \<exists>i. M(i) & otype(M,A,r,i)"
+apply (insert omap_exists [of A r]) 
+apply (simp add: otype_def, clarify) 
+apply (rule_tac x="range(z)" in exI) 
+apply blast 
+done
+
+theorem (in M_axioms) omap_ord_iso_otype:
+     "[| wellordered(M,A,r); M(A); M(r) |]
+      ==> \<exists>f. M(f) & (\<exists>i. M(i) & Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))"
+apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify)
+apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype) 
+apply (rule Ord_otype) 
+    apply (force simp add: otype_def range_closed) 
+   apply (simp_all add: wellordered_is_trans_on) 
+done
+
+lemma (in M_axioms) ordertype_exists:
+     "[| wellordered(M,A,r); M(A); M(r) |]
+      ==> \<exists>f. M(f) & (\<exists>i. M(i) & Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))"
+apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify)
+apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype) 
+apply (rule Ord_otype) 
+    apply (force simp add: otype_def range_closed) 
+   apply (simp_all add: wellordered_is_trans_on) 
+done
+
+
+lemma (in M_axioms) relativized_imp_well_ord: 
+     "[| wellordered(M,A,r); M(A); M(r) |] ==> well_ord(A,r)" 
+apply (insert ordertype_exists [of A r], simp)
+apply (blast intro: well_ord_ord_iso well_ord_Memrel )  
+done
+
+subsection {*Kunen's theorem 5.4, poage 127*}
+
+text{*(a) The notion of Wellordering is absolute*}
+theorem (in M_axioms) well_ord_abs [simp]: 
+     "[| M(A); M(r) |] ==> wellordered(M,A,r) <-> well_ord(A,r)" 
+by (blast intro: well_ord_imp_relativized relativized_imp_well_ord)  
+
+
+text{*(b) Order types are absolute*}
+lemma (in M_axioms) 
+     "[| wellordered(M,A,r); f \<in> ord_iso(A, r, i, Memrel(i));
+       M(A); M(r); M(f); M(i); Ord(i) |] ==> i = ordertype(A,r)"
+by (blast intro: Ord_ordertype relativized_imp_well_ord ordertype_ord_iso
+                 Ord_iso_implies_eq ord_iso_sym ord_iso_trans)
+
+end