src/ZF/Constructible/Datatype_absolute.thy

 theory Datatype_absolute imports Formula WF_absolute begin
 
 
 subsection{*The lfp of a continuous function can be expressed as a union*}
 
-constdefs
+definition
   directed :: "i=>o"
    "directed(A) == A\<noteq>0 & (\<forall>x\<in>A. \<forall>y\<in>A. x \<union> y \<in> A)"
 
   contin :: "(i=>i) => o"
    "contin(h) == (\<forall>A. directed(A) --> h(\<Union>A) = (\<Union>X\<in>A. h(X)))"

 
 
 
 subsection {*Absoluteness for "Iterates"*}
 
-constdefs
+definition
 
   iterates_MH :: "[i=>o, [i,i]=>o, i, i, i, i] => o"
    "iterates_MH(M,isF,v,n,g,z) ==
         is_nat_case(M, v, \<lambda>m u. \<exists>gm[M]. fun_apply(M,g,m,gm) & isF(gm,u),
                     n, z)"

 lemma list_eq_Union:
      "list(A) = (\<Union>n\<in>nat. (\<lambda>X. {0} + A*X) ^ n (0))"
 by (simp add: list_eq_lfp2 lfp_eq_Union list_fun_bnd_mono list_fun_contin)
 
 
-constdefs
+definition
   is_list_functor :: "[i=>o,i,i,i] => o"
     "is_list_functor(M,A,X,Z) == 
         \<exists>n1[M]. \<exists>AX[M]. 
          number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)"
 

       (\<Union>n\<in>nat. (\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X)) ^ n (0))"
 by (simp add: formula_eq_lfp2 lfp_eq_Union formula_fun_bnd_mono 
               formula_fun_contin)
 
 
-constdefs
+definition
   is_formula_functor :: "[i=>o,i,i] => o"
     "is_formula_functor(M,X,Z) == 
         \<exists>nat'[M]. \<exists>natnat[M]. \<exists>natnatsum[M]. \<exists>XX[M]. \<exists>X3[M]. 
           omega(M,nat') & cartprod(M,nat',nat',natnat) & 
           is_sum(M,natnat,natnat,natnatsum) &

 by (simp add: is_formula_functor_def) 
 
 
 subsection{*@{term M} Contains the List and Formula Datatypes*}
 
-constdefs
+definition
   list_N :: "[i,i] => i"
     "list_N(A,n) == (\<lambda>X. {0} + A * X)^n (0)"
 
 lemma Nil_in_list_N [simp]: "[] \<in> list_N(A,succ(n))"
 by (simp add: list_N_def Nil_def)

 apply (subst transrec, simp) 
 apply (subst transrec) 
 apply (simp add: list_imp_list_N) 
 done
 
-constdefs
+definition
   is_list_N :: "[i=>o,i,i,i] => o"
     "is_list_N(M,A,n,Z) == 
       \<exists>zero[M]. empty(M,zero) & 
                 is_iterates(M, is_list_functor(M,A), zero, n, Z)"
   

 
 lemma depth_type [TC]: "p \<in> formula ==> depth(p) \<in> nat"
 by (induct_tac p, simp_all) 
 
 
-constdefs
+definition
   formula_N :: "i => i"
     "formula_N(n) == (\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X)) ^ n (0)"
 
 lemma Member_in_formula_N [simp]:
      "Member(x,y) \<in> formula_N(succ(n)) <-> x \<in> nat & y \<in> nat"

 apply (rule_tac i = m and j = n in Ord_linear_le, auto) 
 apply (simp_all add: subset_Un_iff [THEN iffD1] subset_Un_iff2 [THEN iffD1] 
                      le_imp_subset formula_N_mono)
 done
 
-constdefs
+definition
   is_formula_N :: "[i=>o,i,i] => o"
     "is_formula_N(M,n,Z) == 
       \<exists>zero[M]. empty(M,zero) & 
                 is_iterates(M, is_formula_functor(M), zero, n, Z)"
 
 
-constdefs
+definition
   
   mem_formula :: "[i=>o,i] => o"
     "mem_formula(M,p) == 
       \<exists>n[M]. \<exists>formn[M]. 
        finite_ordinal(M,n) & is_formula_N(M,n,formn) & p \<in> formn"

 apply (induct_tac n)
 apply (simp add: nat_rec_0)
 apply (simp add: nat_rec_succ)
 done
 
-constdefs
+definition
   is_eclose_n :: "[i=>o,i,i,i] => o"
     "is_eclose_n(M,A,n,Z) == is_iterates(M, big_union(M), A, n, Z)"
 
   mem_eclose :: "[i=>o,i,i] => o"
     "mem_eclose(M,A,l) ==

 
 
 subsection {*Absoluteness for @{term transrec}*}
 
 text{* @{term "transrec(a,H) \<equiv> wfrec(Memrel(eclose({a})), a, H)"} *}
-constdefs
+definition
 
   is_transrec :: "[i=>o, [i,i,i]=>o, i, i] => o"
    "is_transrec(M,MH,a,z) ==
       \<exists>sa[M]. \<exists>esa[M]. \<exists>mesa[M].
        upair(M,a,a,sa) & is_eclose(M,sa,esa) & membership(M,esa,mesa) &

 
 
 subsection{*Absoluteness for the List Operator @{term length}*}
 text{*But it is never used.*}
 
-constdefs
+definition
   is_length :: "[i=>o,i,i,i] => o"
     "is_length(M,A,l,n) ==
        \<exists>sn[M]. \<exists>list_n[M]. \<exists>list_sn[M].
         is_list_N(M,A,n,list_n) & l \<notin> list_n &
         successor(M,n,sn) & is_list_N(M,A,sn,list_sn) & l \<in> list_sn"

 apply (case_tac "n < length(xs)")
  apply (blast intro: nth_type transM)
 apply (simp add: not_lt_iff_le nth_eq_0)
 done
 
-constdefs
+definition
   is_nth :: "[i=>o,i,i,i] => o"
     "is_nth(M,n,l,Z) ==
       \<exists>X[M]. is_iterates(M, is_tl(M), l, n, X) & is_hd(M,X,Z)"
 
 lemma (in M_datatypes) nth_abs [simp]:

 done
 
 
 subsection{*Relativization and Absoluteness for the @{term formula} Constructors*}
 
-constdefs
+definition
   is_Member :: "[i=>o,i,i,i] => o"
      --{* because @{term "Member(x,y) \<equiv> Inl(Inl(\<langle>x,y\<rangle>))"}*}
     "is_Member(M,x,y,Z) ==
 	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inl(M,u,Z)"
 

 
 lemma (in M_trivial) Member_in_M_iff [iff]:
      "M(Member(x,y)) <-> M(x) & M(y)"
 by (simp add: Member_def)
 
-constdefs
+definition
   is_Equal :: "[i=>o,i,i,i] => o"
      --{* because @{term "Equal(x,y) \<equiv> Inl(Inr(\<langle>x,y\<rangle>))"}*}
     "is_Equal(M,x,y,Z) ==
 	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inr(M,p,u) & is_Inl(M,u,Z)"
 

 by (simp add: is_Equal_def Equal_def)
 
 lemma (in M_trivial) Equal_in_M_iff [iff]: "M(Equal(x,y)) <-> M(x) & M(y)"
 by (simp add: Equal_def)
 
-constdefs
+definition
   is_Nand :: "[i=>o,i,i,i] => o"
      --{* because @{term "Nand(x,y) \<equiv> Inr(Inl(\<langle>x,y\<rangle>))"}*}
     "is_Nand(M,x,y,Z) ==
 	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inr(M,u,Z)"
 

 by (simp add: is_Nand_def Nand_def)
 
 lemma (in M_trivial) Nand_in_M_iff [iff]: "M(Nand(x,y)) <-> M(x) & M(y)"
 by (simp add: Nand_def)
 
-constdefs
+definition
   is_Forall :: "[i=>o,i,i] => o"
      --{* because @{term "Forall(x) \<equiv> Inr(Inr(p))"}*}
     "is_Forall(M,p,Z) == \<exists>u[M]. is_Inr(M,p,u) & is_Inr(M,u,Z)"
 
 lemma (in M_trivial) Forall_abs [simp]:

 
 
 
 subsection {*Absoluteness for @{term formula_rec}*}
 
-constdefs
+definition
 
   formula_rec_case :: "[[i,i]=>i, [i,i]=>i, [i,i,i,i]=>i, [i,i]=>i, i, i] => i"
     --{* the instance of @{term formula_case} in @{term formula_rec}*}
    "formula_rec_case(a,b,c,d,h) ==
         formula_case (a, b,

 apply (simp add: formula_imp_formula_N formula.intros)
 done
 
 
 subsubsection{*Absoluteness for the Formula Operator @{term depth}*}
-constdefs
+definition
 
   is_depth :: "[i=>o,i,i] => o"
     "is_depth(M,p,n) ==
        \<exists>sn[M]. \<exists>formula_n[M]. \<exists>formula_sn[M].
         is_formula_N(M,n,formula_n) & p \<notin> formula_n &

 by (simp add: nat_into_M)
 
 
 subsubsection{*@{term is_formula_case}: relativization of @{term formula_case}*}
 
-constdefs
+definition
 
  is_formula_case ::
     "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o"
   --{*no constraint on non-formulas*}
   "is_formula_case(M, is_a, is_b, is_c, is_d, p, z) ==

 by (erule formula.cases, simp_all)
 
 
 subsubsection {*Absoluteness for @{term formula_rec}: Final Results*}
 
-constdefs
+definition
   is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o"
     --{* predicate to relativize the functional @{term formula_rec}*}
    "is_formula_rec(M,MH,p,z)  ==
       \<exists>dp[M]. \<exists>i[M]. \<exists>f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) &
              successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)"