--- a/src/ZF/Constructible/L_axioms.thy Tue Jul 16 16:28:49 2002 +0200
+++ b/src/ZF/Constructible/L_axioms.thy Tue Jul 16 16:29:36 2002 +0200
@@ -66,7 +66,8 @@
apply (simp_all add: Replace_iff univalent_def, blast)
done
-subsection{*Instantiation of the locale @{text M_triv_axioms}*}
+subsection{*Instantiating the locale @{text M_triv_axioms}*}
+text{*No instances of Separation yet.*}
lemma Lset_mono_le: "mono_le_subset(Lset)"
by (simp add: mono_le_subset_def le_imp_subset Lset_mono)
@@ -90,57 +91,57 @@
fun kill_flex_triv_prems st = Seq.hd ((REPEAT_FIRST assume_tac) st);
-fun trivaxL th =
+fun triv_axioms_L th =
kill_flex_triv_prems
([transL, nonempty, upair_ax, Union_ax, power_ax, replacement, L_nat]
MRS (inst "M" "L" th));
-bind_thm ("ball_abs", trivaxL (thm "M_triv_axioms.ball_abs"));
-bind_thm ("rall_abs", trivaxL (thm "M_triv_axioms.rall_abs"));
-bind_thm ("bex_abs", trivaxL (thm "M_triv_axioms.bex_abs"));
-bind_thm ("rex_abs", trivaxL (thm "M_triv_axioms.rex_abs"));
-bind_thm ("ball_iff_equiv", trivaxL (thm "M_triv_axioms.ball_iff_equiv"));
-bind_thm ("M_equalityI", trivaxL (thm "M_triv_axioms.M_equalityI"));
-bind_thm ("empty_abs", trivaxL (thm "M_triv_axioms.empty_abs"));
-bind_thm ("subset_abs", trivaxL (thm "M_triv_axioms.subset_abs"));
-bind_thm ("upair_abs", trivaxL (thm "M_triv_axioms.upair_abs"));
-bind_thm ("upair_in_M_iff", trivaxL (thm "M_triv_axioms.upair_in_M_iff"));
-bind_thm ("singleton_in_M_iff", trivaxL (thm "M_triv_axioms.singleton_in_M_iff"));
-bind_thm ("pair_abs", trivaxL (thm "M_triv_axioms.pair_abs"));
-bind_thm ("pair_in_M_iff", trivaxL (thm "M_triv_axioms.pair_in_M_iff"));
-bind_thm ("pair_components_in_M", trivaxL (thm "M_triv_axioms.pair_components_in_M"));
-bind_thm ("cartprod_abs", trivaxL (thm "M_triv_axioms.cartprod_abs"));
-bind_thm ("union_abs", trivaxL (thm "M_triv_axioms.union_abs"));
-bind_thm ("inter_abs", trivaxL (thm "M_triv_axioms.inter_abs"));
-bind_thm ("setdiff_abs", trivaxL (thm "M_triv_axioms.setdiff_abs"));
-bind_thm ("Union_abs", trivaxL (thm "M_triv_axioms.Union_abs"));
-bind_thm ("Union_closed", trivaxL (thm "M_triv_axioms.Union_closed"));
-bind_thm ("Un_closed", trivaxL (thm "M_triv_axioms.Un_closed"));
-bind_thm ("cons_closed", trivaxL (thm "M_triv_axioms.cons_closed"));
-bind_thm ("successor_abs", trivaxL (thm "M_triv_axioms.successor_abs"));
-bind_thm ("succ_in_M_iff", trivaxL (thm "M_triv_axioms.succ_in_M_iff"));
-bind_thm ("separation_closed", trivaxL (thm "M_triv_axioms.separation_closed"));
-bind_thm ("strong_replacementI", trivaxL (thm "M_triv_axioms.strong_replacementI"));
-bind_thm ("strong_replacement_closed", trivaxL (thm "M_triv_axioms.strong_replacement_closed"));
-bind_thm ("RepFun_closed", trivaxL (thm "M_triv_axioms.RepFun_closed"));
-bind_thm ("lam_closed", trivaxL (thm "M_triv_axioms.lam_closed"));
-bind_thm ("image_abs", trivaxL (thm "M_triv_axioms.image_abs"));
-bind_thm ("powerset_Pow", trivaxL (thm "M_triv_axioms.powerset_Pow"));
-bind_thm ("powerset_imp_subset_Pow", trivaxL (thm "M_triv_axioms.powerset_imp_subset_Pow"));
-bind_thm ("nat_into_M", trivaxL (thm "M_triv_axioms.nat_into_M"));
-bind_thm ("nat_case_closed", trivaxL (thm "M_triv_axioms.nat_case_closed"));
-bind_thm ("Inl_in_M_iff", trivaxL (thm "M_triv_axioms.Inl_in_M_iff"));
-bind_thm ("Inr_in_M_iff", trivaxL (thm "M_triv_axioms.Inr_in_M_iff"));
-bind_thm ("lt_closed", trivaxL (thm "M_triv_axioms.lt_closed"));
-bind_thm ("transitive_set_abs", trivaxL (thm "M_triv_axioms.transitive_set_abs"));
-bind_thm ("ordinal_abs", trivaxL (thm "M_triv_axioms.ordinal_abs"));
-bind_thm ("limit_ordinal_abs", trivaxL (thm "M_triv_axioms.limit_ordinal_abs"));
-bind_thm ("successor_ordinal_abs", trivaxL (thm "M_triv_axioms.successor_ordinal_abs"));
-bind_thm ("finite_ordinal_abs", trivaxL (thm "M_triv_axioms.finite_ordinal_abs"));
-bind_thm ("omega_abs", trivaxL (thm "M_triv_axioms.omega_abs"));
-bind_thm ("number1_abs", trivaxL (thm "M_triv_axioms.number1_abs"));
-bind_thm ("number1_abs", trivaxL (thm "M_triv_axioms.number1_abs"));
-bind_thm ("number3_abs", trivaxL (thm "M_triv_axioms.number3_abs"));
+bind_thm ("ball_abs", triv_axioms_L (thm "M_triv_axioms.ball_abs"));
+bind_thm ("rall_abs", triv_axioms_L (thm "M_triv_axioms.rall_abs"));
+bind_thm ("bex_abs", triv_axioms_L (thm "M_triv_axioms.bex_abs"));
+bind_thm ("rex_abs", triv_axioms_L (thm "M_triv_axioms.rex_abs"));
+bind_thm ("ball_iff_equiv", triv_axioms_L (thm "M_triv_axioms.ball_iff_equiv"));
+bind_thm ("M_equalityI", triv_axioms_L (thm "M_triv_axioms.M_equalityI"));
+bind_thm ("empty_abs", triv_axioms_L (thm "M_triv_axioms.empty_abs"));
+bind_thm ("subset_abs", triv_axioms_L (thm "M_triv_axioms.subset_abs"));
+bind_thm ("upair_abs", triv_axioms_L (thm "M_triv_axioms.upair_abs"));
+bind_thm ("upair_in_M_iff", triv_axioms_L (thm "M_triv_axioms.upair_in_M_iff"));
+bind_thm ("singleton_in_M_iff", triv_axioms_L (thm "M_triv_axioms.singleton_in_M_iff"));
+bind_thm ("pair_abs", triv_axioms_L (thm "M_triv_axioms.pair_abs"));
+bind_thm ("pair_in_M_iff", triv_axioms_L (thm "M_triv_axioms.pair_in_M_iff"));
+bind_thm ("pair_components_in_M", triv_axioms_L (thm "M_triv_axioms.pair_components_in_M"));
+bind_thm ("cartprod_abs", triv_axioms_L (thm "M_triv_axioms.cartprod_abs"));
+bind_thm ("union_abs", triv_axioms_L (thm "M_triv_axioms.union_abs"));
+bind_thm ("inter_abs", triv_axioms_L (thm "M_triv_axioms.inter_abs"));
+bind_thm ("setdiff_abs", triv_axioms_L (thm "M_triv_axioms.setdiff_abs"));
+bind_thm ("Union_abs", triv_axioms_L (thm "M_triv_axioms.Union_abs"));
+bind_thm ("Union_closed", triv_axioms_L (thm "M_triv_axioms.Union_closed"));
+bind_thm ("Un_closed", triv_axioms_L (thm "M_triv_axioms.Un_closed"));
+bind_thm ("cons_closed", triv_axioms_L (thm "M_triv_axioms.cons_closed"));
+bind_thm ("successor_abs", triv_axioms_L (thm "M_triv_axioms.successor_abs"));
+bind_thm ("succ_in_M_iff", triv_axioms_L (thm "M_triv_axioms.succ_in_M_iff"));
+bind_thm ("separation_closed", triv_axioms_L (thm "M_triv_axioms.separation_closed"));
+bind_thm ("strong_replacementI", triv_axioms_L (thm "M_triv_axioms.strong_replacementI"));
+bind_thm ("strong_replacement_closed", triv_axioms_L (thm "M_triv_axioms.strong_replacement_closed"));
+bind_thm ("RepFun_closed", triv_axioms_L (thm "M_triv_axioms.RepFun_closed"));
+bind_thm ("lam_closed", triv_axioms_L (thm "M_triv_axioms.lam_closed"));
+bind_thm ("image_abs", triv_axioms_L (thm "M_triv_axioms.image_abs"));
+bind_thm ("powerset_Pow", triv_axioms_L (thm "M_triv_axioms.powerset_Pow"));
+bind_thm ("powerset_imp_subset_Pow", triv_axioms_L (thm "M_triv_axioms.powerset_imp_subset_Pow"));
+bind_thm ("nat_into_M", triv_axioms_L (thm "M_triv_axioms.nat_into_M"));
+bind_thm ("nat_case_closed", triv_axioms_L (thm "M_triv_axioms.nat_case_closed"));
+bind_thm ("Inl_in_M_iff", triv_axioms_L (thm "M_triv_axioms.Inl_in_M_iff"));
+bind_thm ("Inr_in_M_iff", triv_axioms_L (thm "M_triv_axioms.Inr_in_M_iff"));
+bind_thm ("lt_closed", triv_axioms_L (thm "M_triv_axioms.lt_closed"));
+bind_thm ("transitive_set_abs", triv_axioms_L (thm "M_triv_axioms.transitive_set_abs"));
+bind_thm ("ordinal_abs", triv_axioms_L (thm "M_triv_axioms.ordinal_abs"));
+bind_thm ("limit_ordinal_abs", triv_axioms_L (thm "M_triv_axioms.limit_ordinal_abs"));
+bind_thm ("successor_ordinal_abs", triv_axioms_L (thm "M_triv_axioms.successor_ordinal_abs"));
+bind_thm ("finite_ordinal_abs", triv_axioms_L (thm "M_triv_axioms.finite_ordinal_abs"));
+bind_thm ("omega_abs", triv_axioms_L (thm "M_triv_axioms.omega_abs"));
+bind_thm ("number1_abs", triv_axioms_L (thm "M_triv_axioms.number1_abs"));
+bind_thm ("number1_abs", triv_axioms_L (thm "M_triv_axioms.number1_abs"));
+bind_thm ("number3_abs", triv_axioms_L (thm "M_triv_axioms.number3_abs"));
*}
declare ball_abs [simp]
@@ -563,6 +564,39 @@
done
+subsubsection{*The Number 1, Internalized*}
+
+(* "number1(M,a) == (\<exists>x[M]. empty(M,x) & successor(M,x,a))" *)
+constdefs number1_fm :: "i=>i"
+ "number1_fm(a) == Exists(And(empty_fm(0), succ_fm(0,succ(a))))"
+
+lemma number1_type [TC]:
+ "x \<in> nat ==> number1_fm(x) \<in> formula"
+by (simp add: number1_fm_def)
+
+lemma arity_number1_fm [simp]:
+ "x \<in> nat ==> arity(number1_fm(x)) = succ(x)"
+by (simp add: number1_fm_def succ_Un_distrib [symmetric] Un_ac)
+
+lemma sats_number1_fm [simp]:
+ "[| x \<in> nat; env \<in> list(A)|]
+ ==> sats(A, number1_fm(x), env) <-> number1(**A, nth(x,env))"
+by (simp add: number1_fm_def number1_def)
+
+lemma number1_iff_sats:
+ "[| nth(i,env) = x; nth(j,env) = y;
+ i \<in> nat; env \<in> list(A)|]
+ ==> number1(**A, x) <-> sats(A, number1_fm(i), env)"
+by simp
+
+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 (intro FOL_reflections empty_reflection successor_reflection)
+done
+
+
subsubsection{*Big Union, Internalized*}
(* "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y[M]. y\<in>A & x \<in> y)" *)
@@ -1076,7 +1110,8 @@
by simp
lemmas function_reflections =
- empty_reflection upair_reflection pair_reflection union_reflection
+ empty_reflection number1_reflection
+ upair_reflection pair_reflection union_reflection
big_union_reflection cons_reflection successor_reflection
fun_apply_reflection subset_reflection
transitive_set_reflection membership_reflection
@@ -1085,7 +1120,8 @@
is_relation_reflection is_function_reflection
lemmas function_iff_sats =
- empty_iff_sats upair_iff_sats pair_iff_sats union_iff_sats
+ empty_iff_sats number1_iff_sats
+ upair_iff_sats pair_iff_sats union_iff_sats
cons_iff_sats successor_iff_sats
fun_apply_iff_sats Memrel_iff_sats
pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats