src/ZF/Constructible/Formula.thy
changeset 13385 31df66ca0780
parent 13339 0f89104dd377
child 13398 1cadd412da48
     1.1 --- a/src/ZF/Constructible/Formula.thy	Tue Jul 16 20:25:21 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Formula.thy	Wed Jul 17 15:48:54 2002 +0200
     1.3 @@ -1013,4 +1013,80 @@
     1.4  theorem LPow_in_L: "L(X) ==> L({y \<in> Pow(X). L(y)})"
     1.5  by (blast intro: L_I dest: L_D LPow_in_Lset)
     1.6  
     1.7 +
     1.8 +subsection{*Eliminating @{term arity} from the Definition of @{term Lset}*}
     1.9 +
    1.10 +
    1.11 +lemma nth_zero_eq_0: "n \<in> nat ==> nth(n,[0]) = 0"
    1.12 +by (induct_tac n, auto)
    1.13 +
    1.14 +lemma sats_app_0_iff [rule_format]:
    1.15 +  "[| p \<in> formula; 0 \<in> A |]
    1.16 +   ==> \<forall>env \<in> list(A). sats(A,p, env@[0]) <-> sats(A,p,env)"
    1.17 +apply (induct_tac p)
    1.18 +apply (simp_all del: app_Cons add: app_Cons [symmetric]
    1.19 +		add: nth_zero_eq_0 nth_append not_lt_iff_le nth_eq_0)
    1.20 +done
    1.21 +
    1.22 +lemma sats_app_zeroes_iff:
    1.23 +  "[| p \<in> formula; 0 \<in> A; env \<in> list(A); n \<in> nat |]
    1.24 +   ==> sats(A,p,env @ repeat(0,n)) <-> sats(A,p,env)"
    1.25 +apply (induct_tac n, simp) 
    1.26 +apply (simp del: repeat.simps
    1.27 +            add: repeat_succ_app sats_app_0_iff app_assoc [symmetric]) 
    1.28 +done
    1.29 +
    1.30 +lemma exists_bigger_env:
    1.31 +  "[| p \<in> formula; 0 \<in> A; env \<in> list(A) |]
    1.32 +   ==> \<exists>env' \<in> list(A). arity(p) \<le> succ(length(env')) & 
    1.33 +              (\<forall>a\<in>A. sats(A,p,Cons(a,env')) <-> sats(A,p,Cons(a,env)))"
    1.34 +apply (rule_tac x="env @ repeat(0,arity(p))" in bexI) 
    1.35 +apply (simp del: app_Cons add: app_Cons [symmetric]
    1.36 +	    add: length_repeat sats_app_zeroes_iff, typecheck)
    1.37 +done
    1.38 +
    1.39 +
    1.40 +text{*A simpler version of @{term DPow}: no arity check!*}
    1.41 +constdefs DPow' :: "i => i"
    1.42 +  "DPow'(A) == {X \<in> Pow(A). 
    1.43 +                \<exists>env \<in> list(A). \<exists>p \<in> formula. 
    1.44 +                    X = {x\<in>A. sats(A, p, Cons(x,env))}}"
    1.45 +
    1.46 +lemma DPow_subset_DPow': "DPow(A) <= DPow'(A)";
    1.47 +by (simp add: DPow_def DPow'_def, blast)
    1.48 +
    1.49 +lemma DPow'_0: "DPow'(0) = {0}"
    1.50 +by (auto simp add: DPow'_def)
    1.51 +
    1.52 +lemma DPow'_subset_DPow: "0 \<in> A ==> DPow'(A) \<subseteq> DPow(A)"
    1.53 +apply (auto simp add: DPow'_def DPow_def) 
    1.54 +apply (frule exists_bigger_env, assumption+, force)  
    1.55 +done
    1.56 +
    1.57 +lemma DPow_eq_DPow': "Transset(A) ==> DPow(A) = DPow'(A)"
    1.58 +apply (drule Transset_0_disj) 
    1.59 +apply (erule disjE) 
    1.60 + apply (simp add: DPow'_0 DPow_0) 
    1.61 +apply (rule equalityI)
    1.62 + apply (rule DPow_subset_DPow') 
    1.63 +apply (erule DPow'_subset_DPow) 
    1.64 +done
    1.65 +
    1.66 +text{*And thus we can relativize @{term Lset} without bothering with
    1.67 +      @{term arity} and @{term length}*}
    1.68 +lemma Lset_eq_transrec_DPow': "Lset(i) = transrec(i, %x f. \<Union>y\<in>x. DPow'(f`y))"
    1.69 +apply (rule_tac a=i in eps_induct)
    1.70 +apply (subst Lset)
    1.71 +apply (subst transrec)
    1.72 +apply (simp only: DPow_eq_DPow' [OF Transset_Lset], simp) 
    1.73 +done
    1.74 +
    1.75 +text{*With this rule we can specify @{term p} later and don't worry about
    1.76 +      arities at all!*}
    1.77 +lemma DPow_LsetI [rule_format]:
    1.78 +  "[|\<forall>x\<in>Lset(i). P(x) <-> sats(Lset(i), p, Cons(x,env));
    1.79 +     env \<in> list(Lset(i));  p \<in> formula|]
    1.80 +   ==> {x\<in>Lset(i). P(x)} \<in> DPow(Lset(i))"
    1.81 +by (simp add: DPow_eq_DPow' [OF Transset_Lset] DPow'_def, blast) 
    1.82 +
    1.83  end