src/ZF/Constructible/Formula.thy
changeset 13647 7f6f0ffc45c3
parent 13634 99a593b49b04
child 13651 ac80e101306a
     1.1 --- a/src/ZF/Constructible/Formula.thy	Mon Oct 14 10:44:32 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Formula.thy	Mon Oct 14 11:32:00 2002 +0200
     1.3 @@ -188,6 +188,63 @@
     1.4          disj_iff_sats imp_iff_sats iff_iff_sats imp_iff_sats ball_iff_sats
     1.5          bex_iff_sats
     1.6  
     1.7 +
     1.8 +subsection{*Arity of a Formula: Maximum Free de Bruijn Index*}
     1.9 +
    1.10 +consts   arity :: "i=>i"
    1.11 +primrec
    1.12 +  "arity(Member(x,y)) = succ(x) \<union> succ(y)"
    1.13 +
    1.14 +  "arity(Equal(x,y)) = succ(x) \<union> succ(y)"
    1.15 +
    1.16 +  "arity(Nand(p,q)) = arity(p) \<union> arity(q)"
    1.17 +
    1.18 +  "arity(Forall(p)) = Arith.pred(arity(p))"
    1.19 +
    1.20 +
    1.21 +lemma arity_type [TC]: "p \<in> formula ==> arity(p) \<in> nat"
    1.22 +by (induct_tac p, simp_all) 
    1.23 +
    1.24 +lemma arity_Neg [simp]: "arity(Neg(p)) = arity(p)"
    1.25 +by (simp add: Neg_def) 
    1.26 +
    1.27 +lemma arity_And [simp]: "arity(And(p,q)) = arity(p) \<union> arity(q)"
    1.28 +by (simp add: And_def) 
    1.29 +
    1.30 +lemma arity_Or [simp]: "arity(Or(p,q)) = arity(p) \<union> arity(q)"
    1.31 +by (simp add: Or_def) 
    1.32 +
    1.33 +lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \<union> arity(q)"
    1.34 +by (simp add: Implies_def) 
    1.35 +
    1.36 +lemma arity_Iff [simp]: "arity(Iff(p,q)) = arity(p) \<union> arity(q)"
    1.37 +by (simp add: Iff_def, blast)
    1.38 +
    1.39 +lemma arity_Exists [simp]: "arity(Exists(p)) = Arith.pred(arity(p))"
    1.40 +by (simp add: Exists_def) 
    1.41 +
    1.42 +
    1.43 +lemma arity_sats_iff [rule_format]:
    1.44 +  "[| p \<in> formula; extra \<in> list(A) |]
    1.45 +   ==> \<forall>env \<in> list(A). 
    1.46 +           arity(p) \<le> length(env) --> 
    1.47 +           sats(A, p, env @ extra) <-> sats(A, p, env)"
    1.48 +apply (induct_tac p)
    1.49 +apply (simp_all add: Arith.pred_def nth_append Un_least_lt_iff nat_imp_quasinat
    1.50 +                split: split_nat_case, auto) 
    1.51 +done
    1.52 +
    1.53 +lemma arity_sats1_iff:
    1.54 +  "[| arity(p) \<le> succ(length(env)); p \<in> formula; x \<in> A; env \<in> list(A); 
    1.55 +      extra \<in> list(A) |]
    1.56 +   ==> sats(A, p, Cons(x, env @ extra)) <-> sats(A, p, Cons(x, env))"
    1.57 +apply (insert arity_sats_iff [of p extra A "Cons(x,env)"])
    1.58 +apply simp 
    1.59 +done
    1.60 +
    1.61 +
    1.62 +subsection{*Renaming Some de Bruijn Variables*}
    1.63 +
    1.64  constdefs incr_var :: "[i,i]=>i"
    1.65      "incr_var(x,lev) == if x<lev then x else succ(x)"
    1.66  
    1.67 @@ -214,22 +271,15 @@
    1.68        (\<lambda>lev \<in> nat. Forall (incr_bv(p) ` succ(lev)))"
    1.69  
    1.70  
    1.71 -constdefs incr_boundvars :: "i => i"
    1.72 -    "incr_boundvars(p) == incr_bv(p)`0"
    1.73 -
    1.74 -
    1.75  lemma [TC]: "x \<in> nat ==> incr_var(x,lev) \<in> nat"
    1.76  by (simp add: incr_var_def) 
    1.77  
    1.78  lemma incr_bv_type [TC]: "p \<in> formula ==> incr_bv(p) \<in> nat -> formula"
    1.79  by (induct_tac p, simp_all) 
    1.80  
    1.81 -lemma incr_boundvars_type [TC]: "p \<in> formula ==> incr_boundvars(p) \<in> formula"
    1.82 -by (simp add: incr_boundvars_def) 
    1.83 -
    1.84 -(*Obviously DPow is closed under complements and finite intersections and
    1.85 -unions.  Needs an inductive lemma to allow two lists of parameters to 
    1.86 -be combined.*)
    1.87 +text{*Obviously, @{term DPow} is closed under complements and finite
    1.88 +intersections and unions.  Needs an inductive lemma to allow two lists of
    1.89 +parameters to be combined.*}
    1.90  
    1.91  lemma sats_incr_bv_iff [rule_format]:
    1.92    "[| p \<in> formula; env \<in> list(A); x \<in> A |]
    1.93 @@ -241,76 +291,6 @@
    1.94  apply (auto simp add: diff_succ not_lt_iff_le)
    1.95  done
    1.96  
    1.97 -(*UNUSED*)
    1.98 -lemma sats_incr_boundvars_iff:
    1.99 -  "[| p \<in> formula; env \<in> list(A); x \<in> A |]
   1.100 -   ==> sats(A, incr_boundvars(p), Cons(x,env)) <-> sats(A, p, env)"
   1.101 -apply (insert sats_incr_bv_iff [of p env A x Nil])
   1.102 -apply (simp add: incr_boundvars_def) 
   1.103 -done
   1.104 -
   1.105 -(*UNUSED
   1.106 -lemma formula_add_params [rule_format]:
   1.107 -  "[| p \<in> formula; n \<in> nat |]
   1.108 -   ==> \<forall>bvs \<in> list(A). \<forall>env \<in> list(A). 
   1.109 -         length(bvs) = n --> 
   1.110 -         sats(A, iterates(incr_boundvars,n,p), bvs@env) <-> sats(A, p, env)"
   1.111 -apply (induct_tac n, simp, clarify) 
   1.112 -apply (erule list.cases)
   1.113 -apply (auto simp add: sats_incr_boundvars_iff)  
   1.114 -done
   1.115 -*)
   1.116 -
   1.117 -consts   arity :: "i=>i"
   1.118 -primrec
   1.119 -  "arity(Member(x,y)) = succ(x) \<union> succ(y)"
   1.120 -
   1.121 -  "arity(Equal(x,y)) = succ(x) \<union> succ(y)"
   1.122 -
   1.123 -  "arity(Nand(p,q)) = arity(p) \<union> arity(q)"
   1.124 -
   1.125 -  "arity(Forall(p)) = nat_case(0, %x. x, arity(p))"
   1.126 -
   1.127 -
   1.128 -lemma arity_type [TC]: "p \<in> formula ==> arity(p) \<in> nat"
   1.129 -by (induct_tac p, simp_all) 
   1.130 -
   1.131 -lemma arity_Neg [simp]: "arity(Neg(p)) = arity(p)"
   1.132 -by (simp add: Neg_def) 
   1.133 -
   1.134 -lemma arity_And [simp]: "arity(And(p,q)) = arity(p) \<union> arity(q)"
   1.135 -by (simp add: And_def) 
   1.136 -
   1.137 -lemma arity_Or [simp]: "arity(Or(p,q)) = arity(p) \<union> arity(q)"
   1.138 -by (simp add: Or_def) 
   1.139 -
   1.140 -lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \<union> arity(q)"
   1.141 -by (simp add: Implies_def) 
   1.142 -
   1.143 -lemma arity_Iff [simp]: "arity(Iff(p,q)) = arity(p) \<union> arity(q)"
   1.144 -by (simp add: Iff_def, blast)
   1.145 -
   1.146 -lemma arity_Exists [simp]: "arity(Exists(p)) = nat_case(0, %x. x, arity(p))"
   1.147 -by (simp add: Exists_def) 
   1.148 -
   1.149 -
   1.150 -lemma arity_sats_iff [rule_format]:
   1.151 -  "[| p \<in> formula; extra \<in> list(A) |]
   1.152 -   ==> \<forall>env \<in> list(A). 
   1.153 -           arity(p) \<le> length(env) --> 
   1.154 -           sats(A, p, env @ extra) <-> sats(A, p, env)"
   1.155 -apply (induct_tac p)
   1.156 -apply (simp_all add: nth_append Un_least_lt_iff arity_type nat_imp_quasinat
   1.157 -                split: split_nat_case, auto) 
   1.158 -done
   1.159 -
   1.160 -lemma arity_sats1_iff:
   1.161 -  "[| arity(p) \<le> succ(length(env)); p \<in> formula; x \<in> A; env \<in> list(A); 
   1.162 -    extra \<in> list(A) |]
   1.163 -   ==> sats(A, p, Cons(x, env @ extra)) <-> sats(A, p, Cons(x, env))"
   1.164 -apply (insert arity_sats_iff [of p extra A "Cons(x,env)"])
   1.165 -apply simp 
   1.166 -done
   1.167  
   1.168  (*the following two lemmas prevent huge case splits in arity_incr_bv_lemma*)
   1.169  lemma incr_var_lemma:
   1.170 @@ -336,7 +316,7 @@
   1.171  apply (induct_tac p) 
   1.172  apply (simp_all add: imp_disj not_lt_iff_le Un_least_lt_iff lt_Un_iff le_Un_iff
   1.173                       succ_Un_distrib [symmetric] incr_var_lt incr_var_le
   1.174 -                     Un_commute incr_var_lemma arity_type nat_imp_quasinat
   1.175 +                     Un_commute incr_var_lemma Arith.pred_def nat_imp_quasinat
   1.176              split: split_nat_case) 
   1.177   txt{*the Forall case reduces to linear arithmetic*}
   1.178   prefer 2
   1.179 @@ -350,24 +330,8 @@
   1.180  apply (simp add: Un_commute)
   1.181  done
   1.182  
   1.183 -lemma arity_incr_boundvars_eq:
   1.184 -  "p \<in> formula
   1.185 -   ==> arity(incr_boundvars(p)) =
   1.186 -        (if 0 < arity(p) then succ(arity(p)) else arity(p))"
   1.187 -apply (insert arity_incr_bv_lemma [of p 0])
   1.188 -apply (simp add: incr_boundvars_def) 
   1.189 -done
   1.190  
   1.191 -lemma arity_iterates_incr_boundvars_eq:
   1.192 -  "[| p \<in> formula; n \<in> nat |]
   1.193 -   ==> arity(incr_boundvars^n(p)) =
   1.194 -         (if 0 < arity(p) then n #+ arity(p) else arity(p))"
   1.195 -apply (induct_tac n) 
   1.196 -apply (simp_all add: arity_incr_boundvars_eq not_lt_iff_le) 
   1.197 -done
   1.198 -
   1.199 -
   1.200 -subsection{*Renaming all but the first bound variable*}
   1.201 +subsection{*Renaming all but the First de Bruijn Variable*}
   1.202  
   1.203  constdefs incr_bv1 :: "i => i"
   1.204      "incr_bv1(p) == incr_bv(p)`1"
   1.205 @@ -377,7 +341,7 @@
   1.206  by (simp add: incr_bv1_def) 
   1.207  
   1.208  (*For renaming all but the bound variable at level 0*)
   1.209 -lemma sats_incr_bv1_iff [rule_format]:
   1.210 +lemma sats_incr_bv1_iff:
   1.211    "[| p \<in> formula; env \<in> list(A); x \<in> A; y \<in> A |]
   1.212     ==> sats(A, incr_bv1(p), Cons(x, Cons(y, env))) <-> 
   1.213         sats(A, p, Cons(x,env))"
   1.214 @@ -416,7 +380,10 @@
   1.215  done
   1.216  
   1.217  
   1.218 -(*Definable powerset operation: Kunen's definition 1.1, page 165.*)
   1.219 +
   1.220 +subsection{*Definable Powerset*}
   1.221 +
   1.222 +text{*The definable powerset operation: Kunen's definition VI 1.1, page 165.*}
   1.223  constdefs DPow :: "i => i"
   1.224    "DPow(A) == {X \<in> Pow(A). 
   1.225                 \<exists>env \<in> list(A). \<exists>p \<in> formula. 
   1.226 @@ -445,7 +412,7 @@
   1.227  
   1.228  lemmas DPow_imp_subset = DPowD [THEN conjunct1]
   1.229  
   1.230 -(*Lemma 1.2*)
   1.231 +(*Kunen's Lemma VI 1.2*)
   1.232  lemma "[| p \<in> formula; env \<in> list(A); arity(p) \<le> succ(length(env)) |] 
   1.233         ==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"
   1.234  by (blast intro: DPowI)