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