src/ZF/Constructible/Satisfies_absolute.thy
author ballarin
Thu Dec 11 18:30:26 2008 +0100 (2008-12-11)
changeset 29223 e09c53289830
parent 23464 bc2563c37b1a
child 32960 69916a850301
permissions -rw-r--r--
Conversion of HOL-Main and ZF to new locales.
paulson@13494
     1
(*  Title:      ZF/Constructible/Satisfies_absolute.thy
paulson@13634
     2
    ID:  $Id$
paulson@13494
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@13494
     4
*)
paulson@13494
     5
paulson@13496
     6
header {*Absoluteness for the Satisfies Relation on Formulas*}
paulson@13496
     7
haftmann@16417
     8
theory Satisfies_absolute imports Datatype_absolute Rec_Separation begin 
paulson@13494
     9
paulson@13494
    10
paulson@13687
    11
subsection {*More Internalization*}
paulson@13496
    12
paulson@13494
    13
subsubsection{*The Formula @{term is_depth}, Internalized*}
paulson@13494
    14
paulson@13494
    15
(*    "is_depth(M,p,n) == 
paulson@13494
    16
       \<exists>sn[M]. \<exists>formula_n[M]. \<exists>formula_sn[M]. 
paulson@13494
    17
         2          1                0
paulson@13494
    18
        is_formula_N(M,n,formula_n) & p \<notin> formula_n &
paulson@13494
    19
        successor(M,n,sn) & is_formula_N(M,sn,formula_sn) & p \<in> formula_sn" *)
wenzelm@21404
    20
definition
wenzelm@21404
    21
  depth_fm :: "[i,i]=>i" where
paulson@13494
    22
  "depth_fm(p,n) == 
paulson@13494
    23
     Exists(Exists(Exists(
paulson@13494
    24
       And(formula_N_fm(n#+3,1),
paulson@13494
    25
         And(Neg(Member(p#+3,1)),
paulson@13494
    26
          And(succ_fm(n#+3,2),
paulson@13494
    27
           And(formula_N_fm(2,0), Member(p#+3,0))))))))"
paulson@13494
    28
paulson@13494
    29
lemma depth_fm_type [TC]:
paulson@13494
    30
 "[| x \<in> nat; y \<in> nat |] ==> depth_fm(x,y) \<in> formula"
paulson@13494
    31
by (simp add: depth_fm_def)
paulson@13494
    32
paulson@13494
    33
lemma sats_depth_fm [simp]:
paulson@13494
    34
   "[| x \<in> nat; y < length(env); env \<in> list(A)|]
paulson@13494
    35
    ==> sats(A, depth_fm(x,y), env) <->
paulson@13807
    36
        is_depth(##A, nth(x,env), nth(y,env))"
paulson@13494
    37
apply (frule_tac x=y in lt_length_in_nat, assumption)  
paulson@13494
    38
apply (simp add: depth_fm_def is_depth_def) 
paulson@13494
    39
done
paulson@13494
    40
paulson@13494
    41
lemma depth_iff_sats:
paulson@13494
    42
      "[| nth(i,env) = x; nth(j,env) = y; 
paulson@13494
    43
          i \<in> nat; j < length(env); env \<in> list(A)|]
paulson@13807
    44
       ==> is_depth(##A, x, y) <-> sats(A, depth_fm(i,j), env)"
paulson@13494
    45
by (simp add: sats_depth_fm)
paulson@13494
    46
paulson@13494
    47
theorem depth_reflection:
paulson@13494
    48
     "REFLECTS[\<lambda>x. is_depth(L, f(x), g(x)),  
paulson@13807
    49
               \<lambda>i x. is_depth(##Lset(i), f(x), g(x))]"
paulson@13655
    50
apply (simp only: is_depth_def)
paulson@13494
    51
apply (intro FOL_reflections function_reflections formula_N_reflection) 
paulson@13494
    52
done
paulson@13494
    53
paulson@13494
    54
paulson@13494
    55
paulson@13494
    56
subsubsection{*The Operator @{term is_formula_case}*}
paulson@13494
    57
paulson@13494
    58
text{*The arguments of @{term is_a} are always 2, 1, 0, and the formula
paulson@13494
    59
      will be enclosed by three quantifiers.*}
paulson@13494
    60
paulson@13494
    61
(* is_formula_case :: 
paulson@13494
    62
    "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o"
paulson@13494
    63
  "is_formula_case(M, is_a, is_b, is_c, is_d, v, z) == 
paulson@13494
    64
      (\<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> is_Member(M,x,y,v) --> is_a(x,y,z)) &
paulson@13494
    65
      (\<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> is_Equal(M,x,y,v) --> is_b(x,y,z)) &
paulson@13494
    66
      (\<forall>x[M]. \<forall>y[M]. x\<in>formula --> y\<in>formula --> 
paulson@13494
    67
                     is_Nand(M,x,y,v) --> is_c(x,y,z)) &
paulson@13494
    68
      (\<forall>x[M]. x\<in>formula --> is_Forall(M,x,v) --> is_d(x,z))" *)
paulson@13494
    69
wenzelm@21404
    70
definition
wenzelm@21404
    71
  formula_case_fm :: "[i, i, i, i, i, i]=>i" where
wenzelm@21404
    72
  "formula_case_fm(is_a, is_b, is_c, is_d, v, z) == 
paulson@13494
    73
        And(Forall(Forall(Implies(finite_ordinal_fm(1), 
paulson@13494
    74
                           Implies(finite_ordinal_fm(0), 
paulson@13494
    75
                            Implies(Member_fm(1,0,v#+2), 
paulson@13494
    76
                             Forall(Implies(Equal(0,z#+3), is_a))))))),
paulson@13494
    77
        And(Forall(Forall(Implies(finite_ordinal_fm(1), 
paulson@13494
    78
                           Implies(finite_ordinal_fm(0), 
paulson@13494
    79
                            Implies(Equal_fm(1,0,v#+2), 
paulson@13494
    80
                             Forall(Implies(Equal(0,z#+3), is_b))))))),
paulson@13494
    81
        And(Forall(Forall(Implies(mem_formula_fm(1), 
paulson@13494
    82
                           Implies(mem_formula_fm(0), 
paulson@13494
    83
                            Implies(Nand_fm(1,0,v#+2), 
paulson@13494
    84
                             Forall(Implies(Equal(0,z#+3), is_c))))))),
paulson@13494
    85
        Forall(Implies(mem_formula_fm(0), 
paulson@13494
    86
                       Implies(Forall_fm(0,succ(v)), 
paulson@13494
    87
                             Forall(Implies(Equal(0,z#+2), is_d))))))))"
paulson@13494
    88
paulson@13494
    89
paulson@13494
    90
lemma is_formula_case_type [TC]:
paulson@13494
    91
     "[| is_a \<in> formula;  is_b \<in> formula;  is_c \<in> formula;  is_d \<in> formula;  
paulson@13494
    92
         x \<in> nat; y \<in> nat |] 
paulson@13494
    93
      ==> formula_case_fm(is_a, is_b, is_c, is_d, x, y) \<in> formula"
paulson@13494
    94
by (simp add: formula_case_fm_def)
paulson@13494
    95
paulson@13494
    96
lemma sats_formula_case_fm:
paulson@13494
    97
  assumes is_a_iff_sats: 
paulson@13494
    98
      "!!a0 a1 a2. 
paulson@13494
    99
        [|a0\<in>A; a1\<in>A; a2\<in>A|]  
paulson@13494
   100
        ==> ISA(a2, a1, a0) <-> sats(A, is_a, Cons(a0,Cons(a1,Cons(a2,env))))"
paulson@13494
   101
  and is_b_iff_sats: 
paulson@13494
   102
      "!!a0 a1 a2. 
paulson@13494
   103
        [|a0\<in>A; a1\<in>A; a2\<in>A|]  
paulson@13494
   104
        ==> ISB(a2, a1, a0) <-> sats(A, is_b, Cons(a0,Cons(a1,Cons(a2,env))))"
paulson@13494
   105
  and is_c_iff_sats: 
paulson@13494
   106
      "!!a0 a1 a2. 
paulson@13494
   107
        [|a0\<in>A; a1\<in>A; a2\<in>A|]  
paulson@13494
   108
        ==> ISC(a2, a1, a0) <-> sats(A, is_c, Cons(a0,Cons(a1,Cons(a2,env))))"
paulson@13494
   109
  and is_d_iff_sats: 
paulson@13494
   110
      "!!a0 a1. 
paulson@13494
   111
        [|a0\<in>A; a1\<in>A|]  
paulson@13494
   112
        ==> ISD(a1, a0) <-> sats(A, is_d, Cons(a0,Cons(a1,env)))"
paulson@13494
   113
  shows 
paulson@13494
   114
      "[|x \<in> nat; y < length(env); env \<in> list(A)|]
paulson@13494
   115
       ==> sats(A, formula_case_fm(is_a,is_b,is_c,is_d,x,y), env) <->
paulson@13807
   116
           is_formula_case(##A, ISA, ISB, ISC, ISD, nth(x,env), nth(y,env))"
paulson@13494
   117
apply (frule_tac x=y in lt_length_in_nat, assumption)  
paulson@13494
   118
apply (simp add: formula_case_fm_def is_formula_case_def 
paulson@13494
   119
                 is_a_iff_sats [THEN iff_sym] is_b_iff_sats [THEN iff_sym]
paulson@13494
   120
                 is_c_iff_sats [THEN iff_sym] is_d_iff_sats [THEN iff_sym])
paulson@13494
   121
done
paulson@13494
   122
paulson@13494
   123
lemma formula_case_iff_sats:
paulson@13494
   124
  assumes is_a_iff_sats: 
paulson@13494
   125
      "!!a0 a1 a2. 
paulson@13494
   126
        [|a0\<in>A; a1\<in>A; a2\<in>A|]  
paulson@13494
   127
        ==> ISA(a2, a1, a0) <-> sats(A, is_a, Cons(a0,Cons(a1,Cons(a2,env))))"
paulson@13494
   128
  and is_b_iff_sats: 
paulson@13494
   129
      "!!a0 a1 a2. 
paulson@13494
   130
        [|a0\<in>A; a1\<in>A; a2\<in>A|]  
paulson@13494
   131
        ==> ISB(a2, a1, a0) <-> sats(A, is_b, Cons(a0,Cons(a1,Cons(a2,env))))"
paulson@13494
   132
  and is_c_iff_sats: 
paulson@13494
   133
      "!!a0 a1 a2. 
paulson@13494
   134
        [|a0\<in>A; a1\<in>A; a2\<in>A|]  
paulson@13494
   135
        ==> ISC(a2, a1, a0) <-> sats(A, is_c, Cons(a0,Cons(a1,Cons(a2,env))))"
paulson@13494
   136
  and is_d_iff_sats: 
paulson@13494
   137
      "!!a0 a1. 
paulson@13494
   138
        [|a0\<in>A; a1\<in>A|]  
paulson@13494
   139
        ==> ISD(a1, a0) <-> sats(A, is_d, Cons(a0,Cons(a1,env)))"
paulson@13494
   140
  shows 
paulson@13494
   141
      "[|nth(i,env) = x; nth(j,env) = y; 
paulson@13494
   142
      i \<in> nat; j < length(env); env \<in> list(A)|]
paulson@13807
   143
       ==> is_formula_case(##A, ISA, ISB, ISC, ISD, x, y) <->
paulson@13494
   144
           sats(A, formula_case_fm(is_a,is_b,is_c,is_d,i,j), env)"
paulson@13494
   145
by (simp add: sats_formula_case_fm [OF is_a_iff_sats is_b_iff_sats 
paulson@13494
   146
                                       is_c_iff_sats is_d_iff_sats])
paulson@13494
   147
paulson@13494
   148
paulson@13494
   149
text{*The second argument of @{term is_a} gives it direct access to @{term x},
paulson@13494
   150
  which is essential for handling free variable references.  Treatment is
paulson@13494
   151
  based on that of @{text is_nat_case_reflection}.*}
paulson@13494
   152
theorem is_formula_case_reflection:
paulson@13494
   153
  assumes is_a_reflection:
paulson@13494
   154
    "!!h f g g'. REFLECTS[\<lambda>x. is_a(L, h(x), f(x), g(x), g'(x)),
paulson@13807
   155
                     \<lambda>i x. is_a(##Lset(i), h(x), f(x), g(x), g'(x))]"
paulson@13494
   156
  and is_b_reflection:
paulson@13494
   157
    "!!h f g g'. REFLECTS[\<lambda>x. is_b(L, h(x), f(x), g(x), g'(x)),
paulson@13807
   158
                     \<lambda>i x. is_b(##Lset(i), h(x), f(x), g(x), g'(x))]"
paulson@13494
   159
  and is_c_reflection:
paulson@13494
   160
    "!!h f g g'. REFLECTS[\<lambda>x. is_c(L, h(x), f(x), g(x), g'(x)),
paulson@13807
   161
                     \<lambda>i x. is_c(##Lset(i), h(x), f(x), g(x), g'(x))]"
paulson@13494
   162
  and is_d_reflection:
paulson@13494
   163
    "!!h f g g'. REFLECTS[\<lambda>x. is_d(L, h(x), f(x), g(x)),
paulson@13807
   164
                     \<lambda>i x. is_d(##Lset(i), h(x), f(x), g(x))]"
paulson@13494
   165
  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)),
paulson@13807
   166
               \<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))]"
paulson@13655
   167
apply (simp (no_asm_use) only: is_formula_case_def)
paulson@13494
   168
apply (intro FOL_reflections function_reflections finite_ordinal_reflection
paulson@13494
   169
         mem_formula_reflection
paulson@13494
   170
         Member_reflection Equal_reflection Nand_reflection Forall_reflection
paulson@13494
   171
         is_a_reflection is_b_reflection is_c_reflection is_d_reflection)
paulson@13494
   172
done
paulson@13494
   173
paulson@13494
   174
paulson@13494
   175
paulson@13494
   176
subsection {*Absoluteness for the Function @{term satisfies}*}
paulson@13494
   177
wenzelm@21233
   178
definition
wenzelm@21404
   179
  is_depth_apply :: "[i=>o,i,i,i] => o" where
paulson@13494
   180
   --{*Merely a useful abbreviation for the sequel.*}
wenzelm@21404
   181
  "is_depth_apply(M,h,p,z) ==
paulson@13494
   182
    \<exists>dp[M]. \<exists>sdp[M]. \<exists>hsdp[M]. 
paulson@13496
   183
	finite_ordinal(M,dp) & is_depth(M,p,dp) & successor(M,dp,sdp) &
paulson@13494
   184
	fun_apply(M,h,sdp,hsdp) & fun_apply(M,hsdp,p,z)"
paulson@13494
   185
paulson@13494
   186
lemma (in M_datatypes) is_depth_apply_abs [simp]:
paulson@13494
   187
     "[|M(h); p \<in> formula; M(z)|] 
paulson@13494
   188
      ==> is_depth_apply(M,h,p,z) <-> z = h ` succ(depth(p)) ` p"
paulson@13494
   189
by (simp add: is_depth_apply_def formula_into_M depth_type eq_commute)
paulson@13494
   190
paulson@13494
   191
paulson@13494
   192
paulson@13494
   193
text{*There is at present some redundancy between the relativizations in
paulson@13494
   194
 e.g. @{text satisfies_is_a} and those in e.g. @{text Member_replacement}.*}
paulson@13494
   195
paulson@13494
   196
text{*These constants let us instantiate the parameters @{term a}, @{term b},
paulson@13504
   197
      @{term c}, @{term d}, etc., of the locale @{text Formula_Rec}.*}
wenzelm@21233
   198
definition
wenzelm@21404
   199
  satisfies_a :: "[i,i,i]=>i" where
paulson@13494
   200
   "satisfies_a(A) == 
paulson@13494
   201
    \<lambda>x y. \<lambda>env \<in> list(A). bool_of_o (nth(x,env) \<in> nth(y,env))"
paulson@13494
   202
wenzelm@21404
   203
definition
wenzelm@21404
   204
  satisfies_is_a :: "[i=>o,i,i,i,i]=>o" where
paulson@13494
   205
   "satisfies_is_a(M,A) == 
paulson@13496
   206
    \<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) -->
paulson@13496
   207
             is_lambda(M, lA, 
paulson@13496
   208
		\<lambda>env z. is_bool_of_o(M, 
paulson@13496
   209
                      \<exists>nx[M]. \<exists>ny[M]. 
paulson@13496
   210
 		       is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & nx \<in> ny, z),
paulson@13496
   211
                zz)"
paulson@13494
   212
wenzelm@21404
   213
definition
wenzelm@21404
   214
  satisfies_b :: "[i,i,i]=>i" where
paulson@13494
   215
   "satisfies_b(A) ==
paulson@13494
   216
    \<lambda>x y. \<lambda>env \<in> list(A). bool_of_o (nth(x,env) = nth(y,env))"
paulson@13494
   217
wenzelm@21404
   218
definition
wenzelm@21404
   219
  satisfies_is_b :: "[i=>o,i,i,i,i]=>o" where
paulson@13494
   220
   --{*We simplify the formula to have just @{term nx} rather than 
paulson@13494
   221
       introducing @{term ny} with  @{term "nx=ny"} *}
wenzelm@21404
   222
  "satisfies_is_b(M,A) == 
paulson@13496
   223
    \<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) -->
paulson@13496
   224
             is_lambda(M, lA, 
paulson@13496
   225
                \<lambda>env z. is_bool_of_o(M, 
paulson@13496
   226
                      \<exists>nx[M]. is_nth(M,x,env,nx) & is_nth(M,y,env,nx), z),
paulson@13496
   227
                zz)"
wenzelm@21404
   228
wenzelm@21404
   229
definition 
wenzelm@21404
   230
  satisfies_c :: "[i,i,i,i,i]=>i" where
paulson@13502
   231
   "satisfies_c(A) == \<lambda>p q rp rq. \<lambda>env \<in> list(A). not(rp ` env and rq ` env)"
paulson@13494
   232
wenzelm@21404
   233
definition
wenzelm@21404
   234
  satisfies_is_c :: "[i=>o,i,i,i,i,i]=>o" where
paulson@13494
   235
   "satisfies_is_c(M,A,h) == 
paulson@13496
   236
    \<lambda>p q zz. \<forall>lA[M]. is_list(M,A,lA) -->
paulson@13496
   237
             is_lambda(M, lA, \<lambda>env z. \<exists>hp[M]. \<exists>hq[M]. 
paulson@13494
   238
		 (\<exists>rp[M]. is_depth_apply(M,h,p,rp) & fun_apply(M,rp,env,hp)) & 
paulson@13494
   239
		 (\<exists>rq[M]. is_depth_apply(M,h,q,rq) & fun_apply(M,rq,env,hq)) & 
paulson@13496
   240
                 (\<exists>pq[M]. is_and(M,hp,hq,pq) & is_not(M,pq,z)),
paulson@13496
   241
                zz)"
paulson@13494
   242
wenzelm@21404
   243
definition
wenzelm@21404
   244
  satisfies_d :: "[i,i,i]=>i" where
paulson@13494
   245
   "satisfies_d(A) 
paulson@13494
   246
    == \<lambda>p rp. \<lambda>env \<in> list(A). bool_of_o (\<forall>x\<in>A. rp ` (Cons(x,env)) = 1)"
paulson@13494
   247
wenzelm@21404
   248
definition
wenzelm@21404
   249
  satisfies_is_d :: "[i=>o,i,i,i,i]=>o" where
paulson@13494
   250
   "satisfies_is_d(M,A,h) == 
paulson@13496
   251
    \<lambda>p zz. \<forall>lA[M]. is_list(M,A,lA) -->
paulson@13496
   252
             is_lambda(M, lA, 
paulson@13496
   253
                \<lambda>env z. \<exists>rp[M]. is_depth_apply(M,h,p,rp) & 
paulson@13496
   254
                    is_bool_of_o(M, 
paulson@13496
   255
                           \<forall>x[M]. \<forall>xenv[M]. \<forall>hp[M]. 
paulson@13496
   256
                              x\<in>A --> is_Cons(M,x,env,xenv) --> 
paulson@13496
   257
                              fun_apply(M,rp,xenv,hp) --> number1(M,hp),
paulson@13496
   258
                  z),
paulson@13496
   259
               zz)"
paulson@13494
   260
wenzelm@21404
   261
definition
wenzelm@21404
   262
  satisfies_MH :: "[i=>o,i,i,i,i]=>o" where
paulson@13496
   263
    --{*The variable @{term u} is unused, but gives @{term satisfies_MH} 
paulson@13496
   264
        the correct arity.*}
wenzelm@21404
   265
  "satisfies_MH == 
paulson@13502
   266
    \<lambda>M A u f z. 
paulson@13496
   267
         \<forall>fml[M]. is_formula(M,fml) -->
paulson@13496
   268
             is_lambda (M, fml, 
paulson@13496
   269
               is_formula_case (M, satisfies_is_a(M,A), 
paulson@13496
   270
                                satisfies_is_b(M,A), 
paulson@13496
   271
                                satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)),
paulson@13502
   272
               z)"
paulson@13494
   273
wenzelm@21404
   274
definition
wenzelm@21404
   275
  is_satisfies :: "[i=>o,i,i,i]=>o" where
wenzelm@21404
   276
  "is_satisfies(M,A) == is_formula_rec (M, satisfies_MH(M,A))"
paulson@13502
   277
paulson@13502
   278
paulson@13502
   279
text{*This lemma relates the fragments defined above to the original primitive
paulson@13502
   280
      recursion in @{term satisfies}.
paulson@13502
   281
      Induction is not required: the definitions are directly equal!*}
paulson@13502
   282
lemma satisfies_eq:
paulson@13502
   283
  "satisfies(A,p) = 
paulson@13502
   284
   formula_rec (satisfies_a(A), satisfies_b(A), 
paulson@13502
   285
                satisfies_c(A), satisfies_d(A), p)"
paulson@13502
   286
by (simp add: satisfies_formula_def satisfies_a_def satisfies_b_def 
paulson@13502
   287
              satisfies_c_def satisfies_d_def) 
paulson@13494
   288
paulson@13494
   289
text{*Further constraints on the class @{term M} in order to prove
paulson@13494
   290
      absoluteness for the constants defined above.  The ultimate goal
paulson@13494
   291
      is the absoluteness of the function @{term satisfies}. *}
paulson@13502
   292
locale M_satisfies = M_eclose +
paulson@13494
   293
 assumes 
paulson@13494
   294
   Member_replacement:
paulson@13494
   295
    "[|M(A); x \<in> nat; y \<in> nat|]
paulson@13494
   296
     ==> strong_replacement
paulson@13494
   297
	 (M, \<lambda>env z. \<exists>bo[M]. \<exists>nx[M]. \<exists>ny[M]. 
paulson@13494
   298
              env \<in> list(A) & is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & 
paulson@13494
   299
              is_bool_of_o(M, nx \<in> ny, bo) &
paulson@13494
   300
              pair(M, env, bo, z))"
paulson@13494
   301
 and
paulson@13494
   302
   Equal_replacement:
paulson@13494
   303
    "[|M(A); x \<in> nat; y \<in> nat|]
paulson@13494
   304
     ==> strong_replacement
paulson@13494
   305
	 (M, \<lambda>env z. \<exists>bo[M]. \<exists>nx[M]. \<exists>ny[M]. 
paulson@13494
   306
              env \<in> list(A) & is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & 
paulson@13494
   307
              is_bool_of_o(M, nx = ny, bo) &
paulson@13494
   308
              pair(M, env, bo, z))"
paulson@13494
   309
 and
paulson@13494
   310
   Nand_replacement:
paulson@13494
   311
    "[|M(A); M(rp); M(rq)|]
paulson@13494
   312
     ==> strong_replacement
paulson@13494
   313
	 (M, \<lambda>env z. \<exists>rpe[M]. \<exists>rqe[M]. \<exists>andpq[M]. \<exists>notpq[M]. 
paulson@13494
   314
               fun_apply(M,rp,env,rpe) & fun_apply(M,rq,env,rqe) & 
paulson@13494
   315
               is_and(M,rpe,rqe,andpq) & is_not(M,andpq,notpq) & 
paulson@13494
   316
               env \<in> list(A) & pair(M, env, notpq, z))"
paulson@13494
   317
 and
paulson@13494
   318
  Forall_replacement:
paulson@13494
   319
   "[|M(A); M(rp)|]
paulson@13494
   320
    ==> strong_replacement
paulson@13494
   321
	(M, \<lambda>env z. \<exists>bo[M]. 
paulson@13494
   322
	      env \<in> list(A) & 
paulson@13494
   323
	      is_bool_of_o (M, 
paulson@13494
   324
			    \<forall>a[M]. \<forall>co[M]. \<forall>rpco[M]. 
paulson@13494
   325
			       a\<in>A --> is_Cons(M,a,env,co) -->
paulson@13494
   326
			       fun_apply(M,rp,co,rpco) --> number1(M, rpco), 
paulson@13494
   327
                            bo) &
paulson@13494
   328
	      pair(M,env,bo,z))"
paulson@13494
   329
 and
paulson@13494
   330
  formula_rec_replacement: 
paulson@13494
   331
      --{*For the @{term transrec}*}
paulson@13494
   332
   "[|n \<in> nat; M(A)|] ==> transrec_replacement(M, satisfies_MH(M,A), n)"
paulson@13494
   333
 and
paulson@13494
   334
  formula_rec_lambda_replacement:  
paulson@13494
   335
      --{*For the @{text "\<lambda>-abstraction"} in the @{term transrec} body*}
paulson@13502
   336
   "[|M(g); M(A)|] ==>
paulson@13502
   337
    strong_replacement (M, 
paulson@13502
   338
       \<lambda>x y. mem_formula(M,x) &
paulson@13502
   339
             (\<exists>c[M]. is_formula_case(M, satisfies_is_a(M,A),
paulson@13502
   340
                                  satisfies_is_b(M,A),
paulson@13502
   341
                                  satisfies_is_c(M,A,g),
paulson@13502
   342
                                  satisfies_is_d(M,A,g), x, c) &
paulson@13502
   343
             pair(M, x, c, y)))"
paulson@13494
   344
paulson@13494
   345
paulson@13494
   346
lemma (in M_satisfies) Member_replacement':
paulson@13494
   347
    "[|M(A); x \<in> nat; y \<in> nat|]
paulson@13494
   348
     ==> strong_replacement
paulson@13494
   349
	 (M, \<lambda>env z. env \<in> list(A) &
paulson@13494
   350
		     z = \<langle>env, bool_of_o(nth(x, env) \<in> nth(y, env))\<rangle>)"
paulson@13494
   351
by (insert Member_replacement, simp) 
paulson@13494
   352
paulson@13494
   353
lemma (in M_satisfies) Equal_replacement':
paulson@13494
   354
    "[|M(A); x \<in> nat; y \<in> nat|]
paulson@13494
   355
     ==> strong_replacement
paulson@13494
   356
	 (M, \<lambda>env z. env \<in> list(A) &
paulson@13494
   357
		     z = \<langle>env, bool_of_o(nth(x, env) = nth(y, env))\<rangle>)"
paulson@13494
   358
by (insert Equal_replacement, simp) 
paulson@13494
   359
paulson@13494
   360
lemma (in M_satisfies) Nand_replacement':
paulson@13494
   361
    "[|M(A); M(rp); M(rq)|]
paulson@13494
   362
     ==> strong_replacement
paulson@13494
   363
	 (M, \<lambda>env z. env \<in> list(A) & z = \<langle>env, not(rp`env and rq`env)\<rangle>)"
paulson@13494
   364
by (insert Nand_replacement, simp) 
paulson@13494
   365
paulson@13494
   366
lemma (in M_satisfies) Forall_replacement':
paulson@13494
   367
   "[|M(A); M(rp)|]
paulson@13494
   368
    ==> strong_replacement
paulson@13494
   369
	(M, \<lambda>env z.
paulson@13494
   370
	       env \<in> list(A) &
paulson@13494
   371
	       z = \<langle>env, bool_of_o (\<forall>a\<in>A. rp ` Cons(a,env) = 1)\<rangle>)"
paulson@13494
   372
by (insert Forall_replacement, simp) 
paulson@13494
   373
paulson@13494
   374
lemma (in M_satisfies) a_closed:
paulson@13494
   375
     "[|M(A); x\<in>nat; y\<in>nat|] ==> M(satisfies_a(A,x,y))"
paulson@13494
   376
apply (simp add: satisfies_a_def) 
paulson@13494
   377
apply (blast intro: lam_closed2 Member_replacement') 
paulson@13494
   378
done
paulson@13494
   379
paulson@13494
   380
lemma (in M_satisfies) a_rel:
paulson@13634
   381
     "M(A) ==> Relation2(M, nat, nat, satisfies_is_a(M,A), satisfies_a(A))"
paulson@13634
   382
apply (simp add: Relation2_def satisfies_is_a_def satisfies_a_def)
paulson@13702
   383
apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def) 
paulson@13494
   384
done
paulson@13494
   385
paulson@13494
   386
lemma (in M_satisfies) b_closed:
paulson@13494
   387
     "[|M(A); x\<in>nat; y\<in>nat|] ==> M(satisfies_b(A,x,y))"
paulson@13494
   388
apply (simp add: satisfies_b_def) 
paulson@13494
   389
apply (blast intro: lam_closed2 Equal_replacement') 
paulson@13494
   390
done
paulson@13494
   391
paulson@13494
   392
lemma (in M_satisfies) b_rel:
paulson@13634
   393
     "M(A) ==> Relation2(M, nat, nat, satisfies_is_b(M,A), satisfies_b(A))"
paulson@13634
   394
apply (simp add: Relation2_def satisfies_is_b_def satisfies_b_def)
paulson@13702
   395
apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def) 
paulson@13494
   396
done
paulson@13494
   397
paulson@13494
   398
lemma (in M_satisfies) c_closed:
paulson@13494
   399
     "[|M(A); x \<in> formula; y \<in> formula; M(rx); M(ry)|] 
paulson@13494
   400
      ==> M(satisfies_c(A,x,y,rx,ry))"
paulson@13494
   401
apply (simp add: satisfies_c_def) 
paulson@13494
   402
apply (rule lam_closed2) 
paulson@13494
   403
apply (rule Nand_replacement') 
paulson@13494
   404
apply (simp_all add: formula_into_M list_into_M [of _ A])
paulson@13494
   405
done
paulson@13494
   406
paulson@13494
   407
lemma (in M_satisfies) c_rel:
paulson@13494
   408
 "[|M(A); M(f)|] ==> 
paulson@13634
   409
  Relation2 (M, formula, formula, 
paulson@13494
   410
               satisfies_is_c(M,A,f),
paulson@13494
   411
	       \<lambda>u v. satisfies_c(A, u, v, f ` succ(depth(u)) ` u, 
paulson@13494
   412
					  f ` succ(depth(v)) ` v))"
paulson@13634
   413
apply (simp add: Relation2_def satisfies_is_c_def satisfies_c_def)
paulson@13702
   414
apply (auto del: iffI intro!: lambda_abs2 
paulson@13702
   415
            simp add: Relation1_def formula_into_M) 
paulson@13494
   416
done
paulson@13494
   417
paulson@13494
   418
lemma (in M_satisfies) d_closed:
paulson@13494
   419
     "[|M(A); x \<in> formula; M(rx)|] ==> M(satisfies_d(A,x,rx))"
paulson@13494
   420
apply (simp add: satisfies_d_def) 
paulson@13494
   421
apply (rule lam_closed2) 
paulson@13494
   422
apply (rule Forall_replacement') 
paulson@13494
   423
apply (simp_all add: formula_into_M list_into_M [of _ A])
paulson@13494
   424
done
paulson@13494
   425
paulson@13494
   426
lemma (in M_satisfies) d_rel:
paulson@13494
   427
 "[|M(A); M(f)|] ==> 
paulson@13634
   428
  Relation1(M, formula, satisfies_is_d(M,A,f), 
paulson@13494
   429
     \<lambda>u. satisfies_d(A, u, f ` succ(depth(u)) ` u))"
paulson@13494
   430
apply (simp del: rall_abs 
paulson@13634
   431
            add: Relation1_def satisfies_is_d_def satisfies_d_def)
paulson@13702
   432
apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def) 
paulson@13494
   433
done
paulson@13494
   434
paulson@13494
   435
paulson@13494
   436
lemma (in M_satisfies) fr_replace:
paulson@13494
   437
      "[|n \<in> nat; M(A)|] ==> transrec_replacement(M,satisfies_MH(M,A),n)" 
paulson@13494
   438
by (blast intro: formula_rec_replacement) 
paulson@13494
   439
paulson@13502
   440
lemma (in M_satisfies) formula_case_satisfies_closed:
paulson@13502
   441
 "[|M(g); M(A); x \<in> formula|] ==>
paulson@13502
   442
  M(formula_case (satisfies_a(A), satisfies_b(A),
paulson@13502
   443
       \<lambda>u v. satisfies_c(A, u, v, 
paulson@13502
   444
                         g ` succ(depth(u)) ` u, g ` succ(depth(v)) ` v),
paulson@13502
   445
       \<lambda>u. satisfies_d (A, u, g ` succ(depth(u)) ` u),
paulson@13502
   446
       x))"
paulson@13502
   447
by (blast intro: formula_case_closed a_closed b_closed c_closed d_closed) 
paulson@13502
   448
paulson@13494
   449
lemma (in M_satisfies) fr_lam_replace:
paulson@13502
   450
   "[|M(g); M(A)|] ==>
paulson@13494
   451
    strong_replacement (M, \<lambda>x y. x \<in> formula &
paulson@13494
   452
            y = \<langle>x, 
paulson@13494
   453
                 formula_rec_case(satisfies_a(A),
paulson@13494
   454
                                  satisfies_b(A),
paulson@13494
   455
                                  satisfies_c(A),
paulson@13494
   456
                                  satisfies_d(A), g, x)\<rangle>)"
paulson@13502
   457
apply (insert formula_rec_lambda_replacement) 
paulson@13502
   458
apply (simp add: formula_rec_case_def formula_case_satisfies_closed
paulson@13502
   459
                 formula_case_abs [OF a_rel b_rel c_rel d_rel]) 
paulson@13502
   460
done
paulson@13494
   461
paulson@13494
   462
paulson@13494
   463
paulson@13504
   464
text{*Instantiate locale @{text Formula_Rec} for the 
paulson@13502
   465
      Function @{term satisfies}*}
paulson@13494
   466
paulson@13504
   467
lemma (in M_satisfies) Formula_Rec_axioms_M:
paulson@13502
   468
   "M(A) ==>
paulson@13504
   469
    Formula_Rec_axioms(M, satisfies_a(A), satisfies_is_a(M,A), 
paulson@13504
   470
			  satisfies_b(A), satisfies_is_b(M,A), 
paulson@13504
   471
			  satisfies_c(A), satisfies_is_c(M,A), 
paulson@13504
   472
			  satisfies_d(A), satisfies_is_d(M,A))"
paulson@13504
   473
apply (rule Formula_Rec_axioms.intro)
paulson@13502
   474
apply (assumption | 
paulson@13502
   475
       rule a_closed a_rel b_closed b_rel c_closed c_rel d_closed d_rel
paulson@13502
   476
       fr_replace [unfolded satisfies_MH_def]
paulson@13502
   477
       fr_lam_replace) +
paulson@13494
   478
done
paulson@13494
   479
paulson@13494
   480
paulson@13504
   481
theorem (in M_satisfies) Formula_Rec_M: 
paulson@13502
   482
    "M(A) ==>
paulson@13504
   483
     PROP Formula_Rec(M, satisfies_a(A), satisfies_is_a(M,A), 
paulson@13504
   484
			 satisfies_b(A), satisfies_is_b(M,A), 
paulson@13504
   485
			 satisfies_c(A), satisfies_is_c(M,A), 
paulson@13504
   486
			 satisfies_d(A), satisfies_is_d(M,A))"
ballarin@19931
   487
  apply (rule Formula_Rec.intro)
wenzelm@23464
   488
   apply (rule M_satisfies.axioms, rule M_satisfies_axioms)
ballarin@19931
   489
  apply (erule Formula_Rec_axioms_M) 
ballarin@19931
   490
  done
paulson@13494
   491
paulson@13502
   492
lemmas (in M_satisfies) 
wenzelm@13535
   493
    satisfies_closed' = Formula_Rec.formula_rec_closed [OF Formula_Rec_M]
wenzelm@13535
   494
and satisfies_abs'    = Formula_Rec.formula_rec_abs [OF Formula_Rec_M]
paulson@13494
   495
paulson@13494
   496
paulson@13502
   497
lemma (in M_satisfies) satisfies_closed:
paulson@13502
   498
  "[|M(A); p \<in> formula|] ==> M(satisfies(A,p))"
paulson@13504
   499
by (simp add: Formula_Rec.formula_rec_closed [OF Formula_Rec_M]  
paulson@13502
   500
              satisfies_eq) 
paulson@13494
   501
paulson@13502
   502
lemma (in M_satisfies) satisfies_abs:
paulson@13502
   503
  "[|M(A); M(z); p \<in> formula|] 
paulson@13502
   504
   ==> is_satisfies(M,A,p,z) <-> z = satisfies(A,p)"
paulson@13504
   505
by (simp only: Formula_Rec.formula_rec_abs [OF Formula_Rec_M]  
paulson@13503
   506
               satisfies_eq is_satisfies_def satisfies_MH_def)
paulson@13494
   507
paulson@13494
   508
paulson@13502
   509
subsection{*Internalizations Needed to Instantiate @{text "M_satisfies"}*}
paulson@13494
   510
paulson@13496
   511
subsubsection{*The Operator @{term is_depth_apply}, Internalized*}
paulson@13496
   512
paulson@13496
   513
(* is_depth_apply(M,h,p,z) ==
paulson@13496
   514
    \<exists>dp[M]. \<exists>sdp[M]. \<exists>hsdp[M]. 
paulson@13496
   515
      2        1         0
paulson@13496
   516
	finite_ordinal(M,dp) & is_depth(M,p,dp) & successor(M,dp,sdp) &
paulson@13496
   517
	fun_apply(M,h,sdp,hsdp) & fun_apply(M,hsdp,p,z) *)
wenzelm@21404
   518
definition
wenzelm@21404
   519
  depth_apply_fm :: "[i,i,i]=>i" where
paulson@13496
   520
    "depth_apply_fm(h,p,z) ==
paulson@13496
   521
       Exists(Exists(Exists(
paulson@13496
   522
        And(finite_ordinal_fm(2),
paulson@13496
   523
         And(depth_fm(p#+3,2),
paulson@13496
   524
          And(succ_fm(2,1),
paulson@13496
   525
           And(fun_apply_fm(h#+3,1,0), fun_apply_fm(0,p#+3,z#+3))))))))"
paulson@13496
   526
paulson@13496
   527
lemma depth_apply_type [TC]:
paulson@13496
   528
     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> depth_apply_fm(x,y,z) \<in> formula"
paulson@13496
   529
by (simp add: depth_apply_fm_def)
paulson@13496
   530
paulson@13496
   531
lemma sats_depth_apply_fm [simp]:
paulson@13496
   532
   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
paulson@13496
   533
    ==> sats(A, depth_apply_fm(x,y,z), env) <->
paulson@13807
   534
        is_depth_apply(##A, nth(x,env), nth(y,env), nth(z,env))"
paulson@13496
   535
by (simp add: depth_apply_fm_def is_depth_apply_def)
paulson@13496
   536
paulson@13496
   537
lemma depth_apply_iff_sats:
paulson@13496
   538
    "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
paulson@13496
   539
        i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
paulson@13807
   540
     ==> is_depth_apply(##A, x, y, z) <-> sats(A, depth_apply_fm(i,j,k), env)"
paulson@13496
   541
by simp
paulson@13496
   542
paulson@13496
   543
lemma depth_apply_reflection:
paulson@13496
   544
     "REFLECTS[\<lambda>x. is_depth_apply(L,f(x),g(x),h(x)),
paulson@13807
   545
               \<lambda>i x. is_depth_apply(##Lset(i),f(x),g(x),h(x))]"
paulson@13655
   546
apply (simp only: is_depth_apply_def)
paulson@13496
   547
apply (intro FOL_reflections function_reflections depth_reflection 
paulson@13496
   548
             finite_ordinal_reflection)
paulson@13496
   549
done
paulson@13496
   550
paulson@13496
   551
paulson@13496
   552
subsubsection{*The Operator @{term satisfies_is_a}, Internalized*}
paulson@13496
   553
paulson@13496
   554
(* satisfies_is_a(M,A) == 
paulson@13496
   555
    \<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) -->
paulson@13496
   556
             is_lambda(M, lA, 
paulson@13496
   557
		\<lambda>env z. is_bool_of_o(M, 
paulson@13496
   558
                      \<exists>nx[M]. \<exists>ny[M]. 
paulson@13496
   559
 		       is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & nx \<in> ny, z),
paulson@13496
   560
                zz)  *)
paulson@13496
   561
wenzelm@21404
   562
definition
wenzelm@21404
   563
  satisfies_is_a_fm :: "[i,i,i,i]=>i" where
wenzelm@21404
   564
  "satisfies_is_a_fm(A,x,y,z) ==
paulson@13496
   565
   Forall(
paulson@13496
   566
     Implies(is_list_fm(succ(A),0),
paulson@13496
   567
       lambda_fm(
paulson@13496
   568
         bool_of_o_fm(Exists(
paulson@13496
   569
                       Exists(And(nth_fm(x#+6,3,1), 
paulson@13496
   570
                               And(nth_fm(y#+6,3,0), 
paulson@13496
   571
                                   Member(1,0))))), 0), 
paulson@13496
   572
         0, succ(z))))"
paulson@13496
   573
paulson@13496
   574
lemma satisfies_is_a_type [TC]:
paulson@13496
   575
     "[| A \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
paulson@13496
   576
      ==> satisfies_is_a_fm(A,x,y,z) \<in> formula"
paulson@13496
   577
by (simp add: satisfies_is_a_fm_def)
paulson@13496
   578
paulson@13496
   579
lemma sats_satisfies_is_a_fm [simp]:
paulson@13496
   580
   "[| u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
paulson@13496
   581
    ==> sats(A, satisfies_is_a_fm(u,x,y,z), env) <->
paulson@13807
   582
        satisfies_is_a(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
paulson@13496
   583
apply (frule_tac x=x in lt_length_in_nat, assumption)  
paulson@13496
   584
apply (frule_tac x=y in lt_length_in_nat, assumption)  
paulson@13496
   585
apply (simp add: satisfies_is_a_fm_def satisfies_is_a_def sats_lambda_fm 
paulson@13496
   586
                 sats_bool_of_o_fm)
paulson@13496
   587
done
paulson@13496
   588
paulson@13496
   589
lemma satisfies_is_a_iff_sats:
paulson@13496
   590
  "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
paulson@13496
   591
      u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
paulson@13807
   592
   ==> satisfies_is_a(##A,nu,nx,ny,nz) <->
paulson@13496
   593
       sats(A, satisfies_is_a_fm(u,x,y,z), env)"
paulson@13496
   594
by simp
paulson@13496
   595
paulson@13494
   596
theorem satisfies_is_a_reflection:
paulson@13494
   597
     "REFLECTS[\<lambda>x. satisfies_is_a(L,f(x),g(x),h(x),g'(x)),
paulson@13807
   598
               \<lambda>i x. satisfies_is_a(##Lset(i),f(x),g(x),h(x),g'(x))]"
paulson@13494
   599
apply (unfold satisfies_is_a_def) 
paulson@13494
   600
apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection 
paulson@13496
   601
             nth_reflection is_list_reflection)
paulson@13494
   602
done
paulson@13494
   603
paulson@13494
   604
paulson@13496
   605
subsubsection{*The Operator @{term satisfies_is_b}, Internalized*}
paulson@13496
   606
paulson@13496
   607
(* satisfies_is_b(M,A) == 
paulson@13496
   608
    \<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) -->
paulson@13496
   609
             is_lambda(M, lA, 
paulson@13496
   610
                \<lambda>env z. is_bool_of_o(M, 
paulson@13496
   611
                      \<exists>nx[M]. is_nth(M,x,env,nx) & is_nth(M,y,env,nx), z),
paulson@13496
   612
                zz) *)
paulson@13496
   613
wenzelm@21404
   614
definition
wenzelm@21404
   615
  satisfies_is_b_fm :: "[i,i,i,i]=>i" where
paulson@13496
   616
 "satisfies_is_b_fm(A,x,y,z) ==
paulson@13496
   617
   Forall(
paulson@13496
   618
     Implies(is_list_fm(succ(A),0),
paulson@13496
   619
       lambda_fm(
paulson@13496
   620
         bool_of_o_fm(Exists(And(nth_fm(x#+5,2,0), nth_fm(y#+5,2,0))), 0), 
paulson@13496
   621
         0, succ(z))))"
paulson@13496
   622
paulson@13496
   623
lemma satisfies_is_b_type [TC]:
paulson@13496
   624
     "[| A \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
paulson@13496
   625
      ==> satisfies_is_b_fm(A,x,y,z) \<in> formula"
paulson@13496
   626
by (simp add: satisfies_is_b_fm_def)
paulson@13496
   627
paulson@13496
   628
lemma sats_satisfies_is_b_fm [simp]:
paulson@13496
   629
   "[| u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
paulson@13496
   630
    ==> sats(A, satisfies_is_b_fm(u,x,y,z), env) <->
paulson@13807
   631
        satisfies_is_b(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
paulson@13496
   632
apply (frule_tac x=x in lt_length_in_nat, assumption)  
paulson@13496
   633
apply (frule_tac x=y in lt_length_in_nat, assumption)  
paulson@13496
   634
apply (simp add: satisfies_is_b_fm_def satisfies_is_b_def sats_lambda_fm 
paulson@13496
   635
                 sats_bool_of_o_fm)
paulson@13496
   636
done
paulson@13496
   637
paulson@13496
   638
lemma satisfies_is_b_iff_sats:
paulson@13496
   639
  "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
paulson@13496
   640
      u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
paulson@13807
   641
   ==> satisfies_is_b(##A,nu,nx,ny,nz) <->
paulson@13496
   642
       sats(A, satisfies_is_b_fm(u,x,y,z), env)"
paulson@13496
   643
by simp
paulson@13496
   644
paulson@13494
   645
theorem satisfies_is_b_reflection:
paulson@13494
   646
     "REFLECTS[\<lambda>x. satisfies_is_b(L,f(x),g(x),h(x),g'(x)),
paulson@13807
   647
               \<lambda>i x. satisfies_is_b(##Lset(i),f(x),g(x),h(x),g'(x))]"
paulson@13494
   648
apply (unfold satisfies_is_b_def) 
paulson@13494
   649
apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection 
paulson@13496
   650
             nth_reflection is_list_reflection)
paulson@13494
   651
done
paulson@13494
   652
paulson@13496
   653
paulson@13496
   654
subsubsection{*The Operator @{term satisfies_is_c}, Internalized*}
paulson@13496
   655
paulson@13496
   656
(* satisfies_is_c(M,A,h) == 
paulson@13496
   657
    \<lambda>p q zz. \<forall>lA[M]. is_list(M,A,lA) -->
paulson@13496
   658
             is_lambda(M, lA, \<lambda>env z. \<exists>hp[M]. \<exists>hq[M]. 
paulson@13496
   659
		 (\<exists>rp[M]. is_depth_apply(M,h,p,rp) & fun_apply(M,rp,env,hp)) & 
paulson@13496
   660
		 (\<exists>rq[M]. is_depth_apply(M,h,q,rq) & fun_apply(M,rq,env,hq)) & 
paulson@13496
   661
                 (\<exists>pq[M]. is_and(M,hp,hq,pq) & is_not(M,pq,z)),
paulson@13496
   662
                zz) *)
paulson@13496
   663
wenzelm@21404
   664
definition
wenzelm@21404
   665
  satisfies_is_c_fm :: "[i,i,i,i,i]=>i" where
paulson@13496
   666
 "satisfies_is_c_fm(A,h,p,q,zz) ==
paulson@13496
   667
   Forall(
paulson@13496
   668
     Implies(is_list_fm(succ(A),0),
paulson@13496
   669
       lambda_fm(
paulson@13496
   670
         Exists(Exists(
paulson@13496
   671
          And(Exists(And(depth_apply_fm(h#+7,p#+7,0), fun_apply_fm(0,4,2))),
paulson@13496
   672
          And(Exists(And(depth_apply_fm(h#+7,q#+7,0), fun_apply_fm(0,4,1))),
paulson@13496
   673
              Exists(And(and_fm(2,1,0), not_fm(0,3))))))),
paulson@13496
   674
         0, succ(zz))))"
paulson@13496
   675
paulson@13496
   676
lemma satisfies_is_c_type [TC]:
paulson@13496
   677
     "[| A \<in> nat; h \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
paulson@13496
   678
      ==> satisfies_is_c_fm(A,h,x,y,z) \<in> formula"
paulson@13496
   679
by (simp add: satisfies_is_c_fm_def)
paulson@13496
   680
paulson@13496
   681
lemma sats_satisfies_is_c_fm [simp]:
paulson@13496
   682
   "[| u \<in> nat; v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
paulson@13496
   683
    ==> sats(A, satisfies_is_c_fm(u,v,x,y,z), env) <->
paulson@13807
   684
        satisfies_is_c(##A, nth(u,env), nth(v,env), nth(x,env), 
paulson@13496
   685
                            nth(y,env), nth(z,env))"  
paulson@13496
   686
by (simp add: satisfies_is_c_fm_def satisfies_is_c_def sats_lambda_fm)
paulson@13496
   687
paulson@13496
   688
lemma satisfies_is_c_iff_sats:
paulson@13496
   689
  "[| nth(u,env) = nu; nth(v,env) = nv; nth(x,env) = nx; nth(y,env) = ny; 
paulson@13496
   690
      nth(z,env) = nz;
paulson@13496
   691
      u \<in> nat; v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
paulson@13807
   692
   ==> satisfies_is_c(##A,nu,nv,nx,ny,nz) <->
paulson@13496
   693
       sats(A, satisfies_is_c_fm(u,v,x,y,z), env)"
paulson@13496
   694
by simp
paulson@13496
   695
paulson@13494
   696
theorem satisfies_is_c_reflection:
paulson@13494
   697
     "REFLECTS[\<lambda>x. satisfies_is_c(L,f(x),g(x),h(x),g'(x),h'(x)),
paulson@13807
   698
               \<lambda>i x. satisfies_is_c(##Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
paulson@13496
   699
apply (unfold satisfies_is_c_def) 
paulson@13494
   700
apply (intro FOL_reflections function_reflections is_lambda_reflection
paulson@13496
   701
             extra_reflections nth_reflection depth_apply_reflection 
paulson@13496
   702
             is_list_reflection)
paulson@13494
   703
done
paulson@13494
   704
paulson@13496
   705
subsubsection{*The Operator @{term satisfies_is_d}, Internalized*}
paulson@13496
   706
paulson@13496
   707
(* satisfies_is_d(M,A,h) == 
paulson@13496
   708
    \<lambda>p zz. \<forall>lA[M]. is_list(M,A,lA) -->
paulson@13496
   709
             is_lambda(M, lA, 
paulson@13496
   710
                \<lambda>env z. \<exists>rp[M]. is_depth_apply(M,h,p,rp) & 
paulson@13496
   711
                    is_bool_of_o(M, 
paulson@13496
   712
                           \<forall>x[M]. \<forall>xenv[M]. \<forall>hp[M]. 
paulson@13496
   713
                              x\<in>A --> is_Cons(M,x,env,xenv) --> 
paulson@13496
   714
                              fun_apply(M,rp,xenv,hp) --> number1(M,hp),
paulson@13496
   715
                  z),
paulson@13496
   716
               zz) *)
paulson@13496
   717
wenzelm@21404
   718
definition
wenzelm@21404
   719
  satisfies_is_d_fm :: "[i,i,i,i]=>i" where
paulson@13496
   720
 "satisfies_is_d_fm(A,h,p,zz) ==
paulson@13496
   721
   Forall(
paulson@13496
   722
     Implies(is_list_fm(succ(A),0),
paulson@13496
   723
       lambda_fm(
paulson@13496
   724
         Exists(
paulson@13496
   725
           And(depth_apply_fm(h#+5,p#+5,0),
paulson@13496
   726
               bool_of_o_fm(
paulson@13496
   727
                Forall(Forall(Forall(
paulson@13496
   728
                 Implies(Member(2,A#+8),
paulson@13496
   729
                  Implies(Cons_fm(2,5,1),
paulson@13496
   730
                   Implies(fun_apply_fm(3,1,0), number1_fm(0))))))), 1))),
paulson@13496
   731
         0, succ(zz))))"
paulson@13496
   732
paulson@13496
   733
lemma satisfies_is_d_type [TC]:
paulson@13496
   734
     "[| A \<in> nat; h \<in> nat; x \<in> nat; z \<in> nat |]
paulson@13496
   735
      ==> satisfies_is_d_fm(A,h,x,z) \<in> formula"
paulson@13496
   736
by (simp add: satisfies_is_d_fm_def)
paulson@13496
   737
paulson@13496
   738
lemma sats_satisfies_is_d_fm [simp]:
paulson@13496
   739
   "[| u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
paulson@13496
   740
    ==> sats(A, satisfies_is_d_fm(u,x,y,z), env) <->
paulson@13807
   741
        satisfies_is_d(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"  
paulson@13496
   742
by (simp add: satisfies_is_d_fm_def satisfies_is_d_def sats_lambda_fm
paulson@13496
   743
              sats_bool_of_o_fm)
paulson@13496
   744
paulson@13496
   745
lemma satisfies_is_d_iff_sats:
paulson@13496
   746
  "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
paulson@13496
   747
      u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
paulson@13807
   748
   ==> satisfies_is_d(##A,nu,nx,ny,nz) <->
paulson@13496
   749
       sats(A, satisfies_is_d_fm(u,x,y,z), env)"
paulson@13496
   750
by simp
paulson@13496
   751
paulson@13494
   752
theorem satisfies_is_d_reflection:
paulson@13494
   753
     "REFLECTS[\<lambda>x. satisfies_is_d(L,f(x),g(x),h(x),g'(x)),
paulson@13807
   754
               \<lambda>i x. satisfies_is_d(##Lset(i),f(x),g(x),h(x),g'(x))]"
paulson@13505
   755
apply (unfold satisfies_is_d_def) 
paulson@13494
   756
apply (intro FOL_reflections function_reflections is_lambda_reflection
paulson@13496
   757
             extra_reflections nth_reflection depth_apply_reflection 
paulson@13496
   758
             is_list_reflection)
paulson@13496
   759
done
paulson@13496
   760
paulson@13496
   761
paulson@13496
   762
subsubsection{*The Operator @{term satisfies_MH}, Internalized*}
paulson@13496
   763
paulson@13496
   764
(* satisfies_MH == 
paulson@13496
   765
    \<lambda>M A u f zz. 
paulson@13496
   766
         \<forall>fml[M]. is_formula(M,fml) -->
paulson@13496
   767
             is_lambda (M, fml, 
paulson@13496
   768
               is_formula_case (M, satisfies_is_a(M,A), 
paulson@13496
   769
                                satisfies_is_b(M,A), 
paulson@13496
   770
                                satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)),
paulson@13496
   771
               zz) *)
paulson@13496
   772
wenzelm@21404
   773
definition
wenzelm@21404
   774
  satisfies_MH_fm :: "[i,i,i,i]=>i" where
paulson@13496
   775
 "satisfies_MH_fm(A,u,f,zz) ==
paulson@13496
   776
   Forall(
paulson@13496
   777
     Implies(is_formula_fm(0),
paulson@13496
   778
       lambda_fm(
paulson@13496
   779
         formula_case_fm(satisfies_is_a_fm(A#+7,2,1,0), 
paulson@13496
   780
                         satisfies_is_b_fm(A#+7,2,1,0), 
paulson@13496
   781
                         satisfies_is_c_fm(A#+7,f#+7,2,1,0), 
paulson@13496
   782
                         satisfies_is_d_fm(A#+6,f#+6,1,0), 
paulson@13496
   783
                         1, 0),
paulson@13496
   784
         0, succ(zz))))"
paulson@13496
   785
paulson@13496
   786
lemma satisfies_MH_type [TC]:
paulson@13496
   787
     "[| A \<in> nat; u \<in> nat; x \<in> nat; z \<in> nat |]
paulson@13496
   788
      ==> satisfies_MH_fm(A,u,x,z) \<in> formula"
paulson@13496
   789
by (simp add: satisfies_MH_fm_def)
paulson@13496
   790
paulson@13496
   791
lemma sats_satisfies_MH_fm [simp]:
paulson@13496
   792
   "[| u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
paulson@13496
   793
    ==> sats(A, satisfies_MH_fm(u,x,y,z), env) <->
paulson@13807
   794
        satisfies_MH(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"  
paulson@13496
   795
by (simp add: satisfies_MH_fm_def satisfies_MH_def sats_lambda_fm
paulson@13496
   796
              sats_formula_case_fm)
paulson@13496
   797
paulson@13496
   798
lemma satisfies_MH_iff_sats:
paulson@13496
   799
  "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
paulson@13496
   800
      u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
paulson@13807
   801
   ==> satisfies_MH(##A,nu,nx,ny,nz) <->
paulson@13496
   802
       sats(A, satisfies_MH_fm(u,x,y,z), env)"
paulson@13496
   803
by simp 
paulson@13496
   804
paulson@13496
   805
lemmas satisfies_reflections =
paulson@13496
   806
       is_lambda_reflection is_formula_reflection 
paulson@13496
   807
       is_formula_case_reflection
paulson@13496
   808
       satisfies_is_a_reflection satisfies_is_b_reflection 
paulson@13496
   809
       satisfies_is_c_reflection satisfies_is_d_reflection
paulson@13496
   810
paulson@13496
   811
theorem satisfies_MH_reflection:
paulson@13496
   812
     "REFLECTS[\<lambda>x. satisfies_MH(L,f(x),g(x),h(x),g'(x)),
paulson@13807
   813
               \<lambda>i x. satisfies_MH(##Lset(i),f(x),g(x),h(x),g'(x))]"
paulson@13496
   814
apply (unfold satisfies_MH_def) 
paulson@13496
   815
apply (intro FOL_reflections satisfies_reflections)
paulson@13494
   816
done
paulson@13494
   817
paulson@13494
   818
paulson@13502
   819
subsection{*Lemmas for Instantiating the Locale @{text "M_satisfies"}*}
paulson@13502
   820
paulson@13502
   821
paulson@13502
   822
subsubsection{*The @{term "Member"} Case*}
paulson@13502
   823
paulson@13502
   824
lemma Member_Reflects:
paulson@13502
   825
 "REFLECTS[\<lambda>u. \<exists>v[L]. v \<in> B \<and> (\<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L].
paulson@13502
   826
          v \<in> lstA \<and> is_nth(L,x,v,nx) \<and> is_nth(L,y,v,ny) \<and>
paulson@13502
   827
          is_bool_of_o(L, nx \<in> ny, bo) \<and> pair(L,v,bo,u)),
paulson@13502
   828
   \<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).
paulson@13807
   829
             v \<in> lstA \<and> is_nth(##Lset(i), x, v, nx) \<and> 
paulson@13807
   830
             is_nth(##Lset(i), y, v, ny) \<and>
paulson@13807
   831
          is_bool_of_o(##Lset(i), nx \<in> ny, bo) \<and> pair(##Lset(i), v, bo, u))]"
paulson@13502
   832
by (intro FOL_reflections function_reflections nth_reflection 
paulson@13502
   833
          bool_of_o_reflection)
paulson@13502
   834
paulson@13502
   835
paulson@13502
   836
lemma Member_replacement:
paulson@13502
   837
    "[|L(A); x \<in> nat; y \<in> nat|]
paulson@13502
   838
     ==> strong_replacement
paulson@13502
   839
	 (L, \<lambda>env z. \<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L]. 
paulson@13502
   840
              env \<in> list(A) & is_nth(L,x,env,nx) & is_nth(L,y,env,ny) & 
paulson@13502
   841
              is_bool_of_o(L, nx \<in> ny, bo) &
paulson@13502
   842
              pair(L, env, bo, z))"
paulson@13566
   843
apply (rule strong_replacementI)
paulson@13566
   844
apply (rule_tac u="{list(A),B,x,y}" 
paulson@13687
   845
         in gen_separation_multi [OF Member_Reflects], 
paulson@13687
   846
       auto simp add: nat_into_M list_closed)
paulson@13687
   847
apply (rule_tac env="[list(A),B,x,y]" in DPow_LsetI)
paulson@13566
   848
apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+
paulson@13502
   849
done
paulson@13502
   850
paulson@13502
   851
paulson@13502
   852
subsubsection{*The @{term "Equal"} Case*}
paulson@13502
   853
paulson@13502
   854
lemma Equal_Reflects:
paulson@13502
   855
 "REFLECTS[\<lambda>u. \<exists>v[L]. v \<in> B \<and> (\<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L].
paulson@13502
   856
          v \<in> lstA \<and> is_nth(L, x, v, nx) \<and> is_nth(L, y, v, ny) \<and>
paulson@13502
   857
          is_bool_of_o(L, nx = ny, bo) \<and> pair(L, v, bo, u)),
paulson@13502
   858
   \<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).
paulson@13807
   859
             v \<in> lstA \<and> is_nth(##Lset(i), x, v, nx) \<and> 
paulson@13807
   860
             is_nth(##Lset(i), y, v, ny) \<and>
paulson@13807
   861
          is_bool_of_o(##Lset(i), nx = ny, bo) \<and> pair(##Lset(i), v, bo, u))]"
paulson@13502
   862
by (intro FOL_reflections function_reflections nth_reflection 
paulson@13502
   863
          bool_of_o_reflection)
paulson@13502
   864
paulson@13502
   865
paulson@13502
   866
lemma Equal_replacement:
paulson@13502
   867
    "[|L(A); x \<in> nat; y \<in> nat|]
paulson@13502
   868
     ==> strong_replacement
paulson@13502
   869
	 (L, \<lambda>env z. \<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L]. 
paulson@13502
   870
              env \<in> list(A) & is_nth(L,x,env,nx) & is_nth(L,y,env,ny) & 
paulson@13502
   871
              is_bool_of_o(L, nx = ny, bo) &
paulson@13502
   872
              pair(L, env, bo, z))"
paulson@13566
   873
apply (rule strong_replacementI)
paulson@13566
   874
apply (rule_tac u="{list(A),B,x,y}" 
paulson@13687
   875
         in gen_separation_multi [OF Equal_Reflects], 
paulson@13687
   876
       auto simp add: nat_into_M list_closed)
paulson@13687
   877
apply (rule_tac env="[list(A),B,x,y]" in DPow_LsetI)
paulson@13566
   878
apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+
paulson@13502
   879
done
paulson@13502
   880
paulson@13502
   881
subsubsection{*The @{term "Nand"} Case*}
paulson@13502
   882
paulson@13502
   883
lemma Nand_Reflects:
paulson@13502
   884
    "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and>
paulson@13502
   885
	       (\<exists>rpe[L]. \<exists>rqe[L]. \<exists>andpq[L]. \<exists>notpq[L].
paulson@13502
   886
		 fun_apply(L, rp, u, rpe) \<and> fun_apply(L, rq, u, rqe) \<and>
paulson@13502
   887
		 is_and(L, rpe, rqe, andpq) \<and> is_not(L, andpq, notpq) \<and>
paulson@13502
   888
		 u \<in> list(A) \<and> pair(L, u, notpq, x)),
paulson@13502
   889
    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and>
paulson@13502
   890
     (\<exists>rpe \<in> Lset(i). \<exists>rqe \<in> Lset(i). \<exists>andpq \<in> Lset(i). \<exists>notpq \<in> Lset(i).
paulson@13807
   891
       fun_apply(##Lset(i), rp, u, rpe) \<and> fun_apply(##Lset(i), rq, u, rqe) \<and>
paulson@13807
   892
       is_and(##Lset(i), rpe, rqe, andpq) \<and> is_not(##Lset(i), andpq, notpq) \<and>
paulson@13807
   893
       u \<in> list(A) \<and> pair(##Lset(i), u, notpq, x))]"
paulson@13502
   894
apply (unfold is_and_def is_not_def) 
paulson@13502
   895
apply (intro FOL_reflections function_reflections)
paulson@13502
   896
done
paulson@13502
   897
paulson@13502
   898
lemma Nand_replacement:
paulson@13502
   899
    "[|L(A); L(rp); L(rq)|]
paulson@13502
   900
     ==> strong_replacement
paulson@13502
   901
	 (L, \<lambda>env z. \<exists>rpe[L]. \<exists>rqe[L]. \<exists>andpq[L]. \<exists>notpq[L]. 
paulson@13502
   902
               fun_apply(L,rp,env,rpe) & fun_apply(L,rq,env,rqe) & 
paulson@13502
   903
               is_and(L,rpe,rqe,andpq) & is_not(L,andpq,notpq) & 
paulson@13502
   904
               env \<in> list(A) & pair(L, env, notpq, z))"
paulson@13566
   905
apply (rule strong_replacementI)
paulson@13687
   906
apply (rule_tac u="{list(A),B,rp,rq}" 
paulson@13687
   907
         in gen_separation_multi [OF Nand_Reflects],
paulson@13687
   908
       auto simp add: list_closed)
paulson@13687
   909
apply (rule_tac env="[list(A),B,rp,rq]" in DPow_LsetI)
paulson@13566
   910
apply (rule sep_rules is_and_iff_sats is_not_iff_sats | simp)+
paulson@13502
   911
done
paulson@13502
   912
paulson@13502
   913
paulson@13502
   914
subsubsection{*The @{term "Forall"} Case*}
paulson@13502
   915
paulson@13502
   916
lemma Forall_Reflects:
paulson@13502
   917
 "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>bo[L]. u \<in> list(A) \<and>
paulson@13502
   918
                 is_bool_of_o (L,
paulson@13502
   919
     \<forall>a[L]. \<forall>co[L]. \<forall>rpco[L]. a \<in> A \<longrightarrow>
paulson@13502
   920
                is_Cons(L,a,u,co) \<longrightarrow> fun_apply(L,rp,co,rpco) \<longrightarrow> 
paulson@13502
   921
                number1(L,rpco),
paulson@13502
   922
                           bo) \<and> pair(L,u,bo,x)),
paulson@13502
   923
 \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>bo \<in> Lset(i). u \<in> list(A) \<and>
paulson@13807
   924
        is_bool_of_o (##Lset(i),
paulson@13502
   925
 \<forall>a \<in> Lset(i). \<forall>co \<in> Lset(i). \<forall>rpco \<in> Lset(i). a \<in> A \<longrightarrow>
paulson@13807
   926
	    is_Cons(##Lset(i),a,u,co) \<longrightarrow> fun_apply(##Lset(i),rp,co,rpco) \<longrightarrow> 
paulson@13807
   927
	    number1(##Lset(i),rpco),
paulson@13807
   928
		       bo) \<and> pair(##Lset(i),u,bo,x))]"
paulson@13502
   929
apply (unfold is_bool_of_o_def) 
paulson@13502
   930
apply (intro FOL_reflections function_reflections Cons_reflection)
paulson@13502
   931
done
paulson@13502
   932
paulson@13502
   933
lemma Forall_replacement:
paulson@13502
   934
   "[|L(A); L(rp)|]
paulson@13502
   935
    ==> strong_replacement
paulson@13502
   936
	(L, \<lambda>env z. \<exists>bo[L]. 
paulson@13502
   937
	      env \<in> list(A) & 
paulson@13502
   938
	      is_bool_of_o (L, 
paulson@13502
   939
			    \<forall>a[L]. \<forall>co[L]. \<forall>rpco[L]. 
paulson@13502
   940
			       a\<in>A --> is_Cons(L,a,env,co) -->
paulson@13502
   941
			       fun_apply(L,rp,co,rpco) --> number1(L, rpco), 
paulson@13502
   942
                            bo) &
paulson@13502
   943
	      pair(L,env,bo,z))"
paulson@13566
   944
apply (rule strong_replacementI)
paulson@13687
   945
apply (rule_tac u="{A,list(A),B,rp}" 
paulson@13687
   946
         in gen_separation_multi [OF Forall_Reflects],
paulson@13687
   947
       auto simp add: list_closed)
paulson@13687
   948
apply (rule_tac env="[A,list(A),B,rp]" in DPow_LsetI)
paulson@13566
   949
apply (rule sep_rules is_bool_of_o_iff_sats Cons_iff_sats | simp)+
paulson@13502
   950
done
paulson@13502
   951
paulson@13502
   952
subsubsection{*The @{term "transrec_replacement"} Case*}
paulson@13502
   953
paulson@13494
   954
lemma formula_rec_replacement_Reflects:
paulson@13494
   955
 "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L, u, y, x) \<and>
paulson@13494
   956
             is_wfrec (L, satisfies_MH(L,A), mesa, u, y)),
paulson@13807
   957
    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) \<and>
paulson@13807
   958
             is_wfrec (##Lset(i), satisfies_MH(##Lset(i),A), mesa, u, y))]"
paulson@13496
   959
by (intro FOL_reflections function_reflections satisfies_MH_reflection 
paulson@13496
   960
          is_wfrec_reflection) 
paulson@13496
   961
paulson@13496
   962
lemma formula_rec_replacement: 
paulson@13496
   963
      --{*For the @{term transrec}*}
paulson@13496
   964
   "[|n \<in> nat; L(A)|] ==> transrec_replacement(L, satisfies_MH(L,A), n)"
paulson@13566
   965
apply (rule transrec_replacementI, simp add: nat_into_M) 
paulson@13496
   966
apply (rule strong_replacementI)
paulson@13566
   967
apply (rule_tac u="{B,A,n,Memrel(eclose({n}))}"
paulson@13687
   968
         in gen_separation_multi [OF formula_rec_replacement_Reflects],
paulson@13687
   969
       auto simp add: nat_into_M)
paulson@13687
   970
apply (rule_tac env="[B,A,n,Memrel(eclose({n}))]" in DPow_LsetI)
paulson@13496
   971
apply (rule sep_rules satisfies_MH_iff_sats is_wfrec_iff_sats | simp)+
paulson@13494
   972
done
paulson@13494
   973
paulson@13502
   974
paulson@13502
   975
subsubsection{*The Lambda Replacement Case*}
paulson@13502
   976
paulson@13502
   977
lemma formula_rec_lambda_replacement_Reflects:
paulson@13502
   978
 "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B &
paulson@13502
   979
     mem_formula(L,u) &
paulson@13502
   980
     (\<exists>c[L].
paulson@13502
   981
	 is_formula_case
paulson@13502
   982
	  (L, satisfies_is_a(L,A), satisfies_is_b(L,A),
paulson@13502
   983
	   satisfies_is_c(L,A,g), satisfies_is_d(L,A,g),
paulson@13502
   984
	   u, c) &
paulson@13502
   985
	 pair(L,u,c,x)),
paulson@13807
   986
  \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & mem_formula(##Lset(i),u) &
paulson@13502
   987
     (\<exists>c \<in> Lset(i).
paulson@13502
   988
	 is_formula_case
paulson@13807
   989
	  (##Lset(i), satisfies_is_a(##Lset(i),A), satisfies_is_b(##Lset(i),A),
paulson@13807
   990
	   satisfies_is_c(##Lset(i),A,g), satisfies_is_d(##Lset(i),A,g),
paulson@13502
   991
	   u, c) &
paulson@13807
   992
	 pair(##Lset(i),u,c,x))]"
paulson@13502
   993
by (intro FOL_reflections function_reflections mem_formula_reflection
paulson@13502
   994
          is_formula_case_reflection satisfies_is_a_reflection
paulson@13502
   995
          satisfies_is_b_reflection satisfies_is_c_reflection
paulson@13502
   996
          satisfies_is_d_reflection)  
paulson@13502
   997
paulson@13502
   998
lemma formula_rec_lambda_replacement: 
paulson@13502
   999
      --{*For the @{term transrec}*}
paulson@13502
  1000
   "[|L(g); L(A)|] ==>
paulson@13502
  1001
    strong_replacement (L, 
paulson@13502
  1002
       \<lambda>x y. mem_formula(L,x) &
paulson@13502
  1003
             (\<exists>c[L]. is_formula_case(L, satisfies_is_a(L,A),
paulson@13502
  1004
                                  satisfies_is_b(L,A),
paulson@13502
  1005
                                  satisfies_is_c(L,A,g),
paulson@13502
  1006
                                  satisfies_is_d(L,A,g), x, c) &
paulson@13502
  1007
             pair(L, x, c, y)))" 
paulson@13502
  1008
apply (rule strong_replacementI)
paulson@13566
  1009
apply (rule_tac u="{B,A,g}"
paulson@13687
  1010
         in gen_separation_multi [OF formula_rec_lambda_replacement_Reflects], 
paulson@13687
  1011
       auto)
paulson@13687
  1012
apply (rule_tac env="[A,g,B]" in DPow_LsetI)
paulson@13502
  1013
apply (rule sep_rules mem_formula_iff_sats
paulson@13502
  1014
          formula_case_iff_sats satisfies_is_a_iff_sats
paulson@13502
  1015
          satisfies_is_b_iff_sats satisfies_is_c_iff_sats
paulson@13502
  1016
          satisfies_is_d_iff_sats | simp)+
paulson@13502
  1017
done
paulson@13502
  1018
paulson@13502
  1019
paulson@13502
  1020
subsection{*Instantiating @{text M_satisfies}*}
paulson@13502
  1021
paulson@13502
  1022
lemma M_satisfies_axioms_L: "M_satisfies_axioms(L)"
paulson@13502
  1023
  apply (rule M_satisfies_axioms.intro)
paulson@13502
  1024
       apply (assumption | rule
paulson@13502
  1025
	 Member_replacement Equal_replacement 
paulson@13502
  1026
         Nand_replacement Forall_replacement
paulson@13502
  1027
         formula_rec_replacement formula_rec_lambda_replacement)+
paulson@13502
  1028
  done
paulson@13502
  1029
paulson@13502
  1030
theorem M_satisfies_L: "PROP M_satisfies(L)"
ballarin@19931
  1031
  apply (rule M_satisfies.intro)
ballarin@19931
  1032
   apply (rule M_eclose_L)
ballarin@19931
  1033
  apply (rule M_satisfies_axioms_L)
ballarin@19931
  1034
  done
paulson@13502
  1035
paulson@13504
  1036
text{*Finally: the point of the whole theory!*}
paulson@13504
  1037
lemmas satisfies_closed = M_satisfies.satisfies_closed [OF M_satisfies_L]
paulson@13504
  1038
   and satisfies_abs = M_satisfies.satisfies_abs [OF M_satisfies_L]
paulson@13504
  1039
paulson@13494
  1040
end