# HG changeset patch
# User paulson
# Date 1034844851 -7200
# Node ID ac80e101306aa05edb002fa26c8d247c3462ab12
# Parent  31bd2a8cdbe2beb5f678777ec6229f6277eed577
Cosmetic changes suggested by writing the paper.  Deleted some
redundant arity proofs

diff -r 31bd2a8cdbe2 -r ac80e101306a src/ZF/Constructible/Formula.thy
--- a/src/ZF/Constructible/Formula.thy	Thu Oct 17 10:52:59 2002 +0200
+++ b/src/ZF/Constructible/Formula.thy	Thu Oct 17 10:54:11 2002 +0200
@@ -453,9 +453,9 @@
 apply (simp add: DPow_def, blast) 
 done
 
-lemma singleton_in_DPow: "x \<in> A ==> {x} \<in> DPow(A)"
+lemma singleton_in_DPow: "a \<in> A ==> {a} \<in> DPow(A)"
 apply (simp add: DPow_def)
-apply (rule_tac x="Cons(x,Nil)" in bexI) 
+apply (rule_tac x="Cons(a,Nil)" in bexI) 
  apply (rule_tac x="Equal(0,1)" in bexI) 
   apply typecheck
 apply (force simp add: succ_Un_distrib [symmetric])  
@@ -473,16 +473,16 @@
 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...*)
+text{*@{term DPow} is not monotonic.  For example, let @{term A} be some
+non-constructible set of natural numbers, and let @{term B} be @{term nat}.
+Then @{term "A<=B"} and obviously @{term "A : DPow(A)"} but @{term "A ~:
+DPow(B)"}.*}
+
+(*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
-
-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)
@@ -493,14 +493,16 @@
 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{*Internalized Formulas for the Ordinals*}
 
-
-subsection{*Internalized formulas for basic concepts*}
+text{*The @{text sats} theorems below differ from the usual form in that they
+include an element of absoluteness.  That is, they relate internalized
+formulas to real concepts such as the subset relation, rather than to the
+relativized concepts defined in theory @{text Relative}.  This lets us prove
+the theorem as @{text Ords_in_DPow} without first having to instantiate the
+locale @{text M_trivial}.  Note that the present theory does not even take
+@{text Relative} as a parent.*}
 
 subsubsection{*The subset relation*}
 
@@ -563,12 +565,25 @@
 apply (blast intro: nth_type) 
 done
 
+text{*The subset consisting of the ordinals is definable.  Essential lemma for
+@{text Ord_in_Lset}.  This result is the objective of the present subsection.*}
+theorem 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 
+
 
 subsection{* Constant Lset: Levels of the Constructible Universe *}
 
-constdefs Lset :: "i=>i"
+constdefs
+  Lset :: "i=>i"
     "Lset(i) == transrec(i, %x f. \<Union>y\<in>x. DPow(f`y))"
 
+  L :: "i=>o" --{*Kunen's definition VI 1.5, page 167*}
+    "L(x) == \<exists>i. Ord(i) & x \<in> Lset(i)"
+  
 text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
 lemma Lset: "Lset(i) = (UN j:i. DPow(Lset(j)))"
 by (subst Lset_def [THEN def_transrec], simp)
@@ -601,7 +616,7 @@
 apply (blast intro: elem_subset_in_DPow dest: DPowD) 
 done
 
-text{*Kunen's VI, 1.6 (a)*}
+text{*Kunen's VI 1.6 (a)*}
 lemma Transset_Lset: "Transset(Lset(i))"
 apply (rule_tac a=i in eps_induct)
 apply (subst Lset)
@@ -615,7 +630,7 @@
 
 subsubsection{* Monotonicity *}
 
-text{*Kunen's VI, 1.6 (b)*}
+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)
@@ -638,7 +653,7 @@
 lemma subset_Lset_ltD: "[|A \<subseteq> Lset(i); i < j|] ==> A \<subseteq> Lset(j)"
 by (blast dest: ltD [THEN Lset_mono_mem]) 
 
-subsubsection{* 0, successor and limit equations fof Lset *}
+subsubsection{* 0, successor and limit equations for Lset *}
 
 lemma Lset_0 [simp]: "Lset(0) = 0"
 by (subst Lset, blast)
@@ -705,15 +720,7 @@
 done
 
 
-subsection{*Constructible Ordinals: Kunen's VI, 1.9 (b)*}
-
-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 
+subsection{*Constructible Ordinals: Kunen's VI 1.9 (b)*}
 
 lemma Ords_of_Lset_eq: "Ord(i) ==> {x\<in>Lset(i). Ord(x)} = i"
 apply (erule trans_induct3)
@@ -744,6 +751,9 @@
        rule Ords_in_DPow [OF Transset_Lset]) 
 done
 
+lemma Ord_in_L: "Ord(i) ==> L(i)"
+by (simp add: L_def, blast intro: Ord_in_Lset)
+
 subsubsection{* Unions *}
 
 lemma Union_in_Lset:
@@ -765,6 +775,12 @@
 apply (blast intro: Limit_has_succ lt_LsetI Union_in_Lset)
 done
 
+theorem 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
+
 subsubsection{* Finite sets and ordered pairs *}
 
 lemma singleton_in_Lset: "a: Lset(i) ==> {a} : Lset(succ(i))"
@@ -780,13 +796,6 @@
 apply (blast intro: doubleton_in_Lset) 
 done
 
-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]
 
@@ -799,6 +808,12 @@
                     Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
 done
 
+theorem 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
+
 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.*}
@@ -809,49 +824,11 @@
                     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*}
+text{*The rank function for the constructible universe*}
 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 :: "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)"
@@ -872,8 +849,9 @@
 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.*}
+text{*Kunen's VI 1.8.  The proof is much harder than the text would
+suggest.  For a start, it needs the previous lemma, which is 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) 
@@ -886,7 +864,7 @@
 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)*}
+text{*Kunen's VI 1.9 (a)*}
 lemma lrank_of_Ord: "Ord(i) ==> lrank(i) = i"
 apply (unfold lrank_def) 
 apply (rule Least_equality) 
@@ -897,13 +875,10 @@
 done
 
 
-lemma Ord_in_L: "Ord(i) ==> L(i)"
-by (blast intro: Ord_in_Lset L_I)
-
 text{*This is lrank(lrank(a)) = lrank(a) *}
 declare Ord_lrank [THEN lrank_of_Ord, simp]
 
-text{*Kunen's VI, 1.10 *}
+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) 
@@ -922,7 +897,7 @@
 apply (blast intro!: le_imp_subset Lset_mono) 
 done
 
-text{*Kunen's VI, 1.11 *}
+text{*Kunen's VI 1.11 *}
 lemma Lset_subset_Vset: "Ord(i) ==> Lset(i) <= Vset(i)";
 apply (erule trans_induct)
 apply (subst Lset) 
@@ -932,7 +907,7 @@
 apply (rule Pow_mono, blast) 
 done
 
-text{*Kunen's VI, 1.12 *}
+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) 
@@ -950,21 +925,7 @@
       ==> P"
 by (blast dest: subset_Lset) 
 
-subsection{*For L to satisfy the ZF axioms*}
-
-theorem 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
-
-theorem 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 *}
+subsubsection{*For L to satisfy the Powerset axiom *}
 
 lemma LPow_env_typing:
     "[| y : Lset(i); Ord(i); y \<subseteq> X |] 
@@ -996,7 +957,6 @@
 
 subsection{*Eliminating @{term arity} from the Definition of @{term Lset}*}
 
-
 lemma nth_zero_eq_0: "n \<in> nat ==> nth(n,[0]) = 0"
 by (induct_tac n, auto)
 
@@ -1046,7 +1006,7 @@
 lemma DPow_eq_DPow': "Transset(A) ==> DPow(A) = DPow'(A)"
 apply (drule Transset_0_disj) 
 apply (erule disjE) 
- apply (simp add: DPow'_0 DPow_0) 
+ apply (simp add: DPow'_0 Finite_DPow_eq_Pow) 
 apply (rule equalityI)
  apply (rule DPow_subset_DPow') 
 apply (erule DPow'_subset_DPow) 
diff -r 31bd2a8cdbe2 -r ac80e101306a src/ZF/Constructible/Internalize.thy
--- a/src/ZF/Constructible/Internalize.thy	Thu Oct 17 10:52:59 2002 +0200
+++ b/src/ZF/Constructible/Internalize.thy	Thu Oct 17 10:54:11 2002 +0200
@@ -726,11 +726,6 @@
      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> cartprod_fm(x,y,z) \<in> formula"
 by (simp add: cartprod_fm_def)
 
-lemma arity_cartprod_fm [simp]:
-     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
-      ==> arity(cartprod_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: cartprod_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_cartprod_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, cartprod_fm(x,y,z), env) <->
@@ -770,11 +765,6 @@
      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> sum_fm(x,y,z) \<in> formula"
 by (simp add: sum_fm_def)
 
-lemma arity_sum_fm [simp]:
-     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
-      ==> arity(sum_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: sum_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_sum_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, sum_fm(x,y,z), env) <->
@@ -805,10 +795,6 @@
      "x \<in> nat ==> quasinat_fm(x) \<in> formula"
 by (simp add: quasinat_fm_def)
 
-lemma arity_quasinat_fm [simp]:
-     "x \<in> nat ==> arity(quasinat_fm(x)) = succ(x)"
-by (simp add: quasinat_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_quasinat_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
     ==> sats(A, quasinat_fm(x), env) <-> is_quasinat(**A, nth(x,env))"
@@ -1081,11 +1067,6 @@
      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> list_functor_fm(x,y,z) \<in> formula"
 by (simp add: list_functor_fm_def)
 
-lemma arity_list_functor_fm [simp]:
-     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
-      ==> arity(list_functor_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: list_functor_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_list_functor_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, list_functor_fm(x,y,z), env) <->
diff -r 31bd2a8cdbe2 -r ac80e101306a src/ZF/Constructible/L_axioms.thy
--- a/src/ZF/Constructible/L_axioms.thy	Thu Oct 17 10:52:59 2002 +0200
+++ b/src/ZF/Constructible/L_axioms.thy	Thu Oct 17 10:54:11 2002 +0200
@@ -88,8 +88,6 @@
 lemma Lset_cont: "cont_Ord(Lset)"
 by (simp add: cont_Ord_def Limit_Lset_eq OUnion_def Limit_is_Ord)
 
-lemmas Pair_in_Lset = Formula.Pair_in_LLimit
-
 lemmas L_nat = Ord_in_L [OF Ord_nat]
 
 theorem M_trivial_L: "PROP M_trivial(L)"
@@ -260,8 +258,9 @@
 
 
 lemma reflection_Lset: "reflection(Lset)"
-apply (blast intro: reflection.intro Lset_mono_le Lset_cont Pair_in_Lset) +
-done
+by (blast intro: reflection.intro Lset_mono_le Lset_cont 
+                 Formula.Pair_in_LLimit)+
+
 
 theorem Ex_reflection:
      "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
@@ -370,10 +369,6 @@
      "x \<in> nat ==> empty_fm(x) \<in> formula"
 by (simp add: empty_fm_def)
 
-lemma arity_empty_fm [simp]:
-     "x \<in> nat ==> arity(empty_fm(x)) = succ(x)"
-by (simp add: empty_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_empty_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
     ==> sats(A, empty_fm(x), env) <-> empty(**A, nth(x,env))"
@@ -416,11 +411,6 @@
      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> upair_fm(x,y,z) \<in> formula"
 by (simp add: upair_fm_def)
 
-lemma arity_upair_fm [simp]:
-     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
-      ==> arity(upair_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: upair_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_upair_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, upair_fm(x,y,z), env) <->
@@ -462,11 +452,6 @@
      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> pair_fm(x,y,z) \<in> formula"
 by (simp add: pair_fm_def)
 
-lemma arity_pair_fm [simp]:
-     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
-      ==> arity(pair_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: pair_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_pair_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, pair_fm(x,y,z), env) <->
@@ -498,11 +483,6 @@
      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> union_fm(x,y,z) \<in> formula"
 by (simp add: union_fm_def)
 
-lemma arity_union_fm [simp]:
-     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
-      ==> arity(union_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: union_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_union_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, union_fm(x,y,z), env) <->
@@ -535,11 +515,6 @@
      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> cons_fm(x,y,z) \<in> formula"
 by (simp add: cons_fm_def)
 
-lemma arity_cons_fm [simp]:
-     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
-      ==> arity(cons_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: cons_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_cons_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, cons_fm(x,y,z), env) <->
@@ -569,11 +544,6 @@
      "[| x \<in> nat; y \<in> nat |] ==> succ_fm(x,y) \<in> formula"
 by (simp add: succ_fm_def)
 
-lemma arity_succ_fm [simp]:
-     "[| x \<in> nat; y \<in> nat |]
-      ==> arity(succ_fm(x,y)) = succ(x) \<union> succ(y)"
-by (simp add: succ_fm_def)
-
 lemma sats_succ_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, succ_fm(x,y), env) <->
@@ -604,10 +574,6 @@
      "x \<in> nat ==> number1_fm(x) \<in> formula"
 by (simp add: number1_fm_def)
 
-lemma arity_number1_fm [simp]:
-     "x \<in> nat ==> arity(number1_fm(x)) = succ(x)"
-by (simp add: number1_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_number1_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
     ==> sats(A, number1_fm(x), env) <-> number1(**A, nth(x,env))"
@@ -639,11 +605,6 @@
      "[| x \<in> nat; y \<in> nat |] ==> big_union_fm(x,y) \<in> formula"
 by (simp add: big_union_fm_def)
 
-lemma arity_big_union_fm [simp]:
-     "[| x \<in> nat; y \<in> nat |]
-      ==> arity(big_union_fm(x,y)) = succ(x) \<union> succ(y)"
-by (simp add: big_union_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_big_union_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, big_union_fm(x,y), env) <->
@@ -666,8 +627,11 @@
 
 subsubsection{*Variants of Satisfaction Definitions for Ordinals, etc.*}
 
-text{*Differs from the one in Formula by using "ordinal" rather than "Ord"*}
-
+text{*The @{text sats} theorems below are standard versions of the ones proved
+in theory @{text Formula}.  They relate elements of type @{term formula} to
+relativized concepts such as @{term subset} or @{term ordinal} rather than to
+real concepts such as @{term Ord}.  Now that we have instantiated the locale
+@{text M_trivial}, we no longer require the earlier versions.*}
 
 lemma sats_subset_fm':
    "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
@@ -724,11 +688,6 @@
      "[| x \<in> nat; y \<in> nat |] ==> Memrel_fm(x,y) \<in> formula"
 by (simp add: Memrel_fm_def)
 
-lemma arity_Memrel_fm [simp]:
-     "[| x \<in> nat; y \<in> nat |]
-      ==> arity(Memrel_fm(x,y)) = succ(x) \<union> succ(y)"
-by (simp add: Memrel_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_Memrel_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, Memrel_fm(x,y), env) <->
@@ -763,11 +722,6 @@
       ==> pred_set_fm(A,x,r,B) \<in> formula"
 by (simp add: pred_set_fm_def)
 
-lemma arity_pred_set_fm [simp]:
-   "[| A \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat |]
-    ==> arity(pred_set_fm(A,x,r,B)) = succ(A) \<union> succ(x) \<union> succ(r) \<union> succ(B)"
-by (simp add: pred_set_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_pred_set_fm [simp]:
    "[| U \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat; env \<in> list(A)|]
     ==> sats(A, pred_set_fm(U,x,r,B), env) <->
@@ -803,11 +757,6 @@
      "[| x \<in> nat; y \<in> nat |] ==> domain_fm(x,y) \<in> formula"
 by (simp add: domain_fm_def)
 
-lemma arity_domain_fm [simp]:
-     "[| x \<in> nat; y \<in> nat |]
-      ==> arity(domain_fm(x,y)) = succ(x) \<union> succ(y)"
-by (simp add: domain_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_domain_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, domain_fm(x,y), env) <->
@@ -842,11 +791,6 @@
      "[| x \<in> nat; y \<in> nat |] ==> range_fm(x,y) \<in> formula"
 by (simp add: range_fm_def)
 
-lemma arity_range_fm [simp]:
-     "[| x \<in> nat; y \<in> nat |]
-      ==> arity(range_fm(x,y)) = succ(x) \<union> succ(y)"
-by (simp add: range_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_range_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, range_fm(x,y), env) <->
@@ -882,11 +826,6 @@
      "[| x \<in> nat; y \<in> nat |] ==> field_fm(x,y) \<in> formula"
 by (simp add: field_fm_def)
 
-lemma arity_field_fm [simp]:
-     "[| x \<in> nat; y \<in> nat |]
-      ==> arity(field_fm(x,y)) = succ(x) \<union> succ(y)"
-by (simp add: field_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_field_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, field_fm(x,y), env) <->
@@ -923,11 +862,6 @@
      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> image_fm(x,y,z) \<in> formula"
 by (simp add: image_fm_def)
 
-lemma arity_image_fm [simp]:
-     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
-      ==> arity(image_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: image_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_image_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, image_fm(x,y,z), env) <->
@@ -963,11 +897,6 @@
      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> pre_image_fm(x,y,z) \<in> formula"
 by (simp add: pre_image_fm_def)
 
-lemma arity_pre_image_fm [simp]:
-     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
-      ==> arity(pre_image_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: pre_image_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_pre_image_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, pre_image_fm(x,y,z), env) <->
@@ -1003,11 +932,6 @@
      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> fun_apply_fm(x,y,z) \<in> formula"
 by (simp add: fun_apply_fm_def)
 
-lemma arity_fun_apply_fm [simp]:
-     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
-      ==> arity(fun_apply_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: fun_apply_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_fun_apply_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, fun_apply_fm(x,y,z), env) <->
@@ -1041,10 +965,6 @@
      "[| x \<in> nat |] ==> relation_fm(x) \<in> formula"
 by (simp add: relation_fm_def)
 
-lemma arity_relation_fm [simp]:
-     "x \<in> nat ==> arity(relation_fm(x)) = succ(x)"
-by (simp add: relation_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_relation_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
     ==> sats(A, relation_fm(x), env) <-> is_relation(**A, nth(x,env))"
@@ -1081,10 +1001,6 @@
      "[| x \<in> nat |] ==> function_fm(x) \<in> formula"
 by (simp add: function_fm_def)
 
-lemma arity_function_fm [simp]:
-     "x \<in> nat ==> arity(function_fm(x)) = succ(x)"
-by (simp add: function_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_function_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
     ==> sats(A, function_fm(x), env) <-> is_function(**A, nth(x,env))"
@@ -1122,11 +1038,6 @@
      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> typed_function_fm(x,y,z) \<in> formula"
 by (simp add: typed_function_fm_def)
 
-lemma arity_typed_function_fm [simp]:
-     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
-      ==> arity(typed_function_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: typed_function_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_typed_function_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, typed_function_fm(x,y,z), env) <->
@@ -1187,11 +1098,6 @@
      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> composition_fm(x,y,z) \<in> formula"
 by (simp add: composition_fm_def)
 
-lemma arity_composition_fm [simp]:
-     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
-      ==> arity(composition_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: composition_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_composition_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, composition_fm(x,y,z), env) <->
@@ -1232,11 +1138,6 @@
      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> injection_fm(x,y,z) \<in> formula"
 by (simp add: injection_fm_def)
 
-lemma arity_injection_fm [simp]:
-     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
-      ==> arity(injection_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: injection_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_injection_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, injection_fm(x,y,z), env) <->
@@ -1274,11 +1175,6 @@
      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> surjection_fm(x,y,z) \<in> formula"
 by (simp add: surjection_fm_def)
 
-lemma arity_surjection_fm [simp]:
-     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
-      ==> arity(surjection_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: surjection_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_surjection_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, surjection_fm(x,y,z), env) <->
@@ -1311,11 +1207,6 @@
      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> bijection_fm(x,y,z) \<in> formula"
 by (simp add: bijection_fm_def)
 
-lemma arity_bijection_fm [simp]:
-     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
-      ==> arity(bijection_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: bijection_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_bijection_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, bijection_fm(x,y,z), env) <->
@@ -1352,11 +1243,6 @@
      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> restriction_fm(x,y,z) \<in> formula"
 by (simp add: restriction_fm_def)
 
-lemma arity_restriction_fm [simp]:
-     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
-      ==> arity(restriction_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: restriction_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_restriction_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, restriction_fm(x,y,z), env) <->
@@ -1404,12 +1290,6 @@
       ==> order_isomorphism_fm(A,r,B,s,f) \<in> formula"
 by (simp add: order_isomorphism_fm_def)
 
-lemma arity_order_isomorphism_fm [simp]:
-     "[| A \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat |]
-      ==> arity(order_isomorphism_fm(A,r,B,s,f)) =
-          succ(A) \<union> succ(r) \<union> succ(B) \<union> succ(s) \<union> succ(f)"
-by (simp add: order_isomorphism_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_order_isomorphism_fm [simp]:
    "[| U \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat; env \<in> list(A)|]
     ==> sats(A, order_isomorphism_fm(U,r,B,s,f), env) <->
@@ -1452,10 +1332,6 @@
      "x \<in> nat ==> limit_ordinal_fm(x) \<in> formula"
 by (simp add: limit_ordinal_fm_def)
 
-lemma arity_limit_ordinal_fm [simp]:
-     "x \<in> nat ==> arity(limit_ordinal_fm(x)) = succ(x)"
-by (simp add: limit_ordinal_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_limit_ordinal_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
     ==> sats(A, limit_ordinal_fm(x), env) <-> limit_ordinal(**A, nth(x,env))"
@@ -1523,10 +1399,6 @@
      "x \<in> nat ==> omega_fm(x) \<in> formula"
 by (simp add: omega_fm_def)
 
-lemma arity_omega_fm [simp]:
-     "x \<in> nat ==> arity(omega_fm(x)) = succ(x)"
-by (simp add: omega_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_omega_fm [simp]:
    "[| x \<in> nat; env \<in> list(A)|]
     ==> sats(A, omega_fm(x), env) <-> omega(**A, nth(x,env))"
diff -r 31bd2a8cdbe2 -r ac80e101306a src/ZF/Constructible/Rec_Separation.thy
--- a/src/ZF/Constructible/Rec_Separation.thy	Thu Oct 17 10:52:59 2002 +0200
+++ b/src/ZF/Constructible/Rec_Separation.thy	Thu Oct 17 10:54:11 2002 +0200
@@ -53,11 +53,6 @@
  "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> rtran_closure_mem_fm(x,y,z) \<in> formula"
 by (simp add: rtran_closure_mem_fm_def)
 
-lemma arity_rtran_closure_mem_fm [simp]:
-     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
-      ==> arity(rtran_closure_mem_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: rtran_closure_mem_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_rtran_closure_mem_fm [simp]:
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, rtran_closure_mem_fm(x,y,z), env) <->
@@ -103,11 +98,6 @@
      "[| x \<in> nat; y \<in> nat |] ==> rtran_closure_fm(x,y) \<in> formula"
 by (simp add: rtran_closure_fm_def)
 
-lemma arity_rtran_closure_fm [simp]:
-     "[| x \<in> nat; y \<in> nat |]
-      ==> arity(rtran_closure_fm(x,y)) = succ(x) \<union> succ(y)"
-by (simp add: rtran_closure_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_rtran_closure_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, rtran_closure_fm(x,y), env) <->
@@ -140,11 +130,6 @@
      "[| x \<in> nat; y \<in> nat |] ==> tran_closure_fm(x,y) \<in> formula"
 by (simp add: tran_closure_fm_def)
 
-lemma arity_tran_closure_fm [simp]:
-     "[| x \<in> nat; y \<in> nat |]
-      ==> arity(tran_closure_fm(x,y)) = succ(x) \<union> succ(y)"
-by (simp add: tran_closure_fm_def succ_Un_distrib [symmetric] Un_ac)
-
 lemma sats_tran_closure_fm [simp]:
    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
     ==> sats(A, tran_closure_fm(x,y), env) <->