tidying and reorganization
authorpaulson
Mon Oct 14 11:32:00 2002 +0200 (2002-10-14)
changeset 136477f6f0ffc45c3
parent 13646 46ed3d042ba5
child 13648 610cedff5538
tidying and reorganization
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/Formula.thy
src/ZF/Constructible/Rank.thy
src/ZF/Constructible/Rec_Separation.thy
src/ZF/Constructible/WF_absolute.thy
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Mon Oct 14 10:44:32 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Mon Oct 14 11:32:00 2002 +0200
     1.3 @@ -425,7 +425,7 @@
     1.4  done
     1.5  
     1.6  
     1.7 -
     1.8 +text{*This result and the next are unused.*}
     1.9  lemma formula_N_mono [rule_format]:
    1.10    "[| m \<in> nat; n \<in> nat |] ==> m\<le>n --> formula_N(m) \<subseteq> formula_N(n)"
    1.11  apply (rule_tac m = m and n = n in diff_induct)
    1.12 @@ -577,8 +577,6 @@
    1.13  done
    1.14  
    1.15  
    1.16 -subsection{*Absoluteness for Some List Operators*}
    1.17 -
    1.18  subsection{*Absoluteness for @{text \<epsilon>}-Closure: the @{term eclose} Operator*}
    1.19  
    1.20  text{*Re-expresses eclose using "iterates"*}
    1.21 @@ -705,8 +703,9 @@
    1.22  
    1.23  
    1.24  subsection{*Absoluteness for the List Operator @{term length}*}
    1.25 +text{*But it is never used.*}
    1.26 +
    1.27  constdefs
    1.28 -
    1.29    is_length :: "[i=>o,i,i,i] => o"
    1.30      "is_length(M,A,l,n) == 
    1.31         \<exists>sn[M]. \<exists>list_n[M]. \<exists>list_sn[M]. 
    1.32 @@ -729,7 +728,7 @@
    1.33  by (simp add: nat_into_M) 
    1.34  
    1.35  
    1.36 -subsection {*Absoluteness for @{term nth}*}
    1.37 +subsection {*Absoluteness for the List Operator @{term nth}*}
    1.38  
    1.39  lemma nth_eq_hd_iterates_tl [rule_format]:
    1.40       "xs \<in> list(A) ==> \<forall>n \<in> nat. nth(n,xs) = hd' (tl'^n (xs))"
    1.41 @@ -828,8 +827,67 @@
    1.42  by (simp add: Forall_def)
    1.43  
    1.44  
    1.45 +
    1.46  subsection {*Absoluteness for @{term formula_rec}*}
    1.47  
    1.48 +constdefs
    1.49 +
    1.50 +  formula_rec_case :: "[[i,i]=>i, [i,i]=>i, [i,i,i,i]=>i, [i,i]=>i, i, i] => i"
    1.51 +    --{* the instance of @{term formula_case} in @{term formula_rec}*}
    1.52 +   "formula_rec_case(a,b,c,d,h) ==
    1.53 +        formula_case (a, b,
    1.54 +                \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u, 
    1.55 +                              h ` succ(depth(v)) ` v),
    1.56 +                \<lambda>u. d(u, h ` succ(depth(u)) ` u))"
    1.57 +
    1.58 +text{*Unfold @{term formula_rec} to @{term formula_rec_case}.
    1.59 +     Express @{term formula_rec} without using @{term rank} or @{term Vset},
    1.60 +neither of which is absolute.*}
    1.61 +lemma (in M_trivial) formula_rec_eq:
    1.62 +  "p \<in> formula ==>
    1.63 +   formula_rec(a,b,c,d,p) = 
    1.64 +   transrec (succ(depth(p)),
    1.65 +             \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h))) ` p"
    1.66 +apply (simp add: formula_rec_case_def)
    1.67 +apply (induct_tac p)
    1.68 +   txt{*Base case for @{term Member}*}
    1.69 +   apply (subst transrec, simp add: formula.intros) 
    1.70 +  txt{*Base case for @{term Equal}*}
    1.71 +  apply (subst transrec, simp add: formula.intros)
    1.72 + txt{*Inductive step for @{term Nand}*}
    1.73 + apply (subst transrec) 
    1.74 + apply (simp add: succ_Un_distrib formula.intros)
    1.75 +txt{*Inductive step for @{term Forall}*}
    1.76 +apply (subst transrec) 
    1.77 +apply (simp add: formula_imp_formula_N formula.intros) 
    1.78 +done
    1.79 +
    1.80 +
    1.81 +subsubsection{*Absoluteness for the Formula Operator @{term depth}*}
    1.82 +constdefs
    1.83 +
    1.84 +  is_depth :: "[i=>o,i,i] => o"
    1.85 +    "is_depth(M,p,n) == 
    1.86 +       \<exists>sn[M]. \<exists>formula_n[M]. \<exists>formula_sn[M]. 
    1.87 +        is_formula_N(M,n,formula_n) & p \<notin> formula_n &
    1.88 +        successor(M,n,sn) & is_formula_N(M,sn,formula_sn) & p \<in> formula_sn"
    1.89 +
    1.90 +
    1.91 +lemma (in M_datatypes) depth_abs [simp]:
    1.92 +     "[|p \<in> formula; n \<in> nat|] ==> is_depth(M,p,n) <-> n = depth(p)"
    1.93 +apply (subgoal_tac "M(p) & M(n)")
    1.94 + prefer 2 apply (blast dest: transM)  
    1.95 +apply (simp add: is_depth_def)
    1.96 +apply (blast intro: formula_imp_formula_N nat_into_Ord formula_N_imp_eq_depth
    1.97 +             dest: formula_N_imp_depth_lt)
    1.98 +done
    1.99 +
   1.100 +text{*Proof is trivial since @{term depth} returns natural numbers.*}
   1.101 +lemma (in M_trivial) depth_closed [intro,simp]:
   1.102 +     "p \<in> formula ==> M(depth(p))"
   1.103 +by (simp add: nat_into_M) 
   1.104 +
   1.105 +
   1.106  subsubsection{*@{term is_formula_case}: relativization of @{term formula_case}*}
   1.107  
   1.108  constdefs
   1.109 @@ -866,73 +924,17 @@
   1.110  by (erule formula.cases, simp_all) 
   1.111  
   1.112  
   1.113 -subsection{*Absoluteness for the Formula Operator @{term depth}*}
   1.114 -constdefs
   1.115 -
   1.116 -  is_depth :: "[i=>o,i,i] => o"
   1.117 -    "is_depth(M,p,n) == 
   1.118 -       \<exists>sn[M]. \<exists>formula_n[M]. \<exists>formula_sn[M]. 
   1.119 -        is_formula_N(M,n,formula_n) & p \<notin> formula_n &
   1.120 -        successor(M,n,sn) & is_formula_N(M,sn,formula_sn) & p \<in> formula_sn"
   1.121 -
   1.122 -
   1.123 -lemma (in M_datatypes) depth_abs [simp]:
   1.124 -     "[|p \<in> formula; n \<in> nat|] ==> is_depth(M,p,n) <-> n = depth(p)"
   1.125 -apply (subgoal_tac "M(p) & M(n)")
   1.126 - prefer 2 apply (blast dest: transM)  
   1.127 -apply (simp add: is_depth_def)
   1.128 -apply (blast intro: formula_imp_formula_N nat_into_Ord formula_N_imp_eq_depth
   1.129 -             dest: formula_N_imp_depth_lt)
   1.130 -done
   1.131 -
   1.132 -text{*Proof is trivial since @{term depth} returns natural numbers.*}
   1.133 -lemma (in M_trivial) depth_closed [intro,simp]:
   1.134 -     "p \<in> formula ==> M(depth(p))"
   1.135 -by (simp add: nat_into_M) 
   1.136 -
   1.137 -
   1.138 -subsection {*Absoluteness for @{term formula_rec}*}
   1.139 +subsubsection {*Absoluteness for @{term formula_rec}: Final Results*}
   1.140  
   1.141  constdefs
   1.142 -
   1.143 -  formula_rec_case :: "[[i,i]=>i, [i,i]=>i, [i,i,i,i]=>i, [i,i]=>i, i, i] => i"
   1.144 -    --{* the instance of @{term formula_case} in @{term formula_rec}*}
   1.145 -   "formula_rec_case(a,b,c,d,h) ==
   1.146 -        formula_case (a, b,
   1.147 -                \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u, 
   1.148 -                              h ` succ(depth(v)) ` v),
   1.149 -                \<lambda>u. d(u, h ` succ(depth(u)) ` u))"
   1.150 -
   1.151    is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o"
   1.152      --{* predicate to relativize the functional @{term formula_rec}*}
   1.153     "is_formula_rec(M,MH,p,z)  ==
   1.154        \<exists>dp[M]. \<exists>i[M]. \<exists>f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) & 
   1.155               successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)"
   1.156  
   1.157 -text{*Unfold @{term formula_rec} to @{term formula_rec_case}.
   1.158 -     Express @{term formula_rec} without using @{term rank} or @{term Vset},
   1.159 -neither of which is absolute.*}
   1.160 -lemma (in M_trivial) formula_rec_eq:
   1.161 -  "p \<in> formula ==>
   1.162 -   formula_rec(a,b,c,d,p) = 
   1.163 -   transrec (succ(depth(p)),
   1.164 -             \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h))) ` p"
   1.165 -apply (simp add: formula_rec_case_def)
   1.166 -apply (induct_tac p)
   1.167 -   txt{*Base case for @{term Member}*}
   1.168 -   apply (subst transrec, simp add: formula.intros) 
   1.169 -  txt{*Base case for @{term Equal}*}
   1.170 -  apply (subst transrec, simp add: formula.intros)
   1.171 - txt{*Inductive step for @{term Nand}*}
   1.172 - apply (subst transrec) 
   1.173 - apply (simp add: succ_Un_distrib formula.intros)
   1.174 -txt{*Inductive step for @{term Forall}*}
   1.175 -apply (subst transrec) 
   1.176 -apply (simp add: formula_imp_formula_N formula.intros) 
   1.177 -done
   1.178  
   1.179 -
   1.180 -text{*Sufficient conditions to relative the instance of @{term formula_case}
   1.181 +text{*Sufficient conditions to relativize the instance of @{term formula_case}
   1.182        in @{term formula_rec}*}
   1.183  lemma (in M_datatypes) Relation1_formula_rec_case:
   1.184       "[|Relation2(M, nat, nat, is_a, a);
     2.1 --- a/src/ZF/Constructible/Formula.thy	Mon Oct 14 10:44:32 2002 +0200
     2.2 +++ b/src/ZF/Constructible/Formula.thy	Mon Oct 14 11:32:00 2002 +0200
     2.3 @@ -188,6 +188,63 @@
     2.4          disj_iff_sats imp_iff_sats iff_iff_sats imp_iff_sats ball_iff_sats
     2.5          bex_iff_sats
     2.6  
     2.7 +
     2.8 +subsection{*Arity of a Formula: Maximum Free de Bruijn Index*}
     2.9 +
    2.10 +consts   arity :: "i=>i"
    2.11 +primrec
    2.12 +  "arity(Member(x,y)) = succ(x) \<union> succ(y)"
    2.13 +
    2.14 +  "arity(Equal(x,y)) = succ(x) \<union> succ(y)"
    2.15 +
    2.16 +  "arity(Nand(p,q)) = arity(p) \<union> arity(q)"
    2.17 +
    2.18 +  "arity(Forall(p)) = Arith.pred(arity(p))"
    2.19 +
    2.20 +
    2.21 +lemma arity_type [TC]: "p \<in> formula ==> arity(p) \<in> nat"
    2.22 +by (induct_tac p, simp_all) 
    2.23 +
    2.24 +lemma arity_Neg [simp]: "arity(Neg(p)) = arity(p)"
    2.25 +by (simp add: Neg_def) 
    2.26 +
    2.27 +lemma arity_And [simp]: "arity(And(p,q)) = arity(p) \<union> arity(q)"
    2.28 +by (simp add: And_def) 
    2.29 +
    2.30 +lemma arity_Or [simp]: "arity(Or(p,q)) = arity(p) \<union> arity(q)"
    2.31 +by (simp add: Or_def) 
    2.32 +
    2.33 +lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \<union> arity(q)"
    2.34 +by (simp add: Implies_def) 
    2.35 +
    2.36 +lemma arity_Iff [simp]: "arity(Iff(p,q)) = arity(p) \<union> arity(q)"
    2.37 +by (simp add: Iff_def, blast)
    2.38 +
    2.39 +lemma arity_Exists [simp]: "arity(Exists(p)) = Arith.pred(arity(p))"
    2.40 +by (simp add: Exists_def) 
    2.41 +
    2.42 +
    2.43 +lemma arity_sats_iff [rule_format]:
    2.44 +  "[| p \<in> formula; extra \<in> list(A) |]
    2.45 +   ==> \<forall>env \<in> list(A). 
    2.46 +           arity(p) \<le> length(env) --> 
    2.47 +           sats(A, p, env @ extra) <-> sats(A, p, env)"
    2.48 +apply (induct_tac p)
    2.49 +apply (simp_all add: Arith.pred_def nth_append Un_least_lt_iff nat_imp_quasinat
    2.50 +                split: split_nat_case, auto) 
    2.51 +done
    2.52 +
    2.53 +lemma arity_sats1_iff:
    2.54 +  "[| arity(p) \<le> succ(length(env)); p \<in> formula; x \<in> A; env \<in> list(A); 
    2.55 +      extra \<in> list(A) |]
    2.56 +   ==> sats(A, p, Cons(x, env @ extra)) <-> sats(A, p, Cons(x, env))"
    2.57 +apply (insert arity_sats_iff [of p extra A "Cons(x,env)"])
    2.58 +apply simp 
    2.59 +done
    2.60 +
    2.61 +
    2.62 +subsection{*Renaming Some de Bruijn Variables*}
    2.63 +
    2.64  constdefs incr_var :: "[i,i]=>i"
    2.65      "incr_var(x,lev) == if x<lev then x else succ(x)"
    2.66  
    2.67 @@ -214,22 +271,15 @@
    2.68        (\<lambda>lev \<in> nat. Forall (incr_bv(p) ` succ(lev)))"
    2.69  
    2.70  
    2.71 -constdefs incr_boundvars :: "i => i"
    2.72 -    "incr_boundvars(p) == incr_bv(p)`0"
    2.73 -
    2.74 -
    2.75  lemma [TC]: "x \<in> nat ==> incr_var(x,lev) \<in> nat"
    2.76  by (simp add: incr_var_def) 
    2.77  
    2.78  lemma incr_bv_type [TC]: "p \<in> formula ==> incr_bv(p) \<in> nat -> formula"
    2.79  by (induct_tac p, simp_all) 
    2.80  
    2.81 -lemma incr_boundvars_type [TC]: "p \<in> formula ==> incr_boundvars(p) \<in> formula"
    2.82 -by (simp add: incr_boundvars_def) 
    2.83 -
    2.84 -(*Obviously DPow is closed under complements and finite intersections and
    2.85 -unions.  Needs an inductive lemma to allow two lists of parameters to 
    2.86 -be combined.*)
    2.87 +text{*Obviously, @{term DPow} is closed under complements and finite
    2.88 +intersections and unions.  Needs an inductive lemma to allow two lists of
    2.89 +parameters to be combined.*}
    2.90  
    2.91  lemma sats_incr_bv_iff [rule_format]:
    2.92    "[| p \<in> formula; env \<in> list(A); x \<in> A |]
    2.93 @@ -241,76 +291,6 @@
    2.94  apply (auto simp add: diff_succ not_lt_iff_le)
    2.95  done
    2.96  
    2.97 -(*UNUSED*)
    2.98 -lemma sats_incr_boundvars_iff:
    2.99 -  "[| p \<in> formula; env \<in> list(A); x \<in> A |]
   2.100 -   ==> sats(A, incr_boundvars(p), Cons(x,env)) <-> sats(A, p, env)"
   2.101 -apply (insert sats_incr_bv_iff [of p env A x Nil])
   2.102 -apply (simp add: incr_boundvars_def) 
   2.103 -done
   2.104 -
   2.105 -(*UNUSED
   2.106 -lemma formula_add_params [rule_format]:
   2.107 -  "[| p \<in> formula; n \<in> nat |]
   2.108 -   ==> \<forall>bvs \<in> list(A). \<forall>env \<in> list(A). 
   2.109 -         length(bvs) = n --> 
   2.110 -         sats(A, iterates(incr_boundvars,n,p), bvs@env) <-> sats(A, p, env)"
   2.111 -apply (induct_tac n, simp, clarify) 
   2.112 -apply (erule list.cases)
   2.113 -apply (auto simp add: sats_incr_boundvars_iff)  
   2.114 -done
   2.115 -*)
   2.116 -
   2.117 -consts   arity :: "i=>i"
   2.118 -primrec
   2.119 -  "arity(Member(x,y)) = succ(x) \<union> succ(y)"
   2.120 -
   2.121 -  "arity(Equal(x,y)) = succ(x) \<union> succ(y)"
   2.122 -
   2.123 -  "arity(Nand(p,q)) = arity(p) \<union> arity(q)"
   2.124 -
   2.125 -  "arity(Forall(p)) = nat_case(0, %x. x, arity(p))"
   2.126 -
   2.127 -
   2.128 -lemma arity_type [TC]: "p \<in> formula ==> arity(p) \<in> nat"
   2.129 -by (induct_tac p, simp_all) 
   2.130 -
   2.131 -lemma arity_Neg [simp]: "arity(Neg(p)) = arity(p)"
   2.132 -by (simp add: Neg_def) 
   2.133 -
   2.134 -lemma arity_And [simp]: "arity(And(p,q)) = arity(p) \<union> arity(q)"
   2.135 -by (simp add: And_def) 
   2.136 -
   2.137 -lemma arity_Or [simp]: "arity(Or(p,q)) = arity(p) \<union> arity(q)"
   2.138 -by (simp add: Or_def) 
   2.139 -
   2.140 -lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \<union> arity(q)"
   2.141 -by (simp add: Implies_def) 
   2.142 -
   2.143 -lemma arity_Iff [simp]: "arity(Iff(p,q)) = arity(p) \<union> arity(q)"
   2.144 -by (simp add: Iff_def, blast)
   2.145 -
   2.146 -lemma arity_Exists [simp]: "arity(Exists(p)) = nat_case(0, %x. x, arity(p))"
   2.147 -by (simp add: Exists_def) 
   2.148 -
   2.149 -
   2.150 -lemma arity_sats_iff [rule_format]:
   2.151 -  "[| p \<in> formula; extra \<in> list(A) |]
   2.152 -   ==> \<forall>env \<in> list(A). 
   2.153 -           arity(p) \<le> length(env) --> 
   2.154 -           sats(A, p, env @ extra) <-> sats(A, p, env)"
   2.155 -apply (induct_tac p)
   2.156 -apply (simp_all add: nth_append Un_least_lt_iff arity_type nat_imp_quasinat
   2.157 -                split: split_nat_case, auto) 
   2.158 -done
   2.159 -
   2.160 -lemma arity_sats1_iff:
   2.161 -  "[| arity(p) \<le> succ(length(env)); p \<in> formula; x \<in> A; env \<in> list(A); 
   2.162 -    extra \<in> list(A) |]
   2.163 -   ==> sats(A, p, Cons(x, env @ extra)) <-> sats(A, p, Cons(x, env))"
   2.164 -apply (insert arity_sats_iff [of p extra A "Cons(x,env)"])
   2.165 -apply simp 
   2.166 -done
   2.167  
   2.168  (*the following two lemmas prevent huge case splits in arity_incr_bv_lemma*)
   2.169  lemma incr_var_lemma:
   2.170 @@ -336,7 +316,7 @@
   2.171  apply (induct_tac p) 
   2.172  apply (simp_all add: imp_disj not_lt_iff_le Un_least_lt_iff lt_Un_iff le_Un_iff
   2.173                       succ_Un_distrib [symmetric] incr_var_lt incr_var_le
   2.174 -                     Un_commute incr_var_lemma arity_type nat_imp_quasinat
   2.175 +                     Un_commute incr_var_lemma Arith.pred_def nat_imp_quasinat
   2.176              split: split_nat_case) 
   2.177   txt{*the Forall case reduces to linear arithmetic*}
   2.178   prefer 2
   2.179 @@ -350,24 +330,8 @@
   2.180  apply (simp add: Un_commute)
   2.181  done
   2.182  
   2.183 -lemma arity_incr_boundvars_eq:
   2.184 -  "p \<in> formula
   2.185 -   ==> arity(incr_boundvars(p)) =
   2.186 -        (if 0 < arity(p) then succ(arity(p)) else arity(p))"
   2.187 -apply (insert arity_incr_bv_lemma [of p 0])
   2.188 -apply (simp add: incr_boundvars_def) 
   2.189 -done
   2.190  
   2.191 -lemma arity_iterates_incr_boundvars_eq:
   2.192 -  "[| p \<in> formula; n \<in> nat |]
   2.193 -   ==> arity(incr_boundvars^n(p)) =
   2.194 -         (if 0 < arity(p) then n #+ arity(p) else arity(p))"
   2.195 -apply (induct_tac n) 
   2.196 -apply (simp_all add: arity_incr_boundvars_eq not_lt_iff_le) 
   2.197 -done
   2.198 -
   2.199 -
   2.200 -subsection{*Renaming all but the first bound variable*}
   2.201 +subsection{*Renaming all but the First de Bruijn Variable*}
   2.202  
   2.203  constdefs incr_bv1 :: "i => i"
   2.204      "incr_bv1(p) == incr_bv(p)`1"
   2.205 @@ -377,7 +341,7 @@
   2.206  by (simp add: incr_bv1_def) 
   2.207  
   2.208  (*For renaming all but the bound variable at level 0*)
   2.209 -lemma sats_incr_bv1_iff [rule_format]:
   2.210 +lemma sats_incr_bv1_iff:
   2.211    "[| p \<in> formula; env \<in> list(A); x \<in> A; y \<in> A |]
   2.212     ==> sats(A, incr_bv1(p), Cons(x, Cons(y, env))) <-> 
   2.213         sats(A, p, Cons(x,env))"
   2.214 @@ -416,7 +380,10 @@
   2.215  done
   2.216  
   2.217  
   2.218 -(*Definable powerset operation: Kunen's definition 1.1, page 165.*)
   2.219 +
   2.220 +subsection{*Definable Powerset*}
   2.221 +
   2.222 +text{*The definable powerset operation: Kunen's definition VI 1.1, page 165.*}
   2.223  constdefs DPow :: "i => i"
   2.224    "DPow(A) == {X \<in> Pow(A). 
   2.225                 \<exists>env \<in> list(A). \<exists>p \<in> formula. 
   2.226 @@ -445,7 +412,7 @@
   2.227  
   2.228  lemmas DPow_imp_subset = DPowD [THEN conjunct1]
   2.229  
   2.230 -(*Lemma 1.2*)
   2.231 +(*Kunen's Lemma VI 1.2*)
   2.232  lemma "[| p \<in> formula; env \<in> list(A); arity(p) \<le> succ(length(env)) |] 
   2.233         ==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"
   2.234  by (blast intro: DPowI)
     3.1 --- a/src/ZF/Constructible/Rank.thy	Mon Oct 14 10:44:32 2002 +0200
     3.2 +++ b/src/ZF/Constructible/Rank.thy	Mon Oct 14 11:32:00 2002 +0200
     3.3 @@ -666,6 +666,12 @@
     3.4  
     3.5  
     3.6  
     3.7 +subsection {*Absoluteness of Well-Founded Relations*}
     3.8 +
     3.9 +text{*Relativized to @{term M}: Every well-founded relation is a subset of some
    3.10 +inverse image of an ordinal.  Key step is the construction (in @{term M}) of a
    3.11 +rank function.*}
    3.12 +
    3.13  locale M_wfrank = M_trancl +
    3.14    assumes wfrank_separation:
    3.15       "M(r) ==>
     4.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Mon Oct 14 10:44:32 2002 +0200
     4.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Mon Oct 14 11:32:00 2002 +0200
     4.3 @@ -204,22 +204,9 @@
     4.4  
     4.5  lemmas iterates_abs = M_trancl.iterates_abs [OF M_trancl_L]
     4.6    and rtran_closure_rtrancl = M_trancl.rtran_closure_rtrancl [OF M_trancl_L]
     4.7 -  and rtrancl_closed = M_trancl.rtrancl_closed [OF M_trancl_L]
     4.8 -  and rtrancl_abs = M_trancl.rtrancl_abs [OF M_trancl_L]
     4.9 -  and trancl_closed = M_trancl.trancl_closed [OF M_trancl_L]
    4.10 -  and trancl_abs = M_trancl.trancl_abs [OF M_trancl_L]
    4.11 -  and wellfounded_on_trancl = M_trancl.wellfounded_on_trancl [OF M_trancl_L]
    4.12 -  and wellfounded_trancl = M_trancl.wellfounded_trancl [OF M_trancl_L]
    4.13 -  and wfrec_relativize = M_trancl.wfrec_relativize [OF M_trancl_L]
    4.14 -  and trans_wfrec_relativize = M_trancl.trans_wfrec_relativize [OF M_trancl_L]
    4.15    and trans_wfrec_abs = M_trancl.trans_wfrec_abs [OF M_trancl_L]
    4.16 -  and trans_eq_pair_wfrec_iff = M_trancl.trans_eq_pair_wfrec_iff [OF M_trancl_L]
    4.17    and eq_pair_wfrec_iff = M_trancl.eq_pair_wfrec_iff [OF M_trancl_L]
    4.18  
    4.19 -declare rtrancl_closed [intro,simp]
    4.20 -declare rtrancl_abs [simp]
    4.21 -declare trancl_closed [intro,simp]
    4.22 -declare trancl_abs [simp]
    4.23  
    4.24  
    4.25  subsection{*@{term L} is Closed Under the Operator @{term list}*}
     5.1 --- a/src/ZF/Constructible/WF_absolute.thy	Mon Oct 14 10:44:32 2002 +0200
     5.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Mon Oct 14 11:32:00 2002 +0200
     5.3 @@ -3,7 +3,7 @@
     5.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.5  *)
     5.6  
     5.7 -header {*Absoluteness for Well-Founded Relations and Well-Founded Recursion*}
     5.8 +header {*Absoluteness of Well-Founded Recursion*}
     5.9  
    5.10  theory WF_absolute = WFrec:
    5.11  
    5.12 @@ -175,13 +175,8 @@
    5.13    apply (simp_all add: trancl_type [THEN field_rel_subset])
    5.14  done
    5.15  
    5.16 -text{*Relativized to M: Every well-founded relation is a subset of some
    5.17 -inverse image of an ordinal.  Key step is the construction (in M) of a
    5.18 -rank function.*}
    5.19  
    5.20 -
    5.21 -
    5.22 -text{*absoluteness for wfrec-defined functions.*}
    5.23 +text{*Absoluteness for wfrec-defined functions.*}
    5.24  
    5.25  (*first use is_recfun, then M_is_recfun*)
    5.26