src/ZF/Constructible/L_axioms.thy
author paulson
Fri, 05 Jul 2002 11:47:44 +0200
changeset 13304 43ef6c6dd906
parent 13299 3a932abf97e8
child 13306 6eebcddee32b
permissions -rw-r--r--
more separation instances
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
     1
header {* The class L satisfies the axioms of ZF*}
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
     2
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13268
diff changeset
     3
theory L_axioms = Formula + Relative + Reflection:
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
     4
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
     5
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
     6
text {* The class L satisfies the premises of locale @{text M_axioms} *}
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
     7
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
     8
lemma transL: "[| y\<in>x; L(x) |] ==> L(y)"
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
     9
apply (insert Transset_Lset) 
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    10
apply (simp add: Transset_def L_def, blast) 
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    11
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    12
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    13
lemma nonempty: "L(0)"
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    14
apply (simp add: L_def) 
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    15
apply (blast intro: zero_in_Lset) 
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    16
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    17
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    18
lemma upair_ax: "upair_ax(L)"
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    19
apply (simp add: upair_ax_def upair_def, clarify)
13299
3a932abf97e8 More use of relativized quantifiers
paulson
parents: 13298
diff changeset
    20
apply (rule_tac x="{x,y}" in rexI)  
3a932abf97e8 More use of relativized quantifiers
paulson
parents: 13298
diff changeset
    21
apply (simp_all add: doubleton_in_L) 
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    22
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    23
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    24
lemma Union_ax: "Union_ax(L)"
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    25
apply (simp add: Union_ax_def big_union_def, clarify)
13299
3a932abf97e8 More use of relativized quantifiers
paulson
parents: 13298
diff changeset
    26
apply (rule_tac x="Union(x)" in rexI)  
3a932abf97e8 More use of relativized quantifiers
paulson
parents: 13298
diff changeset
    27
apply (simp_all add: Union_in_L, auto) 
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    28
apply (blast intro: transL) 
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    29
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    30
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    31
lemma power_ax: "power_ax(L)"
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    32
apply (simp add: power_ax_def powerset_def Relative.subset_def, clarify)
13299
3a932abf97e8 More use of relativized quantifiers
paulson
parents: 13298
diff changeset
    33
apply (rule_tac x="{y \<in> Pow(x). L(y)}" in rexI)  
3a932abf97e8 More use of relativized quantifiers
paulson
parents: 13298
diff changeset
    34
apply (simp_all add: LPow_in_L, auto)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    35
apply (blast intro: transL) 
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    36
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    37
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    38
subsubsection{*For L to satisfy Replacement *}
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    39
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    40
(*Can't move these to Formula unless the definition of univalent is moved
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    41
there too!*)
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    42
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    43
lemma LReplace_in_Lset:
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    44
     "[|X \<in> Lset(i); univalent(L,X,Q); Ord(i)|] 
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    45
      ==> \<exists>j. Ord(j) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Lset(j)"
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    46
apply (rule_tac x="\<Union>y \<in> Replace(X, %x y. Q(x,y) & L(y)). succ(lrank(y))" 
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    47
       in exI)
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    48
apply simp
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    49
apply clarify 
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    50
apply (rule_tac a="x" in UN_I)  
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    51
 apply (simp_all add: Replace_iff univalent_def) 
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    52
apply (blast dest: transL L_I) 
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    53
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    54
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    55
lemma LReplace_in_L: 
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    56
     "[|L(X); univalent(L,X,Q)|] 
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    57
      ==> \<exists>Y. L(Y) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Y"
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    58
apply (drule L_D, clarify) 
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    59
apply (drule LReplace_in_Lset, assumption+)
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    60
apply (blast intro: L_I Lset_in_Lset_succ)
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    61
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    62
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    63
lemma replacement: "replacement(L,P)"
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    64
apply (simp add: replacement_def, clarify)
13268
240509babf00 more use of relativized quantifiers
paulson
parents: 13223
diff changeset
    65
apply (frule LReplace_in_L, assumption+, clarify) 
13299
3a932abf97e8 More use of relativized quantifiers
paulson
parents: 13298
diff changeset
    66
apply (rule_tac x=Y in rexI)   
3a932abf97e8 More use of relativized quantifiers
paulson
parents: 13298
diff changeset
    67
apply (simp_all add: Replace_iff univalent_def, blast) 
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    68
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    69
13291
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    70
subsection{*Instantiation of the locale @{text M_triv_axioms}*}
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    71
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    72
lemma Lset_mono_le: "mono_le_subset(Lset)"
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    73
by (simp add: mono_le_subset_def le_imp_subset Lset_mono) 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    74
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    75
lemma Lset_cont: "cont_Ord(Lset)"
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    76
by (simp add: cont_Ord_def Limit_Lset_eq OUnion_def Limit_is_Ord) 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    77
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    78
lemmas Pair_in_Lset = Formula.Pair_in_LLimit;
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    79
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    80
lemmas L_nat = Ord_in_L [OF Ord_nat];
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    81
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    82
ML
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    83
{*
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    84
val transL = thm "transL";
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    85
val nonempty = thm "nonempty";
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    86
val upair_ax = thm "upair_ax";
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    87
val Union_ax = thm "Union_ax";
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    88
val power_ax = thm "power_ax";
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    89
val replacement = thm "replacement";
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    90
val L_nat = thm "L_nat";
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    91
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    92
fun kill_flex_triv_prems st = Seq.hd ((REPEAT_FIRST assume_tac) st);
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    93
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    94
fun trivaxL th =
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    95
    kill_flex_triv_prems 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    96
       ([transL, nonempty, upair_ax, Union_ax, power_ax, replacement, L_nat] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    97
        MRS (inst "M" "L" th));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    98
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
    99
bind_thm ("ball_abs", trivaxL (thm "M_triv_axioms.ball_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   100
bind_thm ("rall_abs", trivaxL (thm "M_triv_axioms.rall_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   101
bind_thm ("bex_abs", trivaxL (thm "M_triv_axioms.bex_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   102
bind_thm ("rex_abs", trivaxL (thm "M_triv_axioms.rex_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   103
bind_thm ("ball_iff_equiv", trivaxL (thm "M_triv_axioms.ball_iff_equiv"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   104
bind_thm ("M_equalityI", trivaxL (thm "M_triv_axioms.M_equalityI"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   105
bind_thm ("empty_abs", trivaxL (thm "M_triv_axioms.empty_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   106
bind_thm ("subset_abs", trivaxL (thm "M_triv_axioms.subset_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   107
bind_thm ("upair_abs", trivaxL (thm "M_triv_axioms.upair_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   108
bind_thm ("upair_in_M_iff", trivaxL (thm "M_triv_axioms.upair_in_M_iff"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   109
bind_thm ("singleton_in_M_iff", trivaxL (thm "M_triv_axioms.singleton_in_M_iff"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   110
bind_thm ("pair_abs", trivaxL (thm "M_triv_axioms.pair_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   111
bind_thm ("pair_in_M_iff", trivaxL (thm "M_triv_axioms.pair_in_M_iff"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   112
bind_thm ("pair_components_in_M", trivaxL (thm "M_triv_axioms.pair_components_in_M"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   113
bind_thm ("cartprod_abs", trivaxL (thm "M_triv_axioms.cartprod_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   114
bind_thm ("union_abs", trivaxL (thm "M_triv_axioms.union_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   115
bind_thm ("inter_abs", trivaxL (thm "M_triv_axioms.inter_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   116
bind_thm ("setdiff_abs", trivaxL (thm "M_triv_axioms.setdiff_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   117
bind_thm ("Union_abs", trivaxL (thm "M_triv_axioms.Union_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   118
bind_thm ("Union_closed", trivaxL (thm "M_triv_axioms.Union_closed"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   119
bind_thm ("Un_closed", trivaxL (thm "M_triv_axioms.Un_closed"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   120
bind_thm ("cons_closed", trivaxL (thm "M_triv_axioms.cons_closed"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   121
bind_thm ("successor_abs", trivaxL (thm "M_triv_axioms.successor_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   122
bind_thm ("succ_in_M_iff", trivaxL (thm "M_triv_axioms.succ_in_M_iff"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   123
bind_thm ("separation_closed", trivaxL (thm "M_triv_axioms.separation_closed"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   124
bind_thm ("strong_replacementI", trivaxL (thm "M_triv_axioms.strong_replacementI"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   125
bind_thm ("strong_replacement_closed", trivaxL (thm "M_triv_axioms.strong_replacement_closed"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   126
bind_thm ("RepFun_closed", trivaxL (thm "M_triv_axioms.RepFun_closed"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   127
bind_thm ("lam_closed", trivaxL (thm "M_triv_axioms.lam_closed"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   128
bind_thm ("image_abs", trivaxL (thm "M_triv_axioms.image_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   129
bind_thm ("powerset_Pow", trivaxL (thm "M_triv_axioms.powerset_Pow"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   130
bind_thm ("powerset_imp_subset_Pow", trivaxL (thm "M_triv_axioms.powerset_imp_subset_Pow"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   131
bind_thm ("nat_into_M", trivaxL (thm "M_triv_axioms.nat_into_M"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   132
bind_thm ("nat_case_closed", trivaxL (thm "M_triv_axioms.nat_case_closed"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   133
bind_thm ("Inl_in_M_iff", trivaxL (thm "M_triv_axioms.Inl_in_M_iff"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   134
bind_thm ("Inr_in_M_iff", trivaxL (thm "M_triv_axioms.Inr_in_M_iff"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   135
bind_thm ("lt_closed", trivaxL (thm "M_triv_axioms.lt_closed"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   136
bind_thm ("transitive_set_abs", trivaxL (thm "M_triv_axioms.transitive_set_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   137
bind_thm ("ordinal_abs", trivaxL (thm "M_triv_axioms.ordinal_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   138
bind_thm ("limit_ordinal_abs", trivaxL (thm "M_triv_axioms.limit_ordinal_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   139
bind_thm ("successor_ordinal_abs", trivaxL (thm "M_triv_axioms.successor_ordinal_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   140
bind_thm ("finite_ordinal_abs", trivaxL (thm "M_triv_axioms.finite_ordinal_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   141
bind_thm ("omega_abs", trivaxL (thm "M_triv_axioms.omega_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   142
bind_thm ("number1_abs", trivaxL (thm "M_triv_axioms.number1_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   143
bind_thm ("number1_abs", trivaxL (thm "M_triv_axioms.number1_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   144
bind_thm ("number3_abs", trivaxL (thm "M_triv_axioms.number3_abs"));
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   145
*}
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   146
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   147
declare ball_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   148
declare rall_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   149
declare bex_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   150
declare rex_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   151
declare empty_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   152
declare subset_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   153
declare upair_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   154
declare upair_in_M_iff [iff]
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   155
declare singleton_in_M_iff [iff]
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   156
declare pair_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   157
declare pair_in_M_iff [iff]
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   158
declare cartprod_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   159
declare union_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   160
declare inter_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   161
declare setdiff_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   162
declare Union_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   163
declare Union_closed [intro,simp]
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   164
declare Un_closed [intro,simp]
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   165
declare cons_closed [intro,simp]
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   166
declare successor_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   167
declare succ_in_M_iff [iff]
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   168
declare separation_closed [intro,simp]
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   169
declare strong_replacementI [rule_format]
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   170
declare strong_replacement_closed [intro,simp]
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   171
declare RepFun_closed [intro,simp]
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   172
declare lam_closed [intro,simp]
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   173
declare image_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   174
declare nat_into_M [intro]
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   175
declare Inl_in_M_iff [iff]
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   176
declare Inr_in_M_iff [iff]
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   177
declare transitive_set_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   178
declare ordinal_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   179
declare limit_ordinal_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   180
declare successor_ordinal_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   181
declare finite_ordinal_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   182
declare omega_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   183
declare number1_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   184
declare number1_abs [simp] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   185
declare number3_abs [simp]
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   186
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   187
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   188
subsection{*Instantiation of the locale @{text reflection}*}
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   189
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   190
text{*instances of locale constants*}
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   191
constdefs
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   192
  L_Reflects :: "[i=>o,i=>o,[i,i]=>o] => o"
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   193
    "L_Reflects(Cl,P,Q) == Closed_Unbounded(Cl) &
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   194
                           (\<forall>a. Cl(a) --> (\<forall>x \<in> Lset(a). P(x) <-> Q(a,x)))"
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   195
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   196
  L_F0 :: "[i=>o,i] => i"
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   197
    "L_F0(P,y) == \<mu>b. (\<exists>z. L(z) \<and> P(<y,z>)) --> (\<exists>z\<in>Lset(b). P(<y,z>))"
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   198
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   199
  L_FF :: "[i=>o,i] => i"
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   200
    "L_FF(P)   == \<lambda>a. \<Union>y\<in>Lset(a). L_F0(P,y)"
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   201
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   202
  L_ClEx :: "[i=>o,i] => o"
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   203
    "L_ClEx(P) == \<lambda>a. Limit(a) \<and> normalize(L_FF(P),a) = a"
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   204
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   205
theorem Triv_reflection [intro]:
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   206
     "L_Reflects(Ord, P, \<lambda>a x. P(x))"
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   207
by (simp add: L_Reflects_def)
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   208
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   209
theorem Not_reflection [intro]:
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   210
     "L_Reflects(Cl,P,Q) ==> L_Reflects(Cl, \<lambda>x. ~P(x), \<lambda>a x. ~Q(a,x))"
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   211
by (simp add: L_Reflects_def) 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   212
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   213
theorem And_reflection [intro]:
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   214
     "[| L_Reflects(Cl,P,Q); L_Reflects(C',P',Q') |] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   215
      ==> L_Reflects(\<lambda>a. Cl(a) \<and> C'(a), \<lambda>x. P(x) \<and> P'(x), 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   216
                                      \<lambda>a x. Q(a,x) \<and> Q'(a,x))"
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   217
by (simp add: L_Reflects_def Closed_Unbounded_Int, blast)
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   218
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   219
theorem Or_reflection [intro]:
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   220
     "[| L_Reflects(Cl,P,Q); L_Reflects(C',P',Q') |] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   221
      ==> L_Reflects(\<lambda>a. Cl(a) \<and> C'(a), \<lambda>x. P(x) \<or> P'(x), 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   222
                                      \<lambda>a x. Q(a,x) \<or> Q'(a,x))"
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   223
by (simp add: L_Reflects_def Closed_Unbounded_Int, blast)
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   224
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   225
theorem Imp_reflection [intro]:
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   226
     "[| L_Reflects(Cl,P,Q); L_Reflects(C',P',Q') |] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   227
      ==> L_Reflects(\<lambda>a. Cl(a) \<and> C'(a), 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   228
                   \<lambda>x. P(x) --> P'(x), 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   229
                   \<lambda>a x. Q(a,x) --> Q'(a,x))"
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   230
by (simp add: L_Reflects_def Closed_Unbounded_Int, blast)
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   231
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   232
theorem Iff_reflection [intro]:
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   233
     "[| L_Reflects(Cl,P,Q); L_Reflects(C',P',Q') |] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   234
      ==> L_Reflects(\<lambda>a. Cl(a) \<and> C'(a), 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   235
                   \<lambda>x. P(x) <-> P'(x), 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   236
                   \<lambda>a x. Q(a,x) <-> Q'(a,x))"
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   237
by (simp add: L_Reflects_def Closed_Unbounded_Int, blast) 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   238
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   239
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   240
theorem Ex_reflection [intro]:
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   241
     "L_Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))) 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   242
      ==> L_Reflects(\<lambda>a. Cl(a) \<and> L_ClEx(\<lambda>x. P(fst(x),snd(x)), a), 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   243
                   \<lambda>x. \<exists>z. L(z) \<and> P(x,z), 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   244
                   \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z))"
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   245
apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def) 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   246
apply (rule reflection.Ex_reflection [OF Lset_mono_le Lset_cont Pair_in_Lset],
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   247
       assumption+)
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   248
done
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   249
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   250
theorem All_reflection [intro]:
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   251
     "L_Reflects(Cl,  \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   252
      ==> L_Reflects(\<lambda>a. Cl(a) \<and> L_ClEx(\<lambda>x. ~P(fst(x),snd(x)), a), 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   253
                   \<lambda>x. \<forall>z. L(z) --> P(x,z), 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   254
                   \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z))" 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   255
apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def) 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   256
apply (rule reflection.All_reflection [OF Lset_mono_le Lset_cont Pair_in_Lset],
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   257
       assumption+)
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   258
done
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   259
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   260
theorem Rex_reflection [intro]:
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   261
     "L_Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))) 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   262
      ==> L_Reflects(\<lambda>a. Cl(a) \<and> L_ClEx(\<lambda>x. P(fst(x),snd(x)), a), 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   263
                   \<lambda>x. \<exists>z[L]. P(x,z), 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   264
                   \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z))"
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   265
by (unfold rex_def, blast) 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   266
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   267
theorem Rall_reflection [intro]:
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   268
     "L_Reflects(Cl,  \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   269
      ==> L_Reflects(\<lambda>a. Cl(a) \<and> L_ClEx(\<lambda>x. ~P(fst(x),snd(x)), a), 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   270
                   \<lambda>x. \<forall>z[L]. P(x,z), 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   271
                   \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z))" 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   272
by (unfold rall_def, blast) 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   273
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   274
lemma ReflectsD:
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   275
     "[|L_Reflects(Cl,P,Q); Ord(i)|] 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   276
      ==> \<exists>j. i<j & (\<forall>x \<in> Lset(j). P(x) <-> Q(j,x))"
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   277
apply (simp add: L_Reflects_def Closed_Unbounded_def, clarify)
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   278
apply (blast dest!: UnboundedD) 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   279
done
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   280
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   281
lemma ReflectsE:
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   282
     "[| L_Reflects(Cl,P,Q); Ord(i);
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   283
         !!j. [|i<j;  \<forall>x \<in> Lset(j). P(x) <-> Q(j,x)|] ==> R |]
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   284
      ==> R"
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   285
by (blast dest!: ReflectsD) 
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   286
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   287
lemma Collect_mem_eq: "{x\<in>A. x\<in>B} = A \<inter> B";
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   288
by blast
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   289
a73ab154f75c towards proving separation for L
paulson
parents: 13269
diff changeset
   290
13298
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   291
subsection{*Internalized formulas for some relativized ones*}
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   292
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   293
subsubsection{*Unordered pairs*}
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   294
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   295
constdefs upair_fm :: "[i,i,i]=>i"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   296
    "upair_fm(x,y,z) == 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   297
       And(Member(x,z), 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   298
           And(Member(y,z),
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   299
               Forall(Implies(Member(0,succ(z)), 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   300
                              Or(Equal(0,succ(x)), Equal(0,succ(y)))))))"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   301
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   302
lemma upair_type [TC]:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   303
     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> upair_fm(x,y,z) \<in> formula"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   304
by (simp add: upair_fm_def) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   305
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   306
lemma arity_upair_fm [simp]:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   307
     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   308
      ==> arity(upair_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   309
by (simp add: upair_fm_def succ_Un_distrib [symmetric] Un_ac) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   310
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   311
lemma sats_upair_fm [simp]:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   312
   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   313
    ==> sats(A, upair_fm(x,y,z), env) <-> 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   314
            upair(**A, nth(x,env), nth(y,env), nth(z,env))"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   315
by (simp add: upair_fm_def upair_def)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   316
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   317
lemma upair_iff_sats:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   318
      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   319
          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   320
       ==> upair(**A, x, y, z) <-> sats(A, upair_fm(i,j,k), env)"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   321
by (simp add: sats_upair_fm)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   322
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   323
text{*Useful? At least it refers to "real" unordered pairs*}
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   324
lemma sats_upair_fm2 [simp]:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   325
   "[| x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A); Transset(A)|]
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   326
    ==> sats(A, upair_fm(x,y,z), env) <-> 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   327
        nth(z,env) = {nth(x,env), nth(y,env)}"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   328
apply (frule lt_length_in_nat, assumption)  
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   329
apply (simp add: upair_fm_def Transset_def, auto) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   330
apply (blast intro: nth_type) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   331
done
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   332
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   333
subsubsection{*Ordered pairs*}
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   334
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   335
constdefs pair_fm :: "[i,i,i]=>i"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   336
    "pair_fm(x,y,z) == 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   337
       Exists(And(upair_fm(succ(x),succ(x),0),
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   338
              Exists(And(upair_fm(succ(succ(x)),succ(succ(y)),0),
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   339
                         upair_fm(1,0,succ(succ(z)))))))"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   340
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   341
lemma pair_type [TC]:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   342
     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> pair_fm(x,y,z) \<in> formula"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   343
by (simp add: pair_fm_def) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   344
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   345
lemma arity_pair_fm [simp]:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   346
     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   347
      ==> arity(pair_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   348
by (simp add: pair_fm_def succ_Un_distrib [symmetric] Un_ac) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   349
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   350
lemma sats_pair_fm [simp]:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   351
   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   352
    ==> sats(A, pair_fm(x,y,z), env) <-> 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   353
        pair(**A, nth(x,env), nth(y,env), nth(z,env))"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   354
by (simp add: pair_fm_def pair_def)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   355
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   356
lemma pair_iff_sats:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   357
      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   358
          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   359
       ==> pair(**A, x, y, z) <-> sats(A, pair_fm(i,j,k), env)"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   360
by (simp add: sats_pair_fm)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   361
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   362
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   363
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   364
subsection{*Proving instances of Separation using Reflection!*}
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   365
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   366
text{*Helps us solve for de Bruijn indices!*}
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   367
lemma nth_ConsI: "[|nth(n,l) = x; n \<in> nat|] ==> nth(succ(n), Cons(a,l)) = x"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   368
by simp
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   369
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   370
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   371
lemma Collect_conj_in_DPow:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   372
     "[| {x\<in>A. P(x)} \<in> DPow(A);  {x\<in>A. Q(x)} \<in> DPow(A) |] 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   373
      ==> {x\<in>A. P(x) & Q(x)} \<in> DPow(A)"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   374
by (simp add: Int_in_DPow Collect_Int_Collect_eq [symmetric]) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   375
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   376
lemma Collect_conj_in_DPow_Lset:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   377
     "[|z \<in> Lset(j); {x \<in> Lset(j). P(x)} \<in> DPow(Lset(j))|]
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   378
      ==> {x \<in> Lset(j). x \<in> z & P(x)} \<in> DPow(Lset(j))"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   379
apply (frule mem_Lset_imp_subset_Lset)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   380
apply (simp add: Collect_conj_in_DPow Collect_mem_eq 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   381
                 subset_Int_iff2 elem_subset_in_DPow)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   382
done
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   383
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   384
lemma separation_CollectI:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   385
     "(\<And>z. L(z) ==> L({x \<in> z . P(x)})) ==> separation(L, \<lambda>x. P(x))"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   386
apply (unfold separation_def, clarify) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   387
apply (rule_tac x="{x\<in>z. P(x)}" in rexI) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   388
apply simp_all
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   389
done
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   390
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   391
text{*Reduces the original comprehension to the reflected one*}
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   392
lemma reflection_imp_L_separation:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   393
      "[| \<forall>x\<in>Lset(j). P(x) <-> Q(x);
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   394
          {x \<in> Lset(j) . Q(x)} \<in> DPow(Lset(j)); 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   395
          Ord(j);  z \<in> Lset(j)|] ==> L({x \<in> z . P(x)})"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   396
apply (rule_tac i = "succ(j)" in L_I)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   397
 prefer 2 apply simp
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   398
apply (subgoal_tac "{x \<in> z. P(x)} = {x \<in> Lset(j). x \<in> z & (Q(x))}")
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   399
 prefer 2
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   400
 apply (blast dest: mem_Lset_imp_subset_Lset) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   401
apply (simp add: Lset_succ Collect_conj_in_DPow_Lset)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   402
done
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   403
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   404
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   405
subsubsection{*Separation for Intersection*}
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   406
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   407
lemma Inter_Reflects:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   408
     "L_Reflects(?Cl, \<lambda>x. \<forall>y[L]. y\<in>A --> x \<in> y, 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   409
               \<lambda>i x. \<forall>y\<in>Lset(i). y\<in>A --> x \<in> y)"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   410
by fast
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   411
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   412
lemma Inter_separation:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   413
     "L(A) ==> separation(L, \<lambda>x. \<forall>y[L]. y\<in>A --> x\<in>y)"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   414
apply (rule separation_CollectI) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   415
apply (rule_tac A="{A,z}" in subset_LsetE, blast ) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   416
apply (rule ReflectsE [OF Inter_Reflects], assumption)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   417
apply (drule subset_Lset_ltD, assumption) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   418
apply (erule reflection_imp_L_separation)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   419
  apply (simp_all add: lt_Ord2, clarify)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   420
apply (rule DPowI2) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   421
apply (rule ball_iff_sats) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   422
apply (rule imp_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   423
apply (rule_tac [2] i=1 and j=0 and env="[y,x,A]" in mem_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   424
apply (rule_tac i=0 and j=2 in mem_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   425
apply (simp_all add: succ_Un_distrib [symmetric])
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   426
done
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   427
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   428
subsubsection{*Separation for Cartesian Product*}
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   429
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   430
text{*The @{text simplified} attribute tidies up the reflecting class.*}
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   431
theorem upair_reflection [simplified,intro]:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   432
     "L_Reflects(?Cl, \<lambda>x. upair(L,f(x),g(x),h(x)), 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   433
                    \<lambda>i x. upair(**Lset(i),f(x),g(x),h(x)))" 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   434
by (simp add: upair_def, fast) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   435
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   436
theorem pair_reflection [simplified,intro]:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   437
     "L_Reflects(?Cl, \<lambda>x. pair(L,f(x),g(x),h(x)), 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   438
                    \<lambda>i x. pair(**Lset(i),f(x),g(x),h(x)))"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   439
by (simp only: pair_def rex_setclass_is_bex, fast) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   440
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   441
lemma cartprod_Reflects [simplified]:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   442
     "L_Reflects(?Cl, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)),
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   443
                \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). y\<in>B & 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   444
                               pair(**Lset(i),x,y,z)))"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   445
by fast
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   446
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   447
lemma cartprod_separation:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   448
     "[| L(A); L(B) |] 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   449
      ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)))"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   450
apply (rule separation_CollectI) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   451
apply (rule_tac A="{A,B,z}" in subset_LsetE, blast ) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   452
apply (rule ReflectsE [OF cartprod_Reflects], assumption)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   453
apply (drule subset_Lset_ltD, assumption) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   454
apply (erule reflection_imp_L_separation)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   455
  apply (simp_all add: lt_Ord2, clarify) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   456
apply (rule DPowI2)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   457
apply (rename_tac u)  
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   458
apply (rule bex_iff_sats) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   459
apply (rule conj_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   460
apply (rule_tac i=0 and j=2 and env="[x,u,A,B]" in mem_iff_sats, simp_all)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   461
apply (rule bex_iff_sats) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   462
apply (rule conj_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   463
apply (rule mem_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   464
apply (blast intro: nth_0 nth_ConsI) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   465
apply (blast intro: nth_0 nth_ConsI, simp_all)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   466
apply (rule_tac i=1 and j=0 and k=2 in pair_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   467
apply (simp_all add: succ_Un_distrib [symmetric])
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   468
done
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   469
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   470
subsubsection{*Separation for Image*}
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   471
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   472
text{*No @{text simplified} here: it simplifies the occurrence of 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   473
      the predicate @{term pair}!*}
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   474
lemma image_Reflects:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   475
     "L_Reflects(?Cl, \<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)),
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   476
           \<lambda>i y. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). x\<in>A & pair(**Lset(i),x,y,p)))"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   477
by fast
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   478
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   479
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   480
lemma image_separation:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   481
     "[| L(A); L(r) |] 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   482
      ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)))"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   483
apply (rule separation_CollectI) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   484
apply (rule_tac A="{A,r,z}" in subset_LsetE, blast ) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   485
apply (rule ReflectsE [OF image_Reflects], assumption)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   486
apply (drule subset_Lset_ltD, assumption) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   487
apply (erule reflection_imp_L_separation)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   488
  apply (simp_all add: lt_Ord2, clarify)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   489
apply (rule DPowI2)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   490
apply (rule bex_iff_sats) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   491
apply (rule conj_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   492
apply (rule_tac env="[p,y,A,r]" in mem_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   493
apply (blast intro: nth_0 nth_ConsI) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   494
apply (blast intro: nth_0 nth_ConsI, simp_all)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   495
apply (rule bex_iff_sats) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   496
apply (rule conj_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   497
apply (rule mem_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   498
apply (blast intro: nth_0 nth_ConsI) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   499
apply (blast intro: nth_0 nth_ConsI, simp_all)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   500
apply (rule pair_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   501
apply (blast intro: nth_0 nth_ConsI) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   502
apply (blast intro: nth_0 nth_ConsI) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   503
apply (blast intro: nth_0 nth_ConsI)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   504
apply (simp_all add: succ_Un_distrib [symmetric])
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   505
done
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   506
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   507
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   508
subsubsection{*Separation for Converse*}
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   509
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   510
lemma converse_Reflects:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   511
     "L_Reflects(?Cl, 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   512
        \<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)),
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   513
     \<lambda>i z. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i). 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   514
                     pair(**Lset(i),x,y,p) & pair(**Lset(i),y,x,z)))"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   515
by fast
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   516
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   517
lemma converse_separation:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   518
     "L(r) ==> separation(L, 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   519
         \<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)))"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   520
apply (rule separation_CollectI) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   521
apply (rule_tac A="{r,z}" in subset_LsetE, blast ) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   522
apply (rule ReflectsE [OF converse_Reflects], assumption)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   523
apply (drule subset_Lset_ltD, assumption) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   524
apply (erule reflection_imp_L_separation)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   525
  apply (simp_all add: lt_Ord2, clarify)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   526
apply (rule DPowI2)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   527
apply (rename_tac u) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   528
apply (rule bex_iff_sats) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   529
apply (rule conj_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   530
apply (rule_tac i=0 and j="2" and env="[p,u,r]" in mem_iff_sats, simp_all)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   531
apply (rule bex_iff_sats) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   532
apply (rule bex_iff_sats) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   533
apply (rule conj_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   534
apply (rule_tac i=1 and j=0 and k=2 in pair_iff_sats, simp_all)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   535
apply (rule pair_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   536
apply (blast intro: nth_0 nth_ConsI) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   537
apply (blast intro: nth_0 nth_ConsI) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   538
apply (blast intro: nth_0 nth_ConsI)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   539
apply (simp_all add: succ_Un_distrib [symmetric])
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   540
done
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   541
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   542
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   543
subsubsection{*Separation for Restriction*}
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   544
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   545
lemma restrict_Reflects:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   546
     "L_Reflects(?Cl, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)),
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   547
        \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). pair(**Lset(i),x,y,z)))"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   548
by fast
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   549
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   550
lemma restrict_separation:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   551
   "L(A) ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)))"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   552
apply (rule separation_CollectI) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   553
apply (rule_tac A="{A,z}" in subset_LsetE, blast ) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   554
apply (rule ReflectsE [OF restrict_Reflects], assumption)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   555
apply (drule subset_Lset_ltD, assumption) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   556
apply (erule reflection_imp_L_separation)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   557
  apply (simp_all add: lt_Ord2, clarify)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   558
apply (rule DPowI2)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   559
apply (rename_tac u) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   560
apply (rule bex_iff_sats) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   561
apply (rule conj_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   562
apply (rule_tac i=0 and j="2" and env="[x,u,A]" in mem_iff_sats, simp_all)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   563
apply (rule bex_iff_sats) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   564
apply (rule_tac i=1 and j=0 and k=2 in pair_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   565
apply (simp_all add: succ_Un_distrib [symmetric])
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   566
done
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   567
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   568
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   569
subsubsection{*Separation for Composition*}
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   570
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   571
lemma comp_Reflects:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   572
     "L_Reflects(?Cl, \<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L]. 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   573
		  pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) & 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   574
                  xy\<in>s & yz\<in>r,
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   575
        \<lambda>i xz. \<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i). \<exists>z\<in>Lset(i). \<exists>xy\<in>Lset(i). \<exists>yz\<in>Lset(i). 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   576
		  pair(**Lset(i),x,z,xz) & pair(**Lset(i),x,y,xy) & 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   577
                  pair(**Lset(i),y,z,yz) & xy\<in>s & yz\<in>r)"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   578
by fast
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   579
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   580
lemma comp_separation:
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   581
     "[| L(r); L(s) |]
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   582
      ==> separation(L, \<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L]. 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   583
		  pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) & 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   584
                  xy\<in>s & yz\<in>r)"
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   585
apply (rule separation_CollectI) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   586
apply (rule_tac A="{r,s,z}" in subset_LsetE, blast ) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   587
apply (rule ReflectsE [OF comp_Reflects], assumption)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   588
apply (drule subset_Lset_ltD, assumption) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   589
apply (erule reflection_imp_L_separation)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   590
  apply (simp_all add: lt_Ord2, clarify)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   591
apply (rule DPowI2)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   592
apply (rename_tac u) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   593
apply (rule bex_iff_sats)+
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   594
apply (rename_tac x y z)  
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   595
apply (rule conj_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   596
apply (rule_tac env="[z,y,x,u,r,s]" in pair_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   597
apply (blast intro: nth_0 nth_ConsI) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   598
apply (blast intro: nth_0 nth_ConsI) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   599
apply (blast intro: nth_0 nth_ConsI, simp_all)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   600
apply (rule bex_iff_sats) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   601
apply (rule conj_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   602
apply (rule pair_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   603
apply (blast intro: nth_0 nth_ConsI) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   604
apply (blast intro: nth_0 nth_ConsI) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   605
apply (blast intro: nth_0 nth_ConsI, simp_all)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   606
apply (rule bex_iff_sats) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   607
apply (rule conj_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   608
apply (rule pair_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   609
apply (blast intro: nth_0 nth_ConsI) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   610
apply (blast intro: nth_0 nth_ConsI) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   611
apply (blast intro: nth_0 nth_ConsI, simp_all) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   612
apply (rule conj_iff_sats)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   613
apply (rule mem_iff_sats) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   614
apply (blast intro: nth_0 nth_ConsI) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   615
apply (blast intro: nth_0 nth_ConsI, simp) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   616
apply (rule mem_iff_sats) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   617
apply (blast intro: nth_0 nth_ConsI) 
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   618
apply (blast intro: nth_0 nth_ConsI)
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   619
apply (simp_all add: succ_Un_distrib [symmetric])
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   620
done
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   621
13304
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   622
subsubsection{*Separation for Predecessors in an Order*}
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   623
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   624
lemma pred_Reflects:
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   625
     "L_Reflects(?Cl, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p),
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   626
                    \<lambda>i y. \<exists>p \<in> Lset(i). p\<in>r & pair(**Lset(i),y,x,p))"
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   627
by fast
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   628
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   629
lemma pred_separation:
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   630
     "[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p))"
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   631
apply (rule separation_CollectI) 
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   632
apply (rule_tac A="{r,x,z}" in subset_LsetE, blast ) 
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   633
apply (rule ReflectsE [OF pred_Reflects], assumption)
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   634
apply (drule subset_Lset_ltD, assumption) 
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   635
apply (erule reflection_imp_L_separation)
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   636
  apply (simp_all add: lt_Ord2, clarify)
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   637
apply (rule DPowI2)
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   638
apply (rename_tac u) 
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   639
apply (rule bex_iff_sats)
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   640
apply (rule conj_iff_sats)
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   641
apply (rule_tac env = "[p,u,r,x]" in mem_iff_sats) 
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   642
apply (blast intro: nth_0 nth_ConsI) 
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   643
apply (blast intro: nth_0 nth_ConsI, simp) 
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   644
apply (rule pair_iff_sats)
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   645
apply (blast intro: nth_0 nth_ConsI) 
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   646
apply (blast intro: nth_0 nth_ConsI) 
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   647
apply (blast intro: nth_0 nth_ConsI, simp_all)
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   648
apply (simp_all add: succ_Un_distrib [symmetric])
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   649
done
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   650
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   651
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   652
subsubsection{*Separation for the Membership Relation*}
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   653
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   654
lemma Memrel_Reflects:
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   655
     "L_Reflects(?Cl, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y,
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   656
            \<lambda>i z. \<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). pair(**Lset(i),x,y,z) & x \<in> y)"
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   657
by fast
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   658
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   659
lemma Memrel_separation:
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   660
     "separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)"
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   661
apply (rule separation_CollectI) 
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   662
apply (rule_tac A="{z}" in subset_LsetE, blast ) 
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   663
apply (rule ReflectsE [OF Memrel_Reflects], assumption)
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   664
apply (drule subset_Lset_ltD, assumption) 
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   665
apply (erule reflection_imp_L_separation)
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   666
  apply (simp_all add: lt_Ord2)
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   667
apply (rule DPowI2)
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   668
apply (rename_tac u) 
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   669
apply (rule bex_iff_sats)+
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   670
apply (rule conj_iff_sats)
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   671
apply (rule_tac env = "[y,x,u]" in pair_iff_sats) 
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   672
apply (blast intro: nth_0 nth_ConsI) 
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   673
apply (blast intro: nth_0 nth_ConsI) 
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   674
apply (blast intro: nth_0 nth_ConsI, simp_all) 
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   675
apply (rule mem_iff_sats)
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   676
apply (blast intro: nth_0 nth_ConsI) 
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   677
apply (blast intro: nth_0 nth_ConsI)
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   678
apply (simp_all add: succ_Un_distrib [symmetric])
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   679
done
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   680
43ef6c6dd906 more separation instances
paulson
parents: 13299
diff changeset
   681
13298
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   682
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   683
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13291
diff changeset
   684
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   685
end