src/ZF/Constructible/L_axioms.thy
changeset 13363 c26eeb000470
parent 13352 3cd767f8d78b
child 13385 31df66ca0780
     1.1 --- a/src/ZF/Constructible/L_axioms.thy	Tue Jul 16 16:28:49 2002 +0200
     1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Tue Jul 16 16:29:36 2002 +0200
     1.3 @@ -66,7 +66,8 @@
     1.4  apply (simp_all add: Replace_iff univalent_def, blast) 
     1.5  done
     1.6  
     1.7 -subsection{*Instantiation of the locale @{text M_triv_axioms}*}
     1.8 +subsection{*Instantiating the locale @{text M_triv_axioms}*}
     1.9 +text{*No instances of Separation yet.*}
    1.10  
    1.11  lemma Lset_mono_le: "mono_le_subset(Lset)"
    1.12  by (simp add: mono_le_subset_def le_imp_subset Lset_mono) 
    1.13 @@ -90,57 +91,57 @@
    1.14  
    1.15  fun kill_flex_triv_prems st = Seq.hd ((REPEAT_FIRST assume_tac) st);
    1.16  
    1.17 -fun trivaxL th =
    1.18 +fun triv_axioms_L th =
    1.19      kill_flex_triv_prems 
    1.20         ([transL, nonempty, upair_ax, Union_ax, power_ax, replacement, L_nat] 
    1.21          MRS (inst "M" "L" th));
    1.22  
    1.23 -bind_thm ("ball_abs", trivaxL (thm "M_triv_axioms.ball_abs"));
    1.24 -bind_thm ("rall_abs", trivaxL (thm "M_triv_axioms.rall_abs"));
    1.25 -bind_thm ("bex_abs", trivaxL (thm "M_triv_axioms.bex_abs"));
    1.26 -bind_thm ("rex_abs", trivaxL (thm "M_triv_axioms.rex_abs"));
    1.27 -bind_thm ("ball_iff_equiv", trivaxL (thm "M_triv_axioms.ball_iff_equiv"));
    1.28 -bind_thm ("M_equalityI", trivaxL (thm "M_triv_axioms.M_equalityI"));
    1.29 -bind_thm ("empty_abs", trivaxL (thm "M_triv_axioms.empty_abs"));
    1.30 -bind_thm ("subset_abs", trivaxL (thm "M_triv_axioms.subset_abs"));
    1.31 -bind_thm ("upair_abs", trivaxL (thm "M_triv_axioms.upair_abs"));
    1.32 -bind_thm ("upair_in_M_iff", trivaxL (thm "M_triv_axioms.upair_in_M_iff"));
    1.33 -bind_thm ("singleton_in_M_iff", trivaxL (thm "M_triv_axioms.singleton_in_M_iff"));
    1.34 -bind_thm ("pair_abs", trivaxL (thm "M_triv_axioms.pair_abs"));
    1.35 -bind_thm ("pair_in_M_iff", trivaxL (thm "M_triv_axioms.pair_in_M_iff"));
    1.36 -bind_thm ("pair_components_in_M", trivaxL (thm "M_triv_axioms.pair_components_in_M"));
    1.37 -bind_thm ("cartprod_abs", trivaxL (thm "M_triv_axioms.cartprod_abs"));
    1.38 -bind_thm ("union_abs", trivaxL (thm "M_triv_axioms.union_abs"));
    1.39 -bind_thm ("inter_abs", trivaxL (thm "M_triv_axioms.inter_abs"));
    1.40 -bind_thm ("setdiff_abs", trivaxL (thm "M_triv_axioms.setdiff_abs"));
    1.41 -bind_thm ("Union_abs", trivaxL (thm "M_triv_axioms.Union_abs"));
    1.42 -bind_thm ("Union_closed", trivaxL (thm "M_triv_axioms.Union_closed"));
    1.43 -bind_thm ("Un_closed", trivaxL (thm "M_triv_axioms.Un_closed"));
    1.44 -bind_thm ("cons_closed", trivaxL (thm "M_triv_axioms.cons_closed"));
    1.45 -bind_thm ("successor_abs", trivaxL (thm "M_triv_axioms.successor_abs"));
    1.46 -bind_thm ("succ_in_M_iff", trivaxL (thm "M_triv_axioms.succ_in_M_iff"));
    1.47 -bind_thm ("separation_closed", trivaxL (thm "M_triv_axioms.separation_closed"));
    1.48 -bind_thm ("strong_replacementI", trivaxL (thm "M_triv_axioms.strong_replacementI"));
    1.49 -bind_thm ("strong_replacement_closed", trivaxL (thm "M_triv_axioms.strong_replacement_closed"));
    1.50 -bind_thm ("RepFun_closed", trivaxL (thm "M_triv_axioms.RepFun_closed"));
    1.51 -bind_thm ("lam_closed", trivaxL (thm "M_triv_axioms.lam_closed"));
    1.52 -bind_thm ("image_abs", trivaxL (thm "M_triv_axioms.image_abs"));
    1.53 -bind_thm ("powerset_Pow", trivaxL (thm "M_triv_axioms.powerset_Pow"));
    1.54 -bind_thm ("powerset_imp_subset_Pow", trivaxL (thm "M_triv_axioms.powerset_imp_subset_Pow"));
    1.55 -bind_thm ("nat_into_M", trivaxL (thm "M_triv_axioms.nat_into_M"));
    1.56 -bind_thm ("nat_case_closed", trivaxL (thm "M_triv_axioms.nat_case_closed"));
    1.57 -bind_thm ("Inl_in_M_iff", trivaxL (thm "M_triv_axioms.Inl_in_M_iff"));
    1.58 -bind_thm ("Inr_in_M_iff", trivaxL (thm "M_triv_axioms.Inr_in_M_iff"));
    1.59 -bind_thm ("lt_closed", trivaxL (thm "M_triv_axioms.lt_closed"));
    1.60 -bind_thm ("transitive_set_abs", trivaxL (thm "M_triv_axioms.transitive_set_abs"));
    1.61 -bind_thm ("ordinal_abs", trivaxL (thm "M_triv_axioms.ordinal_abs"));
    1.62 -bind_thm ("limit_ordinal_abs", trivaxL (thm "M_triv_axioms.limit_ordinal_abs"));
    1.63 -bind_thm ("successor_ordinal_abs", trivaxL (thm "M_triv_axioms.successor_ordinal_abs"));
    1.64 -bind_thm ("finite_ordinal_abs", trivaxL (thm "M_triv_axioms.finite_ordinal_abs"));
    1.65 -bind_thm ("omega_abs", trivaxL (thm "M_triv_axioms.omega_abs"));
    1.66 -bind_thm ("number1_abs", trivaxL (thm "M_triv_axioms.number1_abs"));
    1.67 -bind_thm ("number1_abs", trivaxL (thm "M_triv_axioms.number1_abs"));
    1.68 -bind_thm ("number3_abs", trivaxL (thm "M_triv_axioms.number3_abs"));
    1.69 +bind_thm ("ball_abs", triv_axioms_L (thm "M_triv_axioms.ball_abs"));
    1.70 +bind_thm ("rall_abs", triv_axioms_L (thm "M_triv_axioms.rall_abs"));
    1.71 +bind_thm ("bex_abs", triv_axioms_L (thm "M_triv_axioms.bex_abs"));
    1.72 +bind_thm ("rex_abs", triv_axioms_L (thm "M_triv_axioms.rex_abs"));
    1.73 +bind_thm ("ball_iff_equiv", triv_axioms_L (thm "M_triv_axioms.ball_iff_equiv"));
    1.74 +bind_thm ("M_equalityI", triv_axioms_L (thm "M_triv_axioms.M_equalityI"));
    1.75 +bind_thm ("empty_abs", triv_axioms_L (thm "M_triv_axioms.empty_abs"));
    1.76 +bind_thm ("subset_abs", triv_axioms_L (thm "M_triv_axioms.subset_abs"));
    1.77 +bind_thm ("upair_abs", triv_axioms_L (thm "M_triv_axioms.upair_abs"));
    1.78 +bind_thm ("upair_in_M_iff", triv_axioms_L (thm "M_triv_axioms.upair_in_M_iff"));
    1.79 +bind_thm ("singleton_in_M_iff", triv_axioms_L (thm "M_triv_axioms.singleton_in_M_iff"));
    1.80 +bind_thm ("pair_abs", triv_axioms_L (thm "M_triv_axioms.pair_abs"));
    1.81 +bind_thm ("pair_in_M_iff", triv_axioms_L (thm "M_triv_axioms.pair_in_M_iff"));
    1.82 +bind_thm ("pair_components_in_M", triv_axioms_L (thm "M_triv_axioms.pair_components_in_M"));
    1.83 +bind_thm ("cartprod_abs", triv_axioms_L (thm "M_triv_axioms.cartprod_abs"));
    1.84 +bind_thm ("union_abs", triv_axioms_L (thm "M_triv_axioms.union_abs"));
    1.85 +bind_thm ("inter_abs", triv_axioms_L (thm "M_triv_axioms.inter_abs"));
    1.86 +bind_thm ("setdiff_abs", triv_axioms_L (thm "M_triv_axioms.setdiff_abs"));
    1.87 +bind_thm ("Union_abs", triv_axioms_L (thm "M_triv_axioms.Union_abs"));
    1.88 +bind_thm ("Union_closed", triv_axioms_L (thm "M_triv_axioms.Union_closed"));
    1.89 +bind_thm ("Un_closed", triv_axioms_L (thm "M_triv_axioms.Un_closed"));
    1.90 +bind_thm ("cons_closed", triv_axioms_L (thm "M_triv_axioms.cons_closed"));
    1.91 +bind_thm ("successor_abs", triv_axioms_L (thm "M_triv_axioms.successor_abs"));
    1.92 +bind_thm ("succ_in_M_iff", triv_axioms_L (thm "M_triv_axioms.succ_in_M_iff"));
    1.93 +bind_thm ("separation_closed", triv_axioms_L (thm "M_triv_axioms.separation_closed"));
    1.94 +bind_thm ("strong_replacementI", triv_axioms_L (thm "M_triv_axioms.strong_replacementI"));
    1.95 +bind_thm ("strong_replacement_closed", triv_axioms_L (thm "M_triv_axioms.strong_replacement_closed"));
    1.96 +bind_thm ("RepFun_closed", triv_axioms_L (thm "M_triv_axioms.RepFun_closed"));
    1.97 +bind_thm ("lam_closed", triv_axioms_L (thm "M_triv_axioms.lam_closed"));
    1.98 +bind_thm ("image_abs", triv_axioms_L (thm "M_triv_axioms.image_abs"));
    1.99 +bind_thm ("powerset_Pow", triv_axioms_L (thm "M_triv_axioms.powerset_Pow"));
   1.100 +bind_thm ("powerset_imp_subset_Pow", triv_axioms_L (thm "M_triv_axioms.powerset_imp_subset_Pow"));
   1.101 +bind_thm ("nat_into_M", triv_axioms_L (thm "M_triv_axioms.nat_into_M"));
   1.102 +bind_thm ("nat_case_closed", triv_axioms_L (thm "M_triv_axioms.nat_case_closed"));
   1.103 +bind_thm ("Inl_in_M_iff", triv_axioms_L (thm "M_triv_axioms.Inl_in_M_iff"));
   1.104 +bind_thm ("Inr_in_M_iff", triv_axioms_L (thm "M_triv_axioms.Inr_in_M_iff"));
   1.105 +bind_thm ("lt_closed", triv_axioms_L (thm "M_triv_axioms.lt_closed"));
   1.106 +bind_thm ("transitive_set_abs", triv_axioms_L (thm "M_triv_axioms.transitive_set_abs"));
   1.107 +bind_thm ("ordinal_abs", triv_axioms_L (thm "M_triv_axioms.ordinal_abs"));
   1.108 +bind_thm ("limit_ordinal_abs", triv_axioms_L (thm "M_triv_axioms.limit_ordinal_abs"));
   1.109 +bind_thm ("successor_ordinal_abs", triv_axioms_L (thm "M_triv_axioms.successor_ordinal_abs"));
   1.110 +bind_thm ("finite_ordinal_abs", triv_axioms_L (thm "M_triv_axioms.finite_ordinal_abs"));
   1.111 +bind_thm ("omega_abs", triv_axioms_L (thm "M_triv_axioms.omega_abs"));
   1.112 +bind_thm ("number1_abs", triv_axioms_L (thm "M_triv_axioms.number1_abs"));
   1.113 +bind_thm ("number1_abs", triv_axioms_L (thm "M_triv_axioms.number1_abs"));
   1.114 +bind_thm ("number3_abs", triv_axioms_L (thm "M_triv_axioms.number3_abs"));
   1.115  *}
   1.116  
   1.117  declare ball_abs [simp] 
   1.118 @@ -563,6 +564,39 @@
   1.119  done
   1.120  
   1.121  
   1.122 +subsubsection{*The Number 1, Internalized*}
   1.123 +
   1.124 +(* "number1(M,a) == (\<exists>x[M]. empty(M,x) & successor(M,x,a))" *)
   1.125 +constdefs number1_fm :: "i=>i"
   1.126 +    "number1_fm(a) == Exists(And(empty_fm(0), succ_fm(0,succ(a))))"
   1.127 +
   1.128 +lemma number1_type [TC]:
   1.129 +     "x \<in> nat ==> number1_fm(x) \<in> formula"
   1.130 +by (simp add: number1_fm_def) 
   1.131 +
   1.132 +lemma arity_number1_fm [simp]:
   1.133 +     "x \<in> nat ==> arity(number1_fm(x)) = succ(x)"
   1.134 +by (simp add: number1_fm_def succ_Un_distrib [symmetric] Un_ac) 
   1.135 +
   1.136 +lemma sats_number1_fm [simp]:
   1.137 +   "[| x \<in> nat; env \<in> list(A)|]
   1.138 +    ==> sats(A, number1_fm(x), env) <-> number1(**A, nth(x,env))"
   1.139 +by (simp add: number1_fm_def number1_def)
   1.140 +
   1.141 +lemma number1_iff_sats:
   1.142 +      "[| nth(i,env) = x; nth(j,env) = y; 
   1.143 +          i \<in> nat; env \<in> list(A)|]
   1.144 +       ==> number1(**A, x) <-> sats(A, number1_fm(i), env)"
   1.145 +by simp
   1.146 +
   1.147 +theorem number1_reflection:
   1.148 +     "REFLECTS[\<lambda>x. number1(L,f(x)), 
   1.149 +               \<lambda>i x. number1(**Lset(i),f(x))]"
   1.150 +apply (simp only: number1_def setclass_simps)
   1.151 +apply (intro FOL_reflections empty_reflection successor_reflection)
   1.152 +done
   1.153 +
   1.154 +
   1.155  subsubsection{*Big Union, Internalized*}
   1.156  
   1.157  (*  "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y[M]. y\<in>A & x \<in> y)" *)
   1.158 @@ -1076,7 +1110,8 @@
   1.159  by simp
   1.160  
   1.161  lemmas function_reflections = 
   1.162 -        empty_reflection upair_reflection pair_reflection union_reflection
   1.163 +        empty_reflection number1_reflection
   1.164 +	upair_reflection pair_reflection union_reflection
   1.165  	big_union_reflection cons_reflection successor_reflection 
   1.166          fun_apply_reflection subset_reflection
   1.167  	transitive_set_reflection membership_reflection
   1.168 @@ -1085,7 +1120,8 @@
   1.169  	is_relation_reflection is_function_reflection
   1.170  
   1.171  lemmas function_iff_sats = 
   1.172 -        empty_iff_sats upair_iff_sats pair_iff_sats union_iff_sats
   1.173 +        empty_iff_sats number1_iff_sats 
   1.174 +	upair_iff_sats pair_iff_sats union_iff_sats
   1.175  	cons_iff_sats successor_iff_sats
   1.176          fun_apply_iff_sats  Memrel_iff_sats
   1.177  	pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats