src/ZF/Constructible/L_axioms.thy
 changeset 13339 0f89104dd377 parent 13323 2c287f50c9f3 child 13348 374d05460db4
```     1.1 --- a/src/ZF/Constructible/L_axioms.thy	Wed Jul 10 16:07:52 2002 +0200
1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Wed Jul 10 16:54:07 2002 +0200
1.3 @@ -1,9 +1,8 @@
1.4 -header {*The Class L Satisfies the ZF Axioms*}
1.5 +header {*The ZF Axioms (Except Separation) in L*}
1.6
1.7  theory L_axioms = Formula + Relative + Reflection + MetaExists:
1.8
1.9 -
1.10 -text {* The class L satisfies the premises of locale @{text M_axioms} *}
1.11 +text {* The class L satisfies the premises of locale @{text M_triv_axioms} *}
1.12
1.13  lemma transL: "[| y\<in>x; L(x) |] ==> L(y)"
1.14  apply (insert Transset_Lset)
1.15 @@ -47,7 +46,7 @@
1.16         in exI)
1.17  apply simp
1.18  apply clarify
1.19 -apply (rule_tac a="x" in UN_I)
1.20 +apply (rule_tac a=x in UN_I)
1.21   apply (simp_all add: Replace_iff univalent_def)
1.22  apply (blast dest: transL L_I)
1.23  done
1.24 @@ -316,7 +315,7 @@
1.25  by blast
1.26
1.27
1.28 -subsection{*Internalized formulas for some relativized ones*}
1.29 +subsection{*Internalized Formulas for some Set-Theoretic Concepts*}
1.30
1.31  lemmas setclass_simps = rall_setclass_is_ball rex_setclass_is_bex
1.32
1.33 @@ -341,7 +340,7 @@
1.34     "9"  == "succ(8)"
1.35
1.36
1.37 -subsubsection{*The Empty Set*}
1.38 +subsubsection{*The Empty Set, Internalized*}
1.39
1.40  constdefs empty_fm :: "i=>i"
1.41      "empty_fm(x) == Forall(Neg(Member(0,succ(x))))"
1.42 @@ -373,7 +372,7 @@
1.43  done
1.44
1.45
1.46 -subsubsection{*Unordered pairs*}
1.47 +subsubsection{*Unordered Pairs, Internalized*}
1.48
1.49  constdefs upair_fm :: "[i,i,i]=>i"
1.50      "upair_fm(x,y,z) ==
1.51 @@ -420,7 +419,7 @@
1.52  apply (intro FOL_reflections)
1.53  done
1.54
1.55 -subsubsection{*Ordered pairs*}
1.56 +subsubsection{*Ordered pairs, Internalized*}
1.57
1.58  constdefs pair_fm :: "[i,i,i]=>i"
1.59      "pair_fm(x,y,z) ==
1.60 @@ -457,7 +456,7 @@
1.61  done
1.62
1.63
1.64 -subsubsection{*Binary Unions*}
1.65 +subsubsection{*Binary Unions, Internalized*}
1.66
1.67  constdefs union_fm :: "[i,i,i]=>i"
1.68      "union_fm(x,y,z) ==
1.69 @@ -493,7 +492,7 @@
1.70  done
1.71
1.72
1.73 -subsubsection{*`Cons' for sets*}
1.74 +subsubsection{*Set ``Cons,'' Internalized*}
1.75
1.76  constdefs cons_fm :: "[i,i,i]=>i"
1.77      "cons_fm(x,y,z) ==
1.78 @@ -530,7 +529,7 @@
1.79  done
1.80
1.81
1.82 -subsubsection{*Successor Function*}
1.83 +subsubsection{*Successor Function, Internalized*}
1.84
1.85  constdefs succ_fm :: "[i,i]=>i"
1.86      "succ_fm(x,y) == cons_fm(x,x,y)"
1.87 @@ -564,7 +563,7 @@
1.88  done
1.89
1.90
1.91 -subsubsection{*Function Applications*}
1.92 +subsubsection{*Function Application, Internalized*}
1.93
1.94  constdefs fun_apply_fm :: "[i,i,i]=>i"
1.95      "fun_apply_fm(f,x,y) ==
1.96 @@ -647,7 +646,7 @@
1.97  done
1.98
1.99
1.100 -subsubsection{*Membership Relation*}
1.101 +subsubsection{*Membership Relation, Internalized*}
1.102
1.103  constdefs Memrel_fm :: "[i,i]=>i"
1.104      "Memrel_fm(A,r) ==
1.105 @@ -685,7 +684,7 @@
1.106  apply (intro FOL_reflections pair_reflection)
1.107  done
1.108
1.109 -subsubsection{*Predecessor Set*}
1.110 +subsubsection{*Predecessor Set, Internalized*}
1.111
1.112  constdefs pred_set_fm :: "[i,i,i,i]=>i"
1.113      "pred_set_fm(A,x,r,B) ==
1.114 @@ -726,7 +725,7 @@
1.115
1.116
1.117
1.118 -subsubsection{*Domain*}
1.119 +subsubsection{*Domain of a Relation, Internalized*}
1.120
1.121  (* "is_domain(M,r,z) ==
1.122  	\<forall>x[M]. (x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w))))" *)
1.123 @@ -765,7 +764,7 @@
1.124  done
1.125
1.126
1.127 -subsubsection{*Range*}
1.128 +subsubsection{*Range of a Relation, Internalized*}
1.129
1.130  (* "is_range(M,r,z) ==
1.131  	\<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w))))" *)
1.132 @@ -804,7 +803,7 @@
1.133  done
1.134
1.135
1.136 -subsubsection{*Field*}
1.137 +subsubsection{*Field of a Relation, Internalized*}
1.138
1.139  (* "is_field(M,r,z) ==
1.140  	\<exists>dr[M]. is_domain(M,r,dr) &
1.141 @@ -845,7 +844,7 @@
1.142  done
1.143
1.144
1.145 -subsubsection{*Image*}
1.146 +subsubsection{*Image under a Relation, Internalized*}
1.147
1.148  (* "image(M,r,A,z) ==
1.149          \<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w))))" *)
1.150 @@ -885,7 +884,7 @@
1.151  done
1.152
1.153
1.154 -subsubsection{*The Concept of Relation*}
1.155 +subsubsection{*The Concept of Relation, Internalized*}
1.156
1.157  (* "is_relation(M,r) ==
1.158          (\<forall>z[M]. z\<in>r --> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))" *)
1.159 @@ -920,7 +919,7 @@
1.160  done
1.161
1.162
1.163 -subsubsection{*The Concept of Function*}
1.164 +subsubsection{*The Concept of Function, Internalized*}
1.165
1.166  (* "is_function(M,r) ==
1.167  	\<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M].
1.168 @@ -960,7 +959,7 @@
1.169  done
1.170
1.171
1.172 -subsubsection{*Typed Functions*}
1.173 +subsubsection{*Typed Functions, Internalized*}
1.174
1.175  (* "typed_function(M,A,B,r) ==
1.176          is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
1.177 @@ -1021,7 +1020,7 @@
1.178  done
1.179
1.180
1.181 -subsubsection{*Composition of Relations*}
1.182 +subsubsection{*Composition of Relations, Internalized*}
1.183
1.184  (* "composition(M,r,s,t) ==
1.185          \<forall>p[M]. p \<in> t <->
1.186 @@ -1066,7 +1065,7 @@
1.187  done
1.188
1.189
1.190 -subsubsection{*Injections*}
1.191 +subsubsection{*Injections, Internalized*}
1.192
1.193  (* "injection(M,A,B,f) ==
1.194  	typed_function(M,A,B,f) &
1.195 @@ -1111,7 +1110,7 @@
1.196  done
1.197
1.198
1.199 -subsubsection{*Surjections*}
1.200 +subsubsection{*Surjections, Internalized*}
1.201
1.202  (*  surjection :: "[i=>o,i,i,i] => o"
1.203      "surjection(M,A,B,f) ==
1.204 @@ -1154,7 +1153,7 @@
1.205
1.206
1.207
1.208 -subsubsection{*Bijections*}
1.209 +subsubsection{*Bijections, Internalized*}
1.210
1.211  (*   bijection :: "[i=>o,i,i,i] => o"
1.212      "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)" *)
1.213 @@ -1190,7 +1189,7 @@
1.214  done
1.215
1.216
1.217 -subsubsection{*Order-Isomorphisms*}
1.218 +subsubsection{*Order-Isomorphisms, Internalized*}
1.219
1.220  (*  order_isomorphism :: "[i=>o,i,i,i,i,i] => o"
1.221     "order_isomorphism(M,A,r,B,s,f) ==
1.222 @@ -1246,7 +1245,7 @@
1.223  apply (intro FOL_reflections function_reflections bijection_reflection)
1.224  done
1.225
1.226 -subsubsection{*Limit Ordinals*}
1.227 +subsubsection{*Limit Ordinals, Internalized*}
1.228
1.229  text{*A limit ordinal is a non-empty, successor-closed ordinal*}
1.230
```