src/ZF/Constructible/Datatype_absolute.thy
changeset 13409 d4ea094c650e
parent 13398 1cadd412da48
child 13418 7c0ba9dba978
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Mon Jul 22 13:55:44 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Tue Jul 23 15:07:12 2002 +0200
     1.3 @@ -321,9 +321,9 @@
     1.4    "l \<in> list(A) ==>
     1.5     list_rec(a,g,l) = 
     1.6     transrec (succ(length(l)),
     1.7 -      \<lambda>x h. Lambda (list_N(A,x),
     1.8 -             list_case' (a, 
     1.9 -                \<lambda>a l. g(a, l, h ` succ(length(l)) ` l)))) ` l"
    1.10 +      \<lambda>x h. Lambda (list(A),
    1.11 +                    list_case' (a, 
    1.12 +                           \<lambda>a l. g(a, l, h ` succ(length(l)) ` l)))) ` l"
    1.13  apply (induct_tac l) 
    1.14  apply (subst transrec, simp) 
    1.15  apply (subst transrec) 
    1.16 @@ -629,10 +629,6 @@
    1.17  apply (simp add: tl'_Cons tl'_closed) 
    1.18  done
    1.19  
    1.20 -locale (open) M_nth = M_datatypes +
    1.21 - assumes nth_replacement1: 
    1.22 -   "M(xs) ==> iterates_replacement(M, %l t. is_tl(M,l,t), xs)"
    1.23 -
    1.24  text{*Immediate by type-checking*}
    1.25  lemma (in M_datatypes) nth_closed [intro,simp]:
    1.26       "[|xs \<in> list(A); n \<in> nat; M(A)|] ==> M(nth(n,xs))" 
    1.27 @@ -649,20 +645,18 @@
    1.28         is_wfrec(M, iterates_MH(M, is_tl(M), l), msn, n, X) &
    1.29         is_hd(M,X,Z)"
    1.30   
    1.31 -lemma (in M_nth) nth_abs [simp]:
    1.32 -     "[|M(A); n \<in> nat; l \<in> list(A); M(Z)|] 
    1.33 +lemma (in M_datatypes) nth_abs [simp]:
    1.34 +     "[|iterates_replacement(M, %l t. is_tl(M,l,t), l);
    1.35 +        M(A); n \<in> nat; l \<in> list(A); M(Z)|] 
    1.36        ==> is_nth(M,n,l,Z) <-> Z = nth(n,l)"
    1.37  apply (subgoal_tac "M(l)") 
    1.38   prefer 2 apply (blast intro: transM)
    1.39 -apply (insert nth_replacement1)
    1.40  apply (simp add: is_nth_def nth_eq_hd_iterates_tl nat_into_M
    1.41                   tl'_closed iterates_tl'_closed 
    1.42                   iterates_abs [OF _ relativize1_tl])
    1.43  done
    1.44  
    1.45  
    1.46 -
    1.47 -
    1.48  subsection{*Relativization and Absoluteness for the @{term formula} Constructors*}
    1.49  
    1.50  constdefs
    1.51 @@ -912,35 +906,29 @@
    1.52                       le_imp_subset formula_N_mono)
    1.53  done
    1.54  
    1.55 -lemma Nand_in_formula_N:
    1.56 -    "[|p \<in> formula; q \<in> formula|]
    1.57 -     ==> Nand(p,q) \<in> formula_N(succ(succ(depth(p))) \<union> succ(succ(depth(q))))"
    1.58 -by (simp add: succ_Un_distrib [symmetric] formula_imp_formula_N le_Un_iff) 
    1.59 -
    1.60 -
    1.61  text{*Express @{term formula_rec} without using @{term rank} or @{term Vset},
    1.62  neither of which is absolute.*}
    1.63  lemma (in M_triv_axioms) formula_rec_eq:
    1.64    "p \<in> formula ==>
    1.65     formula_rec(a,b,c,d,p) = 
    1.66     transrec (succ(depth(p)),
    1.67 -      \<lambda>x h. Lambda (formula_N(x),
    1.68 +      \<lambda>x h. Lambda (formula,
    1.69               formula_case' (a, b,
    1.70                  \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u, 
    1.71                                h ` succ(depth(v)) ` v),
    1.72                  \<lambda>u. d(u, h ` succ(depth(u)) ` u)))) 
    1.73     ` p"
    1.74  apply (induct_tac p)
    1.75 -txt{*Base case for @{term Member}*}
    1.76 -apply (subst transrec, simp) 
    1.77 -txt{*Base case for @{term Equal}*}
    1.78 -apply (subst transrec, simp)
    1.79 -txt{*Inductive step for @{term Nand}*}
    1.80 -apply (subst transrec)
    1.81 -apply (simp add: succ_Un_distrib Nand_in_formula_N)
    1.82 +   txt{*Base case for @{term Member}*}
    1.83 +   apply (subst transrec, simp add: formula.intros) 
    1.84 +  txt{*Base case for @{term Equal}*}
    1.85 +  apply (subst transrec, simp add: formula.intros)
    1.86 + txt{*Inductive step for @{term Nand}*}
    1.87 + apply (subst transrec) 
    1.88 + apply (simp add: succ_Un_distrib formula.intros)
    1.89  txt{*Inductive step for @{term Forall}*}
    1.90  apply (subst transrec) 
    1.91 -apply (simp add: formula_imp_formula_N) 
    1.92 +apply (simp add: formula_imp_formula_N formula.intros) 
    1.93  done
    1.94  
    1.95