src/ZF/Constructible/Datatype_absolute.thy
changeset 21233 5a5c8ea5f66a
parent 16417 9bc16273c2d4
child 21404 eb85850d3eb7
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Tue Nov 07 19:39:54 2006 +0100
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Tue Nov 07 19:40:13 2006 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  subsection{*The lfp of a continuous function can be expressed as a union*}
     1.6  
     1.7 -constdefs
     1.8 +definition
     1.9    directed :: "i=>o"
    1.10     "directed(A) == A\<noteq>0 & (\<forall>x\<in>A. \<forall>y\<in>A. x \<union> y \<in> A)"
    1.11  
    1.12 @@ -113,7 +113,7 @@
    1.13  
    1.14  subsection {*Absoluteness for "Iterates"*}
    1.15  
    1.16 -constdefs
    1.17 +definition
    1.18  
    1.19    iterates_MH :: "[i=>o, [i,i]=>o, i, i, i, i] => o"
    1.20     "iterates_MH(M,isF,v,n,g,z) ==
    1.21 @@ -207,7 +207,7 @@
    1.22  by (simp add: list_eq_lfp2 lfp_eq_Union list_fun_bnd_mono list_fun_contin)
    1.23  
    1.24  
    1.25 -constdefs
    1.26 +definition
    1.27    is_list_functor :: "[i=>o,i,i,i] => o"
    1.28      "is_list_functor(M,A,X,Z) == 
    1.29          \<exists>n1[M]. \<exists>AX[M]. 
    1.30 @@ -260,7 +260,7 @@
    1.31                formula_fun_contin)
    1.32  
    1.33  
    1.34 -constdefs
    1.35 +definition
    1.36    is_formula_functor :: "[i=>o,i,i] => o"
    1.37      "is_formula_functor(M,X,Z) == 
    1.38          \<exists>nat'[M]. \<exists>natnat[M]. \<exists>natnatsum[M]. \<exists>XX[M]. \<exists>X3[M]. 
    1.39 @@ -278,7 +278,7 @@
    1.40  
    1.41  subsection{*@{term M} Contains the List and Formula Datatypes*}
    1.42  
    1.43 -constdefs
    1.44 +definition
    1.45    list_N :: "[i,i] => i"
    1.46      "list_N(A,n) == (\<lambda>X. {0} + A * X)^n (0)"
    1.47  
    1.48 @@ -339,7 +339,7 @@
    1.49  apply (simp add: list_imp_list_N) 
    1.50  done
    1.51  
    1.52 -constdefs
    1.53 +definition
    1.54    is_list_N :: "[i=>o,i,i,i] => o"
    1.55      "is_list_N(M,A,n,Z) == 
    1.56        \<exists>zero[M]. empty(M,zero) & 
    1.57 @@ -366,7 +366,7 @@
    1.58  by (induct_tac p, simp_all) 
    1.59  
    1.60  
    1.61 -constdefs
    1.62 +definition
    1.63    formula_N :: "i => i"
    1.64      "formula_N(n) == (\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X)) ^ n (0)"
    1.65  
    1.66 @@ -441,14 +441,14 @@
    1.67                       le_imp_subset formula_N_mono)
    1.68  done
    1.69  
    1.70 -constdefs
    1.71 +definition
    1.72    is_formula_N :: "[i=>o,i,i] => o"
    1.73      "is_formula_N(M,n,Z) == 
    1.74        \<exists>zero[M]. empty(M,zero) & 
    1.75                  is_iterates(M, is_formula_functor(M), zero, n, Z)"
    1.76  
    1.77  
    1.78 -constdefs
    1.79 +definition
    1.80    
    1.81    mem_formula :: "[i=>o,i] => o"
    1.82      "mem_formula(M,p) == 
    1.83 @@ -584,7 +584,7 @@
    1.84  apply (simp add: nat_rec_succ)
    1.85  done
    1.86  
    1.87 -constdefs
    1.88 +definition
    1.89    is_eclose_n :: "[i=>o,i,i,i] => o"
    1.90      "is_eclose_n(M,A,n,Z) == is_iterates(M, big_union(M), A, n, Z)"
    1.91  
    1.92 @@ -643,7 +643,7 @@
    1.93  subsection {*Absoluteness for @{term transrec}*}
    1.94  
    1.95  text{* @{term "transrec(a,H) \<equiv> wfrec(Memrel(eclose({a})), a, H)"} *}
    1.96 -constdefs
    1.97 +definition
    1.98  
    1.99    is_transrec :: "[i=>o, [i,i,i]=>o, i, i] => o"
   1.100     "is_transrec(M,MH,a,z) ==
   1.101 @@ -691,7 +691,7 @@
   1.102  subsection{*Absoluteness for the List Operator @{term length}*}
   1.103  text{*But it is never used.*}
   1.104  
   1.105 -constdefs
   1.106 +definition
   1.107    is_length :: "[i=>o,i,i,i] => o"
   1.108      "is_length(M,A,l,n) ==
   1.109         \<exists>sn[M]. \<exists>list_n[M]. \<exists>list_sn[M].
   1.110 @@ -739,7 +739,7 @@
   1.111  apply (simp add: not_lt_iff_le nth_eq_0)
   1.112  done
   1.113  
   1.114 -constdefs
   1.115 +definition
   1.116    is_nth :: "[i=>o,i,i,i] => o"
   1.117      "is_nth(M,n,l,Z) ==
   1.118        \<exists>X[M]. is_iterates(M, is_tl(M), l, n, X) & is_hd(M,X,Z)"
   1.119 @@ -757,7 +757,7 @@
   1.120  
   1.121  subsection{*Relativization and Absoluteness for the @{term formula} Constructors*}
   1.122  
   1.123 -constdefs
   1.124 +definition
   1.125    is_Member :: "[i=>o,i,i,i] => o"
   1.126       --{* because @{term "Member(x,y) \<equiv> Inl(Inl(\<langle>x,y\<rangle>))"}*}
   1.127      "is_Member(M,x,y,Z) ==
   1.128 @@ -771,7 +771,7 @@
   1.129       "M(Member(x,y)) <-> M(x) & M(y)"
   1.130  by (simp add: Member_def)
   1.131  
   1.132 -constdefs
   1.133 +definition
   1.134    is_Equal :: "[i=>o,i,i,i] => o"
   1.135       --{* because @{term "Equal(x,y) \<equiv> Inl(Inr(\<langle>x,y\<rangle>))"}*}
   1.136      "is_Equal(M,x,y,Z) ==
   1.137 @@ -784,7 +784,7 @@
   1.138  lemma (in M_trivial) Equal_in_M_iff [iff]: "M(Equal(x,y)) <-> M(x) & M(y)"
   1.139  by (simp add: Equal_def)
   1.140  
   1.141 -constdefs
   1.142 +definition
   1.143    is_Nand :: "[i=>o,i,i,i] => o"
   1.144       --{* because @{term "Nand(x,y) \<equiv> Inr(Inl(\<langle>x,y\<rangle>))"}*}
   1.145      "is_Nand(M,x,y,Z) ==
   1.146 @@ -797,7 +797,7 @@
   1.147  lemma (in M_trivial) Nand_in_M_iff [iff]: "M(Nand(x,y)) <-> M(x) & M(y)"
   1.148  by (simp add: Nand_def)
   1.149  
   1.150 -constdefs
   1.151 +definition
   1.152    is_Forall :: "[i=>o,i,i] => o"
   1.153       --{* because @{term "Forall(x) \<equiv> Inr(Inr(p))"}*}
   1.154      "is_Forall(M,p,Z) == \<exists>u[M]. is_Inr(M,p,u) & is_Inr(M,u,Z)"
   1.155 @@ -813,7 +813,7 @@
   1.156  
   1.157  subsection {*Absoluteness for @{term formula_rec}*}
   1.158  
   1.159 -constdefs
   1.160 +definition
   1.161  
   1.162    formula_rec_case :: "[[i,i]=>i, [i,i]=>i, [i,i,i,i]=>i, [i,i]=>i, i, i] => i"
   1.163      --{* the instance of @{term formula_case} in @{term formula_rec}*}
   1.164 @@ -847,7 +847,7 @@
   1.165  
   1.166  
   1.167  subsubsection{*Absoluteness for the Formula Operator @{term depth}*}
   1.168 -constdefs
   1.169 +definition
   1.170  
   1.171    is_depth :: "[i=>o,i,i] => o"
   1.172      "is_depth(M,p,n) ==
   1.173 @@ -873,7 +873,7 @@
   1.174  
   1.175  subsubsection{*@{term is_formula_case}: relativization of @{term formula_case}*}
   1.176  
   1.177 -constdefs
   1.178 +definition
   1.179  
   1.180   is_formula_case ::
   1.181      "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o"
   1.182 @@ -909,7 +909,7 @@
   1.183  
   1.184  subsubsection {*Absoluteness for @{term formula_rec}: Final Results*}
   1.185  
   1.186 -constdefs
   1.187 +definition
   1.188    is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o"
   1.189      --{* predicate to relativize the functional @{term formula_rec}*}
   1.190     "is_formula_rec(M,MH,p,z)  ==