author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46823  57bf0cecb366 
child 58871  c399ae4b836f 
permissions  rwrr 
13494  1 
(* Title: ZF/Constructible/Satisfies_absolute.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3 
*) 

4 

13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

5 
header {*Absoluteness for the Satisfies Relation on Formulas*} 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

6 

16417  7 
theory Satisfies_absolute imports Datatype_absolute Rec_Separation begin 
13494  8 

9 

13687  10 
subsection {*More Internalization*} 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

11 

13494  12 
subsubsection{*The Formula @{term is_depth}, Internalized*} 
13 

14 
(* "is_depth(M,p,n) == 

15 
\<exists>sn[M]. \<exists>formula_n[M]. \<exists>formula_sn[M]. 

16 
2 1 0 

17 
is_formula_N(M,n,formula_n) & p \<notin> formula_n & 

18 
successor(M,n,sn) & is_formula_N(M,sn,formula_sn) & p \<in> formula_sn" *) 

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 
depth_fm :: "[i,i]=>i" where 
13494  21 
"depth_fm(p,n) == 
22 
Exists(Exists(Exists( 

23 
And(formula_N_fm(n#+3,1), 

24 
And(Neg(Member(p#+3,1)), 

25 
And(succ_fm(n#+3,2), 

26 
And(formula_N_fm(2,0), Member(p#+3,0))))))))" 

27 

28 
lemma depth_fm_type [TC]: 

29 
"[ x \<in> nat; y \<in> nat ] ==> depth_fm(x,y) \<in> formula" 

30 
by (simp add: depth_fm_def) 

31 

32 
lemma sats_depth_fm [simp]: 

33 
"[ x \<in> nat; y < length(env); env \<in> list(A)] 

46823  34 
==> sats(A, depth_fm(x,y), env) \<longleftrightarrow> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

35 
is_depth(##A, nth(x,env), nth(y,env))" 
13494  36 
apply (frule_tac x=y in lt_length_in_nat, assumption) 
37 
apply (simp add: depth_fm_def is_depth_def) 

38 
done 

39 

40 
lemma depth_iff_sats: 

41 
"[ nth(i,env) = x; nth(j,env) = y; 

42 
i \<in> nat; j < length(env); env \<in> list(A)] 

46823  43 
==> is_depth(##A, x, y) \<longleftrightarrow> sats(A, depth_fm(i,j), env)" 
13494  44 
by (simp add: sats_depth_fm) 
45 

46 
theorem depth_reflection: 

47 
"REFLECTS[\<lambda>x. is_depth(L, f(x), g(x)), 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

48 
\<lambda>i x. is_depth(##Lset(i), f(x), g(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13634
diff
changeset

49 
apply (simp only: is_depth_def) 
13494  50 
apply (intro FOL_reflections function_reflections formula_N_reflection) 
51 
done 

52 

53 

54 

55 
subsubsection{*The Operator @{term is_formula_case}*} 

56 

57 
text{*The arguments of @{term is_a} are always 2, 1, 0, and the formula 

58 
will be enclosed by three quantifiers.*} 

59 

60 
(* is_formula_case :: 

61 
"[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o" 

62 
"is_formula_case(M, is_a, is_b, is_c, is_d, v, z) == 

46823  63 
(\<forall>x[M]. \<forall>y[M]. x\<in>nat \<longrightarrow> y\<in>nat \<longrightarrow> is_Member(M,x,y,v) \<longrightarrow> is_a(x,y,z)) & 
64 
(\<forall>x[M]. \<forall>y[M]. x\<in>nat \<longrightarrow> y\<in>nat \<longrightarrow> is_Equal(M,x,y,v) \<longrightarrow> is_b(x,y,z)) & 

65 
(\<forall>x[M]. \<forall>y[M]. x\<in>formula \<longrightarrow> y\<in>formula \<longrightarrow> 

66 
is_Nand(M,x,y,v) \<longrightarrow> is_c(x,y,z)) & 

67 
(\<forall>x[M]. x\<in>formula \<longrightarrow> is_Forall(M,x,v) \<longrightarrow> is_d(x,z))" *) 

13494  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 
formula_case_fm :: "[i, i, i, i, i, i]=>i" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

71 
"formula_case_fm(is_a, is_b, is_c, is_d, v, z) == 
13494  72 
And(Forall(Forall(Implies(finite_ordinal_fm(1), 
73 
Implies(finite_ordinal_fm(0), 

74 
Implies(Member_fm(1,0,v#+2), 

75 
Forall(Implies(Equal(0,z#+3), is_a))))))), 

76 
And(Forall(Forall(Implies(finite_ordinal_fm(1), 

77 
Implies(finite_ordinal_fm(0), 

78 
Implies(Equal_fm(1,0,v#+2), 

79 
Forall(Implies(Equal(0,z#+3), is_b))))))), 

80 
And(Forall(Forall(Implies(mem_formula_fm(1), 

81 
Implies(mem_formula_fm(0), 

82 
Implies(Nand_fm(1,0,v#+2), 

83 
Forall(Implies(Equal(0,z#+3), is_c))))))), 

84 
Forall(Implies(mem_formula_fm(0), 

85 
Implies(Forall_fm(0,succ(v)), 

86 
Forall(Implies(Equal(0,z#+2), is_d))))))))" 

87 

88 

89 
lemma is_formula_case_type [TC]: 

90 
"[ is_a \<in> formula; is_b \<in> formula; is_c \<in> formula; is_d \<in> formula; 

91 
x \<in> nat; y \<in> nat ] 

92 
==> formula_case_fm(is_a, is_b, is_c, is_d, x, y) \<in> formula" 

93 
by (simp add: formula_case_fm_def) 

94 

95 
lemma sats_formula_case_fm: 

96 
assumes is_a_iff_sats: 

97 
"!!a0 a1 a2. 

98 
[a0\<in>A; a1\<in>A; a2\<in>A] 

46823  99 
==> ISA(a2, a1, a0) \<longleftrightarrow> sats(A, is_a, Cons(a0,Cons(a1,Cons(a2,env))))" 
13494  100 
and is_b_iff_sats: 
101 
"!!a0 a1 a2. 

102 
[a0\<in>A; a1\<in>A; a2\<in>A] 

46823  103 
==> ISB(a2, a1, a0) \<longleftrightarrow> sats(A, is_b, Cons(a0,Cons(a1,Cons(a2,env))))" 
13494  104 
and is_c_iff_sats: 
105 
"!!a0 a1 a2. 

106 
[a0\<in>A; a1\<in>A; a2\<in>A] 

46823  107 
==> ISC(a2, a1, a0) \<longleftrightarrow> sats(A, is_c, Cons(a0,Cons(a1,Cons(a2,env))))" 
13494  108 
and is_d_iff_sats: 
109 
"!!a0 a1. 

110 
[a0\<in>A; a1\<in>A] 

46823  111 
==> ISD(a1, a0) \<longleftrightarrow> sats(A, is_d, Cons(a0,Cons(a1,env)))" 
13494  112 
shows 
113 
"[x \<in> nat; y < length(env); env \<in> list(A)] 

46823  114 
==> sats(A, formula_case_fm(is_a,is_b,is_c,is_d,x,y), env) \<longleftrightarrow> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

115 
is_formula_case(##A, ISA, ISB, ISC, ISD, nth(x,env), nth(y,env))" 
13494  116 
apply (frule_tac x=y in lt_length_in_nat, assumption) 
117 
apply (simp add: formula_case_fm_def is_formula_case_def 

118 
is_a_iff_sats [THEN iff_sym] is_b_iff_sats [THEN iff_sym] 

119 
is_c_iff_sats [THEN iff_sym] is_d_iff_sats [THEN iff_sym]) 

120 
done 

121 

122 
lemma formula_case_iff_sats: 

123 
assumes is_a_iff_sats: 

124 
"!!a0 a1 a2. 

125 
[a0\<in>A; a1\<in>A; a2\<in>A] 

46823  126 
==> ISA(a2, a1, a0) \<longleftrightarrow> sats(A, is_a, Cons(a0,Cons(a1,Cons(a2,env))))" 
13494  127 
and is_b_iff_sats: 
128 
"!!a0 a1 a2. 

129 
[a0\<in>A; a1\<in>A; a2\<in>A] 

46823  130 
==> ISB(a2, a1, a0) \<longleftrightarrow> sats(A, is_b, Cons(a0,Cons(a1,Cons(a2,env))))" 
13494  131 
and is_c_iff_sats: 
132 
"!!a0 a1 a2. 

133 
[a0\<in>A; a1\<in>A; a2\<in>A] 

46823  134 
==> ISC(a2, a1, a0) \<longleftrightarrow> sats(A, is_c, Cons(a0,Cons(a1,Cons(a2,env))))" 
13494  135 
and is_d_iff_sats: 
136 
"!!a0 a1. 

137 
[a0\<in>A; a1\<in>A] 

46823  138 
==> ISD(a1, a0) \<longleftrightarrow> sats(A, is_d, Cons(a0,Cons(a1,env)))" 
13494  139 
shows 
140 
"[nth(i,env) = x; nth(j,env) = y; 

141 
i \<in> nat; j < length(env); env \<in> list(A)] 

46823  142 
==> is_formula_case(##A, ISA, ISB, ISC, ISD, x, y) \<longleftrightarrow> 
13494  143 
sats(A, formula_case_fm(is_a,is_b,is_c,is_d,i,j), env)" 
144 
by (simp add: sats_formula_case_fm [OF is_a_iff_sats is_b_iff_sats 

145 
is_c_iff_sats is_d_iff_sats]) 

146 

147 

148 
text{*The second argument of @{term is_a} gives it direct access to @{term x}, 

149 
which is essential for handling free variable references. Treatment is 

150 
based on that of @{text is_nat_case_reflection}.*} 

151 
theorem is_formula_case_reflection: 

152 
assumes is_a_reflection: 

153 
"!!h f g g'. REFLECTS[\<lambda>x. is_a(L, h(x), f(x), g(x), g'(x)), 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

154 
\<lambda>i x. is_a(##Lset(i), h(x), f(x), g(x), g'(x))]" 
13494  155 
and is_b_reflection: 
156 
"!!h f g g'. REFLECTS[\<lambda>x. is_b(L, h(x), f(x), g(x), g'(x)), 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

157 
\<lambda>i x. is_b(##Lset(i), h(x), f(x), g(x), g'(x))]" 
13494  158 
and is_c_reflection: 
159 
"!!h f g g'. REFLECTS[\<lambda>x. is_c(L, h(x), f(x), g(x), g'(x)), 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

160 
\<lambda>i x. is_c(##Lset(i), h(x), f(x), g(x), g'(x))]" 
13494  161 
and is_d_reflection: 
162 
"!!h f g g'. REFLECTS[\<lambda>x. is_d(L, h(x), f(x), g(x)), 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

163 
\<lambda>i x. is_d(##Lset(i), h(x), f(x), g(x))]" 
13494  164 
shows "REFLECTS[\<lambda>x. is_formula_case(L, is_a(L,x), is_b(L,x), is_c(L,x), is_d(L,x), g(x), h(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

165 
\<lambda>i x. is_formula_case(##Lset(i), is_a(##Lset(i), x), is_b(##Lset(i), x), is_c(##Lset(i), x), is_d(##Lset(i), x), g(x), h(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13634
diff
changeset

166 
apply (simp (no_asm_use) only: is_formula_case_def) 
13494  167 
apply (intro FOL_reflections function_reflections finite_ordinal_reflection 
168 
mem_formula_reflection 

169 
Member_reflection Equal_reflection Nand_reflection Forall_reflection 

170 
is_a_reflection is_b_reflection is_c_reflection is_d_reflection) 

171 
done 

172 

173 

174 

175 
subsection {*Absoluteness for the Function @{term satisfies}*} 

176 

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

178 
is_depth_apply :: "[i=>o,i,i,i] => o" where 
13494  179 
{*Merely a useful abbreviation for the sequel.*} 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

180 
"is_depth_apply(M,h,p,z) == 
13494  181 
\<exists>dp[M]. \<exists>sdp[M]. \<exists>hsdp[M]. 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

182 
finite_ordinal(M,dp) & is_depth(M,p,dp) & successor(M,dp,sdp) & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

183 
fun_apply(M,h,sdp,hsdp) & fun_apply(M,hsdp,p,z)" 
13494  184 

185 
lemma (in M_datatypes) is_depth_apply_abs [simp]: 

186 
"[M(h); p \<in> formula; M(z)] 

46823  187 
==> is_depth_apply(M,h,p,z) \<longleftrightarrow> z = h ` succ(depth(p)) ` p" 
13494  188 
by (simp add: is_depth_apply_def formula_into_M depth_type eq_commute) 
189 

190 

191 

192 
text{*There is at present some redundancy between the relativizations in 

193 
e.g. @{text satisfies_is_a} and those in e.g. @{text Member_replacement}.*} 

194 

195 
text{*These constants let us instantiate the parameters @{term a}, @{term b}, 

13504  196 
@{term c}, @{term d}, etc., of the locale @{text Formula_Rec}.*} 
21233  197 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

198 
satisfies_a :: "[i,i,i]=>i" where 
13494  199 
"satisfies_a(A) == 
200 
\<lambda>x y. \<lambda>env \<in> list(A). bool_of_o (nth(x,env) \<in> nth(y,env))" 

201 

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

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

203 
satisfies_is_a :: "[i=>o,i,i,i,i]=>o" where 
13494  204 
"satisfies_is_a(M,A) == 
46823  205 
\<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow> 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

206 
is_lambda(M, lA, 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

207 
\<lambda>env z. is_bool_of_o(M, 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

208 
\<exists>nx[M]. \<exists>ny[M]. 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

209 
is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & nx \<in> ny, z), 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

210 
zz)" 
13494  211 

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

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

213 
satisfies_b :: "[i,i,i]=>i" where 
13494  214 
"satisfies_b(A) == 
215 
\<lambda>x y. \<lambda>env \<in> list(A). bool_of_o (nth(x,env) = nth(y,env))" 

216 

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

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

218 
satisfies_is_b :: "[i=>o,i,i,i,i]=>o" where 
13494  219 
{*We simplify the formula to have just @{term nx} rather than 
220 
introducing @{term ny} with @{term "nx=ny"} *} 

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

221 
"satisfies_is_b(M,A) == 
46823  222 
\<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow> 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

223 
is_lambda(M, lA, 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

224 
\<lambda>env z. is_bool_of_o(M, 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

225 
\<exists>nx[M]. is_nth(M,x,env,nx) & is_nth(M,y,env,nx), z), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

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

227 

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

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

229 
satisfies_c :: "[i,i,i,i,i]=>i" where 
13502  230 
"satisfies_c(A) == \<lambda>p q rp rq. \<lambda>env \<in> list(A). not(rp ` env and rq ` env)" 
13494  231 

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

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

233 
satisfies_is_c :: "[i=>o,i,i,i,i,i]=>o" where 
13494  234 
"satisfies_is_c(M,A,h) == 
46823  235 
\<lambda>p q zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow> 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

236 
is_lambda(M, lA, \<lambda>env z. \<exists>hp[M]. \<exists>hq[M]. 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

237 
(\<exists>rp[M]. is_depth_apply(M,h,p,rp) & fun_apply(M,rp,env,hp)) & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

238 
(\<exists>rq[M]. is_depth_apply(M,h,q,rq) & fun_apply(M,rq,env,hq)) & 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

239 
(\<exists>pq[M]. is_and(M,hp,hq,pq) & is_not(M,pq,z)), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

240 
zz)" 
13494  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 
satisfies_d :: "[i,i,i]=>i" where 
13494  244 
"satisfies_d(A) 
245 
== \<lambda>p rp. \<lambda>env \<in> list(A). bool_of_o (\<forall>x\<in>A. rp ` (Cons(x,env)) = 1)" 

246 

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

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

248 
satisfies_is_d :: "[i=>o,i,i,i,i]=>o" where 
13494  249 
"satisfies_is_d(M,A,h) == 
46823  250 
\<lambda>p zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow> 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

251 
is_lambda(M, lA, 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

252 
\<lambda>env z. \<exists>rp[M]. is_depth_apply(M,h,p,rp) & 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

253 
is_bool_of_o(M, 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

254 
\<forall>x[M]. \<forall>xenv[M]. \<forall>hp[M]. 
46823  255 
x\<in>A \<longrightarrow> is_Cons(M,x,env,xenv) \<longrightarrow> 
256 
fun_apply(M,rp,xenv,hp) \<longrightarrow> number1(M,hp), 

13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

257 
z), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

258 
zz)" 
13494  259 

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

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

261 
satisfies_MH :: "[i=>o,i,i,i,i]=>o" where 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

262 
{*The variable @{term u} is unused, but gives @{term satisfies_MH} 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

263 
the correct arity.*} 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

264 
"satisfies_MH == 
13502  265 
\<lambda>M A u f z. 
46823  266 
\<forall>fml[M]. is_formula(M,fml) \<longrightarrow> 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

267 
is_lambda (M, fml, 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

268 
is_formula_case (M, satisfies_is_a(M,A), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

269 
satisfies_is_b(M,A), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

270 
satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)), 
13502  271 
z)" 
13494  272 

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

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

274 
is_satisfies :: "[i=>o,i,i,i]=>o" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

275 
"is_satisfies(M,A) == is_formula_rec (M, satisfies_MH(M,A))" 
13502  276 

277 

278 
text{*This lemma relates the fragments defined above to the original primitive 

279 
recursion in @{term satisfies}. 

280 
Induction is not required: the definitions are directly equal!*} 

281 
lemma satisfies_eq: 

282 
"satisfies(A,p) = 

283 
formula_rec (satisfies_a(A), satisfies_b(A), 

284 
satisfies_c(A), satisfies_d(A), p)" 

285 
by (simp add: satisfies_formula_def satisfies_a_def satisfies_b_def 

286 
satisfies_c_def satisfies_d_def) 

13494  287 

288 
text{*Further constraints on the class @{term M} in order to prove 

289 
absoluteness for the constants defined above. The ultimate goal 

290 
is the absoluteness of the function @{term satisfies}. *} 

13502  291 
locale M_satisfies = M_eclose + 
13494  292 
assumes 
293 
Member_replacement: 

294 
"[M(A); x \<in> nat; y \<in> nat] 

295 
==> strong_replacement 

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

296 
(M, \<lambda>env z. \<exists>bo[M]. \<exists>nx[M]. \<exists>ny[M]. 
13494  297 
env \<in> list(A) & is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & 
298 
is_bool_of_o(M, nx \<in> ny, bo) & 

299 
pair(M, env, bo, z))" 

300 
and 

301 
Equal_replacement: 

302 
"[M(A); x \<in> nat; y \<in> nat] 

303 
==> strong_replacement 

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

304 
(M, \<lambda>env z. \<exists>bo[M]. \<exists>nx[M]. \<exists>ny[M]. 
13494  305 
env \<in> list(A) & is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & 
306 
is_bool_of_o(M, nx = ny, bo) & 

307 
pair(M, env, bo, z))" 

308 
and 

309 
Nand_replacement: 

310 
"[M(A); M(rp); M(rq)] 

311 
==> strong_replacement 

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

312 
(M, \<lambda>env z. \<exists>rpe[M]. \<exists>rqe[M]. \<exists>andpq[M]. \<exists>notpq[M]. 
13494  313 
fun_apply(M,rp,env,rpe) & fun_apply(M,rq,env,rqe) & 
314 
is_and(M,rpe,rqe,andpq) & is_not(M,andpq,notpq) & 

315 
env \<in> list(A) & pair(M, env, notpq, z))" 

316 
and 

317 
Forall_replacement: 

318 
"[M(A); M(rp)] 

319 
==> strong_replacement 

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

320 
(M, \<lambda>env z. \<exists>bo[M]. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

321 
env \<in> list(A) & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

322 
is_bool_of_o (M, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

323 
\<forall>a[M]. \<forall>co[M]. \<forall>rpco[M]. 
46823  324 
a\<in>A \<longrightarrow> is_Cons(M,a,env,co) \<longrightarrow> 
325 
fun_apply(M,rp,co,rpco) \<longrightarrow> number1(M, rpco), 

13494  326 
bo) & 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

327 
pair(M,env,bo,z))" 
13494  328 
and 
329 
formula_rec_replacement: 

330 
{*For the @{term transrec}*} 

331 
"[n \<in> nat; M(A)] ==> transrec_replacement(M, satisfies_MH(M,A), n)" 

332 
and 

333 
formula_rec_lambda_replacement: 

334 
{*For the @{text "\<lambda>abstraction"} in the @{term transrec} body*} 

13502  335 
"[M(g); M(A)] ==> 
336 
strong_replacement (M, 

337 
\<lambda>x y. mem_formula(M,x) & 

338 
(\<exists>c[M]. is_formula_case(M, satisfies_is_a(M,A), 

339 
satisfies_is_b(M,A), 

340 
satisfies_is_c(M,A,g), 

341 
satisfies_is_d(M,A,g), x, c) & 

342 
pair(M, x, c, y)))" 

13494  343 

344 

345 
lemma (in M_satisfies) Member_replacement': 

346 
"[M(A); x \<in> nat; y \<in> nat] 

347 
==> strong_replacement 

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

348 
(M, \<lambda>env z. env \<in> list(A) & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

349 
z = \<langle>env, bool_of_o(nth(x, env) \<in> nth(y, env))\<rangle>)" 
13494  350 
by (insert Member_replacement, simp) 
351 

352 
lemma (in M_satisfies) Equal_replacement': 

353 
"[M(A); x \<in> nat; y \<in> nat] 

354 
==> strong_replacement 

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

355 
(M, \<lambda>env z. env \<in> list(A) & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

356 
z = \<langle>env, bool_of_o(nth(x, env) = nth(y, env))\<rangle>)" 
13494  357 
by (insert Equal_replacement, simp) 
358 

359 
lemma (in M_satisfies) Nand_replacement': 

360 
"[M(A); M(rp); M(rq)] 

361 
==> strong_replacement 

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

362 
(M, \<lambda>env z. env \<in> list(A) & z = \<langle>env, not(rp`env and rq`env)\<rangle>)" 
13494  363 
by (insert Nand_replacement, simp) 
364 

365 
lemma (in M_satisfies) Forall_replacement': 

366 
"[M(A); M(rp)] 

367 
==> strong_replacement 

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

368 
(M, \<lambda>env z. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

369 
env \<in> list(A) & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

370 
z = \<langle>env, bool_of_o (\<forall>a\<in>A. rp ` Cons(a,env) = 1)\<rangle>)" 
13494  371 
by (insert Forall_replacement, simp) 
372 

373 
lemma (in M_satisfies) a_closed: 

374 
"[M(A); x\<in>nat; y\<in>nat] ==> M(satisfies_a(A,x,y))" 

375 
apply (simp add: satisfies_a_def) 

376 
apply (blast intro: lam_closed2 Member_replacement') 

377 
done 

378 

379 
lemma (in M_satisfies) a_rel: 

13634  380 
"M(A) ==> Relation2(M, nat, nat, satisfies_is_a(M,A), satisfies_a(A))" 
381 
apply (simp add: Relation2_def satisfies_is_a_def satisfies_a_def) 

13702  382 
apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def) 
13494  383 
done 
384 

385 
lemma (in M_satisfies) b_closed: 

386 
"[M(A); x\<in>nat; y\<in>nat] ==> M(satisfies_b(A,x,y))" 

387 
apply (simp add: satisfies_b_def) 

388 
apply (blast intro: lam_closed2 Equal_replacement') 

389 
done 

390 

391 
lemma (in M_satisfies) b_rel: 

13634  392 
"M(A) ==> Relation2(M, nat, nat, satisfies_is_b(M,A), satisfies_b(A))" 
393 
apply (simp add: Relation2_def satisfies_is_b_def satisfies_b_def) 

13702  394 
apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def) 
13494  395 
done 
396 

397 
lemma (in M_satisfies) c_closed: 

398 
"[M(A); x \<in> formula; y \<in> formula; M(rx); M(ry)] 

399 
==> M(satisfies_c(A,x,y,rx,ry))" 

400 
apply (simp add: satisfies_c_def) 

401 
apply (rule lam_closed2) 

402 
apply (rule Nand_replacement') 

403 
apply (simp_all add: formula_into_M list_into_M [of _ A]) 

404 
done 

405 

406 
lemma (in M_satisfies) c_rel: 

407 
"[M(A); M(f)] ==> 

13634  408 
Relation2 (M, formula, formula, 
13494  409 
satisfies_is_c(M,A,f), 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

410 
\<lambda>u v. satisfies_c(A, u, v, f ` succ(depth(u)) ` u, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

411 
f ` succ(depth(v)) ` v))" 
13634  412 
apply (simp add: Relation2_def satisfies_is_c_def satisfies_c_def) 
13702  413 
apply (auto del: iffI intro!: lambda_abs2 
414 
simp add: Relation1_def formula_into_M) 

13494  415 
done 
416 

417 
lemma (in M_satisfies) d_closed: 

418 
"[M(A); x \<in> formula; M(rx)] ==> M(satisfies_d(A,x,rx))" 

419 
apply (simp add: satisfies_d_def) 

420 
apply (rule lam_closed2) 

421 
apply (rule Forall_replacement') 

422 
apply (simp_all add: formula_into_M list_into_M [of _ A]) 

423 
done 

424 

425 
lemma (in M_satisfies) d_rel: 

426 
"[M(A); M(f)] ==> 

13634  427 
Relation1(M, formula, satisfies_is_d(M,A,f), 
13494  428 
\<lambda>u. satisfies_d(A, u, f ` succ(depth(u)) ` u))" 
429 
apply (simp del: rall_abs 

13634  430 
add: Relation1_def satisfies_is_d_def satisfies_d_def) 
13702  431 
apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def) 
13494  432 
done 
433 

434 

435 
lemma (in M_satisfies) fr_replace: 

436 
"[n \<in> nat; M(A)] ==> transrec_replacement(M,satisfies_MH(M,A),n)" 

437 
by (blast intro: formula_rec_replacement) 

438 

13502  439 
lemma (in M_satisfies) formula_case_satisfies_closed: 
440 
"[M(g); M(A); x \<in> formula] ==> 

441 
M(formula_case (satisfies_a(A), satisfies_b(A), 

442 
\<lambda>u v. satisfies_c(A, u, v, 

443 
g ` succ(depth(u)) ` u, g ` succ(depth(v)) ` v), 

444 
\<lambda>u. satisfies_d (A, u, g ` succ(depth(u)) ` u), 

445 
x))" 

446 
by (blast intro: formula_case_closed a_closed b_closed c_closed d_closed) 

447 

13494  448 
lemma (in M_satisfies) fr_lam_replace: 
13502  449 
"[M(g); M(A)] ==> 
13494  450 
strong_replacement (M, \<lambda>x y. x \<in> formula & 
451 
y = \<langle>x, 

452 
formula_rec_case(satisfies_a(A), 

453 
satisfies_b(A), 

454 
satisfies_c(A), 

455 
satisfies_d(A), g, x)\<rangle>)" 

13502  456 
apply (insert formula_rec_lambda_replacement) 
457 
apply (simp add: formula_rec_case_def formula_case_satisfies_closed 

458 
formula_case_abs [OF a_rel b_rel c_rel d_rel]) 

459 
done 

13494  460 

461 

462 

13504  463 
text{*Instantiate locale @{text Formula_Rec} for the 
13502  464 
Function @{term satisfies}*} 
13494  465 

13504  466 
lemma (in M_satisfies) Formula_Rec_axioms_M: 
13502  467 
"M(A) ==> 
13504  468 
Formula_Rec_axioms(M, satisfies_a(A), satisfies_is_a(M,A), 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

469 
satisfies_b(A), satisfies_is_b(M,A), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

470 
satisfies_c(A), satisfies_is_c(M,A), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

471 
satisfies_d(A), satisfies_is_d(M,A))" 
13504  472 
apply (rule Formula_Rec_axioms.intro) 
13502  473 
apply (assumption  
474 
rule a_closed a_rel b_closed b_rel c_closed c_rel d_closed d_rel 

475 
fr_replace [unfolded satisfies_MH_def] 

476 
fr_lam_replace) + 

13494  477 
done 
478 

479 

13504  480 
theorem (in M_satisfies) Formula_Rec_M: 
13502  481 
"M(A) ==> 
13504  482 
PROP Formula_Rec(M, satisfies_a(A), satisfies_is_a(M,A), 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

483 
satisfies_b(A), satisfies_is_b(M,A), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

484 
satisfies_c(A), satisfies_is_c(M,A), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

485 
satisfies_d(A), satisfies_is_d(M,A))" 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset

486 
apply (rule Formula_Rec.intro) 
23464  487 
apply (rule M_satisfies.axioms, rule M_satisfies_axioms) 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset

488 
apply (erule Formula_Rec_axioms_M) 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset

489 
done 
13494  490 

13502  491 
lemmas (in M_satisfies) 
13535  492 
satisfies_closed' = Formula_Rec.formula_rec_closed [OF Formula_Rec_M] 
493 
and satisfies_abs' = Formula_Rec.formula_rec_abs [OF Formula_Rec_M] 

13494  494 

495 

13502  496 
lemma (in M_satisfies) satisfies_closed: 
497 
"[M(A); p \<in> formula] ==> M(satisfies(A,p))" 

13504  498 
by (simp add: Formula_Rec.formula_rec_closed [OF Formula_Rec_M] 
13502  499 
satisfies_eq) 
13494  500 

13502  501 
lemma (in M_satisfies) satisfies_abs: 
502 
"[M(A); M(z); p \<in> formula] 

46823  503 
==> is_satisfies(M,A,p,z) \<longleftrightarrow> z = satisfies(A,p)" 
13504  504 
by (simp only: Formula_Rec.formula_rec_abs [OF Formula_Rec_M] 
13503  505 
satisfies_eq is_satisfies_def satisfies_MH_def) 
13494  506 

507 

13502  508 
subsection{*Internalizations Needed to Instantiate @{text "M_satisfies"}*} 
13494  509 

13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

510 
subsubsection{*The Operator @{term is_depth_apply}, Internalized*} 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

511 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

512 
(* is_depth_apply(M,h,p,z) == 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

513 
\<exists>dp[M]. \<exists>sdp[M]. \<exists>hsdp[M]. 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

514 
2 1 0 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

515 
finite_ordinal(M,dp) & is_depth(M,p,dp) & successor(M,dp,sdp) & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

516 
fun_apply(M,h,sdp,hsdp) & fun_apply(M,hsdp,p,z) *) 
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 
depth_apply_fm :: "[i,i,i]=>i" where 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

519 
"depth_apply_fm(h,p,z) == 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

520 
Exists(Exists(Exists( 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

521 
And(finite_ordinal_fm(2), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

522 
And(depth_fm(p#+3,2), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

523 
And(succ_fm(2,1), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

524 
And(fun_apply_fm(h#+3,1,0), fun_apply_fm(0,p#+3,z#+3))))))))" 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

525 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

526 
lemma depth_apply_type [TC]: 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

527 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> depth_apply_fm(x,y,z) \<in> formula" 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

528 
by (simp add: depth_apply_fm_def) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

529 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

530 
lemma sats_depth_apply_fm [simp]: 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

531 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 
46823  532 
==> sats(A, depth_apply_fm(x,y,z), env) \<longleftrightarrow> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

533 
is_depth_apply(##A, nth(x,env), nth(y,env), nth(z,env))" 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

534 
by (simp add: depth_apply_fm_def is_depth_apply_def) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

535 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

536 
lemma depth_apply_iff_sats: 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

537 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

538 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
46823  539 
==> is_depth_apply(##A, x, y, z) \<longleftrightarrow> sats(A, depth_apply_fm(i,j,k), env)" 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

540 
by simp 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

541 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

542 
lemma depth_apply_reflection: 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

543 
"REFLECTS[\<lambda>x. is_depth_apply(L,f(x),g(x),h(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

544 
\<lambda>i x. is_depth_apply(##Lset(i),f(x),g(x),h(x))]" 
13655
95b95cdb4704
Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents:
13634
diff
changeset

545 
apply (simp only: is_depth_apply_def) 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

546 
apply (intro FOL_reflections function_reflections depth_reflection 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

547 
finite_ordinal_reflection) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

548 
done 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

549 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

550 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

551 
subsubsection{*The Operator @{term satisfies_is_a}, Internalized*} 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

552 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

553 
(* satisfies_is_a(M,A) == 
46823  554 
\<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow> 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

555 
is_lambda(M, lA, 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

556 
\<lambda>env z. is_bool_of_o(M, 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

557 
\<exists>nx[M]. \<exists>ny[M]. 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

558 
is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & nx \<in> ny, z), 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

559 
zz) *) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

560 

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

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

562 
satisfies_is_a_fm :: "[i,i,i,i]=>i" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

563 
"satisfies_is_a_fm(A,x,y,z) == 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

564 
Forall( 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

565 
Implies(is_list_fm(succ(A),0), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

566 
lambda_fm( 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

567 
bool_of_o_fm(Exists( 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

568 
Exists(And(nth_fm(x#+6,3,1), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

569 
And(nth_fm(y#+6,3,0), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

570 
Member(1,0))))), 0), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

571 
0, succ(z))))" 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

572 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

573 
lemma satisfies_is_a_type [TC]: 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

574 
"[ A \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat ] 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

575 
==> satisfies_is_a_fm(A,x,y,z) \<in> formula" 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

576 
by (simp add: satisfies_is_a_fm_def) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

577 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

578 
lemma sats_satisfies_is_a_fm [simp]: 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

579 
"[ u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)] 
46823  580 
==> sats(A, satisfies_is_a_fm(u,x,y,z), env) \<longleftrightarrow> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

581 
satisfies_is_a(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))" 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

582 
apply (frule_tac x=x in lt_length_in_nat, assumption) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

583 
apply (frule_tac x=y in lt_length_in_nat, assumption) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

584 
apply (simp add: satisfies_is_a_fm_def satisfies_is_a_def sats_lambda_fm 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

585 
sats_bool_of_o_fm) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

586 
done 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

587 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

588 
lemma satisfies_is_a_iff_sats: 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

589 
"[ nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz; 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

590 
u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)] 
46823  591 
==> satisfies_is_a(##A,nu,nx,ny,nz) \<longleftrightarrow> 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

592 
sats(A, satisfies_is_a_fm(u,x,y,z), env)" 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

593 
by simp 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

594 

13494  595 
theorem satisfies_is_a_reflection: 
596 
"REFLECTS[\<lambda>x. satisfies_is_a(L,f(x),g(x),h(x),g'(x)), 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

597 
\<lambda>i x. satisfies_is_a(##Lset(i),f(x),g(x),h(x),g'(x))]" 
13494  598 
apply (unfold satisfies_is_a_def) 
599 
apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection 

13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

600 
nth_reflection is_list_reflection) 
13494  601 
done 
602 

603 

13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

604 
subsubsection{*The Operator @{term satisfies_is_b}, Internalized*} 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

605 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

606 
(* satisfies_is_b(M,A) == 
46823  607 
\<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow> 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

608 
is_lambda(M, lA, 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

609 
\<lambda>env z. is_bool_of_o(M, 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

610 
\<exists>nx[M]. is_nth(M,x,env,nx) & is_nth(M,y,env,nx), z), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

611 
zz) *) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

612 

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

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

614 
satisfies_is_b_fm :: "[i,i,i,i]=>i" where 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

615 
"satisfies_is_b_fm(A,x,y,z) == 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

616 
Forall( 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

617 
Implies(is_list_fm(succ(A),0), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

618 
lambda_fm( 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

619 
bool_of_o_fm(Exists(And(nth_fm(x#+5,2,0), nth_fm(y#+5,2,0))), 0), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

620 
0, succ(z))))" 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

621 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

622 
lemma satisfies_is_b_type [TC]: 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

623 
"[ A \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat ] 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

624 
==> satisfies_is_b_fm(A,x,y,z) \<in> formula" 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

625 
by (simp add: satisfies_is_b_fm_def) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

626 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

627 
lemma sats_satisfies_is_b_fm [simp]: 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

628 
"[ u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)] 
46823  629 
==> sats(A, satisfies_is_b_fm(u,x,y,z), env) \<longleftrightarrow> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

630 
satisfies_is_b(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))" 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

631 
apply (frule_tac x=x in lt_length_in_nat, assumption) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

632 
apply (frule_tac x=y in lt_length_in_nat, assumption) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

633 
apply (simp add: satisfies_is_b_fm_def satisfies_is_b_def sats_lambda_fm 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

634 
sats_bool_of_o_fm) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

635 
done 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

636 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

637 
lemma satisfies_is_b_iff_sats: 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

638 
"[ nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz; 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

639 
u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)] 
46823  640 
==> satisfies_is_b(##A,nu,nx,ny,nz) \<longleftrightarrow> 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

641 
sats(A, satisfies_is_b_fm(u,x,y,z), env)" 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

642 
by simp 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

643 

13494  644 
theorem satisfies_is_b_reflection: 
645 
"REFLECTS[\<lambda>x. satisfies_is_b(L,f(x),g(x),h(x),g'(x)), 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

646 
\<lambda>i x. satisfies_is_b(##Lset(i),f(x),g(x),h(x),g'(x))]" 
13494  647 
apply (unfold satisfies_is_b_def) 
648 
apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection 

13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

649 
nth_reflection is_list_reflection) 
13494  650 
done 
651 

13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

652 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

653 
subsubsection{*The Operator @{term satisfies_is_c}, Internalized*} 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

654 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

655 
(* satisfies_is_c(M,A,h) == 
46823  656 
\<lambda>p q zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow> 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

657 
is_lambda(M, lA, \<lambda>env z. \<exists>hp[M]. \<exists>hq[M]. 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

658 
(\<exists>rp[M]. is_depth_apply(M,h,p,rp) & fun_apply(M,rp,env,hp)) & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

659 
(\<exists>rq[M]. is_depth_apply(M,h,q,rq) & fun_apply(M,rq,env,hq)) & 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

660 
(\<exists>pq[M]. is_and(M,hp,hq,pq) & is_not(M,pq,z)), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

661 
zz) *) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

662 

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

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

664 
satisfies_is_c_fm :: "[i,i,i,i,i]=>i" where 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

665 
"satisfies_is_c_fm(A,h,p,q,zz) == 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

666 
Forall( 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

667 
Implies(is_list_fm(succ(A),0), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

668 
lambda_fm( 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

669 
Exists(Exists( 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

670 
And(Exists(And(depth_apply_fm(h#+7,p#+7,0), fun_apply_fm(0,4,2))), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

671 
And(Exists(And(depth_apply_fm(h#+7,q#+7,0), fun_apply_fm(0,4,1))), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

672 
Exists(And(and_fm(2,1,0), not_fm(0,3))))))), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

673 
0, succ(zz))))" 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

674 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

675 
lemma satisfies_is_c_type [TC]: 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

676 
"[ A \<in> nat; h \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat ] 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

677 
==> satisfies_is_c_fm(A,h,x,y,z) \<in> formula" 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

678 
by (simp add: satisfies_is_c_fm_def) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

679 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

680 
lemma sats_satisfies_is_c_fm [simp]: 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

681 
"[ u \<in> nat; v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 
46823  682 
==> sats(A, satisfies_is_c_fm(u,v,x,y,z), env) \<longleftrightarrow> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

683 
satisfies_is_c(##A, nth(u,env), nth(v,env), nth(x,env), 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

684 
nth(y,env), nth(z,env))" 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

685 
by (simp add: satisfies_is_c_fm_def satisfies_is_c_def sats_lambda_fm) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

686 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

687 
lemma satisfies_is_c_iff_sats: 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

688 
"[ nth(u,env) = nu; nth(v,env) = nv; nth(x,env) = nx; nth(y,env) = ny; 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

689 
nth(z,env) = nz; 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

690 
u \<in> nat; v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 
46823  691 
==> satisfies_is_c(##A,nu,nv,nx,ny,nz) \<longleftrightarrow> 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

692 
sats(A, satisfies_is_c_fm(u,v,x,y,z), env)" 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

693 
by simp 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

694 

13494  695 
theorem satisfies_is_c_reflection: 
696 
"REFLECTS[\<lambda>x. satisfies_is_c(L,f(x),g(x),h(x),g'(x),h'(x)), 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

697 
\<lambda>i x. satisfies_is_c(##Lset(i),f(x),g(x),h(x),g'(x),h'(x))]" 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

698 
apply (unfold satisfies_is_c_def) 
13494  699 
apply (intro FOL_reflections function_reflections is_lambda_reflection 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

700 
extra_reflections nth_reflection depth_apply_reflection 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

701 
is_list_reflection) 
13494  702 
done 
703 

13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

704 
subsubsection{*The Operator @{term satisfies_is_d}, Internalized*} 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

705 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

706 
(* satisfies_is_d(M,A,h) == 
46823  707 
\<lambda>p zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow> 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

708 
is_lambda(M, lA, 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

709 
\<lambda>env z. \<exists>rp[M]. is_depth_apply(M,h,p,rp) & 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

710 
is_bool_of_o(M, 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

711 
\<forall>x[M]. \<forall>xenv[M]. \<forall>hp[M]. 
46823  712 
x\<in>A \<longrightarrow> is_Cons(M,x,env,xenv) \<longrightarrow> 
713 
fun_apply(M,rp,xenv,hp) \<longrightarrow> number1(M,hp), 

13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

714 
z), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

715 
zz) *) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

716 

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

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

718 
satisfies_is_d_fm :: "[i,i,i,i]=>i" where 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

719 
"satisfies_is_d_fm(A,h,p,zz) == 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

720 
Forall( 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

721 
Implies(is_list_fm(succ(A),0), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

722 
lambda_fm( 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

723 
Exists( 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

724 
And(depth_apply_fm(h#+5,p#+5,0), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

725 
bool_of_o_fm( 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

726 
Forall(Forall(Forall( 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

727 
Implies(Member(2,A#+8), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

728 
Implies(Cons_fm(2,5,1), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

729 
Implies(fun_apply_fm(3,1,0), number1_fm(0))))))), 1))), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

730 
0, succ(zz))))" 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

731 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

732 
lemma satisfies_is_d_type [TC]: 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

733 
"[ A \<in> nat; h \<in> nat; x \<in> nat; z \<in> nat ] 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

734 
==> satisfies_is_d_fm(A,h,x,z) \<in> formula" 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

735 
by (simp add: satisfies_is_d_fm_def) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

736 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

737 
lemma sats_satisfies_is_d_fm [simp]: 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

738 
"[ u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 
46823  739 
==> sats(A, satisfies_is_d_fm(u,x,y,z), env) \<longleftrightarrow> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

740 
satisfies_is_d(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))" 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

741 
by (simp add: satisfies_is_d_fm_def satisfies_is_d_def sats_lambda_fm 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

742 
sats_bool_of_o_fm) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

743 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

744 
lemma satisfies_is_d_iff_sats: 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

745 
"[ nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz; 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

746 
u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 
46823  747 
==> satisfies_is_d(##A,nu,nx,ny,nz) \<longleftrightarrow> 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

748 
sats(A, satisfies_is_d_fm(u,x,y,z), env)" 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

749 
by simp 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

750 

13494  751 
theorem satisfies_is_d_reflection: 
752 
"REFLECTS[\<lambda>x. satisfies_is_d(L,f(x),g(x),h(x),g'(x)), 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

753 
\<lambda>i x. satisfies_is_d(##Lset(i),f(x),g(x),h(x),g'(x))]" 
13505  754 
apply (unfold satisfies_is_d_def) 
13494  755 
apply (intro FOL_reflections function_reflections is_lambda_reflection 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

756 
extra_reflections nth_reflection depth_apply_reflection 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

757 
is_list_reflection) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

758 
done 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

759 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

760 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

761 
subsubsection{*The Operator @{term satisfies_MH}, Internalized*} 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

762 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

763 
(* satisfies_MH == 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

764 
\<lambda>M A u f zz. 
46823  765 
\<forall>fml[M]. is_formula(M,fml) \<longrightarrow> 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

766 
is_lambda (M, fml, 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

767 
is_formula_case (M, satisfies_is_a(M,A), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

768 
satisfies_is_b(M,A), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

769 
satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

770 
zz) *) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

771 

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

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

773 
satisfies_MH_fm :: "[i,i,i,i]=>i" where 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

774 
"satisfies_MH_fm(A,u,f,zz) == 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

775 
Forall( 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

776 
Implies(is_formula_fm(0), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

777 
lambda_fm( 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

778 
formula_case_fm(satisfies_is_a_fm(A#+7,2,1,0), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

779 
satisfies_is_b_fm(A#+7,2,1,0), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

780 
satisfies_is_c_fm(A#+7,f#+7,2,1,0), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

781 
satisfies_is_d_fm(A#+6,f#+6,1,0), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

782 
1, 0), 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

783 
0, succ(zz))))" 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

784 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

785 
lemma satisfies_MH_type [TC]: 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

786 
"[ A \<in> nat; u \<in> nat; x \<in> nat; z \<in> nat ] 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

787 
==> satisfies_MH_fm(A,u,x,z) \<in> formula" 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

788 
by (simp add: satisfies_MH_fm_def) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

789 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

790 
lemma sats_satisfies_MH_fm [simp]: 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

791 
"[ u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 
46823  792 
==> sats(A, satisfies_MH_fm(u,x,y,z), env) \<longleftrightarrow> 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

793 
satisfies_MH(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))" 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

794 
by (simp add: satisfies_MH_fm_def satisfies_MH_def sats_lambda_fm 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

795 
sats_formula_case_fm) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

796 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

797 
lemma satisfies_MH_iff_sats: 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

798 
"[ nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz; 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

799 
u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 
46823  800 
==> satisfies_MH(##A,nu,nx,ny,nz) \<longleftrightarrow> 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

801 
sats(A, satisfies_MH_fm(u,x,y,z), env)" 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

802 
by simp 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

803 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

804 
lemmas satisfies_reflections = 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

805 
is_lambda_reflection is_formula_reflection 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

806 
is_formula_case_reflection 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

807 
satisfies_is_a_reflection satisfies_is_b_reflection 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

808 
satisfies_is_c_reflection satisfies_is_d_reflection 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

809 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

810 
theorem satisfies_MH_reflection: 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

811 
"REFLECTS[\<lambda>x. satisfies_MH(L,f(x),g(x),h(x),g'(x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

812 
\<lambda>i x. satisfies_MH(##Lset(i),f(x),g(x),h(x),g'(x))]" 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

813 
apply (unfold satisfies_MH_def) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

814 
apply (intro FOL_reflections satisfies_reflections) 
13494  815 
done 
816 

817 

13502  818 
subsection{*Lemmas for Instantiating the Locale @{text "M_satisfies"}*} 
819 

820 

821 
subsubsection{*The @{term "Member"} Case*} 

822 

823 
lemma Member_Reflects: 

824 
"REFLECTS[\<lambda>u. \<exists>v[L]. v \<in> B \<and> (\<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L]. 

825 
v \<in> lstA \<and> is_nth(L,x,v,nx) \<and> is_nth(L,y,v,ny) \<and> 

826 
is_bool_of_o(L, nx \<in> ny, bo) \<and> pair(L,v,bo,u)), 

827 
\<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B \<and> (\<exists>bo \<in> Lset(i). \<exists>nx \<in> Lset(i). \<exists>ny \<in> Lset(i). 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

828 
v \<in> lstA \<and> is_nth(##Lset(i), x, v, nx) \<and> 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

829 
is_nth(##Lset(i), y, v, ny) \<and> 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

830 
is_bool_of_o(##Lset(i), nx \<in> ny, bo) \<and> pair(##Lset(i), v, bo, u))]" 
13502  831 
by (intro FOL_reflections function_reflections nth_reflection 
832 
bool_of_o_reflection) 

833 

834 

835 
lemma Member_replacement: 

836 
"[L(A); x \<in> nat; y \<in> nat] 

837 
==> strong_replacement 

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

838 
(L, \<lambda>env z. \<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L]. 
13502  839 
env \<in> list(A) & is_nth(L,x,env,nx) & is_nth(L,y,env,ny) & 
840 
is_bool_of_o(L, nx \<in> ny, bo) & 

841 
pair(L, env, bo, z))" 

13566  842 
apply (rule strong_replacementI) 
843 
apply (rule_tac u="{list(A),B,x,y}" 

13687  844 
in gen_separation_multi [OF Member_Reflects], 
845 
auto simp add: nat_into_M list_closed) 

846 
apply (rule_tac env="[list(A),B,x,y]" in DPow_LsetI) 

13566  847 
apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats  simp)+ 
13502  848 
done 
849 

850 

851 
subsubsection{*The @{term "Equal"} Case*} 

852 

853 
lemma Equal_Reflects: 

854 
"REFLECTS[\<lambda>u. \<exists>v[L]. v \<in> B \<and> (\<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L]. 

855 
v \<in> lstA \<and> is_nth(L, x, v, nx) \<and> is_nth(L, y, v, ny) \<and> 

856 
is_bool_of_o(L, nx = ny, bo) \<and> pair(L, v, bo, u)), 

857 
\<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B \<and> (\<exists>bo \<in> Lset(i). \<exists>nx \<in> Lset(i). \<exists>ny \<in> Lset(i). 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

858 
v \<in> lstA \<and> is_nth(##Lset(i), x, v, nx) \<and> 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

859 
is_nth(##Lset(i), y, v, ny) \<and> 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

860 
is_bool_of_o(##Lset(i), nx = ny, bo) \<and> pair(##Lset(i), v, bo, u))]" 
13502  861 
by (intro FOL_reflections function_reflections nth_reflection 
862 
bool_of_o_reflection) 

863 

864 

865 
lemma Equal_replacement: 

866 
"[L(A); x \<in> nat; y \<in> nat] 

867 
==> strong_replacement 

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

868 
(L, \<lambda>env z. \<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L]. 
13502  869 
env \<in> list(A) & is_nth(L,x,env,nx) & is_nth(L,y,env,ny) & 
870 
is_bool_of_o(L, nx = ny, bo) & 

871 
pair(L, env, bo, z))" 

13566  872 
apply (rule strong_replacementI) 
873 
apply (rule_tac u="{list(A),B,x,y}" 

13687  874 
in gen_separation_multi [OF Equal_Reflects], 
875 
auto simp add: nat_into_M list_closed) 

876 
apply (rule_tac env="[list(A),B,x,y]" in DPow_LsetI) 

13566  877 
apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats  simp)+ 
13502  878 
done 
879 

880 
subsubsection{*The @{term "Nand"} Case*} 

881 

882 
lemma Nand_Reflects: 

883 
"REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and> 

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

884 
(\<exists>rpe[L]. \<exists>rqe[L]. \<exists>andpq[L]. \<exists>notpq[L]. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

885 
fun_apply(L, rp, u, rpe) \<and> fun_apply(L, rq, u, rqe) \<and> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

886 
is_and(L, rpe, rqe, andpq) \<and> is_not(L, andpq, notpq) \<and> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

887 
u \<in> list(A) \<and> pair(L, u, notpq, x)), 
13502  888 
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> 
889 
(\<exists>rpe \<in> Lset(i). \<exists>rqe \<in> Lset(i). \<exists>andpq \<in> Lset(i). \<exists>notpq \<in> Lset(i). 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

890 
fun_apply(##Lset(i), rp, u, rpe) \<and> fun_apply(##Lset(i), rq, u, rqe) \<and> 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

891 
is_and(##Lset(i), rpe, rqe, andpq) \<and> is_not(##Lset(i), andpq, notpq) \<and> 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

892 
u \<in> list(A) \<and> pair(##Lset(i), u, notpq, x))]" 
13502  893 
apply (unfold is_and_def is_not_def) 
894 
apply (intro FOL_reflections function_reflections) 

895 
done 

896 

897 
lemma Nand_replacement: 

898 
"[L(A); L(rp); L(rq)] 

899 
==> strong_replacement 

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

900 
(L, \<lambda>env z. \<exists>rpe[L]. \<exists>rqe[L]. \<exists>andpq[L]. \<exists>notpq[L]. 
13502  901 
fun_apply(L,rp,env,rpe) & fun_apply(L,rq,env,rqe) & 
902 
is_and(L,rpe,rqe,andpq) & is_not(L,andpq,notpq) & 

903 
env \<in> list(A) & pair(L, env, notpq, z))" 

13566  904 
apply (rule strong_replacementI) 
13687  905 
apply (rule_tac u="{list(A),B,rp,rq}" 
906 
in gen_separation_multi [OF Nand_Reflects], 

907 
auto simp add: list_closed) 

908 
apply (rule_tac env="[list(A),B,rp,rq]" in DPow_LsetI) 

13566  909 
apply (rule sep_rules is_and_iff_sats is_not_iff_sats  simp)+ 
13502  910 
done 
911 

912 

913 
subsubsection{*The @{term "Forall"} Case*} 

914 

915 
lemma Forall_Reflects: 

916 
"REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>bo[L]. u \<in> list(A) \<and> 

917 
is_bool_of_o (L, 

918 
\<forall>a[L]. \<forall>co[L]. \<forall>rpco[L]. a \<in> A \<longrightarrow> 

919 
is_Cons(L,a,u,co) \<longrightarrow> fun_apply(L,rp,co,rpco) \<longrightarrow> 

920 
number1(L,rpco), 

921 
bo) \<and> pair(L,u,bo,x)), 

922 
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>bo \<in> Lset(i). u \<in> list(A) \<and> 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

923 
is_bool_of_o (##Lset(i), 
13502  924 
\<forall>a \<in> Lset(i). \<forall>co \<in> Lset(i). \<forall>rpco \<in> Lset(i). a \<in> A \<longrightarrow> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

925 
is_Cons(##Lset(i),a,u,co) \<longrightarrow> fun_apply(##Lset(i),rp,co,rpco) \<longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

926 
number1(##Lset(i),rpco), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

927 
bo) \<and> pair(##Lset(i),u,bo,x))]" 
13502  928 
apply (unfold is_bool_of_o_def) 
929 
apply (intro FOL_reflections function_reflections Cons_reflection) 

930 
done 

931 

932 
lemma Forall_replacement: 

933 
"[L(A); L(rp)] 

934 
==> strong_replacement 

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

935 
(L, \<lambda>env z. \<exists>bo[L]. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

936 
env \<in> list(A) & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

937 
is_bool_of_o (L, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

938 
\<forall>a[L]. \<forall>co[L]. \<forall>rpco[L]. 
46823  939 
a\<in>A \<longrightarrow> is_Cons(L,a,env,co) \<longrightarrow> 
940 
fun_apply(L,rp,co,rpco) \<longrightarrow> number1(L, rpco), 

13502  941 
bo) & 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

942 
pair(L,env,bo,z))" 
13566  943 
apply (rule strong_replacementI) 
13687  944 
apply (rule_tac u="{A,list(A),B,rp}" 
945 
in gen_separation_multi [OF Forall_Reflects], 

946 
auto simp add: list_closed) 

947 
apply (rule_tac env="[A,list(A),B,rp]" in DPow_LsetI) 

13566  948 
apply (rule sep_rules is_bool_of_o_iff_sats Cons_iff_sats  simp)+ 
13502  949 
done 
950 

951 
subsubsection{*The @{term "transrec_replacement"} Case*} 

952 

13494  953 
lemma formula_rec_replacement_Reflects: 
954 
"REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L, u, y, x) \<and> 

955 
is_wfrec (L, satisfies_MH(L,A), mesa, u, y)), 

13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

956 
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) \<and> 
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

957 
is_wfrec (##Lset(i), satisfies_MH(##Lset(i),A), mesa, u, y))]" 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

958 
by (intro FOL_reflections function_reflections satisfies_MH_reflection 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

959 
is_wfrec_reflection) 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

960 

6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

961 
lemma formula_rec_replacement: 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

962 
{*For the @{term transrec}*} 
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

963 
"[n \<in> nat; L(A)] ==> transrec_replacement(L, satisfies_MH(L,A), n)" 
13566  964 
apply (rule transrec_replacementI, simp add: nat_into_M) 
13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

965 
apply (rule strong_replacementI) 
13566  966 
apply (rule_tac u="{B,A,n,Memrel(eclose({n}))}" 
13687  967 
in gen_separation_multi [OF formula_rec_replacement_Reflects], 
968 
auto simp add: nat_into_M) 

969 
apply (rule_tac env="[B,A,n,Memrel(eclose({n}))]" in DPow_LsetI) 

13496
6f0c57def6d5
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
paulson
parents:
13494
diff
changeset

970 
apply (rule sep_rules satisfies_MH_iff_sats is_wfrec_iff_sats  simp)+ 
13494  971 
done 
972 

13502  973 

974 
subsubsection{*The Lambda Replacement Case*} 

975 

976 
lemma formula_rec_lambda_replacement_Reflects: 

977 
"REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B & 

978 
mem_formula(L,u) & 

979 
(\<exists>c[L]. 

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

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

981 
(L, satisfies_is_a(L,A), satisfies_is_b(L,A), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

982 
satisfies_is_c(L,A,g), satisfies_is_d(L,A,g), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

983 
u, c) & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

984 
pair(L,u,c,x)), 
13807
a28a8fbc76d4
changed ** to ## to avoid conflict with new comment syntax
paulson
parents:
13702
diff
changeset

985 
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & mem_formula(##Lset(i),u) & 
13502  986 
(\<exists>c \<in> Lset(i). 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

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

988 
(##Lset(i), satisfies_is_a(##Lset(i),A), satisfies_is_b(##Lset(i),A), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

989 
satisfies_is_c(##Lset(i),A,g), satisfies_is_d(##Lset(i),A,g), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

990 
u, c) & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23464
diff
changeset

991 
pair(##Lset(i),u,c,x))]" 
13502  992 
by (intro FOL_reflections function_reflections mem_formula_reflection 
993 
is_formula_case_reflection satisfies_is_a_reflection 

994 
satisfies_is_b_reflection satisfies_is_c_reflection 

995 
satisfies_is_d_reflection) 

996 

997 
lemma formula_rec_lambda_replacement: 

998 
{*For the @{term transrec}*} 

999 
"[L(g); L(A)] ==> 

1000 
strong_replacement (L, 

1001 
\<lambda>x y. mem_formula(L,x) & 

1002 
(\<exists>c[L]. is_formula_case(L, satisfies_is_a(L,A), 

1003 
satisfies_is_b(L,A), 

1004 
satisfies_is_c(L,A,g), 

1005 
satisfies_is_d(L,A,g), x, c) & 

1006 
pair(L, x, c, y)))" 

1007 
apply (rule strong_replacementI) 

13566  1008 
apply (rule_tac u="{B,A,g}" 
13687  1009 
in gen_separation_multi [OF formula_rec_lambda_replacement_Reflects], 
1010 
auto) 

1011 
apply (rule_tac env="[A,g,B]" in DPow_LsetI) 

13502  1012 
apply (rule sep_rules mem_formula_iff_sats 
1013 
formula_case_iff_sats satisfies_is_a_iff_sats 

1014 
satisfies_is_b_iff_sats satisfies_is_c_iff_sats 

1015 
satisfies_is_d_iff_sats  simp)+ 

1016 
done 

1017 

1018 

1019 
subsection{*Instantiating @{text M_satisfies}*} 

1020 

1021 
lemma M_satisfies_axioms_L: "M_satisfies_axioms(L)" 

1022 
apply (rule M_satisfies_axioms.intro) 

1023 
apply (assumption  rule 

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

1024 
Member_replacement Equal_replacement 
13502  1025 
Nand_replacement Forall_replacement 
1026 
formula_rec_replacement formula_rec_lambda_replacement)+ 

1027 
done 

1028 

1029 
theorem M_satisfies_L: "PROP M_satisfies(L)" 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset

1030 
apply (rule M_satisfies.intro) 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset

1031 
apply (rule M_eclose_L) 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset

1032 
apply (rule M_satisfies_axioms_L) 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
16417
diff
changeset

1033 
done 
13502  1034 

13504  1035 
text{*Finally: the point of the whole theory!*} 
1036 
lemmas satisfies_closed = M_satisfies.satisfies_closed [OF M_satisfies_L] 

1037 
and satisfies_abs = M_satisfies.satisfies_abs [OF M_satisfies_L] 

1038 

13494  1039 
end 