src/ZF/Constructible/DPow_absolute.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 47072 777549486d44
child 58871 c399ae4b836f
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
     1
(*  Title:      ZF/Constructible/DPow_absolute.thy
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
     3
*)
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
     4
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
     5
header {*Absoluteness for the Definable Powerset Function*}
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
     6
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 13807
diff changeset
     8
theory DPow_absolute imports Satisfies_absolute begin
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
     9
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    10
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    11
subsection{*Preliminary Internalizations*}
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    12
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    13
subsubsection{*The Operator @{term is_formula_rec}*}
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    14
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    15
text{*The three arguments of @{term p} are always 2, 1, 0.  It is buried
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    16
   within 11 quantifiers!!*}
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    17
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    18
(* is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o"
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    19
   "is_formula_rec(M,MH,p,z)  ==
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    20
      \<exists>dp[M]. \<exists>i[M]. \<exists>f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) & 
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    21
       2       1      0
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    22
             successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)"
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    23
*)
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    24
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    25
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    26
  formula_rec_fm :: "[i, i, i]=>i" where
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    27
 "formula_rec_fm(mh,p,z) == 
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    28
    Exists(Exists(Exists(
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    29
      And(finite_ordinal_fm(2),
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    30
       And(depth_fm(p#+3,2),
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    31
        And(succ_fm(2,1), 
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    32
          And(fun_apply_fm(0,p#+3,z#+3), is_transrec_fm(mh,1,0))))))))"
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    33
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    34
lemma is_formula_rec_type [TC]:
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    35
     "[| p \<in> formula; x \<in> nat; z \<in> nat |] 
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    36
      ==> formula_rec_fm(p,x,z) \<in> formula"
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    37
by (simp add: formula_rec_fm_def) 
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    38
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    39
lemma sats_formula_rec_fm:
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    40
  assumes MH_iff_sats: 
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    41
      "!!a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10. 
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    42
        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A; a7\<in>A; a8\<in>A; a9\<in>A; a10\<in>A|]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    43
        ==> MH(a2, a1, a0) \<longleftrightarrow> 
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    44
            sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    45
                          Cons(a4,Cons(a5,Cons(a6,Cons(a7,
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    46
                                  Cons(a8,Cons(a9,Cons(a10,env))))))))))))"
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    47
  shows 
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    48
      "[|x \<in> nat; z \<in> nat; env \<in> list(A)|]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    49
       ==> sats(A, formula_rec_fm(p,x,z), env) \<longleftrightarrow> 
13807
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
    50
           is_formula_rec(##A, MH, nth(x,env), nth(z,env))"
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    51
by (simp add: formula_rec_fm_def sats_is_transrec_fm is_formula_rec_def 
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    52
              MH_iff_sats [THEN iff_sym])
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    53
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    54
lemma formula_rec_iff_sats:
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    55
  assumes MH_iff_sats: 
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    56
      "!!a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10. 
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    57
        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A; a7\<in>A; a8\<in>A; a9\<in>A; a10\<in>A|]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    58
        ==> MH(a2, a1, a0) \<longleftrightarrow> 
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    59
            sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    60
                          Cons(a4,Cons(a5,Cons(a6,Cons(a7,
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    61
                                  Cons(a8,Cons(a9,Cons(a10,env))))))))))))"
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    62
  shows
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    63
  "[|nth(i,env) = x; nth(k,env) = z; 
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    64
      i \<in> nat; k \<in> nat; env \<in> list(A)|]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    65
   ==> is_formula_rec(##A, MH, x, z) \<longleftrightarrow> sats(A, formula_rec_fm(p,i,k), env)" 
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    66
by (simp add: sats_formula_rec_fm [OF MH_iff_sats])
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    67
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    68
theorem formula_rec_reflection:
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    69
  assumes MH_reflection:
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    70
    "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)), 
13807
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
    71
                     \<lambda>i x. MH(##Lset(i), f'(x), f(x), g(x), h(x))]"
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    72
  shows "REFLECTS[\<lambda>x. is_formula_rec(L, MH(L,x), f(x), h(x)), 
13807
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
    73
               \<lambda>i x. is_formula_rec(##Lset(i), MH(##Lset(i),x), f(x), h(x))]"
13655
95b95cdb4704 Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents: 13634
diff changeset
    74
apply (simp (no_asm_use) only: is_formula_rec_def)
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    75
apply (intro FOL_reflections function_reflections fun_plus_reflections
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    76
             depth_reflection is_transrec_reflection MH_reflection)
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    77
done
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    78
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    79
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    80
subsubsection{*The Operator @{term is_satisfies}*}
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    81
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    82
(* is_satisfies(M,A,p,z) == is_formula_rec (M, satisfies_MH(M,A), p, z) *)
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    83
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    84
  satisfies_fm :: "[i,i,i]=>i" where
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    85
    "satisfies_fm(x) == formula_rec_fm (satisfies_MH_fm(x#+5#+6, 2, 1, 0))"
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    86
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    87
lemma is_satisfies_type [TC]:
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    88
     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> satisfies_fm(x,y,z) \<in> formula"
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    89
by (simp add: satisfies_fm_def)
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    90
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    91
lemma sats_satisfies_fm [simp]:
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    92
   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    93
    ==> sats(A, satisfies_fm(x,y,z), env) \<longleftrightarrow>
13807
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
    94
        is_satisfies(##A, nth(x,env), nth(y,env), nth(z,env))"
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    95
by (simp add: satisfies_fm_def is_satisfies_def sats_satisfies_MH_fm
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    96
              sats_formula_rec_fm)
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    97
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    98
lemma satisfies_iff_sats:
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
    99
      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   100
          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   101
       ==> is_satisfies(##A, x, y, z) \<longleftrightarrow> sats(A, satisfies_fm(i,j,k), env)"
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   102
by (simp add: sats_satisfies_fm)
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   103
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   104
theorem satisfies_reflection:
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   105
     "REFLECTS[\<lambda>x. is_satisfies(L,f(x),g(x),h(x)),
13807
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
   106
               \<lambda>i x. is_satisfies(##Lset(i),f(x),g(x),h(x))]"
13655
95b95cdb4704 Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents: 13634
diff changeset
   107
apply (simp only: is_satisfies_def)
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   108
apply (intro formula_rec_reflection satisfies_MH_reflection)
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   109
done
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   110
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   111
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   112
subsection {*Relativization of the Operator @{term DPow'}*}
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   113
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   114
lemma DPow'_eq: 
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   115
  "DPow'(A) = {z . ep \<in> list(A) * formula, 
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   116
                    \<exists>env \<in> list(A). \<exists>p \<in> formula. 
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   117
                       ep = <env,p> & z = {x\<in>A. sats(A, p, Cons(x,env))}}"
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   118
by (simp add: DPow'_def, blast) 
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   119
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   120
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   121
text{*Relativize the use of @{term sats} within @{term DPow'}
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   122
(the comprehension).*}
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   123
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   124
  is_DPow_sats :: "[i=>o,i,i,i,i] => o" where
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   125
   "is_DPow_sats(M,A,env,p,x) ==
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   126
      \<forall>n1[M]. \<forall>e[M]. \<forall>sp[M]. 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   127
             is_satisfies(M,A,p,sp) \<longrightarrow> is_Cons(M,x,env,e) \<longrightarrow> 
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   128
             fun_apply(M, sp, e, n1) \<longrightarrow> number1(M, n1)"
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   129
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   130
lemma (in M_satisfies) DPow_sats_abs:
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   131
    "[| M(A); env \<in> list(A); p \<in> formula; M(x) |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   132
    ==> is_DPow_sats(M,A,env,p,x) \<longleftrightarrow> sats(A, p, Cons(x,env))"
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   133
apply (subgoal_tac "M(env)") 
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   134
 apply (simp add: is_DPow_sats_def satisfies_closed satisfies_abs) 
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   135
apply (blast dest: transM) 
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   136
done
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   137
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   138
lemma (in M_satisfies) Collect_DPow_sats_abs:
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   139
    "[| M(A); env \<in> list(A); p \<in> formula |]
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   140
    ==> Collect(A, is_DPow_sats(M,A,env,p)) = 
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   141
        {x \<in> A. sats(A, p, Cons(x,env))}"
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   142
by (simp add: DPow_sats_abs transM [of _ A])
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   143
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   144
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   145
subsubsection{*The Operator @{term is_DPow_sats}, Internalized*}
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   146
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   147
(* is_DPow_sats(M,A,env,p,x) ==
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   148
      \<forall>n1[M]. \<forall>e[M]. \<forall>sp[M]. 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   149
             is_satisfies(M,A,p,sp) \<longrightarrow> is_Cons(M,x,env,e) \<longrightarrow> 
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   150
             fun_apply(M, sp, e, n1) \<longrightarrow> number1(M, n1) *)
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   151
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   152
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   153
  DPow_sats_fm :: "[i,i,i,i]=>i" where
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   154
  "DPow_sats_fm(A,env,p,x) ==
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   155
   Forall(Forall(Forall(
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   156
     Implies(satisfies_fm(A#+3,p#+3,0), 
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   157
       Implies(Cons_fm(x#+3,env#+3,1), 
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   158
         Implies(fun_apply_fm(0,1,2), number1_fm(2)))))))"
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   159
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   160
lemma is_DPow_sats_type [TC]:
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   161
     "[| A \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   162
      ==> DPow_sats_fm(A,x,y,z) \<in> formula"
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   163
by (simp add: DPow_sats_fm_def)
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   164
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   165
lemma sats_DPow_sats_fm [simp]:
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   166
   "[| u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   167
    ==> sats(A, DPow_sats_fm(u,x,y,z), env) \<longleftrightarrow>
13807
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
   168
        is_DPow_sats(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   169
by (simp add: DPow_sats_fm_def is_DPow_sats_def)
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   170
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   171
lemma DPow_sats_iff_sats:
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   172
  "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   173
      u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   174
   ==> is_DPow_sats(##A,nu,nx,ny,nz) \<longleftrightarrow>
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   175
       sats(A, DPow_sats_fm(u,x,y,z), env)"
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   176
by simp
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   177
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   178
theorem DPow_sats_reflection:
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   179
     "REFLECTS[\<lambda>x. is_DPow_sats(L,f(x),g(x),h(x),g'(x)),
13807
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
   180
               \<lambda>i x. is_DPow_sats(##Lset(i),f(x),g(x),h(x),g'(x))]"
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   181
apply (unfold is_DPow_sats_def) 
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   182
apply (intro FOL_reflections function_reflections extra_reflections
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   183
             satisfies_reflection)
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   184
done
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   185
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   186
13687
22dce9134953 simpler separation/replacement proofs
paulson
parents: 13655
diff changeset
   187
subsection{*A Locale for Relativizing the Operator @{term DPow'}*}
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   188
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   189
locale M_DPow = M_satisfies +
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   190
 assumes sep:
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   191
   "[| M(A); env \<in> list(A); p \<in> formula |]
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   192
    ==> separation(M, \<lambda>x. is_DPow_sats(M,A,env,p,x))"
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   193
 and rep: 
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   194
    "M(A)
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   195
    ==> strong_replacement (M, 
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   196
         \<lambda>ep z. \<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   197
                  pair(M,env,p,ep) & 
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   198
                  is_Collect(M, A, \<lambda>x. is_DPow_sats(M,A,env,p,x), z))"
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   199
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   200
lemma (in M_DPow) sep':
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   201
   "[| M(A); env \<in> list(A); p \<in> formula |]
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   202
    ==> separation(M, \<lambda>x. sats(A, p, Cons(x,env)))"
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   203
by (insert sep [of A env p], simp add: DPow_sats_abs)
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   204
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   205
lemma (in M_DPow) rep':
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   206
   "M(A)
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   207
    ==> strong_replacement (M, 
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   208
         \<lambda>ep z. \<exists>env\<in>list(A). \<exists>p\<in>formula.
13504
59066e97b551 Tidying up
paulson
parents: 13503
diff changeset
   209
                  ep = <env,p> & z = {x \<in> A . sats(A, p, Cons(x, env))})" 
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   210
by (insert rep [of A], simp add: Collect_DPow_sats_abs) 
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   211
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   212
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   213
lemma univalent_pair_eq:
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   214
     "univalent (M, A, \<lambda>xy z. \<exists>x\<in>B. \<exists>y\<in>C. xy = \<langle>x,y\<rangle> \<and> z = f(x,y))"
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   215
by (simp add: univalent_def, blast) 
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   216
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   217
lemma (in M_DPow) DPow'_closed: "M(A) ==> M(DPow'(A))"
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   218
apply (simp add: DPow'_eq)
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   219
apply (fast intro: rep' sep' univalent_pair_eq)  
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   220
done
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   221
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   222
text{*Relativization of the Operator @{term DPow'}*}
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   223
definition 
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   224
  is_DPow' :: "[i=>o,i,i] => o" where
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   225
    "is_DPow'(M,A,Z) == 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   226
       \<forall>X[M]. X \<in> Z \<longleftrightarrow> 
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   227
         subset(M,X,A) & 
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   228
           (\<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   229
                    is_Collect(M, A, is_DPow_sats(M,A,env,p), X))"
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   230
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   231
lemma (in M_DPow) DPow'_abs:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   232
    "[|M(A); M(Z)|] ==> is_DPow'(M,A,Z) \<longleftrightarrow> Z = DPow'(A)"
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   233
apply (rule iffI)
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   234
 prefer 2 apply (simp add: is_DPow'_def DPow'_def Collect_DPow_sats_abs) 
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   235
apply (rule M_equalityI) 
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   236
apply (simp add: is_DPow'_def DPow'_def Collect_DPow_sats_abs, assumption)
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   237
apply (erule DPow'_closed)
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   238
done
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   239
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   240
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   241
subsection{*Instantiating the Locale @{text M_DPow}*}
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   242
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   243
subsubsection{*The Instance of Separation*}
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   244
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   245
lemma DPow_separation:
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   246
    "[| L(A); env \<in> list(A); p \<in> formula |]
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   247
     ==> separation(L, \<lambda>x. is_DPow_sats(L,A,env,p,x))"
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   248
apply (rule gen_separation_multi [OF DPow_sats_reflection, of "{A,env,p}"], 
13687
22dce9134953 simpler separation/replacement proofs
paulson
parents: 13655
diff changeset
   249
       auto intro: transL)
22dce9134953 simpler separation/replacement proofs
paulson
parents: 13655
diff changeset
   250
apply (rule_tac env="[A,env,p]" in DPow_LsetI)
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   251
apply (rule DPow_sats_iff_sats sep_rules | simp)+
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   252
done
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   253
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   254
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   255
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   256
subsubsection{*The Instance of Replacement*}
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   257
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   258
lemma DPow_replacement_Reflects:
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   259
 "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B &
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   260
             (\<exists>env[L]. \<exists>p[L].
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   261
               mem_formula(L,p) & mem_list(L,A,env) & pair(L,env,p,u) &
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   262
               is_Collect (L, A, is_DPow_sats(L,A,env,p), x)),
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   263
    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B &
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   264
             (\<exists>env \<in> Lset(i). \<exists>p \<in> Lset(i).
13807
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
   265
               mem_formula(##Lset(i),p) & mem_list(##Lset(i),A,env) & 
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
   266
               pair(##Lset(i),env,p,u) &
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
   267
               is_Collect (##Lset(i), A, is_DPow_sats(##Lset(i),A,env,p), x))]"
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   268
apply (unfold is_Collect_def) 
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   269
apply (intro FOL_reflections function_reflections mem_formula_reflection
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   270
          mem_list_reflection DPow_sats_reflection)
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   271
done
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   272
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   273
lemma DPow_replacement:
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   274
    "L(A)
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   275
    ==> strong_replacement (L, 
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   276
         \<lambda>ep z. \<exists>env[L]. \<exists>p[L]. mem_formula(L,p) & mem_list(L,A,env) &
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   277
                  pair(L,env,p,ep) & 
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   278
                  is_Collect(L, A, \<lambda>x. is_DPow_sats(L,A,env,p,x), z))"
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   279
apply (rule strong_replacementI)
13687
22dce9134953 simpler separation/replacement proofs
paulson
parents: 13655
diff changeset
   280
apply (rule_tac u="{A,B}" 
22dce9134953 simpler separation/replacement proofs
paulson
parents: 13655
diff changeset
   281
         in gen_separation_multi [OF DPow_replacement_Reflects], 
22dce9134953 simpler separation/replacement proofs
paulson
parents: 13655
diff changeset
   282
       auto)
13566
52a419210d5c Streamlined proofs of instances of Separation
paulson
parents: 13505
diff changeset
   283
apply (unfold is_Collect_def) 
13687
22dce9134953 simpler separation/replacement proofs
paulson
parents: 13655
diff changeset
   284
apply (rule_tac env="[A,B]" in DPow_LsetI)
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   285
apply (rule sep_rules mem_formula_iff_sats mem_list_iff_sats 
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   286
            DPow_sats_iff_sats | simp)+
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   287
done
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   288
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   289
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   290
subsubsection{*Actually Instantiating the Locale*}
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   291
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   292
lemma M_DPow_axioms_L: "M_DPow_axioms(L)"
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   293
  apply (rule M_DPow_axioms.intro)
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   294
   apply (assumption | rule DPow_separation DPow_replacement)+
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   295
  done
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   296
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   297
theorem M_DPow_L: "PROP M_DPow(L)"
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   298
  apply (rule M_DPow.intro)
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 16417
diff changeset
   299
   apply (rule M_satisfies_L)
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   300
  apply (rule M_DPow_axioms_L)
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   301
  done
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   302
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   303
lemmas DPow'_closed [intro, simp] = M_DPow.DPow'_closed [OF M_DPow_L]
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   304
  and DPow'_abs [intro, simp] = M_DPow.DPow'_abs [OF M_DPow_L]
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   305
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   306
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   307
subsubsection{*The Operator @{term is_Collect}*}
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   308
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   309
text{*The formula @{term is_P} has one free variable, 0, and it is
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   310
enclosed within a single quantifier.*}
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   311
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   312
(* is_Collect :: "[i=>o,i,i=>o,i] => o"
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   313
    "is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> x \<in> A & P(x)" *)
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   314
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   315
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   316
  Collect_fm :: "[i, i, i]=>i" where
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   317
 "Collect_fm(A,is_P,z) == 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   318
        Forall(Iff(Member(0,succ(z)),
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   319
                   And(Member(0,succ(A)), is_P)))"
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   320
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   321
lemma is_Collect_type [TC]:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   322
     "[| is_P \<in> formula; x \<in> nat; y \<in> nat |] 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   323
      ==> Collect_fm(x,is_P,y) \<in> formula"
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   324
by (simp add: Collect_fm_def)
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   325
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   326
lemma sats_Collect_fm:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   327
  assumes is_P_iff_sats: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   328
      "!!a. a \<in> A ==> is_P(a) \<longleftrightarrow> sats(A, p, Cons(a, env))"
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   329
  shows 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   330
      "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   331
       ==> sats(A, Collect_fm(x,p,y), env) \<longleftrightarrow>
13807
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
   332
           is_Collect(##A, nth(x,env), is_P, nth(y,env))"
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   333
by (simp add: Collect_fm_def is_Collect_def is_P_iff_sats [THEN iff_sym])
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   334
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   335
lemma Collect_iff_sats:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   336
  assumes is_P_iff_sats: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   337
      "!!a. a \<in> A ==> is_P(a) \<longleftrightarrow> sats(A, p, Cons(a, env))"
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   338
  shows 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   339
  "[| nth(i,env) = x; nth(j,env) = y;
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   340
      i \<in> nat; j \<in> nat; env \<in> list(A)|]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   341
   ==> is_Collect(##A, x, is_P, y) \<longleftrightarrow> sats(A, Collect_fm(i,p,j), env)"
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   342
by (simp add: sats_Collect_fm [OF is_P_iff_sats])
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   343
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   344
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   345
text{*The second argument of @{term is_P} gives it direct access to @{term x},
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   346
  which is essential for handling free variable references.*}
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   347
theorem Collect_reflection:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   348
  assumes is_P_reflection:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   349
    "!!h f g. REFLECTS[\<lambda>x. is_P(L, f(x), g(x)),
13807
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
   350
                     \<lambda>i x. is_P(##Lset(i), f(x), g(x))]"
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   351
  shows "REFLECTS[\<lambda>x. is_Collect(L, f(x), is_P(L,x), g(x)),
13807
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
   352
               \<lambda>i x. is_Collect(##Lset(i), f(x), is_P(##Lset(i), x), g(x))]"
13655
95b95cdb4704 Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents: 13634
diff changeset
   353
apply (simp (no_asm_use) only: is_Collect_def)
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   354
apply (intro FOL_reflections is_P_reflection)
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   355
done
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   356
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   357
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   358
subsubsection{*The Operator @{term is_Replace}*}
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   359
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   360
text{*BEWARE!  The formula @{term is_P} has free variables 0, 1
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   361
 and not the usual 1, 0!  It is enclosed within two quantifiers.*}
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   362
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   363
(*  is_Replace :: "[i=>o,i,[i,i]=>o,i] => o"
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   364
    "is_Replace(M,A,P,z) == \<forall>u[M]. u \<in> z \<longleftrightarrow> (\<exists>x[M]. x\<in>A & P(x,u))" *)
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   365
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   366
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   367
  Replace_fm :: "[i, i, i]=>i" where
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   368
  "Replace_fm(A,is_P,z) == 
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   369
        Forall(Iff(Member(0,succ(z)),
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   370
                   Exists(And(Member(0,A#+2), is_P))))"
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   371
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   372
lemma is_Replace_type [TC]:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   373
     "[| is_P \<in> formula; x \<in> nat; y \<in> nat |] 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   374
      ==> Replace_fm(x,is_P,y) \<in> formula"
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   375
by (simp add: Replace_fm_def)
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   376
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   377
lemma sats_Replace_fm:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   378
  assumes is_P_iff_sats: 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   379
      "!!a b. [|a \<in> A; b \<in> A|] 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   380
              ==> is_P(a,b) \<longleftrightarrow> sats(A, p, Cons(a,Cons(b,env)))"
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   381
  shows 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   382
      "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   383
       ==> sats(A, Replace_fm(x,p,y), env) \<longleftrightarrow>
13807
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
   384
           is_Replace(##A, nth(x,env), is_P, nth(y,env))"
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   385
by (simp add: Replace_fm_def is_Replace_def is_P_iff_sats [THEN iff_sym])
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   386
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   387
lemma Replace_iff_sats:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   388
  assumes is_P_iff_sats: 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   389
      "!!a b. [|a \<in> A; b \<in> A|] 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   390
              ==> is_P(a,b) \<longleftrightarrow> sats(A, p, Cons(a,Cons(b,env)))"
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   391
  shows 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   392
  "[| nth(i,env) = x; nth(j,env) = y;
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   393
      i \<in> nat; j \<in> nat; env \<in> list(A)|]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   394
   ==> is_Replace(##A, x, is_P, y) \<longleftrightarrow> sats(A, Replace_fm(i,p,j), env)"
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   395
by (simp add: sats_Replace_fm [OF is_P_iff_sats])
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   396
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   397
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   398
text{*The second argument of @{term is_P} gives it direct access to @{term x},
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   399
  which is essential for handling free variable references.*}
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   400
theorem Replace_reflection:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   401
  assumes is_P_reflection:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   402
    "!!h f g. REFLECTS[\<lambda>x. is_P(L, f(x), g(x), h(x)),
13807
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
   403
                     \<lambda>i x. is_P(##Lset(i), f(x), g(x), h(x))]"
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   404
  shows "REFLECTS[\<lambda>x. is_Replace(L, f(x), is_P(L,x), g(x)),
13807
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
   405
               \<lambda>i x. is_Replace(##Lset(i), f(x), is_P(##Lset(i), x), g(x))]"
13655
95b95cdb4704 Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents: 13634
diff changeset
   406
apply (simp (no_asm_use) only: is_Replace_def)
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   407
apply (intro FOL_reflections is_P_reflection)
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   408
done
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   409
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   410
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   411
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   412
subsubsection{*The Operator @{term is_DPow'}, Internalized*}
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   413
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   414
(*  "is_DPow'(M,A,Z) == 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   415
       \<forall>X[M]. X \<in> Z \<longleftrightarrow> 
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   416
         subset(M,X,A) & 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   417
           (\<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   418
                    is_Collect(M, A, is_DPow_sats(M,A,env,p), X))" *)
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   419
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   420
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   421
  DPow'_fm :: "[i,i]=>i" where
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   422
    "DPow'_fm(A,Z) == 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   423
      Forall(
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   424
       Iff(Member(0,succ(Z)),
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   425
        And(subset_fm(0,succ(A)),
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   426
         Exists(Exists(
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   427
          And(mem_formula_fm(0),
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   428
           And(mem_list_fm(A#+3,1),
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   429
            Collect_fm(A#+3, 
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   430
                       DPow_sats_fm(A#+4, 2, 1, 0), 2))))))))"
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   431
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   432
lemma is_DPow'_type [TC]:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   433
     "[| x \<in> nat; y \<in> nat |] ==> DPow'_fm(x,y) \<in> formula"
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   434
by (simp add: DPow'_fm_def)
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   435
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   436
lemma sats_DPow'_fm [simp]:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   437
   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   438
    ==> sats(A, DPow'_fm(x,y), env) \<longleftrightarrow>
13807
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
   439
        is_DPow'(##A, nth(x,env), nth(y,env))"
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   440
by (simp add: DPow'_fm_def is_DPow'_def sats_subset_fm' sats_Collect_fm)
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   441
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   442
lemma DPow'_iff_sats:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   443
      "[| nth(i,env) = x; nth(j,env) = y; 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   444
          i \<in> nat; j \<in> nat; env \<in> list(A)|]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   445
       ==> is_DPow'(##A, x, y) \<longleftrightarrow> sats(A, DPow'_fm(i,j), env)"
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   446
by (simp add: sats_DPow'_fm)
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   447
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   448
theorem DPow'_reflection:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   449
     "REFLECTS[\<lambda>x. is_DPow'(L,f(x),g(x)),
13807
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
   450
               \<lambda>i x. is_DPow'(##Lset(i),f(x),g(x))]"
13655
95b95cdb4704 Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents: 13634
diff changeset
   451
apply (simp only: is_DPow'_def)
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   452
apply (intro FOL_reflections function_reflections mem_formula_reflection
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   453
             mem_list_reflection Collect_reflection DPow_sats_reflection)
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   454
done
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   455
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   456
13687
22dce9134953 simpler separation/replacement proofs
paulson
parents: 13655
diff changeset
   457
subsection{*A Locale for Relativizing the Operator @{term Lset}*}
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   458
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   459
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   460
  transrec_body :: "[i=>o,i,i,i,i] => o" where
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   461
    "transrec_body(M,g,x) ==
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   462
      \<lambda>y z. \<exists>gy[M]. y \<in> x & fun_apply(M,g,y,gy) & is_DPow'(M,gy,z)"
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   463
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   464
lemma (in M_DPow) transrec_body_abs:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   465
     "[|M(x); M(g); M(z)|]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   466
    ==> transrec_body(M,g,x,y,z) \<longleftrightarrow> y \<in> x & z = DPow'(g`y)"
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   467
by (simp add: transrec_body_def DPow'_abs transM [of _ x])
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   468
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   469
locale M_Lset = M_DPow +
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   470
 assumes strong_rep:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   471
   "[|M(x); M(g)|] ==> strong_replacement(M, \<lambda>y z. transrec_body(M,g,x,y,z))"
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   472
 and transrec_rep: 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   473
    "M(i) ==> transrec_replacement(M, \<lambda>x f u. 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   474
              \<exists>r[M]. is_Replace(M, x, transrec_body(M,f,x), r) & 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   475
                     big_union(M, r, u), i)"
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   476
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   477
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   478
lemma (in M_Lset) strong_rep':
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   479
   "[|M(x); M(g)|]
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   480
    ==> strong_replacement(M, \<lambda>y z. y \<in> x & z = DPow'(g`y))"
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   481
by (insert strong_rep [of x g], simp add: transrec_body_abs)
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   482
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   483
lemma (in M_Lset) DPow_apply_closed:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   484
   "[|M(f); M(x); y\<in>x|] ==> M(DPow'(f`y))"
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   485
by (blast intro: DPow'_closed dest: transM) 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   486
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   487
lemma (in M_Lset) RepFun_DPow_apply_closed:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   488
   "[|M(f); M(x)|] ==> M({DPow'(f`y). y\<in>x})"
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   489
by (blast intro: DPow_apply_closed RepFun_closed2 strong_rep') 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   490
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   491
lemma (in M_Lset) RepFun_DPow_abs:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   492
     "[|M(x); M(f); M(r) |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   493
      ==> is_Replace(M, x, \<lambda>y z. transrec_body(M,f,x,y,z), r) \<longleftrightarrow>
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   494
          r =  {DPow'(f`y). y\<in>x}"
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   495
apply (simp add: transrec_body_abs RepFun_def) 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   496
apply (rule iff_trans) 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   497
apply (rule Replace_abs) 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   498
apply (simp_all add: DPow_apply_closed strong_rep') 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   499
done
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   500
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   501
lemma (in M_Lset) transrec_rep':
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   502
   "M(i) ==> transrec_replacement(M, \<lambda>x f u. u = (\<Union>y\<in>x. DPow'(f ` y)), i)"
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   503
apply (insert transrec_rep [of i]) 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   504
apply (simp add: RepFun_DPow_apply_closed RepFun_DPow_abs 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   505
       transrec_replacement_def) 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   506
done
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   507
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   508
13687
22dce9134953 simpler separation/replacement proofs
paulson
parents: 13655
diff changeset
   509
text{*Relativization of the Operator @{term Lset}*}
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   510
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   511
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   512
  is_Lset :: "[i=>o, i, i] => o" where
13692
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   513
   --{*We can use the term language below because @{term is_Lset} will
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   514
       not have to be internalized: it isn't used in any instance of
27f3c83e2984 proof streamlining
paulson
parents: 13687
diff changeset
   515
       separation.*}
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   516
   "is_Lset(M,a,z) == is_transrec(M, %x f u. u = (\<Union>y\<in>x. DPow'(f`y)), a, z)"
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   517
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   518
lemma (in M_Lset) Lset_abs:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   519
  "[|Ord(i);  M(i);  M(z)|] 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   520
   ==> is_Lset(M,i,z) \<longleftrightarrow> z = Lset(i)"
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   521
apply (simp add: is_Lset_def Lset_eq_transrec_DPow') 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   522
apply (rule transrec_abs)  
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13566
diff changeset
   523
apply (simp_all add: transrec_rep' relation2_def RepFun_DPow_apply_closed)
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   524
done
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   525
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   526
lemma (in M_Lset) Lset_closed:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   527
  "[|Ord(i);  M(i)|] ==> M(Lset(i))"
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   528
apply (simp add: Lset_eq_transrec_DPow') 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   529
apply (rule transrec_closed [OF transrec_rep']) 
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13566
diff changeset
   530
apply (simp_all add: relation2_def RepFun_DPow_apply_closed)
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   531
done
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   532
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   533
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   534
subsection{*Instantiating the Locale @{text M_Lset}*}
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   535
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   536
subsubsection{*The First Instance of Replacement*}
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   537
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   538
lemma strong_rep_Reflects:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   539
 "REFLECTS [\<lambda>u. \<exists>v[L]. v \<in> B & (\<exists>gy[L].
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   540
                          v \<in> x & fun_apply(L,g,v,gy) & is_DPow'(L,gy,u)),
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   541
   \<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B & (\<exists>gy \<in> Lset(i).
13807
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
   542
            v \<in> x & fun_apply(##Lset(i),g,v,gy) & is_DPow'(##Lset(i),gy,u))]"
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   543
by (intro FOL_reflections function_reflections DPow'_reflection)
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   544
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   545
lemma strong_rep:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   546
   "[|L(x); L(g)|] ==> strong_replacement(L, \<lambda>y z. transrec_body(L,g,x,y,z))"
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   547
apply (unfold transrec_body_def)  
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   548
apply (rule strong_replacementI) 
13687
22dce9134953 simpler separation/replacement proofs
paulson
parents: 13655
diff changeset
   549
apply (rule_tac u="{x,g,B}" 
22dce9134953 simpler separation/replacement proofs
paulson
parents: 13655
diff changeset
   550
         in gen_separation_multi [OF strong_rep_Reflects], auto)
22dce9134953 simpler separation/replacement proofs
paulson
parents: 13655
diff changeset
   551
apply (rule_tac env="[x,g,B]" in DPow_LsetI)
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   552
apply (rule sep_rules DPow'_iff_sats | simp)+
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   553
done
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   554
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   555
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   556
subsubsection{*The Second Instance of Replacement*}
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   557
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   558
lemma transrec_rep_Reflects:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   559
 "REFLECTS [\<lambda>x. \<exists>v[L]. v \<in> B &
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   560
              (\<exists>y[L]. pair(L,v,y,x) &
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   561
             is_wfrec (L, \<lambda>x f u. \<exists>r[L].
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   562
                is_Replace (L, x, \<lambda>y z. 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   563
                     \<exists>gy[L]. y \<in> x & fun_apply(L,f,y,gy) & 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   564
                      is_DPow'(L,gy,z), r) & big_union(L,r,u), mr, v, y)),
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   565
    \<lambda>i x. \<exists>v \<in> Lset(i). v \<in> B &
13807
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
   566
              (\<exists>y \<in> Lset(i). pair(##Lset(i),v,y,x) &
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
   567
             is_wfrec (##Lset(i), \<lambda>x f u. \<exists>r \<in> Lset(i).
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
   568
                is_Replace (##Lset(i), x, \<lambda>y z. 
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
   569
                     \<exists>gy \<in> Lset(i). y \<in> x & fun_apply(##Lset(i),f,y,gy) & 
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
   570
                      is_DPow'(##Lset(i),gy,z), r) & 
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
   571
                      big_union(##Lset(i),r,u), mr, v, y))]" 
13655
95b95cdb4704 Tidying up. New primitives is_iterates and is_iterates_fm.
paulson
parents: 13634
diff changeset
   572
apply (simp only: rex_setclass_is_bex [symmetric])
13807
a28a8fbc76d4 changed ** to ## to avoid conflict with new comment syntax
paulson
parents: 13692
diff changeset
   573
  --{*Convert @{text "\<exists>y\<in>Lset(i)"} to @{text "\<exists>y[##Lset(i)]"} within the body
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   574
       of the @{term is_wfrec} application. *}
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   575
apply (intro FOL_reflections function_reflections 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   576
          is_wfrec_reflection Replace_reflection DPow'_reflection) 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   577
done
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   578
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   579
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   580
lemma transrec_rep: 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   581
    "[|L(j)|]
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   582
    ==> transrec_replacement(L, \<lambda>x f u. 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   583
              \<exists>r[L]. is_Replace(L, x, transrec_body(L,f,x), r) & 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   584
                     big_union(L, r, u), j)"
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   585
apply (rule transrec_replacementI, assumption)
13566
52a419210d5c Streamlined proofs of instances of Separation
paulson
parents: 13505
diff changeset
   586
apply (unfold transrec_body_def)  
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   587
apply (rule strong_replacementI)
13566
52a419210d5c Streamlined proofs of instances of Separation
paulson
parents: 13505
diff changeset
   588
apply (rule_tac u="{j,B,Memrel(eclose({j}))}" 
13687
22dce9134953 simpler separation/replacement proofs
paulson
parents: 13655
diff changeset
   589
         in gen_separation_multi [OF transrec_rep_Reflects], auto)
22dce9134953 simpler separation/replacement proofs
paulson
parents: 13655
diff changeset
   590
apply (rule_tac env="[j,B,Memrel(eclose({j}))]" in DPow_LsetI)
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   591
apply (rule sep_rules is_wfrec_iff_sats Replace_iff_sats DPow'_iff_sats | 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   592
       simp)+
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   593
done
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   594
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   595
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   596
subsubsection{*Actually Instantiating @{text M_Lset}*}
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   597
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   598
lemma M_Lset_axioms_L: "M_Lset_axioms(L)"
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   599
  apply (rule M_Lset_axioms.intro)
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   600
       apply (assumption | rule strong_rep transrec_rep)+
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   601
  done
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   602
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   603
theorem M_Lset_L: "PROP M_Lset(L)"
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 16417
diff changeset
   604
  apply (rule M_Lset.intro) 
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 16417
diff changeset
   605
   apply (rule M_DPow_L)
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 16417
diff changeset
   606
  apply (rule M_Lset_axioms_L) 
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 16417
diff changeset
   607
  done
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   608
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   609
text{*Finally: the point of the whole theory!*}
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   610
lemmas Lset_closed = M_Lset.Lset_closed [OF M_Lset_L]
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   611
   and Lset_abs = M_Lset.Lset_abs [OF M_Lset_L]
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   612
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   613
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   614
subsection{*The Notion of Constructible Set*}
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   615
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 19931
diff changeset
   616
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   617
  constructible :: "[i=>o,i] => o" where
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   618
    "constructible(M,x) ==
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   619
       \<exists>i[M]. \<exists>Li[M]. ordinal(M,i) & is_Lset(M,i,Li) & x \<in> Li"
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   620
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   621
theorem V_equals_L_in_L:
47072
777549486d44 refinements to constructibility
paulson
parents: 46823
diff changeset
   622
  "L(x) \<longleftrightarrow> constructible(L,x)"
777549486d44 refinements to constructibility
paulson
parents: 46823
diff changeset
   623
apply (simp add: constructible_def Lset_abs Lset_closed)
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   624
apply (simp add: L_def)
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   625
apply (blast intro: Ord_in_L) 
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   626
done
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13504
diff changeset
   627
13503
d93f41fe35d2 Relativization and absoluteness for DPow!!
paulson
parents:
diff changeset
   628
end