src/ZF/Constructible/Formula.thy
changeset 13298 b4f370679c65
parent 13291 a73ab154f75c
child 13306 6eebcddee32b
     1.1 --- a/src/ZF/Constructible/Formula.thy	Thu Jul 04 16:48:21 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Formula.thy	Thu Jul 04 16:59:54 2002 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4  
     1.5  declare satisfies.simps [simp del]; 
     1.6  
     1.7 -subsubsection{*Dividing line between primitive and derived connectives*}
     1.8 +subsection{*Dividing line between primitive and derived connectives*}
     1.9  
    1.10  lemma sats_Or_iff [simp]:
    1.11    "env \<in> list(A) 
    1.12 @@ -125,6 +125,11 @@
    1.13         ==> (x\<in>y) <-> sats(A, Member(i,j), env)" 
    1.14  by (simp add: satisfies.simps)
    1.15  
    1.16 +lemma equal_iff_sats:
    1.17 +      "[| nth(i,env) = x; nth(j,env) = y; env \<in> list(A)|]
    1.18 +       ==> (x=y) <-> sats(A, Equal(i,j), env)" 
    1.19 +by (simp add: satisfies.simps)
    1.20 +
    1.21  lemma conj_iff_sats:
    1.22        "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
    1.23         ==> (P & Q) <-> sats(A, And(p,q), env)"
    1.24 @@ -161,22 +166,6 @@
    1.25  by (simp add: sats_Exists_iff) 
    1.26  
    1.27  
    1.28 -
    1.29 -(*pretty but unnecessary
    1.30 -constdefs sat     :: "[i,i] => o"
    1.31 -  "sat(A,p) == satisfies(A,p)`[] = 1"
    1.32 -
    1.33 -syntax "_sat"  :: "[i,i] => o"    (infixl "|=" 50)
    1.34 -translations "A |= p" == "sat(A,p)"
    1.35 -
    1.36 -lemma [simp]: "(A |= Neg(p)) <-> ~ (A |= p)"
    1.37 -by (simp add: sat_def)
    1.38 -
    1.39 -lemma [simp]: "(A |= And(p,q)) <-> A|=p & A|=q"
    1.40 -by (simp add: sat_def)
    1.41 -*) 
    1.42 -
    1.43 -
    1.44  constdefs incr_var :: "[i,i]=>i"
    1.45      "incr_var(x,lev) == if x<lev then x else succ(x)"
    1.46  
    1.47 @@ -355,7 +344,7 @@
    1.48  done
    1.49  
    1.50  
    1.51 -(**** TRYING INCR_BV1 AGAIN ****)
    1.52 +subsection{*Renaming all but the first bound variable*}
    1.53  
    1.54  constdefs incr_bv1 :: "i => i"
    1.55      "incr_bv1(p) == incr_bv(p)`1"
    1.56 @@ -398,7 +387,7 @@
    1.57     ==> arity(incr_bv1^n(p)) =
    1.58           (if 1 < arity(p) then n #+ arity(p) else arity(p))"
    1.59  apply (induct_tac n) 
    1.60 -apply (simp_all add: arity_incr_bv1_eq )
    1.61 +apply (simp_all add: arity_incr_bv1_eq)
    1.62  apply (simp add: not_lt_iff_le)
    1.63  apply (blast intro: le_trans add_le_self2 arity_type) 
    1.64  done
    1.65 @@ -520,6 +509,76 @@
    1.66  oops
    1.67  *)
    1.68  
    1.69 +
    1.70 +subsection{*Internalized formulas for basic concepts*}
    1.71 +
    1.72 +subsubsection{*The subset relation*}
    1.73 +
    1.74 +lemma lt_length_in_nat:
    1.75 +   "[|x < length(xs); xs \<in> list(A)|] ==> x \<in> nat"
    1.76 +apply (frule lt_nat_in_nat, typecheck) 
    1.77 +done
    1.78 +
    1.79 +constdefs subset_fm :: "[i,i]=>i"
    1.80 +    "subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))"
    1.81 +
    1.82 +lemma subset_type [TC]: "[| x \<in> nat; y \<in> nat |] ==> subset_fm(x,y) \<in> formula"
    1.83 +by (simp add: subset_fm_def) 
    1.84 +
    1.85 +lemma arity_subset_fm [simp]:
    1.86 +     "[| x \<in> nat; y \<in> nat |] ==> arity(subset_fm(x,y)) = succ(x) \<union> succ(y)"
    1.87 +by (simp add: subset_fm_def succ_Un_distrib [symmetric]) 
    1.88 +
    1.89 +lemma sats_subset_fm [simp]:
    1.90 +   "[|x < length(env); y \<in> nat; env \<in> list(A); Transset(A)|]
    1.91 +    ==> sats(A, subset_fm(x,y), env) <-> nth(x,env) \<subseteq> nth(y,env)"
    1.92 +apply (frule lt_length_in_nat, assumption)  
    1.93 +apply (simp add: subset_fm_def Transset_def) 
    1.94 +apply (blast intro: nth_type) 
    1.95 +done
    1.96 +
    1.97 +subsubsection{*Transitive sets*}
    1.98 +
    1.99 +constdefs transset_fm :: "i=>i"
   1.100 +   "transset_fm(x) == Forall(Implies(Member(0,succ(x)), subset_fm(0,succ(x))))"
   1.101 +
   1.102 +lemma transset_type [TC]: "x \<in> nat ==> transset_fm(x) \<in> formula"
   1.103 +by (simp add: transset_fm_def) 
   1.104 +
   1.105 +lemma arity_transset_fm [simp]:
   1.106 +     "x \<in> nat ==> arity(transset_fm(x)) = succ(x)"
   1.107 +by (simp add: transset_fm_def succ_Un_distrib [symmetric]) 
   1.108 +
   1.109 +lemma sats_transset_fm [simp]:
   1.110 +   "[|x < length(env); env \<in> list(A); Transset(A)|]
   1.111 +    ==> sats(A, transset_fm(x), env) <-> Transset(nth(x,env))"
   1.112 +apply (frule lt_nat_in_nat, erule length_type) 
   1.113 +apply (simp add: transset_fm_def Transset_def) 
   1.114 +apply (blast intro: nth_type) 
   1.115 +done
   1.116 +
   1.117 +subsubsection{*Ordinals*}
   1.118 +
   1.119 +constdefs ordinal_fm :: "i=>i"
   1.120 +   "ordinal_fm(x) == 
   1.121 +      And(transset_fm(x), Forall(Implies(Member(0,succ(x)), transset_fm(0))))"
   1.122 +
   1.123 +lemma ordinal_type [TC]: "x \<in> nat ==> ordinal_fm(x) \<in> formula"
   1.124 +by (simp add: ordinal_fm_def) 
   1.125 +
   1.126 +lemma arity_ordinal_fm [simp]:
   1.127 +     "x \<in> nat ==> arity(ordinal_fm(x)) = succ(x)"
   1.128 +by (simp add: ordinal_fm_def succ_Un_distrib [symmetric]) 
   1.129 +
   1.130 +lemma sats_ordinal_fm [simp]:
   1.131 +   "[|x < length(env); env \<in> list(A); Transset(A)|]
   1.132 +    ==> sats(A, ordinal_fm(x), env) <-> Ord(nth(x,env))"
   1.133 +apply (frule lt_nat_in_nat, erule length_type) 
   1.134 +apply (simp add: ordinal_fm_def Ord_def Transset_def)
   1.135 +apply (blast intro: nth_type) 
   1.136 +done
   1.137 +
   1.138 +
   1.139  subsection{* Constant Lset: Levels of the Constructible Universe *}
   1.140  
   1.141  constdefs Lset :: "i=>i"
   1.142 @@ -661,63 +720,7 @@
   1.143  done
   1.144  
   1.145  
   1.146 -
   1.147 -text{*Kunen's VI, 1.9 (b)*}
   1.148 -
   1.149 -constdefs subset_fm :: "[i,i]=>i"
   1.150 -    "subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))"
   1.151 -
   1.152 -lemma subset_type [TC]: "[| x \<in> nat; y \<in> nat |] ==> subset_fm(x,y) \<in> formula"
   1.153 -by (simp add: subset_fm_def) 
   1.154 -
   1.155 -lemma arity_subset_fm [simp]:
   1.156 -     "[| x \<in> nat; y \<in> nat |] ==> arity(subset_fm(x,y)) = succ(x) \<union> succ(y)"
   1.157 -by (simp add: subset_fm_def succ_Un_distrib [symmetric]) 
   1.158 -
   1.159 -lemma sats_subset_fm [simp]:
   1.160 -   "[|x < length(env); y \<in> nat; env \<in> list(A); Transset(A)|]
   1.161 -    ==> sats(A, subset_fm(x,y), env) <-> nth(x,env) \<subseteq> nth(y,env)"
   1.162 -apply (frule lt_nat_in_nat, erule length_type) 
   1.163 -apply (simp add: subset_fm_def Transset_def) 
   1.164 -apply (blast intro: nth_type ) 
   1.165 -done
   1.166 -
   1.167 -constdefs transset_fm :: "i=>i"
   1.168 -   "transset_fm(x) == Forall(Implies(Member(0,succ(x)), subset_fm(0,succ(x))))"
   1.169 -
   1.170 -lemma transset_type [TC]: "x \<in> nat ==> transset_fm(x) \<in> formula"
   1.171 -by (simp add: transset_fm_def) 
   1.172 -
   1.173 -lemma arity_transset_fm [simp]:
   1.174 -     "x \<in> nat ==> arity(transset_fm(x)) = succ(x)"
   1.175 -by (simp add: transset_fm_def succ_Un_distrib [symmetric]) 
   1.176 -
   1.177 -lemma sats_transset_fm [simp]:
   1.178 -   "[|x < length(env); env \<in> list(A); Transset(A)|]
   1.179 -    ==> sats(A, transset_fm(x), env) <-> Transset(nth(x,env))"
   1.180 -apply (frule lt_nat_in_nat, erule length_type) 
   1.181 -apply (simp add: transset_fm_def Transset_def) 
   1.182 -apply (blast intro: nth_type ) 
   1.183 -done
   1.184 -
   1.185 -constdefs ordinal_fm :: "i=>i"
   1.186 -   "ordinal_fm(x) == 
   1.187 -      And(transset_fm(x), Forall(Implies(Member(0,succ(x)), transset_fm(0))))"
   1.188 -
   1.189 -lemma ordinal_type [TC]: "x \<in> nat ==> ordinal_fm(x) \<in> formula"
   1.190 -by (simp add: ordinal_fm_def) 
   1.191 -
   1.192 -lemma arity_ordinal_fm [simp]:
   1.193 -     "x \<in> nat ==> arity(ordinal_fm(x)) = succ(x)"
   1.194 -by (simp add: ordinal_fm_def succ_Un_distrib [symmetric]) 
   1.195 -
   1.196 -lemma sats_ordinal_fm [simp]:
   1.197 -   "[|x < length(env); env \<in> list(A); Transset(A)|]
   1.198 -    ==> sats(A, ordinal_fm(x), env) <-> Ord(nth(x,env))"
   1.199 -apply (frule lt_nat_in_nat, erule length_type) 
   1.200 -apply (simp add: ordinal_fm_def Ord_def Transset_def)
   1.201 -apply (blast intro: nth_type ) 
   1.202 -done
   1.203 +subsection{*Constructible Ordinals: Kunen's VI, 1.9 (b)*}
   1.204  
   1.205  text{*The subset consisting of the ordinals is definable.*}
   1.206  lemma Ords_in_DPow: "Transset(A) ==> {x \<in> A. Ord(x)} \<in> DPow(A)"