author  wenzelm 
Mon, 23 Mar 2015 21:05:17 +0100  
changeset 59788  6f7b6adac439 
parent 58871  c399ae4b836f 
child 60770  240563fbf41d 
permissions  rwrr 
13505  1 
(* Title: ZF/Constructible/Relative.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3 
*) 

4 

58871  5 
section {*Relativization and Absoluteness*} 
13223  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) 
13290
28ce81eff3de
separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents:
13269
diff
changeset

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

757 

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

760 

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

762 
makes relativization easier.*} 

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

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

766 
apply (simp add: RepFun_def) 

767 
apply (frule strong_replacement_closed, assumption) 

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

768 
apply (auto dest: transM simp add: Replace_conj_eq univalent_def) 
13353  769 
done 
770 

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

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

772 

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

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

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

777 
(\<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

778 

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

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

780 
"[ 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

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

782 
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

783 

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

784 
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

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

786 
"[strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>); 
46823  787 
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

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

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

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

791 

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

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

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

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

801 
apply (blast dest: transM) 

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

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

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

804 

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

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

806 
"[ A=A'; z=z'; 
46823  807 
!!x y. [ x\<in>A; M(x); M(y) ] ==> is_b(x,y) \<longleftrightarrow> is_b'(x,y) ] 
808 
==> 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

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

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

811 

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

812 
lemma (in M_trivial) image_abs [simp]: 
46823  813 
"[ 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

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

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

816 
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

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

818 

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

819 
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

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

821 

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

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

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

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

825 

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

826 
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

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

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

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

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

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

833 

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

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

835 

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

836 
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

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

838 
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

839 

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

840 
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

841 
"[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

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

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

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

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

846 

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

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

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

851 
lemma (in M_trivial) nat_case_abs [simp]: 
13634  852 
"[ relation1(M,is_b,b); M(k); M(z) ] 
46823  853 
==> 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

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

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

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

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

859 
apply (elim disjE exE) 
13634  860 
apply (simp_all add: relation1_def) 
13350  861 
done 
862 

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

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

13434  866 
lemma is_nat_case_cong: 
13352  867 
"[ a = a'; k = k'; z = z'; M(z'); 
46823  868 
!!x y. [ M(x); M(y) ] ==> is_b(x,y) \<longleftrightarrow> is_b'(x,y) ] 
869 
==> 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

870 
by (simp add: is_nat_case_def) 
13352  871 

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

872 

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

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

874 
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

875 

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

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

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

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

879 

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

880 
lemma (in M_trivial) transitive_set_abs [simp]: 
46823  881 
"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

882 
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

883 

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

884 
lemma (in M_trivial) ordinal_abs [simp]: 
46823  885 
"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

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

887 

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

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

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

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

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

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

894 

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

895 
lemma (in M_trivial) successor_ordinal_abs [simp]: 
46823  896 
"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

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

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

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

900 

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

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

902 
"[ 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

903 
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

904 

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

905 
lemma (in M_trivial) finite_ordinal_abs [simp]: 
46823  906 
"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

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

908 
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

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

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

911 

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

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

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

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

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

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

917 
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

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

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

920 

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

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

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

924 
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

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

926 

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

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

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

930 

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

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

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

934 

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

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

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

938 

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

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

940 

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

941 
(*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

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

943 
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

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

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

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

947 

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

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

949 
"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

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

951 
(\<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

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

953 

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

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

956 
"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

957 

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

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

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

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

961 

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

962 
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

963 

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

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

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

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

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

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

976 
"M(r) ==> separation(M, 
13298  977 
\<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  978 
and restrict_separation: 
13268  979 
"M(A) ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. pair(M,x,y,z)))" 
13223  980 
and comp_separation: 
981 
"[ M(r); M(s) ] 

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

982 
==> 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

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

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

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

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

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

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

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

999 
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

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

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

1003 
lemma (in M_basic) cartprod_iff_lemma: 
46823  1004 
"[ M(C); \<forall>u[M]. u \<in> C \<longleftrightarrow> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}); 
13254  1005 
powerset(M, A \<union> B, p1); powerset(M, p1, p2); M(p2) ] 
13223  1006 
==> 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

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

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

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

1013 
apply (frule transM, assumption, force) 
13223  1014 
done 
1015 

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

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

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

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

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

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

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

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

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

1028 
apply (blast, clarify) 
59788  1029 
apply (drule_tac x=z and P="\<lambda>x. rex(M,Q(x))" for Q in rspec) 
13299  1030 
apply assumption 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1031 
apply (blast intro: cartprod_iff_lemma) 
13223  1032 
done 
1033 

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

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

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

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

1042 
apply (insert cartprod_separation [of A B], simp) 
13223  1043 
done 
1044 

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

1046 
I should have used Replacement instead!*} 

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

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

1050 

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

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

1054 

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

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

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

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

1061 
by (simp add: Inl_def) 
13397  1062 

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

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

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

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

1069 
by (simp add: Inr_def) 
13397  1070 

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

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

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

1075 

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

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

1077 

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

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

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

1080 
converse(r) = 
46823  1081 
{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

1082 
\<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

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

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

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

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

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

1088 

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

1089 
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

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

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

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

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

1094 

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

1095 
lemma (in M_basic) converse_abs [simp]: 
46823  1096 
"[ 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

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

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

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

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

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

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

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

1104 

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

1105 

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

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

1107 

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

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

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

1111 
apply (insert image_separation [of A r], simp) 
13223  1112 
done 
1113 

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

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

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

1118 
apply (blast intro!: equalityI dest: transM, blast) 
13223  1119 
done 
1120 

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

1121 
lemma (in M_basic) vimage_closed [intro,simp]: 
13223  1122 
"[ 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

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

1124 

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

1125 

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

1126 
subsubsection{*Domain, range and field*} 
13223  1127 

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

1128 
lemma (in M_basic) domain_abs [simp]: 
46823  1129 
"[ 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

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

1131 
apply (blast intro!: equalityI dest: transM) 
13223  1132 
done 
1133 

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

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

1137 
done 

1138 

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

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

1143 
done 

1144 

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

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

1148 
done 

1149 

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

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

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

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

1156 
by (simp add: domain_closed range_closed Un_closed field_def) 
13245  1157 

1158 

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

1159 
subsubsection{*Relations, functions and application*} 
13254  1160 

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

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

1163 
apply (simp add: is_relation_def relation_def) 
13223  1164 
apply (blast dest!: bspec dest: pair_components_in_M)+ 
1165 
done 

1166 

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

1167 
lemma (in M_basic) function_abs [simp]: 
46823  1168 
"M(r) ==> is_function(M,r) \<longleftrightarrow> function(r)" 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1169 
apply (simp add: is_function_def function_def, safe) 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1170 
apply (frule transM, assumption) 
13223  1171 
apply (blast dest: pair_components_in_M)+ 
1172 
done 

1173 

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

1174 
lemma (in M_basic) apply_closed [intro,simp]: 
13223  1175 
"[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

1176 
by (simp add: apply_def) 
13223  1177 

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

1178 
lemma (in M_basic) apply_abs [simp]: 
46823  1179 
"[ 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

1180 
apply (simp add: fun_apply_def apply_def, blast) 
13223  1181 
done 
1182 

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

1183 
lemma (in M_basic) typed_function_abs [simp]: 
46823  1184 
"[ 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

1185 
apply (auto simp add: typed_function_def relation_def Pi_iff) 
13223  1186 
apply (blast dest: pair_components_in_M)+ 
1187 
done 

1188 

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

1189 
lemma (in M_basic) injection_abs [simp]: 
46823  1190 
"[ M(A); M(f) ] ==> injection(M,A,B,f) \<longleftrightarrow> f \<in> inj(A,B)" 
13223  1191 
apply (simp add: injection_def apply_iff inj_def apply_closed) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1192 
apply (blast dest: transM [of _ A]) 
13223  1193 
done 
1194 

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

1195 
lemma (in M_basic) surjection_abs [simp]: 
46823  1196 
"[ M(A); M(B); M(f) ] ==> surjection(M,A,B,f) \<longleftrightarrow> f \<in> surj(A,B)" 
13352  1197 
by (simp add: surjection_def surj_def) 
13223  1198 

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

1199 
lemma (in M_basic) bijection_abs [simp]: 
46823  1200 
"[ M(A); M(B); M(f) ] ==> bijection(M,A,B,f) \<longleftrightarrow> f \<in> bij(A,B)" 
13223  1201 
by (simp add: bijection_def bij_def) 
1202 

1203 

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

1204 
subsubsection{*Composition of relations*} 
13223  1205 

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

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

1207 
"[ M(r); M(s) ] 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1208 
==> r O s = 
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

1209 
{xz \<in> domain(s) * range(r). 
13268  1210 
\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. xz = \<langle>x,z\<rangle> & \<langle>x,y\<rangle> \<in> s & \<langle>y,z\<rangle> \<in> r}" 
13223  1211 
apply (simp add: comp_def) 
13628
87482b5e3f2e
Various simplifications of the Constructible theories
paulson
parents:
13615
diff
changeset

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

1213 