src/ZF/Constructible/Relative.thy
author wenzelm
Mon, 23 Mar 2015 21:05:17 +0100
changeset 59788 6f7b6adac439
parent 58871 c399ae4b836f
child 60770 240563fbf41d
permissions -rw-r--r--
prefer local fixes;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
     1
(*  Title:      ZF/Constructible/Relative.thy
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
     3
*)
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
     4
58871
c399ae4b836f modernized header;
wenzelm
parents: 58860
diff changeset
     5
section {*Relativization and Absoluteness*}
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
     6
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 13702
diff changeset
     7
theory Relative imports Main begin
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
     8
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
     9
subsection{* Relativized versions of standard set-theoretic concepts *}
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    10
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 16417
diff changeset
    11
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    12
  empty :: "[i=>o,i] => o" where
13254
5146ccaedf42 class quantifiers (some)
paulson
parents: 13251
diff changeset
    13
    "empty(M,z) == \<forall>x[M]. x \<notin> z"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    14
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    15
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    16
  subset :: "[i=>o,i,i] => o" where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    17
    "subset(M,A,B) == \<forall>x[M]. x\<in>A \<longrightarrow> x \<in> B"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    18
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
  upair :: "[i=>o,i,i,i] => o" where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    21
    "upair(M,a,b,z) == a \<in> z & b \<in> z & (\<forall>x[M]. x\<in>z \<longrightarrow> x = a | x = b)"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    22
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    23
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    24
  pair :: "[i=>o,i,i,i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
    25
    "pair(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) &
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    26
                     (\<exists>y[M]. upair(M,a,b,y) & upair(M,x,y,z))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    27
13306
6eebcddee32b more internalized formulas and separation proofs
paulson
parents: 13299
diff changeset
    28
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    29
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    30
  union :: "[i=>o,i,i,i] => o" where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    31
    "union(M,a,b,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> x \<in> a | x \<in> b"
13245
714f7a423a15 development and tweaks
paulson
parents: 13223
diff changeset
    32
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    33
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    34
  is_cons :: "[i=>o,i,i,i] => o" where
13306
6eebcddee32b more internalized formulas and separation proofs
paulson
parents: 13299
diff changeset
    35
    "is_cons(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) & union(M,x,b,z)"
6eebcddee32b more internalized formulas and separation proofs
paulson
parents: 13299
diff changeset
    36
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    37
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    38
  successor :: "[i=>o,i,i] => o" where
13306
6eebcddee32b more internalized formulas and separation proofs
paulson
parents: 13299
diff changeset
    39
    "successor(M,a,z) == is_cons(M,a,a,z)"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    40
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    41
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    42
  number1 :: "[i=>o,i] => o" where
13436
8fd1d803a3d3 tweaks involving Separation
paulson
parents: 13434
diff changeset
    43
    "number1(M,a) == \<exists>x[M]. empty(M,x) & successor(M,x,a)"
13363
c26eeb000470 instantiation of locales M_trancl and M_wfrank;
paulson
parents: 13353
diff changeset
    44
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    45
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    46
  number2 :: "[i=>o,i] => o" where
13436
8fd1d803a3d3 tweaks involving Separation
paulson
parents: 13434
diff changeset
    47
    "number2(M,a) == \<exists>x[M]. number1(M,x) & successor(M,x,a)"
13363
c26eeb000470 instantiation of locales M_trancl and M_wfrank;
paulson
parents: 13353
diff changeset
    48
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    49
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    50
  number3 :: "[i=>o,i] => o" where
13436
8fd1d803a3d3 tweaks involving Separation
paulson
parents: 13434
diff changeset
    51
    "number3(M,a) == \<exists>x[M]. number2(M,x) & successor(M,x,a)"
13363
c26eeb000470 instantiation of locales M_trancl and M_wfrank;
paulson
parents: 13353
diff changeset
    52
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    53
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    54
  powerset :: "[i=>o,i,i] => o" where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    55
    "powerset(M,A,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> subset(M,x,A)"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    56
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    57
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    58
  is_Collect :: "[i=>o,i,i=>o,i] => o" where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    59
    "is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> x \<in> A & P(x)"
13436
8fd1d803a3d3 tweaks involving Separation
paulson
parents: 13434
diff changeset
    60
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    61
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    62
  is_Replace :: "[i=>o,i,[i,i]=>o,i] => o" where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    63
    "is_Replace(M,A,P,z) == \<forall>u[M]. u \<in> z \<longleftrightarrow> (\<exists>x[M]. x\<in>A & P(x,u))"
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
    64
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    65
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    66
  inter :: "[i=>o,i,i,i] => o" where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    67
    "inter(M,a,b,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> x \<in> a & x \<in> b"
13223
45be08fbdcff new theory of inner models
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
  setdiff :: "[i=>o,i,i,i] => o" where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    71
    "setdiff(M,a,b,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> x \<in> a & x \<notin> b"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    72
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    73
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    74
  big_union :: "[i=>o,i,i] => o" where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    75
    "big_union(M,A,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> (\<exists>y[M]. y\<in>A & x \<in> y)"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    76
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    77
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    78
  big_inter :: "[i=>o,i,i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
    79
    "big_inter(M,A,z) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    80
             (A=0 \<longrightarrow> z=0) &
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    81
             (A\<noteq>0 \<longrightarrow> (\<forall>x[M]. x \<in> z \<longleftrightarrow> (\<forall>y[M]. y\<in>A \<longrightarrow> x \<in> y)))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    82
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    83
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    84
  cartprod :: "[i=>o,i,i,i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
    85
    "cartprod(M,A,B,z) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
    86
        \<forall>u[M]. u \<in> z \<longleftrightarrow> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
    87
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    88
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    89
  is_sum :: "[i=>o,i,i,i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
    90
    "is_sum(M,A,B,Z) ==
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
    91
       \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M].
13350
paulson
parents: 13348
diff changeset
    92
       number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &
paulson
parents: 13348
diff changeset
    93
       cartprod(M,s1,B,B1) & union(M,A0,B1,Z)"
paulson
parents: 13348
diff changeset
    94
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    95
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    96
  is_Inl :: "[i=>o,i,i] => o" where
13397
6e5f4d911435 Absoluteness of the function "nth"
paulson
parents: 13382
diff changeset
    97
    "is_Inl(M,a,z) == \<exists>zero[M]. empty(M,zero) & pair(M,zero,a,z)"
6e5f4d911435 Absoluteness of the function "nth"
paulson
parents: 13382
diff changeset
    98
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
    99
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   100
  is_Inr :: "[i=>o,i,i] => o" where
13397
6e5f4d911435 Absoluteness of the function "nth"
paulson
parents: 13382
diff changeset
   101
    "is_Inr(M,a,z) == \<exists>n1[M]. number1(M,n1) & pair(M,n1,a,z)"
6e5f4d911435 Absoluteness of the function "nth"
paulson
parents: 13382
diff changeset
   102
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   103
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   104
  is_converse :: "[i=>o,i,i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   105
    "is_converse(M,r,z) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   106
        \<forall>x[M]. x \<in> z \<longleftrightarrow>
13299
3a932abf97e8 More use of relativized quantifiers
paulson
parents: 13298
diff changeset
   107
             (\<exists>w[M]. w\<in>r & (\<exists>u[M]. \<exists>v[M]. pair(M,u,v,w) & pair(M,v,u,x)))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   108
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   109
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   110
  pre_image :: "[i=>o,i,i,i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   111
    "pre_image(M,r,A,z) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   112
        \<forall>x[M]. x \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   113
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   114
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   115
  is_domain :: "[i=>o,i,i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   116
    "is_domain(M,r,z) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   117
        \<forall>x[M]. x \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w)))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   118
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   119
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   120
  image :: "[i=>o,i,i,i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   121
    "image(M,r,A,z) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   122
        \<forall>y[M]. y \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w)))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   123
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   124
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   125
  is_range :: "[i=>o,i,i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   126
    --{*the cleaner
13299
3a932abf97e8 More use of relativized quantifiers
paulson
parents: 13298
diff changeset
   127
      @{term "\<exists>r'[M]. is_converse(M,r,r') & is_domain(M,r',z)"}
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   128
      unfortunately needs an instance of separation in order to prove
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   129
        @{term "M(converse(r))"}.*}
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   130
    "is_range(M,r,z) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   131
        \<forall>y[M]. y \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w)))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   132
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   133
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   134
  is_field :: "[i=>o,i,i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   135
    "is_field(M,r,z) ==
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 22710
diff changeset
   136
        \<exists>dr[M]. \<exists>rr[M]. is_domain(M,r,dr) & is_range(M,r,rr) &
13436
8fd1d803a3d3 tweaks involving Separation
paulson
parents: 13434
diff changeset
   137
                        union(M,dr,rr,z)"
13245
714f7a423a15 development and tweaks
paulson
parents: 13223
diff changeset
   138
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   139
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   140
  is_relation :: "[i=>o,i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   141
    "is_relation(M,r) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   142
        (\<forall>z[M]. z\<in>r \<longrightarrow> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   143
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   144
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   145
  is_function :: "[i=>o,i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   146
    "is_function(M,r) ==
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 22710
diff changeset
   147
        \<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M].
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   148
           pair(M,x,y,p) \<longrightarrow> pair(M,x,y',p') \<longrightarrow> p\<in>r \<longrightarrow> p'\<in>r \<longrightarrow> y=y'"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   149
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   150
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   151
  fun_apply :: "[i=>o,i,i,i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   152
    "fun_apply(M,f,x,y) ==
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   153
        (\<exists>xs[M]. \<exists>fxs[M].
13352
3cd767f8d78b new definitions of fun_apply and M_is_recfun
paulson
parents: 13350
diff changeset
   154
         upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   155
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   156
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   157
  typed_function :: "[i=>o,i,i,i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   158
    "typed_function(M,A,B,r) ==
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   159
        is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   160
        (\<forall>u[M]. u\<in>r \<longrightarrow> (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) \<longrightarrow> y\<in>B))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   161
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   162
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   163
  is_funspace :: "[i=>o,i,i,i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   164
    "is_funspace(M,A,B,F) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   165
        \<forall>f[M]. f \<in> F \<longleftrightarrow> typed_function(M,A,B,f)"
13268
240509babf00 more use of relativized quantifiers
paulson
parents: 13254
diff changeset
   166
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   167
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   168
  composition :: "[i=>o,i,i,i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   169
    "composition(M,r,s,t) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   170
        \<forall>p[M]. p \<in> t \<longleftrightarrow>
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   171
               (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M].
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   172
                pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) &
13323
2c287f50c9f3 More relativization, reflection and proofs of separation
paulson
parents: 13319
diff changeset
   173
                xy \<in> s & yz \<in> r)"
13245
714f7a423a15 development and tweaks
paulson
parents: 13223
diff changeset
   174
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   175
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   176
  injection :: "[i=>o,i,i,i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   177
    "injection(M,A,B,f) ==
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 22710
diff changeset
   178
        typed_function(M,A,B,f) &
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   179
        (\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M].
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   180
          pair(M,x,y,p) \<longrightarrow> pair(M,x',y,p') \<longrightarrow> p\<in>f \<longrightarrow> p'\<in>f \<longrightarrow> x=x')"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   181
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   182
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   183
  surjection :: "[i=>o,i,i,i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   184
    "surjection(M,A,B,f) ==
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   185
        typed_function(M,A,B,f) &
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   186
        (\<forall>y[M]. y\<in>B \<longrightarrow> (\<exists>x[M]. x\<in>A & fun_apply(M,f,x,y)))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   187
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   188
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   189
  bijection :: "[i=>o,i,i,i] => o" where
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   190
    "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)"
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   191
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   192
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   193
  restriction :: "[i=>o,i,i,i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   194
    "restriction(M,r,A,z) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   195
        \<forall>x[M]. x \<in> z \<longleftrightarrow> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x))))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   196
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   197
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   198
  transitive_set :: "[i=>o,i] => o" where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   199
    "transitive_set(M,a) == \<forall>x[M]. x\<in>a \<longrightarrow> subset(M,x,a)"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   200
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   201
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   202
  ordinal :: "[i=>o,i] => o" where
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   203
     --{*an ordinal is a transitive set of transitive sets*}
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   204
    "ordinal(M,a) == transitive_set(M,a) & (\<forall>x[M]. x\<in>a \<longrightarrow> transitive_set(M,x))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   205
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   206
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   207
  limit_ordinal :: "[i=>o,i] => o" where
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   208
    --{*a limit ordinal is a non-empty, successor-closed ordinal*}
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   209
    "limit_ordinal(M,a) ==
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 22710
diff changeset
   210
        ordinal(M,a) & ~ empty(M,a) &
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   211
        (\<forall>x[M]. x\<in>a \<longrightarrow> (\<exists>y[M]. y\<in>a & successor(M,x,y)))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   212
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   213
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   214
  successor_ordinal :: "[i=>o,i] => o" where
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   215
    --{*a successor ordinal is any ordinal that is neither empty nor limit*}
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   216
    "successor_ordinal(M,a) ==
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 22710
diff changeset
   217
        ordinal(M,a) & ~ empty(M,a) & ~ limit_ordinal(M,a)"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   218
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   219
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   220
  finite_ordinal :: "[i=>o,i] => o" where
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   221
    --{*an ordinal is finite if neither it nor any of its elements are limit*}
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   222
    "finite_ordinal(M,a) ==
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 22710
diff changeset
   223
        ordinal(M,a) & ~ limit_ordinal(M,a) &
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   224
        (\<forall>x[M]. x\<in>a \<longrightarrow> ~ limit_ordinal(M,x))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   225
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   226
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   227
  omega :: "[i=>o,i] => o" where
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   228
    --{*omega is a limit ordinal none of whose elements are limit*}
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   229
    "omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a \<longrightarrow> ~ limit_ordinal(M,x))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   230
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   231
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   232
  is_quasinat :: "[i=>o,i] => o" where
13350
paulson
parents: 13348
diff changeset
   233
    "is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))"
paulson
parents: 13348
diff changeset
   234
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   235
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   236
  is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   237
    "is_nat_case(M, a, is_b, k, z) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   238
       (empty(M,k) \<longrightarrow> z=a) &
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   239
       (\<forall>m[M]. successor(M,m,k) \<longrightarrow> is_b(m,z)) &
13363
c26eeb000470 instantiation of locales M_trancl and M_wfrank;
paulson
parents: 13353
diff changeset
   240
       (is_quasinat(M,k) | empty(M,z))"
13350
paulson
parents: 13348
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
  relation1 :: "[i=>o, [i,i]=>o, i=>i] => o" where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   244
    "relation1(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. is_f(x,y) \<longleftrightarrow> y = f(x)"
13353
1800e7134d2e towards relativization of "iterates" and "wfrec"
paulson
parents: 13352
diff changeset
   245
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   246
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   247
  Relation1 :: "[i=>o, i, [i,i]=>o, i=>i] => o" where
13423
7ec771711c09 More lemmas, working towards relativization of "satisfies"
paulson
parents: 13418
diff changeset
   248
    --{*as above, but typed*}
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13628
diff changeset
   249
    "Relation1(M,A,is_f,f) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   250
        \<forall>x[M]. \<forall>y[M]. x\<in>A \<longrightarrow> is_f(x,y) \<longleftrightarrow> y = f(x)"
13423
7ec771711c09 More lemmas, working towards relativization of "satisfies"
paulson
parents: 13418
diff changeset
   251
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   252
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   253
  relation2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o" where
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   254
    "relation2(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. is_f(x,y,z) \<longleftrightarrow> z = f(x,y)"
13353
1800e7134d2e towards relativization of "iterates" and "wfrec"
paulson
parents: 13352
diff changeset
   255
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   256
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   257
  Relation2 :: "[i=>o, i, i, [i,i,i]=>o, [i,i]=>i] => o" where
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13628
diff changeset
   258
    "Relation2(M,A,B,is_f,f) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   259
        \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. x\<in>A \<longrightarrow> y\<in>B \<longrightarrow> is_f(x,y,z) \<longleftrightarrow> z = f(x,y)"
13423
7ec771711c09 More lemmas, working towards relativization of "satisfies"
paulson
parents: 13418
diff changeset
   260
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   261
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   262
  relation3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o" where
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13628
diff changeset
   263
    "relation3(M,is_f,f) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   264
       \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M]. is_f(x,y,z,u) \<longleftrightarrow> u = f(x,y,z)"
13353
1800e7134d2e towards relativization of "iterates" and "wfrec"
paulson
parents: 13352
diff changeset
   265
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   266
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   267
  Relation3 :: "[i=>o, i, i, i, [i,i,i,i]=>o, [i,i,i]=>i] => o" where
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13628
diff changeset
   268
    "Relation3(M,A,B,C,is_f,f) ==
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   269
       \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M].
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   270
         x\<in>A \<longrightarrow> y\<in>B \<longrightarrow> z\<in>C \<longrightarrow> is_f(x,y,z,u) \<longleftrightarrow> u = f(x,y,z)"
13423
7ec771711c09 More lemmas, working towards relativization of "satisfies"
paulson
parents: 13418
diff changeset
   271
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   272
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   273
  relation4 :: "[i=>o, [i,i,i,i,i]=>o, [i,i,i,i]=>i] => o" where
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13628
diff changeset
   274
    "relation4(M,is_f,f) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   275
       \<forall>u[M]. \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>a[M]. is_f(u,x,y,z,a) \<longleftrightarrow> a = f(u,x,y,z)"
13423
7ec771711c09 More lemmas, working towards relativization of "satisfies"
paulson
parents: 13418
diff changeset
   276
7ec771711c09 More lemmas, working towards relativization of "satisfies"
paulson
parents: 13418
diff changeset
   277
7ec771711c09 More lemmas, working towards relativization of "satisfies"
paulson
parents: 13418
diff changeset
   278
text{*Useful when absoluteness reasoning has replaced the predicates by terms*}
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13628
diff changeset
   279
lemma triv_Relation1:
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13628
diff changeset
   280
     "Relation1(M, A, \<lambda>x y. y = f(x), f)"
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13628
diff changeset
   281
by (simp add: Relation1_def)
13423
7ec771711c09 More lemmas, working towards relativization of "satisfies"
paulson
parents: 13418
diff changeset
   282
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13628
diff changeset
   283
lemma triv_Relation2:
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13628
diff changeset
   284
     "Relation2(M, A, B, \<lambda>x y a. a = f(x,y), f)"
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13628
diff changeset
   285
by (simp add: Relation2_def)
13423
7ec771711c09 More lemmas, working towards relativization of "satisfies"
paulson
parents: 13418
diff changeset
   286
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   287
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   288
subsection {*The relativized ZF axioms*}
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   289
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 16417
diff changeset
   290
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   291
  extensionality :: "(i=>o) => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   292
    "extensionality(M) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   293
        \<forall>x[M]. \<forall>y[M]. (\<forall>z[M]. z \<in> x \<longleftrightarrow> z \<in> y) \<longrightarrow> x=y"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   294
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   295
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   296
  separation :: "[i=>o, i=>o] => o" where
13563
paulson
parents: 13543
diff changeset
   297
    --{*The formula @{text P} should only involve parameters
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   298
        belonging to @{text M} and all its quantifiers must be relativized
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   299
        to @{text M}.  We do not have separation as a scheme; every instance
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   300
        that we need must be assumed (and later proved) separately.*}
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   301
    "separation(M,P) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   302
        \<forall>z[M]. \<exists>y[M]. \<forall>x[M]. x \<in> y \<longleftrightarrow> x \<in> z & P(x)"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   303
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   304
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   305
  upair_ax :: "(i=>o) => o" where
13563
paulson
parents: 13543
diff changeset
   306
    "upair_ax(M) == \<forall>x[M]. \<forall>y[M]. \<exists>z[M]. upair(M,x,y,z)"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   307
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   308
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   309
  Union_ax :: "(i=>o) => o" where
13514
cc3bbaf1b8d3 tweaked
paulson
parents: 13505
diff changeset
   310
    "Union_ax(M) == \<forall>x[M]. \<exists>z[M]. big_union(M,x,z)"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   311
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   312
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   313
  power_ax :: "(i=>o) => o" where
13514
cc3bbaf1b8d3 tweaked
paulson
parents: 13505
diff changeset
   314
    "power_ax(M) == \<forall>x[M]. \<exists>z[M]. powerset(M,x,z)"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   315
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   316
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   317
  univalent :: "[i=>o, i, [i,i]=>o] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   318
    "univalent(M,A,P) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   319
        \<forall>x[M]. x\<in>A \<longrightarrow> (\<forall>y[M]. \<forall>z[M]. P(x,y) & P(x,z) \<longrightarrow> y=z)"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   320
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   321
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   322
  replacement :: "[i=>o, [i,i]=>o] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   323
    "replacement(M,P) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   324
      \<forall>A[M]. univalent(M,A,P) \<longrightarrow>
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   325
      (\<exists>Y[M]. \<forall>b[M]. (\<exists>x[M]. x\<in>A & P(x,b)) \<longrightarrow> b \<in> Y)"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   326
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   327
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   328
  strong_replacement :: "[i=>o, [i,i]=>o] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   329
    "strong_replacement(M,P) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   330
      \<forall>A[M]. univalent(M,A,P) \<longrightarrow>
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   331
      (\<exists>Y[M]. \<forall>b[M]. b \<in> Y \<longleftrightarrow> (\<exists>x[M]. x\<in>A & P(x,b)))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   332
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   333
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   334
  foundation_ax :: "(i=>o) => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   335
    "foundation_ax(M) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   336
        \<forall>x[M]. (\<exists>y[M]. y\<in>x) \<longrightarrow> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & z \<in> y))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   337
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   338
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   339
subsection{*A trivial consistency proof for $V_\omega$ *}
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   340
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   341
text{*We prove that $V_\omega$
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   342
      (or @{text univ} in Isabelle) satisfies some ZF axioms.
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   343
     Kunen, Theorem IV 3.13, page 123.*}
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   344
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   345
lemma univ0_downwards_mem: "[| y \<in> x; x \<in> univ(0) |] ==> y \<in> univ(0)"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   346
apply (insert Transset_univ [OF Transset_0])
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   347
apply (simp add: Transset_def, blast)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   348
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   349
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   350
lemma univ0_Ball_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   351
     "A \<in> univ(0) ==> (\<forall>x\<in>A. x \<in> univ(0) \<longrightarrow> P(x)) \<longleftrightarrow> (\<forall>x\<in>A. P(x))"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   352
by (blast intro: univ0_downwards_mem)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   353
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   354
lemma univ0_Bex_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   355
     "A \<in> univ(0) ==> (\<exists>x\<in>A. x \<in> univ(0) & P(x)) \<longleftrightarrow> (\<exists>x\<in>A. P(x))"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   356
by (blast intro: univ0_downwards_mem)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   357
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   358
text{*Congruence rule for separation: can assume the variable is in @{text M}*}
13254
5146ccaedf42 class quantifiers (some)
paulson
parents: 13251
diff changeset
   359
lemma separation_cong [cong]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   360
     "(!!x. M(x) ==> P(x) \<longleftrightarrow> P'(x))
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   361
      ==> separation(M, %x. P(x)) \<longleftrightarrow> separation(M, %x. P'(x))"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   362
by (simp add: separation_def)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   363
13254
5146ccaedf42 class quantifiers (some)
paulson
parents: 13251
diff changeset
   364
lemma univalent_cong [cong]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   365
     "[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) \<longleftrightarrow> P'(x,y) |]
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   366
      ==> univalent(M, A, %x y. P(x,y)) \<longleftrightarrow> univalent(M, A', %x y. P'(x,y))"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   367
by (simp add: univalent_def)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   368
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
   369
lemma univalent_triv [intro,simp]:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
   370
     "univalent(M, A, \<lambda>x y. y = f(x))"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   371
by (simp add: univalent_def)
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
   372
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
   373
lemma univalent_conjI2 [intro,simp]:
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
   374
     "univalent(M,A,Q) ==> univalent(M, A, \<lambda>x y. P(x,y) & Q(x,y))"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   375
by (simp add: univalent_def, blast)
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
   376
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
   377
text{*Congruence rule for replacement*}
13254
5146ccaedf42 class quantifiers (some)
paulson
parents: 13251
diff changeset
   378
lemma strong_replacement_cong [cong]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   379
     "[| !!x y. [| M(x); M(y) |] ==> P(x,y) \<longleftrightarrow> P'(x,y) |]
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   380
      ==> strong_replacement(M, %x y. P(x,y)) \<longleftrightarrow>
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   381
          strong_replacement(M, %x y. P'(x,y))"
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   382
by (simp add: strong_replacement_def)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   383
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   384
text{*The extensionality axiom*}
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   385
lemma "extensionality(\<lambda>x. x \<in> univ(0))"
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   386
apply (simp add: extensionality_def)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   387
apply (blast intro: univ0_downwards_mem)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   388
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   389
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   390
text{*The separation axiom requires some lemmas*}
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   391
lemma Collect_in_Vfrom:
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   392
     "[| X \<in> Vfrom(A,j);  Transset(A) |] ==> Collect(X,P) \<in> Vfrom(A, succ(j))"
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   393
apply (drule Transset_Vfrom)
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   394
apply (rule subset_mem_Vfrom)
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   395
apply (unfold Transset_def, blast)
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   396
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   397
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   398
lemma Collect_in_VLimit:
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   399
     "[| X \<in> Vfrom(A,i);  Limit(i);  Transset(A) |]
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   400
      ==> Collect(X,P) \<in> Vfrom(A,i)"
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   401
apply (rule Limit_VfromE, assumption+)
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   402
apply (blast intro: Limit_has_succ VfromI Collect_in_Vfrom)
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   403
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   404
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   405
lemma Collect_in_univ:
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   406
     "[| X \<in> univ(A);  Transset(A) |] ==> Collect(X,P) \<in> univ(A)"
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   407
by (simp add: univ_def Collect_in_VLimit Limit_nat)
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   408
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   409
lemma "separation(\<lambda>x. x \<in> univ(0), P)"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   410
apply (simp add: separation_def, clarify)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   411
apply (rule_tac x = "Collect(z,P)" in bexI)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   412
apply (blast intro: Collect_in_univ Transset_0)+
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   413
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   414
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   415
text{*Unordered pairing axiom*}
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   416
lemma "upair_ax(\<lambda>x. x \<in> univ(0))"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   417
apply (simp add: upair_ax_def upair_def)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   418
apply (blast intro: doubleton_in_univ)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   419
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   420
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   421
text{*Union axiom*}
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   422
lemma "Union_ax(\<lambda>x. x \<in> univ(0))"
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   423
apply (simp add: Union_ax_def big_union_def, clarify)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   424
apply (rule_tac x="\<Union>x" in bexI)
13299
3a932abf97e8 More use of relativized quantifiers
paulson
parents: 13298
diff changeset
   425
 apply (blast intro: univ0_downwards_mem)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   426
apply (blast intro: Union_in_univ Transset_0)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   427
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   428
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   429
text{*Powerset axiom*}
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   430
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   431
lemma Pow_in_univ:
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   432
     "[| X \<in> univ(A);  Transset(A) |] ==> Pow(X) \<in> univ(A)"
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   433
apply (simp add: univ_def Pow_in_VLimit Limit_nat)
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   434
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   435
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   436
lemma "power_ax(\<lambda>x. x \<in> univ(0))"
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   437
apply (simp add: power_ax_def powerset_def subset_def, clarify)
13299
3a932abf97e8 More use of relativized quantifiers
paulson
parents: 13298
diff changeset
   438
apply (rule_tac x="Pow(x)" in bexI)
3a932abf97e8 More use of relativized quantifiers
paulson
parents: 13298
diff changeset
   439
 apply (blast intro: univ0_downwards_mem)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   440
apply (blast intro: Pow_in_univ Transset_0)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   441
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   442
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   443
text{*Foundation axiom*}
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   444
lemma "foundation_ax(\<lambda>x. x \<in> univ(0))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   445
apply (simp add: foundation_ax_def, clarify)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   446
apply (cut_tac A=x in foundation)
13299
3a932abf97e8 More use of relativized quantifiers
paulson
parents: 13298
diff changeset
   447
apply (blast intro: univ0_downwards_mem)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   448
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   449
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   450
lemma "replacement(\<lambda>x. x \<in> univ(0), P)"
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   451
apply (simp add: replacement_def, clarify)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   452
oops
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   453
text{*no idea: maybe prove by induction on the rank of A?*}
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   454
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   455
text{*Still missing: Replacement, Choice*}
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   456
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   457
subsection{*Lemmas Needed to Reduce Some Set Constructions to Instances
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   458
      of Separation*}
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   459
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   460
lemma image_iff_Collect: "r `` A = {y \<in> \<Union>(\<Union>(r)). \<exists>p\<in>r. \<exists>x\<in>A. p=<x,y>}"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   461
apply (rule equalityI, auto)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   462
apply (simp add: Pair_def, blast)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   463
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   464
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   465
lemma vimage_iff_Collect:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   466
     "r -`` A = {x \<in> \<Union>(\<Union>(r)). \<exists>p\<in>r. \<exists>y\<in>A. p=<x,y>}"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   467
apply (rule equalityI, auto)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   468
apply (simp add: Pair_def, blast)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   469
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   470
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   471
text{*These two lemmas lets us prove @{text domain_closed} and
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   472
      @{text range_closed} without new instances of separation*}
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   473
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   474
lemma domain_eq_vimage: "domain(r) = r -`` Union(Union(r))"
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   475
apply (rule equalityI, auto)
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   476
apply (rule vimageI, assumption)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   477
apply (simp add: Pair_def, blast)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   478
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   479
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   480
lemma range_eq_image: "range(r) = r `` Union(Union(r))"
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   481
apply (rule equalityI, auto)
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   482
apply (rule imageI, assumption)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   483
apply (simp add: Pair_def, blast)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   484
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   485
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   486
lemma replacementD:
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   487
    "[| replacement(M,P); M(A);  univalent(M,A,P) |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   488
     ==> \<exists>Y[M]. (\<forall>b[M]. ((\<exists>x[M]. x\<in>A & P(x,b)) \<longrightarrow> b \<in> Y))"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   489
by (simp add: replacement_def)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   490
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   491
lemma strong_replacementD:
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   492
    "[| strong_replacement(M,P); M(A);  univalent(M,A,P) |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   493
     ==> \<exists>Y[M]. (\<forall>b[M]. (b \<in> Y \<longleftrightarrow> (\<exists>x[M]. x\<in>A & P(x,b))))"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   494
by (simp add: strong_replacement_def)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   495
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   496
lemma separationD:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   497
    "[| separation(M,P); M(z) |] ==> \<exists>y[M]. \<forall>x[M]. x \<in> y \<longleftrightarrow> x \<in> z & P(x)"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   498
by (simp add: separation_def)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   499
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   500
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   501
text{*More constants, for order types*}
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   502
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 16417
diff changeset
   503
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   504
  order_isomorphism :: "[i=>o,i,i,i,i,i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   505
    "order_isomorphism(M,A,r,B,s,f) ==
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   506
        bijection(M,A,B,f) &
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   507
        (\<forall>x[M]. x\<in>A \<longrightarrow> (\<forall>y[M]. y\<in>A \<longrightarrow>
13306
6eebcddee32b more internalized formulas and separation proofs
paulson
parents: 13299
diff changeset
   508
          (\<forall>p[M]. \<forall>fx[M]. \<forall>fy[M]. \<forall>q[M].
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   509
            pair(M,x,y,p) \<longrightarrow> fun_apply(M,f,x,fx) \<longrightarrow> fun_apply(M,f,y,fy) \<longrightarrow>
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   510
            pair(M,fx,fy,q) \<longrightarrow> (p\<in>r \<longleftrightarrow> q\<in>s))))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   511
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   512
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   513
  pred_set :: "[i=>o,i,i,i,i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   514
    "pred_set(M,A,x,r,B) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   515
        \<forall>y[M]. y \<in> B \<longleftrightarrow> (\<exists>p[M]. p\<in>r & y \<in> A & pair(M,y,x,p))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   516
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
  membership :: "[i=>o,i,i] => o" where --{*membership relation*}
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   519
    "membership(M,A,r) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   520
        \<forall>p[M]. p \<in> r \<longleftrightarrow> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>A & x\<in>y & pair(M,x,y,p)))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   521
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   522
13418
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   523
subsection{*Introducing a Transitive Class Model*}
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   524
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   525
text{*The class M is assumed to be transitive and to satisfy some
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   526
      relativized ZF axioms*}
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
   527
locale M_trivial =
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   528
  fixes M
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   529
  assumes transM:           "[| y\<in>x; M(x) |] ==> M(y)"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 22710
diff changeset
   530
      and upair_ax:         "upair_ax(M)"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 22710
diff changeset
   531
      and Union_ax:         "Union_ax(M)"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   532
      and power_ax:         "power_ax(M)"
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   533
      and replacement:      "replacement(M,P)"
13268
240509babf00 more use of relativized quantifiers
paulson
parents: 13254
diff changeset
   534
      and M_nat [iff]:      "M(nat)"           (*i.e. the axiom of infinity*)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   535
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   536
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   537
text{*Automatically discovers the proof using @{text transM}, @{text nat_0I}
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   538
and @{text M_nat}.*}
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   539
lemma (in M_trivial) nonempty [simp]: "M(0)"
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   540
by (blast intro: transM)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   541
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   542
lemma (in M_trivial) rall_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   543
     "M(A) ==> (\<forall>x[M]. x\<in>A \<longrightarrow> P(x)) \<longleftrightarrow> (\<forall>x\<in>A. P(x))"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   544
by (blast intro: transM)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   545
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   546
lemma (in M_trivial) rex_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   547
     "M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) \<longleftrightarrow> (\<exists>x\<in>A. P(x))"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   548
by (blast intro: transM)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   549
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   550
lemma (in M_trivial) ball_iff_equiv:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   551
     "M(A) ==> (\<forall>x[M]. (x\<in>A \<longleftrightarrow> P(x))) \<longleftrightarrow>
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   552
               (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) \<longrightarrow> M(x) \<longrightarrow> x\<in>A)"
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   553
by (blast intro: transM)
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   554
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   555
text{*Simplifies proofs of equalities when there's an iff-equality
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   556
      available for rewriting, universally quantified over M.
13702
c7cf8fa66534 Polishing.
paulson
parents: 13687
diff changeset
   557
      But it's not the only way to prove such equalities: its
c7cf8fa66534 Polishing.
paulson
parents: 13687
diff changeset
   558
      premises @{term "M(A)"} and  @{term "M(B)"} can be too strong.*}
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   559
lemma (in M_trivial) M_equalityI:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   560
     "[| !!x. M(x) ==> x\<in>A \<longleftrightarrow> x\<in>B; M(A); M(B) |] ==> A=B"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   561
by (blast intro!: equalityI dest: transM)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   562
13418
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   563
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   564
subsubsection{*Trivial Absoluteness Proofs: Empty Set, Pairs, etc.*}
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   565
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   566
lemma (in M_trivial) empty_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   567
     "M(z) ==> empty(M,z) \<longleftrightarrow> z=0"
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   568
apply (simp add: empty_def)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   569
apply (blast intro: transM)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   570
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   571
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   572
lemma (in M_trivial) subset_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   573
     "M(A) ==> subset(M,A,B) \<longleftrightarrow> A \<subseteq> B"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   574
apply (simp add: subset_def)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   575
apply (blast intro: transM)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   576
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   577
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   578
lemma (in M_trivial) upair_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   579
     "M(z) ==> upair(M,a,b,z) \<longleftrightarrow> z={a,b}"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   580
apply (simp add: upair_def)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   581
apply (blast intro: transM)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   582
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   583
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
   584
lemma (in M_trivial) upair_in_M_iff [iff]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   585
     "M({a,b}) \<longleftrightarrow> M(a) & M(b)"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   586
apply (insert upair_ax, simp add: upair_ax_def)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   587
apply (blast intro: transM)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   588
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   589
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
   590
lemma (in M_trivial) singleton_in_M_iff [iff]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   591
     "M({a}) \<longleftrightarrow> M(a)"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   592
by (insert upair_in_M_iff [of a a], simp)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   593
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   594
lemma (in M_trivial) pair_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   595
     "M(z) ==> pair(M,a,b,z) \<longleftrightarrow> z=<a,b>"
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   596
apply (simp add: pair_def ZF.Pair_def)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   597
apply (blast intro: transM)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   598
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   599
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
   600
lemma (in M_trivial) pair_in_M_iff [iff]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   601
     "M(<a,b>) \<longleftrightarrow> M(a) & M(b)"
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   602
by (simp add: ZF.Pair_def)
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   603
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
   604
lemma (in M_trivial) pair_components_in_M:
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   605
     "[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   606
apply (simp add: Pair_def)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   607
apply (blast dest: transM)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   608
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   609
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   610
lemma (in M_trivial) cartprod_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   611
     "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) \<longleftrightarrow> z = A*B"
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   612
apply (simp add: cartprod_def)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   613
apply (rule iffI)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   614
 apply (blast intro!: equalityI intro: transM dest!: rspec)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   615
apply (blast dest: transM)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   616
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   617
13418
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   618
subsubsection{*Absoluteness for Unions and Intersections*}
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   619
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   620
lemma (in M_trivial) union_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   621
     "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) \<longleftrightarrow> z = a \<union> b"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   622
apply (simp add: union_def)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   623
apply (blast intro: transM)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   624
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   625
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   626
lemma (in M_trivial) inter_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   627
     "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) \<longleftrightarrow> z = a \<inter> b"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   628
apply (simp add: inter_def)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   629
apply (blast intro: transM)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   630
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   631
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   632
lemma (in M_trivial) setdiff_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   633
     "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) \<longleftrightarrow> z = a-b"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   634
apply (simp add: setdiff_def)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   635
apply (blast intro: transM)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   636
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   637
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   638
lemma (in M_trivial) Union_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   639
     "[| M(A); M(z) |] ==> big_union(M,A,z) \<longleftrightarrow> z = \<Union>(A)"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   640
apply (simp add: big_union_def)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   641
apply (blast intro!: equalityI dest: transM)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   642
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   643
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
   644
lemma (in M_trivial) Union_closed [intro,simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   645
     "M(A) ==> M(\<Union>(A))"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   646
by (insert Union_ax, simp add: Union_ax_def)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   647
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
   648
lemma (in M_trivial) Un_closed [intro,simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   649
     "[| M(A); M(B) |] ==> M(A \<union> B)"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   650
by (simp only: Un_eq_Union, blast)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   651
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
   652
lemma (in M_trivial) cons_closed [intro,simp]:
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   653
     "[| M(a); M(A) |] ==> M(cons(a,A))"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   654
by (subst cons_eq [symmetric], blast)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   655
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   656
lemma (in M_trivial) cons_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   657
     "[| M(b); M(z) |] ==> is_cons(M,a,b,z) \<longleftrightarrow> z = cons(a,b)"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   658
by (simp add: is_cons_def, blast intro: transM)
13306
6eebcddee32b more internalized formulas and separation proofs
paulson
parents: 13299
diff changeset
   659
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   660
lemma (in M_trivial) successor_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   661
     "[| M(a); M(z) |] ==> successor(M,a,z) \<longleftrightarrow> z = succ(a)"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   662
by (simp add: successor_def, blast)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   663
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
   664
lemma (in M_trivial) succ_in_M_iff [iff]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   665
     "M(succ(a)) \<longleftrightarrow> M(a)"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   666
apply (simp add: succ_def)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   667
apply (blast intro: transM)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   668
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   669
13418
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   670
subsubsection{*Absoluteness for Separation and Replacement*}
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   671
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
   672
lemma (in M_trivial) separation_closed [intro,simp]:
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   673
     "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   674
apply (insert separation, simp add: separation_def)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   675
apply (drule rspec, assumption, clarify)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   676
apply (subgoal_tac "y = Collect(A,P)", blast)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   677
apply (blast dest: transM)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   678
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   679
13436
8fd1d803a3d3 tweaks involving Separation
paulson
parents: 13434
diff changeset
   680
lemma separation_iff:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   681
     "separation(M,P) \<longleftrightarrow> (\<forall>z[M]. \<exists>y[M]. is_Collect(M,z,P,y))"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   682
by (simp add: separation_def is_Collect_def)
13436
8fd1d803a3d3 tweaks involving Separation
paulson
parents: 13434
diff changeset
   683
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   684
lemma (in M_trivial) Collect_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   685
     "[| M(A); M(z) |] ==> is_Collect(M,A,P,z) \<longleftrightarrow> z = Collect(A,P)"
13436
8fd1d803a3d3 tweaks involving Separation
paulson
parents: 13434
diff changeset
   686
apply (simp add: is_Collect_def)
8fd1d803a3d3 tweaks involving Separation
paulson
parents: 13434
diff changeset
   687
apply (blast intro!: equalityI dest: transM)
8fd1d803a3d3 tweaks involving Separation
paulson
parents: 13434
diff changeset
   688
done
8fd1d803a3d3 tweaks involving Separation
paulson
parents: 13434
diff changeset
   689
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   690
text{*Probably the premise and conclusion are equivalent*}
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
   691
lemma (in M_trivial) strong_replacementI [rule_format]:
13687
22dce9134953 simpler separation/replacement proofs
paulson
parents: 13634
diff changeset
   692
    "[| \<forall>B[M]. separation(M, %u. \<exists>x[M]. x\<in>B & P(x,u)) |]
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   693
     ==> strong_replacement(M,P)"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   694
apply (simp add: strong_replacement_def, clarify)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   695
apply (frule replacementD [OF replacement], assumption, clarify)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   696
apply (drule_tac x=A in rspec, clarify)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   697
apply (drule_tac z=Y in separationD, assumption, clarify)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   698
apply (rule_tac x=y in rexI, force, assumption)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   699
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   700
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
   701
subsubsection{*The Operator @{term is_Replace}*}
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
   702
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
   703
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
   704
lemma is_Replace_cong [cong]:
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   705
     "[| A=A';
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   706
         !!x y. [| M(x); M(y) |] ==> P(x,y) \<longleftrightarrow> P'(x,y);
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   707
         z=z' |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   708
      ==> is_Replace(M, A, %x y. P(x,y), z) \<longleftrightarrow>
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   709
          is_Replace(M, A', %x y. P'(x,y), z')"
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   710
by (simp add: is_Replace_def)
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
   711
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   712
lemma (in M_trivial) univalent_Replace_iff:
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
   713
     "[| M(A); univalent(M,A,P);
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   714
         !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   715
      ==> u \<in> Replace(A,P) \<longleftrightarrow> (\<exists>x. x\<in>A & P(x,u))"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   716
apply (simp add: Replace_iff univalent_def)
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
   717
apply (blast dest: transM)
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
   718
done
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
   719
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   720
(*The last premise expresses that P takes M to M*)
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
   721
lemma (in M_trivial) strong_replacement_closed [intro,simp]:
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   722
     "[| strong_replacement(M,P); M(A); univalent(M,A,P);
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
   723
         !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |] ==> M(Replace(A,P))"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   724
apply (simp add: strong_replacement_def)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   725
apply (drule_tac x=A in rspec, safe)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   726
apply (subgoal_tac "Replace(A,P) = Y")
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   727
 apply simp
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
   728
apply (rule equality_iffI)
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
   729
apply (simp add: univalent_Replace_iff)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   730
apply (blast dest: transM)
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
   731
done
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
   732
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   733
lemma (in M_trivial) Replace_abs:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   734
     "[| M(A); M(z); univalent(M,A,P);
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   735
         !!x y. [| x\<in>A; P(x,y) |] ==> M(y)  |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   736
      ==> is_Replace(M,A,P,z) \<longleftrightarrow> z = Replace(A,P)"
13505
52a16cb7fefb Relativized right up to L satisfies V=L!
paulson
parents: 13436
diff changeset
   737
apply (simp add: is_Replace_def)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   738
apply (rule iffI)
13702
c7cf8fa66534 Polishing.
paulson
parents: 13687
diff changeset
   739
 apply (rule equality_iffI)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   740
 apply (simp_all add: univalent_Replace_iff)
13702
c7cf8fa66534 Polishing.
paulson
parents: 13687
diff changeset
   741
 apply (blast dest: transM)+
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   742
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   743
13702
c7cf8fa66534 Polishing.
paulson
parents: 13687
diff changeset
   744
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   745
(*The first premise can't simply be assumed as a schema.
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   746
  It is essential to take care when asserting instances of Replacement.
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   747
  Let K be a nonconstructible subset of nat and define
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   748
  f(x) = x if x \<in> K and f(x)=0 otherwise.  Then RepFun(nat,f) = cons(0,K), a
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   749
  nonconstructible set.  So we cannot assume that M(X) implies M(RepFun(X,f))
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   750
  even for f \<in> M -> M.
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   751
*)
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
   752
lemma (in M_trivial) RepFun_closed:
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   753
     "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   754
      ==> M(RepFun(A,f))"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   755
apply (simp add: RepFun_def)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   756
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   757
13353
1800e7134d2e towards relativization of "iterates" and "wfrec"
paulson
parents: 13352
diff changeset
   758
lemma Replace_conj_eq: "{y . x \<in> A, x\<in>A & y=f(x)} = {y . x\<in>A, y=f(x)}"
1800e7134d2e towards relativization of "iterates" and "wfrec"
paulson
parents: 13352
diff changeset
   759
by simp
1800e7134d2e towards relativization of "iterates" and "wfrec"
paulson
parents: 13352
diff changeset
   760
1800e7134d2e towards relativization of "iterates" and "wfrec"
paulson
parents: 13352
diff changeset
   761
text{*Better than @{text RepFun_closed} when having the formula @{term "x\<in>A"}
1800e7134d2e towards relativization of "iterates" and "wfrec"
paulson
parents: 13352
diff changeset
   762
      makes relativization easier.*}
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
   763
lemma (in M_trivial) RepFun_closed2:
13353
1800e7134d2e towards relativization of "iterates" and "wfrec"
paulson
parents: 13352
diff changeset
   764
     "[| strong_replacement(M, \<lambda>x y. x\<in>A & y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
1800e7134d2e towards relativization of "iterates" and "wfrec"
paulson
parents: 13352
diff changeset
   765
      ==> M(RepFun(A, %x. f(x)))"
1800e7134d2e towards relativization of "iterates" and "wfrec"
paulson
parents: 13352
diff changeset
   766
apply (simp add: RepFun_def)
1800e7134d2e towards relativization of "iterates" and "wfrec"
paulson
parents: 13352
diff changeset
   767
apply (frule strong_replacement_closed, assumption)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   768
apply (auto dest: transM  simp add: Replace_conj_eq univalent_def)
13353
1800e7134d2e towards relativization of "iterates" and "wfrec"
paulson
parents: 13352
diff changeset
   769
done
1800e7134d2e towards relativization of "iterates" and "wfrec"
paulson
parents: 13352
diff changeset
   770
13418
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   771
subsubsection {*Absoluteness for @{term Lambda}*}
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   772
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 16417
diff changeset
   773
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21233
diff changeset
   774
 is_lambda :: "[i=>o, i, [i,i]=>o, i] => o" where
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   775
    "is_lambda(M, A, is_b, z) ==
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   776
       \<forall>p[M]. p \<in> z \<longleftrightarrow>
13418
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   777
        (\<exists>u[M]. \<exists>v[M]. u\<in>A & pair(M,u,v,p) & is_b(u,v))"
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   778
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
   779
lemma (in M_trivial) lam_closed:
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   780
     "[| strong_replacement(M, \<lambda>x y. y = <x,b(x)>); M(A); \<forall>x\<in>A. M(b(x)) |]
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   781
      ==> M(\<lambda>x\<in>A. b(x))"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   782
by (simp add: lam_def, blast intro: RepFun_closed dest: transM)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   783
13418
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   784
text{*Better than @{text lam_closed}: has the formula @{term "x\<in>A"}*}
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
   785
lemma (in M_trivial) lam_closed2:
13418
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   786
  "[|strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   787
     M(A); \<forall>m[M]. m\<in>A \<longrightarrow> M(b(m))|] ==> M(Lambda(A,b))"
13418
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   788
apply (simp add: lam_def)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   789
apply (blast intro: RepFun_closed2 dest: transM)
13418
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   790
done
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   791
13702
c7cf8fa66534 Polishing.
paulson
parents: 13687
diff changeset
   792
lemma (in M_trivial) lambda_abs2:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   793
     "[| Relation1(M,A,is_b,b); M(A); \<forall>m[M]. m\<in>A \<longrightarrow> M(b(m)); M(z) |]
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   794
      ==> is_lambda(M,A,is_b,z) \<longleftrightarrow> z = Lambda(A,b)"
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13628
diff changeset
   795
apply (simp add: Relation1_def is_lambda_def)
13418
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   796
apply (rule iffI)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   797
 prefer 2 apply (simp add: lam_def)
13702
c7cf8fa66534 Polishing.
paulson
parents: 13687
diff changeset
   798
apply (rule equality_iffI)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   799
apply (simp add: lam_def)
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   800
apply (rule iffI)
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   801
 apply (blast dest: transM)
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   802
apply (auto simp add: transM [of _ A])
13418
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   803
done
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   804
13423
7ec771711c09 More lemmas, working towards relativization of "satisfies"
paulson
parents: 13418
diff changeset
   805
lemma is_lambda_cong [cong]:
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   806
     "[| A=A';  z=z';
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   807
         !!x y. [| x\<in>A; M(x); M(y) |] ==> is_b(x,y) \<longleftrightarrow> is_b'(x,y) |]
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   808
      ==> is_lambda(M, A, %x y. is_b(x,y), z) \<longleftrightarrow>
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   809
          is_lambda(M, A', %x y. is_b'(x,y), z')"
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   810
by (simp add: is_lambda_def)
13423
7ec771711c09 More lemmas, working towards relativization of "satisfies"
paulson
parents: 13418
diff changeset
   811
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   812
lemma (in M_trivial) image_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   813
     "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) \<longleftrightarrow> z = r``A"
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   814
apply (simp add: image_def)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   815
apply (rule iffI)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   816
 apply (blast intro!: equalityI dest: transM, blast)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   817
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   818
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   819
text{*What about @{text Pow_abs}?  Powerset is NOT absolute!
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   820
      This result is one direction of absoluteness.*}
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   821
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   822
lemma (in M_trivial) powerset_Pow:
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   823
     "powerset(M, x, Pow(x))"
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   824
by (simp add: powerset_def)
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   825
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   826
text{*But we can't prove that the powerset in @{text M} includes the
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   827
      real powerset.*}
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   828
lemma (in M_trivial) powerset_imp_subset_Pow:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   829
     "[| powerset(M,x,y); M(y) |] ==> y \<subseteq> Pow(x)"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   830
apply (simp add: powerset_def)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   831
apply (blast dest: transM)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   832
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   833
13418
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   834
subsubsection{*Absoluteness for the Natural Numbers*}
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   835
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
   836
lemma (in M_trivial) nat_into_M [intro]:
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   837
     "n \<in> nat ==> M(n)"
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   838
by (induct n rule: nat_induct, simp_all)
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   839
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
   840
lemma (in M_trivial) nat_case_closed [intro,simp]:
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   841
  "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   842
apply (case_tac "k=0", simp)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   843
apply (case_tac "\<exists>m. k = succ(m)", force)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   844
apply (simp add: nat_case_def)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   845
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   846
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   847
lemma (in M_trivial) quasinat_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   848
     "M(z) ==> is_quasinat(M,z) \<longleftrightarrow> quasinat(z)"
13350
paulson
parents: 13348
diff changeset
   849
by (auto simp add: is_quasinat_def quasinat_def)
paulson
parents: 13348
diff changeset
   850
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   851
lemma (in M_trivial) nat_case_abs [simp]:
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13628
diff changeset
   852
     "[| relation1(M,is_b,b); M(k); M(z) |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   853
      ==> is_nat_case(M,a,is_b,k,z) \<longleftrightarrow> z = nat_case(a,b,k)"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   854
apply (case_tac "quasinat(k)")
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   855
 prefer 2
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   856
 apply (simp add: is_nat_case_def non_nat_case)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   857
 apply (force simp add: quasinat_def)
13350
paulson
parents: 13348
diff changeset
   858
apply (simp add: quasinat_def is_nat_case_def)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   859
apply (elim disjE exE)
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13628
diff changeset
   860
 apply (simp_all add: relation1_def)
13350
paulson
parents: 13348
diff changeset
   861
done
paulson
parents: 13348
diff changeset
   862
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   863
(*NOT for the simplifier.  The assumption M(z') is apparently necessary, but
13363
c26eeb000470 instantiation of locales M_trancl and M_wfrank;
paulson
parents: 13353
diff changeset
   864
  causes the error "Failed congruence proof!"  It may be better to replace
c26eeb000470 instantiation of locales M_trancl and M_wfrank;
paulson
parents: 13353
diff changeset
   865
  is_nat_case by nat_case before attempting congruence reasoning.*)
13434
78b93a667c01 better sats rules for higher-order operators
paulson
parents: 13428
diff changeset
   866
lemma is_nat_case_cong:
13352
3cd767f8d78b new definitions of fun_apply and M_is_recfun
paulson
parents: 13350
diff changeset
   867
     "[| a = a'; k = k';  z = z';  M(z');
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   868
       !!x y. [| M(x); M(y) |] ==> is_b(x,y) \<longleftrightarrow> is_b'(x,y) |]
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   869
      ==> is_nat_case(M, a, is_b, k, z) \<longleftrightarrow> is_nat_case(M, a', is_b', k', z')"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   870
by (simp add: is_nat_case_def)
13352
3cd767f8d78b new definitions of fun_apply and M_is_recfun
paulson
parents: 13350
diff changeset
   871
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   872
13418
7c0ba9dba978 tweaks, aiming towards relativization of "satisfies"
paulson
parents: 13397
diff changeset
   873
subsection{*Absoluteness for Ordinals*}
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   874
text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   875
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
   876
lemma (in M_trivial) lt_closed:
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   877
     "[| j<i; M(i) |] ==> M(j)"
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   878
by (blast dest: ltD intro: transM)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   879
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   880
lemma (in M_trivial) transitive_set_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   881
     "M(a) ==> transitive_set(M,a) \<longleftrightarrow> Transset(a)"
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   882
by (simp add: transitive_set_def Transset_def)
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   883
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   884
lemma (in M_trivial) ordinal_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   885
     "M(a) ==> ordinal(M,a) \<longleftrightarrow> Ord(a)"
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   886
by (simp add: ordinal_def Ord_def)
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   887
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   888
lemma (in M_trivial) limit_ordinal_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   889
     "M(a) ==> limit_ordinal(M,a) \<longleftrightarrow> Limit(a)"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   890
apply (unfold Limit_def limit_ordinal_def)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   891
apply (simp add: Ord_0_lt_iff)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   892
apply (simp add: lt_def, blast)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   893
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   894
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   895
lemma (in M_trivial) successor_ordinal_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   896
     "M(a) ==> successor_ordinal(M,a) \<longleftrightarrow> Ord(a) & (\<exists>b[M]. a = succ(b))"
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   897
apply (simp add: successor_ordinal_def, safe)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   898
apply (drule Ord_cases_disj, auto)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   899
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   900
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   901
lemma finite_Ord_is_nat:
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   902
      "[| Ord(a); ~ Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a \<in> nat"
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   903
by (induct a rule: trans_induct3, simp_all)
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   904
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   905
lemma (in M_trivial) finite_ordinal_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   906
     "M(a) ==> finite_ordinal(M,a) \<longleftrightarrow> a \<in> nat"
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   907
apply (simp add: finite_ordinal_def)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   908
apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   909
             dest: Ord_trans naturals_not_limit)
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   910
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   911
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   912
lemma Limit_non_Limit_implies_nat:
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   913
     "[| Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a = nat"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   914
apply (rule le_anti_sym)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   915
apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   916
 apply (simp add: lt_def)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   917
 apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   918
apply (erule nat_le_Limit)
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   919
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   920
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   921
lemma (in M_trivial) omega_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   922
     "M(a) ==> omega(M,a) \<longleftrightarrow> a = nat"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   923
apply (simp add: omega_def)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   924
apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   925
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   926
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   927
lemma (in M_trivial) number1_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   928
     "M(a) ==> number1(M,a) \<longleftrightarrow> a = 1"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   929
by (simp add: number1_def)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   930
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   931
lemma (in M_trivial) number2_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   932
     "M(a) ==> number2(M,a) \<longleftrightarrow> a = succ(1)"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   933
by (simp add: number2_def)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   934
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   935
lemma (in M_trivial) number3_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   936
     "M(a) ==> number3(M,a) \<longleftrightarrow> a = succ(succ(1))"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   937
by (simp add: number3_def)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   938
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   939
text{*Kunen continued to 20...*}
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   940
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   941
(*Could not get this to work.  The \<lambda>x\<in>nat is essential because everything
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   942
  but the recursion variable must stay unchanged.  But then the recursion
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   943
  equations only hold for x\<in>nat (or in some other set) and not for the
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   944
  whole of the class M.
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   945
  consts
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   946
    natnumber_aux :: "[i=>o,i] => i"
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   947
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   948
  primrec
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   949
      "natnumber_aux(M,0) = (\<lambda>x\<in>nat. if empty(M,x) then 1 else 0)"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   950
      "natnumber_aux(M,succ(n)) =
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 22710
diff changeset
   951
           (\<lambda>x\<in>nat. if (\<exists>y[M]. natnumber_aux(M,n)`y=1 & successor(M,y,x))
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 22710
diff changeset
   952
                     then 1 else 0)"
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   953
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 16417
diff changeset
   954
  definition
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   955
    natnumber :: "[i=>o,i,i] => o"
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   956
      "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1"
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   957
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   958
  lemma (in M_trivial) [simp]:
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   959
       "natnumber(M,0,x) == x=0"
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   960
*)
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   961
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   962
subsection{*Some instances of separation and strong replacement*}
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   963
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
   964
locale M_basic = M_trivial +
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
   965
assumes Inter_separation:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   966
     "M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A \<longrightarrow> x\<in>y)"
13436
8fd1d803a3d3 tweaks involving Separation
paulson
parents: 13434
diff changeset
   967
  and Diff_separation:
8fd1d803a3d3 tweaks involving Separation
paulson
parents: 13434
diff changeset
   968
     "M(B) ==> separation(M, \<lambda>x. x \<notin> B)"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   969
  and cartprod_separation:
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   970
     "[| M(A); M(B) |]
13298
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13290
diff changeset
   971
      ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,z)))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   972
  and image_separation:
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   973
     "[| M(A); M(r) |]
13268
240509babf00 more use of relativized quantifiers
paulson
parents: 13254
diff changeset
   974
      ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,p)))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   975
  and converse_separation:
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   976
     "M(r) ==> separation(M,
13298
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13290
diff changeset
   977
         \<lambda>z. \<exists>p[M]. p\<in>r & (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) & pair(M,y,x,z)))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   978
  and restrict_separation:
13268
240509babf00 more use of relativized quantifiers
paulson
parents: 13254
diff changeset
   979
     "M(A) ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. pair(M,x,y,z)))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   980
  and comp_separation:
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   981
     "[| M(r); M(s) |]
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   982
      ==> separation(M, \<lambda>xz. \<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M].
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 22710
diff changeset
   983
                  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) &
13268
240509babf00 more use of relativized quantifiers
paulson
parents: 13254
diff changeset
   984
                  xy\<in>s & yz\<in>r)"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   985
  and pred_separation:
13298
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13290
diff changeset
   986
     "[| M(r); M(x) |] ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & pair(M,y,x,p))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   987
  and Memrel_separation:
13298
b4f370679c65 Constructible: some separation axioms
paulson
parents: 13290
diff changeset
   988
     "separation(M, \<lambda>z. \<exists>x[M]. \<exists>y[M]. pair(M,x,y,z) & x \<in> y)"
13268
240509babf00 more use of relativized quantifiers
paulson
parents: 13254
diff changeset
   989
  and funspace_succ_replacement:
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   990
     "M(n) ==>
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   991
      strong_replacement(M, \<lambda>p z. \<exists>f[M]. \<exists>b[M]. \<exists>nb[M]. \<exists>cnbf[M].
13306
6eebcddee32b more internalized formulas and separation proofs
paulson
parents: 13299
diff changeset
   992
                pair(M,f,b,p) & pair(M,n,b,nb) & is_cons(M,nb,f,cnbf) &
6eebcddee32b more internalized formulas and separation proofs
paulson
parents: 13299
diff changeset
   993
                upair(M,cnbf,cnbf,z))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
   994
  and is_recfun_separation:
13634
99a593b49b04 Re-organization of Constructible theories
paulson
parents: 13628
diff changeset
   995
     --{*for well-founded recursion: used to prove @{text is_recfun_equal}*}
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   996
     "[| M(r); M(f); M(g); M(a); M(b) |]
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   997
     ==> separation(M,
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   998
            \<lambda>x. \<exists>xa[M]. \<exists>xb[M].
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
   999
                pair(M,x,a,xa) & xa \<in> r & pair(M,x,b,xb) & xb \<in> r &
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1000
                (\<exists>fx[M]. \<exists>gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) &
13319
23de7b3af453 More Separation proofs
paulson
parents: 13316
diff changeset
  1001
                                   fx \<noteq> gx))"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1002
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
  1003
lemma (in M_basic) cartprod_iff_lemma:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
  1004
     "[| M(C);  \<forall>u[M]. u \<in> C \<longleftrightarrow> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}});
13254
5146ccaedf42 class quantifiers (some)
paulson
parents: 13251
diff changeset
  1005
         powerset(M, A \<union> B, p1); powerset(M, p1, p2);  M(p2) |]
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1006
       ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1007
apply (simp add: powerset_def)
13254
5146ccaedf42 class quantifiers (some)
paulson
parents: 13251
diff changeset
  1008
apply (rule equalityI, clarify, simp)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1009
 apply (frule transM, assumption)
13611
2edf034c902a Adapted to new simplifier.
berghofe
parents: 13564
diff changeset
  1010
 apply (frule transM, assumption, simp (no_asm_simp))
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1011
 apply blast
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1012
apply clarify
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1013
apply (frule transM, assumption, force)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1014
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1015
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
  1016
lemma (in M_basic) cartprod_iff:
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1017
     "[| M(A); M(B); M(C) |]
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
  1018
      ==> cartprod(M,A,B,C) \<longleftrightarrow>
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
  1019
          (\<exists>p1[M]. \<exists>p2[M]. powerset(M,A \<union> B,p1) & powerset(M,p1,p2) &
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1020
                   C = {z \<in> p2. \<exists>x\<in>A. \<exists>y\<in>B. z = <x,y>})"
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1021
apply (simp add: Pair_def cartprod_def, safe)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1022
defer 1
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1023
  apply (simp add: powerset_def)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1024
 apply blast
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1025
txt{*Final, difficult case: the left-to-right direction of the theorem.*}
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1026
apply (insert power_ax, simp add: power_ax_def)
59788
6f7b6adac439 prefer local fixes;
wenzelm
parents: 58871
diff changeset
  1027
apply (frule_tac x="A \<union> B" and P="\<lambda>x. rex(M,Q(x))" for Q in rspec)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1028
apply (blast, clarify)
59788
6f7b6adac439 prefer local fixes;
wenzelm
parents: 58871
diff changeset
  1029
apply (drule_tac x=z and P="\<lambda>x. rex(M,Q(x))" for Q in rspec)
13299
3a932abf97e8 More use of relativized quantifiers
paulson
parents: 13298
diff changeset
  1030
apply assumption
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1031
apply (blast intro: cartprod_iff_lemma)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1032
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1033
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
  1034
lemma (in M_basic) cartprod_closed_lemma:
13299
3a932abf97e8 More use of relativized quantifiers
paulson
parents: 13298
diff changeset
  1035
     "[| M(A); M(B) |] ==> \<exists>C[M]. cartprod(M,A,B,C)"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1036
apply (simp del: cartprod_abs add: cartprod_iff)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1037
apply (insert power_ax, simp add: power_ax_def)
59788
6f7b6adac439 prefer local fixes;
wenzelm
parents: 58871
diff changeset
  1038
apply (frule_tac x="A \<union> B" and P="\<lambda>x. rex(M,Q(x))" for Q in rspec)
13299
3a932abf97e8 More use of relativized quantifiers
paulson
parents: 13298
diff changeset
  1039
apply (blast, clarify)
59788
6f7b6adac439 prefer local fixes;
wenzelm
parents: 58871
diff changeset
  1040
apply (drule_tac x=z and P="\<lambda>x. rex(M,Q(x))" for Q in rspec, auto)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1041
apply (intro rexI conjI, simp+)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1042
apply (insert cartprod_separation [of A B], simp)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1043
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1044
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1045
text{*All the lemmas above are necessary because Powerset is not absolute.
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1046
      I should have used Replacement instead!*}
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1047
lemma (in M_basic) cartprod_closed [intro,simp]:
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1048
     "[| M(A); M(B) |] ==> M(A*B)"
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1049
by (frule cartprod_closed_lemma, assumption, force)
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1050
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1051
lemma (in M_basic) sum_closed [intro,simp]:
13268
240509babf00 more use of relativized quantifiers
paulson
parents: 13254
diff changeset
  1052
     "[| M(A); M(B) |] ==> M(A+B)"
240509babf00 more use of relativized quantifiers
paulson
parents: 13254
diff changeset
  1053
by (simp add: sum_def)
240509babf00 more use of relativized quantifiers
paulson
parents: 13254
diff changeset
  1054
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
  1055
lemma (in M_basic) sum_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
  1056
     "[| M(A); M(B); M(Z) |] ==> is_sum(M,A,B,Z) \<longleftrightarrow> (Z = A+B)"
13350
paulson
parents: 13348
diff changeset
  1057
by (simp add: is_sum_def sum_def singleton_0 nat_into_M)
paulson
parents: 13348
diff changeset
  1058
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
  1059
lemma (in M_trivial) Inl_in_M_iff [iff]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
  1060
     "M(Inl(a)) \<longleftrightarrow> M(a)"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1061
by (simp add: Inl_def)
13397
6e5f4d911435 Absoluteness of the function "nth"
paulson
parents: 13382
diff changeset
  1062
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
  1063
lemma (in M_trivial) Inl_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
  1064
     "M(Z) ==> is_Inl(M,a,Z) \<longleftrightarrow> (Z = Inl(a))"
13397
6e5f4d911435 Absoluteness of the function "nth"
paulson
parents: 13382
diff changeset
  1065
by (simp add: is_Inl_def Inl_def)
6e5f4d911435 Absoluteness of the function "nth"
paulson
parents: 13382
diff changeset
  1066
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
  1067
lemma (in M_trivial) Inr_in_M_iff [iff]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
  1068
     "M(Inr(a)) \<longleftrightarrow> M(a)"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1069
by (simp add: Inr_def)
13397
6e5f4d911435 Absoluteness of the function "nth"
paulson
parents: 13382
diff changeset
  1070
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
  1071
lemma (in M_trivial) Inr_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
  1072
     "M(Z) ==> is_Inr(M,a,Z) \<longleftrightarrow> (Z = Inr(a))"
13397
6e5f4d911435 Absoluteness of the function "nth"
paulson
parents: 13382
diff changeset
  1073
by (simp add: is_Inr_def Inr_def)
6e5f4d911435 Absoluteness of the function "nth"
paulson
parents: 13382
diff changeset
  1074
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1075
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1076
subsubsection {*converse of a relation*}
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1077
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
  1078
lemma (in M_basic) M_converse_iff:
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1079
     "M(r) ==>
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1080
      converse(r) =
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
  1081
      {z \<in> \<Union>(\<Union>(r)) * \<Union>(\<Union>(r)).
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1082
       \<exists>p\<in>r. \<exists>x[M]. \<exists>y[M]. p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>}"
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1083
apply (rule equalityI)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1084
 prefer 2 apply (blast dest: transM, clarify, simp)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1085
apply (simp add: Pair_def)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1086
apply (blast dest: transM)
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1087
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1088
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1089
lemma (in M_basic) converse_closed [intro,simp]:
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1090
     "M(r) ==> M(converse(r))"
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1091
apply (simp add: M_converse_iff)
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1092
apply (insert converse_separation [of r], simp)
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1093
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1094
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1095
lemma (in M_basic) converse_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
  1096
     "[| M(r); M(z) |] ==> is_converse(M,r,z) \<longleftrightarrow> z = converse(r)"
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1097
apply (simp add: is_converse_def)
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1098
apply (rule iffI)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1099
 prefer 2 apply blast
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1100
apply (rule M_equalityI)
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1101
  apply simp
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1102
  apply (blast dest: transM)+
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1103
done
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1104
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1105
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1106
subsubsection {*image, preimage, domain, range*}
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1107
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1108
lemma (in M_basic) image_closed [intro,simp]:
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1109
     "[| M(A); M(r) |] ==> M(r``A)"
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1110
apply (simp add: image_iff_Collect)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1111
apply (insert image_separation [of A r], simp)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1112
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1113
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1114
lemma (in M_basic) vimage_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
  1115
     "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) \<longleftrightarrow> z = r-``A"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1116
apply (simp add: pre_image_def)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1117
apply (rule iffI)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1118
 apply (blast intro!: equalityI dest: transM, blast)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1119
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1120
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1121
lemma (in M_basic) vimage_closed [intro,simp]:
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1122
     "[| M(A); M(r) |] ==> M(r-``A)"
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1123
by (simp add: vimage_def)
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1124
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1125
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1126
subsubsection{*Domain, range and field*}
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1127
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1128
lemma (in M_basic) domain_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
  1129
     "[| M(r); M(z) |] ==> is_domain(M,r,z) \<longleftrightarrow> z = domain(r)"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1130
apply (simp add: is_domain_def)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1131
apply (blast intro!: equalityI dest: transM)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1132
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1133
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1134
lemma (in M_basic) domain_closed [intro,simp]:
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1135
     "M(r) ==> M(domain(r))"
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1136
apply (simp add: domain_eq_vimage)
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1137
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1138
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1139
lemma (in M_basic) range_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
  1140
     "[| M(r); M(z) |] ==> is_range(M,r,z) \<longleftrightarrow> z = range(r)"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1141
apply (simp add: is_range_def)
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1142
apply (blast intro!: equalityI dest: transM)
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1143
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1144
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1145
lemma (in M_basic) range_closed [intro,simp]:
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1146
     "M(r) ==> M(range(r))"
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1147
apply (simp add: range_eq_image)
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1148
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1149
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1150
lemma (in M_basic) field_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
  1151
     "[| M(r); M(z) |] ==> is_field(M,r,z) \<longleftrightarrow> z = field(r)"
13245
714f7a423a15 development and tweaks
paulson
parents: 13223
diff changeset
  1152
by (simp add: domain_closed range_closed is_field_def field_def)
714f7a423a15 development and tweaks
paulson
parents: 13223
diff changeset
  1153
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1154
lemma (in M_basic) field_closed [intro,simp]:
13245
714f7a423a15 development and tweaks
paulson
parents: 13223
diff changeset
  1155
     "M(r) ==> M(field(r))"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1156
by (simp add: domain_closed range_closed Un_closed field_def)
13245
714f7a423a15 development and tweaks
paulson
parents: 13223
diff changeset
  1157
714f7a423a15 development and tweaks
paulson
parents: 13223
diff changeset
  1158
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1159
subsubsection{*Relations, functions and application*}
13254
5146ccaedf42 class quantifiers (some)
paulson
parents: 13251
diff changeset
  1160
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1161
lemma (in M_basic) relation_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
  1162
     "M(r) ==> is_relation(M,r) \<longleftrightarrow> relation(r)"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1163
apply (simp add: is_relation_def relation_def)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1164
apply (blast dest!: bspec dest: pair_components_in_M)+
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1165
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1166
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1167
lemma (in M_basic) function_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
  1168
     "M(r) ==> is_function(M,r) \<longleftrightarrow> function(r)"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1169
apply (simp add: is_function_def function_def, safe)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1170
   apply (frule transM, assumption)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1171
  apply (blast dest: pair_components_in_M)+
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1172
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1173
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1174
lemma (in M_basic) apply_closed [intro,simp]:
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1175
     "[|M(f); M(a)|] ==> M(f`a)"
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1176
by (simp add: apply_def)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1177
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1178
lemma (in M_basic) apply_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
  1179
     "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) \<longleftrightarrow> f`x = y"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1180
apply (simp add: fun_apply_def apply_def, blast)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1181
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1182
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1183
lemma (in M_basic) typed_function_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
  1184
     "[| M(A); M(f) |] ==> typed_function(M,A,B,f) \<longleftrightarrow> f \<in> A -> B"
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1185
apply (auto simp add: typed_function_def relation_def Pi_iff)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1186
apply (blast dest: pair_components_in_M)+
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1187
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1188
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1189
lemma (in M_basic) injection_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
  1190
     "[| M(A); M(f) |] ==> injection(M,A,B,f) \<longleftrightarrow> f \<in> inj(A,B)"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1191
apply (simp add: injection_def apply_iff inj_def apply_closed)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1192
apply (blast dest: transM [of _ A])
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1193
done
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1194
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1195
lemma (in M_basic) surjection_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
  1196
     "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) \<longleftrightarrow> f \<in> surj(A,B)"
13352
3cd767f8d78b new definitions of fun_apply and M_is_recfun
paulson
parents: 13350
diff changeset
  1197
by (simp add: surjection_def surj_def)
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1198
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1199
lemma (in M_basic) bijection_abs [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
  1200
     "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) \<longleftrightarrow> f \<in> bij(A,B)"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1201
by (simp add: bijection_def bij_def)
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1202
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1203
13290
28ce81eff3de separation of M_axioms into M_triv_axioms and M_axioms
paulson
parents: 13269
diff changeset
  1204
subsubsection{*Composition of relations*}
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1205
13564
1500a2e48d44 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
paulson
parents: 13563
diff changeset
  1206
lemma (in M_basic) M_comp_iff:
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1207
     "[| M(r); M(s) |]
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1208
      ==> r O s =
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1209
          {xz \<in> domain(s) * range(r).
13268
240509babf00 more use of relativized quantifiers
paulson
parents: 13254
diff changeset
  1210
            \<exists>x[M]. \<exists>y[M]. \<exists>z[M]. xz = \<langle>x,z\<rangle> & \<langle>x,y\<rangle> \<in> s & \<langle>y,z\<rangle> \<in> r}"
13223
45be08fbdcff new theory of inner models
paulson
parents:
diff changeset
  1211
apply (simp add: comp_def)
13628
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1212
apply (rule equalityI)
87482b5e3f2e Various simplifications of the Constructible theories
paulson
parents: 13615
diff changeset
  1213