author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46953  2b6e55924af3 
child 52458  210bca64b894 
permissions  rwrr 
13505  1 
(* Title: ZF/Constructible/Relative.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3 
*) 

4 

13223  5 
header {*Relativization and Absoluteness*} 
6 

16417  7 
theory Relative imports Main begin 
13223  8 

9 
subsection{* Relativized versions of standard settheoretic concepts *} 

10 

21233  11 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

12 
empty :: "[i=>o,i] => o" where 
13254  13 
"empty(M,z) == \<forall>x[M]. x \<notin> z" 
13223  14 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

15 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

16 
subset :: "[i=>o,i,i] => o" where 
46823  17 
"subset(M,A,B) == \<forall>x[M]. x\<in>A \<longrightarrow> x \<in> B" 
13223  18 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

19 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

20 
upair :: "[i=>o,i,i,i] => o" where 
46823  21 
"upair(M,a,b,z) == a \<in> z & b \<in> z & (\<forall>x[M]. x\<in>z \<longrightarrow> x = a  x = b)" 
13223  22 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

23 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

24 
pair :: "[i=>o,i,i,i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

25 
"pair(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) & 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

26 
(\<exists>y[M]. upair(M,a,b,y) & upair(M,x,y,z))" 
13223  27 

13306  28 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

29 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

30 
union :: "[i=>o,i,i,i] => o" where 
46823  31 
"union(M,a,b,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> x \<in> a  x \<in> b" 
13245  32 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

33 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

34 
is_cons :: "[i=>o,i,i,i] => o" where 
13306  35 
"is_cons(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) & union(M,x,b,z)" 
36 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

37 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

38 
successor :: "[i=>o,i,i] => o" where 
13306  39 
"successor(M,a,z) == is_cons(M,a,a,z)" 
13223  40 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

41 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

42 
number1 :: "[i=>o,i] => o" where 
13436  43 
"number1(M,a) == \<exists>x[M]. empty(M,x) & successor(M,x,a)" 
13363  44 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

45 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

46 
number2 :: "[i=>o,i] => o" where 
13436  47 
"number2(M,a) == \<exists>x[M]. number1(M,x) & successor(M,x,a)" 
13363  48 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

49 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

50 
number3 :: "[i=>o,i] => o" where 
13436  51 
"number3(M,a) == \<exists>x[M]. number2(M,x) & successor(M,x,a)" 
13363  52 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

53 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

54 
powerset :: "[i=>o,i,i] => o" where 
46823  55 
"powerset(M,A,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> subset(M,x,A)" 
13223  56 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

57 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

58 
is_Collect :: "[i=>o,i,i=>o,i] => o" where 
46823  59 
"is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> x \<in> A & P(x)" 
13436  60 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

61 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

62 
is_Replace :: "[i=>o,i,[i,i]=>o,i] => o" where 
46823  63 
"is_Replace(M,A,P,z) == \<forall>u[M]. u \<in> z \<longleftrightarrow> (\<exists>x[M]. x\<in>A & P(x,u))" 
13505  64 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

65 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

66 
inter :: "[i=>o,i,i,i] => o" where 
46823  67 
"inter(M,a,b,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> x \<in> a & x \<in> b" 
13223  68 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

69 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

70 
setdiff :: "[i=>o,i,i,i] => o" where 
46823  71 
"setdiff(M,a,b,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> x \<in> a & x \<notin> b" 
13223  72 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

73 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

74 
big_union :: "[i=>o,i,i] => o" where 
46823  75 
"big_union(M,A,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> (\<exists>y[M]. y\<in>A & x \<in> y)" 
13223  76 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

77 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

78 
big_inter :: "[i=>o,i,i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

79 
"big_inter(M,A,z) == 
46823  80 
(A=0 \<longrightarrow> z=0) & 
81 
(A\<noteq>0 \<longrightarrow> (\<forall>x[M]. x \<in> z \<longleftrightarrow> (\<forall>y[M]. y\<in>A \<longrightarrow> x \<in> y)))" 

13223  82 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

83 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

84 
cartprod :: "[i=>o,i,i,i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

85 
"cartprod(M,A,B,z) == 
46823  86 
\<forall>u[M]. u \<in> z \<longleftrightarrow> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))" 
13223  87 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

88 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

89 
is_sum :: "[i=>o,i,i,i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

90 
"is_sum(M,A,B,Z) == 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

91 
\<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M]. 
13350  92 
number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) & 
93 
cartprod(M,s1,B,B1) & union(M,A0,B1,Z)" 

94 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

95 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

96 
is_Inl :: "[i=>o,i,i] => o" where 
13397  97 
"is_Inl(M,a,z) == \<exists>zero[M]. empty(M,zero) & pair(M,zero,a,z)" 
98 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

99 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

100 
is_Inr :: "[i=>o,i,i] => o" where 
13397  101 
"is_Inr(M,a,z) == \<exists>n1[M]. number1(M,n1) & pair(M,n1,a,z)" 
102 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

103 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

104 
is_converse :: "[i=>o,i,i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

105 
"is_converse(M,r,z) == 
46823  106 
\<forall>x[M]. x \<in> z \<longleftrightarrow> 
13299  107 
(\<exists>w[M]. w\<in>r & (\<exists>u[M]. \<exists>v[M]. pair(M,u,v,w) & pair(M,v,u,x)))" 
13223  108 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

109 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

110 
pre_image :: "[i=>o,i,i,i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

111 
"pre_image(M,r,A,z) == 
46823  112 
\<forall>x[M]. x \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))" 
13223  113 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

114 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

115 
is_domain :: "[i=>o,i,i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

116 
"is_domain(M,r,z) == 
46823  117 
\<forall>x[M]. x \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w)))" 
13223  118 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

119 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

120 
image :: "[i=>o,i,i,i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

121 
"image(M,r,A,z) == 
46823  122 
\<forall>y[M]. y \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w)))" 
13223  123 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

124 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

125 
is_range :: "[i=>o,i,i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

126 
{*the cleaner 
13299  127 
@{term "\<exists>r'[M]. is_converse(M,r,r') & is_domain(M,r',z)"} 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

128 
unfortunately needs an instance of separation in order to prove 
13223  129 
@{term "M(converse(r))"}.*} 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

130 
"is_range(M,r,z) == 
46823  131 
\<forall>y[M]. y \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w)))" 
13223  132 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

133 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

134 
is_field :: "[i=>o,i,i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

135 
"is_field(M,r,z) == 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
22710
diff
changeset

136 
\<exists>dr[M]. \<exists>rr[M]. is_domain(M,r,dr) & is_range(M,r,rr) & 
13436  137 
union(M,dr,rr,z)" 
13245  138 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

139 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

140 
is_relation :: "[i=>o,i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

141 
"is_relation(M,r) == 
46823  142 
(\<forall>z[M]. z\<in>r \<longrightarrow> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))" 
13223  143 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

144 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

145 
is_function :: "[i=>o,i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

146 
"is_function(M,r) == 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
22710
diff
changeset

147 
\<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M]. 
46823  148 
pair(M,x,y,p) \<longrightarrow> pair(M,x,y',p') \<longrightarrow> p\<in>r \<longrightarrow> p'\<in>r \<longrightarrow> y=y'" 
13223  149 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

150 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

151 
fun_apply :: "[i=>o,i,i,i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

152 
"fun_apply(M,f,x,y) == 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

153 
(\<exists>xs[M]. \<exists>fxs[M]. 
13352  154 
upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))" 
13223  155 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

156 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

157 
typed_function :: "[i=>o,i,i,i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

158 
"typed_function(M,A,B,r) == 
13223  159 
is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) & 
46823  160 
(\<forall>u[M]. u\<in>r \<longrightarrow> (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) \<longrightarrow> y\<in>B))" 
13223  161 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

162 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

163 
is_funspace :: "[i=>o,i,i,i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

164 
"is_funspace(M,A,B,F) == 
46823  165 
\<forall>f[M]. f \<in> F \<longleftrightarrow> typed_function(M,A,B,f)" 
13268  166 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

167 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

168 
composition :: "[i=>o,i,i,i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

169 
"composition(M,r,s,t) == 
46823  170 
\<forall>p[M]. p \<in> t \<longleftrightarrow> 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

171 
(\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M]. 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

172 
pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) & 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13319
diff
changeset

173 
xy \<in> s & yz \<in> r)" 
13245  174 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

175 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

176 
injection :: "[i=>o,i,i,i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

177 
"injection(M,A,B,f) == 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
22710
diff
changeset

178 
typed_function(M,A,B,f) & 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

179 
(\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M]. 
46823  180 
pair(M,x,y,p) \<longrightarrow> pair(M,x',y,p') \<longrightarrow> p\<in>f \<longrightarrow> p'\<in>f \<longrightarrow> x=x')" 
13223  181 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

182 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

183 
surjection :: "[i=>o,i,i,i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

184 
"surjection(M,A,B,f) == 
13223  185 
typed_function(M,A,B,f) & 
46823  186 
(\<forall>y[M]. y\<in>B \<longrightarrow> (\<exists>x[M]. x\<in>A & fun_apply(M,f,x,y)))" 
13223  187 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

188 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

189 
bijection :: "[i=>o,i,i,i] => o" where 
13223  190 
"bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)" 
191 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

192 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

193 
restriction :: "[i=>o,i,i,i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

194 
"restriction(M,r,A,z) == 
46823  195 
\<forall>x[M]. x \<in> z \<longleftrightarrow> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x))))" 
13223  196 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

197 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

198 
transitive_set :: "[i=>o,i] => o" where 
46823  199 
"transitive_set(M,a) == \<forall>x[M]. x\<in>a \<longrightarrow> subset(M,x,a)" 
13223  200 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

201 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

202 
ordinal :: "[i=>o,i] => o" where 
13223  203 
{*an ordinal is a transitive set of transitive sets*} 
46823  204 
"ordinal(M,a) == transitive_set(M,a) & (\<forall>x[M]. x\<in>a \<longrightarrow> transitive_set(M,x))" 
13223  205 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

206 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

207 
limit_ordinal :: "[i=>o,i] => o" where 
13223  208 
{*a limit ordinal is a nonempty, successorclosed ordinal*} 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

209 
"limit_ordinal(M,a) == 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
22710
diff
changeset

210 
ordinal(M,a) & ~ empty(M,a) & 
46823  211 
(\<forall>x[M]. x\<in>a \<longrightarrow> (\<exists>y[M]. y\<in>a & successor(M,x,y)))" 
13223  212 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

213 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

214 
successor_ordinal :: "[i=>o,i] => o" where 
13223  215 
{*a successor ordinal is any ordinal that is neither empty nor limit*} 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

216 
"successor_ordinal(M,a) == 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
22710
diff
changeset

217 
ordinal(M,a) & ~ empty(M,a) & ~ limit_ordinal(M,a)" 
13223  218 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

219 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

220 
finite_ordinal :: "[i=>o,i] => o" where 
13223  221 
{*an ordinal is finite if neither it nor any of its elements are limit*} 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

222 
"finite_ordinal(M,a) == 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
22710
diff
changeset

223 
ordinal(M,a) & ~ limit_ordinal(M,a) & 
46823  224 
(\<forall>x[M]. x\<in>a \<longrightarrow> ~ limit_ordinal(M,x))" 
13223  225 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

226 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

227 
omega :: "[i=>o,i] => o" where 
13223  228 
{*omega is a limit ordinal none of whose elements are limit*} 
46823  229 
"omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a \<longrightarrow> ~ limit_ordinal(M,x))" 
13223  230 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

231 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

232 
is_quasinat :: "[i=>o,i] => o" where 
13350  233 
"is_quasinat(M,z) == empty(M,z)  (\<exists>m[M]. successor(M,m,z))" 
234 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

235 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

236 
is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

237 
"is_nat_case(M, a, is_b, k, z) == 
46823  238 
(empty(M,k) \<longrightarrow> z=a) & 
239 
(\<forall>m[M]. successor(M,m,k) \<longrightarrow> is_b(m,z)) & 

13363  240 
(is_quasinat(M,k)  empty(M,z))" 
13350  241 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

242 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

243 
relation1 :: "[i=>o, [i,i]=>o, i=>i] => o" where 
46823  244 
"relation1(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. is_f(x,y) \<longleftrightarrow> y = f(x)" 
13353  245 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

246 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

247 
Relation1 :: "[i=>o, i, [i,i]=>o, i=>i] => o" where 
13423
7ec771711c09
More lemmas, working towards relativization of "satisfies"
paulson
parents:
13418
diff
changeset

248 
{*as above, but typed*} 
13634  249 
"Relation1(M,A,is_f,f) == 
46823  250 
\<forall>x[M]. \<forall>y[M]. x\<in>A \<longrightarrow> is_f(x,y) \<longleftrightarrow> y = f(x)" 
13423
7ec771711c09
More lemmas, working towards relativization of "satisfies"
paulson
parents:
13418
diff
changeset

251 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

252 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

253 
relation2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o" where 
46823  254 
"relation2(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. is_f(x,y,z) \<longleftrightarrow> z = f(x,y)" 
13353  255 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

256 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

257 
Relation2 :: "[i=>o, i, i, [i,i,i]=>o, [i,i]=>i] => o" where 
13634  258 
"Relation2(M,A,B,is_f,f) == 
46823  259 
\<forall>x[M]. \<forall>y[M]. \<forall>z[M]. x\<in>A \<longrightarrow> y\<in>B \<longrightarrow> is_f(x,y,z) \<longleftrightarrow> z = f(x,y)" 
13423
7ec771711c09
More lemmas, working towards relativization of "satisfies"
paulson
parents:
13418
diff
changeset

260 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

261 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

262 
relation3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o" where 
13634  263 
"relation3(M,is_f,f) == 
46823  264 
\<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M]. is_f(x,y,z,u) \<longleftrightarrow> u = f(x,y,z)" 
13353  265 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

266 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

267 
Relation3 :: "[i=>o, i, i, i, [i,i,i,i]=>o, [i,i,i]=>i] => o" where 
13634  268 
"Relation3(M,A,B,C,is_f,f) == 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

269 
\<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M]. 
46823  270 
x\<in>A \<longrightarrow> y\<in>B \<longrightarrow> z\<in>C \<longrightarrow> is_f(x,y,z,u) \<longleftrightarrow> u = f(x,y,z)" 
13423
7ec771711c09
More lemmas, working towards relativization of "satisfies"
paulson
parents:
13418
diff
changeset

271 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

272 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

273 
relation4 :: "[i=>o, [i,i,i,i,i]=>o, [i,i,i,i]=>i] => o" where 
13634  274 
"relation4(M,is_f,f) == 
46823  275 
\<forall>u[M]. \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>a[M]. is_f(u,x,y,z,a) \<longleftrightarrow> a = f(u,x,y,z)" 
13423
7ec771711c09
More lemmas, working towards relativization of "satisfies"
paulson
parents:
13418
diff
changeset

276 

7ec771711c09
More lemmas, working towards relativization of "satisfies"
paulson
parents:
13418
diff
changeset

277 

7ec771711c09
More lemmas, working towards relativization of "satisfies"
paulson
parents:
13418
diff
changeset

278 
text{*Useful when absoluteness reasoning has replaced the predicates by terms*} 
13634  279 
lemma triv_Relation1: 
280 
"Relation1(M, A, \<lambda>x y. y = f(x), f)" 

281 
by (simp add: Relation1_def) 

13423
7ec771711c09
More lemmas, working towards relativization of "satisfies"
paulson
parents:
13418
diff
changeset

282 

13634  283 
lemma triv_Relation2: 
284 
"Relation2(M, A, B, \<lambda>x y a. a = f(x,y), f)" 

285 
by (simp add: Relation2_def) 

13423
7ec771711c09
More lemmas, working towards relativization of "satisfies"
paulson
parents:
13418
diff
changeset

286 

13223  287 

288 
subsection {*The relativized ZF axioms*} 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

289 

21233  290 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

291 
extensionality :: "(i=>o) => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

292 
"extensionality(M) == 
46823  293 
\<forall>x[M]. \<forall>y[M]. (\<forall>z[M]. z \<in> x \<longleftrightarrow> z \<in> y) \<longrightarrow> x=y" 
13223  294 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

295 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

296 
separation :: "[i=>o, i=>o] => o" where 
13563  297 
{*The formula @{text P} should only involve parameters 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

298 
belonging to @{text M} and all its quantifiers must be relativized 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

299 
to @{text M}. We do not have separation as a scheme; every instance 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

300 
that we need must be assumed (and later proved) separately.*} 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

301 
"separation(M,P) == 
46823  302 
\<forall>z[M]. \<exists>y[M]. \<forall>x[M]. x \<in> y \<longleftrightarrow> x \<in> z & P(x)" 
13223  303 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

304 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

305 
upair_ax :: "(i=>o) => o" where 
13563  306 
"upair_ax(M) == \<forall>x[M]. \<forall>y[M]. \<exists>z[M]. upair(M,x,y,z)" 
13223  307 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

308 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

309 
Union_ax :: "(i=>o) => o" where 
13514  310 
"Union_ax(M) == \<forall>x[M]. \<exists>z[M]. big_union(M,x,z)" 
13223  311 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

312 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

313 
power_ax :: "(i=>o) => o" where 
13514  314 
"power_ax(M) == \<forall>x[M]. \<exists>z[M]. powerset(M,x,z)" 
13223  315 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

316 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

317 
univalent :: "[i=>o, i, [i,i]=>o] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

318 
"univalent(M,A,P) == 
46823  319 
\<forall>x[M]. x\<in>A \<longrightarrow> (\<forall>y[M]. \<forall>z[M]. P(x,y) & P(x,z) \<longrightarrow> y=z)" 
13223  320 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

321 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

322 
replacement :: "[i=>o, [i,i]=>o] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

323 
"replacement(M,P) == 
46823  324 
\<forall>A[M]. univalent(M,A,P) \<longrightarrow> 
325 
(\<exists>Y[M]. \<forall>b[M]. (\<exists>x[M]. x\<in>A & P(x,b)) \<longrightarrow> b \<in> Y)" 

13223  326 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

327 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

328 
strong_replacement :: "[i=>o, [i,i]=>o] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

329 
"strong_replacement(M,P) == 
46823  330 
\<forall>A[M]. univalent(M,A,P) \<longrightarrow> 
331 
(\<exists>Y[M]. \<forall>b[M]. b \<in> Y \<longleftrightarrow> (\<exists>x[M]. x\<in>A & P(x,b)))" 

13223  332 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

333 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

334 
foundation_ax :: "(i=>o) => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

335 
"foundation_ax(M) == 
46823  336 
\<forall>x[M]. (\<exists>y[M]. y\<in>x) \<longrightarrow> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & z \<in> y))" 
13223  337 

338 

339 
subsection{*A trivial consistency proof for $V_\omega$ *} 

340 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

341 
text{*We prove that $V_\omega$ 
13223  342 
(or @{text univ} in Isabelle) satisfies some ZF axioms. 
343 
Kunen, Theorem IV 3.13, page 123.*} 

344 

345 
lemma univ0_downwards_mem: "[ y \<in> x; x \<in> univ(0) ] ==> y \<in> univ(0)" 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

346 
apply (insert Transset_univ [OF Transset_0]) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

347 
apply (simp add: Transset_def, blast) 
13223  348 
done 
349 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

350 
lemma univ0_Ball_abs [simp]: 
46823  351 
"A \<in> univ(0) ==> (\<forall>x\<in>A. x \<in> univ(0) \<longrightarrow> P(x)) \<longleftrightarrow> (\<forall>x\<in>A. P(x))" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

352 
by (blast intro: univ0_downwards_mem) 
13223  353 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

354 
lemma univ0_Bex_abs [simp]: 
46823  355 
"A \<in> univ(0) ==> (\<exists>x\<in>A. x \<in> univ(0) & P(x)) \<longleftrightarrow> (\<exists>x\<in>A. P(x))" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

356 
by (blast intro: univ0_downwards_mem) 
13223  357 

358 
text{*Congruence rule for separation: can assume the variable is in @{text M}*} 

13254  359 
lemma separation_cong [cong]: 
46823  360 
"(!!x. M(x) ==> P(x) \<longleftrightarrow> P'(x)) 
361 
==> separation(M, %x. P(x)) \<longleftrightarrow> separation(M, %x. P'(x))" 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

362 
by (simp add: separation_def) 
13223  363 

13254  364 
lemma univalent_cong [cong]: 
46823  365 
"[ A=A'; !!x y. [ x\<in>A; M(x); M(y) ] ==> P(x,y) \<longleftrightarrow> P'(x,y) ] 
366 
==> univalent(M, A, %x y. P(x,y)) \<longleftrightarrow> univalent(M, A', %x y. P'(x,y))" 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

367 
by (simp add: univalent_def) 
13223  368 

13505  369 
lemma univalent_triv [intro,simp]: 
370 
"univalent(M, A, \<lambda>x y. y = f(x))" 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

371 
by (simp add: univalent_def) 
13505  372 

373 
lemma univalent_conjI2 [intro,simp]: 

374 
"univalent(M,A,Q) ==> univalent(M, A, \<lambda>x y. P(x,y) & Q(x,y))" 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

375 
by (simp add: univalent_def, blast) 
13505  376 

377 
text{*Congruence rule for replacement*} 

13254  378 
lemma strong_replacement_cong [cong]: 
46823  379 
"[ !!x y. [ M(x); M(y) ] ==> P(x,y) \<longleftrightarrow> P'(x,y) ] 
380 
==> strong_replacement(M, %x y. P(x,y)) \<longleftrightarrow> 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

381 
strong_replacement(M, %x y. P'(x,y))" 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

382 
by (simp add: strong_replacement_def) 
13223  383 

384 
text{*The extensionality axiom*} 

385 
lemma "extensionality(\<lambda>x. x \<in> univ(0))" 

386 
apply (simp add: extensionality_def) 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

387 
apply (blast intro: univ0_downwards_mem) 
13223  388 
done 
389 

390 
text{*The separation axiom requires some lemmas*} 

391 
lemma Collect_in_Vfrom: 

392 
"[ X \<in> Vfrom(A,j); Transset(A) ] ==> Collect(X,P) \<in> Vfrom(A, succ(j))" 

393 
apply (drule Transset_Vfrom) 

394 
apply (rule subset_mem_Vfrom) 

395 
apply (unfold Transset_def, blast) 

396 
done 

397 

398 
lemma Collect_in_VLimit: 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

399 
"[ X \<in> Vfrom(A,i); Limit(i); Transset(A) ] 
13223  400 
==> Collect(X,P) \<in> Vfrom(A,i)" 
401 
apply (rule Limit_VfromE, assumption+) 

402 
apply (blast intro: Limit_has_succ VfromI Collect_in_Vfrom) 

403 
done 

404 

405 
lemma Collect_in_univ: 

406 
"[ X \<in> univ(A); Transset(A) ] ==> Collect(X,P) \<in> univ(A)" 

407 
by (simp add: univ_def Collect_in_VLimit Limit_nat) 

408 

409 
lemma "separation(\<lambda>x. x \<in> univ(0), P)" 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

410 
apply (simp add: separation_def, clarify) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

411 
apply (rule_tac x = "Collect(z,P)" in bexI) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

412 
apply (blast intro: Collect_in_univ Transset_0)+ 
13223  413 
done 
414 

415 
text{*Unordered pairing axiom*} 

416 
lemma "upair_ax(\<lambda>x. x \<in> univ(0))" 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

417 
apply (simp add: upair_ax_def upair_def) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

418 
apply (blast intro: doubleton_in_univ) 
13223  419 
done 
420 

421 
text{*Union axiom*} 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

422 
lemma "Union_ax(\<lambda>x. x \<in> univ(0))" 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

423 
apply (simp add: Union_ax_def big_union_def, clarify) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

424 
apply (rule_tac x="\<Union>x" in bexI) 
13299  425 
apply (blast intro: univ0_downwards_mem) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

426 
apply (blast intro: Union_in_univ Transset_0) 
13223  427 
done 
428 

429 
text{*Powerset axiom*} 

430 

431 
lemma Pow_in_univ: 

432 
"[ X \<in> univ(A); Transset(A) ] ==> Pow(X) \<in> univ(A)" 

433 
apply (simp add: univ_def Pow_in_VLimit Limit_nat) 

434 
done 

435 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

436 
lemma "power_ax(\<lambda>x. x \<in> univ(0))" 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

437 
apply (simp add: power_ax_def powerset_def subset_def, clarify) 
13299  438 
apply (rule_tac x="Pow(x)" in bexI) 
439 
apply (blast intro: univ0_downwards_mem) 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

440 
apply (blast intro: Pow_in_univ Transset_0) 
13223  441 
done 
442 

443 
text{*Foundation axiom*} 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

444 
lemma "foundation_ax(\<lambda>x. x \<in> univ(0))" 
13223  445 
apply (simp add: foundation_ax_def, clarify) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

446 
apply (cut_tac A=x in foundation) 
13299  447 
apply (blast intro: univ0_downwards_mem) 
13223  448 
done 
449 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

450 
lemma "replacement(\<lambda>x. x \<in> univ(0), P)" 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

451 
apply (simp add: replacement_def, clarify) 
13223  452 
oops 
453 
text{*no idea: maybe prove by induction on the rank of A?*} 

454 

455 
text{*Still missing: Replacement, Choice*} 

456 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

457 
subsection{*Lemmas Needed to Reduce Some Set Constructions to Instances 
13223  458 
of Separation*} 
459 

46823  460 
lemma image_iff_Collect: "r `` A = {y \<in> \<Union>(\<Union>(r)). \<exists>p\<in>r. \<exists>x\<in>A. p=<x,y>}" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

461 
apply (rule equalityI, auto) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

462 
apply (simp add: Pair_def, blast) 
13223  463 
done 
464 

465 
lemma vimage_iff_Collect: 

46823  466 
"r `` A = {x \<in> \<Union>(\<Union>(r)). \<exists>p\<in>r. \<exists>y\<in>A. p=<x,y>}" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

467 
apply (rule equalityI, auto) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

468 
apply (simp add: Pair_def, blast) 
13223  469 
done 
470 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

471 
text{*These two lemmas lets us prove @{text domain_closed} and 
13223  472 
@{text range_closed} without new instances of separation*} 
473 

474 
lemma domain_eq_vimage: "domain(r) = r `` Union(Union(r))" 

475 
apply (rule equalityI, auto) 

476 
apply (rule vimageI, assumption) 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

477 
apply (simp add: Pair_def, blast) 
13223  478 
done 
479 

480 
lemma range_eq_image: "range(r) = r `` Union(Union(r))" 

481 
apply (rule equalityI, auto) 

482 
apply (rule imageI, assumption) 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

483 
apply (simp add: Pair_def, blast) 
13223  484 
done 
485 

486 
lemma replacementD: 

487 
"[ replacement(M,P); M(A); univalent(M,A,P) ] 

46823  488 
==> \<exists>Y[M]. (\<forall>b[M]. ((\<exists>x[M]. x\<in>A & P(x,b)) \<longrightarrow> b \<in> Y))" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

489 
by (simp add: replacement_def) 
13223  490 

491 
lemma strong_replacementD: 

492 
"[ strong_replacement(M,P); M(A); univalent(M,A,P) ] 

46823  493 
==> \<exists>Y[M]. (\<forall>b[M]. (b \<in> Y \<longleftrightarrow> (\<exists>x[M]. x\<in>A & P(x,b))))" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

494 
by (simp add: strong_replacement_def) 
13223  495 

496 
lemma separationD: 

46823  497 
"[ separation(M,P); M(z) ] ==> \<exists>y[M]. \<forall>x[M]. x \<in> y \<longleftrightarrow> x \<in> z & P(x)" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

498 
by (simp add: separation_def) 
13223  499 

500 

501 
text{*More constants, for order types*} 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

502 

21233  503 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

504 
order_isomorphism :: "[i=>o,i,i,i,i,i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

505 
"order_isomorphism(M,A,r,B,s,f) == 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

506 
bijection(M,A,B,f) & 
46823  507 
(\<forall>x[M]. x\<in>A \<longrightarrow> (\<forall>y[M]. y\<in>A \<longrightarrow> 
13306  508 
(\<forall>p[M]. \<forall>fx[M]. \<forall>fy[M]. \<forall>q[M]. 
46823  509 
pair(M,x,y,p) \<longrightarrow> fun_apply(M,f,x,fx) \<longrightarrow> fun_apply(M,f,y,fy) \<longrightarrow> 
510 
pair(M,fx,fy,q) \<longrightarrow> (p\<in>r \<longleftrightarrow> q\<in>s))))" 

13223  511 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

512 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

513 
pred_set :: "[i=>o,i,i,i,i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

514 
"pred_set(M,A,x,r,B) == 
46823  515 
\<forall>y[M]. y \<in> B \<longleftrightarrow> (\<exists>p[M]. p\<in>r & y \<in> A & pair(M,y,x,p))" 
13223  516 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

517 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

518 
membership :: "[i=>o,i,i] => o" where {*membership relation*} 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

519 
"membership(M,A,r) == 
46823  520 
\<forall>p[M]. p \<in> r \<longleftrightarrow> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>A & x\<in>y & pair(M,x,y,p)))" 
13223  521 

522 

13418
7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

523 
subsection{*Introducing a Transitive Class Model*} 
13223  524 

525 
text{*The class M is assumed to be transitive and to satisfy some 

526 
relativized ZF axioms*} 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

527 
locale M_trivial = 
13223  528 
fixes M 
529 
assumes transM: "[ y\<in>x; M(x) ] ==> M(y)" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
22710
diff
changeset

530 
and upair_ax: "upair_ax(M)" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
22710
diff
changeset

531 
and Union_ax: "Union_ax(M)" 
13223  532 
and power_ax: "power_ax(M)" 
533 
and replacement: "replacement(M,P)" 

13268  534 
and M_nat [iff]: "M(nat)" (*i.e. the axiom of infinity*) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

535 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

536 

87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

537 
text{*Automatically discovers the proof using @{text transM}, @{text nat_0I} 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

538 
and @{text M_nat}.*} 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

539 
lemma (in M_trivial) nonempty [simp]: "M(0)" 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

540 
by (blast intro: transM) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

541 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

542 
lemma (in M_trivial) rall_abs [simp]: 
46823  543 
"M(A) ==> (\<forall>x[M]. x\<in>A \<longrightarrow> P(x)) \<longleftrightarrow> (\<forall>x\<in>A. P(x))" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

544 
by (blast intro: transM) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

545 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

546 
lemma (in M_trivial) rex_abs [simp]: 
46823  547 
"M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) \<longleftrightarrow> (\<exists>x\<in>A. P(x))" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

548 
by (blast intro: transM) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

549 

87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

550 
lemma (in M_trivial) ball_iff_equiv: 
46823  551 
"M(A) ==> (\<forall>x[M]. (x\<in>A \<longleftrightarrow> P(x))) \<longleftrightarrow> 
552 
(\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) \<longrightarrow> M(x) \<longrightarrow> x\<in>A)" 

13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

553 
by (blast intro: transM) 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

554 

28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

555 
text{*Simplifies proofs of equalities when there's an iffequality 
46823  556 
available for rewriting, universally quantified over M. 
13702  557 
But it's not the only way to prove such equalities: its 
558 
premises @{term "M(A)"} and @{term "M(B)"} can be too strong.*} 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

559 
lemma (in M_trivial) M_equalityI: 
46823  560 
"[ !!x. M(x) ==> x\<in>A \<longleftrightarrow> x\<in>B; M(A); M(B) ] ==> A=B" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

561 
by (blast intro!: equalityI dest: transM) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

562 

13418
7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

563 

7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

564 
subsubsection{*Trivial Absoluteness Proofs: Empty Set, Pairs, etc.*} 
7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

565 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

566 
lemma (in M_trivial) empty_abs [simp]: 
46823  567 
"M(z) ==> empty(M,z) \<longleftrightarrow> z=0" 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

568 
apply (simp add: empty_def) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

569 
apply (blast intro: transM) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

570 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

571 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

572 
lemma (in M_trivial) subset_abs [simp]: 
46823  573 
"M(A) ==> subset(M,A,B) \<longleftrightarrow> A \<subseteq> B" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

574 
apply (simp add: subset_def) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

575 
apply (blast intro: transM) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

576 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

577 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

578 
lemma (in M_trivial) upair_abs [simp]: 
46823  579 
"M(z) ==> upair(M,a,b,z) \<longleftrightarrow> z={a,b}" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

580 
apply (simp add: upair_def) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

581 
apply (blast intro: transM) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

582 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

583 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

584 
lemma (in M_trivial) upair_in_M_iff [iff]: 
46823  585 
"M({a,b}) \<longleftrightarrow> M(a) & M(b)" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

586 
apply (insert upair_ax, simp add: upair_ax_def) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

587 
apply (blast intro: transM) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

588 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

589 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

590 
lemma (in M_trivial) singleton_in_M_iff [iff]: 
46823  591 
"M({a}) \<longleftrightarrow> M(a)" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

592 
by (insert upair_in_M_iff [of a a], simp) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

593 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

594 
lemma (in M_trivial) pair_abs [simp]: 
46823  595 
"M(z) ==> pair(M,a,b,z) \<longleftrightarrow> z=<a,b>" 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

596 
apply (simp add: pair_def ZF.Pair_def) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

597 
apply (blast intro: transM) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

598 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

599 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

600 
lemma (in M_trivial) pair_in_M_iff [iff]: 
46823  601 
"M(<a,b>) \<longleftrightarrow> M(a) & M(b)" 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

602 
by (simp add: ZF.Pair_def) 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

603 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

604 
lemma (in M_trivial) pair_components_in_M: 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

605 
"[ <x,y> \<in> A; M(A) ] ==> M(x) & M(y)" 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

606 
apply (simp add: Pair_def) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

607 
apply (blast dest: transM) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

608 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

609 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

610 
lemma (in M_trivial) cartprod_abs [simp]: 
46823  611 
"[ M(A); M(B); M(z) ] ==> cartprod(M,A,B,z) \<longleftrightarrow> z = A*B" 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

612 
apply (simp add: cartprod_def) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

613 
apply (rule iffI) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

614 
apply (blast intro!: equalityI intro: transM dest!: rspec) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

615 
apply (blast dest: transM) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

616 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

617 

13418
7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

618 
subsubsection{*Absoluteness for Unions and Intersections*} 
7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

619 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

620 
lemma (in M_trivial) union_abs [simp]: 
46823  621 
"[ M(a); M(b); M(z) ] ==> union(M,a,b,z) \<longleftrightarrow> z = a \<union> b" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

622 
apply (simp add: union_def) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

623 
apply (blast intro: transM) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

624 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

625 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

626 
lemma (in M_trivial) inter_abs [simp]: 
46823  627 
"[ M(a); M(b); M(z) ] ==> inter(M,a,b,z) \<longleftrightarrow> z = a \<inter> b" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

628 
apply (simp add: inter_def) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

629 
apply (blast intro: transM) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

630 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

631 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

632 
lemma (in M_trivial) setdiff_abs [simp]: 
46823  633 
"[ M(a); M(b); M(z) ] ==> setdiff(M,a,b,z) \<longleftrightarrow> z = ab" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

634 
apply (simp add: setdiff_def) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

635 
apply (blast intro: transM) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

636 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

637 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

638 
lemma (in M_trivial) Union_abs [simp]: 
46823  639 
"[ M(A); M(z) ] ==> big_union(M,A,z) \<longleftrightarrow> z = \<Union>(A)" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

640 
apply (simp add: big_union_def) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

641 
apply (blast intro!: equalityI dest: transM) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

642 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

643 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

644 
lemma (in M_trivial) Union_closed [intro,simp]: 
46823  645 
"M(A) ==> M(\<Union>(A))" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

646 
by (insert Union_ax, simp add: Union_ax_def) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

647 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

648 
lemma (in M_trivial) Un_closed [intro,simp]: 
46823  649 
"[ M(A); M(B) ] ==> M(A \<union> B)" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

650 
by (simp only: Un_eq_Union, blast) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

651 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

652 
lemma (in M_trivial) cons_closed [intro,simp]: 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

653 
"[ M(a); M(A) ] ==> M(cons(a,A))" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

654 
by (subst cons_eq [symmetric], blast) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

655 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

656 
lemma (in M_trivial) cons_abs [simp]: 
46823  657 
"[ M(b); M(z) ] ==> is_cons(M,a,b,z) \<longleftrightarrow> z = cons(a,b)" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

658 
by (simp add: is_cons_def, blast intro: transM) 
13306  659 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

660 
lemma (in M_trivial) successor_abs [simp]: 
46823  661 
"[ M(a); M(z) ] ==> successor(M,a,z) \<longleftrightarrow> z = succ(a)" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

662 
by (simp add: successor_def, blast) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

663 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

664 
lemma (in M_trivial) succ_in_M_iff [iff]: 
46823  665 
"M(succ(a)) \<longleftrightarrow> M(a)" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

666 
apply (simp add: succ_def) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

667 
apply (blast intro: transM) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

668 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

669 

13418
7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

670 
subsubsection{*Absoluteness for Separation and Replacement*} 
7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

671 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

672 
lemma (in M_trivial) separation_closed [intro,simp]: 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

673 
"[ separation(M,P); M(A) ] ==> M(Collect(A,P))" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

674 
apply (insert separation, simp add: separation_def) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

675 
apply (drule rspec, assumption, clarify) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

676 
apply (subgoal_tac "y = Collect(A,P)", blast) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

677 
apply (blast dest: transM) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

678 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

679 

13436  680 
lemma separation_iff: 
46823  681 
"separation(M,P) \<longleftrightarrow> (\<forall>z[M]. \<exists>y[M]. is_Collect(M,z,P,y))" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

682 
by (simp add: separation_def is_Collect_def) 
13436  683 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

684 
lemma (in M_trivial) Collect_abs [simp]: 
46823  685 
"[ M(A); M(z) ] ==> is_Collect(M,A,P,z) \<longleftrightarrow> z = Collect(A,P)" 
13436  686 
apply (simp add: is_Collect_def) 
687 
apply (blast intro!: equalityI dest: transM) 

688 
done 

689 

13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

690 
text{*Probably the premise and conclusion are equivalent*} 
13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

691 
lemma (in M_trivial) strong_replacementI [rule_format]: 
13687  692 
"[ \<forall>B[M]. separation(M, %u. \<exists>x[M]. x\<in>B & P(x,u)) ] 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

693 
==> strong_replacement(M,P)" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

694 
apply (simp add: strong_replacement_def, clarify) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

695 
apply (frule replacementD [OF replacement], assumption, clarify) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

696 
apply (drule_tac x=A in rspec, clarify) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

697 
apply (drule_tac z=Y in separationD, assumption, clarify) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

698 
apply (rule_tac x=y in rexI, force, assumption) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

699 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

700 

13505  701 
subsubsection{*The Operator @{term is_Replace}*} 
702 

703 

704 
lemma is_Replace_cong [cong]: 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

705 
"[ A=A'; 
46823  706 
!!x y. [ M(x); M(y) ] ==> P(x,y) \<longleftrightarrow> P'(x,y); 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

707 
z=z' ] 
46823  708 
==> is_Replace(M, A, %x y. P(x,y), z) \<longleftrightarrow> 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

709 
is_Replace(M, A', %x y. P'(x,y), z')" 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

710 
by (simp add: is_Replace_def) 
13505  711 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

712 
lemma (in M_trivial) univalent_Replace_iff: 
13505  713 
"[ M(A); univalent(M,A,P); 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

714 
!!x y. [ x\<in>A; P(x,y) ] ==> M(y) ] 
46823  715 
==> u \<in> Replace(A,P) \<longleftrightarrow> (\<exists>x. x\<in>A & P(x,u))" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

716 
apply (simp add: Replace_iff univalent_def) 
13505  717 
apply (blast dest: transM) 
718 
done 

719 

13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

720 
(*The last premise expresses that P takes M to M*) 
13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

721 
lemma (in M_trivial) strong_replacement_closed [intro,simp]: 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

722 
"[ strong_replacement(M,P); M(A); univalent(M,A,P); 
13505  723 
!!x y. [ x\<in>A; P(x,y) ] ==> M(y) ] ==> M(Replace(A,P))" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

724 
apply (simp add: strong_replacement_def) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

725 
apply (drule_tac x=A in rspec, safe) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

726 
apply (subgoal_tac "Replace(A,P) = Y") 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

727 
apply simp 
13505  728 
apply (rule equality_iffI) 
729 
apply (simp add: univalent_Replace_iff) 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

730 
apply (blast dest: transM) 
13505  731 
done 
732 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

733 
lemma (in M_trivial) Replace_abs: 
46823  734 
"[ M(A); M(z); univalent(M,A,P); 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

735 
!!x y. [ x\<in>A; P(x,y) ] ==> M(y) ] 
46823  736 
==> is_Replace(M,A,P,z) \<longleftrightarrow> z = Replace(A,P)" 
13505  737 
apply (simp add: is_Replace_def) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

738 
apply (rule iffI) 
13702  739 
apply (rule equality_iffI) 
46823  740 
apply (simp_all add: univalent_Replace_iff) 
13702  741 
apply (blast dest: transM)+ 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

742 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

743 

13702  744 

13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

745 
(*The first premise can't simply be assumed as a schema. 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

746 
It is essential to take care when asserting instances of Replacement. 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

747 
Let K be a nonconstructible subset of nat and define 
46953  748 
f(x) = x if x \<in> K and f(x)=0 otherwise. Then RepFun(nat,f) = cons(0,K), a 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

749 
nonconstructible set. So we cannot assume that M(X) implies M(RepFun(X,f)) 
46823  750 
even for f \<in> M > M. 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

751 
*) 
13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

752 
lemma (in M_trivial) RepFun_closed: 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

753 
"[ strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) ] 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

754 
==> M(RepFun(A,f))" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

755 
apply (simp add: RepFun_def) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

756 
apply (rule strong_replacement_closed) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

757 
apply (auto dest: transM simp add: univalent_def) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

758 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

759 

13353  760 
lemma Replace_conj_eq: "{y . x \<in> A, x\<in>A & y=f(x)} = {y . x\<in>A, y=f(x)}" 
761 
by simp 

762 

763 
text{*Better than @{text RepFun_closed} when having the formula @{term "x\<in>A"} 

764 
makes relativization easier.*} 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

765 
lemma (in M_trivial) RepFun_closed2: 
13353  766 
"[ strong_replacement(M, \<lambda>x y. x\<in>A & y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) ] 
767 
==> M(RepFun(A, %x. f(x)))" 

768 
apply (simp add: RepFun_def) 

769 
apply (frule strong_replacement_closed, assumption) 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

770 
apply (auto dest: transM simp add: Replace_conj_eq univalent_def) 
13353  771 
done 
772 

13418
7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

773 
subsubsection {*Absoluteness for @{term Lambda}*} 
7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

774 

21233  775 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

776 
is_lambda :: "[i=>o, i, [i,i]=>o, i] => o" where 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

777 
"is_lambda(M, A, is_b, z) == 
46823  778 
\<forall>p[M]. p \<in> z \<longleftrightarrow> 
13418
7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

779 
(\<exists>u[M]. \<exists>v[M]. u\<in>A & pair(M,u,v,p) & is_b(u,v))" 
7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

780 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

781 
lemma (in M_trivial) lam_closed: 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

782 
"[ strong_replacement(M, \<lambda>x y. y = <x,b(x)>); M(A); \<forall>x\<in>A. M(b(x)) ] 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

783 
==> M(\<lambda>x\<in>A. b(x))" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

784 
by (simp add: lam_def, blast intro: RepFun_closed dest: transM) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

785 

13418
7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

786 
text{*Better than @{text lam_closed}: has the formula @{term "x\<in>A"}*} 
13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

787 
lemma (in M_trivial) lam_closed2: 
13418
7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

788 
"[strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>); 
46823  789 
M(A); \<forall>m[M]. m\<in>A \<longrightarrow> M(b(m))] ==> M(Lambda(A,b))" 
13418
7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

790 
apply (simp add: lam_def) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

791 
apply (blast intro: RepFun_closed2 dest: transM) 
13418
7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

792 
done 
7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

793 

13702  794 
lemma (in M_trivial) lambda_abs2: 
46823  795 
"[ Relation1(M,A,is_b,b); M(A); \<forall>m[M]. m\<in>A \<longrightarrow> M(b(m)); M(z) ] 
796 
==> is_lambda(M,A,is_b,z) \<longleftrightarrow> z = Lambda(A,b)" 

13634  797 
apply (simp add: Relation1_def is_lambda_def) 
13418
7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

798 
apply (rule iffI) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

799 
prefer 2 apply (simp add: lam_def) 
13702  800 
apply (rule equality_iffI) 
46823  801 
apply (simp add: lam_def) 
802 
apply (rule iffI) 

803 
apply (blast dest: transM) 

804 
apply (auto simp add: transM [of _ A]) 

13418
7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

805 
done 
7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

806 

13423
7ec771711c09
More lemmas, working towards relativization of "satisfies"
paulson
parents:
13418
diff
changeset

807 
lemma is_lambda_cong [cong]: 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

808 
"[ A=A'; z=z'; 
46823  809 
!!x y. [ x\<in>A; M(x); M(y) ] ==> is_b(x,y) \<longleftrightarrow> is_b'(x,y) ] 
810 
==> is_lambda(M, A, %x y. is_b(x,y), z) \<longleftrightarrow> 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

811 
is_lambda(M, A', %x y. is_b'(x,y), z')" 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

812 
by (simp add: is_lambda_def) 
13423
7ec771711c09
More lemmas, working towards relativization of "satisfies"
paulson
parents:
13418
diff
changeset

813 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

814 
lemma (in M_trivial) image_abs [simp]: 
46823  815 
"[ M(r); M(A); M(z) ] ==> image(M,r,A,z) \<longleftrightarrow> z = r``A" 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

816 
apply (simp add: image_def) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

817 
apply (rule iffI) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

818 
apply (blast intro!: equalityI dest: transM, blast) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

819 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

820 

28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

821 
text{*What about @{text Pow_abs}? Powerset is NOT absolute! 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

822 
This result is one direction of absoluteness.*} 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

823 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

824 
lemma (in M_trivial) powerset_Pow: 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

825 
"powerset(M, x, Pow(x))" 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

826 
by (simp add: powerset_def) 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

827 

28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

828 
text{*But we can't prove that the powerset in @{text M} includes the 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

829 
real powerset.*} 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

830 
lemma (in M_trivial) powerset_imp_subset_Pow: 
46823  831 
"[ powerset(M,x,y); M(y) ] ==> y \<subseteq> Pow(x)" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

832 
apply (simp add: powerset_def) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

833 
apply (blast dest: transM) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

834 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

835 

13418
7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

836 
subsubsection{*Absoluteness for the Natural Numbers*} 
7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

837 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

838 
lemma (in M_trivial) nat_into_M [intro]: 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

839 
"n \<in> nat ==> M(n)" 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

840 
by (induct n rule: nat_induct, simp_all) 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

841 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

842 
lemma (in M_trivial) nat_case_closed [intro,simp]: 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

843 
"[M(k); M(a); \<forall>m[M]. M(b(m))] ==> M(nat_case(a,b,k))" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

844 
apply (case_tac "k=0", simp) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

845 
apply (case_tac "\<exists>m. k = succ(m)", force) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

846 
apply (simp add: nat_case_def) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

847 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

848 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

849 
lemma (in M_trivial) quasinat_abs [simp]: 
46823  850 
"M(z) ==> is_quasinat(M,z) \<longleftrightarrow> quasinat(z)" 
13350  851 
by (auto simp add: is_quasinat_def quasinat_def) 
852 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

853 
lemma (in M_trivial) nat_case_abs [simp]: 
13634  854 
"[ relation1(M,is_b,b); M(k); M(z) ] 
46823  855 
==> is_nat_case(M,a,is_b,k,z) \<longleftrightarrow> z = nat_case(a,b,k)" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

856 
apply (case_tac "quasinat(k)") 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

857 
prefer 2 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

858 
apply (simp add: is_nat_case_def non_nat_case) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

859 
apply (force simp add: quasinat_def) 
13350  860 
apply (simp add: quasinat_def is_nat_case_def) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

861 
apply (elim disjE exE) 
13634  862 
apply (simp_all add: relation1_def) 
13350  863 
done 
864 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

865 
(*NOT for the simplifier. The assumption M(z') is apparently necessary, but 
13363  866 
causes the error "Failed congruence proof!" It may be better to replace 
867 
is_nat_case by nat_case before attempting congruence reasoning.*) 

13434  868 
lemma is_nat_case_cong: 
13352  869 
"[ a = a'; k = k'; z = z'; M(z'); 
46823  870 
!!x y. [ M(x); M(y) ] ==> is_b(x,y) \<longleftrightarrow> is_b'(x,y) ] 
871 
==> is_nat_case(M, a, is_b, k, z) \<longleftrightarrow> is_nat_case(M, a', is_b', k', z')" 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

872 
by (simp add: is_nat_case_def) 
13352  873 

13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

874 

13418
7c0ba9dba978
tweaks, aiming towards relativization of "satisfies"
paulson
parents:
13397
diff
changeset

875 
subsection{*Absoluteness for Ordinals*} 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

876 
text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*} 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

877 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

878 
lemma (in M_trivial) lt_closed: 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

879 
"[ j<i; M(i) ] ==> M(j)" 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

880 
by (blast dest: ltD intro: transM) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

881 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

882 
lemma (in M_trivial) transitive_set_abs [simp]: 
46823  883 
"M(a) ==> transitive_set(M,a) \<longleftrightarrow> Transset(a)" 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

884 
by (simp add: transitive_set_def Transset_def) 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

885 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

886 
lemma (in M_trivial) ordinal_abs [simp]: 
46823  887 
"M(a) ==> ordinal(M,a) \<longleftrightarrow> Ord(a)" 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

888 
by (simp add: ordinal_def Ord_def) 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

889 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

890 
lemma (in M_trivial) limit_ordinal_abs [simp]: 
46823  891 
"M(a) ==> limit_ordinal(M,a) \<longleftrightarrow> Limit(a)" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

892 
apply (unfold Limit_def limit_ordinal_def) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

893 
apply (simp add: Ord_0_lt_iff) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

894 
apply (simp add: lt_def, blast) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

895 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

896 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

897 
lemma (in M_trivial) successor_ordinal_abs [simp]: 
46823  898 
"M(a) ==> successor_ordinal(M,a) \<longleftrightarrow> Ord(a) & (\<exists>b[M]. a = succ(b))" 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

899 
apply (simp add: successor_ordinal_def, safe) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

900 
apply (drule Ord_cases_disj, auto) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

901 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

902 

28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

903 
lemma finite_Ord_is_nat: 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

904 
"[ Ord(a); ~ Limit(a); \<forall>x\<in>a. ~ Limit(x) ] ==> a \<in> nat" 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

905 
by (induct a rule: trans_induct3, simp_all) 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

906 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

907 
lemma (in M_trivial) finite_ordinal_abs [simp]: 
46823  908 
"M(a) ==> finite_ordinal(M,a) \<longleftrightarrow> a \<in> nat" 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

909 
apply (simp add: finite_ordinal_def) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

910 
apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

911 
dest: Ord_trans naturals_not_limit) 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

912 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

913 

28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

914 
lemma Limit_non_Limit_implies_nat: 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

915 
"[ Limit(a); \<forall>x\<in>a. ~ Limit(x) ] ==> a = nat" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

916 
apply (rule le_anti_sym) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

917 
apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

918 
apply (simp add: lt_def) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

919 
apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

920 
apply (erule nat_le_Limit) 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

921 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

922 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

923 
lemma (in M_trivial) omega_abs [simp]: 
46823  924 
"M(a) ==> omega(M,a) \<longleftrightarrow> a = nat" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

925 
apply (simp add: omega_def) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

926 
apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit) 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

927 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

928 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

929 
lemma (in M_trivial) number1_abs [simp]: 
46823  930 
"M(a) ==> number1(M,a) \<longleftrightarrow> a = 1" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

931 
by (simp add: number1_def) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

932 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

933 
lemma (in M_trivial) number2_abs [simp]: 
46823  934 
"M(a) ==> number2(M,a) \<longleftrightarrow> a = succ(1)" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

935 
by (simp add: number2_def) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

936 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

937 
lemma (in M_trivial) number3_abs [simp]: 
46823  938 
"M(a) ==> number3(M,a) \<longleftrightarrow> a = succ(succ(1))" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

939 
by (simp add: number3_def) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

940 

28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

941 
text{*Kunen continued to 20...*} 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

942 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

943 
(*Could not get this to work. The \<lambda>x\<in>nat is essential because everything 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

944 
but the recursion variable must stay unchanged. But then the recursion 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

945 
equations only hold for x\<in>nat (or in some other set) and not for the 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

946 
whole of the class M. 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

947 
consts 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

948 
natnumber_aux :: "[i=>o,i] => i" 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

949 

28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

950 
primrec 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

951 
"natnumber_aux(M,0) = (\<lambda>x\<in>nat. if empty(M,x) then 1 else 0)" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

952 
"natnumber_aux(M,succ(n)) = 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
22710
diff
changeset

953 
(\<lambda>x\<in>nat. if (\<exists>y[M]. natnumber_aux(M,n)`y=1 & successor(M,y,x)) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
22710
diff
changeset

954 
then 1 else 0)" 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

955 

21233  956 
definition 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

957 
natnumber :: "[i=>o,i,i] => o" 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

958 
"natnumber(M,n,x) == natnumber_aux(M,n)`x = 1" 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

959 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

960 
lemma (in M_trivial) [simp]: 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

961 
"natnumber(M,0,x) == x=0" 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

962 
*) 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

963 

28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

964 
subsection{*Some instances of separation and strong replacement*} 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

965 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

966 
locale M_basic = M_trivial + 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

967 
assumes Inter_separation: 
46823  968 
"M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A \<longrightarrow> x\<in>y)" 
13436  969 
and Diff_separation: 
970 
"M(B) ==> separation(M, \<lambda>x. x \<notin> B)" 

13223  971 
and cartprod_separation: 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

972 
"[ M(A); M(B) ] 
13298  973 
==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,z)))" 
13223  974 
and image_separation: 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

975 
"[ M(A); M(r) ] 
13268  976 
==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,p)))" 
13223  977 
and converse_separation: 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

978 
"M(r) ==> separation(M, 
13298  979 
\<lambda>z. \<exists>p[M]. p\<in>r & (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) & pair(M,y,x,z)))" 
13223  980 
and restrict_separation: 
13268  981 
"M(A) ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. pair(M,x,y,z)))" 
13223  982 
and comp_separation: 
983 
"[ M(r); M(s) ] 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

984 
==> separation(M, \<lambda>xz. \<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M]. 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
22710
diff
changeset

985 
pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) & 
13268  986 
xy\<in>s & yz\<in>r)" 
13223  987 
and pred_separation: 
13298  988 
"[ M(r); M(x) ] ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & pair(M,y,x,p))" 
13223  989 
and Memrel_separation: 
13298  990 
"separation(M, \<lambda>z. \<exists>x[M]. \<exists>y[M]. pair(M,x,y,z) & x \<in> y)" 
13268  991 
and funspace_succ_replacement: 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

992 
"M(n) ==> 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

993 
strong_replacement(M, \<lambda>p z. \<exists>f[M]. \<exists>b[M]. \<exists>nb[M]. \<exists>cnbf[M]. 
13306  994 
pair(M,f,b,p) & pair(M,n,b,nb) & is_cons(M,nb,f,cnbf) & 
995 
upair(M,cnbf,cnbf,z))" 

13223  996 
and is_recfun_separation: 
13634  997 
{*for wellfounded recursion: used to prove @{text is_recfun_equal}*} 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

998 
"[ M(r); M(f); M(g); M(a); M(b) ] 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

999 
==> separation(M, 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1000 
\<lambda>x. \<exists>xa[M]. \<exists>xb[M]. 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1001 
pair(M,x,a,xa) & xa \<in> r & pair(M,x,b,xb) & xb \<in> r & 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1002 
(\<exists>fx[M]. \<exists>gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) & 
13319  1003 
fx \<noteq> gx))" 
13223  1004 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

1005 
lemma (in M_basic) cartprod_iff_lemma: 
46823  1006 
"[ M(C); \<forall>u[M]. u \<in> C \<longleftrightarrow> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}); 
13254  1007 
powerset(M, A \<union> B, p1); powerset(M, p1, p2); M(p2) ] 
13223  1008 
==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1009 
apply (simp add: powerset_def) 
13254  1010 
apply (rule equalityI, clarify, simp) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1011 
apply (frule transM, assumption) 
13611  1012 
apply (frule transM, assumption, simp (no_asm_simp)) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1013 
apply blast 
13223  1014 
apply clarify 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1015 
apply (frule transM, assumption, force) 
13223  1016 
done 
1017 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

1018 
lemma (in M_basic) cartprod_iff: 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1019 
"[ M(A); M(B); M(C) ] 
46823  1020 
==> cartprod(M,A,B,C) \<longleftrightarrow> 
1021 
(\<exists>p1[M]. \<exists>p2[M]. powerset(M,A \<union> B,p1) & powerset(M,p1,p2) & 

13223  1022 
C = {z \<in> p2. \<exists>x\<in>A. \<exists>y\<in>B. z = <x,y>})" 
1023 
apply (simp add: Pair_def cartprod_def, safe) 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1024 
defer 1 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1025 
apply (simp add: powerset_def) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1026 
apply blast 
13223  1027 
txt{*Final, difficult case: the lefttoright direction of the theorem.*} 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1028 
apply (insert power_ax, simp add: power_ax_def) 
46823  1029 
apply (frule_tac x="A \<union> B" and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1030 
apply (blast, clarify) 
13299  1031 
apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
1032 
apply assumption 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1033 
apply (blast intro: cartprod_iff_lemma) 
13223  1034 
done 
1035 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

1036 
lemma (in M_basic) cartprod_closed_lemma: 
13299  1037 
"[ M(A); M(B) ] ==> \<exists>C[M]. cartprod(M,A,B,C)" 
13223  1038 
apply (simp del: cartprod_abs add: cartprod_iff) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1039 
apply (insert power_ax, simp add: power_ax_def) 
46823  1040 
apply (frule_tac x="A \<union> B" and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
13299  1041 
apply (blast, clarify) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1042 
apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec, auto) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1043 
apply (intro rexI conjI, simp+) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1044 
apply (insert cartprod_separation [of A B], simp) 
13223  1045 
done 
1046 

1047 
text{*All the lemmas above are necessary because Powerset is not absolute. 

1048 
I should have used Replacement instead!*} 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1049 
lemma (in M_basic) cartprod_closed [intro,simp]: 
13223  1050 
"[ M(A); M(B) ] ==> M(A*B)" 
1051 
by (frule cartprod_closed_lemma, assumption, force) 

1052 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1053 
lemma (in M_basic) sum_closed [intro,simp]: 
13268  1054 
"[ M(A); M(B) ] ==> M(A+B)" 
1055 
by (simp add: sum_def) 

1056 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

1057 
lemma (in M_basic) sum_abs [simp]: 
46823  1058 
"[ M(A); M(B); M(Z) ] ==> is_sum(M,A,B,Z) \<longleftrightarrow> (Z = A+B)" 
13350  1059 
by (simp add: is_sum_def sum_def singleton_0 nat_into_M) 
1060 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

1061 
lemma (in M_trivial) Inl_in_M_iff [iff]: 
46823  1062 
"M(Inl(a)) \<longleftrightarrow> M(a)" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1063 
by (simp add: Inl_def) 
13397  1064 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

1065 
lemma (in M_trivial) Inl_abs [simp]: 
46823  1066 
"M(Z) ==> is_Inl(M,a,Z) \<longleftrightarrow> (Z = Inl(a))" 
13397  1067 
by (simp add: is_Inl_def Inl_def) 
1068 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

1069 
lemma (in M_trivial) Inr_in_M_iff [iff]: 
46823  1070 
"M(Inr(a)) \<longleftrightarrow> M(a)" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1071 
by (simp add: Inr_def) 
13397  1072 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

1073 
lemma (in M_trivial) Inr_abs [simp]: 
46823  1074 
"M(Z) ==> is_Inr(M,a,Z) \<longleftrightarrow> (Z = Inr(a))" 
13397  1075 
by (simp add: is_Inr_def Inr_def) 
1076 

13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1077 

28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1078 
subsubsection {*converse of a relation*} 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1079 

13564
1500a2e48d44
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents:
13563
diff
changeset

1080 
lemma (in M_basic) M_converse_iff: 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1081 
"M(r) ==> 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1082 
converse(r) = 
46823  1083 
{z \<in> \<Union>(\<Union>(r)) * \<Union>(\<Union>(r)). 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1084 
\<exists>p\<in>r. \<exists>x[M]. \<exists>y[M]. p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>}" 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1085 
apply (rule equalityI) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1086 
prefer 2 apply (blast dest: transM, clarify, simp) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1087 
apply (simp add: Pair_def) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1088 
apply (blast dest: transM) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1089 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1090 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1091 
lemma (in M_basic) converse_closed [intro,simp]: 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1092 
"M(r) ==> M(converse(r))" 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1093 
apply (simp add: M_converse_iff) 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1094 
apply (insert converse_separation [of r], simp) 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1095 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1096 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1097 
lemma (in M_basic) converse_abs [simp]: 
46823  1098 
"[ M(r); M(z) ] ==> is_converse(M,r,z) \<longleftrightarrow> z = converse(r)" 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1099 
apply (simp add: is_converse_def) 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1100 
apply (rule iffI) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1101 
prefer 2 apply blast 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1102 
apply (rule M_equalityI) 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1103 
apply simp 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1104 
apply (blast dest: transM)+ 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1105 
done 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1106 

28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1107 

28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1108 
subsubsection {*image, preimage, domain, range*} 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1109 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1110 
lemma (in M_basic) image_closed [intro,simp]: 
13223  1111 
"[ M(A); M(r) ] ==> M(r``A)" 
1112 
apply (simp add: image_iff_Collect) 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1113 
apply (insert image_separation [of A r], simp) 
13223  1114 
done 
1115 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1116 
lemma (in M_basic) vimage_abs [simp]: 
46823  1117 
"[ M(r); M(A); M(z) ] ==> pre_image(M,r,A,z) \<longleftrightarrow> z = r``A" 
13223  1118 
apply (simp add: pre_image_def) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1119 
apply (rule iffI) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1120 
apply (blast intro!: equalityI dest: transM, blast) 
13223  1121 
done 
1122 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1123 
lemma (in M_basic) vimage_closed [intro,simp]: 
13223  1124 
"[ M(A); M(r) ] ==> M(r``A)" 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1125 
by (simp add: vimage_def) 
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1126 

28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1127 

28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1128 
subsubsection{*Domain, range and field*} 
13223  1129 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1130 
lemma (in M_basic) domain_abs [simp]: 
46823  1131 
"[ M(r); M(z) ] ==> is_domain(M,r,z) \<longleftrightarrow> z = domain(r)" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1132 
apply (simp add: is_domain_def) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1133 
apply (blast intro!: equalityI dest: transM) 
13223  1134 
done 
1135 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1136 
lemma (in M_basic) domain_closed [intro,simp]: 
13223  1137 
"M(r) ==> M(domain(r))" 
1138 
apply (simp add: domain_eq_vimage) 

1139 
done 

1140 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1141 
lemma (in M_basic) range_abs [simp]: 
46823  1142 
"[ M(r); M(z) ] ==> is_range(M,r,z) \<longleftrightarrow> z = range(r)" 
13223  1143 
apply (simp add: is_range_def) 
1144 
apply (blast intro!: equalityI dest: transM) 

1145 
done 

1146 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1147 
lemma (in M_basic) range_closed [intro,simp]: 
13223  1148 
"M(r) ==> M(range(r))" 
1149 
apply (simp add: range_eq_image) 

1150 
done 

1151 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1152 
lemma (in M_basic) field_abs [simp]: 
46823  1153 
"[ M(r); M(z) ] ==> is_field(M,r,z) \<longleftrightarrow> z = field(r)" 
13245  1154 
by (simp add: domain_closed range_closed is_field_def field_def) 
1155 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1156 
lemma (in M_basic) field_closed [intro,simp]: 
13245  1157 
"M(r) ==> M(field(r))" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1158 
by (simp add: domain_closed range_closed Un_closed field_def) 
13245  1159 

1160 

13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1161 
subsubsection{*Relations, functions and application*} 
13254  1162 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1163 
lemma (in M_basic) relation_abs [simp]: 
46823  1164 
"M(r) ==> is_relation(M,r) \<longleftrightarrow> relation(r)" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1165 
apply (simp add: is_relation_def relation_def) 
13223  1166 
apply (blast dest!: bspec dest: pair_components_in_M)+ 
1167 
done 

1168 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1169 
lemma (in M_basic) function_abs [simp]: 
46823  1170 
"M(r) ==> is_function(M,r) \<longleftrightarrow> function(r)" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1171 
apply (simp add: is_function_def function_def, safe) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1172 
apply (frule transM, assumption) 
13223  1173 
apply (blast dest: pair_components_in_M)+ 
1174 
done 

1175 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1176 
lemma (in M_basic) apply_closed [intro,simp]: 
13223  1177 
"[M(f); M(a)] ==> M(f`a)" 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1178 
by (simp add: apply_def) 
13223  1179 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1180 
lemma (in M_basic) apply_abs [simp]: 
46823  1181 
"[ M(f); M(x); M(y) ] ==> fun_apply(M,f,x,y) \<longleftrightarrow> f`x = y" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1182 
apply (simp add: fun_apply_def apply_def, blast) 
13223  1183 
done 
1184 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1185 
lemma (in M_basic) typed_function_abs [simp]: 
46823  1186 
"[ M(A); M(f) ] ==> typed_function(M,A,B,f) \<longleftrightarrow> f \<in> A > B" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1187 
apply (auto simp add: typed_function_def relation_def Pi_iff) 
13223  1188 
apply (blast dest: pair_components_in_M)+ 
1189 
done 

1190 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1191 
lemma (in M_basic) injection_abs [simp]: 
46823  1192 
"[ M(A); M(f) ] ==> injection(M,A,B,f) \<longleftrightarrow> f \<in> inj(A,B)" 
13223  1193 
apply (simp add: injection_def apply_iff inj_def apply_closed) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1194 
apply (blast dest: transM [of _ A]) 
13223  1195 
done 
1196 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1197 
lemma (in M_basic) surjection_abs [simp]: 
46823  1198 
"[ M(A); M(B); M(f) ] ==> surjection(M,A,B,f) \<longleftrightarrow> f \<in> surj(A,B)" 
13352  1199 
by (simp add: surjection_def surj_def) 
13223  1200 

13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1201 
lemma (in M_basic) bijection_abs [simp]: 
46823  1202 
"[ M(A); M(B); M(f) ] ==> bijection(M,A,B,f) \<longleftrightarrow> f \<in> bij(A,B)" 
13223  1203 
by (simp add: bijection_def bij_def) 
1204 

1205 

13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

1206 
subsubsection{*Composition of relations*} 
13223  1207 
