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