Cosmetic changes suggested by writing the paper. Deleted some
authorpaulson
Thu Oct 17 10:54:11 2002 +0200 (2002-10-17)
changeset 13651ac80e101306a
parent 13650 31bd2a8cdbe2
child 13652 172600c40793
Cosmetic changes suggested by writing the paper. Deleted some
redundant arity proofs
src/ZF/Constructible/Formula.thy
src/ZF/Constructible/Internalize.thy
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/Rec_Separation.thy
     1.1 --- a/src/ZF/Constructible/Formula.thy	Thu Oct 17 10:52:59 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Formula.thy	Thu Oct 17 10:54:11 2002 +0200
     1.3 @@ -453,9 +453,9 @@
     1.4  apply (simp add: DPow_def, blast) 
     1.5  done
     1.6  
     1.7 -lemma singleton_in_DPow: "x \<in> A ==> {x} \<in> DPow(A)"
     1.8 +lemma singleton_in_DPow: "a \<in> A ==> {a} \<in> DPow(A)"
     1.9  apply (simp add: DPow_def)
    1.10 -apply (rule_tac x="Cons(x,Nil)" in bexI) 
    1.11 +apply (rule_tac x="Cons(a,Nil)" in bexI) 
    1.12   apply (rule_tac x="Equal(0,1)" in bexI) 
    1.13    apply typecheck
    1.14  apply (force simp add: succ_Un_distrib [symmetric])  
    1.15 @@ -473,16 +473,16 @@
    1.16  apply (blast intro: cons_in_DPow) 
    1.17  done
    1.18  
    1.19 -(*DPow is not monotonic.  For example, let A be some non-constructible set
    1.20 -  of natural numbers, and let B be nat.  Then A<=B and obviously A : DPow(A)
    1.21 -  but A ~: DPow(B).*)
    1.22 -lemma DPow_mono: "A : DPow(B) ==> DPow(A) <= DPow(B)"
    1.23 -apply (simp add: DPow_def, auto) 
    1.24 -(*must use the formula defining A in B to relativize the new formula...*)
    1.25 +text{*@{term DPow} is not monotonic.  For example, let @{term A} be some
    1.26 +non-constructible set of natural numbers, and let @{term B} be @{term nat}.
    1.27 +Then @{term "A<=B"} and obviously @{term "A : DPow(A)"} but @{term "A ~:
    1.28 +DPow(B)"}.*}
    1.29 +
    1.30 +(*This may be true but the proof looks difficult, requiring relativization 
    1.31 +lemma DPow_insert: "DPow (cons(a,A)) = DPow(A) Un {cons(a,X) . X: DPow(A)}"
    1.32 +apply (rule equalityI, safe)
    1.33  oops
    1.34 -
    1.35 -lemma DPow_0: "DPow(0) = {0}" 
    1.36 -by (blast intro: empty_in_DPow dest: DPow_imp_subset)
    1.37 +*)
    1.38  
    1.39  lemma Finite_Pow_subset_Pow: "Finite(A) ==> Pow(A) <= DPow(A)" 
    1.40  by (blast intro: Fin_into_DPow Finite_into_Fin Fin_subset)
    1.41 @@ -493,14 +493,16 @@
    1.42  apply (erule Finite_Pow_subset_Pow) 
    1.43  done
    1.44  
    1.45 -(*This may be true but the proof looks difficult, requiring relativization 
    1.46 -lemma DPow_insert: "DPow (cons(a,A)) = DPow(A) Un {cons(a,X) . X: DPow(A)}"
    1.47 -apply (rule equalityI, safe)
    1.48 -oops
    1.49 -*)
    1.50 +
    1.51 +subsection{*Internalized Formulas for the Ordinals*}
    1.52  
    1.53 -
    1.54 -subsection{*Internalized formulas for basic concepts*}
    1.55 +text{*The @{text sats} theorems below differ from the usual form in that they
    1.56 +include an element of absoluteness.  That is, they relate internalized
    1.57 +formulas to real concepts such as the subset relation, rather than to the
    1.58 +relativized concepts defined in theory @{text Relative}.  This lets us prove
    1.59 +the theorem as @{text Ords_in_DPow} without first having to instantiate the
    1.60 +locale @{text M_trivial}.  Note that the present theory does not even take
    1.61 +@{text Relative} as a parent.*}
    1.62  
    1.63  subsubsection{*The subset relation*}
    1.64  
    1.65 @@ -563,12 +565,25 @@
    1.66  apply (blast intro: nth_type) 
    1.67  done
    1.68  
    1.69 +text{*The subset consisting of the ordinals is definable.  Essential lemma for
    1.70 +@{text Ord_in_Lset}.  This result is the objective of the present subsection.*}
    1.71 +theorem Ords_in_DPow: "Transset(A) ==> {x \<in> A. Ord(x)} \<in> DPow(A)"
    1.72 +apply (simp add: DPow_def Collect_subset) 
    1.73 +apply (rule_tac x=Nil in bexI) 
    1.74 + apply (rule_tac x="ordinal_fm(0)" in bexI) 
    1.75 +apply (simp_all add: sats_ordinal_fm)
    1.76 +done 
    1.77 +
    1.78  
    1.79  subsection{* Constant Lset: Levels of the Constructible Universe *}
    1.80  
    1.81 -constdefs Lset :: "i=>i"
    1.82 +constdefs
    1.83 +  Lset :: "i=>i"
    1.84      "Lset(i) == transrec(i, %x f. \<Union>y\<in>x. DPow(f`y))"
    1.85  
    1.86 +  L :: "i=>o" --{*Kunen's definition VI 1.5, page 167*}
    1.87 +    "L(x) == \<exists>i. Ord(i) & x \<in> Lset(i)"
    1.88 +  
    1.89  text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
    1.90  lemma Lset: "Lset(i) = (UN j:i. DPow(Lset(j)))"
    1.91  by (subst Lset_def [THEN def_transrec], simp)
    1.92 @@ -601,7 +616,7 @@
    1.93  apply (blast intro: elem_subset_in_DPow dest: DPowD) 
    1.94  done
    1.95  
    1.96 -text{*Kunen's VI, 1.6 (a)*}
    1.97 +text{*Kunen's VI 1.6 (a)*}
    1.98  lemma Transset_Lset: "Transset(Lset(i))"
    1.99  apply (rule_tac a=i in eps_induct)
   1.100  apply (subst Lset)
   1.101 @@ -615,7 +630,7 @@
   1.102  
   1.103  subsubsection{* Monotonicity *}
   1.104  
   1.105 -text{*Kunen's VI, 1.6 (b)*}
   1.106 +text{*Kunen's VI 1.6 (b)*}
   1.107  lemma Lset_mono [rule_format]:
   1.108       "ALL j. i<=j --> Lset(i) <= Lset(j)"
   1.109  apply (rule_tac a=i in eps_induct)
   1.110 @@ -638,7 +653,7 @@
   1.111  lemma subset_Lset_ltD: "[|A \<subseteq> Lset(i); i < j|] ==> A \<subseteq> Lset(j)"
   1.112  by (blast dest: ltD [THEN Lset_mono_mem]) 
   1.113  
   1.114 -subsubsection{* 0, successor and limit equations fof Lset *}
   1.115 +subsubsection{* 0, successor and limit equations for Lset *}
   1.116  
   1.117  lemma Lset_0 [simp]: "Lset(0) = 0"
   1.118  by (subst Lset, blast)
   1.119 @@ -705,15 +720,7 @@
   1.120  done
   1.121  
   1.122  
   1.123 -subsection{*Constructible Ordinals: Kunen's VI, 1.9 (b)*}
   1.124 -
   1.125 -text{*The subset consisting of the ordinals is definable.*}
   1.126 -lemma Ords_in_DPow: "Transset(A) ==> {x \<in> A. Ord(x)} \<in> DPow(A)"
   1.127 -apply (simp add: DPow_def Collect_subset) 
   1.128 -apply (rule_tac x=Nil in bexI) 
   1.129 - apply (rule_tac x="ordinal_fm(0)" in bexI) 
   1.130 -apply (simp_all add: sats_ordinal_fm)
   1.131 -done 
   1.132 +subsection{*Constructible Ordinals: Kunen's VI 1.9 (b)*}
   1.133  
   1.134  lemma Ords_of_Lset_eq: "Ord(i) ==> {x\<in>Lset(i). Ord(x)} = i"
   1.135  apply (erule trans_induct3)
   1.136 @@ -744,6 +751,9 @@
   1.137         rule Ords_in_DPow [OF Transset_Lset]) 
   1.138  done
   1.139  
   1.140 +lemma Ord_in_L: "Ord(i) ==> L(i)"
   1.141 +by (simp add: L_def, blast intro: Ord_in_Lset)
   1.142 +
   1.143  subsubsection{* Unions *}
   1.144  
   1.145  lemma Union_in_Lset:
   1.146 @@ -765,6 +775,12 @@
   1.147  apply (blast intro: Limit_has_succ lt_LsetI Union_in_Lset)
   1.148  done
   1.149  
   1.150 +theorem Union_in_L: "L(X) ==> L(Union(X))"
   1.151 +apply (simp add: L_def, clarify) 
   1.152 +apply (drule Ord_imp_greater_Limit) 
   1.153 +apply (blast intro: lt_LsetI Union_in_LLimit Limit_is_Ord) 
   1.154 +done
   1.155 +
   1.156  subsubsection{* Finite sets and ordered pairs *}
   1.157  
   1.158  lemma singleton_in_Lset: "a: Lset(i) ==> {a} : Lset(succ(i))"
   1.159 @@ -780,13 +796,6 @@
   1.160  apply (blast intro: doubleton_in_Lset) 
   1.161  done
   1.162  
   1.163 -lemma singleton_in_LLimit:
   1.164 -    "[| a: Lset(i);  Limit(i) |] ==> {a} : Lset(i)"
   1.165 -apply (erule Limit_LsetE, assumption)
   1.166 -apply (erule singleton_in_Lset [THEN lt_LsetI])
   1.167 -apply (blast intro: Limit_has_succ) 
   1.168 -done
   1.169 -
   1.170  lemmas Lset_UnI1 = Un_upper1 [THEN Lset_mono [THEN subsetD], standard]
   1.171  lemmas Lset_UnI2 = Un_upper2 [THEN Lset_mono [THEN subsetD], standard]
   1.172  
   1.173 @@ -799,6 +808,12 @@
   1.174                      Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
   1.175  done
   1.176  
   1.177 +theorem doubleton_in_L: "[| L(a); L(b) |] ==> L({a, b})"
   1.178 +apply (simp add: L_def, clarify) 
   1.179 +apply (drule Ord2_imp_greater_Limit, assumption) 
   1.180 +apply (blast intro: lt_LsetI doubleton_in_LLimit Limit_is_Ord) 
   1.181 +done
   1.182 +
   1.183  lemma Pair_in_LLimit:
   1.184      "[| a: Lset(i);  b: Lset(i);  Limit(i) |] ==> <a,b> : Lset(i)"
   1.185  txt{*Infer that a, b occur at ordinals x,xa < i.*}
   1.186 @@ -809,49 +824,11 @@
   1.187                      Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
   1.188  done
   1.189  
   1.190 -lemma product_LLimit: "Limit(i) ==> Lset(i) * Lset(i) <= Lset(i)"
   1.191 -by (blast intro: Pair_in_LLimit)
   1.192 -
   1.193 -lemmas Sigma_subset_LLimit = subset_trans [OF Sigma_mono product_LLimit]
   1.194 -
   1.195 -lemma nat_subset_LLimit: "Limit(i) ==> nat \<subseteq> Lset(i)"
   1.196 -by (blast dest: Ord_subset_Lset nat_le_Limit le_imp_subset Limit_is_Ord)
   1.197 -
   1.198 -lemma nat_into_LLimit: "[| n: nat;  Limit(i) |] ==> n : Lset(i)"
   1.199 -by (blast intro: nat_subset_LLimit [THEN subsetD])
   1.200  
   1.201  
   1.202 -subsubsection{* Closure under disjoint union *}
   1.203 -
   1.204 -lemmas zero_in_LLimit = Limit_has_0 [THEN ltD, THEN zero_in_Lset, standard]
   1.205 -
   1.206 -lemma one_in_LLimit: "Limit(i) ==> 1 : Lset(i)"
   1.207 -by (blast intro: nat_into_LLimit)
   1.208 -
   1.209 -lemma Inl_in_LLimit:
   1.210 -    "[| a: Lset(i); Limit(i) |] ==> Inl(a) : Lset(i)"
   1.211 -apply (unfold Inl_def)
   1.212 -apply (blast intro: zero_in_LLimit Pair_in_LLimit)
   1.213 -done
   1.214 -
   1.215 -lemma Inr_in_LLimit:
   1.216 -    "[| b: Lset(i); Limit(i) |] ==> Inr(b) : Lset(i)"
   1.217 -apply (unfold Inr_def)
   1.218 -apply (blast intro: one_in_LLimit Pair_in_LLimit)
   1.219 -done
   1.220 -
   1.221 -lemma sum_LLimit: "Limit(i) ==> Lset(i) + Lset(i) <= Lset(i)"
   1.222 -by (blast intro!: Inl_in_LLimit Inr_in_LLimit)
   1.223 -
   1.224 -lemmas sum_subset_LLimit = subset_trans [OF sum_mono sum_LLimit]
   1.225 -
   1.226 -
   1.227 -text{*The constructible universe and its rank function*}
   1.228 +text{*The rank function for the constructible universe*}
   1.229  constdefs
   1.230 -  L :: "i=>o" --{*Kunen's definition VI, 1.5, page 167*}
   1.231 -    "L(x) == \<exists>i. Ord(i) & x \<in> Lset(i)"
   1.232 -  
   1.233 -  lrank :: "i=>i" --{*Kunen's definition VI, 1.7*}
   1.234 +  lrank :: "i=>i" --{*Kunen's definition VI 1.7*}
   1.235      "lrank(x) == \<mu>i. x \<in> Lset(succ(i))"
   1.236  
   1.237  lemma L_I: "[|x \<in> Lset(i); Ord(i)|] ==> L(x)"
   1.238 @@ -872,8 +849,9 @@
   1.239  apply (blast intro: ltI Limit_is_Ord lt_trans) 
   1.240  done
   1.241  
   1.242 -text{*Kunen's VI, 1.8, and the proof is much less trivial than the text
   1.243 -would suggest.  For a start it need the previous lemma, proved by induction.*}
   1.244 +text{*Kunen's VI 1.8.  The proof is much harder than the text would
   1.245 +suggest.  For a start, it needs the previous lemma, which is proved by
   1.246 +induction.*}
   1.247  lemma Lset_iff_lrank_lt: "Ord(i) ==> x \<in> Lset(i) <-> L(x) & lrank(x) < i"
   1.248  apply (simp add: L_def, auto) 
   1.249   apply (blast intro: Lset_lrank_lt) 
   1.250 @@ -886,7 +864,7 @@
   1.251  lemma Lset_succ_lrank_iff [simp]: "x \<in> Lset(succ(lrank(x))) <-> L(x)"
   1.252  by (simp add: Lset_iff_lrank_lt)
   1.253  
   1.254 -text{*Kunen's VI, 1.9 (a)*}
   1.255 +text{*Kunen's VI 1.9 (a)*}
   1.256  lemma lrank_of_Ord: "Ord(i) ==> lrank(i) = i"
   1.257  apply (unfold lrank_def) 
   1.258  apply (rule Least_equality) 
   1.259 @@ -897,13 +875,10 @@
   1.260  done
   1.261  
   1.262  
   1.263 -lemma Ord_in_L: "Ord(i) ==> L(i)"
   1.264 -by (blast intro: Ord_in_Lset L_I)
   1.265 -
   1.266  text{*This is lrank(lrank(a)) = lrank(a) *}
   1.267  declare Ord_lrank [THEN lrank_of_Ord, simp]
   1.268  
   1.269 -text{*Kunen's VI, 1.10 *}
   1.270 +text{*Kunen's VI 1.10 *}
   1.271  lemma Lset_in_Lset_succ: "Lset(i) \<in> Lset(succ(i))";
   1.272  apply (simp add: Lset_succ DPow_def) 
   1.273  apply (rule_tac x=Nil in bexI) 
   1.274 @@ -922,7 +897,7 @@
   1.275  apply (blast intro!: le_imp_subset Lset_mono) 
   1.276  done
   1.277  
   1.278 -text{*Kunen's VI, 1.11 *}
   1.279 +text{*Kunen's VI 1.11 *}
   1.280  lemma Lset_subset_Vset: "Ord(i) ==> Lset(i) <= Vset(i)";
   1.281  apply (erule trans_induct)
   1.282  apply (subst Lset) 
   1.283 @@ -932,7 +907,7 @@
   1.284  apply (rule Pow_mono, blast) 
   1.285  done
   1.286  
   1.287 -text{*Kunen's VI, 1.12 *}
   1.288 +text{*Kunen's VI 1.12 *}
   1.289  lemma Lset_subset_Vset': "i \<in> nat ==> Lset(i) = Vset(i)";
   1.290  apply (erule nat_induct)
   1.291   apply (simp add: Vfrom_0) 
   1.292 @@ -950,21 +925,7 @@
   1.293        ==> P"
   1.294  by (blast dest: subset_Lset) 
   1.295  
   1.296 -subsection{*For L to satisfy the ZF axioms*}
   1.297 -
   1.298 -theorem Union_in_L: "L(X) ==> L(Union(X))"
   1.299 -apply (simp add: L_def, clarify) 
   1.300 -apply (drule Ord_imp_greater_Limit) 
   1.301 -apply (blast intro: lt_LsetI Union_in_LLimit Limit_is_Ord) 
   1.302 -done
   1.303 -
   1.304 -theorem doubleton_in_L: "[| L(a); L(b) |] ==> L({a, b})"
   1.305 -apply (simp add: L_def, clarify) 
   1.306 -apply (drule Ord2_imp_greater_Limit, assumption) 
   1.307 -apply (blast intro: lt_LsetI doubleton_in_LLimit Limit_is_Ord) 
   1.308 -done
   1.309 -
   1.310 -subsubsection{*For L to satisfy Powerset *}
   1.311 +subsubsection{*For L to satisfy the Powerset axiom *}
   1.312  
   1.313  lemma LPow_env_typing:
   1.314      "[| y : Lset(i); Ord(i); y \<subseteq> X |] 
   1.315 @@ -996,7 +957,6 @@
   1.316  
   1.317  subsection{*Eliminating @{term arity} from the Definition of @{term Lset}*}
   1.318  
   1.319 -
   1.320  lemma nth_zero_eq_0: "n \<in> nat ==> nth(n,[0]) = 0"
   1.321  by (induct_tac n, auto)
   1.322  
   1.323 @@ -1046,7 +1006,7 @@
   1.324  lemma DPow_eq_DPow': "Transset(A) ==> DPow(A) = DPow'(A)"
   1.325  apply (drule Transset_0_disj) 
   1.326  apply (erule disjE) 
   1.327 - apply (simp add: DPow'_0 DPow_0) 
   1.328 + apply (simp add: DPow'_0 Finite_DPow_eq_Pow) 
   1.329  apply (rule equalityI)
   1.330   apply (rule DPow_subset_DPow') 
   1.331  apply (erule DPow'_subset_DPow) 
     2.1 --- a/src/ZF/Constructible/Internalize.thy	Thu Oct 17 10:52:59 2002 +0200
     2.2 +++ b/src/ZF/Constructible/Internalize.thy	Thu Oct 17 10:54:11 2002 +0200
     2.3 @@ -726,11 +726,6 @@
     2.4       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> cartprod_fm(x,y,z) \<in> formula"
     2.5  by (simp add: cartprod_fm_def)
     2.6  
     2.7 -lemma arity_cartprod_fm [simp]:
     2.8 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
     2.9 -      ==> arity(cartprod_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
    2.10 -by (simp add: cartprod_fm_def succ_Un_distrib [symmetric] Un_ac)
    2.11 -
    2.12  lemma sats_cartprod_fm [simp]:
    2.13     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    2.14      ==> sats(A, cartprod_fm(x,y,z), env) <->
    2.15 @@ -770,11 +765,6 @@
    2.16       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> sum_fm(x,y,z) \<in> formula"
    2.17  by (simp add: sum_fm_def)
    2.18  
    2.19 -lemma arity_sum_fm [simp]:
    2.20 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
    2.21 -      ==> arity(sum_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
    2.22 -by (simp add: sum_fm_def succ_Un_distrib [symmetric] Un_ac)
    2.23 -
    2.24  lemma sats_sum_fm [simp]:
    2.25     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    2.26      ==> sats(A, sum_fm(x,y,z), env) <->
    2.27 @@ -805,10 +795,6 @@
    2.28       "x \<in> nat ==> quasinat_fm(x) \<in> formula"
    2.29  by (simp add: quasinat_fm_def)
    2.30  
    2.31 -lemma arity_quasinat_fm [simp]:
    2.32 -     "x \<in> nat ==> arity(quasinat_fm(x)) = succ(x)"
    2.33 -by (simp add: quasinat_fm_def succ_Un_distrib [symmetric] Un_ac)
    2.34 -
    2.35  lemma sats_quasinat_fm [simp]:
    2.36     "[| x \<in> nat; env \<in> list(A)|]
    2.37      ==> sats(A, quasinat_fm(x), env) <-> is_quasinat(**A, nth(x,env))"
    2.38 @@ -1081,11 +1067,6 @@
    2.39       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> list_functor_fm(x,y,z) \<in> formula"
    2.40  by (simp add: list_functor_fm_def)
    2.41  
    2.42 -lemma arity_list_functor_fm [simp]:
    2.43 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
    2.44 -      ==> arity(list_functor_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
    2.45 -by (simp add: list_functor_fm_def succ_Un_distrib [symmetric] Un_ac)
    2.46 -
    2.47  lemma sats_list_functor_fm [simp]:
    2.48     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    2.49      ==> sats(A, list_functor_fm(x,y,z), env) <->
     3.1 --- a/src/ZF/Constructible/L_axioms.thy	Thu Oct 17 10:52:59 2002 +0200
     3.2 +++ b/src/ZF/Constructible/L_axioms.thy	Thu Oct 17 10:54:11 2002 +0200
     3.3 @@ -88,8 +88,6 @@
     3.4  lemma Lset_cont: "cont_Ord(Lset)"
     3.5  by (simp add: cont_Ord_def Limit_Lset_eq OUnion_def Limit_is_Ord)
     3.6  
     3.7 -lemmas Pair_in_Lset = Formula.Pair_in_LLimit
     3.8 -
     3.9  lemmas L_nat = Ord_in_L [OF Ord_nat]
    3.10  
    3.11  theorem M_trivial_L: "PROP M_trivial(L)"
    3.12 @@ -260,8 +258,9 @@
    3.13  
    3.14  
    3.15  lemma reflection_Lset: "reflection(Lset)"
    3.16 -apply (blast intro: reflection.intro Lset_mono_le Lset_cont Pair_in_Lset) +
    3.17 -done
    3.18 +by (blast intro: reflection.intro Lset_mono_le Lset_cont 
    3.19 +                 Formula.Pair_in_LLimit)+
    3.20 +
    3.21  
    3.22  theorem Ex_reflection:
    3.23       "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
    3.24 @@ -370,10 +369,6 @@
    3.25       "x \<in> nat ==> empty_fm(x) \<in> formula"
    3.26  by (simp add: empty_fm_def)
    3.27  
    3.28 -lemma arity_empty_fm [simp]:
    3.29 -     "x \<in> nat ==> arity(empty_fm(x)) = succ(x)"
    3.30 -by (simp add: empty_fm_def succ_Un_distrib [symmetric] Un_ac)
    3.31 -
    3.32  lemma sats_empty_fm [simp]:
    3.33     "[| x \<in> nat; env \<in> list(A)|]
    3.34      ==> sats(A, empty_fm(x), env) <-> empty(**A, nth(x,env))"
    3.35 @@ -416,11 +411,6 @@
    3.36       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> upair_fm(x,y,z) \<in> formula"
    3.37  by (simp add: upair_fm_def)
    3.38  
    3.39 -lemma arity_upair_fm [simp]:
    3.40 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
    3.41 -      ==> arity(upair_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
    3.42 -by (simp add: upair_fm_def succ_Un_distrib [symmetric] Un_ac)
    3.43 -
    3.44  lemma sats_upair_fm [simp]:
    3.45     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    3.46      ==> sats(A, upair_fm(x,y,z), env) <->
    3.47 @@ -462,11 +452,6 @@
    3.48       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> pair_fm(x,y,z) \<in> formula"
    3.49  by (simp add: pair_fm_def)
    3.50  
    3.51 -lemma arity_pair_fm [simp]:
    3.52 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
    3.53 -      ==> arity(pair_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
    3.54 -by (simp add: pair_fm_def succ_Un_distrib [symmetric] Un_ac)
    3.55 -
    3.56  lemma sats_pair_fm [simp]:
    3.57     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    3.58      ==> sats(A, pair_fm(x,y,z), env) <->
    3.59 @@ -498,11 +483,6 @@
    3.60       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> union_fm(x,y,z) \<in> formula"
    3.61  by (simp add: union_fm_def)
    3.62  
    3.63 -lemma arity_union_fm [simp]:
    3.64 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
    3.65 -      ==> arity(union_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
    3.66 -by (simp add: union_fm_def succ_Un_distrib [symmetric] Un_ac)
    3.67 -
    3.68  lemma sats_union_fm [simp]:
    3.69     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    3.70      ==> sats(A, union_fm(x,y,z), env) <->
    3.71 @@ -535,11 +515,6 @@
    3.72       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> cons_fm(x,y,z) \<in> formula"
    3.73  by (simp add: cons_fm_def)
    3.74  
    3.75 -lemma arity_cons_fm [simp]:
    3.76 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
    3.77 -      ==> arity(cons_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
    3.78 -by (simp add: cons_fm_def succ_Un_distrib [symmetric] Un_ac)
    3.79 -
    3.80  lemma sats_cons_fm [simp]:
    3.81     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    3.82      ==> sats(A, cons_fm(x,y,z), env) <->
    3.83 @@ -569,11 +544,6 @@
    3.84       "[| x \<in> nat; y \<in> nat |] ==> succ_fm(x,y) \<in> formula"
    3.85  by (simp add: succ_fm_def)
    3.86  
    3.87 -lemma arity_succ_fm [simp]:
    3.88 -     "[| x \<in> nat; y \<in> nat |]
    3.89 -      ==> arity(succ_fm(x,y)) = succ(x) \<union> succ(y)"
    3.90 -by (simp add: succ_fm_def)
    3.91 -
    3.92  lemma sats_succ_fm [simp]:
    3.93     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
    3.94      ==> sats(A, succ_fm(x,y), env) <->
    3.95 @@ -604,10 +574,6 @@
    3.96       "x \<in> nat ==> number1_fm(x) \<in> formula"
    3.97  by (simp add: number1_fm_def)
    3.98  
    3.99 -lemma arity_number1_fm [simp]:
   3.100 -     "x \<in> nat ==> arity(number1_fm(x)) = succ(x)"
   3.101 -by (simp add: number1_fm_def succ_Un_distrib [symmetric] Un_ac)
   3.102 -
   3.103  lemma sats_number1_fm [simp]:
   3.104     "[| x \<in> nat; env \<in> list(A)|]
   3.105      ==> sats(A, number1_fm(x), env) <-> number1(**A, nth(x,env))"
   3.106 @@ -639,11 +605,6 @@
   3.107       "[| x \<in> nat; y \<in> nat |] ==> big_union_fm(x,y) \<in> formula"
   3.108  by (simp add: big_union_fm_def)
   3.109  
   3.110 -lemma arity_big_union_fm [simp]:
   3.111 -     "[| x \<in> nat; y \<in> nat |]
   3.112 -      ==> arity(big_union_fm(x,y)) = succ(x) \<union> succ(y)"
   3.113 -by (simp add: big_union_fm_def succ_Un_distrib [symmetric] Un_ac)
   3.114 -
   3.115  lemma sats_big_union_fm [simp]:
   3.116     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   3.117      ==> sats(A, big_union_fm(x,y), env) <->
   3.118 @@ -666,8 +627,11 @@
   3.119  
   3.120  subsubsection{*Variants of Satisfaction Definitions for Ordinals, etc.*}
   3.121  
   3.122 -text{*Differs from the one in Formula by using "ordinal" rather than "Ord"*}
   3.123 -
   3.124 +text{*The @{text sats} theorems below are standard versions of the ones proved
   3.125 +in theory @{text Formula}.  They relate elements of type @{term formula} to
   3.126 +relativized concepts such as @{term subset} or @{term ordinal} rather than to
   3.127 +real concepts such as @{term Ord}.  Now that we have instantiated the locale
   3.128 +@{text M_trivial}, we no longer require the earlier versions.*}
   3.129  
   3.130  lemma sats_subset_fm':
   3.131     "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
   3.132 @@ -724,11 +688,6 @@
   3.133       "[| x \<in> nat; y \<in> nat |] ==> Memrel_fm(x,y) \<in> formula"
   3.134  by (simp add: Memrel_fm_def)
   3.135  
   3.136 -lemma arity_Memrel_fm [simp]:
   3.137 -     "[| x \<in> nat; y \<in> nat |]
   3.138 -      ==> arity(Memrel_fm(x,y)) = succ(x) \<union> succ(y)"
   3.139 -by (simp add: Memrel_fm_def succ_Un_distrib [symmetric] Un_ac)
   3.140 -
   3.141  lemma sats_Memrel_fm [simp]:
   3.142     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   3.143      ==> sats(A, Memrel_fm(x,y), env) <->
   3.144 @@ -763,11 +722,6 @@
   3.145        ==> pred_set_fm(A,x,r,B) \<in> formula"
   3.146  by (simp add: pred_set_fm_def)
   3.147  
   3.148 -lemma arity_pred_set_fm [simp]:
   3.149 -   "[| A \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat |]
   3.150 -    ==> arity(pred_set_fm(A,x,r,B)) = succ(A) \<union> succ(x) \<union> succ(r) \<union> succ(B)"
   3.151 -by (simp add: pred_set_fm_def succ_Un_distrib [symmetric] Un_ac)
   3.152 -
   3.153  lemma sats_pred_set_fm [simp]:
   3.154     "[| U \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat; env \<in> list(A)|]
   3.155      ==> sats(A, pred_set_fm(U,x,r,B), env) <->
   3.156 @@ -803,11 +757,6 @@
   3.157       "[| x \<in> nat; y \<in> nat |] ==> domain_fm(x,y) \<in> formula"
   3.158  by (simp add: domain_fm_def)
   3.159  
   3.160 -lemma arity_domain_fm [simp]:
   3.161 -     "[| x \<in> nat; y \<in> nat |]
   3.162 -      ==> arity(domain_fm(x,y)) = succ(x) \<union> succ(y)"
   3.163 -by (simp add: domain_fm_def succ_Un_distrib [symmetric] Un_ac)
   3.164 -
   3.165  lemma sats_domain_fm [simp]:
   3.166     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   3.167      ==> sats(A, domain_fm(x,y), env) <->
   3.168 @@ -842,11 +791,6 @@
   3.169       "[| x \<in> nat; y \<in> nat |] ==> range_fm(x,y) \<in> formula"
   3.170  by (simp add: range_fm_def)
   3.171  
   3.172 -lemma arity_range_fm [simp]:
   3.173 -     "[| x \<in> nat; y \<in> nat |]
   3.174 -      ==> arity(range_fm(x,y)) = succ(x) \<union> succ(y)"
   3.175 -by (simp add: range_fm_def succ_Un_distrib [symmetric] Un_ac)
   3.176 -
   3.177  lemma sats_range_fm [simp]:
   3.178     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   3.179      ==> sats(A, range_fm(x,y), env) <->
   3.180 @@ -882,11 +826,6 @@
   3.181       "[| x \<in> nat; y \<in> nat |] ==> field_fm(x,y) \<in> formula"
   3.182  by (simp add: field_fm_def)
   3.183  
   3.184 -lemma arity_field_fm [simp]:
   3.185 -     "[| x \<in> nat; y \<in> nat |]
   3.186 -      ==> arity(field_fm(x,y)) = succ(x) \<union> succ(y)"
   3.187 -by (simp add: field_fm_def succ_Un_distrib [symmetric] Un_ac)
   3.188 -
   3.189  lemma sats_field_fm [simp]:
   3.190     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   3.191      ==> sats(A, field_fm(x,y), env) <->
   3.192 @@ -923,11 +862,6 @@
   3.193       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> image_fm(x,y,z) \<in> formula"
   3.194  by (simp add: image_fm_def)
   3.195  
   3.196 -lemma arity_image_fm [simp]:
   3.197 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
   3.198 -      ==> arity(image_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   3.199 -by (simp add: image_fm_def succ_Un_distrib [symmetric] Un_ac)
   3.200 -
   3.201  lemma sats_image_fm [simp]:
   3.202     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   3.203      ==> sats(A, image_fm(x,y,z), env) <->
   3.204 @@ -963,11 +897,6 @@
   3.205       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> pre_image_fm(x,y,z) \<in> formula"
   3.206  by (simp add: pre_image_fm_def)
   3.207  
   3.208 -lemma arity_pre_image_fm [simp]:
   3.209 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
   3.210 -      ==> arity(pre_image_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   3.211 -by (simp add: pre_image_fm_def succ_Un_distrib [symmetric] Un_ac)
   3.212 -
   3.213  lemma sats_pre_image_fm [simp]:
   3.214     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   3.215      ==> sats(A, pre_image_fm(x,y,z), env) <->
   3.216 @@ -1003,11 +932,6 @@
   3.217       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> fun_apply_fm(x,y,z) \<in> formula"
   3.218  by (simp add: fun_apply_fm_def)
   3.219  
   3.220 -lemma arity_fun_apply_fm [simp]:
   3.221 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
   3.222 -      ==> arity(fun_apply_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   3.223 -by (simp add: fun_apply_fm_def succ_Un_distrib [symmetric] Un_ac)
   3.224 -
   3.225  lemma sats_fun_apply_fm [simp]:
   3.226     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   3.227      ==> sats(A, fun_apply_fm(x,y,z), env) <->
   3.228 @@ -1041,10 +965,6 @@
   3.229       "[| x \<in> nat |] ==> relation_fm(x) \<in> formula"
   3.230  by (simp add: relation_fm_def)
   3.231  
   3.232 -lemma arity_relation_fm [simp]:
   3.233 -     "x \<in> nat ==> arity(relation_fm(x)) = succ(x)"
   3.234 -by (simp add: relation_fm_def succ_Un_distrib [symmetric] Un_ac)
   3.235 -
   3.236  lemma sats_relation_fm [simp]:
   3.237     "[| x \<in> nat; env \<in> list(A)|]
   3.238      ==> sats(A, relation_fm(x), env) <-> is_relation(**A, nth(x,env))"
   3.239 @@ -1081,10 +1001,6 @@
   3.240       "[| x \<in> nat |] ==> function_fm(x) \<in> formula"
   3.241  by (simp add: function_fm_def)
   3.242  
   3.243 -lemma arity_function_fm [simp]:
   3.244 -     "x \<in> nat ==> arity(function_fm(x)) = succ(x)"
   3.245 -by (simp add: function_fm_def succ_Un_distrib [symmetric] Un_ac)
   3.246 -
   3.247  lemma sats_function_fm [simp]:
   3.248     "[| x \<in> nat; env \<in> list(A)|]
   3.249      ==> sats(A, function_fm(x), env) <-> is_function(**A, nth(x,env))"
   3.250 @@ -1122,11 +1038,6 @@
   3.251       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> typed_function_fm(x,y,z) \<in> formula"
   3.252  by (simp add: typed_function_fm_def)
   3.253  
   3.254 -lemma arity_typed_function_fm [simp]:
   3.255 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
   3.256 -      ==> arity(typed_function_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   3.257 -by (simp add: typed_function_fm_def succ_Un_distrib [symmetric] Un_ac)
   3.258 -
   3.259  lemma sats_typed_function_fm [simp]:
   3.260     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   3.261      ==> sats(A, typed_function_fm(x,y,z), env) <->
   3.262 @@ -1187,11 +1098,6 @@
   3.263       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> composition_fm(x,y,z) \<in> formula"
   3.264  by (simp add: composition_fm_def)
   3.265  
   3.266 -lemma arity_composition_fm [simp]:
   3.267 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
   3.268 -      ==> arity(composition_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   3.269 -by (simp add: composition_fm_def succ_Un_distrib [symmetric] Un_ac)
   3.270 -
   3.271  lemma sats_composition_fm [simp]:
   3.272     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   3.273      ==> sats(A, composition_fm(x,y,z), env) <->
   3.274 @@ -1232,11 +1138,6 @@
   3.275       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> injection_fm(x,y,z) \<in> formula"
   3.276  by (simp add: injection_fm_def)
   3.277  
   3.278 -lemma arity_injection_fm [simp]:
   3.279 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
   3.280 -      ==> arity(injection_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   3.281 -by (simp add: injection_fm_def succ_Un_distrib [symmetric] Un_ac)
   3.282 -
   3.283  lemma sats_injection_fm [simp]:
   3.284     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   3.285      ==> sats(A, injection_fm(x,y,z), env) <->
   3.286 @@ -1274,11 +1175,6 @@
   3.287       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> surjection_fm(x,y,z) \<in> formula"
   3.288  by (simp add: surjection_fm_def)
   3.289  
   3.290 -lemma arity_surjection_fm [simp]:
   3.291 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
   3.292 -      ==> arity(surjection_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   3.293 -by (simp add: surjection_fm_def succ_Un_distrib [symmetric] Un_ac)
   3.294 -
   3.295  lemma sats_surjection_fm [simp]:
   3.296     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   3.297      ==> sats(A, surjection_fm(x,y,z), env) <->
   3.298 @@ -1311,11 +1207,6 @@
   3.299       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> bijection_fm(x,y,z) \<in> formula"
   3.300  by (simp add: bijection_fm_def)
   3.301  
   3.302 -lemma arity_bijection_fm [simp]:
   3.303 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
   3.304 -      ==> arity(bijection_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   3.305 -by (simp add: bijection_fm_def succ_Un_distrib [symmetric] Un_ac)
   3.306 -
   3.307  lemma sats_bijection_fm [simp]:
   3.308     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   3.309      ==> sats(A, bijection_fm(x,y,z), env) <->
   3.310 @@ -1352,11 +1243,6 @@
   3.311       "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> restriction_fm(x,y,z) \<in> formula"
   3.312  by (simp add: restriction_fm_def)
   3.313  
   3.314 -lemma arity_restriction_fm [simp]:
   3.315 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
   3.316 -      ==> arity(restriction_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   3.317 -by (simp add: restriction_fm_def succ_Un_distrib [symmetric] Un_ac)
   3.318 -
   3.319  lemma sats_restriction_fm [simp]:
   3.320     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   3.321      ==> sats(A, restriction_fm(x,y,z), env) <->
   3.322 @@ -1404,12 +1290,6 @@
   3.323        ==> order_isomorphism_fm(A,r,B,s,f) \<in> formula"
   3.324  by (simp add: order_isomorphism_fm_def)
   3.325  
   3.326 -lemma arity_order_isomorphism_fm [simp]:
   3.327 -     "[| A \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat |]
   3.328 -      ==> arity(order_isomorphism_fm(A,r,B,s,f)) =
   3.329 -          succ(A) \<union> succ(r) \<union> succ(B) \<union> succ(s) \<union> succ(f)"
   3.330 -by (simp add: order_isomorphism_fm_def succ_Un_distrib [symmetric] Un_ac)
   3.331 -
   3.332  lemma sats_order_isomorphism_fm [simp]:
   3.333     "[| U \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat; env \<in> list(A)|]
   3.334      ==> sats(A, order_isomorphism_fm(U,r,B,s,f), env) <->
   3.335 @@ -1452,10 +1332,6 @@
   3.336       "x \<in> nat ==> limit_ordinal_fm(x) \<in> formula"
   3.337  by (simp add: limit_ordinal_fm_def)
   3.338  
   3.339 -lemma arity_limit_ordinal_fm [simp]:
   3.340 -     "x \<in> nat ==> arity(limit_ordinal_fm(x)) = succ(x)"
   3.341 -by (simp add: limit_ordinal_fm_def succ_Un_distrib [symmetric] Un_ac)
   3.342 -
   3.343  lemma sats_limit_ordinal_fm [simp]:
   3.344     "[| x \<in> nat; env \<in> list(A)|]
   3.345      ==> sats(A, limit_ordinal_fm(x), env) <-> limit_ordinal(**A, nth(x,env))"
   3.346 @@ -1523,10 +1399,6 @@
   3.347       "x \<in> nat ==> omega_fm(x) \<in> formula"
   3.348  by (simp add: omega_fm_def)
   3.349  
   3.350 -lemma arity_omega_fm [simp]:
   3.351 -     "x \<in> nat ==> arity(omega_fm(x)) = succ(x)"
   3.352 -by (simp add: omega_fm_def succ_Un_distrib [symmetric] Un_ac)
   3.353 -
   3.354  lemma sats_omega_fm [simp]:
   3.355     "[| x \<in> nat; env \<in> list(A)|]
   3.356      ==> sats(A, omega_fm(x), env) <-> omega(**A, nth(x,env))"
     4.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Thu Oct 17 10:52:59 2002 +0200
     4.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Thu Oct 17 10:54:11 2002 +0200
     4.3 @@ -53,11 +53,6 @@
     4.4   "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> rtran_closure_mem_fm(x,y,z) \<in> formula"
     4.5  by (simp add: rtran_closure_mem_fm_def)
     4.6  
     4.7 -lemma arity_rtran_closure_mem_fm [simp]:
     4.8 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
     4.9 -      ==> arity(rtran_closure_mem_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
    4.10 -by (simp add: rtran_closure_mem_fm_def succ_Un_distrib [symmetric] Un_ac)
    4.11 -
    4.12  lemma sats_rtran_closure_mem_fm [simp]:
    4.13     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    4.14      ==> sats(A, rtran_closure_mem_fm(x,y,z), env) <->
    4.15 @@ -103,11 +98,6 @@
    4.16       "[| x \<in> nat; y \<in> nat |] ==> rtran_closure_fm(x,y) \<in> formula"
    4.17  by (simp add: rtran_closure_fm_def)
    4.18  
    4.19 -lemma arity_rtran_closure_fm [simp]:
    4.20 -     "[| x \<in> nat; y \<in> nat |]
    4.21 -      ==> arity(rtran_closure_fm(x,y)) = succ(x) \<union> succ(y)"
    4.22 -by (simp add: rtran_closure_fm_def succ_Un_distrib [symmetric] Un_ac)
    4.23 -
    4.24  lemma sats_rtran_closure_fm [simp]:
    4.25     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
    4.26      ==> sats(A, rtran_closure_fm(x,y), env) <->
    4.27 @@ -140,11 +130,6 @@
    4.28       "[| x \<in> nat; y \<in> nat |] ==> tran_closure_fm(x,y) \<in> formula"
    4.29  by (simp add: tran_closure_fm_def)
    4.30  
    4.31 -lemma arity_tran_closure_fm [simp]:
    4.32 -     "[| x \<in> nat; y \<in> nat |]
    4.33 -      ==> arity(tran_closure_fm(x,y)) = succ(x) \<union> succ(y)"
    4.34 -by (simp add: tran_closure_fm_def succ_Un_distrib [symmetric] Un_ac)
    4.35 -
    4.36  lemma sats_tran_closure_fm [simp]:
    4.37     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
    4.38      ==> sats(A, tran_closure_fm(x,y), env) <->