src/ZF/Constructible/L_axioms.thy
changeset 13291 a73ab154f75c
parent 13269 3ba9be497c33
child 13298 b4f370679c65
     1.1 --- a/src/ZF/Constructible/L_axioms.thy	Thu Jul 04 10:51:52 2002 +0200
     1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Thu Jul 04 10:52:33 2002 +0200
     1.3 @@ -67,12 +67,231 @@
     1.4  apply (simp add: Replace_iff univalent_def, blast) 
     1.5  done
     1.6  
     1.7 +subsection{*Instantiation of the locale @{text M_triv_axioms}*}
     1.8 +
     1.9 +lemma Lset_mono_le: "mono_le_subset(Lset)"
    1.10 +by (simp add: mono_le_subset_def le_imp_subset Lset_mono) 
    1.11 +
    1.12 +lemma Lset_cont: "cont_Ord(Lset)"
    1.13 +by (simp add: cont_Ord_def Limit_Lset_eq OUnion_def Limit_is_Ord) 
    1.14 +
    1.15 +lemmas Pair_in_Lset = Formula.Pair_in_LLimit;
    1.16 +
    1.17 +lemmas L_nat = Ord_in_L [OF Ord_nat];
    1.18 +
    1.19 +ML
    1.20 +{*
    1.21 +val transL = thm "transL";
    1.22 +val nonempty = thm "nonempty";
    1.23 +val upair_ax = thm "upair_ax";
    1.24 +val Union_ax = thm "Union_ax";
    1.25 +val power_ax = thm "power_ax";
    1.26 +val replacement = thm "replacement";
    1.27 +val L_nat = thm "L_nat";
    1.28 +
    1.29 +fun kill_flex_triv_prems st = Seq.hd ((REPEAT_FIRST assume_tac) st);
    1.30 +
    1.31 +fun trivaxL th =
    1.32 +    kill_flex_triv_prems 
    1.33 +       ([transL, nonempty, upair_ax, Union_ax, power_ax, replacement, L_nat] 
    1.34 +        MRS (inst "M" "L" th));
    1.35 +
    1.36 +bind_thm ("ball_abs", trivaxL (thm "M_triv_axioms.ball_abs"));
    1.37 +bind_thm ("rall_abs", trivaxL (thm "M_triv_axioms.rall_abs"));
    1.38 +bind_thm ("bex_abs", trivaxL (thm "M_triv_axioms.bex_abs"));
    1.39 +bind_thm ("rex_abs", trivaxL (thm "M_triv_axioms.rex_abs"));
    1.40 +bind_thm ("ball_iff_equiv", trivaxL (thm "M_triv_axioms.ball_iff_equiv"));
    1.41 +bind_thm ("M_equalityI", trivaxL (thm "M_triv_axioms.M_equalityI"));
    1.42 +bind_thm ("empty_abs", trivaxL (thm "M_triv_axioms.empty_abs"));
    1.43 +bind_thm ("subset_abs", trivaxL (thm "M_triv_axioms.subset_abs"));
    1.44 +bind_thm ("upair_abs", trivaxL (thm "M_triv_axioms.upair_abs"));
    1.45 +bind_thm ("upair_in_M_iff", trivaxL (thm "M_triv_axioms.upair_in_M_iff"));
    1.46 +bind_thm ("singleton_in_M_iff", trivaxL (thm "M_triv_axioms.singleton_in_M_iff"));
    1.47 +bind_thm ("pair_abs", trivaxL (thm "M_triv_axioms.pair_abs"));
    1.48 +bind_thm ("pair_in_M_iff", trivaxL (thm "M_triv_axioms.pair_in_M_iff"));
    1.49 +bind_thm ("pair_components_in_M", trivaxL (thm "M_triv_axioms.pair_components_in_M"));
    1.50 +bind_thm ("cartprod_abs", trivaxL (thm "M_triv_axioms.cartprod_abs"));
    1.51 +bind_thm ("union_abs", trivaxL (thm "M_triv_axioms.union_abs"));
    1.52 +bind_thm ("inter_abs", trivaxL (thm "M_triv_axioms.inter_abs"));
    1.53 +bind_thm ("setdiff_abs", trivaxL (thm "M_triv_axioms.setdiff_abs"));
    1.54 +bind_thm ("Union_abs", trivaxL (thm "M_triv_axioms.Union_abs"));
    1.55 +bind_thm ("Union_closed", trivaxL (thm "M_triv_axioms.Union_closed"));
    1.56 +bind_thm ("Un_closed", trivaxL (thm "M_triv_axioms.Un_closed"));
    1.57 +bind_thm ("cons_closed", trivaxL (thm "M_triv_axioms.cons_closed"));
    1.58 +bind_thm ("successor_abs", trivaxL (thm "M_triv_axioms.successor_abs"));
    1.59 +bind_thm ("succ_in_M_iff", trivaxL (thm "M_triv_axioms.succ_in_M_iff"));
    1.60 +bind_thm ("separation_closed", trivaxL (thm "M_triv_axioms.separation_closed"));
    1.61 +bind_thm ("strong_replacementI", trivaxL (thm "M_triv_axioms.strong_replacementI"));
    1.62 +bind_thm ("strong_replacement_closed", trivaxL (thm "M_triv_axioms.strong_replacement_closed"));
    1.63 +bind_thm ("RepFun_closed", trivaxL (thm "M_triv_axioms.RepFun_closed"));
    1.64 +bind_thm ("lam_closed", trivaxL (thm "M_triv_axioms.lam_closed"));
    1.65 +bind_thm ("image_abs", trivaxL (thm "M_triv_axioms.image_abs"));
    1.66 +bind_thm ("powerset_Pow", trivaxL (thm "M_triv_axioms.powerset_Pow"));
    1.67 +bind_thm ("powerset_imp_subset_Pow", trivaxL (thm "M_triv_axioms.powerset_imp_subset_Pow"));
    1.68 +bind_thm ("nat_into_M", trivaxL (thm "M_triv_axioms.nat_into_M"));
    1.69 +bind_thm ("nat_case_closed", trivaxL (thm "M_triv_axioms.nat_case_closed"));
    1.70 +bind_thm ("Inl_in_M_iff", trivaxL (thm "M_triv_axioms.Inl_in_M_iff"));
    1.71 +bind_thm ("Inr_in_M_iff", trivaxL (thm "M_triv_axioms.Inr_in_M_iff"));
    1.72 +bind_thm ("lt_closed", trivaxL (thm "M_triv_axioms.lt_closed"));
    1.73 +bind_thm ("transitive_set_abs", trivaxL (thm "M_triv_axioms.transitive_set_abs"));
    1.74 +bind_thm ("ordinal_abs", trivaxL (thm "M_triv_axioms.ordinal_abs"));
    1.75 +bind_thm ("limit_ordinal_abs", trivaxL (thm "M_triv_axioms.limit_ordinal_abs"));
    1.76 +bind_thm ("successor_ordinal_abs", trivaxL (thm "M_triv_axioms.successor_ordinal_abs"));
    1.77 +bind_thm ("finite_ordinal_abs", trivaxL (thm "M_triv_axioms.finite_ordinal_abs"));
    1.78 +bind_thm ("omega_abs", trivaxL (thm "M_triv_axioms.omega_abs"));
    1.79 +bind_thm ("number1_abs", trivaxL (thm "M_triv_axioms.number1_abs"));
    1.80 +bind_thm ("number1_abs", trivaxL (thm "M_triv_axioms.number1_abs"));
    1.81 +bind_thm ("number3_abs", trivaxL (thm "M_triv_axioms.number3_abs"));
    1.82 +*}
    1.83 +
    1.84 +declare ball_abs [simp] 
    1.85 +declare rall_abs [simp] 
    1.86 +declare bex_abs [simp] 
    1.87 +declare rex_abs [simp] 
    1.88 +declare empty_abs [simp] 
    1.89 +declare subset_abs [simp] 
    1.90 +declare upair_abs [simp] 
    1.91 +declare upair_in_M_iff [iff]
    1.92 +declare singleton_in_M_iff [iff]
    1.93 +declare pair_abs [simp] 
    1.94 +declare pair_in_M_iff [iff]
    1.95 +declare cartprod_abs [simp] 
    1.96 +declare union_abs [simp] 
    1.97 +declare inter_abs [simp] 
    1.98 +declare setdiff_abs [simp] 
    1.99 +declare Union_abs [simp] 
   1.100 +declare Union_closed [intro,simp]
   1.101 +declare Un_closed [intro,simp]
   1.102 +declare cons_closed [intro,simp]
   1.103 +declare successor_abs [simp] 
   1.104 +declare succ_in_M_iff [iff]
   1.105 +declare separation_closed [intro,simp]
   1.106 +declare strong_replacementI [rule_format]
   1.107 +declare strong_replacement_closed [intro,simp]
   1.108 +declare RepFun_closed [intro,simp]
   1.109 +declare lam_closed [intro,simp]
   1.110 +declare image_abs [simp] 
   1.111 +declare nat_into_M [intro]
   1.112 +declare Inl_in_M_iff [iff]
   1.113 +declare Inr_in_M_iff [iff]
   1.114 +declare transitive_set_abs [simp] 
   1.115 +declare ordinal_abs [simp] 
   1.116 +declare limit_ordinal_abs [simp] 
   1.117 +declare successor_ordinal_abs [simp] 
   1.118 +declare finite_ordinal_abs [simp] 
   1.119 +declare omega_abs [simp] 
   1.120 +declare number1_abs [simp] 
   1.121 +declare number1_abs [simp] 
   1.122 +declare number3_abs [simp]
   1.123 +
   1.124 +
   1.125 +subsection{*Instantiation of the locale @{text reflection}*}
   1.126 +
   1.127 +text{*instances of locale constants*}
   1.128 +constdefs
   1.129 +  L_Reflects :: "[i=>o,i=>o,[i,i]=>o] => o"
   1.130 +    "L_Reflects(Cl,P,Q) == Closed_Unbounded(Cl) &
   1.131 +                           (\<forall>a. Cl(a) --> (\<forall>x \<in> Lset(a). P(x) <-> Q(a,x)))"
   1.132 +
   1.133 +  L_F0 :: "[i=>o,i] => i"
   1.134 +    "L_F0(P,y) == \<mu>b. (\<exists>z. L(z) \<and> P(<y,z>)) --> (\<exists>z\<in>Lset(b). P(<y,z>))"
   1.135 +
   1.136 +  L_FF :: "[i=>o,i] => i"
   1.137 +    "L_FF(P)   == \<lambda>a. \<Union>y\<in>Lset(a). L_F0(P,y)"
   1.138 +
   1.139 +  L_ClEx :: "[i=>o,i] => o"
   1.140 +    "L_ClEx(P) == \<lambda>a. Limit(a) \<and> normalize(L_FF(P),a) = a"
   1.141 +
   1.142 +theorem Triv_reflection [intro]:
   1.143 +     "L_Reflects(Ord, P, \<lambda>a x. P(x))"
   1.144 +by (simp add: L_Reflects_def)
   1.145 +
   1.146 +theorem Not_reflection [intro]:
   1.147 +     "L_Reflects(Cl,P,Q) ==> L_Reflects(Cl, \<lambda>x. ~P(x), \<lambda>a x. ~Q(a,x))"
   1.148 +by (simp add: L_Reflects_def) 
   1.149 +
   1.150 +theorem And_reflection [intro]:
   1.151 +     "[| L_Reflects(Cl,P,Q); L_Reflects(C',P',Q') |] 
   1.152 +      ==> L_Reflects(\<lambda>a. Cl(a) \<and> C'(a), \<lambda>x. P(x) \<and> P'(x), 
   1.153 +                                      \<lambda>a x. Q(a,x) \<and> Q'(a,x))"
   1.154 +by (simp add: L_Reflects_def Closed_Unbounded_Int, blast)
   1.155 +
   1.156 +theorem Or_reflection [intro]:
   1.157 +     "[| L_Reflects(Cl,P,Q); L_Reflects(C',P',Q') |] 
   1.158 +      ==> L_Reflects(\<lambda>a. Cl(a) \<and> C'(a), \<lambda>x. P(x) \<or> P'(x), 
   1.159 +                                      \<lambda>a x. Q(a,x) \<or> Q'(a,x))"
   1.160 +by (simp add: L_Reflects_def Closed_Unbounded_Int, blast)
   1.161 +
   1.162 +theorem Imp_reflection [intro]:
   1.163 +     "[| L_Reflects(Cl,P,Q); L_Reflects(C',P',Q') |] 
   1.164 +      ==> L_Reflects(\<lambda>a. Cl(a) \<and> C'(a), 
   1.165 +                   \<lambda>x. P(x) --> P'(x), 
   1.166 +                   \<lambda>a x. Q(a,x) --> Q'(a,x))"
   1.167 +by (simp add: L_Reflects_def Closed_Unbounded_Int, blast)
   1.168 +
   1.169 +theorem Iff_reflection [intro]:
   1.170 +     "[| L_Reflects(Cl,P,Q); L_Reflects(C',P',Q') |] 
   1.171 +      ==> L_Reflects(\<lambda>a. Cl(a) \<and> C'(a), 
   1.172 +                   \<lambda>x. P(x) <-> P'(x), 
   1.173 +                   \<lambda>a x. Q(a,x) <-> Q'(a,x))"
   1.174 +by (simp add: L_Reflects_def Closed_Unbounded_Int, blast) 
   1.175 +
   1.176 +
   1.177 +theorem Ex_reflection [intro]:
   1.178 +     "L_Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))) 
   1.179 +      ==> L_Reflects(\<lambda>a. Cl(a) \<and> L_ClEx(\<lambda>x. P(fst(x),snd(x)), a), 
   1.180 +                   \<lambda>x. \<exists>z. L(z) \<and> P(x,z), 
   1.181 +                   \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z))"
   1.182 +apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def) 
   1.183 +apply (rule reflection.Ex_reflection [OF Lset_mono_le Lset_cont Pair_in_Lset],
   1.184 +       assumption+)
   1.185 +done
   1.186 +
   1.187 +theorem All_reflection [intro]:
   1.188 +     "L_Reflects(Cl,  \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
   1.189 +      ==> L_Reflects(\<lambda>a. Cl(a) \<and> L_ClEx(\<lambda>x. ~P(fst(x),snd(x)), a), 
   1.190 +                   \<lambda>x. \<forall>z. L(z) --> P(x,z), 
   1.191 +                   \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z))" 
   1.192 +apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def) 
   1.193 +apply (rule reflection.All_reflection [OF Lset_mono_le Lset_cont Pair_in_Lset],
   1.194 +       assumption+)
   1.195 +done
   1.196 +
   1.197 +theorem Rex_reflection [intro]:
   1.198 +     "L_Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))) 
   1.199 +      ==> L_Reflects(\<lambda>a. Cl(a) \<and> L_ClEx(\<lambda>x. P(fst(x),snd(x)), a), 
   1.200 +                   \<lambda>x. \<exists>z[L]. P(x,z), 
   1.201 +                   \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z))"
   1.202 +by (unfold rex_def, blast) 
   1.203 +
   1.204 +theorem Rall_reflection [intro]:
   1.205 +     "L_Reflects(Cl,  \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
   1.206 +      ==> L_Reflects(\<lambda>a. Cl(a) \<and> L_ClEx(\<lambda>x. ~P(fst(x),snd(x)), a), 
   1.207 +                   \<lambda>x. \<forall>z[L]. P(x,z), 
   1.208 +                   \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z))" 
   1.209 +by (unfold rall_def, blast) 
   1.210 +
   1.211 +lemma ReflectsD:
   1.212 +     "[|L_Reflects(Cl,P,Q); Ord(i)|] 
   1.213 +      ==> \<exists>j. i<j & (\<forall>x \<in> Lset(j). P(x) <-> Q(j,x))"
   1.214 +apply (simp add: L_Reflects_def Closed_Unbounded_def, clarify)
   1.215 +apply (blast dest!: UnboundedD) 
   1.216 +done
   1.217 +
   1.218 +lemma ReflectsE:
   1.219 +     "[| L_Reflects(Cl,P,Q); Ord(i);
   1.220 +         !!j. [|i<j;  \<forall>x \<in> Lset(j). P(x) <-> Q(j,x)|] ==> R |]
   1.221 +      ==> R"
   1.222 +by (blast dest!: ReflectsD) 
   1.223 +
   1.224 +lemma Collect_mem_eq: "{x\<in>A. x\<in>B} = A \<inter> B";
   1.225 +by blast
   1.226 +
   1.227 +
   1.228  end
   1.229  
   1.230  (*
   1.231  
   1.232 -  and Inter_separation:
   1.233 -     "L(A) ==> separation(L, \<lambda>x. \<forall>y\<in>A. L(y) --> x\<in>y)"
   1.234    and cartprod_separation:
   1.235       "[| L(A); L(B) |] 
   1.236        ==> separation(L, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. L(x) & L(y) & pair(L,x,y,z))"