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