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.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.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.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.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
```