Tidying up. New primitives is_iterates and is_iterates_fm.
--- a/src/ZF/Constructible/DPow_absolute.thy Fri Oct 18 09:53:18 2002 +0200
+++ b/src/ZF/Constructible/DPow_absolute.thy Fri Oct 18 17:50:13 2002 +0200
@@ -71,7 +71,7 @@
\<lambda>i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]"
shows "REFLECTS[\<lambda>x. is_formula_rec(L, MH(L,x), f(x), h(x)),
\<lambda>i x. is_formula_rec(**Lset(i), MH(**Lset(i),x), f(x), h(x))]"
-apply (simp (no_asm_use) only: is_formula_rec_def setclass_simps)
+apply (simp (no_asm_use) only: is_formula_rec_def)
apply (intro FOL_reflections function_reflections fun_plus_reflections
depth_reflection is_transrec_reflection MH_reflection)
done
@@ -103,7 +103,7 @@
theorem satisfies_reflection:
"REFLECTS[\<lambda>x. is_satisfies(L,f(x),g(x),h(x)),
\<lambda>i x. is_satisfies(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: is_satisfies_def setclass_simps)
+apply (simp only: is_satisfies_def)
apply (intro formula_rec_reflection satisfies_MH_reflection)
done
@@ -351,7 +351,7 @@
\<lambda>i x. is_P(**Lset(i), f(x), g(x))]"
shows "REFLECTS[\<lambda>x. is_Collect(L, f(x), is_P(L,x), g(x)),
\<lambda>i x. is_Collect(**Lset(i), f(x), is_P(**Lset(i), x), g(x))]"
-apply (simp (no_asm_use) only: is_Collect_def setclass_simps)
+apply (simp (no_asm_use) only: is_Collect_def)
apply (intro FOL_reflections is_P_reflection)
done
@@ -403,7 +403,7 @@
\<lambda>i x. is_P(**Lset(i), f(x), g(x), h(x))]"
shows "REFLECTS[\<lambda>x. is_Replace(L, f(x), is_P(L,x), g(x)),
\<lambda>i x. is_Replace(**Lset(i), f(x), is_P(**Lset(i), x), g(x))]"
-apply (simp (no_asm_use) only: is_Replace_def setclass_simps)
+apply (simp (no_asm_use) only: is_Replace_def)
apply (intro FOL_reflections is_P_reflection)
done
@@ -447,7 +447,7 @@
theorem DPow'_reflection:
"REFLECTS[\<lambda>x. is_DPow'(L,f(x),g(x)),
\<lambda>i x. is_DPow'(**Lset(i),f(x),g(x))]"
-apply (simp only: is_DPow'_def setclass_simps)
+apply (simp only: is_DPow'_def)
apply (intro FOL_reflections function_reflections mem_formula_reflection
mem_list_reflection Collect_reflection DPow_body_reflection)
done
@@ -574,7 +574,7 @@
\<exists>gy \<in> Lset(i). y \<in> x & fun_apply(**Lset(i),f,y,gy) &
is_DPow'(**Lset(i),gy,z), r) &
big_union(**Lset(i),r,u), mr, v, y))]"
-apply (simp only: setclass_simps [symmetric])
+apply (simp only: rex_setclass_is_bex [symmetric])
--{*Convert @{text "\<exists>y\<in>Lset(i)"} to @{text "\<exists>y[**Lset(i)]"} within the body
of the @{term is_wfrec} application. *}
apply (intro FOL_reflections function_reflections
--- a/src/ZF/Constructible/Datatype_absolute.thy Fri Oct 18 09:53:18 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy Fri Oct 18 17:50:13 2002 +0200
@@ -125,6 +125,11 @@
\<forall>n[M]. n\<in>nat -->
wfrec_replacement(M, iterates_MH(M,isF,v), Memrel(succ(n)))"
+ is_iterates :: "[i=>o, [i,i]=>o, i, i, i] => o"
+ "is_iterates(M,isF,v,n,Z) ==
+ \<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
+ is_wfrec(M, iterates_MH(M,isF,v), msn, n, Z)"
+
lemma (in M_basic) iterates_MH_abs:
"[| relation1(M,isF,F); M(n); M(g); M(z) |]
==> iterates_MH(M,isF,v,n,g,z) <-> z = nat_case(v, \<lambda>m. F(g`m), n)"
@@ -140,11 +145,10 @@
theorem (in M_trancl) iterates_abs:
"[| iterates_replacement(M,isF,v); relation1(M,isF,F);
n \<in> nat; M(v); M(z); \<forall>x[M]. M(F(x)) |]
- ==> is_wfrec(M, iterates_MH(M,isF,v), Memrel(succ(n)), n, z) <->
- z = iterates(F,n,v)"
+ ==> is_iterates(M,isF,v,n,z) <-> z = iterates(F,n,v)"
apply (frule iterates_imp_wfrec_replacement, assumption+)
apply (simp add: wf_Memrel trans_Memrel relation_Memrel nat_into_M
- relation2_def iterates_MH_abs
+ is_iterates_def relation2_def iterates_MH_abs
iterates_nat_def recursor_def transrec_def
eclose_sing_Ord_eq nat_into_M
trans_wfrec_abs [of _ _ _ _ "\<lambda>n g. nat_case(v, \<lambda>m. F(g`m), n)"])
@@ -338,10 +342,8 @@
constdefs
is_list_N :: "[i=>o,i,i,i] => o"
"is_list_N(M,A,n,Z) ==
- \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M].
- empty(M,zero) &
- successor(M,n,sn) & membership(M,sn,msn) &
- is_wfrec(M, iterates_MH(M, is_list_functor(M,A),zero), msn, n, Z)"
+ \<exists>zero[M]. empty(M,zero) &
+ is_iterates(M, is_list_functor(M,A), zero, n, Z)"
mem_list :: "[i=>o,i,i] => o"
"mem_list(M,A,l) ==
@@ -442,11 +444,9 @@
constdefs
is_formula_N :: "[i=>o,i,i] => o"
"is_formula_N(M,n,Z) ==
- \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M].
- empty(M,zero) &
- successor(M,n,sn) & membership(M,sn,msn) &
- is_wfrec(M, iterates_MH(M, is_formula_functor(M),zero), msn, n, Z)"
-
+ \<exists>zero[M]. empty(M,zero) &
+ is_iterates(M, is_formula_functor(M), zero, n, Z)"
+
constdefs
@@ -459,40 +459,34 @@
"is_formula(M,Z) == \<forall>p[M]. p \<in> Z <-> mem_formula(M,p)"
locale M_datatypes = M_trancl +
- assumes list_replacement1:
+ assumes list_replacement1:
"M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
- and list_replacement2:
- "M(A) ==> strong_replacement(M,
- \<lambda>n y. n\<in>nat &
- (\<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
- is_wfrec(M, iterates_MH(M,is_list_functor(M,A), 0),
- msn, n, y)))"
- and formula_replacement1:
+ and list_replacement2:
+ "M(A) ==> strong_replacement(M,
+ \<lambda>n y. n\<in>nat & is_iterates(M, is_list_functor(M,A), 0, n, y))"
+ and formula_replacement1:
"iterates_replacement(M, is_formula_functor(M), 0)"
- and formula_replacement2:
- "strong_replacement(M,
- \<lambda>n y. n\<in>nat &
- (\<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
- is_wfrec(M, iterates_MH(M,is_formula_functor(M), 0),
- msn, n, y)))"
+ and formula_replacement2:
+ "strong_replacement(M,
+ \<lambda>n y. n\<in>nat & is_iterates(M, is_formula_functor(M), 0, n, y))"
and nth_replacement:
"M(l) ==> iterates_replacement(M, %l t. is_tl(M,l,t), l)"
-
+
subsubsection{*Absoluteness of the List Construction*}
-lemma (in M_datatypes) list_replacement2':
+lemma (in M_datatypes) list_replacement2':
"M(A) ==> strong_replacement(M, \<lambda>n y. n\<in>nat & y = (\<lambda>X. {0} + A * X)^n (0))"
-apply (insert list_replacement2 [of A])
-apply (rule strong_replacement_cong [THEN iffD1])
-apply (rule conj_cong [OF iff_refl iterates_abs [of "is_list_functor(M,A)"]])
-apply (simp_all add: list_replacement1 relation1_def)
+apply (insert list_replacement2 [of A])
+apply (rule strong_replacement_cong [THEN iffD1])
+apply (rule conj_cong [OF iff_refl iterates_abs [of "is_list_functor(M,A)"]])
+apply (simp_all add: list_replacement1 relation1_def)
done
lemma (in M_datatypes) list_closed [intro,simp]:
"M(A) ==> M(list(A))"
apply (insert list_replacement1)
-by (simp add: RepFun_closed2 list_eq_Union
+by (simp add: RepFun_closed2 list_eq_Union
list_replacement2' relation1_def
iterates_closed [of "is_list_functor(M,A)"])
@@ -500,7 +494,7 @@
lemmas (in M_datatypes) list_into_M = transM [OF _ list_closed]
lemma (in M_datatypes) list_N_abs [simp]:
- "[|M(A); n\<in>nat; M(Z)|]
+ "[|M(A); n\<in>nat; M(Z)|]
==> is_list_N(M,A,n,Z) <-> Z = list_N(A,n)"
apply (insert list_replacement1)
apply (simp add: is_list_N_def list_N_def relation1_def nat_into_M
@@ -518,7 +512,7 @@
"M(A) ==> mem_list(M,A,l) <-> l \<in> list(A)"
apply (insert list_replacement1)
apply (simp add: mem_list_def list_N_def relation1_def list_eq_Union
- iterates_closed [of "is_list_functor(M,A)"])
+ iterates_closed [of "is_list_functor(M,A)"])
done
lemma (in M_datatypes) list_abs [simp]:
@@ -529,18 +523,18 @@
subsubsection{*Absoluteness of Formulas*}
-lemma (in M_datatypes) formula_replacement2':
+lemma (in M_datatypes) formula_replacement2':
"strong_replacement(M, \<lambda>n y. n\<in>nat & y = (\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X))^n (0))"
-apply (insert formula_replacement2)
-apply (rule strong_replacement_cong [THEN iffD1])
-apply (rule conj_cong [OF iff_refl iterates_abs [of "is_formula_functor(M)"]])
-apply (simp_all add: formula_replacement1 relation1_def)
+apply (insert formula_replacement2)
+apply (rule strong_replacement_cong [THEN iffD1])
+apply (rule conj_cong [OF iff_refl iterates_abs [of "is_formula_functor(M)"]])
+apply (simp_all add: formula_replacement1 relation1_def)
done
lemma (in M_datatypes) formula_closed [intro,simp]:
"M(formula)"
apply (insert formula_replacement1)
-apply (simp add: RepFun_closed2 formula_eq_Union
+apply (simp add: RepFun_closed2 formula_eq_Union
formula_replacement2' relation1_def
iterates_closed [of "is_formula_functor(M)"])
done
@@ -548,11 +542,11 @@
lemmas (in M_datatypes) formula_into_M = transM [OF _ formula_closed]
lemma (in M_datatypes) formula_N_abs [simp]:
- "[|n\<in>nat; M(Z)|]
+ "[|n\<in>nat; M(Z)|]
==> is_formula_N(M,n,Z) <-> Z = formula_N(n)"
apply (insert formula_replacement1)
apply (simp add: is_formula_N_def formula_N_def relation1_def nat_into_M
- iterates_abs [of "is_formula_functor(M)" _
+ iterates_abs [of "is_formula_functor(M)" _
"\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X)"])
done
@@ -567,7 +561,7 @@
"mem_formula(M,l) <-> l \<in> formula"
apply (insert formula_replacement1)
apply (simp add: mem_formula_def relation1_def formula_eq_Union formula_N_def
- iterates_closed [of "is_formula_functor(M)"])
+ iterates_closed [of "is_formula_functor(M)"])
done
lemma (in M_datatypes) formula_abs [simp]:
@@ -582,24 +576,21 @@
text{*Re-expresses eclose using "iterates"*}
lemma eclose_eq_Union:
"eclose(A) = (\<Union>n\<in>nat. Union^n (A))"
-apply (simp add: eclose_def)
-apply (rule UN_cong)
+apply (simp add: eclose_def)
+apply (rule UN_cong)
apply (rule refl)
apply (induct_tac n)
-apply (simp add: nat_rec_0)
-apply (simp add: nat_rec_succ)
+apply (simp add: nat_rec_0)
+apply (simp add: nat_rec_succ)
done
constdefs
is_eclose_n :: "[i=>o,i,i,i] => o"
- "is_eclose_n(M,A,n,Z) ==
- \<exists>sn[M]. \<exists>msn[M].
- successor(M,n,sn) & membership(M,sn,msn) &
- is_wfrec(M, iterates_MH(M, big_union(M), A), msn, n, Z)"
-
+ "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) ==
- \<exists>n[M]. \<exists>eclosen[M].
+ "mem_eclose(M,A,l) ==
+ \<exists>n[M]. \<exists>eclosen[M].
finite_ordinal(M,n) & is_eclose_n(M,A,n,eclosen) & l \<in> eclosen"
is_eclose :: "[i=>o,i,i] => o"
@@ -607,27 +598,24 @@
locale M_eclose = M_datatypes +
- assumes eclose_replacement1:
+ assumes eclose_replacement1:
"M(A) ==> iterates_replacement(M, big_union(M), A)"
- and eclose_replacement2:
- "M(A) ==> strong_replacement(M,
- \<lambda>n y. n\<in>nat &
- (\<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
- is_wfrec(M, iterates_MH(M,big_union(M), A),
- msn, n, y)))"
+ and eclose_replacement2:
+ "M(A) ==> strong_replacement(M,
+ \<lambda>n y. n\<in>nat & is_iterates(M, big_union(M), A, n, y))"
-lemma (in M_eclose) eclose_replacement2':
+lemma (in M_eclose) eclose_replacement2':
"M(A) ==> strong_replacement(M, \<lambda>n y. n\<in>nat & y = Union^n (A))"
-apply (insert eclose_replacement2 [of A])
-apply (rule strong_replacement_cong [THEN iffD1])
-apply (rule conj_cong [OF iff_refl iterates_abs [of "big_union(M)"]])
-apply (simp_all add: eclose_replacement1 relation1_def)
+apply (insert eclose_replacement2 [of A])
+apply (rule strong_replacement_cong [THEN iffD1])
+apply (rule conj_cong [OF iff_refl iterates_abs [of "big_union(M)"]])
+apply (simp_all add: eclose_replacement1 relation1_def)
done
lemma (in M_eclose) eclose_closed [intro,simp]:
"M(A) ==> M(eclose(A))"
apply (insert eclose_replacement1)
-by (simp add: RepFun_closed2 eclose_eq_Union
+by (simp add: RepFun_closed2 eclose_eq_Union
eclose_replacement2' relation1_def
iterates_closed [of "big_union(M)"])
@@ -642,7 +630,7 @@
"M(A) ==> mem_eclose(M,A,l) <-> l \<in> eclose(A)"
apply (insert eclose_replacement1)
apply (simp add: mem_eclose_def relation1_def eclose_eq_Union
- iterates_closed [of "big_union(M)"])
+ iterates_closed [of "big_union(M)"])
done
lemma (in M_eclose) eclose_abs [simp]:
@@ -652,54 +640,52 @@
done
-
-
subsection {*Absoluteness for @{term transrec}*}
-
text{* @{term "transrec(a,H) \<equiv> wfrec(Memrel(eclose({a})), a, H)"} *}
constdefs
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].
+ "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) &
is_wfrec(M,MH,mesa,a,z)"
transrec_replacement :: "[i=>o, [i,i,i]=>o, i] => o"
"transrec_replacement(M,MH,a) ==
- \<exists>sa[M]. \<exists>esa[M]. \<exists>mesa[M].
+ \<exists>sa[M]. \<exists>esa[M]. \<exists>mesa[M].
upair(M,a,a,sa) & is_eclose(M,sa,esa) & membership(M,esa,mesa) &
wfrec_replacement(M,MH,mesa)"
-text{*The condition @{term "Ord(i)"} lets us use the simpler
+text{*The condition @{term "Ord(i)"} lets us use the simpler
@{text "trans_wfrec_abs"} rather than @{text "trans_wfrec_abs"},
which I haven't even proved yet. *}
theorem (in M_eclose) transrec_abs:
"[|transrec_replacement(M,MH,i); relation2(M,MH,H);
Ord(i); M(i); M(z);
- \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|]
- ==> is_transrec(M,MH,i,z) <-> z = transrec(i,H)"
+ \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|]
+ ==> is_transrec(M,MH,i,z) <-> z = transrec(i,H)"
by (simp add: trans_wfrec_abs transrec_replacement_def is_transrec_def
transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
theorem (in M_eclose) transrec_closed:
"[|transrec_replacement(M,MH,i); relation2(M,MH,H);
- Ord(i); M(i);
- \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|]
+ Ord(i); M(i);
+ \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|]
==> M(transrec(i,H))"
by (simp add: trans_wfrec_closed transrec_replacement_def is_transrec_def
transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
text{*Helps to prove instances of @{term transrec_replacement}*}
-lemma (in M_eclose) transrec_replacementI:
+lemma (in M_eclose) transrec_replacementI:
"[|M(a);
- strong_replacement (M,
- \<lambda>x z. \<exists>y[M]. pair(M, x, y, z) \<and> is_wfrec(M,MH,Memrel(eclose({a})),x,y))|]
+ strong_replacement (M,
+ \<lambda>x z. \<exists>y[M]. pair(M, x, y, z) &
+ is_wfrec(M,MH,Memrel(eclose({a})),x,y))|]
==> transrec_replacement(M,MH,a)"
-by (simp add: transrec_replacement_def wfrec_replacement_def)
+by (simp add: transrec_replacement_def wfrec_replacement_def)
subsection{*Absoluteness for the List Operator @{term length}*}
@@ -707,8 +693,8 @@
constdefs
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_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"
@@ -716,7 +702,7 @@
lemma (in M_datatypes) length_abs [simp]:
"[|M(A); l \<in> list(A); n \<in> nat|] ==> is_length(M,A,l,n) <-> n = length(l)"
apply (subgoal_tac "M(l) & M(n)")
- prefer 2 apply (blast dest: transM)
+ prefer 2 apply (blast dest: transM)
apply (simp add: is_length_def)
apply (blast intro: list_imp_list_N nat_into_Ord list_N_imp_eq_length
dest: list_N_imp_length_lt)
@@ -725,29 +711,29 @@
text{*Proof is trivial since @{term length} returns natural numbers.*}
lemma (in M_trivial) length_closed [intro,simp]:
"l \<in> list(A) ==> M(length(l))"
-by (simp add: nat_into_M)
+by (simp add: nat_into_M)
subsection {*Absoluteness for the List Operator @{term nth}*}
lemma nth_eq_hd_iterates_tl [rule_format]:
"xs \<in> list(A) ==> \<forall>n \<in> nat. nth(n,xs) = hd' (tl'^n (xs))"
-apply (induct_tac xs)
-apply (simp add: iterates_tl_Nil hd'_Nil, clarify)
+apply (induct_tac xs)
+apply (simp add: iterates_tl_Nil hd'_Nil, clarify)
apply (erule natE)
-apply (simp add: hd'_Cons)
-apply (simp add: tl'_Cons iterates_commute)
+apply (simp add: hd'_Cons)
+apply (simp add: tl'_Cons iterates_commute)
done
lemma (in M_basic) iterates_tl'_closed:
"[|n \<in> nat; M(x)|] ==> M(tl'^n (x))"
-apply (induct_tac n, simp)
-apply (simp add: tl'_Cons tl'_closed)
+apply (induct_tac n, simp)
+apply (simp add: tl'_Cons tl'_closed)
done
text{*Immediate by type-checking*}
lemma (in M_datatypes) nth_closed [intro,simp]:
- "[|xs \<in> list(A); n \<in> nat; M(A)|] ==> M(nth(n,xs))"
+ "[|xs \<in> list(A); n \<in> nat; M(A)|] ==> M(nth(n,xs))"
apply (case_tac "n < length(xs)")
apply (blast intro: nth_type transM)
apply (simp add: not_lt_iff_le nth_eq_0)
@@ -755,19 +741,16 @@
constdefs
is_nth :: "[i=>o,i,i,i] => o"
- "is_nth(M,n,l,Z) ==
- \<exists>X[M]. \<exists>sn[M]. \<exists>msn[M].
- successor(M,n,sn) & membership(M,sn,msn) &
- is_wfrec(M, iterates_MH(M, is_tl(M), l), msn, n, X) &
- is_hd(M,X,Z)"
-
+ "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]:
- "[|M(A); n \<in> nat; l \<in> list(A); M(Z)|]
+ "[|M(A); n \<in> nat; l \<in> list(A); M(Z)|]
==> is_nth(M,n,l,Z) <-> Z = nth(n,l)"
-apply (subgoal_tac "M(l)")
+apply (subgoal_tac "M(l)")
prefer 2 apply (blast intro: transM)
apply (simp add: is_nth_def nth_eq_hd_iterates_tl nat_into_M
- tl'_closed iterates_tl'_closed
+ tl'_closed iterates_tl'_closed
iterates_abs [OF _ relation1_tl] nth_replacement)
done
@@ -786,7 +769,7 @@
lemma (in M_trivial) Member_in_M_iff [iff]:
"M(Member(x,y)) <-> M(x) & M(y)"
-by (simp add: Member_def)
+by (simp add: Member_def)
constdefs
is_Equal :: "[i=>o,i,i,i] => o"
@@ -799,7 +782,7 @@
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)
+by (simp add: Equal_def)
constdefs
is_Nand :: "[i=>o,i,i,i] => o"
@@ -812,7 +795,7 @@
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)
+by (simp add: Nand_def)
constdefs
is_Forall :: "[i=>o,i,i] => o"
@@ -836,7 +819,7 @@
--{* the instance of @{term formula_case} in @{term formula_rec}*}
"formula_rec_case(a,b,c,d,h) ==
formula_case (a, b,
- \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u,
+ \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u,
h ` succ(depth(v)) ` v),
\<lambda>u. d(u, h ` succ(depth(u)) ` u))"
@@ -845,21 +828,21 @@
neither of which is absolute.*}
lemma (in M_trivial) formula_rec_eq:
"p \<in> formula ==>
- formula_rec(a,b,c,d,p) =
+ formula_rec(a,b,c,d,p) =
transrec (succ(depth(p)),
\<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h))) ` p"
apply (simp add: formula_rec_case_def)
apply (induct_tac p)
txt{*Base case for @{term Member}*}
- apply (subst transrec, simp add: formula.intros)
+ apply (subst transrec, simp add: formula.intros)
txt{*Base case for @{term Equal}*}
apply (subst transrec, simp add: formula.intros)
txt{*Inductive step for @{term Nand}*}
- apply (subst transrec)
+ apply (subst transrec)
apply (simp add: succ_Un_distrib formula.intros)
txt{*Inductive step for @{term Forall}*}
-apply (subst transrec)
-apply (simp add: formula_imp_formula_N formula.intros)
+apply (subst transrec)
+apply (simp add: formula_imp_formula_N formula.intros)
done
@@ -867,8 +850,8 @@
constdefs
is_depth :: "[i=>o,i,i] => o"
- "is_depth(M,p,n) ==
- \<exists>sn[M]. \<exists>formula_n[M]. \<exists>formula_sn[M].
+ "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 &
successor(M,n,sn) & is_formula_N(M,sn,formula_sn) & p \<in> formula_sn"
@@ -876,7 +859,7 @@
lemma (in M_datatypes) depth_abs [simp]:
"[|p \<in> formula; n \<in> nat|] ==> is_depth(M,p,n) <-> n = depth(p)"
apply (subgoal_tac "M(p) & M(n)")
- prefer 2 apply (blast dest: transM)
+ prefer 2 apply (blast dest: transM)
apply (simp add: is_depth_def)
apply (blast intro: formula_imp_formula_N nat_into_Ord formula_N_imp_eq_depth
dest: formula_N_imp_depth_lt)
@@ -885,43 +868,43 @@
text{*Proof is trivial since @{term depth} returns natural numbers.*}
lemma (in M_trivial) depth_closed [intro,simp]:
"p \<in> formula ==> M(depth(p))"
-by (simp add: nat_into_M)
+by (simp add: nat_into_M)
subsubsection{*@{term is_formula_case}: relativization of @{term formula_case}*}
constdefs
- is_formula_case ::
+ 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) ==
- (\<forall>x[M]. \<forall>y[M]. finite_ordinal(M,x) --> finite_ordinal(M,y) -->
+ "is_formula_case(M, is_a, is_b, is_c, is_d, p, z) ==
+ (\<forall>x[M]. \<forall>y[M]. finite_ordinal(M,x) --> finite_ordinal(M,y) -->
is_Member(M,x,y,p) --> is_a(x,y,z)) &
- (\<forall>x[M]. \<forall>y[M]. finite_ordinal(M,x) --> finite_ordinal(M,y) -->
+ (\<forall>x[M]. \<forall>y[M]. finite_ordinal(M,x) --> finite_ordinal(M,y) -->
is_Equal(M,x,y,p) --> is_b(x,y,z)) &
- (\<forall>x[M]. \<forall>y[M]. mem_formula(M,x) --> mem_formula(M,y) -->
+ (\<forall>x[M]. \<forall>y[M]. mem_formula(M,x) --> mem_formula(M,y) -->
is_Nand(M,x,y,p) --> is_c(x,y,z)) &
(\<forall>x[M]. mem_formula(M,x) --> is_Forall(M,x,p) --> is_d(x,z))"
-lemma (in M_datatypes) formula_case_abs [simp]:
- "[| Relation2(M,nat,nat,is_a,a); Relation2(M,nat,nat,is_b,b);
- Relation2(M,formula,formula,is_c,c); Relation1(M,formula,is_d,d);
- p \<in> formula; M(z) |]
- ==> is_formula_case(M,is_a,is_b,is_c,is_d,p,z) <->
+lemma (in M_datatypes) formula_case_abs [simp]:
+ "[| Relation2(M,nat,nat,is_a,a); Relation2(M,nat,nat,is_b,b);
+ Relation2(M,formula,formula,is_c,c); Relation1(M,formula,is_d,d);
+ p \<in> formula; M(z) |]
+ ==> is_formula_case(M,is_a,is_b,is_c,is_d,p,z) <->
z = formula_case(a,b,c,d,p)"
apply (simp add: formula_into_M is_formula_case_def)
-apply (erule formula.cases)
- apply (simp_all add: Relation1_def Relation2_def)
+apply (erule formula.cases)
+ apply (simp_all add: Relation1_def Relation2_def)
done
lemma (in M_datatypes) formula_case_closed [intro,simp]:
- "[|p \<in> formula;
- \<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> M(a(x,y));
- \<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> M(b(x,y));
- \<forall>x[M]. \<forall>y[M]. x\<in>formula --> y\<in>formula --> M(c(x,y));
+ "[|p \<in> formula;
+ \<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> M(a(x,y));
+ \<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> M(b(x,y));
+ \<forall>x[M]. \<forall>y[M]. x\<in>formula --> y\<in>formula --> M(c(x,y));
\<forall>x[M]. x\<in>formula --> M(d(x))|] ==> M(formula_case(a,b,c,d,p))"
-by (erule formula.cases, simp_all)
+by (erule formula.cases, simp_all)
subsubsection {*Absoluteness for @{term formula_rec}: Final Results*}
@@ -930,7 +913,7 @@
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) &
+ \<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)"
@@ -939,16 +922,16 @@
lemma (in M_datatypes) Relation1_formula_rec_case:
"[|Relation2(M, nat, nat, is_a, a);
Relation2(M, nat, nat, is_b, b);
- Relation2 (M, formula, formula,
+ Relation2 (M, formula, formula,
is_c, \<lambda>u v. c(u, v, h`succ(depth(u))`u, h`succ(depth(v))`v));
- Relation1(M, formula,
+ Relation1(M, formula,
is_d, \<lambda>u. d(u, h ` succ(depth(u)) ` u));
- M(h) |]
+ M(h) |]
==> Relation1(M, formula,
is_formula_case (M, is_a, is_b, is_c, is_d),
formula_rec_case(a, b, c, d, h))"
-apply (simp (no_asm) add: formula_rec_case_def Relation1_def)
-apply (simp add: formula_case_abs)
+apply (simp (no_asm) add: formula_rec_case_def Relation1_def)
+apply (simp add: formula_case_abs)
done
@@ -970,12 +953,12 @@
and c_closed: "[|x \<in> formula; y \<in> formula; M(gx); M(gy)|]
==> M(c(x, y, gx, gy))"
and c_rel:
- "M(f) ==>
+ "M(f) ==>
Relation2 (M, formula, formula, is_c(f),
\<lambda>u v. c(u, v, f ` succ(depth(u)) ` u, f ` succ(depth(v)) ` v))"
and d_closed: "[|x \<in> formula; M(gx)|] ==> M(d(x, gx))"
and d_rel:
- "M(f) ==>
+ "M(f) ==>
Relation1(M, formula, is_d(f), \<lambda>u. d(u, f ` succ(depth(u)) ` u))"
and fr_replace: "n \<in> nat ==> transrec_replacement(M,MH,n)"
and fr_lam_replace:
@@ -986,7 +969,7 @@
lemma (in Formula_Rec) formula_rec_case_closed:
"[|M(g); p \<in> formula|] ==> M(formula_rec_case(a, b, c, d, g, p))"
-by (simp add: formula_rec_case_def a_closed b_closed c_closed d_closed)
+by (simp add: formula_rec_case_def a_closed b_closed c_closed d_closed)
lemma (in Formula_Rec) formula_rec_lam_closed:
"M(g) ==> M(Lambda (formula, formula_rec_case(a,b,c,d,g)))"
@@ -995,29 +978,29 @@
lemma (in Formula_Rec) MH_rel2:
"relation2 (M, MH,
\<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h)))"
-apply (simp add: relation2_def MH_def, clarify)
-apply (rule lambda_abs2)
+apply (simp add: relation2_def MH_def, clarify)
+apply (rule lambda_abs2)
apply (rule fr_lam_replace, assumption)
-apply (rule Relation1_formula_rec_case)
-apply (simp_all add: a_rel b_rel c_rel d_rel formula_rec_case_closed)
+apply (rule Relation1_formula_rec_case)
+apply (simp_all add: a_rel b_rel c_rel d_rel formula_rec_case_closed)
done
lemma (in Formula_Rec) fr_transrec_closed:
"n \<in> nat
==> M(transrec
(n, \<lambda>x h. Lambda(formula, formula_rec_case(a, b, c, d, h))))"
-by (simp add: transrec_closed [OF fr_replace MH_rel2]
- nat_into_M formula_rec_lam_closed)
+by (simp add: transrec_closed [OF fr_replace MH_rel2]
+ nat_into_M formula_rec_lam_closed)
text{*The main two results: @{term formula_rec} is absolute for @{term M}.*}
theorem (in Formula_Rec) formula_rec_closed:
"p \<in> formula ==> M(formula_rec(a,b,c,d,p))"
-by (simp add: formula_rec_eq fr_transrec_closed
+by (simp add: formula_rec_eq fr_transrec_closed
transM [OF _ formula_closed])
theorem (in Formula_Rec) formula_rec_abs:
- "[| p \<in> formula; M(z)|]
- ==> is_formula_rec(M,MH,p,z) <-> z = formula_rec(a,b,c,d,p)"
+ "[| p \<in> formula; M(z)|]
+ ==> is_formula_rec(M,MH,p,z) <-> z = formula_rec(a,b,c,d,p)"
by (simp add: is_formula_rec_def formula_rec_eq transM [OF _ formula_closed]
transrec_abs [OF fr_replace MH_rel2] depth_type
fr_transrec_closed formula_rec_lam_closed eq_commute)
--- a/src/ZF/Constructible/Internalize.thy Fri Oct 18 09:53:18 2002 +0200
+++ b/src/ZF/Constructible/Internalize.thy Fri Oct 18 17:50:13 2002 +0200
@@ -31,7 +31,7 @@
theorem Inl_reflection:
"REFLECTS[\<lambda>x. is_Inl(L,f(x),h(x)),
\<lambda>i x. is_Inl(**Lset(i),f(x),h(x))]"
-apply (simp only: is_Inl_def setclass_simps)
+apply (simp only: is_Inl_def)
apply (intro FOL_reflections function_reflections)
done
@@ -60,7 +60,7 @@
theorem Inr_reflection:
"REFLECTS[\<lambda>x. is_Inr(L,f(x),h(x)),
\<lambda>i x. is_Inr(**Lset(i),f(x),h(x))]"
-apply (simp only: is_Inr_def setclass_simps)
+apply (simp only: is_Inr_def)
apply (intro FOL_reflections function_reflections)
done
@@ -88,7 +88,7 @@
theorem Nil_reflection:
"REFLECTS[\<lambda>x. is_Nil(L,f(x)),
\<lambda>i x. is_Nil(**Lset(i),f(x))]"
-apply (simp only: is_Nil_def setclass_simps)
+apply (simp only: is_Nil_def)
apply (intro FOL_reflections function_reflections Inl_reflection)
done
@@ -120,7 +120,7 @@
theorem Cons_reflection:
"REFLECTS[\<lambda>x. is_Cons(L,f(x),g(x),h(x)),
\<lambda>i x. is_Cons(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: is_Cons_def setclass_simps)
+apply (simp only: is_Cons_def)
apply (intro FOL_reflections pair_reflection Inr_reflection)
done
@@ -148,7 +148,7 @@
theorem quasilist_reflection:
"REFLECTS[\<lambda>x. is_quasilist(L,f(x)),
\<lambda>i x. is_quasilist(**Lset(i),f(x))]"
-apply (simp only: is_quasilist_def setclass_simps)
+apply (simp only: is_quasilist_def)
apply (intro FOL_reflections Nil_reflection Cons_reflection)
done
@@ -186,7 +186,7 @@
theorem hd_reflection:
"REFLECTS[\<lambda>x. is_hd(L,f(x),g(x)),
\<lambda>i x. is_hd(**Lset(i),f(x),g(x))]"
-apply (simp only: is_hd_def setclass_simps)
+apply (simp only: is_hd_def)
apply (intro FOL_reflections Nil_reflection Cons_reflection
quasilist_reflection empty_reflection)
done
@@ -222,7 +222,7 @@
theorem tl_reflection:
"REFLECTS[\<lambda>x. is_tl(L,f(x),g(x)),
\<lambda>i x. is_tl(**Lset(i),f(x),g(x))]"
-apply (simp only: is_tl_def setclass_simps)
+apply (simp only: is_tl_def)
apply (intro FOL_reflections Nil_reflection Cons_reflection
quasilist_reflection empty_reflection)
done
@@ -260,7 +260,7 @@
"REFLECTS [P(L), \<lambda>i. P(**Lset(i))] ==>
REFLECTS[\<lambda>x. is_bool_of_o(L, P(L,x), f(x)),
\<lambda>i x. is_bool_of_o(**Lset(i), P(**Lset(i),x), f(x))]"
-apply (simp (no_asm) only: is_bool_of_o_def setclass_simps)
+apply (simp (no_asm) only: is_bool_of_o_def)
apply (intro FOL_reflections function_reflections, assumption+)
done
@@ -301,24 +301,13 @@
is_lambda(**A, nth(x,env), is_b, nth(y,env))"
by (simp add: lambda_fm_def is_lambda_def is_b_iff_sats [THEN iff_sym])
-lemma is_lambda_iff_sats:
- assumes is_b_iff_sats:
- "!!a0 a1 a2.
- [|a0\<in>A; a1\<in>A; a2\<in>A|]
- ==> is_b(a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,env))))"
- shows
- "[|nth(i,env) = x; nth(j,env) = y;
- i \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> is_lambda(**A, x, is_b, y) <-> sats(A, lambda_fm(p,i,j), env)"
-by (simp add: sats_lambda_fm [OF is_b_iff_sats])
-
theorem is_lambda_reflection:
assumes is_b_reflection:
"!!f' f g h. REFLECTS[\<lambda>x. is_b(L, f'(x), f(x), g(x)),
\<lambda>i x. is_b(**Lset(i), f'(x), f(x), g(x))]"
shows "REFLECTS[\<lambda>x. is_lambda(L, A(x), is_b(L,x), f(x)),
\<lambda>i x. is_lambda(**Lset(i), A(x), is_b(**Lset(i),x), f(x))]"
-apply (simp (no_asm_use) only: is_lambda_def setclass_simps)
+apply (simp (no_asm_use) only: is_lambda_def)
apply (intro FOL_reflections is_b_reflection pair_reflection)
done
@@ -350,7 +339,7 @@
theorem Member_reflection:
"REFLECTS[\<lambda>x. is_Member(L,f(x),g(x),h(x)),
\<lambda>i x. is_Member(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: is_Member_def setclass_simps)
+apply (simp only: is_Member_def)
apply (intro FOL_reflections pair_reflection Inl_reflection)
done
@@ -382,7 +371,7 @@
theorem Equal_reflection:
"REFLECTS[\<lambda>x. is_Equal(L,f(x),g(x),h(x)),
\<lambda>i x. is_Equal(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: is_Equal_def setclass_simps)
+apply (simp only: is_Equal_def)
apply (intro FOL_reflections pair_reflection Inl_reflection Inr_reflection)
done
@@ -414,7 +403,7 @@
theorem Nand_reflection:
"REFLECTS[\<lambda>x. is_Nand(L,f(x),g(x),h(x)),
\<lambda>i x. is_Nand(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: is_Nand_def setclass_simps)
+apply (simp only: is_Nand_def)
apply (intro FOL_reflections pair_reflection Inl_reflection Inr_reflection)
done
@@ -444,7 +433,7 @@
theorem Forall_reflection:
"REFLECTS[\<lambda>x. is_Forall(L,f(x),g(x)),
\<lambda>i x. is_Forall(**Lset(i),f(x),g(x))]"
-apply (simp only: is_Forall_def setclass_simps)
+apply (simp only: is_Forall_def)
apply (intro FOL_reflections pair_reflection Inr_reflection)
done
@@ -477,7 +466,7 @@
theorem is_and_reflection:
"REFLECTS[\<lambda>x. is_and(L,f(x),g(x),h(x)),
\<lambda>i x. is_and(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: is_and_def setclass_simps)
+apply (simp only: is_and_def)
apply (intro FOL_reflections function_reflections)
done
@@ -511,7 +500,7 @@
theorem is_or_reflection:
"REFLECTS[\<lambda>x. is_or(L,f(x),g(x),h(x)),
\<lambda>i x. is_or(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: is_or_def setclass_simps)
+apply (simp only: is_or_def)
apply (intro FOL_reflections function_reflections)
done
@@ -544,7 +533,7 @@
theorem is_not_reflection:
"REFLECTS[\<lambda>x. is_not(L,f(x),g(x)),
\<lambda>i x. is_not(**Lset(i),f(x),g(x))]"
-apply (simp only: is_not_def setclass_simps)
+apply (simp only: is_not_def)
apply (intro FOL_reflections function_reflections)
done
@@ -555,13 +544,6 @@
is_lambda_reflection Member_reflection Equal_reflection Nand_reflection
Forall_reflection is_and_reflection is_or_reflection is_not_reflection
-lemmas extra_iff_sats =
- Inl_iff_sats Inr_iff_sats Nil_iff_sats Cons_iff_sats quasilist_iff_sats
- hd_iff_sats tl_iff_sats is_bool_of_o_iff_sats is_lambda_iff_sats
- Member_iff_sats Equal_iff_sats Nand_iff_sats Forall_iff_sats
- is_and_iff_sats is_or_iff_sats is_not_iff_sats
-
-
subsection{*Well-Founded Recursion!*}
subsubsection{*The Operator @{term M_is_recfun}*}
@@ -643,14 +625,15 @@
\<lambda>i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]"
shows "REFLECTS[\<lambda>x. M_is_recfun(L, MH(L,x), f(x), g(x), h(x)),
\<lambda>i x. M_is_recfun(**Lset(i), MH(**Lset(i),x), f(x), g(x), h(x))]"
-apply (simp (no_asm_use) only: M_is_recfun_def setclass_simps)
+apply (simp (no_asm_use) only: M_is_recfun_def)
apply (intro FOL_reflections function_reflections
restriction_reflection MH_reflection)
done
subsubsection{*The Operator @{term is_wfrec}*}
-text{*The three arguments of @{term p} are always 2, 1, 0*}
+text{*The three arguments of @{term p} are always 2, 1, 0;
+ @{term p} is enclosed by 5 quantifiers.*}
(* is_wfrec :: "[i=>o, i, [i,i,i]=>o, i, i] => o"
"is_wfrec(M,MH,r,a,z) ==
@@ -704,7 +687,7 @@
\<lambda>i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]"
shows "REFLECTS[\<lambda>x. is_wfrec(L, MH(L,x), f(x), g(x), h(x)),
\<lambda>i x. is_wfrec(**Lset(i), MH(**Lset(i),x), f(x), g(x), h(x))]"
-apply (simp (no_asm_use) only: is_wfrec_def setclass_simps)
+apply (simp (no_asm_use) only: is_wfrec_def)
apply (intro FOL_reflections MH_reflection is_recfun_reflection)
done
@@ -741,7 +724,7 @@
theorem cartprod_reflection:
"REFLECTS[\<lambda>x. cartprod(L,f(x),g(x),h(x)),
\<lambda>i x. cartprod(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: cartprod_def setclass_simps)
+apply (simp only: cartprod_def)
apply (intro FOL_reflections pair_reflection)
done
@@ -780,7 +763,7 @@
theorem sum_reflection:
"REFLECTS[\<lambda>x. is_sum(L,f(x),g(x),h(x)),
\<lambda>i x. is_sum(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: is_sum_def setclass_simps)
+apply (simp only: is_sum_def)
apply (intro FOL_reflections function_reflections cartprod_reflection)
done
@@ -809,7 +792,7 @@
theorem quasinat_reflection:
"REFLECTS[\<lambda>x. is_quasinat(L,f(x)),
\<lambda>i x. is_quasinat(**Lset(i),f(x))]"
-apply (simp only: is_quasinat_def setclass_simps)
+apply (simp only: is_quasinat_def)
apply (intro FOL_reflections function_reflections)
done
@@ -868,7 +851,7 @@
\<lambda>i x. is_b(**Lset(i), h(x), f(x), g(x))]"
shows "REFLECTS[\<lambda>x. is_nat_case(L, f(x), is_b(L,x), g(x), h(x)),
\<lambda>i x. is_nat_case(**Lset(i), f(x), is_b(**Lset(i), x), g(x), h(x))]"
-apply (simp (no_asm_use) only: is_nat_case_def setclass_simps)
+apply (simp (no_asm_use) only: is_nat_case_def)
apply (intro FOL_reflections function_reflections
restriction_reflection is_b_reflection quasinat_reflection)
done
@@ -931,33 +914,92 @@
shows "REFLECTS[\<lambda>x. iterates_MH(L, p(L,x), e(x), f(x), g(x), h(x)),
\<lambda>i x. iterates_MH(**Lset(i), p(**Lset(i),x), e(x), f(x), g(x), h(x))]"
apply (simp (no_asm_use) only: iterates_MH_def)
-txt{*Must be careful: simplifying with @{text setclass_simps} above would
- change @{text "\<exists>gm[**Lset(i)]"} into @{text "\<exists>gm \<in> Lset(i)"}, when
- it would no longer match rule @{text is_nat_case_reflection}. *}
-apply (rule is_nat_case_reflection)
-apply (simp (no_asm_use) only: setclass_simps)
apply (intro FOL_reflections function_reflections is_nat_case_reflection
restriction_reflection p_reflection)
done
+subsubsection{*The Operator @{term is_iterates}*}
+
+text{*The three arguments of @{term p} are always 2, 1, 0;
+ @{term p} is enclosed by 9 (??) quantifiers.*}
+
+(* "is_iterates(M,isF,v,n,Z) ==
+ \<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
+ 1 0 is_wfrec(M, iterates_MH(M,isF,v), msn, n, Z)"*)
+
+constdefs is_iterates_fm :: "[i, i, i, i]=>i"
+ "is_iterates_fm(p,v,n,Z) ==
+ Exists(Exists(
+ And(succ_fm(n#+2,1),
+ And(Memrel_fm(1,0),
+ is_wfrec_fm(iterates_MH_fm(p, v#+7, 2, 1, 0),
+ 0, n#+2, Z#+2)))))"
+
+text{*We call @{term p} with arguments a, f, z by equating them with
+ the corresponding quantified variables with de Bruijn indices 2, 1, 0.*}
+
+
+lemma is_iterates_type [TC]:
+ "[| p \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |]
+ ==> is_iterates_fm(p,x,y,z) \<in> formula"
+by (simp add: is_iterates_fm_def)
+
+lemma sats_is_iterates_fm:
+ assumes is_F_iff_sats:
+ "!!a b c d e f g h i j k.
+ [| a \<in> A; b \<in> A; c \<in> A; d \<in> A; e \<in> A; f \<in> A;
+ g \<in> A; h \<in> A; i \<in> A; j \<in> A; k \<in> A|]
+ ==> is_F(a,b) <->
+ sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d, Cons(e, Cons(f,
+ Cons(g, Cons(h, Cons(i, Cons(j, Cons(k, env))))))))))))"
+ shows
+ "[|x \<in> nat; y < length(env); z < length(env); env \<in> list(A)|]
+ ==> sats(A, is_iterates_fm(p,x,y,z), env) <->
+ is_iterates(**A, is_F, nth(x,env), nth(y,env), nth(z,env))"
+apply (frule_tac x=z in lt_length_in_nat, assumption)
+apply (frule lt_length_in_nat, assumption)
+apply (simp add: is_iterates_fm_def is_iterates_def sats_is_nat_case_fm
+ is_F_iff_sats [symmetric] sats_is_wfrec_fm sats_iterates_MH_fm)
+done
+
+
+lemma is_iterates_iff_sats:
+ assumes is_F_iff_sats:
+ "!!a b c d e f g h i j k.
+ [| a \<in> A; b \<in> A; c \<in> A; d \<in> A; e \<in> A; f \<in> A;
+ g \<in> A; h \<in> A; i \<in> A; j \<in> A; k \<in> A|]
+ ==> is_F(a,b) <->
+ sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d, Cons(e, Cons(f,
+ Cons(g, Cons(h, Cons(i, Cons(j, Cons(k, env))))))))))))"
+ shows
+ "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
+ i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
+ ==> is_iterates(**A, is_F, x, y, z) <->
+ sats(A, is_iterates_fm(p,i,j,k), env)"
+by (simp add: sats_is_iterates_fm [OF is_F_iff_sats])
+
+text{*The second argument of @{term p} gives it direct access to @{term x},
+ which is essential for handling free variable references. Without this
+ argument, we cannot prove reflection for @{term list_N}.*}
+theorem is_iterates_reflection:
+ assumes p_reflection:
+ "!!f g h. REFLECTS[\<lambda>x. p(L, h(x), f(x), g(x)),
+ \<lambda>i x. p(**Lset(i), h(x), f(x), g(x))]"
+ shows "REFLECTS[\<lambda>x. is_iterates(L, p(L,x), f(x), g(x), h(x)),
+ \<lambda>i x. is_iterates(**Lset(i), p(**Lset(i),x), f(x), g(x), h(x))]"
+apply (simp (no_asm_use) only: is_iterates_def)
+apply (intro FOL_reflections function_reflections p_reflection
+ is_wfrec_reflection iterates_MH_reflection)
+done
+
subsubsection{*The Formula @{term is_eclose_n}, Internalized*}
-(* is_eclose_n(M,A,n,Z) ==
- \<exists>sn[M]. \<exists>msn[M].
- 1 0
- successor(M,n,sn) & membership(M,sn,msn) &
- is_wfrec(M, iterates_MH(M, big_union(M), A), msn, n, Z) *)
+(* is_eclose_n(M,A,n,Z) == is_iterates(M, big_union(M), A, n, Z) *)
constdefs eclose_n_fm :: "[i,i,i]=>i"
- "eclose_n_fm(A,n,Z) ==
- Exists(Exists(
- And(succ_fm(n#+2,1),
- And(Memrel_fm(1,0),
- is_wfrec_fm(iterates_MH_fm(big_union_fm(1,0),
- A#+7, 2, 1, 0),
- 0, n#+2, Z#+2)))))"
+ "eclose_n_fm(A,n,Z) == is_iterates_fm(big_union_fm(1,0), A, n, Z)"
lemma eclose_n_fm_type [TC]:
"[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> eclose_n_fm(x,y,z) \<in> formula"
@@ -969,8 +1011,8 @@
is_eclose_n(**A, nth(x,env), nth(y,env), nth(z,env))"
apply (frule_tac x=z in lt_length_in_nat, assumption)
apply (frule_tac x=y in lt_length_in_nat, assumption)
-apply (simp add: eclose_n_fm_def is_eclose_n_def sats_is_wfrec_fm
- sats_iterates_MH_fm)
+apply (simp add: eclose_n_fm_def is_eclose_n_def
+ sats_is_iterates_fm)
done
lemma eclose_n_iff_sats:
@@ -982,9 +1024,8 @@
theorem eclose_n_reflection:
"REFLECTS[\<lambda>x. is_eclose_n(L, f(x), g(x), h(x)),
\<lambda>i x. is_eclose_n(**Lset(i), f(x), g(x), h(x))]"
-apply (simp only: is_eclose_n_def setclass_simps)
-apply (intro FOL_reflections function_reflections is_wfrec_reflection
- iterates_MH_reflection)
+apply (simp only: is_eclose_n_def)
+apply (intro FOL_reflections function_reflections is_iterates_reflection)
done
@@ -1017,7 +1058,7 @@
theorem mem_eclose_reflection:
"REFLECTS[\<lambda>x. mem_eclose(L,f(x),g(x)),
\<lambda>i x. mem_eclose(**Lset(i),f(x),g(x))]"
-apply (simp only: mem_eclose_def setclass_simps)
+apply (simp only: mem_eclose_def)
apply (intro FOL_reflections finite_ordinal_reflection eclose_n_reflection)
done
@@ -1047,7 +1088,7 @@
theorem is_eclose_reflection:
"REFLECTS[\<lambda>x. is_eclose(L,f(x),g(x)),
\<lambda>i x. is_eclose(**Lset(i),f(x),g(x))]"
-apply (simp only: is_eclose_def setclass_simps)
+apply (simp only: is_eclose_def)
apply (intro FOL_reflections mem_eclose_reflection)
done
@@ -1082,7 +1123,7 @@
theorem list_functor_reflection:
"REFLECTS[\<lambda>x. is_list_functor(L,f(x),g(x),h(x)),
\<lambda>i x. is_list_functor(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: is_list_functor_def setclass_simps)
+apply (simp only: is_list_functor_def)
apply (intro FOL_reflections number1_reflection
cartprod_reflection sum_reflection)
done
@@ -1091,20 +1132,14 @@
subsubsection{*The Formula @{term is_list_N}, Internalized*}
(* "is_list_N(M,A,n,Z) ==
- \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M].
- empty(M,zero) &
- successor(M,n,sn) & membership(M,sn,msn) &
- is_wfrec(M, iterates_MH(M, is_list_functor(M,A),zero), msn, n, Z)" *)
-
+ \<exists>zero[M]. empty(M,zero) &
+ is_iterates(M, is_list_functor(M,A), zero, n, Z)" *)
+
constdefs list_N_fm :: "[i,i,i]=>i"
"list_N_fm(A,n,Z) ==
- Exists(Exists(Exists(
- And(empty_fm(2),
- And(succ_fm(n#+3,1),
- And(Memrel_fm(1,0),
- is_wfrec_fm(iterates_MH_fm(list_functor_fm(A#+9#+3,1,0),
- 7,2,1,0),
- 0, n#+3, Z#+3)))))))"
+ Exists(
+ And(empty_fm(0),
+ is_iterates_fm(list_functor_fm(A#+9#+3,1,0), 0, n#+1, Z#+1)))"
lemma list_N_fm_type [TC]:
"[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> list_N_fm(x,y,z) \<in> formula"
@@ -1116,8 +1151,7 @@
is_list_N(**A, nth(x,env), nth(y,env), nth(z,env))"
apply (frule_tac x=z in lt_length_in_nat, assumption)
apply (frule_tac x=y in lt_length_in_nat, assumption)
-apply (simp add: list_N_fm_def is_list_N_def sats_is_wfrec_fm
- sats_iterates_MH_fm)
+apply (simp add: list_N_fm_def is_list_N_def sats_is_iterates_fm)
done
lemma list_N_iff_sats:
@@ -1129,9 +1163,9 @@
theorem list_N_reflection:
"REFLECTS[\<lambda>x. is_list_N(L, f(x), g(x), h(x)),
\<lambda>i x. is_list_N(**Lset(i), f(x), g(x), h(x))]"
-apply (simp only: is_list_N_def setclass_simps)
-apply (intro FOL_reflections function_reflections is_wfrec_reflection
- iterates_MH_reflection list_functor_reflection)
+apply (simp only: is_list_N_def)
+apply (intro FOL_reflections function_reflections
+ is_iterates_reflection list_functor_reflection)
done
@@ -1165,7 +1199,7 @@
theorem mem_list_reflection:
"REFLECTS[\<lambda>x. mem_list(L,f(x),g(x)),
\<lambda>i x. mem_list(**Lset(i),f(x),g(x))]"
-apply (simp only: mem_list_def setclass_simps)
+apply (simp only: mem_list_def)
apply (intro FOL_reflections finite_ordinal_reflection list_N_reflection)
done
@@ -1195,7 +1229,7 @@
theorem is_list_reflection:
"REFLECTS[\<lambda>x. is_list(L,f(x),g(x)),
\<lambda>i x. is_list(**Lset(i),f(x),g(x))]"
-apply (simp only: is_list_def setclass_simps)
+apply (simp only: is_list_def)
apply (intro FOL_reflections mem_list_reflection)
done
@@ -1237,7 +1271,7 @@
theorem formula_functor_reflection:
"REFLECTS[\<lambda>x. is_formula_functor(L,f(x),g(x)),
\<lambda>i x. is_formula_functor(**Lset(i),f(x),g(x))]"
-apply (simp only: is_formula_functor_def setclass_simps)
+apply (simp only: is_formula_functor_def)
apply (intro FOL_reflections omega_reflection
cartprod_reflection sum_reflection)
done
@@ -1245,20 +1279,14 @@
subsubsection{*The Formula @{term is_formula_N}, Internalized*}
-(* "is_formula_N(M,n,Z) ==
- \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M].
- 2 1 0
- empty(M,zero) &
- successor(M,n,sn) & membership(M,sn,msn) &
- is_wfrec(M, iterates_MH(M, is_formula_functor(M),zero), msn, n, Z)" *)
+(* "is_formula_N(M,n,Z) ==
+ \<exists>zero[M]. empty(M,zero) &
+ is_iterates(M, is_formula_functor(M), zero, n, Z)" *)
constdefs formula_N_fm :: "[i,i]=>i"
"formula_N_fm(n,Z) ==
- Exists(Exists(Exists(
- And(empty_fm(2),
- And(succ_fm(n#+3,1),
- And(Memrel_fm(1,0),
- is_wfrec_fm(iterates_MH_fm(formula_functor_fm(1,0),7,2,1,0),
- 0, n#+3, Z#+3)))))))"
+ Exists(
+ And(empty_fm(0),
+ is_iterates_fm(formula_functor_fm(1,0), 0, n#+1, Z#+1)))"
lemma formula_N_fm_type [TC]:
"[| x \<in> nat; y \<in> nat |] ==> formula_N_fm(x,y) \<in> formula"
@@ -1270,7 +1298,7 @@
is_formula_N(**A, nth(x,env), nth(y,env))"
apply (frule_tac x=y in lt_length_in_nat, assumption)
apply (frule lt_length_in_nat, assumption)
-apply (simp add: formula_N_fm_def is_formula_N_def sats_is_wfrec_fm sats_iterates_MH_fm)
+apply (simp add: formula_N_fm_def is_formula_N_def sats_is_iterates_fm)
done
lemma formula_N_iff_sats:
@@ -1282,9 +1310,9 @@
theorem formula_N_reflection:
"REFLECTS[\<lambda>x. is_formula_N(L, f(x), g(x)),
\<lambda>i x. is_formula_N(**Lset(i), f(x), g(x))]"
-apply (simp only: is_formula_N_def setclass_simps)
-apply (intro FOL_reflections function_reflections is_wfrec_reflection
- iterates_MH_reflection formula_functor_reflection)
+apply (simp only: is_formula_N_def)
+apply (intro FOL_reflections function_reflections
+ is_iterates_reflection formula_functor_reflection)
done
@@ -1317,7 +1345,7 @@
theorem mem_formula_reflection:
"REFLECTS[\<lambda>x. mem_formula(L,f(x)),
\<lambda>i x. mem_formula(**Lset(i),f(x))]"
-apply (simp only: mem_formula_def setclass_simps)
+apply (simp only: mem_formula_def)
apply (intro FOL_reflections finite_ordinal_reflection formula_N_reflection)
done
@@ -1346,7 +1374,7 @@
theorem is_formula_reflection:
"REFLECTS[\<lambda>x. is_formula(L,f(x)),
\<lambda>i x. is_formula(**Lset(i),f(x))]"
-apply (simp only: is_formula_def setclass_simps)
+apply (simp only: is_formula_def)
apply (intro FOL_reflections mem_formula_reflection)
done
@@ -1413,7 +1441,7 @@
\<lambda>i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]"
shows "REFLECTS[\<lambda>x. is_transrec(L, MH(L,x), f(x), h(x)),
\<lambda>i x. is_transrec(**Lset(i), MH(**Lset(i),x), f(x), h(x))]"
-apply (simp (no_asm_use) only: is_transrec_def setclass_simps)
+apply (simp (no_asm_use) only: is_transrec_def)
apply (intro FOL_reflections function_reflections MH_reflection
is_wfrec_reflection is_eclose_reflection)
done
--- a/src/ZF/Constructible/L_axioms.thy Fri Oct 18 09:53:18 2002 +0200
+++ b/src/ZF/Constructible/L_axioms.thy Fri Oct 18 17:50:13 2002 +0200
@@ -337,8 +337,6 @@
subsection{*Internalized Formulas for some Set-Theoretic Concepts*}
-lemmas setclass_simps = rall_setclass_is_ball rex_setclass_is_bex
-
subsubsection{*Some numbers to help write de Bruijn indices*}
syntax
@@ -383,7 +381,7 @@
theorem empty_reflection:
"REFLECTS[\<lambda>x. empty(L,f(x)),
\<lambda>i x. empty(**Lset(i),f(x))]"
-apply (simp only: empty_def setclass_simps)
+apply (simp only: empty_def)
apply (intro FOL_reflections)
done
@@ -467,7 +465,7 @@
theorem pair_reflection:
"REFLECTS[\<lambda>x. pair(L,f(x),g(x),h(x)),
\<lambda>i x. pair(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: pair_def setclass_simps)
+apply (simp only: pair_def)
apply (intro FOL_reflections upair_reflection)
done
@@ -498,7 +496,7 @@
theorem union_reflection:
"REFLECTS[\<lambda>x. union(L,f(x),g(x),h(x)),
\<lambda>i x. union(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: union_def setclass_simps)
+apply (simp only: union_def)
apply (intro FOL_reflections)
done
@@ -530,7 +528,7 @@
theorem cons_reflection:
"REFLECTS[\<lambda>x. is_cons(L,f(x),g(x),h(x)),
\<lambda>i x. is_cons(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: is_cons_def setclass_simps)
+apply (simp only: is_cons_def)
apply (intro FOL_reflections upair_reflection union_reflection)
done
@@ -559,7 +557,7 @@
theorem successor_reflection:
"REFLECTS[\<lambda>x. successor(L,f(x),g(x)),
\<lambda>i x. successor(**Lset(i),f(x),g(x))]"
-apply (simp only: successor_def setclass_simps)
+apply (simp only: successor_def)
apply (intro cons_reflection)
done
@@ -588,7 +586,7 @@
theorem number1_reflection:
"REFLECTS[\<lambda>x. number1(L,f(x)),
\<lambda>i x. number1(**Lset(i),f(x))]"
-apply (simp only: number1_def setclass_simps)
+apply (simp only: number1_def)
apply (intro FOL_reflections empty_reflection successor_reflection)
done
@@ -620,7 +618,7 @@
theorem big_union_reflection:
"REFLECTS[\<lambda>x. big_union(L,f(x),g(x)),
\<lambda>i x. big_union(**Lset(i),f(x),g(x))]"
-apply (simp only: big_union_def setclass_simps)
+apply (simp only: big_union_def)
apply (intro FOL_reflections)
done
@@ -641,7 +639,7 @@
theorem subset_reflection:
"REFLECTS[\<lambda>x. subset(L,f(x),g(x)),
\<lambda>i x. subset(**Lset(i),f(x),g(x))]"
-apply (simp only: Relative.subset_def setclass_simps)
+apply (simp only: Relative.subset_def)
apply (intro FOL_reflections)
done
@@ -653,7 +651,7 @@
theorem transitive_set_reflection:
"REFLECTS[\<lambda>x. transitive_set(L,f(x)),
\<lambda>i x. transitive_set(**Lset(i),f(x))]"
-apply (simp only: transitive_set_def setclass_simps)
+apply (simp only: transitive_set_def)
apply (intro FOL_reflections subset_reflection)
done
@@ -669,7 +667,7 @@
theorem ordinal_reflection:
"REFLECTS[\<lambda>x. ordinal(L,f(x)), \<lambda>i x. ordinal(**Lset(i),f(x))]"
-apply (simp only: ordinal_def setclass_simps)
+apply (simp only: ordinal_def)
apply (intro FOL_reflections transitive_set_reflection)
done
@@ -703,7 +701,7 @@
theorem membership_reflection:
"REFLECTS[\<lambda>x. membership(L,f(x),g(x)),
\<lambda>i x. membership(**Lset(i),f(x),g(x))]"
-apply (simp only: membership_def setclass_simps)
+apply (simp only: membership_def)
apply (intro FOL_reflections pair_reflection)
done
@@ -737,7 +735,7 @@
theorem pred_set_reflection:
"REFLECTS[\<lambda>x. pred_set(L,f(x),g(x),h(x),b(x)),
\<lambda>i x. pred_set(**Lset(i),f(x),g(x),h(x),b(x))]"
-apply (simp only: pred_set_def setclass_simps)
+apply (simp only: pred_set_def)
apply (intro FOL_reflections pair_reflection)
done
@@ -772,7 +770,7 @@
theorem domain_reflection:
"REFLECTS[\<lambda>x. is_domain(L,f(x),g(x)),
\<lambda>i x. is_domain(**Lset(i),f(x),g(x))]"
-apply (simp only: is_domain_def setclass_simps)
+apply (simp only: is_domain_def)
apply (intro FOL_reflections pair_reflection)
done
@@ -806,7 +804,7 @@
theorem range_reflection:
"REFLECTS[\<lambda>x. is_range(L,f(x),g(x)),
\<lambda>i x. is_range(**Lset(i),f(x),g(x))]"
-apply (simp only: is_range_def setclass_simps)
+apply (simp only: is_range_def)
apply (intro FOL_reflections pair_reflection)
done
@@ -841,7 +839,7 @@
theorem field_reflection:
"REFLECTS[\<lambda>x. is_field(L,f(x),g(x)),
\<lambda>i x. is_field(**Lset(i),f(x),g(x))]"
-apply (simp only: is_field_def setclass_simps)
+apply (simp only: is_field_def)
apply (intro FOL_reflections domain_reflection range_reflection
union_reflection)
done
@@ -877,7 +875,7 @@
theorem image_reflection:
"REFLECTS[\<lambda>x. image(L,f(x),g(x),h(x)),
\<lambda>i x. image(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: Relative.image_def setclass_simps)
+apply (simp only: Relative.image_def)
apply (intro FOL_reflections pair_reflection)
done
@@ -912,7 +910,7 @@
theorem pre_image_reflection:
"REFLECTS[\<lambda>x. pre_image(L,f(x),g(x),h(x)),
\<lambda>i x. pre_image(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: Relative.pre_image_def setclass_simps)
+apply (simp only: Relative.pre_image_def)
apply (intro FOL_reflections pair_reflection)
done
@@ -947,7 +945,7 @@
theorem fun_apply_reflection:
"REFLECTS[\<lambda>x. fun_apply(L,f(x),g(x),h(x)),
\<lambda>i x. fun_apply(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: fun_apply_def setclass_simps)
+apply (simp only: fun_apply_def)
apply (intro FOL_reflections upair_reflection image_reflection
big_union_reflection)
done
@@ -979,7 +977,7 @@
theorem is_relation_reflection:
"REFLECTS[\<lambda>x. is_relation(L,f(x)),
\<lambda>i x. is_relation(**Lset(i),f(x))]"
-apply (simp only: is_relation_def setclass_simps)
+apply (simp only: is_relation_def)
apply (intro FOL_reflections pair_reflection)
done
@@ -1015,7 +1013,7 @@
theorem is_function_reflection:
"REFLECTS[\<lambda>x. is_function(L,f(x)),
\<lambda>i x. is_function(**Lset(i),f(x))]"
-apply (simp only: is_function_def setclass_simps)
+apply (simp only: is_function_def)
apply (intro FOL_reflections pair_reflection)
done
@@ -1073,7 +1071,7 @@
theorem typed_function_reflection:
"REFLECTS[\<lambda>x. typed_function(L,f(x),g(x),h(x)),
\<lambda>i x. typed_function(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: typed_function_def setclass_simps)
+apply (simp only: typed_function_def)
apply (intro FOL_reflections function_reflections)
done
@@ -1113,7 +1111,7 @@
theorem composition_reflection:
"REFLECTS[\<lambda>x. composition(L,f(x),g(x),h(x)),
\<lambda>i x. composition(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: composition_def setclass_simps)
+apply (simp only: composition_def)
apply (intro FOL_reflections pair_reflection)
done
@@ -1153,7 +1151,7 @@
theorem injection_reflection:
"REFLECTS[\<lambda>x. injection(L,f(x),g(x),h(x)),
\<lambda>i x. injection(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: injection_def setclass_simps)
+apply (simp only: injection_def)
apply (intro FOL_reflections function_reflections typed_function_reflection)
done
@@ -1190,7 +1188,7 @@
theorem surjection_reflection:
"REFLECTS[\<lambda>x. surjection(L,f(x),g(x),h(x)),
\<lambda>i x. surjection(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: surjection_def setclass_simps)
+apply (simp only: surjection_def)
apply (intro FOL_reflections function_reflections typed_function_reflection)
done
@@ -1222,7 +1220,7 @@
theorem bijection_reflection:
"REFLECTS[\<lambda>x. bijection(L,f(x),g(x),h(x)),
\<lambda>i x. bijection(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: bijection_def setclass_simps)
+apply (simp only: bijection_def)
apply (intro And_reflection injection_reflection surjection_reflection)
done
@@ -1258,7 +1256,7 @@
theorem restriction_reflection:
"REFLECTS[\<lambda>x. restriction(L,f(x),g(x),h(x)),
\<lambda>i x. restriction(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: restriction_def setclass_simps)
+apply (simp only: restriction_def)
apply (intro FOL_reflections pair_reflection)
done
@@ -1308,7 +1306,7 @@
theorem order_isomorphism_reflection:
"REFLECTS[\<lambda>x. order_isomorphism(L,f(x),g(x),h(x),g'(x),h'(x)),
\<lambda>i x. order_isomorphism(**Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
-apply (simp only: order_isomorphism_def setclass_simps)
+apply (simp only: order_isomorphism_def)
apply (intro FOL_reflections function_reflections bijection_reflection)
done
@@ -1346,7 +1344,7 @@
theorem limit_ordinal_reflection:
"REFLECTS[\<lambda>x. limit_ordinal(L,f(x)),
\<lambda>i x. limit_ordinal(**Lset(i),f(x))]"
-apply (simp only: limit_ordinal_def setclass_simps)
+apply (simp only: limit_ordinal_def)
apply (intro FOL_reflections ordinal_reflection
empty_reflection successor_reflection)
done
@@ -1381,7 +1379,7 @@
theorem finite_ordinal_reflection:
"REFLECTS[\<lambda>x. finite_ordinal(L,f(x)),
\<lambda>i x. finite_ordinal(**Lset(i),f(x))]"
-apply (simp only: finite_ordinal_def setclass_simps)
+apply (simp only: finite_ordinal_def)
apply (intro FOL_reflections ordinal_reflection limit_ordinal_reflection)
done
@@ -1413,7 +1411,7 @@
theorem omega_reflection:
"REFLECTS[\<lambda>x. omega(L,f(x)),
\<lambda>i x. omega(**Lset(i),f(x))]"
-apply (simp only: omega_def setclass_simps)
+apply (simp only: omega_def)
apply (intro FOL_reflections limit_ordinal_reflection)
done
--- a/src/ZF/Constructible/Rec_Separation.thy Fri Oct 18 09:53:18 2002 +0200
+++ b/src/ZF/Constructible/Rec_Separation.thy Fri Oct 18 17:50:13 2002 +0200
@@ -68,7 +68,7 @@
lemma rtran_closure_mem_reflection:
"REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)),
\<lambda>i x. rtran_closure_mem(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: rtran_closure_mem_def setclass_simps)
+apply (simp only: rtran_closure_mem_def)
apply (intro FOL_reflections function_reflections fun_plus_reflections)
done
@@ -113,7 +113,7 @@
theorem rtran_closure_reflection:
"REFLECTS[\<lambda>x. rtran_closure(L,f(x),g(x)),
\<lambda>i x. rtran_closure(**Lset(i),f(x),g(x))]"
-apply (simp only: rtran_closure_def setclass_simps)
+apply (simp only: rtran_closure_def)
apply (intro FOL_reflections function_reflections rtran_closure_mem_reflection)
done
@@ -145,7 +145,7 @@
theorem tran_closure_reflection:
"REFLECTS[\<lambda>x. tran_closure(L,f(x),g(x)),
\<lambda>i x. tran_closure(**Lset(i),f(x),g(x))]"
-apply (simp only: tran_closure_def setclass_simps)
+apply (simp only: tran_closure_def)
apply (intro FOL_reflections function_reflections
rtran_closure_reflection composition_reflection)
done
@@ -229,26 +229,16 @@
lemma list_replacement2_Reflects:
"REFLECTS
- [\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and>
- (\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and>
- is_wfrec (L, iterates_MH (L, is_list_functor(L, A), 0),
- msn, u, x)),
- \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and>
- (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i).
- successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and>
- is_wfrec (**Lset(i),
- iterates_MH (**Lset(i), is_list_functor(**Lset(i), A), 0),
- msn, u, x))]"
-by (intro FOL_reflections function_reflections is_wfrec_reflection
- iterates_MH_reflection list_functor_reflection)
-
+ [\<lambda>x. \<exists>u[L]. u \<in> B & u \<in> nat &
+ is_iterates(L, is_list_functor(L, A), 0, u, x),
+ \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & u \<in> nat &
+ is_iterates(**Lset(i), is_list_functor(**Lset(i), A), 0, u, x)]"
+by (intro FOL_reflections
+ is_iterates_reflection list_functor_reflection)
lemma list_replacement2:
"L(A) ==> strong_replacement(L,
- \<lambda>n y. n\<in>nat &
- (\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) &
- is_wfrec(L, iterates_MH(L,is_list_functor(L,A), 0),
- msn, n, y)))"
+ \<lambda>n y. n\<in>nat & is_iterates(L, is_list_functor(L,A), 0, n, y))"
apply (rule strong_replacementI)
apply (rename_tac B)
apply (rule_tac u="{A,B,0,nat}"
@@ -258,8 +248,7 @@
apply (rule DPow_LsetI)
apply (rule bex_iff_sats conj_iff_sats)+
apply (rule_tac env = "[u,x,A,B,0,nat]" in mem_iff_sats)
-apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats
- is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
+apply (rule sep_rules list_functor_iff_sats is_iterates_iff_sats | simp)+
done
@@ -267,11 +256,13 @@
subsubsection{*Instances of Replacement for Formulas*}
+(*FIXME: could prove a lemma iterates_replacementI to eliminate the
+need to expand iterates_replacement and wfrec_replacement*)
lemma formula_replacement1_Reflects:
"REFLECTS
- [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
+ [\<lambda>x. \<exists>u[L]. u \<in> B & (\<exists>y[L]. pair(L,u,y,x) &
is_wfrec(L, iterates_MH(L, is_formula_functor(L), 0), memsn, u, y)),
- \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
+ \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) &
is_wfrec(**Lset(i),
iterates_MH(**Lset(i),
is_formula_functor(**Lset(i)), 0), memsn, u, y))]"
@@ -296,26 +287,16 @@
lemma formula_replacement2_Reflects:
"REFLECTS
- [\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and>
- (\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and>
- is_wfrec (L, iterates_MH (L, is_formula_functor(L), 0),
- msn, u, x)),
- \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and>
- (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i).
- successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and>
- is_wfrec (**Lset(i),
- iterates_MH (**Lset(i), is_formula_functor(**Lset(i)), 0),
- msn, u, x))]"
-by (intro FOL_reflections function_reflections is_wfrec_reflection
- iterates_MH_reflection formula_functor_reflection)
-
+ [\<lambda>x. \<exists>u[L]. u \<in> B & u \<in> nat &
+ is_iterates(L, is_formula_functor(L), 0, u, x),
+ \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & u \<in> nat &
+ is_iterates(**Lset(i), is_formula_functor(**Lset(i)), 0, u, x)]"
+by (intro FOL_reflections
+ is_iterates_reflection formula_functor_reflection)
lemma formula_replacement2:
"strong_replacement(L,
- \<lambda>n y. n\<in>nat &
- (\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) &
- is_wfrec(L, iterates_MH(L,is_formula_functor(L), 0),
- msn, n, y)))"
+ \<lambda>n y. n\<in>nat & is_iterates(L, is_formula_functor(L), 0, n, y))"
apply (rule strong_replacementI)
apply (rename_tac B)
apply (rule_tac u="{B,0,nat}"
@@ -325,8 +306,7 @@
apply (rule DPow_LsetI)
apply (rule bex_iff_sats conj_iff_sats)+
apply (rule_tac env = "[u,x,B,0,nat]" in mem_iff_sats)
-apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats
- is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
+apply (rule sep_rules formula_functor_iff_sats is_iterates_iff_sats | simp)+
done
text{*NB The proofs for type @{term formula} are virtually identical to those
@@ -335,18 +315,12 @@
subsubsection{*The Formula @{term is_nth}, Internalized*}
-(* "is_nth(M,n,l,Z) ==
- \<exists>X[M]. \<exists>sn[M]. \<exists>msn[M].
- 2 1 0
- successor(M,n,sn) & membership(M,sn,msn) &
- is_wfrec(M, iterates_MH(M, is_tl(M), l), msn, n, X) &
- is_hd(M,X,Z)" *)
+(* "is_nth(M,n,l,Z) ==
+ \<exists>X[M]. is_iterates(M, is_tl(M), l, n, X) & is_hd(M,X,Z)" *)
constdefs nth_fm :: "[i,i,i]=>i"
"nth_fm(n,l,Z) ==
- Exists(Exists(Exists(
- And(succ_fm(n#+3,1),
- And(Memrel_fm(1,0),
- And(is_wfrec_fm(iterates_MH_fm(tl_fm(1,0),l#+8,2,1,0), 0, n#+3, 2), hd_fm(2,Z#+3)))))))"
+ Exists(And(is_iterates_fm(tl_fm(1,0), succ(l), succ(n), 0),
+ hd_fm(0,succ(Z))))"
lemma nth_fm_type [TC]:
"[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> nth_fm(x,y,z) \<in> formula"
@@ -357,7 +331,7 @@
==> sats(A, nth_fm(x,y,z), env) <->
is_nth(**A, nth(x,env), nth(y,env), nth(z,env))"
apply (frule lt_length_in_nat, assumption)
-apply (simp add: nth_fm_def is_nth_def sats_is_wfrec_fm sats_iterates_MH_fm)
+apply (simp add: nth_fm_def is_nth_def sats_is_iterates_fm)
done
lemma nth_iff_sats:
@@ -369,27 +343,29 @@
theorem nth_reflection:
"REFLECTS[\<lambda>x. is_nth(L, f(x), g(x), h(x)),
\<lambda>i x. is_nth(**Lset(i), f(x), g(x), h(x))]"
-apply (simp only: is_nth_def setclass_simps)
-apply (intro FOL_reflections function_reflections is_wfrec_reflection
- iterates_MH_reflection hd_reflection tl_reflection)
+apply (simp only: is_nth_def)
+apply (intro FOL_reflections is_iterates_reflection
+ hd_reflection tl_reflection)
done
subsubsection{*An Instance of Replacement for @{term nth}*}
+(*FIXME: could prove a lemma iterates_replacementI to eliminate the
+need to expand iterates_replacement and wfrec_replacement*)
lemma nth_replacement_Reflects:
"REFLECTS
- [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
+ [\<lambda>x. \<exists>u[L]. u \<in> B & (\<exists>y[L]. pair(L,u,y,x) &
is_wfrec(L, iterates_MH(L, is_tl(L), z), memsn, u, y)),
- \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
+ \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) &
is_wfrec(**Lset(i),
iterates_MH(**Lset(i),
is_tl(**Lset(i)), z), memsn, u, y))]"
by (intro FOL_reflections function_reflections is_wfrec_reflection
- iterates_MH_reflection list_functor_reflection tl_reflection)
+ iterates_MH_reflection tl_reflection)
lemma nth_replacement:
- "L(w) ==> iterates_replacement(L, %l t. is_tl(L,l,t), w)"
+ "L(w) ==> iterates_replacement(L, is_tl(L), w)"
apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
apply (rule strong_replacementI)
apply (rule_tac u="{A,n,w,Memrel(succ(n))}"
@@ -439,9 +415,9 @@
lemma eclose_replacement1_Reflects:
"REFLECTS
- [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
+ [\<lambda>x. \<exists>u[L]. u \<in> B & (\<exists>y[L]. pair(L,u,y,x) &
is_wfrec(L, iterates_MH(L, big_union(L), A), memsn, u, y)),
- \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
+ \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) &
is_wfrec(**Lset(i),
iterates_MH(**Lset(i), big_union(**Lset(i)), A),
memsn, u, y))]"
@@ -466,26 +442,15 @@
lemma eclose_replacement2_Reflects:
"REFLECTS
- [\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and>
- (\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and>
- is_wfrec (L, iterates_MH (L, big_union(L), A),
- msn, u, x)),
- \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and>
- (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i).
- successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and>
- is_wfrec (**Lset(i),
- iterates_MH (**Lset(i), big_union(**Lset(i)), A),
- msn, u, x))]"
-by (intro FOL_reflections function_reflections is_wfrec_reflection
- iterates_MH_reflection)
-
+ [\<lambda>x. \<exists>u[L]. u \<in> B & u \<in> nat &
+ is_iterates(L, big_union(L), A, u, x),
+ \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & u \<in> nat &
+ is_iterates(**Lset(i), big_union(**Lset(i)), A, u, x)]"
+by (intro FOL_reflections function_reflections is_iterates_reflection)
lemma eclose_replacement2:
"L(A) ==> strong_replacement(L,
- \<lambda>n y. n\<in>nat &
- (\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) &
- is_wfrec(L, iterates_MH(L,big_union(L), A),
- msn, n, y)))"
+ \<lambda>n y. n\<in>nat & is_iterates(L, big_union(L), A, n, y))"
apply (rule strong_replacementI)
apply (rename_tac B)
apply (rule_tac u="{A,B,nat}"
@@ -494,8 +459,7 @@
apply (rule DPow_LsetI)
apply (rule bex_iff_sats conj_iff_sats)+
apply (rule_tac env = "[u,x,A,B,nat]" in mem_iff_sats)
-apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats
- is_wfrec_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+
+apply (rule sep_rules is_iterates_iff_sats big_union_iff_sats | simp)+
done
--- a/src/ZF/Constructible/Satisfies_absolute.thy Fri Oct 18 09:53:18 2002 +0200
+++ b/src/ZF/Constructible/Satisfies_absolute.thy Fri Oct 18 17:50:13 2002 +0200
@@ -45,7 +45,7 @@
theorem depth_reflection:
"REFLECTS[\<lambda>x. is_depth(L, f(x), g(x)),
\<lambda>i x. is_depth(**Lset(i), f(x), g(x))]"
-apply (simp only: is_depth_def setclass_simps)
+apply (simp only: is_depth_def)
apply (intro FOL_reflections function_reflections formula_N_reflection)
done
@@ -161,7 +161,7 @@
\<lambda>i x. is_d(**Lset(i), h(x), f(x), g(x))]"
shows "REFLECTS[\<lambda>x. is_formula_case(L, is_a(L,x), is_b(L,x), is_c(L,x), is_d(L,x), g(x), h(x)),
\<lambda>i x. is_formula_case(**Lset(i), is_a(**Lset(i), x), is_b(**Lset(i), x), is_c(**Lset(i), x), is_d(**Lset(i), x), g(x), h(x))]"
-apply (simp (no_asm_use) only: is_formula_case_def setclass_simps)
+apply (simp (no_asm_use) only: is_formula_case_def)
apply (intro FOL_reflections function_reflections finite_ordinal_reflection
mem_formula_reflection
Member_reflection Equal_reflection Nand_reflection Forall_reflection
@@ -530,7 +530,7 @@
lemma depth_apply_reflection:
"REFLECTS[\<lambda>x. is_depth_apply(L,f(x),g(x),h(x)),
\<lambda>i x. is_depth_apply(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: is_depth_apply_def setclass_simps)
+apply (simp only: is_depth_apply_def)
apply (intro FOL_reflections function_reflections depth_reflection
finite_ordinal_reflection)
done