src/ZF/Constructible/Formula.thy
 changeset 13291 a73ab154f75c parent 13269 3ba9be497c33 child 13298 b4f370679c65
```     1.1 --- a/src/ZF/Constructible/Formula.thy	Thu Jul 04 10:51:52 2002 +0200
1.2 +++ b/src/ZF/Constructible/Formula.thy	Thu Jul 04 10:52:33 2002 +0200
1.3 @@ -2,8 +2,10 @@
1.4
1.5  theory Formula = Main:
1.6
1.7 -(*Internalized formulas of FOL. De Bruijn representation.
1.8 -  Unbound variables get their denotations from an environment.*)
1.9 +subsection{*Internalized formulas of FOL*}
1.10 +
1.11 +text{*De Bruijn representation.
1.12 +  Unbound variables get their denotations from an environment.*}
1.13
1.14  consts   formula :: i
1.15  datatype
1.16 @@ -21,6 +23,9 @@
1.17  constdefs Implies :: "[i,i]=>i"
1.18      "Implies(p,q) == Neg(And(p,Neg(q)))"
1.19
1.20 +constdefs Iff :: "[i,i]=>i"
1.21 +    "Iff(p,q) == And(Implies(p,q), Implies(q,p))"
1.22 +
1.23  constdefs Exists :: "i=>i"
1.24      "Exists(p) == Neg(Forall(Neg(p)))";
1.25
1.26 @@ -31,6 +36,10 @@
1.27       "[| p \<in> formula; q \<in> formula |] ==> Implies(p,q) \<in> formula"
1.29
1.30 +lemma Iff_type [TC]:
1.31 +     "[| p \<in> formula; q \<in> formula |] ==> Iff(p,q) \<in> formula"
1.33 +
1.34  lemma Exists_type [TC]: "p \<in> formula ==> Exists(p) \<in> formula"
1.36
1.37 @@ -86,7 +95,7 @@
1.38
1.39  declare satisfies.simps [simp del];
1.40
1.41 -(**** DIVIDING LINE BETWEEN PRIMITIVE AND DERIVED CONNECTIVES ****)
1.42 +subsubsection{*Dividing line between primitive and derived connectives*}
1.43
1.44  lemma sats_Or_iff [simp]:
1.45    "env \<in> list(A)
1.46 @@ -96,8 +105,12 @@
1.47  lemma sats_Implies_iff [simp]:
1.48    "env \<in> list(A)
1.49     ==> (sats(A, Implies(p,q), env)) <-> (sats(A,p,env) --> sats(A,q,env))"
1.50 -apply (simp add: Implies_def, blast)
1.51 -done
1.52 +by (simp add: Implies_def, blast)
1.53 +
1.54 +lemma sats_Iff_iff [simp]:
1.55 +  "env \<in> list(A)
1.56 +   ==> (sats(A, Iff(p,q), env)) <-> (sats(A,p,env) <-> sats(A,q,env))"
1.57 +by (simp add: Iff_def, blast)
1.58
1.59  lemma sats_Exists_iff [simp]:
1.60    "env \<in> list(A)
1.61 @@ -105,6 +118,48 @@
1.63
1.64
1.65 +subsubsection{*Derived rules to help build up formulas*}
1.66 +
1.67 +lemma mem_iff_sats:
1.68 +      "[| nth(i,env) = x; nth(j,env) = y; env \<in> list(A)|]
1.69 +       ==> (x\<in>y) <-> sats(A, Member(i,j), env)"
1.71 +
1.72 +lemma conj_iff_sats:
1.73 +      "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
1.74 +       ==> (P & Q) <-> sats(A, And(p,q), env)"
1.76 +
1.77 +lemma disj_iff_sats:
1.78 +      "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
1.79 +       ==> (P | Q) <-> sats(A, Or(p,q), env)"
1.81 +
1.82 +lemma imp_iff_sats:
1.83 +      "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
1.84 +       ==> (P --> Q) <-> sats(A, Implies(p,q), env)"
1.86 +
1.87 +lemma iff_iff_sats:
1.88 +      "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
1.89 +       ==> (P <-> Q) <-> sats(A, Iff(p,q), env)"
1.91 +
1.92 +lemma imp_iff_sats:
1.93 +      "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
1.94 +       ==> (P --> Q) <-> sats(A, Implies(p,q), env)"
1.96 +
1.97 +lemma ball_iff_sats:
1.98 +      "[| !!x. x\<in>A ==> P(x) <-> sats(A, p, Cons(x, env)); env \<in> list(A)|]
1.99 +       ==> (\<forall>x\<in>A. P(x)) <-> sats(A, Forall(p), env)"
1.101 +
1.102 +lemma bex_iff_sats:
1.103 +      "[| !!x. x\<in>A ==> P(x) <-> sats(A, p, Cons(x, env)); env \<in> list(A)|]
1.104 +       ==> (\<exists>x\<in>A. P(x)) <-> sats(A, Exists(p), env)"
1.106 +
1.107
1.108
1.109  (*pretty but unnecessary
1.110 @@ -220,6 +275,9 @@
1.111  lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \<union> arity(q)"
1.113
1.114 +lemma arity_Iff [simp]: "arity(Iff(p,q)) = arity(p) \<union> arity(q)"
1.115 +by (simp add: Iff_def, blast)
1.116 +
1.117  lemma arity_Exists [simp]: "arity(Exists(p)) = nat_case(0, %x. x, arity(p))"
1.119
1.120 @@ -354,11 +412,17 @@
1.121                   X = {x\<in>A. sats(A, p, Cons(x,env))}}"
1.122
1.123  lemma DPowI:
1.124 -  "[|X <= A;  env \<in> list(A);  p \<in> formula;
1.125 -     arity(p) \<le> succ(length(env))|]
1.126 +  "[|env \<in> list(A);  p \<in> formula;  arity(p) \<le> succ(length(env))|]
1.127     ==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"
1.128  by (simp add: DPow_def, blast)
1.129
1.130 +text{*With this rule we can specify @{term p} later.*}
1.131 +lemma DPowI2 [rule_format]:
1.132 +  "[|\<forall>x\<in>A. P(x) <-> sats(A, p, Cons(x,env));
1.133 +     env \<in> list(A);  p \<in> formula;  arity(p) \<le> succ(length(env))|]
1.134 +   ==> {x\<in>A. P(x)} \<in> DPow(A)"
1.135 +by (simp add: DPow_def, blast)
1.136 +
1.137  lemma DPowD:
1.138    "X \<in> DPow(A)
1.139     ==> X <= A &
1.140 @@ -500,6 +564,11 @@
1.141  apply (blast intro!: Transset_Union_family Transset_Un Transset_DPow)
1.142  done
1.143
1.144 +lemma mem_Lset_imp_subset_Lset: "a \<in> Lset(i) ==> a \<subseteq> Lset(i)"
1.145 +apply (insert Transset_Lset)
1.147 +done
1.148 +
1.149  subsubsection{* Monotonicity *}
1.150
1.151  text{*Kunen's VI, 1.6 (b)*}
1.152 @@ -521,6 +590,10 @@
1.153  apply (blast intro: elem_subset_in_DPow dest: LsetD DPowD)
1.154  done
1.155
1.156 +text{*Useful with Reflection to bump up the ordinal*}
1.157 +lemma subset_Lset_ltD: "[|A \<subseteq> Lset(i); i < j|] ==> A \<subseteq> Lset(j)"
1.158 +by (blast dest: ltD [THEN Lset_mono_mem])
1.159 +
1.160  subsubsection{* 0, successor and limit equations fof Lset *}
1.161
1.162  lemma Lset_0 [simp]: "Lset(0) = 0"
1.163 @@ -880,6 +953,17 @@
1.164  apply (simp add: Lset_succ Vset_succ Finite_Vset Finite_DPow_eq_Pow)
1.165  done
1.166
1.167 +text{*Every set of constructible sets is included in some @{term Lset}*}
1.168 +lemma subset_Lset:
1.169 +     "(\<forall>x\<in>A. L(x)) ==> \<exists>i. Ord(i) & A \<subseteq> Lset(i)"
1.170 +by (rule_tac x = "\<Union>x\<in>A. succ(lrank(x))" in exI, force)
1.171 +
1.172 +lemma subset_LsetE:
1.173 +     "[|\<forall>x\<in>A. L(x);
1.174 +        !!i. [|Ord(i); A \<subseteq> Lset(i)|] ==> P|]
1.175 +      ==> P"
1.176 +by (blast dest: subset_Lset)
1.177 +
1.178  subsection{*For L to satisfy the ZF axioms*}
1.179
1.180  theorem Union_in_L: "L(X) ==> L(Union(X))"
```