src/ZF/Constructible/Formula.thy
changeset 13687 22dce9134953
parent 13651 ac80e101306a
child 13721 2cf506c09946
     1.1 --- a/src/ZF/Constructible/Formula.thy	Wed Oct 30 12:18:23 2002 +0100
     1.2 +++ b/src/ZF/Constructible/Formula.thy	Wed Oct 30 12:44:18 2002 +0100
     1.3 @@ -246,12 +246,12 @@
     1.4  subsection{*Renaming Some de Bruijn Variables*}
     1.5  
     1.6  constdefs incr_var :: "[i,i]=>i"
     1.7 -    "incr_var(x,lev) == if x<lev then x else succ(x)"
     1.8 +    "incr_var(x,nq) == if x<nq then x else succ(x)"
     1.9  
    1.10 -lemma incr_var_lt: "x<lev ==> incr_var(x,lev) = x"
    1.11 +lemma incr_var_lt: "x<nq ==> incr_var(x,nq) = x"
    1.12  by (simp add: incr_var_def)
    1.13  
    1.14 -lemma incr_var_le: "lev\<le>x ==> incr_var(x,lev) = succ(x)"
    1.15 +lemma incr_var_le: "nq\<le>x ==> incr_var(x,nq) = succ(x)"
    1.16  apply (simp add: incr_var_def) 
    1.17  apply (blast dest: lt_trans1) 
    1.18  done
    1.19 @@ -259,19 +259,19 @@
    1.20  consts   incr_bv :: "i=>i"
    1.21  primrec
    1.22    "incr_bv(Member(x,y)) = 
    1.23 -      (\<lambda>lev \<in> nat. Member (incr_var(x,lev), incr_var(y,lev)))"
    1.24 +      (\<lambda>nq \<in> nat. Member (incr_var(x,nq), incr_var(y,nq)))"
    1.25  
    1.26    "incr_bv(Equal(x,y)) = 
    1.27 -      (\<lambda>lev \<in> nat. Equal (incr_var(x,lev), incr_var(y,lev)))"
    1.28 +      (\<lambda>nq \<in> nat. Equal (incr_var(x,nq), incr_var(y,nq)))"
    1.29  
    1.30    "incr_bv(Nand(p,q)) =
    1.31 -      (\<lambda>lev \<in> nat. Nand (incr_bv(p)`lev, incr_bv(q)`lev))"
    1.32 +      (\<lambda>nq \<in> nat. Nand (incr_bv(p)`nq, incr_bv(q)`nq))"
    1.33  
    1.34    "incr_bv(Forall(p)) = 
    1.35 -      (\<lambda>lev \<in> nat. Forall (incr_bv(p) ` succ(lev)))"
    1.36 +      (\<lambda>nq \<in> nat. Forall (incr_bv(p) ` succ(nq)))"
    1.37  
    1.38  
    1.39 -lemma [TC]: "x \<in> nat ==> incr_var(x,lev) \<in> nat"
    1.40 +lemma [TC]: "x \<in> nat ==> incr_var(x,nq) \<in> nat"
    1.41  by (simp add: incr_var_def) 
    1.42  
    1.43  lemma incr_bv_type [TC]: "p \<in> formula ==> incr_bv(p) \<in> nat -> formula"
    1.44 @@ -294,8 +294,8 @@
    1.45  
    1.46  (*the following two lemmas prevent huge case splits in arity_incr_bv_lemma*)
    1.47  lemma incr_var_lemma:
    1.48 -     "[| x \<in> nat; y \<in> nat; lev \<le> x |]
    1.49 -      ==> succ(x) \<union> incr_var(y,lev) = succ(x \<union> y)"
    1.50 +     "[| x \<in> nat; y \<in> nat; nq \<le> x |]
    1.51 +      ==> succ(x) \<union> incr_var(y,nq) = succ(x \<union> y)"
    1.52  apply (simp add: incr_var_def Ord_Un_if, auto)
    1.53    apply (blast intro: leI)
    1.54   apply (simp add: not_lt_iff_le)  
    1.55 @@ -757,7 +757,7 @@
    1.56  subsubsection{* Unions *}
    1.57  
    1.58  lemma Union_in_Lset:
    1.59 -     "X \<in> Lset(j) ==> Union(X) \<in> Lset(succ(j))"
    1.60 +     "X \<in> Lset(i) ==> Union(X) \<in> Lset(succ(i))"
    1.61  apply (insert Transset_Lset)
    1.62  apply (rule LsetI [OF succI1])
    1.63  apply (simp add: Transset_def DPow_def) 
    1.64 @@ -769,17 +769,8 @@
    1.65  apply (simp add: succ_Un_distrib [symmetric], blast) 
    1.66  done
    1.67  
    1.68 -lemma Union_in_LLimit:
    1.69 -     "[| X: Lset(i);  Limit(i) |] ==> Union(X) : Lset(i)"
    1.70 -apply (rule Limit_LsetE, assumption+)
    1.71 -apply (blast intro: Limit_has_succ lt_LsetI Union_in_Lset)
    1.72 -done
    1.73 -
    1.74  theorem Union_in_L: "L(X) ==> L(Union(X))"
    1.75 -apply (simp add: L_def, clarify) 
    1.76 -apply (drule Ord_imp_greater_Limit) 
    1.77 -apply (blast intro: lt_LsetI Union_in_LLimit Limit_is_Ord) 
    1.78 -done
    1.79 +by (simp add: L_def, blast dest: Union_in_Lset) 
    1.80  
    1.81  subsubsection{* Finite sets and ordered pairs *}
    1.82