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.28  by (simp add: Implies_def) 
    1.29  
    1.30 +lemma Iff_type [TC]:
    1.31 +     "[| p \<in> formula; q \<in> formula |] ==> Iff(p,q) \<in> formula"
    1.32 +by (simp add: Iff_def) 
    1.33 +
    1.34  lemma Exists_type [TC]: "p \<in> formula ==> Exists(p) \<in> formula"
    1.35  by (simp add: Exists_def) 
    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.62  by (simp add: Exists_def)
    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.70 +by (simp add: satisfies.simps)
    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.75 +by (simp add: sats_And_iff)
    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.80 +by (simp add: sats_Or_iff)
    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.85 +by (simp add: sats_Forall_iff) 
    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.90 +by (simp add: sats_Forall_iff) 
    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.95 +by (simp add: sats_Forall_iff) 
    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.100 +by (simp add: sats_Forall_iff) 
   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.105 +by (simp add: sats_Exists_iff) 
   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.112  by (simp add: Implies_def) 
   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.118  by (simp add: Exists_def) 
   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.146 +apply (simp add: Transset_def) 
   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))"