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)"
```