--- a/src/ZF/Constructible/Datatype_absolute.thy Mon Oct 14 10:44:32 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy Mon Oct 14 11:32:00 2002 +0200
@@ -425,7 +425,7 @@
done
-
+text{*This result and the next are unused.*}
lemma formula_N_mono [rule_format]:
"[| m \<in> nat; n \<in> nat |] ==> m\<le>n --> formula_N(m) \<subseteq> formula_N(n)"
apply (rule_tac m = m and n = n in diff_induct)
@@ -577,8 +577,6 @@
done
-subsection{*Absoluteness for Some List Operators*}
-
subsection{*Absoluteness for @{text \<epsilon>}-Closure: the @{term eclose} Operator*}
text{*Re-expresses eclose using "iterates"*}
@@ -705,8 +703,9 @@
subsection{*Absoluteness for the List Operator @{term length}*}
+text{*But it is never used.*}
+
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].
@@ -729,7 +728,7 @@
by (simp add: nat_into_M)
-subsection {*Absoluteness for @{term nth}*}
+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))"
@@ -828,8 +827,67 @@
by (simp add: Forall_def)
+
subsection {*Absoluteness for @{term formula_rec}*}
+constdefs
+
+ 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,
+ \<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))"
+
+text{*Unfold @{term formula_rec} to @{term formula_rec_case}.
+ Express @{term formula_rec} without using @{term rank} or @{term Vset},
+neither of which is absolute.*}
+lemma (in M_trivial) formula_rec_eq:
+ "p \<in> formula ==>
+ 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)
+ txt{*Base case for @{term Equal}*}
+ apply (subst transrec, simp add: formula.intros)
+ txt{*Inductive step for @{term Nand}*}
+ 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)
+done
+
+
+subsubsection{*Absoluteness for the Formula Operator @{term depth}*}
+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_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"
+
+
+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)
+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)
+done
+
+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)
+
+
subsubsection{*@{term is_formula_case}: relativization of @{term formula_case}*}
constdefs
@@ -866,73 +924,17 @@
by (erule formula.cases, simp_all)
-subsection{*Absoluteness for the Formula Operator @{term depth}*}
-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_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"
-
-
-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)
-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)
-done
-
-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)
-
-
-subsection {*Absoluteness for @{term formula_rec}*}
+subsubsection {*Absoluteness for @{term formula_rec}: Final Results*}
constdefs
-
- 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,
- \<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))"
-
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)"
-text{*Unfold @{term formula_rec} to @{term formula_rec_case}.
- Express @{term formula_rec} without using @{term rank} or @{term Vset},
-neither of which is absolute.*}
-lemma (in M_trivial) formula_rec_eq:
- "p \<in> formula ==>
- 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)
- txt{*Base case for @{term Equal}*}
- apply (subst transrec, simp add: formula.intros)
- txt{*Inductive step for @{term Nand}*}
- 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)
-done
-
-text{*Sufficient conditions to relative the instance of @{term formula_case}
+text{*Sufficient conditions to relativize the instance of @{term formula_case}
in @{term formula_rec}*}
lemma (in M_datatypes) Relation1_formula_rec_case:
"[|Relation2(M, nat, nat, is_a, a);
--- a/src/ZF/Constructible/Formula.thy Mon Oct 14 10:44:32 2002 +0200
+++ b/src/ZF/Constructible/Formula.thy Mon Oct 14 11:32:00 2002 +0200
@@ -188,6 +188,63 @@
disj_iff_sats imp_iff_sats iff_iff_sats imp_iff_sats ball_iff_sats
bex_iff_sats
+
+subsection{*Arity of a Formula: Maximum Free de Bruijn Index*}
+
+consts arity :: "i=>i"
+primrec
+ "arity(Member(x,y)) = succ(x) \<union> succ(y)"
+
+ "arity(Equal(x,y)) = succ(x) \<union> succ(y)"
+
+ "arity(Nand(p,q)) = arity(p) \<union> arity(q)"
+
+ "arity(Forall(p)) = Arith.pred(arity(p))"
+
+
+lemma arity_type [TC]: "p \<in> formula ==> arity(p) \<in> nat"
+by (induct_tac p, simp_all)
+
+lemma arity_Neg [simp]: "arity(Neg(p)) = arity(p)"
+by (simp add: Neg_def)
+
+lemma arity_And [simp]: "arity(And(p,q)) = arity(p) \<union> arity(q)"
+by (simp add: And_def)
+
+lemma arity_Or [simp]: "arity(Or(p,q)) = arity(p) \<union> arity(q)"
+by (simp add: Or_def)
+
+lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \<union> arity(q)"
+by (simp add: Implies_def)
+
+lemma arity_Iff [simp]: "arity(Iff(p,q)) = arity(p) \<union> arity(q)"
+by (simp add: Iff_def, blast)
+
+lemma arity_Exists [simp]: "arity(Exists(p)) = Arith.pred(arity(p))"
+by (simp add: Exists_def)
+
+
+lemma arity_sats_iff [rule_format]:
+ "[| p \<in> formula; extra \<in> list(A) |]
+ ==> \<forall>env \<in> list(A).
+ arity(p) \<le> length(env) -->
+ sats(A, p, env @ extra) <-> sats(A, p, env)"
+apply (induct_tac p)
+apply (simp_all add: Arith.pred_def nth_append Un_least_lt_iff nat_imp_quasinat
+ split: split_nat_case, auto)
+done
+
+lemma arity_sats1_iff:
+ "[| arity(p) \<le> succ(length(env)); p \<in> formula; x \<in> A; env \<in> list(A);
+ extra \<in> list(A) |]
+ ==> sats(A, p, Cons(x, env @ extra)) <-> sats(A, p, Cons(x, env))"
+apply (insert arity_sats_iff [of p extra A "Cons(x,env)"])
+apply simp
+done
+
+
+subsection{*Renaming Some de Bruijn Variables*}
+
constdefs incr_var :: "[i,i]=>i"
"incr_var(x,lev) == if x<lev then x else succ(x)"
@@ -214,22 +271,15 @@
(\<lambda>lev \<in> nat. Forall (incr_bv(p) ` succ(lev)))"
-constdefs incr_boundvars :: "i => i"
- "incr_boundvars(p) == incr_bv(p)`0"
-
-
lemma [TC]: "x \<in> nat ==> incr_var(x,lev) \<in> nat"
by (simp add: incr_var_def)
lemma incr_bv_type [TC]: "p \<in> formula ==> incr_bv(p) \<in> nat -> formula"
by (induct_tac p, simp_all)
-lemma incr_boundvars_type [TC]: "p \<in> formula ==> incr_boundvars(p) \<in> formula"
-by (simp add: incr_boundvars_def)
-
-(*Obviously DPow is closed under complements and finite intersections and
-unions. Needs an inductive lemma to allow two lists of parameters to
-be combined.*)
+text{*Obviously, @{term DPow} is closed under complements and finite
+intersections and unions. Needs an inductive lemma to allow two lists of
+parameters to be combined.*}
lemma sats_incr_bv_iff [rule_format]:
"[| p \<in> formula; env \<in> list(A); x \<in> A |]
@@ -241,76 +291,6 @@
apply (auto simp add: diff_succ not_lt_iff_le)
done
-(*UNUSED*)
-lemma sats_incr_boundvars_iff:
- "[| p \<in> formula; env \<in> list(A); x \<in> A |]
- ==> sats(A, incr_boundvars(p), Cons(x,env)) <-> sats(A, p, env)"
-apply (insert sats_incr_bv_iff [of p env A x Nil])
-apply (simp add: incr_boundvars_def)
-done
-
-(*UNUSED
-lemma formula_add_params [rule_format]:
- "[| p \<in> formula; n \<in> nat |]
- ==> \<forall>bvs \<in> list(A). \<forall>env \<in> list(A).
- length(bvs) = n -->
- sats(A, iterates(incr_boundvars,n,p), bvs@env) <-> sats(A, p, env)"
-apply (induct_tac n, simp, clarify)
-apply (erule list.cases)
-apply (auto simp add: sats_incr_boundvars_iff)
-done
-*)
-
-consts arity :: "i=>i"
-primrec
- "arity(Member(x,y)) = succ(x) \<union> succ(y)"
-
- "arity(Equal(x,y)) = succ(x) \<union> succ(y)"
-
- "arity(Nand(p,q)) = arity(p) \<union> arity(q)"
-
- "arity(Forall(p)) = nat_case(0, %x. x, arity(p))"
-
-
-lemma arity_type [TC]: "p \<in> formula ==> arity(p) \<in> nat"
-by (induct_tac p, simp_all)
-
-lemma arity_Neg [simp]: "arity(Neg(p)) = arity(p)"
-by (simp add: Neg_def)
-
-lemma arity_And [simp]: "arity(And(p,q)) = arity(p) \<union> arity(q)"
-by (simp add: And_def)
-
-lemma arity_Or [simp]: "arity(Or(p,q)) = arity(p) \<union> arity(q)"
-by (simp add: Or_def)
-
-lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \<union> arity(q)"
-by (simp add: Implies_def)
-
-lemma arity_Iff [simp]: "arity(Iff(p,q)) = arity(p) \<union> arity(q)"
-by (simp add: Iff_def, blast)
-
-lemma arity_Exists [simp]: "arity(Exists(p)) = nat_case(0, %x. x, arity(p))"
-by (simp add: Exists_def)
-
-
-lemma arity_sats_iff [rule_format]:
- "[| p \<in> formula; extra \<in> list(A) |]
- ==> \<forall>env \<in> list(A).
- arity(p) \<le> length(env) -->
- sats(A, p, env @ extra) <-> sats(A, p, env)"
-apply (induct_tac p)
-apply (simp_all add: nth_append Un_least_lt_iff arity_type nat_imp_quasinat
- split: split_nat_case, auto)
-done
-
-lemma arity_sats1_iff:
- "[| arity(p) \<le> succ(length(env)); p \<in> formula; x \<in> A; env \<in> list(A);
- extra \<in> list(A) |]
- ==> sats(A, p, Cons(x, env @ extra)) <-> sats(A, p, Cons(x, env))"
-apply (insert arity_sats_iff [of p extra A "Cons(x,env)"])
-apply simp
-done
(*the following two lemmas prevent huge case splits in arity_incr_bv_lemma*)
lemma incr_var_lemma:
@@ -336,7 +316,7 @@
apply (induct_tac p)
apply (simp_all add: imp_disj not_lt_iff_le Un_least_lt_iff lt_Un_iff le_Un_iff
succ_Un_distrib [symmetric] incr_var_lt incr_var_le
- Un_commute incr_var_lemma arity_type nat_imp_quasinat
+ Un_commute incr_var_lemma Arith.pred_def nat_imp_quasinat
split: split_nat_case)
txt{*the Forall case reduces to linear arithmetic*}
prefer 2
@@ -350,24 +330,8 @@
apply (simp add: Un_commute)
done
-lemma arity_incr_boundvars_eq:
- "p \<in> formula
- ==> arity(incr_boundvars(p)) =
- (if 0 < arity(p) then succ(arity(p)) else arity(p))"
-apply (insert arity_incr_bv_lemma [of p 0])
-apply (simp add: incr_boundvars_def)
-done
-lemma arity_iterates_incr_boundvars_eq:
- "[| p \<in> formula; n \<in> nat |]
- ==> arity(incr_boundvars^n(p)) =
- (if 0 < arity(p) then n #+ arity(p) else arity(p))"
-apply (induct_tac n)
-apply (simp_all add: arity_incr_boundvars_eq not_lt_iff_le)
-done
-
-
-subsection{*Renaming all but the first bound variable*}
+subsection{*Renaming all but the First de Bruijn Variable*}
constdefs incr_bv1 :: "i => i"
"incr_bv1(p) == incr_bv(p)`1"
@@ -377,7 +341,7 @@
by (simp add: incr_bv1_def)
(*For renaming all but the bound variable at level 0*)
-lemma sats_incr_bv1_iff [rule_format]:
+lemma sats_incr_bv1_iff:
"[| p \<in> formula; env \<in> list(A); x \<in> A; y \<in> A |]
==> sats(A, incr_bv1(p), Cons(x, Cons(y, env))) <->
sats(A, p, Cons(x,env))"
@@ -416,7 +380,10 @@
done
-(*Definable powerset operation: Kunen's definition 1.1, page 165.*)
+
+subsection{*Definable Powerset*}
+
+text{*The definable powerset operation: Kunen's definition VI 1.1, page 165.*}
constdefs DPow :: "i => i"
"DPow(A) == {X \<in> Pow(A).
\<exists>env \<in> list(A). \<exists>p \<in> formula.
@@ -445,7 +412,7 @@
lemmas DPow_imp_subset = DPowD [THEN conjunct1]
-(*Lemma 1.2*)
+(*Kunen's Lemma VI 1.2*)
lemma "[| p \<in> formula; env \<in> list(A); arity(p) \<le> succ(length(env)) |]
==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"
by (blast intro: DPowI)
--- a/src/ZF/Constructible/Rank.thy Mon Oct 14 10:44:32 2002 +0200
+++ b/src/ZF/Constructible/Rank.thy Mon Oct 14 11:32:00 2002 +0200
@@ -666,6 +666,12 @@
+subsection {*Absoluteness of Well-Founded Relations*}
+
+text{*Relativized to @{term M}: Every well-founded relation is a subset of some
+inverse image of an ordinal. Key step is the construction (in @{term M}) of a
+rank function.*}
+
locale M_wfrank = M_trancl +
assumes wfrank_separation:
"M(r) ==>
--- a/src/ZF/Constructible/Rec_Separation.thy Mon Oct 14 10:44:32 2002 +0200
+++ b/src/ZF/Constructible/Rec_Separation.thy Mon Oct 14 11:32:00 2002 +0200
@@ -204,22 +204,9 @@
lemmas iterates_abs = M_trancl.iterates_abs [OF M_trancl_L]
and rtran_closure_rtrancl = M_trancl.rtran_closure_rtrancl [OF M_trancl_L]
- and rtrancl_closed = M_trancl.rtrancl_closed [OF M_trancl_L]
- and rtrancl_abs = M_trancl.rtrancl_abs [OF M_trancl_L]
- and trancl_closed = M_trancl.trancl_closed [OF M_trancl_L]
- and trancl_abs = M_trancl.trancl_abs [OF M_trancl_L]
- and wellfounded_on_trancl = M_trancl.wellfounded_on_trancl [OF M_trancl_L]
- and wellfounded_trancl = M_trancl.wellfounded_trancl [OF M_trancl_L]
- and wfrec_relativize = M_trancl.wfrec_relativize [OF M_trancl_L]
- and trans_wfrec_relativize = M_trancl.trans_wfrec_relativize [OF M_trancl_L]
and trans_wfrec_abs = M_trancl.trans_wfrec_abs [OF M_trancl_L]
- and trans_eq_pair_wfrec_iff = M_trancl.trans_eq_pair_wfrec_iff [OF M_trancl_L]
and eq_pair_wfrec_iff = M_trancl.eq_pair_wfrec_iff [OF M_trancl_L]
-declare rtrancl_closed [intro,simp]
-declare rtrancl_abs [simp]
-declare trancl_closed [intro,simp]
-declare trancl_abs [simp]
subsection{*@{term L} is Closed Under the Operator @{term list}*}
--- a/src/ZF/Constructible/WF_absolute.thy Mon Oct 14 10:44:32 2002 +0200
+++ b/src/ZF/Constructible/WF_absolute.thy Mon Oct 14 11:32:00 2002 +0200
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)
-header {*Absoluteness for Well-Founded Relations and Well-Founded Recursion*}
+header {*Absoluteness of Well-Founded Recursion*}
theory WF_absolute = WFrec:
@@ -175,13 +175,8 @@
apply (simp_all add: trancl_type [THEN field_rel_subset])
done
-text{*Relativized to M: Every well-founded relation is a subset of some
-inverse image of an ordinal. Key step is the construction (in M) of a
-rank function.*}
-
-
-text{*absoluteness for wfrec-defined functions.*}
+text{*Absoluteness for wfrec-defined functions.*}
(*first use is_recfun, then M_is_recfun*)