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